X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgType.ml;h=4bf5882a4885a48cf53e1fc4af257e875820bc9e;hb=8f5f3f5c96fd3ab0c466b828a731b8517a91bbd0;hp=fb7862c242223dc32b3a618959fdd4cf06e723bd;hpb=f23388dbd51574725a11b0ab5373f09838a32ab5;p=helm.git diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index fb7862c24..4bf5882a4 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -10,13 +10,14 @@ V_______________________________________________________________ *) module U = NUri -module S = Share +module C = Cps +module A = Share module L = Log module H = Hierarchy -module I = AutItem module B = Brg module O = BrgOutput module E = BrgEnvironment +module S = BrgSubstitution module R = BrgReduction exception TypeError of B.message @@ -25,95 +26,103 @@ exception TypeError of B.message let level = 4 -let error1 s c t = - raise (TypeError (L.ct_items1 s c t)) +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 error2 s1 c1 t1 s2 c2 t2 = - raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2)) +let error1 st c t = + let sc = "In the context" in + raise (TypeError (L.ct_items1 sc c st t)) -let mk_gref u l = - let map t v = B.Appl (v, t) in - List.fold_left map (B.GRef u) l +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 si = ref false + let rec b_type_of f g c x = - L.log O.specs level (L.ct_items1 "Now checking" c x); +(* L.warn "Entering T.b_type_of"; *) + log1 "Now checking" c x; match x with - | B.Sort h -> - let f h = f x (B.Sort h) in H.apply f g h - | B.LRef i -> - let f = function - | Some (_, B.Abst w) -> f x w - | Some (_, B.Abbr (B.Cast (w, v))) -> f x w - | Some (_, B.Abbr _) -> assert false - | Some (_, B.Void) -> + | 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 B.get f c i - | B.GRef uri -> + | B.GRef (_, uri) -> let f = function - | _, _, B.Abst w -> f x w - | _, _, B.Abbr (B.Cast (w, v)) -> f x w - | _, _, B.Abbr _ -> assert false - | _, _, B.Void -> + | _, _, 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 v, t) -> + | B.Bind (a, B.Abbr v, t) -> let f xv xt tt = - f (S.sh2 v xv t xt x (B.bind_abbr id)) (B.bind_abbr id xv 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 id (B.Abbr xv) 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)) + | _ -> f (B.Cast ([], vv, xv)) in type_of f g c v - | B.Bind (id, B.Abst u, t) -> + | B.Bind (a, B.Abst u, t) -> let f xu xt tt = - f (S.sh2 u xu t xt x (B.bind_abst id)) (B.bind_abst id xu 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 id (B.Abst xu) in + let f xu _ = B.push (f xu) c a (B.Abst xu) in type_of f g c u - | B.Bind (id, B.Void, t) -> + | B.Bind (a, B.Void, t) -> let f xt tt = - f (S.sh1 t xt x (B.bind id B.Void)) (B.bind id B.Void 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 id B.Void - | B.Appl (v, t) -> - let h xv vv xt tt cc = function - | R.Sort _ -> error1 "not a function" c xt - | R.Abst w -> - L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w); - let f b = - if b then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else - error2 "the term" cc xv "must be of type" cc w + 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 - R.are_convertible f cc w vv - in - let f xv vv xt = function -(* inserting a missing "modus ponens" *) - | B.Appl (y2, B.Appl (y1, B.GRef u)) when U.eq u I.imp -> - b_type_of f g c (mk_gref I.mp [y1; y2; xv; xt]) - | tt -> R.ho_whd (h xv vv xt tt) c tt + R.are_convertible f ~si:!si c w vv + | None -> + error1 "not a function" c xt in + 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 (u, t) -> - let f xu xt b = - if b then f (S.sh2 u xu t xt x B.cast) xu else - error2 "the term" c xt "must be of type" c xu + | 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 xu xt tt = R.are_convertible (f xu xt) c xu tt 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 (); f t u in - L.box (); b_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