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