From 2e451dca46e509fd7e7772f3d2e438c189ce10a1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 3 Nov 2009 17:06:32 +0000 Subject: [PATCH] basic_rg: reduction was not tail recursive by mistake --- helm/software/lambda-delta/.depend.opt | 4 +- .../lambda-delta/basic_ag/bagOutput.ml | 1 + .../lambda-delta/basic_ag/bagReduction.ml | 1 + .../software/lambda-delta/basic_ag/bagType.ml | 1 + .../lambda-delta/basic_ag/bagUntrusted.ml | 1 + helm/software/lambda-delta/basic_rg/brg.ml | 12 +- .../lambda-delta/basic_rg/brgEnvironment.ml | 9 +- .../lambda-delta/basic_rg/brgEnvironment.mli | 4 +- .../lambda-delta/basic_rg/brgOutput.ml | 24 +-- .../lambda-delta/basic_rg/brgReduction.ml | 158 +++++++++--------- .../lambda-delta/basic_rg/brgReduction.mli | 9 +- .../lambda-delta/basic_rg/brgSubstitution.ml | 12 +- .../lambda-delta/basic_rg/brgSubstitution.mli | 2 +- .../software/lambda-delta/basic_rg/brgType.ml | 68 ++++---- .../lambda-delta/basic_rg/brgType.mli | 2 +- .../lambda-delta/basic_rg/brgUntrusted.ml | 15 +- helm/software/lambda-delta/common/entity.ml | 15 +- .../software/lambda-delta/common/hierarchy.ml | 6 +- helm/software/lambda-delta/common/library.ml | 10 +- .../software/lambda-delta/toplevel/metaBrg.ml | 9 +- .../lambda-delta/toplevel/metaOutput.ml | 2 + helm/software/lambda-delta/toplevel/top.ml | 87 +++++----- 22 files changed, 236 insertions(+), 216 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 00b1db36f..f0d13c9a2 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -87,14 +87,14 @@ basic_rg/brgEnvironment.cmx: lib/nUri.cmx common/entity.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: lib/log.cmi common/entity.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmo: lib/share.cmx common/output.cmi lib/nUri.cmi \ lib/log.cmi common/entity.cmx lib/cps.cmx basic_rg/brgOutput.cmi \ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi basic_rg/brgReduction.cmx: lib/share.cmx common/output.cmx lib/nUri.cmx \ lib/log.cmx common/entity.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/log.cmi common/hierarchy.cmi \ +basic_rg/brgType.cmi: lib/log.cmi common/hierarchy.cmi common/entity.cmx \ basic_rg/brgReduction.cmi basic_rg/brg.cmx basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ common/hierarchy.cmi common/entity.cmx lib/cps.cmx \ diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index a97219120..763f61af4 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -70,6 +70,7 @@ let count_entity f c = function | _, _, Y.Abbr v -> let c = {c with eabbrs = succ c.eabbrs} in count_term f c v + | _, _, Y.Void -> assert false let print_counters f c = let terms = diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index a05d4b5d6..b7eb88f63 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -120,6 +120,7 @@ let rec ho_whd f c m x = | GRef_ (_, _, Y.Abst w) -> ho_whd f c m w | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v | LRef_ (_, None) -> assert false + | GRef_ (_, _, Y.Void) -> assert false in whd aux c m x diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index 1bc6fb225..30d8ac48b 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -68,6 +68,7 @@ let rec b_type_of f ~si g c x = | _, _, Y.Abst w -> f x w | _, _, Y.Abbr (B.Cast (w, v)) -> f x w | _, _, Y.Abbr _ -> assert false + | _, _, Y.Void -> assert false in E.get_entity f uri | B.Bind (l, id, B.Abbr v, t) -> diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml index 08a1750c4..8c6cbb47e 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml @@ -26,3 +26,4 @@ let type_check f ?(si=false) g = function | a, uri, Y.Abbr t -> let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in L.loc := U.string_of_uri uri; T.type_of f ~si g B.empty_lenv t + | _, _, Y.Void -> assert false diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index baa83afed..e77682381 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -60,8 +60,7 @@ let bind_abbr a v t = Bind (Abbr (a, v), t) let empty_lenv = Null -let push f es ?c b = - let es = Cons (es, c, b) in f es +let push es ?c b = Cons (es, c, b) let get err f es i = let rec aux j = function @@ -72,6 +71,7 @@ let get err f es i = in aux i es +(* check closure *) let rec rev_iter f map = function | Null -> f () | Cons (tl, None, b) -> @@ -79,8 +79,6 @@ let rec rev_iter f map = function | Cons (tl, Some c, b) -> let f _ = map f c b in rev_iter f map tl -let rec fold_left f map x = function - | Null -> f x - | Cons (tl, _, b) -> - let f x = fold_left f map x tl in - map f x b +let rec fold_left map x = function + | Null -> x + | Cons (tl, _, b) -> fold_left map (map x b) tl diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml index 5a4cf3cb6..121da88da 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml @@ -25,10 +25,11 @@ let get_age = (* Interface functions ******************************************************) -let set_entity f (a, uri, b) = +(* decps *) +let set_entity (a, uri, b) = let age = get_age () in let entity = (Y.Apix age :: a), uri, b in - H.add env uri entity; f entity + H.add env uri entity; entity -let get_entity err f uri = - try f (H.find env uri) with Not_found -> err () +let get_entity uri = + try H.find env uri with Not_found -> [], uri, Y.Void diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli index 5f5d86bf3..1f51f1e61 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli @@ -9,6 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val set_entity: (Brg.entity -> 'a) -> Brg.entity -> 'a +val set_entity: Brg.entity -> Brg.entity -val get_entity: (unit -> 'a) -> (Brg.entity -> 'a) -> Brg.uri -> 'a +val get_entity: Brg.uri -> Brg.entity diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 58a407f04..a9cec439a 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -86,8 +86,7 @@ and count_term f c e = function let f c = count_term f c e t in count_term f c e v | B.Bind (b, t) -> - let f c e = count_term f c e t in - let f c = B.push (f c) e b in + let f c = count_term f c (B.push e b) t in count_term_binder f c e b let count_entity f c = function @@ -99,6 +98,7 @@ let count_entity f c = function | _, _, Y.Abbr v -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in count_term f c B.empty_lenv v + | _, _, Y.Void -> assert false let print_counters f c = let terms = @@ -186,20 +186,22 @@ let rec pp_term c frm = function | B.Appl (_, v, t) -> F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t | B.Bind (B.Abst (a, w), t) -> - let f a cc = - F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t + let f a = + let cc = B.push c (B.abst a w) in + F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t in - let f a = B.push (f a) c (B.abst a w) in rename f c a | B.Bind (B.Abbr (a, v), t) -> - let f a cc = - F.fprintf frm "@[[%a=%a].%a@]" name a (pp_term c) v (pp_term cc) t + let f a = + let cc = B.push c (B.abbr a v) in + F.fprintf frm "@[[%a=%a].%a@]" name a (pp_term c) v (pp_term cc) t in - let f a = B.push (f a) c (B.abbr a v) in rename f c a | B.Bind (B.Void a, t) -> - let f a cc = F.fprintf frm "@[[%a].%a@]" name a (pp_term cc) t in - let f a = B.push (f a) c (B.Void a) in + let f a = + let cc = B.push c (B.Void a) in + F.fprintf frm "@[[%a].%a@]" name a (pp_term cc) t + in rename f c a let pp_lenv frm c = @@ -255,7 +257,7 @@ let rec exp_term e t out tab = match t with | B.Bind (b, t) -> let b = rename_bind C.start e b in exp_bind e b out tab; - exp_term (B.push C.start e b) t out tab + exp_term (B.push e b) t out tab and exp_bind e b out tab = match b with | B.Abst (a, w) -> diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 12e637659..43911dab1 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -37,6 +37,12 @@ let log2 s cu u ct t = let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) +let rec list_and map = function + | hd1 :: tl1, hd2 :: tl2 -> + if map hd1 hd2 then list_and map (tl1, tl2) else false + | l1, l2 -> l1 = l2 + +(* check closure *) let are_alpha_convertible err f t1 t2 = let rec aux f = function | B.Sort (_, p1), B.Sort (_, p2) @@ -60,122 +66,117 @@ let are_alpha_convertible err f t1 t2 = in if S.eq t1 t2 then f () else aux f (t1, t2) -let get err f m i = - B.get err f m.c i +let get m i = + let f c b = c, b in + B.get C.err f m.c i (* to share *) -let rec step f ?(delta=false) ?(rt=false) m x = +let rec step st m x = (* L.warn "entering R.step"; *) match x with - | B.Sort _ -> f m None x + | B.Sort _ -> m, None, x | B.GRef (_, uri) -> - let f = function - | _, _, Y.Abbr v when delta -> - P.add ~gdelta:1 (); step f ~delta ~rt m v - | _, _, Y.Abst w when rt -> - P.add ~grt:1 (); step f ~delta ~rt m w - | a, _, Y.Abbr v -> - let f e = f m (Some (e, B.Abbr (a, v))) x in - Y.apix C.err f a - | a, _, Y.Abst w -> - let f e = f m (Some (e, B.Abst (a, w))) x in - Y.apix C.err f a - in - E.get_entity C.err f uri + begin match E.get_entity uri with + | _, _, Y.Abbr v when st.Y.delta -> + P.add ~gdelta:1 (); step st m v + | _, _, Y.Abst w when st.Y.rt -> + P.add ~grt:1 (); step st m w + | a, _, Y.Abbr v -> + let e = Y.apix C.err C.start a in + m, Some (e, B.Abbr (a, v)), x + | a, _, Y.Abst w -> + let e = Y.apix C.err C.start a in + m, Some (e, B.Abst (a, w)), x + | _, _, Y.Void -> assert false + end | B.LRef (_, i) -> - let f c = function - | B.Abbr (_, v) -> + begin match get m i with + | c, B.Abbr (_, v) -> P.add ~ldelta:1 (); - step f ~delta ~rt {m with c = c} v - | B.Abst (_, w) when rt -> + step st {m with c = c} v + | c, B.Abst (_, w) when st.Y.rt -> P.add ~lrt:1 (); - step f ~delta ~rt {m with c = c} w - | B.Void _ -> + step st {m with c = c} w + | c, B.Void _ -> assert false - | B.Abst (a, _) as b -> - let f e = f {m with c = c} (Some (e, b)) x in - Y.apix C.err f a - in - get C.err f m i + | c, (B.Abst (a, _) as b) -> + let e = Y.apix C.err C.start a in + {m with c = c}, Some (e, b), x + end | B.Cast (_, _, t) -> P.add ~tau:1 (); - step f ~delta ~rt m t + step st m t | B.Appl (_, v, t) -> - step f ~delta ~rt {m with s = (m.c, v) :: m.s} t + step st {m with s = (m.c, v) :: m.s} t | B.Bind (B.Abst (a, w), t) -> begin match m.s with - | [] -> f m None x + | [] -> m, None, x | (c, v) :: s -> P.add ~beta:1 ~upsilon:(List.length s) (); - let f c = step f ~delta ~rt {m with c = c; s = s} t in - B.push f m.c ~c (B.abbr a v) (* (B.Cast ([], w, v)) *) + let c = B.push m.c ~c (B.abbr a v) (* (B.Cast ([], w, v)) *) in + step st {m with c = c; s = s} t end | B.Bind (b, t) -> P.add ~upsilon:(List.length m.s) (); - let f c = step f ~delta ~rt {m with c = c} t in - B.push f m.c ~c:m.c b + let c = B.push m.c ~c:m.c b in + step st {m with c = c} t -let push f m b = +let push m b = assert (m.s = []); let b, i = match b with | B.Abst (a, w) -> B.abst (Y.Apix m.i :: a) w, succ m.i | b -> b, m.i in - let f c = f {m with c = c; i = i} in - B.push f m.c ~c:m.c b + let c = B.push m.c ~c:m.c b in + {m with c = c; i = i} -let rec ac_nfs err f ~si m1 a1 u m2 a2 t = +let rec ac_nfs st (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 () else err () + h1 = h2 | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _ -> - if e1 = e2 then ac_stacks err f m1 m2 else err () + if e1 = e2 then ac_stacks st m1 m2 else false | 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 - ac_stacks err f m1 m2 + if ac_stacks st m1 m2 then true else begin + P.add ~gdelta:2 (); ac st m1 v1 m2 v2 + end else if e1 < e2 then begin P.add ~gdelta:1 (); - step (ac_nfs err f ~si m1 a1 u) m2 v2 + ac_nfs st (m1, a1, u) (step st m2 v2) end else begin P.add ~gdelta:1 (); - step (ac_nfs_rev err f ~si m2 a2 t) m1 v1 + ac_nfs st (step st m1 v1) (m2, a2, t) end | _, _, Some (_, B.Abbr (_, v2)), _ -> P.add ~gdelta:1 (); - step (ac_nfs err f ~si m1 a1 u) m2 v2 + ac_nfs st (m1, a1, u) (step st m2 v2) | Some (_, B.Abbr (_, v1)), _, _, _ -> P.add ~gdelta:1 (); - step (ac_nfs_rev err f ~si m2 a2 t) m1 v1 + ac_nfs st (step st m1 v1) (m2, a2, t) | _, B.Bind ((B.Abst (_, w1) as b1), t1), _, 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 - ac err f ~si:false m1 w1 m2 w2 - | _, B.Sort _, _, B.Bind (b, t) when si -> + if ac {st with Y.si = false} m1 w1 m2 w2 then + ac st (push m1 b1) t1 (push m2 b2) t2 + else false + | _, B.Sort _, _, B.Bind (b, t) when st.Y.si -> P.add ~si:1 (); - 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 - | _ -> err () - -and ac_nfs_rev err f ~si m2 a2 t m1 a1 u = ac_nfs err f ~si m1 a1 u m2 a2 t + ac st (push m1 b) u (push m2 b) t + | _ -> false -and ac err f ~si m1 t1 m2 t2 = +and ac st m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) - let f m1 a1 t1 = step (ac_nfs err f ~si m1 a1 t1) m2 t2 in - step f m1 t1 + ac_nfs st (step st m1 t1) (step st m2 t2) -and ac_stacks err f m1 m2 = +and ac_stacks st m1 m2 = (* L.warn "entering R.are_convertible_stacks"; *) - if List.length m1.s <> List.length m2.s then err () else - let map f (c1, v1) (c2, v2) = +(* if List.length m1.s <> List.length m2.s then false else *) + let map (c1, v1) (c2, v2) = let m1, m2 = {m1 with c = c1; s = []}, {m2 with c = c2; s = []} in - ac err f ~si:false m1 v1 m2 v2 + ac {st with Y.si = false} m1 v1 m2 v2 in - C.list_iter2 f map m1.s m2.s + list_and map (m1.s, m2.s) (* Interface functions ******************************************************) @@ -186,18 +187,19 @@ let empty_kam = { let get err f m i = assert (m.s = []); let f c = f in - get err f m i - -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 are_convertible err f ?(si=false) mu u mw w = - L.box level; log2 "Now converting" mu.c u mw.c w; - 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 () + B.get err f m.c i + +let xwhd st m t = + L.box level; log1 "Now scanning" m.c t; + let m, _, t = step {st with Y.delta = true; Y.rt = true} m t in + L.unbox level; m, t + +let are_convertible st mu u mw w = + L.box level; log2 "Now converting" mu.c u mw.c w; + let r = ac {st with Y.delta = false; Y.rt = false} mu u mw w in + L.unbox level; r +(* let err _ = in + if S.eq mu mw then are_alpha_convertible err f u w else err () *) (* error reporting **********************************************************) diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index 94f6543e0..840b72fd3 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -15,13 +15,12 @@ val empty_kam: kam val get: (unit -> 'a) -> (Brg.bind -> 'a) -> kam -> int -> 'a -val push: (kam -> 'a) -> kam -> Brg.bind -> 'a +val push: kam -> Brg.bind -> kam -val xwhd: (kam -> Brg.term -> 'a) -> kam -> Brg.term -> 'a +val xwhd: Entity.status -> kam -> Brg.term -> kam * Brg.term (* arguments: expected type, inferred type *) -val are_convertible: - (unit -> 'a) -> (unit -> 'a) -> - ?si:bool -> kam -> Brg.term -> kam -> Brg.term -> 'a +val are_convertible: + Entity.status -> kam -> Brg.term -> kam -> Brg.term -> bool val specs: (kam, Brg.term) Log.specs diff --git a/helm/software/lambda-delta/basic_rg/brgSubstitution.ml b/helm/software/lambda-delta/basic_rg/brgSubstitution.ml index e482b66c0..4355376e8 100644 --- a/helm/software/lambda-delta/basic_rg/brgSubstitution.ml +++ b/helm/software/lambda-delta/basic_rg/brgSubstitution.ml @@ -29,10 +29,10 @@ let iter map d = let lift_map h _ a i = if i + h >= 0 then B.LRef (a, i + h) else assert false -let lift g h d t = - if h = 0 then g t else g (iter (lift_map h) d t) +let lift h d t = + if h = 0 then t else iter (lift_map h) d t -let lift_bind g h d = function - | B.Void _ as b -> g b - | B.Abst (a, w) -> let g w = g (B.abst a w) in lift g h d w - | B.Abbr (a, v) -> let g v = g (B.abbr a v) in lift g h d v +let lift_bind h d = function + | B.Void _ as b -> b + | B.Abst (a, w) -> B.abst a (lift h d w) + | B.Abbr (a, v) -> B.abbr a (lift h d v) diff --git a/helm/software/lambda-delta/basic_rg/brgSubstitution.mli b/helm/software/lambda-delta/basic_rg/brgSubstitution.mli index f20350af6..a1717666f 100644 --- a/helm/software/lambda-delta/basic_rg/brgSubstitution.mli +++ b/helm/software/lambda-delta/basic_rg/brgSubstitution.mli @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val lift: (Brg.term -> 'a) -> int -> int -> Brg.term -> 'a +val lift: int -> int -> Brg.term -> Brg.term (* val lift_bind: (Brg.bind -> 'a) -> int -> int -> Brg.bind -> 'a *) diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index a35a9c32a..0afb9c70b 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -50,21 +50,19 @@ let message3 m t1 t2 ?mu t3 = let error3 err m t1 t2 ?mu t3 = err (message3 m t1 t2 ?mu t3) -let assert_convertibility err f ~si m u w v = - let err _ = error3 err m v w u in - R.are_convertible err f ~si m u m w +let assert_convertibility err f st m u w v = + if R.are_convertible st m u m w then f () else + error3 err m v w u -let assert_applicability err f ~si m u w v = - let f mu = function - | B.Sort _ -> error1 err "not a function type" m u - | B.Bind (B.Abst (_, u), _) -> - let err _ = error3 err m v w ~mu u in - R.are_convertible err f ~si mu u m w - | _ -> assert false - in - R.xwhd f m u +let assert_applicability err f st m u w v = + match R.xwhd st m u with + | _, B.Sort _ -> error1 err "not a function type" m u + | mu, B.Bind (B.Abst (_, u), _) -> + if R.are_convertible st mu u m w then f () else + error3 err m v w ~mu u + | _ -> assert false (**) -let rec b_type_of err f ~si g m x = +let rec b_type_of err f st g m x = log1 "Now checking" m x; match x with | B.Sort (a, h) -> @@ -72,9 +70,9 @@ let rec b_type_of err f ~si g m x = | B.LRef (_, i) -> let f = function | B.Abst (_, w) -> - S.lift (f x) (succ i) (0) w + f x (S.lift (succ i) (0) w) | B.Abbr (_, B.Cast (_, w, _)) -> - S.lift (f x) (succ i) (0) w + f x (S.lift (succ i) (0) w) | B.Abbr _ -> assert false | B.Void _ -> error1 err "reference to excluded variable" m x @@ -82,54 +80,54 @@ let rec b_type_of err f ~si g m x = let err _ = error1 err "reference to unknown variable" m x in R.get err f m i | B.GRef (_, uri) -> - let f = function + begin match E.get_entity uri with | _, _, Y.Abst w -> f x w | _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w | _, _, Y.Abbr _ -> assert false - in - let err _ = error1 err "reference to unknown entry" m x in - E.get_entity err f uri + | _, _, Y.Void -> + error1 err "reference to unknown entry" m x + end | 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) in - let f xv m = b_type_of err (f xv) ~si g m t in - let f xv = R.push (f xv) m (B.abbr a xv) in + let f xv m = b_type_of err (f xv) st g m t in + let f xv = f xv (R.push m (B.abbr a xv)) in let f xv vv = match xv with | B.Cast _ -> f xv | _ -> f (B.Cast ([], vv, xv)) in - type_of err f ~si g m v + type_of err f st g m v | B.Bind (B.Abst (a, u), t) -> let f xu xt tt = f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt) in - let f xu m = b_type_of err (f xu) ~si g m t in - let f xu _ = R.push (f xu) m (B.abst a xu) in - type_of err f ~si g m u + let f xu m = b_type_of err (f xu) st g m t in + let f xu _ = f xu (R.push m (B.abst a xu)) in + type_of err f st g m u | B.Bind (B.Void a as b, t) -> let f xt tt = f (A.sh1 t xt x (B.bind b)) (B.bind b tt) in - let f m = b_type_of err f ~si g m t in - R.push f m b + b_type_of err f st g (R.push m b) t + | 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 - assert_applicability err f ~si m tt vv xv + assert_applicability err f st m tt vv xv in - let f xv vv = b_type_of err (f xv vv) ~si g m t in - type_of err f ~si g m v + let f xv vv = b_type_of err (f xv vv) st g m t in + type_of err f st 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 - assert_convertibility err f ~si m xu tt xt + assert_convertibility err f st m xu tt xt in - let f xu _ = b_type_of err (f xu) ~si g m t in - type_of err f ~si g m u + let f xu _ = b_type_of err (f xu) st g m t in + type_of err f st g m u (* Interface functions ******************************************************) -and type_of err f ?(si=false) g m x = +and type_of err f st g m x = let f t u = L.unbox level; f t u in - L.box level; b_type_of err f ~si g m x + L.box level; b_type_of err f st g m x diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index 2d7a14663..b235b47e9 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -13,4 +13,4 @@ type message = (BrgReduction.kam, Brg.term) Log.message val type_of: (message -> 'a) -> (Brg.term -> Brg.term -> 'a) -> - ?si:bool -> Hierarchy.graph -> BrgReduction.kam -> Brg.term -> 'a + Entity.status -> Hierarchy.graph -> BrgReduction.kam -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index 77098b84e..959a74619 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -22,8 +22,15 @@ module T = BrgType (* to share *) let type_check err f ?(si=false) g = function | a, uri, Y.Abst t -> - let f xt tt = E.set_entity (f tt) (a, uri, Y.Abst xt) in - L.loc := U.string_of_uri uri; T.type_of err f ~si g R.empty_kam t + let f xt tt = + let e = E.set_entity (a, uri, Y.Abst xt) in f tt e + in + let st = Y.initial_status si in + L.loc := U.string_of_uri uri; T.type_of err f st g R.empty_kam t | a, uri, Y.Abbr t -> - let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in - L.loc := U.string_of_uri uri; T.type_of err f ~si g R.empty_kam t + let f xt tt = + let e = E.set_entity (a, uri, Y.Abbr xt) in f tt e + in + let st = Y.initial_status si in + L.loc := U.string_of_uri uri; T.type_of err f st g R.empty_kam t + | _, _, Y.Void -> assert false diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index 7b8dab950..5bef9ff33 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -21,10 +21,17 @@ type attrs = attr list (* attributes *) type 'term bind = Abst of 'term (* declaration: domain *) | Abbr of 'term (* definition: body *) + | Void (* exclusion *) type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *) -type uri_generator = string -> string (* this could be in CPS *) +type uri_generator = string -> string + +type status = { + delta: bool; (* global delta-expansion *) + rt: bool; (* reference typing *) + si: bool (* sort inclusion *) +} (* helpers ******************************************************************) @@ -84,3 +91,9 @@ let xlate f xlate_term = function let f t = f (a, uri, Abst t) in xlate_term f t | a, uri, Abbr t -> let f t = f (a, uri, Abbr t) in xlate_term f t + | _, _, Void -> + assert false + +let initial_status si = { + delta = false; rt = false; si = si +} diff --git a/helm/software/lambda-delta/common/hierarchy.ml b/helm/software/lambda-delta/common/hierarchy.ml index 375390bdc..e00cfc72c 100644 --- a/helm/software/lambda-delta/common/hierarchy.ml +++ b/helm/software/lambda-delta/common/hierarchy.ml @@ -20,13 +20,13 @@ let sort = H.create sorts (* Internal functions *******************************************************) -let set_sort f (h:int) (s:string) = - H.add sort h s; f (succ h) +let set_sort h s = + H.add sort h s; succ h (* Interface functions ******************************************************) let set_sorts f ss i = - C.list_fold_left f set_sort i ss + f (List.fold_left set_sort i ss) let get_sort err f h = try f (H.find sort h) with Not_found -> err () diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index 25bca63a9..61af97921 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -9,8 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module F = Format -module N = Filename +module F = Filename module U = NUri module C = Cps module H = Hierarchy @@ -27,7 +26,7 @@ let root = "ENTITY" let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd" let path_of_uri uri = - N.concat base (Str.string_after (U.string_of_uri uri) 3) + F.concat base (Str.string_after (U.string_of_uri uri) 3) (* interface functions ******************************************************) @@ -108,7 +107,7 @@ let mark a = let export_entity pp_term si g (a, u, b) = let path = path_of_uri u in - let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in + let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in let och = open_out (path ^ obj_ext) in let out = output_string och in xml out "1.0" "UTF-8"; doctype out root system; @@ -116,7 +115,8 @@ let export_entity pp_term si g (a, u, b) = let attrs = [uri u; name a; mark a] in let contents = match b with | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w) - | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) + | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) + | Y.Void -> assert false in let opts = if si then "si" else "" in let shp = H.string_of_graph C.start g in diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index 4ee25812e..ff74f8e75 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -34,22 +34,21 @@ let rec xlate_term c f = function let f w = let a = [Y.Name (id, true)] in let f t = f (B.Bind (B.abst a w, t)) in - let f c = xlate_term c f t in - B.push f c (B.abst a w) + xlate_term (B.push c (B.abst a w)) f t in xlate_term c f w let xlate_pars f pars = let map f (id, w) c = let a = [Y.Name (id, true)] in - let f w = B.push f c (B.abst a w) in + let f w = f (B.push c (B.abst a w)) in xlate_term c f w in C.list_fold_right f map pars B.empty_lenv let unwind_to_xlate_term f c t = - let map f t b = f (B.bind b t) in - let f t = B.fold_left f map t c in + let map t b = B.bind b t in + let f t = f (B.fold_left map t c) in xlate_term c f t let xlate_entry f = function diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index caf3cc960..21d735d0e 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -83,6 +83,7 @@ let count_entity f c = function let f c = count_xterm f c xv in let f c = count_term f c w in Cps.list_fold_left f count_par c pars + | _, _, Y.Void -> assert false let print_counters f c = let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in @@ -155,6 +156,7 @@ let pp_entity frm = function F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" (Y.mark C.err C.start a) (U.string_of_uri uri) pp_pars pars (pp_body a) body pp_term u + | _, _, Y.Void -> assert false let pp_entity f frm entity = pp_entity frm entity; f () diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 12e639c56..1bab9136b 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -55,9 +55,6 @@ let initial_status mk_uri cover = { ast = AP.initial_status } -let count count_fun c entity = - if !L.level > 2 then count_fun C.start c entity else c - let flush_all () = L.flush 0; L.flush_err () let bag_error s msg = @@ -66,9 +63,9 @@ let bag_error s msg = let brg_error s msg = L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all () -let process_entity f st = +let process_entity f st entity = let f ast = f {st with ast = ast} in - AP.process_entity f st.ast + AP.process_entity f st.ast entity (* kernel related ***********************************************************) @@ -85,14 +82,14 @@ let print_counters st = match !kernel with | Brg -> BrgO.print_counters C.start st.brgc | Bag -> BagO.print_counters C.start st.bagc -let xlate f st entity = match !kernel, entity with +let xlate_entity entity = match !kernel, entity with | Brg, CrgEntity e -> - let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e + let f e = (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e | Brg, MetaEntity e -> - let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e + let f e = (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e | Bag, MetaEntity e -> - let f e = f st (BagEntity e) in Y.xlate f MBag.bag_of_meta e - | _, entity -> f st entity + let f e = (BagEntity e) in Y.xlate f MBag.bag_of_meta e + | _, entity -> entity let pp_progress e = let f a u = @@ -108,9 +105,9 @@ let pp_progress e = | MetaEntity e -> Y.common f e let count_entity st = function - | MetaEntity e -> {st with mc = count MO.count_entity st.mc e} - | BrgEntity e -> {st with brgc = count BrgO.count_entity st.brgc e} - | BagEntity e -> {st with bagc = count BagO.count_entity st.bagc e} + | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e} + | BrgEntity e -> {st with brgc = BrgO.count_entity C.start st.brgc e} + | BagEntity e -> {st with bagc = BagO.count_entity C.start st.bagc e} | _ -> st let export_entity si g moch = function @@ -123,14 +120,14 @@ let export_entity si g moch = function end | BagEntity _ -> () -let type_check f st si g k = +let type_check st si g k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in - let ok _ _ = f st in + let ok _ _ = st in match k with | BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity | BagEntity entity -> BagU.type_check ok ~si g entity | CrgEntity _ - | MetaEntity _ -> f st + | MetaEntity _ -> st (****************************************************************************) @@ -146,38 +143,36 @@ let export = ref false let graph = ref (H.graph_of_string C.err C.start "Z2") let old = ref false -let process_3 f st = - f st - -let process_2 f st entity = - let st = count_entity st entity in +let process_2 st entity = + let st = if !L.level > 2 then count_entity st entity else st in if !export then export_entity !si !graph !moch entity; - if !stage > 2 then type_check (process_3 f) st !si !graph entity else f st + if !stage > 2 then type_check st !si !graph entity else st -let process_1 f st entity = +let process_1 st entity = if !progress then pp_progress entity; - let st = count_entity st entity in + let st = if !L.level > 2 then count_entity st entity else st in if !export && !stage = 1 then export_entity !si !graph !moch entity; - if !stage > 1 then xlate (process_2 f) st entity else f st + if !stage > 1 then process_2 st (xlate_entity entity) else st -let process_0 f st entity = +let process_0 st entity = let f st entity = - if !stage = 0 then f st else - let frr mst = f {st with mst = mst} in - let h mst e = process_1 f {st with mst = mst} (MetaEntity e) in - let err dst = f {st with dst = dst} in - let g dst e = process_1 f {st with dst = dst} (CrgEntity e) in + if !stage = 0 then st else + let frr mst = {st with mst = mst} in + let h mst e = process_1 {st with mst = mst} (MetaEntity e) in + let err dst = {st with dst = dst} in + let g dst e = process_1 {st with dst = dst} (CrgEntity e) in if !old then MA.meta_of_aut frr h st.mst entity else DA.crg_of_aut err g st.dst entity in - let st = {st with ac = count AO.count_entity st.ac entity} in + let st = + if !L.level > 2 then {st with ac = AO.count_entity C.start st.ac entity} + else st + in if !preprocess then process_entity f st entity else f st entity -let rec process f book st = match book with - | [] -> f st - | entity :: tl -> -(* we exploit tail recursion rather than CPS *) - process f tl (process_0 C.start st entity) +let rec process st = function + | [] -> st + | entity :: tl -> process (process_0 st entity) tl (****************************************************************************) @@ -225,15 +220,15 @@ try | Bag -> Bag.mk_uri in let cover = if !use_cover then base_name else "" in - let f st = - if !L.level > 0 then T.utime_stamp "processed"; - if !L.level > 2 then AO.print_counters C.start st.ac; - if !L.level > 2 && !preprocess then AO.print_process_counters C.start st.ast; - if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc; - if !L.level > 2 && !stage > 1 then print_counters st; - if !L.level > 2 && !stage > 1 then O.print_reductions () - in - process f book (initial_status mk_uri cover) + let st = process (initial_status mk_uri cover) book in + if !L.level > 0 then T.utime_stamp "processed"; + if !L.level > 2 then begin + AO.print_counters C.start st.ac; + if !preprocess then AO.print_process_counters C.start st.ast; + if !stage > 0 then MO.print_counters C.start st.mc; + if !stage > 1 then print_counters st; + if !stage > 2 then O.print_reductions () + end in let exit () = close !moch; -- 2.39.2