aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml17
-rw-r--r--interp/constrintern.ml14
-rw-r--r--interp/declare.ml19
-rw-r--r--interp/declare.mli3
-rw-r--r--interp/discharge.ml118
-rw-r--r--interp/discharge.mli16
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/notation_ops.ml6
8 files changed, 28 insertions, 166 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fe50bd4b08..701c07dc8d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -757,11 +757,10 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
(* mapping glob_constr to constr_expr *)
let extern_glob_sort = function
- | GSProp -> GSProp
- | GProp -> GProp
- | GSet -> GSet
- | GType _ as s when !print_universes -> s
- | GType _ -> GType []
+ (* In case we print a glob_constr w/o having passed through detyping *)
+ | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u
+ | UNamed _ when not !print_universes -> UAnonymous {rigid=true}
+ | UNamed _ | UAnonymous _ as u -> u
let extern_universes = function
| Some _ as l when !print_universes -> l
@@ -1312,10 +1311,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
Array.map (fun (bl,_,_) -> bl) v,
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
- | PSort Sorts.InSProp -> GSort GSProp
- | PSort Sorts.InProp -> GSort GProp
- | PSort Sorts.InSet -> GSort GSet
- | PSort Sorts.InType -> GSort (GType [])
+ | PSort Sorts.InSProp -> GSort (UNamed [GSProp,0])
+ | PSort Sorts.InProp -> GSort (UNamed [GProp,0])
+ | PSort Sorts.InSet -> GSort (UNamed [GSet,0])
+ | PSort Sorts.InType -> GSort (UAnonymous {rigid=true})
| PInt i -> GInt i
let extern_constr_pattern env sigma pat =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1dd68f2abf..1a81dc41a1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -998,18 +998,10 @@ let intern_reference qid =
in
Smartlocate.global_of_extended_global r
-let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option =
- match info with
- | UAnonymous -> None
- | UUnknown -> None
- | UNamed id -> Some (id, 0)
-
let glob_sort_of_level (level: glob_level) : glob_sort =
match level with
- | GSProp -> GSProp
- | GProp -> GProp
- | GSet -> GSet
- | GType info -> GType [sort_info_of_level_info info]
+ | UAnonymous {rigid} -> UAnonymous {rigid}
+ | UNamed id -> UNamed [id,0]
(* Is it a global reference or a syntactic definition? *)
let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
@@ -1045,7 +1037,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
| _ -> err ()
end
- | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+ | Some [s], GSort (UAnonymous {rigid=true}) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
| Some [_old_level], GSort _new_sort ->
(* TODO: add old_level and new_sort to the error message *)
user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
diff --git a/interp/declare.ml b/interp/declare.ml
index b3595b2dae..cc6f29f756 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -53,6 +53,13 @@ let load_constant i ((sp,kn), obj) =
Nametab.push (Nametab.Until i) sp (ConstRef con);
add_constant_kind con obj.cst_kind
+let cooking_info segment =
+ let modlist = replacement_context () in
+ let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in
+ let named_ctx = List.map fst hyps in
+ let abstract = (named_ctx, subst, uctx) in
+ { Opaqueproof.modlist; abstract }
+
(* Opening means making the name without its module qualification available *)
let open_constant i ((sp,kn), obj) =
(* Never open a local definition *)
@@ -89,13 +96,10 @@ let cache_constant ((sp,kn), obj) =
let discharge_constant ((sp, kn), obj) =
let con = Constant.make1 kn in
let from = Global.lookup_constant con in
- let modlist = replacement_context () in
- let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in
- let abstract = (named_of_variable_context hyps, subst, uctx) in
- let new_decl = { from; info = { Opaqueproof.modlist; abstract } } in
+ let info = cooking_info (section_segment_of_constant con) in
(* This is a hack: when leaving a section, we lose the constant definition, so
we have to store it in the libobject to be able to retrieve it after. *)
- Some { obj with cst_decl = Some new_decl; }
+ Some { obj with cst_decl = Some { from; info } }
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
let dummy_constant cst = {
@@ -312,9 +316,8 @@ let cache_inductive ((sp,kn),mie) =
let discharge_inductive ((sp,kn),mie) =
let mind = Global.mind_of_delta_kn kn in
let mie = Global.lookup_mind mind in
- let repl = replacement_context () in
- let info = section_segment_of_mutual_inductive mind in
- Some (Discharge.process_inductive info repl mie)
+ let info = cooking_info (section_segment_of_mutual_inductive mind) in
+ Some (Cooking.cook_inductive info mie)
let dummy_one_inductive_entry mie = {
mind_entry_typename = mie.mind_entry_typename;
diff --git a/interp/declare.mli b/interp/declare.mli
index 795d9a767d..0b1a396a34 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -90,5 +90,4 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
val do_universe : polymorphic -> lident list -> unit
-val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
- unit
+val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit
diff --git a/interp/discharge.ml b/interp/discharge.ml
deleted file mode 100644
index 1efd13adb1..0000000000
--- a/interp/discharge.ml
+++ /dev/null
@@ -1,118 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Util
-open Term
-open Constr
-open Vars
-open Declarations
-open Cooking
-open Entries
-
-(********************************)
-(* Discharging mutual inductive *)
-
-(* Replace
-
- Var(y1)..Var(yq):C1..Cq |- Ij:Bj
- Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
-
- by
-
- |- Ij: (y1..yq:C1..Cq)Bj
- I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
-*)
-
-let abstract_inductive decls nparamdecls inds =
- let ntyp = List.length inds in
- let ndecls = Context.Named.length decls in
- let args = Context.Named.to_instance mkVar (List.rev decls) in
- let args = Array.of_list args in
- let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in
- let inds' =
- List.map
- (function (tname,arity,template,cnames,lc) ->
- let lc' = List.map (substl subs) lc in
- let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in
- let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in
- (tname,arity',template,cnames,lc''))
- inds in
- let nparamdecls' = nparamdecls + Array.length args in
-(* To be sure to be the same as before, should probably be moved to process_inductive *)
- let params' = let (_,arity,_,_,_) = List.hd inds' in
- let (params,_) = decompose_prod_n_assum nparamdecls' arity in
- params
- in
- let ind'' =
- List.map
- (fun (a,arity,template,c,lc) ->
- let _, short_arity = decompose_prod_n_assum nparamdecls' arity in
- let shortlc =
- List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in
- { mind_entry_typename = a;
- mind_entry_arity = short_arity;
- mind_entry_template = template;
- mind_entry_consnames = c;
- mind_entry_lc = shortlc })
- inds'
- in (params',ind'')
-
-let refresh_polymorphic_type_of_inductive (_,mip) =
- match mip.mind_arity with
- | RegularArity s -> s.mind_user_arity, false
- | TemplateArity ar ->
- let ctx = List.rev mip.mind_arity_ctxt in
- mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
-
-let process_inductive info modlist mib =
- let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in
- let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
- let subst, ind_univs =
- match mib.mind_universes with
- | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx
- | Polymorphic auctx ->
- let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
- let nas = Univ.AUContext.names auctx in
- let auctx = Univ.AUContext.repr auctx in
- subst, Polymorphic_entry (nas, auctx)
- in
- let variance = match mib.mind_variance with
- | None -> None
- | Some _ -> Some (InferCumulativity.dummy_variance ind_univs)
- in
- let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
- let inds =
- Array.map_to_list
- (fun mip ->
- let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
- let arity = discharge ty in
- let lc = Array.map discharge mip.mind_user_lc in
- (mip.mind_typename,
- arity, template,
- Array.to_list mip.mind_consnames,
- Array.to_list lc))
- mib.mind_packets in
- let section_decls' = Context.Named.map discharge section_decls in
- let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
- let record = match mib.mind_record with
- | PrimRecord info ->
- Some (Some (Array.map (fun (x,_,_,_) -> x) info))
- | FakeRecord -> Some None
- | NotRecord -> None
- in
- { mind_entry_record = record;
- mind_entry_finite = mib.mind_finite;
- mind_entry_params = params';
- mind_entry_inds = inds';
- mind_entry_private = mib.mind_private;
- mind_entry_variance = variance;
- mind_entry_universes = ind_univs
- }
-
diff --git a/interp/discharge.mli b/interp/discharge.mli
deleted file mode 100644
index f7408937cf..0000000000
--- a/interp/discharge.mli
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Declarations
-open Entries
-open Opaqueproof
-
-val process_inductive :
- Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 1262dbb181..b65a171ef9 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -16,5 +16,4 @@ Implicit_quantifiers
Constrintern
Modintern
Constrextern
-Discharge
Declare
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7f084fffdd..08619d912e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1190,7 +1190,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
| GCast(t1, c1), NCast(t2, c2) ->
match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
- | GSort (GType _), NSort (GType _) when not u -> sigma
+
+ (* Next pair of lines useful only if not coming from detyping *)
+ | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match
+ | GSort _, NSort (UAnonymous _) when not u -> sigma
+
| GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
| GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:23:13 +0000