X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgReduction.ml;h=3b4820abf5fdc0eaf6e9fbc0b78d1f6b0d00df14;hb=94c6cfe7e6b833190904c6b546668d716978a812;hp=16dc395bbfe39c7eb6e4c94a1936ae2ff2874705;hpb=29cfb9e2961e62c836cb50217905c0594a074e81;p=helm.git diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 16dc395bb..3b4820abf 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -18,7 +18,7 @@ module O = BrgOutput module E = BrgEnvironment module S = BrgSubstitution -exception LRefNotFound of B.message +exception TypeError of B.message type machine = { c: B.context; @@ -29,44 +29,49 @@ type machine = { 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 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 empty_machine = { - c = B.empty_context; s = [] +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 empty_machine c = { + c = c; s = [] } -let get f c m i = +let get f m i = let f e = function | Some (_, b) -> f e b - | None -> error i + | None -> error0 i in - let f c = B.get f c i in - B.append f c m.c + B.get f m.c i let lift_stack f s = let map f (v, i) = f (v, succ i) in Cps.list_map f map s -let unwind_to_term f m t = - let map f t (a, b) = f (B.Bind (a, b, t)) in - let f mc = C.list_fold_left f map t mc in - assert (m.s = []); - B.contents f m.c - let push f m a b = assert (m.s = []); f {m with c = (a, b) :: m.c} (* to share *) -let rec step f ?(delta=false) ?(rt=false) c m x = +let rec step f ?(delta=false) ?(rt=false) m x = (* L.warn "entering R.step"; *) match x with | B.Sort _ -> f m x @@ -74,10 +79,10 @@ let rec step f ?(delta=false) ?(rt=false) c m x = let f = function | _, _, B.Abbr v when delta -> P.add ~gdelta:1 (); - step f ~delta ~rt c m v + step f ~delta ~rt m v | _, _, B.Abst w when rt -> P.add ~grt:1 (); - step f ~delta ~rt c m w + step f ~delta ~rt m w | e, _, b -> f m (B.GRef (B.Entry (e, b) :: a, uri)) in @@ -86,61 +91,59 @@ let rec step f ?(delta=false) ?(rt=false) c m x = let f e = function | B.Abbr v -> P.add ~ldelta:1 (); - step f ~delta ~rt c m v + step f ~delta ~rt m v | B.Abst w when rt -> P.add ~lrt:1 (); - step f ~delta ~rt c m w + step f ~delta ~rt m w | b -> f m (B.LRef (B.Entry (e, b) :: a, i)) in let f e = S.lift_bind (f e) (succ i) (0) in - get f c m i + get f m i | B.Cast (_, _, t) -> P.add ~tau:1 (); - step f ~delta ~rt c m t + step f ~delta ~rt m t | B.Appl (_, v, t) -> - step f ~delta ~rt c {m with s = (v, 0) :: m.s} t + step f ~delta ~rt {m with s = (v, 0) :: m.s} t | B.Bind (a, B.Abst w, t) -> begin match m.s with | [] -> f m x | (v, h) :: tl -> P.add ~beta:1 ~upsilon:(List.length tl) (); - let f mc sc = step f ~delta ~rt c {c = mc; s = sc} t in - let f mc = lift_stack (f mc) tl in + let f c s = step f ~delta ~rt {c = c; s = s} t in + let f c = lift_stack (f c) tl in let f v = B.push f m.c a (B.Abbr v (* (B.Cast ([], w, v)) *) ) in S.lift f h (0) v end | B.Bind (a, b, t) -> P.add ~upsilon:(List.length m.s) (); - let f sc mc = step f ~delta ~rt c {c = mc; s = sc} t in - let f sc = B.push (f sc) m.c a b in + let f s c = step f ~delta ~rt {c = c; s = s} t in + let f s = B.push (f s) m.c a b in lift_stack f m.s (* Interface functions ******************************************************) - -let domain f c t = + +let domain f m t = let f r = L.unbox level; f r in let f m = function - | B.Bind (_, B.Abst w, _) -> - let f w = f (Some w) in unwind_to_term f m w - | x -> f None + | B.Bind (_, B.Abst w, _) -> f m w + | _ -> error1 "not a function" m.c t in - L.box level; log1 "Now scanning" c t; - step f ~delta:true ~rt:true c empty_machine t + L.box level; log1 "Now scanning" m.c t; + step f ~delta:true ~rt:true m t -let rec ac_nfs f ~si r c m1 u m2 t = -(* L.warn "entering R.are_convertible_aux"; *) - log2 "Now converting nfs" c u t; +let rec ac_nfs f ~si r m1 u m2 t = + log2 "Now converting nfs" m1.c u m2.c t; match u, t with | B.Sort (_, h1), B.Sort (_, h2) -> if h1 = h2 then f r else f false | B.LRef (B.Entry (e1, B.Abst _) :: _, i1), B.LRef (B.Entry (e2, B.Abst _) :: _, i2) -> P.add ~zeta:(i1+i2-e1-e2) (); - if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false + if e1 = e2 then ac_stacks f ~si r m1 m2 else f false | B.GRef (B.Entry (e1, B.Abst _) :: _, _), B.GRef (B.Entry (e2, B.Abst _) :: _, _) -> - if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false + if e1 = e2 then ac_stacks f ~si r m1 m2 else f false | B.GRef (B.Entry (e1, B.Abbr v1) :: _, _), B.GRef (B.Entry (e2, B.Abbr v2) :: _, _) -> if e1 = e2 then @@ -148,48 +151,48 @@ let rec ac_nfs f ~si r c m1 u m2 t = if r then f r else begin P.add ~gdelta:2 (); - ac f ~si true c m1 v1 m2 v2 + ac f ~si true m1 v1 m2 v2 end in - ac_stacks f ~si r c m1 m2 + ac_stacks f ~si r m1 m2 else if e1 < e2 then begin P.add ~gdelta:1 (); - step (ac_nfs f ~si r c m1 u) c m2 v2 + step (ac_nfs f ~si r m1 u) m2 v2 end else begin P.add ~gdelta:1 (); - step (ac_nfs_rev f ~si r c m2 t) c m1 v1 + step (ac_nfs_rev f ~si r m2 t) m1 v1 end | _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) -> P.add ~gdelta:1 (); - step (ac_nfs f ~si r c m1 u) c m2 v2 + step (ac_nfs f ~si r m1 u) m2 v2 | B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ -> P.add ~gdelta:1 (); - step (ac_nfs_rev f ~si r c m2 t) c m1 v1 + step (ac_nfs_rev f ~si r m2 t) m1 v1 | B.Bind (a1, (B.Abst w1 as b1), t1), B.Bind (a2, (B.Abst w2 as b2), t2) -> - let g m1 m2 = ac f ~si r c m1 t1 m2 t2 in + let g m1 m2 = ac f ~si r m1 t1 m2 t2 in let g m1 = push (g m1) m2 a2 b2 in let f r = if r then push g m1 a1 b1 else f false in - ac f ~si r c m1 w1 m2 w2 + ac f ~si r m1 w1 m2 w2 | B.Sort _, B.Bind (a, b, t) when si -> P.add ~si:1 (); - let f m1 m2 = ac f ~si r c m1 u m2 t in + let f m1 m2 = ac f ~si r m1 u m2 t in let f m1 = push (f m1) m2 a b in push f m1 a b | _ -> f false -and ac_nfs_rev f ~si r c m2 t m1 u = ac_nfs f ~si r c m1 u m2 t +and ac_nfs_rev f ~si r m2 t m1 u = ac_nfs f ~si r m1 u m2 t -and ac f ~si r c m1 t1 m2 t2 = +and ac f ~si r m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) - let g m1 t1 = step (ac_nfs f ~si r c m1 t1) c m2 t2 in - if r = false then f false else step g c m1 t1 + let g m1 t1 = step (ac_nfs f ~si r m1 t1) m2 t2 in + if r = false then f false else step g m1 t1 -and ac_stacks f ~si r c m1 m2 = +and ac_stacks f ~si r m1 m2 = (* L.warn "entering R.are_convertible_stacks"; *) let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in let map f r (v1, h1) (v2, h2) = - let f v1 = S.lift (ac f ~si r c mm1 v1 mm2) h2 (0) v2 in + let f v1 = S.lift (ac f ~si r mm1 v1 mm2) h2 (0) v2 in S.lift f h1 (0) v1 in if List.length m1.s <> List.length m2.s then @@ -202,7 +205,15 @@ and ac_stacks f ~si r c m1 m2 = else C.list_fold_left2 f map r m1.s m2.s -let are_convertible f ?(si=false) c u t = +let assert_conversion f ?(si=false) ?(rt=false) c u w v = let f b = L.unbox level; f b in - L.box level; log2 "Now converting" c u t; - ac f ~si true c empty_machine u empty_machine t + let mw = empty_machine c in + let f mu u = + let f = function + | true -> f () + | false -> error3 c v w u + in + L.box level; log2 "Now converting" c u c w; + ac f ~si true mu u mw w + in + if rt then domain f mw u else f mw u