- aux test_equality_only context t1 term' ugraph
- with CicUtil.Subst_not_found _ -> false,ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
- (try
- true,(CicUniv.add_eq t2 t1 ugraph)
- with CicUniv.UniverseInconsistency _ -> false,ugraph)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- (try
- true,(CicUniv.add_ge t2 t1 ugraph)
- with CicUniv.UniverseInconsistency _ -> false,ugraph)
- | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
- | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
- | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
- let b',ugraph' = aux true context s1 s2 ugraph in
- if b' then
- aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
- t1 t2 ugraph'
- else
- false,ugraph
- | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
- let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
- if b' then
- aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
- t1 t2 ugraph'
- else
- false,ugraph
- | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
- let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
- if b' then
- aux test_equality_only
- ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
- else
- false,ugraph
- | (C.Appl l1, C.Appl l2) ->
- (try
- List.fold_right2
- (fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph) l1 l2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
- let b' = U.eq uri1 uri2 in
- if b' then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.MutInd (uri1,i1,exp_named_subst1),
- C.MutInd (uri2,i2,exp_named_subst2)
- ) ->
- let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
- C.MutConstruct (uri2,i2,j2,exp_named_subst2)
- ) ->
- let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
- if b' then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.MutCase (uri1,i1,outtype1,term1,pl1),
- C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
- let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
- let b'',ugraph''=aux test_equality_only context
- outtype1 outtype2 ugraph in
- if b'' then
- let b''',ugraph'''= aux test_equality_only context
- term1 term2 ugraph'' in
- List.fold_right2
- (fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph)
- pl1 pl2 (b''',ugraph''')
- else
- false,ugraph
- else
- false,ugraph
- | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
- let tys,_ =
- List.fold_left
- (fun (types,len) (n,_,ty,_) ->
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- len+1)
- ) ([],0) fl1
- in
- if i1 = i2 then
- List.fold_right2
- (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
- if b && recindex1 = recindex2 then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
- | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
- let tys,_ =
- List.fold_left
- (fun (types,len) (n,ty,_) ->
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- len+1)
- ) ([],0) fl1
- in
- if i1 = i2 then
- List.fold_right2
- (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
- if b then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
- | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph
- | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph
- | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
- | (_,_) -> false,ugraph
- end
+ (try
+ HExtlib.list_forall_default3_var
+ (fun t1 t2 b -> not b || aux true context t1 t2 )
+ tl1 tl2 true relevance
+ with Invalid_argument _ -> false
+ | HExtlib.FailureAt fail ->
+ let relevance =
+ !get_relevance ~metasenv ~subst context hd1 tl1 in
+ let _,relevance = HExtlib.split_nth fail relevance in
+ let b,relevance = (match relevance with
+ | [] -> assert false
+ | b::tl -> b,tl) in
+ if (not b) then
+ let _,tl1 = HExtlib.split_nth (fail+1) tl1 in
+ let _,tl2 = HExtlib.split_nth (fail+1) tl2 in
+ try
+ HExtlib.list_forall_default3
+ (fun t1 t2 b -> not b || aux true context t1 t2)
+ tl1 tl2 true relevance
+ with Invalid_argument _ -> false
+ else false)
+
+ | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
+ aux test_eq_only context hd1 hd2 &&
+ let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in
+ (try
+ HExtlib.list_forall_default3
+ (fun t1 t2 b -> not b || aux true context t1 t2)
+ tl1 tl2 true relevance
+ with Invalid_argument _ -> false)
+
+ | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
+ C.Match (ref2,outtype2,term2,pl2)) ->
+ let _,_,itl,_,_ = E.get_checked_indtys ref1 in
+ let _,_,ty,_ = List.nth itl tyno in
+ let rec remove_prods ~subst context ty =
+ let ty = whd ~subst context ty in
+ match ty with
+ | C.Sort _ -> ty
+ | C.Prod (name,so,ta) -> remove_prods ~subst ((name,(C.Decl so))::context) ta
+ | _ -> assert false
+ in
+ let is_prop =
+ match remove_prods ~subst [] ty with
+ | C.Sort C.Prop -> true
+ | _ -> false
+ in
+ Ref.eq ref1 ref2 &&
+ aux test_eq_only context outtype1 outtype2 &&
+ (is_prop || aux test_eq_only context term1 term2) &&
+ (try List.for_all2 (aux test_eq_only context) pl1 pl2
+ with Invalid_argument _ -> false)
+ | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+ | (_,_) -> false
+;;
+
+(* t1, t2 must be well-typed *)
+let are_convertible ~metasenv ~subst =
+ let rec aux test_eq_only context t1 t2 =
+ let alpha_eq test_eq_only =
+ alpha_eq ~test_lambda_source:false aux test_eq_only metasenv subst context