Cloning: support inlining a type via clone-inline (clinline)

Adds a 'tyd_clinline' flag to 'tydecl', the type-level analogue of the
existing 'op_clinline'. A type cloned with an inline override ('<-' or
'<=') is tagged clinline and retains its body; when it is later used as
the target of a 'theory ... <=' override, the consumer receives that
body rather than a reference to the type (the two remain convertible —
the difference shows only when printing). The replay 'ByPath' branch now
consults 'reftyd.tyd_clinline' to choose body-vs-reference, mirroring
the operator side.

All three type override paths (BySyntax / ByPath / Direct) set
tyd_clinline = (mode <> `Alias), matching the operator side exactly.

Threads the field through ecDecl, ecHiInductive, ecScope, ecSection,
ecSubst. Adds tests/clone-type-inline.ec (expect-based).

Author: strub

src/ecDecl.ml

@@ -35,10 +35,11 @@ type ty_body =
 
 
 type tydecl = {
-  tyd_params  : ty_params;
-  tyd_type    : ty_body;
-  tyd_loca    : locality;
-  tyd_subtype : (EcTypes.ty * EcCoreFol.form) option;
+  tyd_params   : ty_params;
+  tyd_type     : ty_body;
+  tyd_loca     : locality;
+  tyd_clinline : bool;
+  tyd_subtype  : (EcTypes.ty * EcCoreFol.form) option;
 }
 
 let tydecl_as_concrete (td : tydecl) =
@@ -66,10 +67,11 @@ let abs_tydecl ?(params = `Int 0) lc =
           (EcUid.NameGen.bulk ~fmt n)
   in
 
-  { tyd_params  = params;
-    tyd_type    = Abstract;
-    tyd_loca    = lc;
-    tyd_subtype = None; }
+  { tyd_params   = params;
+    tyd_type     = Abstract;
+    tyd_loca     = lc;
+    tyd_clinline = false;
+    tyd_subtype  = None; }
 
 (* -------------------------------------------------------------------- *)
 let ty_instantiate (params : ty_params) (args : ty list) (ty : ty) =

src/ecDecl.mli

@@ -30,9 +30,10 @@ type ty_body =
 
 
 type tydecl = {
-  tyd_params  : ty_params;
-  tyd_type    : ty_body;
-  tyd_loca    : locality;
+  tyd_params   : ty_params;
+  tyd_type     : ty_body;
+  tyd_loca     : locality;
+  tyd_clinline : bool;
   (* For [subtype]-declared types: the carrier and the predicate. The
      declared type itself stays [tyd_type = Abstract], because a
      subtype is semantically a fresh abstract type — but its dependency
@@ -41,7 +42,7 @@ type tydecl = {
      carrier+predicate fv into the type's fv when this field is set,
      so a subtype declared inside [section. declare type c.] gets the
      section's tparams added at close, just like type aliases do.      *)
-  tyd_subtype : (EcTypes.ty * EcCoreFol.form) option;
+  tyd_subtype  : (EcTypes.ty * EcCoreFol.form) option;
 }
 
 val tydecl_as_concrete : tydecl -> EcTypes.ty option

src/ecHiInductive.ml

@@ -83,10 +83,11 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
   let tpath = EcPath.pqname (EcEnv.root env) (unloc name) in
   let env0  =
     let myself = {
-      tyd_params  = EcUnify.UniEnv.tparams ue;
-      tyd_type    = Abstract;
-      tyd_loca    = lc;
-      tyd_subtype = None;
+      tyd_params   = EcUnify.UniEnv.tparams ue;
+      tyd_type     = Abstract;
+      tyd_loca     = lc;
+      tyd_clinline = false;
+      tyd_subtype  = None;
     } in
       EcEnv.Ty.bind (unloc name) myself env
   in

src/ecScope.ml

@@ -2297,7 +2297,7 @@ module Ty = struct
     in
 
     bind scope (unloc name,
-      { tyd_params; tyd_type; tyd_loca; tyd_subtype = None; })
+      { tyd_params; tyd_type; tyd_loca; tyd_clinline = false; tyd_subtype = None; })
 
   (* ------------------------------------------------------------------ *)
   let add_subtype (scope : scope) ({ pl_desc = subtype } : psubtype located) =
@@ -2326,10 +2326,11 @@ module Ty = struct
 
     let scope =
       let decl = EcDecl.{
-        tyd_params  = [];
-        tyd_type    = Abstract;
-        tyd_loca    = `Global;
-        tyd_subtype = Some (carrier, pred);
+        tyd_params   = [];
+        tyd_type     = Abstract;
+        tyd_loca     = `Global;
+        tyd_clinline = false;
+        tyd_subtype  = Some (carrier, pred);
       } in bind scope (unloc subtype.pst_name, decl) in
 
     let evclone =

src/ecSection.ml

@@ -870,8 +870,9 @@ let generalize_tydecl to_gen prefix (name, tydecl) =
     let to_gen = { to_gen with tg_subst} in
     let tydecl = {
         tyd_params; tyd_type;
-        tyd_loca    = `Global;
-        tyd_subtype = tydecl.tyd_subtype; } in
+        tyd_loca     = `Global;
+        tyd_clinline = tydecl.tyd_clinline;
+        tyd_subtype  = tydecl.tyd_subtype; } in
     to_gen, Some (Th_type (name, tydecl))
 
   | `Declare ->

src/ecSubst.ml

@@ -873,10 +873,11 @@ let subst_tydecl (s : subst) (tyd : tydecl) =
       (fun (carrier, pred) -> (subst_ty s carrier, subst_form s pred))
       tyd.tyd_subtype in
 
-  { tyd_params  = tparams;
-    tyd_type    = body;
-    tyd_loca    = tyd.tyd_loca;
-    tyd_subtype = subtype; }
+  { tyd_params   = tparams;
+    tyd_type     = body;
+    tyd_loca     = tyd.tyd_loca;
+    tyd_clinline = tyd.tyd_clinline;
+    tyd_subtype  = subtype; }
 
 (* -------------------------------------------------------------------- *)
 let rec subst_op_kind (s : subst) (kind : operator_kind) =

src/ecTheoryReplay.ml

@@ -429,19 +429,29 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
             let ue    = EcUnify.UniEnv.create (Some nargs) in
             let ntyd  = EcTyping.transty EcTyping.tp_tydecl env ue ntyd in
             let decl  =
-              { tyd_params  = nargs;
-                tyd_type    = Concrete ntyd;
-                tyd_loca    = otyd.tyd_loca;
-                tyd_subtype = None; }
+              { tyd_params   = nargs;
+                tyd_type     = Concrete ntyd;
+                tyd_loca     = otyd.tyd_loca;
+                tyd_clinline = (mode <> `Alias);
+                tyd_subtype  = None; }
 
             in (decl, ntyd)
 
         | `ByPath p -> begin
             match EcEnv.Ty.by_path_opt p env with
             | Some reftyd ->
-                let tyargs = List.map tvar reftyd.tyd_params in
-                let body   = tconstr p tyargs in
-                let decl   = { reftyd with tyd_type = Concrete body; } in
+                let body =
+                  if reftyd.tyd_clinline then
+                    (match reftyd.tyd_type with
+                     | Concrete body -> body
+                     | _ -> assert false)
+                  else
+                    let tyargs = List.map tvar reftyd.tyd_params in
+                    tconstr p tyargs in
+                let decl =
+                  { reftyd with
+                      tyd_type     = Concrete body;
+                      tyd_clinline = (mode <> `Alias); } in
                 (decl, body)
 
             | _ -> assert false
