Rework import mechanism.

The import mechanism is currently brittle, buggy, interact wrongly
with the cloning mechanism. Moreover, some declarations duplicate it
by reimplementing an ad-hoc, "non-import" mechanism. This commit fixes
this issues.

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) =
@@ -137,13 +136,11 @@ and opopaque = { smt: bool; reduction: bool; }
 type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma]
 
 type axiom = {
-  ax_tparams    : ty_params;
-  ax_spec       : EcCoreFol.form;
-  ax_kind       : axiom_kind;
-  ax_loca       : locality;
-  ax_visibility : ax_visibility; }
-
-and ax_visibility = [`Visible | `NoSmt | `Hidden]
+  ax_tparams : ty_params;
+  ax_spec    : EcCoreFol.form;
+  ax_kind    : axiom_kind;
+  ax_loca    : locality;
+  ax_smt     : bool; }
 
 let is_axiom  (x : axiom_kind) = match x with `Axiom _ -> true | _ -> false
 let is_lemma  (x : axiom_kind) = match x with `Lemma   -> true | _ -> false
@@ -272,11 +269,11 @@ let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, axbd) lc =
   let op     = f_app op opargs axbd.f_ty in
   let axspec = f_forall args (f_eq op axbd) in
 
-  { ax_tparams    = axpm;
-    ax_spec       = axspec;
-    ax_kind       = `Axiom (Ssym.empty, false);
-    ax_loca       = lc;
-    ax_visibility = if nosmt then `NoSmt else `Visible; }
+  { ax_tparams = axpm;
+    ax_spec    = axspec;
+    ax_kind    = `Axiom (Ssym.empty, false);
+    ax_loca    = lc;
+    ax_smt     = not nosmt; }
 
 (* -------------------------------------------------------------------- *)
 type typeclass = {

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
 
@@ -135,15 +134,13 @@ val operator_as_prind : operator -> prind
 type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma]
 
 type axiom = {
-  ax_tparams    : ty_params;
-  ax_spec       : form;
-  ax_kind       : axiom_kind;
-  ax_loca       : locality;
-  ax_visibility : ax_visibility;
+  ax_tparams : ty_params;
+  ax_spec    : form;
+  ax_kind    : axiom_kind;
+  ax_loca    : locality;
+  ax_smt     : bool;
 }
 
-and ax_visibility = [`Visible | `NoSmt | `Hidden]
-
 (* -------------------------------------------------------------------- *)
 val is_axiom  : axiom_kind -> bool
 val is_lemma  : axiom_kind -> bool