fix: Adjust to main

Author: TDiazT

template-rocq/src/ast_denoter.ml

@@ -32,7 +32,7 @@ struct
   type quoted_univ_constraint = Universes0.UnivConstraint.t
   type quoted_univ_constraints = Universes0.ConstraintSet.t
   type quoted_univ_level = Universes0.Level.t
-  type quoted_instance = Universes0.Instance.t
+  type quoted_univ_instance = Universes0.Instance.t
   type quoted_univ_context = Universes0.UContext.t
   type quoted_contextset = Universes0.ContextSet.t
   type quoted_abstract_univ_context = Universes0.AUContext.t
@@ -88,7 +88,7 @@ struct
       rarg=rarg x
     }
 
-  let unquote_predicate (x: 't Ast0.predicate) : ('t, quoted_aname, quoted_instance) apredicate =
+  let unquote_predicate (x: 't Ast0.predicate) : ('t, quoted_aname, quoted_univ_instance) apredicate =
     {
       auinst = puinst x;
       apars = pparams x;
@@ -106,7 +106,7 @@ struct
       aci_relevance = x.ci_relevance }
 
   let inspect_term (tt: t):(t, quoted_int, quoted_ident, quoted_aname, quoted_sort, quoted_cast_kind,
-    quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_instance, quoted_proj,
+    quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj,
     quoted_int63, quoted_float64, quoted_pstring) structure_of_term =
     match tt with
     | Coq_tRel n -> ACoq_tRel n
@@ -206,7 +206,7 @@ struct
     let { inductive_mind = kn; inductive_ind = i } = q in
     (MutInd.make1 (unquote_kn kn), unquote_int i)
 
-  (*val unquote_instance :  quoted_instance -> UVars.Instance.t *)
+  (*val unquote_instance :  quoted_univ_instance -> UVars.Instance.t *)
   let unquote_proj (q : quoted_proj) : (quoted_inductive * quoted_int * quoted_int) =
     let { proj_ind = ind; proj_npars = ps; proj_arg = idx } = q in
     (ind, ps, idx)
@@ -249,7 +249,7 @@ struct
 
   let unquote_universe_level evm l = evm, unquote_level l
 
-  let unquote_instance(evm: Evd.evar_map) (inst: quoted_instance): Evd.evar_map * UVars.Instance.t =
+  let unquote_universe_instance(evm: Evd.evar_map) (inst: quoted_univ_instance): Evd.evar_map * UVars.Instance.t =
     let qarr = Array.of_list (List.map unquote_quality (Universes0.Instance.qualities inst)) in
     let uarr = Array.of_list (List.map unquote_level (Universes0.Instance.universes inst)) in
     (evm, UVars.Instance.of_array (qarr, uarr))

template-rocq/src/ast_quoter.ml

@@ -33,7 +33,7 @@ struct
   type quoted_univ_constraint = Universes0.UnivConstraint.t
   type quoted_univ_constraints = Universes0.ConstraintSet.t
   type quoted_univ_level = Universes0.Level.t
-  type quoted_instance = Universes0.Instance.t
+  type quoted_univ_instance = Universes0.Instance.t
   type quoted_univ_context = Universes0.UContext.t
   type quoted_contextset = Universes0.ContextSet.t
   type quoted_abstract_univ_context = Universes0.AUContext.t
@@ -176,7 +176,7 @@ struct
 
   let quote_univ_level = quote_level
 
-  let quote_instance (i : UVars.Instance.t) : quoted_instance =
+  let quote_univ_instance (i : UVars.Instance.t) : quoted_univ_instance =
     let qarr, uarr = UVars.Instance.to_array i in
     (* we assume that valid instances do not contain [Prop] or [SProp] *)
     try Universes0.Instance.make
@@ -206,8 +206,9 @@ struct
     let qnames = CArray.map_to_list quote_name qarr  in
     let unames = CArray.map_to_list quote_name uarr  in
     let inst = UVars.UContext.instance uctx  in
-    let constraints = UVars.UContext.constraints uctx in
-    (Universes0.mk_bound_names qnames unames, (quote_instance inst, quote_univ_constraints constraints))
+    (* FIXME: Missing elim constraints *)
+    let _, constraints = UVars.UContext.constraints uctx in
+    (Universes0.mk_bound_names qnames unames, (quote_univ_instance inst, quote_univ_constraints constraints))
 
   let quote_contextset (uctx : Univ.ContextSet.t) : quoted_contextset =
     let levels = List.map quote_level (Univ.Level.Set.elements (Univ.ContextSet.levels uctx)) in
@@ -218,7 +219,8 @@ struct
     let {UVars.quals = qnames; UVars.univs = unames} = UVars.AbstractContext.names uctx in
     let qnames = CArray.map_to_list quote_name qnames in
     let unames = CArray.map_to_list quote_name unames in
