a new substitution which is _NOT_ unwinded. It must be unwinded before
applying it. *)
-let rec fo_unif_subst subst context metasenv t1 t2 =
+let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 =
let module C = Cic in
let module R = CicMetaSubst in
let module S = CicSubstitution in
else
(try
let subst,metasenv =
- fo_unif_subst subst context metasenv t1' t2'
+ fo_unif_subst
+ test_equality_only subst context metasenv t1' t2'
in
true,subst,metasenv
with
"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
+ fo_unif_subst test_equality_only subst context metasenv t2 t1
| (C.Meta (n,l), t)
| (t, C.Meta (n,l)) ->
let swap =
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)
+ let fo_unif_subst_ordered
+ test_equality_only subst context metasenv m1 m2 =
+ fo_unif_subst test_equality_only 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_ordered subst context metasenv t lifted_oldt
+ fo_unif_subst_ordered
+ test_equality_only subst context metasenv t lifted_oldt
with Not_found ->
let t',metasenv',subst' =
try
(CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
| (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
in
- (n, t')::subst', metasenv'
+ let t'' =
+ match t' with
+ C.Sort (C.Type u) when not test_equality_only ->
+ let u' = CicUniv.fresh () in
+ let s = C.Sort (C.Type u') in
+ ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
+ s
+ | _ -> t'
+ in
+ (n, t'')::subst', metasenv'
in
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)
+ fo_unif_subst
+ test_equality_only
+ 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
| (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
- fo_unif_subst_exp_named_subst subst context metasenv
+ fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
exp_named_subst1 exp_named_subst2
else
raise (UnificationFailure (sprintf
(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
+ fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
exp_named_subst1 exp_named_subst2
else
raise (UnificationFailure (sprintf
| 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
- fo_unif_subst_exp_named_subst subst context metasenv
+ fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
exp_named_subst1 exp_named_subst2
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different inductive constructors"
(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.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
+ subst context metasenv te t2
+ | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
+ subst context metasenv t1 te
| (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
- let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
- fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
+ (* TASSI: this is the only case in which we want == *)
+ let subst',metasenv' = fo_unif_subst true
+ subst context metasenv s1 s2 in
+ fo_unif_subst test_equality_only
+ subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
| (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
- let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
- fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
+ (* TASSI: ask someone a reason for not putting true here *)
+ let subst',metasenv' = fo_unif_subst test_equality_only
+ subst context metasenv s1 s2 in
+ fo_unif_subst test_equality_only
+ subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
| (C.LetIn (_,s1,t1), t2)
| (t2, C.LetIn (_,s1,t1)) ->
- fo_unif_subst subst context metasenv t2 (S.subst s1 t1)
+ fo_unif_subst
+ test_equality_only subst context metasenv t2 (S.subst s1 t1)
| (C.Appl l1, C.Appl l2) ->
let lr1 = List.rev l1 in
let lr2 = List.rev l2 in
- let rec fo_unif_l subst metasenv =
+ let rec fo_unif_l test_equality_only subst metasenv =
function
[],_
| _,[] -> assert false
| ([h1],[h2]) ->
- fo_unif_subst subst context metasenv h1 h2
+ fo_unif_subst test_equality_only subst context metasenv h1 h2
| ([h],l)
| (l,[h]) ->
- fo_unif_subst subst context metasenv h (C.Appl (List.rev l))
+ fo_unif_subst
+ test_equality_only subst context metasenv h (C.Appl (List.rev l))
| ((h1::l1),(h2::l2)) ->
let subst', metasenv' =
- fo_unif_subst subst context metasenv h1 h2
+ fo_unif_subst test_equality_only subst context metasenv h1 h2
in
- fo_unif_l subst' metasenv' (l1,l2)
+ fo_unif_l test_equality_only subst' metasenv' (l1,l2)
in
- fo_unif_l subst metasenv (lr1, lr2)
+ fo_unif_l test_equality_only subst metasenv (lr1, lr2)
| (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
let subst', metasenv' =
- fo_unif_subst subst context metasenv outt1 outt2 in
+ fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
let subst'',metasenv'' =
- fo_unif_subst subst' context metasenv' t1' t2' in
+ fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in
(try
List.fold_left2
(function (subst,metasenv) ->
- fo_unif_subst subst context metasenv
+ fo_unif_subst test_equality_only subst context metasenv
) (subst'',metasenv'') pl1 pl2
with
Invalid_argument _ ->
"Can't unify %s with %s because they are not convertible"
(CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
-and fo_unif_subst_exp_named_subst subst context metasenv
+and fo_unif_subst_exp_named_subst test_equality_only 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
+ fo_unif_subst test_equality_only subst context metasenv t1 t2
) (subst,metasenv) exp_named_subst1 exp_named_subst2
with
Invalid_argument _ ->
(* 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 = fo_unif_subst [] context metasenv t1 t2 ;;
+let fo_unif metasenv context t1 t2 =
+ fo_unif_subst false [] context metasenv t1 t2 ;;
let fo_unif_subst subst context metasenv t1 t2 =
let enrich_msg msg =
(CicMetaSubst.ppmetasenv metasenv subst) msg
in
try
- fo_unif_subst subst context metasenv t1 t2
+ fo_unif_subst false subst context metasenv t1 t2
with
| AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
| UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))
projects / helm.git / blobdiff