open Printf
-exception AssertFailure of string;;
exception UnificationFailure of string;;
+exception Uncertain of string;;
+exception AssertFailure of string;;
let debug_print = prerr_endline
let type_of_aux' metasenv subst context term =
try
CicMetaSubst.type_of_aux' metasenv subst context term
- with CicMetaSubst.MetaSubstFailure msg ->
+ with
+ | CicMetaSubst.MetaSubstFailure msg ->
raise (AssertFailure
((sprintf
- "Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
- (CicPp.ppterm (CicMetaSubst.apply_subst subst term))
- (CicMetaSubst.ppcontext subst context) msg)))
+ "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
+ (CicMetaSubst.ppterm subst term)
+ (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppmetasenv metasenv subst) msg)))
(* NUOVA UNIFICAZIONE *)
(* A substitution is a (int * Cic.term) list that associates a
let module S = CicSubstitution in
match (t1, t2) with
(C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
- let ok =
+ let ok,subst,metasenv =
+ try
List.fold_left2
- (fun b t1 t2 ->
- b &&
+ (fun (b,subst,metasenv) t1 t2 ->
+ if b then true,subst,metasenv else
match t1,t2 with
None,_
- | _,None -> true
+ | _,None -> true,subst,metasenv
| Some t1', Some t2' ->
(* First possibility: restriction *)
(* Second possibility: unification *)
(* Third possibility: convertibility *)
- R.are_convertible subst context t1' t2'
- ) true ln lm
+ if R.are_convertible subst context t1' t2' then
+ true,subst,metasenv
+ else
+ (try
+ let subst,metasenv =
+ fo_unif_subst subst context metasenv t1' t2'
+ in
+ true,subst,metasenv
+ with
+ Not_found -> false,subst,metasenv)
+ ) (true,subst,metasenv) ln lm
+ with
+ Invalid_argument _ ->
+ raise (UnificationFailure (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)))
in
if ok then
subst,metasenv
else
raise (UnificationFailure (sprintf
- "Error trying to unify %s with %s: the algorithm only tried to check convertibility of the two substitutions"
- (CicPp.ppterm t1) (CicPp.ppterm t2)))
- | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
+ "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)))
+ | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
fo_unif_subst subst context metasenv t2 t1
| (C.Meta (n,l), t)
| (t, C.Meta (n,l)) ->
- let subst',metasenv' =
+ let swap =
+ match t1,t2 with
+ C.Meta (n,_), C.Meta (m,_) when n < m -> false
+ | _, C.Meta _ -> false
+ | _,_ -> true
+ in
+ let lower = fun x y -> if swap then y else x in
+ let upper = fun x y -> if swap then x else y in
+ let fo_unif_subst_ordered subst context metasenv m1 m2 =
+ fo_unif_subst subst context metasenv (lower m1 m2) (upper m1 m2)
+ in
+ let subst'',metasenv' =
try
let oldt = (List.assoc n subst) in
let lifted_oldt = S.lift_meta l oldt in
- fo_unif_subst subst context metasenv lifted_oldt t
+ fo_unif_subst_ordered subst context metasenv t lifted_oldt
with Not_found ->
- let t',metasenv' = CicMetaSubst.delift context metasenv l t in
- (n, t')::subst, metasenv'
+ let t',metasenv',subst' =
+ try
+ CicMetaSubst.delift n subst context metasenv l t
+ with
+ (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
+ | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
+ in
+ (n, t')::subst', metasenv'
in
- let (_,_,meta_type) =
- List.find (function (m,_,_) -> m=n) metasenv' in
- let tyt = type_of_aux' metasenv' subst' context t in
- fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+ let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in
+ (try
+ let tyt =
+ type_of_aux' metasenv' subst'' context t
+ in
+ fo_unif_subst subst'' context metasenv' tyt (S.lift_meta l meta_type)
+ with AssertFailure _ ->
+ (* TODO huge hack!!!!
+ * we keep on unifying/refining in the hope that the problem will be
+ * eventually solved. In the meantime we're breaking a big invariant:
+ * the terms that we are unifying are no longer well typed in the
+ * current context (in the worst case we could even diverge)
+ *)
+(*
+prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
+prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
+*)
+ (subst'', metasenv'))
| (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
| (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
if UriManager.eq uri1 uri2 then
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different constants"
- (CicPp.ppterm t1) (CicPp.ppterm t1)))
+ (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm 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 subst context metasenv
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different inductive principles"
- (CicPp.ppterm t1) (CicPp.ppterm t1)))
+ (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm 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
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different inductive constructors"
- (CicPp.ppterm t1) (CicPp.ppterm t1)))
- | (C.Implicit, _) | (_, C.Implicit) -> assert false
+ (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+ | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
| (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
| (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
fo_unif_l subst' metasenv' (l1,l2)
in
fo_unif_l subst metasenv (lr1, lr2)
- | (C.MutCase (_,_,outt1,t1,pl1), C.MutCase (_,_,outt2,t2,pl2))->
+ | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
let subst', metasenv' =
fo_unif_subst subst context metasenv outt1 outt2 in
let subst'',metasenv'' =
- fo_unif_subst subst' context metasenv' t1 t2 in
- List.fold_left2
- (function (subst,metasenv) ->
- fo_unif_subst subst context metasenv
- ) (subst'',metasenv'') pl1 pl2
+ fo_unif_subst subst' context metasenv' t1' t2' in
+ (try
+ List.fold_left2
+ (function (subst,metasenv) ->
+ fo_unif_subst subst context metasenv
+ ) (subst'',metasenv'') pl1 pl2
+ with
+ Invalid_argument _ ->
+ raise (UnificationFailure (sprintf
+ "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
| (C.Rel _, _) | (_, C.Rel _)
| (C.Sort _ ,_) | (_, C.Sort _)
| (C.Const _, _) | (_, C.Const _)
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s because they are not convertible"
- (CicPp.ppterm t1) (CicPp.ppterm t2)))
+ (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
| (_,_) ->
if R.are_convertible subst context t1 t2 then
subst, metasenv
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s because they are not convertible"
- (CicPp.ppterm t1) (CicPp.ppterm t2)))
+ (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
and fo_unif_subst_exp_named_subst subst context metasenv
exp_named_subst1 exp_named_subst2
=
-try
- List.fold_left2
- (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
- assert (uri1=uri2) ;
- fo_unif_subst subst context metasenv t1 t2
- ) (subst,metasenv) exp_named_subst1 exp_named_subst2
-with
-e ->
-let uri = UriManager.uri_of_string "cic:/dummy.var" in
-debug_print ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^
-" <==> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst2))) ; raise e
+ try
+ List.fold_left2
+ (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
+ assert (uri1=uri2) ;
+ fo_unif_subst subst context metasenv t1 t2
+ ) (subst,metasenv) exp_named_subst1 exp_named_subst2
+ with
+ Invalid_argument _ ->
+ let print_ens ens =
+ String.concat " ; "
+ (List.map
+ (fun (uri,t) ->
+ UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
+ ) ens)
+ in
+ raise (UnificationFailure (sprintf
+ "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))
(* A substitution is a (int * Cic.term) list that associates a *)
(* metavariable i with its body. *)
(* a new substitution which is already unwinded and ready to be applied and *)
(* a new metasenv in which some hypothesis in the contexts of the *)
(* metavariables may have been restricted. *)
-let fo_unif metasenv context t1 t2 =
- let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv t1 t2 in
- CicMetaSubst.unwind_subst metasenv' subst_to_unwind
-;;
+let fo_unif metasenv context t1 t2 = fo_unif_subst [] context metasenv t1 t2 ;;
let fo_unif_subst subst context metasenv t1 t2 =
let enrich_msg msg =
sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
- (CicPp.ppterm (CicMetaSubst.apply_subst subst t1))
+ (CicMetaSubst.ppterm subst t1)
(try
CicPp.ppterm (type_of_aux' metasenv subst context t1)
with _ -> "MALFORMED")
- (CicPp.ppterm (CicMetaSubst.apply_subst subst t2))
+ (CicMetaSubst.ppterm subst t2)
(try
CicPp.ppterm (type_of_aux' metasenv subst context t2)
with _ -> "MALFORMED")
(CicMetaSubst.ppcontext subst context)
- (CicMetaSubst.ppmetasenv subst metasenv) msg
+ (CicMetaSubst.ppmetasenv metasenv subst) msg
in
try
fo_unif_subst subst context metasenv t1 t2
projects / helm.git / blobdiff