@@ -450,10 +460,11 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
         | `Direct ty -> begin
           assert (List.is_empty otyd.tyd_params);
           let decl  =
-            { tyd_params  = [];
-              tyd_type    = Concrete ty;
-              tyd_loca    = otyd.tyd_loca;
-              tyd_subtype = None; }
+            { tyd_params   = [];
+              tyd_type     = Concrete ty;
+              tyd_loca     = otyd.tyd_loca;
+              tyd_clinline = (mode <> `Alias);
+              tyd_subtype  = None; }
 
           in (decl, ty)
     end

tests/clone-type-inline.ec

@@ -0,0 +1,38 @@
+(* clinline (clone-inline) for types.
+
+   A type cloned with the inline-keep override `<=` carries its body and
+   is tagged [tyd_clinline]. When such a type is later used as the target
+   of a `theory ... <=` override, the consumer receives the *body* of the
+   type rather than a reference to it. The two stay convertible; the
+   difference is only visible when printing.
+
+   Contrast (checked below with `expect ... by print`):
+     - K.t cloned with `type t <= int` (clinline)    -> consumer prints `int`
+     - L.t cloned with `type t =  int` (plain alias)  -> consumer prints `L.t`
+*)
+
+require import AllCore.
+
+abstract theory BV.
+  type t.
+end BV.
+
+(* A theory with an abstract subtheory [P] and a use of [P.t]. *)
+abstract theory Use.
+  clone import BV as P.
+  op probe : P.t.
+end Use.
+
+(* Two instances of BV: one clinline (<=), one a plain alias (=). *)
+clone BV as K with type t <= int.   (* K.t is clinline, body = int *)
+clone BV as L with type t =  int.   (* L.t is a plain alias        *)
+
+(* Override Use's subtheory P, once by each, via a `theory <=` override. *)
+clone import Use as UK with theory P <= K.
+clone import Use as UL with theory P <= L.
+
+(* UK.P.t receives K.t's *body* (K.t is clinline): prints `int`. *)
+expect "type t = int." by print type UK.P.t.
+
+(* UL.P.t keeps the reference to L.t (L.t is a plain alias): prints `L.t`. *)
+expect "type t = L.t." by print type UL.P.t.