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.mli24
-rw-r--r--interp/declare.ml100
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/impargs.ml14
-rw-r--r--interp/notation.ml2
6 files changed, 79 insertions, 71 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 23d0536df8..d5f0b7bff6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -526,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/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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 09:43:23 +0000