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

fix: location est par defaut en activelyup

parent f9910891
Branches
No related tags found
1 merge request!1Module
...@@ -29,11 +29,13 @@ let rec parse_args args (proof_name : string) (type_name : string) (overwrite: b ...@@ -29,11 +29,13 @@ let rec parse_args args (proof_name : string) (type_name : string) (overwrite: b
@param args: string array, array of command line arguments @param args: string array, array of command line arguments
*) *)
let gen (args : string array) = let gen (args : string array) =
if Array.length args < 2 then (print_endline usage; exit 0)
else
let list_args = Array.to_list args in let list_args = Array.to_list args in
try
let name = args.(1) in let name = args.(1) in
let (proof_name, type_name, overwrite,repo_gen, graph_gen) = parse_args list_args ((Filename.basename name)^"_proof") ((Filename.basename name)^"_world_type") true "./generate" false in let (proof_name, type_name, overwrite,repo_gen, graph_gen) = parse_args list_args ((Filename.basename name)^"_proof") ((Filename.basename name)^"_world_type") true "./generate" false in
Gencoq.generate_coq_2files (Interface.parse_description name) (Filename.basename name) proof_name type_name overwrite repo_gen graph_gen Gencoq.generate_coq_2files (Interface.parse_description name) (Filename.basename name) proof_name type_name overwrite repo_gen graph_gen
with _ -> print_endline usage; exit 0;; ;;
gen Sys.argv;; gen Sys.argv;;
...@@ -28,13 +28,13 @@ let get_val_ret (infos : information list) : string list = ...@@ -28,13 +28,13 @@ let get_val_ret (infos : information list) : string list =
| Location::tl -> "location" :: (locdir tl ) | Location::tl -> "location" :: (locdir tl )
| Direction::tl -> "direction" ::(locdir tl) | Direction::tl -> "direction" ::(locdir tl)
| Str x ::tl -> if x = "Light" then "light" :: (locdir tl) else (locdir tl) | Str x ::tl -> if x = "Light" then "light" :: (locdir tl) else (locdir tl)
| [] -> [] | [] -> ["location"]
in in
let valret = List.find_opt (fun x -> match x with |ActivelyUpdate _ -> true | _ -> false) infos let valret = List.find (fun x -> match x with |ActivelyUpdate _ -> true | _ -> false) infos
in in
match valret with match valret with
| Some (ActivelyUpdate x) -> locdir x | ActivelyUpdate x -> locdir x
| _-> ["location"] | _-> []
(**[get_space infos] returns the string corresponding to the space (**[get_space infos] returns the string corresponding to the space
@param information list corresponding to the description of the world @param information list corresponding to the description of the world
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment