1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Jan 01 21:28:38 2009 +0100
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Jan 01 21:30:13 2009 +0100
1.3 @@ -87,10 +87,10 @@
1.4 \begin{isamarkuptext}%
1.5 \isatypewriter%
1.6 \noindent%
1.7 -\hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
1.8 -\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
1.9 +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
1.10 +\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y,~Queue xs ys);\\
1.11 \hspace*{0pt}dequeue (Queue xs []) =\\
1.12 -\hspace*{0pt} ~(if nulla xs then (Nothing, Queue [] [])\\
1.13 +\hspace*{0pt} ~(if nulla xs then (Nothing,~Queue [] [])\\
1.14 \hspace*{0pt} ~~~else dequeue (Queue [] (rev xs)));%
1.15 \end{isamarkuptext}%
1.16 \isamarkuptrue%
1.17 @@ -286,7 +286,7 @@
1.18 \hspace*{0pt} ~neutral ::~a;\\
1.19 \hspace*{0pt}{\char125};\\
1.20 \hspace*{0pt}\\
1.21 -\hspace*{0pt}pow ::~forall a. (Monoid a) => Nat -> a -> a;\\
1.22 +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
1.23 \hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
1.24 \hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
1.25 \hspace*{0pt}\\
1.26 @@ -346,7 +346,7 @@
1.27 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
1.28 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
1.29 \hspace*{0pt}\\
1.30 -\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup, neutral :~'a{\char125};\\
1.31 +\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
1.32 \hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\
1.33 \hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
1.34 \hspace*{0pt}\\
1.35 @@ -356,7 +356,7 @@
1.36 \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
1.37 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
1.38 \hspace*{0pt}\\
1.39 -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
1.40 +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\
1.41 \hspace*{0pt}\\
1.42 \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
1.43 \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
1.44 @@ -364,12 +364,12 @@
1.45 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
1.46 \hspace*{0pt}\\
1.47 \hspace*{0pt}val monoid{\char95}nat =\\
1.48 -\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat, neutral = neutral{\char95}nat{\char125}~:\\
1.49 +\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}~:\\
1.50 \hspace*{0pt} ~nat monoid;\\
1.51 \hspace*{0pt}\\
1.52 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
1.53 \hspace*{0pt}\\
1.54 -\hspace*{0pt}end; (*struct Example*)%
1.55 +\hspace*{0pt}end;~(*struct Example*)%
1.56 \end{isamarkuptext}%
1.57 \isamarkuptrue%
1.58 %
1.59 @@ -675,7 +675,7 @@
1.60 \hspace*{0pt} ~| plus{\char95}nat m Zero{\char95}nat = m\\
1.61 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
1.62 \hspace*{0pt}\\
1.63 -\hspace*{0pt}end; (*struct Example*)%
1.64 +\hspace*{0pt}end;~(*struct Example*)%
1.65 \end{isamarkuptext}%
1.66 \isamarkuptrue%
1.67 %
1.68 @@ -794,7 +794,7 @@
1.69 \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
1.70 \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
1.71 \hspace*{0pt}\\
1.72 -\hspace*{0pt}end; (*struct Example*)%
1.73 +\hspace*{0pt}end;~(*struct Example*)%
1.74 \end{isamarkuptext}%
1.75 \isamarkuptrue%
1.76 %
1.77 @@ -918,7 +918,7 @@
1.78 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
1.79 \hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
1.80 \hspace*{0pt}\\
1.81 -\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool, less :~'a -> 'a -> bool{\char125};\\
1.82 +\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool,~less :~'a -> 'a -> bool{\char125};\\
1.83 \hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\
1.84 \hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\
1.85 \hspace*{0pt}\\
1.86 @@ -930,16 +930,16 @@
1.87 \hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\
1.88 \hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\
1.89 \hspace*{0pt}\\
1.90 -\hspace*{0pt}fun less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\
1.91 +\hspace*{0pt}fun less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\
1.92 \hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
1.93 \hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\
1.94 \hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\
1.95 -\hspace*{0pt} ~| less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\
1.96 +\hspace*{0pt} ~| less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\
1.97 \hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
1.98 \hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\
1.99 \hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\
1.100 \hspace*{0pt}\\
1.101 -\hspace*{0pt}end; (*struct Example*)%
1.102 +\hspace*{0pt}end;~(*struct Example*)%
1.103 \end{isamarkuptext}%
1.104 \isamarkuptrue%
1.105 %
1.106 @@ -1052,10 +1052,10 @@
1.107 \hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\
1.108 \hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\
1.109 \hspace*{0pt}\\
1.110 -\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =\\
1.111 +\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\
1.112 \hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\
1.113 \hspace*{0pt}\\
1.114 -\hspace*{0pt}end; (*struct Example*)%
1.115 +\hspace*{0pt}end;~(*struct Example*)%
1.116 \end{isamarkuptext}%
1.117 \isamarkuptrue%
1.118 %
1.119 @@ -1108,12 +1108,12 @@
1.120 \begin{isamarkuptext}%
1.121 \isatypewriter%
1.122 \noindent%
1.123 -\hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\
1.124 -\hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\
1.125 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
1.126 +\hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y,~Queue xs ys);\\
1.127 \hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\
1.128 \hspace*{0pt} ~let {\char123}\\
1.129 \hspace*{0pt} ~~~(y :~ys) = rev xs;\\
1.130 -\hspace*{0pt} ~{\char125}~in (y, Queue [] ys);%
1.131 +\hspace*{0pt} ~{\char125}~in (y,~Queue [] ys);%
1.132 \end{isamarkuptext}%
1.133 \isamarkuptrue%
1.134 %
1.135 @@ -1204,13 +1204,13 @@
1.136 \begin{isamarkuptext}%
1.137 \isatypewriter%
1.138 \noindent%
1.139 -\hspace*{0pt}empty{\char95}queue ::~forall a. a;\\
1.140 +\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
1.141 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
1.142 \hspace*{0pt}\\
1.143 -\hspace*{0pt}strict{\char95}dequeue' ::~forall a. Queue a -> (a, Queue a);\\
1.144 +\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
1.145 \hspace*{0pt}strict{\char95}dequeue' (Queue xs []) =\\
1.146 \hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue' (Queue [] (rev xs)));\\
1.147 -\hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y, Queue xs ys);%
1.148 +\hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y,~Queue xs ys);%
1.149 \end{isamarkuptext}%
1.150 \isamarkuptrue%
1.151 %