diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 53 | ||||
| -rw-r--r-- | pretyping/cases.mli | 5 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
4 files changed, 55 insertions, 9 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1063493c0..3b27a32b3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -17,6 +17,47 @@ open Retyping open Evarutil open Pretype_errors +(*********************************************************************) +(* This was previously in Indrec but creates existential holes *) + +let mkExistential isevars env = + let (c,_) = new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI in c + +let norec_branch_scheme env isevars typc = + let rec crec typc = match whd_betadeltaiota env !isevars typc with + | DOP2(Prod,c,DLAM(name,t)) -> DOP2(Prod,c,DLAM(name,crec t)) + | _ -> mkExistential isevars env + in + crec typc + +let rec_branch_scheme env isevars ((sp,j),_) typc recargs = + let rec crec (typc,recargs) = + match whd_betadeltaiota env !isevars typc, recargs with + | (DOP2(Prod,c,DLAM(name,t)),(ra::reca)) -> + DOP2(Prod,c, + match ra with + | Mrec k -> + if k=j then + DLAM(name,mkArrow (mkExistential isevars env) + (crec (lift 1 t,reca))) + else + DLAM(name,crec (t,reca)) + | _ -> DLAM(name,crec (t,reca))) + | (_,_) -> mkExistential isevars env + in + crec (typc,recargs) + +let branch_scheme env isevars isrec i (mind,args as appmind) = + let typc = type_inst_construct env !isevars i appmind in + if isrec then + let mispec = lookup_mind_specif mind env in + let recarg = (mis_recarg mispec).(i-1) in + rec_branch_scheme env isevars mind typc recarg + else + norec_branch_scheme env isevars typc + +(************************************************************************) + exception CasesError of env * type_error (* == General purpose functions == *) @@ -1018,21 +1059,21 @@ let apply_to_dep env sigma pred = function (* == Special functions to deal with mlcase on objects of dependent types == *) (* analogue strategy as Christine's MLCASE *) -let find_implicit_pred sigma ith_branch_builder env (current,ind_data,_) = +let find_implicit_pred isevars ith_branch_builder env (current,ind_data,_) = let {nconstr=nconstr;mind=mind;params=params;realargs=realargs} = ind_data in let isrec = false in let rec findtype i = if i > nconstr then raise (CasesError (env, CantFindCaseType current)) else try - (let expti = Indrec.branch_scheme env sigma isrec i (mind,params) in + (let expti = branch_scheme env isevars isrec i (mind,params) in let _,bri= ith_branch_builder i in let fi = bri.uj_type in - let efit = nf_ise1 sigma fi in + let efit = nf_ise1 !isevars fi in let pred = - Indrec.pred_case_ml_onebranch env sigma isrec + Indrec.pred_case_ml_onebranch env !isevars isrec (current,(mind,params,realargs)) (i,bri.uj_val,efit) in - if has_ise sigma pred then error"isevar" else pred) + if has_ise !isevars pred then error"isevar" else pred) with UserError _ -> findtype (i+1) in findtype 1 @@ -1454,7 +1495,7 @@ and match_current trad env (current,ind_data,info as cji) gd = mat = gd.mat} in try (* we try to find out the predicate and recall match_current *) - (let ipred = find_implicit_pred !(trad.isevars) + (let ipred = find_implicit_pred trad.isevars (build_ith_branch next_gd) env cji in (* we abstract with the rest of tomatch *) diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 011c7fcbe..9f121b122 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -10,6 +10,11 @@ open Rawterm open Evarutil (*i*) +(* Used for old cases in pretyping *) + +val branch_scheme : + env -> 'a evar_defs -> bool -> int -> inductive * constr list -> constr + (* Compilation of pattern-matching. *) val compile_multcase : diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index af42d3cd4..53bcbc8ce 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -167,8 +167,8 @@ let restrict_hyps isevars c = c let has_ise sigma t = - try let _ = whd_ise sigma t in true - with UserError _ -> false + try let _ = whd_ise sigma t in false + with Uninstantiated_evar _ -> true (* We try to instanciate the evar assuming the body won't depend * on arguments that are not Rels or VARs, or appearing several times. diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 59716c5d6..1854e7eeb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -393,7 +393,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) else try let expti = - Indrec.branch_scheme env !isevars isrec i (mind,params) in + Cases.branch_scheme env isevars isrec i (mind,params) in let fj = pretype (mk_tycon expti) env isevars lf.(i-1) in let efjt = nf_ise1 !isevars fj.uj_type in let pred = |