X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;h=b47d00725a9f056434c4523981ceb5adb4355a60;hb=d145ea48ed0bdb9642ced01283231f3f13d476b8;hp=579f5e6585211f665c3119548ebca5a44d79d10b;hpb=e7f64fe2cc67f3514131c8831f87311ff600d005;p=helm.git diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index 579f5e658..b47d00725 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -20,11 +20,11 @@ module H = Hierarchy module O = Output module E = Entity module S = Status -module TD = CrgTxt +module DO = CrgOutput +module TD = TxtCrg module AA = AutProcess module AO = AutOutput -module AD = CrgAut -module DO = CrgOutput +module AD = AutCrg module XL = XmlLibrary module XD = XmlCrg module BD = BrgCrg @@ -35,11 +35,6 @@ module ZO = BagOutput module ZT = BagType module ZU = BagUntrusted -module MA = MetaAut -module MO = MetaOutput -module MB = MetaBrg -module MZ = MetaBag - type status = { kst: S.status; tst: TD.status; @@ -49,8 +44,6 @@ type status = { dc : DO.counters; bc : BO.counters; zc : ZO.counters; - mst: MA.status; - mc : MO.counters; } let flush_all () = L.flush 0; L.flush_err () @@ -70,23 +63,19 @@ let initial_status () = { 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; } (* 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.Crg -> DO.print_counters C.start st.dc @@ -94,13 +83,9 @@ let print_counters st = function | 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 + | _, entity -> entity let pp_progress e = let f a u = @@ -110,22 +95,19 @@ let pp_progress e = 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 - | MetaEntity e -> E.common f e + | 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} - | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e} + | 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 _ -> () let type_check st k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in @@ -133,8 +115,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 ***********************************************************) @@ -213,7 +194,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) *) @@ -231,20 +211,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 -> + 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, _ -> + | 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 @@ -282,7 +258,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.1 M - November 2010" in let print_version () = L.warn (version_string ^ "\n"); exit 0 in let set_hierarchy s = if H.set_graph s then () else @@ -298,7 +274,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 (); @@ -319,9 +295,7 @@ try 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 - if !old then MO.print_counters C.start !st.mc - else print_counters !st G.Crg; + 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 @@ -331,7 +305,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" @@ -349,12 +323,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 @@ -373,12 +346,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;