module Disco.Compile where
import Control.Monad ((<=<))
import Data.Bool (bool)
import Data.Coerce
import qualified Data.Map as M
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as S
import Data.Set.Lens (setOf)
import Disco.Effects.Fresh
import Polysemy (Member, Sem, run)
import Unbound.Generics.LocallyNameless (Name, bind, string2Name,
unembed)
import Disco.AST.Core
import Disco.AST.Desugared
import Disco.AST.Generic
import Disco.AST.Typed
import Disco.Context as Ctx
import Disco.Desugar
import Disco.Module
import Disco.Names
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import qualified Disco.Typecheck.Graph as G
import Disco.Types
import Disco.Util
compileThing :: (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing :: (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing a -> Sem '[Fresh] DTerm
desugarThing = Sem '[] Core -> Core
forall a. Sem '[] a -> a
run (Sem '[] Core -> Core) -> (a -> Sem '[] Core) -> a -> Core
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem '[Fresh] Core -> Sem '[] Core
forall (r :: [(* -> *) -> * -> *]) a. Sem (Fresh : r) a -> Sem r a
runFresh (Sem '[Fresh] Core -> Sem '[] Core)
-> (a -> Sem '[Fresh] Core) -> a -> Sem '[] Core
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DTerm -> Sem '[Fresh] Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm (DTerm -> Sem '[Fresh] Core)
-> (a -> Sem '[Fresh] DTerm) -> a -> Sem '[Fresh] Core
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< a -> Sem '[Fresh] DTerm
desugarThing)
compileTerm :: ATerm -> Core
compileTerm :: ATerm -> Core
compileTerm = (ATerm -> Sem '[Fresh] DTerm) -> ATerm -> Core
forall a. (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing ATerm -> Sem '[Fresh] DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm
compileProperty :: AProperty -> Core
compileProperty :: ATerm -> Core
compileProperty = (ATerm -> Sem '[Fresh] DTerm) -> ATerm -> Core
forall a. (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing ATerm -> Sem '[Fresh] DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarProperty
compileDefns :: Ctx ATerm Defn -> [(QName Core, Core)]
compileDefns :: Ctx ATerm Defn -> [(QName Core, Core)]
compileDefns Ctx ATerm Defn
defs = Sem '[] [(QName Core, Core)] -> [(QName Core, Core)]
forall a. Sem '[] a -> a
run (Sem '[] [(QName Core, Core)] -> [(QName Core, Core)])
-> (Sem '[Fresh] [(QName Core, Core)]
-> Sem '[] [(QName Core, Core)])
-> Sem '[Fresh] [(QName Core, Core)]
-> [(QName Core, Core)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem '[Fresh] [(QName Core, Core)] -> Sem '[] [(QName Core, Core)]
forall (r :: [(* -> *) -> * -> *]) a. Sem (Fresh : r) a -> Sem r a
runFresh (Sem '[Fresh] [(QName Core, Core)] -> [(QName Core, Core)])
-> Sem '[Fresh] [(QName Core, Core)] -> [(QName Core, Core)]
forall a b. (a -> b) -> a -> b
$ do
let vars :: Set (QName ATerm)
vars = Ctx ATerm Defn -> Set (QName ATerm)
forall a b. Ctx a b -> Set (QName a)
Ctx.keysSet Ctx ATerm Defn
defs
deps :: Set (QName ATerm, QName ATerm)
deps :: Set (QName ATerm, QName ATerm)
deps = [Set (QName ATerm, QName ATerm)] -> Set (QName ATerm, QName ATerm)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set (QName ATerm, QName ATerm)]
-> Set (QName ATerm, QName ATerm))
-> (Ctx ATerm Defn -> [Set (QName ATerm, QName ATerm)])
-> Ctx ATerm Defn
-> Set (QName ATerm, QName ATerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName ATerm, Defn) -> Set (QName ATerm, QName ATerm))
-> [(QName ATerm, Defn)] -> [Set (QName ATerm, QName ATerm)]
forall a b. (a -> b) -> [a] -> [b]
map (\(QName ATerm
x, Defn
body) -> (QName ATerm -> (QName ATerm, QName ATerm))
-> Set (QName ATerm) -> Set (QName ATerm, QName ATerm)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (,QName ATerm
x) (Getting (Set (QName ATerm)) Defn (QName ATerm)
-> Defn -> Set (QName ATerm)
forall a s. Getting (Set a) s a -> s -> Set a
setOf ((Data Defn, Typeable ATerm) => Traversal' Defn (QName ATerm)
forall t e. (Data t, Typeable e) => Traversal' t (QName e)
fvQ @Defn @ATerm) Defn
body)) ([(QName ATerm, Defn)] -> [Set (QName ATerm, QName ATerm)])
-> (Ctx ATerm Defn -> [(QName ATerm, Defn)])
-> Ctx ATerm Defn
-> [Set (QName ATerm, QName ATerm)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx ATerm Defn -> [(QName ATerm, Defn)]
forall a b. Ctx a b -> [(QName a, b)]
Ctx.assocs (Ctx ATerm Defn -> Set (QName ATerm, QName ATerm))
-> Ctx ATerm Defn -> Set (QName ATerm, QName ATerm)
forall a b. (a -> b) -> a -> b
$ Ctx ATerm Defn
defs
defnGroups :: [Set (QName ATerm)]
defnGroups :: [Set (QName ATerm)]
defnGroups = Graph (Set (QName ATerm)) -> [Set (QName ATerm)]
forall a. Graph a -> [a]
G.topsort (Graph (QName ATerm) -> Graph (Set (QName ATerm))
forall a. Ord a => Graph a -> Graph (Set a)
G.condensation (Set (QName ATerm)
-> Set (QName ATerm, QName ATerm) -> Graph (QName ATerm)
forall a. (Show a, Ord a) => Set a -> Set (a, a) -> Graph a
G.mkGraph Set (QName ATerm)
vars Set (QName ATerm, QName ATerm)
deps))
[[(QName Core, Core)]] -> [(QName Core, Core)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(QName Core, Core)]] -> [(QName Core, Core)])
-> Sem '[Fresh] [[(QName Core, Core)]]
-> Sem '[Fresh] [(QName Core, Core)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set (QName ATerm) -> Sem '[Fresh] [(QName Core, Core)])
-> [Set (QName ATerm)] -> Sem '[Fresh] [[(QName Core, Core)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([(QName ATerm, Defn)] -> Sem '[Fresh] [(QName Core, Core)]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[(QName ATerm, Defn)] -> Sem r [(QName Core, Core)]
compileDefnGroup ([(QName ATerm, Defn)] -> Sem '[Fresh] [(QName Core, Core)])
-> (Set (QName ATerm) -> [(QName ATerm, Defn)])
-> Set (QName ATerm)
-> Sem '[Fresh] [(QName Core, Core)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx ATerm Defn -> [(QName ATerm, Defn)]
forall a b. Ctx a b -> [(QName a, b)]
Ctx.assocs (Ctx ATerm Defn -> [(QName ATerm, Defn)])
-> (Set (QName ATerm) -> Ctx ATerm Defn)
-> Set (QName ATerm)
-> [(QName ATerm, Defn)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx ATerm Defn -> Set (QName ATerm) -> Ctx ATerm Defn
forall a b. Ctx a b -> Set (QName a) -> Ctx a b
Ctx.restrictKeys Ctx ATerm Defn
defs) [Set (QName ATerm)]
defnGroups
compileDefnGroup :: Member Fresh r => [(QName ATerm, Defn)] -> Sem r [(QName Core, Core)]
compileDefnGroup :: [(QName ATerm, Defn)] -> Sem r [(QName Core, Core)]
compileDefnGroup [(QName ATerm
f, Defn
defn)]
| QName ATerm
f QName ATerm -> Set (QName ATerm) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Getting (Set (QName ATerm)) Defn (QName ATerm)
-> Defn -> Set (QName ATerm)
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set (QName ATerm)) Defn (QName ATerm)
forall t e. (Data t, Typeable e) => Traversal' t (QName e)
fvQ Defn
defn = [(QName Core, Core)] -> Sem r [(QName Core, Core)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(QName Core, Core)] -> Sem r [(QName Core, Core)])
-> ((QName Core, Core) -> [(QName Core, Core)])
-> (QName Core, Core)
-> Sem r [(QName Core, Core)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName Core, Core) -> [(QName Core, Core)] -> [(QName Core, Core)]
forall a. a -> [a] -> [a]
:[]) ((QName Core, Core) -> Sem r [(QName Core, Core)])
-> (QName Core, Core) -> Sem r [(QName Core, Core)]
forall a b. (a -> b) -> a -> b
$
(QName Core
fT, Core -> Core
CForce (Side -> Core -> Core
CProj Side
L (Bind [Name Core] [Core] -> Core
CDelay ([Name Core] -> [Core] -> Bind [Name Core] [Core]
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [QName Core -> Name Core
forall a. QName a -> Name a
qname QName Core
fL] [QName Core -> Core -> Core -> Core
substQC QName Core
fT (Core -> Core
CForce (QName Core -> Core
CVar QName Core
fL)) Core
cdefn]))))
| Bool
otherwise =
[(QName Core, Core)] -> Sem r [(QName Core, Core)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(QName Core
fT, Core
cdefn)]
where
fT, fL :: QName Core
fT :: QName Core
fT = QName ATerm -> QName Core
coerce QName ATerm
f
fL :: QName Core
fL = Name Core -> QName Core
forall a. Name a -> QName a
localName (Name ATerm -> Name Core
coerce (QName ATerm -> Name ATerm
forall a. QName a -> Name a
qname QName ATerm
f))
cdefn :: Core
cdefn = (Defn -> Sem '[Fresh] DTerm) -> Defn -> Core
forall a. (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing Defn -> Sem '[Fresh] DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Defn -> Sem r DTerm
desugarDefn Defn
defn
compileDefnGroup [(QName ATerm, Defn)]
defs = do
QName Core
grp :: QName Core <- String -> Sem r (QName Core)
forall (r :: [(* -> *) -> * -> *]) a.
Member Fresh r =>
String -> Sem r (QName a)
freshQ String
"__grp"
let ([QName ATerm]
vars, [Defn]
bodies) = [(QName ATerm, Defn)] -> ([QName ATerm], [Defn])
forall a b. [(a, b)] -> ([a], [b])
unzip [(QName ATerm, Defn)]
defs
varsT, varsL :: [QName Core]
varsT :: [QName Core]
varsT = [QName ATerm] -> [QName Core]
coerce [QName ATerm]
vars
varsL :: [QName Core]
varsL = (QName Core -> QName Core) -> [QName Core] -> [QName Core]
forall a b. (a -> b) -> [a] -> [b]
map (Name Core -> QName Core
forall a. Name a -> QName a
localName (Name Core -> QName Core)
-> (QName Core -> Name Core) -> QName Core -> QName Core
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName Core -> Name Core
forall a. QName a -> Name a
qname) [QName Core]
varsT
forceVars :: [(QName Core, Core)]
forceVars :: [(QName Core, Core)]
forceVars = (QName Core -> QName Core -> (QName Core, Core))
-> [QName Core] -> [QName Core] -> [(QName Core, Core)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\QName Core
t QName Core
l -> (QName Core
t, Core -> Core
CForce (QName Core -> Core
CVar QName Core
l))) [QName Core]
varsT [QName Core]
varsL
bodies' :: [Core]
bodies' :: [Core]
bodies' = (Defn -> Core) -> [Defn] -> [Core]
forall a b. (a -> b) -> [a] -> [b]
map ([(QName Core, Core)] -> Core -> Core
substsQC [(QName Core, Core)]
forceVars (Core -> Core) -> (Defn -> Core) -> Defn -> Core
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Sem '[Fresh] DTerm) -> Defn -> Core
forall a. (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing Defn -> Sem '[Fresh] DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Defn -> Sem r DTerm
desugarDefn) [Defn]
bodies
[(QName Core, Core)] -> Sem r [(QName Core, Core)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(QName Core, Core)] -> Sem r [(QName Core, Core)])
-> [(QName Core, Core)] -> Sem r [(QName Core, Core)]
forall a b. (a -> b) -> a -> b
$
(QName Core
grp, Bind [Name Core] [Core] -> Core
CDelay ([Name Core] -> [Core] -> Bind [Name Core] [Core]
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ((QName Core -> Name Core) -> [QName Core] -> [Name Core]
forall a b. (a -> b) -> [a] -> [b]
map QName Core -> Name Core
forall a. QName a -> Name a
qname [QName Core]
varsL) [Core]
bodies')) (QName Core, Core) -> [(QName Core, Core)] -> [(QName Core, Core)]
forall a. a -> [a] -> [a]
:
[QName Core] -> [Core] -> [(QName Core, Core)]
forall a b. [a] -> [b] -> [(a, b)]
zip [QName Core]
varsT ([Int] -> (Int -> Core) -> [Core]
forall a b. [a] -> (a -> b) -> [b]
for [Int
0 ..] ((Int -> Core) -> [Core]) -> (Int -> Core) -> [Core]
forall a b. (a -> b) -> a -> b
$ Core -> Core
CForce (Core -> Core) -> (Int -> Core) -> Int -> Core
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Core -> Core) -> Core -> Int -> Core
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Core -> Core
proj (QName Core -> Core
CVar QName Core
grp))
where
proj :: Int -> Core -> Core
proj :: Int -> Core -> Core
proj Int
0 = Side -> Core -> Core
CProj Side
L
proj Int
n = Int -> Core -> Core
proj (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Core -> Core) -> (Core -> Core) -> Core -> Core
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Core -> Core
CProj Side
R
compileDTerm :: Member Fresh r => DTerm -> Sem r Core
compileDTerm :: DTerm -> Sem r Core
compileDTerm (DTVar Type
_ QName DTerm
x) = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ QName Core -> Core
CVar (QName DTerm -> QName Core
coerce QName DTerm
x)
compileDTerm (DTPrim Type
ty Prim
x) = Type -> Prim -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Prim -> Sem r Core
compilePrim Type
ty Prim
x
compileDTerm DTerm
DTUnit = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return Core
CUnit
compileDTerm (DTBool Type
_ Bool
b) = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Side -> Core -> Core
CInj (Side -> Side -> Bool -> Side
forall a. a -> a -> Bool -> a
bool Side
L Side
R Bool
b) Core
CUnit
compileDTerm (DTChar Char
c) = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ RationalDisplay -> Rational -> Core
CNum RationalDisplay
Fraction (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1)
compileDTerm (DTNat Type
_ Integer
n) = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ RationalDisplay -> Rational -> Core
CNum RationalDisplay
Fraction (Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1)
compileDTerm (DTRat Rational
r) = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ RationalDisplay -> Rational -> Core
CNum RationalDisplay
Decimal Rational
r
compileDTerm term :: DTerm
term@(DTAbs Quantifier
q Type
_ Bind (Name DTerm) DTerm
_) = do
([Name DTerm]
xs, [Type]
tys, DTerm
body) <- DTerm -> Sem r ([Name DTerm], [Type], DTerm)
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r ([Name DTerm], [Type], DTerm)
unbindDeep DTerm
term
Core
cbody <- DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
body
case Quantifier
q of
Quantifier
Lam -> Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ [Name DTerm] -> Core -> Core
abstract [Name DTerm]
xs Core
cbody
Quantifier
Ex -> Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core -> Core
quantify ([Type] -> Op
OExists [Type]
tys) ([Name DTerm] -> Core -> Core
abstract [Name DTerm]
xs Core
cbody)
Quantifier
All -> Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core -> Core
quantify ([Type] -> Op
OForall [Type]
tys) ([Name DTerm] -> Core -> Core
abstract [Name DTerm]
xs Core
cbody)
where
unbindDeep :: Member Fresh r => DTerm -> Sem r ([Name DTerm], [Type], DTerm)
unbindDeep :: DTerm -> Sem r ([Name DTerm], [Type], DTerm)
unbindDeep (DTAbs Quantifier
q' Type
ty Bind (Name DTerm) DTerm
l) | Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
q' = do
(Name DTerm
name, DTerm
inner) <- Bind (Name DTerm) DTerm -> Sem r (Name DTerm, DTerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Name DTerm) DTerm
l
([Name DTerm]
ns, [Type]
tys, DTerm
body) <- DTerm -> Sem r ([Name DTerm], [Type], DTerm)
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r ([Name DTerm], [Type], DTerm)
unbindDeep DTerm
inner
([Name DTerm], [Type], DTerm)
-> Sem r ([Name DTerm], [Type], DTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name DTerm
name Name DTerm -> [Name DTerm] -> [Name DTerm]
forall a. a -> [a] -> [a]
: [Name DTerm]
ns, Type
ty Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
tys, DTerm
body)
unbindDeep DTerm
t = ([Name DTerm], [Type], DTerm)
-> Sem r ([Name DTerm], [Type], DTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], DTerm
t)
abstract :: [Name DTerm] -> Core -> Core
abstract :: [Name DTerm] -> Core -> Core
abstract [Name DTerm]
xs Core
body = Bind [Name Core] Core -> Core
CAbs ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ((Name DTerm -> Name Core) -> [Name DTerm] -> [Name Core]
forall a b. (a -> b) -> [a] -> [b]
map Name DTerm -> Name Core
coerce [Name DTerm]
xs) Core
body)
quantify :: Op -> Core -> Core
quantify :: Op -> Core -> Core
quantify Op
op = Core -> Core -> Core
CApp (Op -> Core
CConst Op
op)
compileDTerm (DTApp Type
_ (DTPrim Type
_ (PrimBOp BOp
Cons)) (DTPair Type
_ DTerm
t1 DTerm
t2)) =
Side -> Core -> Core
CInj Side
R (Core -> Core) -> Sem r Core -> Sem r Core
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Core -> Core -> Core
CPair (Core -> Core -> Core) -> Sem r Core -> Sem r (Core -> Core)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
t1 Sem r (Core -> Core) -> Sem r Core -> Sem r Core
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
t2)
compileDTerm (DTApp Type
_ (DTPrim Type
_ Prim
PrimLeft) DTerm
t) =
Side -> Core -> Core
CInj Side
L (Core -> Core) -> Sem r Core -> Sem r Core
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
t
compileDTerm (DTApp Type
_ (DTPrim Type
_ Prim
PrimRight) DTerm
t) =
Side -> Core -> Core
CInj Side
R (Core -> Core) -> Sem r Core -> Sem r Core
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
t
compileDTerm (DTApp Type
_ DTerm
t1 DTerm
t2) = Core -> Core -> Core
CApp (Core -> Core -> Core) -> Sem r Core -> Sem r (Core -> Core)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
t1 Sem r (Core -> Core) -> Sem r Core -> Sem r Core
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
t2
compileDTerm (DTPair Type
_ DTerm
t1 DTerm
t2) =
Core -> Core -> Core
CPair (Core -> Core -> Core) -> Sem r Core -> Sem r (Core -> Core)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
t1 Sem r (Core -> Core) -> Sem r Core -> Sem r Core
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
t2
compileDTerm (DTCase Type
_ [DBranch]
bs) = Core -> Core -> Core
CApp (Core -> Core -> Core) -> Sem r Core -> Sem r (Core -> Core)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DBranch] -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[DBranch] -> Sem r Core
compileCase [DBranch]
bs Sem r (Core -> Core) -> Sem r Core -> Sem r Core
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Core -> Sem r Core
forall (f :: * -> *) a. Applicative f => a -> f a
pure Core
CUnit
compileDTerm (DTTyOp Type
_ TyOp
op Type
ty) = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Core -> Core -> Core
CApp (Op -> Core
CConst (Map TyOp Op
tyOps Map TyOp Op -> TyOp -> Op
forall k v. (Show k, Ord k) => Map k v -> k -> v
! TyOp
op)) (Type -> Core
CType Type
ty)
where
tyOps :: Map TyOp Op
tyOps =
[(TyOp, Op)] -> Map TyOp Op
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ TyOp
Enumerate TyOp -> Op -> (TyOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OEnum,
TyOp
Count TyOp -> Op -> (TyOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OCount
]
compileDTerm (DTNil Type
_) = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Side -> Core -> Core
CInj Side
L Core
CUnit
compileDTerm (DTTest [(String, Type, Name DTerm)]
info DTerm
t) = [(String, Type, Name Core)] -> Core -> Core
CTest ([(String, Type, Name DTerm)] -> [(String, Type, Name Core)]
coerce [(String, Type, Name DTerm)]
info) (Core -> Core) -> Sem r Core -> Sem r Core
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
t
compilePrim :: Member Fresh r => Type -> Prim -> Sem r Core
compilePrim :: Type -> Prim -> Sem r Core
compilePrim (Type
argTy :->: Type
_) (PrimUOp UOp
uop) = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Type -> UOp -> Core
compileUOp Type
argTy UOp
uop
compilePrim Type
ty p :: Prim
p@(PrimUOp UOp
_) = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
p Type
ty
compilePrim Type
_ (PrimBOp BOp
Cons) = do
Name Core
hd <- Name Core -> Sem r (Name Core)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name Core
forall a. String -> Name a
string2Name String
"hd")
Name Core
tl <- Name Core -> Sem r (Name Core)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name Core
forall a. String -> Name a
string2Name String
"tl")
Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs (Bind [Name Core] Core -> Core) -> Bind [Name Core] Core -> Core
forall a b. (a -> b) -> a -> b
$ [Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Core
hd, Name Core
tl] (Core -> Bind [Name Core] Core) -> Core -> Bind [Name Core] Core
forall a b. (a -> b) -> a -> b
$ Side -> Core -> Core
CInj Side
R (Core -> Core -> Core
CPair (QName Core -> Core
CVar (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
hd)) (QName Core -> Core
CVar (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
tl)))
compilePrim Type
_ Prim
PrimLeft = do
Name Core
a <- Name Core -> Sem r (Name Core)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name Core
forall a. String -> Name a
string2Name String
"a")
Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs (Bind [Name Core] Core -> Core) -> Bind [Name Core] Core -> Core
forall a b. (a -> b) -> a -> b
$ [Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Core
a] (Core -> Bind [Name Core] Core) -> Core -> Bind [Name Core] Core
forall a b. (a -> b) -> a -> b
$ Side -> Core -> Core
CInj Side
L (QName Core -> Core
CVar (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
a))
compilePrim Type
_ Prim
PrimRight = do
Name Core
a <- Name Core -> Sem r (Name Core)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name Core
forall a. String -> Name a
string2Name String
"a")
Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs (Bind [Name Core] Core -> Core) -> Bind [Name Core] Core -> Core
forall a b. (a -> b) -> a -> b
$ [Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Core
a] (Core -> Bind [Name Core] Core) -> Core -> Bind [Name Core] Core
forall a b. (a -> b) -> a -> b
$ Side -> Core -> Core
CInj Side
R (QName Core -> Core
CVar (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
a))
compilePrim (Type
ty1 :*: Type
ty2 :->: Type
resTy) (PrimBOp BOp
bop) = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type -> BOp -> Core
compileBOp Type
ty1 Type
ty2 Type
resTy BOp
bop
compilePrim Type
ty p :: Prim
p@(PrimBOp BOp
_) = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
p Type
ty
compilePrim Type
_ Prim
PrimSqrt = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OSqrt
compilePrim Type
_ Prim
PrimFloor = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFloor
compilePrim Type
_ Prim
PrimCeil = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OCeil
compilePrim Type
_ Prim
PrimAbs = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OAbs
compilePrim Type
_ Prim
PrimSize = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OSize
compilePrim (TySet Type
_ :->: Type
_) Prim
PrimPower = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OPower
compilePrim (TyBag Type
_ :->: Type
_) Prim
PrimPower = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OPower
compilePrim Type
ty Prim
PrimPower = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimPower Type
ty
compilePrim (TySet Type
_ :->: Type
_) Prim
PrimList = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OSetToList
compilePrim (TyBag Type
_ :->: Type
_) Prim
PrimSet = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OBagToSet
compilePrim (TyBag Type
_ :->: Type
_) Prim
PrimList = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OBagToList
compilePrim (TyList Type
_ :->: Type
_) Prim
PrimSet = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OListToSet
compilePrim (TyList Type
_ :->: Type
_) Prim
PrimBag = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OListToBag
compilePrim Type
_ Prim
p | Prim
p Prim -> [Prim] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prim
PrimList, Prim
PrimBag, Prim
PrimSet] = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OId
compilePrim Type
ty Prim
PrimList = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimList Type
ty
compilePrim Type
ty Prim
PrimBag = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimBag Type
ty
compilePrim Type
ty Prim
PrimSet = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimSet Type
ty
compilePrim Type
_ Prim
PrimB2C = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OBagToCounts
compilePrim (Type
_ :->: TyBag Type
_) Prim
PrimC2B = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OCountsToBag
compilePrim Type
ty Prim
PrimC2B = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimC2B Type
ty
compilePrim (TyMap Type
_ Type
_ :->: Type
_) Prim
PrimMapToSet = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OMapToSet
compilePrim (Type
_ :->: TyMap Type
_ Type
_) Prim
PrimSetToMap = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OSetToMap
compilePrim Type
ty Prim
PrimMapToSet = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimMapToSet Type
ty
compilePrim Type
ty Prim
PrimSetToMap = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimSetToMap Type
ty
compilePrim Type
_ Prim
PrimSummary = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OSummary
compilePrim (Type
_ :->: TyGraph Type
_) Prim
PrimVertex = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OVertex
compilePrim (TyGraph Type
_) Prim
PrimEmptyGraph = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OEmptyGraph
compilePrim (Type
_ :->: TyGraph Type
_) Prim
PrimOverlay = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OOverlay
compilePrim (Type
_ :->: TyGraph Type
_) Prim
PrimConnect = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OConnect
compilePrim Type
ty Prim
PrimVertex = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimVertex Type
ty
compilePrim Type
ty Prim
PrimEmptyGraph = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimEmptyGraph Type
ty
compilePrim Type
ty Prim
PrimOverlay = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimOverlay Type
ty
compilePrim Type
ty Prim
PrimConnect = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimConnect Type
ty
compilePrim Type
_ Prim
PrimInsert = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OInsert
compilePrim Type
_ Prim
PrimLookup = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OLookup
compilePrim (Type
_ :*: TyList Type
_ :->: Type
_) Prim
PrimEach = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$
QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
forall a. String -> Name a
string2Name String
"eachlist")
compilePrim (Type
_ :*: TyBag Type
_ :->: TyBag Type
_) Prim
PrimEach = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OEachBag
compilePrim (Type
_ :*: TySet Type
_ :->: TySet Type
_) Prim
PrimEach = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OEachSet
compilePrim Type
ty Prim
PrimEach = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimEach Type
ty
compilePrim (Type
_ :*: Type
_ :*: TyList Type
_ :->: Type
_) Prim
PrimReduce =
Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
forall a. String -> Name a
string2Name String
"foldr")
compilePrim (Type
_ :*: Type
_ :*: TyBag Type
_ :->: Type
_) Prim
PrimReduce = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$
QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
forall a. String -> Name a
string2Name String
"reducebag")
compilePrim (Type
_ :*: Type
_ :*: TySet Type
_ :->: Type
_) Prim
PrimReduce = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$
QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
forall a. String -> Name a
string2Name String
"reduceset")
compilePrim Type
ty Prim
PrimReduce = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimReduce Type
ty
compilePrim (Type
_ :*: TyList Type
_ :->: Type
_) Prim
PrimFilter = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$
QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
forall a. String -> Name a
string2Name String
"filterlist")
compilePrim (Type
_ :*: TyBag Type
_ :->: Type
_) Prim
PrimFilter = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFilterBag
compilePrim (Type
_ :*: TySet Type
_ :->: Type
_) Prim
PrimFilter = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFilterBag
compilePrim Type
ty Prim
PrimFilter = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimFilter Type
ty
compilePrim (Type
_ :->: TyList Type
_) Prim
PrimJoin = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$
QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
forall a. String -> Name a
string2Name String
"concat")
compilePrim (Type
_ :->: TyBag Type
_) Prim
PrimJoin = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OBagUnions
compilePrim (Type
_ :->: TySet Type
_) Prim
PrimJoin = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$
QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
forall a. String -> Name a
string2Name String
"unions")
compilePrim Type
ty Prim
PrimJoin = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimJoin Type
ty
compilePrim (Type
_ :*: TyBag Type
_ :*: Type
_ :->: Type
_) Prim
PrimMerge = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OMerge
compilePrim (Type
_ :*: TySet Type
_ :*: Type
_ :->: Type
_) Prim
PrimMerge = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OMerge
compilePrim Type
ty Prim
PrimMerge = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimMerge Type
ty
compilePrim Type
_ Prim
PrimIsPrime = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OIsPrime
compilePrim Type
_ Prim
PrimFactor = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFactor
compilePrim Type
_ Prim
PrimFrac = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFrac
compilePrim Type
_ Prim
PrimCrash = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OCrash
compilePrim Type
_ Prim
PrimUntil = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OUntil
compilePrim Type
_ Prim
PrimHolds = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OHolds
compilePrim Type
_ Prim
PrimLookupSeq = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OLookupSeq
compilePrim Type
_ Prim
PrimExtendSeq = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OExtendSeq
compilePrimErr :: Prim -> Type -> a
compilePrimErr :: Prim -> Type -> a
compilePrimErr Prim
p Type
ty = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Impossible! compilePrim " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Prim -> String
forall a. Show a => a -> String
show Prim
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on bad type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty
compileCase :: Member Fresh r => [DBranch] -> Sem r Core
compileCase :: [DBranch] -> Sem r Core
compileCase [] = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [String -> Name Core
forall a. String -> Name a
string2Name String
"_"] (Op -> Core
CConst Op
OMatchErr))
compileCase (DBranch
b : [DBranch]
bs) = do
Core
c1 <- DBranch -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DBranch -> Sem r Core
compileBranch DBranch
b
Core
c2 <- [DBranch] -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[DBranch] -> Sem r Core
compileCase [DBranch]
bs
Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [String -> Name Core
forall a. String -> Name a
string2Name String
"_"] (Core -> Core -> Core
CApp Core
c1 Core
c2))
compileBranch :: Member Fresh r => DBranch -> Sem r Core
compileBranch :: DBranch -> Sem r Core
compileBranch DBranch
b = do
(Telescope DGuard
gs, DTerm
e) <- DBranch -> Sem r (Telescope DGuard, DTerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind DBranch
b
Core
c <- DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm DTerm
e
Name Core
k <- Name Core -> Sem r (Name Core)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name Core
forall a. String -> Name a
string2Name String
"k")
Core
bc <- [DGuard] -> Name Core -> Core -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[DGuard] -> Name Core -> Core -> Sem r Core
compileGuards (Telescope DGuard -> [DGuard]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope DGuard
gs) Name Core
k Core
c
Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Core
k] Core
bc)
compileGuards :: Member Fresh r => [DGuard] -> Name Core -> Core -> Sem r Core
compileGuards :: [DGuard] -> Name Core -> Core -> Sem r Core
compileGuards [] Name Core
_ Core
e = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return Core
e
compileGuards (DGPat (Embed DTerm -> Embedded (Embed DTerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed DTerm)
s) DPattern
p : [DGuard]
gs) Name Core
k Core
e = do
Core
e' <- [DGuard] -> Name Core -> Core -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[DGuard] -> Name Core -> Core -> Sem r Core
compileGuards [DGuard]
gs Name Core
k Core
e
Core
s' <- DTerm -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm Embedded (Embed DTerm)
DTerm
s
DPattern -> Core -> Name Core -> Core -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DPattern -> Core -> Name Core -> Core -> Sem r Core
compileMatch DPattern
p Core
s' Name Core
k Core
e'
compileMatch :: Member Fresh r => DPattern -> Core -> Name Core -> Core -> Sem r Core
compileMatch :: DPattern -> Core -> Name Core -> Core -> Sem r Core
compileMatch (DPVar Type
_ Name DTerm
x) Core
s Name Core
_ Core
e = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Core -> Core -> Core
CApp (Bind [Name Core] Core -> Core
CAbs ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name DTerm -> Name Core
coerce Name DTerm
x] Core
e)) Core
s
compileMatch (DPWild Type
_) Core
s Name Core
_ Core
e = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Core -> Core -> Core
CApp (Bind [Name Core] Core -> Core
CAbs ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [String -> Name Core
forall a. String -> Name a
string2Name String
"_"] Core
e)) Core
s
compileMatch DPattern
DPUnit Core
s Name Core
_ Core
e = Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Core -> Core -> Core
CApp (Bind [Name Core] Core -> Core
CAbs ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [String -> Name Core
forall a. String -> Name a
string2Name String
"_"] Core
e)) Core
s
compileMatch (DPPair Type
_ Name DTerm
x1 Name DTerm
x2) Core
s Name Core
_ Core
e = do
Name Core
y <- Name Core -> Sem r (Name Core)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name Core
forall a. String -> Name a
string2Name String
"y")
Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$
Core -> Core -> Core
CApp
( Bind [Name Core] Core -> Core
CAbs
( [Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind
[Name Core
y]
( Core -> Core -> Core
CApp
( Core -> Core -> Core
CApp
(Bind [Name Core] Core -> Core
CAbs ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name DTerm -> Name Core
coerce Name DTerm
x1, Name DTerm -> Name Core
coerce Name DTerm
x2] Core
e))
(Side -> Core -> Core
CProj Side
L (QName Core -> Core
CVar (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
y)))
)
(Side -> Core -> Core
CProj Side
R (QName Core -> Core
CVar (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
y)))
)
)
)
Core
s
compileMatch (DPInj Type
_ Side
L Name DTerm
x) Core
s Name Core
k Core
e =
Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Core -> Bind (Name Core) Core -> Bind (Name Core) Core -> Core
CCase Core
s (Name Core -> Core -> Bind (Name Core) Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Name DTerm -> Name Core
coerce Name DTerm
x) Core
e) (Name Core -> Core -> Bind (Name Core) Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (String -> Name Core
forall a. String -> Name a
string2Name String
"_") (Core -> Core -> Core
CApp (QName Core -> Core
CVar (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
k)) Core
CUnit))
compileMatch (DPInj Type
_ Side
R Name DTerm
x) Core
s Name Core
k Core
e =
Core -> Sem r Core
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Core -> Bind (Name Core) Core -> Bind (Name Core) Core -> Core
CCase Core
s (Name Core -> Core -> Bind (Name Core) Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (String -> Name Core
forall a. String -> Name a
string2Name String
"_") (Core -> Core -> Core
CApp (QName Core -> Core
CVar (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
k)) Core
CUnit)) (Name Core -> Core -> Bind (Name Core) Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Name DTerm -> Name Core
coerce Name DTerm
x) Core
e)
compileUOp ::
Type ->
UOp ->
Core
compileUOp :: Type -> UOp -> Core
compileUOp Type
_ UOp
op = Op -> Core
CConst (Map UOp Op
coreUOps Map UOp Op -> UOp -> Op
forall k v. (Show k, Ord k) => Map k v -> k -> v
! UOp
op)
where
coreUOps :: Map UOp Op
coreUOps =
[(UOp, Op)] -> Map UOp Op
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ UOp
Neg UOp -> Op -> (UOp, Op)
forall a b. a -> b -> (a, b)
==> Op
ONeg,
UOp
Fact UOp -> Op -> (UOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OFact
]
compileBOp :: Type -> Type -> Type -> BOp -> Core
compileBOp :: Type -> Type -> Type -> BOp -> Core
compileBOp (TyGraph Type
_) (TyGraph Type
_) (TyGraph Type
_) BOp
op
| BOp
op BOp -> [BOp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Add, BOp
Mul] =
Op -> Core
CConst (Map BOp Op
regularOps Map BOp Op -> BOp -> Op
forall k v. (Show k, Ord k) => Map k v -> k -> v
! BOp
op)
where
regularOps :: Map BOp Op
regularOps =
[(BOp, Op)] -> Map BOp Op
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ BOp
Add BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OOverlay,
BOp
Mul BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OConnect
]
compileBOp Type
_ Type
_ Type
_ BOp
op
| BOp
op BOp -> Map BOp Op -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map BOp Op
regularOps = Op -> Core
CConst (Map BOp Op
regularOps Map BOp Op -> BOp -> Op
forall k v. (Show k, Ord k) => Map k v -> k -> v
! BOp
op)
where
regularOps :: Map BOp Op
regularOps =
[(BOp, Op)] -> Map BOp Op
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ BOp
Add BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OAdd,
BOp
Mul BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OMul,
BOp
Div BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
ODiv,
BOp
Exp BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OExp,
BOp
Mod BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OMod,
BOp
Divides BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
ODivides,
BOp
Choose BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OMultinom,
BOp
Eq BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OEq,
BOp
Lt BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OLt
]
compileBOp Type
ty Type
_ Type
_ BOp
ShouldEq = Op -> Core
CConst (Type -> Op
OShouldEq Type
ty)
compileBOp Type
_ty (TyList Type
_) Type
_ BOp
Elem = Op -> Core
CConst Op
OListElem
compileBOp Type
_ty Type
_ Type
_ BOp
Elem = Op -> Core
CConst Op
OBagElem
compileBOp Type
ty1 Type
ty2 Type
resTy BOp
op =
String -> Core
forall a. HasCallStack => String -> a
error (String -> Core) -> String -> Core
forall a b. (a -> b) -> a -> b
$ String
"Impossible! missing case in compileBOp: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Type, Type, Type, BOp) -> String
forall a. Show a => a -> String
show (Type
ty1, Type
ty2, Type
resTy, BOp
op)