diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 131 | ||||
| -rw-r--r-- | kernel/cClosure.mli | 46 | ||||
| -rw-r--r-- | kernel/constr.ml | 21 | ||||
| -rw-r--r-- | kernel/constr.mli | 4 | ||||
| -rw-r--r-- | kernel/reduction.ml | 6 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 277 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 272 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 42 |
8 files changed, 383 insertions, 416 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/constr.ml b/kernel/constr.ml index b490aa5092..d7f35da10d 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -452,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 c012f04260..8753c20eac 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -470,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/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 625b7e5073..12f9592ab7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -216,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 @@ -257,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 @@ -507,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 @@ -520,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/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 |