diff --git a/bin/main.ml b/bin/main.ml index c45c8734d0b9b3fd83ab2cccfebc42a8c827cb0b..44640ddeab306f5d1dbbf8d93cc569dbd9e3a3ac 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -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 *) let gen (args : string array) = - let list_args = Array.to_list args in - try - 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 - 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;; + if Array.length args < 2 then (print_endline usage; exit 0) + else + let list_args = Array.to_list args 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 + Gencoq.generate_coq_2files (Interface.parse_description name) (Filename.basename name) proof_name type_name overwrite repo_gen graph_gen + ;; + gen Sys.argv;; diff --git a/lib/gencoq.ml b/lib/gencoq.ml index e20b77f4fdf30c04457ceb587f294f94b2800e2b..3a1f785e73ea8494df86a983af9ee7dd1c47e460 100644 --- a/lib/gencoq.ml +++ b/lib/gencoq.ml @@ -28,13 +28,13 @@ let get_val_ret (infos : information list) : string list = | Location::tl -> "location" :: (locdir tl ) | Direction::tl -> "direction" ::(locdir tl) | Str x ::tl -> if x = "Light" then "light" :: (locdir tl) else (locdir tl) - | [] -> [] + | [] -> ["location"] 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 match valret with - | Some (ActivelyUpdate x) -> locdir x - | _-> ["location"] + | ActivelyUpdate x -> locdir x + | _-> [] (**[get_space infos] returns the string corresponding to the space @param information list corresponding to the description of the world