From: Ferruccio Guidi Date: Mon, 17 Aug 2009 17:40:02 +0000 (+0000) Subject: - alpha conversion check added to the brg kernel (succeeds 1/4 of the times) X-Git-Tag: make_still_working~3537 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=828a190748fe67669df59d8813d32e17a3bbfd7a;p=helm.git - 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 740fce2ce..ce9d23e2b 100644 --- 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 ac4183f72..dcdb7eeb3 100644 --- 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 8ac7021f9..b57cb552b 100644 --- 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 c8097d568..600ae9d85 100644 --- 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 5d674bd66..01009680e 100644 --- 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 +