From: Ferruccio Guidi Date: Mon, 30 Jun 2008 14:07:46 +0000 (+0000) Subject: we tranlate an Automath book in an itermediate format where: X-Git-Tag: make_still_working~4982 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b00b8de85c5ae6c5fbb6f47dc559bf4cfcf2a5b6;p=helm.git we tranlate an Automath book in an itermediate format where: - the local references are resolved as position indexes - the global references are disambiguated - the parameter applications are completed For now the trnslation is slow because the involved data structures are inefficient --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index a0d42bdd9..144dab5e6 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,6 +1,6 @@ -automath/autHelpers.cmi: automath/aut.cmx -automath/autHelpers.cmo: cps/cps.cmx automath/aut.cmx automath/autHelpers.cmi -automath/autHelpers.cmx: cps/cps.cmx automath/aut.cmx automath/autHelpers.cmi +automath/autOutput.cmi: automath/aut.cmx +automath/autOutput.cmo: cps/cps.cmx automath/aut.cmx automath/autOutput.cmi +automath/autOutput.cmx: cps/cps.cmx automath/aut.cmx automath/autOutput.cmi automath/autParser.cmi: automath/aut.cmx automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi @@ -8,12 +8,17 @@ automath/autLexer.cmo: automath/autParser.cmi automath/autLexer.cmx: automath/autParser.cmx toplevel/meta.cmo: automath/aut.cmx toplevel/meta.cmx: automath/aut.cmx +toplevel/metaOutput.cmi: toplevel/meta.cmx +toplevel/metaOutput.cmo: toplevel/meta.cmx cps/cps.cmx \ + toplevel/metaOutput.cmi +toplevel/metaOutput.cmx: toplevel/meta.cmx cps/cps.cmx \ + toplevel/metaOutput.cmi toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx toplevel/metaAut.cmo: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx \ toplevel/metaAut.cmi toplevel/metaAut.cmx: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx \ toplevel/metaAut.cmi -toplevel/top.cmo: cps/cps.cmx automath/autParser.cmi automath/autLexer.cmx \ - automath/autHelpers.cmi -toplevel/top.cmx: cps/cps.cmx automath/autParser.cmx automath/autLexer.cmx \ - automath/autHelpers.cmx +toplevel/top.cmo: toplevel/metaOutput.cmi toplevel/metaAut.cmi cps/cps.cmx \ + automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx +toplevel/top.cmx: toplevel/metaOutput.cmx toplevel/metaAut.cmx cps/cps.cmx \ + automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx diff --git a/helm/software/lambda-delta/automath/Make b/helm/software/lambda-delta/automath/Make index 5a619153d..9a773e0fc 100644 --- a/helm/software/lambda-delta/automath/Make +++ b/helm/software/lambda-delta/automath/Make @@ -1 +1 @@ -aut autHelpers autParser autLexer +aut autOutput autParser autLexer diff --git a/helm/software/lambda-delta/automath/autHelpers.ml b/helm/software/lambda-delta/automath/autHelpers.ml deleted file mode 100644 index 769902529..000000000 --- a/helm/software/lambda-delta/automath/autHelpers.ml +++ /dev/null @@ -1,94 +0,0 @@ -(* 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/. - *) - -module A = Aut - -type counters = { - sections: int; - contexts: int; - blocks: int; - decls: int; - defs: int; - sorts: int; - grefs: int; - appls: int; - absts: int -} - -let initial_counters = { - sections = 0; contexts = 0; blocks = 0; decls = 0; defs = 0; - sorts = 0; grefs = 0; appls = 0; absts = 0 -} - -let rec count_term f c = function - | A.Sort _ -> - f {c with sorts = succ c.sorts} - | A.GRef (_, ts) -> - let c = {c with grefs = succ c.grefs} in - Cps.list_fold_left f count_term c ts - | A.Appl (v, t) -> - let c = {c with appls = succ c.appls} in - let f c = count_term f c t in - count_term f c v - | A.Abst (_, w, t) -> - let c = {c with absts = succ c.absts} in - let f c = count_term f c t in - count_term f c w - -let count_item f c = function - | A.Section _ -> - f {c with sections = succ c.sections} - | A.Context _ -> - f {c with contexts = succ c.contexts} - | A.Block (_, w) -> - let c = {c with blocks = succ c.blocks} in - count_term f c w - | A.Decl (_, w) -> - let c = {c with decls = succ c.decls} in - count_term f c w - | A.Def (_, w, _, t) -> - let c = {c with defs = succ c.defs} in - let f c = count_term f c t in - count_term f c w - -let count f c b = - Cps.list_fold_left f count_item c b - -let print_counters f c = - let terms = c.sorts + c.grefs + c.appls + c.absts in - let items = c.sections + c.contexts + c.blocks + c.decls + c.defs in - Printf.printf " Automath representation summary\n"; - Printf.printf " Total book items: %6u\n" items; - Printf.printf " Section items: %6u\n" c.sections; - Printf.printf " Context items: %6u\n" c.contexts; - Printf.printf " Block items: %6u\n" c.blocks; - Printf.printf " Declaration items: %6u\n" c.decls; - Printf.printf " Definition items: %6u\n" c.defs; - Printf.printf " Total term items: %6u\n" terms; - Printf.printf " Sort items: %6u\n" c.sorts; - Printf.printf " Reference items: %6u\n" c.grefs; - Printf.printf " Application items: %6u\n" c.appls; - Printf.printf " Abstraction items: %6u\n" c.absts; - flush stdout; f () diff --git a/helm/software/lambda-delta/automath/autHelpers.mli b/helm/software/lambda-delta/automath/autHelpers.mli deleted file mode 100644 index 6ff94387b..000000000 --- a/helm/software/lambda-delta/automath/autHelpers.mli +++ /dev/null @@ -1,32 +0,0 @@ -(* 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/. - *) - -type counters - -val initial_counters: counters - -val count: (counters -> 'a) -> counters -> Aut.book -> 'a - -val print_counters: (unit -> 'a) -> counters -> 'a diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml new file mode 100644 index 000000000..1acb075b2 --- /dev/null +++ b/helm/software/lambda-delta/automath/autOutput.ml @@ -0,0 +1,98 @@ +(* 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/. + *) + +module A = Aut + +type counters = { + sections: int; + contexts: int; + blocks: int; + decls: int; + defs: int; + sorts: int; + grefs: int; + appls: int; + absts: int; + pars: int +} + +let initial_counters = { + sections = 0; contexts = 0; blocks = 0; decls = 0; defs = 0; + sorts = 0; grefs = 0; appls = 0; absts = 0; pars = 0 +} + +let rec count_term f c = function + | A.Sort _ -> + f {c with sorts = succ c.sorts} + | A.GRef (_, ts) -> + let c = {c with grefs = succ c.grefs} in + let c = {c with pars = c.pars + List.length ts} in + Cps.list_fold_left f count_term c ts + | A.Appl (v, t) -> + let c = {c with appls = succ c.appls} in + let f c = count_term f c t in + count_term f c v + | A.Abst (_, w, t) -> + let c = {c with absts = succ c.absts} in + let f c = count_term f c t in + count_term f c w + +let count_item f c = function + | A.Section _ -> + f {c with sections = succ c.sections} + | A.Context _ -> + f {c with contexts = succ c.contexts} + | A.Block (_, w) -> + let c = {c with blocks = succ c.blocks} in + count_term f c w + | A.Decl (_, w) -> + let c = {c with decls = succ c.decls} in + count_term f c w + | A.Def (_, w, _, t) -> + let c = {c with defs = succ c.defs} in + let f c = count_term f c t in + count_term f c w + +let count f c b = + Cps.list_fold_left f count_item c b + +let print_counters f c = + let terms = c.sorts + c.grefs + c.appls + c.absts in + let items = c.sections + c.contexts + c.blocks + c.decls + c.defs in + Printf.printf " Automath representation summary\n"; + Printf.printf " Total book items: %6u\n" items; + Printf.printf " Section items: %6u\n" c.sections; + Printf.printf " Context items: %6u\n" c.contexts; + Printf.printf " Block items: %6u\n" c.blocks; + Printf.printf " Declaration items: %6u\n" c.decls; + Printf.printf " Definition items: %6u\n" c.defs; + Printf.printf " Total Parameter items: %6u\n" c.pars; + Printf.printf " Application items: %6u\n" c.pars; + Printf.printf " Total term items: %6u\n" terms; + Printf.printf " Sort items: %6u\n" c.sorts; + Printf.printf " Reference items: %6u\n" c.grefs; + Printf.printf " Application items: %6u\n" c.appls; + Printf.printf " Abstraction items: %6u\n" c.absts; + flush stdout; f () diff --git a/helm/software/lambda-delta/automath/autOutput.mli b/helm/software/lambda-delta/automath/autOutput.mli new file mode 100644 index 000000000..6ff94387b --- /dev/null +++ b/helm/software/lambda-delta/automath/autOutput.mli @@ -0,0 +1,32 @@ +(* 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/. + *) + +type counters + +val initial_counters: counters + +val count: (counters -> 'a) -> counters -> Aut.book -> 'a + +val print_counters: (unit -> 'a) -> counters -> 'a diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly index 912770560..2f7c06349 100644 --- a/helm/software/lambda-delta/automath/autParser.mly +++ b/helm/software/lambda-delta/automath/autParser.mly @@ -54,8 +54,8 @@ | IDENT path idents { $1 :: $3 } ; qid: - | IDENT { ($1, false, []) } - | IDENT QT QT { ($1, false, []) } + | IDENT { ($1, true, []) } + | IDENT QT QT { ($1, true, []) } | IDENT QT local idents QT { ($1, $3, $4) } ; term: diff --git a/helm/software/lambda-delta/toplevel/Make b/helm/software/lambda-delta/toplevel/Make index 94d41ca4f..33afbe36e 100644 --- a/helm/software/lambda-delta/toplevel/Make +++ b/helm/software/lambda-delta/toplevel/Make @@ -1 +1 @@ -meta metaAut top +meta metaOutput metaAut top diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index ac481a21d..e94fd37bc 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -23,39 +23,64 @@ * http://cs.unibo.it/helm/. *) -module H = Hashtbl module M = Meta module A = Aut type context_node = M.qid option (* context node: None = root *) -type context = (M.qid, M.term * context_node) H.t (* context: son, parent *) +type context = (M.qid * M.term * context_node) list (* context: son, parent *) type status = { - genv: M.environment; (* global environment *) - path: M.id list; (* current section path *) - cnt: context; (* context *) - node: context_node; (* current context node *) - explicit: bool (* need explicit context root? *) + genv: M.environment; (* global environment *) + path: M.id list; (* current section path *) + cnt: context; (* context *) + node: context_node; (* current context node *) + nodes: context_node list; (* context node list *) + explicit: bool (* need explicit context root? *) } type resolver = Local of int | Global of M.pars - | Unresolved let initial_status = { - genv = []; path = []; cnt = H.create 11; node = None; explicit = true + genv = []; path = []; cnt = []; node = None; nodes = []; explicit = true } +let find f cnt qid = + let rec aux f = function + | (name, w, node) :: tl when name = qid -> f tl (Some (w, node)) + | _ :: tl -> aux f tl + | [] -> f cnt None + in + aux f cnt + let complete_qid f st (id, is_local, qs) = let f qs = f (id, qs) in - if is_local then Cps.list_rev_append f st.path ~tail:qs else f qs + let f path = Cps.list_rev_append f path ~tail:qs in + let rec skip f = function + | phd :: ptl, qshd :: _ when phd = qshd -> f ptl + | _ :: ptl, _ :: _ -> skip f (ptl, qs) + | _ -> f [] + in + if is_local then f st.path else skip f (st.path, qs) + +let relax_qid f (id, path) = + let f path = f (id, path) in + let f = function + | _ :: tl -> Cps.list_rev f tl + | [] -> assert false + in + Cps.list_rev f path + +let relax_opt_qid f = function + | None -> f None + | Some qid -> let f qid = f (Some qid) in relax_qid f qid let resolve_gref f st lenv gref = let rec get_local f i = function - | [] -> f None - | (name, _) :: _ when name = gref -> f (Some i) - | _ :: tl -> get_local f (succ i) tl + | [] -> f None + | (name, _) :: _ when fst name = fst gref -> f (Some i) + | _ :: tl -> get_local f (succ i) tl in let rec get_global f = function | [] -> f None @@ -63,15 +88,43 @@ let resolve_gref f st lenv gref = | _ :: tl -> get_global f tl in let g = function - | Some args -> f (Global args) - | None -> f Unresolved + | Some args -> f gref (Some (Global args)) + | None -> f gref None in let f = function - | Some i -> f (Local i) + | Some i -> f gref (Some (Local i)) | None -> get_global g st.genv in get_local f 0 lenv +let resolve_gref_relaxed f st lenv gref = + let rec g gref = function + | None -> relax_qid (resolve_gref g st lenv) gref + | Some resolved -> f gref resolved + in + resolve_gref g st lenv gref + +let get_pars f st pars node = + let rec aux f cnt pars = function + | None -> + let f pars = f pars None in + Cps.list_rev f pars + | Some name as node -> + let f cnt = function + | Some (w, node) -> aux f cnt ((name, w) :: pars) node + | None -> f pars (Some node) + in + find f cnt name + in + aux f st.cnt pars node + +let get_pars_relaxed f st = + let rec g pars = function + | None -> f pars + | Some node -> relax_opt_qid (get_pars g st pars) node + in + get_pars g st [] st.node + let rec xlate_term f st lenv = function | A.Sort sort -> f (M.Sort sort) | A.Appl (v, t) -> @@ -98,18 +151,18 @@ let rec xlate_term f st lenv = function Cps.list_sub_strict f defs args in Cps.list_map f map1 args - | Unresolved -> assert false in - let f name = resolve_gref (f name) st lenv name in + let f name = resolve_gref_relaxed f st lenv name in complete_qid f st name let xlate_item f st = function | A.Section (Some name) -> - f {st with path = name :: st.path} + f {st with path = name :: st.path; nodes = st.node :: st.nodes} | A.Section None -> - begin match st.path with - | [] -> assert false - | _ :: tl -> f {st with path = tl} + begin match st.path, st.nodes with + | _ :: ptl, nhd :: ntl -> + f {st with path = ptl; node = nhd; nodes = ntl} + | _ -> assert false end | A.Context None -> f {st with node = None} @@ -117,11 +170,40 @@ let xlate_item f st = function let f name = f {st with node = Some name} in complete_qid f st name | A.Block (name, w) -> - let f name ww = H.add st.cnt name (ww, st.node); f st in - let f name = xlate_term (f name) st [] w in - complete_qid f st (name, true, []) - | A.Decl (name, w) -> f st - | A.Def (name, w, trans, v) -> f st + let f name = + let f ww = + let st = {st with cnt = (name, ww, st.node) :: st.cnt} in + f {st with node = Some name} + in + let f pars = xlate_term f st pars w in + get_pars_relaxed f st + in + complete_qid f st (name, true, []) + | A.Decl (name, w) -> + let f pars = + let f name = + let f ww = + let entry = (pars, name, ww, None) in + f {st with genv = entry :: st.genv} + in + xlate_term f st pars w + in + complete_qid f st (name, true, []) + in + get_pars_relaxed f st + | A.Def (name, w, trans, v) -> + let f pars = + let f name = + let f ww vv = + let entry = (pars, name, ww, Some (trans, vv)) in + f {st with genv = entry :: st.genv} + in + let f ww = xlate_term (f ww) st pars v in + xlate_term f st pars w + in + complete_qid f st (name, true, []) + in + get_pars_relaxed f st let meta_of_aut f book = let f st = f st.genv in diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml new file mode 100644 index 000000000..27157de37 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -0,0 +1,103 @@ +(* 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/. + *) + +module M = Meta + +type counters = { + eabsts: int; + eabbrs: int; + pabsts: int; + tsorts: int; + tlrefs: int; + tgrefs: int; + pappls: int; + tappls: int; + tabsts: int; +} + +let initial_counters = { + eabsts = 0; eabbrs = 0; pabsts = 0; pappls = 0; + tsorts = 0; tlrefs = 0; tgrefs = 0; tappls = 0; tabsts = 0 +} + +let rec count_term f c = function + | M.Sort _ -> + f {c with tsorts = succ c.tsorts} + | M.LRef _ -> + f {c with tlrefs = succ c.tlrefs} + | M.GRef (_, ts) -> + let c = {c with tgrefs = succ c.tgrefs} in + let c = {c with pappls = c.pappls + List.length ts} in + Cps.list_fold_left f count_term c ts + | M.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 + | M.Abst (_, w, t) -> + let c = {c with tabsts = succ c.tabsts} in + let f c = count_term f c t in + count_term f c w + +let count_par f c (_, w) = count_term f c w + +let count_item f c = function + | pars, _, w, None -> + let c = {c with eabsts = succ c.eabsts} in + let c = {c with pabsts = c.pabsts + List.length pars} in + let f c = count_term f c w in + Cps.list_fold_left f count_par c pars + | pars, _, w, Some (_, v) -> + let c = {c with eabbrs = succ c.eabbrs} in + let c = {c with pabsts = c.pabsts + List.length pars} in + let f c = count_term f c v in + let f c = count_term f c w in + Cps.list_fold_left f count_par c pars + +let count f c b = + Cps.list_fold_left f count_item c b + +let print_counters f c = + let terms = c.tsorts + c.tgrefs + c.tgrefs + c.tappls + c.tabsts in + let pars = c.pabsts + c.pappls in + let items = c.eabsts + c.eabbrs in + Printf.printf " Intermediate representation summary\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 parameter items: %6u\n" pars; + Printf.printf " Application items: %6u\n" c.pappls; + Printf.printf " Abstraction items: %6u\n" c.pabsts; + 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 " Application items: %6u\n" c.tappls; + Printf.printf " Abstraction items: %6u\n" c.tabsts; + flush stdout; f () + +let string_of_qid (id, path) = + let path = String.concat "/" path in + Filename.concat path id + diff --git a/helm/software/lambda-delta/toplevel/metaOutput.mli b/helm/software/lambda-delta/toplevel/metaOutput.mli new file mode 100644 index 000000000..d0d5766c9 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaOutput.mli @@ -0,0 +1,32 @@ +(* 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/. + *) + +type counters + +val initial_counters: counters + +val count: (counters -> 'a) -> counters -> Meta.environment -> 'a + +val print_counters: (unit -> 'a) -> counters -> 'a diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 1fd2b718c..c6ad99df9 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -23,7 +23,9 @@ * http://cs.unibo.it/helm/. *) -module AH = AutHelpers +module AO = AutOutput +module MA = MetaAut +module MO = MetaOutput let main = let version_string = "Helena Checker 0.8.0 M (June 2008)" in @@ -38,7 +40,12 @@ let main = let book = AutParser.book AutLexer.token lexbuf in close_in ich; if !summary > 1 then - AH.count (AH.print_counters Cps.id) AH.initial_counters book + AO.count (AO.print_counters Cps.id) AO.initial_counters book; + let f env = + if !summary > 1 then + MO.count (MO.print_counters Cps.id) MO.initial_counters env + in + MA.meta_of_aut f book in let help = "Usage: helena [ -V | -S ] ..." in let help_S = " Set summary level" in