incremental typing in src/parser

Makefile.in

@@ -117,7 +117,7 @@ LIB_UTIL = exn_printer debug pp loc print_tree \
 
 LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
 
-LIB_PARSER = ptree parser lexer denv typing
+LIB_PARSER = ptree denv typing parser lexer
 
 LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 	     whyconf
@@ -158,6 +158,20 @@ LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
 $(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
 $(LIBCMX): OFLAGS += -for-pack Why
 
+LIB_PARSER_POSTLUDE = \
+  "let logic_file_eof env = inside_env env logic_file_eof\n" \
+  "let list0_decl_eof env lenv uc = inside_uc env lenv uc list0_decl_eof"
+
+LIB_PARSER_INTERFACE = \
+  -e "s/^val \+logic_file_eof *:/\0 Env.env ->/" \
+  -e "s/^val \+list0_decl_eof *:/\0 Env.env -> \
+  Theory.theory Theory.Mnm.t -> Theory.theory_uc ->/"
+
+src/parser/parser.ml src/parser/parser.mli: src/parser/parser.mly
+	$(OCAMLYACC) $<
+	echo $(LIB_PARSER_POSTLUDE) >> src/parser/parser.ml
+	sed -i $(LIB_PARSER_INTERFACE) src/parser/parser.mli
+
 # build targets
 
 byte: src/why.cma

src/ide/gmain.ml

@@ -106,7 +106,7 @@ let source_text =
   close_in ic;
   buf
 
-let env = Why.Env.create_env (Why.Typing.retrieve config.loadpath)
+let env = Why.Env.create_env (Why.Lexer.retrieve config.loadpath)
 
 
 (***********************)

src/main.ml

@@ -450,7 +450,7 @@ let do_input env drv = function
 
 let () =
   try
-    let env = Env.create_env (Typing.retrieve !opt_loadpath) in
+    let env = Env.create_env (Lexer.retrieve !opt_loadpath) in
     let drv = Util.option_map (load_driver env) !opt_driver in
     Queue.iter (do_input env drv) opt_queue
   with e when not debug ->

src/parser/lexer.mli

@@ -17,12 +17,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Theory
+
 (** parsing entry points *)
 
-val parse_list0_decl : Lexing.lexbuf -> Ptree.decl list
-val parse_lexpr      : Lexing.lexbuf -> Ptree.lexpr
+val retrieve : string list -> Env.retrieve_theory
+  (** creates a new typing environment for a given loadpath *)
+
+val parse_list0_decl :
+  Env.env -> theory Mnm.t -> theory_uc -> Lexing.lexbuf -> theory_uc
 
-val parse_logic_file : Lexing.lexbuf -> Ptree.logic_file
+val parse_lexpr : Lexing.lexbuf -> Ptree.lexpr
 
 (** other functions to be re-used in other lexers/parsers *)
 

src/parser/lexer.mll

@@ -29,11 +29,14 @@
   exception IllegalCharacter of char
   exception UnterminatedComment
   exception UnterminatedString
+  exception AmbiguousPath of string * string
 
   let () = Exn_printer.register (fun fmt e -> match e with
     | IllegalCharacter c -> fprintf fmt "illegal character %c" c
     | UnterminatedComment -> fprintf fmt "unterminated comment"
     | UnterminatedString -> fprintf fmt "unterminated string"
+    | AmbiguousPath (f1, f2) ->
+        fprintf fmt "ambiguous path:@ both `%s'@ and `%s'@ match" f1 f2
     | _ -> raise e)
 
   let keywords = Hashtbl.create 97
@@ -239,10 +242,7 @@ and string = parse
   | _ as c
       { Buffer.add_char string_buf c; string lexbuf }
 
-
-
 {
-
   let with_location f lb =
     try 
       f lb 
@@ -250,11 +250,35 @@ and string = parse
       | Loc.Located _ as e -> raise e
       | e -> raise (Loc.Located (loc lb, e))
 
-  let parse_logic_file = with_location (logic_file token)
+  let parse_logic_file env = with_location (logic_file_eof env token)
+
+  let parse_list0_decl env lenv uc =
+    with_location (list0_decl_eof env lenv uc token)
+
+  let parse_lexpr = with_location (lexpr_eof token)
+
+  let read_channel env file c =
+    let lb = Lexing.from_channel c in
+    Loc.set_file file lb;
+    parse_logic_file env lb
 
-  let parse_lexpr = with_location (lexpr token)
-  let parse_list0_decl = with_location (list0_decl token)
+  let retrieve lp env sl =
+    let f = List.fold_left Filename.concat "" sl ^ ".why" in
+    let fl = List.map (fun dir -> Filename.concat dir f) lp in
+    let file = match List.filter Sys.file_exists fl with
+      | [] -> raise Not_found
+      | [file] -> file
+      | file1 :: file2 :: _ -> raise (AmbiguousPath (file1, file2))
+    in
+    let c = open_in file in
+    try
+      let tl = read_channel env file c in
+      close_in c;
+      tl
+    with
+      | e -> close_in c; raise e
 
+  let () = Env.register_format "why" ["why"] read_channel
 }
 
 (*

src/parser/parser.mly

@@ -18,6 +18,37 @@
 /**************************************************************************/
 
 %{
+  open Theory
+
+  let env_ref  = ref []
+  let lenv_ref = ref []
+  let uc_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 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 inside_uc env lenv uc rule lexer lexbuf =
+    ref_push env_ref env;
+      ref_push lenv_ref lenv;
+        ref_push uc_ref uc;
+    let res = rule lexer lexbuf in
+        ref_drop uc_ref;
+      ref_drop lenv_ref;
+    ref_drop env_ref;
+    res
 
   open Ptree
   open Parsing
@@ -93,40 +124,79 @@
 %left OP3
 %left OP4
 %nonassoc prefix_op
-%nonassoc OPPREF
 
 /* Entry points */
 
-%type <Ptree.lexpr> lexpr
-%start lexpr
-%type <Ptree.decl list> list0_decl
-%start list0_decl
-%type <Ptree.logic_file> logic_file
-%start logic_file
+%type <Ptree.lexpr> lexpr_eof
+%start lexpr_eof
+%type <Theory.theory_uc> list0_decl_eof
+%start list0_decl_eof
+%type <Theory.theory Theory.Mnm.t> logic_file_eof
+%start logic_file_eof
 %%
 
-/* File, theory, declaration */
+logic_file_eof:
+| list0_theory EOF  { ref_get lenv_ref }
+;
+
+list0_decl_eof:
+| list0_decl EOF  { ref_get uc_ref }
+;
+
+lexpr_eof:
+| lexpr EOF  { $1 }
+;
+
+/* File, theory, namespace */
 
-logic_file:
-| list1_theory EOF  { $1 }
-| EOF               { [] }
+list0_theory:
+| /* epsilon */         { () }
+| theory list0_theory   { () }
 ;
 
-list1_theory:
-| theory                { [$1] }
-| theory list1_theory   { $1 :: $2 }
+theory_head:
+| THEORY uident
+   { let id = $2 in
+     let name = Ident.id_user id.id id.id_loc in
+     ref_push uc_ref (create_theory name); id }
 ;
 
 theory:
-| THEORY uident list0_decl END
-   { { pt_loc = loc (); pt_name = $2; pt_decl = $3 } }
+| 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) }
 ;
 
 list0_decl:
-| /* epsilon */    { [] }
-| decl list0_decl  { $1 :: $2 }
+| /* epsilon */        { () }
+| new_decl 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) }
+| namespace_head namespace_import namespace_name list0_decl END
+   { ref_set uc_ref (Typing.close_namespace (loc ()) $2 $3 (ref_get uc_ref)) }
 ;
 
