{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}

module Application.TermSearch.TermSearch where

import           Data.List                      ( (\\)
                                                , permutations
                                                )
import           Data.List.Extra                ( nubOrd )
import qualified Data.Map                      as Map
import           Data.Maybe                     ( fromMaybe )
import           Data.Text                      ( Text )
import           Data.Tuple                     ( swap )
import           System.IO                      ( hFlush
                                                , stdout
                                                )

import           Data.ECTA
import           Data.ECTA.Paths
import           Data.ECTA.Term
import           Data.Text.Extended.Pretty
import           Utility.Fixpoint

import           Application.TermSearch.Dataset
import           Application.TermSearch.Type
import           Application.TermSearch.Utils

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

tau :: Node
tau :: Node
tau = (Node -> Node) -> Node
createMu
  (\Node
n -> [Node] -> Node
union
    (  [Node -> Node -> Node
arrowType Node
n Node
n, Node
var1, Node
var2, Node
var3, Node
var4]
    [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, Int)]
allConstructors

allConstructors :: [(Text, Int)]
allConstructors :: [(Text, Int)]
allConstructors =
  [(Text, Int)] -> [(Text, Int)]
forall a. Ord a => [a] -> [a]
nubOrd ((TypeSkeleton -> [(Text, Int)]) -> [TypeSkeleton] -> [(Text, Int)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TypeSkeleton -> [(Text, Int)]
getConstructors (Map TypeSkeleton Text -> [TypeSkeleton]
forall k a. Map k a -> [k]
Map.keys Map TypeSkeleton Text
hoogleComponents))
    [(Text, Int)] -> [(Text, Int)] -> [(Text, Int)]
forall a. Eq a => [a] -> [a] -> [a]
\\ [(Text
"Fun", Int
2)]
 where
  getConstructors :: TypeSkeleton -> [(Text, Int)]
  getConstructors :: TypeSkeleton -> [(Text, Int)]
getConstructors (TVar Text
_    ) = []
  getConstructors (TFun TypeSkeleton
t1 TypeSkeleton
t2) = TypeSkeleton -> [(Text, Int)]
getConstructors TypeSkeleton
t1 [(Text, Int)] -> [(Text, Int)] -> [(Text, Int)]
forall a. [a] -> [a] -> [a]
++ TypeSkeleton -> [(Text, Int)]
getConstructors TypeSkeleton
t2
  getConstructors (TCons Text
nm [TypeSkeleton]
ts) =
    (Text
nm, [TypeSkeleton] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeSkeleton]
ts) (Text, Int) -> [(Text, Int)] -> [(Text, Int)]
forall a. a -> [a] -> [a]
: (TypeSkeleton -> [(Text, Int)]) -> [TypeSkeleton] -> [(Text, Int)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TypeSkeleton -> [(Text, Int)]
getConstructors [TypeSkeleton]
ts

generalize :: Node -> Node
generalize :: Node -> Node
generalize n :: Node
n@(Node [Edge
_]) = [Edge] -> Node
Node
  [Symbol -> [Node] -> EqConstraints -> Edge
mkEdge Symbol
s [Node]
ns' ([[Path]] -> EqConstraints
mkEqConstraints ([[Path]] -> EqConstraints) -> [[Path]] -> EqConstraints
forall a b. (a -> b) -> a -> b
$ (Node -> [Path]) -> [Node] -> [[Path]]
forall a b. (a -> b) -> [a] -> [b]
map Node -> [Path]
pathsForVar [Node]
vars)]
 where
  vars :: [Node]
vars                = [Node
var1, Node
var2, Node
var3, Node
var4, Node
varAcc]
  nWithVarsRemoved :: Node
nWithVarsRemoved    = (Node -> Node) -> Node -> Node
mapNodes (\Node
x -> if Node
x Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node]
vars then Node
tau else Node
x) Node
n
  (Node [Edge Symbol
s [Node]
ns']) = Node
nWithVarsRemoved

  pathsForVar :: Node -> [Path]
  pathsForVar :: Node -> [Path]
pathsForVar Node
v = (Node -> Bool) -> Node -> [Path]
pathsMatching (Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
v) Node
n
generalize Node
n = [Char] -> Node
forall a. HasCallStack => [Char] -> a
error ([Char] -> Node) -> [Char] -> Node
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot generalize: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Node -> [Char]
forall a. Show a => a -> [Char]
show Node
n

-- Use of `getPath (path [0, 2]) n1` instead of `tau` effectively pre-computes some reduction.
-- Sometimes this can be desirable, but for enumeration,
app :: Node -> Node -> Node
app :: Node -> Node -> Node
app Node
n1 Node
n2 = [Edge] -> Node
Node
  [ Symbol -> [Node] -> EqConstraints -> Edge
mkEdge
      Symbol
"app"
      [Node
tau, Node
theArrowNode, Node
n1, Node
n2]
      ([[Path]] -> EqConstraints
mkEqConstraints
        [ [[Int] -> Path
path [Int
1], [Int] -> Path
path [Int
2, Int
0, Int
0]]
        , [[Int] -> Path
path [Int
3, Int
0], [Int] -> Path
path [Int
2, Int
0, Int
1]]
        , [[Int] -> Path
path [Int
0], [Int] -> Path
path [Int
2, Int
0, Int
2]]
        ]
      )
  ]

--------------------------------------------------------------------------------
------------------------------- Relevancy Encoding -----------------------------
--------------------------------------------------------------------------------

applyOperator :: Node
applyOperator :: Node
applyOperator = [Edge] -> Node
Node
  [ Symbol -> Node -> Edge
constFunc
    Symbol
"$"
    (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node -> Node
arrowType Node
var1 Node
var2) (Node -> Node -> Node
arrowType Node
var1 Node
var2))
  , Symbol -> Node -> Edge
constFunc Symbol
"id" (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType Node
var1 Node
var1)
  ]

hoogleComps :: [Edge]
hoogleComps :: [Edge]
hoogleComps =
  (Edge -> Bool) -> [Edge] -> [Edge]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (\Edge
e ->
        Edge -> Symbol
edgeSymbol Edge
e
          Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (Text -> Symbol) -> [Text] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> Symbol
Symbol (Text -> Symbol) -> (Text -> Text) -> Text -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
toMappedName) [Text]
speciallyTreatedFunctions
      )
    ([Edge] -> [Edge]) -> [Edge] -> [Edge]
forall a b. (a -> b) -> a -> b
$ ((TypeSkeleton, Text) -> Edge) -> [(TypeSkeleton, Text)] -> [Edge]
forall a b. (a -> b) -> [a] -> [b]
map ((Text -> TypeSkeleton -> Edge) -> (Text, TypeSkeleton) -> Edge
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> TypeSkeleton -> Edge
parseHoogleComponent ((Text, TypeSkeleton) -> Edge)
-> ((TypeSkeleton, Text) -> (Text, TypeSkeleton))
-> (TypeSkeleton, Text)
-> Edge
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeSkeleton, Text) -> (Text, TypeSkeleton)
forall a b. (a, b) -> (b, a)
swap)
    ([(TypeSkeleton, Text)] -> [Edge])
-> [(TypeSkeleton, Text)] -> [Edge]
forall a b. (a -> b) -> a -> b
$ Map TypeSkeleton Text -> [(TypeSkeleton, Text)]
forall k a. Map k a -> [(k, a)]
Map.toList Map TypeSkeleton Text
hoogleComponents

anyFunc :: Node
anyFunc :: Node
anyFunc = [Edge] -> Node
Node [Edge]
hoogleComps

filterType :: Node -> Node -> Node
filterType :: Node -> Node -> Node
filterType Node
n Node
t =
  [Edge] -> Node
Node [Symbol -> [Node] -> EqConstraints -> Edge
mkEdge Symbol
"filter" [Node
t, Node
n] ([[Path]] -> EqConstraints
mkEqConstraints [[[Int] -> Path
path [Int
0], [Int] -> Path
path [Int
1, Int
0]]])]

