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

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

-- |
-- Module      :  Disco.Compile
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Compiling the typechecked, desugared AST to the untyped core
-- language.
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

------------------------------------------------------------
-- Convenience operations
------------------------------------------------------------

-- | Utility function to desugar and compile a thing, given a
--   desugaring function for it.
compileThing :: (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing :: forall a. (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing a -> Sem '[Fresh] DTerm
desugarThing = forall a. Sem '[] a -> a
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< a -> Sem '[Fresh] DTerm
desugarThing)

-- | Compile a typechecked term ('ATerm') directly to a 'Core' term,
--   by desugaring and then compiling.
compileTerm :: ATerm -> Core
compileTerm :: ATerm -> Core
compileTerm = forall a. (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing forall (r :: EffectRow). Member Fresh r => ATerm -> Sem r DTerm
desugarTerm

-- | Compile a typechecked property ('AProperty') directly to a 'Core' term,
--   by desugaring and then compilling.
compileProperty :: AProperty -> Core
compileProperty :: ATerm -> Core
compileProperty = forall a. (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing forall (r :: EffectRow). Member Fresh r => ATerm -> Sem r DTerm
desugarProperty

------------------------------------------------------------
-- Compiling definitions
------------------------------------------------------------

-- | Compile a context of typechecked definitions ('Defn') to a
--   sequence of compiled 'Core' bindings, such that the body of each
--   binding depends only on previous ones in the list.  First
--   topologically sorts the definitions into mutually recursive
--   groups, then compiles recursive definitions specially in terms of
--   'delay' and 'force'.
compileDefns :: Ctx ATerm Defn -> [(QName Core, Core)]
compileDefns :: Ctx ATerm Defn -> [(QName Core, Core)]
compileDefns Ctx ATerm Defn
defs = forall a. Sem '[] a -> a
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh forall a b. (a -> b) -> a -> b
$ do
  let vars :: Set (QName ATerm)
vars = forall a b. Ctx a b -> Set (QName a)
Ctx.keysSet Ctx ATerm Defn
defs

      -- Get a list of pairs of the form (y,x) where x uses y in its
      -- definition.  We want them in the order (y,x) since y needs to
      -- be evaluated before x.  These will be the edges in our
      -- dependency graph.  Note that some of these edges may refer to
      -- things that were imported, and hence not in the set of
      -- definitions; those edges will simply be dropped by G.mkGraph.
      deps :: Set (QName ATerm, QName ATerm)
      deps :: Set (QName ATerm, QName ATerm)
deps = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\(QName ATerm
x, Defn
body) -> forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (,QName ATerm
x) (forall a s. Getting (Set a) s a -> s -> Set a
setOf (forall t e. (Data t, Typeable e) => Traversal' t (QName e)
fvQ @Defn @ATerm) Defn
body)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Ctx a b -> [(QName a, b)]
Ctx.assocs forall a b. (a -> b) -> a -> b
$ Ctx ATerm Defn
defs

      -- Do a topological sort of the condensation of the dependency
      -- graph.  Each SCC corresponds to a group of mutually recursive
      -- definitions; each such group depends only on groups that come
      -- before it in the topsort.
      defnGroups :: [Set (QName ATerm)]
      defnGroups :: [Set (QName ATerm)]
defnGroups = forall a. Graph a -> [a]
G.topsort (forall a. Ord a => Graph a -> Graph (Set a)
G.condensation (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))

  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (r :: EffectRow).
Member Fresh r =>
[(QName ATerm, Defn)] -> Sem r [(QName Core, Core)]
compileDefnGroup forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Ctx a b -> [(QName a, b)]
Ctx.assocs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Ctx a b -> Set (QName a) -> Ctx a b
Ctx.restrictKeys Ctx ATerm Defn
defs) [Set (QName ATerm)]
defnGroups

-- | Compile a group of mutually recursive definitions, using @delay@
--   to compile recursion via references to memory cells.
compileDefnGroup :: Member Fresh r => [(QName ATerm, Defn)] -> Sem r [(QName Core, Core)]
compileDefnGroup :: forall (r :: EffectRow).
Member Fresh r =>
[(QName ATerm, Defn)] -> Sem r [(QName Core, Core)]
compileDefnGroup [(QName ATerm
f, Defn
defn)]
  -- Informally, a recursive definition f = body compiles to
  --
  --   f = force (delay f. [force f / f] body).
  --
  -- However, we have to be careful: in the informal notation above,
  -- all the variables are named 'f', but in fully renamed syntax they
  -- are different.  Writing fT for the top-level f bound in a
  -- specific module etc.  and fL for a locally bound f, we really
  -- have
  --
  --   fT = force (delay fL. [force fL / fT] body)
  | QName ATerm
f forall a. Ord a => a -> Set a -> Bool
`S.member` forall a s. Getting (Set a) s a -> s -> Set a
setOf forall t e. (Data t, Typeable e) => Traversal' t (QName e)
fvQ Defn
defn =
      forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
: []) 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 (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [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]))))
  -- A non-recursive definition just compiles simply.
  | Bool
