X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2FbagType.ml;h=8aee519202eac11501752fb8b2c75c0ee3e56dc7;hb=1ae23fe33b8647a4b8616e666dc5703c17678069;hp=80b883ff44612101b47dcead611ef55aa88b438a;hpb=4924ddb52a836eea45a593a7f4faccca64bac9e7;p=helm.git diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index 80b883ff4..8aee51920 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -55,6 +55,7 @@ let add_coercion f t (i, uri, vs) = add f v | B.Bind (l, _, _, _) when i = l -> if U.eq uri I.imp then f (mk_gref I.mt (vs @ [x])) else + if U.eq uri I.all then f (mk_gref I.alli (vs @ [x])) else assert false | B.Bind (l, id, B.Abst w, t) -> let f ww = @@ -128,35 +129,41 @@ let rec b_type_of f g c x = let f cc = b_type_of f g cc t in B.push f c l 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 -> + let f xv vv xt tt = function + | R.Abst w -> L.box (succ level); - L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w); + L.log O.specs (succ level) (L.ct_items1 "Just scanned" c w); L.unbox (succ level); let f = function - | Some l -> f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) - | None -> error2 "the term" cc xv "must be of type" cc w + | Some [] -> f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) + | Some l -> + L.log O.specs level (L.items1 "Rechecking coerced term"); + let f xv = b_type_of f g c (S.sh2 v xv t xt x B.appl) in + add_coercions f xv l + | None -> error2 "The term" c xv "must be of type" c 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 uri)) when U.eq uri I.imp -> - b_type_of f g c (mk_gref I.mp [y1; y2; xv; xt]) - | B.Appl (y1, B.GRef uri) when U.eq uri I.not -> - b_type_of f g c (mk_gref I.mp [y1; B.GRef I.con; xv; xt]) - | tt -> R.ho_whd (h xv vv xt tt) c tt + R.are_convertible f c w vv +(* inserting a missing "modus ponens" *) + | R.GRef (uri, vs) when U.eq uri I.imp -> + L.log O.specs level (L.items1 "Rechecking coerced term"); + b_type_of f g c (mk_gref I.mp (vs @ [xv; xt])) + | R.GRef (uri, vs) when U.eq uri I.all -> + L.log O.specs level (L.items1 "Rechecking coerced term"); + b_type_of f g c (mk_gref I.alle (vs @ [xv; xt])) + | _ -> + 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 = b_type_of (f xv vv) g c t in type_of f g c v | B.Cast (u, t) -> let f xu xt = function | Some [] -> f (S.sh2 u xu t xt x B.cast) xu | Some l -> - let f xt = type_of f g c (S.sh2 u xu t xt x B.cast) in + L.log O.specs level (L.items1 "Rechecking coerced term"); + let f xt = b_type_of f g c (S.sh2 u xu t xt x B.cast) in add_coercions f xt l - | None -> error2 "the term" c xt "must be of type" c xu + | None -> error2 "The term" c xt "must be of type" c xu in let f xu xt tt = R.are_convertible (f xu xt) c xu tt in let f xu _ = b_type_of (f xu) g c t in