termsK :: Node -> Bool -> Int -> [Node]
termsK :: Node -> Bool -> Int -> [Node]
termsK Node
_      Bool
_     Int
0 = []
termsK Node
anyArg Bool
False Int
1 = [Node
anyArg, Node
anyFunc]
termsK Node
anyArg Bool
True  Int
1 = [Node
anyArg, Node
anyFunc, Node
applyOperator]
termsK Node
anyArg Bool
_ Int
2 =
  [ Node -> Node -> Node
app Node
anyListFunc ([Node] -> Node
union [Node
anyNonNilFunc, Node
anyArg, Node
applyOperator])
  , Node -> Node -> Node
app Node
fromJustFunc ([Node] -> Node
union [Node
anyNonNothingFunc, Node
anyArg, Node
applyOperator])
  , Node -> Node -> Node
app ([Node] -> Node
union [Node
anyNonListFunc, Node
anyArg]) ([Node] -> Node
union (Node -> Bool -> Int -> [Node]
termsK Node
anyArg Bool
True Int
1))
  ]
termsK Node
anyArg Bool
_ Int
k = (Int -> Node) -> [Int] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Node
constructApp [Int
1 .. (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
 where
  constructApp :: Int -> Node
  constructApp :: Int -> Node
constructApp Int
i =
    Node -> Node -> Node
app ([Node] -> Node
union (Node -> Bool -> Int -> [Node]
termsK Node
anyArg Bool
False Int
i)) ([Node] -> Node
union (Node -> Bool -> Int -> [Node]
termsK Node
anyArg Bool
True (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i)))

relevantTermK :: Node -> Bool -> Int -> [Argument] -> [Node]
relevantTermK :: Node -> Bool -> Int -> [Argument] -> [Node]
relevantTermK Node
anyArg Bool
includeApplyOp Int
k []       = Node -> Bool -> Int -> [Node]
termsK Node
anyArg Bool
includeApplyOp Int
k
relevantTermK Node
_      Bool
_              Int
1 [(Symbol
x, Node
t)] = [[Edge] -> Node
Node [Symbol -> Node -> Edge
constArg Symbol
x Node
t]]
relevantTermK Node
anyArg Bool
_ Int
k [Argument]
argNames
  | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Argument] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Argument]
argNames = []
  | Bool
otherwise = (Int -> [Node]) -> [Int] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Int
i -> (([Argument], [Argument]) -> Node)
-> [([Argument], [Argument])] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> ([Argument], [Argument]) -> Node
constructApp Int
i) [([Argument], [Argument])]
allSplits) [Int
1 .. (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
 where
  allSplits :: [([Argument], [Argument])]
allSplits = (Int -> ([Argument], [Argument]))
-> [Int] -> [([Argument], [Argument])]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [Argument] -> ([Argument], [Argument])
forall a. Int -> [a] -> ([a], [a])
`splitAt` [Argument]
argNames) [Int
0 .. ([Argument] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Argument]
argNames)]

  constructApp :: Int -> ([Argument], [Argument]) -> Node
  constructApp :: Int -> ([Argument], [Argument]) -> Node
constructApp Int
i ([Argument]
xs, [Argument]
ys) =
    let f :: Node
f = [Node] -> Node
union (Node -> Bool -> Int -> [Argument] -> [Node]
relevantTermK Node
anyArg Bool
False Int
i [Argument]
xs)
        x :: Node
x = [Node] -> Node
union (Node -> Bool -> Int -> [Argument] -> [Node]
relevantTermK Node
anyArg Bool
True (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) [Argument]
ys)
    in  Node -> Node -> Node
app Node
f Node
x

relevantTermsOfSize :: Node -> [Argument] -> Int -> Node
relevantTermsOfSize :: Node -> [Argument] -> Int -> Node
relevantTermsOfSize Node
anyArg [Argument]
args Int
k = [Node] -> Node
union ([Node] -> Node) -> [Node] -> Node
forall a b. (a -> b) -> a -> b
$ ([Argument] -> [Node]) -> [[Argument]] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Node -> Bool -> Int -> [Argument] -> [Node]
relevantTermK Node
anyArg Bool
True Int
k) ([Argument] -> [[Argument]]
forall a. [a] -> [[a]]
permutations [Argument]
args)

