diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declareops.ml | 7 | ||||
| -rw-r--r-- | kernel/declareops.mli | 5 | ||||
| -rw-r--r-- | kernel/entries.ml | 17 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 67 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 17 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 119 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 10 |
7 files changed, 96 insertions, 146 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index b0d8410873..51ec3defb3 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -306,13 +306,6 @@ let hcons_mind mib = mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; mind_universes = hcons_mind_universes mib.mind_universes } -(** {6 Stm machinery } *) - -let string_of_side_effect { Entries.eff } = match eff with - | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")" - | Entries.SEscheme (cl,_) -> - "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")" - (** Hashconsing of modules *) let hcons_functorize hty he hself f = match f with diff --git a/kernel/declareops.mli b/kernel/declareops.mli index f91e69807f..35490ceef9 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -11,7 +11,6 @@ open Declarations open Mod_subst open Univ -open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -39,10 +38,6 @@ val constant_is_polymorphic : constant_body -> bool val is_opaque : constant_body -> bool -(** Side effects *) - -val string_of_side_effect : side_effect -> string - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool diff --git a/kernel/entries.ml b/kernel/entries.ml index 40873bea76..94248ad26b 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -120,11 +120,14 @@ type seff_env = Same as the constant_body's but not in an ephemeron *) | `Opaque of Constr.t * Univ.ContextSet.t ] -type side_eff = - | SEsubproof of Constant.t * Declarations.constant_body * seff_env - | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string - -type side_effect = { - from_env : Declarations.structure_body CEphemeron.key; - eff : side_eff; +(** Not used by the kernel. *) +type side_effect_role = + | Subproof + | Schema of inductive * string + +type side_eff = { + seff_constant : Constant.t; + seff_body : Declarations.constant_body; + seff_env : seff_env; + seff_role : side_effect_role; } diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f87ec9e023..6c87ff570f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -210,13 +210,8 @@ let get_opaque_body env cbo = (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) -type private_constant = Entries.side_effect type private_constants = Term_typing.side_effects -type private_constant_role = Term_typing.side_effect_role = - | Subproof - | Schema of inductive * string - let empty_private_constants = Term_typing.empty_seff let add_private = Term_typing.add_seff let concat_private = Term_typing.concat_seff @@ -225,44 +220,38 @@ 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 +let make_eff env cst r = + let open Entries in + let cbo = Environ.lookup_constant cst env.env in + { + seff_constant = cst; + seff_body = cbo; + seff_env = get_opaque_body env.env cbo; + seff_role = r; + } + let private_con_of_con env c = - let cbo = Environ.lookup_constant c env.env in - { Entries.from_env = CEphemeron.create env.revstruct; - Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } + let open Entries in + let eff = [make_eff env c Subproof] in + add_private env.revstruct eff empty_private_constants let private_con_of_scheme ~kind env cl = - { Entries.from_env = CEphemeron.create env.revstruct; - Entries.eff = Entries.SEscheme( - List.map (fun (i,c) -> - let cbo = Environ.lookup_constant c env.env in - i, c, cbo, get_opaque_body env.env cbo) cl, - kind) } + let open Entries in + let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in + add_private env.revstruct eff empty_private_constants let universes_of_private eff = - let open Declarations in - List.fold_left - (fun acc { Entries.eff } -> - match eff with - | Entries.SEscheme (l,s) -> - List.fold_left - (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc - in - match cb.const_universes with - | Monomorphic_const ctx -> - ctx :: acc - | Polymorphic_const _ -> acc - ) - acc l - | Entries.SEsubproof (c, cb, e) -> - match cb.const_universes with - | Monomorphic_const ctx -> - ctx :: acc - | Polymorphic_const _ -> acc - ) - [] (Term_typing.uniq_seff eff) + let open Entries in + let fold acc eff = + let acc = match eff.seff_env with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc + in + match eff.seff_body.const_universes with + | Monomorphic_const ctx -> ctx :: acc + | Polymorphic_const _ -> acc + in + List.fold_left fold [] (Term_typing.uniq_seff eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -489,7 +478,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - Constant.t * private_constant_role + Constant.t * Entries.side_effect_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index aca77ccd13..502e2970a1 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -41,29 +41,20 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) -type private_constant type private_constants -type private_constant_role = - | Subproof - | Schema of inductive * string - val side_effects_of_private_constants : - private_constants -> Entries.side_effect list + private_constants -> Entries.side_eff list (** Return the list of individual side-effects in the order of their creation. *) val empty_private_constants : private_constants -val add_private : private_constant -> private_constants -> private_constants -(** Add a constant to a list of private constants. The former must be more - recent than all constants appearing in the latter, i.e. one should not - create a dependency cycle. *) val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) -val private_con_of_con : safe_environment -> Constant.t -> private_constant -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constant +val private_con_of_con : safe_environment -> Constant.t -> private_constants +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : @@ -105,7 +96,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - Constant.t * private_constant_role + Constant.t * Entries.side_effect_role val export_private_constants : in_section:bool -> private_constants Entries.definition_entry -> diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 1f7ee145a2..43351737e5 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -27,16 +27,10 @@ module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) -let equal_eff e1 e2 = - let open Entries in - match e1, e2 with - | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } -> - Names.Constant.equal c1 c2 - | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } -> - CList.for_all2eq - (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2) - cl1 cl2 - | _ -> false +type side_effect = { + from_env : Declarations.structure_body CEphemeron.key; + eff : side_eff list; +} module SideEffects : sig @@ -48,17 +42,11 @@ sig end = struct -let compare_seff e1 e2 = match e1, e2 with -| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2 -| SEscheme (cl1, _), SEscheme (cl2, _) -> - let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in - CList.compare cmp cl1 cl2 -| SEsubproof _, SEscheme _ -> -1 -| SEscheme _, SEsubproof _ -> 1 - module SeffOrd = struct type t = side_effect -let compare e1 e2 = compare_seff e1.eff e2.eff +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) @@ -83,10 +71,14 @@ type _ trust = | SideEffects : structure_body -> side_effects trust let uniq_seff_rev = SideEffects.repr -let uniq_seff l = List.rev (SideEffects.repr l) +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 = SideEffects.add +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 @@ -94,11 +86,8 @@ 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 cbl = match se with - | SEsubproof (c, cb, b) -> [c, cb, b] - | SEscheme (cl,_) -> - List.map (fun (_, c, cb, b) -> c, cb, b) cl - in + 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 @@ -468,58 +457,50 @@ let constant_entry_of_side_effect cb u = const_entry_inline_code = cb.const_inline_code } ;; -let turn_direct (kn,cb,u,r as orig) = - match cb.const_body, u with - | OpaqueDef _, `Opaque (b,c) -> - let pt = Future.from_val (b,c) in - kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r - | _ -> orig -;; - -type side_effect_role = - | Subproof - | Schema of inductive * string +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 (c,_,_,_) = - try ignore(Environ.lookup_constant c env); false + 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 = match se with - | SEsubproof (c,cb,b) -> [c,cb,b,Subproof] - | SEscheme (cl,k) -> - List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in - let cbl = List.filter not_exists cbl in - if cbl = [] then acc, sl + 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 = function - | kn, cb, `Nothing, _ -> - begin - let env = Environ.add_constant kn cb env in - match cb.const_universes with - | Monomorphic_const ctx -> - Environ.push_context_set ~strict:true ctx env - | Polymorphic_const _ -> env - end - | kn, cb, `Opaque(_, ctx), _ -> - begin - let env = Environ.add_constant kn cb env in - match cb.const_universes with - | Monomorphic_const cstctx -> - let env = Environ.push_context_set ~strict:true cstctx env in - Environ.push_context_set ~strict:true ctx env - | Polymorphic_const _ -> env - end + 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 @@ -527,18 +508,22 @@ let export_side_effects mb env c = | cbs :: rest -> if Int.equal sl 0 then let env, cbs = - List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> + 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 - (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) + 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 (fun (kn,cb,u,r) -> - kn, cb, r) 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 diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 6a0ff072f5..b05e05e4dc 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -38,24 +38,18 @@ val inline_entry_side_effects : yet type checked proof. *) val empty_seff : side_effects -val add_seff : side_effect -> side_effects -> 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_effect list +val uniq_seff : side_effects -> side_eff list (** Return the list of individual side-effects in the order of their creation. *) -val equal_eff : side_effect -> side_effect -> bool - val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body -type side_effect_role = - | Subproof - | Schema of inductive * string - type exported_side_effect = Constant.t * constant_body * side_effect_role |