Merge pull request #562 from SkySkimmer/sort-poly

Adapt to coq/coq#17836 (sort poly)

src/equations_common.ml

@@ -222,16 +222,12 @@ let e_type_of env evd t =
 
 let collapse_term_qualities uctx c =
   let nf_evar _ = None in
-  let nf_univ u = u in
-  let nf_sort s = s in
-  let nf_relevance r = match r with
-  | Sorts.Relevant | Sorts.Irrelevant -> r
-  | Sorts.RelevanceVar q ->
-    match UState.nf_qvar uctx q with
-    | QVar _ (* Hack *) | QType | QProp -> Sorts.Relevant
-    | QSProp -> Sorts.Irrelevant
+  let nf_qvar q = match UState.nf_qvar uctx q with
+    | QConstant _ as q -> q
+    | QVar q -> (* hack *) QConstant QType
   in
-  UnivSubst.nf_evars_and_universes_opt_subst nf_evar nf_univ nf_sort nf_relevance c
+  let nf_univ _ = None in
+  UnivSubst.nf_evars_and_universes_opt_subst nf_evar nf_qvar nf_univ c
 
 let make_definition ?opaque ?(poly=false) evm ?types b =
   let env = Global.env () in
@@ -247,7 +243,10 @@ let make_definition ?opaque ?(poly=false) evm ?types b =
   let body = to_constr b in
   let typ = Option.map to_constr types in
   let used = Vars.universes_of_constr body in
-  let used' = Option.cata Vars.universes_of_constr Univ.Level.Set.empty typ in
+  let used' = match typ with
+    | None -> Univ.Level.Set.empty
+    | Some typ -> Vars.universes_of_constr typ
+  in
   let used = Univ.Level.Set.union used used' in
   let evm = Evd.restrict_universe_context evm used in
   let univs = Evd.univ_entry ~poly evm in
@@ -258,9 +257,9 @@ let declare_constant id body ty ~poly ~kind evd =
   let cst = Declare.declare_constant ~name:id (Declare.DefinitionEntry ce) ~kind in
   Flags.if_verbose Feedback.msg_info (str((Id.to_string id) ^ " is defined"));
   if poly then
-    let cstr = EConstr.(mkConstU (cst, EInstance.make (Univ.UContext.instance (Evd.to_universe_context evm)))) in
+    let cstr = EConstr.(mkConstU (cst, EInstance.make (UVars.UContext.instance (Evd.to_universe_context evm)))) in
     cst, (evm0, cstr)
-  else cst, (evm0, EConstr.mkConst cst)
+  else cst, (evm0, EConstr.UnsafeMonomorphic.mkConst cst)
 
 let make_definition ?opaque ?(poly=false) evm ?types b =
   let evm', _, t = make_definition ?opaque ~poly evm ?types b in
@@ -677,7 +676,7 @@ let call_tac_on_ref tac c =
   let tac = Locus.ArgArg (dummy_loc, tac) in
   let val_reference = Geninterp.val_tag (Genarg.topwit Stdarg.wit_constr) in
   (* This is a hack to avoid generating useless universes *)
-  let c = Constr.mkRef (c, Univ.Instance.empty) in
+  let c = Constr.mkRef (c, UVars.Instance.empty) in
   let c = Geninterp.Val.inject val_reference (EConstr.of_constr c) in
   let ist = Geninterp.{ lfun = Names.Id.Map.add var c Names.Id.Map.empty;
                         extra = Geninterp.TacStore.empty; poly = false } in
@@ -1117,8 +1116,8 @@ let instance_of env sigma ?argu goalu =
     match argu with
     | Some equ ->
       let equ = EConstr.EInstance.kind sigma equ in
-      let equarray = Univ.Instance.to_array equ in
-      EConstr.EInstance.make (Univ.Instance.of_array (Array.append equarray [| goall |]))
-    | None -> EConstr.EInstance.make (Univ.Instance.of_array [| goall |])
+      let quals, equarray = UVars.Instance.to_array equ in
+      EConstr.EInstance.make (UVars.Instance.of_array (quals, Array.append equarray [| goall |]))
+    | None -> EConstr.EInstance.make (UVars.Instance.of_array ([||], [| goall |]))
   in
   sigma, inst, goalu

src/equations_common.mli

