Tentative cloning of "val"

src/parser/parser.mly

@@ -344,6 +344,7 @@ subst:
 | CONSTANT  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
 | FUNCTION  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
 | PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
+| VAL       qualid EQUAL qualid { CSvsym (floc (), $2, $4) }
 | LEMMA     qualid              { CSlemma (floc (), $2) }
 | GOAL      qualid              { CSgoal  (floc (), $2) }
 ;

src/parser/ptree.ml

@@ -105,6 +105,7 @@ type clone_subst =
   | 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
 

src/parser/typing.ml

@@ -790,6 +790,9 @@ let type_inst th t s =
       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

src/whyml/mlw_expr.ml

@@ -239,13 +239,6 @@ let create_psymbol_raw ~poly id ghost syms aty =
 
 (** specification *)
 
-let rec aty_pvset aty =
-  let spv = match aty.aty_result with
-    | VTarrow a -> aty_pvset a
-    | VTvalue _ -> Spv.empty in
-  let spv = spec_pvset spv aty.aty_spec in
-  List.fold_right Spv.remove aty.aty_args spv
-
 let rec aty_check vars aty =
   if aty.aty_spec.c_letrec <> 0 then invalid_arg "Mlw_expr.aty_check";
   let test_or_raise c = if not c then Loc.errorm

src/whyml/mlw_module.ml

@@ -425,7 +425,12 @@ let create_module env ?(path=[]) n =
 
 (** Clone *)
 
-let clone_export uc m inst =
+type mod_inst = {
+  inst_pv : pvsymbol Mpv.t;
+  inst_ps : psymbol Mps.t;
+}
+
+let clone_export uc m minst inst =
   let nth = Theory.clone_export uc.muc_theory m.mod_theory inst in
   let sm = match Theory.get_rev_decls nth with
     | { td_node = Clone (_,sm) } :: _ -> sm
@@ -489,6 +494,7 @@ let clone_export uc m inst =
     muc_decls = d :: uc.muc_decls;
     muc_known = known_add_decl (Theory.get_known nth) uc.muc_known d;
     muc_local = Sid.union uc.muc_local d.pd_news } in
+  let rnth = ref nth in
   let add_pd uc pd = match pd.pd_node with
     | PDtype its ->
         add_pdecl uc (create_ty_decl (conv_its its))
@@ -504,20 +510,56 @@ let clone_export uc m inst =
         (* TODO? Should we clone the defining expression and
            let it participate in the top-level module WP?
            If not, what do we do about its effects? *)
+    | PDval (LetV pv) when Mpv.mem pv minst.inst_pv ->
+        (* TODO: ensure that we do not introduce undetected aliases.
+           This may happen when the cloned module uses a base module
+           with a global variable, and then we instantiate another
+           global variable with it. *)
+          Loc.errorm "Cannot instantiate top-level variables"
     | PDval (LetV pv) ->
         let npv = conv_pv pv in
         Hid.add psh pv.pv_vs.vs_name (PV npv);
         mvs := Mvs.add pv.pv_vs npv.pv_vs !mvs;
         add_pdecl uc (create_val_decl (LetV npv))
-    | PDval (LetA ps) ->
+    | PDval (LetA ps) when Mps.mem ps minst.inst_ps ->
+        let nps = Mps.find ps minst.inst_ps in
         let aty = conv_aty !mvs ps.ps_aty in
