diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-09 15:06:44 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-09 15:06:44 +0000 |
commit | a580a7a07da8651887c6fb386bd9af55bbe673a2 (patch) | |
tree | 4233682720571f3fa09fba77bb31e446dc6203e1 /pretyping | |
parent | 51cd60453da3f1fe136904404046098d9c4f1cc3 (diff) |
Ajout construction If primitive dans constr_expr et rawconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 20 | ||||
-rw-r--r-- | pretyping/detyping.ml | 2 | ||||
-rw-r--r-- | pretyping/indrec.ml | 16 | ||||
-rw-r--r-- | pretyping/indrec.mli | 2 | ||||
-rw-r--r-- | pretyping/pattern.ml | 3 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 169 | ||||
-rw-r--r-- | pretyping/rawterm.ml | 32 | ||||
-rw-r--r-- | pretyping/rawterm.mli | 3 |
8 files changed, 136 insertions, 111 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e2aa74cba..a79c2a523 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -130,10 +130,11 @@ let count_rec_arg j = * [a_bar:A'_bar](lift k pred) * where A'_bar = A_bar[p_bar <- globargs] *) -let build_notdep_pred env sigma indf pred = +let build_dep_pred env sigma indf pred = let arsign,_ = get_arity env indf in - let nar = List.length arsign in - it_mkLambda_or_LetIn_name env (lift nar pred) arsign + let psign = (Anonymous,None,build_dependent_inductive env indf)::arsign in + let nar = List.length psign in + it_mkLambda_or_LetIn_name env (lift nar pred) psign type ml_case_error = | MlCaseAbsurd @@ -157,10 +158,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) = else raise (NotInferable MlCaseDependent) in - if realargs = [] then - pred - else (* we try with [_:T1]..[_:Tn](lift n pred) *) - build_notdep_pred env sigma indf pred + build_dep_pred env sigma indf pred (************************************************************************) (* Pattern-matching compilation (Cases) *) @@ -597,9 +595,11 @@ let occur_rawconstr id = or (List.exists occur_pattern pl) | ROrderedCase (loc,b,tyopt,tm,bv,_) -> (occur_option tyopt) or (occur tm) or (array_exists occur bv) - | RLetTuple (loc,nal,(na,tyopt),b,c) -> - (na <> Name id & occur_option tyopt) + | RLetTuple (loc,nal,rtntyp,b,c) -> + occur_return_type rtntyp id or (occur b) or (not (List.mem (Name id) nal) & (occur c)) + | RIf (loc,c,rtntyp,b1,b2) -> + occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2) | RRec (loc,fk,idl,tyl,bv) -> (array_exists occur tyl) or (not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv) @@ -610,6 +610,8 @@ let occur_rawconstr id = and occur_option = function None -> false | Some p -> occur p + and occur_return_type (na,tyopt) id = na <> Name id & occur_option tyopt + in occur let occur_in_rhs na rhs = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 49034b1b1..00895a1f6 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -276,6 +276,8 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl = | _ -> (RApp (dummy_loc,p,[a]))) in let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl.(0) in RLetTuple (dummy_loc,nal,(alias,newpred),tomatch,d) + else if not !Options.v7 && tag = IfStyle && aliastyp = None then + RIf (dummy_loc,tomatch,(alias,newpred),bl.(0),bl.(1)) else let rec remove_type avoid args c = match c,args with diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 78c23ae61..bf7e13158 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -464,29 +464,25 @@ let build_indrec env sigma ind = (**********************************************************************) (* To handle old Case/Match syntax in Pretyping *) -(***********************************) +(*****************************************) (* To interpret Case and Match operators *) +(* Expects a dependent predicate *) -let type_rec_branches recursive env sigma indt pj c = +let type_rec_branches recursive env sigma indt p c = let IndType (indf,realargs) = indt in - let p = pj.uj_val in let (ind,params) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let recargs = mip.mind_recargs in let tyi = snd ind in - let is_rec = recursive && mis_is_recursive_subset [tyi] recargs in - let dep = is_dependent_elimination env pj.uj_type indf in - let init_depPvec i = if i = tyi then Some(dep,p) else None in + let init_depPvec i = if i = tyi then Some(true,p) else None in let depPvec = Array.init mib.mind_ntypes init_depPvec in let vargs = Array.of_list params in let constructors = get_constructors env indf in let lft = array_map2 - (type_rec_branch recursive dep env sigma (params,depPvec,0) tyi) + (type_rec_branch recursive true env sigma (params,depPvec,0) tyi) constructors (dest_subterms recargs) in - (lft, - if dep then Reduction.beta_appvect p (Array.of_list (realargs@[c])) - else Reduction.beta_appvect p (Array.of_list realargs)) + (lft,Reduction.beta_appvect p (Array.of_list (realargs@[c]))) (* Non recursive case. Pb: does not deal with unification let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in (p,ra) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 65fefb83f..38d07d1d9 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -42,7 +42,7 @@ val build_mutual_indrec : (* These are for old Case/Match typing *) val type_rec_branches : bool -> env -> evar_map -> inductive_type - -> unsafe_judgment -> constr -> constr array * constr + -> constr -> constr -> constr array * constr val make_rec_branch_arg : env -> evar_map -> int * ('b * constr) option array * int -> diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index d3479a846..f453e911e 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -241,6 +241,9 @@ let rec pat_of_raw metas vars = function PCase ((None,st),option_app (pat_of_raw metas vars) po, pat_of_raw metas vars c, Array.map (pat_of_raw metas vars) br) + | RIf (_,c,(_,None),b1,b2) -> + PCase ((None,IfStyle),None, pat_of_raw metas vars c, + [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|]) | RCases (loc,(po,_),[c,_],brs) -> let sp = match brs with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ffbca83ea..0dbcaef44 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -349,7 +349,9 @@ let rec pretype tycon env isevars lvar = function let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) (List.rev nal) cs.cs_args in let env_f = push_rels fsign env in + (* Make dependencies from arity signature impossible *) let arsgn,_ = get_arity env indf in + let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in let psign = (na,None,build_dependent_inductive env indf)::arsgn in let nar = List.length arsgn in (match po with @@ -410,7 +412,7 @@ let rec pretype tycon env isevars lvar = function let pj = if dep then pj else make_dep_of_undep env indt pj in let (bty,rsty) = Indrec.type_rec_branches - false env (evars_of isevars) indt pj cj.uj_val + false env (evars_of isevars) indt pj.uj_val cj.uj_val in if Array.length bty <> 1 then error_number_branches_loc @@ -443,6 +445,10 @@ let rec pretype tycon env isevars lvar = function (* may be Type while Prop or Set would be expected *) match tycon with | Some pred -> + let arsgn = make_arity_signature env true indf in + let pred = + it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred) + arsgn in false, Retyping.get_judgment_of env (evars_of isevars) pred | None -> @@ -461,19 +467,21 @@ let rec pretype tycon env isevars lvar = function let pty = Retyping.get_type_of env (evars_of isevars) pred in let pj = { uj_val = pred; uj_type = pty } in +(* let _ = option_app (the_conv_x_leq env isevars pred) tycon in +*) true, pj with Cases.NotInferable _ -> use_constraint () in let pj = j_nf_evar (evars_of isevars) pj in - let pj = make_dep_of_undep env indt pj in let (bty,rsty) = Indrec.type_rec_branches - false env (evars_of isevars) indt pj cj.uj_val + false env (evars_of isevars) indt pj.uj_val cj.uj_val in + let _ = option_app (the_conv_x_leq env isevars rsty) tycon in let fj = if ok then fj else pretype (mk_tycon bty.(0)) env isevars lvar f @@ -588,6 +596,80 @@ let rec pretype tycon env isevars lvar = function (* End building the v8 syntax *) j + | RIf (loc,c,(na,po),b1,b2) -> + let cj = pretype empty_tycon env isevars lvar c in + let (IndType (indf,realargs) as indt) = + try find_rectype env (evars_of isevars) cj.uj_type + with Not_found -> + let cloc = loc_of_rawconstr c in + error_case_not_inductive_loc cloc env (evars_of isevars) cj in + (* Make dependencies from arity signature impossible *) + let arsgn,_ = get_arity env indf in + let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in + let psign = (na,None,build_dependent_inductive env indf)::arsgn in + let nar = List.length arsgn in + let p = + match po with + | Some p -> + let env_p = push_rels psign env in + let pj = pretype_type empty_valcon env_p isevars lvar p in + let ccl = nf_evar (evars_of isevars) pj.utj_val in + it_mkLambda_or_LetIn ccl psign + | None -> + (* get type information from type of branches *) + let expbr = Cases.branch_scheme env isevars false indf in + try + let fj = pretype (mk_tycon expbr.(0)) env isevars lvar b1 in + let pred = + Cases.pred_case_ml + env (evars_of isevars) false indt (0,fj.uj_type) in + if has_undefined_isevars isevars pred then + raise Not_found + else +(* + let _ = option_app (the_conv_x_leq env isevars pred) tycon in +*) + pred + with Cases.NotInferable _ | Not_found -> + try + let fj = pretype (mk_tycon expbr.(1)) env isevars lvar b2 in + let pred = + Cases.pred_case_ml + env (evars_of isevars) false indt (1,fj.uj_type) in + if has_undefined_isevars isevars pred then + raise Not_found + else +(* + let _ = option_app (the_conv_x_leq env isevars pred) tycon in +*) + pred + with Cases.NotInferable _ | Not_found -> + (* get type information from constraint *) + (* warning: if the constraint comes from an evar type, it *) + (* may be Type while Prop or Set would be expected *) + match tycon with + | Some pred -> + let arsgn = make_arity_signature env true indf in + it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred) arsgn + | None -> + let sigma = evars_of isevars in + error_cant_find_case_type_loc loc env sigma cj.uj_val in + let (bty,rsty) = + Indrec.type_rec_branches false + env (evars_of isevars) indt p cj.uj_val in + let _ = option_app (the_conv_x_leq env isevars rsty) tycon in + if Array.length bty <> 2 then + user_err_loc (loc,"", + str "If is only for inductive types with two constructors"); + let bj1 = pretype (mk_tycon bty.(0)) env isevars lvar b1 in + let bj2 = pretype (mk_tycon bty.(1)) env isevars lvar b2 in + let v = + let mis,_ = dest_ind_family indf in + let ci = make_default_case_info env IfStyle mis in + mkCase (ci, p, cj.uj_val, [|bj1.uj_val;bj2.uj_val|]) + in + { uj_val = v; uj_type = rsty } + | ROrderedCase (loc,st,po,c,lf,x) -> let isrec = (st = MatchStyle) in let cj = pretype empty_tycon env isevars lvar c in @@ -615,7 +697,11 @@ let rec pretype tycon env isevars lvar = function (* may be Type while Prop or Set would be expected *) match tycon with | Some pred -> - (false, + let arsgn = make_arity_signature env true indf in + let pred = + it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred) + arsgn in + (true, Retyping.get_judgment_of env (evars_of isevars) pred) | None -> let sigma = evars_of isevars in @@ -626,15 +712,18 @@ let rec pretype tycon env isevars lvar = function let fj = pretype (mk_tycon expti) env isevars lvar lf.(i) in let pred = - Cases.pred_case_ml + Cases.pred_case_ml (* eta-expanse *) env (evars_of isevars) isrec indt (i,fj.uj_type) in if has_undefined_isevars isevars pred then findtype (i+1) else let pty = Retyping.get_type_of env (evars_of isevars) pred in let pj = { uj_val = pred; uj_type = pty } in +(* let _ = option_app (the_conv_x_leq env isevars pred) tycon - in (false,pj) + in +*) + (true,pj) with Cases.NotInferable _ -> findtype (i+1) in findtype 0 in @@ -642,7 +731,8 @@ let rec pretype tycon env isevars lvar = function let pj = if dep then pj else make_dep_of_undep env indt pj in let (bty,rsty) = Indrec.type_rec_branches - isrec env (evars_of isevars) indt pj cj.uj_val in + isrec env (evars_of isevars) indt pj.uj_val cj.uj_val in + let _ = option_app (the_conv_x_leq env isevars rsty) tycon in if Array.length bty <> Array.length lf then error_number_branches_loc loc env (evars_of isevars) cj (Array.length bty) @@ -676,67 +766,6 @@ let rec pretype tycon env isevars lvar = function Some (Detyping.detype env (ids_of_context env) (names_of_rel_context env) (nf_evar (evars_of isevars) v)) - (* - let sigma = evars_of isevars in - let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in - let depFvec = Array.init mib.mind_ntypes init_depFvec in - (* build now the fixpoint *) - let lnames,_ = get_arity env indf in - let nar = List.length lnames in - let nparams = mip.mind_nparams in - let constrs = get_constructors env (lift_inductive_family (nar+2) indf) in - let branches = - array_map3 - (fun f t reca -> - whd_beta - (Indrec.make_rec_branch_arg env sigma - (nparams,depFvec,nar+1) - f t reca)) - (Array.map (lift (nar+2)) lfv) constrs (dest_subterms recargs) - in - let ci = make_default_case_info env RegularStyle ind in - let deffix = - it_mkLambda_or_LetIn_name env - (lambda_create env - (applist (mI,List.append (List.map (lift (nar+1)) params) - (extended_rel_list 0 lnames)), - mkCase (ci, lift (nar+2) pj.uj_val, mkRel 1, branches))) - (lift_rel_context 1 lnames) - in - if noccurn 1 deffix then - Some - (Detyping.detype env [] (names_of_rel_context env) - (whd_beta (applist (pop deffix,realargs@[cj.uj_val])))) - else - let ind = applist (mI,(List.append - (List.map (lift nar) params) - (extended_rel_list 0 lnames))) in - let typPfix = - let rec aux = function - | (na,Some b,t)::l -> - | (na,None,t)::l -> RProd (dummy_loc,na, - | [] -> - it_mkProd_or_LetIn_name env - (prod_create env - (ind, - (if dep then - let ext_lnames = (Anonymous,None,ind)::lnames in - let args = extended_rel_list 0 ext_lnames in - whd_beta (applist (lift (nar+1) p, args)) - else - let args = extended_rel_list 1 lnames in - whd_beta (applist (lift (nar+1) p, args))))) - lnames in - let fix = - RRec (dummy_loc,RFix ([|nar|],0), - ([|(id_of_string "F")|],[|typPfix|],[|deffix|])) in - RApp (dummy_loc,fix,realargs@[c]) - (msgerrnl (str "Warning: could't translate Match"); None) -*) - else if st = IfStyle & po = None then - (* Translate into a "if ... then ... else" *) - (* TODO: translate into a "if" even if po is dependent *) - None else (* Translate into a "match ... with" *) let rtntypopt, indnalopt = match po with @@ -762,10 +791,10 @@ let rec pretype tycon env isevars lvar = function else [Anonymous],p,[] in let args = List.map (fun _ -> Anonymous) params @ nal in (Some rtntyopt,(List.hd na,Some (dummy_loc,ind,args))) in - if st = IfStyle & po = None then + if st = IfStyle & snd indnalopt = None then (* Translate into a "if ... then ... else" *) (* TODO: translate into a "if" even if po is dependent *) - None + Some (RIf (loc,c,(fst indnalopt,rtntypopt),lf.(0),lf.(1))) else let detype_eqn constr construct_nargs branch = let name_cons = function diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index bdb6914c2..a1eb589ff 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -75,6 +75,7 @@ type rawconstr = rawconstr array * rawconstr option ref | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr + | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr | RRec of loc * fix_kind * identifier array * rawconstr array * rawconstr array | RSort of loc * rawsort @@ -97,24 +98,6 @@ let cases_predicate_names tml = - boolean in POldCase means it is recursive i*) -let loc = function - | RVar (loc,_) -> loc - | RApp (loc,_,_) -> loc - | RLambda (loc,_,_,_) -> loc - | RProd (loc,_,_,_) -> loc - | RLetIn (loc,_,_,_) -> loc - | RCases (loc,_,_,_) -> loc - | ROrderedCase (loc,_,_,_,_,_) -> loc - | RLetTuple (loc,_,_,_,_) -> loc - | RRec (loc,_,_,_,_) -> loc - | RCast (loc,_,_) -> loc - | RSort (loc,_) -> loc - | RHole (loc,_) -> loc - | RRef (loc,_) -> loc - | REvar (loc,_) -> loc - | RPatVar (loc,_) -> loc - | RDynamic (loc,_) -> loc - let map_rawconstr f = function | RVar (loc,id) -> RVar (loc,id) | RApp (loc,g,args) -> RApp (loc,f g, List.map f args) @@ -129,6 +112,8 @@ let map_rawconstr f = function ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv,ref (option_app f !x)) | RLetTuple (loc,nal,(na,po),b,c) -> RLetTuple (loc,nal,(na,option_app f po),f b,f c) + | RIf (loc,c,(na,po),b1,b2) -> + RIf (loc,f c,(na,option_app f po),f b1,f b2) | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv) | RCast (loc,c,t) -> RCast (loc,f c,f t) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x @@ -248,8 +233,16 @@ let rec subst_raw subst raw = and b' = subst_raw subst b and c' = subst_raw subst c in if po' == po && b' == b && c' == c then raw else - RLetTuple (loc,nal,(na,po),b,c) + RLetTuple (loc,nal,(na,po'),b',c') + | RIf (loc,c,(na,po),b1,b2) -> + let po' = option_smartmap (subst_raw subst) po + and b1' = subst_raw subst b1 + and b2' = subst_raw subst b2 + and c' = subst_raw subst c in + if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else + RIf (loc,c',(na,po'),b1',b2') + | RRec (loc,fix,ida,ra1,ra2) -> let ra1' = array_smartmap (subst_raw subst) ra1 and ra2' = array_smartmap (subst_raw subst) ra2 in @@ -284,6 +277,7 @@ let loc_of_rawconstr = function | RCases (loc,_,_,_) -> loc | ROrderedCase (loc,_,_,_,_,_) -> loc | RLetTuple (loc,_,_,_,_) -> loc + | RIf (loc,_,_,_,_) -> loc | RRec (loc,_,_,_,_) -> loc | RSort (loc,_) -> loc | RHole (loc,_) -> loc diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 27bb76b69..2718cf9bb 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -72,6 +72,7 @@ type rawconstr = rawconstr array * rawconstr option ref | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr + | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr | RRec of loc * fix_kind * identifier array * rawconstr array * rawconstr array | RSort of loc * rawsort @@ -94,8 +95,6 @@ val cases_predicate_names : - option in PHole tell if the "?" was apparent or has been implicitely added i*) -val loc : rawconstr -> loc - val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr (* |