Have Evd use einstance everywhere

Author: yannl35133

engine/eConstr.mli

@@ -71,7 +71,7 @@ end
 
 module EInstance :
 sig
-  type t
+  type t = Evd.einstance
   (** Type of universe instances up-to universe unification. Similar to
       [ESorts.t] for [UVars.Instance.t]. *)
 
@@ -452,7 +452,7 @@ val identity_subst_val : named_context_val -> t SList.t
 
 (* XXX Missing Sigma proxy *)
 val fresh_global :
-  ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:UVars.Instance.t -> Environ.env ->
+  ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:EInstance.t -> Environ.env ->
   Evd.evar_map -> GlobRef.t -> Evd.evar_map * t
 
 val is_global : Environ.env -> Evd.evar_map -> GlobRef.t -> t -> bool

engine/evarutil.ml

@@ -787,8 +787,8 @@ let eq_constr_univs_test ~evd ~extended_evd t u =
   and u = EConstr.Unsafe.to_constr u in
   let sigma = ref extended_evd in
   let eq_universes _ u1 u2 =
-    let u1 = normalize_universe_instance !sigma u1 in
-    let u2 = normalize_universe_instance !sigma u2 in
+    let u1 = EConstr.EInstance.(kind !sigma (make u1)) in
+    let u2 = EConstr.EInstance.(kind !sigma (make u2)) in
     UGraph.check_eq_instances (universes !sigma) u1 u2
   in
   let eq_sorts s1 s2 =

engine/evd.ml

@@ -23,6 +23,8 @@ type econstr = constr
 type etypes = types
 type esorts = Sorts.t
 type erelevance = Sorts.relevance
+type einstance = UVars.Instance.t
+type 'a puniverses = 'a * einstance
 
 (** Generic filters *)
 module Filter :

engine/evd.mli

@@ -32,6 +32,8 @@ type econstr
 type etypes = econstr
 type esorts
 type erelevance
+type einstance
+type 'a puniverses = 'a * einstance
 
 (** {5 Existential variables and unification states} *)
 
@@ -571,14 +573,14 @@ val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
 
 val is_flexible_level : evar_map -> Univ.Level.t -> bool
 
-val normalize_universe_instance : evar_map -> UVars.Instance.t -> UVars.Instance.t
+val normalize_universe_instance : evar_map -> einstance -> einstance
 
 val set_leq_sort : evar_map -> esorts -> esorts -> evar_map
 val set_eq_sort : evar_map -> esorts -> esorts -> evar_map
 val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_eq_instances : ?flex:bool ->
-  evar_map -> UVars.Instance.t -> UVars.Instance.t -> evar_map
+  evar_map -> einstance -> einstance -> evar_map
 
 val set_eq_qualities : evar_map -> Sorts.Quality.t -> Sorts.Quality.t -> evar_map
 val set_above_prop : evar_map -> Sorts.Quality.t -> evar_map
@@ -641,15 +643,15 @@ val update_sigma_univs : UGraph.t -> evar_map -> evar_map
 val fresh_sort_in_quality : ?loc:Loc.t -> ?rigid:rigid
   -> evar_map -> UnivGen.QualityOrSet.t -> evar_map * esorts
 val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid
-  -> env -> evar_map -> Constant.t -> evar_map * pconstant
+  -> env -> evar_map -> Constant.t -> evar_map * Constant.t puniverses
 val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid
-  -> env -> evar_map -> inductive -> evar_map * pinductive
+  -> env -> evar_map -> inductive -> evar_map * inductive puniverses
 val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid
-  -> env -> evar_map -> constructor -> evar_map * pconstructor
+  -> env -> evar_map -> constructor -> evar_map * constructor puniverses
 val fresh_array_instance : ?loc:Loc.t -> ?rigid:rigid
-  -> env -> evar_map  -> evar_map * UVars.Instance.t
+  -> env -> evar_map  -> evar_map * einstance
 
-val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:UVars.Instance.t -> env ->
+val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:einstance -> env ->
   evar_map -> GlobRef.t -> evar_map * econstr
 
 (********************************************************************)
@@ -693,7 +695,7 @@ module MiniEConstr : sig
   end
 
   module EInstance : sig
-    type t
+    type t = einstance
     val make : UVars.Instance.t -> t
     val kind : evar_map -> t -> UVars.Instance.t
     val empty : t

interp/primNotations.ml

@@ -267,7 +267,9 @@ exception NotAValidPrimToken
     what it means for a term to be ground / to be able to be
     considered for parsing. *)
 
-let constr_of_globref ?(allow_constant=true) env sigma = function
+let constr_of_globref ?(allow_constant=true) env sigma =
+  let open EConstr in
+  function
   | GlobRef.ConstructRef c ->
      let sigma,c = Evd.fresh_constructor_instance env sigma c in
      sigma,mkConstructU c
