doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex
changeset 28714 1992553cccfe
parent 28636 d5342d4c7360
child 28727 185110a4b97a
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Fri Oct 31 10:39:04 2008 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Mon Nov 03 14:15:25 2008 +0100
     1.3 @@ -151,33 +151,33 @@
     1.4  \begin{isamarkuptext}%
     1.5  \isaverbatim%
     1.6  \noindent%
     1.7 -\verb|structure Example = |\newline%
     1.8 -\verb|struct|\newline%
     1.9 -\newline%
    1.10 -\verb|fun foldl f a [] = a|\newline%
    1.11 -\verb|  |\verb,|,\verb| foldl f a (x :: xs) = foldl f (f a x) xs;|\newline%
    1.12 -\newline%
    1.13 -\verb|fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;|\newline%
    1.14 -\newline%
    1.15 -\verb|fun list_case f1 f2 (a :: lista) = f2 a lista|\newline%
    1.16 -\verb|  |\verb,|,\verb| list_case f1 f2 [] = f1;|\newline%
    1.17 -\newline%
    1.18 -\verb|datatype 'a queue = Queue of 'a list * 'a list;|\newline%
    1.19 -\newline%
    1.20 -\verb|val empty : 'a queue = Queue ([], []);|\newline%
    1.21 -\newline%
    1.22 -\verb|fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))|\newline%
    1.23 -\verb|  |\verb,|,\verb| dequeue (Queue (xs, y :: ys)) = (SOME y, Queue (xs, ys))|\newline%
    1.24 -\verb|  |\verb,|,\verb| dequeue (Queue (v :: va, [])) =|\newline%
    1.25 -\verb|    let|\newline%
    1.26 -\verb|      val y :: ys = rev (v :: va);|\newline%
    1.27 -\verb|    in|\newline%
    1.28 -\verb|      (SOME y, Queue ([], ys))|\newline%
    1.29 -\verb|    end;|\newline%
    1.30 -\newline%
    1.31 -\verb|fun enqueue x (Queue (xs, ys)) = Queue (x :: xs, ys);|\newline%
    1.32 -\newline%
    1.33 -\verb|end; (*struct Example*)|%
    1.34 +\hspace*{0pt}structure Example = \\
    1.35 +\hspace*{0pt}struct\\
    1.36 +\hspace*{0pt}\\
    1.37 +\hspace*{0pt}fun foldl f a [] = a\\
    1.38 +\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
    1.39 +\hspace*{0pt}\\
    1.40 +\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
    1.41 +\hspace*{0pt}\\
    1.42 +\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\
    1.43 +\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\
    1.44 +\hspace*{0pt}\\
    1.45 +\hspace*{0pt}datatype 'a queue = Queue of 'a list * 'a list;\\
    1.46 +\hspace*{0pt}\\
    1.47 +\hspace*{0pt}val empty :~'a queue = Queue ([], []);\\
    1.48 +\hspace*{0pt}\\
    1.49 +\hspace*{0pt}fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))\\
    1.50 +\hspace*{0pt} ~| dequeue (Queue (xs, y ::~ys)) = (SOME y, Queue (xs, ys))\\
    1.51 +\hspace*{0pt} ~| dequeue (Queue (v ::~va, [])) =\\
    1.52 +\hspace*{0pt} ~~~let\\
    1.53 +\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
    1.54 +\hspace*{0pt} ~~~in\\
    1.55 +\hspace*{0pt} ~~~~~(SOME y, Queue ([], ys))\\
    1.56 +\hspace*{0pt} ~~~end;\\
    1.57 +\hspace*{0pt}\\
    1.58 +\hspace*{0pt}fun enqueue x (Queue (xs, ys)) = Queue (x ::~xs, ys);\\
    1.59 +\hspace*{0pt}\\
    1.60 +\hspace*{0pt}end; (*struct Example*)%
    1.61  \end{isamarkuptext}%
    1.62  \isamarkuptrue%
    1.63  %
    1.64 @@ -230,37 +230,37 @@
    1.65  \begin{isamarkuptext}%
    1.66  \isaverbatim%
    1.67  \noindent%
    1.68 -\verb|module Example where {|\newline%
    1.69 -\newline%
    1.70 -\newline%
    1.71 -\verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline%
    1.72 -\verb|foldla f a [] = a;|\newline%
    1.73 -\verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline%
    1.74 -\newline%
    1.75 -\verb|rev :: forall a. [a] -> [a];|\newline%
    1.76 -\verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline%
    1.77 -\newline%
    1.78 -\verb|list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;|\newline%
    1.79 -\verb|list_case f1 f2 (a : list) = f2 a list;|\newline%
    1.80 -\verb|list_case f1 f2 [] = f1;|\newline%
    1.81 -\newline%
    1.82 -\verb|data Queue a = Queue [a] [a];|\newline%
    1.83 -\newline%
    1.84 -\verb|empty :: forall a. Queue a;|\newline%
    1.85 -\verb|empty = Queue [] [];|\newline%
    1.86 -\newline%
    1.87 -\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline%
    1.88 -\verb|dequeue (Queue [] []) = (Nothing, Queue [] []);|\newline%
    1.89 -\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline%
    1.90 -\verb|dequeue (Queue (v : va) []) =|\newline%
    1.91 -\verb|  let {|\newline%
    1.92 -\verb|    (y : ys) = rev (v : va);|\newline%
    1.93 -\verb|  } in (Just y, Queue [] ys);|\newline%
    1.94 -\newline%
    1.95 -\verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline%
    1.96 -\verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline%
    1.97 -\newline%
    1.98 -\verb|}|%
    1.99 +\hspace*{0pt}module Example where {\char123}\\
   1.100 +\hspace*{0pt}\\
   1.101 +\hspace*{0pt}\\
   1.102 +\hspace*{0pt}foldla ::~forall a b. (a -> b -> a) -> a -> [b] -> a;\\
   1.103 +\hspace*{0pt}foldla f a [] = a;\\
   1.104 +\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
   1.105 +\hspace*{0pt}\\
   1.106 +\hspace*{0pt}rev ::~forall a. [a] -> [a];\\
   1.107 +\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
   1.108 +\hspace*{0pt}\\
   1.109 +\hspace*{0pt}list{\char95}case ::~forall t a. t -> (a -> [a] -> t) -> [a] -> t;\\
   1.110 +\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
   1.111 +\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
   1.112 +\hspace*{0pt}\\
   1.113 +\hspace*{0pt}data Queue a = Queue [a] [a];\\
   1.114 +\hspace*{0pt}\\
   1.115 +\hspace*{0pt}empty ::~forall a. Queue a;\\
   1.116 +\hspace*{0pt}empty = Queue [] [];\\
   1.117 +\hspace*{0pt}\\
   1.118 +\hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
   1.119 +\hspace*{0pt}dequeue (Queue [] []) = (Nothing, Queue [] []);\\
   1.120 +\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
   1.121 +\hspace*{0pt}dequeue (Queue (v :~va) []) =\\
   1.122 +\hspace*{0pt} ~let {\char123}\\
   1.123 +\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
   1.124 +\hspace*{0pt} ~{\char125}~in (Just y, Queue [] ys);\\
   1.125 +\hspace*{0pt}\\
   1.126 +\hspace*{0pt}enqueue ::~forall a. a -> Queue a -> Queue a;\\
   1.127 +\hspace*{0pt}enqueue x (Queue xs ys) = Queue (x :~xs) ys;\\
   1.128 +\hspace*{0pt}\\
   1.129 +\hspace*{0pt}{\char125}%
   1.130  \end{isamarkuptext}%
   1.131  \isamarkuptrue%
   1.132  %