From a46a0dcfd97373045074ad421df89a66e3199628 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 10 Nov 2014 19:40:58 +0000 Subject: [PATCH] the commit contnues by updating the RTM and modifying the typechecker accordingly --- helm/software/helena/.depend.opt | 14 +- .../helena/src/basic_rg/brgReduction.ml | 166 +++++++++++------- .../helena/src/basic_rg/brgReduction.mli | 6 +- helm/software/helena/src/basic_rg/brgType.ml | 8 +- 4 files changed, 114 insertions(+), 80 deletions(-) diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index 8843aa957..8f1a57695 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -153,14 +153,14 @@ src/basic_rg/brgReduction.cmx: src/common/status.cmx src/lib/share.cmx \ src/common/ccs.cmx src/basic_rg/brgOutput.cmx \ src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgReduction.cmi -src/basic_rg/brgValid.cmi: src/common/status.cmx \ +src/basic_rg/brgValidity.cmi: src/common/status.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx -src/basic_rg/brgValid.cmo: src/lib/log.cmi src/common/entity.cmx \ +src/basic_rg/brgValidity.cmo: src/lib/log.cmi src/common/entity.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \ - src/basic_rg/brg.cmx src/basic_rg/brgValid.cmi -src/basic_rg/brgValid.cmx: src/lib/log.cmx src/common/entity.cmx \ + src/basic_rg/brg.cmx src/basic_rg/brgValidity.cmi +src/basic_rg/brgValidity.cmx: src/lib/log.cmx src/common/entity.cmx \ src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgValid.cmi + src/basic_rg/brg.cmx src/basic_rg/brgValidity.cmi src/basic_rg/brgType.cmi: src/common/status.cmx src/basic_rg/brgReduction.cmi \ src/basic_rg/brg.cmx src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \ @@ -176,11 +176,11 @@ src/basic_rg/brgType.cmx: src/lib/share.cmx src/lib/log.cmx \ src/basic_rg/brgUntrusted.cmi: src/common/status.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \ - src/basic_rg/brgValid.cmi src/basic_rg/brgType.cmi \ + src/basic_rg/brgValidity.cmi src/basic_rg/brgType.cmi \ src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \ src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi src/basic_rg/brgUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \ - src/basic_rg/brgValid.cmx src/basic_rg/brgType.cmx \ + src/basic_rg/brgValidity.cmx src/basic_rg/brgType.cmx \ src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \ src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 98747ab55..d4b5e68fd 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -13,6 +13,7 @@ module U = NUri module C = Cps module W = Share module L = Log +module H = Hierarchy module E = Entity module N = Level module O = Output @@ -23,11 +24,15 @@ module BO = BrgOutput module BE = BrgEnvironment type kam = { - e: B.lenv; (* environment *) - s: (B.lenv * B.term) list; (* stack *) - d: int (* depth *) + e: B.lenv; (* environment *) + s: (B.lenv * B.term) list; (* stack *) + l: int; (* level *) + d: int; (* inferred type iterations *) + n: int option; (* expected type iterations *) } +type message = (kam, B.term) L.message + (* Internal functions *******************************************************) let level = 5 @@ -37,7 +42,7 @@ let log1 s c t = L.log BO.specs level (L.et_items1 sc c st t) let log2 s cu u ct t = - let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in + let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in L.log BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) let rec list_and map = function @@ -45,6 +50,8 @@ let rec list_and map = function if map hd1 hd2 then list_and map (tl1, tl2) else false | l1, l2 -> l1 = l2 +let zero = Some 0 + (* check closure *) let are_alpha_convertible err f t1 t2 = let rec aux f = function @@ -69,50 +76,64 @@ let are_alpha_convertible err f t1 t2 = in if W.eq t1 t2 then f () else aux f (t1, t2) +let assert_tstep m vo = match m.n with + | Some n -> n > m.d + | None -> vo + +let tstep m = {m with d = succ m.d} + let get m i = let _, c, a, b = B.get m.e i in c, a, b (* to share *) let rec step st m x = -(* L.warn "entering R.step"; *) + log1 (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x; match x with - | B.Sort _ -> m, None, x + | B.Sort (a, h) -> + if assert_tstep m false then + step st (tstep m) (B.Sort (a, H.apply h)) + else m, x, None | B.GRef (_, uri) -> begin match BE.get_entity uri with - | _, _, E.Abbr v when st.S.delta -> + | _, _, E.Abbr v when st.S.delta -> O.add ~gdelta:1 (); step st m v - | _, _, E.Abst (_, w) when st.S.rt -> - O.add ~grt:1 (); step st m w - | a, _, E.Abbr v -> - let e = E.apix C.err C.start a in - m, Some (e, a, B.Abbr v), x - | a, _, E.Abst (n, w) -> - let e = E.apix C.err C.start a in - m, Some (e, a, B.Abst (n, w)), x - | _, _, E.Void -> assert false + | _, _, E.Abst (_, w) when assert_tstep m true -> + O.add ~grt:1 (); step st (tstep m) w + | _, _, E.Abbr v -> + m, x, Some v + | _, _, E.Abst _ -> + m, x, None + | _, _, E.Void -> + assert false end | B.LRef (_, i) -> begin match get m i with - | c, _, B.Abbr v -> + | c, _, B.Abbr v -> O.add ~ldelta:1 (); step st {m with e = c} v - | c, _, B.Abst (_, w) when st.S.rt -> + | c, _, B.Abst (_, w) when assert_tstep m true -> O.add ~lrt:1 (); - step st {m with e = c} w - | c, _, B.Void -> + step st {(tstep m) with e = c} w + | _, a, B.Abst _ -> + m, B.LRef (a, i), None + | _, _, B.Void -> assert false - | c, a, (B.Abst _ as b) -> - let e = E.apix C.err C.start a in - {m with e = c}, Some (e, a, b), x end - | B.Cast (_, _, t) -> - O.add ~tau:1 (); - step st m t + | B.Cast (_, u, t) -> + if assert_tstep m false then begin + O.add ~e:1 (); + step st (tstep m) u + end else begin + O.add ~epsilon:1 (); + step st m t + end | B.Appl (_, v, t) -> step st {m with s = (m.e, v) :: m.s} t | B.Bind (a, B.Abst (n, w), t) -> + let n = N.minus n m.d in + let x = B.Bind (a, B.Abst (n, w), t) in begin match m.s with - | [] -> m, None, x + | [] -> m, x, None | (c, v) :: s -> if N.is_zero n then Q.add_nonzero st.S.cc a; O.add ~beta:1 ~theta:(List.length s) (); @@ -124,51 +145,64 @@ let rec step st m x = let e = B.push m.e m.e a b in step st {m with e = e} t +let reset m ?(e=m.e) n = + {m with e = e; n = n; s = []; d = 0} + +let assert_iterations m1 m2 = match m1.n, m2.n with + | Some n1, Some n2 -> n1 - m1.d = n2 - m2.d + | _ -> false + let push m a b = assert (m.s = []); - let a, d = match b with - | B.Abst _ -> E.Apix m.d :: a, succ m.d - | b -> a, m.d + let a, l = match b with + | B.Abst _ -> E.Apix m.l :: a, succ m.l + | b -> a, m.l in let e = B.push m.e m.e a b in - {m with e = e; d = d} - -let rec ac_nfs st (m1, r1, u) (m2, r2, t) = - log2 "Now converting nfs" m1.e u m2.e t; - match r1, u, r2, t with - | _, B.Sort (_, h1), _, B.Sort (_, h2) -> - h1 = h2 - | Some (e1, _, B.Abst _), _, Some (e2, _, B.Abst _), _ -> + {m with e = e; l = l} + +let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = + log2 "Now converting nfs" m1.e t1 m2.e t2; + match t1, r1, t2, r2 with + | B.Sort (_, h1), _, B.Sort (_, h2), _ -> + h1 = h2 + | B.LRef (a1, _), _, B.LRef (a2, _), _ -> + let e1 = E.apix C.err C.start a1 in + let e2 = E.apix C.err C.start a2 in 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 - if ac_stacks st m1 m2 then true else begin - O.add ~gdelta:2 (); ac st m1 v1 m2 v2 - end - else if e1 < e2 then begin + | B.GRef (_, u1), None, B.GRef (_, u2), None -> + if U.eq u1 u2 & assert_iterations m1 m2 then ac_stacks st m1 m2 else false + | B.GRef (a1, u1), Some v1, B.GRef (a2, u2), Some v2 -> + let e1 = E.apix C.err C.start a1 in + let e2 = E.apix C.err C.start a2 in + if e1 < e2 then begin O.add ~gdelta:1 (); - ac_nfs st (m1, r1, u) (step st m2 v2) - end else begin + ac_nfs st (m1, t1, r1) (step st m2 v2) + end else if e2 < e1 then begin O.add ~gdelta:1 (); - ac_nfs st (step st m1 v1) (m2, r2, t) - end - | _, _, Some (_, _, B.Abbr v2), _ -> - O.add ~gdelta:1 (); - ac_nfs st (m1, r1, u) (step st m2 v2) - | Some (_, _, B.Abbr v1), _, _, _ -> + ac_nfs st (step st m1 v1) (m2, t2, r2) + end else if U.eq u1 u2 & assert_iterations m1 m2 && ac_stacks st m1 m2 then true + else begin + O.add ~gdelta:2 (); + ac st m1 v1 m2 v2 + end + | _, _, B.GRef _, Some v2 -> O.add ~gdelta:1 (); - ac_nfs st (step st m1 v1) (m2, r2, t) - | _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1), - _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) -> + ac_nfs st (m1, t1, r1) (step st m2 v2) + | B.GRef _, Some v1, _, _ -> + O.add ~gdelta:1 (); + ac_nfs st (step st m1 v1) (m2, t2, r2) + | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _, + B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _ -> if n1 = n2 then () else Q.add_equal st.S.cc a1 a2; - if ac {st with S.si = false} m1 w1 m2 w2 then + if ac {st with S.si = false} (reset m1 zero) w1 (reset m2 zero) w2 then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2 else false - | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t) -> + | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ -> if N.is_zero n then () else Q.add_zero st.S.cc a; O.add ~si:1 (); - ac st (push m1 a b) u (push m2 a b) t - | _ -> false + ac st (push m1 a b) t1 (push m2 a b) t + | _ -> false and ac st m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) @@ -178,7 +212,7 @@ and ac_stacks st m1 m2 = (* L.warn "entering R.are_convertible_stacks"; *) if List.length m1.s <> List.length m2.s then false else let map (c1, v1) (c2, v2) = - let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in + let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in ac {st with S.si = false} m1 v1 m2 v2 in list_and map (m1.s, m2.s) @@ -186,21 +220,21 @@ and ac_stacks st m1 m2 = (* Interface functions ******************************************************) let empty_kam = { - e = B.empty; s = []; d = 0 + e = B.empty; s = []; l = 0; d = 0; n = None } let get m i = assert (m.s = []); let _, _, _, b = B.get m.e i in b -let xwhd st m t = +let xwhd st m n t = L.box level; log1 "Now scanning" m.e t; - let m, _, t = step {st with S.delta = true; S.rt = true} m t in + let m, t, _ = step {st with S.delta = true} (reset m n) t in L.unbox level; m, t -let are_convertible st mu u mw w = - L.box level; log2 "Now converting" mu.e u mw.e w; - let r = ac {st with S.delta = st.S.expand; S.rt = false} mu u mw w in +let are_convertible st m1 n1 t1 m2 n2 t2 = + L.box level; log2 "Now converting" m1.e t1 m2.e t2; + let r = ac {st with S.delta = st.S.expand} (reset m1 n1) t1 (reset m2 n2) t2 in L.unbox level; r (* let err _ = in if W.eq mu mw then are_alpha_convertible err f u w else err () *) diff --git a/helm/software/helena/src/basic_rg/brgReduction.mli b/helm/software/helena/src/basic_rg/brgReduction.mli index e8df9f7aa..e73d2df8a 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.mli +++ b/helm/software/helena/src/basic_rg/brgReduction.mli @@ -11,16 +11,18 @@ type kam +type message = (kam, Brg.term) Log.message + val empty_kam: kam val get: kam -> int -> Brg.bind val push: kam -> Entity.attrs -> Brg.bind -> kam -val xwhd: Status.status -> kam -> Brg.term -> kam * Brg.term +val xwhd: Status.status -> kam -> int option -> Brg.term -> kam * Brg.term (* arguments: expected type, inferred type *) val are_convertible: - Status.status -> kam -> Brg.term -> kam -> Brg.term -> bool + Status.status -> kam -> int option -> Brg.term -> kam -> int option -> Brg.term -> bool val specs: (kam, Brg.term) Log.specs diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml index f23da87d0..9dcce08a6 100644 --- a/helm/software/helena/src/basic_rg/brgType.ml +++ b/helm/software/helena/src/basic_rg/brgType.ml @@ -21,8 +21,6 @@ module BE = BrgEnvironment module BS = BrgSubstitution module BR = BrgReduction -type message = (BR.kam, B.term) Log.message - (* Internal functions *******************************************************) let level = 4 @@ -51,15 +49,15 @@ let error3 err m t1 t2 ?mu t3 = err (message3 m t1 t2 ?mu t3) let assert_convertibility err f st m u w v = - if BR.are_convertible st m u m w then f () else + if BR.are_convertible st m (Some 0) u m (Some 0) w then f () else error3 err m v w u let assert_applicability err f st m u w v = - match BR.xwhd st m u with + match BR.xwhd st m None u with | _, B.Sort _ -> error1 err "not a function type" m u | mu, B.Bind (_, B.Abst (_, u), _) -> - if BR.are_convertible st mu u m w then f () else + if BR.are_convertible st mu (Some 0) u m (Some 0) w then f () else error3 err m v w ~mu u | _ -> assert false (**) -- 2.39.2