From: Ferruccio Guidi Date: Sun, 14 Dec 2008 15:23:54 +0000 (+0000) Subject: autItem : the uris of the objects involved in the implicit coercions X-Git-Tag: make_still_working~4401 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f23388dbd51574725a11b0ab5373f09838a32ab5;p=helm.git autItem : the uris of the objects involved in the implicit coercions log : improved log output basic_rg: improved logging --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 311265788..ae6e441cc 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -16,6 +16,8 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx +automath/autItem.cmo: lib/nUri.cmi +automath/autItem.cmx: lib/nUri.cmx basic_rg/brg.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx basic_rg/brg.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx @@ -36,11 +38,13 @@ basic_rg/brgReduction.cmx: lib/share.cmx lib/log.cmx lib/cps.cmx \ basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ basic_rg/brgReduction.cmi basic_rg/brgType.cmi: lib/hierarchy.cmi basic_rg/brg.cmx -basic_rg/brgType.cmo: lib/log.cmi lib/hierarchy.cmi basic_rg/brgReduction.cmi \ - basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \ +basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ + lib/hierarchy.cmi basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \ + basic_rg/brgEnvironment.cmi basic_rg/brg.cmx automath/autItem.cmx \ basic_rg/brgType.cmi -basic_rg/brgType.cmx: lib/log.cmx lib/hierarchy.cmx basic_rg/brgReduction.cmx \ - basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ +basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ + lib/hierarchy.cmx basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \ + basic_rg/brgEnvironment.cmx basic_rg/brg.cmx automath/autItem.cmx \ basic_rg/brgType.cmi basic_rg/brgUntrusted.cmi: lib/hierarchy.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgEnvironment.cmi \ diff --git a/helm/software/lambda-delta/automath/Make b/helm/software/lambda-delta/automath/Make index 9a773e0fc..4b46c0bbd 100644 --- a/helm/software/lambda-delta/automath/Make +++ b/helm/software/lambda-delta/automath/Make @@ -1 +1 @@ -aut autOutput autParser autLexer +aut autOutput autParser autLexer autItem diff --git a/helm/software/lambda-delta/automath/autItem.ml b/helm/software/lambda-delta/automath/autItem.ml new file mode 100644 index 000000000..0f8b08234 --- /dev/null +++ b/helm/software/lambda-delta/automath/autItem.ml @@ -0,0 +1,22 @@ +(* + ||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 U = NUri + +(* Internal functions *******************************************************) + +let uri s = U.uri_of_string ("ld:" ^ s) + +(* Interface functions ******************************************************) + +let imp = uri "/l/imp" + +let mp = uri "/l/mp" diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 4778e5c3e..73da25b2d 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -43,6 +43,10 @@ let appl u t = Appl (u, t) let bind id b t = Bind (id, b, t) +let bind_abst id u t = Bind (id, Abst u, t) + +let bind_abbr id v t = Bind (id, Abbr v, t) + (* context handling functions ***********************************************) let empty_context = 0, [] diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 958408303..66c7ed3d8 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -29,6 +29,8 @@ type counters = { tabbrs: int } +let indexes = ref false + let initial_counters = { eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 @@ -110,7 +112,7 @@ let rec pp_term c frm = function | Some (id, _) -> F.fprintf frm "@[%s@]" id | None -> F.fprintf frm "@[#%u@]" i in - B.get f c i + if !indexes then f None else B.get f c i | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) | B.Cast (u, t) -> F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t @@ -131,20 +133,18 @@ let rec pp_term c frm = function B.push f c id B.Void let pp_context frm c = - let pp_entry f = function + let pp_entry frm = function | id, B.Abst w -> - F.fprintf frm "%s : %a\n%!" id (pp_term c) w; f () + F.fprintf frm "@,@[%s : %a@]" id (pp_term c) w | id, B.Abbr v -> - F.fprintf frm "%s = %a\n%!" id (pp_term c) v; f () + F.fprintf frm "@,@[%s = %a@]" id (pp_term c) v | id, B.Void -> - F.fprintf frm "%s\n%!" id; f () + F.fprintf frm "@,%s" id in - let f _ es = C.list_iter C.start pp_entry (List.rev es) in + let iter map frm l = List.iter (map frm) l in + let f _ es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in B.contents f c -let pp_term frm c t = - F.fprintf frm "%a\n%!" (pp_term c) t - let specs = { L.pp_term = pp_term; L.pp_context = pp_context } diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index 9fa180abd..566dfe8f3 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -18,3 +18,5 @@ val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Brg.context, Brg.term) Log.specs + +val indexes: bool ref diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index 50d20b754..fb7862c24 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -9,8 +9,11 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module U = NUri +module S = Share module L = Log module H = Hierarchy +module I = AutItem module B = Brg module O = BrgOutput module E = BrgEnvironment @@ -28,17 +31,21 @@ let error1 s c t = let error2 s1 c1 t1 s2 c2 t2 = raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2)) +let mk_gref u l = + let map t v = B.Appl (v, t) in + List.fold_left map (B.GRef u) l + (* Interface functions ******************************************************) -let rec type_of f g c x = - L.log O.specs level (L.ct_items1 "now checking" c x); +let rec b_type_of f g c x = + L.log O.specs level (L.ct_items1 "Now checking" c x); match x with | B.Sort h -> - let f h = f (B.Sort h) in H.apply f g h + let f h = f x (B.Sort h) in H.apply f g h | B.LRef i -> let f = function - | Some (_, B.Abst w) -> f w - | Some (_, B.Abbr (B.Cast (w, v))) -> f w + | Some (_, B.Abst w) -> f x w + | Some (_, B.Abbr (B.Cast (w, v))) -> f x w | Some (_, B.Abbr _) -> assert false | Some (_, B.Void) -> error1 "reference to excluded variable" c x @@ -48,48 +55,65 @@ let rec type_of f g c x = B.get f c i | B.GRef uri -> let f = function - | _, _, B.Abst w -> f w - | _, _, B.Abbr (B.Cast (w, v)) -> f w + | _, _, B.Abst w -> f x w + | _, _, B.Abbr (B.Cast (w, v)) -> f x w | _, _, B.Abbr _ -> assert false | _, _, B.Void -> error1 "reference to excluded object" c x in - E.get_obj f uri - | B.Bind (id, B.Abbr u, t) -> - let f tt = f (B.Bind (id, B.Abbr u, tt)) in - let f cc = type_of f g cc t in - let f u = B.push f c id (B.Abbr u) in - let f uu = match u with - | B.Cast _ -> f u - | _ -> f (B.Cast (uu, u)) + E.get_obj f uri + | B.Bind (id, B.Abbr v, t) -> + let f xv xt tt = + f (S.sh2 v xv t xt x (B.bind_abbr id)) (B.bind_abbr id xv tt) in - type_of f g c u + let f xv cc = b_type_of (f xv) g cc t in + let f xv = B.push (f xv) c id (B.Abbr xv) in + let f xv vv = match xv with + | B.Cast _ -> f xv + | _ -> f (B.Cast (vv, xv)) + in + type_of f g c v | B.Bind (id, B.Abst u, t) -> - let f tt = f (B.Bind (id, B.Abst u, tt)) in - let f cc = type_of f g cc t in - let f _ = B.push f c id (B.Abst u) in + let f xu xt tt = + f (S.sh2 u xu t xt x (B.bind_abst id)) (B.bind_abst id xu tt) + in + let f xu cc = b_type_of (f xu) g cc t in + let f xu _ = B.push (f xu) c id (B.Abst xu) in type_of f g c u | B.Bind (id, B.Void, t) -> - let f tt = f (B.Bind (id, B.Void, tt)) in - let f cc = type_of f g cc t in - B.push f c id B.Void + let f xt tt = + f (S.sh1 t xt x (B.bind id B.Void)) (B.bind id B.Void tt) + in + let f cc = b_type_of f g cc t in + B.push f c id B.Void | B.Appl (v, t) -> - let f tt cc = function - | R.Sort _ -> error1 "not a function" c t + let h xv vv xt tt cc = function + | R.Sort _ -> error1 "not a function" c xt | R.Abst w -> L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w); let f b = - if b then f (B.Appl (v, tt)) else - error2 "the term" c v "must be of type" cc w + if b then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else + error2 "the term" cc xv "must be of type" cc w in - type_of (R.are_convertible f cc w) g c v + R.are_convertible f cc w vv + in + let f xv vv xt = function +(* inserting a missing "modus ponens" *) + | B.Appl (y2, B.Appl (y1, B.GRef u)) when U.eq u I.imp -> + b_type_of f g c (mk_gref I.mp [y1; y2; xv; xt]) + | tt -> R.ho_whd (h xv vv xt tt) c tt in - let f tt = R.ho_whd (f tt) c t in - type_of f g c t + let f xv vv = b_type_of (f xv vv) g c t in + type_of f g c v | B.Cast (u, t) -> - let f b = - if b then f u else - error2 "the term" c t "must be of type" c u + let f xu xt b = + if b then f (S.sh2 u xu t xt x B.cast) xu else + error2 "the term" c xt "must be of type" c xu in - let f _ = type_of (R.are_convertible f c u) g c t in + let f xu xt tt = R.are_convertible (f xu xt) c xu tt in + let f xu _ = b_type_of (f xu) g c t in type_of f g c u + +and type_of f g c x = + let f t u = L.unbox (); f t u in + L.box (); b_type_of f g c x diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index ccccaedfa..e7e2d7ed7 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -12,4 +12,5 @@ exception TypeError of Brg.message val type_of: - (Brg.term -> 'a) -> Hierarchy.graph -> Brg.context -> Brg.term -> 'a + (Brg.term -> Brg.term -> 'a) -> + Hierarchy.graph -> Brg.context -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index 80a9d4fe7..96be16217 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -15,11 +15,17 @@ module T = BrgType (* Interface functions ******************************************************) +(* to share *) let type_check f g = function - | None -> f None - | Some ((_, _, B.Abst t) as obj) - | Some ((_, _, B.Abbr t) as obj) -> - let f tt obj = f (Some (tt, obj)) in - let f tt = E.set_obj (f tt) obj in - T.type_of f g B.empty_context t - | Some (_, _, B.Void) -> assert false + | None -> f None None + | Some (a, uri, B.Abst t) -> + let f tt obj = f (Some tt) (Some obj) in + let f xt tt = E.set_obj (f tt) (a, uri, B.Abst xt) in + T.type_of f g B.empty_context t + | Some (a, uri, B.Abbr t) -> + let f tt obj = f (Some tt) (Some obj) in + let f xt tt = E.set_obj (f tt) (a, uri, B.Abbr xt) in + T.type_of f g B.empty_context t + | Some (a, uri, B.Void) -> + let f obj = f None (Some obj) in + E.set_obj f (a, uri, B.Void) diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli index e65d67d99..92e401e7d 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli @@ -10,4 +10,4 @@ V_______________________________________________________________ *) val type_check: - ((Brg.term * Brg.obj) option -> 'a) -> Hierarchy.graph -> Brg.item -> 'a + (Brg.term option -> Brg.item -> 'a) -> Hierarchy.graph -> Brg.item -> 'a diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index 78e57fdfa..b33f6726b 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -19,7 +19,7 @@ type ('a, 'b) item = Term of 'a * 'b | String of string type ('a, 'b) specs = { - pp_term : F.formatter -> 'a -> 'b -> unit; + pp_term : 'a -> F.formatter -> 'b -> unit; pp_context: F.formatter -> 'a -> unit } @@ -27,6 +27,10 @@ let level = ref 0 (* Internal functions *******************************************************) +let std = F.std_formatter + +let err = F.err_formatter + let init = let started = ref false in fun () -> @@ -34,22 +38,34 @@ let init = begin P.printf "\n"; started := true end let pp_items frm st l items = - let pp_item = function - | Term (c, t) -> st.pp_context frm c; st.pp_term frm c t - | Context c -> st.pp_context frm c - | Warn s -> F.fprintf frm "@[%s\n@]" s - | String s -> F.fprintf frm "@[%s @]" s + let pp_item frm = function + | Term (c, t) -> F.fprintf frm "%a@,%a" st.pp_context c (st.pp_term c) t + | Context c -> F.fprintf frm "%a" st.pp_context c + | Warn s -> F.fprintf frm "@,%s" s + | String s -> F.fprintf frm "%s " s in - if !level >= l then List.iter pp_item items + let iter map frm l = List.iter (map frm) l in + if !level >= l then F.fprintf frm "%a" (iter pp_item) items (* Interface functions ******************************************************) +(* let warn msg = init (); P.printf " %s\n" msg; flush stdout +*) +let box () = F.fprintf std "@,@[%s" " "; F.pp_print_if_newline std () + +let unbox () = F.fprintf std "@]" -let log st l items = pp_items F.std_formatter st l items +let flush () = F.fprintf std "@]@." -let error st items = pp_items F.err_formatter st 0 items +let box_err () = F.fprintf err "@[" + +let flush_err () = F.fprintf err "@]@." + +let log st l items = pp_items std st l items + +let error st items = pp_items err st 0 items let items1 s = [Warn s] @@ -58,3 +74,5 @@ let ct_items1 s c t = let ct_items2 s1 c1 t1 s2 c2 t2 = [Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)] + +let warn msg = F.fprintf std "@,%s" msg diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli index 184594077..43e811915 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -15,7 +15,7 @@ type ('a, 'b) item = Term of 'a * 'b | String of string type ('a, 'b) specs = { - pp_term : Format.formatter -> 'a -> 'b -> unit; + pp_term : 'a -> Format.formatter -> 'b -> unit; pp_context: Format.formatter -> 'a -> unit } @@ -23,6 +23,16 @@ val level: int ref val warn: string -> unit +val box: unit -> unit + +val unbox: unit -> unit + +val flush: unit -> unit + +val box_err: unit -> unit + +val flush_err: unit -> unit + val log: ('a, 'b) specs -> int -> ('a, 'b) item list -> unit val error: ('a, 'b) specs -> ('a, 'b) item list -> unit diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index a2bac5616..06df1ab03 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -38,8 +38,10 @@ let initial_status = { let count count_fun c item = if !L.level > 2 then count_fun C.start c item else c +let flush () = L.flush (); L.flush_err () + let brg_error s msg = - L.error BrgO.specs (L.Warn s :: msg) + L.error BrgO.specs (L.Warn s :: msg); flush () let main = try @@ -81,9 +83,9 @@ try | [] -> st | item :: tl -> (* stage 3 *) - let f st = function - | None -> st - | Some (_, (i, u, _)) -> + let f st _ = function + | None -> st + | Some (i, u, _) -> Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); st in (* stage 2 *) @@ -116,23 +118,27 @@ try if !L.level > 2 && !stage > 1 then BrgO.print_counters C.start st.brgc; in let help = - "Usage: helena [ -V | -Ss | -m | -h ] ...\n\n" ^ + "Usage: helena [ -Vi | -Ss | -m | -h ] ...\n\n" ^ "Summary levels: 0 just errors, 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\n" in - let help_S = " Set summary level" in - let help_V = " Show version information" in + let help_S = " set summary level" in + let help_V = " show version information" in let help_h = " set type hierarchy" in + let help_i = " show local references by index" in let help_m = " output intermediate representation" in let help_s = " Set translation stage" in + L.box (); L.box_err (); H.set_new_sorts ignore ["Set"; "Prop"]; Arg.parse [ ("-S", Arg.Int set_summary, help_S); ("-V", Arg.Unit print_version, help_V); ("-h", Arg.String set_hierarchy, help_h); + ("-i", Arg.Set BrgO.indexes, help_i); ("-m", Arg.String set_meta_file, help_m); ("-s", Arg.Int set_stage, help_s); ] read_file help; - if !L.level > 0 then Time.utime_stamp "at exit" + if !L.level > 0 then Time.utime_stamp "at exit"; + flush () with BrgType.TypeError msg -> brg_error "Type Error" msg