- alpha conversion check added to the brg kernel (succeeds 1/4 of the times)

[helm.git] / helm / software / lambda-delta / basic_rg / brgReduction.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 8ac7021f9baeee76ca2009bd3bc5267df9694b82..b57cb552b909452740884682804811a5d14ecd27 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -11,6 +11,7 @@
 
 module U = NUri
 module C = Cps
+module S = Share
 module L = Log
 module P = Output
 module B = Brg
@@ -51,6 +52,28 @@ let error3 c t1 t2 t3 =
    in
    raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
 
+let are_alpha_convertible f t1 t2 =
+   let rec aux f = function
+      | B.Sort (_, p1), B.Sort (_, p2)
+      | B.LRef (_, p1), B.LRef (_, p2)         -> f (p1 = p2)
+      | B.GRef (_, u1), B.GRef (_, u2)         -> f (U.eq u1 u2) 
+      | B.Cast (_, v1, t1), B.Cast (_, v2, t2)         
+      | B.Appl (_, v1, t1), B.Appl (_, v2, t2) ->
+         let f r = if r then aux f (t1, t2) else f r in
+        aux f (v1, v2)
+      | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
+         let f r = if r then aux f (t1, t2) else f r in
+        aux_bind f (b1, b2)
+      | B.Sort _ as t1, B.Bind (_, _, t2)      -> aux f (t1, t2)
+      | _                                      -> f false
+   and aux_bind f = function
+      | B.Abbr v1, B.Abbr v2
+      | B.Abst v1, B.Abst v2                   -> aux f (v1, v2)
+      | B.Void, B.Void                         -> f true
+      | _                                      -> f false
+   in
+   if S.eq t1 t2 then f true else aux f (t1, t2)
+
 let get f m i =
    B.get error0 f m.c i
 
@@ -194,14 +217,13 @@ let get f m i =
    get f m i
 
 let assert_conversion f ?(si=false) ?(rt=false) mw u w v = 
-   let f b = L.unbox level; f b in
    let f mu u =
-      let f = function
-         | true  -> f ()
-         | false -> error3 mw.c v w u
-      in
       L.box level; log2 "Now converting" mu.c u mw.c w;
-      ac f ~si true mu u mw w
+      let f r = 
+         if r then begin L.unbox level; f () end else error3 mw.c v w u
+      in
+      let g r = if r then f r else ac f ~si true mu u mw w in
+      if S.eq mu mw then are_alpha_convertible g u w else g false
    in
    if rt then domain f mw u else f mw u