-        let nps =
-          Mlw_expr.create_psymbol (id_clone ps.ps_name) ~ghost:ps.ps_ghost aty
-        in
+        let app = match aty.aty_result, nps.ps_aty.aty_result with
+          | VTvalue res, VTvalue _ ->
+              let argl = List.map (fun pv -> pv.pv_ity) aty.aty_args in
+              e_app (e_arrow nps argl res) (List.map e_value aty.aty_args)
+          | _ -> Loc.errorm "Program@ symbol@ instantiation@ does@ not@ \
+              support@ specifications@ for@ partially@ applied@ symbols" in
+        let spec = { aty.aty_spec with c_variant = []; c_letrec = 0 } in
+        let lam = { l_args = aty.aty_args; l_expr = app; l_spec = spec } in
+        let fd = create_fun_defn (id_clone ps.ps_name) lam in
+        if fd.fun_ps.ps_ghost && not ps.ps_ghost then Loc.errorm
+          "Program@ symbol@ instantiation@ must@ preserve@ ghostness";
+        let oeff = aty.aty_spec.c_effect in
+        let neff = fd.fun_ps.ps_aty.aty_spec.c_effect in
+        if not (Sreg.subset neff.eff_writes oeff.eff_writes &&
+                Sexn.subset neff.eff_raises oeff.eff_raises &&
+                Sreg.subset neff.eff_ghostw oeff.eff_ghostw &&
+                Sexn.subset neff.eff_ghostx oeff.eff_ghostx &&
+                Mreg.submap (fun _ -> Opt.equal reg_equal)
+                  neff.eff_resets oeff.eff_resets &&
+                Stv.subset neff.eff_compar oeff.eff_compar &&
+                (oeff.eff_diverg || not neff.eff_diverg)) then
+          Loc.errorm "Extra effects in program symbol instantiation";
+        if not (Spv.subset nps.ps_pvset (aty_pvset aty)) then
+          Loc.errorm "Extra hidden state in program symbol instantiation";
+        rnth := Mlw_wp.wp_rec ~wp:true uc.muc_env uc.muc_known !rnth [fd];
         Hid.add psh ps.ps_name (PS nps);
+        uc
+    | PDval (LetA { ps_name = id; ps_ghost = ghost; ps_aty = aty }) ->
+        let aty = conv_aty !mvs aty in
+        let nps = Mlw_expr.create_psymbol (id_clone id) ~ghost aty in
+        Hid.add psh id (PS nps);
         add_pdecl uc (create_val_decl (LetA nps))
     | PDrec fdl ->
         let conv_fd uc { fun_ps = ps } =
+          if Mps.mem ps minst.inst_ps then
+            raise (Theory.CannotInstantiate ps.ps_name);
           let id = id_clone ps.ps_name in
           let aty = conv_aty !mvs ps.ps_aty in
           let vari = Spv.fold (fun pv l ->
@@ -534,11 +576,14 @@ let clone_export uc m inst =
     muc_known = merge_known uc.muc_known extras;
     muc_used = Sid.union uc.muc_used m.mod_used } in
   let uc = List.fold_left add_pd uc m.mod_decls in
+  let nth = !rnth in
   let g_ts _ = function
     | TS ts -> not (Mts.mem ts inst.inst_ts)
     | _ -> true in
   let g_ps _ = function
     | LS ls -> not (Mls.mem ls inst.inst_ls)
+    | PV pv -> not (Mpv.mem pv minst.inst_pv)
+    | PS ps -> not (Mps.mem ps minst.inst_ps)
     | _ -> true in
   let f_ts p = function
     | TS ts ->

src/whyml/mlw_module.mli

@@ -92,7 +92,13 @@ val restore_module : theory -> modul
 (** {2 Use and clone} *)
 
 val use_export : module_uc -> modul -> module_uc
-val clone_export : module_uc -> modul -> th_inst -> module_uc
+
+type mod_inst = {
+  inst_pv : pvsymbol Mpv.t;
+  inst_ps : psymbol Mps.t;
+}
+
+val clone_export : module_uc -> modul -> mod_inst -> th_inst -> module_uc
 
 (** {2 Logic decls} *)
 

src/whyml/mlw_ty.ml

@@ -896,6 +896,13 @@ and vty_vars = function
   | VTvalue ity -> ity.ity_vars
   | VTarrow aty -> aty_vars aty
 
+let rec aty_pvset aty =
+  let spv = match aty.aty_result with
+    | VTarrow a -> aty_pvset a
+    | VTvalue _ -> Spv.empty in
+  let spv = spec_pvset spv aty.aty_spec in
+  List.fold_right Spv.remove aty.aty_args spv
+
 let ity_of_vty = function
   | VTvalue ity -> ity
   | VTarrow _   -> ity_unit