relevantTermsUptoK :: Node -> [Argument] -> Int -> Node
relevantTermsUptoK :: Node -> [Argument] -> Int -> Node
relevantTermsUptoK Node
anyArg [Argument]
args Int
k = [Node] -> Node
union ((Int -> Node) -> [Int] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (Node -> [Argument] -> Int -> Node
relevantTermsOfSize Node
anyArg [Argument]
args) [Int
1 .. Int
k])

prettyTerm :: Term -> Term
prettyTerm :: Term -> Term
prettyTerm (Term Symbol
"app" [Term]
ns) = Symbol -> [Term] -> Term
Term
  Symbol
"app"
  [Term -> Term
prettyTerm ([Term]
ns [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ns Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)), Term -> Term
prettyTerm ([Term]
ns [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ns Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))]
prettyTerm (Term Symbol
"filter" [Term]
ns) = Term -> Term
prettyTerm ([Term] -> Term
forall a. [a] -> a
last [Term]
ns)
prettyTerm (Term Symbol
s        [Term]
_ ) = Symbol -> [Term] -> Term
Term Symbol
s []

dropTypes :: Node -> Node
dropTypes :: Node -> Node
dropTypes (Node [Edge]
es) = [Edge] -> Node
Node ((Edge -> Edge) -> [Edge] -> [Edge]
forall a b. (a -> b) -> [a] -> [b]
map Edge -> Edge
dropEdgeTypes [Edge]
es)
 where
  dropEdgeTypes :: Edge -> Edge
dropEdgeTypes (Edge Symbol
"app" [Node
_, Node
_, Node
a, Node
b]) =
    Symbol -> [Node] -> Edge
Edge Symbol
"app" [Node -> Node
dropTypes Node
a, Node -> Node
dropTypes Node
b]
  dropEdgeTypes (Edge Symbol
"filter" [Node
_, Node
a]) = Symbol -> [Node] -> Edge
Edge Symbol
"filter" [Node -> Node
dropTypes Node
a]
  dropEdgeTypes (Edge Symbol
s        [Node
_]   ) = Symbol -> [Node] -> Edge
Edge Symbol
s []
  dropEdgeTypes Edge
e                      = Edge
e
dropTypes Node
n = Node
n

getText :: Symbol -> Text
getText :: Symbol -> Text
getText (Symbol Text
s) = Text
s

--------------------------
-------- Remove uninteresting terms
--------------------------

fromJustFunc :: Node
fromJustFunc :: Node
fromJustFunc =
  [Edge] -> Node
Node ([Edge] -> Node) -> [Edge] -> Node
forall a b. (a -> b) -> a -> b
$ (Edge -> Bool) -> [Edge] -> [Edge]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Edge
e -> Edge -> Symbol
edgeSymbol Edge
e Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
maybeFunctions) [Edge]
hoogleComps

maybeFunctions :: [Symbol]
maybeFunctions :: [Symbol]
maybeFunctions =
  [ Symbol
"Data.Maybe.fromJust"
  , Symbol
"Data.Maybe.maybeToList"
  , Symbol
"Data.Maybe.isJust"
  , Symbol
"Data.Maybe.isNothing"
  ]

listReps :: [Text]
listReps :: [Text]
listReps = (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map
  Text -> Text
toMappedName
  [ Text
"Data.Maybe.listToMaybe"
  , Text
"Data.Either.lefts"
  , Text
"Data.Either.rights"
  , Text
"Data.Either.partitionEithers"
  , Text
"Data.Maybe.catMaybes"
  , Text
"GHC.List.head"
  , Text
"GHC.List.last"
  , Text
"GHC.List.tail"
  , Text
"GHC.List.init"
  , Text
"GHC.List.null"
  , Text
"GHC.List.length"
  , Text
"GHC.List.reverse"
  , Text
"GHC.List.concat"
  , Text
"GHC.List.concatMap"
  , Text
"GHC.List.sum"
  , Text
"GHC.List.product"
  , Text
"GHC.List.maximum"
  , Text
"GHC.List.minimum"
  , Text
"(GHC.List.!!)"
  , Text
"(GHC.List.++)"
  ]

isListFunction :: Symbol -> Bool
isListFunction :: Symbol -> Bool
isListFunction (Symbol Text
sym) = Text
sym Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
listReps

maybeReps :: [Text]
maybeReps :: [Text]
maybeReps = (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map
  Text -> Text
toMappedName
  [ Text
"Data.Maybe.maybeToList"
  , Text
"Data.Maybe.isJust"
  , Text
"Data.Maybe.isNothing"
  , Text
"Data.Maybe.fromJust"
  ]

isMaybeFunction :: Symbol -> Bool
isMaybeFunction :: Symbol -> Bool
isMaybeFunction (Symbol Text
sym) = Text
sym Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
maybeReps

anyListFunc :: Node
anyListFunc :: Node
anyListFunc = [Edge] -> Node
Node ([Edge] -> Node) -> [Edge] -> Node
forall a b. (a -> b) -> a -> b
$ (Edge -> Bool) -> [Edge] -> [Edge]
forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol -> Bool
isListFunction (Symbol -> Bool) -> (Edge -> Symbol) -> Edge -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Edge -> Symbol
edgeSymbol) [Edge]
hoogleComps

anyNonListFunc :: Node
anyNonListFunc :: Node
anyNonListFunc = [Edge] -> Node
Node ([Edge] -> Node) -> [Edge] -> Node
forall a b. (a -> b) -> a -> b
$ (Edge -> Bool) -> [Edge] -> [Edge]
forall a. (a -> Bool) -> [a] -> [a]
filter
  (\Edge
e -> Bool -> Bool
not (Symbol -> Bool
isListFunction (Edge -> Symbol
edgeSymbol Edge
e))
    Bool -> Bool -> Bool
&& Bool -> Bool
not (Symbol -> Bool
isMaybeFunction (Edge -> Symbol
edgeSymbol Edge
e))
  )
  [Edge]
hoogleComps

anyNonNilFunc :: Node
anyNonNilFunc :: Node
anyNonNilFunc =
  [Edge] -> Node
Node ([Edge] -> Node) -> [Edge] -> Node
forall a b. (a -> b) -> a -> b
$ (Edge -> Bool) -> [Edge] -> [Edge]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Edge
e -> Edge -> Symbol
edgeSymbol Edge
e Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Text -> Symbol
Symbol (Text -> Text
toMappedName Text
"Nil")) [Edge]
hoogleComps

anyNonNothingFunc :: Node
anyNonNothingFunc :: Node
anyNonNothingFunc = [Edge] -> Node
Node ([Edge] -> Node) -> [Edge] -> Node
forall a b. (a -> b) -> a -> b
$ (Edge -> Bool) -> [Edge] -> [Edge]
forall a. (a -> Bool) -> [a] -> [a]
filter
  (\Edge
e -> Edge -> Symbol
edgeSymbol Edge
e Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Text -> Symbol
Symbol (Text -> Text
toMappedName Text
"Data.Maybe.Nothing"))
  [Edge]
hoogleComps

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

reduceFully :: Node -> Node
reduceFully :: Node -> Node
reduceFully = (Node -> Node) -> Node -> Node
forall a. Eq a => (a -> a) -> a -> a
fixUnbounded (Node -> Node
withoutRedundantEdges (Node -> Node) -> (Node -> Node) -> Node -> Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Node
reducePartially)
-- reduceFully = fixUnbounded (reducePartially)

checkSolution :: Term -> [Term] -> IO ()
checkSolution :: Term -> [Term] -> IO ()
checkSolution Term
_ [] = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkSolution Term
target (Term
s : [Term]
solutions)
  | Term -> Term
prettyTerm Term
s Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
target = Text -> IO ()
forall a. Show a => a -> IO ()
print (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Term -> Text
forall a. Pretty a => a -> Text
pretty (Term -> Term
prettyTerm Term
s)
  | Bool
otherwise = do
    -- print $ pretty (prettyTerm s)
    -- print (s)
    Term -> [Term] -> IO ()
checkSolution Term
target [Term]
solutions

reduceFullyAndLog :: Node -> IO Node
reduceFullyAndLog :: Node -> IO Node
reduceFullyAndLog = Int -> Node -> IO Node
go Int
0
 where
  go :: Int -> Node -> IO Node
  go :: Int -> Node -> IO Node
go Int
i Node
n = do
    [Char] -> IO ()
putStrLn
      ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$  [Char]
"Round "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Node -> Int
nodeCount Node
n)
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" nodes, "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Node -> Int
edgeCount Node
n)
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" edges"
    Handle -> IO ()
hFlush Handle
stdout
    -- putStrLn $ renderDot $ toDot n
    -- print n
    let n' :: Node
n' = Node -> Node
withoutRedundantEdges (Node -> Node
reducePartially Node
n)
    if Node
n Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
n' Bool -> Bool -> Bool
|| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
30 then Node -> IO Node
forall (m :: * -> *) a. Monad m => a -> m a
return Node
n else Int -> Node -> IO Node
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Node
n'

--------------------------------------------------------------------------------
--------------------------------- Test Functions -------------------------------
--------------------------------------------------------------------------------

f1 :: Edge
f1 :: Edge
f1 = Symbol -> Node -> Edge
constFunc Symbol
"Nothing" (Node -> Node
maybeType Node
tau)

f2 :: Edge
f2 :: Edge
f2 = Symbol -> Node -> Edge
constFunc Symbol
"Just" (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType Node
var1 (Node -> Node
maybeType Node
var1))

f3 :: Edge
f3 :: Edge
f3 = Symbol -> Node -> Edge
constFunc
  Symbol
"fromMaybe"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType Node
var1 (Node -> Node -> Node
arrowType (Node -> Node
maybeType Node
var1) Node
var1))

f4 :: Edge
f4 :: Edge
f4 = Symbol -> Node -> Edge
constFunc Symbol
"listToMaybe"
               (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node
listType Node
var1) (Node -> Node
maybeType Node
var1))

f5 :: Edge
f5 :: Edge
f5 = Symbol -> Node -> Edge
constFunc Symbol
"maybeToList"
               (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node
maybeType Node
var1) (Node -> Node
listType Node
var1))

f6 :: Edge
f6 :: Edge
f6 = Symbol -> Node -> Edge
constFunc
  Symbol
"catMaybes"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node
listType (Node -> Node
maybeType Node
var1)) (Node -> Node
listType Node
var1))

f7 :: Edge
f7 :: Edge
f7 = Symbol -> Node -> Edge
constFunc
  Symbol
"mapMaybe"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node -> Node
arrowType Node
var1 (Node -> Node
maybeType Node
var2))
                          (Node -> Node -> Node
arrowType (Node -> Node
listType Node
var1) (Node -> Node
listType Node
var2))
  )

f8 :: Edge
f8 :: Edge
f8 = Symbol -> Node -> Edge
constFunc Symbol
"id" (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType Node
var1 Node
var1)

f9 :: Edge
f9 :: Edge
f9 = Symbol -> Node -> Edge
constFunc
  Symbol
"replicate"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Text -> Node
constrType0 Text
"Int") (Node -> Node -> Node
arrowType Node
var1 (Node -> Node
listType Node
var1)))

f10 :: Edge
f10 :: Edge
f10 = Symbol -> Node -> Edge
constFunc
  Symbol
"foldr"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node -> Node
arrowType Node
var1 (Node -> Node -> Node
arrowType Node
var2 Node
var2))
                          (Node -> Node -> Node
arrowType Node
var2 (Node -> Node -> Node
arrowType (Node -> Node
listType Node
var1) Node
var2))
  )

f11 :: Edge
f11 :: Edge
f11 = Symbol -> Node -> Edge
constFunc
  Symbol
"iterate"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node -> Node
arrowType Node
var1 Node
var1) (Node -> Node -> Node
arrowType Node
var1 (Node -> Node
listType Node
var1))
  )

f12 :: Edge
f12 :: Edge
f12 = Symbol -> Node -> Edge
constFunc
  Symbol
"(!!)"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node
listType Node
var1) (Node -> Node -> Node
arrowType (Text -> Node
constrType0 Text
"Int") Node
var1))

