From 75620ca64e3038fcbebb51559fdc31b2e8a00f93 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 12 Dec 2008 21:26:57 +0000 Subject: [PATCH] improved type hierarchy management --- helm/software/lambda-delta/.depend.opt | 32 ++++++------ helm/software/lambda-delta/Makefile | 1 + helm/software/lambda-delta/Makefile.common | 3 +- helm/software/lambda-delta/basic_rg/brg.ml | 2 - .../lambda-delta/basic_rg/brgOutput.ml | 8 ++- .../software/lambda-delta/basic_rg/brgType.ml | 4 +- .../lambda-delta/basic_rg/brgType.mli | 2 +- .../lambda-delta/basic_rg/brgUntrusted.mli | 2 +- helm/software/lambda-delta/lib/Make | 2 +- helm/software/lambda-delta/lib/hierarchy.ml | 49 +++++++++++++++++++ helm/software/lambda-delta/lib/hierarchy.mli | 24 +++++++++ .../software/lambda-delta/toplevel/metaBrg.ml | 11 +++-- helm/software/lambda-delta/toplevel/top.ml | 27 +++++++--- 13 files changed, 132 insertions(+), 35 deletions(-) create mode 100644 helm/software/lambda-delta/lib/hierarchy.ml create mode 100644 helm/software/lambda-delta/lib/hierarchy.mli diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 65ad62e6a..311265788 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -4,6 +4,8 @@ lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx +lib/hierarchy.cmo: lib/cps.cmx lib/hierarchy.cmi +lib/hierarchy.cmx: lib/cps.cmx lib/hierarchy.cmi automath/autOutput.cmi: automath/aut.cmx automath/autOutput.cmo: lib/log.cmi lib/cps.cmx automath/aut.cmx \ automath/autOutput.cmi @@ -17,10 +19,10 @@ automath/autLexer.cmx: lib/log.cmx automath/autParser.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/cps.cmx basic_rg/brg.cmx \ - basic_rg/brgOutput.cmi -basic_rg/brgOutput.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx basic_rg/brg.cmx \ - basic_rg/brgOutput.cmi +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/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 @@ -33,14 +35,14 @@ basic_rg/brgReduction.cmo: lib/share.cmx lib/log.cmi lib/cps.cmx \ basic_rg/brgReduction.cmx: lib/share.cmx lib/log.cmx lib/cps.cmx \ basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ basic_rg/brgReduction.cmi -basic_rg/brgType.cmi: basic_rg/brg.cmx -basic_rg/brgType.cmo: lib/log.cmi basic_rg/brgReduction.cmi \ +basic_rg/brgType.cmi: lib/hierarchy.cmi basic_rg/brg.cmx +basic_rg/brgType.cmo: lib/log.cmi lib/hierarchy.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/log.cmx basic_rg/brgReduction.cmx \ +basic_rg/brgType.cmx: lib/log.cmx lib/hierarchy.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: basic_rg/brg.cmx +basic_rg/brgUntrusted.cmi: lib/hierarchy.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgEnvironment.cmi \ basic_rg/brg.cmx basic_rg/brgUntrusted.cmi basic_rg/brgUntrusted.cmx: basic_rg/brgType.cmx basic_rg/brgEnvironment.cmx \ @@ -63,10 +65,12 @@ toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ 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/metaAut.cmi lib/log.cmi lib/cps.cmx \ - basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi basic_rg/brgOutput.cmi \ - automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx + toplevel/metaBrg.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 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/metaAut.cmx lib/log.cmx lib/cps.cmx \ - basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx basic_rg/brgOutput.cmx \ - automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx + toplevel/metaBrg.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 automath/autParser.cmx automath/autOutput.cmx \ + automath/autLexer.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index a568047d9..2be69cba3 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -17,6 +17,7 @@ test: $(MAIN).opt meta: $(MAIN).opt @echo " HELENA -m meta.txt automath/*.aut" $(H)./$(MAIN).opt -m meta.txt -s 1 -S 3 automath/*.aut > /dev/null + $(H)$(GZIP) meta.txt ifeq ($(MAKECMDGOALS), test) include .depend.opt diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index c9173f76c..e4489040d 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -4,9 +4,10 @@ INCLUDES = $(DIRECTORIES:%=-I %) OCAMLDEP = ocamlfind ocamldep -native $(INCLUDES) OCAMLOPT = ocamlfind opt -linkpkg -package "$(REQUIRES)" $(INCLUDES) -OCAMLLEX = ocamllex +OCAMLLEX = ocamllex.opt OCAMLYACC = ocamlyacc -v TAR = tar -czf $(MAIN:%=%.tgz) +GZIP = gzip define DIR_TEMPLATE MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make)) diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 17532c970..4778e5c3e 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -31,8 +31,6 @@ type context = int * (id * bind) list type message = (context, term) Log.item list -type hierarchy = int -> int - (* Currified constructors ***************************************************) let abst w = Abst w diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 4d3eb0ff7..958408303 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -14,6 +14,7 @@ module F = Format module U = NUri module C = Cps module L = Log +module H = Hierarchy module B = Brg type counters = { @@ -98,7 +99,12 @@ let print_counters f c = f () let rec pp_term c frm = function - | B.Sort h -> F.fprintf frm "@[*%u@]" h + | B.Sort h -> + let f = function + | Some s -> F.fprintf frm "@[%s@]" s + | None -> F.fprintf frm "@[*%u@]" h + in + H.get_sort f h | B.LRef i -> let f = function | Some (id, _) -> F.fprintf frm "@[%s@]" id diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index fd2409945..50d20b754 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -10,6 +10,7 @@ V_______________________________________________________________ *) module L = Log +module H = Hierarchy module B = Brg module O = BrgOutput module E = BrgEnvironment @@ -32,7 +33,8 @@ let error2 s1 c1 t1 s2 c2 t2 = let rec type_of f g c x = L.log O.specs level (L.ct_items1 "now checking" c x); match x with - | B.Sort h -> f (B.Sort (g h)) + | B.Sort h -> + let f h = f (B.Sort h) in H.apply f g h | B.LRef i -> let f = function | Some (_, B.Abst w) -> f w diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index 05845ce61..ccccaedfa 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -12,4 +12,4 @@ exception TypeError of Brg.message val type_of: - (Brg.term -> 'a) -> Brg.hierarchy -> Brg.context -> Brg.term -> 'a + (Brg.term -> 'a) -> Hierarchy.graph -> Brg.context -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli index 1c79b77e3..e65d67d99 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli @@ -10,4 +10,4 @@ V_______________________________________________________________ *) val type_check: - ((Brg.term * Brg.obj) option -> 'a) -> Brg.hierarchy -> Brg.item -> 'a + ((Brg.term * Brg.obj) option -> 'a) -> Hierarchy.graph -> Brg.item -> 'a diff --git a/helm/software/lambda-delta/lib/Make b/helm/software/lambda-delta/lib/Make index 5b884ad1b..4e21411d0 100644 --- a/helm/software/lambda-delta/lib/Make +++ b/helm/software/lambda-delta/lib/Make @@ -1 +1 @@ -nUri cps share log time +nUri cps share log time hierarchy diff --git a/helm/software/lambda-delta/lib/hierarchy.ml b/helm/software/lambda-delta/lib/hierarchy.ml new file mode 100644 index 000000000..f916e1e43 --- /dev/null +++ b/helm/software/lambda-delta/lib/hierarchy.ml @@ -0,0 +1,49 @@ +(* + ||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 S = Scanf +module C = Cps + +type graph = string * (int -> int) + +let sorts = 2 +let sort = H.create sorts +let index = ref 0 + +(* Internal functions *******************************************************) + +let set_sort f (h:int) (s:string) = + H.add sort h s; f (succ h) + +(* Interface functions ******************************************************) + +let set_new_sorts f ss = + let f i = index := i; f i in + C.list_fold_left f set_sort !index ss + +let get_sort f h = + try f (Some (H.find sort h)) + with Not_found -> f None + +let string_of_graph f (s, _) = f s + +let apply f (_, g) h = f (g h) + +let graph_of_string f s = + try + let x = S.sscanf s "Z%u" C.start in + if x > 0 then f (Some (s, fun h -> x + h)) else f None + with + S.Scan_failure _ | Failure _ | End_of_file -> f None + +let graph = + ref (graph_of_string (function Some g -> g | None -> assert false) "Z2") diff --git a/helm/software/lambda-delta/lib/hierarchy.mli b/helm/software/lambda-delta/lib/hierarchy.mli new file mode 100644 index 000000000..57413d909 --- /dev/null +++ b/helm/software/lambda-delta/lib/hierarchy.mli @@ -0,0 +1,24 @@ +(* + ||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 graph + +val set_new_sorts: (int -> 'a) -> string list -> 'a + +val get_sort: (string option -> 'a) -> int -> 'a + +val graph_of_string: (graph option -> 'a) -> string -> 'a + +val string_of_graph: (string -> 'a) -> graph -> 'a + +val apply: (int -> 'a) -> graph -> int -> 'a + +val graph: graph ref diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index 192613264..dfc7e8b56 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -9,13 +9,14 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module C = Cps 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 + let f a = C.list_fold_left f map2 a l in map1 f a let map_args f t v = f (B.Appl (v, t)) @@ -29,8 +30,8 @@ let rec xlate_term f = function | M.LRef (l, i) -> f (B.LRef (l - succ i)) | M.GRef (_, uri, vs) -> - let f vs = map_fold_left f Cps.id map_args (B.GRef uri) vs in - Cps.list_map f xlate_term vs + let f vs = map_fold_left f C.id map_args (B.GRef uri) vs in + C.list_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 @@ -48,12 +49,12 @@ let xlate_entry f = function | e, pars, uri, u, None -> let f u = f (e, uri, B.Abst u) in let f pars = map_fold_left f xlate_term map_pars u pars in - Cps.list_map f xlate_pars pars + C.list_map f xlate_pars pars | e, pars, uri, u, Some (_, t) -> let f u t = f (e, 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_map f xlate_pars pars + C.list_map f xlate_pars pars let xlate_item f = function | None -> f None diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index b3f65bb84..a2bac5616 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -11,7 +11,9 @@ module P = Printf module U = NUri +module C = Cps module L = Log +module H = Hierarchy module AO = AutOutput module MA = MetaAut module MO = MetaOutput @@ -34,7 +36,7 @@ let initial_status = { } let count count_fun c item = - if !L.level > 2 then count_fun Cps.start c item else c + if !L.level > 2 then count_fun C.start c item else c let brg_error s msg = L.error BrgO.specs (L.Warn s :: msg) @@ -44,7 +46,13 @@ try let version_string = "Helena Checker 0.8.0 M - December 2008" in let stage = ref 3 in let meta_file = ref None in - let hierarchy = ref (fun h -> h + 2) in + let set_hierarchy s = + let f = function + | Some g -> H.graph := g + | None -> L.warn (P.sprintf "Unknown type hierarchy: %s" s) + in + H.graph_of_string f s + in let set_summary i = L.level := i in let print_version () = L.warn version_string; exit 0 in let set_stage i = stage := i in @@ -81,7 +89,7 @@ try (* stage 2 *) let f st item = let st = {st with brgc = count BrgO.count_item st.brgc item} in - if !stage > 2 then BrgU.type_check (f st) !hierarchy item else st + if !stage > 2 then BrgU.type_check (f st) !H.graph item else st in (* stage 1 *) let f mst item = @@ -90,7 +98,7 @@ try } in begin match !meta_file with | None -> () - | Some (_, frm) -> MO.pp_item Cps.start frm item + | Some (_, frm) -> MO.pp_item C.start frm item end; if !stage > 1 then MBrg.brg_of_meta (f st) item else st in @@ -103,23 +111,26 @@ try in let st = aux initial_status book in if !L.level > 0 then Time.utime_stamp "processed"; - if !L.level > 2 then AO.print_counters Cps.start st.ac; - if !L.level > 2 && !stage > 0 then MO.print_counters Cps.start st.mc; - if !L.level > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc; + 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 BrgO.print_counters C.start st.brgc; in let help = - "Usage: helena [ -V | -Ss | -m ] ...\n\n" ^ + "Usage: helena [ -V | -Ss | -m | -h ] ...\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" in let help_S = " Set summary level" in let help_V = " Show version information" in + let help_h = " set type hierarchy" in let help_m = " output intermediate representation" in let help_s = " Set translation stage" in + H.set_new_sorts ignore ["Set"; "Prop"]; Arg.parse [ ("-S", Arg.Int set_summary, help_S); ("-V", Arg.Unit print_version, help_V); + ("-h", Arg.String set_hierarchy, help_h); ("-m", Arg.String set_meta_file, help_m); ("-s", Arg.Int set_stage, help_s); ] read_file help; -- 2.39.2