X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=36c114d8f8f85fff695a01040ec3185e83934247;hb=987627a48b2a3c2345d1af2c2a6b1ab78aa90b58;hp=91d10242d6469bf4f09f81701a5b30c2c9109585;hpb=094ad6d3aa96472adb6614f0f21f4cbdf94ad0bc;p=helm.git diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index 91d10242d..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,103 +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 - CoercDb.is_a_coercion' c1 && - CoercDb.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) -> (*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 + 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 = 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 + 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 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 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 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 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 _ -> + 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) + 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 car1 car2 in + let meets = + CoercGraph.meets + metasenv subst context (grow1,car1) (grow2,car2) + in (match meets with | [] -> raise exn - | _::_::_ -> -prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); -let m1::m2::_ = meets in -prerr_endline ("M1 = " ^ CoercDb.name_of_carr m1 ^ "\nM2 = " ^ CoercDb.name_of_carr m2); -assert false - | [m] -> - let last_tl1',(subst,metasenv,ugraph) = - match last_tl1 with - | Cic.Meta (i1,l1) - when not (CoercDb.eq_carr m car1) -> - (match - CoercGraph.look_for_coercion' metasenv subst - context m car1 - with - | CoercGraph.SomeCoercion [metasenv,last,coerced] - -> - last, - fo_unif_subst test_equality_only subst context - metasenv coerced last_tl1 ugraph - | _ -> -prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); -assert false) - | _ -> last_tl1,(subst,metasenv,ugraph) in - let last_tl2',(subst,metasenv,ugraph) = - match last_tl2 with - Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) -> - (match - CoercGraph.look_for_coercion' metasenv subst - context m car2 - with - (*CSC: bu here: I am considering only the first one*) - | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_) - -> - last, - fo_unif_subst test_equality_only subst context - metasenv coerced last_tl2 ugraph - | _ -> -prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); -assert false) - | _ -> 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 + | (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 - 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 + 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 @@ -710,7 +775,9 @@ res 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 = @@ -765,28 +832,22 @@ res 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: