accept type expressions in clone substitutions

syntax: clone type t 'a 'b = my_t ('b, 'a)

implicitly introduces a type alias for the RHS type
and accepts unknown type alises in a substitution,
provided every type in the ts_def is known.

src/core/theory.ml

@@ -308,8 +308,12 @@ let close_namespace uc import =
 
 (* Base constructors *)
 
+let known_ts kn ts = match ts.ts_def with
+  | Some ty -> ty_s_fold (fun () ts -> known_id kn ts.ts_name) () ty
+  | None -> known_id kn ts.ts_name
+
 let known_clone kn sm =
-  Mts.iter (fun _ ts -> known_id kn ts.ts_name) sm.sm_ts;
+  Mts.iter (fun _ ts -> known_ts kn ts) sm.sm_ts;
   Mls.iter (fun _ ls -> known_id kn ls.ls_name) sm.sm_ls;
   Mpr.iter (fun _ pr -> known_id kn pr.pr_name) sm.sm_pr
 

src/parser/parser.mly

@@ -357,7 +357,8 @@ list1_comma_subst:
 
 subst:
 | NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
-| TYPE      qualid EQUAL qualid { CStsym (floc (), $2, $4) }
+| TYPE qualid type_args EQUAL primitive_type
+                                { CStsym (floc (), $2, $3, $5) }
 | CONSTANT  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
 | FUNCTION  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
 | PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }

src/parser/ptree.ml

@@ -95,7 +95,7 @@ type use = {
 
 type clone_subst =
   | CSns    of loc * qualid option * qualid option
-  | CStsym  of loc * qualid * qualid
+  | CStsym  of loc * qualid * ident list * pty
   | CSfsym  of loc * qualid * qualid
   | CSpsym  of loc * qualid * qualid
   | CSlemma of loc * qualid

src/parser/typing.ml

@@ -196,6 +196,17 @@ let rec dty uc = function
       let ts = ts_tuple (List.length tyl) in
       tyapp ts (List.map (dty uc) tyl)
 
+let rec ty_of_pty uc = function
+  | PPTtyvar {id=x} ->
+      ty_var (create_user_tv x)
+  | PPTtyapp (p, x) ->
+      let ts = find_tysymbol x uc in
+      let tyl = List.map (ty_of_pty uc) p in
+      Loc.try2 (qloc x) ty_app ts tyl
+  | PPTtuple tyl ->
+      let ts = ts_tuple (List.length tyl) in
+      ty_app ts (List.map (ty_of_pty uc) tyl)
+
 let specialize_lsymbol p uc =
   let s = find_lsymbol p uc in
   let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
@@ -1125,12 +1136,21 @@ let type_inst th t s =
       let ns1 = Opt.fold find t.th_export p in
       let ns2 = Opt.fold find (get_namespace th) q in
       clone_ns loc t.th_local ns2 ns1 s
-    | CStsym (loc,p,q) ->
+    | CStsym (loc,p,[],PPTtyapp ([],q)) ->
       let ts1 = find_tysymbol_ns p t.th_export in
       let ts2 = find_tysymbol q th in
       if Mts.mem ts1 s.inst_ts
       then 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 p t.th_export in
+      let id = id_user (ts1.ts_name.id_string ^ "_subst") loc in
+      let tvl = List.map (fun id -> create_user_tv id.id) tvl in
+      let def = Some (ty_of_pty th pty) in
+      let ts2 = Loc.try3 loc create_tysymbol id tvl def in
+      if Mts.mem ts1 s.inst_ts
+      then 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 p t.th_export in
       let ls2 = find_fsymbol q th in