ProgTutorial/General.thy
changeset 336 a12bb28fe2bd
parent 335 163ac0662211
child 337 a456a21f608a
equal deleted inserted replaced
335:163ac0662211 336:a12bb28fe2bd
  1129 local_setup %gray {* 
  1129 local_setup %gray {* 
  1130   LocalTheory.note Thm.theoremK 
  1130   LocalTheory.note Thm.theoremK 
  1131     ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
  1131     ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
  1132 
  1132 
  1133 
  1133 
  1134 (* FIXME: some code below *)
       
  1135 
       
  1136 (*<*)
       
  1137 (*
  1134 (*
  1138 setup {*
  1135 setup {*
  1139  Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] 
  1136  Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] 
  1140 *}
  1137 *}
  1141 *)
       
  1142 lemma "bar = (1::nat)"
  1138 lemma "bar = (1::nat)"
  1143   oops
  1139   oops
  1144 
  1140 
  1145 (*
       
  1146 setup {*   
  1141 setup {*   
  1147   Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
  1142   Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
  1148  #> PureThy.add_defs false [((@{binding "foo_def"}, 
  1143  #> PureThy.add_defs false [((@{binding "foo_def"}, 
  1149        Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 
  1144        Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 
  1150  #> snd
  1145  #> snd
  1155   apply(simp add: foo_def)
  1150   apply(simp add: foo_def)
  1156   done
  1151   done
  1157 
  1152 
  1158 thm foo_def
  1153 thm foo_def
  1159 *)
  1154 *)
  1160 (*>*)
  1155 
  1161 
  1156 
  1162 section {* Pretty-Printing\label{sec:pretty} *}
  1157 section {* Pretty-Printing\label{sec:pretty} *}
  1163 
  1158 
  1164 text {*
  1159 text {*
  1165   So far we printed out only plain strings without any formatting except for
  1160   So far we printed out only plain strings without any formatting except for
  1166   occasional explicit line breaks using @{text [quotes] "\\n"}. This is
  1161   occasional explicit line breaks using @{text [quotes] "\\n"}. This is
  1167   sufficient for ``quick-and-dirty'' printouts. For something more
  1162   sufficient for ``quick-and-dirty'' printouts. For something more
  1168   sophisticated, Isabelle includes an infrastructure for properly formatting text.
  1163   sophisticated, Isabelle includes an infrastructure for properly formatting
  1169   This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
  1164   text. Most of its functions do not operate on @{ML_type string}s, but on
  1170   its functions do not operate on @{ML_type string}s, but on instances of the
  1165   instances of the pretty type:
  1171   type:
       
  1172 
  1166 
  1173   @{ML_type_ind [display, gray] "Pretty.T"}
  1167   @{ML_type_ind [display, gray] "Pretty.T"}
  1174 
  1168 
  1175   The function @{ML str in Pretty} transforms a (plain) string into such a pretty 
  1169   The function @{ML str in Pretty} transforms a (plain) string into such a pretty 
  1176   type. For example
  1170   type. For example
  1215 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
  1209 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
  1216 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
  1210 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
  1217 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
  1211 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
  1218 oooooooooooooobaaaaaaaaaaaar"}
  1212 oooooooooooooobaaaaaaaaaaaar"}
  1219 
  1213 
  1220   We obtain the same if we just use
  1214   We obtain the same if we just use the function @{ML pprint}.
  1221 
  1215 
  1222 @{ML_response_fake [display,gray]
  1216 @{ML_response_fake [display,gray]
  1223 "pprint (Pretty.str test_str)"
  1217 "pprint (Pretty.str test_str)"
  1224 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
  1218 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
  1225 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
  1219 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
  1226 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
  1220 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
  1227 oooooooooooooobaaaaaaaaaaaar"}
  1221 oooooooooooooobaaaaaaaaaaaar"}
  1228 
  1222 
  1229   However by using pretty types you have the ability to indicate a possible
  1223   However by using pretty types you have the ability to indicate possible
  1230   line break for example at each space. You can achieve this with the function
  1224   linebreaks for example at each whitespace. You can achieve this with the
  1231   @{ML_ind  breaks in Pretty}, which expects a list of pretty types and inserts a
  1225   function @{ML_ind breaks in Pretty}, which expects a list of pretty types
  1232   possible line break in between every two elements in this list. To print
  1226   and inserts a possible line break in between every two elements in this
  1233   this list of pretty types as a single string, we concatenate them 
  1227   list. To print this list of pretty types as a single string, we concatenate
  1234   with the function @{ML_ind  blk in Pretty} as follows:
  1228   them with the function @{ML_ind blk in Pretty} as follows:
  1235 
       
  1236 
  1229 
  1237 @{ML_response_fake [display,gray]
  1230 @{ML_response_fake [display,gray]
  1238 "let
  1231 "let
  1239   val ptrs = map Pretty.str (space_explode \" \" test_str)
  1232   val ptrs = map Pretty.str (space_explode \" \" test_str)
  1240 in
  1233 in
  1306 "{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
  1299 "{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
  1307   100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
  1300   100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
  1308   100016, 100017, 100018, 100019, 100020}"}
  1301   100016, 100017, 100018, 100019, 100020}"}
  1309 
  1302 
  1310   As can be seen, this function prints out the ``set'' so that starting 
  1303   As can be seen, this function prints out the ``set'' so that starting 
  1311   from the second, each new line as an indentation of 2.
  1304   from the second, each new line has an indentation of 2.
  1312   
  1305   
  1313   If you print out something that goes beyond the capabilities of the
  1306   If you print out something that goes beyond the capabilities of the
  1314   standard functions, you can do relatively easily the formatting
  1307   standard functions, you can do relatively easily the formatting
  1315   yourself. Assume you want to print out a list of items where like in ``English''
  1308   yourself. Assume you want to print out a list of items where like in ``English''
  1316   the last two items are separated by @{text [quotes] "and"}. For this you can
  1309   the last two items are separated by @{text [quotes] "and"}. For this you can
  1336   can occur. We do the same after the @{text [quotes] "and"}. This gives you
  1329   can occur. We do the same after the @{text [quotes] "and"}. This gives you
  1337   for example
  1330   for example
  1338 
  1331 
  1339 @{ML_response_fake [display,gray]
  1332 @{ML_response_fake [display,gray]
  1340 "let
  1333 "let
  1341   val ptrs = map (Pretty.str o string_of_int) (1 upto 22)
  1334   val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
  1342 in
  1335   val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)
  1343   pprint (Pretty.blk (0, and_list ptrs))
  1336 in
       
  1337   pprint (Pretty.blk (0, and_list ptrs1));
       
  1338   pprint (Pretty.blk (0, and_list ptrs2))
  1344 end"
  1339 end"
  1345 "1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
  1340 "1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
  1346 and 22"}
  1341 and 22
       
  1342 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
       
  1343 28"}
  1347 
  1344 
  1348   Next we like to pretty-print a term and its type. For this we use the
  1345   Next we like to pretty-print a term and its type. For this we use the
  1349   function @{text "tell_type"}.
  1346   function @{text "tell_type"}.
  1350 *}
  1347 *}
  1351 
  1348 
  1366   using the functions @{ML_ind  pretty_term in Syntax} and @{ML_ind 
  1363   using the functions @{ML_ind  pretty_term in Syntax} and @{ML_ind 
  1367   pretty_typ in Syntax}. We also use the function @{ML_ind quote in
  1364   pretty_typ in Syntax}. We also use the function @{ML_ind quote in
  1368   Pretty} in order to enclose the term and type inside quotation marks. In
  1365   Pretty} in order to enclose the term and type inside quotation marks. In
  1369   Line 9 we add a period right after the type without the possibility of a
  1366   Line 9 we add a period right after the type without the possibility of a
  1370   line break, because we do not want that a line break occurs there.
  1367   line break, because we do not want that a line break occurs there.
  1371 
       
  1372 
       
  1373   Now you can write
  1368   Now you can write
  1374 
  1369 
  1375   @{ML_response_fake [display,gray]
  1370   @{ML_response_fake [display,gray]
  1376   "tell_type @{context} @{term \"min (Suc 0)\"}"
  1371   "tell_type @{context} @{term \"min (Suc 0)\"}"
  1377   "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
  1372   "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
  1382   @{ML_response_fake [display,gray]
  1377   @{ML_response_fake [display,gray]
  1383   "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
  1378   "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
  1384   "The term \"op = (op = (op = (op = (op = op =))))\" has type 
  1379   "The term \"op = (op = (op = (op = (op = op =))))\" has type 
  1385 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
  1380 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
  1386 
  1381 
  1387 
  1382   The function @{ML_ind big_list in Pretty} helps with printing long lists.
  1388   FIXME: TBD below
  1383   It is used for example in the command \isacommand{print\_theorems}. An
  1389 *}
  1384   example is as follows.
  1390 
  1385 
  1391 ML {* pprint (Pretty.big_list "header"  (map (Pretty.str o string_of_int) (4 upto 10))) *}
  1386   @{ML_response_fake [display,gray]
  1392 
  1387   "let
  1393 text {*
  1388   val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
  1394 chunks inserts forced breaks (unlike blk where you have to do this yourself)
  1389 in
  1395 *}
  1390   pprint (Pretty.big_list \"header\" pstrs)
  1396 
  1391 end"
  1397 ML {* (Pretty.chunks [Pretty.str "a", Pretty.str "b"], 
  1392   "header
  1398        Pretty.blk (0, [Pretty.str "a", Pretty.str "b"])) *}
  1393   4
  1399 
  1394   5
       
  1395   6
       
  1396   7
       
  1397   8
       
  1398   9
       
  1399   10"}
       
  1400 
       
  1401   Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out 
       
  1402   a list of items, but automatically inserts forced breaks between each item.
       
  1403   Compare
       
  1404 
       
  1405   @{ML_response_fake [display,gray]
       
  1406   "let
       
  1407   val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
       
  1408 in
       
  1409   pprint (Pretty.blk (0, a_and_b));
       
  1410   pprint (Pretty.chunks a_and_b)
       
  1411 end"
       
  1412 "ab
       
  1413 a
       
  1414 b"}
       
  1415   
       
  1416   \footnote{\bf What happens with printing big formulae?}
       
  1417 
       
  1418   
       
  1419 
       
  1420   \begin{readmore}
       
  1421   The general infrastructure for pretty-printing is implemented in the file
       
  1422   @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
       
  1423   contains pretty-printing functions for terms, types, theorems and so on.
       
  1424   
       
  1425   @{ML_file "Pure/General/markup.ML"}
       
  1426   \end{readmore}
       
  1427 *}
       
  1428 
       
  1429 (*
       
  1430 text {*
       
  1431   printing into the goal buffer as part of the proof state
       
  1432 *}
       
  1433 
       
  1434 text {* writing into the goal buffer *}
       
  1435 
       
  1436 ML {* fun my_hook interactive state =
       
  1437          (interactive ? Proof.goal_message (fn () => Pretty.str  
       
  1438 "foo")) state
       
  1439 *}
       
  1440 
       
  1441 setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
       
  1442 
       
  1443 lemma "False"
       
  1444 oops
       
  1445 *)
       
  1446 
       
  1447 (*
  1400 ML {*
  1448 ML {*
  1401 fun setmp_show_all_types f =
  1449 fun setmp_show_all_types f =
  1402    setmp show_all_types
  1450    setmp show_all_types
  1403          (! show_types orelse ! show_sorts orelse ! show_all_types) f;
  1451          (! show_types orelse ! show_sorts orelse ! show_all_types) f;
  1404 
  1452 
  1407 val t2 = @{term "Suc y"};
  1455 val t2 = @{term "Suc y"};
  1408 val pty =        Pretty.block (Pretty.breaks
  1456 val pty =        Pretty.block (Pretty.breaks
  1409              [(setmp show_question_marks false o setmp_show_all_types)
  1457              [(setmp show_question_marks false o setmp_show_all_types)
  1410                   (Syntax.pretty_term ctxt) t1,
  1458                   (Syntax.pretty_term ctxt) t1,
  1411               Pretty.str "=", Syntax.pretty_term ctxt t2]);
  1459               Pretty.str "=", Syntax.pretty_term ctxt t2]);
  1412 pty |> Pretty.string_of |> priority
  1460 pty |> Pretty.string_of  
  1413 *}
  1461 *}
  1414 
  1462 
  1415 text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely  *}
  1463 text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely  *}
  1416 
  1464 
  1417 
  1465 
  1418 ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
  1466 ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
  1419 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
  1467 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
  1420 
  1468 *)
  1421 
       
  1422 ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
       
  1423 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
       
  1424 
       
  1425 text {*
       
  1426   Still to be done:
       
  1427 
       
  1428   What happens with big formulae?
       
  1429 
       
  1430   \begin{readmore}
       
  1431   The general infrastructure for pretty-printing is implemented in the file
       
  1432   @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
       
  1433   contains pretty-printing functions for terms, types, theorems and so on.
       
  1434   
       
  1435   @{ML_file "Pure/General/markup.ML"}
       
  1436   \end{readmore}
       
  1437 *}
       
  1438 
       
  1439 text {*
       
  1440   printing into the goal buffer as part of the proof state
       
  1441 *}
       
  1442 
       
  1443 
       
  1444 ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
       
  1445 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
       
  1446 
       
  1447 text {* writing into the goal buffer *}
       
  1448 
       
  1449 ML {* fun my_hook interactive state =
       
  1450          (interactive ? Proof.goal_message (fn () => Pretty.str  
       
  1451 "foo")) state
       
  1452 *}
       
  1453 
       
  1454 setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
       
  1455 
       
  1456 lemma "False"
       
  1457 oops
       
  1458 
  1469 
  1459 
  1470 
  1460 section {* Misc (TBD) *}
  1471 section {* Misc (TBD) *}
  1461 
  1472 
  1462 ML {*Datatype.get_info @{theory} "List.list"*}
  1473 ML {*Datatype.get_info @{theory} "List.list"*}