;;
(* the argument must be a term in whd *)
-let rec could_reduce =
+let rec could_reduce status ~subst context =
function
| C.Meta _ -> true
| C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
- when List.length args > recno -> could_reduce (List.nth args recno)
- | C.Match (_,_,arg,_) -> could_reduce arg
- | C.Appl (he::_) -> could_reduce he
+ when List.length args > recno ->
+ let t = NCicReduction.whd status ~subst context (List.nth args recno) in
+ could_reduce status ~subst context t
+ | C.Match (_,_,he,_) ->
+ let he = NCicReduction.whd status ~subst context he in
+ could_reduce status ~subst context he
+ | C.Appl (he::_) -> could_reduce status ~subst context he
| C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
| C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
;;
in
metasenv,subst,t
+let indfy status exc metasenv subst context t =
+ let t = NCicReduction.whd status ~subst context t in
+ let metasenv,subst =
+ match t with
+ | NCic.Const (Ref.Ref (_, Ref.Ind _))
+ | NCic.Appl (NCic.Const (Ref.Ref (_, Ref.Ind _))::_) -> metasenv, subst
+(*
+ | NCic.Meta (n,_) ->
+ let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
+ let kind = NCicUntrusted.kind_of_meta attrs in
+ if kind = `IsSort then
+ metasenv,subst
+ else
+ (match ty with
+ | NCic.Implicit (`Typeof _) ->
+ metasenv_to_subst n (`IsSort,[],ty) metasenv subst
+ | ty ->
+ let metasenv,subst,ty = sortfy status exc metasenv subst context ty in
+ metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
+*)
+ | NCic.Implicit _ -> assert false
+ | _ -> raise exc
+ in
+ metasenv,subst,t
+
let tipify status exc metasenv subst context t ty =
let is_type attrs =
match NCicUntrusted.kind_of_meta attrs with
try Some
(fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst
context (false,t1) (false,t2))
+ (*(unify status true(*test_eq_only*) metasenv subst
+ context t1 t2 false)*)
with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None
in
indent := ind; res
with Invalid_argument _ -> assert false)
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| _ when norm1 && norm2 ->
- if (could_reduce t1 || could_reduce t2) then
+ if (could_reduce status ~subst context t1 || could_reduce status ~subst context t2) then
raise (Uncertain (mk_msg status metasenv subst context t1 t2))
else
raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
| UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
-> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
| UnificationFailure msg
- when could_reduce (NCicReduction.unwind status (fst m1))
- || could_reduce (NCicReduction.unwind status (fst m2))
+ when could_reduce status ~subst context (NCicReduction.unwind status (fst m1))
+ || could_reduce status ~subst context (NCicReduction.unwind status (fst m2))
-> raise (Uncertain msg)
(*D*) in outside None; rc with exn -> outside (Some exn); raise exn
in