X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicUnification.ml;h=912ae1e8e0cbbee2d4deba85595418032c9ce04b;hb=40a6a2eb15bc50a7fe8f47704ea0244bc9d18ef5;hp=8ba0ae917c828e807d85980acdb0a6a560a77718;hpb=5919a51b69b776dfc03cf44fab30263e232ef5f1;p=helm.git diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml index 8ba0ae917..912ae1e8e 100644 --- a/components/cic_unification/cicUnification.ml +++ b/components/cic_unification/cicUnification.ml @@ -53,22 +53,22 @@ let foo () = (sprintf "Kernel Type checking error: %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." - (CicMetaSubst.ppterm subst term) - (CicMetaSubst.ppterm [] term) - (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppterm ~metasenv subst term) + (CicMetaSubst.ppterm ~metasenv [] term) + (CicMetaSubst.ppcontext ~metasenv subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in + (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in raise (AssertFailure msg) | CicTypeChecker.AssertFailure msg -> let msg = lazy (sprintf "Kernel Type checking assertion failure: %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." - (CicMetaSubst.ppterm subst term) - (CicMetaSubst.ppterm [] term) - (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppterm ~metasenv subst term) + (CicMetaSubst.ppterm ~metasenv [] term) + (CicMetaSubst.ppcontext ~metasenv subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in + (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in raise (AssertFailure msg) in profiler_toa.HExtlib.profile foo () ;; @@ -367,16 +367,16 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (* (sprintf "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) *) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2))) *) | Invalid_argument _ -> raise (UnificationFailure (lazy "2"))) (* (sprintf "Error trying to unify %s with %s: the lengths of the two local contexts do not match." - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) *) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) *) in subst,metasenv,ugraph1 | (C.Meta (n,_), C.Meta (m,_)) when n>m -> fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph @@ -431,10 +431,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ C.Sort (C.Type u) when not test_equality_only -> let u' = CicUniv.fresh () in let s = C.Sort (C.Type u') in - let ugraph2 = - CicUniv.add_ge (upper u u') (lower u u') ugraph1 - in - s,ugraph2 + (try + let ugraph2 = + CicUniv.add_ge (upper u u') (lower u u') ugraph1 + in + s,ugraph2 + with + CicUniv.UniverseInconsistency msg -> + raise (UnificationFailure msg)) | _ -> t',ugraph1 in (* Unifying the types may have already instantiated n. Let's check *) @@ -460,8 +464,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ raise (UnificationFailure (lazy (sprintf "Can't unify %s with %s due to different constants" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 then fo_unif_subst_exp_named_subst @@ -472,8 +476,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (lazy (sprintf "Can't unify %s with %s due to different inductive principles" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) | C.MutConstruct (uri1,i1,j1,exp_named_subst1), C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then @@ -485,8 +489,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (lazy (sprintf "Can't unify %s with %s due to different inductive constructors" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only subst context metasenv te t2 ugraph @@ -589,55 +593,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 @@ -661,7 +703,7 @@ 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 subst t2 )))) + (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 )))) | _ -> raise exn))) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv',ugraph1 = @@ -681,8 +723,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ raise (UnificationFailure (lazy "6.1"))) (* (sprintf "Error trying to unify %s with %s: the number of branches is not the same." - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) *) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) *) | (C.Rel _, _) | (_, C.Rel _) -> if t1 = t2 then subst, metasenv,ugraph @@ -690,8 +732,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ raise (UnificationFailure (lazy (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) -> let subst,metasenv,beta_expanded,ugraph1 = beta_expand_many @@ -735,8 +777,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ raise (UnificationFailure (lazy (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2))))) *) | (_,_) -> (* delta-beta reduction should almost never be a problem for @@ -755,8 +797,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (lazy (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) else try fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph @@ -767,8 +809,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (lazy (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph @@ -785,7 +827,7 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv String.concat " ; " (List.map (fun (uri,t) -> - UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t) + UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t) ) ens) in raise (UnificationFailure (lazy (sprintf @@ -805,7 +847,7 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph = lazy ( if verbose then sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" - (CicMetaSubst.ppterm subst t1) + (CicMetaSubst.ppterm ~metasenv subst t1) (try let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in CicPp.ppterm ty_t1 @@ -813,7 +855,7 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph = | UnificationFailure s | Uncertain s | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppterm subst t2) + (CicMetaSubst.ppterm ~metasenv subst t2) (try let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in CicPp.ppterm ty_t2 @@ -821,28 +863,28 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph = | UnificationFailure s | Uncertain s | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppcontext ~metasenv subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) (Lazy.force msg) + (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg) else sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" - (CicMetaSubst.ppterm_in_context subst t1 context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context) (try let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in - CicMetaSubst.ppterm_in_context subst ty_t1 context + CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context with | UnificationFailure s | Uncertain s | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppterm_in_context subst t2 context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context) (try let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in - CicMetaSubst.ppterm_in_context subst ty_t2 context + CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context with | UnificationFailure s | Uncertain s | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppcontext ~metasenv subst context) (CicMetaSubst.ppmetasenv subst metasenv) (Lazy.force msg) )