1.1 --- a/doc-src/Classes/Thy/document/Classes.tex Tue Sep 07 14:11:05 2010 +0200
1.2 +++ b/doc-src/Classes/Thy/document/Classes.tex Tue Sep 07 17:36:33 2010 +0200
1.3 @@ -1134,65 +1134,64 @@
1.4 \noindent%
1.5 \hspace*{0pt}module Example where {\char123}\\
1.6 \hspace*{0pt}\\
1.7 -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\
1.8 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
1.9 \hspace*{0pt}\\
1.10 -\hspace*{0pt}nat{\char95}aux ::~Integer -> Example.Nat -> Example.Nat;\\
1.11 -\hspace*{0pt}nat{\char95}aux i n =\\
1.12 -\hspace*{0pt} ~(if i <= 0 then n else Example.nat{\char95}aux (i - 1) (Example.Suc n));\\
1.13 +\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
1.14 +\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
1.15 \hspace*{0pt}\\
1.16 -\hspace*{0pt}nat ::~Integer -> Example.Nat;\\
1.17 -\hspace*{0pt}nat i = Example.nat{\char95}aux i Example.Zero{\char95}nat;\\
1.18 +\hspace*{0pt}nat ::~Integer -> Nat;\\
1.19 +\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
1.20 \hspace*{0pt}\\
1.21 \hspace*{0pt}class Semigroup a where {\char123}\\
1.22 \hspace*{0pt} ~mult ::~a -> a -> a;\\
1.23 \hspace*{0pt}{\char125};\\
1.24 \hspace*{0pt}\\
1.25 -\hspace*{0pt}class (Example.Semigroup a) => Monoidl a where {\char123}\\
1.26 +\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
1.27 \hspace*{0pt} ~neutral ::~a;\\
1.28 \hspace*{0pt}{\char125};\\
1.29 \hspace*{0pt}\\
1.30 -\hspace*{0pt}class (Example.Monoidl a) => Monoid a where {\char123}\\
1.31 +\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
1.32 \hspace*{0pt}{\char125};\\
1.33 \hspace*{0pt}\\
1.34 -\hspace*{0pt}class (Example.Monoid a) => Group a where {\char123}\\
1.35 +\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
1.36 \hspace*{0pt} ~inverse ::~a -> a;\\
1.37 \hspace*{0pt}{\char125};\\
1.38 \hspace*{0pt}\\
1.39 +\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
1.40 +\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
1.41 +\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
1.42 +\hspace*{0pt}\\
1.43 +\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
1.44 +\hspace*{0pt}pow{\char95}int k x =\\
1.45 +\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
1.46 +\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
1.47 +\hspace*{0pt}\\
1.48 \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
1.49 \hspace*{0pt}mult{\char95}int i j = i + j;\\
1.50 \hspace*{0pt}\\
1.51 +\hspace*{0pt}instance Semigroup Integer where {\char123}\\
1.52 +\hspace*{0pt} ~mult = mult{\char95}int;\\
1.53 +\hspace*{0pt}{\char125};\\
1.54 +\hspace*{0pt}\\
1.55 \hspace*{0pt}neutral{\char95}int ::~Integer;\\
1.56 \hspace*{0pt}neutral{\char95}int = 0;\\
1.57 \hspace*{0pt}\\
1.58 +\hspace*{0pt}instance Monoidl Integer where {\char123}\\
1.59 +\hspace*{0pt} ~neutral = neutral{\char95}int;\\
1.60 +\hspace*{0pt}{\char125};\\
1.61 +\hspace*{0pt}\\
1.62 +\hspace*{0pt}instance Monoid Integer where {\char123}\\
1.63 +\hspace*{0pt}{\char125};\\
1.64 +\hspace*{0pt}\\
1.65 \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
1.66 \hspace*{0pt}inverse{\char95}int i = negate i;\\
1.67 \hspace*{0pt}\\
1.68 -\hspace*{0pt}instance Example.Semigroup Integer where {\char123}\\
1.69 -\hspace*{0pt} ~mult = Example.mult{\char95}int;\\
1.70 +\hspace*{0pt}instance Group Integer where {\char123}\\
1.71 +\hspace*{0pt} ~inverse = inverse{\char95}int;\\
1.72 \hspace*{0pt}{\char125};\\
1.73 \hspace*{0pt}\\
1.74 -\hspace*{0pt}instance Example.Monoidl Integer where {\char123}\\
1.75 -\hspace*{0pt} ~neutral = Example.neutral{\char95}int;\\
1.76 -\hspace*{0pt}{\char125};\\
1.77 -\hspace*{0pt}\\
1.78 -\hspace*{0pt}instance Example.Monoid Integer where {\char123}\\
1.79 -\hspace*{0pt}{\char125};\\
1.80 -\hspace*{0pt}\\
1.81 -\hspace*{0pt}instance Example.Group Integer where {\char123}\\
1.82 -\hspace*{0pt} ~inverse = Example.inverse{\char95}int;\\
1.83 -\hspace*{0pt}{\char125};\\
1.84 -\hspace*{0pt}\\
1.85 -\hspace*{0pt}pow{\char95}nat ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\
1.86 -\hspace*{0pt}pow{\char95}nat Example.Zero{\char95}nat x = Example.neutral;\\
1.87 -\hspace*{0pt}pow{\char95}nat (Example.Suc n) x = Example.mult x (Example.pow{\char95}nat n x);\\
1.88 -\hspace*{0pt}\\
1.89 -\hspace*{0pt}pow{\char95}int ::~forall a.~(Example.Group a) => Integer -> a -> a;\\
1.90 -\hspace*{0pt}pow{\char95}int k x =\\
1.91 -\hspace*{0pt} ~(if 0 <= k then Example.pow{\char95}nat (Example.nat k) x\\
1.92 -\hspace*{0pt} ~~~else Example.inverse (Example.pow{\char95}nat (Example.nat (negate k)) x));\\
1.93 -\hspace*{0pt}\\
1.94 \hspace*{0pt}example ::~Integer;\\
1.95 -\hspace*{0pt}example = Example.pow{\char95}int 10 (-2);\\
1.96 +\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
1.97 \hspace*{0pt}\\
1.98 \hspace*{0pt}{\char125}%
1.99 \end{isamarkuptext}%
2.1 --- a/doc-src/Codegen/Thy/document/Foundations.tex Tue Sep 07 14:11:05 2010 +0200
2.2 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Tue Sep 07 17:36:33 2010 +0200
2.3 @@ -247,11 +247,11 @@
2.4 \begin{isamarkuptext}%
2.5 \isatypewriter%
2.6 \noindent%
2.7 -\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
2.8 -\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
2.9 -\hspace*{0pt}dequeue (Example.AQueue xs []) =\\
2.10 -\hspace*{0pt} ~(if null xs then (Nothing,~Example.AQueue [] [])\\
2.11 -\hspace*{0pt} ~~~else Example.dequeue (Example.AQueue [] (reverse xs)));%
2.12 +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
2.13 +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
2.14 +\hspace*{0pt}dequeue (AQueue xs []) =\\
2.15 +\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
2.16 +\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
2.17 \end{isamarkuptext}%
2.18 \isamarkuptrue%
2.19 %
2.20 @@ -444,12 +444,12 @@
2.21 \begin{isamarkuptext}%
2.22 \isatypewriter%
2.23 \noindent%
2.24 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
2.25 -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
2.26 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
2.27 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
2.28 \hspace*{0pt} ~let {\char123}\\
2.29 \hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
2.30 -\hspace*{0pt} ~{\char125}~in (y,~Example.AQueue [] ys);\\
2.31 -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);%
2.32 +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
2.33 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
2.34 \end{isamarkuptext}%
2.35 \isamarkuptrue%
2.36 %
2.37 @@ -538,11 +538,11 @@
2.38 \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
2.39 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
2.40 \hspace*{0pt}\\
2.41 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
2.42 -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);\\
2.43 -\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
2.44 -\hspace*{0pt} ~(if null xs then Example.empty{\char95}queue\\
2.45 -\hspace*{0pt} ~~~else Example.strict{\char95}dequeue (Example.AQueue [] (reverse xs)));%
2.46 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
2.47 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
2.48 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
2.49 +\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
2.50 +\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
2.51 \end{isamarkuptext}%
2.52 \isamarkuptrue%
2.53 %
3.1 --- a/doc-src/Codegen/Thy/document/Further.tex Tue Sep 07 14:11:05 2010 +0200
3.2 +++ b/doc-src/Codegen/Thy/document/Further.tex Tue Sep 07 17:36:33 2010 +0200
3.3 @@ -216,13 +216,13 @@
3.4 \begin{isamarkuptext}%
3.5 \isatypewriter%
3.6 \noindent%
3.7 -\hspace*{0pt}funpow ::~forall a.~Example.Nat -> (a -> a) -> a -> a;\\
3.8 -\hspace*{0pt}funpow Example.Zero{\char95}nat f = id;\\
3.9 -\hspace*{0pt}funpow (Example.Suc n) f = f .~Example.funpow n f;\\
3.10 +\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
3.11 +\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
3.12 +\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
3.13 \hspace*{0pt}\\
3.14 -\hspace*{0pt}funpows ::~forall a.~[Example.Nat] -> (a -> a) -> a -> a;\\
3.15 +\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
3.16 \hspace*{0pt}funpows [] = id;\\
3.17 -\hspace*{0pt}funpows (x :~xs) = Example.funpow x .~Example.funpows xs;%
3.18 +\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
3.19 \end{isamarkuptext}%
3.20 \isamarkuptrue%
3.21 %
4.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Sep 07 14:11:05 2010 +0200
4.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Sep 07 17:36:33 2010 +0200
4.3 @@ -231,19 +231,19 @@
4.4 \hspace*{0pt}\\
4.5 \hspace*{0pt}data Queue a = AQueue [a] [a];\\
4.6 \hspace*{0pt}\\
4.7 -\hspace*{0pt}empty ::~forall a.~Example.Queue a;\\
4.8 -\hspace*{0pt}empty = Example.AQueue [] [];\\
4.9 +\hspace*{0pt}empty ::~forall a.~Queue a;\\
4.10 +\hspace*{0pt}empty = AQueue [] [];\\
4.11 \hspace*{0pt}\\
4.12 -\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
4.13 -\hspace*{0pt}dequeue (Example.AQueue [] []) = (Nothing,~Example.AQueue [] []);\\
4.14 -\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
4.15 -\hspace*{0pt}dequeue (Example.AQueue (v :~va) []) =\\
4.16 +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
4.17 +\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
4.18 +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
4.19 +\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
4.20 \hspace*{0pt} ~let {\char123}\\
4.21 \hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\
4.22 -\hspace*{0pt} ~{\char125}~in (Just y,~Example.AQueue [] ys);\\
4.23 +\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
4.24 \hspace*{0pt}\\
4.25 -\hspace*{0pt}enqueue ::~forall a.~a -> Example.Queue a -> Example.Queue a;\\
4.26 -\hspace*{0pt}enqueue x (Example.AQueue xs ys) = Example.AQueue (x :~xs) ys;\\
4.27 +\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
4.28 +\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
4.29 \hspace*{0pt}\\
4.30 \hspace*{0pt}{\char125}%
4.31 \end{isamarkuptext}%
4.32 @@ -397,41 +397,41 @@
4.33 \noindent%
4.34 \hspace*{0pt}module Example where {\char123}\\
4.35 \hspace*{0pt}\\
4.36 -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\
4.37 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
4.38 \hspace*{0pt}\\
4.39 -\hspace*{0pt}plus{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\
4.40 -\hspace*{0pt}plus{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat m (Example.Suc n);\\
4.41 -\hspace*{0pt}plus{\char95}nat Example.Zero{\char95}nat n = n;\\
4.42 +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
4.43 +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
4.44 +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
4.45 \hspace*{0pt}\\
4.46 \hspace*{0pt}class Semigroup a where {\char123}\\
4.47 \hspace*{0pt} ~mult ::~a -> a -> a;\\
4.48 \hspace*{0pt}{\char125};\\
4.49 \hspace*{0pt}\\
4.50 -\hspace*{0pt}class (Example.Semigroup a) => Monoid a where {\char123}\\
4.51 +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
4.52 \hspace*{0pt} ~neutral ::~a;\\
4.53 \hspace*{0pt}{\char125};\\
4.54 \hspace*{0pt}\\
4.55 -\hspace*{0pt}pow ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\
4.56 -\hspace*{0pt}pow Example.Zero{\char95}nat a = Example.neutral;\\
4.57 -\hspace*{0pt}pow (Example.Suc n) a = Example.mult a (Example.pow n a);\\
4.58 +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
4.59 +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
4.60 +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
4.61 \hspace*{0pt}\\
4.62 -\hspace*{0pt}mult{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\
4.63 -\hspace*{0pt}mult{\char95}nat Example.Zero{\char95}nat n = Example.Zero{\char95}nat;\\
4.64 -\hspace*{0pt}mult{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat n (Example.mult{\char95}nat m n);\\
4.65 +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
4.66 +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
4.67 +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
4.68 \hspace*{0pt}\\
4.69 -\hspace*{0pt}neutral{\char95}nat ::~Example.Nat;\\
4.70 -\hspace*{0pt}neutral{\char95}nat = Example.Suc Example.Zero{\char95}nat;\\
4.71 -\hspace*{0pt}\\
4.72 -\hspace*{0pt}instance Example.Semigroup Example.Nat where {\char123}\\
4.73 -\hspace*{0pt} ~mult = Example.mult{\char95}nat;\\
4.74 +\hspace*{0pt}instance Semigroup Nat where {\char123}\\
4.75 +\hspace*{0pt} ~mult = mult{\char95}nat;\\
4.76 \hspace*{0pt}{\char125};\\
4.77 \hspace*{0pt}\\
4.78 -\hspace*{0pt}instance Example.Monoid Example.Nat where {\char123}\\
4.79 -\hspace*{0pt} ~neutral = Example.neutral{\char95}nat;\\
4.80 +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
4.81 +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
4.82 +\hspace*{0pt}\\
4.83 +\hspace*{0pt}instance Monoid Nat where {\char123}\\
4.84 +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
4.85 \hspace*{0pt}{\char125};\\
4.86 \hspace*{0pt}\\
4.87 -\hspace*{0pt}bexp ::~Example.Nat -> Example.Nat;\\
4.88 -\hspace*{0pt}bexp n = Example.pow n (Example.Suc (Example.Suc Example.Zero{\char95}nat));\\
4.89 +\hspace*{0pt}bexp ::~Nat -> Nat;\\
4.90 +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
4.91 \hspace*{0pt}\\
4.92 \hspace*{0pt}{\char125}%
4.93 \end{isamarkuptext}%
5.1 --- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Sep 07 14:11:05 2010 +0200
5.2 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Sep 07 17:36:33 2010 +0200
5.3 @@ -74,11 +74,10 @@
5.4 \begin{isamarkuptext}%
5.5 \isatypewriter%
5.6 \noindent%
5.7 -\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\
5.8 -\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;\\
5.9 -\hspace*{0pt}fib (Example.Suc Example.Zero{\char95}nat) = Example.Suc Example.Zero{\char95}nat;\\
5.10 -\hspace*{0pt}fib (Example.Suc (Example.Suc n)) =\\
5.11 -\hspace*{0pt} ~Example.plus{\char95}nat (Example.fib n) (Example.fib (Example.Suc n));%
5.12 +\hspace*{0pt}fib ::~Nat -> Nat;\\
5.13 +\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\
5.14 +\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\
5.15 +\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));%
5.16 \end{isamarkuptext}%
5.17 \isamarkuptrue%
5.18 %
5.19 @@ -173,17 +172,15 @@
5.20 \begin{isamarkuptext}%
5.21 \isatypewriter%
5.22 \noindent%
5.23 -\hspace*{0pt}fib{\char95}step ::~Example.Nat -> (Example.Nat,~Example.Nat);\\
5.24 -\hspace*{0pt}fib{\char95}step (Example.Suc n) =\\
5.25 -\hspace*{0pt} ~let {\char123}\\
5.26 -\hspace*{0pt} ~~~(m,~q) = Example.fib{\char95}step n;\\
5.27 -\hspace*{0pt} ~{\char125}~in (Example.plus{\char95}nat m q,~m);\\
5.28 -\hspace*{0pt}fib{\char95}step Example.Zero{\char95}nat =\\
5.29 -\hspace*{0pt} ~(Example.Suc Example.Zero{\char95}nat,~Example.Zero{\char95}nat);\\
5.30 +\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\
5.31 +\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\
5.32 +\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\
5.33 +\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\
5.34 +\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\
5.35 \hspace*{0pt}\\
5.36 -\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\
5.37 -\hspace*{0pt}fib (Example.Suc n) = fst (Example.fib{\char95}step n);\\
5.38 -\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;%
5.39 +\hspace*{0pt}fib ::~Nat -> Nat;\\
5.40 +\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\
5.41 +\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;%
5.42 \end{isamarkuptext}%
5.43 \isamarkuptrue%
5.44 %
5.45 @@ -593,30 +590,28 @@
5.46 \hspace*{0pt}\\
5.47 \hspace*{0pt}newtype Dlist a = Dlist [a];\\
5.48 \hspace*{0pt}\\
5.49 -\hspace*{0pt}empty ::~forall a.~Example.Dlist a;\\
5.50 -\hspace*{0pt}empty = Example.Dlist [];\\
5.51 +\hspace*{0pt}empty ::~forall a.~Dlist a;\\
5.52 +\hspace*{0pt}empty = Dlist [];\\
5.53 \hspace*{0pt}\\
5.54 \hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\
5.55 \hspace*{0pt}member [] y = False;\\
5.56 -\hspace*{0pt}member (x :~xs) y = x == y || Example.member xs y;\\
5.57 +\hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\
5.58 \hspace*{0pt}\\
5.59 -\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> [a] -> [a];\\
5.60 -\hspace*{0pt}inserta x xs = (if Example.member xs x then xs else x :~xs);\\
5.61 +\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> [a] -> [a];\\
5.62 +\hspace*{0pt}insert x xs = (if member xs x then xs else x :~xs);\\
5.63 \hspace*{0pt}\\
5.64 -\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Example.Dlist a -> [a];\\
5.65 -\hspace*{0pt}list{\char95}of{\char95}dlist (Example.Dlist x) = x;\\
5.66 +\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\
5.67 +\hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\
5.68 \hspace*{0pt}\\
5.69 -\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\
5.70 -\hspace*{0pt}insert x dxs =\\
5.71 -\hspace*{0pt} ~Example.Dlist (Example.inserta x (Example.list{\char95}of{\char95}dlist dxs));\\
5.72 +\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
5.73 +\hspace*{0pt}inserta x dxs = Dlist (insert x (list{\char95}of{\char95}dlist dxs));\\
5.74 \hspace*{0pt}\\
5.75 \hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\
5.76 \hspace*{0pt}remove1 x [] = [];\\
5.77 -\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~Example.remove1 x xs);\\
5.78 +\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\
5.79 \hspace*{0pt}\\
5.80 -\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\
5.81 -\hspace*{0pt}remove x dxs =\\
5.82 -\hspace*{0pt} ~Example.Dlist (Example.remove1 x (Example.list{\char95}of{\char95}dlist dxs));\\
5.83 +\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
5.84 +\hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\
5.85 \hspace*{0pt}\\
5.86 \hspace*{0pt}{\char125}%
5.87 \end{isamarkuptext}%
6.1 --- a/doc-src/Codegen/Thy/examples/Example.hs Tue Sep 07 14:11:05 2010 +0200
6.2 +++ b/doc-src/Codegen/Thy/examples/Example.hs Tue Sep 07 17:36:33 2010 +0200
6.3 @@ -4,18 +4,18 @@
6.4
6.5 data Queue a = AQueue [a] [a];
6.6
6.7 -empty :: forall a. Example.Queue a;
6.8 -empty = Example.AQueue [] [];
6.9 +empty :: forall a. Queue a;
6.10 +empty = AQueue [] [];
6.11
6.12 -dequeue :: forall a. Example.Queue a -> (Maybe a, Example.Queue a);
6.13 -dequeue (Example.AQueue [] []) = (Nothing, Example.AQueue [] []);
6.14 -dequeue (Example.AQueue xs (y : ys)) = (Just y, Example.AQueue xs ys);
6.15 -dequeue (Example.AQueue (v : va) []) =
6.16 +dequeue :: forall a. Queue a -> (Maybe a, Queue a);
6.17 +dequeue (AQueue [] []) = (Nothing, AQueue [] []);
6.18 +dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
6.19 +dequeue (AQueue (v : va) []) =
6.20 let {
6.21 (y : ys) = reverse (v : va);
6.22 - } in (Just y, Example.AQueue [] ys);
6.23 + } in (Just y, AQueue [] ys);
6.24
6.25 -enqueue :: forall a. a -> Example.Queue a -> Example.Queue a;
6.26 -enqueue x (Example.AQueue xs ys) = Example.AQueue (x : xs) ys;
6.27 +enqueue :: forall a. a -> Queue a -> Queue a;
6.28 +enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
6.29
6.30 }
7.1 --- a/src/Tools/Code/code_haskell.ML Tue Sep 07 14:11:05 2010 +0200
7.2 +++ b/src/Tools/Code/code_haskell.ML Tue Sep 07 17:36:33 2010 +0200
7.3 @@ -27,7 +27,6 @@
7.4 fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
7.5 reserved deresolve contr_classparam_typs deriving_show =
7.6 let
7.7 - val deresolve_base = Long_Name.base_name o deresolve;
7.8 fun class_name class = case class_syntax class
7.9 of NONE => deresolve class
7.10 | SOME class => class;
7.11 @@ -121,7 +120,7 @@
7.12 val tyvars = intro_vars (map fst vs) reserved;
7.13 fun print_err n =
7.14 semicolon (
7.15 - (str o deresolve_base) name
7.16 + (str o deresolve) name
7.17 :: map str (replicate n "_")
7.18 @ str "="
7.19 :: str "error"
7.20 @@ -138,7 +137,7 @@
7.21 (insert (op =)) ts []);
7.22 in
7.23 semicolon (
7.24 - (str o deresolve_base) name
7.25 + (str o deresolve) name
7.26 :: map (print_term tyvars some_thm vars BR) ts
7.27 @ str "="
7.28 @@ print_term tyvars some_thm vars NOBR t
7.29 @@ -147,7 +146,7 @@
7.30 in
7.31 Pretty.chunks (
7.32 semicolon [
7.33 - (str o suffix " ::" o deresolve_base) name,
7.34 + (str o suffix " ::" o deresolve) name,
7.35 print_typscheme tyvars (vs, ty)
7.36 ]
7.37 :: (case filter (snd o snd) raw_eqs
7.38 @@ -161,7 +160,7 @@
7.39 in
7.40 semicolon [
7.41 str "data",
7.42 - print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
7.43 + print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
7.44 ]
7.45 end
7.46 | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
7.47 @@ -170,9 +169,9 @@
7.48 in
7.49 semicolon (
7.50 str "newtype"
7.51 - :: print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
7.52 + :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
7.53 :: str "="
7.54 - :: (str o deresolve_base) co
7.55 + :: (str o deresolve) co
7.56 :: print_typ tyvars BR ty
7.57 :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
7.58 )
7.59 @@ -182,13 +181,13 @@
7.60 val tyvars = intro_vars (map fst vs) reserved;
7.61 fun print_co ((co, _), tys) =
7.62 concat (
7.63 - (str o deresolve_base) co
7.64 + (str o deresolve) co
7.65 :: map (print_typ tyvars BR) tys
7.66 )
7.67 in
7.68 semicolon (
7.69 str "data"
7.70 - :: print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
7.71 + :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
7.72 :: str "="
7.73 :: print_co co
7.74 :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
7.75 @@ -200,7 +199,7 @@
7.76 val tyvars = intro_vars [v] reserved;
7.77 fun print_classparam (classparam, ty) =
7.78 semicolon [
7.79 - (str o deresolve_base) classparam,
7.80 + (str o deresolve) classparam,
7.81 str "::",
7.82 print_typ tyvars NOBR ty
7.83 ]
7.84 @@ -209,7 +208,7 @@
7.85 Pretty.block [
7.86 str "class ",
7.87 Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
7.88 - str (deresolve_base name ^ " " ^ lookup_var tyvars v),
7.89 + str (deresolve name ^ " " ^ lookup_var tyvars v),
7.90 str " where {"
7.91 ],
7.92 str "};"
7.93 @@ -219,17 +218,17 @@
7.94 let
7.95 val tyvars = intro_vars (map fst vs) reserved;
7.96 fun requires_args classparam = case const_syntax classparam
7.97 - of NONE => 0
7.98 - | SOME (Code_Printer.Plain_const_syntax _) => 0
7.99 - | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
7.100 + of NONE => NONE
7.101 + | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
7.102 + | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
7.103 fun print_classparam_instance ((classparam, const), (thm, _)) =
7.104 case requires_args classparam
7.105 - of 0 => semicolon [
7.106 - (str o deresolve_base) classparam,
7.107 + of NONE => semicolon [
7.108 + (str o Long_Name.base_name o deresolve) classparam,
7.109 str "=",
7.110 print_app tyvars (SOME thm) reserved NOBR (const, [])
7.111 ]
7.112 - | k =>
7.113 + | SOME k =>
7.114 let
7.115 val (c, (_, tys)) = const;
7.116 val (vs, rhs) = (apfst o map) fst
7.117 @@ -261,82 +260,51 @@
7.118 end;
7.119 in print_stmt end;
7.120
7.121 -fun mk_name_module reserved module_prefix module_alias program =
7.122 +fun haskell_program_of_program labelled_name module_alias module_prefix reserved =
7.123 let
7.124 - fun mk_alias name = case module_alias name
7.125 - of SOME name' => name'
7.126 - | NONE => name
7.127 - |> Long_Name.explode
7.128 - |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
7.129 - |> Long_Name.implode;
7.130 - fun mk_prefix name = case module_prefix
7.131 - of SOME module_prefix => Long_Name.append module_prefix name
7.132 - | NONE => name;
7.133 - val tab =
7.134 - Symtab.empty
7.135 - |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
7.136 - o fst o Code_Namespace.dest_name o fst)
7.137 - program
7.138 - in the o Symtab.lookup tab end;
7.139 -
7.140 -fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
7.141 - let
7.142 - val reserved = Name.make_context reserved;
7.143 - val mk_name_module = mk_name_module reserved module_prefix module_alias program;
7.144 - fun add_stmt (name, (stmt, deps)) =
7.145 + fun namify_fun upper base (nsp_fun, nsp_typ) =
7.146 let
7.147 - val (module_name, base) = Code_Namespace.dest_name name;
7.148 - val module_name' = mk_name_module module_name;
7.149 - val mk_name_stmt = yield_singleton Name.variants;
7.150 - fun add_fun upper (nsp_fun, nsp_typ) =
7.151 - let
7.152 - val (base', nsp_fun') =
7.153 - mk_name_stmt (if upper then first_upper base else base) nsp_fun
7.154 - in (base', (nsp_fun', nsp_typ)) end;
7.155 - fun add_typ (nsp_fun, nsp_typ) =
7.156 - let
7.157 - val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
7.158 - in (base', (nsp_fun, nsp_typ')) end;
7.159 - val add_name = case stmt
7.160 - of Code_Thingol.Fun (_, (_, SOME _)) => pair base
7.161 - | Code_Thingol.Fun _ => add_fun false
7.162 - | Code_Thingol.Datatype _ => add_typ
7.163 - | Code_Thingol.Datatypecons _ => add_fun true
7.164 - | Code_Thingol.Class _ => add_typ
7.165 - | Code_Thingol.Classrel _ => pair base
7.166 - | Code_Thingol.Classparam _ => add_fun false
7.167 - | Code_Thingol.Classinst _ => pair base;
7.168 - fun add_stmt' base' = case stmt
7.169 - of Code_Thingol.Fun (_, (_, SOME _)) =>
7.170 - I
7.171 - | Code_Thingol.Datatypecons _ =>
7.172 - cons (name, (Long_Name.append module_name' base', NONE))
7.173 - | Code_Thingol.Classrel _ => I
7.174 - | Code_Thingol.Classparam _ =>
7.175 - cons (name, (Long_Name.append module_name' base', NONE))
7.176 - | _ => cons (name, (Long_Name.append module_name' base', SOME stmt));
7.177 - in
7.178 - Symtab.map_default (module_name', ([], ([], (reserved, reserved))))
7.179 - (apfst (fold (insert (op = : string * string -> bool)) deps))
7.180 - #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
7.181 - #-> (fn (base', names) =>
7.182 - (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
7.183 - (add_stmt' base' stmts, names)))
7.184 - end;
7.185 - val hs_program = fold add_stmt (AList.make (fn name =>
7.186 - (Graph.get_node program name, Graph.imm_succs program name))
7.187 - (Graph.strong_conn program |> flat)) Symtab.empty;
7.188 - fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
7.189 - o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Namespace.dest_name) name))) name
7.190 - handle Option => error ("Unknown statement name: " ^ labelled_name name);
7.191 - in (deresolver, hs_program) end;
7.192 + val (base', nsp_fun') = yield_singleton Name.variants
7.193 + (if upper then first_upper base else base) nsp_fun;
7.194 + in (base', (nsp_fun', nsp_typ)) end;
7.195 + fun namify_typ base (nsp_fun, nsp_typ) =
7.196 + let
7.197 + val (base', nsp_typ') = yield_singleton Name.variants
7.198 + (first_upper base) nsp_typ
7.199 + in (base', (nsp_fun, nsp_typ')) end;
7.200 + fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
7.201 + | namify_stmt (Code_Thingol.Fun _) = namify_fun false
7.202 + | namify_stmt (Code_Thingol.Datatype _) = namify_typ
7.203 + | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
7.204 + | namify_stmt (Code_Thingol.Class _) = namify_typ
7.205 + | namify_stmt (Code_Thingol.Classrel _) = pair
7.206 + | namify_stmt (Code_Thingol.Classparam _) = namify_fun false
7.207 + | namify_stmt (Code_Thingol.Classinst _) = pair;
7.208 + fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
7.209 + | select_stmt (Code_Thingol.Fun _) = true
7.210 + | select_stmt (Code_Thingol.Datatype _) = true
7.211 + | select_stmt (Code_Thingol.Datatypecons _) = false
7.212 + | select_stmt (Code_Thingol.Class _) = true
7.213 + | select_stmt (Code_Thingol.Classrel _) = false
7.214 + | select_stmt (Code_Thingol.Classparam _) = false
7.215 + | select_stmt (Code_Thingol.Classinst _) = true;
7.216 + in
7.217 + Code_Namespace.flat_program labelled_name
7.218 + { module_alias = module_alias, module_prefix = module_prefix,
7.219 + reserved = reserved, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
7.220 + modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
7.221 + end;
7.222
7.223 fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms,
7.224 includes, module_alias, class_syntax, tyco_syntax, const_syntax, program } =
7.225 let
7.226 +
7.227 + (* build program *)
7.228 val reserved = fold (insert (op =) o fst) includes reserved_syms;
7.229 - val (deresolver, hs_program) = haskell_program_of_program labelled_name
7.230 - module_prefix reserved module_alias program;
7.231 + val { deresolver, flat_program = haskell_program } = haskell_program_of_program
7.232 + labelled_name module_alias module_prefix (Name.make_context reserved) program;
7.233 +
7.234 + (* print statements *)
7.235 val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
7.236 fun deriving_show tyco =
7.237 let
7.238 @@ -351,62 +319,58 @@
7.239 andalso forall (deriv' tycos) tys
7.240 | deriv' _ (ITyVar _) = true
7.241 in deriv [] tyco end;
7.242 - val reserved = make_vars reserved;
7.243 - fun print_stmt qualified = print_haskell_stmt labelled_name
7.244 - class_syntax tyco_syntax const_syntax reserved
7.245 - (if qualified then deresolver else Long_Name.base_name o deresolver)
7.246 - contr_classparam_typs
7.247 + fun print_stmt deresolve = print_haskell_stmt labelled_name
7.248 + class_syntax tyco_syntax const_syntax (make_vars reserved)
7.249 + deresolve contr_classparam_typs
7.250 (if string_classes then deriving_show else K false);
7.251 - fun print_module name content =
7.252 - (name, Pretty.chunks2 [
7.253 - str ("module " ^ name ^ " where {"),
7.254 - content,
7.255 - str "}"
7.256 - ]);
7.257 - fun serialize_module (module_name', (deps, (stmts, _))) =
7.258 +
7.259 + (* print modules *)
7.260 + val import_includes_ps =
7.261 + map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes;
7.262 + fun print_module_frame module_name ps =
7.263 + (module_name, Pretty.chunks2 (
7.264 + str ("module " ^ module_name ^ " where {")
7.265 + :: ps
7.266 + @| str "}"
7.267 + ));
7.268 + fun print_module module_name (gr, imports) =
7.269 let
7.270 - val stmt_names = map fst stmts;
7.271 - val qualified = true;
7.272 - val imports = subtract (op =) stmt_names deps
7.273 - |> distinct (op =)
7.274 - |> map_filter (try deresolver)
7.275 - |> map Long_Name.qualifier
7.276 - |> distinct (op =);
7.277 - fun print_import_include (name, _) = str ("import qualified " ^ name ^ ";");
7.278 - fun print_import_module name = str ((if qualified
7.279 - then "import qualified "
7.280 - else "import ") ^ name ^ ";");
7.281 - val import_ps = map print_import_include includes @ map print_import_module imports
7.282 - val content = Pretty.chunks2 ((if null import_ps then [] else [Pretty.chunks import_ps])
7.283 - @ map_filter
7.284 - (fn (name, (_, SOME stmt)) => SOME (markup_stmt name (print_stmt qualified (name, stmt)))
7.285 - | (_, (_, NONE)) => NONE) stmts
7.286 - );
7.287 - in print_module module_name' content end;
7.288 - fun write_module width (SOME destination) (modlname, content) =
7.289 + val deresolve = deresolver module_name
7.290 + fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
7.291 + val import_ps = import_includes_ps @ map (print_import o fst) imports;
7.292 + fun print_stmt' gr name = case Graph.get_node gr name
7.293 + of (_, NONE) => NONE
7.294 + | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
7.295 + val body_ps = map_filter (print_stmt' gr) ((flat o rev o Graph.strong_conn) gr);
7.296 + in
7.297 + print_module_frame module_name
7.298 + ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
7.299 + end;
7.300 +
7.301 + (*serialization*)
7.302 + fun write_module width (SOME destination) (module_name, content) =
7.303 let
7.304 val _ = File.check destination;
7.305 - val filename = case modlname
7.306 - of "" => Path.explode "Main.hs"
7.307 - | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
7.308 - o Long_Name.explode) modlname;
7.309 - val pathname = Path.append destination filename;
7.310 - val _ = File.mkdir_leaf (Path.dir pathname);
7.311 - in File.write pathname
7.312 - ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
7.313 - ^ format [] width content)
7.314 + val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
7.315 + o separate "/" o Long_Name.explode) module_name;
7.316 + val _ = File.mkdir_leaf (Path.dir filepath);
7.317 + in
7.318 + (File.write filepath o format [] width o Pretty.chunks2)
7.319 + [str "{-# OPTIONS_GHC -fglasgow-exts #-}", content]
7.320 end
7.321 | write_module width NONE (_, content) = writeln (format [] width content);
7.322 in
7.323 Code_Target.serialization
7.324 (fn width => fn destination => K () o map (write_module width destination))
7.325 - (fn present => fn width => rpair (fn _ => error "no deresolving") o format present width o Pretty.chunks o map snd)
7.326 - (map (uncurry print_module) includes
7.327 - @ map serialize_module (Symtab.dest hs_program))
7.328 + (fn present => fn width => rpair (fn _ => error "no deresolving")
7.329 + o format present width o Pretty.chunks o map snd)
7.330 + (map (uncurry print_module_frame o apsnd single) includes
7.331 + @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
7.332 + ((flat o rev o Graph.strong_conn) haskell_program))
7.333 end;
7.334
7.335 val serializer : Code_Target.serializer =
7.336 - Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
7.337 + Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) ""
7.338 -- Scan.optional (Args.$$$ "string_classes" >> K true) false
7.339 >> (fn (module_prefix, string_classes) =>
7.340 serialize_haskell module_prefix string_classes));
8.1 --- a/src/Tools/Code/code_namespace.ML Tue Sep 07 14:11:05 2010 +0200
8.2 +++ b/src/Tools/Code/code_namespace.ML Tue Sep 07 17:36:33 2010 +0200
8.3 @@ -6,12 +6,20 @@
8.4
8.5 signature CODE_NAMESPACE =
8.6 sig
8.7 - val dest_name: string -> string * string
8.8 + type flat_program
8.9 + val flat_program: (string -> string) -> { module_alias: string -> string option,
8.10 + module_prefix: string, reserved: Name.context, empty_nsp: 'a,
8.11 + namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
8.12 + modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
8.13 + -> Code_Thingol.program
8.14 + -> { deresolver: string -> string -> string,
8.15 + flat_program: flat_program }
8.16 +
8.17 datatype ('a, 'b) node =
8.18 Dummy
8.19 | Stmt of 'a
8.20 | Module of ('b * (string * ('a, 'b) node) Graph.T)
8.21 - type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T
8.22 + type ('a, 'b) hierarchical_program
8.23 val hierarchical_program: (string -> string) -> { module_alias: string -> string option,
8.24 reserved: Name.context, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
8.25 namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
8.26 @@ -29,11 +37,97 @@
8.27 structure Code_Namespace : CODE_NAMESPACE =
8.28 struct
8.29
8.30 -(** splitting names in module and base part **)
8.31 +(** building module name hierarchy **)
8.32
8.33 val dest_name =
8.34 apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
8.35
8.36 +fun build_module_namespace { module_alias, module_prefix, reserved } program =
8.37 + let
8.38 + fun alias_fragments name = case module_alias name
8.39 + of SOME name' => Long_Name.explode name'
8.40 + | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
8.41 + (Long_Name.explode name);
8.42 + val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
8.43 + in
8.44 + fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
8.45 + module_names Symtab.empty
8.46 + end;
8.47 +
8.48 +
8.49 +(** flat program structure **)
8.50 +
8.51 +type flat_program = ((string * Code_Thingol.stmt option) Graph.T * (string * string list) list) Graph.T;
8.52 +
8.53 +fun flat_program labelled_name { module_alias, module_prefix, reserved,
8.54 + empty_nsp, namify_stmt, modify_stmt } program =
8.55 + let
8.56 +
8.57 + (* building module name hierarchy *)
8.58 + val fragments_tab = build_module_namespace { module_alias = module_alias,
8.59 + module_prefix = module_prefix, reserved = reserved } program;
8.60 + val dest_name = dest_name
8.61 + #>> (Long_Name.implode o the o Symtab.lookup fragments_tab);
8.62 +
8.63 + (* distribute statements over hierarchy *)
8.64 + fun add_stmt name stmt =
8.65 + let
8.66 + val (module_name, base) = dest_name name;
8.67 + in
8.68 + Graph.default_node (module_name, (Graph.empty, []))
8.69 + #> (Graph.map_node module_name o apfst) (Graph.new_node (name, (base, stmt)))
8.70 + end;
8.71 + fun add_dependency name name' =
8.72 + let
8.73 + val (module_name, base) = dest_name name;
8.74 + val (module_name', base') = dest_name name';
8.75 + in if module_name = module_name'
8.76 + then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
8.77 + else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
8.78 + end;
8.79 + val proto_program = Graph.empty
8.80 + |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
8.81 + |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
8.82 +
8.83 + (* name declarations and statement modifications *)
8.84 + fun declare name (base, stmt) (gr, nsp) =
8.85 + let
8.86 + val (base', nsp') = namify_stmt stmt base nsp;
8.87 + val gr' = (Graph.map_node name o apfst) (K base') gr;
8.88 + in (gr', nsp') end;
8.89 + fun declarations gr = (gr, empty_nsp)
8.90 + |> fold (fn name => declare name (Graph.get_node gr name)) (Graph.keys gr)
8.91 + |> fst
8.92 + |> (Graph.map o K o apsnd) modify_stmt;
8.93 + val flat_program = proto_program
8.94 + |> (Graph.map o K o apfst) declarations;
8.95 +
8.96 + (* qualified and unqualified imports, deresolving *)
8.97 + fun base_deresolver name = fst (Graph.get_node
8.98 + (fst (Graph.get_node flat_program (fst (dest_name name)))) name);
8.99 + fun classify_names gr imports =
8.100 + let
8.101 + val import_tab = maps
8.102 + (fn (module_name, names) => map (rpair module_name) names) imports;
8.103 + val imported_names = map fst import_tab;
8.104 + val here_names = Graph.keys gr;
8.105 + in
8.106 + Symtab.empty
8.107 + |> fold (fn name => Symtab.update (name, base_deresolver name)) here_names
8.108 + |> fold (fn name => Symtab.update (name,
8.109 + Long_Name.append (the (AList.lookup (op =) import_tab name))
8.110 + (base_deresolver name))) imported_names
8.111 + end;
8.112 + val name_tabs = AList.make (uncurry classify_names o Graph.get_node flat_program)
8.113 + (Graph.keys flat_program);
8.114 + val deresolver_tab = Symtab.empty
8.115 + |> fold (fn (module_name, name_tab) => Symtab.update (module_name, name_tab)) name_tabs;
8.116 + fun deresolver module_name name =
8.117 + the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
8.118 + handle Option => error ("Unknown statement name: " ^ labelled_name name);
8.119 +
8.120 + in { deresolver = deresolver, flat_program = flat_program } end;
8.121 +
8.122
8.123 (** hierarchical program structure **)
8.124
8.125 @@ -56,13 +150,8 @@
8.126 let
8.127
8.128 (* building module name hierarchy *)
8.129 - fun alias_fragments name = case module_alias name
8.130 - of SOME name' => Long_Name.explode name'
8.131 - | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
8.132 - (Long_Name.explode name);
8.133 - val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
8.134 - val fragments_tab = fold (fn name => Symtab.update
8.135 - (name, alias_fragments name)) module_names Symtab.empty;
8.136 + val fragments_tab = build_module_namespace { module_alias = module_alias,
8.137 + module_prefix = "", reserved = reserved } program;
8.138 val dest_name = dest_name #>> (the o Symtab.lookup fragments_tab);
8.139
8.140 (* building empty module hierarchy *)
9.1 --- a/src/Tools/Code/code_thingol.ML Tue Sep 07 14:11:05 2010 +0200
9.2 +++ b/src/Tools/Code/code_thingol.ML Tue Sep 07 17:36:33 2010 +0200
9.3 @@ -271,7 +271,6 @@
9.4 of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
9.5 | NONE => Codegen.thyname_of_const thy c);
9.6 fun purify_base "==>" = "follows"
9.7 - | purify_base "op =" = "eq"
9.8 | purify_base s = Name.desymbolize false s;
9.9 fun namify thy get_basename get_thyname name =
9.10 let