otherwise =
      forall (m :: * -> *) a. Monad m => a -> m a
return [(QName Core
fT, Core
cdefn)]
 where
  fT, fL :: QName Core
  fT :: QName Core
fT = coerce :: forall a b. Coercible a b => a -> b
coerce QName ATerm
f
  fL :: QName Core
fL = forall a. Name a -> QName a
localName (coerce :: forall a b. Coercible a b => a -> b
coerce (forall a. QName a -> Name a
qname QName ATerm
f))

  cdefn :: Core
cdefn = forall a. (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing forall (r :: EffectRow). Member Fresh r => Defn -> Sem r DTerm
desugarDefn Defn
defn

-- A group of mutually recursive definitions  {f = fbody, g = gbody, ...}
-- compiles to
--   { _grp = delay fL gL ... . (forceVars fbody, forceVars gbody, ...)
--   , fT = fst (force _grp)
--   , gT = snd (force _grp)
--   , ...
--   }
-- where forceVars is the substitution [force fL / fT, force gL / gT, ...]

compileDefnGroup [(QName ATerm, Defn)]
defs = do
  QName Core
grp :: QName Core <- forall (r :: EffectRow) a.
Member Fresh r =>
String -> Sem r (QName a)
freshQ String
"__grp"
  let ([QName ATerm]
vars, [Defn]
bodies) = forall a b. [(a, b)] -> ([a], [b])
unzip [(QName ATerm, Defn)]
defs
      varsT, varsL :: [QName Core]
      varsT :: [QName Core]
varsT = coerce :: forall a b. Coercible a b => a -> b
coerce [QName ATerm]
vars
      varsL :: [QName Core]
varsL = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Name a -> QName a
localName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. QName a -> Name a
qname) [QName Core]
varsT
      forceVars :: [(QName Core, Core)]
      forceVars :: [(QName Core, Core)]
