From: Ferruccio Guidi Date: Mon, 29 Jun 2009 17:46:08 +0000 (+0000) Subject: lambda-delta: X-Git-Tag: make_still_working~3770 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=75d417a2bb12a56052dd520c513c789fd9256252;p=helm.git lambda-delta: - lib/output: infrastructrure for reduction reporting we found just one instance of "referene typing" in the "Grundlagen" rt.txt reports where it occurs - lib/time: bugfix - basic_rg: bugfix (some relocations were missing) the "Grundlagen" now typechecks :) --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 90909683b..b68ea6dd8 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -13,6 +13,9 @@ lib/time.cmx: lib/log.cmx lib/hierarchy.cmi: lib/hierarchy.cmo: lib/cps.cmx lib/hierarchy.cmi lib/hierarchy.cmx: lib/cps.cmx lib/hierarchy.cmi +lib/output.cmi: +lib/output.cmo: lib/log.cmi lib/output.cmi +lib/output.cmx: lib/log.cmx lib/output.cmi automath/aut.cmo: automath/aut.cmx: automath/autOutput.cmi: automath/aut.cmx @@ -28,10 +31,10 @@ automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx basic_rg/brg.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx basic_rg/brg.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx -basic_rg/brgOutput.cmo: lib/nUri.cmi lib/log.cmi lib/hierarchy.cmi \ - lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi -basic_rg/brgOutput.cmx: lib/nUri.cmx lib/log.cmx lib/hierarchy.cmx \ - lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi +basic_rg/brgOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ + lib/hierarchy.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi +basic_rg/brgOutput.cmx: lib/output.cmx lib/nUri.cmx lib/log.cmx \ + lib/hierarchy.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx basic_rg/brgEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi @@ -40,22 +43,22 @@ basic_rg/brgEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_rg/brg.cmx \ 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: basic_rg/brgOutput.cmi basic_rg/brg.cmx -basic_rg/brgReduction.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx \ - basic_rg/brgSubstitution.cmi basic_rg/brgOutput.cmi \ +basic_rg/brgReduction.cmi: basic_rg/brg.cmx +basic_rg/brgReduction.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ + lib/cps.cmx basic_rg/brgSubstitution.cmi basic_rg/brgOutput.cmi \ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi -basic_rg/brgReduction.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \ - basic_rg/brgSubstitution.cmx basic_rg/brgOutput.cmx \ +basic_rg/brgReduction.cmx: lib/output.cmx lib/nUri.cmx lib/log.cmx \ + lib/cps.cmx basic_rg/brgSubstitution.cmx basic_rg/brgOutput.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi basic_rg/brgType.cmi: lib/hierarchy.cmi basic_rg/brg.cmx basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ - lib/hierarchy.cmi lib/cps.cmx basic_rg/brgReduction.cmi \ - basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \ - basic_rg/brgType.cmi + lib/hierarchy.cmi lib/cps.cmx basic_rg/brgSubstitution.cmi \ + basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \ + basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgType.cmi basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ - lib/hierarchy.cmx lib/cps.cmx basic_rg/brgReduction.cmx \ - basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ - basic_rg/brgType.cmi + lib/hierarchy.cmx lib/cps.cmx basic_rg/brgSubstitution.cmx \ + basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \ + basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgType.cmi basic_rg/brgUntrusted.cmi: lib/hierarchy.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi @@ -64,10 +67,10 @@ basic_rg/brgUntrusted.cmx: lib/log.cmx basic_rg/brgType.cmx \ basic_ag/bag.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx basic_ag/bag.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx -basic_ag/bagOutput.cmo: lib/nUri.cmi lib/log.cmi lib/hierarchy.cmi \ - lib/cps.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi -basic_ag/bagOutput.cmx: lib/nUri.cmx lib/log.cmx lib/hierarchy.cmx \ - lib/cps.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi +basic_ag/bagOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ + lib/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi +basic_ag/bagOutput.cmx: lib/output.cmx lib/nUri.cmx lib/log.cmx \ + lib/hierarchy.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi: lib/nUri.cmi basic_ag/bag.cmx basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_ag/bag.cmx \ basic_ag/bagEnvironment.cmi @@ -121,17 +124,17 @@ toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmi toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmi -toplevel/top.cmo: lib/time.cmx lib/nUri.cmi toplevel/metaOutput.cmi \ - toplevel/metaBrg.cmi toplevel/metaBag.cmi toplevel/metaAut.cmi \ - lib/log.cmi lib/hierarchy.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \ - basic_rg/brgType.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagReduction.cmi \ - basic_ag/bagOutput.cmi basic_ag/bag.cmx automath/autParser.cmi \ - automath/autOutput.cmi automath/autLexer.cmx -toplevel/top.cmx: lib/time.cmx lib/nUri.cmx toplevel/metaOutput.cmx \ - toplevel/metaBrg.cmx toplevel/metaBag.cmx toplevel/metaAut.cmx \ - lib/log.cmx lib/hierarchy.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ - basic_rg/brgType.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagReduction.cmx \ - basic_ag/bagOutput.cmx basic_ag/bag.cmx automath/autParser.cmx \ - automath/autOutput.cmx automath/autLexer.cmx +toplevel/top.cmo: lib/time.cmx lib/output.cmi lib/nUri.cmi \ + toplevel/metaOutput.cmi toplevel/metaBrg.cmi toplevel/metaBag.cmi \ + toplevel/metaAut.cmi lib/log.cmi lib/hierarchy.cmi lib/cps.cmx \ + basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi basic_rg/brgOutput.cmi \ + basic_rg/brg.cmx basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi \ + basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \ + automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx +toplevel/top.cmx: lib/time.cmx lib/output.cmx lib/nUri.cmx \ + toplevel/metaOutput.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \ + toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx lib/cps.cmx \ + basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx basic_rg/brgOutput.cmx \ + basic_rg/brg.cmx basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx \ + basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \ + automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 4982986a3..24807817e 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -18,7 +18,7 @@ test: $(MAIN).opt test-si: $(MAIN).opt @echo " HELENA -u $(INPUT-ORIG)" - $(H)./$(MAIN).opt -k bag -u -S 3 $(O) $(INPUT-ORIG) > log.txt + $(H)./$(MAIN).opt -u -S 3 $(O) $(INPUT-ORIG) > log.txt meta: $(MAIN).opt @echo " HELENA -m meta.txt $(INPUT)" diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index 3eb96a2d5..17bfe0659 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -12,9 +12,9 @@ module P = Printf module F = Format module U = NUri -module C = Cps module L = Log module H = Hierarchy +module O = Output module B = Bag type counters = { @@ -100,10 +100,8 @@ let print_counters f c = L.warn (P.sprintf " Total binder locations: %7u" locations); f () -let indexes = ref false - let res l id = - if !indexes then P.sprintf "#%u" l else id + if !O.indexes then P.sprintf "#%u" l else id let rec pp_term c frm = function | B.Sort h -> @@ -117,7 +115,7 @@ let rec pp_term c frm = function | Some (id, _) -> F.fprintf frm "@[%s@]" id | None -> F.fprintf frm "@[#%u@]" i in - if !indexes then f None else B.get f c i + if !O.indexes then f None else B.get f c i | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) | B.Cast (u, t) -> F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.mli b/helm/software/lambda-delta/basic_ag/bagOutput.mli index fe4d9f344..e176227d9 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.mli +++ b/helm/software/lambda-delta/basic_ag/bagOutput.mli @@ -18,5 +18,3 @@ val count_item: (counters -> 'a) -> counters -> Bag.item -> 'a val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Bag.context, Bag.term) Log.specs - -val indexes: bool ref diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index b8fc2d0c2..2d1fa96ae 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -12,9 +12,9 @@ module P = Printf module F = Format module U = NUri -module C = Cps module L = Log module H = Hierarchy +module O = Output module B = Brg (* nodes count **************************************************************) @@ -97,35 +97,11 @@ let print_counters f c = L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts); L.warn (P.sprintf " Application items: %7u" c.tappls); L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); - L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs); + L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs); f () -(* reductions count *********************************************************) - -type reductions = { - beta : int; - upsilon: int; - tau : int; - ldelta : int; - gdelta : int -} - -let initial_reductions = { - beta = 0; upsilon = 0; tau = 0; ldelta = 0; gdelta = 0 -} - -let add ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) r = { - beta = r.beta + beta; - upsilon = r.upsilon + upsilon; - tau = r.tau + tau; - ldelta = r.ldelta + ldelta; - gdelta = r.gdelta + gdelta -} - (* context/term pretty printing *********************************************) -let indexes = ref false - let id frm a = let f = function | None -> assert false @@ -146,7 +122,7 @@ let rec pp_term c frm = function | Some (a, _) -> F.fprintf frm "@[%a@]" id a | None -> F.fprintf frm "@[#%u@]" i in - if !indexes then f 0 None else B.get f c i + if !O.indexes then f 0 None else B.get f c i | B.GRef (_, s) -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) | B.Cast (_, u, t) -> F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index 6e578d80a..9fa180abd 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -18,13 +18,3 @@ val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Brg.context, Brg.term) Log.specs - -val indexes: bool ref - -type reductions - -val initial_reductions: reductions - -val add: - ?beta:int -> ?upsilon:int -> ?tau:int -> ?ldelta:int -> ?gdelta:int -> - reductions -> reductions diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 8ad752bad..87d093d82 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -12,6 +12,7 @@ module U = NUri module C = Cps module L = Log +module P = Output module B = Brg module O = BrgOutput module E = BrgEnvironment @@ -26,8 +27,6 @@ type machine = { (* Internal functions *******************************************************) -let reductions = ref O.initial_reductions - let level = 5 let error i = raise (LRefNotFound (L.items1 (string_of_int i))) @@ -67,17 +66,18 @@ let push f m a b = f {m with c = (a, b) :: m.c} (* to share *) -let rec step f ?(delta=false) ?(sty=false) c m x = +let rec step f ?(delta=false) ?(rt=false) c m x = (* L.warn "entering R.step"; *) match x with | B.Sort _ -> f m x | B.GRef (a, uri) -> let f = function | _, _, B.Abbr v when delta -> - reductions := O.add ~gdelta:1 !reductions; - step f ~delta ~sty c m v - | _, _, B.Abst w when sty -> - step f ~delta ~sty c m w + P.add ~gdelta:1 (); + step f ~delta ~rt c m v + | _, _, B.Abst w when rt -> + P.add ~grt:1 (); + step f ~delta ~rt c m w | e, _, b -> f m (B.GRef (B.Entry (e, b) :: a, uri)) in @@ -85,32 +85,34 @@ let rec step f ?(delta=false) ?(sty=false) c m x = | B.LRef (a, i) -> let f e = function | B.Abbr v -> - reductions := O.add ~ldelta:1 !reductions; - step f ~delta ~sty c m v - | B.Abst w when sty -> - step f ~delta ~sty c m w + P.add ~ldelta:1 (); + step f ~delta ~rt c m v + | B.Abst w when rt -> + P.add ~lrt:1 (); + step f ~delta ~rt c m w | b -> f m (B.LRef (B.Entry (e, b) :: a, i)) in let f e = S.lift_bind (f e) (succ i) (0) in get f c m i | B.Cast (_, _, t) -> - reductions := O.add ~tau:1 !reductions; - step f ~delta ~sty c m t + P.add ~tau:1 (); + step f ~delta ~rt c m t | B.Appl (_, v, t) -> - step f ~delta ~sty c {m with s = (v, 0) :: m.s} t + step f ~delta ~rt c {m with s = (v, 0) :: m.s} t | B.Bind (a, B.Abst w, t) -> begin match m.s with | [] -> f m x | (v, h) :: tl -> - reductions := O.add ~beta:1 !reductions; - let f mc = step f ~delta ~sty c {c = mc; s = tl} t in + P.add ~beta:1 ~upsilon:(List.length tl) (); + let f mc sc = step f ~delta ~rt c {c = mc; s = sc} t in + let f mc = lift_stack (f mc) tl in let f v = B.push f m.c a (B.Abbr (B.Cast ([], w, v))) in S.lift f h (0) v end | B.Bind (a, b, t) -> - reductions := O.add ~upsilon:(List.length m.s) !reductions; - let f sc mc = step f ~delta ~sty c {c = mc; s = sc} t in + P.add ~upsilon:(List.length m.s) (); + let f sc mc = step f ~delta ~rt c {c = mc; s = sc} t in let f sc = B.push (f sc) m.c a b in lift_stack f m.s @@ -124,7 +126,7 @@ let domain f c t = | x -> f None in L.box level; log1 "Now scanning" c t; - step f ~delta:true ~sty:true c empty_machine t + step f ~delta:true ~rt:true c empty_machine t let rec ac_nfs f ~si r c m1 u m2 t = (* L.warn "entering R.are_convertible_aux"; *) @@ -132,8 +134,9 @@ let rec ac_nfs f ~si r c m1 u m2 t = match u, t with | B.Sort (_, h1), B.Sort (_, h2) -> if h1 = h2 then f r else f false - | B.LRef (B.Entry (e1, B.Abst _) :: _, _), - B.LRef (B.Entry (e2, B.Abst _) :: _, _) -> + | B.LRef (B.Entry (e1, B.Abst _) :: _, i1), + B.LRef (B.Entry (e2, B.Abst _) :: _, i2) -> + P.add ~zeta:(i1+i2-e1-e2) (); if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false | B.GRef (B.Entry (e1, B.Abst _) :: _, _), B.GRef (B.Entry (e2, B.Abst _) :: _, _) -> @@ -144,23 +147,23 @@ let rec ac_nfs f ~si r c m1 u m2 t = let f r = if r then f r else begin - reductions := O.add ~gdelta:2 !reductions; + P.add ~gdelta:2 (); ac f ~si true c m1 v1 m2 v2 end in ac_stacks f ~si r c m1 m2 else if e1 < e2 then begin - reductions := O.add ~gdelta:1 !reductions; + P.add ~gdelta:1 (); step (ac_nfs f ~si r c m1 u) c m2 v2 end else begin - reductions := O.add ~gdelta:1 !reductions; + P.add ~gdelta:1 (); step (ac_nfs_rev f ~si r c m2 t) c m1 v1 end | _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) -> - reductions := O.add ~gdelta:1 !reductions; + P.add ~gdelta:1 (); step (ac_nfs f ~si r c m1 u) c m2 v2 | B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ -> - reductions := O.add ~gdelta:1 !reductions; + P.add ~gdelta:1 (); step (ac_nfs_rev f ~si r c m2 t) c m1 v1 | B.Bind (a1, (B.Abst w1 as b1), t1), B.Bind (a2, (B.Abst w2 as b2), t2) -> @@ -169,6 +172,7 @@ let rec ac_nfs f ~si r c m1 u m2 t = let f r = if r then push g m1 a1 b1 else f false in ac f ~si r c m1 w1 m2 w2 | B.Sort _, B.Bind (a, b, t) when si -> + P.add ~si:1 (); let f m1 m2 = ac f ~si r c m1 u m2 t in let f m1 = push (f m1) m2 a b in push f m1 a b diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index a384548b3..57e2bfb41 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -17,5 +17,3 @@ val domain: val are_convertible: (bool -> 'a) -> ?si:bool -> Brg.context -> Brg.term -> Brg.term -> 'a - -val reductions: BrgOutput.reductions ref diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index 8c9996c22..4bf5882a4 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -11,12 +11,13 @@ module U = NUri module C = Cps -module S = Share +module A = Share module L = Log module H = Hierarchy module B = Brg module O = BrgOutput module E = BrgEnvironment +module S = BrgSubstitution module R = BrgReduction exception TypeError of B.message @@ -51,8 +52,10 @@ let rec b_type_of f g c x = let f h = f x (B.Sort (a, h)) in H.apply f g h | B.LRef (_, i) -> let f _ = function - | Some (_, B.Abst w) -> f x w - | Some (_, B.Abbr (B.Cast (_, w, _))) -> f x w + | Some (_, B.Abst w) -> + S.lift (f x) (succ i) (0) w + | Some (_, B.Abbr (B.Cast (_, w, _))) -> + S.lift (f x) (succ i) (0) w | Some (_, B.Abbr _) -> assert false | Some (_, B.Void) -> error1 "reference to excluded variable" c x @@ -71,7 +74,7 @@ let rec b_type_of f g c x = E.get_obj f uri | B.Bind (a, B.Abbr v, t) -> let f xv xt tt = - f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) + f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) in let f xv cc = b_type_of (f xv) g cc t in let f xv = B.push (f xv) c a (B.Abbr xv) in @@ -82,14 +85,14 @@ let rec b_type_of f g c x = type_of f g c v | B.Bind (a, B.Abst u, t) -> let f xu xt tt = - f (S.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt) + f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt) in let f xu cc = b_type_of (f xu) g cc t in let f xu _ = B.push (f xu) c a (B.Abst xu) in type_of f g c u | B.Bind (a, B.Void, t) -> let f xt tt = - f (S.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt) + f (A.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt) in let f cc = b_type_of f g cc t in B.push f c a B.Void @@ -101,7 +104,7 @@ let rec b_type_of f g c x = L.unbox (succ level); let f r = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if r then f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) + if r then f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) else error3 c xv vv w in R.are_convertible f ~si:!si c w vv @@ -114,7 +117,7 @@ let rec b_type_of f g c x = | B.Cast (a, u, t) -> let f xu xt tt r = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if r then f (S.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu + if r then f (A.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu in let f xu xt tt = R.are_convertible ~si:!si (f xu xt tt) c xu tt in let f xu _ = b_type_of (f xu) g c t in diff --git a/helm/software/lambda-delta/lib/Make b/helm/software/lambda-delta/lib/Make index 4e21411d0..f0be78e29 100644 --- a/helm/software/lambda-delta/lib/Make +++ b/helm/software/lambda-delta/lib/Make @@ -1 +1 @@ -nUri cps share log time hierarchy +nUri cps share log time hierarchy output diff --git a/helm/software/lambda-delta/lib/output.ml b/helm/software/lambda-delta/lib/output.ml new file mode 100644 index 000000000..6dd526bfb --- /dev/null +++ b/helm/software/lambda-delta/lib/output.ml @@ -0,0 +1,72 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module P = Printf +module L = Log + +type reductions = { + beta : int; + zeta : int; + upsilon: int; + tau : int; + ldelta : int; + gdelta : int; + si : int; + lrt : int; + grt : int +} + +let initial_reductions = { + beta = 0; upsilon = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0; + si = 0; lrt = 0; grt = 0 +} + +let reductions = ref initial_reductions + +let clear_reductions () = reductions := initial_reductions + +let add + ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) + ?(si=0) ?(lrt=0) ?(grt=0) () += reductions := { + beta = !reductions.beta + beta; + zeta = !reductions.zeta + zeta; + upsilon = !reductions.upsilon + upsilon; + tau = !reductions.tau + tau; + ldelta = !reductions.ldelta + ldelta; + gdelta = !reductions.gdelta + gdelta; + si = !reductions.si + si; + lrt = !reductions.lrt + lrt; + grt = !reductions.grt + grt +} + +let print_reductions () = + let r = !reductions in + let rs = r.beta + r.ldelta + r.zeta + r.upsilon + r.tau + r.gdelta in + let prs = r.si + r.lrt + r.grt in + let delta = r.ldelta + r.gdelta in + let rt = r.lrt + r.grt in + L.warn (P.sprintf " Reductions summary"); + L.warn (P.sprintf " Proper reductions: %7u" rs); + L.warn (P.sprintf " Beta: %7u" r.beta); + L.warn (P.sprintf " Delta: %7u" delta); + L.warn (P.sprintf " Local: %7u" r.ldelta); + L.warn (P.sprintf " Global: %7u" r.gdelta); + L.warn (P.sprintf " Zeta: %7u" r.zeta); + L.warn (P.sprintf " Upsilon: %7u" r.upsilon); + L.warn (P.sprintf " Tau: %7u" r.tau); + L.warn (P.sprintf " Pseudo reductions: %7u" prs); + L.warn (P.sprintf " Reference typing: %7u" rt); + L.warn (P.sprintf " Local: %7u" r.lrt); + L.warn (P.sprintf " Global: %7u" r.grt); + L.warn (P.sprintf " Sort inclusion: %7u" r.si) + +let indexes = ref false diff --git a/helm/software/lambda-delta/lib/output.mli b/helm/software/lambda-delta/lib/output.mli new file mode 100644 index 000000000..812531585 --- /dev/null +++ b/helm/software/lambda-delta/lib/output.mli @@ -0,0 +1,21 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val indexes: bool ref + +val clear_reductions: unit -> unit + +val add: + ?beta:int -> ?upsilon:int -> ?tau:int -> ?ldelta:int -> ?gdelta:int -> + ?zeta:int -> ?si:int -> ?lrt:int -> ?grt:int -> + unit -> unit + +val print_reductions: unit -> unit diff --git a/helm/software/lambda-delta/lib/time.ml b/helm/software/lambda-delta/lib/time.ml index f139fdfbe..2eec540c9 100644 --- a/helm/software/lambda-delta/lib/time.ml +++ b/helm/software/lambda-delta/lib/time.ml @@ -24,7 +24,7 @@ let utime_stamp = let gmtime msg = let gmt = Unix.gmtime (Unix.time ()) in let yy = gmt.Unix.tm_year + 1900 in - let mm = gmt.Unix.tm_mon in + let mm = gmt.Unix.tm_mon + 1 in let dd = gmt.Unix.tm_mday in let h = gmt.Unix.tm_hour in let m = gmt.Unix.tm_min in diff --git a/helm/software/lambda-delta/rt.txt b/helm/software/lambda-delta/rt.txt new file mode 100644 index 000000000..a24b968e6 --- /dev/null +++ b/helm/software/lambda-delta/rt.txt @@ -0,0 +1,8 @@ +Type Error (line 366) +In the context +a : Prop +b : [x:a1].Prop +a1 : (a1).(b).$ld:/l/and +not a function +(a1).(b).(a).$ld:/l/ande2 + diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 6cbac04a4..842f02b2d 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -14,6 +14,7 @@ module U = NUri module C = Cps module L = Log module H = Hierarchy +module O = Output module AO = AutOutput module MA = MetaAut module MO = MetaOutput @@ -92,10 +93,6 @@ let type_check f st g = function in BagU.type_check f g item -let indexes () = match !kernel with - | Brg -> BrgO.indexes := true - | Bag -> BagO.indexes := true - let si () = match !kernel with | Brg -> BrgT.si := true | Bag -> BagR.nsi := true @@ -107,6 +104,7 @@ try let version_string = "Helena 0.8.0 M - June 2009" in let stage = ref 3 in let meta_file = ref None in + let progress = ref false in let set_hierarchy s = let f = function | Some g -> H.graph := g @@ -150,7 +148,8 @@ try let f st = function | None -> st | Some (i, u) -> - Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); + if !progress then + Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); st in (* stage 2 *) @@ -176,14 +175,16 @@ try in aux st tl in + O.clear_reductions (); let st = aux initial_status book in if !L.level > 0 then Time.utime_stamp "processed"; if !L.level > 2 then AO.print_counters C.start st.ac; if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc; - if !L.level > 2 && !stage > 1 then print_counters st + if !L.level > 2 && !stage > 1 then print_counters st; + if !L.level > 2 && !stage > 1 then O.print_reductions () in let help = - "Usage: helena [ -Viu | -Ss | -m | -hk ] ...\n\n" ^ + "Usage: helena [ -Vipu | -Ss | -m | -hk ] ...\n\n" ^ "Summary levels: 0 just errors, 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted\n" @@ -194,6 +195,7 @@ try let help_i = " show local references by index" in let help_k = " set kernel version" in let help_m = " output intermediate representation" in + let help_p = " activate progress indicator" in let help_u = " activate sort inclusion" in let help_s = " Set translation stage" in L.box 0; L.box_err (); @@ -202,9 +204,10 @@ try ("-S", Arg.Int set_summary, help_S); ("-V", Arg.Unit print_version, help_V); ("-h", Arg.String set_hierarchy, help_h); - ("-i", Arg.Unit indexes, help_i); + ("-i", Arg.Set O.indexes, help_i); ("-k", Arg.String set_kernel, help_k); ("-m", Arg.String set_meta_file, help_m); + ("-p", Arg.Set progress, help_p); ("-u", Arg.Unit si, help_u); ("-s", Arg.Int set_stage, help_s) ] read_file help;