Merge pull request #984 from SkySkimmer/sort-poly

Adapt to coq/coq#17836 (sort poly)

safechecker-plugin/src/g_metacoq_safechecker.mlg

@@ -23,7 +23,7 @@ let check env evm poly (c, ustate) =
   let uctx =
     if poly then
       let uctx = Evd.to_universe_context evm in
-      let inst, auctx = Univ.abstract_universes uctx in
+      let inst, auctx = UVars.abstract_universes uctx in
       Ast_quoter.mkPolymorphic_ctx (Ast_quoter.quote_abstract_univ_context auctx)
     else Ast_quoter.mkMonomorphic_ctx ()
   in
@@ -55,15 +55,18 @@ let retypecheck_term_dependencies env gr =
   let typecheck env c = ignore (Typeops.infer env c) in
   let typecheck_constant c =
     let auctx = Environ.constant_context env c in
-    let names = Univ.AbstractContext.names auctx in
+    let qnames, unames as names = UVars.AbstractContext.names auctx in
     let dp = Names.DirPath.make [Names.Id.of_string "MetaCoq"; Names.Id.of_string "Retypecheck"] in
+    let fake_quality i _ =
+      Sorts.Quality.QVar (Sorts.QVar.make_unif "" i)
+    in
     let fake_level i _ =
      Univ.Level.make (Univ.UGlobal.make dp "" i)
     in
-    let fake_inst = Univ.Instance.of_array (Array.mapi fake_level names) in
+    let fake_inst = UVars.Instance.of_array (Array.mapi fake_quality qnames, Array.mapi fake_level unames) in
     let cu = (c, fake_inst) in
     let cbody, ctype, cstrs = Environ.constant_value_and_type env cu in
