- (try
- fo_unif_l
- test_equality_only subst metasenv (lr1, lr2) ugraph
- with
- | UnificationFailure s
- | Uncertain s as exn ->
- (match l1, l2 with
- (* {{{ pullback *)
- | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
- (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
- CoercDb.is_a_coercion cc1 <> None &&
- CoercDb.is_a_coercion cc2 <> None &&
- not (UriManager.eq uri1 uri2) ->
-(*DEBUGGING ONLY:
-prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
-*)
- let inner_coerced t =
- let t = CicMetaSubst.apply_subst subst t in
- let rec aux c x t =
- match t with
- | Cic.Appl l ->
- (match CoercGraph.coerced_arg l with
- | None -> c, x
- | Some (t,_) -> aux (List.hd l) t t)
- | _ -> c, x
- in
- aux (Cic.Implicit None) (Cic.Implicit None) t
- in
- let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
- let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
- let car1, car2 =
- match
- CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
- with
- | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
- | _ -> assert false
- in
- let head1_c, head2_c =
- match
- CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
- with
- | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
- | _ -> assert false
- in
- let unfold uri ens args =
- let o, _ =
- CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
- in
- assert (ens = []);
- match o with
- | Cic.Constant (_,Some bo,_,_,_) ->
- CicReduction.head_beta_reduce ~delta:false
- (Cic.Appl (bo::args))
- | _ -> assert false
- in
- let conclude subst metasenv ugraph last_tl1' last_tl2' =
- let subst',metasenv,ugraph =
-(*DEBUGGING ONLY:
-prerr_endline
- ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
- " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
-*)
- fo_unif_subst test_equality_only subst context
- metasenv last_tl1' last_tl2' ugraph
- in
- if subst = subst' then raise exn
- else
-(*DEBUGGING ONLY:
-let subst,metasenv,ugrph as res =
-*)
- fo_unif_subst test_equality_only subst' context
- metasenv (C.Appl l1) (C.Appl l2) ugraph
-(*DEBUGGING ONLY:
-in
-(prerr_endline
- (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
- " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
-res)
-*)
- in
- if CoercDb.eq_carr car1 car2 then
- match last_tl1,last_tl2 with
- | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
- | _, C.Meta _
- | C.Meta _, _ ->
- let subst,metasenv,ugraph =
- fo_unif_subst test_equality_only subst context
- metasenv last_tl1 last_tl2 ugraph
- in
- fo_unif_subst test_equality_only subst context
- metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
- | _ when CoercDb.eq_carr head1_c head2_c ->
- (* composite VS composition + metas avoiding
- * coercions not only in coerced position *)
- if c1 <> cc1 && c2 <> cc2 then
- conclude subst metasenv ugraph
- last_tl1 last_tl2
- else
- let l1, l2 =
- if c1 = cc1 then
- unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
- else
- Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
- in
- fo_unif_subst test_equality_only subst context
- metasenv l1 l2 ugraph
- | _ -> raise exn
- else
- let grow1 =
- match last_tl1 with Cic.Meta _ -> true | _ -> false in
- let grow2 =
- match last_tl2 with Cic.Meta _ -> true | _ -> false in
- if not (grow1 || grow2) then
- (* no flexible terminals -> no pullback, but
- * we still unify them, in some cases it helps *)
- conclude subst metasenv ugraph last_tl1 last_tl2
- else
- let meets =
- CoercGraph.meets
- metasenv subst context (grow1,car1) (grow2,car2)
- in
- (match meets with
- | [] -> raise exn
- | (carr,metasenv,to1,to2)::xxx ->
- warn_if_not_unique xxx to1 to2 carr car1 car2;
- let last_tl1',(subst,metasenv,ugraph) =
- match grow1,to1 with
- | true,Some (last,coerced) ->
- last,
- fo_unif_subst test_equality_only subst context
- metasenv coerced last_tl1 ugraph
- | _ -> last_tl1,(subst,metasenv,ugraph)
- in
- let last_tl2',(subst,metasenv,ugraph) =
- match grow2,to2 with
- | true,Some (last,coerced) ->
- last,
- fo_unif_subst test_equality_only subst context
- metasenv coerced last_tl2 ugraph
- | _ -> last_tl2,(subst,metasenv,ugraph)
- in
- conclude subst metasenv ugraph last_tl1' last_tl2')
- (* }}} pullback *)
- (* {{{ CSC: This is necessary because of the "elim H" tactic
- where the type of H is only reducible to an
- inductive type. This could be extended from inductive
- types to any rigid term. However, the code is
- duplicated in two places: inside applications and
- outside them. Probably it would be better to
- work with lambda-bar terms instead. *)
- | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
- | (_, Cic.MutInd _::_) ->
- let t1' = R.whd ~subst context t1 in
- (match t1' with
- C.Appl (C.MutInd _::_) ->
- fo_unif_subst test_equality_only
- subst context metasenv t1' t2 ugraph
- | _ -> raise (UnificationFailure (lazy "88")))
- | (Cic.MutInd _::_,_) ->
- let t2' = R.whd ~subst context t2 in
- (match t2' with
- C.Appl (C.MutInd _::_) ->
- fo_unif_subst test_equality_only
- subst context metasenv t1 t2' ugraph
- | _ -> raise
- (UnificationFailure
- (lazy ("not a mutind :"^
- CicMetaSubst.ppterm ~metasenv subst t2 ))))
- (* }}} elim H *)
- | _ -> raise exn)))
- | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
- let subst', metasenv',ugraph1 =
- fo_unif_subst test_equality_only subst context metasenv outt1 outt2
- ugraph in
- let subst'',metasenv'',ugraph2 =
- fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
- ugraph1 in
- (try
- List.fold_left2
- (fun (subst,metasenv,ugraph) t1 t2 ->
- fo_unif_subst
- test_equality_only subst context metasenv t1 t2 ugraph
- ) (subst'',metasenv'',ugraph2) pl1 pl2
- with
- Invalid_argument _ ->
- raise (UnificationFailure (lazy "6.1")))
- (* (sprintf
- "Error trying to unify %s with %s: the number of branches is not the same."
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
- | (C.Rel _, _) | (_, C.Rel _) ->
- if t1 = t2 then
- subst, metasenv,ugraph
- else
- raise (UnificationFailure (lazy
- (sprintf
- "Can't unify %s with %s because they are not convertible"
- (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
- test_equality_only metasenv subst context t2 args ugraph
- in
- fo_unif_subst test_equality_only subst context metasenv
- (C.Meta (i,l)) beta_expanded ugraph1
- | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
- let subst,metasenv,beta_expanded,ugraph1 =
- beta_expand_many
- test_equality_only metasenv subst context t1 args ugraph
- in
- fo_unif_subst test_equality_only subst context metasenv
- beta_expanded (C.Meta (i,l)) ugraph1
-(* Works iff there are no arguments applied to it; similar to the
- case below
- | (_, C.MutInd _) ->
- let t1' = R.whd ~subst context t1 in
- (match t1' with
- C.MutInd _ ->
- fo_unif_subst test_equality_only
- subst context metasenv t1' t2 ugraph
- | _ -> raise (UnificationFailure (lazy "8")))
-*)
- | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
- let subst',metasenv',ugraph1 =
- fo_unif_subst true subst context metasenv s1 s2 ugraph
- in
- fo_unif_subst test_equality_only
- subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
- | (C.Prod _, _) ->
- (match CicReduction.whd ~subst context t2 with
- | C.Prod _ as t2 ->
- fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
- | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
- | (_, C.Prod _) ->
- (match CicReduction.whd ~subst context t1 with
- | C.Prod _ as t1 ->
- fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
- | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
- | (_,_) ->
- (* delta-beta reduction should almost never be a problem for
- unification since:
- 1. long computations require iota reduction
- 2. it is extremely rare that a close term t1 (that could be unified
- to t2) beta-delta reduces to t1' while t2 does not beta-delta
- reduces in the same way. This happens only if one meta of t2
- occurs in head position during beta reduction. In this unluky
- case too much reduction will be performed on t1 and unification
- will surely fail. *)
- let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
- let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
- if t1 = t1' && t2 = t2' then
- raise (UnificationFailure
- (lazy
- (sprintf
- "Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2))))
- else
- try
- fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
- with
- UnificationFailure _
- | Uncertain _ ->
- raise (UnificationFailure
- (lazy
- (sprintf
- "Can't unify %s with %s because they are not convertible"
- (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
-=
- try
- List.fold_left2
- (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
- assert (uri1=uri2) ;
- fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
- ) (subst,metasenv,ugraph) 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 ~metasenv subst t)
- ) ens)
- in
- raise (UnificationFailure (lazy (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. *)
-(* metasenv is of type Cic.metasenv *)
-(* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
-(* 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 ugraph =
- fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
-
-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 ~metasenv subst t1)
- (try
- let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
- CicPp.ppterm ty_t1
- with
- | UnificationFailure s
- | Uncertain s
- | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
- (CicMetaSubst.ppterm ~metasenv subst t2)
- (try
- let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
- CicPp.ppterm ty_t2
- with
- | UnificationFailure s
- | Uncertain s
- | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
- (CicMetaSubst.ppcontext ~metasenv subst context)
- (CicMetaSubst.ppmetasenv subst metasenv)
- (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 ~metasenv subst t1 context)
- (try
- let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
- CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
- with
- | UnificationFailure s
- | Uncertain s
- | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
- (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 ~metasenv subst ty_t2 context
- with
- | UnificationFailure s
- | Uncertain s
- | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
- (CicMetaSubst.ppcontext ~metasenv subst context)
- (CicMetaSubst.ppmetasenv subst metasenv)
- (Lazy.force msg)
- )
-
-let fo_unif_subst subst context metasenv t1 t2 ugraph =
- try
- fo_unif_subst false subst context metasenv t1 t2 ugraph
- with
- | AssertFailure msg ->
- raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
- | UnificationFailure msg ->
- raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
+ unify hdb test_eq_only metasenv subst context
+ beta_expanded (C.Meta (i,l))
+
+ (* processing this case here we avoid a useless small delta step *)
+ | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
+ when Ref.eq r1 r2 ->
+ let relevance = NCicEnvironment.get_relevance r1 in
+ let relevance = match r1 with
+ | Ref.Ref (_,Ref.Con (_,_,lno)) ->
+ let _,relevance = HExtlib.split_nth lno relevance in
+ HExtlib.mk_list false lno @ relevance
+ | _ -> relevance
+ in
+ let metasenv, subst, _ =
+ try
+ List.fold_left2
+ (fun (metasenv, subst, relevance) t1 t2 ->
+ let b, relevance =
+ match relevance with b::tl -> b,tl | _ -> true, [] in
+ let metasenv, subst =
+ try unify hdb test_eq_only metasenv subst context t1 t2
+ with UnificationFailure _ | Uncertain _ when not b ->
+ metasenv, subst
+ in
+ metasenv, subst, relevance)
+ (metasenv, subst, relevance) tl1 tl2
+ with Invalid_argument _ ->
+ raise (uncert_exc metasenv subst context t1 t2)
+ in
+ metasenv, subst
+
+ | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
+ C.Match (ref2,outtype2,term2,pl2)) ->
+ let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
+ let _,_,ty,_ = List.nth itl tyno in
+ let rec remove_prods ~subst context ty =
+ let ty = NCicReduction.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
+ if not (Ref.eq ref1 ref2) then
+ raise (uncert_exc metasenv subst context t1 t2)
+ else
+ let metasenv, subst =
+ unify hdb test_eq_only metasenv subst context outtype1 outtype2 in
+ let metasenv, subst =
+ try unify hdb test_eq_only metasenv subst context term1 term2
+ with UnificationFailure _ | Uncertain _ when is_prop ->
+ metasenv, subst
+ in
+ (try
+ List.fold_left2
+ (fun (metasenv,subst) ->
+ unify hdb test_eq_only metasenv subst context)
+ (metasenv, subst) pl1 pl2
+ with Invalid_argument _ ->
+ raise (uncert_exc metasenv subst context t1 t2))
+ | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+ | _ when NCicUntrusted.metas_of_term subst context t1 = [] &&
+ NCicUntrusted.metas_of_term subst context t2 = [] ->
+ raise (fail_exc metasenv subst context t1 t2)
+ | _ -> raise (uncert_exc metasenv subst context t1 t2)
+ (*D*) in outside(); rc with exn -> outside (); raise exn
+ in
+ let try_hints metasenv subst t1 t2 (* exc*) =
+ let candidates =
+ NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
+ in
+ let rec cand_iter = function
+ | [] -> None (* raise exc *)
+ | (metasenv,c1,c2)::tl ->
+ try
+ let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in
+ let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in
+ Some (metasenv, subst)
+ with
+ UnificationFailure _ | Uncertain _ -> cand_iter tl
+ in
+ cand_iter candidates
+ in
+ let height_of = function
+ | NCic.Const (Ref.Ref (_,Ref.Def h))
+ | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
+ | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
+ | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
+ | _ -> 0
+ in
+ let put_in_whd m1 m2 =
+ NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
+ NCicReduction.reduce_machine ~delta:max_int ~subst context m2
+ in
+ let small_delta_step ~subst
+ ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
+ =
+ assert (not (norm1 && norm2));
+ if norm1 then
+ x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
+ else if norm2 then
+ NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
+ else
+ let h1 = height_of t1 in
+ let h2 = height_of t2 in
+ let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
+ NCicReduction.reduce_machine ~delta ~subst context m1,
+ NCicReduction.reduce_machine ~delta ~subst context m2
+ in
+ let rec unif_machines metasenv subst =
+ function
+ | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
+ (*D*) inside 'M'; try let rc =
+ pp (lazy("UM: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context
+ (NCicReduction.unwind (k1,e1,t1,s1)) ^
+ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context
+ (NCicReduction.unwind (k2,e2,t2,s2))));
+pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
+ let relevance = [] (* TO BE UNDERSTOOD
+ match t1 with
+ | C.Const r -> NCicEnvironment.get_relevance r
+ | _ -> [] *) in
+ let unif_from_stack t1 t2 b metasenv subst =
+ try
+ let t1 = NCicReduction.from_stack t1 in
+ let t2 = NCicReduction.from_stack t2 in
+ unif_machines metasenv subst (put_in_whd t1 t2)
+ with UnificationFailure _ | Uncertain _ when not b ->
+ metasenv, subst
+ in
+ let rec check_stack l1 l2 r todo =
+ match l1,l2,r with
+ | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
+ | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
+ | l1, l2, _ ->
+ NCicReduction.unwind (k1,e1,t1,List.rev l1),
+ NCicReduction.unwind (k2,e2,t2,List.rev l2),
+ todo
+ in
+ let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
+ try
+ let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in
+ List.fold_left
+ (fun (metasenv,subst) (x1,x2,r) ->
+ unif_from_stack x1 x2 r metasenv subst
+ ) (metasenv,subst) todo
+ with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
+ unif_machines metasenv subst (small_delta_step ~subst m1 m2)
+ (*D*) in outside(); rc with exn -> outside (); raise exn
+ in
+ try fo_unif test_eq_only metasenv subst t1 t2
+ with UnificationFailure msg | Uncertain msg as exn ->
+ match try_hints metasenv subst t1 t2 with
+ | Some x -> x
+ | None ->
+ try
+ unif_machines metasenv subst
+ (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
+ with
+ | UnificationFailure _ -> raise (UnificationFailure msg)
+ | Uncertain _ -> raise exn
+ (*D*) in outside(); rc with exn -> outside (); raise exn