-----------------------------------------------------------------------------
-- |
-- 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 :: (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)

-- | Compile a typechecked term ('ATerm') directly to a 'Core' term,
--   by desugaring and then compiling.
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

-- | Compile a typechecked property ('AProperty') directly to a 'Core' term,
--   by desugaring and then compilling.
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

------------------------------------------------------------
-- 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 = 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

      -- 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 = [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

      -- 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 = 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

-- | 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 :: [(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 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]))))

  -- A non-recursive definition just compiles simply.
  | 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

-- 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 <- 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

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

-- | Compile a typechecked, desugared 'DTerm' to an untyped 'Core'
--   term.
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) -- compileNat ty n
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
    -- Gather nested abstractions with the same quantifier.
    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)

-- 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 (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)
-- 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 (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

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

-- | 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 :: 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
-- 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 <- 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

------------------------------------------------------------
-- 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 :: [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))
-- empty case ==>  λ _ . error

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))

-- | 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 :: 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") -- Fresh name for the failure continuation
  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' 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 :: [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' 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 :: 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
-- 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 = 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")

  -- {? e when s is (x1,x2) ?}   ==>   (\y. (\x1.\x2. e) (fst y) (snd y)) s
  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 =
  -- {? e when s is left(x) ?}   ==>   case s of {left x -> e; right _ -> k unit}
  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 =
  -- {? e when s is right(x) ?}   ==>   case s of {left _ -> k unit; right x -> 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)

------------------------------------------------------------
-- 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 Map UOp Op -> UOp -> Op
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 =
      [(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
        ]

-- | 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 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
        ]

-- Some regular arithmetic operations that just translate straightforwardly.
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
        ]

-- 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 (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)