From 8094637d0bf5a8b476b7f0ae3ed8f46106e4c337 Mon Sep 17 00:00:00 2001
From: Kylian Fontaine <kylian.fontaine@etu.univ-lyon1.fr>
Date: Tue, 23 Jul 2024 10:14:28 +0200
Subject: [PATCH] fix: location est par defaut en activelyup
---
bin/main.ml | 14 ++++++++------
lib/gencoq.ml | 8 ++++----
2 files changed, 12 insertions(+), 10 deletions(-)
diff --git a/bin/main.ml b/bin/main.ml
index c45c873..44640dd 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 e20b77f..3a1f785 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
--
GitLab