{-# LANGUAGE CPP                   #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

module AlgebraCheckers.Homos where

import           AlgebraCheckers.Types
import           AlgebraCheckers.Unification
import           Control.Arrow (second)
import           Data.Group
import           Data.List (foldl')
import qualified Data.Map as M
import           Data.Maybe
import           Language.Haskell.TH hiding (ppr, Arity)

#if __GLASGOW_HASKELL__ <= 802
import           Data.Semigroup
#endif


appHead :: Exp -> Maybe Name
appHead :: Exp -> Maybe Name
appHead = ((Name, [Exp]) -> Name) -> Maybe (Name, [Exp]) -> Maybe Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, [Exp]) -> Name
forall a b. (a, b) -> a
fst (Maybe (Name, [Exp]) -> Maybe Name)
-> (Exp -> Maybe (Name, [Exp])) -> Exp -> Maybe Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Maybe (Name, [Exp])
splitApps

splitApps :: Exp -> Maybe (Name, [Exp])
splitApps :: Exp -> Maybe (Name, [Exp])
splitApps (VarE Name
n)         = (Name, [Exp]) -> Maybe (Name, [Exp])
forall a. a -> Maybe a
Just (Name
n, [])
splitApps (ConE Name
n)         = (Name, [Exp]) -> Maybe (Name, [Exp])
forall a. a -> Maybe a
Just (Name
n, [])
splitApps (AppE Exp
f Exp
e)       = ((Name, [Exp]) -> (Name, [Exp]))
-> Maybe (Name, [Exp]) -> Maybe (Name, [Exp])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Exp] -> [Exp]) -> (Name, [Exp]) -> (Name, [Exp])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ([Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
++ [Exp
e])) (Maybe (Name, [Exp]) -> Maybe (Name, [Exp]))
-> Maybe (Name, [Exp]) -> Maybe (Name, [Exp])
forall a b. (a -> b) -> a -> b
$ Exp -> Maybe (Name, [Exp])
splitApps Exp
f
splitApps (InfixE Maybe Exp
e1 Exp
f Maybe Exp
e2) =
  ((Name, [Exp]) -> (Name, [Exp]))
-> Maybe (Name, [Exp]) -> Maybe (Name, [Exp])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Exp] -> [Exp]) -> (Name, [Exp]) -> (Name, [Exp])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (\[Exp]
e -> [Exp]
e [Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
++ Maybe Exp -> [Exp]
forall a. Maybe a -> [a]
maybeToList Maybe Exp
e1 [Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
++ Maybe Exp -> [Exp]
forall a. Maybe a -> [a]
maybeToList Maybe Exp
e2)) (Maybe (Name, [Exp]) -> Maybe (Name, [Exp]))
-> Maybe (Name, [Exp]) -> Maybe (Name, [Exp])
forall a b. (a -> b) -> a -> b
$ Exp -> Maybe (Name, [Exp])
splitApps Exp
f
splitApps Exp
_                = Maybe (Name, [Exp])
forall a. Maybe a
Nothing

aritySize :: Arity -> Int
aritySize :: Arity -> Int
aritySize Arity
Binary     = Int
2
aritySize (Prefix Int
n) = Int
n

makeHomo :: Name -> [(Name, Arity)] -> Exp -> [Law LawSort]
makeHomo :: Name -> [(Name, Arity)] -> Exp -> [Law LawSort]
makeHomo Name
ty [(Name, Arity)]
ops (LamE [VarP Name
name] Exp
body) =
  let app_head :: [Char]
app_head = [Char] -> (Name -> [Char]) -> Maybe Name -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"<expr>" Name -> [Char]
nameBase (Maybe Name -> [Char]) -> Maybe Name -> [Char]
forall a b. (a -> b) -> a -> b
$ Exp -> Maybe Name
appHead Exp
body
      homo_name :: [Char]
homo_name = Name -> [Char]
nameBase Name
ty
      hs :: [Exp]
hs = (Int -> Exp) -> [Int] -> [Exp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Exp
UnboundVarE (Name -> Exp) -> (Int -> Name) -> Int -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Name
mkName ([Char] -> Name) -> (Int -> [Char]) -> Int -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> [Char]
nameBase Name
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> (Int -> [Char]) -> Int -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show)
                [Int
1 .. [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ ((Name, Arity) -> Int) -> [(Name, Arity)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Arity -> Int
aritySize (Arity -> Int) -> ((Name, Arity) -> Arity) -> (Name, Arity) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Arity) -> Arity
forall a b. (a, b) -> b
snd) [(Name, Arity)]
ops]
      mk_lawname :: Name -> [Char]
mk_lawname Name
fn =
        [[Char]] -> [Char]
forall a. Monoid a => [a] -> a
mconcat
          [ [Char]
app_head, [Char]
":", [Char]
homo_name, [Char]
":", Name -> [Char]
nameBase Name
fn ]
   in (((Name, Arity) -> Law LawSort)
 -> [(Name, Arity)] -> [Law LawSort])
-> [(Name, Arity)]
-> ((Name, Arity) -> Law LawSort)
-> [Law LawSort]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Name, Arity) -> Law LawSort) -> [(Name, Arity)] -> [Law LawSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Name, Arity)]
ops (((Name, Arity) -> Law LawSort) -> [Law LawSort])
-> ((Name, Arity) -> Law LawSort) -> [Law LawSort]
forall a b. (a -> b) -> a -> b
$ \(Name
fn_name, Arity
arity) ->
        Name -> [Exp] -> Exp -> [Char] -> Exp -> Arity -> Law LawSort
