summaryrefslogtreecommitdiff
path: root/pretyping/tacred.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r--pretyping/tacred.ml155
1 files changed, 119 insertions, 36 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 57fdbb09..88a6f499 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacred.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: tacred.ml 11654 2008-12-03 18:39:40Z barras $ *)
open Pp
open Util
@@ -99,10 +99,11 @@ let reference_value sigma env c =
(* One reuses the name of the function after reduction of the fixpoint *)
type constant_evaluation =
- | EliminationFix of int * (int * (int * constr) list * int)
+ | EliminationFix of int * int * (int * (int * constr) list * int)
| EliminationMutualFix of
int * evaluable_reference *
- (evaluable_reference option array * (int * (int * constr) list * int))
+ ((int*evaluable_reference) option array *
+ (int * (int * constr) list * int))
| EliminationCases of int
| NotAnElimination
@@ -171,24 +172,24 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
| _ ->
raise Elimconst) args
in
- if list_distinct (List.map fst li) then
- let k = lv.(i) in
- if k < nargs then
+ if not (list_distinct (List.map fst li)) then
+ raise Elimconst;
+ let k = lv.(i) in
+ if k < nargs then
(* Such an optimisation would need eta-expansion
let p = destRel (List.nth args k) in
EliminationFix (n-p+1,(nbfix,li,n))
*)
- EliminationFix (n,(nbfix,li,n))
- else
- EliminationFix (n-nargs+lv.(i)+1,(nbfix,li,n))
- else
- raise Elimconst
+ EliminationFix (n,nargs,(nbfix,li,n))
+ else
+ EliminationFix (n-nargs+k+1,nargs,(nbfix,li,n))
(* Heuristic to look if global names are associated to other
components of a mutual fixpoint *)
let invert_name labs l na0 env sigma ref = function
| Name id ->
+ let minfxargs = List.length l in
if na0 <> Name id then
let refi = match ref with
| EvalRel _ | EvalEvar _ -> None
@@ -205,9 +206,10 @@ let invert_name labs l na0 env sigma ref = function
let labs',ccl = decompose_lam c in
let _, l' = whd_betalet_stack ccl in
let labs' = List.map snd labs' in
- if labs' = labs & l = l' then Some ref else None
+ if labs' = labs & l = l' then Some (minfxargs,ref)
+ else None
with Not_found (* Undefined ref *) -> None
- else Some ref
+ else Some (minfxargs,ref)
| Anonymous -> None (* Actually, should not occur *)
(* [compute_consteval_direct] expand all constant in a whole, but
@@ -242,7 +244,7 @@ let compute_consteval_mutual_fix sigma env ref =
(match compute_consteval_direct sigma env ref with
| NotAnElimination -> (*Above const was eliminable but this not!*)
NotAnElimination
- | EliminationFix (minarg',infos) ->
+ | EliminationFix (minarg',minfxargs,infos) ->
let refs =
Array.map
(invert_name labs l names.(i) env sigma ref) names in
@@ -263,7 +265,7 @@ let compute_consteval_mutual_fix sigma env ref =
let compute_consteval sigma env ref =
match compute_consteval_direct sigma env ref with
- | EliminationFix (_,(nbfix,_,_)) when nbfix <> 1 ->
+ | EliminationFix (_,_,(nbfix,_,_)) when nbfix <> 1 ->
compute_consteval_mutual_fix sigma env ref
| elim -> elim
@@ -323,28 +325,107 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
fun i ->
match names.(i) with
| None -> None
- | Some ref ->
+ | Some (minargs,ref) ->
let body = applistc (mkEvalRef ref) la in
let g =
list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) ->
let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in
let tij' = substl (List.rev subst) tij in
mkLambda (x,tij',c)) 1 body (List.rev lv)
- in Some g
+ in Some (minargs,g)
(* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]:
do so that the reduction uses this extra information *)
-let contract_fix_use_function f
+let dummy = mkProp
+let vfx = id_of_string"_expanded_fix_"
+let vfun = id_of_string"_elimminator_function_"
+
+(* Mark every occurrence of substituted vars (associated to a function)
+ as a problem variable: an evar that can be instantiated either by
+ vfx (expanded fixpoint) or vfun (named function). *)
+let substl_with_function subst constr =
+ let cnt = ref 0 in
+ let evd = ref Evd.empty in
+ let minargs = ref Intmap.empty in
+ let v = Array.of_list subst in
+ let rec subst_total k c =
+ match kind_of_term c with
+ Rel i when k<i ->
+ if i <= k + Array.length v then
+ match v.(i-k-1) with
+ | (fx,Some(min,ref)) ->
+ decr cnt;
+ evd := Evd.add !evd !cnt
+ (Evd.make_evar
+ (val_of_named_context
+ [(vfx,None,dummy);(vfun,None,dummy)])
+ dummy);
+ minargs := Intmap.add !cnt min !minargs;
+ lift k (mkEvar(!cnt,[|fx;ref|]))
+ | (fx,None) -> lift k fx
+ else mkRel (i - Array.length v)
+ | _ ->
+ map_constr_with_binders succ subst_total k c in
+ let c = subst_total 0 constr in
+ (c,!evd,!minargs)
+
+exception Partial
+
+(* each problem variable that cannot be made totally applied even by
+ reduction is solved by the expanded fix term. *)
+let solve_arity_problem env sigma fxminargs c =
+ let evm = ref sigma in
+ let set_fix i = evm := Evd.define !evm i (mkVar vfx) in
+ let rec check strict c =
+ let c' = whd_betaiotazeta c in
+ let (h,rcargs) = decompose_app c' in
+ match kind_of_term h with
+ Evar(i,_) when Intmap.mem i fxminargs && not (Evd.is_defined !evm i) ->
+ let minargs = Intmap.find i fxminargs in
+ if List.length rcargs < minargs then
+ if strict then set_fix i
+ else raise Partial;
+ List.iter (check strict) rcargs
+ | (Var _|Const _) when isEvalRef env h ->
+ (match reference_opt_value sigma env (destEvalRef h) with
+ Some h' ->
+ let bak = !evm in
+ (try List.iter (check false) rcargs
+ with Partial ->
+ evm := bak;
+ check strict (applist(h',rcargs)))
+ | None -> List.iter (check strict) rcargs)
+ | _ -> iter_constr (check strict) c' in
+ check true c;
+ !evm
+
+let substl_checking_arity env subst c =
+ (* we initialize the problem: *)
+ let body,sigma,minargs = substl_with_function subst c in
+ (* we collect arity constraints *)
+ let sigma' = solve_arity_problem env sigma minargs body in
+ (* we propagate the constraints: solved problems are substituted;
+ the other ones are replaced by the function symbol *)
+ let rec nf_fix c =
+ match kind_of_term c with
+ Evar(i,[|fx;f|] as ev) when Intmap.mem i minargs ->
+ (match Evd.existential_opt_value sigma' ev with
+ Some c' -> c'
+ | None -> f)
+ | _ -> map_constr nf_fix c in
+ nf_fix body
+
+
+
+let contract_fix_use_function env f
((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
let nbodies = Array.length recindices in
- let make_Fi j = match f j with
- | None -> mkFix((recindices,j),typedbodies)
- | Some c -> c in
+ let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
let lbodies = list_tabulate make_Fi nbodies in
- substl (List.rev lbodies) bodies.(bodynum)
+ substl_checking_arity env (List.rev lbodies) (nf_beta bodies.(bodynum))
-let reduce_fix_use_function f whfun fix stack =
+let reduce_fix_use_function env f whfun fix stack =
match fix_recarg fix stack with
| None -> NotReducible
| Some (recargnum,recarg) ->
@@ -357,16 +438,15 @@ let reduce_fix_use_function f whfun fix stack =
let stack' = stack_assign stack recargnum (app_stack recarg') in
(match kind_of_term recarg'hd with
| Construct _ ->
- Reduced (contract_fix_use_function f fix,stack')
+ Reduced (contract_fix_use_function env f fix,stack')
| _ -> NotReducible)
-let contract_cofix_use_function f (bodynum,(_names,_,bodies as typedbodies)) =
+let contract_cofix_use_function env 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
+ let make_Fi j = (mkCoFix(j,typedbodies), f j) in
let subbodies = list_tabulate make_Fi nbodies in
- substl (List.rev subbodies) bodies.(bodynum)
+ substl_checking_arity env (List.rev subbodies) (nf_beta bodies.(bodynum))
let reduce_mind_case_use_function func env mia =
match kind_of_term mia.mconstr with
@@ -377,8 +457,9 @@ let reduce_mind_case_use_function func env mia =
let build_cofix_name =
if isConst func then
let (mp,dp,_) = repr_con (destConst func) in
+ let minargs = List.length mia.mcargs in
fun i ->
- if i = bodynum then Some func
+ if i = bodynum then Some (minargs,func)
else match names.(i) with
| Anonymous -> None
| Name id ->
@@ -389,11 +470,13 @@ let reduce_mind_case_use_function func env mia =
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)
+ (* TODO: check kn is correct *)
+ | Some _ -> Some (minargs,mkConst kn)
with Not_found -> None
else
fun _ -> None in
- let cofix_def = contract_cofix_use_function build_cofix_name cofix in
+ let cofix_def =
+ contract_cofix_use_function env build_cofix_name cofix in
mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
| _ -> assert false
@@ -432,12 +515,12 @@ let rec red_elim_const env sigma ref largs =
let c', lrest = whd_betadelta_state env sigma (c,largs) in
let whfun = whd_simpl_state env sigma in
(special_red_case sigma env whfun (destCase c'), lrest)
- | EliminationFix (min,infos) when stack_args_size largs >=min ->
+ | EliminationFix (min,minfxargs,infos) when stack_args_size largs >=min ->
let c = reference_value sigma env ref in
let d, lrest = whd_betadelta_state env sigma (c,largs) in
- let f = make_elim_fun ([|Some ref|],infos) largs in
+ let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
let whfun = whd_construct_state env sigma in
- (match reduce_fix_use_function f whfun (destFix d) lrest with
+ (match reduce_fix_use_function env f whfun (destFix d) lrest with
| NotReducible -> raise Redelimination
| Reduced (c,rest) -> (nf_beta c, rest))
| EliminationMutualFix (min,refgoal,refinfos)
@@ -453,7 +536,7 @@ let rec red_elim_const env sigma ref largs =
let d, lrest = whd_betadelta_state env sigma s in
let f = make_elim_fun refinfos midargs in
let whfun = whd_construct_state env sigma in
- (match reduce_fix_use_function f whfun (destFix d) lrest with
+ (match reduce_fix_use_function env f whfun (destFix d) lrest with
| NotReducible -> raise Redelimination
| Reduced (c,rest) -> (nf_beta c, rest))
| _ -> raise Redelimination