no more need to patch parser files

Makefile.in

@@ -160,15 +160,11 @@ LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
 $(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
 $(LIBCMX): OFLAGS += -for-pack Why
 
-LIB_PARSER_POSTLUDE  = "let logic_file env = inside_env env logic_file\n"
-LIB_PARSER_INTERFACE = "s/^val  *logic_file *:/val logic_file : Env.env ->/"
-
 src/parser/parser.ml: src/parser/parser.pre.ml
 	cp $^ $@
-	printf $(LIB_PARSER_POSTLUDE) >> $@
 
 src/parser/parser.mli: src/parser/parser.pre.mli
-	sed -e $(LIB_PARSER_INTERFACE) $^ > $@
+	cp $^ $@
 
 # build targets
 

src/parser/lexer.mll

@@ -315,7 +315,9 @@ and string = parse
       | Loc.Located _ as e -> raise e
       | e -> raise (Loc.Located (loc lb, e))
 
-  let parse_logic_file env = with_location (logic_file env token)
+  let parse_logic_file env lb =
+    pre_logic_file token (Lexing.from_string "") env;
+    with_location (logic_file token) lb
 
   let parse_program_file = with_location (program_file token)
 

src/parser/parser.pre.mly

@@ -18,8 +18,7 @@
 /**************************************************************************/
 
 %{
-  open Theory
-
+module Incremental = struct
   let env_ref  = ref []
   let lenv_ref = ref []
   let uc_ref   = ref []
@@ -32,13 +31,29 @@
   let ref_push ref v = ref := v :: !ref
   let ref_set  ref v = ref := v :: ref_tail ref
 
-  let inside_env env rule lexer lexbuf =
-    ref_push env_ref env;
-      ref_push lenv_ref Mnm.empty;
-    let res = rule lexer lexbuf in
-      ref_drop lenv_ref;
-    ref_drop env_ref;
-    res
+  let open_logic_file env =
+    ref_push env_ref env; ref_push lenv_ref Theory.Mnm.empty
+
+  let close_logic_file () =
+    ref_drop env_ref; ref_pop lenv_ref
+
+  let open_theory id =
+    ref_push uc_ref (Theory.create_theory (Denv.create_user_id id))
+
+  let close_theory loc =
+    let uc = ref_pop uc_ref in
+    ref_set lenv_ref (Typing.close_theory loc (ref_get lenv_ref) uc)
+
+  let open_namespace () =
+    ref_set uc_ref (Theory.open_namespace (ref_get uc_ref))
+
+  let close_namespace loc import name =
+    ref_set uc_ref (Typing.close_namespace loc import name (ref_get uc_ref))
+
+  let new_decl d =
+    let env = ref_get env_ref in let lenv = ref_get lenv_ref in
+    ref_set uc_ref (Typing.add_decl env lenv (ref_get uc_ref) d)
+end
 
   open Ptree
   open Parsing
@@ -226,14 +241,20 @@
 
 /* Entry points */
 
+%type <Env.env -> unit> pre_logic_file
+%start pre_logic_file
 %type <Theory.theory Theory.Mnm.t> logic_file
 %start logic_file
 %type <Ptree.program_file> program_file
 %start program_file
 %%
 
+pre_logic_file:
+| /* epsilon */  { Incremental.open_logic_file }
+;
+
 logic_file:
-| list0_theory EOF  { ref_get lenv_ref }
+| list0_theory EOF  { Incremental.close_logic_file () }
 ;
 
 /* File, theory, namespace */
@@ -244,16 +265,11 @@ list0_theory:
 ;
 
 theory_head:
-| THEORY uident labels
-   { let id = add_lab $2 $3 in
-     let name = Denv.create_user_id id in
-     ref_push uc_ref (create_theory name); id }
+| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
 ;
 
 theory:
-| theory_head list0_decl END
-   { let uc = ref_pop uc_ref in
-     ref_set lenv_ref (Typing.close_theory (ref_get lenv_ref) $1 uc) }
+| theory_head list0_decl END  { Incremental.close_theory (floc_i 1) }
 ;
 
 list0_decl:
@@ -263,15 +279,13 @@ list0_decl:
 
 new_decl:
 | decl
-   { let env = ref_get env_ref in let lenv = ref_get lenv_ref in
-     ref_set uc_ref (Typing.add_decl env lenv (ref_get uc_ref) $1) }
+   { Incremental.new_decl $1 }
 | namespace_head namespace_import namespace_name list0_decl END
-   { ref_set uc_ref (Typing.close_namespace (floc ()) $2 $3 (ref_get uc_ref)) }
+   { Incremental.close_namespace (floc_i 3) $2 $3 }
 ;
 
 namespace_head:
-| NAMESPACE
-   { ref_set uc_ref (open_namespace (ref_get uc_ref)) }
+| NAMESPACE  { Incremental.open_namespace () }
 ;
 
 namespace_import:

src/parser/typing.ml

@@ -735,9 +735,11 @@ and dfmla_node ~localize loc uc env = function
       in
       let f1 = dfmla ~localize uc env f1 in
       Fnamed (x, f1)
+(*
   | PPvar (Qident s | Qdot (_,s) as x) when is_uppercase s.id.[0] ->
       let pr = find_prop x uc in
       Fvar (Decl.find_prop (Theory.get_known uc) pr)
+*)
   | PPvar x ->
       let s, tyl = specialize_psymbol x uc in
       let tl = dtype_args s.ls_name loc uc env tyl [] in
@@ -1194,10 +1196,12 @@ let add_decl env lenv th d =
   if Debug.test_flag debug_parse_only then th else
   add_decl env lenv th d
 
-let close_theory lenv { id = id ; id_loc = loc } th =
-  if Mnm.mem id lenv then error ~loc (ClashTheory id);
+let close_theory loc lenv th =
   if Debug.test_flag debug_parse_only then lenv else
-  Mnm.add id (close_theory th) lenv
+  let th = close_theory th in
+  let id = th.th_name.id_string in
+  if Mnm.mem id lenv then error ~loc (ClashTheory id);
+  Mnm.add id th lenv
 
 let close_namespace loc import name th =
   let id = option_map (fun id -> id.id) name in

src/parser/typing.mli

@@ -34,7 +34,7 @@ val add_decl : Env.env -> theory Mnm.t -> theory_uc -> Ptree.decl -> theory_uc
 val close_namespace :
   Loc.position -> bool -> Ptree.ident option -> theory_uc -> theory_uc
 
-val close_theory : theory Mnm.t -> Ptree.ident -> theory_uc -> theory Mnm.t
+val close_theory : Loc.position -> theory Mnm.t -> theory_uc -> theory Mnm.t
 
 (******************************************************************************)
 (** The following is exported for program typing (src/programs/pgm_typing.ml) *)
@@ -70,7 +70,8 @@ val dty : theory_uc -> denv -> Ptree.pty -> Denv.dty
 val dterm : ?localize:bool -> theory_uc -> denv -> Ptree.lexpr -> Denv.dterm
 val dfmla : ?localize:bool -> theory_uc -> denv -> Ptree.lexpr -> Denv.dfmla
 val dpat : theory_uc -> denv -> Ptree.pattern -> denv * Denv.dpattern
-val dpat_list : theory_uc -> denv -> Denv.dty -> Ptree.pattern -> denv * Denv.dpattern
+val dpat_list :
+  theory_uc -> denv -> Denv.dty -> Ptree.pattern -> denv * Denv.dpattern
 
 val print_denv : Format.formatter -> denv -> unit