+namespace_head:
+| NAMESPACE
+   { ref_set uc_ref (open_namespace (ref_get uc_ref)) }
+;
+
+namespace_import:
+| /* epsilon */  { false }
+| IMPORT         { true }
+;
+
+namespace_name:
+| uident      { Some $1 }
+| UNDERSCORE  { None }
+;
+
+/* Declaration */
+
 decl:
 | TYPE list1_type_decl
     { TypeDecl $2 }
@@ -144,14 +214,6 @@ decl:
     { UseClone (loc (), $2, None) }
 | CLONE use clone_subst
     { UseClone (loc (), $2, Some $3) }
-| NAMESPACE uident list0_decl END
-    { Namespace (loc (), false, Some $2, $3) }
-| NAMESPACE UNDERSCORE list0_decl END
-    { Namespace (loc (), false, None, $3) }
-| NAMESPACE IMPORT uident list0_decl END
-    { Namespace (loc (), true, Some $3, $4) }
-| NAMESPACE IMPORT UNDERSCORE list0_decl END
-    { Namespace (loc (), true, None, $4) }
 | META ident list1_meta_arg_sep_comma
     { Meta (loc (), $2, $3) }
 | META STRING list1_meta_arg_sep_comma

src/parser/ptree.ml

@@ -144,14 +144,5 @@ type decl =
   | IndDecl of ind_decl list
   | PropDecl of loc * prop_kind * ident * lexpr
   | UseClone of loc * use * clone_subst list option
