X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2FbagType.ml;h=4f447276b3f71a4fb529d04883604be4c7106792;hb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;hp=bb4ee83d47e6e660300c126824ee052b0be8c3d2;hpb=ab13cfa248f0ee58d239ceeddfb50ec49a6b5c6d;p=helm.git diff --git a/helm/software/lambda-delta/src/basic_ag/bagType.ml b/helm/software/lambda-delta/src/basic_ag/bagType.ml index bb4ee83d4..4f447276b 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagType.ml @@ -9,18 +9,19 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module C = Cps -module S = Share -module L = Log -module Y = Entity -module H = Hierarchy -module B = Bag -module O = BagOutput -module E = BagEnvironment -module R = BagReduction +module U = NUri +module C = Cps +module W = Share +module L = Log +module E = Entity +module H = Hierarchy +module S = Status +module Z = Bag +module ZO = BagOutput +module ZE = BagEnvironment +module ZR = BagReduction -exception TypeError of B.message +exception TypeError of Z.message (* Internal functions *******************************************************) @@ -28,7 +29,7 @@ let level = 4 let log1 s c t = let sc, st = s ^ " in the envireonment", "the term" in - L.log O.specs level (L.et_items1 sc c st t) + L.log ZO.specs level (L.et_items1 sc c st t) let error1 st c t = let sc = "In the envireonment" in @@ -41,8 +42,8 @@ let error3 c t1 t2 t3 = raise (TypeError (L.et_items3 sc c st1 t1 st2 t2 st3 t3)) let mk_gref u l = - let map t v = B.Appl (v, t) in - List.fold_left map (B.GRef u) l + let map t v = Z.Appl (v, t) in + List.fold_left map (Z.GRef u) l (* Interface functions ******************************************************) @@ -50,75 +51,73 @@ let rec b_type_of f st c x = (* L.warn "Entering T.b_type_of"; *) log1 "Now checking" c x; match x with - | B.Sort h -> - let h = H.apply h in f x (B.Sort 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) -> - error1 "reference to excluded variable" c x - | None -> - error1 "variable not found" c x + | Z.Sort h -> + let h = H.apply h in f x (Z.Sort h) + | Z.LRef i -> + let err () = error1 "variable not found" c x in + let f _ = function + | Z.Abst w -> f x w + | Z.Abbr (Z.Cast (w, v)) -> f x w + | Z.Abbr _ -> assert false + | Z.Void -> error1 "reference to excluded variable" c x in - B.get f c i - | B.GRef uri -> + Z.get err f c i + | Z.GRef uri -> let f = function - | _, _, Y.Abst w -> f x w - | _, _, Y.Abbr (B.Cast (w, v)) -> f x w - | _, _, Y.Abbr _ -> assert false - | _, _, Y.Void -> assert false + | _, _, E.Abst (_, w) -> f x w + | _, _, E.Abbr (Z.Cast (w, v)) -> f x w + | _, _, E.Abbr _ -> assert false + | _, _, E.Void -> assert false in - E.get_entity f uri - | B.Bind (l, id, B.Abbr v, t) -> + ZE.get_entity f uri + | Z.Bind (a, l, Z.Abbr v, t) -> let f xv xt tt = - f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l id xv tt) + f (W.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt) in let f xv cc = b_type_of (f xv) st cc t in - let f xv = B.push "type abbr" (f xv) c l id (B.Abbr xv) in + let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in let f xv vv = match xv with - | B.Cast _ -> f xv - | _ -> f (B.Cast (vv, xv)) + | Z.Cast _ -> f xv + | _ -> f (Z.Cast (vv, xv)) in type_of f st c v - | B.Bind (l, id, B.Abst u, t) -> + | Z.Bind (a, l, Z.Abst u, t) -> let f xu xt tt = - f (S.sh2 u xu t xt x (B.bind_abst l id)) (B.bind_abst l id xu tt) + f (W.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt) in let f xu cc = b_type_of (f xu) st cc t in - let f xu _ = B.push "type abst" (f xu) c l id (B.Abst xu) in + let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in type_of f st c u - | B.Bind (l, id, B.Void, t) -> + | Z.Bind (a, l, Z.Void, t) -> let f xt tt = - f (S.sh1 t xt x (B.bind l id B.Void)) (B.bind l id B.Void tt) + f (W.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt) in let f cc = b_type_of f st cc t in - B.push "type void" f c l id B.Void - | B.Appl (v, t) -> + Z.push "type void" f c a l Z.Void + | Z.Appl (v, t) -> let f xv vv xt tt = function - | R.Abst w -> + | ZR.Abst w -> L.box (succ level); - L.log O.specs (succ level) (L.t_items1 "Just scanned" c w); + L.log ZO.specs (succ level) (L.t_items1 "Just scanned" c w); L.unbox (succ level); let f a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if a then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) + if a then f (W.sh2 v xv t xt x Z.appl) (Z.appl xv tt) else error3 c xv vv w in - R.are_convertible f ~si:st.Y.si c w vv + ZR.are_convertible f ~si:st.S.si c w vv | _ -> error1 "not a function" c xt in - let f xv vv xt tt = R.ho_whd (f xv vv xt tt) c tt in + let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) c tt in let f xv vv = b_type_of (f xv vv) st c t in type_of f st c v - | B.Cast (u, t) -> + | Z.Cast (u, t) -> let f xu xt tt a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if a then f (S.sh2 u xu t xt x B.cast) xu else error3 c xt tt xu + if a then f (W.sh2 u xu t xt x Z.cast) xu else error3 c xt tt xu in - let f xu xt tt = R.are_convertible (f xu xt tt) ~si:st.Y.si c xu tt in + let f xu xt tt = ZR.are_convertible (f xu xt tt) ~si:st.S.si c xu tt in let f xu _ = b_type_of (f xu) st c t in type_of f st c u