X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=36c114d8f8f85fff695a01040ec3185e83934247;hb=30641ee6278838b8b2a0b567d61f8f143582a217;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..36c114d8f 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,18 +290,33 @@ 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 +and warn_if_not_unique xxx to1 to2 carr car1 car2 = + match xxx with + | [] -> () + | (m2,_,c2,c2')::_ -> + let m1,c1,c1' = carr,to1,to2 in + let unopt = + function Some (_,t) -> CicPp.ppterm t + | None -> "id" + in + HLog.warn + ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^ + CoercDb.string_of_carr car2^": " ^ + CoercDb.string_of_carr m1^" via "^unopt c1^" + "^ + unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^ + unopt c2^" + "^unopt c2') (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a @@ -316,11 +333,20 @@ 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 @@ -496,20 +522,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ subst context metasenv te t2 ugraph | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only subst context metasenv t1 te ugraph - | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> - let subst',metasenv',ugraph1 = - fo_unif_subst true subst context metasenv s1 s2 ugraph - in - fo_unif_subst test_equality_only - subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> let subst',metasenv',ugraph1 = fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph 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) -> @@ -591,58 +611,148 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ | UnificationFailure s | Uncertain s as exn -> (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 && + (* {{{ pullback *) + | (((Cic.Const (uri1, ens1)) as cc1) :: tl1), + (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when + CoercDb.is_a_coercion cc1 <> None && + CoercDb.is_a_coercion cc2 <> None && 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 +(*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 inner_coerced ?(skip_non_c=false) t = + let t = CicMetaSubst.apply_subst subst t in + let rec aux c x t = + match t with + | Cic.Appl l -> + (match CoercGraph.coerced_arg l with + | None when skip_non_c -> + aux c (HExtlib.list_last l) + (HExtlib.list_last l) + | None -> c, x + | Some (t,_) -> aux (List.hd l) t t) + | _ -> c, x + in + aux (Cic.Implicit None) (Cic.Implicit None) t + in + let c1,last_tl1 = inner_coerced (Cic.Appl l1) in + let c2,last_tl2 = inner_coerced (Cic.Appl l2) in + let car1, car2 = + match + CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2 + with + | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2 | _ -> assert false in - let body2, attrs2, ugraph = - match CicEnvironment.get_obj ugraph uri2 with - | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u + let head1_c, head2_c = + match + CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2 + with + | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2 | _ -> assert false in - let is_composite1 = - List.exists - (function `Class (`Coercion _) -> true | _-> false) - attrs1 + let unfold uri ens args = + let o, _ = + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri + in + assert (ens = []); + match o with + | Cic.Constant (_,Some bo,_,_,_) -> + CicReduction.head_beta_reduce ~delta:false + (Cic.Appl (bo::args)) + | _ -> assert false in - let is_composite2 = - List.exists - (function `Class (`Coercion _) -> true | _-> false) - attrs2 + let conclude subst metasenv ugraph last_tl1' last_tl2' = + let subst',metasenv,ugraph = +(*DEBUGGING ONLY: +prerr_endline + ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ + " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context); +*) + fo_unif_subst test_equality_only subst context + metasenv last_tl1' last_tl2' ugraph + in + if subst = subst' then raise exn + else +(*DEBUGGING ONLY: +let subst,metasenv,ugrph as res = +*) + fo_unif_subst test_equality_only subst' context + metasenv (C.Appl l1) (C.Appl l2) ugraph +(*DEBUGGING ONLY: +in +(prerr_endline + (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ + " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); +res) +*) 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) - (*CSC: This is necessary because of the "elim H" tactic + 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 (Cic.Appl l1) (Cic.Appl l2) ugraph + | _ when CoercDb.eq_carr head1_c head2_c -> + (* composite VS composition + metas avoiding + * coercions not only in coerced position *) + if c1 <> cc1 && c2 <> cc2 then + conclude subst metasenv ugraph + last_tl1 last_tl2 + else + let l1, l2 = + if c1 = cc1 then + unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2) + else + Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2 + in + fo_unif_subst test_equality_only subst context + metasenv l1 l2 ugraph + | _ -> raise exn + else + let grow1 = + match last_tl1 with Cic.Meta _ -> true | _ -> false in + let grow2 = + match last_tl2 with Cic.Meta _ -> true | _ -> false in + if not (grow1 || grow2) then + let _,last_tl1 = + inner_coerced ~skip_non_c:true (Cic.Appl l1) in + let _,last_tl2 = + inner_coerced ~skip_non_c:true (Cic.Appl l2) in + conclude subst metasenv ugraph last_tl1 last_tl2 + else + let meets = + CoercGraph.meets + metasenv subst context (grow1,car1) (grow2,car2) + in + (match meets with + | [] -> raise exn + | (carr,metasenv,to1,to2)::xxx -> + warn_if_not_unique xxx to1 to2 carr car1 car2; + let last_tl1',(subst,metasenv,ugraph) = + match grow1,to1 with + | true,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 grow2,to2 with + | true,Some (last,coerced) -> + last, + fo_unif_subst test_equality_only subst context + metasenv coerced last_tl2 ugraph + | _ -> last_tl2,(subst,metasenv,ugraph) + in + conclude subst metasenv ugraph last_tl1' last_tl2') + (* }}} pullback *) + (* {{{ 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 types to any rigid term. However, the code is @@ -665,7 +775,9 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ subst context metasenv t1 t2' ugraph | _ -> raise (UnificationFailure - (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 )))) + (lazy ("not a mutind :"^ + CicMetaSubst.ppterm ~metasenv subst t2 )))) + (* }}} elim H *) | _ -> raise exn))) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv',ugraph1 = @@ -720,28 +832,22 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ subst context metasenv t1' t2 ugraph | _ -> raise (UnificationFailure (lazy "8"))) *) -(* The following idea could be exploited again; right now we have no - longer any example requiring it - | (C.Prod _, t2) -> - let t2' = R.whd ~subst context t2 in - (match t2' with - C.Prod _ -> - fo_unif_subst test_equality_only - subst context metasenv t1 t2' ugraph - | _ -> raise (UnificationFailure (lazy "8"))) - | (t1, C.Prod _) -> - let t1' = R.whd ~subst context t1 in - (match t1' with - C.Prod _ -> - fo_unif_subst test_equality_only - subst context metasenv t1' t2 ugraph - | _ -> (* raise (UnificationFailure "9")) *) - raise - (UnificationFailure (lazy (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2))))) -*) + | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> + let subst',metasenv',ugraph1 = + fo_unif_subst true subst context metasenv s1 s2 ugraph + in + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 + | (C.Prod _, _) -> + (match CicReduction.whd ~subst context t2 with + | C.Prod _ as t2 -> + fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph + | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product")))) + | (_, C.Prod _) -> + (match CicReduction.whd ~subst context t1 with + | C.Prod _ as t1 -> + fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph + | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product")))) | (_,_) -> (* delta-beta reduction should almost never be a problem for unification since: