From 4767d724d489a7ad67f696e9401e70b9f9ae2143 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 15 Oct 2007 19:55:12 +0000 Subject: Imported Upstream version 8.1.pl2+dfsg --- pretyping/cases.ml | 14 +++++++------- pretyping/detyping.ml | 6 ++++-- pretyping/tacred.ml | 39 +++++++++++++++++++++++---------------- 3 files changed, 34 insertions(+), 25 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 58dda021..1f7bdad3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 9215 2006-10-05 15:40:31Z herbelin $ *) +(* $Id: cases.ml 10071 2007-08-10 15:34:41Z herbelin $ *) open Util open Names @@ -1021,18 +1021,18 @@ let abstract_predicate env sigma indf cur tms = function (* Depending on whether the predicate is dependent or not, and has real args or not, we lift it to make room for [sign] *) (* Even if not intrinsically dep, we move the predicate into a dep one *) - let sign,k = + let sign,q = if names = [] & n <> 1 then (* Real args were not considered *) (if dep<>Anonymous then - ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1) + (let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign) else - (sign,n)) + sign),n else (* Real args are OK *) - (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign, - if dep<>Anonymous then 0 else 1) in - let pred = lift_predicate k pred in + (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,1) in + let q,k = if dep <> Anonymous then (q-1,2) else (q,1) in + let pred = liftn_predicate q k pred in let pred = extract_predicate [] (pred,tms) in (true, it_mkLambda_or_LetIn_name env pred sign) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 4a2e5ee3..29ec7904 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: detyping.ml 10135 2007-09-21 14:28:12Z herbelin $ *) open Pp open Util @@ -241,7 +241,9 @@ and align_tree nal isgoal (e,c as rhs) = match nal with | [] -> [[],rhs] | na::nal -> match kind_of_term c with - | Case (ci,_,c,cl) when c = mkRel (list_index na (snd e)) -> + | Case (ci,p,c,cl) when c = mkRel (list_index na (snd e)) + & (* don't contract if p dependent *) + computable p (ci.ci_pp_info.ind_nargs) -> let clauses = build_tree na isgoal e ci cl in List.flatten (List.map (fun (pat,rhs) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 92617820..64e9ebec 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 9762 2007-04-13 12:46:50Z herbelin $ *) +(* $Id: tacred.ml 10135 2007-09-21 14:28:12Z herbelin $ *) open Pp open Util @@ -358,12 +358,11 @@ let reduce_fix_use_function f whfun fix stack = Reduced (contract_fix_use_function f fix,stack') | _ -> NotReducible) -let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) = +let contract_cofix_use_function f (bodynum,(_names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = match f j with | None -> mkCoFix(j,typedbodies) | Some c -> c in -(* match List.nth names j with Name id -> f id | _ -> assert false in*) let subbodies = list_tabulate make_Fi nbodies in substl (List.rev subbodies) bodies.(bodynum) @@ -372,19 +371,27 @@ let reduce_mind_case_use_function func env mia = | Construct(ind_sp,i) -> let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1), real_cargs) - | CoFix (_,(names,_,_) as cofix) -> - let build_fix_name i = - match names.(i) with - | Name id -> - if isConst func then - let (mp,dp,_) = repr_con (destConst func) in - let kn = make_con mp dp (label_of_id id) in - (match constant_opt_value env kn with - | None -> None - | Some _ -> Some (mkConst kn)) - else None - | Anonymous -> None in - let cofix_def = contract_cofix_use_function build_fix_name cofix in + | CoFix (bodynum,(names,_,_) as cofix) -> + let build_cofix_name = + if isConst func then + let (mp,dp,_) = repr_con (destConst func) in + fun i -> + if i = bodynum then Some func + else match names.(i) with + | Anonymous -> None + | Name id -> + (* In case of a call to another component of a block of + mutual inductive, try to reuse the global name if + the block was indeed initially built as a global + definition *) + let kn = make_con mp dp (label_of_id id) in + try match constant_opt_value env kn with + | None -> None + | Some _ -> Some (mkConst kn) + with Not_found -> None + else + fun _ -> None in + let cofix_def = contract_cofix_use_function build_cofix_name cofix in mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false -- cgit v1.2.3