incremental parsing for programs

Makefile.in

@@ -120,7 +120,7 @@ LIB_UTIL = stdlib exn_printer pp debug loc print_tree \
 
 LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
 
-LIB_PARSER = ptree denv glob typing parser lexer
+LIB_PARSER = ptree denv glob parser typing lexer
 
 LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 	     whyconf autodetection

src/parser/lexer.mli

@@ -23,9 +23,10 @@
 val library_of_env : Env.env -> unit Env.library
 
 val parse_logic_file :
-  Env.env -> string list -> Lexing.lexbuf -> Theory.theory Util.Mstr.t
+  Env.env -> Env.pathname -> Lexing.lexbuf -> Theory.theory Util.Mstr.t
 
-val parse_program_file : Lexing.lexbuf -> Ptree.program_file
+val parse_program_file :
+  Ptree.incremental -> Lexing.lexbuf -> unit
 
 val token_counter : Lexing.lexbuf -> int * int
 

src/parser/lexer.mll

@@ -316,10 +316,13 @@ and string = parse
       | e -> raise (Loc.Located (loc lb, e))
 
   let parse_logic_file env path lb =
-    pre_logic_file token (Lexing.from_string "") env path;
-    with_location (logic_file token) lb
+    open_file token (Lexing.from_string "") (Typing.open_file env path);
+    with_location (logic_file token) lb;
+    Typing.close_file ()
 
-  let parse_program_file = with_location (program_file token)
+  let parse_program_file inc lb =
+    open_file token (Lexing.from_string "") inc;
+    with_location (program_file token) lb
 
   let token_counter lb =
     let rec loop in_annot a p =

src/parser/parser.mly

