From 44c3d5dfdf11a3fc948006e7da2ca70e9cd77357 Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 3 Dec 2008 18:13:19 +0000 Subject: improved simpl git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11653 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/tacred.ml | 121 ++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 89 insertions(+), 32 deletions(-) (limited to 'pretyping/tacred.ml') diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index d1afdfc2c..418bb5d2f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -174,15 +174,6 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = in if not (list_distinct (List.map fst li)) then raise Elimconst; - (* Recursive calls must be applied enough to avoid eta-expansion *) -(* let rec no_partial_app k c = - let (h,rcargs) = decompose_app c in - if eq_constr h (mkRel (k+nbfix-i)) then - if List.length rcargs < nargs then raise Elimconst - else List.iter (no_partial_app k) rcargs - else iter_constr_with_binders succ no_partial_app k c in - Array.iter (no_partial_app 0) bds; -*) let k = lv.(i) in if k < nargs then (* Such an optimisation would need eta-expansion @@ -346,31 +337,95 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: do so that the reduction uses this extra information *) -let substl_with_arity subst constr = +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 = - let (h,rcargs) = decompose_app c in - match kind_of_term h with + match kind_of_term c with Rel i when k - let h' = - if i <= k + Array.length v then - match v.(i-k-1) with - (_,Some(min,ref)) when List.length rcargs >= min -> - lift k ref - | (fx,_) -> lift k fx - else mkRel (i - Array.length v) in - applist(h',List.map(subst_total k)rcargs) - | _ -> map_constr_with_binders succ subst_total k c in - subst_total 0 constr - -let contract_fix_use_function f + 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 = (mkFix((recindices,j),typedbodies), f j) in let lbodies = list_tabulate make_Fi nbodies in - substl_with_arity (List.rev lbodies) (nf_beta 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) -> @@ -383,14 +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 = (mkCoFix(j,typedbodies), f j) in let subbodies = list_tabulate make_Fi nbodies in - substl_with_arity (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 @@ -419,7 +475,8 @@ let reduce_mind_case_use_function func env mia = 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 @@ -463,7 +520,7 @@ let rec red_elim_const env sigma ref largs = let d, lrest = whd_betadelta_state env sigma (c,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) @@ -479,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 -- cgit v1.2.3