aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml8
-rw-r--r--interp/constrexpr_ops.mli2
-rw-r--r--interp/constrextern.ml3
-rw-r--r--interp/constrintern.ml24
-rw-r--r--interp/declare.ml12
-rw-r--r--interp/discharge.ml6
-rw-r--r--interp/impargs.ml2
-rw-r--r--interp/notation_ops.ml19
8 files changed, 59 insertions, 17 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 7cc8de85d2..da04d8786b 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -173,10 +173,12 @@ let rec constr_expr_eq e1 e2 =
| CDelimiters(s1,e1), CDelimiters(s2,e2) ->
String.equal s1 s2 &&
constr_expr_eq e1 e2
+ | CProj(p1,c1), CProj(p2,c2) ->
+ eq_reference p1 p2 && constr_expr_eq c1 c2
| (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
| CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
| CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
- | CGeneralization _ | CDelimiters _), _ -> false
+ | CGeneralization _ | CDelimiters _ | CProj _), _ -> false
and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_located explicitation_eq) e1 e2 &&
@@ -365,6 +367,8 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (_,_) ->
Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
+ | CProj (_,c) ->
+ f n acc c
)
let free_vars_of_constr_expr c =
@@ -446,6 +450,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function
let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,bl',t',d')) dl)
+ | CProj (p,c) ->
+ CProj (p, f e c)
)
(* Used in constrintern *)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 3ecb3d3212..6e5c0f8515 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -84,7 +84,7 @@ val names_of_local_assums : local_binder_expr list -> Name.t located list
(** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into
account. *)
-(** { 6 Folds and maps } *)
+(** {6 Folds and maps} *)
(** Used in typeclasses *)
val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1330b3741e..4f7d537d3f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -908,6 +908,9 @@ let rec extern inctx scopes vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
Miscops.map_cast_type (extern_typ scopes vars) c')
+ | GProj (p, c) ->
+ let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in
+ CProj (pr, sub_extern inctx scopes vars c)
) r'
and extern_typ (_,scopes) =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 61b33aa415..4afe301dd7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -836,6 +836,18 @@ let intern_reference ref =
in
Smartlocate.global_of_extended_global r
+let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option =
+ match info with
+ | Misctypes.UAnonymous -> None
+ | Misctypes.UUnknown -> None
+ | Misctypes.UNamed id -> Some (id, 0)
+
+let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
+ match level with
+ | Misctypes.GProp -> Misctypes.GProp
+ | Misctypes.GSet -> Misctypes.GSet
+ | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
+
(* Is it a global reference or a syntactic definition? *)
let intern_qualid loc qid intern env lvar us args =
match intern_extended_global_of_qualid (loc,qid) with
@@ -867,6 +879,10 @@ let intern_qualid loc qid intern env lvar us args =
DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
| _ -> err ()
end
+ | Some [s], GSort (Misctypes.GType []) -> 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)
| Some _, _ -> err ()
in
c, projapp, args2
@@ -1869,7 +1885,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CCast (c1, c2) ->
DAst.make ?loc @@
GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
- )
+ | CProj (pr, c) ->
+ match intern_reference pr with
+ | ConstRef p ->
+ DAst.make ?loc @@ GProj (Projection.make p false, intern env c)
+ | _ ->
+ raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *)
+ )
and intern_type env = intern (set_type_scope env)
and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
diff --git a/interp/declare.ml b/interp/declare.ml
index d1b79ffcdd..72cdabfd20 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -104,7 +104,7 @@ 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 hyps,subst,uctx = section_segment_of_constant con in
+ let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in
let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
let abstract = (named_of_variable_context hyps, subst, uctx) in
let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
@@ -333,7 +333,8 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
let mind = Global.mind_of_delta_kn kn in
let mie = Global.lookup_mind mind in
let repl = replacement_context () in
- let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in
+ let info = section_segment_of_mutual_inductive mind in
+ let sechyps = info.Lib.abstr_ctx in
Some (discharged_hyps kn sechyps,
Discharge.process_inductive info repl mie)
@@ -363,13 +364,8 @@ let infer_inductive_subtyping (pth, mind_ent) =
| Cumulative_ind_entry cumi ->
begin
let env = Global.env () in
- let env' =
- Environ.push_context
- (Univ.CumulativityInfo.univ_context cumi) env
- in
(* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
- let evd = Evd.from_env env' in
- (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
+ (pth, InferCumulativity.infer_inductive env mind_ent)
end
type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 5b4b5f67b8..710f88c3ff 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -78,8 +78,8 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
let ctx = List.rev mip.mind_arity_ctxt in
mkArity (List.rev ctx, Type ar.template_level), true
-let process_inductive (section_decls,_,_ as info) modlist mib =
- let section_decls = Lib.named_of_variable_context section_decls in
+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
@@ -92,7 +92,7 @@ let process_inductive (section_decls,_,_ as info) modlist mib =
let auctx = Univ.ACumulativityInfo.univ_context cumi in
let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
let auctx = Univ.AUContext.repr auctx in
- subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
+ subst, Cumulative_ind_entry (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 3105214d5e..ed1cd5276c 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -548,7 +548,7 @@ let discharge_implicits (_,(req,l)) =
| ImplConstant (con,flags) ->
(try
let con' = pop_con con in
- let vars,_,_ = section_segment_of_constant con in
+ let vars = variable_section_segment_of_reference (ConstRef con) in
let extra_impls = impls_of_context vars in
let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
let l' = [ConstRef con',newimpls] in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 20492e38c8..326d05cba6 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -86,9 +86,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
Miscops.glob_sort_eq s1 s2
| NCast (t1, c1), NCast (t2, c2) ->
(eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
+| NProj (p1, c1), NProj (p2, c2) ->
+ Projection.equal p1 p2 && eq_notation_constr vars c1 c2
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _), _ -> false
+ | NRec _ | NSort _ | NCast _ | NProj _), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -189,6 +191,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NSort x -> GSort x
| NHole (x, naming, arg) -> GHole (x, naming, arg)
| NRef x -> GRef (x,None)
+ | NProj (p,c) -> GProj (p, f e c)
let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
@@ -383,6 +386,7 @@ let notation_constr_and_vars_of_glob_constr a =
if arg != None then has_ltac := true;
NHole (w, naming, arg)
| GRef (r,_) -> NRef r
+ | GProj (p, c) -> NProj (p, aux c)
| GEvar _ | GPatVar _ ->
user_err Pp.(str "Existential variables not allowed in notations.")
) x
@@ -576,6 +580,14 @@ let rec subst_notation_constr subst bound raw =
let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in
if r1' == r1 && k' == k then raw else NCast(r1',k')
+ | NProj (p, c) ->
+ let kn = Projection.constant p in
+ let b = Projection.unfolded p in
+ let kn' = subst_constant subst kn in
+ let c' = subst_notation_constr subst bound c in
+ if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c')
+
+
let subst_interpretation subst (metas,pat) =
let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
(metas,subst_notation_constr subst bound pat)
@@ -1167,9 +1179,12 @@ let rec match_ inner u alp metas sigma a1 a2 =
match_names metas (alp,sigma) (Name id') na in
match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
+ | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 ->
+ match_in u alp metas sigma t1 t2
+
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
- | GCast _), _ -> raise No_match
+ | GCast _ | GProj _ ), _ -> raise No_match
and match_in u = match_ true u
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:40:30 +0000