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
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
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
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
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
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)"
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 = {
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 ->
| 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
val print_counters: (unit -> 'a) -> counters -> 'a
val specs: (Bag.context, Bag.term) Log.specs
-
-val indexes: bool ref
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 **************************************************************)
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
| 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
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
module U = NUri
module C = Cps
module L = Log
+module P = Output
module B = Brg
module O = BrgOutput
module E = BrgEnvironment
(* Internal functions *******************************************************)
-let reductions = ref O.initial_reductions
-
let level = 5
let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
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
| 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
| 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"; *)
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 _) :: _, _) ->
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) ->
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
val are_convertible:
(bool -> 'a) -> ?si:bool -> Brg.context -> Brg.term -> Brg.term -> 'a
-
-val reductions: BrgOutput.reductions ref
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
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
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
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
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
| 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
-nUri cps share log time hierarchy
+nUri cps share log time hierarchy output
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
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
--- /dev/null
+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
+
module C = Cps
module L = Log
module H = Hierarchy
+module O = Output
module AO = AutOutput
module MA = MetaAut
module MO = MetaOutput
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
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
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 *)
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 <number> | -m <file> | -hk <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -Vipu | -Ss <number> | -m <file> | -hk <string> ] <file> ...\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"
let help_i = " show local references by index" in
let help_k = "<string> set kernel version" in
let help_m = "<file> output intermediate representation" in
+ let help_p = " activate progress indicator" in
let help_u = " activate sort inclusion" in
let help_s = "<number> Set translation stage" in
L.box 0; L.box_err ();
("-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;
projects / helm.git / commitdiff