aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-03-25 17:04:38 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-03-25 17:54:20 +0100
commit5047734648d83890eb4fc4e5cff7ab77d46b48eb (patch)
treefa283d97afb0023c72a0ff37deae54a5c42d0e0f
parent7c7ceb48c12cad0bcfd59e1e8ae944d7c6137cbe (diff)
More clever representation of substituted Cemitcode.
Module substitution is made nodewise, allowing to drop it for opaque terms in the VM. This saves a few useless substitutions.
-rw-r--r--kernel/cemitcodes.ml44
1 files changed, 30 insertions, 14 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 9ecae2b36..c5f88f6f5 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -333,25 +333,41 @@ let subst_patch s (ri,pos) =
let subst_to_patch s (code,pl,fv) =
code,List.rev_map (subst_patch s) pl,fv
+let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
+
type body_code =
| BCdefined of to_patch
| BCallias of pconstant
| BCconstant
-let subst_body_code s = function
- | BCdefined tp -> BCdefined (subst_to_patch s tp)
- | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u)
- | BCconstant -> BCconstant
-
-type to_patch_substituted = body_code substituted
-
-let from_val = from_val
-
-let force = force subst_body_code
-
-let subst_to_patch_subst = subst_substituted
-
-let repr_body_code = repr_substituted
+type to_patch_substituted =
+| PBCdefined of to_patch substituted
+| PBCallias of pconstant substituted
+| PBCconstant
+
+let from_val = function
+| BCdefined tp -> PBCdefined (from_val tp)
+| BCallias cu -> PBCallias (from_val cu)
+| BCconstant -> PBCconstant
+
+let force = function
+| PBCdefined tp -> BCdefined (force subst_to_patch tp)
+| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCconstant -> BCconstant
+
+let subst_to_patch_subst s = function
+| PBCdefined tp -> PBCdefined (subst_substituted s tp)
+| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCconstant -> PBCconstant
+
+let repr_body_code = function
+| PBCdefined tp ->
+ let (s, tp) = repr_substituted tp in
+ (s, BCdefined tp)
+| PBCallias cu ->
+ let (s, cu) = repr_substituted cu in
+ (s, BCallias cu)
+| PBCconstant -> (None, BCconstant)
let to_memory (init_code, fun_code, fv) =
init();