Mlw: cloning (wip)

src/core/theory.ml

@@ -287,8 +287,6 @@ let close_theory uc = match uc.uc_export with
   | _ -> raise CloseTheory
 
 let get_namespace uc = List.hd uc.uc_import
-let get_known uc = uc.uc_known
-let get_rev_decls uc = uc.uc_decls
 
 let open_namespace uc s = match uc.uc_import with
   | ns :: _ -> { uc with

src/core/theory.mli

@@ -116,7 +116,17 @@ val td_hash : tdecl -> int
 
 (** {2 Constructors and utilities} *)
 
-type theory_uc  (** a theory under construction *)
+type theory_uc = private {
+  uc_name   : ident;
+  uc_path   : string list;
+  uc_decls  : tdecl list;
+  uc_prefix : string list;
+  uc_import : namespace list;
+  uc_export : namespace list;
+  uc_known  : known_map;
+  uc_local  : Sid.t;
+  uc_used   : Sid.t;
+}
 
 val create_theory : ?path:string list -> preid -> theory_uc
 val close_theory  : theory_uc -> theory
@@ -125,8 +135,6 @@ val open_namespace  : theory_uc -> string -> theory_uc
 val close_namespace : theory_uc -> bool (* import *) -> theory_uc
 
 val get_namespace : theory_uc -> namespace
-val get_known : theory_uc -> known_map
-val get_rev_decls : theory_uc -> tdecl list
 
 val restore_path : ident -> string list * string * string list
 (** [restore_path id] returns the triple (library path, theory,

src/mlw/pdecl.ml

@@ -440,7 +440,9 @@ let create_exn_decl xs =
     "The type of top-level exception %a has mutable components" print_xs xs;
   mk_decl (PDexn xs) []
 
-let create_pure_decl d = mk_decl PDpure [d]
+let create_pure_decl d = match d.d_node with
+  | Dtype _ | Ddata _ -> invalid_arg "Pdecl.create_pure_decl"
+  | Dparam _ | Dlogic _ | Dind _ | Dprop _ -> mk_decl PDpure [d]
 
 (** {2 Built-in decls} *)
 

src/mlw/pmodule.mli

@@ -11,6 +11,9 @@
 
 open Stdlib
 open Ident
+open Ty
+open Term
+open Decl
 open Theory
 open Ity
 open Expr
@@ -42,22 +45,36 @@ val ns_find_ns  : namespace -> string list -> namespace
 (** {2 Module} *)
 
 type pmodule = private {
-  mod_theory : theory;      (* pure theory *)
-  mod_decls  : pdecl list;  (* module declarations *)
-  mod_export : namespace;   (* exported namespace *)
-  mod_known  : known_map;   (* known identifiers *)
-  mod_local  : Sid.t;       (* locally declared idents *)
-  mod_used   : Sid.t;       (* used modules *)
+  mod_theory : theory;        (* pure theory *)
+  mod_units  : mod_unit list; (* module declarations *)
+  mod_export : namespace;     (* exported namespace *)
+  mod_known  : known_map;     (* known identifiers *)
+  mod_local  : Sid.t;         (* locally declared idents *)
+  mod_used   : Sid.t;         (* used modules *)
+}
+
+and mod_unit =
+  | Udecl  of pdecl
+  | Uuse   of pmodule
+  | Uinst  of mod_inst
+  | Umeta  of meta * meta_arg list
+  | Uscope of string * bool * mod_unit list
+
+and mod_inst = private {
+  mi_mod : pmodule;
+  mi_ts  : itysymbol Mts.t;
+  mi_ls  : lsymbol Mls.t;
+  mi_pr  : prsymbol Mpr.t;
+  mi_pv  : pvsymbol Mpv.t;
+  mi_rs  : rsymbol Mrs.t;
+  mi_xs  : xsymbol Mexn.t;
 }
 
 (** {2 Module under construction} *)
 
 type pmodule_uc = private {
   muc_theory : theory_uc;
-  muc_name   : string;
-  muc_path   : string list;
-  muc_decls  : pdecl list;
-  muc_prefix : string list;
+  muc_units  : mod_unit list;
   muc_import : namespace list;
   muc_export : namespace list;
   muc_known  : known_map;
@@ -88,6 +105,8 @@ val restore_module : theory -> pmodule
 
 val use_export : pmodule_uc -> pmodule -> pmodule_uc
 
+val clone_export : pmodule_uc -> pmodule -> Theory.th_inst -> pmodule_uc
+
 (** {2 Logic decls} *)
 
 val add_meta : pmodule_uc -> meta -> meta_arg list -> pmodule_uc
@@ -119,3 +138,8 @@ val mlw_language_builtin : pathname -> mlw_file
 exception ModuleNotFound of pathname * string
 
 val read_module : env -> pathname -> string -> pmodule
+
+(** {2 Pretty-printing} *)
+
+val print_unit : Format.formatter -> mod_unit -> unit
+val print_module : Format.formatter -> pmodule -> unit

src/parser/lexer.mll

@@ -233,12 +233,9 @@ rule token = parse
     Typing.open_file env path;
     let mm = Loc.with_location (mlw_file token) lb in
     if path = [] && Debug.test_flag debug then begin
+      let print_m _ m = Format.eprintf "%a@\n@." print_module m in
       let add_m _ m mm = Mid.add m.mod_theory.th_name m mm in
-      let mm = Mstr.fold add_m mm Mid.empty in
-      let print_m _ m = Format.eprintf
-        "@[<hov 2>module %a@\n%a@]@\nend@\n@." Pretty.print_th m.mod_theory
-        (Pp.print_list Pp.newline2 Pdecl.print_pdecl) m.mod_decls in
-      Mid.iter print_m mm
+      Mid.iter print_m (Mstr.fold add_m mm Mid.empty)
     end;
     mm
 

src/parser/parser.mly

@@ -215,13 +215,13 @@ clone_subst:
 | 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) }
-| PREDICATE qualid EQUAL qualid { CSpsym  (floc $startpos $endpos, $2,$4) }
-| VAL       qualid EQUAL qualid { CSvsym  (floc $startpos $endpos, $2,$4) }
-| LEMMA     qualid              { CSlemma (floc $startpos $endpos, $2) }
-| GOAL      qualid              { CSgoal  (floc $startpos $endpos, $2) }
+| TYPE qualid ty_var* EQUAL ty  { CStsym  ($2,$3,$5) }
+| CONSTANT  qualid EQUAL qualid { CSfsym  ($2,$4) }
+| FUNCTION  qualid EQUAL qualid { CSfsym  ($2,$4) }
+| PREDICATE qualid EQUAL qualid { CSpsym  ($2,$4) }
+| VAL       qualid EQUAL qualid { CSvsym  ($2,$4) }
+| LEMMA     qualid              { CSlemma ($2) }
+| GOAL      qualid              { CSgoal  ($2) }
 
 (* Meta declarations *)
 

src/parser/ptree.ml

@@ -205,12 +205,12 @@ type metarg =
   | 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
+  | CStsym  of qualid * ident list * pty
+  | CSfsym  of qualid * qualid
+  | CSpsym  of qualid * qualid
+  | CSvsym  of qualid * qualid
+  | CSlemma of qualid
+  | CSgoal  of qualid
 
 type decl =
   | Dtype of type_decl list

src/parser/typing.ml

@@ -80,7 +80,7 @@ let find_prop     tuc q = find_prop_ns     (Theory.get_namespace tuc) q
 
 let find_prop_of_kind k tuc q =
   let pr = find_prop tuc q in
-  match (Mid.find pr.pr_name (Theory.get_known tuc)).d_node with
+  match (Mid.find pr.pr_name tuc.uc_known).d_node with
   | Dprop (l,_,_) when l = k -> pr
   | _ -> Loc.errorm ~loc:(qloc q) "proposition %a is not %s"
       print_qualid q (match k with
@@ -164,7 +164,7 @@ let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
 
 let parse_record ~loc tuc get_val fl =
   let fl = List.map (fun (q,e) -> find_lsymbol tuc q, e) fl in
-  let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known tuc) fl in
+  let cs,pjl,flm = Loc.try2 ~loc parse_record tuc.uc_known fl in
   let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
   cs, List.map get_val pjl
 
@@ -974,8 +974,53 @@ let find_module env file q =
   if Debug.test_flag Glob.flag then Glob.use (qloc_last q) m.mod_theory.th_name;
   m
 
+let type_inst ({muc_theory = tuc} as muc) {mod_theory = t} s =
+  let add_inst s = function
+    | CStsym (p,[],PTtyapp (q,[])) ->
+        let ts1 = find_tysymbol_ns t.th_export p in
+        let ts2 = find_tysymbol tuc q in
+        if Mts.mem ts1 s.inst_ts then
+          Loc.error ~loc:(qloc p) (ClashSymbol ts1.ts_name.id_string);
+        { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
+    | CStsym (p,tvl,pty) ->
+        let ts1 = find_tysymbol_ns t.th_export p in
+        let id = id_user (ts1.ts_name.id_string ^ "_subst") (qloc p) in
+        let tvl = List.map (fun id -> tv_of_string id.id_str) tvl in
+        let ts2 = Loc.try3 ~loc:(qloc p)
+          create_itysymbol_alias id tvl (ity_of_pty muc pty) in
+        if Mts.mem ts1 s.inst_ts then
+          Loc.error ~loc:(qloc p) (ClashSymbol ts1.ts_name.id_string);
+        { s with inst_ts = Mts.add ts1 ts2.its_ts s.inst_ts }
+    | CSfsym (p,q) ->
+        let ls1 = find_fsymbol_ns t.th_export p in
+        let ls2 = find_fsymbol tuc q in
+        if Mls.mem ls1 s.inst_ls then
+          Loc.error ~loc:(qloc p) (ClashSymbol ls1.ls_name.id_string);
+        { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
+    | CSpsym (p,q) ->
+        let ls1 = find_psymbol_ns t.th_export p in
+        let ls2 = find_psymbol tuc q in
+        if Mls.mem ls1 s.inst_ls then
+          Loc.error ~loc:(qloc p) (ClashSymbol ls1.ls_name.id_string);
+        { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
+    | CSvsym (p,_) ->
+        Loc.errorm ~loc:(qloc p)
+          "program symbol instantiation is not supported yet" (* TODO *)
+    | CSlemma p ->
+        let pr = find_prop_ns t.th_export p in
+        if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal then
+          Loc.error ~loc:(qloc p) (ClashSymbol pr.pr_name.id_string);
+        { s with inst_lemma = Spr.add pr s.inst_lemma }
+    | CSgoal p ->
+        let pr = find_prop_ns t.th_export p in
+        if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal then
+          Loc.error ~loc:(qloc p) (ClashSymbol pr.pr_name.id_string);
+        { s with inst_goal = Spr.add pr s.inst_goal }
+  in
+  List.fold_left add_inst empty_inst s
+
 let add_decl muc env file d =
-  let vc = muc.muc_path = [] &&
+  let vc = muc.muc_theory.uc_path = [] &&
     Debug.test_noflag debug_type_only in
   match d with
   | Ptree.Dtype dl ->
@@ -1012,118 +1057,10 @@ let add_decl muc env file d =
       add_pdecl ~vc muc (create_exn_decl xs)
   | Ptree.Duse use ->
       use_export muc (find_module env file use)
-  | Ptree.Dclone (use, _subst) ->
+  | Ptree.Dclone (use, inst) ->
       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 =
-  let qualid fmt path = Pp.print_list
-    (fun fmt () -> Format.pp_print_char fmt '.')
-    Format.pp_print_string fmt (List.rev path) in
-  let s = Mstr.fold (fun nm ns1 acc ->
-    let ns2 = Mstr.find_def empty_ns nm ns2.ns_ns in
-    clone_ns kn sl (nm::path) ns2 ns1 acc) ns1.ns_ns s
-  in
-  let inst_ts = Mstr.fold (fun nm ts1 acc ->
-    match Mstr.find_opt nm ns2.ns_ts with
-    | Some ts2 when ts_equal ts1 ts2 -> acc
-    | Some _ when not (Sid.mem ts1.ts_name sl) ->
-        raise (NonLocal ts1.ts_name)
-    | Some _ when ts1.ts_def <> None ->
-        raise (CannotInstantiate ts1.ts_name)
-    | Some ts2 ->
-        begin match (Mid.find ts1.ts_name kn).d_node with
-          | Decl.Dtype _ -> Mts.add_new (ClashSymbol nm) ts1 ts2 acc
-          | _ -> raise (CannotInstantiate ts1.ts_name)
-        end
-    | None when not (Sid.mem ts1.ts_name sl) -> acc
-    | None when ts1.ts_def <> None -> acc
-    | None ->
-        begin match (Mid.find ts1.ts_name kn).d_node with
-          | Decl.Dtype _ -> Loc.errorm
-              "type symbol %a not found in the target theory"
-              qualid (nm::path)
-          | _ -> acc
-        end)
-    ns1.ns_ts s.inst_ts
-  in
-  let inst_ls = Mstr.fold (fun nm ls1 acc ->
-    match Mstr.find_opt nm ns2.ns_ls with
-    | Some ls2 when ls_equal ls1 ls2 -> acc
-    | Some _ when not (Sid.mem ls1.ls_name sl) ->
-       raise (NonLocal ls1.ls_name)
-    | Some ls2 ->
-        begin match (Mid.find ls1.ls_name kn).d_node with
-          | Decl.Dparam _ -> Mls.add_new (ClashSymbol nm) ls1 ls2 acc
-          | _ -> raise (CannotInstantiate ls1.ls_name)
-        end
-    | None when not (Sid.mem ls1.ls_name sl) -> acc
-    | None ->
-        begin match (Mid.find ls1.ls_name kn).d_node with
-          | Decl.Dparam _ -> Loc.errorm
-              "%s symbol %a not found in the target theory"
-              (if ls1.ls_value <> None then "function" else "predicate")
-              qualid (nm::path)
-          | _ -> acc
-        end)
-    ns1.ns_ls s.inst_ls
-  in
-  { s with inst_ts = inst_ts; inst_ls = inst_ls }
-
-let find_namespace_ns ns q =
-  find_qualid (fun _ -> Glob.dummy_id) ns_find_ns ns q
-
-let type_inst tuc t s =
-  let add_inst s = function
-    | CSns (loc,p,q) ->
-      let ns1 = Opt.fold find_namespace_ns t.th_export p in
-      let ns2 = Opt.fold find_namespace_ns (get_namespace tuc) q in
-      Loc.try6 ~loc clone_ns t.th_known t.th_local [] ns2 ns1 s
-    | CStsym (loc,p,[],PTtyapp (q,[])) ->
-      let ts1 = find_tysymbol_ns t.th_export p in
-      let ts2 = find_tysymbol tuc q in
-      if Mts.mem ts1 s.inst_ts
-      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
-      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
-    | CStsym (loc,p,tvl,pty) ->
-      let ts1 = find_tysymbol_ns t.th_export p in
-      let id = id_user (ts1.ts_name.id_string ^ "_subst") loc in
-      let tvl = List.map (fun id -> tv_of_string id.id_str) tvl in
-      let def = Some (ty_of_pty tuc pty) in
-      let ts2 = Loc.try3 ~loc create_tysymbol id tvl def in
-      if Mts.mem ts1 s.inst_ts
-      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
-      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
-    | CSfsym (loc,p,q) ->
-      let ls1 = find_fsymbol_ns t.th_export p in
-      let ls2 = find_fsymbol tuc q in
-      if Mls.mem ls1 s.inst_ls
-      then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string);
-      { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
-    | CSpsym (loc,p,q) ->
-      let ls1 = find_psymbol_ns t.th_export p in
-      let ls2 = find_psymbol tuc q in
-      if Mls.mem ls1 s.inst_ls
-      then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string);
-      { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
-    | CSvsym (loc,_,_) ->
-      Loc.errorm ~loc "program symbol instantiation \
-        is not supported in pure theories"
-    | CSlemma (loc,p) ->
-      let pr = find_prop_ns t.th_export p in
-      if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
-      then Loc.error ~loc (ClashSymbol pr.pr_name.id_string);
-      { s with inst_lemma = Spr.add pr s.inst_lemma }
-    | CSgoal (loc,p) ->
-      let pr = find_prop_ns t.th_export p in
-      if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
-      then Loc.error ~loc (ClashSymbol pr.pr_name.id_string);
-      { s with inst_goal = Spr.add pr s.inst_goal }
-  in
-  List.fold_left add_inst empty_inst s
-*)
+      clone_export muc m (type_inst muc m inst)
 
 (* incremental parsing *)