From c01357249f005ee5ee531351c848e1410b970b6e Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 13 Dec 2006 09:58:09 +0000 Subject: Dépliage du terme d'induction avant suppression quand celui-ci est un terme arbitraire, possiblement dépendant, qui a été transformé en let-in (cf success/destruct.v) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9447 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tactics.ml | 57 ++++++++++++++++++++++++++++-------------------------- 1 file changed, 30 insertions(+), 27 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index eba3fa4e4..074ccadf9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1172,6 +1172,35 @@ let forward usetac ipat c gl = | Some tac -> tclTHENFIRST (assert_as true ipat c) tac gl +(*****************************) +(* Ad hoc unfold *) +(*****************************) + +(* The two following functions should already exist, but found nowhere *) +(* Unfolds x by its definition everywhere *) +let unfold_body x gl = + let hyps = pf_hyps gl in + let xval = + match Sign.lookup_named x hyps with + (_,Some xval,_) -> xval + | _ -> errorlabstrm "unfold_body" + (pr_id x ++ str" is not a defined hypothesis") in + let aft = afterHyp x gl in + let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in + let xvar = mkVar x in + let rfun _ _ c = replace_term xvar xval c in + tclTHENLIST + [tclMAP (fun h -> reduct_in_hyp rfun h) hl; + reduct_in_concl (rfun,DEFAULTcast)] gl + +(* Unfolds x by its definition everywhere and clear x. This may raise + an error if x is not defined. *) +let unfold_all x gl = + let (_,xval,_) = pf_get_hyp gl x in + (* If x has a body, simply replace x with body and clear x *) + if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl + else tclIDTAC gl + (*****************************) (* High-level induction *) (*****************************) @@ -2040,7 +2069,7 @@ let induction_from_context isrec elim_info hyp0 names gl = (if isrec then tclTHENFIRSTn else tclTHENLASTn) (tclTHENLIST [ induction_tac hyp0 typ0 scheme (*scheme.elimc,scheme.elimt*); - thin [hyp0]; + tclTHEN (tclTRY (unfold_body hyp0)) (thin [hyp0]); tclTRY (thin indhyps) ]) (array_map2 (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names) @@ -2091,32 +2120,6 @@ let new_induct_gen isrec elim names c gl = (letin_tac true (Name id) c allClauses) (induction_with_atomization_of_ind_arg isrec elim names id) gl -(* The two following functions should already exist, but found nowhere *) -(* Unfolds x by its definition everywhere *) -let unfold_body x gl = - let hyps = pf_hyps gl in - let xval = - match Sign.lookup_named x hyps with - (_,Some xval,_) -> xval - | _ -> errorlabstrm "unfold_body" - (pr_id x ++ str" is not a defined hypothesis") in - let aft = afterHyp x gl in - let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in - let xvar = mkVar x in - let rfun _ _ c = replace_term xvar xval c in - tclTHENLIST - [tclMAP (fun h -> reduct_in_hyp rfun h) hl; - reduct_in_concl (rfun,DEFAULTcast)] gl - -(* Unfolds x by its definition everywhere and clear x. This may raise - an error if x is not defined. *) -let unfold_all x gl = - let (_,xval,_) = pf_get_hyp gl x in - (* If x has a body, simply replace x with body and clear x *) - if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl - else tclIDTAC gl - - (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is that all arguments and parameters of the scheme are given -- cgit v1.2.3