@@ -282,7 +284,9 @@ let constr_of_globref ?(allow_constant=true) env sigma = function
 (** [check_glob g c] checks that glob [g] is equal to constr [c]
     and returns [g] as a constr (with fresh universe instances)
     or raises [NotAValidPrimToken]. *)
-let rec check_glob env sigma g c = match DAst.get g, Constr.kind c with
+let rec check_glob env sigma g c =
+  let open EConstr in
+  match DAst.get g, Constr.kind c with
   | Glob_term.GRef (GlobRef.ConstructRef c as g, _), Constr.Construct (c', _)
        when Environ.QConstruct.equal env c c' -> constr_of_globref env sigma g
   | Glob_term.GRef (GlobRef.IndRef c as g, _), Constr.Ind (c', _)
@@ -308,12 +312,14 @@ let rec check_glob env sigma g c = match DAst.get g, Constr.kind c with
      sigma, mkArray (u,t,def,ty)
   | Glob_term.GSort s, Constr.Sort s' ->
      let sigma,s = Glob_ops.fresh_glob_sort_in_quality sigma s in
-     let s = EConstr.ESorts.kind sigma s in
-     if not (Sorts.equal s s') then raise NotAValidPrimToken;
+     let s' = ESorts.make s' in
+     if not (ESorts.equal sigma s s') then raise NotAValidPrimToken;
      sigma,mkSort s
   | _ -> raise NotAValidPrimToken
 
-let rec constr_of_glob to_post post env sigma g = match DAst.get g with
+let rec constr_of_glob to_post post env sigma g =
+  let open EConstr in
+  match DAst.get g with
   | Glob_term.GRef (r, _) ->
       let o = List.find_opt (fun (_,r',_) -> Environ.QGlobRef.equal env r r') post in
       begin match o with
@@ -367,7 +373,6 @@ let rec constr_of_glob to_post post env sigma g = match DAst.get g with
        sigma, mkArray (u',t',def',ty')
   | Glob_term.GSort gs ->
       let sigma,c = Glob_ops.fresh_glob_sort_in_quality sigma gs in
-      let c = EConstr.ESorts.kind sigma c in
       sigma,mkSort c
   | _ ->
       raise NotAValidPrimToken
@@ -514,6 +519,7 @@ let uninterp to_raw o n =
   let of_ty = EConstr.Unsafe.to_constr of_ty in
   try
     let sigma,n = constr_of_glob o.to_post env sigma n in
+    let n = EConstr.Unsafe.to_constr n in
     let c = eval_constr_app env sigma of_ty n in
     let c = match snd o.of_kind with
       | Direct -> c

plugins/funind/gen_principle.ml

@@ -191,17 +191,17 @@ let build_functional_principle env (sigma : Evd.evar_map) old_princ_type sorts f
     (Induction.compute_elim_sig sigma (EConstr.of_constr old_princ_type))
       .Induction.nparams
   in
+  let funs = Array.map EConstr.mkConstU funs in
   let new_principle_type =
     Functional_principles_types.compute_new_princ_type_from_rel (Global.env ())
-      (Array.map Constr.mkConstU funs)
+      (Array.map (EConstr.to_constr sigma) funs)
       (Array.map (fun s -> EConstr.ESorts.kind sigma s) sorts) old_princ_type
   in
   let sigma, _ =
     Typing.type_of ~refresh:true env sigma
       (EConstr.of_constr new_principle_type)
   in
-  let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
-  let ftac = proof_tac (Array.map map funs) mutr_nparams in
+  let ftac = proof_tac funs mutr_nparams in
   let uctx = Evd.ustate sigma in
   let typ = EConstr.of_constr new_principle_type in
   let body, typ, univs, _safe, _uctx =
@@ -364,7 +364,7 @@ let generate_principle (evd : Evd.evar_map ref) pconstants on_error is_general
             evd := sigma;
             let princ_type = EConstr.Unsafe.to_constr princ_type in
             generate_functional_principle evd princ_type None None
-              (Array.of_list pconstants) (* funs_kn *)
+              (Array.map_of_list (fun (c, u) -> c, EConstr.EInstance.make u ) pconstants) (* funs_kn *)
               i
               (continue_proof 0 [|funs_kn.(i)|]))
           0 fix_rec_l
@@ -1274,7 +1274,7 @@ let get_funs_constant mp =
     in
     l_const
 
-let make_scheme evd (fas : (Constr.pconstant * UnivGen.QualityOrSet.t) list) : _ list =
+let make_scheme evd (fas : (Constant.t EConstr.puniverses * UnivGen.QualityOrSet.t) list) : _ list =
   let exception Found_type of int in
   let env = Global.env () in
   let funs = List.map fst fas in
@@ -1300,7 +1300,7 @@ let make_scheme evd (fas : (Constr.pconstant * UnivGen.QualityOrSet.t) list) : _
     List.map
       (fun idx ->
         let ind = (first_fun_kn, idx) in
-        ((ind, EConstr.EInstance.make @@ snd first_fun), true, EConstr.ESorts.prop))
+        ((ind, snd first_fun), true, EConstr.ESorts.prop))
       funs_indexes
   in
   let sigma, schemes = Indrec.build_mutual_induction_scheme env !evd ind_list in
@@ -1354,7 +1354,7 @@ let make_scheme evd (fas : (Constr.pconstant * UnivGen.QualityOrSet.t) list) : _
   if List.is_empty other_princ_types then [(body, typ, univs, opaque)]
   else
     let other_fun_princ_types =
-      let funs = Array.map Constr.mkConstU this_block_funs in
+      let funs = Array.map EConstr.(mkConstU %> to_constr sigma) this_block_funs in
       let sorts = Array.of_list sorts in
       let sorts = Array.map (fun s -> EConstr.ESorts.kind sigma s) sorts in
       List.map
@@ -1418,14 +1418,13 @@ let make_scheme evd (fas : (Constr.pconstant * UnivGen.QualityOrSet.t) list) : _
    lemmas for each function in [funs] w.r.t. [graphs]
 *)
 
-let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
+let derive_correctness (funs : Constant.t EConstr.puniverses list) (graphs : inductive list)
     =
   let open EConstr in
   assert (funs <> []);
   assert (graphs <> []);
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
-  let map (c, u) = mkConstU (c, EInstance.make u) in
-  let funs_constr = Array.map map funs in
+  let funs_constr = Array.map mkConstU funs in
   (* XXX STATE Why do we need this... why is the toplevel protection not enough *)
   funind_purify
     (fun () ->
@@ -1595,8 +1594,7 @@ let derive_inversion env fix_names =
             Evd.fresh_global env evd
               (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident id)))
           in
-          let cst, u = EConstr.destConst evd c in
-          (evd, (cst, EConstr.EInstance.kind evd u) :: l))
+          (evd, EConstr.destConst evd c :: l))
         fix_names (evd', [])
     in
     (*
@@ -2154,7 +2152,7 @@ let build_scheme fas =
                 ++ spc ()
                 ++ str "should be the named of a globally defined function")
         in
-        ((c, EConstr.EInstance.kind !evd u), sort))
+        ((c, u), sort))
       fas
   in
   let bodies_types = make_scheme evd pconstants in