f13 :: Edge
f13 :: Edge
f13 = Symbol -> Node -> Edge
constFunc
  Symbol
"either"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType
    (Node -> Node -> Node
arrowType Node
var1 Node
var3)
    (Node -> Node -> Node
arrowType (Node -> Node -> Node
arrowType Node
var2 Node
var3)
               (Node -> Node -> Node
arrowType (Text -> Node -> Node -> Node
constrType2 Text
"Either" Node
var1 Node
var2) Node
var3)
    )
  )

f14 :: Edge
f14 :: Edge
f14 = Symbol -> Node -> Edge
constFunc
  Symbol
"Left"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType Node
var1 (Text -> Node -> Node -> Node
constrType2 Text
"Either" Node
var1 Node
var2))

f15 :: Edge
f15 :: Edge
f15 = Symbol -> Node -> Edge
constFunc Symbol
"id" (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType Node
var1 Node
var1)

f16 :: Edge
f16 :: Edge
f16 = Symbol -> Node -> Edge
constFunc
  Symbol
"(,)"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType Node
var1 (Node -> Node -> Node
arrowType Node
var2 (Text -> Node -> Node -> Node
constrType2 Text
"Pair" Node
var1 Node
var2)))

f17 :: Edge
f17 :: Edge
f17 =
  Symbol -> Node -> Edge
constFunc Symbol
"fst" (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Text -> Node -> Node -> Node
constrType2 Text
"Pair" Node
var1 Node
var2) Node
var1)

f18 :: Edge
f18 :: Edge
f18 =
  Symbol -> Node -> Edge
constFunc Symbol
"snd" (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Text -> Node -> Node -> Node
constrType2 Text
"Pair" Node
var1 Node
var2) Node
var2)

f19 :: Edge
f19 :: Edge
f19 = Symbol -> Node -> Edge
constFunc
  Symbol
"foldl"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node -> Node
arrowType Node
var2 (Node -> Node -> Node
arrowType Node
var1 Node
var2))
                          (Node -> Node -> Node
arrowType Node
var2 (Node -> Node -> Node
arrowType (Node -> Node
listType Node
var1) Node
var2))
  )

f20 :: Edge
f20 :: Edge
f20 = Symbol -> Node -> Edge
constFunc
  Symbol
"swap"
  ( Node -> Node
generalize
  (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Text -> Node -> Node -> Node
constrType2 Text
"Pair" Node
var1 Node
var2) (Text -> Node -> Node -> Node
constrType2 Text
"Pair" Node
var2 Node
var1)
  )

f21 :: Edge
f21 :: Edge
f21 = Symbol -> Node -> Edge
constFunc
  Symbol
"curry"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node -> Node
arrowType (Text -> Node -> Node -> Node
constrType2 Text
"Pair" Node
var1 Node
var2) Node
var3)
                          (Node -> Node -> Node
arrowType Node
var1 (Node -> Node -> Node
arrowType Node
var2 Node
var3))
  )

f22 :: Edge
f22 :: Edge
f22 = Symbol -> Node -> Edge
constFunc
  Symbol
"uncurry"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node -> Node
arrowType Node
var1 (Node -> Node -> Node
arrowType Node
var2 Node
var3))
                          (Node -> Node -> Node
arrowType (Text -> Node -> Node -> Node
constrType2 Text
"Pair" Node
var1 Node
var2) Node
var3)
  )

f23 :: Edge
f23 :: Edge
f23 = Symbol -> Node -> Edge
constFunc Symbol
"head" (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node
listType Node
var1) Node
var1)

f24 :: Edge
f24 :: Edge
f24 = Symbol -> Node -> Edge
constFunc Symbol
"last" (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType (Node -> Node
listType Node
var1) Node
var1)

f25 :: Edge
f25 :: Edge
f25 = Symbol -> Node -> Edge
constFunc
  Symbol
