From: Ferruccio Guidi Date: Thu, 18 Dec 2008 15:48:01 +0000 (+0000) Subject: - improved logging X-Git-Tag: make_still_working~4372 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d38cea7e4865091412e1414f5594dd7c124de47e;p=helm.git - improved logging - we started to support the coercion for "non" --- diff --git a/helm/software/lambda-delta/automath/autItem.ml b/helm/software/lambda-delta/automath/autItem.ml index cda1d1c27..dae038cce 100644 --- a/helm/software/lambda-delta/automath/autItem.ml +++ b/helm/software/lambda-delta/automath/autItem.ml @@ -28,3 +28,7 @@ let all = uri "/l/all" let alle = uri "/l/alle" let alli = uri "/l/alli" + +let non = uri "/l/non" + +let lppc0 = uri "/l/lppc0" diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index 279ca072f..ca22c1dbc 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -51,6 +51,14 @@ let level = 5 let error i = raise (LRefNotFound (L.items1 (string_of_int i))) +let log1 s c t = + let sc, st = s ^ " in the context", "the term" in + L.log O.specs level (L.ct_items1 sc c st t) + +let log2 s c u t = + let sc, su, st = s ^ " in the context", "the term", "and the term" in + L.log O.specs level (L.ct_items2 sc c su u st t) + let empty_machine = {i = 0; c = B.empty_context; s = []} let inc m = {m with i = succ m.i} @@ -131,13 +139,13 @@ let rec ho_whd f c m x = let ho_whd f c t = let f r = L.unbox level; f r in - L.box level; L.log O.specs level (L.ct_items1 "Now scanning" c t); + L.box level; log1 "Now scanning" c t; ho_whd f c empty_machine t let rec are_convertible f xl c m1 t1 m2 t2 = let rec aux m1 r1 m2 r2 = let u, t = term_of_whdr r1, term_of_whdr r2 in - L.log O.specs level (L.ct_items2 "Now really converting" c u "and" c t); + log2 "Now really converting" c u t; match r1, r2 with | Sort_ h1, Sort_ h2 -> if h1 = h2 then f xl else f None @@ -181,6 +189,5 @@ and are_convertible_stacks f xl c m1 m2 = let are_convertible f c u t = let f b = L.unbox level; f b in - L.box level; - L.log O.specs level (L.ct_items2 "Now converting" c u "and" c t); + L.box level; log2 "Now converting" c u t; are_convertible f (Some []) c empty_machine u empty_machine t diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index 8aee51920..4ffa2e1f4 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -26,11 +26,19 @@ exception TypeError of B.message let level = 4 -let error1 s c t = - raise (TypeError (L.ct_items1 s c t)) +let log1 s c t = + let sc, st = s ^ " in the context", "the term" in + L.log O.specs level (L.ct_items1 sc c st t) -let error2 s1 c1 t1 s2 c2 t2 = - raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2)) +let error1 st c t = + let sc = "In the context" in + raise (TypeError (L.ct_items1 sc c st t)) + +let error3 c t1 t2 t3 = + let sc, st1, st2, st3 = + "In the context", "the term", "is of type", "but must be of type" + in + raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) let mk_gref u l = let map t v = B.Appl (v, t) in @@ -80,7 +88,7 @@ let add_coercions f = C.list_fold_left f add_coercion (* Interface functions ******************************************************) let rec b_type_of f g c x = - L.log O.specs level (L.ct_items1 "Now checking" c x); + log1 "Now checking" c x; match x with | B.Sort h -> let f h = f x (B.Sort h) in H.apply f g h @@ -132,7 +140,7 @@ let rec b_type_of f g c x = let f xv vv xt tt = function | R.Abst w -> L.box (succ level); - L.log O.specs (succ level) (L.ct_items1 "Just scanned" c w); + L.log O.specs (succ level) (L.t_items1 "Just scanned" c w); L.unbox (succ level); let f = function | Some [] -> f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) @@ -140,7 +148,7 @@ let rec b_type_of f g c x = L.log O.specs level (L.items1 "Rechecking coerced term"); let f xv = b_type_of f g c (S.sh2 v xv t xt x B.appl) in add_coercions f xv l - | None -> error2 "The term" c xv "must be of type" c w + | None -> error3 c xv vv w in R.are_convertible f c w vv (* inserting a missing "modus ponens" *) @@ -149,23 +157,23 @@ let rec b_type_of f g c x = b_type_of f g c (mk_gref I.mp (vs @ [xv; xt])) | R.GRef (uri, vs) when U.eq uri I.all -> L.log O.specs level (L.items1 "Rechecking coerced term"); - b_type_of f g c (mk_gref I.alle (vs @ [xv; xt])) - | _ -> + b_type_of f g c (mk_gref I.alle (vs @ [xt; xv])) + | _ -> error1 "not a function" c xt in let f xv vv xt tt = R.ho_whd (f xv vv xt tt) c tt in 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 xu xt = function + let f xu xt tt = function | Some [] -> f (S.sh2 u xu t xt x B.cast) xu | Some l -> L.log O.specs level (L.items1 "Rechecking coerced term"); let f xt = b_type_of f g c (S.sh2 u xu t xt x B.cast) in add_coercions f xt l - | None -> error2 "The term" c xt "must be of type" c xu + | None -> error3 c xt tt xu in - let f xu xt tt = R.are_convertible (f xu xt) c xu tt in + let f xu xt tt = R.are_convertible (f xu xt tt) c xu tt in let f xu _ = b_type_of (f xu) g c t in type_of f g c u diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index fd99db2d2..4cea12cda 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -33,7 +33,7 @@ let err = F.err_formatter let pp_items frm st l items = let pp_item frm = function - | Term (c, t) -> F.fprintf frm "%a@,%a" st.pp_context c (st.pp_term c) t + | Term (c, t) -> F.fprintf frm "@,%a" (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 @@ -61,10 +61,16 @@ let error st items = pp_items err st 0 items let items1 s = [Warn s] -let ct_items1 s c t = - [Warn s; Term (c, t)] +let t_items1 st c t = + [Warn st; Term (c, t)] -let ct_items2 s1 c1 t1 s2 c2 t2 = - [Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)] +let ct_items1 sc c st t = + [Warn sc; Context c; Warn st; Term (c, t)] + +let ct_items2 sc c st1 t1 st2 t2 = + ct_items1 sc c st1 t1 @ [Warn st2; Term (c, t2)] + +let ct_items3 sc c st1 t1 st2 t2 st3 t3 = + ct_items2 sc c st1 t1 st2 t2 @ [Warn st3; Term (c, t3)] 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 821cb0f31..bdaee06e0 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -39,6 +39,14 @@ val error: ('a, 'b) specs -> ('a, 'b) item list -> unit val items1: string -> ('a, 'b) item list -val ct_items1: string -> 'a -> 'b -> ('a, 'b) item list +val t_items1: string -> 'a -> 'b -> ('a, 'b) item list -val ct_items2: string -> 'a -> 'b -> string -> 'a -> 'b -> ('a, 'b) item list +val ct_items1: + string -> 'a -> string -> 'b -> ('a, 'b) item list + +val ct_items2: + string -> 'a -> string -> 'b -> string -> 'b -> ('a, 'b) item list + +val ct_items3: + string -> 'a -> string -> 'b -> string -> 'b -> string -> 'b -> + ('a, 'b) item list