diff --git a/lib/ast.ml b/lib/ast.ml index c78bb1a65e21e470ad1ac723d1ab4a091b43b0e3..0f6eea81cd5e33551122fcc5a92b74638f1ceae3 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -25,7 +25,7 @@ type 'a set = type expr = | None - | Bool of bool + | Bool of bool | Cst of int | Cstf of float | BinOp of expr * binop * expr @@ -37,7 +37,7 @@ type expr = | App of expr * expr | Affectation of string * expr | Set of expr set - | Point of string * string + | Point of string * string *int (* int : line to raise error*) | PatternMatching of expr * (expr * expr)list | Cons of expr *expr @@ -104,14 +104,14 @@ type color = | Orange -(* type light: List of colors +(* type light: List of colors * line to raise error (int) Intern -> Light seen by the robot itself Extern -> Light seen by robots other than himself All -> Light seen by all robots including themselves *) type light = - | Intern of string list - | Extern of string list - | All of string list + | Intern of string list * int + | Extern of string list *int + | All of string list *int (* type opacity: @@ -225,7 +225,7 @@ let rec string_of_expression (e : expr) : string = | Let (v,e1,e2) -> "Let " ^ v ^ " = " ^ string_of_expression e1 ^ " in \n(" ^string_of_expression e2 ^")" | Fun (s,e) -> "Function " ^ s ^ " = (" ^ string_of_expression e ^")" | App (f,arg) -> "("^string_of_expression f ^" "^ string_of_expression arg^")" - | Point (k,v) -> "value " ^ v^ " of "^ k ^"" + | Point (k,v,_) -> "value " ^ v^ " of "^ k ^"" | PatternMatching (m,l) -> "match "^string_of_expression m^" with \n | "^ String.concat "\n | "(List.map (fun e -> match e with | e1,e2 -> string_of_expression e1 ^" => "^string_of_expression e2 ) l)^ "\nend" @@ -567,7 +567,7 @@ let check_light d : bool = let rec check flist = ( fun x -> match x with | [] -> true - | Public (_,Light(Intern _))::_ | Private (_, Light(Extern _))::_ -> raise(Failure("Error light in wrong field")) + | Public (_,Light(Intern (_ ,line)))::_ | Private (_, Light(Extern (_ ,line)))::_ -> raise(Failure("Error line "^string_of_int line^" light in wrong field")) | _::t-> check t ) flist in diff --git a/lib/gencoq.ml b/lib/gencoq.ml index ea273af82e45eff480f67b150579dbd59b476b8a..bca01f9a423ff4f4a0a086809b5583fd0bf98870 100644 --- a/lib/gencoq.ml +++ b/lib/gencoq.ml @@ -107,11 +107,11 @@ let rec expr_to_coq (r : expr) : Formula.t = | Fun (s,e) -> Fun(Some s, expr_to_coq e) | App (f,arg) -> App(expr_to_coq f, [expr_to_coq arg]) | Set s -> Set (set_to_coq s) - | Point (m,f) -> let c = StringMap.find_opt m Module.correspondance in + | Point (m,f,l) -> let c = StringMap.find_opt m Module.correspondance in (match c with - |None -> raise(Failure("Problem: "^m^" unknow")) + |None -> raise(Failure("Problem line "^string_of_int l^": "^m^" unknow")) |Some x -> (match StringMap.find_opt f x with - | None -> raise(Failure("Problem "^m^"."^f^" unknow")) + | None -> raise(Failure("Problem line "^string_of_int l^": "^m^"."^f^" unknow")) | Some x' -> x') ) | _ -> Raw("Not Implemented") @@ -216,7 +216,7 @@ let instance_info (fl:field list) : stmt list = let l = List.assoc_opt "Light" (List.map (fun x -> match x with | Private p -> p | Public p -> p) fl) in (match l with - |Some(Light (x)) -> let l' = match x with | Intern p -> p |Extern p -> p | All p -> p in + |Some(Light (x)) -> let l' = match x with | Intern (p,_) -> p |Extern (p,_) -> p | All (p,_) -> p in let l'' = String.concat " | " l' in RawCoq(["Inductive light:= "^l''^"."]) ::Instance("light_Setoid",Cst "Setoid light",Cst "eq_setoid light") diff --git a/lib/parser.mly b/lib/parser.mly index 294cdc485c907643a2f83acceefe32d254547418..a271f5ac69aaae352f2c098a0b3dbd4b3891702a 100644 --- a/lib/parser.mly +++ b/lib/parser.mly @@ -166,11 +166,11 @@ value : lights: /*Internal light -> visible only to the robot*/ - | INTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Intern i)} + | INTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Intern (i,$startpos.Lexing.pos_lnum))} /*External light -> visible only to other robots*/ - | EXTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Extern i)} + | EXTERNE LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(Extern (i,$startpos.Lexing.pos_lnum))} /*Light visible to all*/ - | FULL LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(All i)} + | FULL LIGHT BRACKETOPEN i = separated_list(SEMICOLON,KEYWORD) BRACKETCLOSE {Light(All (i,$startpos.Lexing.pos_lnum))} %inline range : @@ -261,7 +261,7 @@ argument : id : | VARIABLE {Var $1} - | x = KEYWORD POINT e = VARIABLE {Point(x,e)} + | x = KEYWORD POINT e = VARIABLE {Point(x,e,$startpos.Lexing.pos_lnum)} set : | e = expression COMMA s = set {Some(s,e)}