X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=86f280842f6a7480bb95cb60b35f00811b89b9fc;hb=0de62d69d01f334e0300633d22b63c91edd8fc7f;hp=d1e010ca696558aefe36f8b2ec95f334634aea16;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index d1e010ca6..86f280842 100644 --- a/helm/software/components/cic_unification/cicUnification.ml +++ b/helm/software/components/cic_unification/cicUnification.ml @@ -39,10 +39,13 @@ let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand" let profiler_deref = HExtlib.profile "fo_unif_subst.deref'" let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible" +let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'" + let type_of_aux' metasenv subst context term ugraph = let foo () = try - CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph + profile.HExtlib.profile + (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph with CicTypeChecker.TypeCheckerFailure msg -> let msg = @@ -50,28 +53,32 @@ 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 () ;; let exists_a_meta l = - List.exists (function Cic.Meta _ -> true | _ -> false) l + List.exists + (function + | Cic.Meta _ + | Cic.Appl (Cic.Meta _::_) -> true + | _ -> false) l let rec deref subst t = let snd (_,a,_) = a in @@ -360,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 @@ -389,7 +396,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (lower m1 m2) (upper m1 m2) ugraph in begin - let subst,metasenv,ugraph1 = + let subst,metasenv,ugraph1 = let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in (try let tyt,ugraph1 = @@ -424,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 *) @@ -453,19 +464,20 @@ 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 test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure (lazy "4")) - (* (sprintf - "Can't unify %s with %s due to different inductive principles" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) *) + raise (UnificationFailure + (lazy + (sprintf + "Can't unify %s with %s due to different inductive principles" + (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 @@ -473,11 +485,12 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure (lazy "5")) - (* (sprintf + raise (UnificationFailure + (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 @@ -575,13 +588,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ fo_unif_l test_equality_only subst metasenv (lr1, lr2) ugraph with - | UnificationFailure _ - | Uncertain _ as exn -> + | 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 -> + CoercGraph.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 @@ -593,9 +607,15 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ | _ -> assert false in let is_composite1 = - List.exists ((=) (`Class `Coercion)) attrs1 in + List.exists + (function `Class (`Coercion _) -> true | _-> false) + attrs1 + in let is_composite2 = - List.exists ((=) (`Class `Coercion)) attrs2 in + List.exists + (function `Class (`Coercion _) -> true | _-> false) + attrs2 + in (match is_composite1, is_composite2 with | false, false -> raise exn | true, false -> @@ -622,6 +642,30 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ fo_unif_subst test_equality_only subst context metasenv redappl1 redappl2 ugraph) + (*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 + duplicated in two places: inside applications and + outside them. Probably it would be better to + work with lambda-bar terms instead. *) + | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn + | (_, Cic.MutInd _::_) -> + let t1' = R.whd ~subst context t1 in + (match t1' with + C.Appl (C.MutInd _::_) -> + fo_unif_subst test_equality_only + subst context metasenv t1' t2 ugraph + | _ -> raise (UnificationFailure (lazy "88"))) + | (Cic.MutInd _::_,_) -> + let t2' = R.whd ~subst context t2 in + (match t2' with + C.Appl (C.MutInd _::_) -> + fo_unif_subst test_equality_only + subst context metasenv t1 t2' ugraph + | _ -> raise + (UnificationFailure + (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 = @@ -641,8 +685,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 @@ -650,8 +694,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 @@ -666,26 +710,18 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ in fo_unif_subst test_equality_only subst context metasenv beta_expanded (C.Meta (i,l)) ugraph1 - | (C.Sort _ ,_) | (_, C.Sort _) - | (C.Const _, _) | (_, C.Const _) - | (C.MutInd _, _) | (_, C.MutInd _) - | (C.MutConstruct _, _) | (_, C.MutConstruct _) - | (C.Fix _, _) | (_, C.Fix _) - | (C.CoFix _, _) | (_, C.CoFix _) -> - if t1 = t2 then - subst, metasenv, ugraph - else - let b,ugraph1 = - R.are_convertible ~subst ~metasenv context t1 t2 ugraph - in - if b then - subst, metasenv, ugraph1 - else - raise - (UnificationFailure (lazy (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) +(* Works iff there are no arguments applied to it; similar to the + case below + | (_, C.MutInd _) -> + let t1' = R.whd ~subst context t1 in + (match t1' with + C.MutInd _ -> + fo_unif_subst test_equality_only + 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 @@ -703,14 +739,40 @@ 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))))) +*) | (_,_) -> - raise (UnificationFailure (lazy "10")) - (* (sprintf + (* delta-beta reduction should almost never be a problem for + unification since: + 1. long computations require iota reduction + 2. it is extremely rare that a close term t1 (that could be unified + to t2) beta-delta reduces to t1' while t2 does not beta-delta + reduces in the same way. This happens only if one meta of t2 + occurs in head position during beta reduction. In this unluky + case too much reduction will be performed on t1 and unification + will surely fail. *) + let t1' = CicReduction.head_beta_reduce ~delta:true t1 in + let t2' = CicReduction.head_beta_reduce ~delta:true t2 in + if t1 = t1' && t2 = t2' then + 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)))) + else + try + fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph + with + UnificationFailure _ + | Uncertain _ -> + 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)))) and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph @@ -727,7 +789,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 @@ -747,7 +809,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 @@ -755,7 +817,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 @@ -763,28 +825,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) )