aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml131
-rw-r--r--kernel/cClosure.mli46
-rw-r--r--kernel/clambda.ml2
-rw-r--r--kernel/constr.ml33
-rw-r--r--kernel/constr.mli9
-rw-r--r--kernel/conv_oracle.ml15
-rw-r--r--kernel/entries.ml10
-rw-r--r--kernel/environ.ml58
-rw-r--r--kernel/environ.mli10
-rw-r--r--kernel/indtypes.ml3
-rw-r--r--kernel/names.ml2
-rw-r--r--kernel/names.mli3
-rw-r--r--kernel/reduction.ml6
-rw-r--r--kernel/safe_typing.ml283
-rw-r--r--kernel/safe_typing.mli3
-rw-r--r--kernel/term_typing.ml272
-rw-r--r--kernel/term_typing.mli42
-rw-r--r--kernel/typeops.ml93
-rw-r--r--kernel/typeops.mli30
-rw-r--r--kernel/univ.ml3
-rw-r--r--kernel/univ.mli3
-rw-r--r--kernel/vars.ml14
-rw-r--r--kernel/vars.mli2
23 files changed, 577 insertions, 496 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 819a66c190..c558689595 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -224,11 +224,6 @@ let unfold_red kn =
* abstractions, storing a representation (of type 'a) of the body of
* this constant or abstraction.
* * i_tab is the cache table of the results
- * * i_repr is the function to get the representation from the current
- * state of the cache and the body of the constant. The result
- * is stored in the table.
- * * i_rels is the array of free rel variables together with their optional
- * body
*
* ref_value_cache searchs in the tab, otherwise uses i_repr to
* compute the result and store it in the table. If the constant can't
@@ -256,74 +251,12 @@ end
module KeyTable = Hashtbl.Make(IdKeyHash)
-let eq_table_key = IdKeyHash.equal
-
-type 'a infos_tab = 'a KeyTable.t
-
-type 'a infos_cache = {
- i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
- i_env : env;
- i_sigma : existential -> constr option;
- i_rels : (Constr.rel_declaration * lazy_val) Range.t;
- i_share : bool;
-}
-
-and 'a infos = {
- i_flags : reds;
- i_cache : 'a infos_cache }
-
-let info_flags info = info.i_flags
-let info_env info = info.i_cache.i_env
-
open Context.Named.Declaration
let assoc_defined id env = match Environ.lookup_named id env with
| LocalDef (_, c, _) -> c
| _ -> raise Not_found
-let ref_value_cache ({i_cache = cache;_} as infos) tab ref =
- try
- Some (KeyTable.find tab ref)
- with Not_found ->
- try
- let body =
- match ref with
- | RelKey n ->
- let open! Context.Rel.Declaration in
- let i = n - 1 in
- let (d, _) =
- try Range.get cache.i_rels i
- with Invalid_argument _ -> raise Not_found
- in
- begin match d with
- | LocalAssum _ -> raise Not_found
- | LocalDef (_, t, _) -> lift n t
- end
- | VarKey id -> assoc_defined id cache.i_env
- | ConstKey cst -> constant_value_in cache.i_env cst
- in
- let v = cache.i_repr infos tab body in
- KeyTable.add tab ref v;
- Some v
- with
- | Not_found (* List.assoc *)
- | NotEvaluableConst _ (* Const *)
- -> None
-
-let evar_value cache ev =
- cache.i_sigma ev
-
-let create ~repr ~share flgs env evars =
- let cache =
- { i_repr = repr;
- i_env = env;
- i_sigma = evars;
- i_rels = env.env_rel_context.env_rel_map;
- i_share = share;
- }
- in { i_flags = flgs; i_cache = cache }
-
-
(**********************************************************************)
(* Lazy reduction: the one used in kernel operations *)
@@ -391,6 +324,23 @@ let update ~share v1 no t =
v1)
else {norm=no;term=t}
+(** Reduction cache *)
+
+type infos_cache = {
+ i_env : env;
+ i_sigma : existential -> constr option;
+ i_share : bool;
+}
+
+type clos_infos = {
+ i_flags : reds;
+ i_cache : infos_cache }
+
+type clos_tab = fconstr KeyTable.t
+
+let info_flags info = info.i_flags
+let info_env info = info.i_cache.i_env
+
(**********************************************************************)
(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
@@ -539,6 +489,8 @@ let mk_clos e t =
| (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
{norm = Red; term = FCLOS(t,e)}
+let inject c = mk_clos (subs_id 0) c
+
(** Hand-unrolling of the map function to bypass the call to the generic array
allocation *)
let mk_clos_vect env v = match v with
@@ -550,6 +502,35 @@ let mk_clos_vect env v = match v with
[|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|]
| v -> Array.Fun1.map mk_clos env v
+let ref_value_cache ({ i_cache = cache; _ }) tab ref =
+ try
+ Some (KeyTable.find tab ref)
+ with Not_found ->
+ try
+ let body =
+ match ref with
+ | RelKey n ->
+ let open! Context.Rel.Declaration in
+ let i = n - 1 in
+ let (d, _) =
+ try Range.get cache.i_env.env_rel_context.env_rel_map i
+ with Invalid_argument _ -> raise Not_found
+ in
+ begin match d with
+ | LocalAssum _ -> raise Not_found
+ | LocalDef (_, t, _) -> lift n t
+ end
+ | VarKey id -> assoc_defined id cache.i_env
+ | ConstKey cst -> constant_value_in cache.i_env cst
+ in
+ let v = inject body in
+ KeyTable.add tab ref v;
+ Some v
+ with
+ | Not_found (* List.assoc *)
+ | NotEvaluableConst _ (* Const *)
+ -> None
+
(* The inverse of mk_clos: move back to constr *)
let rec to_constr lfts v =
match v.term with
@@ -944,7 +925,7 @@ let rec knr info tab m stk =
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
knit info tab (subs_cons([|v|],e)) bd stk
| FEvar(ev,env) ->
- (match evar_value info.i_cache ev with
+ (match info.i_cache.i_sigma ev with
Some c -> knit info tab env c stk
| None -> (m,stk))
| FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _
@@ -1040,8 +1021,6 @@ let whd_val info tab v =
let norm_val info tab v =
with_stats (lazy (kl info tab v))
-let inject c = mk_clos (subs_id 0) c
-
let whd_stack infos tab m stk = match m.norm with
| Whnf | Norm ->
(** No need to perform [kni] nor to unlock updates because
@@ -1052,19 +1031,19 @@ let whd_stack infos tab m stk = match m.norm with
let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
k
-(* cache of constants: the body is computed only when needed. *)
-type clos_infos = fconstr infos
-
let create_clos_infos ?(evars=fun _ -> None) flgs env =
let share = (Environ.typing_flags env).Declarations.share_reduction in
- create ~share ~repr:(fun _ _ c -> inject c) flgs env evars
+ let cache = {
+ i_env = env;
+ i_sigma = evars;
+ i_share = share;
+ } in
+ { i_flags = flgs; i_cache = cache }
let create_tab () = KeyTable.create 17
let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
-let env_of_infos infos = infos.i_cache.i_env
-
let infos_with_reds infos reds =
{ infos with i_flags = reds }
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 2a018d172a..1ee4bccc25 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -98,25 +98,7 @@ val unfold_red : evaluable_global_reference -> reds
(***********************************************************************)
type table_key = Constant.t Univ.puniverses tableKey
-type 'a infos_cache
-type 'a infos_tab
-type 'a infos = {
- i_flags : reds;
- i_cache : 'a infos_cache }
-
-val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option
-val create:
- repr:('a infos -> 'a infos_tab -> constr -> 'a) ->
- share:bool ->
- reds ->
- env ->
- (existential -> constr option) ->
- 'a infos
-val create_tab : unit -> 'a infos_tab
-val evar_value : 'a infos_cache -> existential -> constr option
-
-val info_env : 'a infos -> env
-val info_flags: 'a infos -> reds
+module KeyTable : Hashtbl.S with type key = table_key
(***********************************************************************
s Lazy reduction. *)
@@ -173,7 +155,6 @@ val stack_tail : int -> stack -> stack
val stack_nth : stack -> int -> fconstr
val zip_term : (fconstr -> constr) -> constr -> stack -> constr
val eta_expand_stack : stack -> stack
-val unfold_projection : 'a infos -> Projection.t -> stack_member option
(** To lazy reduce a constr, create a [clos_infos] with
[create_clos_infos], inject the term to reduce with [inject]; then use
@@ -193,27 +174,32 @@ val destFLambda :
(fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr
(** Global and local constant cache *)
-type clos_infos = fconstr infos
+type clos_infos
+type clos_tab
val create_clos_infos :
?evars:(existential->constr option) -> reds -> env -> clos_infos
val oracle_of_infos : clos_infos -> Conv_oracle.oracle
-val env_of_infos : 'a infos -> env
+val create_tab : unit -> clos_tab
+
+val info_env : clos_infos -> env
+val info_flags: clos_infos -> reds
+val unfold_projection : clos_infos -> Projection.t -> stack_member option
val infos_with_reds : clos_infos -> reds -> clos_infos
(** Reduction function *)
(** [norm_val] is for strong normalization *)
-val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
+val norm_val : clos_infos -> clos_tab -> fconstr -> constr
(** [whd_val] is for weak head normalization *)
-val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
+val whd_val : clos_infos -> clos_tab -> fconstr -> constr
(** [whd_stack] performs weak head normalization in a given stack. It
stops whenever a reduction is blocked. *)
val whd_stack :
- clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
+ clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
to the conversion of the eta expansion of t, considered as an inhabitant
@@ -230,9 +216,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
(** Conversion auxiliary functions to do step by step normalisation *)
(** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option
-
-val eq_table_key : table_key -> table_key -> bool
+val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr option
(***********************************************************************
i This is for lazy debug *)
@@ -243,9 +227,9 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array
val mk_clos : fconstr subs -> constr -> fconstr
val mk_clos_vect : fconstr subs -> constr array -> fconstr array
-val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
-val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
-val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr
+val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
+val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
+val kl : clos_infos -> clos_tab -> fconstr -> constr
val to_constr : lift -> fconstr -> constr
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index c21ce22421..1e4dbfd418 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -764,7 +764,7 @@ and lambda_of_app env f args =
and such, which can't be done at this time.
for instance, for int31: if one of the digit is
not closed, it's not impossible that the number
- gets fully instanciated at run-time, thus to ensure
+ gets fully instantiated at run-time, thus to ensure
uniqueness of the representation in the vm
it is necessary to try and build a caml integer
during the execution *)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c97969c0e0..d7f35da10d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -227,6 +227,12 @@ let mkMeta n = Meta n
(* Constructs a Variable named id *)
let mkVar id = Var id
+let mkRef (gr,u) = let open GlobRef in match gr with
+ | ConstRef c -> mkConstU (c,u)
+ | IndRef ind -> mkIndU (ind,u)
+ | ConstructRef c -> mkConstructU (c,u)
+ | VarRef x -> mkVar x
+
(************************************************************************)
(* kind_of_term = constructions as seen by the user *)
(************************************************************************)
@@ -401,6 +407,12 @@ let destCoFix c = match kind c with
| CoFix cofix -> cofix
| _ -> raise DestKO
+let destRef c = let open GlobRef in match kind c with
+ | Var x -> VarRef x, Univ.Instance.empty
+ | Const (c,u) -> ConstRef c, u
+ | Ind (ind,u) -> IndRef ind, u
+ | Construct (c,u) -> ConstructRef c, u
+ | _ -> raise DestKO
(******************************************************************)
(* Flattening and unflattening of embedded applications and casts *)
@@ -440,6 +452,27 @@ let fold f acc c = match kind c with
| CoFix (_,(_lna,tl,bl)) ->
Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+let fold_with_full_binders g f n acc c =
+ let open Context.Rel.Declaration in
+ match kind c with
+ | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc
+ | Cast (c,_, t) -> f n (f n acc c) t
+ | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Proj (_,c) -> f n acc c
+ | Evar (_,l) -> Array.fold_left (f n) acc l
+ | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | CoFix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+
(* [iter f c] iters [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
not specified *)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 3c9cc96a0d..8753c20eac 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -128,6 +128,9 @@ val mkConstruct : constructor -> constr
val mkConstructU : pconstructor -> constr
val mkConstructUi : pinductive * int -> constr
+(** Make a constant, inductive, constructor or variable. *)
+val mkRef : GlobRef.t Univ.puniverses -> constr
+
(** Constructs a destructor of inductive type.
[mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac]
@@ -340,6 +343,8 @@ val destFix : constr -> fixpoint
val destCoFix : constr -> cofixpoint
+val destRef : constr -> GlobRef.t Univ.puniverses
+
(** {6 Equality} *)
(** [equal a b] is true if [a] equals [b] modulo alpha, casts,
@@ -465,6 +470,10 @@ val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Decla
val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
+val fold_with_full_binders :
+ (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
+ 'a -> 'b -> constr -> 'b
+
(** [map f c] maps [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
not specified *)
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index c74f2ab318..ac78064235 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -83,18 +83,27 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu =
let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate)
+let dep_order l2r k1 k2 = match k1, k2 with
+| RelKey _, RelKey _ -> l2r
+| RelKey _, (VarKey _ | ConstKey _) -> true
+| VarKey _, RelKey _ -> false
+| VarKey _, VarKey _ -> l2r
+| VarKey _, ConstKey _ -> true
+| ConstKey _, (RelKey _ | VarKey _) -> false
+| ConstKey _, ConstKey _ -> l2r
+
(* Unfold the first constant only if it is "more transparent" than the
second one. In case of tie, use the recommended default. *)
let oracle_order f o l2r k1 k2 =
match get_strategy o f k1, get_strategy o f k2 with
- | Expand, Expand -> l2r
+ | Expand, Expand -> dep_order l2r k1 k2
| Expand, (Opaque | Level _) -> true
| (Opaque | Level _), Expand -> false
- | Opaque, Opaque -> l2r
+ | Opaque, Opaque -> dep_order l2r k1 k2
| Level _, Opaque -> true
| Opaque, Level _ -> false
| Level n1, Level n2 ->
- if Int.equal n1 n2 then l2r
+ if Int.equal n1 n2 then dep_order l2r k1 k2
else n1 < n2
let get_strategy o = get_strategy o (fun x -> x)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 94248ad26b..c5bcd74072 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -16,14 +16,6 @@ open Constr
constants/axioms, mutual inductive definitions, modules and module
types *)
-
-(** {6 Local entries } *)
-
-type local_entry =
- | LocalDefEntry of constr
- | LocalAssumEntry of constr
-
-
(** {6 Declaration of inductive types. } *)
(** Assume the following definition in concrete syntax:
@@ -54,7 +46,7 @@ type mutual_inductive_entry = {
record in their respective projections. Not used by the kernel.
Some None: non-primitive record *)
mind_entry_finite : Declarations.recursivity_kind;
- mind_entry_params : (Id.t * local_entry) list;
+ mind_entry_params : Constr.rel_context;
mind_entry_inds : one_inductive_entry list;
mind_entry_universes : inductive_universes;
(* universe constraints and the constraints for subtyping of
diff --git a/kernel/environ.ml b/kernel/environ.ml
index dffcd70282..3b7e3ae544 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -419,12 +419,6 @@ let constant_type env (kn,u) =
let csts = constraints_of cb u in
(subst_instance_constr u cb.const_type, csts)
-let constant_context env kn =
- let cb = lookup_constant kn env in
- match cb.const_universes with
- | Monomorphic_const _ -> Univ.AUContext.empty
- | Polymorphic_const ctx -> ctx
-
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
@@ -550,28 +544,38 @@ let lookup_inductive_variables (kn,_i) env =
let lookup_constructor_variables (ind,_) env =
lookup_inductive_variables ind env
+(* Universes *)
+let constant_context env c =
+ let cb = lookup_constant c env in
+ Declareops.constant_polymorphic_context cb
+
+let universes_of_global env r =
+ let open GlobRef in
+ match r with
+ | VarRef _ -> Univ.AUContext.empty
+ | ConstRef c -> constant_context env c
+ | IndRef (mind,_) | ConstructRef ((mind,_),_) ->
+ let mib = lookup_mind mind env in
+ Declareops.inductive_polymorphic_context mib
+
(* Returns the list of global variables in a term *)
-let vars_of_global env constr =
- match kind constr with
- Var id -> Id.Set.singleton id
- | Const (kn, _) -> lookup_constant_variables kn env
- | Ind (ind, _) -> lookup_inductive_variables ind env
- | Construct (cstr, _) -> lookup_constructor_variables cstr env
- (** FIXME: is Proj missing? *)
- | _ -> raise Not_found
+let vars_of_global env gr =
+ let open GlobRef in
+ match gr with
+ | VarRef id -> Id.Set.singleton id
+ | ConstRef kn -> lookup_constant_variables kn env
+ | IndRef ind -> lookup_inductive_variables ind env
+ | ConstructRef cstr -> lookup_constructor_variables cstr env
let global_vars_set env constr =
let rec filtrec acc c =
- let acc =
- match kind c with
- | Var _ | Const _ | Ind _ | Construct _ ->
- Id.Set.union (vars_of_global env c) acc
- | _ ->
- acc in
- Constr.fold filtrec acc c
+ match destRef c with
+ | gr, _ ->
+ Id.Set.union (vars_of_global env gr) acc
+ | exception DestKO -> Constr.fold filtrec acc c
in
- filtrec Id.Set.empty constr
+ filtrec Id.Set.empty constr
(* [keep_hyps env ids] keeps the part of the section context of [env] which
@@ -680,6 +684,16 @@ let remove_hyps ids check_context check_value ctxt =
in
fst (remove_hyps ctxt)
+(* A general request *)
+
+let is_polymorphic env r =
+ let open Names.GlobRef in
+ match r with
+ | VarRef _id -> false
+ | ConstRef c -> polymorphic_constant c env
+ | IndRef ind -> polymorphic_ind ind env
+ | ConstructRef cstr -> polymorphic_ind (inductive_of_constructor cstr) env
+
(*spiwack: the following functions assemble the pieces of the retroknowledge
note that the "consistent" register function is available in the module
Safetyping, Environ only synchronizes the proactive and the reactive parts*)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 55ff7ff162..43bfe7c2fb 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -156,6 +156,9 @@ val fold_named_context :
(env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
val set_universes : env -> UGraph.t -> env
+(** This is used to update universes during a proof for the sake of
+ evar map-unaware functions, eg [Typing] calling
+ [Typeops.check_hyps_inclusion]. *)
(** Recurrence on [named_context] starting from younger decl *)
val fold_named_context_reverse :
@@ -267,6 +270,8 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env
val set_engagement : engagement -> env -> env
val set_typing_flags : typing_flags -> env -> env
+val universes_of_global : env -> GlobRef.t -> AUContext.t
+
(** {6 Sets of referred section variables }
[global_vars_set env c] returns the list of [id]'s occurring either
directly as [Var id] in [c] or indirectly as a section variable
@@ -274,8 +279,7 @@ val set_typing_flags : typing_flags -> env -> env
val global_vars_set : env -> constr -> Id.Set.t
-(** the constr must be a global reference *)
-val vars_of_global : env -> constr -> Id.Set.t
+val vars_of_global : env -> GlobRef.t -> Id.Set.t
(** closure of the input id set w.r.t. dependency *)
val really_needed : env -> Id.Set.t -> Id.Set.t
@@ -315,7 +319,7 @@ val apply_to_hyp : named_context_val -> variable ->
val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val
-
+val is_polymorphic : env -> Names.GlobRef.t -> bool
open Retroknowledge
(** functions manipulating the retroknowledge
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b976469ff7..0346026aa4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -271,7 +271,8 @@ let typecheck_inductive env mie =
| Polymorphic_ind_entry ctx -> push_context ctx env
| Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
in
- let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
+ let env_params = check_context env' mie.mind_entry_params in
+ let paramsctxt = mie.mind_entry_params in
(* We first type arity of each inductive definition *)
(* This allows building the environment of arities and to share *)
(* the set of constraints *)
diff --git a/kernel/names.ml b/kernel/names.ml
index 7cd749de1d..18560d5f8d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -872,6 +872,8 @@ struct
let equal (c, b) (c', b') = Repr.equal c c' && b == b'
+ let repr_equal p p' = Repr.equal (repr p) (repr p')
+
let hash (c, b) = (if b then 0 else 1) + Repr.hash c
module SyntacticOrd = struct
diff --git a/kernel/names.mli b/kernel/names.mli
index 37930c12e2..98995752a2 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -608,6 +608,9 @@ module Projection : sig
val hcons : t -> t
(** Hashconsing of projections. *)
+ val repr_equal : t -> t -> bool
+ (** Ignoring the unfolding boolean. *)
+
val compare : t -> t -> int
val map : (MutInd.t -> MutInd.t) -> t -> t
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 00576476ab..18697d07e5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -316,8 +316,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
type conv_tab = {
cnv_inf : clos_infos;
- lft_tab : fconstr infos_tab;
- rgt_tab : fconstr infos_tab;
+ lft_tab : clos_tab;
+ rgt_tab : clos_tab;
}
(** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
location contained both in tl and in tr. *)
@@ -346,7 +346,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| (Sort s1, Sort s2) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
- sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv
+ sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if Int.equal n m
then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 820c5b3a2b..12f9592ab7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -168,6 +168,12 @@ let is_initial senv =
let delta_of_senv senv = senv.modresolver,senv.paramresolver
+let constant_of_delta_kn_senv senv kn =
+ Mod_subst.constant_of_deltas_kn senv.paramresolver senv.modresolver kn
+
+let mind_of_delta_kn_senv senv kn =
+ Mod_subst.mind_of_deltas_kn senv.paramresolver senv.modresolver kn
+
(** The safe_environment state monad *)
type safe_transformer0 = safe_environment -> safe_environment
@@ -210,15 +216,55 @@ let get_opaque_body env cbo =
(Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
-type private_constants = Term_typing.side_effects
+type side_effect = {
+ from_env : Declarations.structure_body CEphemeron.key;
+ eff : Entries.side_eff list;
+}
-let empty_private_constants = Term_typing.empty_seff
-let add_private = Term_typing.add_seff
-let concat_private = Term_typing.concat_seff
-let mk_pure_proof = Term_typing.mk_pure_proof
-let inline_private_constants_in_constr = Term_typing.inline_side_effects
-let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
-let side_effects_of_private_constants = Term_typing.uniq_seff
+module SideEffects :
+sig
+ type t
+ val repr : t -> side_effect list
+ val empty : t
+ val add : side_effect -> t -> t
+ val concat : t -> t -> t
+end =
+struct
+
+module SeffOrd = struct
+open Entries
+type t = side_effect
+let compare e1 e2 =
+ let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in
+ List.compare cmp e1.eff e2.eff
+end
+
+module SeffSet = Set.Make(SeffOrd)
+
+type t = { seff : side_effect list; elts : SeffSet.t }
+(** Invariant: [seff] is a permutation of the elements of [elts] *)
+
+let repr eff = eff.seff
+let empty = { seff = []; elts = SeffSet.empty }
+let add x es =
+ if SeffSet.mem x es.elts then es
+ else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
+let concat xes yes =
+ List.fold_right add xes.seff yes
+
+end
+
+type private_constants = SideEffects.t
+
+let side_effects_of_private_constants l =
+ let ans = List.rev (SideEffects.repr l) in
+ List.map_append (fun { eff; _ } -> eff) ans
+
+let empty_private_constants = SideEffects.empty
+let add_private mb eff effs =
+ let from_env = CEphemeron.create mb in
+ SideEffects.add { eff; from_env } effs
+let concat_private = SideEffects.concat
let make_eff env cst r =
let open Entries in
@@ -251,7 +297,7 @@ let universes_of_private eff =
| Monomorphic_const ctx -> ctx :: acc
| Polymorphic_const _ -> acc
in
- List.fold_left fold [] (Term_typing.uniq_seff eff)
+ List.fold_left fold [] (side_effects_of_private_constants eff)
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
@@ -501,8 +547,218 @@ let add_constant_aux ~in_section senv (kn, cb) =
in
senv''
+let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty
+
+let inline_side_effects env body side_eff =
+ let open Entries in
+ let open Constr in
+ (** First step: remove the constants that are still in the environment *)
+ let filter { eff = se; from_env = mb } =
+ let map e = (e.seff_constant, e.seff_body, e.seff_env) in
+ let cbl = List.map map se in
+ let not_exists (c,_,_) =
+ try ignore(Environ.lookup_constant c env); false
+ with Not_found -> true in
+ let cbl = List.filter not_exists cbl in
+ (cbl, mb)
+ in
+ (* CAVEAT: we assure that most recent effects come first *)
+ let side_eff = List.map filter (SideEffects.repr side_eff) in
+ let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in
+ let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in
+ let side_eff = List.rev side_eff in
+ (** Most recent side-effects first in side_eff *)
+ if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs)
+ else
+ (** Second step: compute the lifts and substitutions to apply *)
+ let cname c = Name (Label.to_id (Constant.label c)) in
+ let fold (subst, var, ctx, args) (c, cb, b) =
+ let (b, opaque) = match cb.const_body, b with
+ | Def b, _ -> (Mod_subst.force_constr b, false)
+ | OpaqueDef _, `Opaque (b,_) -> (b, true)
+ | _ -> assert false
+ in
+ match cb.const_universes with
+ | Monomorphic_const univs ->
+ (** Abstract over the term at the top of the proof *)
+ let ty = cb.const_type in
+ let subst = Cmap_env.add c (Inr var) subst in
+ let ctx = Univ.ContextSet.union ctx univs in
+ (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
+ | Polymorphic_const _auctx ->
+ (** Inline the term to emulate universe polymorphism *)
+ let subst = Cmap_env.add c (Inl b) subst in
+ (subst, var, ctx, args)
+ in
+ let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, Univ.ContextSet.empty, []) side_eff in
+ (** Third step: inline the definitions *)
+ let rec subst_const i k t = match Constr.kind t with
+ | Const (c, u) ->
+ let data = try Some (Cmap_env.find c subst) with Not_found -> None in
+ begin match data with
+ | None -> t
+ | Some (Inl b) ->
+ (** [b] is closed but may refer to other constants *)
+ subst_const i k (Vars.subst_instance_constr u b)
+ | Some (Inr n) ->
+ mkRel (k + n - i)
+ end
+ | Rel n ->
+ (** Lift free rel variables *)
+ if n <= k then t
+ else mkRel (n + len - i - 1)
+ | _ -> Constr.map_with_binders ((+) 1) (fun k t -> subst_const i k t) k t
+ in
+ let map_args i (na, b, ty, opaque) =
+ (** Both the type and the body may mention other constants *)
+ let ty = subst_const (len - i - 1) 0 ty in
+ let b = subst_const (len - i - 1) 0 b in
+ (na, b, ty, opaque)
+ in
+ let args = List.mapi map_args args in
+ let body = subst_const 0 0 body in
+ let fold_arg (na, b, ty, opaque) accu =
+ if opaque then mkApp (mkLambda (na, ty, accu), [|b|])
+ else mkLetIn (na, b, ty, accu)
+ in
+ let body = List.fold_right fold_arg args body in
+ (body, ctx, sigs)
+
+let inline_private_constants_in_definition_entry env ce =
+ let open Entries in
+ { ce with
+ const_entry_body = Future.chain
+ ce.const_entry_body (fun ((body, ctx), side_eff) ->
+ let body, ctx',_ = inline_side_effects env body side_eff in
+ let ctx' = Univ.ContextSet.union ctx ctx' in
+ (body, ctx'), ());
+ }
+
+let inline_private_constants_in_constr env body side_eff =
+ pi1 (inline_side_effects env body side_eff)
+
+let rec is_nth_suffix n l suf =
+ if Int.equal n 0 then l == suf
+ else match l with
+ | [] -> false
+ | _ :: l -> is_nth_suffix (pred n) l suf
+
+(* Given the list of signatures of side effects, checks if they match.
+ * I.e. if they are ordered descendants of the current revstruct.
+ Returns the number of effects that can be trusted. *)
+let check_signatures curmb sl =
+ let is_direct_ancestor accu (mb, how_many) =
+ match accu with
+ | None -> None
+ | Some (n, curmb) ->
+ try
+ let mb = CEphemeron.get mb in
+ if is_nth_suffix how_many mb curmb
+ then Some (n + how_many, mb)
+ else None
+ with CEphemeron.InvalidKey -> None in
+ let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in
+ match sl with
+ | None -> 0
+ | Some (n, _) -> n
+
+
+let constant_entry_of_side_effect cb u =
+ let open Entries in
+ let univs =
+ match cb.const_universes with
+ | Monomorphic_const uctx ->
+ Monomorphic_const_entry uctx
+ | Polymorphic_const auctx ->
+ Polymorphic_const_entry (Univ.AUContext.repr auctx)
+ in
+ let pt =
+ match cb.const_body, u with
+ | OpaqueDef _, `Opaque (b, c) -> b, c
+ | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+ | _ -> assert false in
+ DefinitionEntry {
+ const_entry_body = Future.from_val (pt, ());
+ const_entry_secctx = None;
+ const_entry_feedback = None;
+ const_entry_type = Some cb.const_type;
+ const_entry_universes = univs;
+ const_entry_opaque = Declareops.is_opaque cb;
+ const_entry_inline_code = cb.const_inline_code }
+
+let turn_direct orig =
+ let open Entries in
+ let cb = orig.seff_body in
+ if Declareops.is_opaque cb then
+ let p = match orig.seff_env with
+ | `Opaque (b, c) -> (b, c)
+ | _ -> assert false
+ in
+ let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in
+ let cb = { cb with const_body } in
+ { orig with seff_body = cb }
+ else orig
+
+let export_eff eff =
+ let open Entries in
+ (eff.seff_constant, eff.seff_body, eff.seff_role)
+
+let export_side_effects mb env c =
+ let open Entries in
+ let body = c.const_entry_body in
+ let _, eff = Future.force body in
+ let ce = { c with
+ Entries.const_entry_body = Future.chain body
+ (fun (b_ctx, _) -> b_ctx, ()) } in
+ let not_exists e =
+ try ignore(Environ.lookup_constant e.seff_constant env); false
+ with Not_found -> true in
+ let aux (acc,sl) { eff = se; from_env = mb } =
+ let cbl = List.filter not_exists se in
+ if List.is_empty cbl then acc, sl
+ else cbl :: acc, (mb,List.length cbl) :: sl in
+ let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in
+ let trusted = check_signatures mb signatures in
+ let push_seff env eff =
+ let { seff_constant = kn; seff_body = cb ; _ } = eff in
+ let env = Environ.add_constant kn cb env in
+ match cb.const_universes with
+ | Polymorphic_const _ -> env
+ | Monomorphic_const ctx ->
+ let ctx = match eff.seff_env with
+ | `Nothing -> ctx
+ | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
+ in
+ Environ.push_context_set ~strict:true ctx env
+ in
+ let rec translate_seff sl seff acc env =
+ match seff with
+ | [] -> List.rev acc, ce
+ | cbs :: rest ->
+ if Int.equal sl 0 then
+ let env, cbs =
+ List.fold_left (fun (env,cbs) eff ->
+ let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
+ let ce = constant_entry_of_side_effect ocb u in
+ let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
+ let eff = { eff with
+ seff_body = cb;
+ seff_env = `Nothing;
+ } in
+ (push_seff env eff, export_eff eff :: cbs))
+ (env,[]) cbs in
+ translate_seff 0 rest (cbs @ acc) env
+ else
+ let cbs_len = List.length cbs in
+ let cbs = List.map turn_direct cbs in
+ let env = List.fold_left push_seff env cbs in
+ let ecbs = List.map export_eff cbs in
+ translate_seff (sl - cbs_len) rest (ecbs @ acc) env
+ in
+ translate_seff trusted seff [] env
+
let export_private_constants ~in_section ce senv =
- let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
+ let exported, ce = export_side_effects senv.revstruct senv.env ce in
let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -514,7 +770,12 @@ let add_constant ~in_section l decl senv =
let cb =
match decl with
| ConstantEntry (EffectEntry, ce) ->
- Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce
+ let handle env body eff =
+ let body, uctx, signatures = inline_side_effects env body eff in
+ let trusted = check_signatures senv.revstruct signatures in
+ body, uctx, trusted
+ in
+ Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce
| ConstantEntry (PureEntry, ce) ->
Term_typing.translate_constant Term_typing.Pure senv.env kn ce
| GlobalRecipe r ->
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 0f150ea971..26fa91adbd 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -204,6 +204,9 @@ val exists_objlabel : Label.t -> safe_environment -> bool
val delta_of_senv :
safe_environment -> Mod_subst.delta_resolver * Mod_subst.delta_resolver
+val constant_of_delta_kn_senv : safe_environment -> KerName.t -> Constant.t
+val mind_of_delta_kn_senv : safe_environment -> KerName.t -> MutInd.t
+
(** {6 Retroknowledge / Native compiler } *)
open Retroknowledge
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 5ccc23eefc..fb1b3e236c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -27,159 +27,12 @@ module NamedDecl = Context.Named.Declaration
(* Insertion of constants and parameters in environment. *)
-type side_effect = {
- from_env : Declarations.structure_body CEphemeron.key;
- eff : side_eff list;
-}
-
-module SideEffects :
-sig
- type t
- val repr : t -> side_effect list
- val empty : t
- val add : side_effect -> t -> t
- val concat : t -> t -> t
-end =
-struct
-
-module SeffOrd = struct
-type t = side_effect
-let compare e1 e2 =
- let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in
- List.compare cmp e1.eff e2.eff
-end
-
-module SeffSet = Set.Make(SeffOrd)
-
-type t = { seff : side_effect list; elts : SeffSet.t }
-(** Invariant: [seff] is a permutation of the elements of [elts] *)
-
-let repr eff = eff.seff
-let empty = { seff = []; elts = SeffSet.empty }
-let add x es =
- if SeffSet.mem x es.elts then es
- else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
-let concat xes yes =
- List.fold_right add xes.seff yes
-
-end
-
-type side_effects = SideEffects.t
+type 'a effect_handler =
+ env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
type _ trust =
| Pure : unit trust
-| SideEffects : structure_body -> side_effects trust
-
-let uniq_seff_rev = SideEffects.repr
-let uniq_seff l =
- let ans = List.rev (SideEffects.repr l) in
- List.map_append (fun { eff ; _ } -> eff) ans
-
-let empty_seff = SideEffects.empty
-let add_seff mb eff effs =
- let from_env = CEphemeron.create mb in
- SideEffects.add { eff; from_env } effs
-let concat_seff = SideEffects.concat
-
-let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
-
-let inline_side_effects env body ctx side_eff =
- (** First step: remove the constants that are still in the environment *)
- let filter { eff = se; from_env = mb } =
- let map e = (e.seff_constant, e.seff_body, e.seff_env) in
- let cbl = List.map map se in
- let not_exists (c,_,_) =
- try ignore(Environ.lookup_constant c env); false
- with Not_found -> true in
- let cbl = List.filter not_exists cbl in
- (cbl, mb)
- in
- (* CAVEAT: we assure that most recent effects come first *)
- let side_eff = List.map filter (uniq_seff_rev side_eff) in
- let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in
- let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in
- let side_eff = List.rev side_eff in
- (** Most recent side-effects first in side_eff *)
- if List.is_empty side_eff then (body, ctx, sigs)
- else
- (** Second step: compute the lifts and substitutions to apply *)
- let cname c = Name (Label.to_id (Constant.label c)) in
- let fold (subst, var, ctx, args) (c, cb, b) =
- let (b, opaque) = match cb.const_body, b with
- | Def b, _ -> (Mod_subst.force_constr b, false)
- | OpaqueDef _, `Opaque (b,_) -> (b, true)
- | _ -> assert false
- in
- match cb.const_universes with
- | Monomorphic_const univs ->
- (** Abstract over the term at the top of the proof *)
- let ty = cb.const_type in
- let subst = Cmap_env.add c (Inr var) subst in
- let ctx = Univ.ContextSet.union ctx univs in
- (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
- | Polymorphic_const _auctx ->
- (** Inline the term to emulate universe polymorphism *)
- let subst = Cmap_env.add c (Inl b) subst in
- (subst, var, ctx, args)
- in
- let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in
- (** Third step: inline the definitions *)
- let rec subst_const i k t = match Constr.kind t with
- | Const (c, u) ->
- let data = try Some (Cmap_env.find c subst) with Not_found -> None in
- begin match data with
- | None -> t
- | Some (Inl b) ->
- (** [b] is closed but may refer to other constants *)
- subst_const i k (Vars.subst_instance_constr u b)
- | Some (Inr n) ->
- mkRel (k + n - i)
- end
- | Rel n ->
- (** Lift free rel variables *)
- if n <= k then t
- else mkRel (n + len - i - 1)
- | _ -> Constr.map_with_binders ((+) 1) (fun k t -> subst_const i k t) k t
- in
- let map_args i (na, b, ty, opaque) =
- (** Both the type and the body may mention other constants *)
- let ty = subst_const (len - i - 1) 0 ty in
- let b = subst_const (len - i - 1) 0 b in
- (na, b, ty, opaque)
- in
- let args = List.mapi map_args args in
- let body = subst_const 0 0 body in
- let fold_arg (na, b, ty, opaque) accu =
- if opaque then mkApp (mkLambda (na, ty, accu), [|b|])
- else mkLetIn (na, b, ty, accu)
- in
- let body = List.fold_right fold_arg args body in
- (body, ctx, sigs)
-
-let rec is_nth_suffix n l suf =
- if Int.equal n 0 then l == suf
- else match l with
- | [] -> false
- | _ :: l -> is_nth_suffix (pred n) l suf
-
-(* Given the list of signatures of side effects, checks if they match.
- * I.e. if they are ordered descendants of the current revstruct.
- Returns the number of effects that can be trusted. *)
-let check_signatures curmb sl =
- let is_direct_ancestor accu (mb, how_many) =
- match accu with
- | None -> None
- | Some (n, curmb) ->
- try
- let mb = CEphemeron.get mb in
- if is_nth_suffix how_many mb curmb
- then Some (n + how_many, mb)
- else None
- with CEphemeron.InvalidKey -> None in
- let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in
- match sl with
- | None -> 0
- | Some (n, _) -> n
+| SideEffects : 'a effect_handler -> 'a trust
let skip_trusted_seff sl b e =
let rec aux sl b e acc =
@@ -259,9 +112,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let j = infer env body in
let _ = judge_of_cast env j DEFAULTcast tyj in
j, uctx
- | SideEffects mb ->
- let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in
- let valid_signatures = check_signatures mb signatures in
+ | SideEffects handle ->
+ let (body, uctx', valid_signatures) = handle env body side_eff in
+ let uctx = Univ.ContextSet.union uctx uctx' in
let env = push_context_set uctx env in
let body,env,ectx = skip_trusted_seff valid_signatures body env in
let j = infer env body in
@@ -286,9 +139,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
let (body, ctx), side_eff = Future.join body in
- let body, ctx, _ = match trust with
- | Pure -> body, ctx, []
- | SideEffects _ -> inline_side_effects env body ctx side_eff
+ let body, ctx = match trust with
+ | Pure -> body, ctx
+ | SideEffects handle ->
+ let body, ctx', _ = handle env body side_eff in
+ body, Univ.ContextSet.union ctx ctx'
in
let env, usubst, univs = match c.const_entry_universes with
| Monomorphic_const_entry univs ->
@@ -431,101 +286,6 @@ let translate_constant mb env kn ce =
build_constant_declaration kn env
(infer_declaration ~trust:mb env ce)
-let constant_entry_of_side_effect cb u =
- let univs =
- match cb.const_universes with
- | Monomorphic_const uctx ->
- Monomorphic_const_entry uctx
- | Polymorphic_const auctx ->
- Polymorphic_const_entry (Univ.AUContext.repr auctx)
- in
- let pt =
- match cb.const_body, u with
- | OpaqueDef _, `Opaque (b, c) -> b, c
- | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
- | _ -> assert false in
- DefinitionEntry {
- const_entry_body = Future.from_val (pt, ());
- const_entry_secctx = None;
- const_entry_feedback = None;
- const_entry_type = Some cb.const_type;
- const_entry_universes = univs;
- const_entry_opaque = Declareops.is_opaque cb;
- const_entry_inline_code = cb.const_inline_code }
-;;
-
-let turn_direct orig =
- let cb = orig.seff_body in
- if Declareops.is_opaque cb then
- let p = match orig.seff_env with
- | `Opaque (b, c) -> (b, c)
- | _ -> assert false
- in
- let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in
- let cb = { cb with const_body } in
- { orig with seff_body = cb }
- else orig
-
-type exported_side_effect =
- Constant.t * constant_body * side_effect_role
-
-let export_eff eff =
- (eff.seff_constant, eff.seff_body, eff.seff_role)
-
-let export_side_effects mb env c =
- let { const_entry_body = body; _ } = c in
- let _, eff = Future.force body in
- let ce = { c with
- const_entry_body = Future.chain body
- (fun (b_ctx, _) -> b_ctx, ()) } in
- let not_exists e =
- try ignore(Environ.lookup_constant e.seff_constant env); false
- with Not_found -> true in
- let aux (acc,sl) { eff = se; from_env = mb } =
- let cbl = List.filter not_exists se in
- if List.is_empty cbl then acc, sl
- else cbl :: acc, (mb,List.length cbl) :: sl in
- let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in
- let trusted = check_signatures mb signatures in
- let push_seff env eff =
- let { seff_constant = kn; seff_body = cb ; _ } = eff in
- let env = Environ.add_constant kn cb env in
- match cb.const_universes with
- | Polymorphic_const _ -> env
- | Monomorphic_const ctx ->
- let ctx = match eff.seff_env with
- | `Nothing -> ctx
- | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
- in
- Environ.push_context_set ~strict:true ctx env
- in
- let rec translate_seff sl seff acc env =
- match seff with
- | [] -> List.rev acc, ce
- | cbs :: rest ->
- if Int.equal sl 0 then
- let env, cbs =
- List.fold_left (fun (env,cbs) eff ->
- let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
- let ce = constant_entry_of_side_effect ocb u in
- let cb = translate_constant Pure env kn ce in
- let eff = { eff with
- seff_body = cb;
- seff_env = `Nothing;
- } in
- (push_seff env eff, export_eff eff :: cbs))
- (env,[]) cbs in
- translate_seff 0 rest (cbs @ acc) env
- else
- let cbs_len = List.length cbs in
- let cbs = List.map turn_direct cbs in
- let env = List.fold_left push_seff env cbs in
- let ecbs = List.map export_eff cbs in
- translate_seff (sl - cbs_len) rest (ecbs @ acc) env
- in
- translate_seff trusted seff [] env
-;;
-
let translate_local_assum env t =
let j = infer env t in
let t = Typeops.assumption_of_judgment env j in
@@ -578,13 +338,3 @@ let translate_local_def env _id centry =
(* Insertion of inductive types. *)
let translate_mind env kn mie = Indtypes.check_inductive env kn mie
-
-let inline_entry_side_effects env ce = { ce with
- const_entry_body = Future.chain
- ce.const_entry_body (fun ((body, ctx), side_eff) ->
- let body, ctx',_ = inline_side_effects env body ctx side_eff in
- (body, ctx'), ());
-}
-
-let inline_side_effects env body side_eff =
- pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index ab25090b00..faf434c142 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -14,53 +14,27 @@ open Environ
open Declarations
open Entries
-type side_effects
+(** Handlers are used to manage side-effects. The ['a] type stands for the type
+ of side-effects, and it is parametric because they are only defined later
+ on. Handlers inline the provided side-effects into the term, and return
+ the set of additional global constraints that need to be added for the term
+ to be well typed. *)
+type 'a effect_handler =
+ env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
type _ trust =
| Pure : unit trust
-| SideEffects : structure_body -> side_effects trust
+| SideEffects : 'a effect_handler -> 'a trust
val translate_local_def : env -> Id.t -> section_def_entry ->
constr * types
val translate_local_assum : env -> types -> types
-val mk_pure_proof : constr -> side_effects proof_output
-
-val inline_side_effects : env -> constr -> side_effects -> constr
-(** Returns the term where side effects have been turned into let-ins or beta
- redexes. *)
-
-val inline_entry_side_effects :
- env -> side_effects definition_entry -> unit definition_entry
-(** Same as {!inline_side_effects} but applied to entries. Only modifies the
- {!Entries.const_entry_body} field. It is meant to get a term out of a not
- yet type checked proof. *)
-
-val empty_seff : side_effects
-val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects
-val concat_seff : side_effects -> side_effects -> side_effects
-(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in
- [e1] must be more recent than those of [e2]. *)
-val uniq_seff : side_effects -> side_eff list
-(** Return the list of individual side-effects in the order of their
- creation. *)
-
val translate_constant :
'a trust -> env -> Constant.t -> 'a constant_entry ->
constant_body
-type exported_side_effect =
- Constant.t * constant_body * side_effect_role
-
-(* Given a constant entry containing side effects it exports them (either
- * by re-checking them or trusting them). Returns the constant bodies to
- * be pushed in the safe_env by safe typing. The main constant entry
- * needs to be translated as usual after this step. *)
-val export_side_effects :
- structure_body -> env -> side_effects definition_entry ->
- exported_side_effect list * unit definition_entry
-
val translate_mind :
env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7456ecea56..1bb2d3c79c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -319,6 +319,52 @@ let check_fixpoint env lna lar vdef vdeft =
with NotConvertibleVect i ->
error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar
+(* Global references *)
+
+let type_of_global_in_context env r =
+ let open Names.GlobRef in
+ match r with
+ | VarRef id -> Environ.named_type id env, Univ.AUContext.empty
+ | ConstRef c ->
+ let cb = Environ.lookup_constant c env in
+ let univs = Declareops.constant_polymorphic_context cb in
+ cb.Declarations.const_type, univs
+ | IndRef ind ->
+ let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+ let univs = Declareops.inductive_polymorphic_context mib in
+ let inst = Univ.make_abstract_instance univs in
+ let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
+ Inductive.type_of_inductive env (specif, inst), univs
+ | ConstructRef cstr ->
+ let (mib,_ as specif) =
+ Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+ in
+ let univs = Declareops.inductive_polymorphic_context mib in
+ let inst = Univ.make_abstract_instance univs in
+ Inductive.type_of_constructor (cstr,inst) specif, univs
+
+(* Build a fresh instance for a given context, its associated substitution and
+ the instantiated constraints. *)
+
+let constr_of_global_in_context env r =
+ let open GlobRef in
+ match r with
+ | VarRef id -> mkVar id, Univ.AUContext.empty
+ | ConstRef c ->
+ let cb = lookup_constant c env in
+ let univs = Declareops.constant_polymorphic_context cb in
+ mkConstU (c, Univ.make_abstract_instance univs), univs
+ | IndRef ind ->
+ let (mib,_) = Inductive.lookup_mind_specif env ind in
+ let univs = Declareops.inductive_polymorphic_context mib in
+ mkIndU (ind, Univ.make_abstract_instance univs), univs
+ | ConstructRef cstr ->
+ let (mib,_) =
+ Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+ in
+ let univs = Declareops.inductive_polymorphic_context mib in
+ mkConstructU (cstr, Univ.make_abstract_instance univs), univs
+
(************************************************************************)
(************************************************************************)
@@ -432,21 +478,8 @@ and execute_array env = Array.map (execute env)
(* Derived functions *)
-let universe_levels_of_constr _env c =
- let rec aux s c =
- match kind c with
- | Const (_c, u) ->
- LSet.fold LSet.add (Instance.levels u) s
- | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) ->
- LSet.fold LSet.add (Instance.levels u) s
- | Sort u when not (Sorts.is_small u) ->
- let u = Sorts.univ_of_sort u in
- LSet.fold LSet.add (Universe.levels u) s
- | _ -> Constr.fold aux s c
- in aux LSet.empty c
-
let check_wellformed_universes env c =
- let univs = universe_levels_of_constr env c in
+ let univs = universes_of_constr c in
try UGraph.check_declared_universes (universes env) univs
with UGraph.UndeclaredLevel u ->
error_undeclared_universe env u
@@ -482,25 +515,19 @@ let infer_v env cv =
(* Typing of several terms. *)
-let infer_local_decl env id = function
- | Entries.LocalDefEntry c ->
- let () = check_wellformed_universes env c in
- let t = execute env c in
- RelDecl.LocalDef (Name id, c, t)
- | Entries.LocalAssumEntry c ->
- let () = check_wellformed_universes env c in
- let t = execute env c in
- RelDecl.LocalAssum (Name id, check_assumption env c t)
-
-let infer_local_decls env decls =
- let rec inferec env = function
- | (id, d) :: l ->
- let (env, l) = inferec env l in
- let d = infer_local_decl env id d in
- (push_rel d env, Context.Rel.add d l)
- | [] -> (env, Context.Rel.empty)
- in
- inferec env decls
+let check_context env rels =
+ let open Context.Rel.Declaration in
+ Context.Rel.fold_outside (fun d env ->
+ match d with
+ | LocalAssum (_,ty) ->
+ let _ = infer_type env ty in
+ push_rel d env
+ | LocalDef (_,bd,ty) ->
+ let j1 = infer env bd in
+ let _ = infer_type env ty in
+ conv_leq false env j1.uj_type ty;
+ push_rel d env)
+ rels ~init:env
let judge_of_prop = make_judge mkProp type1
let judge_of_set = make_judge mkSet type1
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 57acdfe4b5..d24002065b 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -12,7 +12,6 @@ open Names
open Constr
open Univ
open Environ
-open Entries
(** {6 Typing functions (not yet tagged as safe) }
@@ -27,8 +26,8 @@ val infer : env -> constr -> unsafe_judgment
val infer_v : env -> constr array -> unsafe_judgment array
val infer_type : env -> types -> unsafe_type_judgment
-val infer_local_decls :
- env -> (Id.t * local_entry) list -> (env * Constr.rel_context)
+val check_context :
+ env -> Constr.rel_context -> env
(** {6 Basic operations of the typing machine. } *)
@@ -54,11 +53,10 @@ val type_of_variable : env -> variable -> types
val judge_of_variable : env -> variable -> unsafe_judgment
(** {6 type of a constant } *)
-
+val type_of_constant_in : env -> pconstant -> types
val judge_of_constant : env -> pconstant -> unsafe_judgment
(** {6 type of an applied projection } *)
-
val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment
(** {6 Type of application. } *)
@@ -89,9 +87,7 @@ val judge_of_cast :
unsafe_judgment
(** {6 Inductive types. } *)
-
val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment
-
val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
(** {6 Type of Cases. } *)
@@ -99,7 +95,25 @@ val judge_of_case : env -> case_info
-> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
-> unsafe_judgment
-val type_of_constant_in : env -> pconstant -> types
+(** {6 Type of global references. } *)
+
+val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
+(** Returns the type of the global reference, by creating a fresh
+ instance of polymorphic references and computing their
+ instantiated universe context. The type should not be used
+ without pushing it's universe context in the environmnent of
+ usage. For non-universe-polymorphic constants, it does not
+ matter. *)
+
+(** {6 Building a term from a global reference *)
+
+(** Map a global reference to a term in its local universe
+ context. The term should not be used without pushing it's universe
+ context in the environmnent of usage. For non-universe-polymorphic
+ constants, it does not matter. *)
+val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
+
+(** {6 Miscellaneous. } *)
(** Check that hyps are included in env and fails with error otherwise *)
val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fa37834a23..d09b54e7ec 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1065,6 +1065,9 @@ type universe_context_set = ContextSet.t
type 'a in_universe_context = 'a * universe_context
type 'a in_universe_context_set = 'a * universe_context_set
+let extend_in_context_set (a, ctx) ctx' =
+ (a, ContextSet.union ctx ctx')
+
(** Substitutions. *)
let empty_subst = LMap.empty
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1aa53b8aa8..7ac8247ca4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -433,6 +433,9 @@ end
type 'a in_universe_context = 'a * UContext.t
type 'a in_universe_context_set = 'a * ContextSet.t
+val extend_in_context_set : 'a in_universe_context_set -> ContextSet.t ->
+ 'a in_universe_context_set
+
val empty_level_subst : universe_level_subst
val is_empty_level_subst : universe_level_subst -> bool
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 9d5d79124b..7380a860dd 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -312,3 +312,17 @@ let subst_instance_constr subst c =
let subst_instance_context s ctx =
if Univ.Instance.is_empty s then ctx
else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
+
+let universes_of_constr c =
+ let open Univ in
+ let rec aux s c =
+ match kind c with
+ | Const (_c, u) ->
+ LSet.fold LSet.add (Instance.levels u) s
+ | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) ->
+ LSet.fold LSet.add (Instance.levels u) s
+ | Sort u when not (Sorts.is_small u) ->
+ let u = Sorts.univ_of_sort u in
+ LSet.fold LSet.add (Universe.levels u) s
+ | _ -> Constr.fold aux s c
+ in aux LSet.empty c
diff --git a/kernel/vars.mli b/kernel/vars.mli
index fdddbdb342..7c928e2694 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -139,3 +139,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context
(** Instance substitution for polymorphism. *)
val subst_instance_constr : Instance.t -> constr -> constr
val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context
+
+val universes_of_constr : constr -> Univ.LSet.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 13:26:32 +0000