From 54a3bae291e06b969ede3623ae9651bb07c929ac Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 27 May 2024 12:07:08 +0200 Subject: [PATCH 1/2] Adapt to PR #18903 --- builtin-doc/coq-builtin.elpi | 11 ++-- src/rocq_elpi_HOAS.ml | 105 ++++++++++++++++++++++---------- src/rocq_elpi_HOAS.mli | 2 +- src/rocq_elpi_arg_HOAS.ml | 4 ++ src/rocq_elpi_builtins.ml | 73 +++++++++++++--------- src/rocq_elpi_glob_quotation.ml | 48 +++++++++------ src/rocq_elpi_utils.ml | 2 +- 7 files changed, 156 insertions(+), 89 deletions(-) diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index cc545f4f4..5fa885bc8 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -1040,11 +1040,9 @@ external pred coq.univ.variable.of-term i:term, o:coq.univ.variable.set. % -- Universe instance (for universe polymorphic global terms) ------ -% As of today a universe polymorphic constant can only be instantiated -% with universe level variables. That is f@{Prop} is not valid, nor -% is f@{u+1}. One can only write f@{u} for any u. +% A universe polymorphic constant can be instantiated with universes. % -% A univ-instance is morally a list of universe level variables, +% A univ-instance is morally a list of universes, % but its list syntax is hidden in the terms. If you really need to % craft or inspect one of these, the following APIs can help you. % @@ -1082,9 +1080,8 @@ external pred coq.univ-instance.unify-leq i:gref, i:univ-instance, % Constraint between two universes level variables kind univ-constraint type. -type lt univ.variable -> univ.variable -> univ-constraint. -type le univ.variable -> univ.variable -> univ-constraint. -type eq univ.variable -> univ.variable -> univ-constraint. +type le univ -> univ -> univ-constraint. +type eq univ -> univ -> univ-constraint. % Variance of a universe level variable kind univ-variance type. diff --git a/src/rocq_elpi_HOAS.ml b/src/rocq_elpi_HOAS.ml index c1f8135f7..ccd6170cd 100644 --- a/src/rocq_elpi_HOAS.ml +++ b/src/rocq_elpi_HOAS.ml @@ -130,7 +130,7 @@ let add_universe_constraint state c = let new_univ_level_variable ?(flexible=false) state = S.update_return (Option.get !pre_engine) state (fun ({ sigma } as e) -> (* ~name: really mean the universe level is a binder as in Definition f@{x} *) - let rigidity = if flexible then UState.univ_flexible_alg else UState.univ_rigid in + let rigidity = if flexible then UState.univ_flexible else UState.univ_rigid in let sigma, v = Evd.new_univ_level_variable ?name:None rigidity sigma in let u = Univ.Universe.make v in (* @@ -210,13 +210,10 @@ let universe_constraint : Univ.univ_constraint API.Conversion.t = doc = "Constraint between two universes level variables"; pp = (fun fmt _ -> Format.fprintf fmt ""); constructors = [ - K("lt","",A(universe_level_variable,A(universe_level_variable,N)), - B (fun u1 u2 -> (u1,Univ.Lt,u2)), - M (fun ~ok ~ko -> function (l1,Univ.Lt,l2) -> ok l1 l2 | _ -> ko ())); - K("le","",A(universe_level_variable,A(universe_level_variable,N)), + K("le","",A(univ,A(univ,N)), B (fun u1 u2 -> (u1,Univ.Le,u2)), M (fun ~ok ~ko -> function (l1,Univ.Le,l2) -> ok l1 l2 | _ -> ko ())); - K("eq","",A(universe_level_variable,A(universe_level_variable,N)), + K("eq","",A(univ,A(univ,N)), B (fun u1 u2 -> (u1,Univ.Eq,u2)), M (fun ~ok ~ko -> function (l1,Univ.Eq,l2) -> ok l1 l2 | _ -> ko ())) ] @@ -269,7 +266,17 @@ let universe_decl_cumul : universe_decl_cumul API.Conversion.t = ] } |> API.ContextualConversion.(!<) +let collapse_to_type_sigma sigma s = + match s with + | Sorts.QSort (q, u) -> + let sigma = Evd.set_eq_qualities sigma (Sorts.Quality.QVar q) Sorts.Quality.qtype in + sigma, Sorts.make Sorts.Quality.qtype u + | x -> sigma, s +let collapse_to_type_state state s = + S.update_return (Option.get !pre_engine) state (fun ({ sigma } as x) -> + let sigma, s = collapse_to_type_sigma sigma s in + { x with sigma }, s) (* All in one data structure to represent the Coq context and its link with the elpi one: @@ -336,7 +343,7 @@ let default_options () = { keepunivs = None; redflags = None; no_tc = None; - algunivs = None; + algunivs = Some true; } let make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs @@ -400,6 +407,7 @@ let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversi | Sorts.SProp -> Format.fprintf fmt "SProp" | Sorts.QSort _ -> Format.fprintf fmt "QSort"); embed = (fun ~depth { options } _ state s -> + let state, s = collapse_to_type_state state s in match s with | Sorts.Prop -> state, E.mkConst propc, [] | Sorts.SProp -> state, E.mkConst spropc, [] @@ -409,7 +417,7 @@ let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversi | Sorts.Type u -> let state, u, gls = univ.embed ~depth state u in state, E.mkApp typc u [], gls - | Sorts.QSort _ -> nYI "sort polymorphism"); + | Sorts.QSort (q, u) -> nYI ("sort polymorphism: " ^ Sorts.QVar.to_string q)); readback = (fun ~depth { options } _ state t -> match E.look ~depth t with | E.Const c when c == propc -> state, Sorts.prop, [] @@ -526,14 +534,14 @@ let constructorina ~loc x = A.mkOpaque ~loc (constructorino x) let compare_instances x y = let qx, ux = UVars.Instance.to_array x and qy, uy = UVars.Instance.to_array y in - Util.Compare.(compare [(CArray.compare Sorts.Quality.compare, qx, qy); (CArray.compare Univ.Level.compare, ux, uy)]) + Util.Compare.(compare [(CArray.compare Sorts.Quality.compare, qx, qy); (CArray.compare Univ.Universe.compare, ux, uy)]) let uinstancein, uinstanceino, isuinstance, uinstanceout, uinstance = let { CD.cin; cino; isc; cout }, uinstance = CD.declare { CD.name = "univ-instance"; doc = "Universes level instance for a universe-polymorphic constant"; pp = (fun fmt x -> - let s = Pp.string_of_ppcmds (UVars.Instance.pr Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes x) in + let s = Pp.string_of_ppcmds (UVars.Instance.pr Sorts.QVar.raw_pr (Univ.Universe.pr UnivNames.pr_level_with_global_universes) x) in Format.fprintf fmt "«%s»" s); compare = compare_instances; hash = UVars.Instance.hash; @@ -1077,6 +1085,9 @@ let force_level_of_universe state u = let w = Sorts.sort_of_univ v in add_universe_constraint state (constraint_eq (Sorts.sort_of_univ u) w), l, v, w +[%%if coq = "9.1"] +let purge_algebraic_univs_sort state s = state, EConstr.ESorts.kind (S.get engine state).sigma s +[%%else] let purge_algebraic_univs_sort state s = let sigma = (S.get engine state).sigma in match EConstr.ESorts.kind sigma s with @@ -1084,6 +1095,12 @@ let purge_algebraic_univs_sort state s = let state, _, _, s = force_level_of_universe state u in state, s | x -> state, x +[%%endif] + +let collapse_to_type state s = + S.update_return engine state (fun ({ sigma } as e) -> + let sigma, s = collapse_to_type_sigma sigma s in + { e with sigma }, s) let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) [] let in_elpiast_flex_sort ~loc t = @@ -1094,7 +1111,9 @@ let sort = { sort with API.ContextualConversion.embed = (fun ~depth ctx csts sta if ctx.options.algunivs = None || ctx.options.algunivs = Some false then purge_algebraic_univs_sort state (EConstr.ESorts.make s) else - state, s in + let state, s = collapse_to_type state s in + state, s + in sort.API.ContextualConversion.embed ~depth ctx csts state s) } let in_elpi_sort ~depth ctx csts state s = @@ -1704,7 +1723,6 @@ let body_of_constant state c inst_opt = S.update_return engine state (fun x -> let sigma = match priv with | Opaqueproof.PrivateMonomorphic () -> sigma | Opaqueproof.PrivatePolymorphic ctx -> - let ctx = Util.on_snd (Univ.subst_univs_level_constraints (snd (UVars.make_instance_subst inst))) ctx in Evd.merge_context_set Evd.univ_rigid sigma ctx in { x with sigma }, (Some (EConstr.of_constr bo), Some inst) @@ -1844,8 +1862,8 @@ let analyze_scope ~depth coq_ctx args = module UIM = F.Map(struct type t = UVars.Instance.t let compare = compare_instances - let show x = Pp.string_of_ppcmds @@ UVars.Instance.pr Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes x - let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (UVars.Instance.pr Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes x) + let show x = Pp.string_of_ppcmds @@ UVars.Instance.pr Sorts.QVar.raw_pr (Univ.Universe.pr UnivNames.pr_level_with_global_universes) x + let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (UVars.Instance.pr Sorts.QVar.raw_pr (Univ.Universe.pr UnivNames.pr_level_with_global_universes) x) end) let uim = S.declare_component ~name:"rocq-elpi:evar-univ-instance-map" ~descriptor:interp_state @@ -1862,7 +1880,7 @@ let in_coq_poly_gref ~depth ~origin ~failsafe s t i = s, u, [] with Not_found -> let u, ctx = UnivGen.fresh_global_instance (get_global_env s) t in - let s = update_sigma s (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx) in + let s = update_sigma s (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx) in let u = match C.kind u with | C.Const (_, u) -> u @@ -2947,7 +2965,7 @@ let universes_of_udecl state ({ UState.univdecl_instance ; univdecl_constraints let used1 = univdecl_instance in let used2 = List.map (fun (x,_,y) -> [x;y]) (Univ.Constraints.elements univdecl_constraints) in let used = List.fold_right Univ.Level.Set.add used1 Univ.Level.Set.empty in - let used = List.fold_right Univ.Level.Set.add (List.flatten used2) used in + let used = List.fold_right (fun x acc -> Univ.Level.Set.union (Univ.Universe.levels x) acc) (List.flatten used2) used in used let name_universe_level = ref 0 @@ -2965,7 +2983,17 @@ let name_universe_level state l = { e with sigma }, id ) - +[%%if coq = "9.1"] +let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance = + let open UState in + { univdecl_qualities = []; + univdecl_extensible_instance; + univdecl_extensible_qualities = false; + univdecl_extensible_constraints; + univdecl_constraints; + univdecl_variances = None; + univdecl_instance; } +[%%else] let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance = let open UState in { univdecl_qualities = []; @@ -2973,22 +3001,22 @@ let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraint univdecl_extensible_qualities = false; univdecl_extensible_constraints; univdecl_constraints; - univdecl_instance} + univdecl_instance; } +[%%endif] let poly_cumul_udecl_variance_of_options state options = match options.universe_decl with - | NotUniversePolymorphic -> state, false, false, UState.default_univ_decl, [| |] + | NotUniversePolymorphic -> state, false, false, UState.default_univ_decl, None | Cumulative ((univ_lvlt_var,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) -> let univdecl_instance, variance = List.split univ_lvlt_var in state, true, true, mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance, - Array.of_list variance + Some (Array.of_list variance) | NonCumulative((univ_lvlt,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) -> let univdecl_instance = univ_lvlt in - let variance = List.init (List.length univdecl_instance) (fun _ -> None) in state, true, false, mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance, - Array.of_list variance + None [%%if coq = "8.20"] let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~finite = @@ -3004,6 +3032,20 @@ let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~fin } in ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags +[%%elif coq = "9.1"] +let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~finite ~udecl ~variances = + let flags = { + ComInductive.poly; + cumulative; + template = Some false; + finite; + mode = None; + } + in + let udecl = + UState.{ udecl with univdecl_variances = variances } + in + ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags ~udecl [%%else] let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~finite ~ctx_params ~env_ar_params = let flags = { @@ -3495,19 +3537,20 @@ let upoly_decl_of ~depth state ~loose_udecl mie = let open Entries in match mie.mind_entry_universes with | Template_ind_entry _ -> nYI "template polymorphic inductives" - | Polymorphic_ind_entry uc -> - let qvars, vars = UVars.Instance.to_array @@ UVars.UContext.instance uc in + | Polymorphic_ind_entry (uc, variances) -> + let qvars, vars = UVars.LevelInstance.to_array @@ UVars.UContext.instance uc in if not (CArray.is_empty qvars) then nYI "sort poly inductives" else let state, vars = CArray.fold_left_map (fun s l -> fst (name_universe_level s l), l) state vars in let csts = UVars.UContext.constraints uc in - begin match mie.mind_entry_variance with - | None -> + begin match variances with + | None | Some Infer_variances -> let state, up, gls = universe_decl.API.Conversion.embed ~depth state ((Array.to_list vars,loose_udecl),(csts,loose_udecl)) in state, (fun i -> E.mkApp uideclc i [up]), gls - | Some variance -> + | Some (Check_variances variance) -> + let variance = UVars.Variances.repr variance in assert(Array.length variance = Array.length vars); - let uv = Array.map2 (fun x y -> (x,y)) vars variance |> Array.to_list in + let uv = Array.map2 (fun x y -> (x,Some (UVars.VarianceOccurrence.typing_variances y))) vars variance |> Array.to_list in let state, up, gls = universe_decl_cumul.API.Conversion.embed ~depth state ((uv,loose_udecl),(csts,loose_udecl)) in state, (fun i -> E.mkApp uideclc i [up]), gls end @@ -3532,7 +3575,7 @@ let inductive_entry2lp ~depth coq_ctx constraints state ~loose_udecl e = let state = match mie.mind_entry_universes with | Template_ind_entry _ -> nYI "template polymorphic inductives" | Monomorphic_ind_entry -> state - | Polymorphic_ind_entry cs -> S.update engine state (fun e -> + | Polymorphic_ind_entry (cs, _variances) -> S.update engine state (fun e -> { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma (snd (UVars.UContext.to_context_set cs)) }) (* ???? *) in let state, upoly_decl_of, upoly_decl_gls = upoly_decl_of ~depth state ~loose_udecl mie in let allparams = mie.mind_entry_params in @@ -3588,7 +3631,7 @@ let record_entry2lp ~depth coq_ctx constraints state ~loose_udecl e = let state = match mie.mind_entry_universes with | Template_ind_entry _ -> nYI "template polymorphic inductives" | Monomorphic_ind_entry -> state - | Polymorphic_ind_entry cs -> S.update engine state (fun e -> + | Polymorphic_ind_entry (cs, _variances) -> S.update engine state (fun e -> { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma (snd (UVars.UContext.to_context_set cs)) }) (* ???? *) in let state, upoly_decl_of, upoly_decl_gls = upoly_decl_of ~depth state ~loose_udecl mie in @@ -3657,7 +3700,7 @@ let record_entry2lp ~depth coq_ctx constraints state ~loose_udecl (decl:Record.R let state = match mie.mind_entry_universes with | Template_ind_entry _ -> nYI "template polymorphic inductives" | Monomorphic_ind_entry -> state - | Polymorphic_ind_entry cs -> S.update engine state (fun e -> + | Polymorphic_ind_entry (cs, _variances) -> S.update engine state (fun e -> { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma (snd (UVars.UContext.to_context_set cs)) }) (* ???? *) in let state, upoly_decl_of, upoly_decl_gls = upoly_decl_of ~depth state ~loose_udecl mie in diff --git a/src/rocq_elpi_HOAS.mli b/src/rocq_elpi_HOAS.mli index 5a936f062..4d2d5d014 100644 --- a/src/rocq_elpi_HOAS.mli +++ b/src/rocq_elpi_HOAS.mli @@ -344,7 +344,7 @@ val force_level_of_universe : state -> Univ.Universe.t -> state * Univ.Level.t * val purge_algebraic_univs_sort : state -> EConstr.ESorts.t -> state * Sorts.t val ideclc : constant val uideclc : constant -val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.universe_decl * Entries.variance_entry +val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.universe_decl * UVars.Variance.t option array option val merge_universe_context : state -> UState.t -> state val restricted_sigma_of : Univ.Level.Set.t -> state -> Evd.evar_map val universes_of_term : state -> EConstr.t -> Univ.Level.Set.t diff --git a/src/rocq_elpi_arg_HOAS.ml b/src/rocq_elpi_arg_HOAS.ml index 57710a207..d435dfb46 100644 --- a/src/rocq_elpi_arg_HOAS.ml +++ b/src/rocq_elpi_arg_HOAS.ml @@ -328,7 +328,11 @@ let intern_record_decl glob_sign (it : raw_record_decl) = glob_sign, it let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,None,y,z) let dest_entry (_,_,_,_,x) = x +[%%if coq = "9.1"] +let expr_Type_sort = Constrexpr_ops.expr_Type_sort UState.univ_flexible +[%%else] let expr_Type_sort = Constrexpr_ops.expr_Type_sort +[%%endif] [%%if coq = "8.20" || coq = "9.0"] let raw_record_decl_to_glob_synterp ({ name; sort; parameters; constructor; fields; univpoly } : raw_record_decl_elpi) : glob_record_decl_elpi = diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 134593bad..2ab366d08 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -164,6 +164,11 @@ let mk_algebraic_super x = Sorts.super x (* I don't want the user to even know that algebraic universes exist *) + +[%%if coq = "9.1"] +let univ_super state u v = + add_universe_constraint state (constraint_eq (mk_algebraic_super u) v) +[%%else] let univ_super state u v = let state, u = match u with | Sorts.Set | Sorts.Prop | Sorts.SProp -> state, u @@ -172,8 +177,10 @@ let univ_super state u v = else let state, (_,w) = new_univ_level_variable state in let w = Sorts.sort_of_univ w in - add_universe_constraint state (constraint_leq u w), w in - add_universe_constraint state (constraint_leq (mk_algebraic_super u) v) + add_universe_constraint state (constraint_leq u w), w + in + add_universe_constraint state (constraint_leq (mk_algebraic_super u) v) +[%%endif] let univ_product state s1 s2 = let s = Typeops.sort_of_product (get_global_env state) s1 s2 in @@ -314,7 +321,7 @@ let handle_uinst_option_for_inductive ~depth options i state = match options.uinstance with | NoInstance -> let term, ctx = UnivGen.fresh_global_instance (get_global_env state) (GlobRef.IndRef i) in - let state = update_sigma state (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx) in + let state = update_sigma state (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx) in snd @@ Constr.destInd term, state, [] | ConcreteInstance i -> i, state, [] | VarInstance (v_head, v_args, v_depth) -> @@ -323,7 +330,7 @@ let handle_uinst_option_for_inductive ~depth options i state = UnivGen.fresh_global_instance (get_global_env state) (GlobRef.IndRef i) in let uinst = snd @@ Constr.destInd term in let state, lp_uinst, extra_goals = uinstance.Conv.embed ~depth state uinst in - let state = update_sigma state (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx) in + let state = update_sigma state (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx) in uinst, state, API.Conversion.Unify (v', lp_uinst) :: extra_goals (* FIXME PARTIAL API @@ -878,8 +885,13 @@ let warn_deprecated_add_axiom = "section variables is deprecated. Use coq.env.add-axiom or " ^ "coq.env.add-section-variable instead")) +[%%if coq = "9.1"] +let comAssumption_declare_variable coe ~kind ty ~univs ~impargs impl ~name = + ComAssumption.declare_variable ~coe ~kind ty ~univs ~impargs ~impl ~name:name.CAst.v +[%%else] let comAssumption_declare_variable coe ~kind ty ~univs ~impargs impl ~name = ComAssumption.declare_variable ~coe ~kind ty ~univs ~impargs ~impl ~name:name.CAst.v +[%%endif] [%%if coq = "8.20" || coq = "9.0"] let comAssumption_declare_axiom coe ~local ~kind ~univs ~impargs ~inline ~name ty = ComAssumption.declare_axiom ~coe ~local ~kind ~univs ~impargs ~inline ~name:name.CAst.v ty @@ -925,32 +937,33 @@ let warns_of_options options = options.user_warns |> Option.map UserWarn.with_em let add_axiom_or_variable api id ty local_bkind options state = let state, poly, cumul, udecl, _ = poly_cumul_udecl_variance_of_options state options in let used = universes_of_term state ty in + if not (is_ground (get_sigma state) ty) then + err Pp.(str"coq.env.add-const: the type must be ground. Did you forge to call coq.typecheck-indt-decl?"); + let ty = EConstr.to_constr (get_sigma state) ty in let sigma = restricted_sigma_of used state in if cumul then err Pp.(str api ++ str": unsupported attribute @udecl-cumul! or @univpoly-cumul!"); if poly && Option.has_some local_bkind then err Pp.(str api ++ str": section variables cannot be universe polymorphic"); - let univs = UState.check_univ_decl (Evd.evar_universe_context sigma) udecl ~poly in + let univs = UState.check_univ_decl (Evd.evar_universe_context sigma) udecl ~poly ~cumulative:cumul ~kind:UVars.Assumption in let kind = Decls.Logical in let impargs = [] in let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in let id = Id.of_string id in let name = CAst.(make ~loc id) in - if not (is_ground sigma ty) then - err Pp.(str"coq.env.add-const: the type must be ground. Did you forge to call coq.typecheck-indt-decl?"); let gr, _ = match local_bkind with | Some implicit_kind -> begin Dumpglob.dump_definition name true "var"; - comAssumption_declare_variable Vernacexpr.NoCoercion ~kind (EConstr.to_constr sigma ty) ~univs ~impargs implicit_kind ~name + comAssumption_declare_variable Vernacexpr.NoCoercion ~kind ty ~univs ~impargs implicit_kind ~name end | None -> begin Dumpglob.dump_definition name false "ax"; - comAssumption_declare_axiom Vernacexpr.NoCoercion ~local:Locality.ImportDefaultBehavior ~kind (EConstr.to_constr sigma ty) + comAssumption_declare_axiom Vernacexpr.NoCoercion ~local:Locality.ImportDefaultBehavior ~kind ty ~univs ~impargs ~inline:options.inline ~name end in - let ucsts = match univs with UState.Monomorphic_entry x, _ -> x | _ -> Univ.ContextSet.empty in + let ucsts = match univs.UState.universes_entry_universes with UState.Monomorphic_entry x -> x | _ -> Univ.ContextSet.empty in gr, ucsts ;; @@ -1276,12 +1289,12 @@ let unify_instances_gref gr ui1 ui2 diag env state cmp_constr_universes = | IndRef ind -> let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in - Conversion.inductive_cumulativity_arguments (mib,snd ind), UVars.AbstractContext.size univs + UCompare.inductive_cumulativity_arguments (mib,snd ind), UVars.AbstractContext.size univs | ConstructRef (ind,kno) -> let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in - Conversion.constructor_cumulativity_arguments (mib,snd ind,kno), UVars.AbstractContext.size univs + UCompare.constructor_cumulativity_arguments (mib,snd ind,kno), UVars.AbstractContext.size univs in let l1 = UVars.Instance.length ui1 in let l2 = UVars.Instance.length ui2 in @@ -1817,7 +1830,7 @@ Supported attributes: UnivGen.fresh_global_instance (get_global_env state) (GlobRef.ConstructRef kon) in snd @@ Constr.destConstruct term, update_sigma state - (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx), + (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx), [] else UVars.Instance.empty, state, [] @@ -1830,7 +1843,7 @@ Supported attributes: let state, lp_uinst, extra_goals = uinstance.Conv.embed ~depth state uinst in uinst, update_sigma state - (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx), + (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx), API.Conversion.Unify (v', lp_uinst) :: extra_goals in let ty = if_keep ty (fun () -> @@ -2251,8 +2264,8 @@ Supported attributes: match me.mind_entry_universes with | Monomorphic_ind_entry -> (Monomorphic_entry, UState.Monomorphic_entry uctx, univ_binders) | Template_ind_entry _ -> nYI "template polymorphic inductives" - | Polymorphic_ind_entry uctx -> - (Polymorphic_entry uctx, UState.Polymorphic_entry uctx, univ_binders) + | Polymorphic_ind_entry (uctx, variances) -> + (Polymorphic_entry (uctx, variances), UState.Polymorphic_entry (uctx, variances), univ_binders) in let () = global_push_context_set uctx in let mind = @@ -2561,11 +2574,12 @@ phase unnecessary.|}; | Data u1, Data u2 -> if Sorts.equal u1 u2 then Univ.ContextSet.empty, state, !: u1 +! u2,[] else - let state, u2 = if true (* options.algunivs != Some true *) + let state, u2 = if options.algunivs != Some true then purge_algebraic_univs_sort state (EConstr.ESorts.make u2) else state, u2 in Univ.ContextSet.empty, add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[] - | _ -> err Pp.(str"coq.sort.leq: called with _ as argument")))), + | _ -> + err Pp.(str"coq.sort.leq: called with _ as argument")))), DocAbove); MLCode(Pred("coq.sort.eq", @@ -2578,7 +2592,7 @@ phase unnecessary.|}; | Data u1, Data u2 -> if Sorts.equal u1 u2 then Univ.ContextSet.empty, state, !: u1 +! u2,[] else - let state, u2 = if true (* options.algunivs != Some true *) + let state, u2 = if options.algunivs != Some true then purge_algebraic_univs_sort state (EConstr.ESorts.make u2) else state, u2 in Univ.ContextSet.empty, add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, [] @@ -2714,7 +2728,8 @@ phase unnecessary.|}; let sigma = get_sigma state in let ustate = Evd.evar_universe_context sigma in let constraints = UState.constraints ustate in - let v_constraints = Univ.Constraints.filter (fun (l1,_,l2) -> Univ.Level.(equal v l1 || equal v l2)) constraints in + let v = Univ.Universe.make v in + let v_constraints = Univ.Constraints.filter (fun (l1,_,l2) -> Univ.Universe.(equal v l1 || equal v l2)) constraints in state, !: (Univ.Constraints.elements v_constraints), [] )), DocAbove); @@ -2731,11 +2746,9 @@ phase unnecessary.|}; LPDoc "-- Universe instance (for universe polymorphic global terms) ------"; - LPDoc {|As of today a universe polymorphic constant can only be instantiated -with universe level variables. That is f@{Prop} is not valid, nor -is f@{u+1}. One can only write f@{u} for any u. + LPDoc {|A universe polymorphic constant can be instantiated with universes. -A univ-instance is morally a list of universe level variables, +A univ-instance is morally a list of universes, but its list syntax is hidden in the terms. If you really need to craft or inspect one of these, the following APIs can help you. @@ -2752,20 +2765,22 @@ term (of the instance it contains) with another one.|}; (fun uinst_arg univs_arg ~depth { env ; options } _ state -> match uinst_arg, univs_arg with | Data uinst, _ -> - let elpi_term_of_level state l = - let state, t, gls = universe_level_variable.Conv.embed ~depth state l in + let elpi_term_of_univ state u = + let state, t, gls = univ.Conv.embed ~depth state u in assert (gls = []); state, mkData t in let quals, univs = UVars.Instance.to_array uinst in let () = if not (CArray.is_empty quals) then nYI "sort poly" in let state, univs = - CArray.fold_left_map elpi_term_of_level state univs in + CArray.fold_left_map elpi_term_of_univ state univs in state, ?: None +! Array.to_list univs, [] | NoData, Data univs -> let readback_or_new state = function - | NoData -> let state, (l,_) = new_univ_level_variable state in state, l, [] - | Data t -> universe_level_variable.Conv.readback ~depth state t in + | NoData -> let state, (_,u) = new_univ_level_variable state in state, u, [] + | Data t -> let state, l, gls = universe_level_variable.Conv.readback ~depth state t in + state, Univ.Universe.make l, gls + in let state, levels, gls = U.map_acc readback_or_new state univs in state, !: (UVars.Instance.of_array ([||], Array.of_list levels)) +? None, gls | NoData, NoData -> diff --git a/src/rocq_elpi_glob_quotation.ml b/src/rocq_elpi_glob_quotation.ml index 6a275cde5..c0254a88f 100644 --- a/src/rocq_elpi_glob_quotation.ml +++ b/src/rocq_elpi_glob_quotation.ml @@ -216,7 +216,27 @@ let universe_level_name evd ({CAst.v=id} as lid) = CErrors.user_err ?loc:lid.CAst.loc (Pp.(str "Undeclared universe: " ++ Id.print id ++ str ".")) -let sort_name env sigma l = match l with +let glob_level loc state = function + | GSProp + | GProp -> + CErrors.user_err ?loc + Pp.(str "Universe instances cannot contain non-Set small levels, polymorphic" ++ + str " universe instances must be greater or equal to Set."); + | GSet -> Univ.Level.set + | GUniv u -> u + | GRawUniv u -> nYI "GRawUniv" + | GLocalUniv l -> universe_level_name (get_sigma state) l + +let glob_level_expr loc state (l, k) = + (glob_level loc state l, k) + +let glob_univ loc state = function + | UAnonymous _ -> nYI "UAnonymous" + | UNamed l -> + let us = List.map (glob_level_expr loc state) l in + Univ.Universe.of_list us + +let sort_name loc state l = match l with | [] -> assert false | [u, 0] -> begin match u with @@ -225,30 +245,18 @@ let sort_name env sigma l = match l with | GProp -> Sorts.prop | GUniv u -> Sorts.sort_of_univ (Univ.Universe.make u) | GLocalUniv l -> - let u = universe_level_name sigma l in + let u = universe_level_name (get_sigma state) l in Sorts.sort_of_univ (Univ.Universe.make u) | GRawUniv _ -> nYI "GRawUniv" end -| [_] | _ :: _ :: _ -> - nYI "(glob)HOAS for Type@{i j}" + | l -> + let us = List.map (glob_level_expr loc state) l in + Sorts.sort_of_univ (Univ.Universe.of_list us) -let glob_level loc state = function - | UAnonymous _ -> nYI "UAnonymous" - | UNamed s -> - match s with - | GSProp - | GProp -> - CErrors.user_err ?loc - Pp.(str "Universe instances cannot contain non-Set small levels, polymorphic" ++ - str " universe instances must be greater or equal to Set."); - | GSet -> Univ.Level.set - | GUniv u -> u - | GRawUniv u -> nYI "GRawUniv" - | GLocalUniv l -> universe_level_name (get_sigma state) l let nogls f ~depth state = let state, x = f ~depth state in state, x, () -let rigid_anon_type = function GSort(None, UAnonymous {rigid=UnivRigid}) -> true | _ -> false +let rigid_anon_type = function GSort(None, UAnonymous {rigid=_}) -> true | _ -> false let named_type = function GSort(None, UNamed _) -> true | _ -> false let name_of_type = function GSort(None, UNamed u) -> u | _ -> assert false let dest_GProd = function GProd(n,_,_,s,t) -> n,s,t | _ -> assert false @@ -344,7 +352,7 @@ let gterm2lpast ~pattern ~language state glob = in_elpiast_poly_gr ~loc gr s | Some (ql,l) -> let () = if not (CList.is_empty ql) then nYI "sort poly" in - let l' = List.map (glob_level x.CAst.loc state) l in + let l' = List.map (glob_univ x.CAst.loc state) l in in_elpiast_poly_gr_instance ~loc gr (UVars.Instance.of_array ([||], Array.of_list l')) end | GRef(gr,_ul) -> in_elpiast_gr ~loc gr @@ -355,7 +363,7 @@ let gterm2lpast ~pattern ~language state glob = | GSort _ as t when named_type t -> let u = name_of_type t in let env = get_glob_env state in - in_elpiast_sort ~loc state (sort_name env (get_sigma state) u) + in_elpiast_sort ~loc state (sort_name x.CAst.loc state u) | GSort(_) -> nYI "(glob)HOAS for Type@{i j}" | GProd _ as t -> diff --git a/src/rocq_elpi_utils.ml b/src/rocq_elpi_utils.ml index 6ce1e8ae0..fbd001a41 100644 --- a/src/rocq_elpi_utils.ml +++ b/src/rocq_elpi_utils.ml @@ -377,7 +377,7 @@ let detype_instance ku sigma l = else let qs, us = UVars.Instance.to_array l in let qs = List.map (detype_quality sigma) (Array.to_list qs) in - let us = List.map (detype_level sigma) (Array.to_list us) in + let us = List.map (detype_universe sigma) (Array.to_list us) in Some (qs, us) let it_destRLambda_or_LetIn_names l c = From dd63870dc00c003e3befc180c8b614615dabbcbe Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 26 Jun 2025 14:47:50 +0200 Subject: [PATCH 2/2] nix ontop of rocq branch #18903 --- .nix/config.nix | 75 +++++++++++++++++++++++++++---------------------- 1 file changed, 41 insertions(+), 34 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 79f6812fb..6ac7d1925 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -1,5 +1,7 @@ -with builtins; with (import {}).lib; -let master = [ +with builtins; +with (import { }).lib; +let + master = [ "coqeal" "hierarchy-builder" "mathcomp" @@ -11,9 +13,10 @@ let master = [ "multinomials" "odd-order" ]; - common-bundles = listToAttrs (forEach master (p: - { name = p; value.override.version = "master"; })) - // { + common-bundles = listToAttrs (forEach master (p: { + name = p; + value.override.version = "master"; + })) // { coq-elpi-tests.job = true; stdlib.job = true; coq-elpi-tests-stdlib.job = true; @@ -25,12 +28,12 @@ let master = [ deriving.job = false; reglang.job = false; -}; in -{ + }; +in { format = "1.0.0"; attribute = "rocq-elpi"; coq-attribute = "coq-elpi"; - default-bundle = "coq-8.20"; + default-bundle = "rocq-master"; bundles = { "coq-8.20".coqPackages = common-bundles // { @@ -44,36 +47,40 @@ let master = [ coq-elpi.override.elpi-version = "2.0.7"; }; - "coq-master" = { rocqPackages = { - rocq-core.override.version = "master"; - rocq-elpi.override.elpi-version = "2.0.7"; - stdlib.override.version = "master"; - bignums.override.version = "master"; - }; coqPackages = common-bundles // { - coq.override.version = "master"; - coq-elpi.override.elpi-version = "2.0.7"; - stdlib.override.version = "master"; - bignums.override.version = "master"; - }; }; - + "rocq-master" = { + rocqPackages = { + rocq-core.override.version = "#18903"; + rocq-elpi.override.elpi-version = "2.0.7"; + stdlib.override.version = "master"; + bignums.override.version = "master"; + }; + coqPackages = common-bundles // { + coq.override.version = "#18903"; + coq-elpi.override.elpi-version = "2.0.7"; + stdlib.override.version = "master"; + bignums.override.version = "master"; + }; + }; + /* uncomment bundle below if min and max elpi version start to differ - "coq-master-min-elpi" = { rocqPackages = { - rocq-core.override.version = "master"; - rocq-elpi.override.elpi-version = "2.0.7"; - stdlib.override.version = "master"; - bignums.override.version = "master"; - }; coqPackages = common-bundles // { - coq.override.version = "master"; - coq-elpi.override.elpi-version = "2.0.7"; - stdlib.override.version = "master"; - bignums.override.version = "master"; - }; }; */ + "coq-master-min-elpi" = { rocqPackages = { + rocq-core.override.version = "master"; + rocq-elpi.override.elpi-version = "2.0.7"; + stdlib.override.version = "master"; + bignums.override.version = "master"; + }; coqPackages = common-bundles // { + coq.override.version = "master"; + coq-elpi.override.elpi-version = "2.0.7"; + stdlib.override.version = "master"; + bignums.override.version = "master"; + }; }; + */ }; - cachix.coq = {}; - cachix.math-comp = {}; - cachix.coq-community = {}; + cachix.coq = { }; + cachix.math-comp = { }; + cachix.coq-community = { }; cachix.coq-elpi.authToken = "CACHIX_AUTH_TOKEN"; }