{-# 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
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]]
]
)
]
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
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)
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
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
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'
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)
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)