-    let constraints = UVars.UContext.constraints (UVars.AbstractContext.repr uctx) in
+    (* FIXME: Missing elim constraints *)
+    let _, constraints = UVars.UContext.constraints (UVars.AbstractContext.repr uctx) in
     (Universes0.mk_bound_names qnames unames, quote_univ_constraints constraints)
 
   let quote_context_decl na b t =
@@ -393,7 +395,7 @@ struct
 
   let inspectTerm (t : term) :  (term, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind,
     quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level,
-    quoted_instance, quoted_proj,
+    quoted_univ_instance, quoted_proj,
     quoted_int63, quoted_float64, quoted_pstring) structure_of_term =
    match t with
   | Coq_tRel n -> ACoq_tRel n

template-rocq/src/constr_denoter.ml

@@ -311,7 +311,7 @@ struct
       | _ -> bad_term_verb trm "unquote_sort_type_too_many_args"
     else bad_term_verb trm "unquote_sort_type_no_args"
 
-  let unquote_instance evm trm (* of type instance *) =
+  let unquote_universe_instance evm trm (* of type instance *) =
     let qs, us = unquote_pair trm in
     let ql = unquote_list qs in
     let ul = unquote_list us in
@@ -416,7 +416,7 @@ struct
 
   let inspect_term (t:Constr.t)
   : (Constr.t, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name,
-    quoted_inductive, quoted_relevance, quoted_univ_level, quoted_instance, quoted_proj,
+    quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj,
     quoted_int63, quoted_float64, quoted_pstring) structure_of_term =
     (* debug (fun () -> Pp.(str "denote_term" ++ spc () ++ print_term t)) ; *)
     let (h,args) = app_full t [] in

template-rocq/src/constr_quoter.ml

@@ -248,7 +248,7 @@ struct
     | QConstant QType -> Lazy.force qType
     | QVar q -> constr_mkApp (qVar, [| quote_qvar q |])
 
-  let quote_instance u =
+  let quote_univ_instance u =
     let qarr, uarr = UVars.Instance.to_array u in
     (* we assume that valid instances do not contain [Prop] or [SProp] *)
 	constr_mkApp
@@ -343,7 +343,7 @@ struct
       constr_mkApp (cPolymorphic_entry, [| ctx |])
 
   let quote_ugraph (g : UGraph.t) =
-    let inst' = quote_instance UVars.Instance.empty in
+    let inst' = quote_univ_instance UVars.Instance.empty in
     let const' = quote_univ_constraints (fst (UGraph.constraints_of_universes g)) in
     let uctx = constr_mkApp (tUContextmake, [|inst' ; const'|]) in
     constr_mkApp (tadd_global_constraints, [|constr_mkApp (cMonomorphic_ctx, [| uctx |]); Lazy.force tinit_graph|])

template-rocq/src/constr_reification.ml

@@ -27,7 +27,7 @@ struct
   type quoted_univ_constraint = Constr.t (* of type Universes.univ_constraint *)
   type quoted_univ_constraints = Constr.t (* of type Universes.constraints *)
   type quoted_univ_level = Constr.t (* of type Universes.Level.t *)
-  type quoted_instance = Constr.t (* of type Universes.universe_instance *)
+  type quoted_univ_instance = Constr.t (* of type Universes.universe_instance *)
   type quoted_univ_context = Constr.t (* of type Universes.UContext.t *)
   type quoted_contextset = Constr.t (* of type Universes.ContextSet.t *)
   type quoted_abstract_univ_context = Constr.t (* of type Universes.AUContext.t *)

template-rocq/src/denoter.ml

@@ -21,16 +21,16 @@ sig
   val unquote_cast_kind : quoted_cast_kind -> Constr.cast_kind
   val unquote_kn :  quoted_kernel_name -> KerName.t
   val unquote_inductive :  quoted_inductive -> Names.inductive
-  (*val unquote_instance :  quoted_instance -> UVars.Instance.t *)
+  (*val unquote_instance :  quoted_univ_instance -> UVars.Instance.t *)
   val unquote_proj : quoted_proj -> (quoted_inductive * quoted_int * quoted_int)
   (* val unquote_universe : Evd.evar_map -> quoted_universe -> Evd.evar_map * Univ.Universe.t *)
   val unquote_universe_level : Evd.evar_map -> quoted_univ_level -> Evd.evar_map * Univ.Level.t
-  val unquote_instance: Evd.evar_map -> quoted_instance -> Evd.evar_map * UVars.Instance.t
+  val unquote_universe_instance: Evd.evar_map -> quoted_univ_instance -> Evd.evar_map * UVars.Instance.t
   val unquote_sort : Evd.evar_map -> quoted_sort -> Evd.evar_map * Sorts.t
   (* val unquote_sort_family : quoted_sort_family -> Sorts.family *)
   (* val representsIndConstuctor : quoted_inductive -> Term.constr -> bool *)
   val inspect_term : t -> (t, quoted_int, quoted_ident, quoted_aname, quoted_sort, quoted_cast_kind,
-    quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_instance, quoted_proj,
+    quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj,
     quoted_int63, quoted_float64, quoted_pstring) structure_of_term
 
 end