forceVars = 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' = forall a b. (a -> b) -> [a] -> [b]
map ([(QName Core, Core)] -> Core -> Core
substsQC [(QName Core, Core)]
forceVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Sem '[Fresh] DTerm) -> a -> Core
compileThing forall (r :: EffectRow). Member Fresh r => Defn -> Sem r DTerm
desugarDefn) [Defn]
bodies
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    (QName Core
grp, Bind [Name Core] [Core] -> Core
CDelay (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (forall a b. (a -> b) -> [a] -> [b]
map forall a. QName a -> Name a
qname [QName Core]
varsL) [Core]
bodies'))
      forall a. a -> [a] -> [a]
: forall a b. [a] -> [b] -> [(a, b)]
zip [QName Core]
varsT (forall a b. [a] -> (a -> b) -> [b]
for [Int
0 ..] forall a b. (a -> b) -> a -> b
$ Core -> Core
CForce forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Num a => a -> a -> a
- Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Side -> Core -> Core
CProj Side
R

------------------------------------------------------------
-- Compiling terms
------------------------------------------------------------

-- | Compile a typechecked, desugared 'DTerm' to an untyped 'Core'
--   term.
compileDTerm :: Member Fresh r => DTerm -> Sem r Core
compileDTerm :: forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm (DTVar Type
_ QName DTerm
x) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName Core -> Core
CVar (coerce :: forall a b. Coercible a b => a -> b
coerce QName DTerm
x)
compileDTerm (DTPrim Type
ty Prim
x) = forall (r :: EffectRow).
Member Fresh r =>
Type -> Prim -> Sem r Core
compilePrim Type
ty Prim
x
compileDTerm DTerm
DTUnit = forall (m :: * -> *) a. Monad m => a -> m a
return Core
CUnit
compileDTerm (DTBool Type
_ Bool
b) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Side -> Core -> Core
CInj (forall a. a -> a -> Bool -> a
bool Side
L Side
R Bool
b) Core
CUnit
compileDTerm (DTChar Char
c) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ RationalDisplay -> Rational -> Core
CNum RationalDisplay
Fraction (forall a. Integral a => a -> Integer
toInteger (forall a. Enum a => a -> Int
fromEnum Char
c) forall a. Integral a => a -> a -> Ratio a
% Integer
1)
compileDTerm (DTNat Type
_ Integer
n) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ RationalDisplay -> Rational -> Core
CNum RationalDisplay
Fraction (Integer
n forall a. Integral a => a -> a -> Ratio a
% Integer
1) -- compileNat ty n
compileDTerm (DTRat Rational
r) = forall (m :: * -> *) a. Monad m => a -> m a
return 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) <- forall (r :: EffectRow).
Member Fresh r =>
DTerm -> Sem r ([Name DTerm], [Type], DTerm)
unbindDeep DTerm
term
  Core
cbody <- forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
body
  case Quantifier
q of
    Quantifier
Lam -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Name DTerm] -> Core -> Core
abstract [Name DTerm]
xs Core
cbody
    Quantifier
Ex -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return 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
  -- Gather nested abstractions with the same quantifier.
  unbindDeep :: Member Fresh r => DTerm -> Sem r ([Name DTerm], [Type], DTerm)
  unbindDeep :: forall (r :: EffectRow).
Member Fresh r =>
DTerm -> Sem r ([Name DTerm], [Type], DTerm)
unbindDeep (DTAbs Quantifier
q' Type
ty Bind (Name DTerm) DTerm
l) | Quantifier
q forall a. Eq a => a -> a -> Bool
== Quantifier
q' = do
    (Name DTerm
name, DTerm
inner) <- forall (r :: EffectRow) 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) <- forall (r :: EffectRow).
Member Fresh r =>
DTerm -> Sem r ([Name DTerm], [Type], DTerm)
unbindDeep DTerm
inner
    forall (m :: * -> *) a. Monad m => a -> m a
return (Name DTerm
name forall a. a -> [a] -> [a]
: [Name DTerm]
ns, Type
ty forall a. a -> [a] -> [a]
: [Type]
tys, DTerm
body)
  unbindDeep DTerm
t = 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 (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (forall a b. (a -> b) -> [a] -> [b]
map coerce :: forall a b. Coercible a b => a -> b
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)

-- Special case for Cons, which compiles to a constructor application
-- rather than a function application.
compileDTerm (DTApp Type
_ (DTPrim Type
_ (PrimBOp BOp
Cons)) (DTPair Type
_ DTerm
t1 DTerm
t2)) =
  Side -> Core -> Core
CInj Side
R forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Core -> Core -> Core
CPair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
t2)
-- Special cases for left and right, which also compile to constructor applications.
compileDTerm (DTApp Type
_ (DTPrim Type
_ Prim
PrimLeft) DTerm
t) =
  Side -> Core -> Core
CInj Side
L forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow). 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
t
compileDTerm (DTApp Type
_ DTerm
t1 DTerm
t2) = Core -> Core -> Core
CApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
t2
compileDTerm (DTPair Type
_ DTerm
t1 DTerm
t2) =
  Core -> Core -> Core
