From b28161fc468e210f147d6b09c57e094433cf5721 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 19 Sep 2023 13:48:59 +0200 Subject: [PATCH] Adapt to coq/coq#17836 (sort poly) --- src/metaCoqInterp.ml | 6 +++--- src/metaCoqInterp.mli | 2 +- src/run.ml | 35 ++++++++++++++++++----------------- 3 files changed, 22 insertions(+), 21 deletions(-) diff --git a/src/metaCoqInterp.ml b/src/metaCoqInterp.ml index cebf6e5e..70659ddb 100644 --- a/src/metaCoqInterp.ml +++ b/src/metaCoqInterp.ml @@ -2,7 +2,7 @@ open Constrs open Ltac_pretype type mrun_arg_type = - | PolyProgram of (Univ.AbstractContext.t * EConstr.types) + | PolyProgram of (UVars.AbstractContext.t * EConstr.types) | MonoProgram of (EConstr.types) | GTactic @@ -43,7 +43,7 @@ let glob_mtac_type ist r = (* need to instantiate and register the abstract universes a *) let inst, ctx = UnivGen.fresh_instance_from au None in (* TODO: find out why UnivFlexible needs a bool & select correct bool. *) - let sigma = Evd.merge_context_set ?sideff:(Some false) (Evd.UnivFlexible true) sigma ctx in + let sigma = Evd.merge_sort_context_set ?sideff:(Some false) (Evd.UnivFlexible true) sigma ctx in sigma, Vars.subst_instance_constr inst ty, (fun ty -> PolyProgram (au, ty)) in let ty = EConstr.of_constr ty in @@ -200,7 +200,7 @@ module MetaCoqRun = struct try let inst, ctx = UnivGen.fresh_instance_from au None in (* TODO: find out why UnivFlexible needs a bool & select correct bool. *) - let sigma = Evd.merge_context_set ?sideff:(Some false) (Evd.UnivFlexible true) sigma ctx in + let sigma = Evd.merge_sort_context_set ?sideff:(Some false) (Evd.UnivFlexible true) sigma ctx in let sigma = Evarconv.unify_leq_delay env sigma concl ty in ((false, sigma, ty, EConstr.mkConst c), None) with Evarconv.UnableToUnify(_,_) -> CErrors.user_err (Pp.str "Different types") diff --git a/src/metaCoqInterp.mli b/src/metaCoqInterp.mli index 1f187c9b..7cc90d11 100644 --- a/src/metaCoqInterp.mli +++ b/src/metaCoqInterp.mli @@ -3,7 +3,7 @@ module MetaCoqRun : sig val run_tac_constr : closed_glob_constr -> unit Proofview.tactic *) type mrun_arg_type = - | PolyProgram of (Univ.AbstractContext.t * EConstr.types) + | PolyProgram of (UVars.AbstractContext.t * EConstr.types) | MonoProgram of (EConstr.types) | GTactic diff --git a/src/run.ml b/src/run.ml index b57084a5..553307fd 100644 --- a/src/run.ml +++ b/src/run.ml @@ -980,8 +980,8 @@ let run_declare_def env sigma kind name opaque ty bod = ; Instance ; Method|] in - let univs = EConstr.universes_of_constr sigma bod in - let univs = Univ.Level.Set.union univs (EConstr.universes_of_constr sigma ty) in + let _, univs = EConstr.universes_of_constr sigma bod in + let univs = Univ.Level.Set.union univs (snd (EConstr.universes_of_constr sigma ty)) in let ty = Unsafe.to_constr ty in let bod = Unsafe.to_constr bod in @@ -1237,7 +1237,7 @@ let declare_mind env sigma params sigs mut_constrs = let univs, ubinders = Evd.univ_entry ~poly:false 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 @@ -1347,8 +1347,8 @@ let _zip_term m stk = zip_term zfun t s *) assert false - | Zproj p::s -> - let t = mkProj (Projection.make p true, m) in + | Zproj (p,r)::s -> + let t = mkProj (Projection.make p true, r, m) in zip_term zfun t s | Zfix(fx,par)::s -> let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in @@ -1581,8 +1581,8 @@ and eval ctxt (vms : vm list) ?(reduced_to_let=false) t = end (* [whd_stack] considers unfolded primitive projections fully reduced. That will not do. *) - | Monadic, FProj (proj, t) -> - let stack = Zproj (Projection.repr proj) :: stack in + | Monadic, FProj (proj, r, t) -> + let stack = Zproj (Projection.repr proj, r) :: stack in let ctxt = {ctxt with stack} in (eval[@tailcall]) ctxt vms t @@ -1850,13 +1850,14 @@ and primitive ctxt vms mh univs reduced_term = | MConstr (Mhyps, _) -> let sigma, hyps, expected_type = let ulist, uhyp = - let univs = Univ.Instance.to_array univs in - match univs with - | [|ulist; uhyp|] -> ulist, uhyp - | _ -> failwith ("Expected `M.hyps` to have two universes; found " ^ string_of_int (Array.length univs)) + let qs, univs = UVars.Instance.to_array univs in + match qs, univs with + | [||], [|ulist; uhyp|] -> ulist, uhyp + | _ -> failwith ("Expected `M.hyps` to have zero qualities and two universes; found " ^ + string_of_int (Array.length qs) ^ " and " ^ string_of_int (Array.length univs)) in - let ulist = EInstance.make (Univ.Instance.of_array [|ulist|]) in - let uhyp = EInstance.make (Univ.Instance.of_array [|uhyp|]) in + let ulist = EInstance.make (UVars.Instance.of_array ([||], [|ulist|])) in + let uhyp = EInstance.make (UVars.Instance.of_array ([||], [|uhyp|])) in let sigma, hyps = build_hypotheses ~univ_hyp:uhyp ~univ_list:ulist sigma env in let sigma, hyp_ty = UConstrBuilder.build_app ~univs:uhyp Hypotheses.hyp_builder sigma env [||] in let sigma, list_ty = UConstrBuilder.build_app ~univs:ulist CoqList.listBuilder sigma env [|hyp_ty|] in @@ -2085,7 +2086,7 @@ and primitive ctxt vms mh univs reduced_term = can simply unify the record values. Otherwise it could be literally anything. In that case, we expand [c_head]. *) - let c_proj, c_rval = destProj sigma c_head in + let c_proj, _, c_rval = destProj sigma c_head in let c_constant = (Projection.constant c_proj) in if isConstant sigma env c_constant t_head then let n_params = Structures.Structure.projection_nparams c_constant in @@ -2105,7 +2106,7 @@ and primitive ctxt vms mh univs reduced_term = However, this breaks the requirement that if the pattern mentions the parameters we should unify them. Thus, we always expand in this case. *) - let t_proj, t_rval = destProj sigma t_head in + let t_proj, _, t_rval = destProj sigma t_head in (* Code for clever version: * let t_constant = (Projection.constant t_proj) in * let n_params = Recordops.find_projection_nparams (GlobRef.ConstRef t_constant) in @@ -2118,8 +2119,8 @@ and primitive ctxt vms mh univs reduced_term = let t_head, t_args = decompose_app_list sigma t in (c_head, c_args), (t_head, t_args) | (true, true) -> - let (c_proj, c_rval) = destProj sigma c_head in - let (t_proj, t_rval) = destProj sigma t_head in + let (c_proj, _, c_rval) = destProj sigma c_head in + let (t_proj, _, t_rval) = destProj sigma t_head in if QProjection.equal env c_proj t_proj then (* we use [c_head] on both sides to make sure they are considered equal *) (c_head, c_rval :: c_args), (c_head, t_rval :: t_args)