--- a/src/HOL/Eisbach/Eisbach.thy Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Thu Apr 30 17:02:57 2015 +0200
@@ -8,14 +8,15 @@
imports Pure
keywords
"method" :: thy_decl and
- "concl"
- "prems" (* FIXME conflict with "prems" in Isar, which is presently dormant *)
+ "conclusion"
+ "premises"
"declares"
"methods"
"\<bar>" "\<Rightarrow>"
"uses"
begin
+
ML_file "parse_tools.ML"
ML_file "eisbach_rule_insts.ML"
ML_file "method_closure.ML"
@@ -38,6 +39,6 @@
Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close>
"rotated theorem premises"
-method solves methods m = \<open>m; fail\<close>
+method solves methods m = (m; fail)
end
--- a/src/HOL/Eisbach/Eisbach_Tools.thy Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy Thu Apr 30 17:02:57 2015 +0200
@@ -35,7 +35,12 @@
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
(fn ctxt => fn (tok, t) =>
(* FIXME proper formatting!? *)
- Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t));
+ Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t) #>
+ setup_trace_method @{binding print_type}
+ (Scan.lift (Scan.ahead Parse.not_eof) -- Args.typ)
+ (fn ctxt => fn (tok, t) =>
+ (* FIXME proper formatting!? *)
+ Token.unparse tok ^ ": " ^ Syntax.string_of_typ ctxt t));
end
\<close>
--- a/src/HOL/Eisbach/Examples.thy Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Examples.thy Thu Apr 30 17:02:57 2015 +0200
@@ -11,19 +11,19 @@
subsection \<open>Basic methods\<close>
-method my_intros = \<open>rule conjI | rule impI\<close>
+method my_intros = (rule conjI | rule impI)
lemma "P \<and> Q \<longrightarrow> Z \<and> X"
apply my_intros+
oops
-method my_intros' uses intros = \<open>rule conjI | rule impI | rule intros\<close>
+method my_intros' uses intros = (rule conjI | rule impI | rule intros)
lemma "P \<and> Q \<longrightarrow> Z \<or> X"
apply (my_intros' intros: disjI1)+
oops
-method my_spec for x :: 'a = \<open>drule spec[where x="x"]\<close>
+method my_spec for x :: 'a = (drule spec[where x="x"])
lemma "\<forall>x. P x \<Longrightarrow> P x"
apply (my_spec x)
@@ -34,11 +34,11 @@
subsection \<open>Focusing and matching\<close>
method match_test =
- \<open>match prems in U: "P x \<and> Q x" for P Q x \<Rightarrow>
+ (match premises in U: "P x \<and> Q x" for P Q x \<Rightarrow>
\<open>print_term P,
print_term Q,
print_term x,
- print_fact U\<close>\<close>
+ print_fact U\<close>)
lemma "\<And>x. P x \<and> Q x \<Longrightarrow> A x \<and> B x \<Longrightarrow> R x y \<Longrightarrow> True"
apply match_test -- \<open>Valid match, but not quite what we were expecting..\<close>
@@ -51,8 +51,6 @@
back
back
back
- back
- back
oops
text \<open>Use matching to avoid "improper" methods\<close>
@@ -60,18 +58,18 @@
lemma focus_test:
shows "\<And>x. \<forall>x. P x \<Longrightarrow> P x"
apply (my_spec "x :: 'a", assumption)? -- \<open>Wrong x\<close>
- apply (match concl in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
+ apply (match conclusion in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
done
text \<open>Matches are exclusive. Backtracking will not occur past a match\<close>
method match_test' =
- \<open>match concl in
+ (match conclusion in
"P \<and> Q" for P Q \<Rightarrow>
\<open>print_term P, print_term Q, rule conjI[where P="P" and Q="Q"]; assumption\<close>
\<bar> "H" for H \<Rightarrow> \<open>print_term H\<close>
- \<close>
+ )
text \<open>Solves goal\<close>
lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q"
@@ -89,20 +87,20 @@
method my_spec_guess =
- \<open>match concl in "P (x :: 'a)" for P x \<Rightarrow>
+ (match conclusion in "P (x :: 'a)" for P x \<Rightarrow>
\<open>drule spec[where x=x],
print_term P,
- print_term x\<close>\<close>
+ print_term x\<close>)
lemma "\<forall>x. P (x :: nat) \<Longrightarrow> Q (x :: nat)"
apply my_spec_guess
oops
method my_spec_guess2 =
- \<open>match prems in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
+ (match premises in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
\<open>insert spec[where x=x, OF U],
print_term P,
- print_term Q\<close>\<close>
+ print_term Q\<close>)
lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> Q x \<Longrightarrow> Q x"
apply my_spec_guess2? -- \<open>Fails. Note that both "P"s must match\<close>
@@ -118,7 +116,7 @@
subsection \<open>Higher-order methods\<close>
method higher_order_example for x methods meth =
- \<open>cases x, meth, meth\<close>
+ (cases x, meth, meth)
lemma
assumes A: "x = Some a"
@@ -129,12 +127,12 @@
subsection \<open>Recursion\<close>
method recursion_example for x :: bool =
- \<open>print_term x,
+ (print_term x,
match (x) in "A \<and> B" for A B \<Rightarrow>
- \<open>(print_term A,
+ \<open>print_term A,
print_term B,
recursion_example A,
- recursion_example B) | -\<close>\<close>
+ recursion_example B | -\<close>)
lemma "P"
apply (recursion_example "(A \<and> D) \<and> (B \<and> C)")
@@ -151,15 +149,15 @@
subsection \<open>Demo\<close>
-method solve methods m = \<open>m;fail\<close>
+method solve methods m = (m; fail)
named_theorems intros and elims and subst
method prop_solver declares intros elims subst =
- \<open>(assumption |
+ (assumption |
rule intros | erule elims |
subst subst | subst (asm) subst |
- (erule notE; solve \<open>prop_solver\<close>))+\<close>
+ (erule notE; solve \<open>prop_solver\<close>))+
lemmas [intros] =
conjI
@@ -177,11 +175,11 @@
done
method guess_all =
- \<open>match prems in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
- \<open>match prems in "?H (y :: 'a)" for y \<Rightarrow>
+ (match premises in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
+ \<open>match premises in "?H (y :: 'a)" for y \<Rightarrow>
\<open>rule allE[where P = P and x = y, OF U]\<close>
- | match concl in "?H (y :: 'a)" for y \<Rightarrow>
- \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>\<close>
+ | match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
+ \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> P y \<Longrightarrow> Q y"
apply guess_all
@@ -193,10 +191,10 @@
done
method guess_ex =
- \<open>match concl in
+ (match conclusion in
"\<exists>x. P (x :: 'a)" for P \<Rightarrow>
- \<open>match prems in "?H (x :: 'a)" for x \<Rightarrow>
- \<open>rule exI[where x=x]\<close>\<close>\<close>
+ \<open>match premises in "?H (x :: 'a)" for x \<Rightarrow>
+ \<open>rule exI[where x=x]\<close>\<close>)
lemma "P x \<Longrightarrow> \<exists>x. P x"
apply guess_ex
@@ -204,7 +202,7 @@
done
method fol_solver =
- \<open>(guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>\<close>
+ ((guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>)
declare
allI [intros]
--- a/src/HOL/Eisbach/Tests.thy Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Tests.thy Thu Apr 30 17:02:57 2015 +0200
@@ -8,12 +8,12 @@
imports Main Eisbach_Tools
begin
+
section \<open>Named Theorems Tests\<close>
named_theorems foo
-method foo declares foo =
- \<open>rule foo\<close>
+method foo declares foo = (rule foo)
lemma
assumes A [foo]: A
@@ -30,12 +30,12 @@
fix A y
have "(\<And>x. A x) \<Longrightarrow> A y"
- apply (rule dup, match prems in Y: "\<And>B. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
- apply (rule dup, match prems in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
- apply (rule dup, match prems in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match concl in "P y" for y \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=y]\<close>\<close>)
- apply (rule dup, match prems in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match concl in "P z" for z \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=z]\<close>\<close>)
- apply (rule dup, match concl in "P y" for P \<Rightarrow> \<open>match prems in Y: "\<And>z. P z" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
- apply (match prems in Y: "\<And>z :: 'a. P z" for P \<Rightarrow> \<open>match concl in "P y" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
+ apply (rule dup, match premises in Y: "\<And>B. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
+ apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
+ apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P y" for y \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=y]\<close>\<close>)
+ apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P z" for z \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=z]\<close>\<close>)
+ apply (rule dup, match conclusion in "P y" for P \<Rightarrow> \<open>match premises in Y: "\<And>z. P z" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
+ apply (match premises in Y: "\<And>z :: 'a. P z" for P \<Rightarrow> \<open>match conclusion in "P y" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
done
assume X: "\<And>x. A x" "A y"
@@ -44,37 +44,48 @@
apply (match X in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
apply (match X in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B, print_term x\<close>)
apply (insert X)
- apply (match prems in Y:"\<And>B. A B" and Y':"B y" for B and y :: 'a \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>)
- apply (match prems in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
- apply (match prems in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
- apply (match concl in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>)
+ apply (match premises in Y:"\<And>B. A B" and Y':"B y" for B and y :: 'a \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>)
+ apply (match premises in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
+ apply (match premises in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
+ apply (match conclusion in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>)
apply assumption
done
+ {
+ fix B x y
+ assume X: "\<And>x y. B x x y"
+ have "B x x y"
+ by (match X in Y:"\<And>y. B y y z" for z \<Rightarrow> \<open>rule Y[where y=x]\<close>)
+
+ fix A B
+ have "(\<And>x y. A (B x) y) \<Longrightarrow> A (B x) y"
+ by (match premises in Y: "\<And>xx. ?H (B xx)" \<Rightarrow> \<open>rule Y\<close>)
+ }
+
(* match focusing retains prems *)
fix B x
have "(\<And>x. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x"
- apply (match prems in Y: "\<And>z :: 'a. A z" \<Rightarrow> \<open>match prems in Y': "\<And>z :: 'b. B z" \<Rightarrow> \<open>print_fact Y, print_fact Y', rule Y'[where z=x]\<close>\<close>)
+ apply (match premises in Y: "\<And>z :: 'a. A z" \<Rightarrow> \<open>match premises in Y': "\<And>z :: 'b. B z" \<Rightarrow> \<open>print_fact Y, print_fact Y', rule Y'[where z=x]\<close>\<close>)
done
(*Attributes *)
fix C
have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x \<and> B x \<and> A y"
apply (intro conjI)
- apply (match prems in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>)
- apply (match prems in Y: "\<And>z :: 'a. A z" \<Rightarrow> \<open>match prems in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>\<close>)
- apply (match prems in Y[thin]: "\<And>z :: 'a. A z" \<Rightarrow> \<open>(match prems in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>fail\<close> \<bar> Y': "?H" \<Rightarrow> \<open>-\<close>)\<close>)
+ apply (match premises in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>)
+ apply (match premises in Y: "\<And>z :: 'a. A z" \<Rightarrow> \<open>match premises in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>\<close>)
+ apply (match premises in Y[thin]: "\<And>z :: 'a. A z" \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>print_fact Y,fail\<close> \<bar> Y': "?H" \<Rightarrow> \<open>-\<close>)\<close>)
apply assumption
done
fix A B C D
have "\<And>uu'' uu''' uu uu'. (\<And>x :: 'a. A uu' x) \<Longrightarrow> D uu y \<Longrightarrow> (\<And>z. B uu z) \<Longrightarrow> C uu y \<Longrightarrow> (\<And>z y. C uu z) \<Longrightarrow> B uu x \<and> B uu x \<and> C uu y"
- apply (match prems in Y[thin]: "\<And>z :: 'a. A ?zz' z" and
+ apply (match premises in Y[thin]: "\<And>z :: 'a. A ?zz' z" and
Y'[thin]: "\<And>rr :: 'b. B ?zz rr" \<Rightarrow>
\<open>print_fact Y, print_fact Y', intro conjI, rule Y', insert Y', insert Y'[where rr=x]\<close>)
- apply (match prems in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
+ apply (match premises in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
apply (insert TrueI)
- apply (match prems in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>)
+ apply (match premises in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>)
apply assumption
done
@@ -82,33 +93,33 @@
(* Multi-matches. As many facts as match are bound. *)
fix A B C x
have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
- apply (match prems in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
- apply (match prems in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
- apply (match prems in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
+ apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
+ apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
+ apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
done
fix A B C x
have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
- apply (match prems in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
- apply (match prems in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
- apply (match prems in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
+ apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
+ apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
+ apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
done
(*We may use for-fixes in multi-matches too. All bound facts must agree on the fixed term *)
fix A B C x
have "(\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> (\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
- apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
- apply (match prems in Y: "\<And>z :: 'a. ?A z \<longrightarrow> False" (multi) \<Rightarrow> \<open>print_fact Y, fail\<close> \<bar> "C y" \<Rightarrow> \<open>print_term C\<close>) (* multi-match must bind something *)
- apply (match prems in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
- apply (match prems in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
+ apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
+ apply (match premises in Y: "\<And>z :: 'a. ?A z \<longrightarrow> False" (multi) \<Rightarrow> \<open>print_fact Y, fail\<close> \<bar> "C y" \<Rightarrow> \<open>print_term C\<close>) (* multi-match must bind something *)
+ apply (match premises in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
+ apply (match premises in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
done
(* Attributes *)
fix A B C x
have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
- apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct1] in Y':"?H" (multi) \<Rightarrow> \<open>intro conjI,rule Y'\<close>\<close>)
- apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct2] in Y':"?H" (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>)
+ apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct1] in Y':"?H" (multi) \<Rightarrow> \<open>intro conjI,rule Y'\<close>\<close>)
+ apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct2] in Y':"?H" (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>)
apply assumption
done
@@ -123,20 +134,31 @@
(* Testing THEN_ALL_NEW within match *)
fix A B C x
have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
- apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI ; ((rule Y[THEN conjunct1])?); rule Y[THEN conjunct2] \<close>)
+ apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI ; ((rule Y[THEN conjunct1])?); rule Y[THEN conjunct2] \<close>)
done
(* Cut tests *)
fix A B C
have "D \<and> C \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
- by (((match prems in I: "P \<and> Q" (cut)
+ by (((match premises in I: "P \<and> Q" (cut)
and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?), simp)
have "A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
- by (((match prems in I: "P \<and> Q" (cut)
+ by (((match premises in I: "P \<and> Q" (cut)
and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?, simp) | simp)
+ fix f x y
+ have "f x y \<Longrightarrow> f x y"
+ by (match conclusion in "f x y" for f x y \<Rightarrow> \<open>print_term f\<close>)
+
+ fix A B C
+ assume X: "A \<and> B" "A \<and> C" C
+ have "A \<and> B \<and> C"
+ by (match X in H: "A \<and> ?H" (multi,cut) \<Rightarrow>
+ \<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> \<open>fail\<close>\<close>
+ | simp add: X)
+
end
(* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
@@ -144,7 +166,7 @@
legitimate pairs.*)
schematic_lemma "?A x \<Longrightarrow> A x"
- apply (match concl in "H" for H \<Rightarrow> \<open>match concl in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
+ apply (match conclusion in "H" for H \<Rightarrow> \<open>match conclusion in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
apply assumption
done
@@ -171,7 +193,7 @@
NONE => ()
| SOME _ => error "Found internal fact")\<close>
-method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = \<open>rule uses_test\<^sub>1_uses\<close>
+method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = (rule uses_test\<^sub>1_uses)
lemma assumes A shows A by (uses_test\<^sub>1 uses_test\<^sub>1_uses: assms)
@@ -184,9 +206,9 @@
(* Testing term and fact passing in recursion *)
method recursion_example for x :: bool uses facts =
- \<open>match (x) in
+ (match (x) in
"A \<and> B" for A B \<Rightarrow> \<open>(recursion_example A facts: facts, recursion_example B facts: facts)\<close>
- \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>\<close>
+ \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>)
lemma
assumes asms: "A" "B" "C" "D"
@@ -196,11 +218,11 @@
done
(*Method.sections in existing method*)
-method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = \<open>simp add: my_simp\<^sub>1_facts\<close>
+method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = (simp add: my_simp\<^sub>1_facts)
lemma assumes A shows A by (my_simp\<^sub>1 my_simp\<^sub>1_facts: assms)
(*Method.sections via Eisbach argument parser*)
-method uses_test\<^sub>2 uses uses_test\<^sub>2_uses = \<open>uses_test\<^sub>1 uses_test\<^sub>1_uses: uses_test\<^sub>2_uses\<close>
+method uses_test\<^sub>2 uses uses_test\<^sub>2_uses = (uses_test\<^sub>1 uses_test\<^sub>1_uses: uses_test\<^sub>2_uses)
lemma assumes A shows A by (uses_test\<^sub>2 uses_test\<^sub>2_uses: assms)
@@ -208,7 +230,7 @@
named_theorems declare_facts\<^sub>1
-method declares_test\<^sub>1 declares declare_facts\<^sub>1 = \<open>rule declare_facts\<^sub>1\<close>
+method declares_test\<^sub>1 declares declare_facts\<^sub>1 = (rule declare_facts\<^sub>1)
lemma assumes A shows A by (declares_test\<^sub>1 declare_facts\<^sub>1: assms)
@@ -218,28 +240,58 @@
subsection \<open>Rule Instantiation Tests\<close>
method my_allE\<^sub>1 for x :: 'a and P :: "'a \<Rightarrow> bool" =
- \<open>erule allE [where x = x and P = P]\<close>
+ (erule allE [where x = x and P = P])
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>1 x Q)
method my_allE\<^sub>2 for x :: 'a and P :: "'a \<Rightarrow> bool" =
- \<open>erule allE [of P x]\<close>
+ (erule allE [of P x])
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>2 x Q)
method my_allE\<^sub>3 for x :: 'a and P :: "'a \<Rightarrow> bool" =
- \<open>match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
- \<open>erule X [where x = x and P = P]\<close>\<close>
+ (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
+ \<open>erule X [where x = x and P = P]\<close>)
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>3 x Q)
method my_allE\<^sub>4 for x :: 'a and P :: "'a \<Rightarrow> bool" =
- \<open>match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
- \<open>erule X [of x P]\<close>\<close>
+ (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
+ \<open>erule X [of x P]\<close>)
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>4 x Q)
+
+(* Polymorphism test *)
+
+axiomatization foo' :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool"
+axiomatization where foo'_ax1: "foo' x y z \<Longrightarrow> z \<and> y"
+axiomatization where foo'_ax2: "foo' x y y \<Longrightarrow> x \<and> z"
+
+lemmas my_thms = foo'_ax1 foo'_ax2
+
+definition first_id where "first_id x = x"
+
+lemmas my_thms' = my_thms[of "first_id x" for x]
+
+method print_conclusion = (match conclusion in concl for concl \<Rightarrow> \<open>print_term concl\<close>)
+
+lemma
+ assumes foo: "\<And>x (y :: bool). foo' (A x) B (A x)"
+ shows "\<And>z. A z \<and> B"
+ apply
+ (match conclusion in "f x y" for f y and x :: "'d :: type" \<Rightarrow> \<open>
+ match my_thms' in R:"\<And>(x :: 'f :: type). ?P (first_id x) \<Longrightarrow> ?R"
+ and R':"\<And>(x :: 'f :: type). ?P' (first_id x) \<Longrightarrow> ?R'" \<Rightarrow> \<open>
+ match (x) in "q :: 'f" for q \<Rightarrow> \<open>
+ rule R[of q,simplified first_id_def],
+ print_conclusion,
+ rule foo
+ \<close>\<close>\<close>)
+ done
+
+
ML {*
structure Data = Generic_Data
(
@@ -254,7 +306,7 @@
setup \<open>Context.theory_map (Data.put @{thms TrueI})\<close>
-method dynamic_thms_test = \<open>rule test_dyn\<close>
+method dynamic_thms_test = (rule test_dyn)
locale foo =
fixes A
@@ -269,4 +321,12 @@
end
+(* Method name internalization test *)
+
+method test2 = (simp)
+
+method simp = fail
+
+lemma "A \<Longrightarrow> A" by test2
+
end
--- a/src/HOL/Eisbach/match_method.ML Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Thu Apr 30 17:02:57 2015 +0200
@@ -46,8 +46,8 @@
val aconv_net = Item_Net.init (op aconv) single;
val parse_match_kind =
- Scan.lift @{keyword "concl"} >> K Match_Concl ||
- Scan.lift @{keyword "prems"} >> K Match_Prems ||
+ Scan.lift @{keyword "conclusion"} >> K Match_Concl ||
+ Scan.lift @{keyword "premises"} >> K Match_Prems ||
Scan.lift (@{keyword "("}) |-- Args.term --| Scan.lift (@{keyword ")"}) >>
(fn t => Match_Term (Item_Net.update t aconv_net)) ||
Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.full_rules));
@@ -60,8 +60,8 @@
Parse_Tools.parse_term_val Parse.binding;
val fixes =
- Parse.and_list1 (Scan.repeat1 bound_term --
- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (rpair T) xs))
+ Parse.and_list1 (Scan.repeat1 (Parse.position bound_term) --
+ Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (fn (nm,pos) => ((nm,T),pos)) xs))
>> flat;
val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
@@ -77,18 +77,17 @@
fun dynamic_fact ctxt =
bound_term -- Args.opt_attribs (Attrib.check_name ctxt);
-type match_args = {unify : bool, multi : bool, cut : bool};
+type match_args = {multi : bool, cut : bool};
val parse_match_args =
Scan.optional (Args.parens (Parse.enum1 ","
- (Args.$$$ "unify" || Args.$$$ "multi" || Args.$$$ "cut"))) [] >>
+ (Args.$$$ "multi" || Args.$$$ "cut"))) [] >>
(fn ss =>
- fold (fn s => fn {unify, multi, cut} =>
+ fold (fn s => fn {multi, cut} =>
(case s of
- "unify" => {unify = true, multi = multi, cut = cut}
- | "multi" => {unify = unify, multi = true, cut = cut}
- | "cut" => {unify = unify, multi = multi, cut = true}))
- ss {unify = false, multi = false, cut = false});
+ "multi" => {multi = true, cut = cut}
+ | "cut" => {multi = multi, cut = true}))
+ ss {multi = false, cut = false});
(*TODO: Shape holes in thms *)
fun parse_named_pats match_kind =
@@ -114,12 +113,12 @@
(Parse_Tools.the_real_val b,
map (Attrib.attribute ctxt) att)) b, match_args), v)
| _ => raise Fail "Expected closed term") ts
- val fixes' = map (fn (p, _) => Parse_Tools.the_real_val p) fixes
+ val fixes' = map (fn ((p, _),_) => Parse_Tools.the_real_val p) fixes
in (ts', fixes', text) end
| SOME _ => error "Unexpected token value in match cartouche"
| NONE =>
let
- val fixes' = map (fn (pb, otyp) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
+ val fixes' = map (fn ((pb, otyp),_) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt;
val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
@@ -134,6 +133,14 @@
map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
|> Syntax.check_terms ctxt3;
+ val pat_fixes = fold (Term.add_frees) pats [] |> map fst;
+
+ val _ = map2 (fn nm => fn (_,pos) => member (op =) pat_fixes nm orelse
+ error ("For-fixed variable must be bound in some pattern." ^ Position.here pos))
+ fix_nms fixes;
+
+ val _ = map (Term.map_types Type.no_tvars) pats
+
val ctxt4 = fold Variable.declare_term pats ctxt3;
val (Ts, ctxt5) = ctxt4 |> fold_map Proof_Context.inferred_param fix_nms;
@@ -146,12 +153,6 @@
| reject_extra_free _ () = ();
val _ = (fold o fold_aterms) reject_extra_free pats ();
- (*fun test_multi_bind {multi = multi, ...} pat = multi andalso
- not (null (inter (op =) (map Free (Term.add_frees pat [])) real_fixes)) andalso
- error "Cannot fix terms in multi-match. Use a schematic instead."
-
- val _ = map2 (fn pat => fn (_, (_, match_args)) => test_multi_bind match_args pat) pats ts*)
-
val binds =
map (fn (b, _) => Option.map (fn (b, att) => (Parse_Tools.the_parse_val b, att)) b) ts;
@@ -184,7 +185,7 @@
|> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
||> Proof_Context.restore_mode ctxt;
- val (src, text) = Method_Closure.read_text_closure ctxt6 (Token.input_of cartouche);
+ val (src, text) = Method_Closure.read_inner_text_closure ctxt6 (Token.input_of cartouche);
val morphism =
Variable.export_morphism ctxt6
@@ -206,7 +207,7 @@
val real_fixes' = map (Morphism.term morphism) real_fixes;
val _ =
- ListPair.app (fn ((Parse_Tools.Parse_Val (_, f), _), t) => f t) (fixes, real_fixes');
+ ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f),_) , _), t) => f t) (fixes, real_fixes');
val match_args = map (fn (_, (_, match_args)) => match_args) ts;
val binds'' = (binds' ~~ match_args) ~~ pats';
@@ -234,19 +235,9 @@
let
val ts' = map (Envir.norm_term env) ts;
val insts = map (Thm.cterm_of ctxt) ts' ~~ map (Thm.cterm_of ctxt) params;
- val tags = Thm.get_tags thm;
- (*
- val Tinsts = Type.raw_matches ((map (fastype_of) params), (map (fastype_of) ts')) Vartab.empty
- |> Vartab.dest
- |> map (fn (xi, (S, typ)) => (certT (TVar (xi, S)), certT typ))
- *)
-
- val thm' = Drule.cterm_instantiate insts thm
- (*|> Thm.instantiate (Tinsts, [])*)
- |> Thm.map_tags (K tags);
in
- thm'
+ Drule.cterm_instantiate insts thm
end;
fun do_inst fact_insts' env text ctxt =
@@ -282,6 +273,7 @@
val morphism =
Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $>
+ Morphism.typ_morphism "do_inst.type" (Envir.norm_type (Envir.type_env env)) $>
Morphism.fact_morphism "do_inst.fact" (maps expand_fact);
val text' = Method.map_source (Token.transform_src morphism) text;
@@ -303,32 +295,61 @@
val pat'' :: params'' = map (Morphism.term morphism) (pat' :: params');
fun prep_head (t, att) = (dest_internal_fact t, att);
+
in
((((Option.map prep_head x, args), params''), pat''), ctxt')
end;
-fun match_filter_env ctxt fixes (ts, params) thm env =
+fun recalculate_maxidx env =
let
+ val tenv = Envir.term_env env;
+ val tyenv = Envir.type_env env;
+ val max_tidx = Vartab.fold (fn (_,(_,t)) => curry Int.max (maxidx_of_term t)) tenv ~1;
+ val max_Tidx = Vartab.fold (fn (_,(_,T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1;
+ in
+ Envir.Envir
+ {maxidx = Int.max (Int.max (max_tidx,max_Tidx),Envir.maxidx_of env),
+ tenv = tenv, tyenv = tyenv}
+ end
+
+fun match_filter_env inner_ctxt morphism pat_vars fixes (ts, params) thm inner_env =
+ let
+ val tenv = Envir.term_env inner_env
+ |> Vartab.map (K (fn (T,t) => (Morphism.typ morphism T,Morphism.term morphism t)));
+
+ val tyenv = Envir.type_env inner_env
+ |> Vartab.map (K (fn (S,T) => (S,Morphism.typ morphism T)));
+
+ val outer_env = Envir.Envir {maxidx = Envir.maxidx_of inner_env, tenv = tenv, tyenv = tyenv};
+
val param_vars = map Term.dest_Var params;
- val params' = map (Envir.lookup env) param_vars;
+
+ val params' = map (fn (xi,_) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars;
val fixes_vars = map Term.dest_Var fixes;
- val tenv = Envir.term_env env;
val all_vars = Vartab.keys tenv;
val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars;
- val tenv' = Envir.term_env env
+ val tenv' = tenv
|> fold (Vartab.delete_safe) extra_vars;
val env' =
- Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env};
+ Envir.Envir {maxidx = Envir.maxidx_of outer_env, tenv = tenv', tyenv = tyenv}
+ |> recalculate_maxidx;
+
+ val all_params_bound = forall (fn SOME (_,(Var _)) => true | _ => false) params';
+
+ val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars;
- val all_params_bound = forall (fn SOME (Var _) => true | _ => false) params';
+ val all_pat_fixes_bound = forall (fn (xi,_) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
+
+ val thm' = Morphism.thm morphism thm;
+
in
- if all_params_bound
- then SOME (case ts of SOME ts => inst_thm ctxt env params ts thm | _ => thm, env')
+ if all_params_bound andalso all_pat_fixes_bound then
+ SOME (case ts of SOME ts => inst_thm inner_ctxt outer_env params ts thm' | _ => thm', env')
else NONE
end;
@@ -436,28 +457,78 @@
val raise_match : (thm * Envir.env) Seq.seq = Seq.make (fn () => raise MATCH_CUT);
+fun map_handle seq =
+ Seq.make (fn () =>
+ (case (Seq.pull seq handle MATCH_CUT => NONE) of
+ SOME (x, seq') => SOME (x, map_handle seq')
+ | NONE => NONE));
+
+fun deduplicate eq prev seq =
+ Seq.make (fn () =>
+ (case (Seq.pull seq) of
+ SOME (x, seq') =>
+ if member eq prev x
+ then Seq.pull (deduplicate eq prev seq')
+ else SOME (x,deduplicate eq (x :: prev) seq')
+ | NONE => NONE));
+
+fun consistent_env env =
+ let
+ val tenv = Envir.term_env env;
+ val tyenv = Envir.type_env env;
+ in
+ forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
+ end;
+
+fun eq_env (env1,env2) =
+ let
+ val tyenv1 = Envir.type_env env1;
+ val tyenv2 = Envir.type_env env2;
+ in
+ Envir.maxidx_of env1 = Envir.maxidx_of env1 andalso
+ ListPair.allEq (fn ((var, (_, t)), (var', (_, t'))) =>
+ (var = var' andalso
+ Envir.eta_contract (Envir.norm_term env1 t) aconv
+ Envir.eta_contract (Envir.norm_term env2 t')))
+ (apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2))
+ andalso
+ ListPair.allEq (fn ((var, (_, T)), (var', (_,T'))) =>
+ var = var' andalso Envir.norm_type tyenv1 T = Envir.norm_type tyenv2 T')
+ (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2))
+ end;
+
+
fun match_facts ctxt fixes prop_pats get =
let
fun is_multi (((_, x : match_args), _), _) = #multi x;
- fun is_unify (_, x : match_args) = #unify x;
fun is_cut (_, x : match_args) = #cut x;
fun match_thm (((x, params), pat), thm) env =
let
fun try_dest_term term = the_default term (try Logic.dest_term term);
+ val pat_vars = Term.add_vars pat [];
+
val pat' = pat |> Envir.norm_term env |> try_dest_term;
- val item' = Thm.prop_of thm |> try_dest_term;
+ val (((Tinsts', insts),[thm']), inner_ctxt) = Variable.import false [thm] ctxt
+
+ val item' = Thm.prop_of thm' |> try_dest_term;
+
val ts = Option.map (fst o fst) (fst x);
- (*FIXME: Do we need to move one of these patterns above the other?*)
+
+ val outer_ctxt = ctxt |> Variable.declare_maxidx (Envir.maxidx_of env);
+
+ val morphism = Variable.export_morphism inner_ctxt outer_ctxt;
val matches =
- (if is_unify x
- then Unify.smash_unifiers (Context.Proof ctxt) [(pat', item') ] env
- else Unify.matchers (Context.Proof ctxt) [(pat', item')])
+ (Unify.matchers (Context.Proof ctxt) [(pat', item')])
+ |> Seq.filter consistent_env
|> Seq.map_filter (fn env' =>
- match_filter_env ctxt fixes (ts, params) thm (Envir.merge (env, env')))
+ match_filter_env inner_ctxt morphism pat_vars fixes
+ (ts, params) thm' (Envir.merge (env, env')))
+ |> Seq.map (apfst (Thm.map_tags (K (Thm.get_tags thm))))
+ |> deduplicate (eq_snd eq_env) []
|> is_cut x ? (fn t => Seq.make (fn () =>
Option.map (fn (x, _) => (x, raise_match)) (Seq.pull t)));
in
@@ -487,12 +558,6 @@
val all_matches =
Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1)
- |> Seq.filter (fn (_, e) => forall (is_some o Envir.lookup e o Term.dest_Var) fixes);
-
- fun map_handle seq = Seq.make (fn () =>
- (case (Seq.pull seq handle MATCH_CUT => NONE) of
- SOME (x, seq') => SOME (x, map_handle seq')
- | NONE => NONE));
in
map_handle all_matches
end;
--- a/src/HOL/Eisbach/method_closure.ML Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Thu Apr 30 17:02:57 2015 +0200
@@ -14,7 +14,8 @@
val tag_free_thm: thm -> thm
val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute
val read_inner_method: Proof.context -> Token.src -> Method.text
- val read_text_closure: Proof.context -> Input.source -> Token.src * Method.text
+ val read_text_closure: Proof.context -> Token.src -> Token.src * Method.text
+ val read_inner_text_closure: Proof.context -> Input.source -> Token.src * Method.text
val method_evaluate: Method.text -> Proof.context -> Method.method
val get_inner_method: Proof.context -> string * Position.T ->
(term list * (string list * string list)) * Method.text
@@ -22,9 +23,9 @@
term list -> (string * thm list) list -> Method.method list ->
Proof.context -> Method.method
val method_definition: binding -> (binding * typ option * mixfix) list ->
- binding list -> binding list -> binding list -> Input.source -> local_theory -> local_theory
+ binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
val method_definition_cmd: binding -> (binding * string option * mixfix) list ->
- binding list -> binding list -> binding list -> Input.source -> local_theory -> local_theory
+ binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
end;
structure Method_Closure: METHOD_CLOSURE =
@@ -97,38 +98,36 @@
val parser = Parse.!!! (Method.parser' ctxt 0 --| Scan.ahead Parse.eof);
in
(case Scan.read Token.stopper parser toks of
- SOME (method_text, _) => method_text
+ SOME (method_text, pos) => (Method.report (method_text, pos); method_text)
| NONE => error ("Failed to parse method" ^ Position.here (#2 (Token.name_of_src src))))
end;
-fun read_text_closure ctxt input =
+fun read_text_closure ctxt source =
let
- (*tokens*)
+ val src = Token.init_assignable_src source;
+ val method_text = read_inner_method ctxt src;
+ val method_text' = Method.map_source (Method.method_closure ctxt) method_text;
+ (*FIXME: Does not markup method parameters. Needs to be done by Method.parser' directly. *)
+ val _ = Method.map_source (fn src => (try (Method.check_name ctxt) (Token.name_of_src src);src)) method_text;
+ val src' = Token.closure_src src;
+ in (src', method_text') end;
+
+fun read_inner_text_closure ctxt input =
+ let
val keywords = Thy_Header.get_keywords' ctxt;
val toks =
Input.source_explode input
|> Token.read_no_commands keywords (Scan.one Token.not_eof);
- val _ =
- toks |> List.app (fn tok =>
- if Token.keyword_with Symbol.is_ascii_identifier tok then
- Context_Position.report ctxt (Token.pos_of tok) Markup.keyword1
- else ());
+ in read_text_closure ctxt (Token.src ("", Input.pos_of input) toks) end;
- (*source closure*)
- val src =
- Token.src ("", Input.pos_of input) toks
- |> Token.init_assignable_src;
- val method_text = read_inner_method ctxt src;
- val method_text' = Method.map_source (Method.method_closure ctxt) method_text;
- val src' = Token.closure_src src;
- in (src', method_text') end;
val parse_method =
Args.context -- Scan.lift (Parse.token Parse.cartouche) >> (fn (ctxt, tok) =>
(case Token.get_value tok of
NONE =>
let
- val (src, text) = read_text_closure ctxt (Token.input_of tok);
+ val input = Token.input_of tok;
+ val (src,text) = read_inner_text_closure ctxt input;
val _ = Token.assign (SOME (Token.Source src)) tok;
in text end
| SOME (Token.Source src) => read_inner_method ctxt src
@@ -274,7 +273,7 @@
fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
end;
-fun gen_method_definition prep_vars name vars uses attribs methods body lthy =
+fun gen_method_definition prep_vars name vars uses attribs methods source lthy =
let
val (uses_nms, lthy1) = lthy
|> Proof_Context.concealed
@@ -304,7 +303,7 @@
(parser term_args
(fn (fixes, decl) => fn ctxt => get_recursive_method ctxt fixes (decl ctxt))) "(internal)";
- val (src, text) = read_text_closure lthy3 body;
+ val (src, text) = read_text_closure lthy3 source;
val morphism =
Variable.export_morphism lthy3
@@ -338,7 +337,8 @@
((Scan.optional (@{keyword "uses"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
(Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) --
(Scan.optional (@{keyword "methods"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
- Parse.!!! (@{keyword "="} |-- Parse.token Parse.cartouche)
- >> (fn ((((name, vars), (uses, attribs)), methods), cartouche) =>
- method_definition_cmd name vars uses attribs methods (Token.input_of cartouche)));
+ Parse.!!! (@{keyword "="}
+ |-- (Parse.position (Parse.args1 (K true)) >> (fn (args, pos) => Token.src ("", pos) args)))
+ >> (fn ((((name, vars), (uses, attribs)), methods), source) =>
+ method_definition_cmd name vars uses attribs methods source));
end;