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
;;
| NCic.Meta _ -> metasenv, subst
| NCic.Implicit _ -> metasenv, subst
| NCic.Appl (NCic.Rel i :: args) as t
- when i >= List.length context - len ->
+ when i > List.length context - len ->
let lefts, _ = HExtlib.split_nth leftno args in
let ctxlen = List.length context in
let (metasenv, subst), _ =