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
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
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
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 \
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
CLEAN = log.txt
-TAGS = test test-si meta export
+TAGS = test test-si meta export-si
include Makefile.common
$(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
(* 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 *)
| 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 *)
(* 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 *)
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 *)
module L = Log
module H = Hierarchy
module O = Output
-module CL = CommonLibrary
module B = Brg
(* nodes count **************************************************************)
tabsts: int;
tabbrs: int;
tvoids: int;
- uris : U.uri list;
+ uris : B.uri list;
nodes : int;
xnodes: int
}
| B.Void ->
F.fprintf frm "<Void%a/>" 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@,@,<ABST uri=%S>%a</ABST>"
- (CL.doctype "ABST") str exp_boxed w
+ F.fprintf frm "<ABST uri=%S/>@,%a" str exp_term w
| _, uri, B.Abbr v ->
let str = U.string_of_uri uri in
- F.fprintf frm "%s@,@,<ABBR uri=%S>%a</ABBR>"
- (CL.doctype "ABBR") str exp_boxed v
+ F.fprintf frm "<ABBR uri=%S/>@,%a" str exp_term v
| _, uri, B.Void ->
let str = U.string_of_uri uri in
- F.fprintf frm "%s@,@,<VOID uri=%S/>"
- (CL.doctype "VOID") str
+ F.fprintf frm "<VOID uri=%S/>" str
+
+let export_obj frm obj =
+ F.fprintf frm "@,@[<v3> %a@]@," exp_obj obj
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
-common commonLibrary
+hierarchy output item library
+++ /dev/null
-(*
- ||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
+++ /dev/null
-(*
- ||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 "<?xml version=%S encoding=%S?>" "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 "<!DOCTYPE %s SYSTEM %S>" 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 "@[<v>%s@,@,%a@]@." xml_head export_obj obj;
- close_out och
- | None -> ()
+++ /dev/null
-(*
- ||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
--- /dev/null
+(*
+ ||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")
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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 "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
+
+let pp_doctype frm =
+ Format.fprintf frm "<!DOCTYPE KERNEL SYSTEM %S>@,@," system
+
+let open_kernel si g frm =
+ let opts = if si then "si" else "" in
+ let f shp =
+ Format.fprintf frm "<KERNEL hierarchy=%S options=%S>" shp opts
+ in
+ H.string_of_graph f g
+
+let close_kernel frm =
+ Format.fprintf frm "</KERNEL>"
+
+(* 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 "@[<v>%t%t%t%a%t@]@."
+ pp_head pp_doctype (open_kernel si g) export_obj obj close_kernel;
+ close_out och
+ | None -> ()
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
-nUri cps share log time hierarchy output
+nUri cps share log time
+++ /dev/null
-(*
- ||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")
+++ /dev/null
-(*
- ||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
+++ /dev/null
-(*
- ||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
+++ /dev/null
-(*
- ||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
module MA = MetaAut
module MO = MetaOutput
module MBrg = MetaBrg
-module CL = CommonLibrary
+module G = Library
module BrgO = BrgOutput
module BrgR = BrgReduction
module BrgU = BrgUntrusted
| 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 =
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
projects / helm.git / commitdiff