-  | Namespace of loc * bool * ident option * decl list
   | Meta of loc * ident * metarg list
 
-type theory = {
-  pt_loc  : loc;
-  pt_name : ident;
-  pt_decl : decl list;
-}
-
-type logic_file = theory list
-

src/parser/typing.ml

@@ -40,11 +40,6 @@ exception TermExpected
 exception BadNumberOfArguments of Ident.ident * int * int
 exception ClashTheory of string
 exception UnboundTheory of qualid
-exception AlreadyTheory of string
-exception UnboundFile of string
-exception UnboundDir of string
-exception AmbiguousPath of string * string
-exception NotInLoadpath of string
 exception CyclicTypeDef
 exception UnboundTypeVar of string
 exception UnboundType of string list
@@ -90,16 +85,6 @@ let () = Exn_printer.register (fun fmt e -> match e with
       fprintf fmt "clash with previous theory %s" s
   | UnboundTheory q ->
       fprintf fmt "unbound theory %a" print_qualid q
-  | AlreadyTheory s ->
-      fprintf fmt "already using a theory with name %s" s
-  | UnboundFile s ->
-      fprintf fmt "no such file %s" s
-  | UnboundDir s ->
-      fprintf fmt "no such directory %s" s
-  | AmbiguousPath (f1, f2) ->
-      fprintf fmt "@[ambiguous path:@ both `%s'@ and `%s'@ match@]" f1 f2
-  | NotInLoadpath f ->
-      fprintf fmt "cannot find `%s' in loadpath" f
   | CyclicTypeDef ->
       fprintf fmt "cyclic type definition"
   | UnboundTypeVar s ->
@@ -110,6 +95,9 @@ let () = Exn_printer.register (fun fmt e -> match e with
        fprintf fmt "Unbound symbol '%a'" (print_list dot pp_print_string) sl
   | _ -> raise e)
 
+let debug_parse_only = Debug.register_flag "parse_only"
+let debug_type_only  = Debug.register_flag "type_only"
+
 (** Environments *)
 
 (** typing using destructive type variables
@@ -184,7 +172,7 @@ let ts_tuple n = Hashtbl.replace tuples_needed n (); ts_tuple n
 let fs_tuple n = Hashtbl.replace tuples_needed n (); fs_tuple n
 
 let add_tuple_decls uc =
-  Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n)) 
+  Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n))
     tuples_needed uc
 
 let with_tuples ?(reset=false) f uc x =
@@ -259,7 +247,7 @@ let specialize_psymbol p uc =
     | None -> s, tl
     | Some _ -> let loc = qloc p in error ~loc PredicateExpected
 
-let is_psymbol p uc = 
+let is_psymbol p uc =
   let s = find_lsymbol p uc in
   s.ls_value = None
 
@@ -585,12 +573,12 @@ let add_projections th d = match d.td_def with
 open Ptree
 
 let add_types dl th =
-  let def = List.fold_left 
+  let def = List.fold_left
     (fun def d ->
-      let id = d.td_ident.id in 
+      let id = d.td_ident.id in
       if Mstr.mem id def then error ~loc:d.td_loc (Clash id);
-      Mstr.add id d def) 
-    Mstr.empty dl 
+      Mstr.add id d def)
+    Mstr.empty dl
   in
   let tysymbols = Hashtbl.create 17 in
   let rec visit x =
@@ -645,7 +633,7 @@ let add_types dl th =
       Hashtbl.add tysymbols x (Some ts);
       ts
   in
-  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in 
+  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in
   let th' = try add_ty_decl th tsl
     with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
   in
@@ -752,7 +740,7 @@ let add_logics dl th =
 	      let loc = t.pp_loc in
 	      let ty = dty denv ty in
 	      let t = dterm denv t in
-	      if not (unify t.dt_ty ty) then 
+	      if not (unify t.dt_ty ty) then
 		term_expected_type ~loc t.dt_ty ty;
               let vl = match fs.ls_value with
                 | Some _ -> mk_vlist fs.ls_args
@@ -821,18 +809,7 @@ let add_inductives dl th =
   | TooSpecificIndDecl (_,pr,t) -> errorm ~loc:(loc_of_id pr.pr_name)
       "term @[%a@] is too specific" Pretty.print_term t
 