src/whyml/mlw_ty.mli

@@ -302,6 +302,9 @@ exception UnboundException of xsymbol
 
 val vty_arrow : pvsymbol list -> ?spec:spec -> vty -> aty
 
+val aty_pvset : aty -> Spv.t
+(** raises [Not_found] if the spec contains non-pv variables *)
+
 val aty_vars_match : ity_subst -> aty -> ity list -> ity -> ity_subst
 (** this only compares the types of arguments and results, and ignores
     the spec. In other words, only the type variables and regions in

src/whyml/mlw_typing.ml

@@ -66,20 +66,24 @@ let add_decl_with_tuples uc d =
 let qloc = Typing.qloc
 let print_qualid = Typing.print_qualid
 
-let uc_find_ts uc p =
+let ns_find_ts ns p =
   let get_id_ts = function
     | PT pt -> pt.its_ts.ts_name
     | TS ts -> ts.ts_name in
-  Typing.find_qualid get_id_ts ns_find_type_symbol (get_namespace uc) p
+  Typing.find_qualid get_id_ts ns_find_type_symbol ns p
 
-let uc_find_ps uc p =
+let uc_find_ts uc p = ns_find_ts (get_namespace uc) p
+
+let ns_find_ps ns p =
   let get_id_ps = function
     | PV pv -> pv.pv_vs.vs_name
     | PS ps -> ps.ps_name
     | PL pl -> pl.pl_ls.ls_name
     | XS xs -> xs.xs_name
     | LS ls -> ls.ls_name in
-  Typing.find_qualid get_id_ps ns_find_prog_symbol (get_namespace uc) p
+  Typing.find_qualid get_id_ps ns_find_prog_symbol ns p
+
+let uc_find_ps uc p = ns_find_ps (get_namespace uc) p
 
 let uc_find_ls uc p =
   let ns = Theory.get_namespace (get_theory uc) in
@@ -1251,7 +1255,30 @@ let use_clone lib mmd mth uc loc (use,inst) =
     | Theory th, None -> use_export_theory uc th
     | Module m, Some inst ->
         Theory.warn_clone_not_abstract loc m.mod_theory;
-        clone_export uc m (Typing.type_inst (get_theory uc) m.mod_theory inst)
+        let pure_inst, prog_inst = List.partition (function
+          | CSvsym _ -> false | _ -> true) inst in
+        let pure_sm = Typing.type_inst (get_theory uc) m.mod_theory pure_inst in
+        let prog_sm = { inst_pv = Mpv.empty; inst_ps = Mps.empty } in
+        let prog_sm = List.fold_left (fun s i -> match i with
+          | CSvsym (loc,p,q) ->
+              begin match ns_find_ps m.mod_export p, uc_find_ps uc q with
+              | PV pv1, PV pv2 ->
+                  if Mpv.mem pv1 s.inst_pv then Loc.error ~loc
+                    (Theory.ClashSymbol pv1.pv_vs.vs_name.id_string);
+                  { s with inst_pv = Mpv.add pv1 pv2 s.inst_pv }
+              | PS ps1, PS ps2 ->
+                  if Mps.mem ps1 s.inst_ps then Loc.error ~loc
+                    (Theory.ClashSymbol ps1.ps_name.id_string);
+                  { s with inst_ps = Mps.add ps1 ps2 s.inst_ps }
+              | PV _, PS _ | PS _, PV _ -> Loc.errorm ~loc
+                  "type mismatch"
+              | PV _, _ | PS _, _ -> Loc.errorm ~loc
+                  "not a program symbol: %a" print_qualid q
+              | _ -> Loc.errorm ~loc
+                  "not a program symbol: %a" print_qualid p
+              end
+          | _ -> assert false) prog_sm prog_inst in
+        clone_export uc m prog_sm pure_sm
     | Theory th, Some inst ->
         Theory.warn_clone_not_abstract loc th;
         clone_export_theory uc th (Typing.type_inst (get_theory uc) th inst) in