CPair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
t2
compileDTerm (DTCase Type
_ [DBranch]
bs) = Core -> Core -> Core
CApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow). Member Fresh r => [DBranch] -> Sem r Core
compileCase [DBranch]
bs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Core
CUnit
compileDTerm (DTTyOp Type
_ TyOp
op Type
ty) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Core -> Core
CApp (Op -> Core
CConst (Map TyOp Op
tyOps 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 =
    forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
      [ TyOp
Enumerate forall a b. a -> b -> (a, b)
==> Op
OEnum
      , TyOp
Count forall a b. a -> b -> (a, b)
==> Op
OCount
      ]
compileDTerm (DTNil Type
_) = forall (m :: * -> *) a. Monad m => a -> m a
return 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 (coerce :: forall a b. Coercible a b => a -> b
coerce [(String, Type, Name DTerm)]
info) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
t

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

-- | Compile a natural number. A separate function is needed in
--   case the number is of a finite type, in which case we must
--   mod it by its type.
-- compileNat :: Member Fresh r => Type -> Integer -> Sem r Core
-- compileNat (TyFin n) x = return $ CNum Fraction ((x `mod` n) % 1)
-- compileNat _         x = return $ CNum Fraction (x % 1)

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

-- | Compile a primitive.  Typically primitives turn into a
--   corresponding function constant in the core language, but
--   sometimes the particular constant it turns into may depend on the
--   type.
compilePrim :: Member Fresh r => Type -> Prim -> Sem r Core
compilePrim :: forall (r :: EffectRow).
Member Fresh r =>
Type -> Prim -> Sem r Core
compilePrim (Type
argTy :->: Type
_) (PrimUOp UOp
uop) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> UOp -> Core
compileUOp Type
argTy UOp
uop
compilePrim Type
ty p :: Prim
p@(PrimUOp UOp
_) = forall a. Prim -> Type -> a
compilePrimErr Prim
p Type
ty
-- This special case for Cons only triggers if we didn't hit the case
-- for fully saturated Cons; just fall back to generating a lambda.  Have to
-- do it here, not in compileBOp, since we need to generate fresh names.
compilePrim Type
_ (PrimBOp BOp
Cons) = do
  Name Core
hd <- forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"hd")
  Name Core
tl <- forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"tl")
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs forall a b. (a -> b) -> a -> b
$ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Core
hd, Name Core
tl] forall a b. (a -> b) -> a -> b
$ Side -> Core -> Core
CInj Side
R (Core -> Core -> Core
CPair (QName Core -> Core
CVar (forall a. Name a -> QName a
localName Name Core
hd)) (QName Core -> Core
CVar (forall a. Name a -> QName a
localName Name Core
tl)))
compilePrim Type
_ Prim
PrimLeft = do
  Name Core
a <- forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"a")
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs forall a b. (a -> b) -> a -> b
$ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Core
a] forall a b. (a -> b) -> a -> b
$ Side -> Core -> Core
CInj Side
L (QName Core -> Core
CVar (forall a. Name a -> QName a
localName Name Core
a))
compilePrim Type
_ Prim
PrimRight = do
  Name Core