-    let env' = Environ.push_context (Univ.UContext.make names (fake_inst, cstrs)) env in
+    let env' = Environ.push_context (UVars.UContext.make names (fake_inst, cstrs)) env in
     typecheck env' ctype;
     Option.iter (typecheck env') cbody
   in

template-coq/src/ast_denoter.ml

@@ -188,7 +188,7 @@ struct
     let { inductive_mind = kn; inductive_ind = i } = q in
     (MutInd.make1 (unquote_kn kn), unquote_int i)
 
-  (*val unquote_univ_instance :  quoted_univ_instance -> Univ.Instance.t *)
+  (*val unquote_univ_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)
@@ -223,8 +223,8 @@ struct
        let u = List.fold_left Univ.Universe.sup (List.hd l) (List.tl l) in
        evd, Sorts.sort_of_univ u
 
-  let unquote_universe_instance(evm: Evd.evar_map) (l: quoted_univ_instance): Evd.evar_map * Univ.Instance.t
-  = (evm,  Univ.Instance.of_array (Array.of_list (List0.map unquote_level l)))
+  let unquote_universe_instance(evm: Evd.evar_map) (l: quoted_univ_instance): Evd.evar_map * UVars.Instance.t
+  = (evm,  UVars.Instance.of_array ([||], Array.of_list (List0.map unquote_level l)))
 
 
   let unquote_global_reference (trm : Kernames.global_reference) : GlobRef.t =

template-coq/src/ast_quoter.ml

@@ -159,10 +159,13 @@ struct
     try ((quote_nonprop_level l, quote_constraint_type ct), quote_nonprop_level l')
     with e -> assert false
 
-  let quote_univ_instance (i : Univ.Instance.t) : quoted_univ_instance =
-    let arr = Univ.Instance.to_array i in
+  let quote_univ_instance (i : UVars.Instance.t) : quoted_univ_instance =
+    let qarr, uarr = UVars.Instance.to_array i in
+    let () = if not (CArray.is_empty qarr) then
+        CErrors.user_err Pp.(str "Quoting sort polymorphic instances not yet supported.")
+    in
     (* we assume that valid instances do not contain [Prop] or [SProp] *)
-    try CArray.map_to_list quote_nonprop_level arr
+    try CArray.map_to_list quote_nonprop_level uarr
     with e -> assert false
 
    (* (Prop, Le | Lt, l),  (Prop, Eq, Prop) -- trivial, (l, c, Prop)  -- unsatisfiable  *)
@@ -176,16 +179,20 @@ struct
     let l = constraints_ (Univ.Constraints.elements c) in
     Universes0.ConstraintSet.(List.fold_right add l empty)
 
-  let quote_variance (v : Univ.Variance.t) =
+  let quote_variance (v : UVars.Variance.t) =
     match v with
-    | Univ.Variance.Irrelevant -> Universes0.Variance.Irrelevant
-    | Univ.Variance.Covariant -> Universes0.Variance.Covariant
-    | Univ.Variance.Invariant -> Universes0.Variance.Invariant
-
-  let quote_univ_context (uctx : Univ.UContext.t) : quoted_univ_context =
-    let names = CArray.map_to_list quote_name (Univ.UContext.names uctx)  in
-    let levels = Univ.UContext.instance uctx  in
-    let constraints = Univ.UContext.constraints uctx in
+    | Irrelevant -> Universes0.Variance.Irrelevant
+    | Covariant -> Universes0.Variance.Covariant
+    | Invariant -> Universes0.Variance.Invariant
+
+  let quote_univ_context (uctx : UVars.UContext.t) : quoted_univ_context =
+    let qarr, uarr = (UVars.UContext.names uctx) in
+    let () = if not (CArray.is_empty qarr) then
+        CErrors.user_err Pp.(str "Quoting sort polymorphic ucontext not yet supported.")
+    in
+    let names = CArray.map_to_list quote_name uarr  in
+    let levels = UVars.UContext.instance uctx  in
+    let constraints = UVars.UContext.constraints uctx in
     (names, (quote_univ_instance levels, quote_univ_constraints constraints))
 
   let quote_univ_contextset (uctx : Univ.ContextSet.t) : quoted_univ_contextset =
@@ -199,9 +206,12 @@ struct
     (Universes0.LevelSetProp.of_list levels, quote_univ_constraints constraints)
 
   let quote_abstract_univ_context uctx : quoted_abstract_univ_context =
-    let names = Univ.AbstractContext.names uctx in
-    let levels = CArray.map_to_list quote_name names in
-    let constraints = Univ.UContext.constraints (Univ.AbstractContext.repr uctx) in
+    let qnames, unames = UVars.AbstractContext.names uctx in
+    let () = if not (CArray.is_empty qnames) then
+        CErrors.user_err Pp.(str "Quoting sort polymorphic abstract universe context not yet supported.")
+    in
+    let levels = CArray.map_to_list quote_name unames in
+    let constraints = UVars.UContext.constraints (UVars.AbstractContext.repr uctx) in
     (levels, quote_univ_constraints constraints)
 
   let quote_context_decl na b t =

template-coq/src/constr_denoter.ml

@@ -264,10 +264,10 @@ struct
   let unquote_universe_instance evm trm (* of type universe_instance *) =
     let l = unquote_list trm in
     let evm, l = map_evm unquote_level evm l in
-    evm, Univ.Instance.of_array (Array.of_list l)
+    evm, UVars.Instance.of_array ([||], Array.of_list l)
 
   let unquote_variance v =
-    let open Univ.Variance in
+    let open UVars.Variance in
     if constr_equall v cIrrelevant then Irrelevant
     else if constr_equall v cCovariant then Covariant
     else if constr_equall v cInvariant then Invariant

template-coq/src/constr_quoter.ml

@@ -229,9 +229,12 @@ struct
 
   (* todo : can be deduced from quote_level, hence shoud be in the Reify module *)
   let quote_univ_instance u =
-    let arr = Univ.Instance.to_array u in
+    let qarr, uarr = UVars.Instance.to_array u in
+    let () = if not (CArray.is_empty qarr) then
+        CErrors.user_err Pp.(str "Quoting sort polymorphic instances not yet supported.")
+    in
     (* we assume that valid instances do not contain [Prop] or [SProp] *)
-    to_coq_listl tlevel (CArray.map_to_list quote_nonprop_level arr)
+    to_coq_listl tlevel (CArray.map_to_list quote_nonprop_level uarr)
 
   let is_Lt = function
     | Univ.Lt -> true
@@ -260,9 +263,9 @@ struct
 
   let quote_variance v =
     match v with
-    | Univ.Variance.Irrelevant -> Lazy.force cIrrelevant
-    | Univ.Variance.Covariant -> Lazy.force cCovariant
-    | Univ.Variance.Invariant -> Lazy.force cInvariant
+    | UVars.Variance.Irrelevant -> Lazy.force cIrrelevant
+    | UVars.Variance.Covariant -> Lazy.force cCovariant
+    | UVars.Variance.Invariant -> Lazy.force cInvariant
 
   let quote_cuminfo_variance var =
     let var_list = CArray.map_to_list quote_variance var in
@@ -274,10 +277,13 @@ struct
     pairl tLevelSet tConstraintSet levels' const'
 
   let quote_univ_context uctx =
-    let arr = (UContext.names uctx) in
-    let idents = to_coq_listl tname (CArray.map_to_list quote_name arr) in
-    let inst' = quote_univ_instance (UContext.instance uctx) in
-    let const' = quote_univ_constraints (UContext.constraints uctx) in
+    let qarr, uarr = (UVars.UContext.names uctx) in
+    let () = if not (CArray.is_empty qarr) then
+        CErrors.user_err Pp.(str "Quoting sort polymorphic ucontext not yet supported.")
+    in
+    let idents = to_coq_listl tname (CArray.map_to_list quote_name uarr) in
+    let inst' = quote_univ_instance (UVars.UContext.instance uctx) in
+    let const' = quote_univ_constraints (UVars.UContext.constraints uctx) in
     let p = constr_mkApp (tUContextmake', [|inst'; const'|]) in
     constr_mkApp (tUContextmake, [|idents; p |])
 
@@ -290,9 +296,12 @@ struct
       constr_mkApp (cSome, [| listvar; var' |]) *)
 
  let quote_abstract_univ_context uctx =
-    let arr = (AbstractContext.names uctx) in
-    let idents = to_coq_listl tname (CArray.map_to_list quote_name arr) in
-    let const' = quote_univ_constraints (UContext.constraints (AbstractContext.repr uctx)) in
+    let qarr, uarr = (UVars.AbstractContext.names uctx) in
+    let () = if not (CArray.is_empty qarr) then
+        CErrors.user_err Pp.(str "Quoting sort polymorphic abstract universe context not yet supported.")
+    in
+    let idents = to_coq_listl tname (CArray.map_to_list quote_name uarr) in
+    let const' = quote_univ_constraints (UVars.UContext.constraints (UVars.AbstractContext.repr uctx)) in
     constr_mkApp (tAUContextmake, [|idents; const'|])
 
   let mkMonomorphic_ctx () = Lazy.force cMonomorphic_ctx
@@ -309,15 +318,15 @@ struct
   let quote_inductive_universes uctx =
     match uctx with
     | Entries.Monomorphic_entry ->
-      let f inst = Array.map (fun _ -> Anonymous) (Instance.to_array inst) in
-      let ctx = quote_univ_context (Univ.ContextSet.to_context f Univ.ContextSet.empty) in
+      let f inst = assert (UVars.Instance.is_empty inst); [||], [||] in
+      let ctx = quote_univ_context (UVars.UContext.of_context_set f Sorts.QVar.Set.empty Univ.ContextSet.empty) in
       constr_mkApp (cMonomorphic_entry, [| ctx |])
     | Entries.Polymorphic_entry uctx ->
       let ctx = quote_univ_context uctx in
       constr_mkApp (cPolymorphic_entry, [| ctx |])
 
   let quote_ugraph (g : UGraph.t) =
-    let inst' = quote_univ_instance Univ.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-coq/src/denoter.ml

@@ -20,10 +20,10 @@ 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_univ_instance :  quoted_univ_instance -> Univ.Instance.t *)
+  (*val unquote_univ_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_sort -> Evd.evar_map * Sorts.t
-  val unquote_universe_instance: Evd.evar_map -> quoted_univ_instance -> Evd.evar_map * Univ.Instance.t
+  val unquote_universe_instance: Evd.evar_map -> quoted_univ_instance -> Evd.evar_map * UVars.Instance.t
   (* 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_instance, quoted_proj, 
@@ -154,10 +154,14 @@ struct
          let ind' = D.unquote_inductive ind in
          let proj_arg = D.unquote_int arg in
          let mib = Environ.lookup_mind (fst ind') env in
-         let p' = Declareops.inductive_make_projection ind' mib ~proj_arg in
+         let p', r = Declareops.inductive_make_projection ind' mib ~proj_arg in
          let p' = Names.Projection.make p' false in
          let evm, t' = aux env evm t in
-         evm, Constr.mkProj (p', t')
+         let r = match r with
+           | Relevant | Irrelevant -> r
+           | RelevanceVar _ -> CErrors.user_err Pp.(str "Unquoting sort poly projections not yet supported.")
+         in
+         evm, Constr.mkProj (p', r, t')
       | ACoq_tInt x -> evm, Constr.mkInt (D.unquote_int63 x)
       | ACoq_tFloat x -> evm, Constr.mkFloat (D.unquote_float64 x)
 

template-coq/src/plugin_core.ml

@@ -281,10 +281,10 @@ let tmInductive (infer_univs : bool) (mie : mutual_inductive_entry) : unit tm =
       if infer_univs then
         let evm = Evd.from_env env in
         let ctx, mie = Tm_util.RetypeMindEntry.infer_mentry_univs env evm mie in
-        DeclareUctx.declare_universe_context ~poly:false ctx; mie
+        Global.push_context_set ~strict:true ctx; mie
       else mie
     in
-    let names = (UState.Monomorphic_entry Univ.ContextSet.empty, Names.Id.Map.empty) in
+    let names = (UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders) in
     ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie names []) ;
     success ~st (Global.env ()) evd ()
 

template-coq/src/quoter.ml

@@ -105,12 +105,12 @@ sig
 
   val quote_constraint_type : Univ.constraint_type -> quoted_constraint_type
   val quote_univ_constraint : Univ.univ_constraint -> quoted_univ_constraint
-  val quote_univ_instance : Univ.Instance.t -> quoted_univ_instance
+  val quote_univ_instance : UVars.Instance.t -> quoted_univ_instance
   val quote_univ_constraints : Univ.Constraints.t -> quoted_univ_constraints
-  val quote_univ_context : Univ.UContext.t -> quoted_univ_context
+  val quote_univ_context : UVars.UContext.t -> quoted_univ_context
   val quote_univ_contextset : Univ.ContextSet.t -> quoted_univ_contextset
-  val quote_variance : Univ.Variance.t -> quoted_variance
-  val quote_abstract_univ_context : Univ.AbstractContext.t -> quoted_abstract_univ_context
+  val quote_variance : UVars.Variance.t -> quoted_variance
+  val quote_abstract_univ_context : UVars.AbstractContext.t -> quoted_abstract_univ_context
 
   val mkMonomorphic_entry : quoted_univ_contextset -> quoted_universes_entry
   val mkPolymorphic_entry : quoted_univ_context -> quoted_universes_entry
@@ -185,8 +185,8 @@ struct
 
   let get_abstract_inductive_universes iu =
     match iu with
-    | Declarations.Monomorphic -> Univ.UContext.empty
-    | Polymorphic ctx -> Univ.AbstractContext.repr ctx
+    | Declarations.Monomorphic -> UVars.UContext.empty
+    | Polymorphic ctx -> UVars.AbstractContext.repr ctx
 
   let quote_universes_entry = function
     | Monomorphic_entry -> Q.mkMonomorphic_entry (Q.quote_univ_contextset Univ.ContextSet.empty)
@@ -336,7 +336,7 @@ struct
 
       | Constr.Fix fp -> quote_fixpoint acc env sigma fp
       | Constr.CoFix fp -> quote_cofixpoint acc env sigma fp
-      | Constr.Proj (p,c) ->
+      | Constr.Proj (p,_,c) ->
          let ind = quote_inductive' (Projection.inductive p) in
          let pars = Q.quote_int (Projection.npars p) in
          let arg  = Q.quote_int (Projection.arg p)   in
@@ -368,7 +368,7 @@ struct
       (Q.mkCoFix (a',decl'), acc)
     and quote_minductive_type (acc : 'a) env sigma (t : MutInd.t) mib =
       let uctx = get_abstract_inductive_universes mib.Declarations.mind_universes in
-      let inst = Univ.UContext.instance uctx in
+      let inst = UVars.UContext.instance uctx in
       let indtys =
         (CArray.map_to_list (fun oib ->
            let ty = Inductive.type_of_inductive ((mib,oib),inst) in
@@ -649,7 +649,7 @@ since  [absrt_info] is a private type *)
   let quote_constant_entry bypass env evm cd =
     let (ty, body) = quote_constant_body_aux bypass env evm cd in
     let uctx = match cd.const_universes with
-      | Polymorphic auctx -> Polymorphic_entry (Univ.AbstractContext.repr auctx)
+      | Polymorphic auctx -> Polymorphic_entry (UVars.AbstractContext.repr auctx)
       | Monomorphic -> Monomorphic_entry
     in
     let univs = quote_universes_entry uctx in

template-coq/src/run_template_monad.ml

@@ -1,4 +1,5 @@
 open Univ
+open UVars
 open Entries
 open Names
 open Redops
@@ -152,23 +153,23 @@ let denote_names evm trm : _ * Name.t array =
   let l = unquote_list trm in
   evm, CArray.map_of_list unquote_name l
 
-let denote_ucontext env evm trm (* of type UContext.t *) : _ * UContext.t =
+let denote_ucontext env evm trm (* of type UContext.t *) : _ * UVars.UContext.t =
   let l, c = unquote_pair trm in
   let evm, names = denote_names evm l in
   let l, c = unquote_pair c in
   let l = unquote_list l in
   let evm, vars = map_evm unquote_level evm l in
   let evm, c = unquote_constraints env evm c in
-  let inst = Instance.of_array (Array.of_list vars) in
-  evm, (UContext.make names (inst, c))
+  let inst = Instance.of_array ([||], Array.of_list vars) in
+  evm, (UVars.UContext.make ([||], names) (inst, c))
 
-let denote_aucontext env evm trm (* of type AbstractContext.t *) : _ * AbstractContext.t =
+let denote_aucontext env evm trm (* of type AbstractContext.t *) : _ * UVars.AbstractContext.t =
   let i, c = unquote_pair trm in
   let l = unquote_list i in
   let vars = List.mapi (fun i l -> Level.var i) l in
-  let vars = Instance.of_array (Array.of_list vars) in
+  let vars = Instance.of_array ([||], Array.of_list vars) in
   let evm, c = unquote_constraints env evm c in
-  evm, snd (abstract_universes (UContext.make (CArray.map_of_list unquote_name l) (vars, c)))
+  evm, snd (abstract_universes (UContext.make ([||], CArray.map_of_list unquote_name l) (vars, c)))
 
 let denote_variance trm (* of type Variance *) : Variance.t =
   if constr_equall trm cIrrelevant then Variance.Irrelevant
@@ -189,12 +190,12 @@ let _denote_variances evm trm : _ * Variance.t array option =
 
 (* todo : stick to Coq implem *)
 type universe_context_type =
-  | Monomorphic_uctx of Univ.ContextSet.t
-  | Polymorphic_uctx of Univ.AbstractContext.t
+  | Monomorphic_uctx of ContextSet.t
+  | Polymorphic_uctx of AbstractContext.t
 
 let _to_entry_inductive_universes = function
   | Monomorphic_uctx ctx -> UState.Monomorphic_entry ctx
-  | Polymorphic_uctx ctx -> UState.Polymorphic_entry (Univ.AbstractContext.repr ctx)
+  | Polymorphic_uctx ctx -> UState.Polymorphic_entry (AbstractContext.repr ctx)
 
 let _denote_universes_decl env evm trm (* of type universes_decl *) : _ * universe_context_type =
   let (h, args) = app_full trm [] in
@@ -300,16 +301,16 @@ let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (infer_univs : bool
   let mind = reduce_all env evm mind in
   let evm' = Evd.from_env env in
   let evm', ctx, mind = unquote_mutual_inductive_entry env evm' mind in
-  let () = DeclareUctx.declare_universe_context ~poly:false ctx in
+  let () = Global.push_context_set ~strict:true ctx in
   let evm, mind = 
     if infer_univs then
       let ctx, mind = Tm_util.RetypeMindEntry.infer_mentry_univs env evm' mind in
       debug (fun () -> Pp.(str "Declaring universe context " ++ Univ.pr_universe_context_set (Level.pr) ctx));
-      DeclareUctx.declare_universe_context ~poly:false ctx;
+      Global.push_context_set ~strict:true ctx;
       Evd.merge_context_set Evd.UnivRigid evm ctx, mind
     else evm, mind
   in
-  let names = (UState.Monomorphic_entry Univ.ContextSet.empty, Names.Id.Map.empty) in
+  let names = (UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders) in
   let primitive_expected =
     match mind.mind_entry_record with
     | Some (Some _) -> true
@@ -322,7 +323,7 @@ let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (infer_univs : bool
     let dflt_pf = { pf_coercion = false; pf_instance = false; pf_priority = None; pf_locality = OptDefault; pf_canonical = false; pf_reversible = false} in
     let decl_projs i oie =
       let ind = (ind_kn, i) in
-      let univs = (Entries.Monomorphic_entry, Names.Id.Map.empty) in
+      let univs = (Entries.Monomorphic_entry, UnivNames.empty_binders) in
       let inhabitant_id = List.hd oie.mind_entry_consnames in
       let fields, _ = Term.decompose_prod_assum (List.hd oie.mind_entry_lc) in
       let fieldimpls = List.map (fun _ -> []) fields in