X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=ff5f396054795b1fafc2a8567a9da8642143fbf9;hb=30704126796b07213d6da3ca25156d82e761d554;hp=86f280842f6a7480bb95cb60b35f00811b89b9fc;hpb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;p=helm.git diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index 86f280842..ff5f39605 100644 --- a/helm/software/components/cic_unification/cicUnification.ml +++ b/helm/software/components/cic_unification/cicUnification.ml @@ -136,7 +136,7 @@ let eta_reduce after_beta_expansion after_beta_expansion_body with WrongShape -> after_beta_expansion -let rec beta_expand test_equality_only metasenv subst context t arg ugraph = +let rec beta_expand num test_equality_only metasenv subst context t arg ugraph = let module S = CicSubstitution in let module C = Cic in let foo () = @@ -197,15 +197,17 @@ let foo () = in (* TASSI: sure this is in serial? *) subst,metasenv,(C.Lambda (nn, s', t')),ugraph2 - | C.LetIn (nn,s,t) -> + | C.LetIn (nn,s,ty,t) -> let subst,metasenv,s',ugraph1 = aux metasenv subst n context s ugraph in + let subst,metasenv,ty',ugraph1 = + aux metasenv subst n context ty ugraph in let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t + aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t ugraph1 in (* TASSI: sure this is in serial? *) - subst,metasenv,(C.LetIn (nn, s', t')),ugraph2 + subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2 | C.Appl l -> let subst,metasenv,revl',ugraph1 = List.fold_left @@ -279,7 +281,7 @@ let foo () = let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in let fresh_name = FreshNamesGenerator.mk_fresh_name ~subst - metasenv context (Cic.Name "Hbeta") ~typ:argty + metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty in let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in @@ -288,15 +290,15 @@ in profiler_beta_expand.HExtlib.profile foo () and beta_expand_many test_equality_only metasenv subst context t args ugraph = - let subst,metasenv,hd,ugraph = + let _,subst,metasenv,hd,ugraph = List.fold_right - (fun arg (subst,metasenv,t,ugraph) -> + (fun arg (num,subst,metasenv,t,ugraph) -> let subst,metasenv,t,ugraph1 = - beta_expand test_equality_only + beta_expand num test_equality_only metasenv subst context t arg ugraph in - subst,metasenv,t,ugraph1 - ) args (subst,metasenv,t,ugraph) + num+1,subst,metasenv,t,ugraph1 + ) args (1,subst,metasenv,t,ugraph) in subst,metasenv,hd,ugraph @@ -316,11 +318,18 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph = let module S = CicSubstitution in let t1 = deref subst t1 in let t2 = deref subst t2 in - let b,ugraph = + let (&&&) a b = (a && b) || ((not a) && (not b)) in +(* let bef = Sys.time () in *) + let b,ugraph = + if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then + false,ugraph + else let foo () = R.are_convertible ~subst ~metasenv context t1 t2 ugraph in profiler_are_convertible.HExtlib.profile foo () in +(* let aft = Sys.time () in +if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *) if b then subst, metasenv, ugraph else @@ -508,8 +517,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ in fo_unif_subst test_equality_only subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 - | (C.LetIn (_,s1,t1), t2) - | (t2, C.LetIn (_,s1,t1)) -> + | (C.LetIn (_,s1,ty1,t1), t2) + | (t2, C.LetIn (_,s1,ty1,t1)) -> fo_unif_subst test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph | (C.Appl l1, C.Appl l2) -> @@ -593,55 +602,93 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (match l1, l2 with | (((Cic.Const (uri1, ens1)) as c1) :: tl1), (((Cic.Const (uri2, ens2)) as c2) :: tl2) when - CoercGraph.is_a_coercion c1 && - CoercGraph.is_a_coercion c2 && + CoercDb.is_a_coercion' c1 && + CoercDb.is_a_coercion' c2 && not (UriManager.eq uri1 uri2) -> - let body1, attrs1, ugraph = - match CicEnvironment.get_obj ugraph uri1 with - | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u - | _ -> assert false - in - let body2, attrs2, ugraph = - match CicEnvironment.get_obj ugraph uri2 with - | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u - | _ -> assert false - in - let is_composite1 = - List.exists - (function `Class (`Coercion _) -> true | _-> false) - attrs1 - in - let is_composite2 = - List.exists - (function `Class (`Coercion _) -> true | _-> false) - attrs2 - in - (match is_composite1, is_composite2 with - | false, false -> raise exn - | true, false -> - let body1 = CicSubstitution.subst_vars ens1 body1 in - let appl = Cic.Appl (body1::tl1) in - let redappl = CicReduction.head_beta_reduce appl in - fo_unif_subst - test_equality_only subst context metasenv - redappl t2 ugraph - | false, true -> - let body2 = CicSubstitution.subst_vars ens2 body2 in - let appl = Cic.Appl (body2::tl2) in - let redappl = CicReduction.head_beta_reduce appl in - fo_unif_subst - test_equality_only subst context metasenv - t1 redappl ugraph - | true, true -> - let body1 = CicSubstitution.subst_vars ens1 body1 in - let appl1 = Cic.Appl (body1::tl1) in - let redappl1 = CicReduction.head_beta_reduce appl1 in - let body2 = CicSubstitution.subst_vars ens2 body2 in - let appl2 = Cic.Appl (body2::tl2) in - let redappl2 = CicReduction.head_beta_reduce appl2 in - fo_unif_subst - test_equality_only subst context metasenv - redappl1 redappl2 ugraph) +(*DEBUGGING ONLY: +prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); +let res = +*) + let rec look_for_first_coercion c tl = + match + CicMetaSubst.apply_subst subst (HExtlib.list_last tl) + with + Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl') + when CoercDb.is_a_coercion' c' -> + look_for_first_coercion c' tl' + | last_tl -> c,last_tl + in + let c1,last_tl1 = look_for_first_coercion c1 tl1 in + let c2,last_tl2 = look_for_first_coercion c2 tl2 in + let car1 = + CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in + let car2 = + CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in + if CoercDb.eq_carr car1 car2 then + (match last_tl1,last_tl2 with + C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn + | C.Meta _, _ + | _, C.Meta _ -> + let subst,metasenv,ugraph = + fo_unif_subst test_equality_only subst context + metasenv last_tl1 last_tl2 ugraph + in + fo_unif_subst test_equality_only subst context + metasenv (C.Appl l1) (C.Appl l2) ugraph + | _ -> raise exn) + else + let meets = + CoercGraph.meets metasenv subst context car1 car2 + in + (match meets with + | [] -> raise exn + | (carr,metasenv,to1,to2)::xxx -> + (match xxx with + [] -> () + | (m2,_,c2,c2')::_ -> + let m1,_,c1,c1' = carr,metasenv,to1,to2 in + let unopt = + function Some (_,t) -> CicPp.ppterm t + | None -> "id" + in + HLog.warn + ("There are two minimal joins of "^ + CoercDb.name_of_carr car1^" and "^ + CoercDb.name_of_carr car2^": " ^ + CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^ + unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^ + unopt c2^" + "^unopt c2')); + let last_tl1',(subst,metasenv,ugraph) = + match last_tl1,to1 with + | Cic.Meta (i1,l1),Some (last,coerced) -> + last, + fo_unif_subst test_equality_only subst context + metasenv coerced last_tl1 ugraph + | _ -> last_tl1,(subst,metasenv,ugraph) + in + let last_tl2',(subst,metasenv,ugraph) = + match last_tl2,to2 with + | Cic.Meta (i2,l2),Some (last,coerced) -> + last, + fo_unif_subst test_equality_only subst context + metasenv coerced last_tl2 ugraph + | _ -> last_tl2,(subst,metasenv,ugraph) + in + (*DEBUGGING ONLY: +prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context); +*) + let subst,metasenv,ugraph = + fo_unif_subst test_equality_only subst context + metasenv last_tl1' last_tl2' ugraph + in + fo_unif_subst test_equality_only subst context + metasenv (C.Appl l1) (C.Appl l2) ugraph) +(*DEBUGGING ONLY: +in +let subst,metasenv,ugraph = res in +prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); +res +*) (*CSC: This is necessary because of the "elim H" tactic where the type of H is only reducible to an inductive type. This could be extended from inductive