X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;fp=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;h=0000000000000000000000000000000000000000;hb=f12f1b61a608140a65990d36045d978575b2dcb0;hp=40fcda5e1db4a2772c343361b297eeee7d6dc3d9;hpb=2b1375e4b44e2ef351a6341a5bb0a4823e8daae5;p=helm.git diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml deleted file mode 100644 index 40fcda5e1..000000000 --- a/helm/software/lambda-delta/toplevel/top.ml +++ /dev/null @@ -1,399 +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 T = Time -module O = Options -module H = Hierarchy -module Op = Output -module Y = Entity -module X = Library -module AL = AutLexer -module AP = AutProcess -module AO = AutOutput -module DT = CrgTxt -module DA = CrgAut -module MA = MetaAut -module MO = MetaOutput -module ML = MetaLibrary -module DX = CrgXml -module DBrg = CrgBrg -module MBrg = MetaBrg -module BrgO = BrgOutput -module BrgR = BrgReduction -module BrgU = BrgUntrusted -module MBag = MetaBag -module BagO = BagOutput -module BagT = BagType -module BagU = BagUntrusted - -type status = { - ast : AP.status; - dst : DA.status; - mst : MA.status; - tst : DT.status; - ac : AO.counters; - mc : MO.counters; - brgc: BrgO.counters; - bagc: BagO.counters; - kst : Y.status -} - -let flush_all () = L.flush 0; L.flush_err () - -let bag_error s msg = - L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush_all () - -let brg_error s msg = - L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all () - -let initial_status () = { - ac = AO.initial_counters; - mc = MO.initial_counters; - brgc = BrgO.initial_counters; - bagc = BagO.initial_counters; - mst = MA.initial_status (); - dst = DA.initial_status (); - tst = DT.initial_status (); - ast = AP.initial_status (); - kst = Y.initial_status () -} - -let refresh_status st = {st with - mst = MA.refresh_status st.mst; - dst = DA.refresh_status st.dst; - tst = DT.refresh_status st.tst; - kst = Y.refresh_status st.kst -} - -(* kernel related ***********************************************************) - -type kernel = Brg | Bag - -type kernel_entity = BrgEntity of Brg.entity - | BagEntity of Bag.entity - | CrgEntity of Crg.entity - | MetaEntity of Meta.entity - -let kernel = ref Brg - -let print_counters st = match !kernel with - | Brg -> BrgO.print_counters C.start st.brgc - | Bag -> BagO.print_counters C.start st.bagc - -let xlate_entity entity = match !kernel, entity with - | Brg, CrgEntity e -> - let f e = (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e - | Brg, MetaEntity e -> - let f e = (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e - | Bag, MetaEntity e -> - let f e = (BagEntity e) in Y.xlate f MBag.bag_of_meta 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 - Y.mark err f a - in - match e with - | CrgEntity e -> Y.common f e - | BrgEntity e -> Y.common f e - | BagEntity e -> Y.common f e - | MetaEntity e -> Y.common f e - -let count_entity st = function - | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e} - | BrgEntity e -> {st with brgc = BrgO.count_entity C.start st.brgc e} - | BagEntity e -> {st with bagc = BagO.count_entity C.start st.bagc e} - | _ -> st - -let export_entity si xdir moch = function - | CrgEntity e -> X.export_entity DX.export_term si xdir e - | BrgEntity e -> X.export_entity BrgO.export_term si xdir e - | MetaEntity e -> - begin match moch with - | None -> () - | Some och -> ML.write_entity C.start och e - end - | BagEntity _ -> () - -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 -> BrgU.type_check brg_err ok st.kst entity - | BagEntity entity -> BagU.type_check ok st.kst entity - | CrgEntity _ - | MetaEntity _ -> 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 ast e = f {st with ast = ast} (AutEntity e) in - AP.process_command f st.ast 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 moch = ref None -let meta = ref false -let progress = ref false -let preprocess = ref false -let root = ref "" -let cc = ref false -let export = ref "" -let old = 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 !O.si !export !moch 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 !O.si !export !moch 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, !old with - | AutEntity e, true -> - let frr mst = {st with mst = mst} in - let h mst e = process_1 {st with mst = mst} (MetaEntity e) in - MA.meta_of_aut frr h st.mst e - | AutEntity e, false -> - let err dst = {st with dst = dst} in - let g dst e = process_1 {st with dst = dst} (CrgEntity e) in - DA.crg_of_aut err g st.dst e - | TxtEntity e, _ -> - let crr tst = {st with tst = tst} in - let d tst e = process_1 {st with tst = tst} (CrgEntity e) in - DT.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 rec aux1 book = match entity_of_input lexbuf input with - | NoEntity -> List.rev book - | e -> aux1 (e :: book) - in - let rec aux2 st = function - | [] -> st - | entity :: tl -> aux2 (process_0 st entity) tl - in - aux2 st (aux1 []) - -let rec process_streaming st lexbuf input = match entity_of_input lexbuf input with - | NoEntity -> st - | e -> process_streaming (process_0 st e) lexbuf input - -(****************************************************************************) - -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; st, input - -let main = -try - let version_string = "Helena 0.8.1 M - August 2010" 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" -> kernel := Brg - | "bag" -> kernel := 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_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; - preprocess := false; root := ""; cc := false; export := ""; - old := false; kernel := Brg; st := initial_status (); - L.clear (); O.clear (); H.clear (); Op.clear_reductions (); - streaming := false; - in - let process_file name = - if !L.level > 0 then T.gmtime version_string; - if !L.level > 1 then - L.warn (P.sprintf "Processing file: %s" name); - if !L.level > 0 then T.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 - | Brg -> Brg.mk_uri - | Bag -> Bag.mk_uri - in - let cover = F.concat !root base_name in - O.mk_uri := mk_uri; O.cover := cover; - let sst, input = process (refresh_status !st) name in - st := sst; - if !L.level > 0 then T.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.ast; - if !stage > 0 then MO.print_counters C.start !st.mc; - if !stage > 1 then print_counters !st; - if !stage > 2 then Op.print_reductions () - end - in - let exit () = - close !moch; - if !L.level > 0 then T.utime_stamp "at exit"; - flush_all () - in - let help = - "Usage: helena [ -LPVXcgijmopqu1 | -Ss | -x | -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_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 = " output 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_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 - let help_r = " set initial segment of URI hierarchy" in - let help_s = " set translation stage (see above)" in - let help_u = " activate sort inclusion" in - let help_x = " export kernel entities (XML) to " in - - let help_1 = " parse files with streaming policy" in - L.box 0; L.box_err (); - at_exit exit; - Arg.parse [ - ("-L", Arg.Set O.debug_lexer, help_L); - ("-P", Arg.Set O.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 cc, help_c); - ("-g", Arg.Set O.expand, help_g); - ("-h", Arg.String set_hierarchy, help_h); - ("-i", Arg.Set O.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 O.unquote, help_q); - ("-r", Arg.String set_root, help_r); - ("-s", Arg.Int set_stage, help_s); - ("-u", Arg.Set O.si, help_u); - ("-x", Arg.String set_xdir, help_x); - ("-1", Arg.Set streaming, help_1); - ] process_file help; -with BagT.TypeError msg -> bag_error "Type Error" msg