From a38d0b898b0d4e4c6535c4f583b4e3a56b3199b3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 28 Mar 2004 14:41:46 +0000 Subject: Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui sont supposes sans dependances en les arguments des constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5589 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrextern.ml | 1 + pretyping/cases.ml | 1 + pretyping/detyping.ml | 46 ++++++++++++++------ pretyping/detyping.mli | 2 +- pretyping/pretyping.ml | 104 +++++++++++++++++++------------------------- theories/Bool/DecBool.v | 2 +- theories/Lists/TheoryList.v | 2 +- 7 files changed, 82 insertions(+), 76 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0c9d9a66c..7657ce445 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1825,6 +1825,7 @@ let rec raw_of_pat tenv env = function let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env) + (fun _ _ -> false (* lazy: don't try to display pattern with "if" *)) tenv avoid ind cs typopt k tm bv | PCase _ -> error "Unsupported case-analysis while printing pattern" | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d80bacbfb..0084fce65 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -142,6 +142,7 @@ type ml_case_error = exception NotInferable of ml_case_error + let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) = let pred = let (ind,params) = dest_ind_family indf in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 67cf0d388..9666008c3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -193,13 +193,23 @@ let lookup_index_as_renamed env t n = | _ -> None in lookup n 1 t -let rec dont_use_args nargs c = - nargs = 0 or - match c with - | RLambda (_,Anonymous,_,c) -> dont_use_args (nargs - 1) c - | _ -> false - -let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl = +let is_nondep_branch c n = + try + let _,ccl = decompose_lam_n_assum n c in + noccur_between 1 n ccl + with _ -> (* Not eta-expanded or not reduced *) + false + +let extract_nondep_branches test c b n = + let rec strip n r = if n=0 then r else + match r with + | RLambda (_,_,_,t) -> strip (n-1) t + | RLetIn (_,_,_,t) -> strip (n-1) t + | _ -> assert false in + if test c n then Some (strip n b) else None + +let detype_case computable detype detype_eqn testdep + tenv avoid indsp st p k c bl = let synth_type = synthetize_type () in let tomatch = detype c in @@ -262,7 +272,7 @@ let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl = if tag = RegularStyle then RCases (dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl) else - let bl = Array.map detype bl in + let bl' = Array.map detype bl in if not !Options.v7 && tag = LetStyle && aliastyp = None then let rec decomp_lam_force n avoid l p = if n = 0 then (List.rev l,p) else @@ -279,12 +289,16 @@ let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl = match p with | RApp (loc,p,l) -> RApp (loc,p,l@[a]) | _ -> (RApp (dummy_loc,p,[a]))) in - let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl.(0) 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 - && array_for_all2 dont_use_args consnargsl bl then - RIf (dummy_loc,tomatch,(alias,newpred),bl.(0),bl.(1)) else + let nondepbrs = + array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in + if not !Options.v7 && tag = IfStyle && aliastyp = None + && array_for_all ((<>) None) nondepbrs then + RIf (dummy_loc,tomatch,(alias,newpred), + out_some nondepbrs.(0),out_some nondepbrs.(1)) + else if !Options.v7 then let rec remove_type avoid args c = match c,args with | RLambda (loc,na,t,c), _::args -> @@ -303,8 +317,11 @@ let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl = let avoid = name_fold (fun x l -> x::l) na avoid in RLetIn (dummy_loc,na,h,remove_type avoid args c) | c, [] -> c in - let bl = array_map2 (remove_type avoid) consnargs bl in - ROrderedCase (dummy_loc,tag,pred,tomatch,bl,ref None) + let bl' = array_map2 (remove_type avoid) consnargs bl' in + ROrderedCase (dummy_loc,tag,pred,tomatch,bl',ref None) + else + RCases(dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl) + let rec detype tenv avoid env t = match kind_of_term (collapse_appl t) with @@ -347,6 +364,7 @@ let rec detype tenv avoid env t = let ind = annot.ci_ind in let st = annot.ci_pp_info.style in detype_case comp (detype tenv avoid env) (detype_eqn tenv avoid env) + is_nondep_branch (snd tenv) avoid ind st (Some p) annot.ci_pp_info.ind_nargs c bl | Fix (nvn,recdef) -> detype_fix tenv avoid env nvn recdef | CoFix (n,recdef) -> detype_cofix tenv avoid env n recdef diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 253e0f51c..7efaf4bbc 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -26,7 +26,7 @@ val detype : bool * env -> identifier list -> names_context -> constr -> val detype_case : bool -> ('a -> rawconstr) -> (constructor -> int -> 'a -> loc * identifier list * cases_pattern list * - rawconstr) -> + rawconstr) -> ('a -> int -> bool) -> env -> identifier list -> inductive -> case_style -> 'a option -> int -> 'a -> 'a array -> rawconstr diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a2ea06e4e..5e8a69e0e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -628,73 +628,44 @@ let rec pretype tycon env isevars lvar = function with Not_found -> let cloc = loc_of_rawconstr c in error_case_not_inductive_loc cloc env (evars_of isevars) cj in + let cstrs = get_constructors env indf in + if Array.length cstrs <> 2 then + user_err_loc (loc,"", + str "If is only for inductive types with two constructors"); + (* 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 + let psign = (na,None,build_dependent_inductive env indf)::arsgn in + let pred,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 env_p = push_rels psign env in + let pj = pretype_type empty_valcon env 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 - let pred = lift (List.length arsgn) pred 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 pred = it_mkLambda_or_LetIn ccl psign in + pred, lift (- nar) (beta_applist (pred,[cj.uj_val])) + | None -> + let p = match tycon with + | Some ty -> ty + | None -> new_isevar isevars env (loc,InternalHole) (new_Type ()) + in + it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in + let bj1 = pretype (Some p) env isevars lvar b1 in + let bj2 = pretype (Some p) env isevars lvar b2 in + let cargs1 = cstrs.(0).cs_args and cargs2 = cstrs.(1).cs_args in + let lb1 = lift (rel_context_length cargs1) bj1.uj_val in + let b1 = it_mkLambda_or_LetIn lb1 cargs1 in + let lb2 = lift (rel_context_length cargs2) bj2.uj_val in + let b2 = it_mkLambda_or_LetIn lb2 cargs2 in + let pred = nf_evar (evars_of isevars) pred in + let p = nf_evar (evars_of isevars) p 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|]) + mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in - { uj_val = v; uj_type = rsty } + { uj_val = v; uj_type = p } | ROrderedCase (loc,st,po,c,lf,x) -> let isrec = (st = MatchStyle) in @@ -821,10 +792,25 @@ let rec pretype tycon env isevars lvar = function let args = List.map (fun _ -> Anonymous) params @ nal in Some (dummy_loc,ind,args) in (Some rtntyopt,(List.hd na,intyp)) in - if st = IfStyle & snd indnalopt = None then + let rawbranches = + array_map3 (fun bj b cstr -> + let rec strip n r = if n=0 then r else + match r with + | RLambda (_,_,_,t) -> strip (n-1) t + | RLetIn (_,_,_,t) -> strip (n-1) t + | _ -> assert false in + let n = rel_context_length cstr.cs_args in + try + let _,ccl = decompose_lam_n_assum n bj.uj_val in + if noccur_between 1 n ccl then Some (strip n b) else None + with _ -> (* Not eta-expanded or not reduced *) None) + lfj lf (get_constructors env indf) in + if st = IfStyle & snd indnalopt = None + & rawbranches.(0) <> None && rawbranches.(1) <> None then (* Translate into a "if ... then ... else" *) (* TODO: translate into a "if" even if po is dependent *) - Some (RIf (loc,c,(fst indnalopt,rtntypopt),lf.(0),lf.(1))) + Some (RIf (loc,c,(fst indnalopt,rtntypopt), + out_some rawbranches.(0),out_some rawbranches.(1))) else let detype_eqn constr construct_nargs branch = let name_cons = function diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 8a15e7624..2a0b2063d 100755 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -11,7 +11,7 @@ Set Implicit Arguments. Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C := - if H then fun _ => x else fun _ => y. + if H then x else y. Theorem ifdec_left : diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index 20f39e0ef..7671b25ff 100755 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -149,7 +149,7 @@ Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}. Fixpoint mem (a:A) (l:list A) {struct l} : bool := match l with | nil => false - | b :: m => if eqA_dec a b then fun H => true else fun H => mem a m + | b :: m => if eqA_dec a b then true else mem a m end. Hint Unfold In. -- cgit v1.2.3