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

typo

parent c17d1884
No related branches found
No related tags found
1 merge request!1Module
......@@ -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
......
......@@ -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
......
......@@ -80,8 +80,6 @@ rule token = parse
| "|" { PIPE}
| "end" { END}
| "->" { ARROW}
| "=>" { IMPLICATION}
| "<=>" { EQUIVALENCE}
| "let" { LET}
| "=" { AFFECT}
| "in" { IN}
......
......@@ -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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment