From cbdccfa38c3e05d697318cfbb9903a451e4e80d6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 16 Jun 2008 17:19:52 +0000 Subject: [PATCH] transformation from automath to intermediate language started --- helm/software/lambda-delta/.depend.opt | 12 +- helm/software/lambda-delta/Makefile | 4 +- .../lambda-delta/automath/autHelpers.ml | 33 +++--- helm/software/lambda-delta/cps/Make | 1 + helm/software/lambda-delta/cps/cps.ml | 56 ++++++++++ helm/software/lambda-delta/toplevel/Make | 2 +- helm/software/lambda-delta/toplevel/meta.ml | 39 +++++++ .../software/lambda-delta/toplevel/metaAut.ml | 104 ++++++++++++++++++ helm/software/lambda-delta/toplevel/top.ml | 3 +- 9 files changed, 226 insertions(+), 28 deletions(-) create mode 100644 helm/software/lambda-delta/cps/Make create mode 100644 helm/software/lambda-delta/cps/cps.ml create mode 100644 helm/software/lambda-delta/toplevel/meta.ml create mode 100644 helm/software/lambda-delta/toplevel/metaAut.ml diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index d97f81518..4df20fa26 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,12 +1,16 @@ 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 diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 054337b5c..e62fb5dfc 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -1,10 +1,10 @@ MAIN = helena -DIRECTORIES = automath toplevel +DIRECTORIES = cps automath toplevel REQUIRES = -KEEP = automath/*.aut +KEEP = README automath/*.aut CLEAN = log.txt diff --git a/helm/software/lambda-delta/automath/autHelpers.ml b/helm/software/lambda-delta/automath/autHelpers.ml index b594ed1df..769902529 100644 --- a/helm/software/lambda-delta/automath/autHelpers.ml +++ b/helm/software/lambda-delta/automath/autHelpers.ml @@ -42,18 +42,12 @@ let initial_counters = { 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 @@ -80,20 +74,21 @@ let count_item f c = function 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 () diff --git a/helm/software/lambda-delta/cps/Make b/helm/software/lambda-delta/cps/Make new file mode 100644 index 000000000..0e120998d --- /dev/null +++ b/helm/software/lambda-delta/cps/Make @@ -0,0 +1 @@ +cps diff --git a/helm/software/lambda-delta/cps/cps.ml b/helm/software/lambda-delta/cps/cps.ml new file mode 100644 index 000000000..83570aa2e --- /dev/null +++ b/helm/software/lambda-delta/cps/cps.ml @@ -0,0 +1,56 @@ +(* 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) + diff --git a/helm/software/lambda-delta/toplevel/Make b/helm/software/lambda-delta/toplevel/Make index bf1a1fdef..94d41ca4f 100644 --- a/helm/software/lambda-delta/toplevel/Make +++ b/helm/software/lambda-delta/toplevel/Make @@ -1 +1 @@ -top +meta metaAut top diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml new file mode 100644 index 000000000..a35ecab8b --- /dev/null +++ b/helm/software/lambda-delta/toplevel/meta.ml @@ -0,0 +1,39 @@ +(* 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 diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml new file mode 100644 index 000000000..2cce50a83 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -0,0 +1,104 @@ +(* 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 diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 823ce1a47..1fd2b718c 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -27,7 +27,6 @@ module AH = AutHelpers 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 @@ -39,7 +38,7 @@ let main = 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 ] ..." in let help_S = " Set summary level" in -- 2.39.2