Add a boolean to indicate the unfolding state of a primitive projection,

so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.

1 files changed, 27 insertions, 1 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index c76d95937f..5d73bd5209 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -782,7 +782,33 @@ let kn_ord = KerName.compare
 (** Compatibility layer for [Constant] *)
 
 type constant = Constant.t
-type projection = constant
+
+
+module Projection = 
+struct 
+  type t = constant * bool
+    
+  let make c b = (c, b)
+
+  let constant = fst
+  let unfolded = snd
+  let unfold (c, b as p) = if b then p else (c, true)
+  let equal (c, b) (c', b') = Constant.equal c c' && b == b'
+  let hash (c, b) = (if b then 0 else 1) + Constant.hash c
+  let hashcons (c, b as x) = 
+    let c' = hcons_con c in 
+      if c' == c then x else (c', b)
+
+  let compare (c, b) (c', b') =
+    if b == b' then Constant.CanOrd.compare c c'
+    else if b then 1 else -1
+
+  let map f (c, b as x) =
+    let c' = f c in
+      if c' == c then x else (c', b)
+end
+
+type projection = Projection.t
 
 let constant_of_kn = Constant.make1
 let constant_of_kn_equiv = Constant.make