(match outtype with
| C.Meta (n,l) ->
- (let candidate,ugraph5,metasenv =
+ (let candidate,ugraph5,metasenv,subst =
let exp_name_subst, metasenv =
let o,_ =
CicEnvironment.get_obj CicUniv.empty_ugraph uri
function
0 -> []
| n -> (Cic.Rel n)::(mk_right_args (n - 1))
+ in
+ let right_args_no = List.length right_args in
+ let lifted_left_args =
+ List.map (CicSubstitution.lift right_args_no) left_args
in
Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
- (left_args @ mk_right_args (List.length right_args)))
+ (lifted_left_args @ mk_right_args right_args_no))
in
let fresh_name =
FreshNamesGenerator.mk_fresh_name ~subst metasenv
match outtypeinstances with
| [] ->
let extended_context =
- let rec add_right_args b =
+ let rec add_right_args =
function
Cic.Prod (name,ty,t) ->
- Some (name,Cic.Decl ty)::(add_right_args b t)
- | _ -> (Some (fresh_name,Cic.Decl ty))::b
+ Some (name,Cic.Decl ty)::(add_right_args t)
+ | _ -> []
in
- add_right_args context arity_instantiated_with_left_args
+ (Some (fresh_name,Cic.Decl ty))::
+ (List.rev
+ (add_right_args arity_instantiated_with_left_args))@
+ context
in
let metasenv,new_meta =
CicMkImplicit.mk_implicit metasenv subst extended_context
add_lambdas (Cic.Meta (new_meta,irl))
arity_instantiated_with_left_args
in
- (Some candidate),ugraph4,metasenv
+ (Some candidate),ugraph4,metasenv,subst
| (constructor_args_no,_,instance,_)::tl ->
try
- let instance' =
- CicSubstitution.delift constructor_args_no
- (CicMetaSubst.apply_subst subst instance)
+ let instance',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
in
- let candidate,ugraph,metasenv =
+ let candidate,ugraph,metasenv,subst =
List.fold_left (
- fun (candidate_oty,ugraph,metasenv)
+ fun (candidate_oty,ugraph,metasenv,subst)
(constructor_args_no,_,instance,_) ->
match candidate_oty with
- | None -> None,ugraph,metasenv
+ | None -> None,ugraph,metasenv,subst
| Some ty ->
try
- let instance' =
- CicSubstitution.delift
- constructor_args_no
- (CicMetaSubst.apply_subst subst instance)
+ let instance',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
in
- let b,ugraph1 =
- CicReduction.are_convertible context
- instance' ty ugraph
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv
+ instance' ty ugraph
in
- if b then
- candidate_oty,ugraph1,metasenv
- else
- None,ugraph,metasenv
- with Failure s -> None,ugraph,metasenv
- ) (Some instance',ugraph4,metasenv) tl
+ candidate_oty,ugraph,metasenv,subst
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ None,ugraph,metasenv,subst
+ ) (Some instance',ugraph4,metasenv,subst) tl
in
match candidate with
- | None -> None, ugraph,metasenv
+ | None -> None, ugraph,metasenv,subst
| Some t ->
let rec add_lambdas n b =
function
in
Some
(add_lambdas 0 t arity_instantiated_with_left_args),
- ugraph,metasenv
- with Failure s ->
- None,ugraph4,metasenv
+ ugraph,metasenv,subst
+ with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+ None,ugraph4,metasenv,subst
in
match candidate with
| None -> raise (Uncertain "can't solve an higher order unification problem")
| Some candidate ->
- let s,m,u =
+ let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv
candidate outtype ugraph5
in
C.MutCase (uri, i, outtype, term', pl'),
- (Cic.Appl (outtype::right_args@[term'])),s,m,u)
+ (Cic.Appl (outtype::right_args@[term'])),
+ subst,metasenv,ugraph)
| _ -> (* easy case *)
let _,_, subst, metasenv,ugraph5 =
type_of_aux subst metasenv context