diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 155 |
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 |