{-

Explore the generators-and-relators presentation of the icosahedral
group (Hamilton's Icosian calculus).

Copyright 2017 Ken Takusagawa

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU 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 General Public License
along with this program.  If not, see <http://www.gnu.org/licenses/>.
-}


{-# LANGUAGE ScopedTypeVariables, LambdaCase #-}
module Main where {
import System.Environment(getArgs);
import Control.Exception(assert);
import Debug.Trace(trace);
import Data.Function((&));
import Control.Category((>>>));
import Prelude hiding((.),(>>));
--import System.IO(hSetBuffering,stdout,BufferMode(LineBuffering));
import Data.List;
import Control.Monad;
import Data.Maybe;
import qualified Data.Map as Map;
import Data.Map(Map);
import qualified Data.Set as Set;
import Data.Set(Set);
import Data.Sequence(Seq);
import qualified Data.Sequence as Seq;
import Data.Foldable(toList);
import qualified Control.Monad.State.Lazy as State;
import Control.Monad.State.Lazy(State);

-- to avoid the redundancy warning
trace_placeholder :: ();
trace_placeholder = (trace,assert) & (id >>> error) "trace_placeholder";

main :: IO();
main = getArgs >>= \case{
[] -> multiplication_table strict_sixty & map show_multiplication_line & mapM_ putStrLn;
["identities_sorted"] -> ik5_shrink & sortBy (tuple_sort compare_strings) & mapM_ (show_identity >>> putStrLn);
-- unsorted gives a better idea of how they were generated
["identities"] -> shrink_down ik5 Seq.empty & mapM_ (show_identity >>> putStrLn);
["ish"] -> sixty_one_ish & length & print;
-- prune the set of 62 down to 60 ("fast-forward" instead of pruning 62*62)
["ff",iters] -> map (\x -> let {f=canonicalize (read iters) x} in (x==f,f)) sixty_one_ish & mapM_ print;
-- see if there are any shorter versions of the 60 found at iters=6
["ffs",iters] -> map (\x -> let {f=canonicalize (read iters) x} in (x==f,f)) strict_sixty & mapM_ print;
["repeat"] -> iterate (itermult_l (repeat_best >>> id)) start_l & map length & mapM_ print;
["counts",iters] -> iterate (itermult_l (repeat_best >>> canonicalize (read iters))) start_l & map length & mapM_ print;
["rules2"] -> iterate (itermult rules2) start & map length & mapM_ print;
_ -> undefined;
};

data Subs a = Subs [a] [a] deriving (Show, Ord, Eq);

reduce :: (Eq a) => Subs a -> [a] -> [a];
reduce _ [] = [];
reduce s@(Subs old new) target@(h:t) = case match_initial old target of {
Nothing -> h:reduce s t;
Just newtail -> new ++ reduce s newtail
};

match_initial :: (Eq a) => [a] -> [a] -> Maybe [a];
match_initial [] rest = Just rest;
match_initial _ [] = Nothing;
match_initial (x:xrest) (y:yrest) = if x==y
then match_initial xrest yrest
else Nothing;

until_fixpoint :: Eq a => (a -> a) -> a -> a;
until_fixpoint f x = let {new = f x} in
if x == new then x else until_fixpoint f new;

subs_string :: (Eq a) => Subs a -> [a] -> [a];
subs_string s = until_fixpoint (reduce s);

data Ops = I | K deriving (Show, Eq, Ord);

type Mystring=Seq Ops;

type SeenStuff = Set (Mystring,Mystring);
type Seen = State SeenStuff;

shrink_down_m :: Mystring -> Mystring -> Seen [(Mystring, Mystring)];
shrink_down_m oldleft oldright = do {
  let {left = base_substs oldleft;
     right = base_substs oldright;};
  seen :: SeenStuff <- State.get;
  if Set.member (left,right) seen then return []
  else do {
  State.modify (Set.insert (left,right));
  -- modifications to the right first is slightly aesthetically prettier
bb <- case Seq.viewr left of {
Seq.EmptyR -> return [];
_ Seq.:> x -> shrink_down_m (left Seq.|> x) (right Seq.|> x);
};
    aa <- case Seq.viewl left of {
Seq.EmptyL -> return[];
x Seq.:< _ -> shrink_down_m (x Seq.<| left) (x Seq.<| right);
};
return $ (left,right):(bb++aa);
}};

shrink_down :: Mystring -> Mystring -> [(Mystring, Mystring)];
shrink_down left right = State.evalState (shrink_down_m left right) Set.empty;

base_substs :: Mystring -> Mystring;
base_substs = toList >>> many_rules [base_i,base_k] >>> Seq.fromList;

base_i :: Subs Ops;
base_i = Subs [I,I] [];

base_k :: Subs Ops;
base_k = Subs [K,K,K] [];

genops :: Char -> Ops;
genops 'i' = I;
genops 'k' = K;
genops _ = error "not i or k";

-- map genops
mg :: String -> Mystring;
mg = map genops >>> Seq.fromList;

ik5 :: Mystring;
ik5 = [I,K] & replicate 5 & concat & Seq.fromList;

-- liftA2
{-
x1 = x2
y1 = y2

x1 * y1 ...
-}
prod_tuple :: (a -> b -> c) -> [a] -> [b] -> [c];
prod_tuple combine x y = do {
ox<-x;
oy<-y;
return $ combine ox oy;
};

tuple_to_list :: (a,a) -> [a];
tuple_to_list (x,y) = [x,y];

form_some_products :: [(Mystring,Mystring)] -> [(Mystring, Mystring)];
form_some_products somelines = do {
i1 :: [Mystring] <- somelines >>= (tuple_to_list >>> return);
i2 :: [Mystring] <- somelines >>= (tuple_to_list >>> return);
p1 <- prod_tuple (Seq.><) i1 i2 >>= (base_substs >>> return);
p2 <- prod_tuple (Seq.><) i1 i2 >>= (base_substs >>> return);
-- guard $ p1 /= p2;
guard $ p1 < p2;
return (p1,p2);
};

uniquify :: (Ord a) => [a] -> [a];
uniquify = Set.fromList >>> Set.toList;

reduce_once_by_many_rules :: (Eq a) => [a] -> [Subs a] -> [a];
reduce_once_by_many_rules = foldr (\r -> subs_string r);

many_rules :: (Eq a) => [Subs a] -> [a] -> [a];
many_rules rs = until_fixpoint (\eachtime -> reduce_once_by_many_rules eachtime rs);

-- (3000,2) gets 61 items instead of 62.
score :: Ops -> Integer;
score I = 1;
score K = 1;

scores :: (Functor m, Foldable m) => m Ops -> Integer;
scores = fmap score >>> sum;

compare_strings :: (Functor m, Foldable m, Ord (m Ops)) => m Ops -> m Ops -> Ordering;
compare_strings x y = case compare (scores x) (scores y) of {
EQ -> compare x y;
z -> z;
};

create_subs :: (Mystring, Mystring) -> Subs Ops;
create_subs (x,y) = case compare_strings x y of {
LT -> Subs (toList y) (toList x);
GT -> Subs (toList x) (toList y);
EQ -> error "equal create_subs";
};

raw_create_subs :: (Mystring, Mystring) -> Subs Ops;
raw_create_subs (x,y) = Subs (toList x) (toList y);

multiplications :: [Mystring] -> [Mystring];
multiplications l = do {
x <- l;
y <- l;
return $ x Seq.>< y;
} & uniquify;

start :: [Mystring];
start = map Seq.fromList start_l;

start_l :: [[Ops]];
start_l = [[],[I],[K]];

rules1 :: [Subs Ops];
rules1 = base_i : base_k : (ik5_shrink & map create_subs);

ik5_shrink :: [(Mystring,Mystring)];
ik5_shrink = shrink_down ik5 Seq.empty & uniquify;

ik5_plus :: [(Mystring,Mystring)];
ik5_plus = (Seq.fromList[I,I],Seq.empty):(Seq.fromList[K,K,K],Seq.empty):ik5_shrink;

rules2 :: [Subs Ops];
rules2 = (form_some_products ik5_plus & map create_subs) ++ rules1 & uniquify;

itermult :: [Subs Ops] -> [Mystring] -> [Mystring];
itermult rules = multiplications >>> map toList >>> map (many_rules rules) >>> uniquify >>> map Seq.fromList;

left_inverse :: Mystring -> Mystring;
left_inverse = go Seq.empty where {
go :: Mystring -> Mystring -> Mystring;
go partial x = case Seq.viewl x of {
Seq.EmptyL -> partial;
K Seq.:< _ -> go ((Seq.<|) K partial) ((Seq.<|) K x & base_substs);
I Seq.:< y -> go ((Seq.<|) I partial) y;
}
};

right_inverse :: Mystring -> Mystring;
right_inverse = go Seq.empty where {
go :: Mystring -> Mystring -> Mystring;
go partial x = case Seq.viewr x of {
Seq.EmptyR -> partial;
_ Seq.:> K -> go ((Seq.|>) partial K) ((Seq.|>) x K & base_substs);
y Seq.:> I -> go ((Seq.|>) partial I) y;
}
};

all_of_size :: Int -> [Mystring];
all_of_size n = replicateM n "ik" & map mg;

-- left_inverse and right_inverse are the same, confirmed up to size 15

--but we can still consider multiplying on the left and right of a target equivalence

one_shrink_r :: (Mystring,Mystring) -> (Mystring,Mystring);
one_shrink_r (left,right) = case Seq.viewr left of
{ Seq.EmptyR -> error "no more to shrink"
; _ Seq.:> x -> ( (left Seq.|> x) & base_substs , (right Seq.|> x) & base_substs )
};

base_lambda :: Subs Ops;
base_lambda = Subs (ik5 & toList) [];

base_inverse_lambda :: Subs Ops;
base_inverse_lambda = Subs (left_inverse ik5 & toList) [];

reductions_lambda :: Integer -> (Mystring, Mystring);
reductions_lambda i = genericIndex (iterate one_shrink_r (ik5, Seq.empty)) i;

interesting_subs :: Subs Ops;
interesting_subs = let { v = mg "kikik" } in raw_create_subs (v, lookup v ik5_shrink & fromJust);

-- this set always decreases the length
safe_set :: [Subs Ops];
safe_set = reverse [base_i, base_k, base_lambda, base_inverse_lambda];
-- reverse on the hunch that the bigger ones are the most exciting to try first

my_set :: [Subs Ops];
my_set = [base_i, base_k, base_lambda, base_inverse_lambda, interesting_subs];

try_interesting_shrink :: Subs Ops -> [Ops] -> Maybe [Ops];
try_interesting_shrink s initial = let
{ step1 :: [Ops]
; step1 = reduce s initial
; step2 :: [Ops]
; step2 = many_rules safe_set step1
} in if step1==step2 then Nothing else Just step2;

avoid_repeating_rule :: Subs Ops -> [Ops] -> Maybe [Ops];
avoid_repeating_rule s initial = do
{ step1 <- try_interesting_shrink s initial
; if reduce s step1 == step1 then return step1 else mzero
};  -- avoid infinite growth

only_if_shrink :: [Ops] -> ([Ops] -> Maybe [Ops]) -> Maybe [Ops];
only_if_shrink initial f = do
{ new <- f initial
; if LT == compare_strings new initial then return new else mzero
};

all_ik5_subs :: [Subs Ops];
all_ik5_subs = do {
(left,right) <- ik5_shrink;
[raw_create_subs (left,right), raw_create_subs (right,left)]
} & filter valid_substitution;

valid_substitution :: Subs Ops -> Bool;
valid_substitution (Subs [] _) = False;
valid_substitution _ = True;

best_among_ik5_shrink :: [Ops] -> [Ops];
best_among_ik5_shrink input = head $ sortBy compare_strings $ (many_rules safe_set input) : (map (try_interesting_shrink >>> only_if_shrink input) all_ik5_subs & catMaybes);

repeat_best :: [Ops] -> [Ops];
repeat_best = until_fixpoint best_among_ik5_shrink;

itermult_l :: ([Ops] -> [Ops]) -> [[Ops]] -> [[Ops]];
itermult_l canonicalizer = map Seq.fromList >>> multiplications >>> map toList >>> map canonicalizer >>> uniquify;

-- roughly straight up theorem prover

reduce1 :: (Eq a) => Subs a -> [a] -> [[a]];
reduce1 _ [] = [];
reduce1 s@(Subs old new) target@(h:t) = mplus (case match_initial old target of
{ Nothing -> mzero
; Just newtail -> return $ new++newtail
}) (do
{ rest <- reduce1 s t
; return $ h:rest
});

-- heuristic: assume safe_set simplifications do not hurt.
reduce1simplify :: Subs Ops -> [Ops] -> [[Ops]];
reduce1simplify s = reduce1 s >>> map (many_rules safe_set);

-- this could do some A* because we know we are looking for the minimum
grow_set :: [Subs Ops] -> [[Ops]] -> [[Ops]];
grow_set s l = do
{ s1 <- s
; case s1 of {(Subs left _) -> guard (length left >2)}  -- avoid substitutions that grow a lot
; l1 <- l
; reduce1simplify s1 l1
} & uniquify ;

canonicalize :: Integer -> [Ops] -> [Ops];
canonicalize iterations initial = iterate (grow_set all_ik5_subs) [many_rules safe_set initial] & genericTake iterations & concat & sortBy compare_strings & head;

my_canonicalize :: [Ops] -> [Ops];
my_canonicalize = canonicalize 6;

-- or 62 depending on score weights
sixty_one_ish :: [[Ops]];
sixty_one_ish = until_fixpoint (itermult_l repeat_best) start_l;

zip_map :: (a -> b) -> [a] -> [(a,b)];
zip_map f l = zip l $ map f l;

-- optimization
canonicalization_map :: Map [Ops] [Ops];
canonicalization_map = zip_map my_canonicalize sixty_one_ish & Map.fromList;

simplify :: [Ops] -> [Ops];
simplify = repeat_best >>> (\x -> Map.lookup x canonicalization_map) >>> fromJust;

strict_sixty :: [[Ops]];
strict_sixty = map simplify sixty_one_ish & uniquify & sortBy compare_strings;

multiplication_table :: [[Ops]] -> [([Ops],[Ops],[Ops])];
multiplication_table l = do
{ x <- l
; y <- l
; return (x,y, x++y & simplify)
};

show1 :: Ops -> Char;
show1 I = 'i';
show1 K = 'k';

show_element :: [Ops] -> String;
show_element [] = "1";
show_element x = map show1 x;

show_multiplication_line :: ([Ops],[Ops],[Ops]) -> String;
show_multiplication_line (x,y,z) = concat [ show_element x, "*", show_element y, "=", show_element z];

-- this probably exists in the library somehow
tuple_sort :: (a -> a -> Ordering) -> (a,a) -> (a,a) -> Ordering;
tuple_sort f (p,q) (x,y) = case f p x of
{ EQ -> f q y
; z -> z
};

show_identity :: (Mystring, Mystring) -> String;
show_identity (x,y) = concat [toList x & show_element,"=",toList y & show_element];

} --end