@@ -20,50 +20,19 @@
 
 %{
 module Incremental = struct
-  let env_ref  = ref []
-  let lenv_ref = ref []
-  let uc_ref   = ref []
-  let path_ref = ref []
-
-  let ref_get  ref = List.hd !ref
-  let ref_tail ref = List.tl !ref
-  let ref_drop ref = ref := ref_tail ref
-  let ref_pop  ref = let v = ref_get ref in ref_drop ref; v
-
-  let ref_push ref v = ref := v :: !ref
-  let ref_set  ref v = ref := v :: ref_tail ref
-
-  let open_logic_file env path =
-    ref_push env_ref env;
-    ref_push path_ref path;
-    ref_push lenv_ref Util.Mstr.empty
-
-  let close_logic_file () =
-    ref_drop path_ref;
-    ref_drop env_ref;
-    ref_pop lenv_ref
-
-  let open_theory id =
-    let path = ref_get path_ref in
-    ref_push uc_ref (Theory.create_theory ~path (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 =
-    ref_set uc_ref (Typing.add_decl (ref_get uc_ref) d)
-
-  let new_use_clone loc d =
-    let env = ref_get env_ref in let lenv = ref_get lenv_ref in
-    ref_set uc_ref (Typing.add_use_clone env lenv (ref_get uc_ref) loc d)
-
+  let stack = Stack.create ()
+  let open_file inc = Stack.push inc stack
+  let close_file () = ignore (Stack.pop stack)
+  let open_theory id = (Stack.top stack).Ptree.open_theory id
+  let close_theory () = (Stack.top stack).Ptree.close_theory ()
+  let open_module id = (Stack.top stack).Ptree.open_module id
+  let close_module () = (Stack.top stack).Ptree.close_module ()
+  let open_namespace () = (Stack.top stack).Ptree.open_namespace ()
+  let close_namespace l b n = (Stack.top stack).Ptree.close_namespace l b n
+  let new_decl loc d = (Stack.top stack).Ptree.new_decl loc d
+  let new_pdecl loc d = (Stack.top stack).Ptree.new_pdecl loc d
+  let use_clone loc use = (Stack.top stack).Ptree.use_clone loc use
+  let use_module loc use = (Stack.top stack).Ptree.use_module loc use
 end
 
   open Ptree
@@ -273,20 +242,20 @@ end
 
 /* Entry points */
 
-%type <unit Env.library -> string list -> unit> pre_logic_file
-%start pre_logic_file
-%type <Theory.theory Util.Mstr.t> logic_file
+%type <Ptree.incremental -> unit> open_file
+%start open_file
+%type <unit> logic_file
 %start logic_file
-%type <Ptree.program_file> program_file
+%type <unit> program_file
 %start program_file
 %%
 
-pre_logic_file:
-| /* epsilon */  { Incremental.open_logic_file }
+open_file:
+| /* epsilon */  { Incremental.open_file }
 ;
 
 logic_file:
-| list0_theory EOF  { Incremental.close_logic_file () }
+| list0_theory EOF  { Incremental.close_file () }
 ;
 
 /* File, theory, namespace */
@@ -301,7 +270,7 @@ theory_head:
 ;
 
 theory:
-| theory_head list0_decl END  { Incremental.close_theory (floc_i 1) }
+| theory_head list0_decl END  { Incremental.close_theory () }
 ;
 
 list0_decl:
@@ -311,9 +280,9 @@ list0_decl:
 
 new_decl:
 | decl
-   { Incremental.new_decl $1 }
+   { Incremental.new_decl (floc ()) $1 }
 | use_clone
-   { Incremental.new_use_clone (floc ()) $1 }
+   { Incremental.use_clone (floc ()) $1 }
 | namespace_head namespace_import namespace_name list0_decl END
    { Incremental.close_namespace (floc_ij 1 3) $2 $3 }
 ;
@@ -346,13 +315,13 @@ decl:
 | inductive list1_inductive_decl
     { IndDecl ($1, $2) }
 | AXIOM ident labels COLON lexpr
-    { PropDecl (floc (), Kaxiom, add_lab $2 $3, $5) }
+    { PropDecl (Kaxiom, add_lab $2 $3, $5) }
 | LEMMA ident labels COLON lexpr
-    { PropDecl (floc (), Klemma, add_lab $2 $3, $5) }
+    { PropDecl (Klemma, add_lab $2 $3, $5) }
 | GOAL ident labels COLON lexpr
-    { PropDecl (floc (), Kgoal, add_lab $2 $3, $5) }
+    { PropDecl (Kgoal, add_lab $2 $3, $5) }
 | META sident list1_meta_arg_sep_comma
-    { Meta (floc (), $2, $3) }
+    { Meta ($2, $3) }
 ;
 
 inductive:
@@ -995,79 +964,46 @@ bar_:
 /****************************************************************************/
 
 program_file:
-| list0_theory_or_module_ EOF { $1 }
-;
-
-list0_theory_or_module_:
-| /* epsilon */
-   { [] }
-| list1_theory_or_module_
-   { $1 }
-;
-
-list1_theory_or_module_:
-| theory_or_module_
-   { [$1] }
-| theory_or_module_ list1_theory_or_module_
-   { $1 :: $2 }
-;
-
-theory_or_module_:
-| THEORY uident labels list0_full_decl END
-   { Ptheory { pth_name = add_lab $2 $3; pth_decl = $4; } }
-| MODULE uident labels list0_program_decl END
-   { Pmodule { mod_name = add_lab $2 $3; mod_decl = $4; } }
+| list0_theory_or_module EOF { Incremental.close_file () }
 ;
 
-list0_full_decl:
-| /* epsilon */
-   { [] }
-| list1_full_decl
-   { $1 }
+list0_theory_or_module:
+| /* epsilon */                   { () }
+| theory list0_theory_or_module   { () }
+| module_ list0_theory_or_module  { () }
 ;
 
-list1_full_decl:
-| full_decl
-   { [$1] }
-| full_decl list1_full_decl
-   { $1 :: $2 }
+module_head:
+| MODULE uident labels  { Incremental.open_module (add_lab $2 $3) }
 ;
 
-full_decl:
-| decl
-   { floc (), Dlogic $1 }
-| use_clone
-   { floc (), Duseclone $1 }
-| NAMESPACE namespace_import namespace_name list0_full_decl END
-   { floc_ij 1 3, Dnamespace ($3, $2, $4) }
+module_:
+| module_head list0_pdecl END  { Incremental.close_module () }
 ;
 
-list0_program_decl:
-| /* epsilon */
-   { [] }
-| list1_program_decl
-   { $1 }
+list0_pdecl:
+| /* epsilon */         { () }
+| new_decl  list0_pdecl { () }
+| new_pdecl list0_pdecl { () }
 ;
 
-list1_program_decl:
-| program_decl
-   { [$1] }
-| program_decl list1_program_decl
-   { $1 :: $2 }
+new_pdecl:
+| pdecl
+    { Incremental.new_pdecl (floc ()) $1 }
+| USE use_module
+    { Incremental.use_module (floc ()) $2 }
 ;
 
-program_decl:
-| program_decl_one
-    { floc (), $1 }
-| NAMESPACE namespace_import namespace_name list0_program_decl END
-    { floc_ij 1 3, Dnamespace ($3, $2, $4) }
+use_module:
+| imp_exp MODULE tqualid
+    { { use_theory = $3; use_as = Some (qualid_last $3); use_imp_exp = $1 } }
+| imp_exp MODULE tqualid AS uident
+    { { use_theory = $3; use_as = Some $5.id; use_imp_exp = $1 } }
+| imp_exp MODULE tqualid AS UNDERSCORE
+    { { use_theory = $3; use_as = None; use_imp_exp = $1 } }
 ;
 
-program_decl_one:
-| decl
-    { Dlogic $1 }
-| use_clone
-    { Duseclone $1 }
+pdecl:
 | LET ghost lident_rich_pgm labels list1_type_v_binder opt_cast EQUAL triple
     { Dlet (add_lab $3 $4, $2, mk_expr_i 8 (Efun ($5, cast_body $6 $8))) }
 | LET ghost lident_rich_pgm labels EQUAL FUN list1_type_v_binder ARROW triple
@@ -1082,8 +1018,6 @@ program_decl_one:
     { Dexn (add_lab $2 $3, None) }
 | EXCEPTION uident labels primitive_type
     { Dexn (add_lab $2 $3, Some $4) }
-| USE use_module
-    { $2 }
 ;
 
 lident_rich_pgm:
@@ -1098,13 +1032,6 @@ opt_semicolon:
 | SEMICOLON     {}
 ;
 
-use_module:
-| imp_exp MODULE tqualid
-    { Duse ($3, $1, Some (qualid_last $3)) }
-| imp_exp MODULE tqualid AS uident
-    { Duse ($3, $1, Some $5.id) }
-;
-
 list1_recfun_sep_and:
 | recfun                           { [ $1 ] }
 | recfun WITH list1_recfun_sep_and { $1 :: $3 }

src/parser/ptree.ml

@@ -168,8 +168,8 @@ type decl =
   | TypeDecl of type_decl list
   | LogicDecl of logic_decl list
   | IndDecl of Decl.ind_sign * ind_decl list
-  | PropDecl of loc * prop_kind * ident * lexpr
-  | Meta of loc * ident * metarg list
+  | PropDecl of prop_kind * ident * lexpr
+  | Meta of ident * metarg list
 
 (* program files *)
 
@@ -252,30 +252,24 @@ and letrec = loc * ident * ghost * binder list * variant list * triple
 
 and triple = pre * expr * post
 
-type program_decl =
-  | Dlet    of ident * ghost * expr
+type pdecl =
+  | Dlet of ident * ghost * expr
   | Dletrec of letrec list
-  | Dlogic  of decl
-  | Duseclone of use_clone
-  | Dparam  of ident * ghost * type_v
-  | Dexn    of ident * pty option
-  (* modules *)
-  | Duse    of qualid * bool option * (*as:*) string option
-  | Dnamespace of string option * (*import:*) bool * (loc * program_decl) list
-
-type theory = {
-  pth_name : ident;
-  pth_decl : (loc * program_decl) list;
+  | Dparam of ident * ghost * type_v
+  | Dexn of ident * pty option
+
+(* incremental parsing *)
+
+type incremental = {
+  open_theory     : ident -> unit;
+  close_theory    : unit -> unit;
+  open_module     : ident -> unit;
+  close_module    : unit -> unit;
+  open_namespace  : unit -> unit;
+  close_namespace : loc -> bool (*import:*) -> string option -> unit;
+  new_decl        : loc -> decl -> unit;
+  new_pdecl       : loc -> pdecl -> unit;
+  use_clone       : loc -> use_clone -> unit;
+  (* TODO: remove this once the new whyml becomes default *)
+  use_module      : loc -> use -> unit;
 }
-
-type module_ = {
-  mod_name : ident;
-  mod_decl : (loc * program_decl) list;
-}
-
-type theory_module =
-  | Ptheory of theory
-  | Pmodule of module_
-
-type program_file = theory_module list
-

src/parser/typing.ml

@@ -1103,16 +1103,16 @@ let rec clone_ns loc sl ns2 ns1 s =
   in
   { s with inst_ts = inst_ts; inst_ls = inst_ls }
 
-let add_decl th = function
+let add_decl loc th = function
   | TypeDecl dl ->
       add_types dl th
   | LogicDecl dl ->
       add_logics dl th
   | IndDecl (s, dl) ->
       add_inductives s dl th
-  | PropDecl (loc, k, s, f) ->
+  | PropDecl (k, s, f) ->
       add_prop (prop_kind k) loc s f th
-  | Meta (loc, id, al) ->
+  | Meta (id, al) ->
       let convert = function
         | PMAts q  -> MAts (find_tysymbol q th)
         | PMAfs q  -> MAls (find_fsymbol q th)
@@ -1124,8 +1124,9 @@ let add_decl th = function
       let add s = add_meta th (lookup_meta s) (List.map convert al) in
       Loc.try1 loc add id.id
 
-let add_decl th d =
-  if Debug.test_flag debug_parse_only then th else add_decl th d
+let add_decl loc th d =
+  if Debug.test_flag debug_parse_only then th else
+  Loc.try3 loc add_decl loc th d
 
 let type_inst th t s =
   let add_inst s = function
@@ -1187,16 +1188,51 @@ let add_use_clone env lenv th loc (use, subst) =
   in
   Loc.try1 loc use_or_clone th
 
-let close_theory loc lenv th =
+let close_theory lenv th =
   if Debug.test_flag debug_parse_only then lenv else
   let th = close_theory th in
   let id = th.th_name.id_string in
-  if Mstr.mem id lenv then error ~loc (ClashTheory id);
+  let loc = th.th_name.Ident.id_loc in
+  if Mstr.mem id lenv then error ?loc (ClashTheory id);
   Mstr.add id th lenv
 
 let close_namespace loc import id th =
   Loc.try3 loc close_namespace th import id
 
+(* incremental parsing *)
+
+let open_file, close_file =
+  let lenv = Stack.create () in
+  let uc   = Stack.create () in
+  let open_file env path =
+    Stack.push Mstr.empty lenv;
+    let open_theory id =
+      Stack.push (Theory.create_theory ~path (Denv.create_user_id id)) uc in
+    let close_theory () =
+      Stack.push (close_theory (Stack.pop lenv) (Stack.pop uc)) lenv in
+    let open_namespace () =
+      Stack.push (Theory.open_namespace (Stack.pop uc)) uc in
+    let close_namespace loc imp name =
+      Stack.push (close_namespace loc imp name (Stack.pop uc)) uc in
+    let new_decl loc d =
+      Stack.push (add_decl loc (Stack.pop uc) d) uc in
+    let use_clone loc use =
+      let lenv = Stack.top lenv in
+      Stack.push (add_use_clone env lenv (Stack.pop uc) loc use) uc in
+    { open_theory = open_theory;
+      close_theory = close_theory;
+      open_namespace = open_namespace;
+      close_namespace = close_namespace;
+      new_decl = new_decl;
+      use_clone = use_clone;
+      open_module = (fun _ -> assert false);
+      close_module = (fun _ -> assert false);
+      new_pdecl = (fun _ -> assert false);
+      use_module = (fun _ _ -> assert false); }
+  in
+  let close_file () = Stack.pop lenv in
+  open_file, close_file
+
 (*
 Local Variables:
 compile-command: "unset LANG; make -C ../.."

src/parser/typing.mli

@@ -30,7 +30,7 @@ val debug_type_only : Debug.flag
 
 (** incremental parsing *)
 
-val add_decl : theory_uc -> Ptree.decl -> theory_uc
+val add_decl : Loc.position -> theory_uc -> Ptree.decl -> theory_uc
 
 val add_use_clone :
   unit Env.library -> theory Mstr.t -> theory_uc ->
@@ -39,7 +39,11 @@ val add_use_clone :
 val close_namespace :
   Loc.position -> bool -> string option -> theory_uc -> theory_uc
 
-val close_theory : Loc.position -> theory Mstr.t -> theory_uc -> theory Mstr.t
+val close_theory : theory Mstr.t -> theory_uc -> theory Mstr.t
+
+val open_file : unit Env.library -> Env.pathname -> Ptree.incremental
+
+val close_file : unit -> theory Mstr.t
 
 (******************************************************************************)
 (** The following is exported for program typing (src/programs/pgm_typing.ml) *)

src/programs/pgm_main.ml

@@ -37,24 +37,37 @@ let () = Exn_printer.register (fun fmt e -> match e with
   | ClashModule m -> fprintf fmt "clash with previous module %s" m
   | _ -> raise e)
 
+type theory_ast = {
+  pth_name : Ptree.ident;
+  pth_decl : (Ptree.loc * Pgm_typing.program_decl) list;
+}
+
+type module_ast = {
+  mod_name : Ptree.ident;
+  mod_decl : (Ptree.loc * Pgm_typing.program_decl) list;
+}
+
+type theory_module_ast =
+  | Ptheory of theory_ast
+  | Pmodule of module_ast
+
 let add_theory env path lenv m =
   let id = m.pth_name in
-  let loc = id.id_loc in
   let env = Lexer.library_of_env (Env.env_of_library env) in
   let th = Theory.create_theory ~path (Denv.create_user_id id) in
   let rec add_decl th (loc,dcl) = match dcl with
-    | Dlogic d ->
-        Typing.add_decl th d
-    | Duseclone d ->
+    | Pgm_typing.PDdecl d ->
+        Typing.add_decl loc th d
+    | Pgm_typing.PDuseclone d ->
         Typing.add_use_clone env lenv th loc d
-    | Dnamespace (name, import, dl) ->
+    | Pgm_typing.PDnamespace (name, import, dl) ->
         let th = Theory.open_namespace th in
         let th = List.fold_left add_decl th dl in
         Typing.close_namespace loc import name th
-    | Dlet _ | Dletrec _ | Dparam _ | Dexn _ | Duse _ -> assert false
+    | Pgm_typing.PDpdecl _ | Pgm_typing.PDuse _ -> assert false
   in
   let th = List.fold_left add_decl th m.pth_decl in
-  close_theory loc lenv th
+  close_theory lenv th
 
 let add_module ?(type_only=false) env path (ltm, lmod) m =
   let id = m.mod_name in
@@ -75,10 +88,57 @@ let add_theory_module ?(type_only=false) env path (ltm, lmod) = function
   | Ptheory t -> add_theory env path ltm t, lmod
   | Pmodule m -> add_module ~type_only env path (ltm, lmod) m
 
+open Pgm_typing
+
+let open_file, close_file =
+  let ids  = Stack.create () in
+  let muc  = Stack.create () in
+  let lenv = Stack.create () in
+  let open_file () =
+    Stack.push [] lenv;
+    let open_theory id = Stack.push id ids; Stack.push [] muc in
+    let open_module id = Stack.push id ids; Stack.push [] muc in
+    let close_theory () =
+      let tast = { pth_name = Stack.pop ids;
+                   pth_decl = List.rev (Stack.pop muc) } in
+      Stack.push (Ptheory tast :: Stack.pop lenv) lenv in
+    let close_module () =
+      let mast = { mod_name = Stack.pop ids;
+                   mod_decl = List.rev (Stack.pop muc) } in
+      Stack.push (Pmodule mast :: Stack.pop lenv) lenv in
+    let open_namespace () = Stack.push [] muc in
+    let close_namespace loc imp name =
+      let decl = List.rev (Stack.pop muc) in
+      Stack.push ((loc, PDnamespace (name,imp,decl)) :: Stack.pop muc) muc in
+    let new_decl loc d =
+      Stack.push ((loc, PDdecl d) :: Stack.pop muc) muc in
+    let new_pdecl loc d =
+      Stack.push ((loc, PDpdecl d) :: Stack.pop muc) muc in
+    let use_clone loc use =
+      Stack.push ((loc, PDuseclone use) :: Stack.pop muc) muc in
+    let use_module loc use =
+      Stack.push ((loc, PDuse use) :: Stack.pop muc) muc in
+    { open_theory = open_theory;
+      close_theory = close_theory;
+      open_module = open_module;
+      close_module = close_module;
+      open_namespace = open_namespace;
+      close_namespace = close_namespace;
+      new_decl = new_decl;
+      new_pdecl = new_pdecl;
+      use_clone = use_clone;
+      use_module = use_module; }
+  in
+  let close_file () = List.rev (Stack.pop lenv) in
+  open_file, close_file
+
+
 let retrieve env path file c =
   let lb = Lexing.from_channel c in
   Loc.set_file file lb;
-  let ml = Lexer.parse_program_file lb in
+  let inc = open_file () in
+  Lexer.parse_program_file inc lb;
+  let ml = close_file () in
   if Debug.test_flag Typing.debug_parse_only then
     Mstr.empty, Mstr.empty
   else

src/programs/pgm_module.ml

@@ -272,14 +272,14 @@ let create_module ?(path=[]) id =
   let uc = empty_module path id in
   use_export_theory uc th_prelude
 
-let add_impure_pdecl d uc =
-  { uc with uc_impure = Typing.add_decl uc.uc_impure d }
+let add_impure_pdecl loc d uc =
+  { uc with uc_impure = Typing.add_decl loc uc.uc_impure d }
 
-let add_effect_pdecl d uc =
-  { uc with uc_effect = Typing.add_decl uc.uc_effect d; }
+let add_effect_pdecl loc d uc =
+  { uc with uc_effect = Typing.add_decl loc uc.uc_effect d; }
 
-let add_pure_pdecl d uc =
-  { uc with uc_pure = Typing.add_decl uc.uc_pure d; }
+let add_pure_pdecl loc d uc =
+  { uc with uc_pure = Typing.add_decl loc uc.uc_pure d; }
 
 let add_use_clone env ltm loc d uc =
   let env = Lexer.library_of_env (Env.env_of_library env) in

src/programs/pgm_module.mli

@@ -75,9 +75,9 @@ val add_impure_decl : Decl.decl -> uc -> uc
 val add_effect_decl : Decl.decl -> uc -> uc
 val add_pure_decl : Decl.decl -> uc -> uc
 
-val add_impure_pdecl : Ptree.decl -> uc -> uc
-val add_effect_pdecl : Ptree.decl -> uc -> uc
-val add_pure_pdecl : Ptree