diff options
author | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-07 16:56:17 +0000 |
---|---|---|
committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-07 16:56:17 +0000 |
commit | 02ae9a0b28366372c9eaad1c25428c65314e6fcb (patch) | |
tree | 3526dd0b974d94975edab48075eb6b8117ff2ecb /kernel/declarations.ml | |
parent | fb8c46171399af936caa3fbab8eff0cfc06ec94d (diff) |
Lazy manuelles dans le code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.ml')
-rw-r--r-- | kernel/declarations.ml | 28 |
1 files changed, 23 insertions, 5 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d3c7681c0..e6dd40c8a 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -21,9 +21,30 @@ open Sign (*s Constants (internal representation) (Definition/Axiom) *) +type subst_internal = + | Constr of constr + | LazyConstr of substitution * constr + +type constr_substituted = subst_internal ref + +let from_val c = ref (Constr c) + +let force cs = match !cs with + Constr c -> c + | LazyConstr (subst,c) -> + let c' = subst_mps subst c in + cs := Constr c'; + c' + +let subst_constr_subst subst cs = match !cs with + Constr c -> ref (LazyConstr (subst,c)) + | LazyConstr (subst',c) -> + let subst'' = join subst' subst in + ref (LazyConstr (subst'',c)) + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) - const_body : constr Lazy.t option; + const_body : constr_substituted option; const_type : types; const_constraints : constraints; const_opaque : bool } @@ -88,12 +109,9 @@ type mutual_inductive_body = { mind_equiv : kernel_name option } -let lazy_subst sub l_constr = - lazy (subst_mps sub (Lazy.force_val l_constr)) - (* TODO: should be changed to non-coping after Term.subst_mps *) let subst_const_body sub cb = - { const_body = option_app (lazy_subst sub) cb.const_body; + { const_body = option_app (subst_constr_subst sub) cb.const_body; const_type = type_app (Term.subst_mps sub) cb.const_type; const_hyps = (assert (cb.const_hyps=[]); []); const_constraints = cb.const_constraints; |