le binaire why prend maintenant une option -I pour fixer le loadpath ; les...

le binaire why prend maintenant  une option -I pour fixer le loadpath ; les theories les plus primitives dans prelude.why

Makefile.in

@@ -124,7 +124,7 @@ bin/top: $(CMO)
 	ocamlmktop $(BFLAGS) -o $@ $^
 
 test: bin/why.byte
-	ocamlrun -bt bin/why.byte src/test.why
+	ocamlrun -bt bin/why.byte -I lib/prelude/ src/test.why
 
 # graphical interface
 #####################

lib/prelude/list.why

-theory List
 
-  type 'a list
+(* additional theories over lists *)
 
-  (* type 'a list = Nil | Cons ('a,'a list) *)
+theory IntList
 
-  logic nil  : 'a list
-
-  logic cons : 'a, 'a list -> 'a list
-
-  logic is_nil : 'a list -> prop
-
-  type int (* use import Int *)
-  
-  logic length : 'a list -> int
+  use prelude.List
 
 end
 

lib/prelude/prelude.why

+
+(* The Why prelude *)
+
+theory Int 
+
+  type int
+
+end
+
+theory List
+
+  (* type 'a list = Nil | Cons ('a, 'a list) *)
+
+  type 'a list
+
+  logic nil : 'a list
+
+  logic cons('a, 'a list) : 'a list
+
+  logic is_nil('a list)
+
+end
+
+

src/main.ml

@@ -23,12 +23,15 @@ let files = ref []
 let parse_only = ref false
 let type_only = ref false
 let debug = ref false
+let loadpath = ref []
 
 let () = 
   Arg.parse 
     ["--parse-only", Arg.Set parse_only, "stops after parsing";
      "--type-only", Arg.Set type_only, "stops after type-checking";
      "--debug", Arg.Set debug, "sets the debug flag";
+     "-I", Arg.String (fun s -> loadpath := s :: !loadpath), 
+       "<dir>  adds dir to the loadpath";
     ]
     (fun f -> files := f :: !files)
     "usage: why [options] files..."
@@ -55,7 +58,7 @@ let type_file env file =
 
 let () =
   try
-    let env = Typing.create ["lib"; ""] in
+    let env = Typing.create !loadpath in
     ignore (List.fold_left type_file env !files)
   with e when not !debug ->
     eprintf "%a@." report e;

src/test.why

 
 (* test file *)
 
-theory A
-  type 'a list
-  logic nil : 'a list
-  logic cons('a, 'a list) : 'a list
+theory TestPrelude 
+  use prelude.List
+  use list.IntList
+end
 
+theory A
   type t
-  logic p('a list)
-  logic is_nil(x: 'a list) = p(x)
-  logic c : t list
+  logic p(t)
+  logic q(x: t) = p(x)
+  logic c : t
 end
 
 theory B
-  use import A
+  use import prelude.List
+  type t
   axiom Ax : forall x : t list. true
 end