automath/autHelpers.cmi: automath/aut.cmx
-automath/autHelpers.cmo: automath/aut.cmx automath/autHelpers.cmi
-automath/autHelpers.cmx: automath/aut.cmx automath/autHelpers.cmi
+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/autParser.cmi: automath/aut.cmx
automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi
automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi
automath/autLexer.cmo: automath/autParser.cmi
automath/autLexer.cmx: automath/autParser.cmx
-toplevel/top.cmo: automath/autParser.cmi automath/autLexer.cmx \
+toplevel/meta.cmo: automath/aut.cmx
+toplevel/meta.cmx: automath/aut.cmx
+toplevel/metaAut.cmo: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx
+toplevel/metaAut.cmx: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx
+toplevel/top.cmo: cps/cps.cmx automath/autParser.cmi automath/autLexer.cmx \
automath/autHelpers.cmi
-toplevel/top.cmx: automath/autParser.cmx automath/autLexer.cmx \
+toplevel/top.cmx: cps/cps.cmx automath/autParser.cmx automath/autLexer.cmx \
automath/autHelpers.cmx
MAIN = helena
-DIRECTORIES = automath toplevel
+DIRECTORIES = cps automath toplevel
REQUIRES =
-KEEP = automath/*.aut
+KEEP = README automath/*.aut
CLEAN = log.txt
sorts = 0; grefs = 0; appls = 0; absts = 0
}
-let rec list_fold_left f map a = function
- | [] -> f a
- | hd :: tl ->
- let f a = list_fold_left f map a tl in
- map f a hd
-
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
- list_fold_left f count_term c ts
+ 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 w
let count f c b =
- list_fold_left f count_item 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 " 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;
+ 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 ()
--- /dev/null
+(* 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 _ = ()
+
+let rec list_sub_strict f l1 l2 = match l1, l2 with
+ | _, [] -> f l1
+ | _ :: tl1, _ :: tl2 -> list_sub_strict f tl1 tl2
+ | _ -> assert false
+
+let rec list_fold_left f map a = function
+ | [] -> f a
+ | hd :: tl ->
+ let f a = list_fold_left f map a tl in
+ map f a hd
+
+let rec list_rev_map_append f map ~tail = function
+ | [] -> f tail
+ | hd :: tl ->
+ let f hd = list_rev_map_append f map ~tail:(hd :: tail) tl in
+ map f hd
+
+let list_rev_append f =
+ list_rev_map_append f (fun f t -> f t)
+
+let list_rev_map =
+ list_rev_map_append ~tail:[]
+
+let list_rev =
+ list_rev_append ~tail:[]
+
+let list_map f =
+ list_rev_map (list_rev f)
+
--- /dev/null
+(* 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 id = Aut.id
+
+type qid = id * id list (* qualified identifier: name, qualifiers *)
+
+type term = Sort of bool (* sorts: true = TYPE, false = PROP *)
+ | LRef of int (* local reference: de bruijn index *)
+ | GRef of qid * term list (* global reference: name, arguments *)
+ | Appl of term * term (* application: argument, function *)
+ | Abst of id * term * term (* abstraction: name, type, body *)
+
+type pars = (qid * term) list (* parameter declarations: name, type *)
+
+(* environment: parameters, name, type, (transparent?, body) *)
+type environment = (pars * qid * term * (bool * term) option) list
--- /dev/null
+(* 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 H = Hashtbl
+module M = Meta
+module A = Aut
+
+type context_node = M.qid option (* context node: None = root *)
+
+type context = (M.qid, context_node) H.t (* 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? *)
+}
+
+type resolver = Local of int
+ | Global of M.pars
+ | Unresolved
+
+let initial_status = {
+ genv = []; path = []; cnt = H.create 11; node = None; explicit = true
+}
+
+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 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
+ in
+ let rec get_global f = function
+ | [] -> None
+ | (args, name, _, _) :: _ when name = gref -> f (Some args)
+ | _ :: tl -> get_global f tl
+ in
+ let g = function
+ | Some args -> f (Global args)
+ | None -> f Unresolved
+ in
+ let f = function
+ | Some i -> f (Local i)
+ | None -> get_global g st.genv
+ in
+ get_local f 0 lenv
+
+let rec xlate_term f st lenv = function
+ | A.Sort sort -> f (M.Sort sort)
+ | A.Appl (v, t) ->
+ let f vv tt = f (M.Appl (vv, tt)) in
+ let f vv = xlate_term (f vv) st lenv t in
+ xlate_term f st lenv v
+ | A.Abst (name, w, t) ->
+ let add name w lenv =
+ let f name = (name, w) :: lenv in
+ complete_qid f st (name, true, [])
+ in
+ let f ww tt = f (M.Abst (name, ww, tt)) in
+ let f ww = xlate_term (f ww) st (add name ww lenv) t in
+ xlate_term f st lenv w
+ | A.GRef (name, args) ->
+ let f name = function
+ | Local i -> f (M.LRef i)
+ | Global defs ->
+ let map1 f = xlate_term f st lenv in
+ let map2 f (name, _) = f (M.GRef (name, [])) in
+ let f tail =
+ let f args = f (M.GRef (name, args)) in
+ let f defs = Cps.list_rev_map_append f map2 defs ~tail in
+ 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
+ complete_qid f st name
let main =
let version_string = "Helena Checker 0.8.0 M (June 2008)" in
- let id _ = () in
let summary = ref 0 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 > 1 then
- AH.count (AH.print_counters id) AH.initial_counters book
+ AH.count (AH.print_counters Cps.id) AH.initial_counters book
in
let help = "Usage: helena [ -V | -S <number> ] <file> ..." in
let help_S = "<number> Set summary level" in
projects / helm.git / commitdiff