From: Ferruccio Guidi Date: Sat, 15 Aug 2009 10:43:46 +0000 (+0000) Subject: - kernel parameters indication added to exported objects (xml) X-Git-Tag: make_still_working~3540 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c8011c7ad75be5d03c4d4bb2e6900af32ad65c07;p=helm.git - kernel parameters indication added to exported objects (xml) - some refactoring --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index ce241a639..148c2377a 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -10,12 +10,6 @@ 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.cmi: -lib/hierarchy.cmo: lib/cps.cmx lib/hierarchy.cmi -lib/hierarchy.cmx: lib/cps.cmx lib/hierarchy.cmi -lib/output.cmi: -lib/output.cmo: lib/log.cmi lib/output.cmi -lib/output.cmx: lib/log.cmx lib/output.cmi automath/aut.cmo: automath/aut.cmx: automath/autProcess.cmi: automath/aut.cmx @@ -31,22 +25,24 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx -common/common.cmo: lib/nUri.cmi automath/aut.cmx -common/common.cmx: lib/nUri.cmx automath/aut.cmx -common/commonLibrary.cmi: common/common.cmx -common/commonLibrary.cmo: lib/nUri.cmi common/common.cmx \ - common/commonLibrary.cmi -common/commonLibrary.cmx: lib/nUri.cmx common/common.cmx \ - common/commonLibrary.cmi -basic_rg/brg.cmo: lib/log.cmi lib/cps.cmx common/common.cmx -basic_rg/brg.cmx: lib/log.cmx lib/cps.cmx common/common.cmx -basic_rg/brgOutput.cmi: lib/log.cmi common/common.cmx basic_rg/brg.cmx -basic_rg/brgOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ - lib/hierarchy.cmi lib/cps.cmx common/commonLibrary.cmi basic_rg/brg.cmx \ - basic_rg/brgOutput.cmi -basic_rg/brgOutput.cmx: lib/output.cmx lib/nUri.cmx lib/log.cmx \ - lib/hierarchy.cmx lib/cps.cmx common/commonLibrary.cmx basic_rg/brg.cmx \ - basic_rg/brgOutput.cmi +common/hierarchy.cmi: +common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi +common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi +common/output.cmi: +common/output.cmo: lib/log.cmi common/output.cmi +common/output.cmx: lib/log.cmx common/output.cmi +common/item.cmo: lib/nUri.cmi automath/aut.cmx +common/item.cmx: lib/nUri.cmx automath/aut.cmx +common/library.cmi: common/item.cmx common/hierarchy.cmi +common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/library.cmi +common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/library.cmi +basic_rg/brg.cmo: lib/log.cmi common/item.cmx lib/cps.cmx +basic_rg/brg.cmx: lib/log.cmx common/item.cmx lib/cps.cmx +basic_rg/brgOutput.cmi: lib/log.cmi common/item.cmx basic_rg/brg.cmx +basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ + common/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi +basic_rg/brgOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ + common/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 @@ -56,33 +52,33 @@ basic_rg/brgSubstitution.cmi: basic_rg/brg.cmx basic_rg/brgSubstitution.cmo: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi basic_rg/brgSubstitution.cmx: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi basic_rg/brgReduction.cmi: basic_rg/brg.cmx -basic_rg/brgReduction.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ +basic_rg/brgReduction.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ lib/cps.cmx basic_rg/brgSubstitution.cmi basic_rg/brgOutput.cmi \ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi -basic_rg/brgReduction.cmx: lib/output.cmx lib/nUri.cmx lib/log.cmx \ +basic_rg/brgReduction.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ lib/cps.cmx basic_rg/brgSubstitution.cmx basic_rg/brgOutput.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi -basic_rg/brgType.cmi: lib/hierarchy.cmi basic_rg/brg.cmx +basic_rg/brgType.cmi: common/hierarchy.cmi basic_rg/brg.cmx basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ - lib/hierarchy.cmi lib/cps.cmx basic_rg/brgSubstitution.cmi \ + common/hierarchy.cmi lib/cps.cmx basic_rg/brgSubstitution.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/share.cmx lib/nUri.cmx lib/log.cmx \ - lib/hierarchy.cmx lib/cps.cmx basic_rg/brgSubstitution.cmx \ + common/hierarchy.cmx lib/cps.cmx basic_rg/brgSubstitution.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: lib/hierarchy.cmi basic_rg/brg.cmx +basic_rg/brgUntrusted.cmi: common/hierarchy.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi basic_rg/brgUntrusted.cmx: lib/log.cmx basic_rg/brgType.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi -basic_ag/bag.cmo: lib/log.cmi lib/cps.cmx common/common.cmx -basic_ag/bag.cmx: lib/log.cmx lib/cps.cmx common/common.cmx +basic_ag/bag.cmo: lib/log.cmi common/item.cmx lib/cps.cmx +basic_ag/bag.cmx: lib/log.cmx common/item.cmx lib/cps.cmx basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx -basic_ag/bagOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ - lib/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi -basic_ag/bagOutput.cmx: lib/output.cmx lib/nUri.cmx lib/log.cmx \ - lib/hierarchy.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi +basic_ag/bagOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ + common/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi +basic_ag/bagOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ + common/hierarchy.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi: lib/nUri.cmi basic_ag/bag.cmx basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_ag/bag.cmx \ basic_ag/bagEnvironment.cmi @@ -100,16 +96,16 @@ basic_ag/bagReduction.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx \ basic_ag/bagReduction.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \ basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \ basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagReduction.cmi -basic_ag/bagType.cmi: lib/hierarchy.cmi basic_ag/bag.cmx +basic_ag/bagType.cmi: common/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ - lib/hierarchy.cmi lib/cps.cmx basic_ag/bagReduction.cmi \ + common/hierarchy.cmi lib/cps.cmx basic_ag/bagReduction.cmi \ basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi basic_ag/bag.cmx \ basic_ag/bagType.cmi basic_ag/bagType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ - lib/hierarchy.cmx lib/cps.cmx basic_ag/bagReduction.cmx \ + common/hierarchy.cmx lib/cps.cmx basic_ag/bagReduction.cmx \ basic_ag/bagOutput.cmx basic_ag/bagEnvironment.cmx basic_ag/bag.cmx \ basic_ag/bagType.cmi -basic_ag/bagUntrusted.cmi: lib/hierarchy.cmi basic_ag/bag.cmx +basic_ag/bagUntrusted.cmi: common/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagUntrusted.cmo: lib/log.cmi basic_ag/bagType.cmi \ basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagUntrusted.cmi basic_ag/bagUntrusted.cmx: lib/log.cmx basic_ag/bagType.cmx \ @@ -136,19 +132,19 @@ 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 lib/output.cmi lib/nUri.cmi \ +toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \ toplevel/metaOutput.cmi toplevel/metaBrg.cmi toplevel/metaBag.cmi \ - toplevel/metaAut.cmi lib/log.cmi lib/hierarchy.cmi lib/cps.cmx \ - common/commonLibrary.cmi basic_rg/brgUntrusted.cmi \ - basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmi basic_ag/bagReduction.cmi \ - basic_ag/bagOutput.cmi basic_ag/bag.cmx automath/autProcess.cmi \ - automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx -toplevel/top.cmx: lib/time.cmx lib/output.cmx lib/nUri.cmx \ + toplevel/metaAut.cmi lib/log.cmi common/library.cmi common/hierarchy.cmi \ + lib/cps.cmx basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \ + basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \ + basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \ + automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \ + automath/autLexer.cmx +toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \ toplevel/metaOutput.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \ - toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx lib/cps.cmx \ - common/commonLibrary.cmx basic_rg/brgUntrusted.cmx \ - basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmx basic_ag/bagReduction.cmx \ - basic_ag/bagOutput.cmx basic_ag/bag.cmx automath/autProcess.cmx \ - automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx + toplevel/metaAut.cmx lib/log.cmx common/library.cmx common/hierarchy.cmx \ + lib/cps.cmx basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \ + basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \ + basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \ + automath/autProcess.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 705dc89bd..b158ae3e0 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -6,7 +6,7 @@ KEEP = README automath/*.aut CLEAN = log.txt -TAGS = test test-si meta export +TAGS = test test-si meta export-si include Makefile.common @@ -27,6 +27,6 @@ meta: $(MAIN).opt $(H)./$(MAIN).opt -m meta.txt -s 1 -S 1 $(INPUT) > log.txt $(H)$(GZIP) meta.txt -export: $(MAIN).opt - @echo " HELENA -x xml $(INPUT)" - $(H)./$(MAIN).opt -x xml -s 2 -S 1 $(INPUT) > log.txt +export-si: $(MAIN).opt + @echo " HELENA -u -x xml $(INPUT)" + $(H)./$(MAIN).opt -u -x xml -s 2 -S 1 $(INPUT) > log.txt diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml index 585e8e388..65a93ab18 100644 --- a/helm/software/lambda-delta/basic_ag/bag.ml +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -12,8 +12,8 @@ (* kernel version: basic, absolute, global *) (* note : experimental *) -type uri = Common.uri -type id = Common.id +type uri = Item.uri +type id = Item.id type bind = Void (* exclusion *) | Abst of term (* abstraction *) @@ -26,9 +26,9 @@ and term = Sort of int (* hierarchy index *) | Appl of term * term (* argument, function *) | Bind of int * id * bind * term (* location, name, binder, scope *) -type obj = bind Common.obj (* age, uri, binder *) +type obj = bind Item.obj (* age, uri, binder *) -type item = bind Common.item +type item = bind Item.item type context = (int * id * bind) list (* location, name, binder *) diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 8b0d54533..d62a130a4 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -12,8 +12,8 @@ (* kernel version: basic, relative, global *) (* note : ufficial basic lambda-delta *) -type uri = Common.uri -type id = Common.id +type uri = Item.uri +type id = Item.id type bind = Void (* exclusion *) | Abst of term (* abstraction *) @@ -31,9 +31,9 @@ and attr = Name of bool * id (* real?, name *) and attrs = attr list -type obj = bind Common.obj (* age, uri, binder *) +type obj = bind Item.obj (* age, uri, binder *) -type item = bind Common.item +type item = bind Item.item type context = (attrs * bind) list (* attrs, binder *) diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 1aa3f9db7..fb33da537 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -15,7 +15,6 @@ module U = NUri module L = Log module H = Hierarchy module O = Output -module CL = CommonLibrary module B = Brg (* nodes count **************************************************************) @@ -32,7 +31,7 @@ type counters = { tabsts: int; tabbrs: int; tvoids: int; - uris : U.uri list; + uris : B.uri list; nodes : int; xnodes: int } @@ -222,16 +221,16 @@ and exp_bind a frm = function | B.Void -> F.fprintf frm "" id a -let export_obj frm = function +let exp_obj frm = function | _, uri, B.Abst w -> let str = U.string_of_uri uri in - F.fprintf frm "%s@,@,%a" - (CL.doctype "ABST") str exp_boxed w + F.fprintf frm "@,%a" str exp_term w | _, uri, B.Abbr v -> let str = U.string_of_uri uri in - F.fprintf frm "%s@,@,%a" - (CL.doctype "ABBR") str exp_boxed v + F.fprintf frm "@,%a" str exp_term v | _, uri, B.Void -> let str = U.string_of_uri uri in - F.fprintf frm "%s@,@," - (CL.doctype "VOID") str + F.fprintf frm "" str + +let export_obj frm obj = + F.fprintf frm "@,@[ %a@]@," exp_obj obj diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index f238af5d0..138a29a9c 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -19,4 +19,4 @@ val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Brg.context, Brg.term) Log.specs -val export_obj: Format.formatter -> Brg.bind Common.obj -> unit +val export_obj: Format.formatter -> Brg.bind Item.obj -> unit diff --git a/helm/software/lambda-delta/common/Make b/helm/software/lambda-delta/common/Make index da8537d07..801c1a84f 100644 --- a/helm/software/lambda-delta/common/Make +++ b/helm/software/lambda-delta/common/Make @@ -1 +1 @@ -common commonLibrary +hierarchy output item library diff --git a/helm/software/lambda-delta/common/common.ml b/helm/software/lambda-delta/common/common.ml deleted file mode 100644 index 7e9b7cea8..000000000 --- a/helm/software/lambda-delta/common/common.ml +++ /dev/null @@ -1,17 +0,0 @@ -(* - ||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 -type id = Aut.id - -type 'bind obj = int * uri * 'bind (* age, uri, binder *) - -type 'bind item = 'bind obj option diff --git a/helm/software/lambda-delta/common/commonLibrary.ml b/helm/software/lambda-delta/common/commonLibrary.ml deleted file mode 100644 index d19f491ae..000000000 --- a/helm/software/lambda-delta/common/commonLibrary.ml +++ /dev/null @@ -1,44 +0,0 @@ -(* - ||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 = Filename -module U = NUri -module P = Printf -module C = Common - -(* internal functions *******************************************************) - -let obj_ext = ".ld.xml" - -let xml_head = - P.sprintf "" "1.0" "UTF-8" - -let system = "http://helm.cs.unibo.it/lambda-delta/ld.dtd" - -let path_of_uri base uri = - F.concat base (Str.string_after (U.string_of_uri uri) 3) - -(* interface functions ******************************************************) - -let doctype s = - P.sprintf "" s system - -let export_item export_obj base = function - | Some obj -> - let _, uri, bind = obj in - let path = path_of_uri base uri in - let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in - let och = open_out (path ^ obj_ext) in - let frm = Format.formatter_of_out_channel och in - Format.pp_set_margin frm max_int; - Format.fprintf frm "@[%s@,@,%a@]@." xml_head export_obj obj; - close_out och - | None -> () diff --git a/helm/software/lambda-delta/common/commonLibrary.mli b/helm/software/lambda-delta/common/commonLibrary.mli deleted file mode 100644 index 9cf3c9f40..000000000 --- a/helm/software/lambda-delta/common/commonLibrary.mli +++ /dev/null @@ -1,16 +0,0 @@ -(* - ||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 export_item: - (Format.formatter -> 'bind Common.obj -> unit) -> - string -> 'bind Common.item -> unit - -val doctype: string -> string diff --git a/helm/software/lambda-delta/common/hierarchy.ml b/helm/software/lambda-delta/common/hierarchy.ml new file mode 100644 index 000000000..f916e1e43 --- /dev/null +++ b/helm/software/lambda-delta/common/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/common/hierarchy.mli b/helm/software/lambda-delta/common/hierarchy.mli new file mode 100644 index 000000000..57413d909 --- /dev/null +++ b/helm/software/lambda-delta/common/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/common/item.ml b/helm/software/lambda-delta/common/item.ml new file mode 100644 index 000000000..7e9b7cea8 --- /dev/null +++ b/helm/software/lambda-delta/common/item.ml @@ -0,0 +1,17 @@ +(* + ||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 +type id = Aut.id + +type 'bind obj = int * uri * 'bind (* age, uri, binder *) + +type 'bind item = 'bind obj option diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml new file mode 100644 index 000000000..80e9c59da --- /dev/null +++ b/helm/software/lambda-delta/common/library.ml @@ -0,0 +1,54 @@ +(* + ||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 = Filename +module U = NUri +module H = Hierarchy + +(* internal functions *******************************************************) + +let obj_ext = ".ld.xml" + +let system = "http://helm.cs.unibo.it/lambda-delta/xml/ld.dtd" + +let path_of_uri base uri = + F.concat base (Str.string_after (U.string_of_uri uri) 3) + +let pp_head frm = + Format.fprintf frm "@,@," "1.0" "UTF-8" + +let pp_doctype frm = + Format.fprintf frm "@,@," system + +let open_kernel si g frm = + let opts = if si then "si" else "" in + let f shp = + Format.fprintf frm "" shp opts + in + H.string_of_graph f g + +let close_kernel frm = + Format.fprintf frm "" + +(* interface functions ******************************************************) + +let export_item export_obj si g base = function + | Some obj -> + let _, uri, bind = obj in + let path = path_of_uri base uri in + let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in + let och = open_out (path ^ obj_ext) in + let frm = Format.formatter_of_out_channel och in + Format.pp_set_margin frm max_int; + Format.fprintf frm "@[%t%t%t%a%t@]@." + pp_head pp_doctype (open_kernel si g) export_obj obj close_kernel; + close_out och + | None -> () diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli new file mode 100644 index 000000000..3c89ab317 --- /dev/null +++ b/helm/software/lambda-delta/common/library.mli @@ -0,0 +1,14 @@ +(* + ||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 export_item: + (Format.formatter -> 'bind Item.obj -> unit) -> + bool -> Hierarchy.graph -> string -> 'bind Item.item -> unit diff --git a/helm/software/lambda-delta/common/output.ml b/helm/software/lambda-delta/common/output.ml new file mode 100644 index 000000000..6dd526bfb --- /dev/null +++ b/helm/software/lambda-delta/common/output.ml @@ -0,0 +1,72 @@ +(* + ||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 P = Printf +module L = Log + +type reductions = { + beta : int; + zeta : int; + upsilon: int; + tau : int; + ldelta : int; + gdelta : int; + si : int; + lrt : int; + grt : int +} + +let initial_reductions = { + beta = 0; upsilon = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0; + si = 0; lrt = 0; grt = 0 +} + +let reductions = ref initial_reductions + +let clear_reductions () = reductions := initial_reductions + +let add + ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) + ?(si=0) ?(lrt=0) ?(grt=0) () += reductions := { + beta = !reductions.beta + beta; + zeta = !reductions.zeta + zeta; + upsilon = !reductions.upsilon + upsilon; + tau = !reductions.tau + tau; + ldelta = !reductions.ldelta + ldelta; + gdelta = !reductions.gdelta + gdelta; + si = !reductions.si + si; + lrt = !reductions.lrt + lrt; + grt = !reductions.grt + grt +} + +let print_reductions () = + let r = !reductions in + let rs = r.beta + r.ldelta + r.zeta + r.upsilon + r.tau + r.gdelta in + let prs = r.si + r.lrt + r.grt in + let delta = r.ldelta + r.gdelta in + let rt = r.lrt + r.grt in + L.warn (P.sprintf " Reductions summary"); + L.warn (P.sprintf " Proper reductions: %7u" rs); + L.warn (P.sprintf " Beta: %7u" r.beta); + L.warn (P.sprintf " Delta: %7u" delta); + L.warn (P.sprintf " Local: %7u" r.ldelta); + L.warn (P.sprintf " Global: %7u" r.gdelta); + L.warn (P.sprintf " Zeta: %7u" r.zeta); + L.warn (P.sprintf " Upsilon: %7u" r.upsilon); + L.warn (P.sprintf " Tau: %7u" r.tau); + L.warn (P.sprintf " Pseudo reductions: %7u" prs); + L.warn (P.sprintf " Reference typing: %7u" rt); + L.warn (P.sprintf " Local: %7u" r.lrt); + L.warn (P.sprintf " Global: %7u" r.grt); + L.warn (P.sprintf " Sort inclusion: %7u" r.si) + +let indexes = ref false diff --git a/helm/software/lambda-delta/common/output.mli b/helm/software/lambda-delta/common/output.mli new file mode 100644 index 000000000..812531585 --- /dev/null +++ b/helm/software/lambda-delta/common/output.mli @@ -0,0 +1,21 @@ +(* + ||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 indexes: bool ref + +val clear_reductions: unit -> unit + +val add: + ?beta:int -> ?upsilon:int -> ?tau:int -> ?ldelta:int -> ?gdelta:int -> + ?zeta:int -> ?si:int -> ?lrt:int -> ?grt:int -> + unit -> unit + +val print_reductions: unit -> unit diff --git a/helm/software/lambda-delta/lib/Make b/helm/software/lambda-delta/lib/Make index f0be78e29..5b884ad1b 100644 --- a/helm/software/lambda-delta/lib/Make +++ b/helm/software/lambda-delta/lib/Make @@ -1 +1 @@ -nUri cps share log time hierarchy output +nUri cps share log time diff --git a/helm/software/lambda-delta/lib/hierarchy.ml b/helm/software/lambda-delta/lib/hierarchy.ml deleted file mode 100644 index f916e1e43..000000000 --- a/helm/software/lambda-delta/lib/hierarchy.ml +++ /dev/null @@ -1,49 +0,0 @@ -(* - ||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 deleted file mode 100644 index 57413d909..000000000 --- a/helm/software/lambda-delta/lib/hierarchy.mli +++ /dev/null @@ -1,24 +0,0 @@ -(* - ||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/lib/output.ml b/helm/software/lambda-delta/lib/output.ml deleted file mode 100644 index 6dd526bfb..000000000 --- a/helm/software/lambda-delta/lib/output.ml +++ /dev/null @@ -1,72 +0,0 @@ -(* - ||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 P = Printf -module L = Log - -type reductions = { - beta : int; - zeta : int; - upsilon: int; - tau : int; - ldelta : int; - gdelta : int; - si : int; - lrt : int; - grt : int -} - -let initial_reductions = { - beta = 0; upsilon = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0; - si = 0; lrt = 0; grt = 0 -} - -let reductions = ref initial_reductions - -let clear_reductions () = reductions := initial_reductions - -let add - ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) - ?(si=0) ?(lrt=0) ?(grt=0) () -= reductions := { - beta = !reductions.beta + beta; - zeta = !reductions.zeta + zeta; - upsilon = !reductions.upsilon + upsilon; - tau = !reductions.tau + tau; - ldelta = !reductions.ldelta + ldelta; - gdelta = !reductions.gdelta + gdelta; - si = !reductions.si + si; - lrt = !reductions.lrt + lrt; - grt = !reductions.grt + grt -} - -let print_reductions () = - let r = !reductions in - let rs = r.beta + r.ldelta + r.zeta + r.upsilon + r.tau + r.gdelta in - let prs = r.si + r.lrt + r.grt in - let delta = r.ldelta + r.gdelta in - let rt = r.lrt + r.grt in - L.warn (P.sprintf " Reductions summary"); - L.warn (P.sprintf " Proper reductions: %7u" rs); - L.warn (P.sprintf " Beta: %7u" r.beta); - L.warn (P.sprintf " Delta: %7u" delta); - L.warn (P.sprintf " Local: %7u" r.ldelta); - L.warn (P.sprintf " Global: %7u" r.gdelta); - L.warn (P.sprintf " Zeta: %7u" r.zeta); - L.warn (P.sprintf " Upsilon: %7u" r.upsilon); - L.warn (P.sprintf " Tau: %7u" r.tau); - L.warn (P.sprintf " Pseudo reductions: %7u" prs); - L.warn (P.sprintf " Reference typing: %7u" rt); - L.warn (P.sprintf " Local: %7u" r.lrt); - L.warn (P.sprintf " Global: %7u" r.grt); - L.warn (P.sprintf " Sort inclusion: %7u" r.si) - -let indexes = ref false diff --git a/helm/software/lambda-delta/lib/output.mli b/helm/software/lambda-delta/lib/output.mli deleted file mode 100644 index 812531585..000000000 --- a/helm/software/lambda-delta/lib/output.mli +++ /dev/null @@ -1,21 +0,0 @@ -(* - ||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 indexes: bool ref - -val clear_reductions: unit -> unit - -val add: - ?beta:int -> ?upsilon:int -> ?tau:int -> ?ldelta:int -> ?gdelta:int -> - ?zeta:int -> ?si:int -> ?lrt:int -> ?grt:int -> - unit -> unit - -val print_reductions: unit -> unit diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 23460410d..6a45f06c5 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -21,7 +21,7 @@ module AO = AutOutput module MA = MetaAut module MO = MetaOutput module MBrg = MetaBrg -module CL = CommonLibrary +module G = Library module BrgO = BrgOutput module BrgR = BrgReduction module BrgU = BrgUntrusted @@ -88,8 +88,8 @@ let count_item st = function | BrgItem item -> {st with brgc = count BrgO.count_item st.brgc item} | BagItem item -> {st with bagc = count BagO.count_item st.bagc item} -let export_item base = function - | BrgItem item -> CL.export_item BrgO.export_obj base item +let export_item si g base = function + | BrgItem item -> G.export_item BrgO.export_obj si g base item | BagItem _ -> () let type_check f st si g k = @@ -167,7 +167,7 @@ try let st = count_item st item in begin match !library_dir with | None -> () - | Some base -> export_item base item + | Some base -> export_item !si !H.graph base item end; if !stage > 2 then type_check f st !si !H.graph item else st in