From 47e5f716f7ded0eec43b00d49955d56c370c3596 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 8 Jun 2008 16:13:37 +0000 Subject: - Extension de "generalize" en "generalize c as id at occs". - Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. 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@11072 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/depends.ml | 10 ++++++---- contrib/interface/pbp.ml | 2 +- contrib/interface/showproof.ml | 4 ++-- contrib/interface/xlate.ml | 20 +++++++++++++------- 4 files changed, 22 insertions(+), 14 deletions(-) (limited to 'contrib/interface') diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index be4f9c091..dd40c5cc3 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -295,16 +295,18 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of | TacCut c -> depends_of_'constr c acc | TacAssert (taco, _, c) -> Option.fold_right depends_of_'tac taco (depends_of_'constr c acc) - | TacGeneralize cl -> list_union_map depends_of_'constr cl acc + | TacGeneralize cl -> + list_union_map depends_of_'constr (List.map (fun ((_,c),_) -> c) cl) + acc | TacGeneralizeDep c -> depends_of_'constr c acc - | TacLetTac (_,c,_) -> depends_of_'constr c acc + | TacLetTac (_,c,_,_) -> depends_of_'constr c acc (* Derived basic tactics *) | TacSimpleInduction _ | TacSimpleDestruct _ | TacDoubleInduction _ -> acc - | TacNewInduction (_, cwbial, cwbo, _) - | TacNewDestruct (_, cwbial, cwbo, _) -> + | TacNewInduction (_, cwbial, cwbo, _, _) + | TacNewDestruct (_, cwbial, cwbo, _, _) -> list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings) cwbial (Option.fold_right depends_of_'constr_with_bindings cwbo acc) diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index c16cde7d7..ac152f906 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -166,7 +166,7 @@ let make_pbp_atomic_tactic = function TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x])) | PbpGeneralize (h,args) -> let l = List.map make_pbp_pattern args in - TacAtom (zz, TacGeneralize [make_app (make_var h) l]) + TacAtom (zz, TacGeneralize [([],make_app (make_var h) l),Anonymous]) | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings)) | PbpRight -> TacAtom (zz, TacRight (false,NoBindings)) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 7f2019681..a2a504fb4 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1185,7 +1185,7 @@ let rec natural_ntree ig ntree = | TacFix (_,n) -> natural_fix ig lh g gs n ltree | TacSplit (_,_,NoBindings) -> natural_split ig lh g gs ge [] ltree | TacSplit(_,_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree - | TacGeneralize l -> natural_generalize ig lh g gs ge (List.map snd l) ltree + | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree | TacRight _ -> natural_right ig lh g gs ltree | TacLeft _ -> natural_left ig lh g gs ltree | (* "Simpl" *)TacReduce (r,cl) -> @@ -1652,7 +1652,7 @@ and natural_split ig lh g gs ge la ltree = | _ -> assert false and natural_generalize ig lh g gs ge la ltree = match la with - [arg] -> + [(_,(_,arg)),_] -> let _env= (gLOB ge) in let arg1= (*dbize env*) arg in let _type_arg=type_of (Global.env()) Evd.empty arg in diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index c2569a142..b041272c1 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1151,9 +1151,12 @@ and xlate_tac = | TacSpecialize (nopt, (c,sl)) -> CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl) | TacGeneralize [] -> xlate_error "" - | TacGeneralize (first :: cl) -> + | TacGeneralize ((([],first),Anonymous) :: cl) + when List.for_all (fun ((o,_),na) -> o = [] & na = Anonymous) cl -> CT_generalize - (CT_formula_ne_list (xlate_formula first, List.map xlate_formula cl)) + (CT_formula_ne_list (xlate_formula first, + List.map (fun ((_,c),_) -> xlate_formula c) cl)) + | TacGeneralize _ -> xlate_error "TODO: Generalize at and as" | TacGeneralizeDep c -> CT_generalize_dependent (xlate_formula c) | TacElimType c -> CT_elim_type (xlate_formula c) @@ -1163,7 +1166,7 @@ and xlate_tac = | TacCase (false,(c1,sl)) -> CT_casetac (xlate_formula c1, xlate_bindings sl) | TacElim (true,_,_) | TacCase (true,_) - | TacNewDestruct (true,_,_,_) | TacNewInduction (true,_,_,_) -> + | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) -> xlate_error "TODO: eelim, ecase, edestruct, einduction" | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h) | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h) @@ -1207,24 +1210,27 @@ and xlate_tac = CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b) | TacDAuto (a, b, _) -> xlate_error "TODO: dauto using" - | TacNewDestruct(false,a,b,c) -> + | TacNewDestruct(false,a,b,c,None) -> CT_new_destruct (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) - | TacNewInduction(false,a,b,c) -> + | TacNewInduction(false,a,b,c,None) -> CT_new_induction (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) + | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in" + | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in" (*| TacInstantiate (a, b, cl) -> CT_instantiate(CT_int a, xlate_formula b, assert false) *) - | TacLetTac (na, c, cl) when cl = nowhere -> + | TacLetTac (na, c, cl, true) when cl = nowhere -> CT_pose(xlate_id_opt_aux na, xlate_formula c) - | TacLetTac (na, c, cl) -> + | TacLetTac (na, c, cl, true) -> CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, (* TODO LATER: This should be shared with Unfold, but the structures are different *) xlate_clause cl) + | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember" | TacAssert (None, IntroIdentifier id, c) -> CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c) | TacAssert (None, IntroAnonymous, c) -> -- cgit v1.2.3