X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;h=d0476f78ac85e9d2cf7144a0112dfe932ec5ff17;hb=4025c3f5b36025380dcad84bb7a97045d08652f6;hp=4a1446734153a79cd18e110ac973274a6ae7ad7e;hpb=f7988fc51f7c96617aa2b3320628645480af681a;p=helm.git diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index 4a1446734..d0476f78a 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -20,34 +20,31 @@ module H = Hierarchy module O = Output module E = Entity module S = Status -module XL = XmlLibrary -module XD = XmlCrg +module DO = CrgOutput +module TD = TxtCrg module AA = AutProcess module AO = AutOutput -module TD = CrgTxt -module AD = CrgAut -module MA = MetaAut -module MO = MetaOutput -module MB = MetaBrg +module AD = AutCrg +module XL = XmlLibrary +module XD = XmlCrg module BD = BrgCrg module BO = BrgOutput module BR = BrgReduction module BU = BrgUntrusted -module MZ = MetaBag +module ZD = BagCrg module ZO = BagOutput module ZT = BagType module ZU = BagUntrusted type status = { - ast : AA.status; - dst : AD.status; - mst : MA.status; - tst : TD.status; - ac : AO.counters; - mc : MO.counters; - brgc: BO.counters; - bagc: ZO.counters; - kst : S.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 () @@ -59,44 +56,39 @@ let brg_error s msg = L.error BR.specs (L.Warn s :: L.Loc :: msg); flush_all () let initial_status () = { - ac = AO.initial_counters; - mc = MO.initial_counters; - brgc = BO.initial_counters; - bagc = ZO.initial_counters; - mst = MA.initial_status (); - dst = AD.initial_status (); - tst = TD.initial_status (); - ast = AA.initial_status (); - kst = S.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 - mst = MA.refresh_status st.mst; - dst = AD.refresh_status st.dst; + kst = S.refresh_status st.kst; tst = TD.refresh_status st.tst; - kst = S.refresh_status st.kst + ast = AD.refresh_status st.ast; } (* kernel related ***********************************************************) -type kernel_entity = BrgEntity of Brg.entity - | BagEntity of Bag.entity - | CrgEntity of Crg.entity - | MetaEntity of Meta.entity +type kernel_entity = BrgEntity of Brg.entity + | BagEntity of Bag.entity + | CrgEntity of Crg.entity let print_counters st = function - | G.Brg -> BO.print_counters C.start st.brgc - | G.Bag -> ZO.print_counters C.start st.bagc - | G.Crg -> () + | 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 -> + | 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 + | 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 = @@ -109,19 +101,16 @@ let pp_progress 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 - | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e} - | BrgEntity e -> {st with brgc = BO.count_entity C.start st.brgc e} - | BagEntity e -> {st with bagc = ZO.count_entity C.start st.bagc e} - | _ -> st + | 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 - | MetaEntity _ - | BagEntity _ -> () + | 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 @@ -129,8 +118,7 @@ let type_check st k = match k with | BrgEntity entity -> BU.type_check brg_err ok st.kst entity | BagEntity entity -> ZU.type_check ok st.kst entity - | CrgEntity _ - | MetaEntity _ -> st + | CrgEntity _ -> st (* extended lexer ***********************************************************) @@ -194,8 +182,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 - AA.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 @@ -209,7 +197,6 @@ let progress = ref false let preprocess = ref false let root = ref "" let export = ref false -let old = ref false let st = ref (initial_status ()) let streaming = ref false (* parsing style (temporary) *) @@ -227,20 +214,16 @@ let process_1 st entity = 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 - AD.crg_of_aut err g st.dst e - | TxtEntity e, _ -> + 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 + | 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 @@ -278,7 +261,7 @@ let process st name = let main = try - let version_string = "Helena 0.8.1 M - October 2010" in + 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 @@ -294,7 +277,7 @@ try let set_xdir s = G.xdir := s in let set_root s = root := s in let clear_options () = - progress := false; old := false; export := false; preprocess := false; + progress := false; export := false; preprocess := false; stage := 3; root := ""; st := initial_status (); L.clear (); G.clear (); H.clear (); O.clear_reductions (); @@ -314,8 +297,8 @@ try 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 !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 @@ -325,7 +308,7 @@ try flush_all () in let help = - "Usage: helena [ -LPVXcgijopqux1 | -Ss | -O | -hkr ]* [ ]*\n\n" ^ + "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" @@ -343,12 +326,11 @@ 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_o = " use old abstract language instead of crg" 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_u = " activate sort inclusion" in let help_x = " export kernel entities (XML)" in let help_1 = " parse files with streaming policy" in @@ -367,12 +349,11 @@ try ("-i", Arg.Set G.indexes, help_i); ("-j", Arg.Set progress, help_j); ("-k", Arg.String set_kernel, help_k); - ("-o", Arg.Set old, help_o); + ("-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); - ("-u", Arg.Set G.si, help_u); ("-x", Arg.Set export, help_x); ("-1", Arg.Set streaming, help_1); ] process_file help;