Skip to content
Snippets Groups Projects
Commit a2c8a0ce authored by Kylian Fontaine's avatar Kylian Fontaine
Browse files

da hors lemmes, declaration des forall

parent 188cf7d2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Readme.md
+ 1
− 1
View file @ a2c8a0ce
...@@ -37,7 +37,7 @@ Rigidity := Flexible delta ...@@ -37,7 +37,7 @@ Rigidity := Flexible delta
``` ```
Couleur : Red; Blue; Yellow; Green; Purple; Orange Couleur : Red; Blue; Yellow; Green; Purple; Orange
- Robot := Permet de definir des champs privée et publique pour le robot, il est necessaire de lister les éléments privée puis les éléments public - Robot := Permet de definir des champs privés et publiques pour le robot, il est necessaire de lister les éléments privés puis les éléments publiques
- Private : Champ 1; Champ 2; ... - Private : Champ 1; Champ 2; ...
- Public : Champ 3; Champ 4; ... - Public : Champ 3; Champ 4; ...
......
bin/main.ml
+ 5
− 10
View file @ a2c8a0ce
open Dsl open Dsl
let repo = "./sourcegenerate";; (*let repo = "./sourcegenerate";;
let files =Array.to_list (Sys.readdir repo);; let files =Array.to_list (Sys.readdir repo);;
print_endline(String.concat "; " files);; print_endline(String.concat "; " files);;
*)
let gen (x : string) = let gen (x : string) =
let path = repo ^"/"^ x in Gencoq.generate_coq (Interface.parse_description x) (Filename.basename x);;
Gencoq.generate (Interface.parse_description path) x;;
gen Sys.argv.(1);;
List.map gen files;;
(*
if (Ast.check_sensors_desc desc) && (Ast.check_activelyup desc)then
print_endline (Ast.string_of_description desc);;
*)
\ No newline at end of file
lib/ast.ml
+ 119
− 43
View file @ a2c8a0ce
open Graphtest
(*ROBOGRAM*) (*ROBOGRAM*)
type binop = type binop =
...@@ -205,14 +205,6 @@ type information = ...@@ -205,14 +205,6 @@ type information =
| Roles of (int * string) list | Roles of (int * string) list
| Share of share | Share of share
type measure = Measure of int * G.t
(* Une description c'est 1: description de l'environnement et des capacites des robot
2: robogram *)
type description = Description of (information list) * (expr list) * measure
(*FONCTION SUR LES SETS*) (*FONCTION SUR LES SETS*)
(** [length s] retourne la longueur du set [s] (** [length s] retourne la longueur du set [s]
@param [s] 'a set dont on veut la longueur @param [s] 'a set dont on veut la longueur
...@@ -222,7 +214,7 @@ let rec length_set (s:'a set): int = ...@@ -222,7 +214,7 @@ let rec length_set (s:'a set): int =
| Vide -> 0 | Vide -> 0
| Some (s,_) -> 1 + (length_set s) | Some (s,_) -> 1 + (length_set s)
(*[push s e] ajoute un element e au set s (**[push s e] ajoute un element e au set s
@param s de type 'a set @param s de type 'a set
@param e de type 'a @param e de type 'a
@return un set correspondant au set s avec l'ajout de e *) @return un set correspondant au set s avec l'ajout de e *)
...@@ -273,7 +265,7 @@ let rec string_of_expression (e : expr) : string = ...@@ -273,7 +265,7 @@ let rec string_of_expression (e : expr) : string =
| Set s -> string_of_set s string_of_expression | Set s -> string_of_set s string_of_expression
| Let (v,e1,e2) -> "Déclaration de la variable " ^ v ^ " avec definition : " ^ string_of_expression e1 ^ " dans \n(" ^string_of_expression e2 ^")" | Let (v,e1,e2) -> "Déclaration de la variable " ^ v ^ " avec definition : " ^ string_of_expression e1 ^ " dans \n(" ^string_of_expression e2 ^")"
| Fun (s,e) -> "Fonction qui prend en parametre " ^ s ^ " et retourne (" ^ string_of_expression e ^")" | Fun (s,e) -> "Fonction qui prend en parametre " ^ s ^ " et retourne (" ^ string_of_expression e ^")"
| App (f,arg) -> "("^ string_of_expression f ^") appliqué a (" ^ string_of_expression arg ^")" | App (f,arg) -> "("^string_of_expression f ^" "^ string_of_expression arg^")"
| Point (k,v) -> "Valeur du champ " ^ v^ " de "^ k ^"" | Point (k,v) -> "Valeur du champ " ^ v^ " de "^ k ^""
| LengthSet s -> (match s with | LengthSet s -> (match s with
| Set s' -> "Taille de "^string_of_expression s ^ " : " ^ string_of_int (length_set s') | Set s' -> "Taille de "^string_of_expression s ^ " : " ^ string_of_int (length_set s')
...@@ -288,7 +280,15 @@ let rec string_of_expression (e : expr) : string = ...@@ -288,7 +280,15 @@ let rec string_of_expression (e : expr) : string =
l)^ "\nend" l)^ "\nend"
| Cons (head,tail) -> string_of_expression head ^ " :: " ^ string_of_expression tail | Cons (head,tail) -> string_of_expression head ^ " :: " ^ string_of_expression tail
(**[get_param f] retourne la liste des paramtre d'une application de fonction,
si un des parametre et aussi une application de fonction, cela retournera les parametre de la deuxieme application
@param f [expr]
@return [expr list]*)
let rec get_param (f:expr) : expr list=
match f with
| App(f',Var v)-> Var v:: get_param f'
| App(f',v)-> get_param v @ get_param f'
| _-> []
let string_of_synchro (s:synchro) : string = let string_of_synchro (s:synchro) : string =
match s with match s with
...@@ -342,7 +342,7 @@ let rec string_of_value (v : value) : string = ...@@ -342,7 +342,7 @@ let rec string_of_value (v : value) : string =
| Intern c -> "Lumiere interne avec couleur :" ^ String.concat ", " (List.map string_of_color c) | Intern c -> "Lumiere interne avec couleur :" ^ String.concat ", " (List.map string_of_color c)
| Extern c ->"Lumiere externe avec couleur :" ^ String.concat ", " (List.map string_of_color c) | Extern c ->"Lumiere externe avec couleur :" ^ String.concat ", " (List.map string_of_color c)
| All c ->"Lumiere visible par tous avec couleur :" ^ String.concat ", " (List.map string_of_color c) | All c ->"Lumiere visible par tous avec couleur :" ^ String.concat ", " (List.map string_of_color c)
) )
let string_of_field (f : field) : string = let string_of_field (f : field) : string =
match f with match f with
| Private (s,v)-> "Private: "^s^"->"^ string_of_value v | Private (s,v)-> "Private: "^s^"->"^ string_of_value v
...@@ -360,30 +360,8 @@ let string_of_rigidity (r: rigidity) : string = ...@@ -360,30 +360,8 @@ let string_of_rigidity (r: rigidity) : string =
| Rigide -> "Rigide" | Rigide -> "Rigide"
| Flexible _ -> "Flexible" | Flexible _ -> "Flexible"
let rec string_of_description (desc:description) : string =
match desc with
| Description (infos,robogram,_) ->
"Description environnement:\n" ^String.concat "\n" (List.map string_of_information infos)
^"\nRobogram : \n " ^ String.concat "\n" (List.map string_of_expression robogram)
and string_of_information (info: information) : string =
match info with
| Sync s -> "Sync: " ^ (string_of_synchro s)
| Rigidity r ->(match r with
| Rigide -> "Rigidity: Rigide"
| Flexible d -> "Rigidity: Flexible d'une distance delta = " ^ string_of_expression d)
| Space e -> "Espace: " ^ (string_of_espace e)
| Byzantines b -> string_of_byzantine b
| Sensors s -> "Sensors: [" ^ String.concat "; " (List.map string_of_sensor s) ^ "] "
| Robot r -> "Robot : ["^ String.concat "; " (List.map string_of_field r) ^ "]"
| Roles r -> "Roles :" ^ String.concat "\n " (List.map string_of_role r)
| ActivelyUpdate a -> "Champ qui sont mise a jour par le robogram: " ^ String.concat ", " (List.map string_of_valretr a )
| Share s ->"Share : " ^ (match s with
|Fullcompass -> "Fullcompass"
|Chirality -> "Chirality"
|DirectionShare -> "Direction"
|OneAxisOrientation ->"1-axis orientation")
(** [info_sync i] verifie qu'une information est une information sur la synchronisation (** [info_sync i] verifie qu'une information est une information sur la synchronisation
@param i information @param i information
@return bool *) @return bool *)
...@@ -400,6 +378,101 @@ let info_space (i : information):bool = ...@@ -400,6 +378,101 @@ let info_space (i : information):bool =
| Space _ -> true | Space _ -> true
| _ -> false | _ -> false
(*GRAPH*)
module Node = struct
type t = expr
let compare = compare
let hash = Hashtbl.hash
let equal = (=)
end
module Edge = struct
type t = string
let compare = compare
let default = ""
end
module G = Graph.Imperative.Digraph.ConcreteLabeled(Node)(Edge)
type edge =
| Nolab of (expr * expr)
let graph_from_edges (el : edge list)=
let g = G.create () in
let nolab = fun (x, y) ->
let vx = G.V.create x in
let vy = G.V.create y in
G.add_edge g vx vy
in
let rec add_edge (el : edge list) =
match el with
| [] -> ()
| (Nolab h)::t -> nolab h ; add_edge t
in add_edge el;
g
let png_from_graph g =
let graph = G.fold_vertex (fun v acc ->
let succs = List.map string_of_expression (G.succ g v)in
let v' = string_of_expression v in
let edges = List.fold_left (fun acc s ->
acc ^ "\"" ^ v' ^ "\" -> \"" ^ s ^ "\";\n") "" succs in
acc ^ "\"" ^ v' ^ "\";\n" ^ edges
) g "" in
let dot = "digraph G {\nrankdir=LR;\n" ^ graph ^ "}" in
let oc = open_out "graph.dot" in
Printf.fprintf oc "%s\n" dot;
close_out oc;
ignore (Sys.command "dot -Tpng graph.dot -o graph.png")
(*/GRAPH*)
type measure = Measure of int * G.t
(* Une description c'est 1: description de l'environnement et des capacites des robot
2: robogram *)
type description = Description of (information list) * (expr list) * measure
let rec string_of_description (desc:description) : string =
match desc with
| Description (infos,robogram,_) ->
"Description environnement:\n" ^String.concat "\n" (List.map string_of_information infos)
^"\nRobogram : \n " ^ String.concat "\n" (List.map string_of_expression robogram)
and string_of_information (info: information) : string =
match info with
| Sync s -> "Sync: " ^ (string_of_synchro s)
| Rigidity r ->(match r with
| Rigide -> "Rigidity: Rigide"
| Flexible d -> "Rigidity: Flexible d'une distance delta = " ^ string_of_expression d)
| Space e -> "Espace: " ^ (string_of_espace e)
| Byzantines b -> string_of_byzantine b
| Sensors s -> "Sensors: [" ^ String.concat "; " (List.map string_of_sensor s) ^ "] "
| Robot r -> "Robot : ["^ String.concat "; " (List.map string_of_field r) ^ "]"
| Roles r -> "Roles :" ^ String.concat "\n " (List.map string_of_role r)
| ActivelyUpdate a -> "Champ qui sont mise a jour par le robogram: " ^ String.concat ", " (List.map string_of_valretr a )
| Share s ->"Share : " ^ (match s with
|Fullcompass -> "Fullcompass"
|Chirality -> "Chirality"
|DirectionShare -> "Direction"
|OneAxisOrientation ->"1-axis orientation")
(** [check_description d] verifie que la description [d] possède bien les informations minimales (** [check_description d] verifie que la description [d] possède bien les informations minimales
attendu pour une description et que chaque type d'information soit unique attendu pour une description et que chaque type d'information soit unique
...@@ -465,7 +538,7 @@ let check_sensor (s: sensor) (r:field list):bool = ...@@ -465,7 +538,7 @@ let check_sensor (s: sensor) (r:field list):bool =
let check_sensors_desc (d:description) :bool = let check_sensors_desc (d:description) :bool =
let res= List.find_opt (fun x -> not (check_sensor x (get_robot d))) (get_sensors d) in let res= List.find_opt (fun x -> not (check_sensor x (get_robot d))) (get_sensors d) in
match res with match res with
| Some x -> print_endline("Error : " ^(match x with |Custom (x',_)-> x' | _->"")^" is not declared public in robot"); false | Some x -> raise(Failure("Error : " ^(match x with |Custom (x',_)-> x' | _->"")^" is not declared public in robot"))
| _-> true | _-> true
(**[check_activelyup d] verifie que les champs renseignés dans activelyupdate soient déclarés dans robot (**[check_activelyup d] verifie que les champs renseignés dans activelyupdate soient déclarés dans robot
...@@ -474,9 +547,10 @@ let check_sensors_desc (d:description) :bool = ...@@ -474,9 +547,10 @@ let check_sensors_desc (d:description) :bool =
let check_activelyup (d:description) :bool = let check_activelyup (d:description) :bool =
let field_to_pair f = List.map(fun x -> match x with Public x -> x | Private x -> x) f in let field_to_pair f = List.map(fun x -> match x with Public x -> x | Private x -> x) f in
let aux s l = List.exists (fun (x,_) -> x = s) (field_to_pair l) in let aux s l = List.exists (fun (x,_) -> x = s) (field_to_pair l) in
let res = List.find_opt (fun x -> not (aux x (get_robot d))) (get_activelyup d) in let fields_to_check f = List.filter (fun x -> (x <> "Location") && (x <> "Direction")) f ;in
let res = List.find_opt (fun x -> not (aux x (get_robot d))) (fields_to_check(get_activelyup d)) in
match res with match res with
| Some x -> print_endline("Error : " ^x^" x is not declared in robot"); false | Some x -> raise(Failure("Error : " ^x^" is not declared in robot"))
| _-> true | _-> true
...@@ -488,9 +562,11 @@ let check_light d : bool = ...@@ -488,9 +562,11 @@ let check_light d : bool =
let rec check flist = ( let rec check flist = (
fun x -> match x with fun x -> match x with
| [] -> true | [] -> true
| Public (_,Light(Intern _))::_ -> false | Public (_,Light(Intern _))::_ -> raise(Failure("Error light in wrong field"))
| Private (_, Light(Extern _))::_ -> false | Private (_, Light(Extern _))::_ -> raise(Failure("Error light in wrong field"))
| _::t-> check t | _::t-> check t
) flist ) flist
in in
check (get_robot d) check (get_robot d)
\ No newline at end of file
lib/gencoq.ml
+ 46
− 36
View file @ a2c8a0ce
open Ast open Ast
(*open Formula*)
open Coq open Coq
let geometry =[("isobarycenter",Formula.Raw("isobarycenter")); let geometry =[("isobarycenter",Formula.Raw("isobarycenter"));
("barycenter",Formula.Raw("barycenter"));
("on_SEC"),Formula.Raw("on_SEC")] ("on_SEC"),Formula.Raw("on_SEC")]
let observation =[("elements", Formula.Raw("(elements s)")); let observation =[("elements", Formula.Raw("(elements s)"));
("support"), Formula.Raw("support s")] ("support"), Formula.Raw("support s")]
...@@ -113,8 +113,6 @@ let rec expr_to_coq (r : expr) : Formula.t = ...@@ -113,8 +113,6 @@ let rec expr_to_coq (r : expr) : Formula.t =
| Diff -> Infix(expr_to_coq x,"!=",expr_to_coq y) | Diff -> Infix(expr_to_coq x,"!=",expr_to_coq y)
| Impli -> Infix(expr_to_coq x, "->", expr_to_coq y) | Impli -> Infix(expr_to_coq x, "->", expr_to_coq y)
| Equiv -> Infix(expr_to_coq x,"<->",expr_to_coq y) | Equiv -> Infix(expr_to_coq x,"<->",expr_to_coq y)
) )
| Cons (e1,e2) -> App(Raw("cons"), ([expr_to_coq e1;expr_to_coq e2])) | Cons (e1,e2) -> App(Raw("cons"), ([expr_to_coq e1;expr_to_coq e2]))
| Fun (s,e) -> Fun(Some s, expr_to_coq e) | Fun (s,e) -> Fun(Some s, expr_to_coq e)
...@@ -185,17 +183,17 @@ let instance_space (s: space) (d : information list): stmt list = ...@@ -185,17 +183,17 @@ let instance_space (s: space) (d : information list): stmt list =
*) *)
let instance_updfunc_rigid (valret : string) (d: information list):stmt list = let instance_updfunc_rigid (valret : string) (d: information list):stmt list =
if not(get_space d = "Ring") then if not(get_space d = "Ring") then
Instance("UpdateFunc",Raw("update_function ("^valret^") (Similarity.similarity "^valret^") unit"),Raw("{update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }")) Instance("UpdFun",Raw("update_function ("^valret^") (Similarity.similarity "^valret^") unit"),Raw("{update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }"))
::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::[] ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::[]
else else
Instance("FrameChoice",App(Cst "frame_choice",[Raw("(Z * bool)")]),Raw(" {frame_choice_bijection := Instance("FC",App(Cst "frame_choice",[Raw("(Z * bool)")]),Raw(" {frame_choice_bijection :=
fun nb => if snd nb then Ring.sym (fst nb) else Ring.trans (fst nb); fun nb => if snd nb then Ring.sym (fst nb) else Ring.trans (fst nb);
frame_choice_Setoid := eq_setoid _ }")):: frame_choice_Setoid := eq_setoid _ }"))::
Instance("UpdateFunc",Raw("update_function direction (Z * bool) unit"),Raw("{ Instance("UpdFun",Raw("update_function direction (Z * bool) unit"),Raw("{
update := fun config g _ dir _ => move_along (config (Good g)) dir; update := fun config g _ dir _ => move_along (config (Good g)) dir;
update_compat := ltac:(repeat intro; subst; now apply move_along_compat) }"))::[] update_compat := ltac:(repeat intro; subst; now apply move_along_compat) }"))::[]
let instance_updfunc_Flexible (d:expr) (valret : string): stmt list = let instance_updfunc_Flexible (d:expr) (valret : string): stmt list =
Instance("UpdateFunc",Raw("update_function (path "^valret^") (Similarity.similarity "^valret^") ratio"),Raw(" FlexibleUpdate "^string_of_expression d)) Instance("UpdFun",Raw("update_function (path "^valret^") (Similarity.similarity "^valret^") ratio"),Raw(" FlexibleUpdate "^string_of_expression d))
::[] ::[]
...@@ -206,12 +204,12 @@ let instance_updfunc_Flexible (d:expr) (valret : string): stmt list = ...@@ -206,12 +204,12 @@ let instance_updfunc_Flexible (d:expr) (valret : string): stmt list =
*) *)
let instance_rigidity (r:rigidity) (valret : string) (world: information list): stmt list = let instance_rigidity (r:rigidity) (valret : string) (world: information list): stmt list =
match r with(*TODO: Est-ce la bonne maniere d'ecrire l'UpdateFunc?*) match r with(*TODO: Est-ce la bonne maniere d'ecrire l'UpdateFunc?*)
| Rigide -> Instance("RobotChoice",Raw("robot_choice "^ valret),Raw("{ robot_choice_Setoid := "^valret^"_Setoid}")) | Rigide -> Instance("RC",Raw("robot_choice "^ valret),Raw("{ robot_choice_Setoid := "^valret^"_Setoid}"))
::Instance("ActiveChoice",App(Var(0,"update_choice"),[Cst("unit")]),Raw("NoChoice")) ::Instance("UC",App(Var(0,"update_choice"),[Cst("unit")]),Raw("NoChoice"))
:: instance_updfunc_rigid valret world :: instance_updfunc_rigid valret world
| Flexible d -> Instance("RobotChoice",Raw("robot_choice (path "^ valret^")"),Raw("{ robot_choice_Setoid := path_Setoid "^valret^"}")) | Flexible d -> Instance("RC",Raw("robot_choice (path "^ valret^")"),Raw("{ robot_choice_Setoid := path_Setoid "^valret^"}"))
::Instance("ActiveChoice",App(Cst("update_choice"),[Cst("ratio")]),Raw "Flexible.OnlyFlexible") ::Instance("UC",App(Cst("update_choice"),[Cst("ratio")]),Raw "Flexible.OnlyFlexible")
::Var(string_of_expression d,Raw("R")) ::Var(string_of_expression d,Raw("R"))
::instance_updfunc_Flexible d valret ::instance_updfunc_Flexible d valret
...@@ -251,10 +249,10 @@ let instance_byzantine (x : int ) : stmt list = ...@@ -251,10 +249,10 @@ let instance_byzantine (x : int ) : stmt list =
*) *)
let instance_sync (s : synchro) : stmt list = let instance_sync (s : synchro) : stmt list =
match s with match s with
| Async -> [RawCoq(["Instance InactiveChoice: Async not implemented | Async -> [RawCoq(["Instance ic: Async not implemented
Instance InactiveFunc : Async not implemented"])] Instance InaFun : Async not implemented"])]
| _ -> [RawCoq([ "Instance InactiveChoice : inactive_choice unit := NoChoiceIna."; | _ -> [RawCoq([ "Instance IC : inactive_choice unit := NoChoiceIna.";
"Instance InactiveFunc : inactive_function unit := NoChoiceInaFun."])] "Instance InaFun : inactive_function unit := NoChoiceInaFun."])]
(**[instance_sensors s] permet d'instancier l'observation celon la liste des capteurs [s] Ne prend en compte que la range et la multiplicité pour le moment (**[instance_sensors s] permet d'instancier l'observation celon la liste des capteurs [s] Ne prend en compte que la range et la multiplicité pour le moment
@param s [sensor list] correspondant a la liste des capteurs de la description @param s [sensor list] correspondant a la liste des capteurs de la description
...@@ -354,39 +352,51 @@ let generate_robogram (r : expr list) (d: information list) : stmt list = ...@@ -354,39 +352,51 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
::[] ::[]
| [] -> Def ("Robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[] | [] -> Def ("Robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[]
let rec n_times (x : int) :string =
if x > 0 then n_times (x -1)^"*"^"nat"
else "nat"
let generate_lemmas (g : Graphtest.G.t) : stmt list =
Graphtest.G.fold_vertex (fun v acc -> (**[generate_lemmas g] retourne la liste de stmt correspondant au lemme extrait du graph g
let succs = Graphtest.G.succ g v in @param g [G.t]
@return [stmt list]*)
let generate_lemmas (g : Ast.G.t) : stmt list =
Ast.G.fold_vertex (fun v acc ->
let succs = Ast.G.succ g v in
let forall v =
String.concat " " (List.map string_of_expression (Ast.get_param v))
in
if succs <> [] then if succs <> [] then
let rcs = List.map (fun x -> x ^ " (round config)") succs in let rcs = List.map (fun x -> x ^ " (round Robogram da config)") (List.map string_of_expression succs) in
Lemma("lemma"^string_of_int (List.length acc),Raw(v^" config -> "^String.concat " \\/ " rcs),[])::acc Lemma("lemma"^string_of_int (List.length acc),Forall(("config "^forall v),Raw(string_of_expression v^" config -> "^String.concat " \\/ " rcs)),[])::acc
else else
acc acc
) g [] ) g []
(**[generate_measure m] retourne la liste de stmt correspondant a la generation de la mesure
@param m [measure]
@return [stmt list] *)
let generate_measure (Measure(i,g): measure) : stmt list = let generate_measure (Measure(i,g): measure) : stmt list =
let ret = String.concat "*"(List.init i (fun _ ->"nat")) in let ret = String.concat "*"(List.init i (fun _ ->"nat")) in
let to_change = String.concat ","(List.init i (fun _ ->"0%nat"))in let to_change = String.concat ","(List.init i (fun _ ->"0%nat"))in
Graphtest.png_from_graph g; Ast.png_from_graph g;
Graphtest.print_relations_test g; let lems =Var("da",Cst "demonic_action")::List.rev (generate_lemmas g) in
let lems =List.rev (generate_lemmas g) in
RawCoq(["Function measure (s : observation) : "^ret ^" := RawCoq(["Function measure (s : observation) : "^ret ^" :=
("^to_change^")."; (*TODO: *)
("^to_change^")."; (*TODO: à modifié pour utiliser le graph*)
"Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete@lems "Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete@lems
let generate (Description(d,r,m) : description) (section_name : string)=
if Ast.check_light (Description (d,r,m)) then (**[generate_coq d] genere a partir de la description complete (world,robogram,measure) l'instance coq
@param descritpion
@return [unit] *)
let generate_coq (Description(d,r,m) : description) (section_name : string)=
if Ast.check_light (Description (d,r,m)) &&
Ast.check_activelyup (Description(d,r,m)) &&
Ast.check_sensors_desc (Description(d,r,m))
then
let file_out = open_out ("./generate/"^section_name^".v") in let file_out = open_out ("./generate/"^section_name^".v") in
let format_file = Format.formatter_of_out_channel file_out in let format_file = Format.formatter_of_out_channel file_out in
let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d@newline::generate_measure m) in let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d@newline::generate_measure m) in
Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@[section]); Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@[section]);
close_out file_out close_out file_out;
print_endline(section_name^".v is generated")
else else
raise(Failure("Error light in wrong field")) ()
\ No newline at end of file \ No newline at end of file
lib/graphtest.ml → lib/graphmeasure.ml
+ 0
− 0
View file @ a2c8a0ce
File moved
lib/parser.mly
+ 12
− 12
View file @ a2c8a0ce
%{ %{
open Ast open Ast
open Graphtest
%} %}
%token EOF %token EOF
...@@ -311,23 +310,24 @@ pattern : ...@@ -311,23 +310,24 @@ pattern :
measure: measure:
| PARENOPEN l = separated_list(COMMA,VARIABLE) PARENCLOSE el = edge_list {Measure(List.length l,graph_from_edges el)} | PARENOPEN l = separated_list(COMMA,VARIABLE) PARENCLOSE el = edge_list {Measure(List.length l,graph_from_edges el)}
edge : edge :
| v1 = sommet ARROW v2 = sommet {Nolab(v1,v2)} | v1 = sommet ARROW v2 = sommet {Nolab(v1,v2)}
edge_list : edge_list :
| v = list(edge) { v } | v = list(edge) { v }
sommet : sommet :
| p = prop {string_of_expression p} | p = prop {p}
prop : prop :
| PARENOPEN prop propop prop PARENCLOSE {BinOp($2,$3,$4)} | PARENOPEN prop propop prop PARENCLOSE {BinOp($2,$3,$4)}
| NOT prop {Not $2} | NOT prop {Not $2}
| VARIABLE {Var $1} | VARIABLE {Var $1}
| PARENOPEN f = appfunc PARENCLOSE {f}
propop : propop :
| AND {And} | AND {And}
| OR {Or} | OR {Or}
| IMPLICATION {Impli} | IMPLICATION {Impli}
| EQUIVALENCE {Equiv} | EQUIVALENCE {Equiv}
\ No newline at end of file \ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment