{-# LANGUAGE OverloadedStrings #-}

module Application.TermSearch.Utils where

import           Data.Map                     ( Map  )
import qualified Data.Map                    as Map
import           Data.Text                    ( Text )
import qualified Data.Text                   as Text

import           Data.ECTA
import           Data.ECTA.Paths
import           Data.ECTA.Term

import           Application.TermSearch.Type

--------------------------------------------------------------------------------
------------------------------- Type Constructors ------------------------------
--------------------------------------------------------------------------------

typeConst :: Text -> Node
typeConst :: Text -> Node
typeConst Text
s = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge (Text -> Symbol
Symbol Text
s) []]

constrType0 :: Text -> Node
constrType0 :: Text -> Node
constrType0 Text
s = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge (Text -> Symbol
Symbol Text
s) []]

constrType1 :: Text -> Node -> Node
constrType1 :: Text -> Node -> Node
constrType1 Text
s Node
n = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge (Text -> Symbol
Symbol Text
s) [Node
n]]

constrType2 :: Text -> Node -> Node -> Node
constrType2 :: Text -> Node -> Node -> Node
constrType2 Text
s Node
n1 Node
n2 = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge (Text -> Symbol
Symbol Text
s) [Node
n1, Node
n2]]

maybeType :: Node -> Node
maybeType :: Node -> Node
maybeType = Text -> Node -> Node
constrType1 Text
"Maybe"

listType :: Node -> Node
listType :: Node -> Node
listType = Text -> Node -> Node
constrType1 Text
"List"

theArrowNode :: Node
theArrowNode :: Node
theArrowNode = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"(->)" []]

arrowType :: Node -> Node -> Node
arrowType :: Node -> Node -> Node
arrowType Node
n1 Node
n2 = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"->" [Node
theArrowNode, Node
n1, Node
n2]]

appType :: Node -> Node -> Node
appType :: Node -> Node -> Node
appType Node
n1 Node
n2 = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"TyApp" [Node
n1, Node
n2]]

mkDatatype :: Text -> [Node] -> Node
mkDatatype :: Text -> [Node] -> Node
mkDatatype Text
s [Node]
ns = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge (Text -> Symbol
Symbol Text
s) [Node]
ns]

--------------------
------- Functions and arguments
--------------------

constFunc :: Symbol -> Node -> Edge
constFunc :: Symbol -> Node -> Edge
constFunc Symbol
s Node
t = Symbol -> [Node] -> Edge
Edge Symbol
s [Node
t]

constArg :: Symbol -> Node -> Edge
constArg :: Symbol -> Node -> Edge
constArg = Symbol -> Node -> Edge
constFunc

var1, var2, var3, var4, varAcc :: Node
var1 :: Node
var1 = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"var1" []]
var2 :: Node
var2 = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"var2" []]
var3 :: Node
var3 = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"var3" []]
var4 :: Node
var4 = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"var4" []]
varAcc :: Node
varAcc = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"acc" []]

--------------------------------------------------------------------------------

--------------------
------- Component Grouping
--------------------

mkGroups :: [(Text, TypeSkeleton)] -> (Map TypeSkeleton Text, Map Text Text)
mkGroups :: [(Text, TypeSkeleton)] -> (Map TypeSkeleton Text, Map Text Text)
mkGroups [] = (Map TypeSkeleton Text
forall k a. Map k a
Map.empty, Map Text Text
forall k a. Map k a
Map.empty)
mkGroups ((Text
name, TypeSkeleton
typ):[(Text, TypeSkeleton)]
comps) = let (Map TypeSkeleton Text
groups, Map Text Text
nameToRepresentative) = [(Text, TypeSkeleton)] -> (Map TypeSkeleton Text, Map Text Text)
mkGroups [(Text, TypeSkeleton)]
comps
                                   freshName :: Text
freshName = String -> Text
Text.pack (String
"f" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Map TypeSkeleton Text -> Int
forall k a. Map k a -> Int
Map.size Map TypeSkeleton Text
groups))
                                in if TypeSkeleton
typ TypeSkeleton -> Map TypeSkeleton Text -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map TypeSkeleton Text
groups 
                                  then (Map TypeSkeleton Text
groups, Text -> Text -> Map Text Text -> Map Text Text
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name (Map TypeSkeleton Text
groups Map TypeSkeleton Text -> TypeSkeleton -> Text
forall k a. Ord k => Map k a -> k -> a
Map.! TypeSkeleton
typ) Map Text Text
nameToRepresentative)
                                  else (TypeSkeleton
-> Text -> Map TypeSkeleton Text -> Map TypeSkeleton Text
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TypeSkeleton
typ Text
freshName Map TypeSkeleton Text
groups, Text -> Text -> Map Text Text -> Map Text Text
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name Text
freshName Map Text Text
nameToRepresentative)

