-let are_convertible whd ?(subst=[]) ?(metasenv=[]) =
- let heuristic = ref true in
- let rec aux test_equality_only context t1 t2 ugraph =
- let rec aux2 test_equality_only t1 t2 ugraph =
-
- (* this trivial euristic cuts down the total time of about five times ;-) *)
- (* this because most of the time t1 and t2 are "sintactically" the same *)
- if t1 === t2 then
- true,ugraph
- else
- begin
- let module C = Cic in
- match (t1,t2) with
- (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
- | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
- if U.eq uri1 uri2 then
- (try
- List.fold_right2
- (fun (uri1,x) (uri2,y) (b,ugraph) ->
- let b',ugraph' = aux test_equality_only context x y ugraph in
- (U.eq uri1 uri2 && b' && b),ugraph'
- ) exp_named_subst1 exp_named_subst2 (true,ugraph)
- with
- Invalid_argument _ -> false,ugraph
- )
- else
- false,ugraph
- | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
- if n1 = n2 then
- let b2, ugraph1 =
- let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
- let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
- List.fold_left2
- (fun (b,ugraph) t1 t2 ->
- if b then
- match t1,t2 with
- None,_
- | _,None -> true,ugraph
- | Some t1',Some t2' ->
- aux test_equality_only context t1' t2' ugraph
- else
- false,ugraph
- ) (true,ugraph) l1 l2
- in
- if b2 then true,ugraph1 else false,ugraph
- else
- false,ugraph
- | C.Meta (n1,l1), _ ->
- (try
- let _,term,_ = NCicUtils.lookup_subst n1 subst in
- let term' = CicSubstitution.subst_meta l1 term in
-(*
-prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2);
-prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t2);
-*)
- aux test_equality_only context term' t2 ugraph
- with CicUtil.Subst_not_found _ -> false,ugraph)
- | _, C.Meta (n2,l2) ->
- (try
- let _,term,_ = CicUtil.lookup_subst n2 subst in
- let term' = CicSubstitution.subst_meta l2 term in
-(*
-prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2);
-prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
-*)
- 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