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

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 740fce2ce1ec5eaeeee5a040d213d10cfad0dc36..ce9d23e2be970e710ae5f3a9e1387028f3086fb5 100644 (file)
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -1,9 +1,17 @@
+lib/nUri.cmi: 
 lib/nUri.cmo: lib/nUri.cmi 
 lib/nUri.cmx: lib/nUri.cmi 
+lib/cps.cmo: 
+lib/cps.cmx: 
+lib/share.cmo: 
+lib/share.cmx: 
+lib/log.cmi: 
 lib/log.cmo: lib/cps.cmx lib/log.cmi 
 lib/log.cmx: lib/cps.cmx lib/log.cmi 
 lib/time.cmo: lib/log.cmi 
 lib/time.cmx: lib/log.cmx 
+automath/aut.cmo: 
+automath/aut.cmx: 
 automath/autProcess.cmi: automath/aut.cmx 
 automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi 
 automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi 
@@ -17,8 +25,10 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi
 automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi 
 automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi 
 automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx 
+common/hierarchy.cmi: 
 common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi 
 common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi 
+common/output.cmi: 
 common/output.cmo: lib/log.cmi common/output.cmi 
 common/output.cmx: lib/log.cmx common/output.cmi 
 common/item.cmo: lib/nUri.cmi automath/aut.cmx 
@@ -42,12 +52,12 @@ basic_rg/brgSubstitution.cmi: basic_rg/brg.cmx
 basic_rg/brgSubstitution.cmo: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi 
 basic_rg/brgSubstitution.cmx: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi 
 basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx 
-basic_rg/brgReduction.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
-    lib/cps.cmx basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi \
-    basic_rg/brg.cmx basic_rg/brgReduction.cmi 
-basic_rg/brgReduction.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \
-    lib/cps.cmx basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx \
-    basic_rg/brg.cmx basic_rg/brgReduction.cmi 
+basic_rg/brgReduction.cmo: lib/share.cmx common/output.cmi lib/nUri.cmi \
+    lib/log.cmi lib/cps.cmx basic_rg/brgOutput.cmi \
+    basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi 
+basic_rg/brgReduction.cmx: lib/share.cmx common/output.cmx lib/nUri.cmx \
+    lib/log.cmx lib/cps.cmx basic_rg/brgOutput.cmx \
+    basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi 
 basic_rg/brgType.cmi: common/hierarchy.cmi basic_rg/brgReduction.cmi \
     basic_rg/brg.cmx 
 basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \

diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile
index ac4183f72000a4f2c88289d9f69d010fd668b6d0..dcdb7eeb37dc87c4c0f40d673f8307c74401fbb0 100644 (file)
--- a/helm/software/lambda-delta/Makefile
+++ b/helm/software/lambda-delta/Makefile
@@ -6,7 +6,7 @@ KEEP = README automath/*.aut
 
 CLEAN = log.txt
 
-TAGS = test test-si test-si-fast hir xml-si
+TAGS = test test-si test-si-fast hal xml-si
 
 include Makefile.common
 
@@ -26,7 +26,7 @@ test-si-fast: $(MAIN).opt
        @echo "  HELENA -u $(INPUT)"
        $(H)./$(MAIN).opt -u -S 1 $(O) $(INPUT) > log.txt
 
-hir: $(MAIN).opt
+hal: $(MAIN).opt
        @echo "  HELENA -m $(INPUT)"
        $(H)./$(MAIN).opt -m -s 1 -S 1 $(INPUT) > log.txt
 

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
 

diff --git a/helm/software/lambda-delta/lib/share.ml b/helm/software/lambda-delta/lib/share.ml
index c8097d568eac398c663e5ac5a11d7be212bd4cda..600ae9d858a2e4b406fbb50be6445e418e184494 100644 (file)
--- a/helm/software/lambda-delta/lib/share.ml
+++ b/helm/software/lambda-delta/lib/share.ml
@@ -17,3 +17,5 @@ let sh1 a1 a2 b1 b2 =
 
 let sh2 a1 a2 b1 b2 c1 c2 =
    if a1 == a2 && b1 == b2 then c1 else c2 (sh a1 a2) (sh b1 b2)
+
+let eq a b = (a == b) || (a = b)

diff --git a/helm/software/lambda-delta/performance.txt b/helm/software/lambda-delta/performance.txt
index 5d674bd66962679e9d31196a72400e02399fcf01..01009680e6f7d8d4da352ed123e9e4c32f3b518d 100644 (file)
--- a/helm/software/lambda-delta/performance.txt
+++ b/helm/software/lambda-delta/performance.txt
@@ -4,3 +4,7 @@ untrusted   : 0.4
 trusted     : 6.5  + 3 with upsilon relocations 
 ------------------
 total       : 9.2
+
+ 107123  alpha conversions  (107021 without si)
+ 298902  proper conversions
+