From c8011c7ad75be5d03c4d4bb2e6900af32ad65c07 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 15 Aug 2009 10:43:46 +0000 Subject: [PATCH] - kernel parameters indication added to exported objects (xml) - some refactoring --- helm/software/lambda-delta/.depend.opt | 100 +++++++++--------- helm/software/lambda-delta/Makefile | 8 +- helm/software/lambda-delta/basic_ag/bag.ml | 8 +- helm/software/lambda-delta/basic_rg/brg.ml | 8 +- .../lambda-delta/basic_rg/brgOutput.ml | 17 ++- .../lambda-delta/basic_rg/brgOutput.mli | 2 +- helm/software/lambda-delta/common/Make | 2 +- .../lambda-delta/{lib => common}/hierarchy.ml | 0 .../{lib => common}/hierarchy.mli | 0 .../common/{common.ml => item.ml} | 0 .../common/{commonLibrary.ml => library.ml} | 32 ++++-- .../common/{commonLibrary.mli => library.mli} | 6 +- .../lambda-delta/{lib => common}/output.ml | 0 .../lambda-delta/{lib => common}/output.mli | 0 helm/software/lambda-delta/lib/Make | 2 +- helm/software/lambda-delta/toplevel/top.ml | 8 +- 16 files changed, 98 insertions(+), 95 deletions(-) rename helm/software/lambda-delta/{lib => common}/hierarchy.ml (100%) rename helm/software/lambda-delta/{lib => common}/hierarchy.mli (100%) rename helm/software/lambda-delta/common/{common.ml => item.ml} (100%) rename helm/software/lambda-delta/common/{commonLibrary.ml => library.ml} (66%) rename helm/software/lambda-delta/common/{commonLibrary.mli => library.mli} (84%) rename helm/software/lambda-delta/{lib => common}/output.ml (100%) rename helm/software/lambda-delta/{lib => common}/output.mli (100%) 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/lib/hierarchy.ml b/helm/software/lambda-delta/common/hierarchy.ml similarity index 100% rename from helm/software/lambda-delta/lib/hierarchy.ml rename to helm/software/lambda-delta/common/hierarchy.ml diff --git a/helm/software/lambda-delta/lib/hierarchy.mli b/helm/software/lambda-delta/common/hierarchy.mli similarity index 100% rename from helm/software/lambda-delta/lib/hierarchy.mli rename to helm/software/lambda-delta/common/hierarchy.mli diff --git a/helm/software/lambda-delta/common/common.ml b/helm/software/lambda-delta/common/item.ml similarity index 100% rename from helm/software/lambda-delta/common/common.ml rename to helm/software/lambda-delta/common/item.ml diff --git a/helm/software/lambda-delta/common/commonLibrary.ml b/helm/software/lambda-delta/common/library.ml similarity index 66% rename from helm/software/lambda-delta/common/commonLibrary.ml rename to helm/software/lambda-delta/common/library.ml index d19f491ae..80e9c59da 100644 --- a/helm/software/lambda-delta/common/commonLibrary.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -11,27 +11,36 @@ module F = Filename module U = NUri -module P = Printf -module C = Common +module H = Hierarchy (* 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 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) -(* interface functions ******************************************************) +let pp_head frm = + Format.fprintf frm "@,@," "1.0" "UTF-8" + +let pp_doctype frm = + Format.fprintf frm "@,@," system -let doctype s = - P.sprintf "" s 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 base = function +let export_item export_obj si g base = function | Some obj -> let _, uri, bind = obj in let path = path_of_uri base uri in @@ -39,6 +48,7 @@ let export_item export_obj base = function 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; + 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/commonLibrary.mli b/helm/software/lambda-delta/common/library.mli similarity index 84% rename from helm/software/lambda-delta/common/commonLibrary.mli rename to helm/software/lambda-delta/common/library.mli index 9cf3c9f40..3c89ab317 100644 --- a/helm/software/lambda-delta/common/commonLibrary.mli +++ b/helm/software/lambda-delta/common/library.mli @@ -10,7 +10,5 @@ V_______________________________________________________________ *) val export_item: - (Format.formatter -> 'bind Common.obj -> unit) -> - string -> 'bind Common.item -> unit - -val doctype: string -> string + (Format.formatter -> 'bind Item.obj -> unit) -> + bool -> Hierarchy.graph -> string -> 'bind Item.item -> unit diff --git a/helm/software/lambda-delta/lib/output.ml b/helm/software/lambda-delta/common/output.ml similarity index 100% rename from helm/software/lambda-delta/lib/output.ml rename to helm/software/lambda-delta/common/output.ml diff --git a/helm/software/lambda-delta/lib/output.mli b/helm/software/lambda-delta/common/output.mli similarity index 100% rename from helm/software/lambda-delta/lib/output.mli rename to helm/software/lambda-delta/common/output.mli 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/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 -- 2.39.2