-(* parse file and store all theories into parsed_theories *)
-
-let load_channel file c =
-  let lb = Lexing.from_channel c in
-  Loc.set_file file lb;
-  Lexer.parse_logic_file lb
-
-let load_file file =
-  let c = open_in file in
-  let tl = load_channel file c in
-  close_in c;
-  tl
+(* parse declarations *)
 
 let prop_kind = function
   | Kaxiom -> Paxiom
@@ -848,15 +825,7 @@ let find_theory env lenv q id = match q with
       (* theory in file f *)
       find_theory env q id
 
-let rec type_theory env lenv id pt =
-  let n = id_user id.id id.id_loc in
-  let th = create_theory n in
-  let th = add_decls env lenv th pt.pt_decl in
-  close_theory th
-
-and add_decls env lenv th = List.fold_left (add_decl env lenv) th
-
-and add_decl env lenv th = function
+let add_decl env lenv th = function
   | TypeDecl dl ->
       add_types dl th
   | LogicDecl dl ->
@@ -872,7 +841,6 @@ and add_decl env lenv th = function
 	  find_theory env lenv q id
 	with
 	  | TheoryNotFound _ -> error ~loc (UnboundTheory use.use_theory)
-	  | AmbiguousPath _ as e -> error ~loc e
       in
       let use_or_clone th = match subst with
 	| None ->
@@ -925,12 +893,6 @@ and add_decl env lenv th = function
 	    use_or_clone th
       with ClashSymbol s -> error ~loc (Clash s)
       end
-  | Namespace (loc, import, name, dl) ->
-      let th = open_namespace th in
-      let th = add_decls env lenv th dl in
-      let id = option_map (fun id -> id.id) name in
-      begin try close_namespace th import id
-      with ClashSymbol s -> error ~loc (Clash s) end
   | Meta (loc, id, al) ->
       let s = id.id in
       let convert = function
@@ -944,46 +906,19 @@ and add_decl env lenv th = function
       begin try add_meta th (lookup_meta s) al
       with e -> raise (Loc.Located (loc,e)) end
 
-and type_and_add_theory env lenv pt =
-  let id = pt.pt_name in
-  if Mnm.mem id.id lenv || id.id = builtin_theory.th_name.id_string
-    then error (ClashTheory id.id);
-  let th = type_theory env lenv id pt in
-  Mnm.add id.id th lenv
-
-let type_theories env tl =
-  List.fold_left (type_and_add_theory env) Mnm.empty tl
+let add_decl env lenv th d =
+  if Debug.test_flag debug_parse_only then th else
+  add_decl env lenv th d
 
-let read_file env file =
-  let tl = load_file file in
-  type_theories env tl
+let close_theory lenv { id = id ; id_loc = loc } th =
+  if Mnm.mem id lenv then error ~loc (ClashTheory id);
+  if Debug.test_flag debug_parse_only then lenv else
+  Mnm.add id (close_theory th) lenv
 
