aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_tactic.ml430
-rw-r--r--parsing/g_tacticnew.ml425
-rw-r--r--parsing/pptactic.ml42
3 files changed, 86 insertions, 11 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 6c8ad0c1b..47977b69b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -224,6 +224,10 @@ GEXTEND Gram
[ [ "in"; idl = LIST1 hypident -> idl
| -> [] ] ]
;
+ simple_clause:
+ [ [ "in"; idl = LIST1 id_or_meta -> idl
+ | -> [] ] ]
+ ;
fixdecl:
[ [ id = base_ident; "/"; n = natural; ":"; c = constr -> (id,n,c) ] ]
;
@@ -252,7 +256,7 @@ GEXTEND Gram
TacIntroMove (Some id, Some id2)
| IDENT "Intro"; IDENT "after"; id2 = identref ->
TacIntroMove (None, Some id2)
- | IDENT "Intro"; id = base_ident -> TacIntroMove (Some id, None)
+ | IDENT "Intro"; id = base_ident -> TacIntroMove (Some id,None)
| IDENT "Intro" -> TacIntroMove (None, None)
| IDENT "Assumption" -> TacAssumption
@@ -344,14 +348,32 @@ GEXTEND Gram
TacSymmetry ido
| IDENT "Transitivity"; c = constr -> TacTransitivity c
+ (* Equality and inversion *)
+ | IDENT "Dependent"; k =
+ [ IDENT "Simple"; IDENT "Inversion" -> SimpleInversion
+ | IDENT "Inversion" -> FullInversion
+ | IDENT "Inversion_clear" -> FullInversionClear ];
+ hyp = quantified_hypothesis;
+ ids = with_names; co = OPT ["with"; c = constr -> c] ->
+ TacInversion (DepInversion (k,co,ids),hyp)
+ | IDENT "Simple"; IDENT "Inversion";
+ hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
+ | IDENT "Inversion";
+ hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
+ | IDENT "Inversion_clear";
+ hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
+ | IDENT "Inversion"; hyp = quantified_hypothesis;
+ "using"; c = constr; cl = simple_clause ->
+ TacInversion (InversionUsing (c,cl), hyp)
+
(* Conversion *)
| r = red_tactic; cl = clause -> TacReduce (r, cl)
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
| IDENT "Change"; (oc,c) = conversion; cl = clause -> TacChange (oc,c,cl)
-(* Unused ??
- | IDENT "ML"; s = string -> ExtraTactic<:ast< (MLTACTIC $s) >>
-*)
] ]
;
END;;
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index b17907844..b03aaf868 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -257,6 +257,10 @@ GEXTEND Gram
[ [ "in"; idl = LIST1 hypident -> idl
| -> [] ] ]
;
+ simple_clause:
+ [ [ "in"; idl = LIST1 id_or_meta -> idl
+ | -> [] ] ]
+ ;
fixdecl:
[ [ id = base_ident; bl=LIST0 Constr.binder; ann=fixannot;
":"; ty=lconstr -> (loc,id,bl,ann,ty) ] ]
@@ -381,6 +385,27 @@ GEXTEND Gram
TacSymmetry ido
| IDENT "transitivity"; c = constr -> TacTransitivity c
+ (* Equality and inversion *)
+ | IDENT "dependent"; k =
+ [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
+ | IDENT "inversion" -> FullInversion
+ | IDENT "inversion_clear" -> FullInversionClear ];
+ hyp = quantified_hypothesis;
+ ids = with_names; co = OPT ["with"; c = constr -> c] ->
+ TacInversion (DepInversion (k,co,ids),hyp)
+ | IDENT "simple"; IDENT "inversion";
+ hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
+ | IDENT "inversion";
+ hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
+ | IDENT "inversion_clear";
+ hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
+ | IDENT "inversion"; hyp = quantified_hypothesis;
+ "using"; c = constr; cl = simple_clause ->
+ TacInversion (InversionUsing (c,cl), hyp)
+
(* Conversion *)
| r = red_tactic; cl = clause -> TacReduce (r, cl)
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 166db8675..0d7230453 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -117,19 +117,23 @@ let pr_bindings prc prlc = function
let pr_with_bindings prc prlc (c,bl) =
prc c ++ hv 0 (pr_bindings prc prlc bl)
+let pr_with_constr prc = function
+ | None -> mt ()
+ | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
+
let rec pr_intro_pattern = function
- | IntroOrAndPattern pll ->
- str "[" ++
- hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
- ++ str "]"
+ | IntroOrAndPattern pll -> pr_case_intro_pattern pll
| IntroWildcard -> str "_"
| IntroIdentifier id -> pr_id id
+and pr_case_intro_pattern pll =
+ str "[" ++
+ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+ ++ str "]"
+
let pr_with_names = function
| [] -> mt ()
- | ids -> spc () ++ str "as [" ++
- hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
- (prlist_with_sep spc pr_intro_pattern) ids ++ str "]")
+ | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids)
let pr_hyp_location pr_id = function
| InHyp id -> spc () ++ pr_id id
@@ -139,6 +143,11 @@ let pr_clause pr_id = function
| [] -> mt ()
| l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
+let pr_simple_clause pr_id = function
+ | [] -> mt ()
+ | l -> spc () ++
+ hov 0 (str "in" ++ spc () ++ prlist_with_sep spc pr_id l)
+
let pr_clause_pattern pr_id = function
| (None, []) -> mt ()
| (glopt,l) ->
@@ -156,6 +165,11 @@ let pr_induction_arg prc = function
| ElimOnIdent (_,id) -> pr_id id
| ElimOnAnonHyp n -> int n
+let pr_induction_kind = function
+ | SimpleInversion -> str "Simple Inversion"
+ | FullInversion -> str "Inversion"
+ | FullInversionClear -> str "Inversion_clear"
+
let pr_match_pattern pr_pat = function
| Term a -> pr_pat a
| Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]"
@@ -526,6 +540,20 @@ and pr_atom1 = function
| TacSymmetry (Some id) -> str "Symmetry " ++ pr_ident id
| TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c
+ (* Equality and inversion *)
+ | TacInversion (DepInversion (k,c,ids),hyp) ->
+ hov 1 (str "Dependent " ++ pr_induction_kind k ++
+ pr_quantified_hypothesis hyp ++
+ pr_with_names ids ++ pr_with_constr pr_constr c)
+ | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+ hov 1 (pr_induction_kind k ++ spc () ++
+ pr_quantified_hypothesis hyp ++
+ pr_with_names ids ++ pr_simple_clause pr_ident cl)
+ | TacInversion (InversionUsing (c,cl),hyp) ->
+ hov 1 (str "Inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
+ str "using" ++ spc () ++ pr_constr c ++
+ pr_simple_clause pr_ident cl)
+
and pr_tactic_seq_body tl =
hv 0 (str "[ " ++
prlist_with_sep (fun () -> spc () ++ str "| ") prtac tl ++ str " ]")
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 09:59:10 +0000