"Data.ByteString.foldr"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType
    (Node -> Node -> Node
arrowType (Text -> Node
constrType0 Text
"Word8") (Node -> Node -> Node
arrowType Node
var2 Node
var2))
    (Node -> Node -> Node
arrowType Node
var2 (Node -> Node -> Node
arrowType (Text -> Node
constrType0 Text
"ByteString") Node
var2))
  )

f26 :: Edge
f26 :: Edge
f26 = Symbol -> Node -> Edge
constFunc
  Symbol
"unfoldr"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType
    (Node -> Node -> Node
arrowType Node
var1 (Node -> Node
maybeType (Text -> Node -> Node -> Node
constrType2 Text
"Pair" (Text -> Node
constrType0 Text
"Word8") Node
var1)))
    (Node -> Node -> Node
arrowType Node
var1 (Text -> Node
constrType0 Text
"ByteString"))
  )

f27 :: Edge
f27 :: Edge
f27 = Symbol -> Node -> Edge
constFunc
  Symbol
"Data.ByteString.foldrChunks"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType
    (Node -> Node -> Node
arrowType (Text -> Node
constrType0 Text
"ByteString") (Node -> Node -> Node
arrowType Node
var2 Node
var2))
    (Node -> Node -> Node
arrowType Node
var2 (Node -> Node -> Node
arrowType (Text -> Node
constrType0 Text
"ByteString") Node
var2))
  )

f28 :: Edge
f28 :: Edge
f28 = Symbol -> Node -> Edge
constFunc
  Symbol
"bool"
  ( Node -> Node
generalize
  (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType Node
var1 (Node -> Node -> Node
arrowType Node
var1 (Node -> Node -> Node
arrowType (Text -> Node
constrType0 Text
"Bool") Node
var1))
  )

f29 :: Edge
f29 :: Edge
f29 = Symbol -> Node -> Edge
constFunc
  Symbol
"lookup"
  (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
arrowType
    (Text -> Node -> Node
constrType1 Text
"@@hplusTC@@Eq" Node
var1)
    (Node -> Node -> Node
arrowType Node
var1 (Node -> Node -> Node
arrowType (Text -> Node -> Node -> Node
constrType2 Text
"Pair" Node
var1 Node
var2) (Node -> Node
maybeType Node
var2)))
  )

f30 :: Edge
f30 :: Edge
f30 = Symbol -> Node -> Edge
constFunc Symbol
"nil" (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node
listType Node
var1)

--------------------------
------ Util functions
--------------------------

toMappedName :: Text -> Text
toMappedName :: Text -> Text
toMappedName Text
x = Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
x (Text -> Map Text Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
x Map Text Text
groupMapping)

prettyPrintAllTerms :: AblationType -> Term -> Node -> IO ()
prettyPrintAllTerms :: AblationType -> Term -> Node -> IO ()
prettyPrintAllTerms AblationType
ablation Term
sol Node
n = do
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Expected: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show (Term -> Text
forall a. Pretty a => a -> Text
pretty Term
sol)
  let ts :: [Term]
ts = case AblationType
ablation of
             AblationType
NoEnumeration -> Node -> [Term]
naiveDenotation Node
n
             AblationType
NoOptimize    -> Node -> [Term]
naiveDenotation Node
n
             AblationType
_             -> Node -> [Term]
getAllTerms Node
n
  Term -> [Term] -> IO ()
checkSolution Term
sol [Term]
ts

substTerm :: Term -> Term
substTerm :: Term -> Term
substTerm (Term (Symbol Text
sym) [Term]
ts) =
  Symbol -> [Term] -> Term
Term (Text -> Symbol
Symbol (Text -> Symbol) -> Text -> Symbol
forall a b. (a -> b) -> a -> b
$ Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
sym (Text -> Map Text Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
sym Map Text Text
groupMapping)) ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
substTerm [Term]
ts)

parseHoogleComponent :: Text -> TypeSkeleton -> Edge
parseHoogleComponent :: Text -> TypeSkeleton -> Edge
parseHoogleComponent Text
name TypeSkeleton
t =
  Symbol -> Node -> Edge
constFunc (Text -> Symbol
Symbol Text
name) (Node -> Node
generalize (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ TypeSkeleton -> Node
typeToFta TypeSkeleton
t)