@@ -105,17 +105,17 @@ struct
         evm, Constr.mkConstU (cst, u)
       | ACoq_tConstruct (i,idx,u) ->
         let ind = D.unquote_inductive i in
-        let evm, u = D.unquote_instance evm u in
+        let evm, u = D.unquote_universe_instance evm u in
         evm, Constr.mkConstructU ((ind, D.unquote_int idx + 1), u)
       | ACoq_tInd (i, u) ->
         let i = D.unquote_inductive i in
-        let evm, u = D.unquote_instance evm u in
+        let evm, u = D.unquote_universe_instance evm u in
         evm, Constr.mkIndU (i, u)
       | ACoq_tCase (ci, p, c, brs) ->
         let ind = D.unquote_inductive ci.aci_ind in
         let relevance = D.unquote_relevance ci.aci_relevance in
         let ci = Inductiveops.make_case_info (Global.env ()) ind Constr.RegularStyle in
-        let evm, puinst = D.unquote_instance evm p.auinst in
+        let evm, puinst = D.unquote_universe_instance evm p.auinst in
         let evm, pars = map_evm (aux env) evm p.apars in
         let pars = Array.of_list pars in
         let napctx = CArray.map_of_list D.unquote_aname (List.rev p.apcontext) in

template-rocq/src/quoter.ml

@@ -71,11 +71,11 @@ sig
   val mkLambda : quoted_aname -> t -> t -> t
   val mkLetIn : quoted_aname -> t -> t -> t -> t
   val mkApp : t -> t array -> t
-  val mkConst : quoted_kernel_name -> quoted_instance -> t
-  val mkInd : quoted_inductive -> quoted_instance -> t
-  val mkConstruct : quoted_inductive * quoted_int -> quoted_instance -> t
+  val mkConst : quoted_kernel_name -> quoted_univ_instance -> t
+  val mkInd : quoted_inductive -> quoted_univ_instance -> t
+  val mkConstruct : quoted_inductive * quoted_int -> quoted_univ_instance -> t
   val mkCase : (quoted_inductive * quoted_int * quoted_relevance) ->
-    (quoted_instance * t array * quoted_aname array * t) -> (* predicate: instance, params, binder names, return type *)
+    (quoted_univ_instance * t array * quoted_aname array * t) -> (* predicate: instance, params, binder names, return type *)
      t -> (quoted_aname array * t) list (* branches *) -> t
   val mkProj : quoted_proj -> t -> t
   val mkFix : (quoted_int array * quoted_int) * (quoted_aname array * t array * t array) -> t
@@ -317,15 +317,15 @@ struct
 
       | Constr.Const (c,pu) ->
         let kn = Constant.canonical c in
-        (Q.mkConst (Q.quote_kn kn) (Q.quote_instance pu), add_constant kn acc)
+        (Q.mkConst (Q.quote_kn kn) (Q.quote_univ_instance pu), add_constant kn acc)
 
       | Constr.Construct ((mind,c),pu) ->
         let mib = Environ.lookup_mind (fst mind) (snd env) in
-         (Q.mkConstruct (quote_inductive' mind, Q.quote_int (c - 1)) (Q.quote_instance pu),
+         (Q.mkConstruct (quote_inductive' mind, Q.quote_int (c - 1)) (Q.quote_univ_instance pu),
           add_inductive mind mib acc)
 
       | Constr.Ind (mind,pu) ->
-         (Q.mkInd (quote_inductive' mind) (Q.quote_instance pu),
+         (Q.mkInd (quote_inductive' mind) (Q.quote_univ_instance pu),
           let mib = Environ.lookup_mind (fst mind) (snd env) in
           add_inductive mind mib acc)
 
@@ -335,7 +335,7 @@ struct
         let npar = Q.quote_int ci.Constr.ci_npar in
         let q_relevance = Q.quote_relevance relevance in
         let acc, q_pars = CArray.fold_left_map (fun acc par -> let (qt, acc) = quote_term acc env sigma par in acc, qt) acc pars in
-        let qu = Q.quote_instance u in
+        let qu = Q.quote_univ_instance u in
         let pctx = CaseCompat.case_predicate_context (snd env) ci u pars predctx in
         let qpctx = quote_name_annots predctx in
         let (qpred,acc) = quote_term acc (push_rel_context pctx env) sigma pred in

template-rocq/src/reification.ml

@@ -27,7 +27,7 @@ sig
   type quoted_univ_constraint
   type quoted_univ_constraints
   type quoted_univ_level
-  type quoted_instance
+  type quoted_univ_instance
   type quoted_univ_context
   type quoted_contextset
   type quoted_abstract_univ_context