plugins/ssr/ssrfwd.ml

@@ -150,7 +150,7 @@ let basecuttac k c =
           let sigma, ug = match qg with
             | QConstant (QSProp | QProp) -> sigma, Univ.Level.set
             | _ -> Evd.new_univ_level_variable Evd.univ_flexible sigma in
-          let names = UVars.Instance.of_array ([|qc;qg|],[|uc;ug|]) in
+          let names = EInstance.make @@ UVars.Instance.of_array ([|qc;qg|],[|uc;ug|]) in
           let sigma, f = EConstr.fresh_global env sigma ~names f in
           let sigma, step = Evarutil.new_evar env sigma c in
           let stepg = Proofview_monad.with_empty_state (fst @@ destEvar sigma step) in

pretyping/cases.ml

@@ -290,7 +290,6 @@ let inductive_template env sigma tmloc ind =
      instead of the global default universes
      (and in the future fresh qualities?) *)
   let sigma, indu = Evd.fresh_inductive_instance env sigma ind in
-  let indu = on_snd EInstance.make indu in
   let templ =
     match (Environ.lookup_mind (fst (fst indu)) env).mind_template with
     | None -> []

pretyping/pretyping.ml

@@ -548,7 +548,7 @@ let instance ?loc evd (ql,ul) =
          (evd, l :: univs)) (evd, [])
       ul
   in
-  evd, Some (UVars.Instance.of_array (Array.rev_of_list ql', Array.rev_of_list ul'))
+  evd, Some (EInstance.make (UVars.Instance.of_array (Array.rev_of_list ql', Array.rev_of_list ul')))
 
 let pretype_global ?loc rigid env evd gr us =
   let evd, instance =

pretyping/reductionops.ml

@@ -1276,7 +1276,7 @@ let sigma_compare_sorts _env pb s0 s1 sigma =
     end
 
 let sigma_compare_instances ~flex i0 i1 sigma =
-  match Evd.set_eq_instances ~flex sigma i0 i1 with
+  match Evd.set_eq_instances ~flex sigma (EInstance.make i0) (EInstance.make i1) with
   | sigma -> Result.Ok sigma
   | exception Evd.UniversesDiffer -> Result.Error None
   | exception UGraph.UniverseInconsistency err -> Result.Error (Some err)