-let classify ~subst ctx i status =
- let _, (NCic.Decl s | NCic.Def (s,_)) = List.nth ctx (i-1) in
- let _,ctx' = HExtlib.split_nth i ctx in
- let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in
- let status, s = term_of_cic_term status s ctx' in
- match s with
- | NCic.Appl [_;_;l;r] ->
- (* FIXME: metasenv *)
- if NCicReduction.are_convertible ~metasenv:[] ~subst ctx' l r
- then status, `Identity
- else status, (match hd_of_term l, hd_of_term r with
- | NCic.Const (NReference.Ref (_,NReference.Con (_,ki,nleft)) as kref),
- NCic.Const (NReference.Ref (_,NReference.Con (_,kj,_))) ->
- if ki != kj then `Discriminate (0,true)
- else
- let rit = NReference.mk_indty true kref in
- let _,_,its,_,itno = NCicEnvironment.get_checked_indtys rit in
- let it = List.nth its itno in
- let newprods = (nargs it nleft (ki-1)) + 1 in
- `Discriminate (newprods, false)
- | NCic.Rel j, _
- when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j r ->
- `Subst `LeftToRight
- | _, NCic.Rel j
- when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j l ->
- `Subst `RightToLeft
- | (NCic.Rel _, _ | _, NCic.Rel _ ) -> `Cycle
- | _ -> `Blob)
- | _ -> raise (Failure "classify")
+(* = select + classify *)
+let select_eq ctx acc status goal =
+ let classify ~subst ctx' l r =
+ (* FIXME: metasenv *)
+ if NCicReduction.are_convertible ~metasenv:[] ~subst ctx' l r
+ then status, `Identity
+ else status, (match hd_of_term l, hd_of_term r with
+ | NCic.Const (NReference.Ref (_,NReference.Con (_,ki,nleft)) as kref),
+ NCic.Const (NReference.Ref (_,NReference.Con (_,kj,_))) ->
+ if ki != kj then `Discriminate (0,true)
+ else
+ let rit = NReference.mk_indty true kref in
+ let _,_,its,_,itno = NCicEnvironment.get_checked_indtys rit in
+ let it = List.nth its itno in
+ let newprods = nargs it nleft (ki-1) in
+ `Discriminate (newprods, false)
+ | NCic.Rel j, _
+ when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j r ->
+ `Subst `LeftToRight
+ | _, NCic.Rel j
+ when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j l ->
+ `Subst `RightToLeft
+ | (NCic.Rel _, _ | _, NCic.Rel _ ) -> `Cycle
+ | _ -> `Blob) in
+ let rec aux i =
+ try
+ let index = List.length ctx - i in
+ pp (lazy ("provo classify di index = " ^string_of_int index));
+ match (List.nth ctx (index - 1)) with
+ | n, (NCic.Decl ty | NCic.Def (ty,_)) ->
+ (let _,ctx_ty = HExtlib.split_nth index ctx in
+ let status, ty = NTacStatus.whd status ctx_ty (mk_cic_term ctx_ty ty) in
+ let status, ty = term_of_cic_term status ty ctx_ty in
+ pp (lazy (Printf.sprintf "select_eq tries %s" (NCicPp.ppterm ~context:ctx_ty ~subst:[] ~metasenv:[] ty)));
+ match ty with
+ | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;l;r] when NUri.name_of_uri u = "eq" ->
+ (let status, kind = classify ~subst:(get_subst status) ctx_ty l r in
+ match kind with
+ | `Identity ->
+ let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in
+ status, Some (List.length ctx - i), kind
+ | `Cycle | `Blob -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
+ | _ ->
+ if (List.for_all (fun x -> x <> n) acc) then
+ status, Some (List.length ctx - i), kind
+ else aux (i+1))
+ | _ -> aux (i+1))
+ with Failure _ | Invalid_argument _ -> status, None, `Blob
+ in aux 0