diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 70 |
1 files changed, 44 insertions, 26 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fcbe90b6..a5a7ace2 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1077,7 +1077,7 @@ let rec ungeneralize n ng body = let p = prod_applist p [mkRel (n+List.length sign+ng)] in it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in mkCase (ci,p,c,Array.map2 (fun q c -> - let sign,b = decompose_lam_n_assum q c in + let sign,b = decompose_lam_n_decls q c in it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign) ci.ci_cstr_ndecls brs) | App (f,args) -> @@ -1102,7 +1102,8 @@ let rec is_dependent_generalization ng body = | Case (ci,p,c,brs) -> (* We traverse a split *) Array.exists2 (fun q c -> - let _,b = decompose_lam_n_assum q c in is_dependent_generalization ng b) + let _,b = decompose_lam_n_decls q c in + is_dependent_generalization ng b) ci.ci_cstr_ndecls brs | App (g,args) -> (* We traverse an inner generalization *) @@ -1466,6 +1467,14 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = compile pb in let sigma = !(pb.evdref) in + (* If the "match" was orginally over a variable, as in "match x with + O => true | n => n end", we give preference to non-expansion in + the default clause (i.e. "match x with O => true | n => n end" + rather than "match x with O => true | S p => S p end"; + computationally, this avoids reallocating constructors in cbv + evaluation; the drawback is that it might duplicate the instances + of the term to match when the corresponding variable is + substituted by a non-evaluated expression *) if not (Flags.is_program_mode ()) && (isRel orig || isVar orig) then (* Try to compile first using non expanded alias *) try @@ -1473,6 +1482,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = else just_pop () with e when precatchable_exception e -> (* Try then to compile using expanded alias *) + (* Could be needed in case of dependent return clause *) pb.evdref := sigma; f expanded expanded_typ else @@ -1480,6 +1490,8 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = try f expanded expanded_typ with e when precatchable_exception e -> (* Try then to compile using non expanded alias *) + (* Could be needed in case of a recursive call which requires to + be on a variable for size reasons *) pb.evdref := sigma; if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig) else just_pop () @@ -1668,7 +1680,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in - let evd,tt = Typing.e_type_of extenv !evdref t in + let evd,tt = Typing.type_of extenv !evdref t in evdref := evd; (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in @@ -1854,10 +1866,10 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = (* We put the tycon inside the arity signature, possibly discovering dependencies. *) -let prepare_predicate_from_arsign_tycon loc tomatchs arsign c = +let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in let subst, len = - List.fold_left2 (fun (subst, len) (tm, tmtype) sign -> + List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in match kind_of_term tm with | Rel n when dependent tm c @@ -1868,19 +1880,21 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c = (match tmtype with NotInd _ -> (subst, len - signlen) | IsInd (_, IndType(indf,realargs),_) -> - let subst = - if dependent tm c && List.for_all isRel realargs - then (n, 1) :: subst else subst - in + let subst, len = List.fold_left (fun (subst, len) arg -> match kind_of_term arg with | Rel n when dependent arg c -> ((n, len) :: subst, pred len) | _ -> (subst, pred len)) - (subst, len) realargs) + (subst, len) realargs + in + let subst = + if dependent tm c && List.for_all isRel realargs + then (n, len) :: subst else subst + in (subst, pred len)) | _ -> (subst, len - signlen)) - ([], nar) tomatchs arsign + (List.rev tomatchs) arsign ([], nar) in let rec predicate lift c = match kind_of_term c with @@ -1894,8 +1908,13 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c = mkRel (n + nar)) | _ -> map_constr_with_binders succ predicate lift c - in predicate 0 c - + in + assert (len == 0); + let p = predicate 0 c in + let env' = List.fold_right push_rel_context arsign env in + try let sigma' = fst (Typing.type_of env' sigma p) in + Some (sigma', p) + with e when precatchable_exception e -> None (* Builds the predicate. If the predicate is dependent, its context is * made of 1+nrealargs assumptions for each matched term in an inductive @@ -1916,11 +1935,13 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = (* If the tycon is not closed w.r.t real variables, we try *) (* two different strategies *) (* First strategy: we abstract the tycon wrt to the dependencies *) - let pred1 = - prepare_predicate_from_arsign_tycon loc tomatchs arsign t in + let p1 = + prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in (* Second strategy: we build an "inversion" predicate *) let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in - [sigma, pred1; sigma2, pred2] + (match p1 with + | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2] + | None -> [sigma2, pred2]) | None, _ -> (* No dependent type constraint, or no constraints at all: *) (* we use two strategies *) @@ -2014,7 +2035,7 @@ let constr_of_pat env evdref arsign pat avoid = let IndType (indf, _) = try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env - {uj_val = ty; uj_type = Typing.type_of env !evdref ty} + {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty} in let (ind,u), params = dest_ind_family indf in if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind; @@ -2214,7 +2235,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in - let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in + let _btype = evd_comb1 (Typing.type_of env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = @@ -2392,14 +2413,11 @@ let compile_program_cases loc style (typing_function, evdref) tycon env | None -> let ev = mkExistential env evdref in ev, ev | Some t -> let pred = - try - let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in - (* The tycon may be ill-typed after abstraction. *) - let env' = push_rel_context (context_of_arsign sign) env in - ignore(Typing.sort_of env' evdref pred); pred - with e when Errors.noncritical e -> - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in - lift nar t + match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with + | Some (evd, pred) -> evdref := evd; pred + | None -> + let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in + lift nar t in Option.get tycon, pred in let neqs, arity = |