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 \
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 \
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 \
module M = meta
module MO = metaOutput
-module ML = metaLibrary
module MA = metaAut
module MZ = metaBag
module MB = metaBrg
-meta metaOutput metaLibrary metaAut metaBag metaBrg top
+meta metaOutput metaAut metaBag metaBrg top
+++ /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 = 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 ()
+++ /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 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
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 ()
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
module AD = CrgAut
module MA = MetaAut
module MO = MetaOutput
-module ML = MetaLibrary
module MB = MetaBrg
module BD = BrgCrg
module BO = BrgOutput
| 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 =
(****************************************************************************)
let stage = ref 3
-let moch = ref None
-let meta = ref false
let progress = ref false
let preprocess = ref false
let root = ref ""
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 =
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
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
end
in
let exit () =
- close !moch;
if !L.level > 0 then Y.utime_stamp "at exit";
flush_all ()
in
let help_i = " show local references by index" in
let help_j = " show URI of processed kernel objects" in
let help_k = "<string> 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
("-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);
projects / helm.git / commitdiff