{-# LANGUAGE ScopedTypeVariables #-}
{-
Copyright 2011 Ken Takusagawa
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Affero General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU Affero General Public License
along with this program.  If not, see <http://www.gnu.org/licenses/>.
-}

module Main (main) where{
import Data.List;
import Data.Maybe;
import Control.Monad;

main :: IO(());
main = (do{
  (putStrLn "=============test1");
  test1;
  (putStrLn "=============test2");
  test;
});
type Btape  = Listzipper(Bool);
btape_initial :: Btape;
btape_initial = (infinite_repeat False);
siblings_blank :: a -> Siblings(a);
siblings_blank x = ((repeat x), (repeat x));
infinite_repeat :: a -> Listzipper(a);
infinite_repeat x = (Listzipper x (siblings_blank x));
tape_left :: Listzipper(a) -> Listzipper(a);
tape_left (Listzipper middle (((:) h t), right)) = (Listzipper h (t, ((:) middle right)));
tape_right :: Listzipper(a) -> Listzipper(a);
tape_right (Listzipper middle (left, ((:) h t))) = (Listzipper h (((:) middle left), t));
type Tt  = Listzipper(Btape);
tt_initial :: Tt;
tt_initial = (infinite_repeat btape_initial);
left :: Zipper -> Zipper;
left (Zipper n parents) = (Zipper (tape_left n) parents);
right :: Zipper -> Zipper;
right (Zipper n parents) = (Zipper (tape_right n) parents);
up :: Zipper -> Zipper;
up (Zipper n ((:) parent grandparents)) = (Zipper (Listzipper (Internal n) parent) grandparents);
down :: (Monad (m)) => Zipper -> m(Zipper);
down (Zipper (Listzipper n sibs) parents) = (case n of {
  (Internal t)-> (return (Zipper t ((:) sibs parents)));
  _ -> (fail "cannot descend leaf")
});
jdown :: Zipper -> Zipper;
jdown z = (fromJust(down(z)));
get_node :: Zipper -> Node;
get_node (Zipper (Listzipper n _) _) = n;
read_tape :: (Monad (m)) => Zipper -> m(Bool);
read_tape z = (case (get_node z) of {
  (Leaf x)-> (return x);
  _ -> (fail "cannot read internal node")
});
is_leaf :: Node -> Bool;
is_leaf n = (case n of {
  (Leaf _)-> True;
  _ -> False
});
write_node_bool :: (Monad (m)) => Node -> Bool -> m(Node);
write_node_bool n x = (case n of {
  (Leaf _)-> (return (Leaf x));
  _ -> (fail "error: tried to write internal node")
});
write_tape_bool :: (Monad (m)) => Bool -> Zipper -> m(Zipper);
write_tape_bool x (Zipper (Listzipper n sibs) parents) = (do{
  new :: Node <- (write_node_bool n x);
  (return (Zipper (Listzipper new sibs) parents));
});
set_tape :: Zipper -> Zipper;
set_tape z = (fromJust((write_tape_bool True)(z)));
data Listzipper a = Listzipper(a)(Siblings(a));
data Node  = Leaf(Bool) | Internal(Tape);
type Tape  = Listzipper(Node);
data Zipper  = Zipper(Tape)([](Siblings(Node)));
type Siblings a = ([](a), [](a));
empty_regular_tape :: Tape;
empty_regular_tape = (infinite_repeat (Leaf False));
first_siblings :: Siblings(Node);
first_siblings = (siblings_blank (Internal empty_regular_tape));
higher_tape :: Tape -> Tape;
higher_tape t = (infinite_repeat (Internal t));
get_sibs :: Listzipper(a) -> Siblings(a);
get_sibs (Listzipper _ sibs) = sibs;
initial_sibs :: [](Siblings(Node));
initial_sibs = ((map get_sibs)(tail((iterate higher_tape)(empty_regular_tape))));

{- |Infinite tapes of Falses are all on the same bottom level.
Every level up, each cell is itself an infinite tape. -}
initial_zipper :: Zipper;
initial_zipper = (Zipper empty_regular_tape initial_sibs);
test1 :: IO(());
test1 = (do{
  let {  z :: Zipper;  z = initial_zipper;};
  let {
p :: Zipper -> IO(());
p z = (print ((read_tape z) :: Maybe(Bool)))
};
  (p(z));
  (p(left(z)));
  (p(up(z)));
  (p(jdown(up(z))));
  (p(jdown(up(left(z)))));
  (p(jdown(left(up(z)))));
  (p(jdown(jdown(up(up(set_tape(z)))))));
  (p(right(left(set_tape(z)))));
  (p(right(jdown(right(jdown(right(left(up(left(up(left(set_tape(z)))))))))))));
});
not_flat_sibs :: Siblings(Node);
not_flat_sibs = (siblings_blank (Leaf False));

{- |The current tape is at the base on an infinite tree.
Going up yields a tape with Falses on either side, and an infinite tape under the current cell -}
not_flat_initial_zipper :: Zipper;
not_flat_initial_zipper = ((Zipper empty_regular_tape)(repeat(siblings_blank(Leaf(False)))));

{- |Replace the current cell with an empty subtape -}
write_tape :: Zipper -> Zipper;
write_tape (Zipper (Listzipper _ sibs) parents) = (Zipper (Listzipper (Internal empty_regular_tape) sibs) parents);
test :: IO(());
test = (do{
  let {  z :: Zipper;  z = not_flat_initial_zipper;};
  let {
p :: Zipper -> IO(());
p z = (print ((read_tape z) :: Maybe(Bool)))
};
  (p(z));
  (p(write_tape(z)));
  (p(jdown(write_tape(right(set_tape(left(z)))))));
  (p(left(up(jdown(write_tape(right(set_tape(left(z)))))))));
  (p(jdown(right(jdown(left(right(up(left(up(set_tape(left(z))))))))))));
})
}