aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml1
-rw-r--r--interp/constrexpr_ops.ml16
-rw-r--r--interp/constrexpr_ops.mli24
-rw-r--r--interp/constrextern.ml3
-rw-r--r--interp/constrintern.ml7
-rw-r--r--interp/declare.ml11
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/impargs.ml14
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/notation_ops.ml17
-rw-r--r--interp/notation_term.ml1
11 files changed, 42 insertions, 56 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index d8dd4ef6dd..77d612cfd9 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -114,7 +114,6 @@ and constr_expr_r =
| CGeneralization of binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
- | CProj of qualid * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr (* expression that is being matched *)
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 011c4a6e4e..d5f0b7bff6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -177,12 +177,10 @@ 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) ->
- qualid_eq 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 _ | CProj _), _ -> false
+ | CGeneralization _ | CDelimiters _ ), _ -> false
and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_ast explicitation_eq) e1 e2 &&
@@ -359,8 +357,6 @@ 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 =
@@ -439,8 +435,6 @@ let map_constr_expr_with_binders g f e = CAst.map (function
let e'' = List.fold_left (fun e ({ CAst.v = 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 *)
@@ -532,6 +526,14 @@ let mkAppC (f,l) =
| CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
| _ -> CAst.make @@ CApp ((None, f), l)
+let mkProdCN ?loc bll c =
+ if bll = [] then c else
+ CAst.make ?loc @@ CProdN (bll,c)
+
+let mkLambdaCN ?loc bll c =
+ if bll = [] then c else
+ CAst.make ?loc @@ CLambdaN (bll,c)
+
let mkCProdN ?loc bll c =
CAst.make ?loc @@ CProdN (bll,c)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 61e8aa1b51..9e83bde8b2 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -38,22 +38,36 @@ val constr_loc : constr_expr -> Loc.t option
val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option
val local_binders_loc : local_binder_expr list -> Loc.t option
-(** {6 Constructors}*)
+(** {6 Constructors} *)
+
+(** {7 Term constructors} *)
+
+(** Basic form of the corresponding constructors *)
val mkIdentC : Id.t -> constr_expr
val mkRefC : qualid -> constr_expr
-val mkAppC : constr_expr * constr_expr list -> constr_expr
val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr
val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr
val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
-val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
-(** Same as [abstract_constr_expr], with location *)
+val mkAppC : constr_expr * constr_expr list -> constr_expr
+(** Basic form of application, collapsing nested applications *)
+(** Optimized constructors: does not add a constructor for an empty binder list *)
+
+val mkLambdaCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkProdCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+
+(** Aliases for the corresponding constructors; generally [mkLambdaCN] and
+ [mkProdCN] should be preferred *)
+
+val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
-(** Same as [prod_constr_expr], with location *)
+(** {7 Pattern constructors} *)
+
+(** Interpretation of a list of patterns as a disjunctive pattern (optimized) *)
val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr
val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3996a1756c..98e1f6dd36 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -958,9 +958,6 @@ let rec extern inctx scopes vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
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)
in insert_coercion coercion (CAst.make ?loc c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1c8d957014..d02f59414e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2062,13 +2062,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CCast (c1, c2) ->
DAst.make ?loc @@
GCast (intern env c1, map_cast_type (intern_type env) c2)
- | CProj (pr, c) ->
- match intern_reference pr with
- | ConstRef p ->
- let p = Option.get @@ Recordops.find_primitive_projection p in
- 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)
diff --git a/interp/declare.ml b/interp/declare.ml
index 22e6cf9d1c..f4e57073cc 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -78,7 +78,6 @@ let check_exists sp =
let cache_constant ((sp,kn), obj) =
let id = basename sp in
- let _,dir,_ = KerName.repr kn in
let kn' =
match obj.cst_decl with
| None ->
@@ -87,7 +86,7 @@ let cache_constant ((sp,kn), obj) =
else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
| Some decl ->
let () = check_exists sp in
- Global.add_constant dir id decl
+ Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl
in
assert (Constant.equal kn' (Constant.make1 kn));
Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
@@ -136,7 +135,7 @@ let register_side_effect (c, role) =
cst_kind = IsProof Theorem;
cst_locl = false;
} in
- let id = Label.to_id (pi3 (Constant.repr3 c)) in
+ let id = Label.to_id (Constant.label c) in
ignore(add_leaf id o);
update_tables c;
match role with
@@ -311,8 +310,7 @@ let cache_inductive ((sp,kn),mie) =
let names = inductive_names sp kn mie in
List.iter check_exists (List.map fst names);
let id = basename sp in
- let _,dir,_ = KerName.repr kn in
- let kn' = Global.add_mind dir id mie in
+ let kn' = Global.add_mind id mie in
assert (MutInd.equal kn' (MutInd.make1 kn));
let mind = Global.lookup_mind kn' in
add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
@@ -491,7 +489,6 @@ let add_universe src (dp, i) =
Option.iter (fun poly ->
let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
Global.push_context_set poly ctx;
- UnivNames.add_global_universe level poly;
if poly then Lib.add_section_context ctx)
optpoly
@@ -580,7 +577,7 @@ let do_constraint poly l =
let open Univ in
let u_of_id x =
let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
- UnivNames.is_polymorphic level, level
+ Lib.is_polymorphic_univ level, level
in
let in_section = Lib.sections_are_opened () in
let () =
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index ccad6b19eb..f5be0ddbae 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -234,7 +234,7 @@ let add_glob ?loc ref =
add_glob_gen ?loc sp lib_dp ty
let mp_of_kn kn =
- let mp,sec,l = Names.KerName.repr kn in
+ let mp,l = Names.KerName.repr kn in
Names.MPdot (mp,l)
let add_glob_kn ?loc kn =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 3603367cf1..ce33cb8731 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -561,29 +561,27 @@ let discharge_implicits (_,(req,l)) =
| ImplInteractive (ref,flags,exp) ->
(try
let vars = variable_section_segment_of_reference ref in
- let ref' = if isVarRef ref then ref else pop_global_reference ref in
let extra_impls = impls_of_context vars in
- let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
- Some (ImplInteractive (ref',flags,exp),l')
+ let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
+ Some (ImplInteractive (ref,flags,exp),l')
with Not_found -> (* ref not defined in this section *) Some (req,l))
| ImplConstant (con,flags) ->
(try
- let con' = pop_con 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
- Some (ImplConstant (con',flags),l')
+ let l' = [ConstRef con,newimpls] in
+ Some (ImplConstant (con,flags),l')
with Not_found -> (* con not defined in this section *) Some (req,l))
| ImplMutualInductive (kn,flags) ->
(try
let l' = List.map (fun (gr, l) ->
let vars = variable_section_segment_of_reference gr in
let extra_impls = impls_of_context vars in
- ((if isVarRef gr then gr else pop_global_reference gr),
+ (gr,
List.map (add_section_impls vars extra_impls) l)) l
in
- Some (ImplMutualInductive (pop_kn kn,flags),l')
+ Some (ImplMutualInductive (kn,flags),l')
with Not_found -> (* ref not defined in this section *) Some (req,l))
let rebuild_implicits (req,l) =
diff --git a/interp/notation.ml b/interp/notation.ml
index 02c7812e21..6104ab16c7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1304,7 +1304,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
vars |> List.map fst |> List.filter is_local_assum |> List.length
with
Not_found (* Not a ref defined in this section *) -> 0 in
- Some (req,Lib.discharge_global r,n,l,[])
+ Some (req,r,n,l,[])
let classify_arguments_scope (req,_,_,_,_ as obj) =
if req == ArgsScopeNoDischarge then Dispose else Substitute obj
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 06943ce7b9..ff5e2bb5f3 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -89,11 +89,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
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 _ | NProj _), _ -> false
+ | NRec _ | NSort _ | NCast _ ), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -220,7 +218,6 @@ 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 =
@@ -440,7 +437,6 @@ let notation_constr_and_vars_of_glob_constr recvars 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
@@ -640,12 +636,6 @@ let rec subst_notation_constr subst bound raw =
let k' = 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 p' = subst_proj subst p in
- let c' = subst_notation_constr subst bound c in
- if p' == p && c' == c then raw else NProj(p', 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)
@@ -1218,12 +1208,9 @@ 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 _ | GProj _ ), _ -> raise No_match
+ | GCast _ ), _ -> raise No_match
and match_in u = match_ true u
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 942ea5ff3f..5fb0ca1b43 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -43,7 +43,6 @@ type notation_constr =
notation_constr array * notation_constr array
| NSort of glob_sort
| NCast of notation_constr * notation_constr cast_type
- | NProj of Projection.t * notation_constr
(** Note concerning NList: first constr is iterator, second is terminator;
first id is where each argument of the list has to be substituted
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:10:20 +0000