# HG changeset patch # User Christian Urban # Date 1243674766 -7200 # Node ID ef1da1abee460637c09d9f37ff75300a1bb713d9 # Parent cb86bf5658e4cde001b7ea249e6cb528074ec6aa added infrastructure for index; antiquotations have now the options [index] and [indexc] diff -r cb86bf5658e4 -r ef1da1abee46 ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Fri May 29 12:15:48 2009 +0200 +++ b/ProgTutorial/Base.thy Sat May 30 11:12:46 2009 +0200 @@ -1,6 +1,7 @@ theory Base imports Main uses + "outputfn.ML" "chunks.ML" "antiquote_setup.ML" begin @@ -37,4 +38,5 @@ *} + end \ No newline at end of file diff -r cb86bf5658e4 -r ef1da1abee46 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Fri May 29 12:15:48 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Sat May 30 11:12:46 2009 +0200 @@ -4,6 +4,7 @@ chapter {* First Steps *} + text {* Isabelle programming is done in ML. Just like lemmas and proofs, ML-code in Isabelle is part of a theory. If you want to follow the code given in @@ -110,7 +111,7 @@ During development you might find it necessary to inspect some data in your code. This can be done in a ``quick-and-dirty'' fashion using - the function @{ML "writeln"}. For example + the function @{ML [indexc] "writeln"}. For example @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""} @@ -716,6 +717,7 @@ "x x"} with the raw ML-constructors. + Sometimes the internal representation of terms can be surprisingly different from what you see at the user-level, because the layers of parsing/type-checking/pretty printing can be quite elaborate. @@ -781,7 +783,7 @@ \end{readmore} *} -section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} +section {* Constructing Terms Manually\label{sec:terms_types_manually} *} text {* While antiquotations are very convenient for constructing terms, they can @@ -877,6 +879,16 @@ @{term \"(\x::nat. x)\"}" "Free (\"x\", \"nat\")"} + There are many convenient functions that construct specific HOL-terms. For + example @{ML "HOLogic.mk_eq"} constructs an equality out of two terms. + The types needed in this equality are calculated from the type of the + arguments. For example + +@{ML_response_fake [gray,display] + "writeln (Syntax.string_of_term @{context} + (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))" + "True = False"} + \begin{readmore} There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms @@ -897,7 +909,11 @@ in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the number representing their sum. \end{exercise} - +*} + +section {* Constants *} + +text {* There are a few subtle issues with constants. They usually crop up when pattern matching terms or types, or when constructing them. While it is perfectly ok to write the function @{text is_true} as follows @@ -1003,7 +1019,11 @@ Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; functions about signatures in @{ML_file "Pure/sign.ML"}. \end{readmore} - +*} + +section {* Constructing Types Manually *} + +text {* Although types of terms can often be inferred, there are many situations where you need to construct types manually, especially when defining constants. For example the function returning a function @@ -1018,6 +1038,13 @@ ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *} text {* + If you want to construct a function type with more than one argument + type, then you can use @{ML "--->"}. +*} + +ML{*fun make_fun_types tys ty = tys ---> ty *} + +text {* A handy function for manipulating terms is @{ML map_types}: it takes a function and applies it to every type in a term. You can, for example, change every @{typ nat} in a term into an @{typ int} using the function: @@ -1551,7 +1578,7 @@ @{text GenericDataFun}: *} -ML {*structure MyThmsData = GenericDataFun +ML{*structure MyThmsData = GenericDataFun (type T = thm list val empty = [] val extend = I diff -r cb86bf5658e4 -r ef1da1abee46 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Fri May 29 12:15:48 2009 +0200 +++ b/ProgTutorial/Tactical.thy Sat May 30 11:12:46 2009 +0200 @@ -694,7 +694,7 @@ quantified variable. So you really have to construct the pattern using the basic term-constructors. This is not necessary in other cases, because their type is always fixed to function types involving only the type @{typ - bool}. (See Section \ref{sec:terms_types_manually} about constructing terms + bool}. (See Section \ref{sec:terms_manually} about constructing terms manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. Consequently, @{ML select_tac} never fails. diff -r cb86bf5658e4 -r ef1da1abee46 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Fri May 29 12:15:48 2009 +0200 +++ b/ProgTutorial/antiquote_setup.ML Sat May 30 11:12:46 2009 +0200 @@ -40,7 +40,7 @@ #> string_explode ""; (* output function *) -fun output_fn txt = Chunks.output (map Pretty.str txt) +fun output_fn txt = OutputFN.output txt (* checks and prints open expressions *) fun output_ml {context = ctxt, ...} (txt, ovars) = diff -r cb86bf5658e4 -r ef1da1abee46 ProgTutorial/chunks.ML --- a/ProgTutorial/chunks.ML Fri May 29 12:15:48 2009 +0200 +++ b/ProgTutorial/chunks.ML Sat May 30 11:12:46 2009 +0200 @@ -2,39 +2,6 @@ structure Chunks = struct -(* rebuilding the output function from ThyOutput in order to *) -(* enable the options [gray, linenos] *) - -val gray = ref false; -val linenos = ref false - -fun output prts = - prts - |> (if ! ThyOutput.quotes then map Pretty.quote else I) - |> (if ! ThyOutput.display then - map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) - #> space_implode "\\isasep\\isanewline%\n" - #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) - #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) - #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" - else - map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) - #> space_implode "\\isasep\\isanewline%\n" - #> enclose "\\isa{" "}"); - - -fun boolean "" = true - | boolean "true" = true - | boolean "false" = false - | boolean s = error ("Bad boolean value: " ^ quote s); - -val _ = ThyOutput.add_options - [("gray", Library.setmp gray o boolean), - ("linenos", Library.setmp linenos o boolean)] - - - - (** theory data **) structure ChunkData = TheoryDataFun @@ -158,8 +125,7 @@ end) val txt = spc ^ implode (transform_cmts toks') in - txt |> split_lines |> - (map Pretty.str) |> output + txt |> split_lines |> OutputFN.output end; val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; diff -r cb86bf5658e4 -r ef1da1abee46 ProgTutorial/document/root.tex --- a/ProgTutorial/document/root.tex Fri May 29 12:15:48 2009 +0200 +++ b/ProgTutorial/document/root.tex Sat May 30 11:12:46 2009 +0200 @@ -1,4 +1,4 @@ -\documentclass[11pt,a4paper]{report} +\documentclass[11pt,a4paper]{book} \usepackage[latin1]{inputenc} \usepackage{amsmath,amsthm} \usepackage{isabelle} @@ -15,6 +15,7 @@ \usepackage{boxedminipage} \usepackage{mathpartir} \usepackage{flafter} +\usepackage{makeidx} \usepackage{pdfsetup} \urlstyle{rm} @@ -24,6 +25,14 @@ \isadroptag{theory} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% adding chapters explicitly to the table of content +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% indexing +\makeindex + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % For cross references to the other manuals: \usepackage{xr} \externaldocument[I-]{implementation} @@ -149,16 +158,24 @@ \end{tabular}} \maketitle + +% table of contents +\tocentry{\contentsname} \setcounter{tocdepth}{1} \tableofcontents % generated text of all theories \input{session} -\newpage +% bibliography +\tocentry{\bibname} \bibliographystyle{abbrv} \bibliography{root} +% index +\tocentry{\indexname} +\printindex + \end{document} %%% Local Variables: diff -r cb86bf5658e4 -r ef1da1abee46 ProgTutorial/outputfn.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ProgTutorial/outputfn.ML Sat May 30 11:12:46 2009 +0200 @@ -0,0 +1,79 @@ + +structure OutputFN = +struct + +(* rebuilding the output function from ThyOutput in order to *) +(* enable the options [gray, linenos, index] *) + +val gray = ref false +val linenos = ref false + +datatype entry = + No_Entry + | Code_Entry of string + | String_Entry of string + +val index = ref No_Entry + +fun string_entry s = prefix ("\\index{" ^ s ^ "}") +fun code_entry s = prefix ("\\index{" ^ s ^ "@{\\tt\\slshape{}" ^ s ^ "}}") + +fun get_word str = +let + fun only_letters [] = true + | only_letters (x::xs) = + if (Symbol.is_ascii_blank x) then false else only_letters xs +in + if (only_letters (Symbol.explode str)) then str + else error ("Underspecified index entry only for single words allowed! Error with " ^ str) +end + +fun index_entry entry txt = + case entry of + No_Entry => I + | String_Entry "" => string_entry (get_word (implode txt)) + | String_Entry s => string_entry s + | Code_Entry "" => code_entry (get_word (implode txt)) + | Code_Entry s => code_entry s + + +fun translate f = Symbol.explode #> map f #> implode; + +val clean_string = translate + (fn "_" => "\\_" + | c => c); + +fun output txt = +let + val prts = map Pretty.str txt +in + prts + |> (if ! ThyOutput.quotes then map Pretty.quote else I) + |> (if ! ThyOutput.display then + map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) + #> space_implode "\\isasep\\isanewline%\n" + #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) + #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) + #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" + #> index_entry (!index) txt + else + map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) + #> space_implode "\\isasep\\isanewline%\n" + #> enclose "\\isa{" "}" + #> index_entry (!index) txt) +end + + +fun boolean "" = true + | boolean "true" = true + | boolean "false" = false + | boolean s = error ("Bad boolean value: " ^ quote s); + +val _ = ThyOutput.add_options + [("gray", Library.setmp gray o boolean), + ("linenos", Library.setmp linenos o boolean), + ("index", Library.setmp index o String_Entry o clean_string), + ("indexc", Library.setmp index o Code_Entry o clean_string)] + + +end \ No newline at end of file diff -r cb86bf5658e4 -r ef1da1abee46 progtutorial.pdf Binary file progtutorial.pdf has changed