a <- forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"a")
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs forall a b. (a -> b) -> a -> b
$ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Core
a] forall a b. (a -> b) -> a -> b
$ Side -> Core -> Core
CInj Side
R (QName Core -> Core
CVar (forall a. Name a -> QName a
localName Name Core
a))
compilePrim (Type
ty1 :*: Type
ty2 :->: Type
resTy) (PrimBOp BOp
bop) = forall (m :: * -> *) a. Monad m => a -> m a
return 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
_) = forall a. Prim -> Type -> a
compilePrimErr Prim
p Type
ty
compilePrim Type
_ Prim
PrimSqrt = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OSqrt
compilePrim Type
_ Prim
PrimFloor = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFloor
compilePrim Type
_ Prim
PrimCeil = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OCeil
compilePrim (TySet Type
_ :->: Type
_) Prim
PrimAbs =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"setSize")
compilePrim (TyBag Type
_ :->: Type
_) Prim
PrimAbs =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"bagSize")
compilePrim (TyList Type
_ :->: Type
_) Prim
PrimAbs =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"length")
compilePrim Type
_ Prim
PrimAbs = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OAbs
compilePrim (TySet Type
_ :->: Type
_) Prim
PrimPower = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OPower
compilePrim (TyBag Type
_ :->: Type
_) Prim
PrimPower = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OPower
compilePrim Type
ty Prim
PrimPower = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimPower Type
ty
compilePrim (TySet Type
_ :->: Type
_) Prim
PrimList = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OSetToList
compilePrim (TyBag Type
_ :->: Type
_) Prim
PrimSet = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OBagToSet
compilePrim (TyBag Type
_ :->: Type
_) Prim
PrimList = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OBagToList
compilePrim (TyList Type
_ :->: Type
_) Prim
PrimSet = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OListToSet
compilePrim (TyList Type
_ :->: Type
_) Prim
PrimBag = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OListToBag
compilePrim Type
_ Prim
p | Prim
p forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prim
PrimList, Prim
PrimBag, Prim
PrimSet] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OId
compilePrim Type
ty Prim
PrimList = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimList Type
ty
compilePrim Type
ty Prim
PrimBag = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimBag Type
ty
compilePrim Type
ty Prim
PrimSet = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimSet Type
ty
compilePrim Type
_ Prim
PrimB2C = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OBagToCounts
compilePrim (Type
_ :->: TyBag Type
_) Prim
PrimC2B = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OCountsToBag
compilePrim Type
ty Prim
PrimC2B = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimC2B Type
ty
compilePrim (Type
_ :->: TyBag Type
_) Prim
PrimUC2B = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OUnsafeCountsToBag
compilePrim Type
ty Prim
PrimUC2B = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimUC2B Type
ty
compilePrim (TyMap Type
_ Type
_ :->: Type
_) Prim
PrimMapToSet = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OMapToSet
compilePrim (Type
_ :->: TyMap Type
_ Type
_) Prim
PrimSetToMap = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OSetToMap
compilePrim Type
ty Prim
PrimMapToSet = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimMapToSet Type
ty
compilePrim Type
ty Prim
PrimSetToMap = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimSetToMap Type
ty
compilePrim Type
_ Prim
PrimSummary = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OSummary
compilePrim (Type
_ :->: TyGraph Type
_) Prim
PrimVertex = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OVertex
compilePrim (TyGraph Type
_) Prim
PrimEmptyGraph = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OEmptyGraph
compilePrim (Type
_ :->: TyGraph Type
_) Prim
PrimOverlay = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OOverlay
compilePrim (Type
_ :->: TyGraph Type
_) Prim
PrimConnect = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OConnect
compilePrim Type
ty Prim
PrimVertex = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimVertex Type
ty
compilePrim Type
ty Prim
PrimEmptyGraph = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimEmptyGraph Type
ty
compilePrim Type
ty Prim
PrimOverlay = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimOverlay Type
ty
compilePrim Type
ty Prim
PrimConnect = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimConnect Type
ty
compilePrim Type
_ Prim
PrimInsert = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OInsert
compilePrim Type
_ Prim
PrimLookup = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OLookup
compilePrim (Type
_ :*: TyList Type
_ :->: Type
_) Prim
PrimEach =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"eachlist")
compilePrim (Type
_ :*: TyBag Type
_ :->: TyBag Type
_) Prim
PrimEach = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OEachBag
compilePrim (Type
_ :*: TySet Type
_ :->: TySet Type
_) Prim
PrimEach = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OEachSet
compilePrim Type
ty Prim
PrimEach = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimEach Type
ty
compilePrim (Type
_ :*: Type
_ :*: TyList Type
_ :->: Type
_) Prim
PrimReduce =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"foldr")
compilePrim (Type
_ :*: Type
_ :*: TyBag Type
_ :->: Type
_) Prim
PrimReduce =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"reducebag")
compilePrim (Type
_ :*: Type
_ :*: TySet Type
_ :->: Type
_) Prim
PrimReduce =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"reduceset")
compilePrim Type
ty Prim
PrimReduce = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimReduce Type
ty
compilePrim (Type
_ :*: TyList Type
_ :->: Type
_) Prim
PrimFilter =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"filterlist")
compilePrim (Type
_ :*: TyBag Type
_ :->: Type
_) Prim
PrimFilter = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFilterBag
compilePrim (Type
_ :*: TySet Type
_ :->: Type
_) Prim
PrimFilter = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFilterBag
compilePrim Type
ty Prim
PrimFilter = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimFilter Type
ty
compilePrim (Type
_ :->: TyList Type
_) Prim
PrimJoin =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"concat")
compilePrim (Type
_ :->: TyBag Type
_) Prim
PrimJoin = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OBagUnions
compilePrim (Type
_ :->: TySet Type
_) Prim
PrimJoin =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"unions")
compilePrim Type
ty Prim
PrimJoin = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimJoin Type
ty
compilePrim (Type
_ :*: TyBag Type
_ :*: Type
_ :->: Type
_) Prim
PrimMerge = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OMerge
compilePrim (Type
_ :*: TySet Type
_ :*: Type
_ :->: Type
_) Prim
PrimMerge = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OMerge
compilePrim Type
ty Prim
PrimMerge = forall a. Prim -> Type -> a
compilePrimErr Prim
PrimMerge Type
ty
compilePrim Type
_ Prim
PrimIsPrime = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OIsPrime
compilePrim Type
_ Prim
PrimFactor = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFactor
compilePrim Type
_ Prim
PrimFrac = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OFrac
compilePrim Type
_ Prim
PrimCrash = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OCrash
compilePrim Type
_ Prim
PrimUntil = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OUntil
compilePrim Type
_ Prim
PrimHolds = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OHolds
compilePrim Type
_ Prim
PrimLookupSeq = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OLookupSeq
compilePrim Type
_ Prim
PrimExtendSeq = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Op -> Core
CConst Op
OExtendSeq

