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.ml100
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/impargs.ml14
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/notation_ops.ml25
-rw-r--r--interp/notation_term.ml1
11 files changed, 87 insertions, 108 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 23c68b5e18..07a0066ea8 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;
@@ -479,20 +477,7 @@ type universe_source =
| QualifiedUniv of Id.t (* global universe introduced by some global value *)
| UnqualifiedUniv (* other global universe *)
-type universe_decl = universe_source * Nametab.universe_id
-
-let add_universe src (dp, i) =
- let level = Univ.Level.make dp i in
- let optpoly = match src with
- | BoundUniv -> Some true
- | UnqualifiedUniv -> Some false
- | QualifiedUniv _ -> None
- in
- Option.iter (fun poly ->
- let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
- Global.push_context_set poly ctx;
- if poly then Lib.add_section_context ctx)
- optpoly
+type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
let check_exists sp =
let depth = sections_depth () in
@@ -501,41 +486,42 @@ let check_exists sp =
alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
else ()
-let qualify_univ src (sp,i as orig) =
+let qualify_univ i sp src id =
+ let open Libnames in
match src with
- | BoundUniv | UnqualifiedUniv -> orig
+ | BoundUniv | UnqualifiedUniv ->
+ let sp = dirpath sp in
+ i, make_path sp id
| QualifiedUniv l ->
- let sp0, id = Libnames.repr_path sp in
- let sp0 = DirPath.repr sp0 in
- Libnames.make_path (DirPath.make (l::sp0)) id, i+1
-
-let cache_universe ((sp, _), (src, id)) =
- let sp, i = qualify_univ src (sp,1) in
- let () = check_exists sp in
- let () = Nametab.push_universe (Nametab.Until i) sp id in
- add_universe src id
-
-let load_universe i ((sp, _), (src, id)) =
- let sp, i = qualify_univ src (sp,i) in
- let () = Nametab.push_universe (Nametab.Until i) sp id in
- add_universe src id
-
-let open_universe i ((sp, _), (src, id)) =
- let sp, i = qualify_univ src (sp,i) in
- let () = Nametab.push_universe (Nametab.Exactly i) sp id in
- ()
-
-let discharge_universe = function
+ let sp = dirpath sp in
+ let sp = DirPath.repr sp in
+ Nametab.map_visibility succ i, make_path (DirPath.make (l::sp)) id
+
+let do_univ_name ~check i sp src (id,univ) =
+ let i, sp = qualify_univ i sp 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 load_univ_names i ((sp, _), (src, univs)) =
+ List.iter (do_univ_name ~check:false (Nametab.Until i) sp src) univs
+
+let open_univ_names i ((sp, _), (src, univs)) =
+ List.iter (do_univ_name ~check:false (Nametab.Exactly i) sp src) univs
+
+let discharge_univ_names = function
| _, (BoundUniv, _) -> None
| _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
-let input_universe : universe_decl -> Libobject.obj =
+let input_univ_names : universe_name_decl -> Libobject.obj =
declare_object
{ (default_object "Global universe name state") with
- cache_function = cache_universe;
- load_function = load_universe;
- open_function = open_universe;
- discharge_function = discharge_universe;
+ cache_function = cache_univ_names;
+ load_function = load_univ_names;
+ open_function = open_univ_names;
+ discharge_function = discharge_univ_names;
subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
classify_function = (fun a -> Substitute a) }
@@ -551,12 +537,12 @@ let declare_univ_binders gr pl =
anomaly ~label:"declare_univ_binders"
Pp.(str "declare_univ_binders on an constructor reference")
in
- Id.Map.iter (fun id lvl ->
- match Univ.Level.name lvl with
- | None -> ()
- | Some na ->
- ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na))))
- pl
+ let univs = Id.Map.fold (fun id univ univs ->
+ match Univ.Level.name univ with
+ | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
+ | Some univ -> (id,univ)::univs) pl []
+ in
+ Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
let do_universe poly l =
let in_section = Lib.sections_are_opened () in
@@ -570,10 +556,12 @@ let do_universe poly l =
let lev = UnivGen.new_univ_id () in
(id, lev)) l
in
+ let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx)
+ Univ.LSet.empty l, Univ.Constraint.empty
+ in
+ let () = declare_universe_context poly ctx in
let src = if poly then BoundUniv else UnqualifiedUniv in
- List.iter (fun (id,lev) ->
- ignore(Lib.add_leaf id (input_universe (src, lev))))
- l
+ Lib.add_anonymous_leaf (input_univ_names (src, l))
let do_constraint poly l =
let open Univ in
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..ab57176643 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 *)
@@ -155,11 +153,13 @@ let protect g e na =
if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
e',na
-let apply_cases_pattern ?loc ((ids,disjpat),id) c =
- let tm = DAst.make ?loc (GVar id) in
+let apply_cases_pattern_term ?loc (ids,disjpat) tm c =
let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in
DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
+let apply_cases_pattern ?loc (ids_disjpat,id) c =
+ apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c
+
let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let lt x = DAst.make ?loc x in lt @@ match nc with
| NVar id -> GVar id
@@ -184,7 +184,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let e',disjpat,na = g e na in
(match disjpat with
| None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
- | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c)))
+ | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
| NCases (sty,rtntypopt,tml,eqnl) ->
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
@@ -220,7 +220,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 +439,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 +638,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 +1210,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 16:23:54 +0000