Parser: refactoring

src/parser/parser.mly

@@ -16,7 +16,9 @@
   let prefix s = "prefix " ^ s
   let mixfix s = "mixfix " ^ s
 
-  let qualid_last = function Qident x | Qdot (_, x) -> x.id_str
+  let qualid_last = function Qident x | Qdot (_, x) -> x
+
+  let use_as q = function Some x -> x | None -> qualid_last q
 
   let floc s e = Loc.extract (s,e)
 
@@ -91,9 +93,9 @@
 (* Tokens *)
 
 %token <string> LIDENT UIDENT
-%token <Ptree.integer_constant> INTEGER
+%token <Number.integer_constant> INTEGER
 %token <string> OP1 OP2 OP3 OP4 OPPREF
-%token <Ptree.real_constant> FLOAT
+%token <Number.real_constant> FLOAT
 %token <string> STRING
 %token <Loc.position> POSITION
 %token <string> QUOTE_LIDENT
@@ -179,32 +181,40 @@ module_head:
 | THEORY labels(uident)  { Typing.open_module $2 }
 | MODULE labels(uident)  { Typing.open_module $2 }
 
+scope_head:
+| SCOPE boption(IMPORT) uident
+    { Typing.open_namespace (floc $startpos $endpos) $3; $2 }
+
 module_decl:
-| decl            { Typing.add_decl  (floc $startpos $endpos) $1 }
-| use_clone       { Typing.use_clone (floc $startpos $endpos) $1 }
-| namespace_head module_decl* END
+| scope_head module_decl* END
     { Typing.close_namespace (floc $startpos($1) $endpos($1)) ~import:$1 }
-
-namespace_head:
-| SCOPE boption(IMPORT) uident  { Typing.open_namespace $3; $2 }
+| d = pure_decl | d = prog_decl | d = meta_decl
+    { Typing.add_decl (floc $startpos $endpos) d }
+| use_clone { () }
 
 (* Use and clone *)
 
 use_clone:
-| USE use                                 { ($2, None) }
-| CLONE use                               { ($2, Some []) }
-| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
-
-use:
-| boption(IMPORT) tqualid
-    { { use_module = $2; use_import = Some ($1, qualid_last $2) } }
-| boption(IMPORT) tqualid AS uident
-    { { use_module = $2; use_import = Some ($1, $4.id_str) } }
-| EXPORT tqualid
-    { { use_module = $2; use_import = None } }
+| USE EXPORT tqualid
+    { Typing.add_decl (floc $startpos $endpos) (Duse $3) }
+| CLONE EXPORT tqualid clone_subst
+    { Typing.add_decl (floc $startpos $endpos) (Dclone ($3, $4)) }
+| USE boption(IMPORT) tqualid option(preceded(AS, uident))
+    { let loc = floc $startpos $endpos in
+      Typing.open_namespace loc (use_as $3 $4);
+      Typing.add_decl loc (Duse $3);
+      Typing.close_namespace loc ~import:$2 }
+| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst
+    { let loc = floc $startpos $endpos in
+      Typing.open_namespace loc (use_as $3 $4);
+      Typing.add_decl loc (Dclone ($3, $5));
+      Typing.close_namespace loc ~import:$2 }
 
 clone_subst:
-| SCOPE     ns     EQUAL ns     { CSns    (floc $startpos $endpos, $2,$4) }
+| (* epsilon *)                         { [] }
+| WITH comma_list1(single_clone_subst)  { $2 }
+
+single_clone_subst:
 | TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
 | CONSTANT  qualid EQUAL qualid { CSfsym  (floc $startpos $endpos, $2,$4) }
 | FUNCTION  qualid EQUAL qualid { CSfsym  (floc $startpos $endpos, $2,$4) }
@@ -213,24 +223,10 @@ clone_subst:
 | LEMMA     qualid              { CSlemma (floc $startpos $endpos, $2) }
 | GOAL      qualid              { CSgoal  (floc $startpos $endpos, $2) }
 
-ns:
-| uqualid { Some $1 }
-| DOT     { None }
+(* Meta declarations *)
 
-(* Theory declarations *)
-
-decl:
-| TYPE with_list1(type_decl)                { Dtype $2 }
-| CONSTANT  constant_decl                   { Dlogic [$2] }
-| FUNCTION  function_decl  with_logic_decl* { Dlogic ($2::$3) }
-| PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) }
-| INDUCTIVE   with_list1(inductive_decl)    { Dind (Decl.Ind, $2) }
-| COINDUCTIVE with_list1(inductive_decl)    { Dind (Decl.Coind, $2) }
-| AXIOM labels(ident) COLON term            { Dprop (Decl.Paxiom, $2, $4) }
-| LEMMA labels(ident) COLON term            { Dprop (Decl.Plemma, $2, $4) }
-| GOAL  labels(ident) COLON term            { Dprop (Decl.Pgoal, $2, $4) }
-| META sident comma_list1(meta_arg)         { Dmeta ($2, $3) }
-| pdecl                                     { $1 }
+meta_decl:
+| META sident comma_list1(meta_arg)  { Dmeta ($2, $3) }
 
 meta_arg:
 | TYPE      ty      { Mty $2 }
