automath/autLexer.cmx: automath/autParser.cmx
basic_rg/brg.cmo: lib/nUri.cmi automath/aut.cmx
basic_rg/brg.cmx: lib/nUri.cmx automath/aut.cmx
+basic_rg/brgOutput.cmi: basic_rg/brg.cmx
+basic_rg/brgOutput.cmo: basic_rg/brg.cmx basic_rg/brgOutput.cmi
+basic_rg/brgOutput.cmx: basic_rg/brg.cmx basic_rg/brgOutput.cmi
toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx
toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx
toplevel/metaOutput.cmi: toplevel/meta.cmx
automath/aut.cmx toplevel/metaAut.cmi
toplevel/metaAut.cmx: lib/nUri.cmx toplevel/meta.cmx lib/cps.cmx \
automath/aut.cmx toplevel/metaAut.cmi
-toplevel/top.cmo: lib/time.cmx toplevel/metaOutput.cmi toplevel/metaAut.cmi \
- lib/cps.cmx automath/autParser.cmi automath/autOutput.cmi \
- automath/autLexer.cmx
-toplevel/top.cmx: lib/time.cmx toplevel/metaOutput.cmx toplevel/metaAut.cmx \
- lib/cps.cmx automath/autParser.cmx automath/autOutput.cmx \
- automath/autLexer.cmx
+toplevel/metaBrg.cmi: toplevel/meta.cmx basic_rg/brg.cmx
+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 toplevel/metaOutput.cmi toplevel/metaBrg.cmi \
+ toplevel/metaAut.cmi lib/cps.cmx basic_rg/brgOutput.cmi \
+ automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx
+toplevel/top.cmx: lib/time.cmx toplevel/metaOutput.cmx toplevel/metaBrg.cmx \
+ toplevel/metaAut.cmx lib/cps.cmx basic_rg/brgOutput.cmx \
+ automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx
-module U = NUri
-module A = Aut
+(*
+ ||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_______________________________________________________________ *)
-type uri = U.uri
-type id = A.id
+type uri = NUri.uri
+type id = Aut.id
-type binder = Abst | Abbr
+type bind = Abst | Abbr (* abstraction, abbreviation *)
-type term = Sort of int
- | LRef of int
- | GRef of uri
- | Cast of term * term
- | Appl of term * term
- | Bind of id * binder * term * term
-
+type term = Sort of int (* hierarchy index *)
+ | LRef of int (* reverse de Bruijn index *)
+ | GRef of uri (* reference *)
+ | Cast of term * term (* type, term *)
+ | Appl of term * term (* argument, function *)
+ | Bind of id * bind * term * term (* name, binder, content, scope *)
+
+type entry = uri * bind * term (* uri, binder, contents *)
+
+type item = entry option
--- /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 B = Brg
+
+type counters = {
+ eabsts: int;
+ eabbrs: int;
+ tsorts: int;
+ tlrefs: int;
+ tgrefs: int;
+ tcasts: int;
+ tappls: int;
+ tabsts: int;
+ tabbrs: int
+}
+
+let initial_counters = {
+ eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
+ tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
+}
+
+let count_term_binder f c = function
+ | B.Abst -> f {c with tabsts = succ c.tabsts}
+ | B.Abbr -> f {c with tabbrs = succ c.tabbrs}
+
+let rec count_term f c = function
+ | B.Sort _ ->
+ f {c with tsorts = succ c.tsorts}
+ | B.LRef _ ->
+ f {c with tlrefs = succ c.tlrefs}
+ | B.GRef _ ->
+ f {c with tgrefs = succ c.tgrefs}
+ | B.Cast (v, t) ->
+ let c = {c with tcasts = succ c.tcasts} in
+ let f c = count_term f c t in
+ count_term f c v
+ | B.Appl (v, t) ->
+ let c = {c with tappls = succ c.tappls} in
+ let f c = count_term f c t in
+ count_term f c v
+ | B.Bind (_, b, u, t) ->
+ let f c = count_term_binder f c b in
+ let f c = count_term f c t in
+ count_term f c u
+
+let count_entry_binder f c = function
+ | B.Abst -> f {c with eabsts = succ c.eabsts}
+ | B.Abbr -> f {c with eabbrs = succ c.eabbrs}
+
+let count_entry f c (_, b, t) =
+ let f c = count_entry_binder f c b in
+ count_term f c t
+
+let count_item f c = function
+ | Some e -> count_entry f c e
+ | None -> f c
+
+let print_counters f c =
+ let terms =
+ c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
+ c.tabbrs
+ in
+ let items = c.eabsts + c.eabbrs in
+ Printf.printf " Kernel representation summary (basic_rg)\n";
+ Printf.printf " Total entry items: %6u\n" items;
+ Printf.printf " Declaration items: %6u\n" c.eabsts;
+ Printf.printf " Definition items: %6u\n" c.eabbrs;
+ Printf.printf " Total term items: %6u\n" terms;
+ Printf.printf " Sort items: %6u\n" c.tsorts;
+ Printf.printf " Local reference items: %6u\n" c.tlrefs;
+ Printf.printf " Global reference items: %6u\n" c.tgrefs;
+ Printf.printf " Explicit Cast items: %6u\n" c.tcasts;
+ Printf.printf " Application items: %6u\n" c.tappls;
+ Printf.printf " Abstraction items: %6u\n" c.tabsts;
+ Printf.printf " Abbreviation items: %6u\n" c.tabbrs;
+ flush stdout; f ()
--- /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_______________________________________________________________ *)
+
+type counters
+
+val initial_counters: counters
+
+val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a
+
+val print_counters: (unit -> 'a) -> counters -> 'a
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-let id x = x
+(*
+ ||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_______________________________________________________________ *)
+
+let start x = x
+
+let id f x = f x
let rec list_sub_strict f l1 l2 = match l1, l2 with
| _, [] -> f l1
-meta metaOutput metaAut top
+meta metaOutput metaAut metaBrg top
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
+(*
+ ||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_______________________________________________________________ *)
type uri = NUri.uri
| LRef of int * int (* local reference: context length, de bruijn index *)
| GRef of int * uri * term list (* global reference: context length, name, arguments *)
| Appl of term * term (* application: argument, function *)
- | Abst of id * term * term (* abstraction: name, type, body *)
+ | Abst of id * term * term (* abstraction: name, type, scope *)
type pars = (id * term) list (* parameter declarations: name, type *)
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
+(*
+ ||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 H = Hashtbl
module U = NUri
--- /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 B = Brg
+module M = Meta
+
+(* Internal functions *******************************************************)
+
+let map_fold_left f map1 map2 a l =
+ let f a = Cps.list_fold_left f map2 a l in
+ map1 f a
+
+let map_args f t v = f (B.Appl (v, t))
+
+let map_pars f t (id, w) = f (B.Bind (id, B.Abst, w, t))
+
+let rec xlate_term f = function
+ | M.Sort s ->
+ let f h = f (B.Sort h) in
+ if s then f 0 else f 1
+ | M.LRef (l, i) ->
+ f (B.LRef (l - i))
+ | M.GRef (_, uri, vs) ->
+ let f vs = map_fold_left f Cps.id map_args (B.GRef uri) vs in
+ Cps.list_rev_map f xlate_term vs
+ | M.Appl (v, t) ->
+ let f v t = f (B.Appl (v, t)) in
+ let f v = xlate_term (f v) t in
+ xlate_term f v
+ | M.Abst (id, w, t) ->
+ let f w t = f (B.Bind (id, B.Abst, w, t)) in
+ let f w = xlate_term (f w) t in
+ xlate_term f w
+
+let xlate_pars f (id, w) =
+ let f w = f (id, w) in
+ xlate_term f w
+
+let xlate_entry f = function
+ | _, pars, uri, u, None ->
+ let f u = f (uri, B.Abst, u) in
+ let f pars = map_fold_left f xlate_term map_pars u pars in
+ Cps.list_rev_map f xlate_pars pars
+ | _, pars, uri, u, Some (_, t) ->
+ let f u t = f (uri, B.Abbr, (B.Cast (u, t))) in
+ let f pars u = map_fold_left (f u) xlate_term map_pars t pars in
+ let f pars = map_fold_left (f pars) xlate_term map_pars u pars in
+ Cps.list_rev_map f xlate_pars pars
+
+let xlate_item f = function
+ | None -> f None
+ | Some e -> let f e = f (Some e) in xlate_entry f e
+
+(* Interface functions ******************************************************)
+
+let brg_of_meta = xlate_item
--- /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 brg_of_meta: (Brg.item -> 'a) -> Meta.item -> 'a
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
+(*
+ ||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 F = Format
module U = NUri
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
+(*
+ ||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_______________________________________________________________ *)
type counters
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
+(*
+ ||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 AO = AutOutput
-module MA = MetaAut
-module MO = MetaOutput
+module AO = AutOutput
+module MA = MetaAut
+module MO = MetaOutput
+module MBrg = MetaBrg
+module BrgO = BrgOutput
+
+type status = {
+ summary: int;
+ mst : MA.status;
+ ac : AO.counters;
+ mc : MO.counters;
+ brgc: BrgO.counters
+}
+
+let initial_status summary = {
+ summary = summary;
+ ac = AO.initial_counters;
+ mc = MO.initial_counters;
+ brgc= BrgO.initial_counters;
+ mst = MA.initial_status
+}
+
+let count st count_fun c item =
+ if st.summary > 2 then count_fun Cps.start c item else c
let main =
- let version_string = "Helena Checker 0.8.0 M - November 2008" in
+ let version_string = "Helena Checker 0.8.0 M - December 2008" in
let summary = ref 0 in
- let stage = ref 1 in
+ let stage = ref 2 in
let meta_file = ref None in
let set_summary i = summary := i in
let print_version () = print_endline version_string; exit 0 in
let book = AutParser.book AutLexer.token lexbuf in
close_in ich;
if !summary > 0 then Time.utime_stamp "parsed";
- let rec aux ac mc st = function
- | [] -> ac, mc, st
- | item :: tl ->
- let ac = if !summary > 2 then AO.count_item Cps.id ac item else ac in
- let f st item =
- let mc = if !summary > 2 then MO.count_item Cps.id mc item else mc in
+ let rec aux st = function
+ | [] -> st
+ | item :: tl ->
+ let st = {st with ac = count st AO.count_item st.ac item} in
+ let f st item =
+ {st with brgc = count st BrgO.count_item st.brgc item}
+ in
+ let f mst item =
+ let st = {st with
+ mst = mst; mc = count st MO.count_item st.mc item
+ } in
begin match !meta_file with
| None -> ()
- | Some (_, frm) -> MO.pp_item Cps.id frm item
+ | Some (_, frm) -> MO.pp_item Cps.start frm item
end;
- st, mc
+ if !stage > 1 then MBrg.brg_of_meta (f st) item else st
+ in
+ let st =
+ if !stage > 0 then MA.meta_of_aut f st.mst item else st
in
- let st, mc = if !stage > 0 then MA.meta_of_aut f st item else st, mc in
- aux ac mc st tl
+ aux st tl
in
- let ac, mc, _st =
- aux AO.initial_counters MO.initial_counters MA.initial_status book
- in
+ let st = aux (initial_status !summary) book in
if !summary > 0 then Time.utime_stamp "processed";
- if !summary > 2 then AO.print_counters Cps.id ac;
- if !summary > 2 && !stage > 0 then MO.print_counters Cps.id mc;
+ if !summary > 2 then AO.print_counters Cps.start st.ac;
+ if !summary > 2 && !stage > 0 then MO.print_counters Cps.start st.mc;
+ if !summary > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc;
in
let help = "Usage: helena [ -V | -Ss <number> | -m <file> ] <file> ..." in
let help_S = "<number> Set summary level" in
projects / helm.git / commitdiff