modules added to the default loadpath

Makefile.in

@@ -223,9 +223,11 @@ install_no_local::
 	mkdir -p $(DATADIR)/why3/lang
 	mkdir -p $(DATADIR)/why3/theories
 	mkdir -p $(DATADIR)/why3/theories/transform
+	mkdir -p $(DATADIR)/why3/modules
 	mkdir -p $(DATADIR)/why3/drivers
 	cp -f theories/*.why $(DATADIR)/why3/theories
 	cp -f theories/transform/*.why $(DATADIR)/why3/theories/transform
+	cp -f modules/*.mlw $(DATADIR)/why3/modules
 	cp -f drivers/*.drv $(DATADIR)/why3/drivers
 	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
 	cp -f share/images/*.png $(DATADIR)/why3/images
@@ -942,6 +944,7 @@ DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
       examples/*.why examples/programs/*.mlw examples/tptp/*.why \
       examples/my_cosine/*.v \
       theories/*.why theories/*/*.why \
+      modules/*.mlw \
       share/*.conf \
       share/emacs/why.el share/images/*.png share/lang/*.lang
 

src/driver/whyconf.ml

@@ -30,7 +30,8 @@ let compilation_datadir =
     (fun d -> Filename.concat d "share") Config.localdir
 
 let compilation_loadpath =
-  Filename.concat compilation_datadir "theories"
+  [ Filename.concat compilation_datadir "theories";
+    Filename.concat compilation_datadir "modules"; ]
 
 let default_conf_file =
   match Config.localdir with
@@ -121,7 +122,7 @@ let default_main =
   {
     private_libdir = compilation_libdir;
     private_datadir = compilation_datadir;
-    loadpath = [compilation_loadpath];
+    loadpath = compilation_loadpath;
     timelimit = 10;
     memlimit = 0;
     running_provers_max = 2;

src/programs/pgm_wp.ml

@@ -453,7 +453,7 @@ let add_wp_decl ps f uc =
     | Some loc -> id_user s loc
   in
   let f = f_btop uc f in
-  printf "wp: f=%a@." print_fmla f;
+  (* printf "wp: f=%a@." print_fmla f; *)
   let pr = create_prsymbol id in
   let d = create_prop_decl Pgoal pr f in
   add_logic_decl d uc

tests/test-pgm-jcf.mlw

 
-module Ref
-
-  { use import programs.Prelude }
-
-  mutable type ref 'a model 'a
-
-  parameter create : v:'a -> {} ref 'a { result=v }
-
-  parameter get : r:ref 'a -> {} 'a reads r { result=r }
-
-  parameter set : r:ref 'a -> v:'a -> {} unit writes r { r=v }
-
-end
-
 module P
 
   { use import programs.Prelude }
   { use import int.Int }
   
-  use module export Ref
+  use module export stdlib.Ref
 
   let incr (r : ref int) : unit =
     {}
@@ -29,7 +15,7 @@ module P
 
   let f () =
     { true }
-    let r = create 0 in
+    let r = ref 0 in
     (* assert { r = 0 }; *)
     incr r;
     get r