From 0dc347a7742e40a828fa98acba70078dd2d7cbd5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 5 Sep 2009 11:26:44 +0000 Subject: [PATCH] basic_rg: we improved the error reporting interface --- helm/software/lambda-delta/.depend.opt | 26 +++++----- helm/software/lambda-delta/basic_rg/brg.ml | 8 ++- .../lambda-delta/basic_rg/brgEnvironment.ml | 9 +--- .../lambda-delta/basic_rg/brgEnvironment.mli | 4 +- .../lambda-delta/basic_rg/brgOutput.ml | 6 +-- .../lambda-delta/basic_rg/brgReduction.ml | 49 +++++++++---------- .../lambda-delta/basic_rg/brgReduction.mli | 9 ++-- .../software/lambda-delta/basic_rg/brgType.ml | 31 +++++++----- .../lambda-delta/basic_rg/brgType.mli | 2 +- helm/software/lambda-delta/toplevel/top.ml | 3 +- 10 files changed, 69 insertions(+), 78 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index c1af16854..90af5cfdc 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -36,22 +36,22 @@ common/item.cmx: lib/nUri.cmx automath/aut.cmx common/library.cmi: common/item.cmx common/hierarchy.cmi common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/library.cmi common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/library.cmi -basic_rg/brg.cmo: lib/log.cmi common/item.cmx -basic_rg/brg.cmx: lib/log.cmx common/item.cmx +basic_rg/brg.cmo: common/item.cmx +basic_rg/brg.cmx: common/item.cmx basic_rg/brgOutput.cmi: lib/log.cmi common/item.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ common/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ common/hierarchy.cmx lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx -basic_rg/brgEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_rg/brg.cmx \ +basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi -basic_rg/brgEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_rg/brg.cmx \ +basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi basic_rg/brgSubstitution.cmi: basic_rg/brg.cmx basic_rg/brgSubstitution.cmo: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi basic_rg/brgSubstitution.cmx: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi -basic_rg/brgReduction.cmi: basic_rg/brg.cmx +basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmo: lib/share.cmx common/output.cmi lib/nUri.cmi \ lib/log.cmi lib/cps.cmx basic_rg/brgOutput.cmi \ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi @@ -142,15 +142,15 @@ toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \ toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \ toplevel/metaBag.cmi toplevel/metaAut.cmi lib/log.cmi common/library.cmi \ common/hierarchy.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \ - basic_rg/brgType.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagOutput.cmi \ - basic_ag/bag.cmx automath/autProcess.cmi automath/autParser.cmi \ - automath/autOutput.cmi automath/autLexer.cmx + basic_rg/brgType.cmi basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \ + basic_rg/brg.cmx basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi \ + basic_ag/bagOutput.cmi basic_ag/bag.cmx automath/autProcess.cmi \ + automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \ toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \ toplevel/metaBag.cmx toplevel/metaAut.cmx lib/log.cmx common/library.cmx \ common/hierarchy.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ - basic_rg/brgType.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagOutput.cmx \ - basic_ag/bag.cmx automath/autProcess.cmx automath/autParser.cmx \ - automath/autOutput.cmx automath/autLexer.cmx + basic_rg/brgType.cmx basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \ + basic_rg/brg.cmx basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx \ + basic_ag/bagOutput.cmx basic_ag/bag.cmx automath/autProcess.cmx \ + automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 779a121e6..6a9f9fd20 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -39,8 +39,6 @@ type context = Null (* Cons: tail, relative context, binder *) | Cons of context * context option * bind -type message = (context, term) Log.item list - (* Currified constructors ***************************************************) let abst a w = Abst (a, w) @@ -68,7 +66,7 @@ let push f es ?c b = let get err f es i = let rec aux j = function - | Null -> err i + | Null -> err () | Cons (tl, None, b) when j = 0 -> f tl b | Cons (_, Some c, b) when j = 0 -> f c b | Cons (tl, _, _) -> aux (pred j) tl @@ -78,9 +76,9 @@ let get err f es i = let rec rev_iter f map = function | Null -> f () | Cons (tl, None, b) -> - let f () = map f tl b in rev_iter f map tl + let f _ = map f tl b in rev_iter f map tl | Cons (tl, Some c, b) -> - let f () = map f c b in rev_iter f map tl + let f _ = map f c b in rev_iter f map tl let rec fold_left f map x = function | Null -> f x diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml index 902eeb45a..29c6dd475 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml @@ -10,20 +10,15 @@ V_______________________________________________________________ *) module U = NUri -module L = Log module H = U.UriHash module B = Brg -exception ObjectNotFound of B.message - let hsize = 7000 let env = H.create hsize let entry = ref 1 (* Internal functions *******************************************************) -let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri))) - (* Interface functions ******************************************************) let set_obj f obj = @@ -31,5 +26,5 @@ let set_obj f obj = let obj = !entry, uri, b in incr entry; H.add env uri obj; f obj -let get_obj f uri = - try f (H.find env uri) with Not_found -> error uri +let get_obj err f uri = + try f (H.find env uri) with Not_found -> err () diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli index 8f9f8b1b0..ee59f37d3 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli @@ -9,8 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception ObjectNotFound of Brg.message - val set_obj: (Brg.obj -> 'a) -> Brg.obj -> 'a -val get_obj: (Brg.obj -> 'a) -> NUri.uri -> 'a +val get_obj: (unit -> 'a) -> (Brg.obj -> 'a) -> NUri.uri -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index fe496e25d..eec76f620 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -175,17 +175,17 @@ let id frm a = let rec pp_term c frm = function | B.Sort (_, h) -> - let err () = F.fprintf frm "@[*%u@]" h in + let err _ = F.fprintf frm "@[*%u@]" h in let f s = F.fprintf frm "@[%s@]" s in H.get_sort err f h | B.LRef (_, i) -> - let err i = F.fprintf frm "@[#%u@]" i in + let err _ = F.fprintf frm "@[#%u@]" i in let f _ = function | B.Abst (a, _) | B.Abbr (a, _) | B.Void a -> F.fprintf frm "@[%a@]" id a in - if !O.indexes then err i else B.get err f c i + if !O.indexes then err () else B.get err f c i | B.GRef (_, s) -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) | B.Cast (_, u, t) -> diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index f9d0a200c..08630cde6 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -24,6 +24,8 @@ type machine = { i: int } +type message = (machine, B.term) Log.item list + (* Internal functions *******************************************************) let level = 5 @@ -45,10 +47,10 @@ let are_alpha_convertible err f t1 t2 = if U.eq u1 u2 then f () else err () | B.Cast (_, v1, t1), B.Cast (_, v2, t2) | B.Appl (_, v1, t1), B.Appl (_, v2, t2) -> - let f () = aux f (t1, t2) in + let f _ = aux f (t1, t2) in aux f (v1, v2) | B.Bind (b1, t1), B.Bind (b2, t2) -> - let f () = aux f (t1, t2) in + let f _ = aux f (t1, t2) in aux_bind f (b1, b2) | _ -> err () and aux_bind f = function @@ -59,8 +61,8 @@ let are_alpha_convertible err f t1 t2 = in if S.eq t1 t2 then f () else aux f (t1, t2) -let get f m i = - B.get C.err f m.c i +let get err f m i = + B.get err f m.c i (* to share *) let rec step f ?(delta=false) ?(rt=false) m x = @@ -78,7 +80,7 @@ let rec step f ?(delta=false) ?(rt=false) m x = | e, _, b -> f m (Some (e, b)) x in - E.get_obj f uri + E.get_obj C.err f uri | B.LRef (_, i) -> let f c = function | B.Abbr (_, v) -> @@ -93,7 +95,7 @@ let rec step f ?(delta=false) ?(rt=false) m x = let f e = f {m with c = c} (Some (e, b)) x in B.apix C.err f a in - get f m i + get C.err f m i | B.Cast (_, _, t) -> P.add ~tau:1 (); step f ~delta ~rt m t @@ -130,10 +132,7 @@ let rec ac_nfs err f ~si m1 a1 u m2 a2 t = if e1 = e2 then ac_stacks err f m1 m2 else err () | Some (e1, B.Abbr (_, v1)), _, Some (e2, B.Abbr (_, v2)), _ -> if e1 = e2 then - let err () = - P.add ~gdelta:2 (); - ac err f ~si m1 v1 m2 v2 - in + let err _ = P.add ~gdelta:2 (); ac err f ~si m1 v1 m2 v2 in ac_stacks err f m1 m2 else if e1 < e2 then begin P.add ~gdelta:1 (); @@ -152,7 +151,7 @@ let rec ac_nfs err f ~si m1 a1 u m2 a2 t = _, B.Bind ((B.Abst (_, w2) as b2), t2) -> let f m1 m2 = ac err f ~si m1 t1 m2 t2 in let f m1 = push (f m1) m2 b2 in - let f () = push f m1 b1 in + let f _ = push f m1 b1 in ac err f ~si:false m1 w1 m2 w2 | _, B.Sort _, _, B.Bind (b, t) when si -> P.add ~si:1 (); @@ -183,10 +182,10 @@ let empty_machine = { c = B.empty_context; s = []; i = 0 } -let get f m i = +let get err f m i = assert (m.s = []); let f c = f in - get f m i + get err f m i let xwhd f m t = L.box level; log1 "Now scanning" m.c t; @@ -195,18 +194,16 @@ let xwhd f m t = let are_convertible err f ?(si=false) mu u mw w = L.box level; log2 "Now converting" mu.c u mw.c w; - let f () = L.unbox level; f () in - let err () = ac err f ~si mu u mw w in + let f x = L.unbox level; f x in + let err _ = ac err f ~si mu u mw w in (* if S.eq mu mw then are_alpha_convertible err f u w else *) err () -let message1 st1 m t1 = - L.ct_items1 "In the context" m.c st1 t1 - -let message3 st1 st2 ?sm3 st3 m1 t1 t2 ?m3 t3 = - let sm1 = "In the context" in - match sm3, m3 with - | Some sm3, Some m3 -> - L.ct_items3 sm1 m1.c st1 t1 st2 t2 ~sc3:sm3 ~c3:m3.c st3 t3 - | None, None -> - L.ct_items3 sm1 m1.c st1 t1 st2 t2 st3 t3 - | _ -> assert false +(* error reporting **********************************************************) + +let pp_term m frm t = O.specs.L.pp_term m.c frm t + +let pp_context frm m = O.specs.L.pp_context frm m.c + +let specs = { + L.pp_term = pp_term; L.pp_context = pp_context +} diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index 01ad7e7a6..7515967cd 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -13,7 +13,7 @@ type machine val empty_machine: machine -val get: (Brg.bind -> 'a) -> machine -> int -> 'a +val get: (unit -> 'a) -> (Brg.bind -> 'a) -> machine -> int -> 'a val push: (machine -> 'a) -> machine -> Brg.bind -> 'a @@ -24,9 +24,6 @@ val are_convertible: (unit -> 'a) -> (unit -> 'a) -> ?si:bool -> machine -> Brg.term -> machine -> Brg.term -> 'a -val message1: - string -> machine -> Brg.term -> Brg.message +type message = (machine, Brg.term) Log.item list -val message3: - string -> string -> ?sm3:string -> string -> - machine -> Brg.term -> Brg.term -> ?m3:machine -> Brg.term -> Brg.message +val specs: (machine, Brg.term) Log.specs diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index 885f1bd8d..96c9cb52a 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -20,40 +20,43 @@ module E = BrgEnvironment module S = BrgSubstitution module R = BrgReduction -exception TypeError of B.message +exception TypeError of R.message (* Internal functions *******************************************************) let level = 4 +let message1 st1 m t1 = + L.ct_items1 "In the context" m st1 t1 + let log1 s m t = let s = s ^ " the term" in - L.log O.specs level (R.message1 s m t) + L.log R.specs level (message1 s m t) let error1 s m t = - raise (TypeError (R.message1 s m t)) + raise (TypeError (message1 s m t)) -let message3 m t1 t2 ?mu t3 = - let st1, st2 = "the term", "is of type" in +let message3 m t1 t2 ?mu t3 = + let sm, st1, st2 = "In the context", "the term", "is of type" in match mu with | Some mu -> let smu, st3 = "but in the context", "it must be of type" in - R.message3 st1 st2 ~sm3:smu st3 m t1 t2 ~m3:mu t3 + L.ct_items3 sm m st1 t1 st2 t2 ~sc3:smu ~c3:mu st3 t3 | None -> let st3 = "but it must be of type" in - R.message3 st1 st2 st3 m t1 t2 t3 + L.ct_items3 sm m st1 t1 st2 t2 st3 t3 let error3 m t1 t2 ?mu t3 = raise (TypeError (message3 m t1 t2 ?mu t3)) let assert_convertibility f ~si m u w v = - let err () = error3 m v w u in + let err _ = error3 m v w u in R.are_convertible err f ~si m u m w let assert_applicability f ~si m u w v = let f mu = function | B.Bind (B.Abst (_, u), _) -> - let err () = error3 m v w ~mu u in + let err _ = error3 m v w ~mu u in R.are_convertible err f ~si mu u m w | _ -> error1 "not a function type" m u in @@ -74,7 +77,8 @@ let rec b_type_of f ~si g m x = | B.Void _ -> error1 "reference to excluded variable" m x in - R.get f m i + let err _ = error1 "reference to unknown variable" m x in + R.get err f m i | B.GRef (_, uri) -> let f = function | _, _, B.Abst (_, w) -> f x w @@ -83,7 +87,8 @@ let rec b_type_of f ~si g m x = | _, _, B.Void _ -> error1 "reference to excluded object" m x in - E.get_obj f uri + let err _ = error1 "reference to unknown object" m x in + E.get_obj err f uri | B.Bind (B.Abbr (a, v), t) -> let f xv xt tt = f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) @@ -110,14 +115,14 @@ let rec b_type_of f ~si g m x = R.push f m b | B.Appl (a, v, t) -> let f xv vv xt tt = - let f () = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in + let f _ = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in assert_applicability f ~si m tt vv xv in let f xv vv = b_type_of (f xv vv) ~si g m t in type_of f ~si g m v | B.Cast (a, u, t) -> let f xu xt tt = - let f () = f (A.sh2 u xu t xt x (B.cast a)) xu in + let f _ = f (A.sh2 u xu t xt x (B.cast a)) xu in assert_convertibility f ~si m xu tt xt in let f xu _ = b_type_of (f xu) ~si g m t in diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index 78c49ae8b..b9117a3a1 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception TypeError of Brg.message +exception TypeError of BrgReduction.message val type_of: (Brg.term -> Brg.term -> 'a) -> ?si:bool -> diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 6a8b92f08..13887c6ef 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -24,6 +24,7 @@ module ML = MetaLibrary module MBrg = MetaBrg module G = Library module BrgO = BrgOutput +module BrgR = BrgReduction module BrgT = BrgType module BrgU = BrgUntrusted module MBag = MetaBag @@ -58,7 +59,7 @@ let bag_error s msg = L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush () let brg_error s msg = - L.error BrgO.specs (L.Warn s :: L.Loc :: msg); flush () + L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush () let process_item f st = let f ast = f {st with ast = ast} in -- 2.39.2