# HG changeset patch # User haftmann # Date 1233686236 -3600 # Node ID 32d00a2a6f28063cfe3efdcb0bce08f280a42dc2 # Parent 86cac1fab6130db30c885cb8140269c2b9359b37 added stub about datatype abstraction diff -r 86cac1fab613 -r 32d00a2a6f28 doc-src/IsarAdvanced/Codegen/Thy/Program.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Feb 03 19:37:00 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Feb 03 19:37:16 2009 +0100 @@ -48,7 +48,7 @@ setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}). Changing the default constructor set of datatypes is also - possible but rarely desired in practice. See \secref{sec:datatypes} for an example. + possible. See \secref{sec:datatypes} for an example. As told in \secref{sec:concept}, code generation is based on a structured collection of code theorems. @@ -75,7 +75,7 @@ from abstract algebra: *} -class %quote semigroup = type + +class %quote semigroup = fixes mult :: "'a \ 'a \ 'a" (infixl "\" 70) assumes assoc: "(x \ y) \ z = x \ (y \ z)" @@ -221,97 +221,99 @@ text {* Conceptually, any datatype is spanned by a set of - \emph{constructors} of type @{text "\ = \ \ \ \\<^isub>1 \ \\<^isub>n"} - where @{text "{\\<^isub>1, \, \\<^isub>n}"} is exactly the set of \emph{all} - type variables in @{text "\"}. The HOL datatype package - by default registers any new datatype in the table - of datatypes, which may be inspected using - the @{command print_codesetup} command. + \emph{constructors} of type @{text "\ = \ \ \ \\<^isub>1 \ \\<^isub>n"} where @{text + "{\\<^isub>1, \, \\<^isub>n}"} is exactly the set of \emph{all} type variables in + @{text "\"}. The HOL datatype package by default registers any new + datatype in the table of datatypes, which may be inspected using the + @{command print_codesetup} command. - In some cases, it may be convenient to alter or - extend this table; as an example, we will develop an alternative - representation of natural numbers as binary digits, whose - size does increase logarithmically with its value, not linear - \footnote{Indeed, the @{theory Efficient_Nat} theory (see \ref{eff_nat}) - does something similar}. First, the digit representation: + In some cases, it is appropriate to alter or extend this table. As + an example, we will develop an alternative representation of the + queue example given in \secref{sec:intro}. The amortised + representation is convenient for generating code but exposes its + \qt{implementation} details, which may be cumbersome when proving + theorems about it. Therefore, here a simple, straightforward + representation of queues: *} -definition %quote Dig0 :: "nat \ nat" where - "Dig0 n = 2 * n" +datatype %quote 'a queue = Queue "'a list" + +definition %quote empty :: "'a queue" where + "empty = Queue []" -definition %quote Dig1 :: "nat \ nat" where - "Dig1 n = Suc (2 * n)" +primrec %quote enqueue :: "'a \ 'a queue \ 'a queue" where + "enqueue x (Queue xs) = Queue (xs @ [x])" + +fun %quote dequeue :: "'a queue \ 'a option \ 'a queue" where + "dequeue (Queue []) = (None, Queue [])" + | "dequeue (Queue (x # xs)) = (Some x, Queue xs)" text {* - \noindent We will use these two \qt{digits} to represent natural numbers - in binary digits, e.g.: -*} - -lemma %quote 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))" - by (simp add: Dig0_def Dig1_def) - -text {* - \noindent Of course we also have to provide proper code equations for - the operations, e.g. @{term "op + \ nat \ nat \ nat"}: + \noindent This we can use directly for proving; for executing, + we provide an alternative characterisation: *} -lemma %quote plus_Dig [code]: - "0 + n = n" - "m + 0 = m" - "1 + Dig0 n = Dig1 n" - "Dig0 m + 1 = Dig1 m" - "1 + Dig1 n = Dig0 (n + 1)" - "Dig1 m + 1 = Dig0 (m + 1)" - "Dig0 m + Dig0 n = Dig0 (m + n)" - "Dig0 m + Dig1 n = Dig1 (m + n)" - "Dig1 m + Dig0 n = Dig1 (m + n)" - "Dig1 m + Dig1 n = Dig0 (m + n + 1)" - by (simp_all add: Dig0_def Dig1_def) +definition %quote AQueue :: "'a list \ 'a list \ 'a queue" where + "AQueue xs ys = Queue (ys @ rev xs)" + +code_datatype %quote AQueue + +text {* *} + +lemma %quote empty_AQueue [code]: + "empty = AQueue [] []" + unfolding AQueue_def empty_def by simp + +lemma %quote enqueue_AQueue [code]: + "enqueue x (AQueue xs ys) = AQueue (x # xs) ys" + unfolding AQueue_def by simp -text {* - \noindent We then instruct the code generator to view @{term "0\nat"}, - @{term "1\nat"}, @{term Dig0} and @{term Dig1} as - datatype constructors: -*} +lemma %quote dequeue_AQueue [code]: + "dequeue (AQueue xs []) = + (if xs = [] then (None, AQueue [] []) else dequeue (AQueue [] (rev xs)))" + "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)" + unfolding AQueue_def by simp_all + +text {* *} + +definition %quote aqueue_case [code inline]: + "aqueue_case = queue_case" -code_datatype %quote "0\nat" "1\nat" Dig0 Dig1 +lemma %quote case_AQueue1 [code]: + "queue_case f (AQueue xs ys) = f (ys @ rev xs)" + unfolding AQueue_def by simp + +lemma %quote case_AQueue2 [code]: + "aqueue_case f (AQueue xs ys) = f (ys @ rev xs)" + unfolding aqueue_case case_AQueue1 .. + +text {* *} + +text %quote {*@{code_stmts empty enqueue dequeue (SML)}*} text {* - \noindent For the former constructor @{term Suc}, we provide a code - equation and remove some parts of the default code generator setup - which are an obstacle here: -*} - -lemma %quote Suc_Dig [code]: - "Suc n = n + 1" - by simp - -declare %quote One_nat_def [code inline del] -declare %quote add_Suc_shift [code del] - -text {* - \noindent This yields the following code: -*} - -text %quote {*@{code_stmts "op + \ nat \ nat \ nat" (SML)}*} - -text {* - \noindent From this example, it can be easily glimpsed that using own constructor sets - is a little delicate since it changes the set of valid patterns for values - of that type. Without going into much detail, here some practical hints: + \noindent From this example, it can be glimpsed that using own + constructor sets is a little delicate since it changes the set of + valid patterns for values of that type. Without going into much + detail, here some practical hints: \begin{itemize} - \item When changing the constructor set for datatypes, take care to - provide an alternative for the @{text case} combinator (e.g.~by replacing - it using the preprocessor). - \item Values in the target language need not to be normalised -- different - values in the target language may represent the same value in the - logic (e.g. @{term "Dig1 0 = 1"}). - \item Usually, a good methodology to deal with the subtleties of pattern - matching is to see the type as an abstract type: provide a set - of operations which operate on the concrete representation of the type, - and derive further operations by combinations of these primitive ones, - without relying on a particular representation. + + \item When changing the constructor set for datatypes, take care + to provide an alternative for the @{text case} combinator + (e.g.~by replacing it using the preprocessor). + + \item Values in the target language need not to be normalised -- + different values in the target language may represent the same + value in the logic. + + \item Usually, a good methodology to deal with the subtleties of + pattern matching is to see the type as an abstract type: provide + a set of operations which operate on the concrete representation + of the type, and derive further operations by combinations of + these primitive ones, without relying on a particular + representation. + \end{itemize} *} diff -r 86cac1fab613 -r 32d00a2a6f28 doc-src/IsarAdvanced/Codegen/Thy/Setup.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Feb 03 19:37:00 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Feb 03 19:37:16 2009 +0100 @@ -5,7 +5,7 @@ ML {* no_document use_thys ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL", - "~~/src/HOL/ex/ReflectedFerrack"] *} + "~~/src/HOL/Reflection/Ferrack"] *} ML_val {* Code_Target.code_width := 74 *} diff -r 86cac1fab613 -r 32d00a2a6f28 src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Tue Feb 03 19:37:00 2009 +0100 +++ b/src/Tools/code/code_haskell.ML Tue Feb 03 19:37:16 2009 +0100 @@ -385,7 +385,7 @@ val imports = deps' |> map NameSpace.qualifier |> distinct (op =); - fun pr_import_include (name, _) = str ("import " ^ name ^ ";"); + fun pr_import_include (name, _) = str ("import qualified " ^ name ^ ";"); val pr_import_module = str o (if qualified then prefix "import qualified " else prefix "import ") o suffix ";";