@@ -414,8 +414,8 @@ val hintdb_set_transparency :
   Constant.t -> bool -> Hints.hint_db_name -> unit
 
 (** To add to the API *)
-val to_peuniverses : 'a Univ.puniverses -> 'a peuniverses
-val from_peuniverses : Evd.evar_map -> 'a peuniverses -> 'a Univ.puniverses
+val to_peuniverses : 'a UVars.puniverses -> 'a peuniverses
+val from_peuniverses : Evd.evar_map -> 'a peuniverses -> 'a UVars.puniverses
 
 val is_global : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> constr -> bool
 val constr_of_global_univ : Evd.evar_map -> Names.GlobRef.t peuniverses -> constr

src/noconf.ml

@@ -79,7 +79,8 @@ let derive_no_confusion ~pm env sigma0 ~poly (ind,u as indu) =
       let () = evd := evm in
       let _, pred' = Term.decompose_lambda_n (List.length pars) (EConstr.to_constr !evd pred) in
       let indty = mkApp (sigma, [|idx; of_constr pred'|]) in
-      Sorts.Relevant, nf_betaiotazeta env !evd indty, mkProj (Lazy.force coq_pr2, mkRel 1), pars, (List.firstn lenargs ctx)
+      (* sigma is not sort poly (at least for now) *)
+      Sorts.Relevant, nf_betaiotazeta env !evd indty, mkProj (Lazy.force coq_pr2, Relevant, mkRel 1), pars, (List.firstn lenargs ctx)
   in
   let tru = get_efresh logic_top evd in
   let fls = get_efresh logic_bot evd in

src/principles.ml

@@ -51,10 +51,15 @@ let pi3 (_,_,z) = z
 (** Objects to keep information about equations *)
 
 let cache_rew_rule (base, gr, l2r) =
+  let gr, ((qvars, univs), csts) = UnivGen.fresh_global_instance (Global.env()) gr in
+  let () = if not (Sorts.QVar.Set.is_empty qvars) then
+      CErrors.user_err Pp.(str "Sort polymorphic autorewrite not supported.")
+  in
+  let gru = gr, (univs, csts) in
   Autorewrite.add_rew_rules
     ~locality:Hints.(if Global.sections_are_opened() then Local else SuperGlobal)
     base
-    [CAst.make (UnivGen.fresh_global_instance (Global.env()) gr, true, None)]
+    [CAst.make (gru, true, None)]
 
 let inRewRule =
   let open Libobject in
@@ -287,9 +292,9 @@ let abstract_rec_calls sigma user_obls ?(do_subst=true) is_rec len protos c =
       let case' = mkCase (Inductive.contract_case (Global.env ()) (ci, p, iv, c', brs)) in
         hyps', EConstr.Unsafe.to_constr (EConstr.Vars.substnl proto_fs (succ len) (EConstr.of_constr case'))
 
-    | Proj (p, c) ->
+    | Proj (p, r, c) ->
       let hyps', c' = aux n env hyps c in
-        hyps', mkProj (p, c')
+        hyps', mkProj (p, r, c')
 
     | _ ->
       let f', args = decompose_app c in
@@ -714,7 +719,7 @@ let subst_protos s gr =
     (equations_debug Pp.(fun () -> str"Fixed hint " ++ Printer.pr_econstr_env env sigma term);
      let sigma, _ = Typing.type_of env sigma term in
      let sigma = Evd.minimize_universes sigma in
-     Hints.hint_constr (Evarutil.nf_evar sigma term, Some (Evd.universe_context_set sigma)))
+     Hints.hint_constr (Evarutil.nf_evar sigma term, Some (Evd.sort_context_set sigma)))
   else Hints.hint_globref gr
   [@@ocaml.warning "-3"]
 
@@ -1628,11 +1633,11 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
           Nameops.add_suffix indid suff) n) stmts
     in
     let merge_universes_of_constr c =
-      Univ.Level.Set.union (EConstr.universes_of_constr !evd c) in
-    let univs = Univ.Level.Set.union (universes_of_constr !evd arity) univs in
+      Univ.Level.Set.union (snd (EConstr.universes_of_constr !evd c)) in
+    let univs = Univ.Level.Set.union (snd (universes_of_constr !evd arity)) univs in
     let univs = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) sign ~init:univs) in
     let univs =