@@ -243,6 +239,19 @@ meta_arg:
 | STRING            { Mstr $1 }
 | INTEGER           { Mint (small_integer $1) }
 
+(* Theory declarations *)
+
+pure_decl:
+| TYPE with_list1(type_decl)                { Dtype $2 }
+| CONSTANT  constant_decl                   { Dlogic [$2] }
+| FUNCTION  function_decl  with_logic_decl* { Dlogic ($2::$3) }
+| PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) }
+| INDUCTIVE   with_list1(inductive_decl)    { Dind (Decl.Ind, $2) }
+| COINDUCTIVE with_list1(inductive_decl)    { Dind (Decl.Coind, $2) }
+| AXIOM labels(ident) COLON term            { Dprop (Decl.Paxiom, $2, $4) }
+| LEMMA labels(ident) COLON term            { Dprop (Decl.Plemma, $2, $4) }
+| GOAL  labels(ident) COLON term            { Dprop (Decl.Pgoal, $2, $4) }
+
 (* Type declarations *)
 
 type_decl:
@@ -584,7 +593,7 @@ numeral:
 
 (* Program declarations *)
 
-pdecl:
+prog_decl:
 | VAL ghost kind labels(lident_rich) mk_expr(val_defn) { Dlet ($4, $2, $3, $5) }
 | LET ghost kind labels(lident_rich) mk_expr(fun_defn) { Dlet ($4, $2, $3, $5) }
 | LET ghost kind labels(lident_rich) EQUAL seq_expr    { Dlet ($4, $2, $3, $6) }

src/parser/ptree.ml

@@ -11,14 +11,6 @@
 
 (*s Parse trees. *)
 
-type loc = Loc.position
-
-(*s Logical terms and formulas *)
-
-type integer_constant = Number.integer_constant
-type real_constant = Number.real_constant
-type constant = Number.constant
-
 type label =
   | Lstr of Ident.label
   | Lpos of Loc.position
@@ -26,9 +18,11 @@ type label =
 type ident = {
   id_str : string;
   id_lab : label list;
-  id_loc : loc;
+  id_loc : Loc.position;
 }
 
+(*s Types *)
+
 type qualid =
   | Qident of ident
   | Qdot of qualid * ident
@@ -40,14 +34,11 @@ type pty =
   | PTarrow of pty * pty
   | PTparen of pty
 
-type ghost = bool
-
-type binder = loc * ident option * ghost * pty option
-type param  = loc * ident option * ghost * pty
+(*s Patterns *)
 
 type pattern = {
   pat_desc : pat_desc;
-  pat_loc  : loc;
+  pat_loc  : Loc.position;
 }
 
 and pat_desc =
@@ -60,15 +51,22 @@ and pat_desc =
   | Pas of pattern * ident
   | Pcast of pattern * pty
 
+(*s Logical terms and formulas *)
+
+type ghost = bool
+
+type binder = Loc.position * ident option * ghost * pty option
+type param  = Loc.position * ident option * ghost * pty
+
 type term = {
   term_desc : term_desc;
-  term_loc  : loc;
+  term_loc  : Loc.position;
 }
 
 and term_desc =
   | Ttrue
   | Tfalse
-  | Tconst of constant
+  | Tconst of Number.constant
   | Tident of qualid
   | Tidapp of qualid * term list
   | Tapply of term * term
@@ -88,84 +86,14 @@ and term_desc =
   | Tupdate of term * (qualid * term) list
   | Tat of term * ident
 
-(*s Declarations. *)
-
-type use = {
-  use_module : qualid;
-  use_import : (bool (* import *) * string (* as *)) option;
-}
-
-type clone_subst =
-  | CSns    of loc * qualid option * qualid option
-  | CStsym  of loc * qualid * ident list * pty
-  | CSfsym  of loc * qualid * qualid
-  | CSpsym  of loc * qualid * qualid
-  | CSvsym  of loc * qualid * qualid
-  | CSlemma of loc * qualid
-  | CSgoal  of loc * qualid
-
-type field = {
-  f_loc     : loc;
-  f_ident   : ident;
-  f_pty     : pty;
-  f_mutable : bool;
-  f_ghost   : bool
-}
-
-type type_def =
-  | TDabstract
-  | TDalias     of pty
-  | TDalgebraic of (loc * ident * param list) list
-  | TDrecord    of field list
-
-type visibility = Public | Private | Abstract (* = Private + ghost fields *)
+(*s Program expressions *)
 
 type invariant = term list
