diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 26 |
1 files changed, 21 insertions, 5 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 92135e834..4262fa11c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -968,6 +968,8 @@ let rec extract_predicate ccl = function | [] -> ccl +let build_inversion_problem_forward = ref (fun _ -> failwith "To be set") + let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = let sign = make_arity_signature env true indf in (* n is the number of real args + 1 (+ possible let-ins in sign) *) @@ -989,9 +991,20 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = | Name _ -> ccl in let pred = extract_predicate ccl tms in + (* Insert inversion on the pattern-structure of the realargs *) + let sigma,pred = + if isEvar ccl then + let thisind = IndType (indf,realargs) in + let thistm = (cur,(IsInd (mkAppliedInd thisind,thisind,names))) in + let sign = List.map2 set_name (na::names) sign in + let env = push_rel_context sign env in + let sigma,pred = !build_inversion_problem_forward Loc.ghost env sigma [thistm] pred in + let pred = substl (Context.Rel.to_extended_list 0 sign) pred in + sigma, pred + else + sigma, pred in (* Build the predicate properly speaking *) - let sign = List.map2 set_name (na::names) sign in - it_mkLambda_or_LetIn_name env pred sign + sigma, it_mkLambda_or_LetIn_name env pred sign (* [expand_arg] is used by [specialize_predicate] if Yk denotes [Xk;xk] or [Xk], @@ -1094,7 +1107,8 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl = snd (List.fold_left (expand_arg tms) (1,ccl''') newtomatchs) let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms = - let pred = abstract_predicate env !evdref indf current realargs dep tms p in + let sigma, pred = abstract_predicate env !evdref indf current realargs dep tms p in + evdref := sigma; (pred, whd_betaiota !evdref (applist (pred, realargs@[current]))) @@ -1882,6 +1896,8 @@ let build_inversion_problem loc env sigma tms t = let pred = (compile pb).uj_val in (!evdref,pred) +let _ = build_inversion_problem_forward := build_inversion_problem + (* Here, [pred] is assumed to be in the context built from all *) (* realargs and terms to match *) let build_initial_predicate arsign pred = @@ -2014,7 +2030,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = (* Second strategy: we build an "inversion" predicate *) let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in (match p1 with - | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2] + | Some (sigma1,pred1) -> [sigma1, pred1(*; sigma2, pred2*)] | None -> [sigma2, pred2]) | None, _ -> (* No dependent type constraint, or no constraints at all: *) @@ -2032,7 +2048,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Second strategy: we directly use the evar as a non dependent pred *) let pred2 = lift (List.length (List.flatten arsign)) t in - [sigma1, pred1; sigma, pred2] + [(*sigma1, pred1;*) sigma, pred2] (* Some type annotation *) | Some rtntyp, _ -> (* We extract the signature of the arity *) |