-let rec select_eq ctx i status acc =
- try
- match (List.nth ctx (List.length ctx - i - 1)) with
- | n, (NCic.Decl s | NCic.Def (s,_)) ->
- (let _,ctx_s = HExtlib.split_nth (List.length ctx - i) ctx in
- let status, s = NTacStatus.whd status ctx_s (mk_cic_term ctx_s s) in
- let status, s = term_of_cic_term status s ctx_s in
- pp (lazy (Printf.sprintf "select_eq tries %s" (NCicPp.ppterm ~context:ctx_s ~subst:[] ~metasenv:[] s)));
- if (List.for_all (fun x -> x <> n) acc) then
- match s with
- | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;_;_] ->
- if NUri.name_of_uri u = "eq" then status, Some (List.length ctx - i)
- else select_eq ctx (i+1) status acc
- | _ -> select_eq ctx (i+1) status acc
- else select_eq ctx (i+1) status acc)
- with Failure _ | Invalid_argument _ -> status, None
+(* = 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)) + 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
+ 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
+ if NCicTypeChecker.does_not_occur ~subst:(get_subst status) ctx (index - 1) index goalty
+ then status, Some (List.length ctx - i), kind
+ else aux (i+1)
+ | `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