compilePrimErr :: Prim -> Type -> a
compilePrimErr :: forall a. Prim -> Type -> a
compilePrimErr Prim
p Type
ty = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! compilePrim " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Prim
p forall a. [a] -> [a] -> [a]
++ String
" on bad type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty

------------------------------------------------------------
-- Case expressions
------------------------------------------------------------

-- | Compile a case expression of type τ to a core language expression
--   of type (Unit → τ), in order to delay evaluation until explicitly
--   applying it to the unit value.
compileCase :: Member Fresh r => [DBranch] -> Sem r Core
compileCase :: forall (r :: EffectRow). Member Fresh r => [DBranch] -> Sem r Core
compileCase [] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [forall a. String -> Name a
string2Name String
"_"] (Op -> Core
CConst Op
OMatchErr))
-- empty case ==>  λ _ . error

compileCase (DBranch
b : [DBranch]
bs) = do
  Core
c1 <- forall (r :: EffectRow). Member Fresh r => DBranch -> Sem r Core
compileBranch DBranch
b
  Core
c2 <- forall (r :: EffectRow). Member Fresh r => [DBranch] -> Sem r Core
compileCase [DBranch]
bs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [forall a. String -> Name a
string2Name String
"_"] (Core -> Core -> Core
CApp Core
c1 Core
c2))

-- | Compile a branch of a case expression of type τ to a core
--   language expression of type (Unit → τ) → τ.  The idea is that it
--   takes a failure continuation representing the subsequent branches
--   in the case expression.  If the branch succeeds, it just returns
--   the associated expression of type τ; if it fails, it calls the
--   continuation to proceed with the case analysis.
compileBranch :: Member Fresh r => DBranch -> Sem r Core
compileBranch :: forall (r :: EffectRow). Member Fresh r => DBranch -> Sem r Core
compileBranch DBranch
b = do
  (Telescope (Guard_ DS)
gs, DTerm
e) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind DBranch
b
  Core
c <- forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm DTerm
e
  Name Core
k <- forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"k") -- Fresh name for the failure continuation
  Core
bc <- forall (r :: EffectRow).
Member Fresh r =>
[Guard_ DS] -> Name Core -> Core -> Sem r Core
compileGuards (forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope (Guard_ DS)
gs) Name Core
k Core
c
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bind [Name Core] Core -> Core
CAbs (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Core
k] Core
bc)

-- | 'compileGuards' takes a list of guards, the name of the failure
--   continuation of type (Unit → τ), and a Core term of type τ to
--   return in the case of success, and compiles to an expression of
--   type τ which evaluates the guards in sequence, ultimately
--   returning the given expression if all guards succeed, or calling
--   the failure continuation at any point if a guard fails.
compileGuards :: Member Fresh r => [DGuard] -> Name Core -> Core -> Sem r Core
compileGuards :: forall (r :: EffectRow).
Member Fresh r =>
[Guard_ DS] -> Name Core -> Core -> Sem r Core
compileGuards [] Name Core
_ Core
e = forall (m :: * -> *) a. Monad m => a -> m a
return Core
e
compileGuards (DGPat (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed DTerm)
s) Pattern_ DS
p : [Guard_ DS]
gs) Name Core
k Core
e = do
  Core
e' <- forall (r :: EffectRow).
Member Fresh r =>
[Guard_ DS] -> Name Core -> Core -> Sem r Core
compileGuards [Guard_ DS]
gs Name Core
k Core
e
  Core
s' <- forall (r :: EffectRow). Member Fresh r => DTerm -> Sem r Core
compileDTerm Embedded (Embed DTerm)
s
  forall (r :: EffectRow).
