X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgType.ml;h=4bf5882a4885a48cf53e1fc4af257e875820bc9e;hb=1b8fc00fe0bac1e6ba9382c9b5a7fe761dedda31;hp=60b5b75bcc54d540a5d063e8d9aaba1aac9b38b4;hpb=8659e85d49be1ad72622d4d3a73d384b744c3c08;p=helm.git diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index 60b5b75bc..4bf5882a4 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -9,82 +9,120 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module U = NUri +module C = Cps +module A = Share module L = Log +module H = Hierarchy module B = Brg module O = BrgOutput module E = BrgEnvironment +module S = BrgSubstitution module R = BrgReduction -exception TypeError of (R.context, B.term) Log.item list +exception TypeError of B.message (* Internal functions *******************************************************) -let error1 s c t = - raise (TypeError (L.ct_items1 s c t)) +let level = 4 -let error2 s1 c1 t1 s2 c2 t2 = - raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2)) +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 are_convertible f c t1 t2 = - L.log O.specs 4 (L.ct_items2 "Now converting" c t1 "and" c t2); - R.are_convertible f c t1 t2 +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)) (* Interface functions ******************************************************) -let rec type_of f g c x = - L.log O.specs 5 (L.ct_items1 "now checking" c x); +let si = ref false + +let rec b_type_of f g c x = +(* L.warn "Entering T.b_type_of"; *) + log1 "Now checking" c x; match x with - | B.Sort h -> f (B.Sort (g h)) - | B.LRef i -> - let f = function - | B.Abst w -> f w - | B.Abbr (B.Cast (w, v)) -> f w - | B.Abbr _ -> assert false - | B.Void -> assert false + | B.Sort (a, h) -> + let f h = f x (B.Sort (a, h)) in H.apply f g h + | B.LRef (_, i) -> + let f _ = function + | Some (_, B.Abst w) -> + S.lift (f x) (succ i) (0) w + | Some (_, B.Abbr (B.Cast (_, w, _))) -> + S.lift (f x) (succ i) (0) w + | Some (_, B.Abbr _) -> assert false + | Some (_, B.Void) -> + error1 "reference to excluded variable" c x + | None -> + error1 "variable not found" c x in - R.get f c i - | B.GRef uri -> + B.get f c i + | B.GRef (_, uri) -> let f = function - | _, _, B.Abst w -> f w - | _, _, B.Abbr (B.Cast (w, v)) -> f w - | _, _, B.Abbr _ -> assert false - | _, _, B.Void -> assert false + | _, _, B.Abst w -> f x w + | _, _, B.Abbr (B.Cast (_, w, _)) -> f x w + | _, _, B.Abbr _ -> assert false + | _, _, B.Void -> + error1 "reference to excluded object" c x in - E.get_obj f uri - | B.Bind (id, B.Abbr u, t) -> - let f tt = f (B.Bind (id, B.Abbr u, tt)) in - let f cc = type_of f g cc t in - let f u = R.push f c (B.Abbr u) in - let f uu = match u with - | B.Cast _ -> f u - | _ -> f (B.Cast (uu, u)) + E.get_obj f uri + | B.Bind (a, B.Abbr 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 cc = b_type_of (f xv) g cc t in + let f xv = B.push (f xv) c a (B.Abbr xv) in + let f xv vv = match xv with + | B.Cast _ -> f xv + | _ -> f (B.Cast ([], vv, xv)) + in + type_of f g c v + | B.Bind (a, B.Abst 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 cc = b_type_of (f xu) g cc t in + let f xu _ = B.push (f xu) c a (B.Abst xu) in type_of f g c u - | B.Bind (id, B.Abst u, t) -> - let f tt = f (B.Bind (id, B.Abst u, tt)) in - let f cc = type_of f g cc t in - let f _ = R.push f c (B.Abst u) in - type_of f g c u - | B.Bind (id, B.Void, t) -> - let f tt = f (B.Bind (id, B.Void, tt)) in - let f cc = type_of f g cc t in - R.push f c B.Void - | B.Appl (v, t) -> - let f tt cc = function - | R.Sort _ -> error1 "not a function" c t - | R.Abst w -> - let f b = - if b then f (B.Appl (v, tt)) else - error2 "the term" c v "must be of type" cc w + | B.Bind (a, B.Void, t) -> + let f xt tt = + f (A.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt) + in + let f cc = b_type_of f g cc t in + B.push f c a B.Void + | B.Appl (a, v, t) -> + let f xv vv xt tt = function + | Some w -> + L.box (succ level); + L.log O.specs (succ level) (L.t_items1 "Just scanned" c w); + L.unbox (succ level); + let f r = +(* L.warn (Printf.sprintf "Convertible: %b" a); *) + if r then f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) + else error3 c xv vv w in - type_of (are_convertible f cc w) g c v + R.are_convertible f ~si:!si c w vv + | None -> + error1 "not a function" c xt in - let f tt = R.ho_whd (f tt) c t in - type_of f g c t - | B.Cast (u, t) -> - let f b = - if b then f u else - error2 "the term" c t "must be of type" c u + let f xv vv xt tt = R.domain (f xv vv xt tt) c tt in + let f xv vv = b_type_of (f xv vv) g c t in + type_of f g c v + | B.Cast (a, u, t) -> + let f xu xt tt r = + (* L.warn (Printf.sprintf "Convertible: %b" a); *) + if r then f (A.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu in - let f _ = type_of (are_convertible f c u) g c t in + let f xu xt tt = R.are_convertible ~si:!si (f xu xt tt) c xu tt in + let f xu _ = b_type_of (f xu) g c t in type_of f g c u + +and type_of f g c x = + let f t u = L.unbox level; f t u in + L.box level; b_type_of f g c x