getRepOf :: [(Text, [Text])] -> Text -> Text
getRepOf :: [(Text, [Text])] -> Text -> Text
getRepOf [] Text
fname = String -> Text
forall a. HasCallStack => String -> a
error (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"cannot find " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
forall a. Show a => a -> String
show Text
fname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in any group"
getRepOf ((Text
x, [Text]
fnames):[(Text, [Text])]
xs) Text
fname
  | Text
fname Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
fnames = Text
x
  | Bool
otherwise = [(Text, [Text])] -> Text -> Text
getRepOf [(Text, [Text])]
xs Text
fname


--------------------
------- Different cases of loops
--------------------

replicatorTau :: Node
replicatorTau :: Node
replicatorTau = (Node -> Node) -> Node
createMu
  (\Node
n -> [Node] -> Node
union
    ([Node
var1, Node
var2] [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ ((Text, Int) -> Node) -> [(Text, Int)] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map ([Edge] -> Node
Node ([Edge] -> Node) -> ((Text, Int) -> [Edge]) -> (Text, Int) -> Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Edge -> [Edge] -> [Edge]
forall a. a -> [a] -> [a]
: []) (Edge -> [Edge]) -> ((Text, Int) -> Edge) -> (Text, Int) -> [Edge]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> (Text, Int) -> Edge
constructorToEdge Node
n) [(Text, Int)]
usedConstructors)
  )
 where
  constructorToEdge :: Node -> (Text, Int) -> Edge
  constructorToEdge :: Node -> (Text, Int) -> Edge
constructorToEdge Node
n (Text
nm, Int
arity) = Symbol -> [Node] -> Edge
Edge (Text -> Symbol
Symbol Text
nm) (Int -> Node -> [Node]
forall a. Int -> a -> [a]
replicate Int
arity Node
n)

  usedConstructors :: [(Text, Int)]
usedConstructors = [(Text
"Pair", Int
2)]

replicator :: Node
replicator :: Node
replicator = [Edge] -> Node
Node
  [ Symbol -> [Node] -> EqConstraints -> Edge
mkEdge
      Symbol
"Pair"
      [ [Edge] -> Node
Node
        [ Symbol -> [Node] -> EqConstraints -> Edge
mkEdge Symbol
"Pair"
                 [Node
replicatorTau, Node
replicatorTau]
                 ([[Path]] -> EqConstraints
mkEqConstraints [[[Int] -> Path
path [Int
0, Int
0], [Int] -> Path
path [Int
0, Int
1], [Int] -> Path
path [Int
1]]])
        ]
      , [Edge] -> Node
Node [
        Symbol -> [Node] -> Edge
Edge Symbol
"Pair" [Node
replicatorTau, Node
replicatorTau]]
      ]
      ([[Path]] -> EqConstraints
mkEqConstraints [[[Int] -> Path
path [Int
0, Int
0], [Int] -> Path
path [Int
0, Int
1], [Int] -> Path
path [Int
1]]])
  ]

loop1 :: Node
loop1 :: Node
loop1 = [Edge] -> Node
Node
  [ Symbol -> [Node] -> EqConstraints -> Edge
mkEdge
      Symbol
"f"
      [ [Edge] -> Node
Node
          [ Symbol -> [Node] -> EqConstraints -> Edge
mkEdge
            Symbol
"g"
            [ [Edge] -> Node
Node
                [ Symbol -> [Node] -> Edge
Edge
                    Symbol
"h"
                    [ [Edge] -> Node
Node
                      [ Symbol -> [Node] -> Edge
Edge Symbol
"Pair" [Node
replicatorTau, Node
replicatorTau]
                      , Symbol -> [Node] -> Edge
Edge Symbol
"var2" []
                      ]
                    , [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"Pair" [Node
replicatorTau, Node
replicatorTau]]
                    ]
                ]
            ]
            ([[Path]] -> EqConstraints
mkEqConstraints [[[Int] -> Path
path [Int
0, Int
0], [Int] -> Path
path [Int
0, Int
1, Int
0]]])
          , Symbol -> [Node] -> Edge
Edge Symbol
"gg" [[Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"Pair" [Node
var2, Node
var2]]]
          ]
      ]
      ([[Path]] -> EqConstraints
mkEqConstraints [[[Int] -> Path
path [Int
0, Int
0, Int
0], [Int] -> Path
path [Int
0, Int
0, Int
1]]])
  ]

loop2 :: Node
loop2 :: Node
loop2 = [Edge] -> Node
Node
  [ Symbol -> [Node] -> EqConstraints -> Edge
mkEdge
      Symbol
"g"
      [ [Edge] -> Node
Node
        [ Symbol -> [Node] -> EqConstraints -> Edge
mkEdge Symbol
"Pair"
                 [[Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"List" [Node
replicatorTau]], Node
replicatorTau]
                 ([[Path]] -> EqConstraints
mkEqConstraints [[[Int] -> Path
path [Int
0, Int
0], [Int] -> Path
path [Int
1]]])
        , Symbol -> [Node] -> Edge
Edge Symbol
"f" [Node
var1, [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"List" [Node
var1]]]
        ]
      , [Edge] -> Node
Node
        [ Symbol -> [Node] -> EqConstraints -> Edge
mkEdge Symbol
"Pair"
                 [[Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"List" [Node
replicatorTau]], Node
replicatorTau]
                 ([[Path]] -> EqConstraints
mkEqConstraints [[[Int] -> Path
path [Int
0], [Int] -> Path
path [Int
1]]])
        , Symbol -> [Node] -> Edge
Edge Symbol
"f" [Node
var1, Node
var1]
        ]
      ]
      ([[Path]] -> EqConstraints
mkEqConstraints
        [[[Int] -> Path
path [Int
0, Int
1, Int
0], [Int] -> Path
path [Int
1, Int
1]], [[Int] -> Path
path [Int
0, Int
0], [Int] -> Path
path [Int
1, Int
0]]]
      )
  ]