Member Fresh r =>
Pattern_ DS -> Core -> Name Core -> Core -> Sem r Core
compileMatch Pattern_ DS
p Core
s' Name Core
k Core
e'

-- | 'compileMatch' takes a pattern, the compiled scrutinee, the name
--   of the failure continuation, and a Core term representing the
--   compilation of any guards which come after this one, and returns
--   a Core expression of type τ that performs the match and either
--   calls the failure continuation in the case of failure, or the
--   rest of the guards in the case of success.
compileMatch :: Member Fresh r => DPattern -> Core -> Name Core -> Core -> Sem r Core
compileMatch :: forall (r :: EffectRow).
Member Fresh r =>
Pattern_ DS -> Core -> Name Core -> Core -> Sem r Core
compileMatch (DPVar Type
_ Name DTerm
x) Core
s Name Core
_ Core
e = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Core -> Core
CApp (Bind [Name Core] Core -> Core
CAbs (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
x] Core
e)) Core
s
-- Note in the below two cases that we can't just discard s since
-- that would result in a lazy semantics.  With an eager/strict
-- semantics, we have to make sure s gets evaluated even if its
-- value is then discarded.
compileMatch (DPWild Type
_) Core
s Name Core
_ Core
e = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Core -> Core
CApp (Bind [Name Core] Core -> Core
CAbs (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [forall a. String -> Name a
string2Name String
"_"] Core
e)) Core
s
compileMatch Pattern_ DS
DPUnit Core
s Name Core
_ Core
e = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Core -> Core
CApp (Bind [Name Core] Core -> Core
CAbs (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [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 <- forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"y")

  -- {? e when s is (x1,x2) ?}   ==>   (\y. (\x1.\x2. e) (fst y) (snd y)) s
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    Core -> Core -> Core
CApp
      ( Bind [Name Core] Core -> Core
CAbs
          ( 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 (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
x1, coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
x2] Core
e))
                      (Side -> Core -> Core
CProj Side
L (QName Core -> Core
CVar (forall a. Name a -> QName a
localName Name Core
y)))
                  )
                  (Side -> Core -> Core
CProj Side
R (QName Core -> Core
CVar (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 =
  -- {? e when s is left(x) ?}   ==>   case s of {left x -> e; right _ -> k unit}
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Bind (Name Core) Core -> Bind (Name Core) Core -> Core
CCase Core
s (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
x) Core
e) (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (forall a. String -> Name a
string2Name String
"_") (Core -> Core -> Core
CApp (QName Core -> Core
CVar (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 =
  -- {? e when s is right(x) ?}   ==>   case s of {left _ -> k unit; right x -> e}
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Bind (Name Core) Core -> Bind (Name Core) Core -> Core
CCase Core
s (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (forall a. String -> Name a
string2Name String
"_") (Core -> Core -> Core
CApp (QName Core -> Core
CVar (forall a. Name a -> QName a
localName Name Core
k)) Core
CUnit)) (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
x) Core
e)

------------------------------------------------------------
-- Unary and binary operators
------------------------------------------------------------

-- | Compile a unary operator.
compileUOp ::
  -- | Type of the operator argument
  Type ->
  UOp ->
  Core
compileUOp :: Type -> UOp -> Core
compileUOp Type
_ UOp
op = Op -> Core
CConst (Map UOp Op
coreUOps forall k v. (Show k, Ord k) => Map k v -> k -> v
! UOp
op)
 where
  -- Just look up the corresponding core operator.
  coreUOps :: Map UOp Op
coreUOps =
    forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
      [ UOp
Neg forall a b. a -> b -> (a, b)
==> Op
ONeg
      , UOp
Fact forall a b. a -> b -> (a, b)
==> Op
OFact
      , UOp
Not forall a b. a -> b -> (a, b)
==> Op
ONotProp
      ]

-- | Compile a binary operator.  This function needs to know the types
--   of the arguments and result since some operators are overloaded
--   and compile to different code depending on their type.
--
--  @arg1 ty -> arg2 ty -> result ty -> op -> result@
compileBOp :: Type -> Type -> Type -> BOp -> Core
-- First, compile some operators specially for modular arithmetic.
-- Most operators on TyFun (add, mul, sub, etc.) have already been
-- desugared to an operation followed by a mod.  The only operators
-- here are the ones that have a special runtime behavior for Zn that
-- can't be implemented in terms of other, existing operators:
--
--   - Division on Zn needs to find modular inverses.
--   - Divisibility testing on Zn similarly needs to find a gcd etc.
--   - Exponentiation on Zn could in theory be implemented as a normal
--     exponentiation on naturals followed by a mod, but that would be
--     silly and inefficient.  Instead we compile to a special modular
--     exponentiation operator which takes mods along the way.  Also,
--     negative powers have similar requirements to division.
--
-- We match on the type of arg1 because that is the only one which
-- will consistently be TyFin in the case of Div, Exp, and Divides.
-- compileBOp (TyFin n) _ _ op
--   | op `elem` [Div, Exp, Divides]
--   = CConst ((omOps ! op) n)
--   where
--     omOps = M.fromList
--       [ Div     ==> OMDiv
--       , Exp     ==> OMExp
--       , Divides ==> OMDivides
--       ]

-- Graph operations are separate, but use the same syntax, as traditional
-- addition and multiplication.
compileBOp :: Type -> Type -> Type -> BOp -> Core
compileBOp (TyGraph Type
_) (TyGraph Type
_) (TyGraph Type
_) BOp
op
  | BOp
op forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Add, BOp
Mul] =
      Op -> Core
CConst (Map BOp Op
regularOps forall k v. (Show k, Ord k) => Map k v -> k -> v
! BOp
op)
 where
  regularOps :: Map BOp Op
regularOps =
    forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
      [ BOp
Add forall a b. a -> b -> (a, b)
==> Op
OOverlay
      , BOp
Mul forall a b. a -> b -> (a, b)
==> Op
OConnect
      ]

-- The Cartesian product operator just compiles to library function calls.
compileBOp (TySet Type
_) Type
_ Type
_ BOp
CartProd =
  QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"setCP")
compileBOp (TyBag Type
_) Type
_ Type
_ BOp
CartProd =
  QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"container" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"bagCP")
compileBOp (TyList Type
_) Type
_ Type
_ BOp
CartProd =
  QName Core -> Core
CVar (ModuleProvenance -> String -> ModuleName
Named ModuleProvenance
Stdlib String
"list" forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
"listCP")
-- Some regular arithmetic operations that just translate straightforwardly.
compileBOp Type
_ Type
_ Type
_ BOp
op
  | BOp
op forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map BOp Op
regularOps = Op -> Core
CConst (Map BOp Op
regularOps forall k v. (Show k, Ord k) => Map k v -> k -> v
! BOp
op)
 where
  regularOps :: Map BOp Op
regularOps =
    forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
      [ BOp
Add forall a b. a -> b -> (a, b)
==> Op
OAdd
      , BOp
Mul forall a b. a -> b -> (a, b)
==> Op
OMul
      , BOp
Div forall a b. a -> b -> (a, b)
==> Op
ODiv
      , BOp
Exp forall a b. a -> b -> (a, b)
==> Op
OExp
      , BOp
Mod forall a b. a -> b -> (a, b)
==> Op
OMod
      , BOp
Divides forall a b. a -> b -> (a, b)
==> Op
ODivides
      , BOp
Choose forall a b. a -> b -> (a, b)
==> Op
OMultinom
      , BOp
Eq forall a b. a -> b -> (a, b)
==> Op
OEq
      , BOp
Lt forall a b. a -> b -> (a, b)
==> Op
OLt
      , BOp
And forall a b. a -> b -> (a, b)
==> Op
OAnd
      , BOp
Or forall a b. a -> b -> (a, b)
==> Op
OOr
      , BOp
Impl forall a b. a -> b -> (a, b)
==> Op
OImpl
      ]

-- ShouldEq needs to know the type at which the comparison is
-- occurring, so values can be correctly pretty-printed if the test
-- fails.
compileBOp Type
ty Type
_ Type
_ BOp
ShouldEq = Op -> Core
CConst (Type -> Op
OShouldEq Type
ty)
compileBOp Type
ty Type
_ Type
_ BOp
ShouldLt = Op -> Core
CConst (Type -> Op
OShouldLt 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 =
  forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! missing case in compileBOp: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Type
ty1, Type
ty2, Type
resTy, BOp
op)