diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.mli | 4 | ||||
| -rw-r--r-- | kernel/declareops.ml | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 6 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 3 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 37 |
5 files changed, 34 insertions, 20 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 6a5b0dbb20..d74c9a0d5e 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -59,7 +59,9 @@ type constant_body = { const_native_name : native_name ref; const_inline_code : bool } -type side_effect = NewConstant of constant * constant_body +type side_effect = + | SEsubproof of constant * constant_body + | SEscheme of (inductive * constant * constant_body) list * string (** {6 Representation of mutual inductive types in the kernel } *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 518a40a6e7..9f981f4828 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -254,7 +254,9 @@ let prune_constant_body cb = else {cb with const_constraints = cst'; const_body = cbo'} let string_of_side_effect = function - | NewConstant (c,_) -> Names.string_of_con c + | SEsubproof (c,_) -> Names.string_of_con c + | SEscheme (cl,_) -> + String.concat ", " (List.map (fun (_,c,_) -> Names.string_of_con c) cl) type side_effects = side_effect list let no_seff = ([] : side_effects) let iter_side_effects f l = List.iter f (List.rev l) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7a25cc5f80..3cde1538d7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -169,8 +169,10 @@ let check_engagement env c = (** {6 Stm machinery } *) -type side_effect = Declarations.side_effect -let sideff_of_con env c = NewConstant (c, Environ.lookup_constant c env.env) +let sideff_of_con env c = SEsubproof (c, Environ.lookup_constant c env.env) +let sideff_of_scheme kind env cl = + SEscheme( + List.map (fun (i,c) -> i, c, Environ.lookup_constant c env.env) cl,kind) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5d1c98de53..a56bb8578e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -34,6 +34,9 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) val sideff_of_con : safe_environment -> constant -> Declarations.side_effect +val sideff_of_scheme : + string -> safe_environment -> (inductive * constant) list -> + Declarations.side_effect val is_curmod_library : safe_environment -> bool diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c65ca8fc05..ef0270e9d6 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -47,27 +47,32 @@ let translate_local_assum env t = (* Insertion of constants and parameters in environment. *) let handle_side_effects env body side_eff = - let handle_sideff t (NewConstant (c,cb)) = - let cname = + let handle_sideff t se = + let cbl = match se with + | SEsubproof (c,cb) -> [c,cb] + | SEscheme (cl,_) -> List.map (fun (_,c,cb) -> c,cb) cl in + let cname c = let name = string_of_con c in for i = 0 to String.length name - 1 do if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done; Name (id_of_string name) in - let rec sub i x = match kind_of_term x with + let rec sub c i x = match kind_of_term x with | Const c' when eq_constant c c' -> mkRel i - | _ -> map_constr_with_binders ((+) 1) sub i x in - match cb.const_body with - | Undef _ -> assert false - | Def b -> - let b = Lazyconstr.force b in - let b_ty = Typeops.type_of_constant_type env cb.const_type in - let t = sub 1 (Vars.lift 1 t) in - mkLetIn (cname, b, b_ty, t) - | OpaqueDef b -> - let b = Lazyconstr.force_opaque (Future.force b) in - let b_ty = Typeops.type_of_constant_type env cb.const_type in - let t = sub 1 (Vars.lift 1 t) in - mkApp (mkLambda (cname, b_ty, t), [|b|]) + | _ -> map_constr_with_binders ((+) 1) (sub c) i x in + let fix_body (c,cb) t = + match cb.const_body with + | Undef _ -> assert false + | Def b -> + let b = Lazyconstr.force b in + let b_ty = Typeops.type_of_constant_type env cb.const_type in + let t = sub c 1 (Vars.lift 1 t) in + mkLetIn (cname c, b, b_ty, t) + | OpaqueDef b -> + let b = Lazyconstr.force_opaque (Future.force b) in + let b_ty = Typeops.type_of_constant_type env cb.const_type in + let t = sub c 1 (Vars.lift 1 t) in + mkApp (mkLambda (cname c, b_ty, t), [|b|]) in + List.fold_right fix_body cbl t in (* CAVEAT: we assure a proper order *) Declareops.fold_side_effects handle_sideff body |