X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;h=0000000000000000000000000000000000000000;hb=95872555aaa040a22ad2d93cb1278f79e20da70c;hp=d0476f78ac85e9d2cf7144a0112dfe932ec5ff17;hpb=4025c3f5b36025380dcad84bb7a97045d08652f6;p=helm.git diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml deleted file mode 100644 index d0476f78a..000000000 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ /dev/null @@ -1,360 +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 P = Printf -module U = NUri -module C = Cps -module L = Log -module Y = Time -module G = Options -module H = Hierarchy -module O = Output -module E = Entity -module S = Status -module DO = CrgOutput -module TD = TxtCrg -module AA = AutProcess -module AO = AutOutput -module AD = AutCrg -module XL = XmlLibrary -module XD = XmlCrg -module BD = BrgCrg -module BO = BrgOutput -module BR = BrgReduction -module BU = BrgUntrusted -module ZD = BagCrg -module ZO = BagOutput -module ZT = BagType -module ZU = BagUntrusted - -type status = { - kst: S.status; - tst: TD.status; - pst: AA.status; - ast: AD.status; - ac : AO.counters; - dc : DO.counters; - bc : BO.counters; - zc : ZO.counters; -} - -let flush_all () = L.flush 0; L.flush_err () - -let bag_error s msg = - L.error ZO.specs (L.Warn s :: L.Loc :: msg); flush_all () - -let brg_error s msg = - L.error BR.specs (L.Warn s :: L.Loc :: msg); flush_all () - -let initial_status () = { - kst = S.initial_status (); - tst = TD.initial_status (); - pst = AA.initial_status (); - ast = AD.initial_status (); - ac = AO.initial_counters; - dc = DO.initial_counters; - bc = BO.initial_counters; - zc = ZO.initial_counters; -} - -let refresh_status st = {st with - kst = S.refresh_status st.kst; - tst = TD.refresh_status st.tst; - ast = AD.refresh_status st.ast; -} - -(* kernel related ***********************************************************) - -type kernel_entity = BrgEntity of Brg.entity - | BagEntity of Bag.entity - | CrgEntity of Crg.entity - -let print_counters st = function - | G.Crg -> DO.print_counters C.start st.dc - | G.Brg -> BO.print_counters C.start st.bc - | G.Bag -> ZO.print_counters C.start st.zc - -let xlate_entity entity = match !G.kernel, entity with - | G.Brg, CrgEntity e -> - let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e - | G.Bag, CrgEntity e -> - let f e = (BagEntity e) in E.xlate f ZD.bag_of_crg e - | _, entity -> entity - -let pp_progress e = - let f a u = - let s = U.string_of_uri u in - let err () = L.warn (P.sprintf "%s" s) in - let f i = L.warn (P.sprintf "[%u] %s" i s) in - E.mark err f a - in - match e with - | CrgEntity e -> E.common f e - | BrgEntity e -> E.common f e - | BagEntity e -> E.common f e - -let count_entity st = function - | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e} - | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e} - | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e} - -let export_entity = function - | CrgEntity e -> XL.export_entity XD.export_term e - | BrgEntity e -> XL.export_entity BO.export_term e - | BagEntity e -> XL.export_entity ZO.export_term e - -let type_check st k = - let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in - let ok _ _ = st in - match k with - | BrgEntity entity -> BU.type_check brg_err ok st.kst entity - | BagEntity entity -> ZU.type_check ok st.kst entity - | CrgEntity _ -> st - -(* extended lexer ***********************************************************) - -type 'token lexer = { - parse : Lexing.lexbuf -> 'token; - mutable tokbuf: 'token option; - mutable unget : bool -} - -let initial_lexer parse = { - parse = parse; tokbuf = None; unget = false -} - -let token xl lexbuf = match xl.tokbuf with - | Some token when xl.unget -> - xl.unget <- false; token - | _ -> - let token = xl.parse lexbuf in - xl.tokbuf <- Some token; token - -(* input related ************************************************************) - -type input = Text | Automath - -type input_entity = TxtEntity of Txt.command - | AutEntity of Aut.command - | NoEntity - -let type_of_input name = - if F.check_suffix name ".hln" then Text - else if F.check_suffix name ".aut" then - let _ = H.set_sorts 0 ["Set"; "Prop"] in - assert (H.set_graph "Z2"); - Automath - else begin - L.warn (P.sprintf "Unknown file type: %s" name); exit 2 - end - -let txt_xl = initial_lexer TxtLexer.token - -let aut_xl = initial_lexer AutLexer.token - -let parbuf = ref [] (* parser buffer *) - -let gen_text command = - parbuf := TxtEntity command :: !parbuf - -let entity_of_input lexbuf i = match i, !parbuf with - | Automath, _ -> - begin match AutParser.entry (token aut_xl) lexbuf with - | Some e -> aut_xl.unget <- true; AutEntity e - | None -> NoEntity - end - | Text, [] -> - begin match TxtParser.entry (token txt_xl) lexbuf with - | Some e -> txt_xl.unget <- true; TxtEntity e - | None -> NoEntity - end - | Text, hd :: tl -> - parbuf := tl; hd - -let process_input f st = function - | AutEntity e -> - let f pst e = f {st with pst = pst} (AutEntity e) in - AA.process_command f st.pst e - | xe -> f st xe - -let count_input st = function - | AutEntity e -> {st with ac = AO.count_command C.start st.ac e} - | xe -> st - -(****************************************************************************) - -let stage = ref 3 -let progress = ref false -let preprocess = ref false -let root = ref "" -let export = ref false -let st = ref (initial_status ()) -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 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 entity; - if !stage > 1 then process_2 st (xlate_entity entity) else st - -let process_0 st entity = - let f st entity = - if !stage = 0 then st else - match entity with - | AutEntity e -> - let err ast = {st with ast = ast} in - let g ast e = process_1 {st with ast = ast} (CrgEntity e) in - AD.crg_of_aut err g st.ast e - | TxtEntity e -> - let crr tst = {st with tst = tst} in - let d tst e = process_1 {st with tst = tst} (CrgEntity e) in - TD.crg_of_txt crr d gen_text st.tst e - | NoEntity -> assert false - in - let st = if !L.level > 2 then count_input st entity else st in - if !preprocess then process_input f st entity else f st entity - -let process_nostreaming st lexbuf input = - let id x = x in - let rec aux1 book = match entity_of_input lexbuf input with - | NoEntity -> List.rev book - | e -> aux1 (id e :: book) - in - let rec aux2 st = function - | [] -> st - | entity :: tl -> aux2 (process_0 st entity) tl - in - aux2 st (aux1 []) - -let process_streaming st lexbuf input = - let rec aux st = match entity_of_input lexbuf input with - | NoEntity -> st - | e -> aux (process_0 st e) - in - aux st - -(****************************************************************************) - -let process st name = - let process = if !streaming then process_streaming else process_nostreaming in - let input = type_of_input name in - let ich = open_in name in - let lexbuf = Lexing.from_channel ich in - let st = process st lexbuf input in - close_in ich; - if !stage > 2 && !G.cc && !G.si then XL.export_csys st.kst.S.cc; - st, input - -let main = -try - let version_string = "Helena 0.8.2 M - January 2011" in - let print_version () = L.warn (version_string ^ "\n"); exit 0 in - let set_hierarchy s = - if H.set_graph s then () else - L.warn (P.sprintf "Unknown type hierarchy: %s" s) - in - let set_kernel = function - | "brg" -> G.kernel := G.Brg - | "bag" -> G.kernel := G.Bag - | s -> L.warn (P.sprintf "Unknown kernel version: %s" s) - in - let set_summary i = L.level := i in - let set_stage i = stage := i in - let set_xdir s = G.xdir := s in - let set_root s = root := s in - let clear_options () = - progress := false; export := false; preprocess := false; - stage := 3; root := ""; - st := initial_status (); - L.clear (); G.clear (); H.clear (); O.clear_reductions (); - streaming := false; - in - let process_file name = - if !L.level > 0 then Y.gmtime version_string; - if !L.level > 1 then - 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 - let cover = F.concat !root base_name in - if !stage < 2 then G.kernel := G.Crg; - G.cover := cover; - let sst, input = process (refresh_status !st) name in - st := sst; - if !L.level > 0 then Y.utime_stamp "processed"; - if !L.level > 2 then begin - AO.print_counters C.start !st.ac; - if !preprocess then AO.print_process_counters C.start !st.pst; - if !stage > 0 then print_counters !st G.Crg; - if !stage > 1 then print_counters !st !G.kernel; - if !stage > 2 then O.print_reductions () - end - in - let exit () = - if !L.level > 0 then Y.utime_stamp "at exit"; - flush_all () - in - let help = - "Usage: helena [ -LPVXcgijopqx1 | -Ss | -O | -hkr ]* [ ]*\n\n" ^ - "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \ - 3 data information, 4 typing information, 5 reduction information\n\n" ^ - "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" - in - let help_L = " show lexer debug information" in - let help_O = " set location of output directory (XML) to (default: current directory)" in - let help_P = " show parser debug information" in - let help_S = " set summary level (see above)" in - let help_V = " show version information" in - let help_X = " clear options" in - - let help_c = " read/write conversion constraints" in - let help_g = " always expand global definitions" in - let help_h = " set type hierarchy (default: \"Z1\")" in - 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_o = " activate sort inclusion" in - let help_p = " preprocess source" in - let help_q = " disable quotation of identifiers" in - let help_r = " set initial segment of URI hierarchy (default: empty)" in - let help_s = " set translation stage (see above)" in - let help_x = " export kernel entities (XML)" in - - let help_1 = " parse files with streaming policy" in - L.box 0; L.box_err (); - at_exit exit; - Arg.parse [ - ("-L", Arg.Set G.debug_lexer, help_L); - ("-O", Arg.String set_xdir, help_O); - ("-P", Arg.Set G.debug_parser, help_P); - ("-S", Arg.Int set_summary, help_S); - ("-V", Arg.Unit print_version, help_V); - ("-X", Arg.Unit clear_options, help_X); - ("-c", Arg.Set G.cc, help_c); - ("-g", Arg.Set G.expand, help_g); - ("-h", Arg.String set_hierarchy, help_h); - ("-i", Arg.Set G.indexes, help_i); - ("-j", Arg.Set progress, help_j); - ("-k", Arg.String set_kernel, help_k); - ("-o", Arg.Set G.si, help_o); - ("-p", Arg.Set preprocess, help_p); - ("-q", Arg.Set G.unquote, help_q); - ("-r", Arg.String set_root, help_r); - ("-s", Arg.Int set_stage, help_s); - ("-x", Arg.Set export, help_x); - ("-1", Arg.Set streaming, help_1); - ] process_file help; -with ZT.TypeError msg -> bag_error "Type Error" msg