remove tyd_resolve (can use import mechanism instead)

Author: strub

src/ecDecl.ml

@@ -16,10 +16,9 @@ type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
 type tydecl = {
-  tyd_params  : ty_params;
-  tyd_type    : ty_body;
-  tyd_loca    : locality;
-  tyd_resolve : bool;
+  tyd_params : ty_params;
+  tyd_type   : ty_body;
+  tyd_loca   : locality;
 }
 
 and ty_body = [
@@ -48,7 +47,7 @@ let tydecl_as_record (td : tydecl) =
   match td.tyd_type with `Record x -> Some x | _ -> None
 
 (* -------------------------------------------------------------------- *)
-let abs_tydecl ?(resolve = true) ?(tc = Sp.empty) ?(params = `Int 0) lc =
+let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
   let params =
     match params with
     | `Named params ->
@@ -60,7 +59,7 @@ let abs_tydecl ?(resolve = true) ?(tc = Sp.empty) ?(params = `Int 0) lc =
           (EcUid.NameGen.bulk ~fmt n)
   in
 
-  { tyd_params = params; tyd_type = `Abstract tc; tyd_resolve = resolve; tyd_loca = lc; }
+  { tyd_params = params; tyd_type = `Abstract tc; tyd_loca = lc; }
 
 (* -------------------------------------------------------------------- *)
 let ty_instanciate (params : ty_params) (args : ty list) (ty : ty) =

src/ecDecl.mli

@@ -12,10 +12,9 @@ type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
 type tydecl = {
-  tyd_params  : ty_params;
-  tyd_type    : ty_body;
-  tyd_loca    : locality;
-  tyd_resolve : bool;
+  tyd_params : ty_params;
+  tyd_type   : ty_body;
+  tyd_loca   : locality;
 }
 
 and ty_body = [
@@ -36,7 +35,7 @@ val tydecl_as_abstract : tydecl -> Sp.t option
 val tydecl_as_datatype : tydecl -> ty_dtype option
 val tydecl_as_record   : tydecl -> (form * (EcSymbols.symbol * EcTypes.ty) list) option
 
-val abs_tydecl : ?resolve:bool -> ?tc:Sp.t -> ?params:ty_pctor -> locality -> tydecl
+val abs_tydecl : ?tc:Sp.t -> ?params:ty_pctor -> locality -> tydecl
 
 val ty_instanciate : ty_params -> ty list -> ty -> ty
 

src/ecEnv.ml

@@ -3026,9 +3026,7 @@ module Theory = struct
 
         match item.ti_item with
         | Th_type (x, ty) ->
-            if   ty.tyd_resolve
-            then MC.import_tydecl (xpath x) ty env
-            else env
+            MC.import_tydecl (xpath x) ty env
 
         | Th_operator (x, op) ->
             MC.import_operator (xpath x) op env

src/ecHiInductive.ml

@@ -86,7 +86,6 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
       tyd_params  = EcUnify.UniEnv.tparams ue;
       tyd_type    = `Abstract EcPath.Sp.empty;
       tyd_loca    = lc;
-      tyd_resolve = true;
     } in
       EcEnv.Ty.bind (unloc name) myself env
   in

src/ecScope.ml

@@ -1608,7 +1608,7 @@ module Ty = struct
         record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields)
     in
 
-    bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; })
+    bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; })
 
   (* ------------------------------------------------------------------ *)
   let bindclass ?(import = true) (scope : scope) (x, tc) =
@@ -1639,8 +1639,7 @@ module Ty = struct
         let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in
           { tyd_params  = [];
             tyd_type    = `Abstract body;
-            tyd_loca    = (lc :> locality);
-            tyd_resolve = true;  } in
+            tyd_loca    = (lc :> locality); } in
       let scenv = EcEnv.Ty.bind name asty scenv in
 
       (* Check for duplicated field names *)

src/ecSection.ml

@@ -786,8 +786,7 @@ 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_resolve = tydecl.tyd_resolve } in
+        tyd_loca = `Global; } in
     to_gen, Some (Th_type (name, tydecl))
 
   | `Declare ->

src/ecSubst.ml

@@ -883,7 +883,6 @@ let subst_tydecl (s : subst) (tyd : tydecl) =
 
   { tyd_params  = tparams;
     tyd_type    = body;
-    tyd_resolve = tyd.tyd_resolve;
     tyd_loca    = tyd.tyd_loca; }
 
 (* -------------------------------------------------------------------- *)

src/ecTheoryReplay.ml

@@ -337,7 +337,6 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
             let decl  =
               { tyd_params  = nargs;
                 tyd_type    = `Concrete ntyd;
-                tyd_resolve = otyd.tyd_resolve && (mode = `Alias);
                 tyd_loca    = otyd.tyd_loca; }
 
             in (decl, ntyd)
@@ -347,10 +346,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
             | Some reftyd ->
                 let tyargs = List.map (fun (x, _) -> EcTypes.tvar x) reftyd.tyd_params in
                 let body   = tconstr p tyargs in
-                let decl   =
-                  { reftyd with
-                      tyd_type    = `Concrete body;
-                      tyd_resolve = otyd.tyd_resolve && (mode = `Alias); } in
+                let decl   = { reftyd with tyd_type = `Concrete body; } in
                 (decl, body)
 
             | _ -> assert false