-      List.fold_left (fun univs c -> Univ.Level.Set.union (universes_of_constr !evd (EConstr.of_constr c)) univs)
+      List.fold_left (fun univs c -> Univ.Level.Set.union (snd (universes_of_constr !evd (EConstr.of_constr c))) univs)
         univs constructors in
     let ind_sort =
       match Retyping.get_sort_family_of env !evd (it_mkProd_or_LetIn arity sign) with
@@ -1674,7 +1679,7 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
     let univs, ubinders = Evd.univ_entry ~poly sigma in
     let uctx = match univs with
     | UState.Monomorphic_entry ctx ->
-      let () = DeclareUctx.declare_universe_context ~poly:false ctx in
+      let () = Global.push_context_set ~strict:true ctx in
       Entries.Monomorphic_ind_entry
     | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
     in
@@ -1743,7 +1748,7 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
     if not poly then
       (* Declare the universe context necessary to typecheck the following
           definitions once and for all. *)
-      (DeclareUctx.declare_universe_context ~poly:false (Evd.universe_context_set !evd);
+      (Global.push_context_set ~strict:true (Evd.universe_context_set !evd);
        evd := Evd.from_env (Global.env ()))
     else ()
   in

src/sigma_types.ml

@@ -47,9 +47,10 @@ let constrs_of_coq_sigma env evd t alias =
 	                   Array.length args = 4 ->
        let ty = Retyping.get_type_of env !evd args.(1) in
 	(match kind !evd ty with
-	| Prod (n, b, t) ->
-	    let p1 = mkProj (Lazy.force coq_pr1, proj) in
-	    let p2 = mkProj (Lazy.force coq_pr2, proj) in
+          | Prod (n, b, t) ->
+            (* sigma is not sort poly (at least for now) *)
+            let p1 = mkProj (Lazy.force coq_pr1, Relevant, proj) in
+            let p2 = mkProj (Lazy.force coq_pr2, Relevant, proj) in
 	    (n, args.(2), p1, args.(0)) ::
               aux (push_rel (of_tuple (n, None, b)) env) p2 args.(3) t
 	| _ -> raise (Invalid_argument "constrs_of_coq_sigma"))
@@ -137,7 +138,7 @@ let telescope env evd = function
             let env = push_rel_context ds env in
             let sigty = mkAppG env evd (Lazy.force coq_sigma) [|t; pred|] in
             let _, u = destInd !evd (fst (destApp !evd sigty)) in
-            let ua = Univ.Instance.to_array (EInstance.kind !evd u) in
+            let _, ua = UVars.Instance.to_array (EInstance.kind !evd u) in
             let l = Sorts.sort_of_univ @@ Univ.Universe.make ua.(0) in
             (* Ensure that the universe of the sigma is only >= those of t and pred *)
             let open UnivProblem in
@@ -164,8 +165,9 @@ let telescope env evd = function
       let (last, _, subst) = List.fold_right2
 	(fun pred d (prev, k, subst) ->
           let (n, b, t) = to_tuple d in
-	  let proj1 = mkProj (Lazy.force coq_pr1, prev) in
-	  let proj2 = mkProj (Lazy.force coq_pr2, prev) in
+          (* sigma is not sort poly (at least for now) *)
+          let proj1 = mkProj (Lazy.force coq_pr1, Relevant, prev) in
+          let proj2 = mkProj (Lazy.force coq_pr2, Relevant, prev) in
 	    (Vars.lift 1 proj2, succ k, of_tuple (n, Some proj1, Vars.liftn 1 k t) :: subst))
 	(List.rev tys) tl (mkRel 1, 1, [])
       in ty, (of_tuple (n, Some last, Vars.liftn 1 len t) :: subst), constr
@@ -826,8 +828,9 @@ let curry_concl env sigma na dom codom =
   let proj last decl (terms, acc) =
     if last then (acc :: terms, acc)
     else
-      let term = mkProj (Lazy.force coq_pr1, acc) in
-      let acc = mkProj (Lazy.force coq_pr2, acc) in
+      (* sigma is not sort poly (at least for now) *)
+      let term = mkProj (Lazy.force coq_pr1, Relevant, acc) in
+      let acc = mkProj (Lazy.force coq_pr2, Relevant, acc) in
       (term :: terms, acc)
   in
   let terms, acc =

src/simplify.ml

@@ -332,7 +332,7 @@ let build_app_infer_concl (env : Environ.env) (evd : Evd.evar_map ref) ((ctx, ty
     | Some u ->
       let tf = EConstr.mkRef (f, u) in
       let auctx = Environ.universes_of_global env f in
-      let univs = Univ.AbstractContext.instantiate (EConstr.EInstance.kind !evd u) auctx in
+      let univs = UVars.AbstractContext.instantiate (EConstr.EInstance.kind !evd u) auctx in
       let sigma = Evd.add_constraints !evd univs in
       let ty = Retyping.get_type_of env sigma tf in
       evd := sigma; tf, ty

src/splitting.ml

@@ -1110,17 +1110,24 @@ let solve_equations_obligations ~pm flags recids loc i sigma hook =
   pm, lemma
 
 let gather_fresh_context sigma u octx =
-  let ctx = Evd.universe_context_set sigma in
-  let univs = Univ.ContextSet.levels ctx in
-  let arr = Univ.Instance.to_array u in
+  let (qvars, univs), _ = Evd.sort_context_set sigma in
+  let qarr, uarr = UVars.Instance.to_array u in
+  let qualities =
+    Array.fold_left (fun ctx' l ->
+        match l with
+        | Sorts.Quality.QConstant _ -> assert false
+        | QVar l ->
+          if not (Sorts.QVar.Set.mem l qvars) then Sorts.QVar.Set.add l ctx'
+          else ctx')
+      Sorts.QVar.Set.empty qarr
+  in
   let levels =
     Array.fold_left (fun ctx' l ->
         if not (Univ.Level.Set.mem l univs) then Univ.Level.Set.add l ctx'
         else ctx')
-      Univ.Level.Set.empty arr
+      Univ.Level.Set.empty uarr
   in
-  let ctx = Univ.ContextSet.of_set levels in
-  Univ.ContextSet.add_constraints (Univ.AbstractContext.instantiate u octx) ctx
+  (qualities, levels), (UVars.AbstractContext.instantiate u octx)
 
 let swap (x, y) = (y, x)
 
@@ -1172,7 +1179,7 @@ let solve_equations_obligations_program ~pm flags recids loc i sigma hook =
          let cst, i = EConstr.destConst !evd hd in
          let ctx = Environ.constant_context (Global.env ()) cst in
          let ctx = gather_fresh_context !evd (EConstr.EInstance.kind sigma i) ctx in
-         evd := Evd.merge_context_set Evd.univ_flexible !evd ctx;
+         evd := Evd.merge_sort_context_set Evd.univ_flexible !evd ctx;
          t)
       else t
     in

src/subterm.ml

@@ -152,7 +152,7 @@ let derive_subterm ~pm env sigma ~poly (ind, u as indu) =
   let univs, ubinders = Evd.univ_entry ~poly sigma in
   let uctx = match univs with
   | UState.Monomorphic_entry ctx ->
-    let () = DeclareUctx.declare_universe_context ~poly:false ctx in
+    let () = Global.push_context_set ~strict:true ctx in
     Entries.Monomorphic_ind_entry
   | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
   in
@@ -207,12 +207,13 @@ let derive_subterm ~pm env sigma ~poly (ind, u as indu) =
           let env' = push_rel_context pars env in
           let subrel =
             let liftindices = List.map (liftn 2 2) indices in
-            let yindices = List.map (subst1 (mkProj (indexproj, mkRel 1))) liftindices in
-            let xindices = List.map (subst1 (mkProj (indexproj, mkRel 2))) liftindices in
+            (* sigma is not sort poly (at least for now) *)
+            let yindices = List.map (subst1 (mkProj (indexproj, Relevant, mkRel 1))) liftindices in
+            let xindices = List.map (subst1 (mkProj (indexproj, Relevant, mkRel 2))) liftindices in
             let apprel =
               applistc subind (extended_rel_list 2 parambinders @
                                  (xindices @ yindices @
-                                    [mkProj (valproj, mkRel 2); mkProj (valproj, mkRel 1)]))
+                                    [mkProj (valproj, Relevant, mkRel 2); mkProj (valproj, Relevant, mkRel 1)]))
             in
             mkLambda (nameR (Id.of_string "x"), typesig,
                       mkLambda (nameR (Id.of_string "y"), lift 1 typesig,