-let debug_parse_only = Debug.register_flag "parse_only"
-let debug_type_only  = Debug.register_flag "type_only"
-
-let read_channel env file ic =
-  let tl = load_channel file ic in
-  if Debug.test_flag debug_parse_only then Mnm.empty else
-  let tl = type_theories env tl in
-  if Debug.test_flag debug_type_only then Mnm.empty else
-  tl
-
-let locate_file lp sl =
-  let f = List.fold_left Filename.concat "" sl ^ ".why" in
-  let fl = List.map (fun dir -> Filename.concat  dir f) lp in
-  match List.filter Sys.file_exists fl with
-    | [] -> raise Not_found
-    | [file] -> file
-    | file1 :: file2 :: _ -> error (AmbiguousPath (file1, file2))
-
-let retrieve lp env sl =
-  let file = locate_file lp sl in
-  read_file env file
-
-
-(** register Why parser *)
-
-let () = Env.register_format "why" ["why"] read_channel
+let close_namespace loc import name th =
+  let id = option_map (fun id -> id.id) name in
+  try close_namespace th import id
+  with ClashSymbol s -> error ~loc (Clash s)
 
 (*
 Local Variables:

src/parser/typing.mli

@@ -23,29 +23,30 @@ open Util
 open Ty
 open Term
 open Theory
-open Env
 
 val debug_parse_only : Debug.flag
 val debug_type_only : Debug.flag
 
-val retrieve : string list -> retrieve_theory
-  (** creates a new typing environment for a given loadpath *)
-
 (** incremental parsing *)
 
-val add_decl : env -> theory Mnm.t -> theory_uc -> Ptree.decl -> theory_uc
+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
 
 (******************************************************************************)
 (** The following is exported for program typing (src/programs/pgm_typing.ml) *)
 (******************************************************************************)
 
-val specialize_fsymbol : 
+val specialize_fsymbol :
   Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty
 
-val specialize_psymbol : 
+val specialize_psymbol :
   Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list
 
-val specialize_tysymbol : 
+val specialize_tysymbol :
   Loc.position -> Ptree.qualid -> theory_uc -> Ty.tysymbol * int
 
 type denv
@@ -72,6 +73,6 @@ val qloc : Ptree.qualid -> Loc.position
 val ts_tuple : int -> Ty.tysymbol
 val fs_tuple : int -> Term.lsymbol
 
-val with_tuples : 
+val with_tuples :
   ?reset:bool -> (theory_uc -> 'a -> 'b) -> theory_uc -> 'a -> 'b
 

src/programs/pgm_env.ml

@@ -160,6 +160,24 @@ let purify env v =
   let tyl, ty = uncurry_type v in 
   make_arrow_type env tyl ty
 
+(* parsing LOGIC strings using functions from src/parser/
+   requires proper relocation *)
+
+let reloc loc lb =
+  lb.Lexing.lex_curr_p <- loc;
+  lb.Lexing.lex_abs_pos <- loc.Lexing.pos_cnum
+
+let parse_string f loc s =
+  let lb = Lexing.from_string s in
+  reloc loc lb;
+  f lb
+
+let logic_lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s
+
+let logic_decls (loc, s) e env =
+  let parse = Lexer.parse_list0_decl e Mnm.empty env.uc in
+  { env with uc = parse_string parse loc s }
+
 (* addition *)
 
 let add_global id tyv env = 
@@ -170,9 +188,6 @@ let add_global id tyv env =
 let add_decl d env = 
   { env with uc = Typing.with_tuples add_decl env.uc d }
 
-let add_pdecl e d env =
-  { env with uc = Typing.add_decl e Mnm.empty env.uc d }
-
 let add_exception id ty env =
   let tyl = match ty with None -> [] | Some ty -> [ty] in
   let s = create_lsymbol id tyl (Some (ty_app env.ts_exn [])) in

src/programs/pgm_env.mli

@@ -62,7 +62,10 @@ val empty_env : theory_uc -> env
 val add_global : preid -> type_v -> env -> lsymbol * env
 
 val add_decl : decl -> env -> env
-val add_pdecl : Env.env -> Ptree.decl -> env -> env
+
+val logic_lexpr : Lexing.position * string -> Ptree.lexpr
+
+val logic_decls : Lexing.position * string -> Env.env -> env -> env
 
 val add_exception : preid -> ty option -> env -> lsymbol * env
 

src/programs/pgm_typing.ml

@@ -56,22 +56,6 @@ let () = Exn_printer.register (fun fmt e -> match e with
 
 let id_result = "result"
 
-(* parsing LOGIC strings using functions from src/parser/
-   requires proper relocation *)
-
-let reloc loc lb =
-  lb.Lexing.lex_curr_p <- loc;
-  lb.Lexing.lex_abs_pos <- loc.Lexing.pos_cnum
-    
-let parse_string f loc s =
-  let lb = Lexing.from_string s in
-  reloc loc lb;
-  f lb
-
-let logic_list0_decl (loc, s) = parse_string Lexer.parse_list0_decl loc s
-  
-let lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s
-
 (* phase 1: typing programs (using destructive type inference) **************)
 
 let dty_app (ts, tyl) = assert (ts.ts_def = None); Tyapp (ts, tyl)
@@ -213,8 +197,8 @@ let deffect env e =
       List.map (fun id -> let ls,_,_ = dexception env id in ls) 
 	e.Pgm_ptree.pe_raises; }
 
-let dterm env l = Typing.dterm env (lexpr l)
-let dfmla env l = Typing.dfmla env (lexpr l)
+let dterm env l = Typing.dterm env (Pgm_env.logic_lexpr l)
+let dfmla env l = Typing.dfmla env (Pgm_env.logic_lexpr l)
 
 let dpost env ty (q, ql) =
   let dexn (id, l) =
@@ -1206,11 +1190,8 @@ let cannot_be_generalized gl = function
       false
 
 let decl env gl = function
-  | Pgm_ptree.Dlogic dl -> 
-      let dl = logic_list0_decl dl in
-      let add1 gl d = Pgm_env.add_pdecl env d gl in
-      let gl = List.fold_left add1 gl dl in
-      gl, []
+  | Pgm_ptree.Dlogic dl ->
+      Pgm_env.logic_decls dl env gl, []