+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
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
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 \
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
@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
module U = NUri
module C = Cps
+module S = Share
module L = Log
module P = Output
module B = Brg
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
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
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)
trusted : 6.5 + 3 with upsilon relocations
------------------
total : 9.2
+
+ 107123 alpha conversions (107021 without si)
+ 298902 proper conversions
+