let hbr t =
if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t
in
- let refine_appl () =
+ let refine_appl metasenv subst args =
let metasenv, subst, he, ty_he =
typeof_aux metasenv subst context None he in
let metasenv, subst, t, ty =
let metasenv, subst, he, ty_he =
typeof_aux metasenv subst context expty he in
metasenv, subst, hbr he, ty_he
- with Uncertain _ | RefineFailure _ -> refine_appl ()
- else refine_appl ()
+ with Uncertain _ | RefineFailure _ -> refine_appl metasenv subst args
+ else
+ (* CSC: whd can be useful on he too... *)
+ (match he with
+ C.Const (Ref.Ref (uri1,Ref.Con _)) -> (
+ match
+ HExtlib.map_option (NCicReduction.whd ~subst context) expty
+ with
+ Some (C.Appl(C.Const(Ref.Ref (uri2,Ref.Ind _) as ref)::expargs))
+ when NUri.eq uri1 uri2 ->
+ (try
+ let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys ref in
+ let leftexpargs,_ = HExtlib.split_nth leftno expargs in
+ let rec instantiate metasenv subst revargs args =
+ function
+ [] ->
+ (* some checks are re-done here, but it would be complex
+ to avoid them (e.g. we did not check yet that the
+ constructor is a constructor for that inductive type)*)
+ refine_appl metasenv subst ((List.rev revargs)@args)
+ | (exparg::expargs) as allexpargs ->
+ match args with
+ [] -> raise (Failure "Not enough args")
+ | (C.Implicit `Vector::args) as allargs ->
+ (try
+ instantiate metasenv subst revargs args allexpargs
+ with
+ Sys.Break as exn -> raise exn
+ | _ ->
+ instantiate metasenv subst revargs
+ (C.Implicit `Term :: allargs) allexpargs)
+ | arg::args ->
+ let metasenv,subst,arg,_ =
+ typeof_aux metasenv subst context None arg in
+ let metasenv,subst =
+ NCicUnification.unify rdb metasenv subst context
+ arg exparg
+ in
+ instantiate metasenv subst(arg::revargs) args expargs
+ in
+ instantiate metasenv subst [] args leftexpargs
+ with
+ | Sys.Break as exn -> raise exn
+ | _ ->
+ refine_appl metasenv subst args (* to try coercions *))
+ | _ -> refine_appl metasenv subst args)
+ | _ -> refine_appl metasenv subst args)
| C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
| C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
outtype,(term as orig_term),pl) as orig ->
;;
let undebruijnate inductive ref t rev_fl =
+ let len = List.length rev_fl in
NCicSubstitution.psubst (fun x -> x)
- (List.rev (HExtlib.list_mapi
+ (HExtlib.list_mapi
(fun (_,_,rno,_,_,_) i ->
+ let i = len - i - 1 in
NCic.Const
(if inductive then NReference.mk_fix i rno ref
else NReference.mk_cofix i ref))
- rev_fl))
+ rev_fl)
t
;;
metasenv,subst,item1::context
) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
with Invalid_argument "List.fold_left2" -> assert false in
+ let metasenv, subst =
+ let rec aux context (metasenv,subst) = function
+ | NCic.Meta _ -> metasenv, subst
+ | NCic.Implicit _ -> metasenv, subst
+ | NCic.Appl (NCic.Rel i :: args) as t
+ when i > List.length context - len ->
+ let lefts, _ = HExtlib.split_nth leftno args in
+ let ctxlen = List.length context in
+ let (metasenv, subst), _ =
+ List.fold_left
+ (fun ((metasenv, subst),l) arg ->
+ NCicUnification.unify rdb
+ ~test_eq_only:true metasenv subst context arg
+ (NCic.Rel (ctxlen - len - l)), l+1
+ )
+ ((metasenv, subst), 0) lefts
+ in
+ metasenv, subst
+ | t -> NCicUtils.fold (fun e c -> e::c) context aux
+ (metasenv,subst) t
+ in
+ aux context (metasenv,subst) te
+ in
let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
(match
NCicReduction.whd ~subst context con_sort,