X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;h=579f5e6585211f665c3119548ebca5a44d79d10b;hb=e7f64fe2cc67f3514131c8831f87311ff600d005;hp=d45bcf98e41241b6deecc909da53d902f290494f;hpb=bb2a0b22a2c38b59ca664b550f34e5e40e6f04c7;p=helm.git diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index d45bcf98e..579f5e658 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -9,97 +9,97 @@ \ / 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 XL = XmlLibrary -module XCrg = XmlCrg -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 MBrg = MetaBrg -module BrgC = BrgCrg -module BrgO = BrgOutput -module BrgR = BrgReduction -module BrgU = BrgUntrusted -module MBag = MetaBag -module BagO = BagOutput -module BagT = BagType -module BagU = BagUntrusted +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 TD = CrgTxt +module AA = AutProcess +module AO = AutOutput +module AD = CrgAut +module DO = CrgOutput +module XL = XmlLibrary +module XD = XmlCrg +module BD = BrgCrg +module BO = BrgOutput +module BR = BrgReduction +module BU = BrgUntrusted +module ZO = BagOutput +module ZT = BagType +module ZU = BagUntrusted + +module MA = MetaAut +module MO = MetaOutput +module MB = MetaBrg +module MZ = MetaBag 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 + kst: S.status; + tst: TD.status; + pst: AA.status; + ast: AD.status; + ac : AO.counters; + dc : DO.counters; + bc : BO.counters; + zc : ZO.counters; + mst: MA.status; + mc : MO.counters; } 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 () + L.error ZO.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 () + L.error BR.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 () + 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; + mst = MA.initial_status (); + mc = MO.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; 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 BrgC.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 +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.Brg, MetaEntity e -> + let f e = (BrgEntity e) in E.xlate f MB.brg_of_meta e + | G.Bag, MetaEntity e -> + let f e = (BagEntity e) in E.xlate f MZ.bag_of_meta e | _, entity -> entity let pp_progress e = @@ -107,36 +107,32 @@ let pp_progress e = 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 + E.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 + | CrgEntity e -> E.common f e + | BrgEntity e -> E.common f e + | BagEntity e -> E.common f e + | MetaEntity 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} | 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 -> XL.export_entity XCrg.export_term si xdir e - | BrgEntity e -> XL.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 + +let export_entity = function + | CrgEntity e -> XL.export_entity XD.export_term e + | BrgEntity e -> XL.export_entity BO.export_term e + | MetaEntity _ | 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 + | BrgEntity entity -> BU.type_check brg_err ok st.kst entity + | BagEntity entity -> ZU.type_check ok st.kst entity | CrgEntity _ | MetaEntity _ -> st @@ -202,8 +198,8 @@ let entity_of_input lexbuf i = match i, !parbuf with 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 + 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 @@ -213,26 +209,23 @@ 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 "" -let cc = ref false -let export = ref "" +let export = ref false 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 !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 !O.si !export !moch entity; + 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 = @@ -244,22 +237,23 @@ let process_0 st entity = 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 + 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 - DT.crg_of_txt crr d gen_text st.tst e + 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 (e :: book) + | e -> aux1 (id e :: book) in let rec aux2 st = function | [] -> st @@ -267,9 +261,12 @@ let process_nostreaming st lexbuf input = 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_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 (****************************************************************************) @@ -279,121 +276,110 @@ let process st name = 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 + 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.1 M - August 2010" in + let version_string = "Helena 0.8.1 M - October 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 + | "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_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_xdir s = G.xdir := 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 (); + progress := false; old := 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 T.gmtime version_string; + 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 T.utime_stamp "started"; + 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 - | 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; + 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 T.utime_stamp "processed"; + 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.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 () + if !preprocess then AO.print_process_counters C.start !st.pst; + if !stage > 0 then + if !old then MO.print_counters C.start !st.mc + else 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 () = - close !moch; - if !L.level > 0 then T.utime_stamp "at exit"; + if !L.level > 0 then Y.utime_stamp "at exit"; flush_all () in let help = - "Usage: helena [ -LPVXcgijmopqu1 | -Ss | -x | -hkr ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXcgijopqux1 | -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 = " output conversion constraints" 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_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_k = " set kernel version (default: \"brg\")" 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_r = " set initial segment of URI hierarchy (default: empty)" 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_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 O.debug_lexer, help_L); - ("-P", Arg.Set O.debug_parser, help_P); + ("-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 cc, help_c); - ("-g", Arg.Set O.expand, help_g); + ("-c", Arg.Set G.cc, help_c); + ("-g", Arg.Set G.expand, help_g); ("-h", Arg.String set_hierarchy, help_h); - ("-i", Arg.Set O.indexes, help_i); + ("-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 O.unquote, help_q); + ("-q", Arg.Set G.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); + ("-u", Arg.Set G.si, help_u); + ("-x", Arg.Set export, help_x); ("-1", Arg.Set streaming, help_1); ] process_file help; -with BagT.TypeError msg -> bag_error "Type Error" msg +with ZT.TypeError msg -> bag_error "Type Error" msg