Move to a representation of universe polymorphic constants using indices for variables.

Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.

1 files changed, 41 insertions, 0 deletions

diff --git a/kernel/vars.ml b/kernel/vars.ml
index 386a3e8ff..ee156d8c9 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -295,3 +295,44 @@ let subst_univs_level_constr subst c =
 
 let subst_univs_level_context s = 
   map_rel_context (subst_univs_level_constr s)
+      
+let subst_instance_constr subst c =
+  if Univ.Instance.is_empty subst then c
+  else
+    let f u = Univ.subst_instance_instance subst u in
+    let changed = ref false in
+    let rec aux t = 
+      match kind t with
+      | Const (c, u) -> 
+	if Univ.Instance.is_empty u then t
+	else 
+          let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; mkConstU (c, u'))
+      | Ind (i, u) ->
+	if Univ.Instance.is_empty u then t
+	else 
+	  let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; mkIndU (i, u'))
+      | Construct (c, u) ->
+	if Univ.Instance.is_empty u then t
+	else 
+          let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; mkConstructU (c, u'))
+      | Sort (Sorts.Type u) -> 
+         let u' = Univ.subst_instance_universe subst u in
+	   if u' == u then t else 
+	     (changed := true; mkSort (Sorts.sort_of_univ u'))
+      | _ -> Constr.map aux t
+    in
+    let c' = aux c in
+      if !changed then c' else c
+
+(* let substkey = Profile.declare_profile "subst_instance_constr";; *)
+(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *)
+
+let subst_instance_context s ctx = 
+  if Univ.Instance.is_empty s then ctx
+  else map_rel_context (fun x -> subst_instance_constr s x) ctx