From c52a5748465e24374aec569bf74fc85e5bbb075a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 4 Sep 2009 20:43:46 +0000 Subject: [PATCH] the TypeError exception is back in place inside the Type modules basic_rg: some typing-related code is back in place inside the Type module log: some improvements in the interface --- helm/software/lambda-delta/.depend.opt | 28 ++-- .../automath/{omega.aut => Omega.aut} | 0 .../lambda-delta/basic_ag/bagReduction.ml | 10 +- .../lambda-delta/basic_ag/bagReduction.mli | 2 - .../software/lambda-delta/basic_ag/bagType.ml | 6 +- .../lambda-delta/basic_ag/bagType.mli | 2 + .../lambda-delta/basic_rg/brgReduction.ml | 137 ++++++++---------- .../lambda-delta/basic_rg/brgReduction.mli | 18 ++- .../software/lambda-delta/basic_rg/brgType.ml | 36 ++++- .../lambda-delta/basic_rg/brgType.mli | 2 + helm/software/lambda-delta/lib/cps.ml | 6 +- helm/software/lambda-delta/lib/log.ml | 20 ++- helm/software/lambda-delta/lib/log.mli | 7 +- helm/software/lambda-delta/toplevel/top.ml | 10 +- 14 files changed, 162 insertions(+), 122 deletions(-) rename helm/software/lambda-delta/automath/{omega.aut => Omega.aut} (100%) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 5c92d5ccd..c1af16854 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,9 +1,17 @@ +lib/nUri.cmi: lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi +lib/cps.cmo: +lib/cps.cmx: +lib/share.cmo: +lib/share.cmx: +lib/log.cmi: lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx +automath/aut.cmo: +automath/aut.cmx: automath/autProcess.cmi: automath/aut.cmx automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi @@ -17,8 +25,10 @@ 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 +common/hierarchy.cmi: common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi +common/output.cmi: common/output.cmo: lib/log.cmi common/output.cmi common/output.cmx: lib/log.cmx common/output.cmi common/item.cmo: lib/nUri.cmi automath/aut.cmx @@ -41,7 +51,7 @@ basic_rg/brgEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_rg/brg.cmx \ 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: lib/log.cmi basic_rg/brg.cmx +basic_rg/brgReduction.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 @@ -132,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/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmi basic_ag/bagReduction.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/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/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmx basic_ag/bagReduction.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/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/automath/omega.aut b/helm/software/lambda-delta/automath/Omega.aut similarity index 100% rename from helm/software/lambda-delta/automath/omega.aut rename to helm/software/lambda-delta/automath/Omega.aut diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index 4e147ae6d..c2de019cd 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -17,8 +17,6 @@ module O = BagOutput module E = BagEnvironment module S = BagSubstitution -exception TypeError of B.message - type machine = { i: int; c: B.context; @@ -45,17 +43,13 @@ let term_of_whdr = function let level = 5 -let error i = - let s = Printf.sprintf "local reference not found %u" i in - raise (TypeError (L.items1 s)) - 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 cu u ct t = let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in - L.log O.specs level (L.ct_items2 s1 cu s2 u s3 ct s2 t) + L.log O.specs level (L.ct_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) let empty_machine = {i = 0; c = B.empty_context; s = []} @@ -73,7 +67,7 @@ let unwind_stack f m = let get f c m i = let f = function | Some (_, b) -> f b - | None -> error i + | None -> assert false in let f c = B.get f c i in B.append f c m.c diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.mli b/helm/software/lambda-delta/basic_ag/bagReduction.mli index 35c017581..c9918704d 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.mli +++ b/helm/software/lambda-delta/basic_ag/bagReduction.mli @@ -9,8 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception TypeError of Bag.message - type ho_whd_result = | Sort of int | Abst of Bag.term diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index c398e034d..02c831994 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -19,6 +19,8 @@ module O = BagOutput module E = BagEnvironment module R = BagReduction +exception TypeError of B.message + (* Internal functions *******************************************************) let level = 4 @@ -29,13 +31,13 @@ let log1 s c t = let error1 st c t = let sc = "In the context" in - raise (R.TypeError (L.ct_items1 sc c st t)) + 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 (R.TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) + 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 diff --git a/helm/software/lambda-delta/basic_ag/bagType.mli b/helm/software/lambda-delta/basic_ag/bagType.mli index e0ec3c3c2..37f92875d 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.mli +++ b/helm/software/lambda-delta/basic_ag/bagType.mli @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +exception TypeError of Bag.message + val type_of: (Bag.term -> Bag.term -> 'a) -> ?si:bool -> Hierarchy.graph -> Bag.context -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index f59d84226..f9d0a200c 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -18,8 +18,6 @@ module B = Brg module O = BrgOutput module E = BrgEnvironment -exception TypeError of B.message - type machine = { c: B.context; s: (B.context * B.term) list; @@ -36,45 +34,33 @@ let log1 s c t = let log2 s cu u ct t = let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in - L.log O.specs level (L.ct_items2 s1 cu s2 u s3 ct s2 t) - -let error0 i = - let s = Printf.sprintf "local reference not found %u" i in - raise (TypeError (L.items1 s)) - -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)) + L.log O.specs level (L.ct_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) -let are_alpha_convertible f t1 t2 = +let are_alpha_convertible err f t1 t2 = let rec aux f = function | B.Sort (_, p1), B.Sort (_, p2) - | B.LRef (_, p1), B.LRef (_, p2) -> f (p1 = p2) - | B.GRef (_, u1), B.GRef (_, u2) -> f (U.eq u1 u2) + | B.LRef (_, p1), B.LRef (_, p2) -> + if p1 = p2 then f () else err () + | B.GRef (_, u1), B.GRef (_, u2) -> + 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 r = if r then aux f (t1, t2) else f r in + let f () = aux f (t1, t2) in aux f (v1, v2) | B.Bind (b1, t1), B.Bind (b2, t2) -> - let f r = if r then aux f (t1, t2) else f r in + let f () = aux f (t1, t2) in aux_bind f (b1, b2) - | _ -> f false + | _ -> err () and aux_bind f = function | B.Abbr (_, v1), B.Abbr (_, v2) | B.Abst (_, v1), B.Abst (_, v2) -> aux f (v1, v2) - | B.Void _, B.Void _ -> f true - | _ -> f false + | B.Void _, B.Void _ -> f () + | _ -> err () in - if S.eq t1 t2 then f true else aux f (t1, t2) + if S.eq t1 t2 then f () else aux f (t1, t2) let get f m i = - B.get error0 f m.c i + B.get C.err f m.c i (* to share *) let rec step f ?(delta=false) ?(rt=false) m x = @@ -126,15 +112,6 @@ let rec step f ?(delta=false) ?(rt=false) m x = let f c = step f ~delta ~rt {m with c = c} t in B.push f m.c ~c:m.c b -let domain f m t = - let f r = L.unbox level; f r in - let f m _ = function - | B.Bind (B.Abst (_, w), _) -> f m w - | _ -> error1 "not a function" m.c t - in - L.box level; log1 "Now scanning" m.c t; - step f ~delta:true ~rt:true m t - let push f m b = assert (m.s = []); let b, i = match b with @@ -144,64 +121,61 @@ let push f m b = let f c = f {m with c = c; i = i} in B.push f m.c ~c:m.c b -let rec ac_nfs f ~si r m1 a1 u m2 a2 t = +let rec ac_nfs err f ~si m1 a1 u m2 a2 t = log2 "Now converting nfs" m1.c u m2.c t; match a1, u, a2, t with | _, B.Sort (_, h1), _, B.Sort (_, h2) -> - if h1 = h2 then f r else f false + if h1 = h2 then f () else err () | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _ -> - if e1 = e2 then ac_stacks f r m1 m2 else f false + 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 f r = - if r then f r - else begin - P.add ~gdelta:2 (); - ac f ~si true m1 v1 m2 v2 - end + let err () = + P.add ~gdelta:2 (); + ac err f ~si m1 v1 m2 v2 in - ac_stacks f r m1 m2 + ac_stacks err f m1 m2 else if e1 < e2 then begin P.add ~gdelta:1 (); - step (ac_nfs f ~si r m1 a1 u) m2 v2 + step (ac_nfs err f ~si m1 a1 u) m2 v2 end else begin P.add ~gdelta:1 (); - step (ac_nfs_rev f ~si r m2 a2 t) m1 v1 + step (ac_nfs_rev err f ~si m2 a2 t) m1 v1 end | _, _, Some (_, B.Abbr (_, v2)), _ -> P.add ~gdelta:1 (); - step (ac_nfs f ~si r m1 a1 u) m2 v2 + step (ac_nfs err f ~si m1 a1 u) m2 v2 | Some (_, B.Abbr (_, v1)), _, _, _ -> P.add ~gdelta:1 (); - step (ac_nfs_rev f ~si r m2 a2 t) m1 v1 + step (ac_nfs_rev err f ~si m2 a2 t) m1 v1 | _, B.Bind ((B.Abst (_, w1) as b1), t1), _, B.Bind ((B.Abst (_, w2) as b2), t2) -> - let g m1 m2 = ac f ~si r m1 t1 m2 t2 in - let g m1 = push (g m1) m2 b2 in - let f r = if r then push g m1 b1 else f false in - ac f ~si:false r m1 w1 m2 w2 + 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 + ac err f ~si:false m1 w1 m2 w2 | _, B.Sort _, _, B.Bind (b, t) when si -> P.add ~si:1 (); - let f m1 m2 = ac f ~si r m1 u m2 t in + let f m1 m2 = ac err f ~si m1 u m2 t in let f m1 = push (f m1) m2 b in push f m1 b - | _ -> f false + | _ -> err () -and ac_nfs_rev f ~si r m2 a2 t m1 a1 u = ac_nfs f ~si r m1 a1 u m2 a2 t +and ac_nfs_rev err f ~si m2 a2 t m1 a1 u = ac_nfs err f ~si m1 a1 u m2 a2 t -and ac f ~si r m1 t1 m2 t2 = +and ac err f ~si m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) - let g m1 a1 t1 = step (ac_nfs f ~si r m1 a1 t1) m2 t2 in - if r = false then f false else step g m1 t1 + let f m1 a1 t1 = step (ac_nfs err f ~si m1 a1 t1) m2 t2 in + step f m1 t1 -and ac_stacks f r m1 m2 = +and ac_stacks err f m1 m2 = (* L.warn "entering R.are_convertible_stacks"; *) - if List.length m1.s <> List.length m2.s then f false else - let map f r (c1, v1) (c2, v2) = + if List.length m1.s <> List.length m2.s then err () else + let map f (c1, v1) (c2, v2) = let m1, m2 = {m1 with c = c1; s = []}, {m2 with c = c2; s = []} in - ac f ~si:false r m1 v1 m2 v2 + ac err f ~si:false m1 v1 m2 v2 in - C.list_fold_left2 f map r m1.s m2.s + C.list_iter2 f map m1.s m2.s (* Interface functions ******************************************************) @@ -214,16 +188,25 @@ let get f m i = let f c = f in get f m i -let assert_conversion f ?(si=false) ?(rt=false) mw u w v = - let f mu u = - L.box level; log2 "Now converting" mu.c u mw.c w; - let f r = - if r then begin L.unbox level; f () end else error3 mw.c v w u - in - let g r = if r then f r else ac f ~si true mu u mw w in -(* if S.eq mu mw then are_alpha_convertible g u w else *) g false - in - if rt then domain f mw u else f mw u +let xwhd f m t = + L.box level; log1 "Now scanning" m.c t; + let f m _ t = L.unbox level; f m t in + step f ~delta:true ~rt:true m t -let message1 st m t = - L.ct_items1 "In the context" m.c st 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 +(* 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 diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index dd97b0d4d..01ad7e7a6 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -9,8 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception TypeError of Brg.message - type machine val empty_machine: machine @@ -19,10 +17,16 @@ val get: (Brg.bind -> 'a) -> machine -> int -> 'a val push: (machine -> 'a) -> machine -> Brg.bind -> 'a -(* arguments: expected type, inferred type, typed term *) -val assert_conversion: - (unit -> 'a) -> ?si:bool -> ?rt:bool -> - machine -> Brg.term -> Brg.term -> Brg.term -> 'a +val xwhd: (machine -> Brg.term -> 'a) -> machine -> Brg.term -> 'a + +(* arguments: expected type, inferred type *) +val are_convertible: + (unit -> 'a) -> (unit -> 'a) -> + ?si:bool -> machine -> Brg.term -> machine -> Brg.term -> 'a val message1: - string -> machine -> Brg.term -> (Brg.context, Brg.term) Log.message + string -> machine -> Brg.term -> Brg.message + +val message3: + string -> string -> ?sm3:string -> string -> + machine -> Brg.term -> Brg.term -> ?m3:machine -> Brg.term -> Brg.message diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index 97872734b..885f1bd8d 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -20,6 +20,8 @@ module E = BrgEnvironment module S = BrgSubstitution module R = BrgReduction +exception TypeError of B.message + (* Internal functions *******************************************************) let level = 4 @@ -29,9 +31,33 @@ let log1 s m t = L.log O.specs level (R.message1 s m t) let error1 s m t = - raise (R.TypeError (R.message1 s m t)) + raise (TypeError (R.message1 s m t)) -(* Interface functions ******************************************************) +let message3 m t1 t2 ?mu t3 = + let st1, st2 = "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 + | None -> + let st3 = "but it must be of type" in + R.message3 st1 st2 st3 m t1 t2 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 + 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 + R.are_convertible err f ~si mu u m w + | _ -> error1 "not a function type" m u + in + R.xwhd f m u let rec b_type_of f ~si g m x = log1 "Now checking" m x; @@ -85,18 +111,20 @@ let rec b_type_of f ~si g m x = | 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 - R.assert_conversion f ~si ~rt:true m tt vv xv + 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 - R.assert_conversion f ~si m xu tt xt + assert_convertibility f ~si m xu tt xt in let f xu _ = b_type_of (f xu) ~si g m t in type_of f ~si g m u +(* Interface functions ******************************************************) + and type_of f ?(si=false) g m x = let f t u = L.unbox level; f t u in L.box level; b_type_of f ~si g m x diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index 215132378..78c49ae8b 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +exception TypeError of Brg.message + val type_of: (Brg.term -> Brg.term -> 'a) -> ?si:bool -> Hierarchy.graph -> BrgReduction.machine -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml index 75f8bcd37..e42faba49 100644 --- a/helm/software/lambda-delta/lib/cps.ml +++ b/helm/software/lambda-delta/lib/cps.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -let err () = assert false +let err _ = assert false let start x = x @@ -66,6 +66,10 @@ let rec list_fold_left2 f map a l1 l2 = match l1, l2 with map f a hd1 hd2 | _ -> assert false +let list_iter2 f map l1 l2 = + let map f () x1 x2 = map f x1 x2 in + list_fold_left2 f map () l1 l2 + let rec list_mem ?(eq=(=)) a = function | [] -> false | hd :: _ when eq a hd -> true diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index 39cc5837a..2d3f07517 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -73,10 +73,20 @@ let t_items1 st c t = let ct_items1 sc c st t = [Warn sc; Context c; Warn st; Term (c, t)] -let ct_items2 sc1 c1 st1 t1 sc2 c2 st2 t2 = - ct_items1 sc1 c1 st1 t1 @ ct_items1 sc2 c2 st2 t2 - -let ct_items3 sc c st1 t1 st2 t2 st3 t3 = - ct_items1 sc c st1 t1 @ [Warn st2; Term (c, t2); Warn st3; Term (c, t3)] +let ct_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 = + let tl = match sc2, c2 with + | Some sc2, Some c2 -> ct_items1 sc2 c2 st2 t2 + | None, None -> t_items1 st2 c1 t2 + | _ -> assert false + in + ct_items1 sc1 c1 st1 t1 @ tl + +let ct_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 = + let tl = match sc3, c3 with + | Some sc3, Some c3 -> ct_items1 sc3 c3 st3 t3 + | None, None -> t_items1 st3 c1 t3 + | _ -> assert false + in + ct_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl 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 b5bc99adf..0de107325 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -50,9 +50,12 @@ val ct_items1: string -> 'a -> string -> 'b -> ('a, 'b) message val ct_items2: - string -> 'a -> string -> 'b -> string -> 'a -> string -> 'b -> + string -> 'a -> string -> 'b -> + ?sc2:string -> ?c2:'a -> string -> 'b -> ('a, 'b) message val ct_items3: - string -> 'a -> string -> 'b -> string -> 'b -> string -> 'b -> + string -> 'a -> string -> 'b -> + ?sc2:string -> ?c2:'a -> string -> 'b -> + ?sc3:string -> ?c3:'a -> string -> 'b -> ('a, 'b) message diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 469078668..6a8b92f08 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -24,11 +24,11 @@ module ML = MetaLibrary module MBrg = MetaBrg module G = Library module BrgO = BrgOutput -module BrgR = BrgReduction +module BrgT = BrgType module BrgU = BrgUntrusted module MBag = MetaBag module BagO = BagOutput -module BagR = BagReduction +module BagT = BagType module BagU = BagUntrusted type status = { @@ -106,7 +106,7 @@ let type_check f st si g k = let main = try - let version_string = "Helena 0.8.0 M - August 2009" in + let version_string = "Helena 0.8.0 M - September 2009" in let stage = ref 3 in let moch = ref None in let meta = ref false in @@ -238,5 +238,5 @@ try ("-s", Arg.Int set_stage, help_s); ("-x", Arg.Set export, help_x) ] read_file help; -with BagR.TypeError msg -> bag_error "Type Error" msg - | BrgR.TypeError msg -> brg_error "Type Error" msg +with BagT.TypeError msg -> bag_error "Type Error" msg + | BrgT.TypeError msg -> brg_error "Type Error" msg -- 2.39.2