1.1 --- a/test/Pure/Isar/Struct_Deriv.thy Sat Aug 14 17:03:35 2010 +0200
1.2 +++ b/test/Pure/Isar/Struct_Deriv.thy Sat Aug 14 18:21:21 2010 +0200
1.3 @@ -121,9 +121,21 @@
1.4 structure Isac_Syn: sig end =
1.5 struct
1.6
1.7 -val _ = List.app(**?find fun app*) KeywordC.keyword
1.8 - [(*"(", ")", "+", "/", "[", "]", ",", "<", "<=", "=", "=>", !!!!!!!!!!!!!!!!!!*)
1.9 - "CAS", "bigtriangledown", "Box", "bullet", "dots", "==", "equiv", "top"];
1.10 +val _ = List.app (*contrib/polyml-5.3.0/src/basis/List.sml*) KeywordC.keyword
1.11 + ["(", ")", "[", "]", ",",
1.12 + "=>", "<=",
1.13 + "==", (* simplification without "=" in term *)
1.14 + "equiv", (* equations, etc *)
1.15 + "bullet", (* indicates a subproblem TODO rewrite_set *)
1.16 + "CAS", "Problem", (* "headlines" of subproblems *)
1.17 + "dots", (* end of subproblem TODO of rewrite_set *)
1.18 +(*"bigtriangledown", indicates a rule *)
1.19 + "THM", "MET", (* a ruleconcerning a theorem, a method *)
1.20 + "Calculate", "Rewrite", "Rewrite_Set", "Rewrite_Inst", "Rewrite_Set_Inst",
1.21 + (* rules; TODO?!? Take REFERENCE *)
1.22 + "top", (* term not following from previous term *)
1.23 + "Box" (* qed *)
1.24 + ];
1.25
1.26 val _ =
1.27 Outer_SyntaxC.command "calculation" "begin calc" (KeywordC.tag_calc KeywordC.calc_begin)
1.28 @@ -144,6 +156,53 @@
1.29 section {* provisional parser for SD *}
1.30 subsection {* calc elements to be executed separately *}
1.31
1.32 +subsubsection {* named_rule *}
1.33 +ML {*
1.34 +"---1----------------------------------------";
1.35 +val named_rule' = (Args.$$$ "Calculate" || Args.$$$ "Rewrite" || Args.$$$ "Rewrite_Set"
1.36 + || Args.$$$ "Rewrite_Inst" || Args.$$$ "Rewrite_Set_Inst")
1.37 + -- Args.name;
1.38 +parse named_rule' "Calculate times";
1.39 +(*(("Calculate", "times"), []) : (string * string) * Token.T list*)
1.40 +
1.41 +fun exec2 (nam, rul) =
1.42 + "*** notebook->ML: " ^ nam ^ " " ^ rul
1.43 + |> (fn x => (x, x))
1.44 + |>> writeln
1.45 + |> #2;
1.46 +(*fn : string * string -> string*)
1.47 +val named_rule = named_rule' >> exec2;
1.48 +"---2----------------------------------------";
1.49 +
1.50 +parse named_rule "Calculate times";
1.51 +(*("*** notebook->ML: Calculate times", []) : string * Token.T list*)
1.52 +
1.53 +"---3--- output on top ----------------------";
1.54 +(*** notebook->ML: Calculate times*)
1.55 +*}
1.56 +
1.57 +subsubsection {* term_rule *}
1.58 +ML {*
1.59 +"---1----------------------------------------";
1.60 +val term_rule' = Args.$$$ "THM" -- Parse.term;
1.61 +parse term_rule' "THM \"(a+x=b)=(x=-a*b)\" ";
1.62 +(*(("THM", "\^E\^Ftoken\^Ea+x=b = x=-a*b\^E\^F\^E"), []) : (string * string) * Token.T list*)
1.63 +val term_rule = term_rule' >> exec2;
1.64 +"---2----------------------------------------";
1.65 +
1.66 +parse term_rule "THM \"(a+x=b)=(x=-a*b)\" ";
1.67 +(*("*** notebook->ML: THM \^E\^Ftoken\^E(a+x=b)=(x=-a*b)\^E\^F\^E", []) : string * Token.T list*)
1.68 +
1.69 +"---3--- output on top ----------------------";
1.70 +(*** notebook->ML: THM (a+x=b)=(x=-a*b)*)
1.71 +*}
1.72 +
1.73 +subsubsection {* rule *}
1.74 +ML {*
1.75 +val rule = named_rule || term_rule;
1.76 +*}
1.77 +
1.78 +
1.79 subsubsection {* PBLheadline *}
1.80 ML {*
1.81 "---1----------------------------------------";
1.82 @@ -204,13 +263,18 @@
1.83
1.84 subsubsection {* headline *}
1.85 ML {*
1.86 -val headline = PBLheadline || CASheadline;
1.87 +val headline = (PBLheadline || CASheadline) -- Scan.option rule;
1.88 +
1.89 +parse headline "Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])";
1.90 +parse headline "CAS \"solve(x+1=2,x)\"";
1.91 +parse headline "CAS \"solve(x+1=2,x)\" Calculate times";
1.92 +parse headline "CAS \"solve(x+1=2,x)\" THM \"(a+x=b)=(x=-a*b)\" ";
1.93 *}
1.94
1.95 subsubsection {* calcline *}
1.96 ML {*
1.97 "---1----------------------------------------";
1.98 -val calcline' = Parse.term;
1.99 +val calcline' = Parse.term ;
1.100 parse calcline' " \"-1 + x = 0\" ";
1.101 (*("\^E\^Ftoken\^E-1 + x = 0\^E\^F\^E", []) : string * Token.T list*)
1.102
1.103 @@ -230,48 +294,6 @@
1.104 (*** notebook->ML: "-1 + x = 0"*)
1.105 *}
1.106
1.107 -subsubsection {* named_rule *}
1.108 -ML {*
1.109 -"---1----------------------------------------";
1.110 -val named_rule' = (Args.$$$ "Calculate" || Args.$$$ "Rewrite" || Args.$$$ "Rewrite_Set"
1.111 - || Args.$$$ "Rewrite_Inst" || Args.$$$ "Rewrite_Set_Inst")
1.112 - -- Args.name;
1.113 -parse named_rule' "Calculate times";
1.114 -(*(("Calculate", "times"), []) : (string * string) * Token.T list*)
1.115 -
1.116 -fun exec2 (nam, rul) =
1.117 - "*** notebook->ML: " ^ nam ^ " " ^ rul
1.118 - |> (fn x => (x, x))
1.119 - |>> writeln
1.120 - |> #2;
1.121 -(*fn : string * string -> string*)
1.122 -val named_rule = named_rule' >> exec2;
1.123 -"---2----------------------------------------";
1.124 -
1.125 -parse named_rule "Calculate times";
1.126 -(*("*** notebook->ML: Calculate times", []) : string * Token.T list*)
1.127 -
1.128 -"---3--- output on top ----------------------";
1.129 -(*** notebook->ML: Calculate times*)
1.130 -*}
1.131 -
1.132 -subsubsection {* term_rule *}
1.133 -ML {*
1.134 -"---1----------------------------------------";
1.135 -val term_rule' = Args.$$$ "THM" -- Parse.term;
1.136 -parse term_rule' "THM \"(a+x=b)=(x=-a*b)\" ";
1.137 -(*(("THM", "\^E\^Ftoken\^Ea+x=b = x=-a*b\^E\^F\^E"), []) : (string * string) * Token.T list*)
1.138 -val term_rule = term_rule' >> exec2;
1.139 -"---2----------------------------------------";
1.140 -
1.141 -parse term_rule "THM \"(a+x=b)=(x=-a*b)\" ";
1.142 -(*("*** notebook->ML: THM \^E\^Ftoken\^E(a+x=b)=(x=-a*b)\^E\^F\^E", []) : string * Token.T list*)
1.143 -
1.144 -"---3--- output on top ----------------------";
1.145 -(*** notebook->ML: THM (a+x=b)=(x=-a*b)*)
1.146 -*}
1.147 -
1.148 -
1.149 subsection {* parser for a whole SD *}
1.150
1.151 subsubsection {* provisional parser setup *}
1.152 @@ -283,7 +305,7 @@
1.153 *}
1.154
1.155 ML {*
1.156 -(*val line = headline || calcline; separate: rewrite_set *)
1.157 +(*val line = headline || calcline; ...this would prevent separation of rewrite_set *)
1.158 val level_up = Args.$$$ "dots" -- calcline;
1.159 *}
1.160
1.161 @@ -316,35 +338,11 @@
1.162 -- (body "")
1.163 -- (Scan.option (Args.$$$ "Box"));
1.164
1.165 -writeln "---0-------";
1.166 +writeln "---0----------------------------------------";
1.167 parse SD "calculation \n\
1.168 \ bullet CAS \"solve(x+1=2,x)\" \n\
1.169 \ dots \"[x = 1]\" ";
1.170 -writeln "---1-------";
1.171 -parse SD "calculation \n\
1.172 - \ bullet CAS \"solve(x+1=2,x)\" \n\
1.173 - \ bullet CAS \"solve (-1 + x = 0, x)\" \n\
1.174 - \ top \"-1 + x = 0\" \n\
1.175 - \ equiv \"[x = 1]\" \n\
1.176 - \ dots \"[x = 1]\" \n\
1.177 - \ dots \"[x = 1]\" ";
1.178 -writeln "---2-------";
1.179 -parse SD "calculation \n\
1.180 - \ bullet CAS \"solve(x+1=2,x)\" \n\
1.181 - \ top \"x + 1 = 2\" \n\
1.182 - \ equiv \"x + 1 - 2 = 0\" \n\
1.183 - \ equiv \"-1 + x = 0\" \n\
1.184 - \ dots \"[x = 1]\" ";
1.185 -writeln "---3-------";
1.186 -parse SD "calculation \n\
1.187 - \ bullet CAS \"solve(x+1=2,x)\" \n\
1.188 - \ top \"x + 1 = 2\" \n\
1.189 - \ equiv \"-1 + x = 0\" \n\
1.190 - \ bullet CAS \"solve (-1 + x = 0, x)\" \n\
1.191 - \ dots \"[x = 1]\" \n\
1.192 - \ dots \"[x = 1]\" \n\
1.193 - \ Box ";
1.194 -writeln "---4-------";
1.195 +writeln "---1-----------------------------------------";
1.196 parse SD "calculation \n\
1.197 \ bullet CAS \"solve(x+1=2,x)\" \n\
1.198 \ top \"x + 1 = 2\" \n\
1.199 @@ -355,20 +353,30 @@
1.200 \ dots \"[x = 1]\" \n\
1.201 \ dots \"[x = 1]\" \n\
1.202 \ Box ";
1.203 -writeln "---5-------";
1.204 -(* GOON
1.205 +writeln "---2-----------------------------------------";
1.206 +
1.207 +(* TODO ?!?
1.208 parse SD "calculation \n\
1.209 \ bullet CAS \"solve(x+1=2,x)\" \n\
1.210 + \ Calculate times \n\
1.211 \ top \"x + 1 = 2\" \n\
1.212 + \ equiv \"-1 + x = 0\" \n\
1.213 + \ THM \"(a+x=b)=(x=-a*b)\" \n\
1.214 + \ dots \"[x = 1]\" \n\
1.215 + \ Box ";
1.216 +*)
1.217 +
1.218 +writeln "---3-----------------------------------------";
1.219 +(* GOON: make equiv a viable prefix at this position !
1.220 +parse SD "calculation \n\
1.221 + \ bullet CAS \"solve(x+1=2,x)\" \n\
1.222 \ bullet CAS \"solve (-1 + x = 0, x)\" \n\
1.223 - \ top \"-1 + x = 0\" \n\
1.224 - \ equiv \"[x = 1]\" \n\
1.225 \ dots \"[x = 1]\" \n\
1.226 \ equiv \"-1 + x = 0\" \n\
1.227 \ dots \"[x = 1]\" \n\
1.228 \ Box ";
1.229 *)
1.230 -writeln "---6-------";
1.231 +writeln "---4-----------------------------------------";
1.232
1.233 *}
1.234
1.235 @@ -380,7 +388,7 @@
1.236 \ top \"x + 1 = 2\" \n\
1.237 \ equiv \"x + 1 - 2 = 0\" \n\
1.238 \ equiv \"-1 + x = 0\" \n\
1.239 - \ bullet CAS \"solve (-1 + x = 0, x\") \n\
1.240 + \ bullet CAS \"solve (-1 + x = 0, x)\" \n\
1.241 \ top \"-1 + x = 0\" \n\
1.242 \ equiv \"x = -1 * -1\" \n\
1.243 \ equiv \"x = 1\" \n\
1.244 @@ -389,7 +397,7 @@
1.245 \ dots \"[x = 1]\" \n\
1.246 \ Box ";
1.247
1.248 -(*parse SD ex1;*)
1.249 +parse SD ex1;
1.250 *}
1.251
1.252 subsubsection {* parser applied to example 2 *}
1.253 @@ -409,6 +417,8 @@
1.254 \ equiv \"y x = -6 * q_0 * L ^ 2 / (-24 * EI) * x ^ 2 + 4 * L * q_0 / (-24 * EI) * x ^ 3 + -1 * q_0 / (-24 * EI) * x ^ 4\" \n\
1.255 \ dots \"y x = -6 * q_0 * L ^ 2 / (-24 * EI) * x ^ 2 + 4 * L * q_0 / (-24 * EI) * x ^ 3 + -1 * q_0 / (-24 * EI) * x ^ 4\" \n\
1.256 \ Box";
1.257 +
1.258 +parse SD ex2;
1.259 *}
1.260
1.261 end
1.262 \ No newline at end of file