-
-type type_decl = {
-  td_loc    : loc;
-  td_ident  : ident;
-  td_params : ident list;
-  td_vis    : visibility; (* records only *)
-  td_mut    : bool;       (* records or abstract types *)
-  td_inv    : invariant;  (* records only *)
-  td_def    : type_def;
-}
-
-type logic_decl = {
-  ld_loc    : loc;
-  ld_ident  : ident;
-  ld_params : param list;
-  ld_type   : pty option;
-  ld_def    : term option;
-}
-
-type ind_decl = {
-  in_loc    : loc;
-  in_ident  : ident;
-  in_params : param list;
-  in_def    : (loc * ident * term) list;
-}
-
-type metarg =
-  | Mty  of pty
-  | Mfs  of qualid
-  | Mps  of qualid
-  | Max  of qualid
-  | Mlm  of qualid
-  | Mgl  of qualid
-  | Mstr of string
-  | Mint of int
-
-type use_clone = use * clone_subst list option
-
-(* program files *)
-
 type variant = (term * qualid option) list
 
 type pre = term
-type post = loc * (pattern * term) list
-type xpost = loc * (qualid * pattern * term) list
+type post = Loc.position * (pattern * term) list
+type xpost = Loc.position * (qualid * pattern * term) list
 
 type spec = {
   sp_pre     : pre list;
@@ -180,13 +108,13 @@ type spec = {
 
 type expr = {
   expr_desc : expr_desc;
-  expr_loc  : loc;
+  expr_loc  : Loc.position;
 }
 
 and expr_desc =
   | Etrue
   | Efalse
-  | Econst of constant
+  | Econst of Number.constant
   (* lambda-calculus *)
   | Eident of qualid
   | Eidapp of qualid * expr list
@@ -223,12 +151,75 @@ and expr_desc =
 and fundef =
   ident * ghost * Expr.rs_kind * binder list * pty option * spec * expr
 
+(*s Declarations *)
+
+type field = {
+  f_loc     : Loc.position;
+  f_ident   : ident;
+  f_pty     : pty;
+  f_mutable : bool;
+  f_ghost   : bool
+}
+
+type type_def =
+  | TDabstract
+  | TDalias     of pty
+  | TDalgebraic of (Loc.position * ident * param list) list
+  | TDrecord    of field list
+
+type visibility = Public | Private | Abstract (* = Private + ghost fields *)
+
+type type_decl = {
+  td_loc    : Loc.position;
+  td_ident  : ident;
+  td_params : ident list;
+  td_vis    : visibility; (* records only *)
+  td_mut    : bool;       (* records or abstract types *)
+  td_inv    : invariant;  (* records only *)
+  td_def    : type_def;
+}
+
+type logic_decl = {
+  ld_loc    : Loc.position;
+  ld_ident  : ident;
+  ld_params : param list;
+  ld_type   : pty option;
+  ld_def    : term option;
+}
+
+type ind_decl = {
+  in_loc    : Loc.position;
+  in_ident  : ident;
+  in_params : param list;
+  in_def    : (Loc.position * ident * term) list;
+}
+
+type metarg =
+  | Mty  of pty
+  | Mfs  of qualid
+  | Mps  of qualid
+  | Max  of qualid
+  | Mlm  of qualid
+  | Mgl  of qualid
+  | Mstr of string
+  | Mint of int
+
+type clone_subst =
+  | CStsym  of Loc.position * qualid * ident list * pty
+  | CSfsym  of Loc.position * qualid * qualid
+  | CSpsym  of Loc.position * qualid * qualid
+  | CSvsym  of Loc.position * qualid * qualid
+  | CSlemma of Loc.position * qualid
+  | CSgoal  of Loc.position * qualid
+
 type decl =
   | Dtype of type_decl list
   | Dlogic of logic_decl list
   | Dind of Decl.ind_sign * ind_decl list
   | Dprop of Decl.prop_kind * ident * term
-  | Dmeta of ident * metarg list
   | Dlet of ident * ghost * Expr.rs_kind * expr
   | Drec of fundef list
   | Dexn of ident * pty
+  | Dmeta of ident * metarg list
+  | Dclone of qualid * clone_subst list
+  | Duse of qualid

src/parser/typing.ml

@@ -966,7 +966,15 @@ let add_prop muc k s f =
 
 (* parse declarations *)
 
-let add_decl muc d =
+let find_module env file q =
+  let m = match q with
+    | Qident {id_str = nm} ->
+        (try Mstr.find nm file with Not_found -> read_module env [] nm)
+    | Qdot (p, {id_str = nm}) -> read_module env (string_list_of_qualid p) nm in
+  if Debug.test_flag Glob.flag then Glob.use (qloc_last q) m.mod_theory.th_name;
+  m
+
+let add_decl muc env file d =
   let vc = muc.muc_path = [] &&
     Debug.test_noflag debug_type_only in
   match d with
@@ -1002,6 +1010,12 @@ let add_decl muc d =
       let ity = ity_of_pty muc pty in
       let xs = create_xsymbol (create_user_id id) ity in
       add_pdecl ~vc muc (create_exn_decl xs)
+  | Ptree.Duse use ->
+      use_export muc (find_module env file use)
+  | Ptree.Dclone (use, _subst) ->
+      let m = find_module env file use in
+      warn_clone_not_abstract (qloc use) m.mod_theory;
+      Loc.errorm "cloning coming soon" (* TODO *)
 
 (* TODO
 let rec clone_ns kn sl path ns2 ns1 s =
@@ -1111,32 +1125,6 @@ let type_inst tuc t s =
   List.fold_left add_inst empty_inst s
 *)
 
-let use_clone loc muc env file (use, subst) =
-  let find_module env file q = match q with
-    | Qident { id_str = id } -> (* local module *)
-        begin try Mstr.find id file
-        with Not_found -> read_module env [] id end
-    | Qdot (p, { id_str = id }) -> (* module in file f *)
-        read_module env (string_list_of_qualid p) id in
-  let use_or_clone muc =
-    let m = find_module env file use.use_module in
-    if Debug.test_flag Glob.flag then
-      Glob.use (qloc_last use.use_module) m.mod_theory.th_name;
-    match subst with
-    | None -> use_export muc m
-    | Some _ ->
-        warn_clone_not_abstract loc m.mod_theory;
-        Loc.errorm ~loc "cloning coming soon" (* TODO *)
-  in
-  match use.use_import with
-  | Some (import, use_as) ->
-      (* use T = namespace T use_export T end *)
-      let muc = open_namespace muc use_as in
-      let muc = use_or_clone muc in
-      close_namespace muc ~import
-  | None ->
-      use_or_clone muc
-
 (* incremental parsing *)
 
 type slice = {
@@ -1174,11 +1162,22 @@ let close_module loc =
   end;
   slice.muc <- None
 
-let open_namespace nm =
-  assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
+let top_muc_on_demand loc slice = 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
+
+let open_namespace loc nm =
+  assert (not (Stack.is_empty state));
+  let slice = Stack.top state in
+  let muc = top_muc_on_demand loc slice in
   if Debug.test_noflag debug_parse_only then
-    let slice = Stack.top state in
-    slice.muc <- Some (open_namespace (Opt.get slice.muc) nm.id_str)
+    slice.muc <- Some (open_namespace muc nm.id_str)
 
 let close_namespace loc ~import =
   assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
@@ -1190,25 +1189,9 @@ let close_namespace loc ~import =
 let add_decl loc d =
   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
+  let muc = top_muc_on_demand loc slice in
   if Debug.test_noflag debug_parse_only then
-    let muc = Loc.try2 ~loc add_decl muc d in
-    slice.muc <- Some muc
-
-let use_clone loc use =
-  assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
-  if Debug.test_noflag debug_parse_only then
-    let slice = Stack.top state in
-    let muc = Loc.try5 ~loc use_clone loc
-      (Opt.get slice.muc) slice.env slice.file use in
+    let muc = Loc.try4 ~loc add_decl muc slice.env slice.file d in
     slice.muc <- Some muc
 
 (** Exception printing *)

src/parser/typing.mli

@@ -19,12 +19,10 @@ val close_file : unit -> Pmodule.pmodule Stdlib.Mstr.t
 
 val open_module : Ptree.ident -> unit
 
-val close_module : Ptree.loc -> unit
+val close_module : Loc.position -> unit
 
-val open_namespace : Ptree.ident -> unit
+val open_namespace : Loc.position -> Ptree.ident -> unit
 
-val close_namespace : Ptree.loc -> import:bool -> unit
+val close_namespace : Loc.position -> import:bool -> unit
 
-val add_decl : Ptree.loc -> Ptree.decl -> unit
-
-val use_clone : Ptree.loc -> Ptree.use_clone -> unit
+val add_decl : Loc.position -> Ptree.decl -> unit