diff -r ab9e09076462 -r cccb25ee1309 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sun May 17 16:22:27 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Mon May 18 05:21:40 2009 +0200 @@ -144,7 +144,7 @@ "Exception- ERROR \"foo\" raised At command \"ML\"."} - (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling}) + (FIXME Mention how to work with @{ML Toplevel.debug} and @{ML Toplevel.profiling}.) *} (* @@ -163,7 +163,8 @@ text {* Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} - or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, + or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing + them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform a term into a string is to use the function @{ML Syntax.string_of_term}. @@ -479,7 +480,7 @@ contains further information about combinators. \end{readmore} - (FIXME: say something abou calling conventions) + (FIXME: say something about calling conventions) *} @@ -552,8 +553,8 @@ Again, this way of referencing simpsets makes you independent from additions of lemmas to the simpset by the user that potentially cause loops. - On the ML-level of Isabelle, you often have to work with qualified names; - these are strings with some additional information, such as positional information + On the ML-level of Isabelle, you often have to work with qualified names. + These are strings with some additional information, such as positional information and qualifiers. Such qualified names can be generated with the antiquotation @{text "@{binding \}"}. @@ -562,7 +563,7 @@ "name"} An example where a binding is needed is the function @{ML define in - LocalTheory}. Below, this function is used to define the constant @{term + LocalTheory}. This function is below used to define the constant @{term "TrueConj"} as the conjunction @{term "True \ True"}. *} @@ -613,16 +614,10 @@ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} will show the term @{term "(a::nat) + b = c"}, but printed using the internal - representation corresponding to the datatype @{ML_type "term"}. Since Isabelle - uses Church-style terms, the datatype @{ML_type term} must be defined in - conjunction with types, that is the datatype @{ML_type typ}: + representation corresponding to the datatype @{ML_type "term"} defined as follows: *} -ML_val{*datatype typ = - Type of string * typ list -| TFree of string * sort -| TVar of indexname * sort -datatype term = +ML_val{*datatype term = Const of string * typ | Free of string * typ | Var of indexname * typ @@ -631,15 +626,15 @@ | $ of term * term *} text {* - The datatype for terms uses the usual de Bruijn index mechanism---where - bound variables are represented by the constructor @{ML Bound}. + Terms use the usual de Bruijn index mechanism---where + bound variables are represented by the constructor @{ML Bound}. For + example in @{ML_response_fake [display, gray] "@{term \"\x y. x y\"}" "Abs (\"x\", \"'a \ 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"} - The index in - @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip + the indices refer to the number of Abstractions (@{ML Abs}) that we need to skip until we hit the @{ML Abs} that binds the corresponding variable. Note that the names of bound variables are kept at abstractions for printing purposes, and so should be treated only as ``comments''. Application in Isabelle is @@ -647,13 +642,13 @@ Isabelle makes a distinction between \emph{free} variables (term-constructor @{ML Free}) and variables (term-constructor @{ML Var}). The latter correspond to the schematic - variables that show up with a question mark in front of them. Consider the following - two examples + variables that when printed show up with a question mark in front of them. Consider + the following two examples @{ML_response_fake [display, gray] "let val v1 = Var ((\"x\", 3), @{typ bool}) - val v2 = Var ((\"x1\",3), @{typ bool}) + val v2 = Var ((\"x1\", 3), @{typ bool}) in writeln (Syntax.string_of_term @{context} v1); writeln (Syntax.string_of_term @{context} v2) @@ -664,13 +659,13 @@ This is different from a free variable @{ML_response_fake [display, gray] - "@{term \"x\"}" + "writeln (Syntax.string_of_term @{context} (Free (\"x\", @{typ bool})))" "x"} When constructing terms, you are usually concerned with free variables (for example you cannot construct schematic variables using the antiquotation @{text "@{term \}"}). - If you deal with theorems, you have to observe the distinction. The same holds - for types. + If you deal with theorems, you have to observe the distinction. A similar + distinction holds for types (see below). \begin{readmore} Terms and types are described in detail in \isccite{sec:terms}. Their @@ -685,8 +680,14 @@ "Type unification failed: Occurs check!"} raises a typing error, while it perfectly ok to construct the term - - @{ML [display,gray] "Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})"} + + @{ML_response_fake [display,gray] +"let + val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat}) +in + writeln (Syntax.string_of_term @{context} omega) +end" + "x x"} with the raw ML-constructors. Sometimes the internal representation of terms can be surprisingly different @@ -731,6 +732,22 @@ @{ML_response_fake [display,gray] "@{typ \"bool \ nat\"}" "bool \ nat"} + Their definition is +*} + +ML_val{*datatype typ = + Type of string * typ list +| TFree of string * sort +| TVar of indexname * sort *} + +text {* + Like with terms, there is the distinction between free type + variables (term-constructor @{ML "TFree"} and schematic + type variables (term-constructor @{ML "TVar"}). A type constant, + like @{typ "int"} or @{typ bool}, are types with an empty list + of argument types. + + \begin{readmore} Types are described in detail in \isccite{sec:types}. Their definition and many useful operations are implemented @@ -944,6 +961,8 @@ @{ML_response [display,gray] "@{type_name \"list\"}" "\"List.list\""} + (FIXME: Explain the following better.) + Occasionally you have to calculate what the ``base'' name of a given constant is. For this you can use the function @{ML Sign.extern_const} or @{ML Long_Name.base_name}. For example: @@ -992,9 +1011,25 @@ "Const (\"op =\", \"int \ int \ bool\") $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} - (FIXME: a readmore about types) + If you want to obtain the list of free type-variables of a term, you + can use the function @{ML Term.add_tfrees} (similarly @{ML Term.add_tvars} + for the schematic type-variables). One would expect that such functions + take a term as input and return a list of types. But their type is actually + + @{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"} - (Explain @{ML Term.add_tvarsT} and @{ML Term.add_tfreesT}) + that is they take, besides a term, also a list of type-variables as input. + So in order to obtain the list of type-variables of a term you have to + call them as follows + + @{ML_response [gray,display] + "Term.add_tfrees @{term \"(a,b)\"} []" + "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"} + + The reason for this definition is that @{ML Term.add_tfrees} can + be easily folded over a list of terms. Similarly for all functions + named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}. + *}