From 673c78501a9e71ac5f897d2ba78f3591de8db876 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 6 Aug 2010 19:24:59 +0000 Subject: [PATCH] we removed old HAL exportation (replaced by XML exportation) --- helm/software/lambda-delta/.depend.opt | 33 +++++------- helm/software/lambda-delta/src/modules.ml | 1 - helm/software/lambda-delta/src/toplevel/Make | 2 +- .../lambda-delta/src/toplevel/metaLibrary.ml | 36 ------------- .../lambda-delta/src/toplevel/metaLibrary.mli | 18 ------- .../lambda-delta/src/toplevel/metaOutput.ml | 54 ------------------- .../lambda-delta/src/toplevel/metaOutput.mli | 2 - .../software/lambda-delta/src/toplevel/top.ml | 31 +++-------- 8 files changed, 21 insertions(+), 156 deletions(-) delete mode 100644 helm/software/lambda-delta/src/toplevel/metaLibrary.ml delete mode 100644 helm/software/lambda-delta/src/toplevel/metaLibrary.mli diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index dcd6c9354..0c298824f 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -206,11 +206,6 @@ src/toplevel/metaOutput.cmo: src/toplevel/meta.cmx src/lib/log.cmi \ src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi src/toplevel/metaOutput.cmx: src/toplevel/meta.cmx src/lib/log.cmx \ src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi -src/toplevel/metaLibrary.cmi: src/toplevel/meta.cmx -src/toplevel/metaLibrary.cmo: src/toplevel/metaOutput.cmi \ - src/toplevel/metaLibrary.cmi -src/toplevel/metaLibrary.cmx: src/toplevel/metaOutput.cmx \ - src/toplevel/metaLibrary.cmi src/toplevel/metaAut.cmi: src/toplevel/meta.cmx src/automath/aut.cmx src/toplevel/metaAut.cmo: src/common/options.cmx src/toplevel/meta.cmx \ src/common/entity.cmx src/lib/cps.cmx src/automath/aut.cmx \ @@ -231,13 +226,13 @@ src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/entity.cmx \ src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txt.cmx \ src/lib/time.cmx src/common/output.cmi src/common/options.cmx \ - src/toplevel/metaOutput.cmi src/toplevel/metaLibrary.cmi \ - src/toplevel/metaBrg.cmi src/toplevel/metaBag.cmi \ - src/toplevel/metaAut.cmi src/toplevel/meta.cmx src/lib/log.cmi \ - src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crgTxt.cmi \ - src/complete_rg/crgAut.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \ - src/basic_rg/brgOutput.cmi src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ + src/toplevel/metaOutput.cmi src/toplevel/metaBrg.cmi \ + src/toplevel/metaBag.cmi src/toplevel/metaAut.cmi src/toplevel/meta.cmx \ + src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \ + src/complete_rg/crgTxt.cmi src/complete_rg/crgAut.cmi \ + src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmi \ + src/basic_rg/brgReduction.cmi src/basic_rg/brgOutput.cmi \ + src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \ src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \ src/automath/autProcess.cmi src/automath/autParser.cmi \ @@ -245,13 +240,13 @@ src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ src/toplevel/top.cmx: src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \ src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txt.cmx \ src/lib/time.cmx src/common/output.cmx src/common/options.cmx \ - src/toplevel/metaOutput.cmx src/toplevel/metaLibrary.cmx \ - src/toplevel/metaBrg.cmx src/toplevel/metaBag.cmx \ - src/toplevel/metaAut.cmx src/toplevel/meta.cmx src/lib/log.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crgTxt.cmx \ - src/complete_rg/crgAut.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \ - src/basic_rg/brgOutput.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ + src/toplevel/metaOutput.cmx src/toplevel/metaBrg.cmx \ + src/toplevel/metaBag.cmx src/toplevel/metaAut.cmx src/toplevel/meta.cmx \ + src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \ + src/complete_rg/crgTxt.cmx src/complete_rg/crgAut.cmx \ + src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmx \ + src/basic_rg/brgReduction.cmx src/basic_rg/brgOutput.cmx \ + src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \ src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \ src/automath/autProcess.cmx src/automath/autParser.cmx \ diff --git a/helm/software/lambda-delta/src/modules.ml b/helm/software/lambda-delta/src/modules.ml index f48cf6ffc..7fad8b893 100644 --- a/helm/software/lambda-delta/src/modules.ml +++ b/helm/software/lambda-delta/src/modules.ml @@ -53,7 +53,6 @@ module BU = brgUntrusted module M = meta module MO = metaOutput -module ML = metaLibrary module MA = metaAut module MZ = metaBag module MB = metaBrg diff --git a/helm/software/lambda-delta/src/toplevel/Make b/helm/software/lambda-delta/src/toplevel/Make index a8a72e17f..c32bec6c7 100644 --- a/helm/software/lambda-delta/src/toplevel/Make +++ b/helm/software/lambda-delta/src/toplevel/Make @@ -1 +1 @@ -meta metaOutput metaLibrary metaAut metaBag metaBrg top +meta metaOutput metaAut metaBag metaBrg top diff --git a/helm/software/lambda-delta/src/toplevel/metaLibrary.ml b/helm/software/lambda-delta/src/toplevel/metaLibrary.ml deleted file mode 100644 index ca0fd9792..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaLibrary.ml +++ /dev/null @@ -1,36 +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 = Format -module MO = MetaOutput - -type out_channel = Pervasives.out_channel * F.formatter - -(* internal functions *******************************************************) - -let hal_dir = "hal" - -let hal_ext = ".hal" - -(* interface functions ******************************************************) - -let open_out f name = - let _ = Sys.command (Printf.sprintf "mkdir -p %s" hal_dir) in - let och = open_out (Filename.concat hal_dir (name ^ hal_ext)) in - let frm = F.formatter_of_out_channel och in - F.pp_set_margin frm max_int; - f (och, frm) - -let write_entity f (_, frm) entity = - MO.pp_entity f frm entity - -let close_out f (och, _) = - close_out och; f () diff --git a/helm/software/lambda-delta/src/toplevel/metaLibrary.mli b/helm/software/lambda-delta/src/toplevel/metaLibrary.mli deleted file mode 100644 index 2f6e41b80..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaLibrary.mli +++ /dev/null @@ -1,18 +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 out_channel - -val open_out: (out_channel -> 'a) -> string -> 'a - -val write_entity: (unit -> 'a) -> out_channel -> Meta.entity -> 'a - -val close_out: (unit -> 'a) -> out_channel -> 'a diff --git a/helm/software/lambda-delta/src/toplevel/metaOutput.ml b/helm/software/lambda-delta/src/toplevel/metaOutput.ml index 859857ebe..2d9246f5d 100644 --- a/helm/software/lambda-delta/src/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/src/toplevel/metaOutput.ml @@ -106,57 +106,3 @@ let print_counters f c = L.warn (P.sprintf " Global Int. Complexity: %7u" c.nodes); L.warn (P.sprintf " + Abbreviation nodes: %7u" nodes); f () - -let string_of_sort = function - | true -> "Type" - | false -> "Prop" - -let pp_transparent frm a = - let err () = F.fprintf frm "%s" "=" in - let f () = F.fprintf frm "%s" "~" in - E.priv err f a - -let pp_list pp opend sep closed frm l = - let rec aux frm = function - | [] -> () - | [hd] -> pp frm hd - | hd :: tl -> F.fprintf frm "%a%s%a" pp hd sep aux tl - in - if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed - -let pp_rev_list pp opend sep closed frm l = - pp_list pp opend sep closed frm (List.rev l) - -let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args - -and pp_term frm = function - | M.Sort s -> - F.fprintf frm "@[*%s@]" (string_of_sort s) - | M.LRef (l, i) -> - F.fprintf frm "@[%u@@#%u@]" l i - | M.GRef (l, uri, ts) -> - F.fprintf frm "@[%u@@$%s%a@]" l (U.string_of_uri uri) pp_args ts - | M.Appl (v, t) -> - F.fprintf frm "@[(%a).%a@]" pp_term v pp_term t - | M.Abst (id, w, t) -> - F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t - -let pp_par frm (id, w) = - F.fprintf frm "%s:%a" id pp_term w - -let pp_pars = pp_rev_list pp_par "[" "," "]" - -let pp_body a frm = function - | None -> () - | Some t -> F.fprintf frm "%a%a" pp_transparent a pp_term t - -let pp_entity frm = function - | a, uri, E.Abst (pars, u, body) - | a, uri, E.Abbr (pars, u, body) -> - F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" - (E.mark C.err C.start a) (U.string_of_uri uri) - pp_pars pars (pp_body a) body pp_term u - | _, _, E.Void -> assert false - -let pp_entity f frm entity = - pp_entity frm entity; f () diff --git a/helm/software/lambda-delta/src/toplevel/metaOutput.mli b/helm/software/lambda-delta/src/toplevel/metaOutput.mli index 1a7b119ce..26b873cf9 100644 --- a/helm/software/lambda-delta/src/toplevel/metaOutput.mli +++ b/helm/software/lambda-delta/src/toplevel/metaOutput.mli @@ -16,5 +16,3 @@ val initial_counters: counters val count_entity: (counters -> 'a) -> counters -> Meta.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a - -val pp_entity: (unit -> 'a) -> Format.formatter -> Meta.entity -> 'a diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index f69c4b8df..be3059ea2 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -27,7 +27,6 @@ module TD = CrgTxt module AD = CrgAut module MA = MetaAut module MO = MetaOutput -module ML = MetaLibrary module MB = MetaBrg module BD = BrgCrg module BO = BrgOutput @@ -120,14 +119,10 @@ let count_entity st = function | BagEntity e -> {st with bagc = ZO.count_entity C.start st.bagc e} | _ -> st -let export_entity si xdir moch = function +let export_entity si xdir = function | CrgEntity e -> XL.export_entity XD.export_term si xdir e | BrgEntity e -> XL.export_entity BO.export_term si xdir e - | MetaEntity e -> - begin match moch with - | None -> () - | Some och -> ML.write_entity C.start och e - end + | MetaEntity _ | BagEntity _ -> () let type_check st k = @@ -212,8 +207,6 @@ let count_input st = function (****************************************************************************) let stage = ref 3 -let moch = ref None -let meta = ref false let progress = ref false let preprocess = ref false let root = ref "" @@ -225,13 +218,13 @@ let streaming = ref false (* parsing style (temporary) *) let process_2 st entity = let st = if !L.level > 2 then count_entity st entity else st in - if !export <> "" then export_entity !G.si !export !moch entity; + if !export <> "" then export_entity !G.si !export entity; if !stage > 2 then type_check st entity else st let process_1 st entity = if !progress then pp_progress entity; let st = if !L.level > 2 then count_entity st entity else st in - if !export <> "" && !stage = 1 then export_entity !G.si !export !moch entity; + if !export <> "" && !stage = 1 then export_entity !G.si !export entity; if !stage > 1 then process_2 st (xlate_entity entity) else st let process_0 st entity = @@ -295,20 +288,12 @@ try in let set_summary i = L.level := i in let set_stage i = stage := i in - let set_meta_file name = - let f och = moch := Some och in - ML.open_out f name - in let set_xdir s = export := s in let set_root s = root := s in - let close = function - | None -> () - | Some och -> ML.close_out C.start och - in let clear_options () = - stage := 3; moch := None; meta := false; progress := false; + stage := 3; progress := false; old := false; preprocess := false; root := ""; cc := false; export := ""; - old := false; kernel := Brg; st := initial_status (); + kernel := Brg; st := initial_status (); L.clear (); G.clear (); H.clear (); O.clear_reductions (); streaming := false; in @@ -318,7 +303,6 @@ try L.warn (P.sprintf "Processing file: %s" name); if !L.level > 0 then Y.utime_stamp "started"; let base_name = Filename.chop_extension (Filename.basename name) in - if !meta then set_meta_file base_name; let mk_uri = if !stage < 2 then Crg.mk_uri else match !kernel with @@ -339,7 +323,6 @@ try end in let exit () = - close !moch; if !L.level > 0 then Y.utime_stamp "at exit"; flush_all () in @@ -361,7 +344,6 @@ try let help_i = " show local references by index" in let help_j = " show URI of processed kernel objects" in let help_k = " set kernel version (default: brg)" in - let help_m = " output intermediate representation (HAL)" in let help_o = " use old abstract language instead of crg" in let help_p = " preprocess source" in let help_q = " disable quotation of identifiers" in @@ -385,7 +367,6 @@ try ("-i", Arg.Set G.indexes, help_i); ("-j", Arg.Set progress, help_j); ("-k", Arg.String set_kernel, help_k); - ("-m", Arg.Set meta, help_m); ("-o", Arg.Set old, help_o); ("-p", Arg.Set preprocess, help_p); ("-q", Arg.Set G.unquote, help_q); -- 2.39.2