aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml34
-rw-r--r--interp/declare.ml52
-rw-r--r--interp/discharge.ml6
-rw-r--r--interp/impargs.ml9
-rw-r--r--interp/modintern.ml4
5 files changed, 52 insertions, 53 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 838ef40545..70ce6cef19 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -716,20 +716,20 @@ let rec flatten_application c = match DAst.get c with
(* one with no delimiter if possible) *)
let extern_possible_prim_token (custom,scopes) r =
- try
- let (sc,n) = uninterp_prim_token r in
- match availability_of_entry_coercion custom InConstrEntrySomeLevel with
- | None -> raise No_match
- | Some coercion ->
- match availability_of_prim_token n sc scopes with
- | None -> None
- | Some key -> Some (insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key))
- with No_match ->
- None
-
-let extern_optimal_prim_token scopes r r' =
- let c = extern_possible_prim_token scopes r in
- let c' = if r==r' then None else extern_possible_prim_token scopes r' in
+ let (sc,n) = uninterp_prim_token r in
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
+ match availability_of_prim_token n sc scopes with
+ | None -> raise No_match
+ | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+
+let extern_possible extern r =
+ try Some (extern r) with No_match -> None
+
+let extern_optimal extern r r' =
+ let c = extern_possible extern r in
+ let c' = if r==r' then None else extern_possible extern r' in
match c,c' with
| Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n
| _ -> raise No_match
@@ -769,12 +769,14 @@ let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_optimal_prim_token scopes r r'
+ extern_optimal (extern_possible_prim_token scopes) r r'
with No_match ->
try
let r'' = flatten_application r' in
if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_notation scopes vars r'' (uninterp_notations r'')
+ extern_optimal
+ (fun r -> extern_notation scopes vars r (uninterp_notations r))
+ r r''
with No_match ->
let loc = r'.CAst.loc in
match DAst.get r' with
diff --git a/interp/declare.ml b/interp/declare.ml
index 7a32018c0e..1e972d3e35 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -219,7 +219,7 @@ let cache_variable ((sp,_),o) =
let (body, uctx), () = Future.force de.const_entry_body in
let poly, univs = match de.const_entry_universes with
| Monomorphic_const_entry uctx -> false, uctx
- | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx
+ | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
in
let univs = Univ.ContextSet.union uctx univs in
(** We must declare the universe constraints before type-checking the
@@ -339,7 +339,7 @@ let infer_inductive_subtyping mind_ent =
match mind_ent.mind_entry_universes with
| Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
mind_ent
- | Cumulative_ind_entry cumi ->
+ | Cumulative_ind_entry (_, cumi) ->
begin
let env = Global.env () in
(* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
@@ -358,27 +358,26 @@ let inInductive : mutual_inductive_entry -> obj =
let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
let id = Label.to_id label in
- let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
- Recordops.declare_primitive_projection p;
- (* ^ needs to happen before declaring the constant, otherwise
- Heads gets confused. *)
let univs = match univs with
| Monomorphic_ind_entry _ ->
(** Global constraints already defined through the inductive *)
Monomorphic_const_entry Univ.ContextSet.empty
- | Polymorphic_ind_entry ctx ->
- Polymorphic_const_entry ctx
- | Cumulative_ind_entry ctx ->
- Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
+ | Polymorphic_ind_entry (nas, ctx) ->
+ Polymorphic_const_entry (nas, ctx)
+ | Cumulative_ind_entry (nas, ctx) ->
+ Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx)
in
let term, types = match univs with
| Monomorphic_const_entry _ -> term, types
- | Polymorphic_const_entry ctx ->
+ | Polymorphic_const_entry (_, ctx) ->
let u = Univ.UContext.instance ctx in
Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
in
let entry = definition_entry ~types ~univs term in
- ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent))
+ let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
+ let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
+ Recordops.declare_primitive_projection p cst
+
let declare_projections univs mind =
let env = Global.env () in
@@ -473,36 +472,33 @@ type universe_source =
type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
let check_exists sp =
- let depth = sections_depth () in
- let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in
if Nametab.exists_universe sp then
alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
else ()
-let qualify_univ i sp src id =
- let open Libnames in
+let qualify_univ i dp src id =
match src with
| BoundUniv | UnqualifiedUniv ->
- let sp = dirpath sp in
- i, make_path sp id
+ i, Libnames.make_path dp id
| QualifiedUniv l ->
- let sp = dirpath sp in
- let sp = DirPath.repr sp in
- Nametab.map_visibility succ i, make_path (DirPath.make (l::sp)) id
+ let dp = DirPath.repr dp in
+ Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id
-let do_univ_name ~check i sp src (id,univ) =
- let i, sp = qualify_univ i sp src id in
+let do_univ_name ~check i dp src (id,univ) =
+ let i, sp = qualify_univ i dp src id in
if check then check_exists sp;
Nametab.push_universe i sp univ
let cache_univ_names ((sp, _), (src, univs)) =
- List.iter (do_univ_name ~check:true (Nametab.Until 1) sp src) univs
+ let depth = sections_depth () in
+ let dp = pop_dirpath_n depth (dirpath sp) in
+ List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs
let load_univ_names i ((sp, _), (src, univs)) =
- List.iter (do_univ_name ~check:false (Nametab.Until i) sp src) univs
+ List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs
let open_univ_names i ((sp, _), (src, univs)) =
- List.iter (do_univ_name ~check:false (Nametab.Exactly i) sp src) univs
+ List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs
let discharge_univ_names = function
| _, (BoundUniv, _) -> None
@@ -520,12 +516,12 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
let declare_univ_binders gr pl =
if Global.is_polymorphic gr then
- UnivNames.register_universe_binders gr pl
+ ()
else
let l = match gr with
| ConstRef c -> Label.to_id @@ Constant.label c
| IndRef (c, _) -> Label.to_id @@ MutInd.label c
- | VarRef id -> id
+ | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
| ConstructRef _ ->
anomaly ~label:"declare_univ_binders"
Pp.(str "declare_univ_binders on an constructor reference")
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 21b2e85e8f..eeda5a6867 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -79,13 +79,15 @@ let process_inductive info modlist mib =
| Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
| Polymorphic_ind 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_ind_entry auctx
+ subst, Polymorphic_ind_entry (nas, auctx)
| Cumulative_ind cumi ->
let auctx = Univ.ACumulativityInfo.univ_context cumi in
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, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx)
+ subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx)
in
let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
let inds =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d8582d856e..d024a9e808 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -19,7 +19,6 @@ open Decl_kinds
open Lib
open Libobject
open EConstr
-open Termops
open Reductionops
open Constrexpr
open Namegen
@@ -200,16 +199,16 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
acc.(i) <- update pos rig acc.(i)
| App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
if strict then () else
- iter_constr_with_full_binders sigma push_lift (frec false) ed c
+ iter_with_full_binders sigma push_lift (frec false) ed c
| Proj (p,c) when rig ->
if strict then () else
- iter_constr_with_full_binders sigma push_lift (frec false) ed c
+ iter_with_full_binders sigma push_lift (frec false) ed c
| Case _ when rig ->
if strict then () else
- iter_constr_with_full_binders sigma push_lift (frec false) ed c
+ iter_with_full_binders sigma push_lift (frec false) ed c
| Evar _ -> ()
| _ ->
- iter_constr_with_full_binders sigma push_lift (frec rig) ed c
+ iter_with_full_binders sigma push_lift (frec rig) ed c
in
let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in
acc
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 51e27299e3..60056dfd90 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -107,8 +107,8 @@ let transl_with_decl env base kind = function
let c, ectx = interp_constr env sigma c in
let poly = lookup_polymorphism env base kind fqid in
begin match UState.check_univ_decl ~poly ectx udecl with
- | Entries.Polymorphic_const_entry ctx ->
- let inst, ctx = Univ.abstract_universes ctx in
+ | Entries.Polymorphic_const_entry (nas, ctx) ->
+ let inst, ctx = Univ.abstract_universes nas ctx in
let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
let c = EConstr.to_constr sigma c in
WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:08:39 +0000