X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicUnification.ml;h=86f280842f6a7480bb95cb60b35f00811b89b9fc;hb=94873bb61a663b4fca3dc6d07b7bb9f42122003e;hp=6004e73fa98e71497447e5d72357683907ea88c0;hpb=020ec6bc6c14c1e39b2564da314a6079bb34f79c;p=helm.git diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml index 6004e73fa..86f280842 100644 --- a/components/cic_unification/cicUnification.ml +++ b/components/cic_unification/cicUnification.ml @@ -53,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 @@ -363,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 @@ -427,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 *) @@ -456,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 @@ -468,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 @@ -481,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 @@ -655,7 +663,9 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ C.Appl (C.MutInd _::_) -> fo_unif_subst test_equality_only subst context metasenv t1 t2' ugraph - | _ -> raise (UnificationFailure (lazy "99"))) + | _ -> 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 = @@ -675,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 @@ -684,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 @@ -729,8 +739,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 @@ -749,8 +759,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 @@ -761,8 +771,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 @@ -779,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 @@ -799,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 @@ -807,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 @@ -815,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) )