mkHomo Name
name [Exp]
hs Exp
body (Name -> [Char]
mk_lawname Name
fn_name) (Name -> Exp
VarE Name
fn_name) Arity
arity
makeHomo Name
_ [(Name, Arity)]
_ Exp
_ = [Char] -> [Law LawSort]
forall a. HasCallStack => [Char] -> a
error [Char]
"monoidal homomorphism needs a lambda"


mkHomo :: Name -> [Exp] -> Exp -> String -> Exp -> Arity -> NamedLaw
mkHomo :: Name -> [Exp] -> Exp -> [Char] -> Exp -> Arity -> Law LawSort
mkHomo Name
name [Exp]
vars Exp
body [Char]
law_name Exp
fn Arity
Binary =
  case [Exp]
vars of
    (Exp
v1:Exp
v2:[Exp]
_) ->
      let replace :: Exp -> Exp
replace Exp
x = Map Name Exp -> Exp -> Exp
forall a. Data a => Map Name Exp -> a -> a
rebindVars (Name -> Exp -> Map Name Exp
forall k a. k -> a -> Map k a
M.singleton Name
name Exp
x) Exp
body
       in LawSort -> Exp -> Exp -> Law LawSort
forall a. a -> Exp -> Exp -> Law a
Law ([Char] -> LawSort
LawName [Char]
law_name)
              (Exp -> Exp
replace (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
v1) Exp
fn (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
v2))
              (Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Exp -> Maybe Exp) -> Exp -> Maybe Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
replace Exp
v1)
                      Exp
fn
                      (Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Exp -> Maybe Exp) -> Exp -> Maybe Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
replace Exp
v2))
    [Exp]
_ -> [Char] -> Law LawSort
forall a. HasCallStack => [Char] -> a
error [Char]
"not enough args to mkHomo"
mkHomo Name
name [Exp]
all_vars Exp
body [Char]
law_name Exp
fn (Prefix Int
n)=
  let replace :: Exp -> Exp
replace Exp
x = Map Name Exp -> Exp -> Exp
forall a. Data a => Map Name Exp -> a -> a
rebindVars (Name -> Exp -> Map Name Exp
forall k a. k -> a -> Map k a
M.singleton Name
name Exp
x) Exp
body
      vars :: [Exp]
vars = Int -> [Exp] -> [Exp]
forall a. Int -> [a] -> [a]
take Int
n [Exp]
all_vars
   in LawSort -> Exp -> Exp -> Law LawSort
forall a. a -> Exp -> Exp -> Law a
Law ([Char] -> LawSort
LawName [Char]
law_name)
          (Exp -> Exp
replace (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Exp -> Exp -> Exp
AppE Exp
fn [Exp]
vars)
          ((Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Exp -> Exp -> Exp
AppE Exp
fn ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> [Exp] -> [Exp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Exp -> Exp
replace [Exp]
vars)


knownHomos :: Name -> [(Name, Arity)]
knownHomos :: Name -> [(Name, Arity)]
knownHomos Name
nm
  | Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Semigroup
        = [ ('(<>),   Arity
Binary) ]
  | Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Monoid
        = [ ('mempty, Int -> Arity
Prefix Int
0)
          , ('(<>),   Arity
Binary)
          ]
  | Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Group
        = [ ('invert, Int -> Arity
Prefix Int
1) ]
  | Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Eq
        = [ ('(==), Arity
Binary) ]
  | Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Ord
        = [ ('compare, Int -> Arity
Prefix Int
2) ]
  | Bool
otherwise = [Char] -> [(Name, Arity)]
forall a. HasCallStack => [Char] -> a
error ([Char] -> [(Name, Arity)]) -> [Char] -> [(Name, Arity)]
forall a b. (a -> b) -> a -> b
$ [Char]
"unsupported homo type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
show Name
nm