Mlw: merge why_file and mlw_file, admit no-module input

src/parser/lexer.mll

@@ -230,7 +230,7 @@ rule token = parse
   let read_channel env path file c =
     let lb = Lexing.from_channel c in
     Loc.set_file file lb;
-    Typing.open_file ~pure:false env path;
+    Typing.open_file env path;
     let mm = Loc.with_location (mlw_file token) lb in
     if path = [] && Debug.test_flag debug then begin
       let add_m _ m mm = Mid.add m.mod_theory.th_name m mm in
@@ -242,15 +242,6 @@ rule token = parse
     end;
     mm
 
-  let () = Env.register_format mlw_language "whyml" ["mlw"] read_channel
+  let () = Env.register_format mlw_language "whyml" ["mlw";"why"] read_channel
     ~desc:"WhyML@ programming@ and@ specification@ language"
-
-  let read_channel env path file c =
-    let lb = Lexing.from_channel c in
-    Loc.set_file file lb;
-    Typing.open_file ~pure:true env path;
-    Loc.with_location (mlw_file token) lb
-
-  let () = Env.register_format mlw_language "whyml_spec" ["why"] read_channel
-    ~desc:"WhyML@ specification@ sublanguage"
 }

src/parser/parser.mly

@@ -162,21 +162,22 @@
 %start <Pmodule.pmodule Stdlib.Mstr.t> mlw_file
 %%
 
-(* Theories, modules, namespaces *)
+(* Modules and namespaces *)
 
 mlw_file:
-| theory_or_module* EOF { Typing.close_file () }
-(* TODO
-| module_decl* EOF { Typing.close_file () }
-*)
+| mlw_module* EOF
+    { Typing.close_file () }
+| module_decl+ EOF
+    { let loc = floc $startpos($2) $endpos($2) in
+      Typing.close_module loc; Typing.close_file () }
 
-theory_or_module:
+mlw_module:
 | module_head module_decl* END
     { Typing.close_module (floc $startpos($3) $endpos($3)) }
 
 module_head:
-| THEORY labels(uident)  { Typing.open_module $2 ~theory:true  }
-| MODULE labels(uident)  { Typing.open_module $2 ~theory:false }
+| THEORY labels(uident)  { Typing.open_module $2 }
+| MODULE labels(uident)  { Typing.open_module $2 }
 
 module_decl:
 | decl            { Typing.add_decl  (floc $startpos $endpos) $1 }

src/parser/typing.ml

@@ -1000,7 +1000,7 @@ let add_prop muc k s f =
 
 (* parse declarations *)
 
-let add_decl muc inth d =
+let add_decl muc d =
   let vc = muc.muc_path = [] &&
     Debug.test_noflag debug_type_only in
   match d with
@@ -1026,9 +1026,6 @@ let add_decl muc inth d =
         | Ptree.Mstr s -> MAstr s
         | Ptree.Mint i -> MAint i in
       add_meta muc (lookup_meta id.id_str) (List.map convert al)
-  | _ when inth ->
-      (* TODO: should we allow "let function"? what about mixed letrecs? *)
-      Loc.errorm "Program declarations are not allowed in pure theories"
   | Ptree.Dlet (id, gh, kind, e) ->
       let ld = create_user_id id, gh, kind, dexpr muc denv_empty e in
       add_pdecl ~vc muc (create_let_decl (let_defn ~keep_loc:true ld))
@@ -1179,32 +1176,27 @@ let use_clone loc muc env file (use, subst) =
 type slice = {
   env           : Env.env;
   path          : Env.pathname;
-  pure          : bool;
   mutable file  : pmodule Mstr.t;
   mutable muc   : pmodule_uc option;
-  mutable inth  : bool;
 }
 
 let state = (Stack.create () : slice Stack.t)
 
-let open_file env path ~pure =
+let open_file env path =
   assert (Stack.is_empty state || (Stack.top state).muc <> None);
-  Stack.push { env = env; path = path; pure = pure;
-               file = Mstr.empty; muc = None; inth = false } state
+  Stack.push { env = env; path = path; file = Mstr.empty; muc = None } state
 
 let close_file () =
   assert (not (Stack.is_empty state) && (Stack.top state).muc = None);
   (Stack.pop state).file
 
-let open_module ({id_str = nm; id_loc = loc} as id) ~theory =
+let open_module ({id_str = nm; id_loc = loc} as id) =
   assert (not (Stack.is_empty state) && (Stack.top state).muc = None);
   let slice = Stack.top state in
   if Mstr.mem nm slice.file then Loc.errorm ~loc
     "module %s is already defined in this file" nm;
-  if slice.pure && not theory then Loc.errorm ~loc
-    "this file can only contain pure theories";
   let muc = create_module slice.env ~path:slice.path (create_user_id id) in
-  slice.muc <- Some muc; slice.inth <- theory
+  slice.muc <- Some muc
 
 let close_module loc =
   assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
@@ -1230,10 +1222,19 @@ let close_namespace loc ~import =
     slice.muc <- Some muc
 
 let add_decl loc d =
-  assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
+  assert (not (Stack.is_empty state));
+  let slice = Stack.top state in
+  let muc = match slice.muc with
+    | Some muc -> muc
+    | None ->
+        assert (Mstr.is_empty slice.file);
+        if slice.path <> [] then Loc.errorm ~loc
+          "All declarations in library files must be inside modules";
+        let muc = create_module slice.env ~path:[] (id_fresh "Top") in
+        slice.muc <- Some muc;
+        muc in
   if Debug.test_noflag debug_parse_only then
-    let slice = Stack.top state in
-    let muc = Loc.try3 ~loc add_decl (Opt.get slice.muc) slice.inth d in
+    let muc = Loc.try2 ~loc add_decl muc d in
     slice.muc <- Some muc
 
 let use_clone loc use =

src/parser/typing.mli

@@ -13,11 +13,11 @@ val debug_parse_only : Debug.flag
 
 val debug_type_only : Debug.flag
 
-val open_file : Env.env -> Env.pathname -> pure:bool -> unit
+val open_file : Env.env -> Env.pathname -> unit
 
 val close_file : unit -> Pmodule.pmodule Stdlib.Mstr.t
 
-val open_module : Ptree.ident -> theory:bool -> unit
+val open_module : Ptree.ident -> unit
 
 val close_module : Ptree.loc -> unit
 

src/tools/why3prove.ml

@@ -58,13 +58,17 @@ let add_opt_theory x =
       Queue.push (x, p, t, glist,elist) tlist;
       opt_theory := Some glist
 
-let add_opt_goal x = match !opt_theory with
-  | None ->
-      eprintf "Option '-G'/'--goal' requires a theory.@.";
-      exit 1
-  | Some glist ->
-      let l = Strings.split '.' x in
-      Queue.push (x, l) glist
+let add_opt_goal x =
+  let glist = match !opt_theory, !opt_input with
+    | None, None -> eprintf
+        "Option '-G'/'--goal' requires an input file or a library theory.@.";
+        exit 1
+    | None, Some _ ->
+        add_opt_theory "Top";
+        Opt.get !opt_theory
+    | Some glist, _ -> glist in
+  let l = Strings.split '.' x in
+  Queue.push (x, l) glist
 
 let add_opt_trans x = opt_trans := x::!opt_trans