diff --git a/lib/ast.ml b/lib/ast.ml
index 55a5ca2c657d6fbe5a34fa8674713692c50544cb..25549ae100cac09829cd759722fdb049d409c956 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -12,8 +12,6 @@ type binop =
| Inf
| Equal
| Diff
- | Impli
- | Equiv
(*tail::head au lieu de head::tail pour éviter les empilements inutiles
(((vide,x),y),z)
@@ -214,13 +212,11 @@ let rec string_of_expression (e : expr) : string =
| Inf -> "("^string_of_expression(x) ^ " < " ^string_of_expression(y)^")"
| Equal -> string_of_expression(x) ^ " == " ^string_of_expression(y)
| Diff -> string_of_expression(x) ^ " != " ^string_of_expression(y)
- | Impli -> string_of_expression(x) ^ "->" ^string_of_expression(y)
- | Equiv -> string_of_expression(x) ^ " <-> " ^string_of_expression(y)
)
| Not b -> "!("^string_of_expression b^")"
| Var v -> v
| Cond(c,e1,e2) -> "if (" ^string_of_expression c ^ ") then \n {" ^ string_of_expression e1 ^ "} \n else {" ^ string_of_expression e2 ^ "}"
- | Affectation(v,e) -> v ^ " prend la valeur " ^ string_of_expression e
+ | Affectation(v,e) -> v ^ " = " ^ string_of_expression e
| Set s -> string_of_set s string_of_expression
| 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 ^")"
@@ -341,7 +337,7 @@ let png_from_graph g name dir =
let oc = open_out (dir^"/"^name^"_measure.dot") in
Printf.fprintf oc "%s\n" dot;
close_out oc;
- ignore (Sys.command ("dot -Tpng ./generate/"^name^"_measure.dot -o "^dir^"/"^ name^"_measure.png"))
+ ignore (Sys.command ("dot -Tpng "^dir^"/"^name^"_measure.dot -o "^dir^"/"^ name^"_measure.png"))
(**[assign_heigth g] returns the phase, phase weight association list. The phase weight is deduced from the order
topology of the phase
@@ -362,19 +358,19 @@ let assign_height (g : G.t) : (expr * int) list =
module NodeMap = Map.Make(Node)
-(** [update_lowlink v w lowlink] met à jour la valeur de lowlink pour le noeud [v] en fonction du noeud [w]. *)
+(** [update_lowlink v w lowlink] updates the lowlink value for node [v] based on node [w].*)
let update_lowlink v w lowlink =
let v_lowlink = NodeMap.find v lowlink in
let w_lowlink = NodeMap.find w lowlink in
NodeMap.add v (min v_lowlink w_lowlink) lowlink
-(** [update_on_stack w on_stack] supprime le noeud [w] de la liste [on_stack]. *)
+(** [update_on_stack w on_stack] remove node [w] from list [on_stack]. *)
let update_on_stack w on_stack =
List.filter (fun v -> v <> w) on_stack
-(** [pop_stack v stack on_stack scc] retire les éléments de la pile jusqu'à atteindre le noeud [v].
- Cela met à jour [on_stack] en supprimant les noeuds retirés de la pile, et [scc] en ajoutant ces noeuds à la nouvelle composante fortement connexe.*)
+(** [pop_stack v stack on_stack scc] removes elements from the [stack] until reaching node [v].
+ This updates [on_stack] by removing nodes removed from the [stack], and [scc] by adding these nodes to the new strongly connected component.*)
let rec pop_stack v stack on_stack scc =
match stack with
| w :: rest -> if w <> v then pop_stack v rest (update_on_stack w on_stack) (w :: scc)
@@ -382,9 +378,9 @@ let update_lowlink v w lowlink =
| [] -> raise(Failure "Error: stack empty")
-(** [strongconnect v index stack indices lowlink on_stack sccs g] est la fonction qui effectue le parcours en profondeur pour trouver les composantes fortement connexes.
- Pour chaque successeur [w] de [v] dans le graphe [g], si [w] n'est pas encore visité, il est récursivement visité.
- Après avoir visité tous les successeurs, si [v] est une racine de SCC, tous les noeuds dans la pile jusqu'à [v] sont ajoutés à une nouvelle SCC.
+(** [strongconnect v index stack indices lowlink on_stack sccs g] is the function that performs the dfs to find strongly connected components.
+ For each successor [w] of [v] in graph [g], if [w] is not yet visited, it is recursively visited.
+ After visiting all successors, if [v] is a root of SCC, all nodes in the stack up to [v] are added to a new SCC..
*)
let rec strongconnect (g : G.t) (v:expr) (index:int) stack indices lowlink on_stack sccs =
let indices = NodeMap.add v index indices in
@@ -417,8 +413,8 @@ let rec strongconnect (g : G.t) (v:expr) (index:int) stack indices lowlink on_st
else
index, stack, indices, lowlink, on_stack, sccs
-(** [tarjan g] est la fonction principale qui initialise les structures de données et lance le parcours en profondeur.
- et renvoie la liste des composants fortements connexes*)
+(** [tarjan g] is the main function that initializes the data structures and initiates dfs .
+ and returns the list of strongly related components *)
let tarjan g =
(*Tarjan : *)
let _, _, _, _, _, sccs =
@@ -441,7 +437,7 @@ let tarjan g =
module G2 = Graph.Imperative.Digraph.ConcreteLabeled(SCC)(Edge)
- (**[string_of_expr_list expr_list] retourne une chaine de caractere à partir d'une liste d'expression tel que [[X;Y]] correspondant à : string_of_expression X, string_of_expression Y, .... *)
+ (**[string_of_expr_list expr_list] returns a character string from a list of expressions such as [[X;Y]] corresponding to: string_of_expression X, string_of_expression Y, .... *)
let string_of_expr_list expr_list =
let string_list = List.map string_of_expression expr_list in
String.concat ", " string_list
@@ -460,17 +456,17 @@ let png_from_graph2 (g:G2.t) (name : string) (dir : string) :unit =
let oc = open_out (dir^"/"^name^"_measure.dot") in
Printf.fprintf oc "%s\n" dot;
close_out oc;
- ignore (Sys.command ("dot -Tpng ./generate/"^name^"_measure.dot -o "^dir^"/"^ name^"_measure.png"))
+ ignore (Sys.command ("dot -Tpng "^dir^"/"^name^"_measure.dot -o "^dir^"/"^ name^"_measure.png"))
-(** [scc_graph g] retourne le graphe G2.t correspondant au graphe de composants fortement connexe du graphe [g]
- en recupérant la liste des composants fortement connexe et en les ajoutant au graphe G2.t créé[scc_graph].
- Ensuite, la fonction itère sur chaque SCC et ajoute des arêtes entre les SCC en se basant sur le graphe original [g].
- Pour chaque sommet dans un SCC, elle itère sur ses successeurs et trouve le SCC auquel chaque successeur appartient.
- Si le SCC du sommet et le SCC du successeur sont différents, une arête est ajoutée entre les SCC correspondants dans [scc_graph].
+(** [scc_graph g] returns the graph G2.t corresponding to the strongly connected component graph of graph [g]
+ by retrieving the list of strongly connected components and adding them to the created G2.t graph[scc_graph].
+ Then the function iterates over each SCC and adds edges between the SCCs based on the original graph [g].
+ For each vertex in an SCC, it iterates over its successors and finds the SCC to which each successor belongs.
+ If the vertex SCC and the successor SCC are different, an edge is added between the corresponding SCCs in [scc_graph].
@param g [G.t]
- @return [scc_graph] de type [G2.t], le graphe des composants fortement connexe de [g] *)
+ @return [scc_graph] of type [G2.t], the strongly connected component graph of [g] *)
let scc_graph g =
let scc_list = tarjan g in
let scc_graph = G2.create () in
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index c1ffcf930e92561475cf2608ddeedd25740b2c70..e20b77f4fdf30c04457ceb587f294f94b2800e2b 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -100,8 +100,6 @@ let rec expr_to_coq (r : expr) : Formula.t =
| Inf -> Infix(expr_to_coq x,"<",expr_to_coq y)
| Equal -> 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)
- | Equiv -> Infix(expr_to_coq x,"<->",expr_to_coq y)
)
| Cons (e1,e2) -> App(Raw("cons"), ([expr_to_coq e1;expr_to_coq e2]))
| Fun (s,e) -> Fun(Some s, expr_to_coq e)
@@ -470,38 +468,10 @@ let generate_lt (t:string * Formula.t * stmt list -> stmt) : stmt list =
let generate_module_proof (m: measure)(s:string) (gmpp:stmt list) (gdp : stmt list) =
-
ModuleImpType(s^"_proof",s^"_type", RawCoq(["Import World.";"Variable da : demonic_action."])::generate_measure_all m (fun (a,b,c) -> Lemma(a, b, c)) gmpp gdp
@newline::generate_lt (fun (a,b,c) -> Lemma(a, b, c)))::[]
- (** [read_and_save_after_keyword filename keyword] is a function that reads the contents of a file specified by [filename] and returns all the lines that appear after the first occurrence of [keyword].
- The function opens the file, reads its contents line by line, and stores them in a list. It then searches for the first occurrence of [keyword] in the lines and returns all the lines that appear after it.
- If [keyword] is not found, an empty list is returned.
- @param filename is the path to the file to be read.
- @param keyword is the string to search for in the file.
- *)
- let read_and_save_after_keyword filename keyword =
- let in_channel = open_in filename in
- let rec loop lines =
- try
- let line = input_line in_channel in
- loop (line :: lines)
- with End_of_file ->
- close_in in_channel;
- List.rev lines
- in
- let lines = loop [] in
- let rec find_keyword lines =
- match lines with
- | [] -> []
- | line :: rest -> try ignore (Str.search_forward (Str.regexp keyword) line 0); rest
- with Not_found -> find_keyword rest
- in
- String.concat "\n" (find_keyword lines)
-
-
-
(** [write_coq_file gen filename] writes the generated Coq code to the specified file.
@param gen stmt list representing the generated Coq code.
@param filename The name of the file to write the generated code to.
@@ -513,34 +483,6 @@ let write_coq_file (gen: stmt list) (filename : string) =
close_out file_out;
print_endline(filename^ " has been generated");;
-
-(*
-(**[generate_coq d s] generates the coq file containing the world description module, the type module and the proof module
- @param description of
- @param string s
- @return[unit] *)
-let generate_coq (Description(d,r,Measure g) : description) (name : string)=
- if Ast.check_description (Description(d,r,Measure g))
- then
- let gmpptype, gmpp_proof = generate_measure_per_phase g in
- let gdp_type, gdp_proof = generate_definition_phase g in
- Ast.png_from_graph g name ;
- Ast.png_from_graph2 (Ast.scc_graph g;) (name^"_scc_graph");
- let file_exists =
- Sys.file_exists ("./generate/"^name^".v") in
- (* if file exist we save the proof part, else we generate the proof part*)
- let proof = if file_exists then
- [RawCoq([read_and_save_after_keyword ("./generate/"^name^".v") ("End "^name^"_type.")])]
- else newline::generate_module_proof (Measure g) name gmpp_proof gdp_proof
- in
- let module_world_type = (generate_requires d)@Module("World",(generate_instances d)@newline::generate_robogram r d)
- :: generate_module_type (Measure g) name gmpptype gdp_type in
- write_coq_file (module_world_type@proof) ("./generate/"^name^"world_type.v");
-
-
- else
- ()
-*)
(**[generate_filename base n dir]
@param base : string, base file name
@param n : integer, number of file iterations
diff --git a/lib/lexer.mll b/lib/lexer.mll
index f96a35cc951416a2c5d7affe62528de5a0b28a51..be04b7a5e38b59ac293851759505765ae63a5b30 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -80,8 +80,6 @@ rule token = parse
| "|" { PIPE}
| "end" { END}
| "->" { ARROW}
- | "=>" { IMPLICATION}
- | "<=>" { EQUIVALENCE}
| "let" { LET}
| "=" { AFFECT}
| "in" { IN}
diff --git a/lib/parser.mly b/lib/parser.mly
index 9a4ae99fa26c279fd3170fc87bff80229a1f2971..1250f87c956355f086360eaef388045eeb2f42fb 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -29,7 +29,6 @@
%token <string> VARIABLE
%token <string> KEYWORD
%token IF THEN ELSE MATCH WITH PIPE ARROW END
-%token IMPLICATION EQUIVALENCE
%token LET AFFECT IN FUN
%token PLUS MINUS MULT DIV AND OR NOT
%token SUP INF EQUAL DIFF
@@ -216,7 +215,6 @@ robogram:
| expression * {$1}
expression:
- /*(e)*/
| e = constant {e}
/*if e1 then e2 else e3*/
| IF e1 = expression THEN e2 = expression ELSE e3 = expression {Cond(e1,e2,e3)} %prec AFFECT
@@ -271,7 +269,7 @@ set :
| {Vide}
%inline binop :
- | PLUS {(*Format.eprintf "PLUS ";*) Plus}
+ | PLUS {Plus}
| MINUS {Minus}
| MULT {Mult}
| DIV {Div}
@@ -307,17 +305,8 @@ edge_list :
sommet :
- | p = prop {p}
+ | p = phase {p}
-prop :
- | PARENOPEN prop propop prop PARENCLOSE {BinOp($2,$3,$4)}
- | NOT prop {Not $2}
+phase :
| VARIABLE {Var $1}
| KEYWORD {Var $1}
- | PARENOPEN f = appfunc PARENCLOSE {f}
-
-propop :
- | AND {And}
- | OR {Or}
- | IMPLICATION {Impli}
- | EQUIVALENCE {Equiv}
\ No newline at end of file