-- |
-- 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 = 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 (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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 :: forall (r :: [(* -> *) -> * -> *]).
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 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)
Traversal' Defn (QName ATerm)
fvQ Defn
defn =
      [(QName Core, Core)] -> Sem r [(QName Core, Core)]
forall a. a -> Sem r a
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 a. a -> Sem r a
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
forall a b. Coercible a b => a -> b
coerce QName ATerm
f
  fL :: QName Core
fL = Name Core -> QName Core
forall a. Name a -> QName a
localName (Name ATerm -> Name Core
forall a b. Coercible a b => a -> b
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]
forall a b. Coercible a b => a -> b
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 a. a -> Sem r a
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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r Core
compileDTerm (DTVar Type
_ QName DTerm
x) = Core -> Sem r Core
forall a. a -> Sem r a
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
forall a b. Coercible a b => a -> b
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Core
CUnit
compileDTerm (DTBool Type
_ Bool
b) = Core -> Sem r Core
forall a. a -> Sem r a
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Rational -> Core
CNum (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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Rational -> Core
CNum (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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ Rational -> Core
CNum 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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ ShouldMemo -> [Name DTerm] -> Core -> Core
abstract ([Type] -> ShouldMemo
canMemo [Type]
tys) [Name DTerm]
xs Core
cbody
    Quantifier
Ex -> Core -> Sem r Core
forall a. a -> Sem r a
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) (ShouldMemo -> [Name DTerm] -> Core -> Core
abstract ShouldMemo
NoMemo [Name DTerm]
xs Core
cbody)
    Quantifier
All -> Core -> Sem r Core
forall a. a -> Sem r a
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) (ShouldMemo -> [Name DTerm] -> Core -> Core
abstract ShouldMemo
NoMemo [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 :: [(* -> *) -> * -> *]).
Member Fresh r =>
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 a. a -> Sem r a
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], DTerm
t)

  abstract :: ShouldMemo -> [Name DTerm] -> Core -> Core
  abstract :: ShouldMemo -> [Name DTerm] -> Core -> Core
abstract ShouldMemo
m [Name DTerm]
xs Core
body = ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
m ([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
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)

  -- Given a function's arguments, determine if it is memoizable.
  -- A function is memoizable if its arguments can be converted into
  -- a simple value (Haskell Ord instance can be derived).
  canMemo :: [Type] -> ShouldMemo
  canMemo :: [Type] -> ShouldMemo
canMemo [Type]
tys
    | (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
canMemoTy [Type]
tys = ShouldMemo
Memo
    | Bool
otherwise = ShouldMemo
NoMemo

  canMemoTy :: Type -> Bool
  canMemoTy :: Type -> Bool
canMemoTy (TyAtom Atom
a) = Atom -> Bool
canMemoAtom Atom
a
  -- Anti-higher order while allowing for curried functions.
  canMemoTy (TyCon Con
CArr tys :: [Type]
tys@(Type
t : [Type]
_)) = case Type
t of
    TyCon Con
CArr [Type]
_ -> Bool
False
    Type
_ -> (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
canMemoTy [Type]
tys
  canMemoTy (TyCon Con
c [Type]
tys) = Con -> Bool
canMemoCon Con
c Bool -> Bool -> Bool
&& (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
canMemoTy [Type]
tys

  canMemoCon :: Con -> Bool
  canMemoCon :: Con -> Bool
canMemoCon = \case
    Con
CArr -> Bool
False
    CUser String
_ -> Bool
False
    Con
CGraph -> Bool
False
    Con
CMap -> Bool
False
    CContainer Atom
a -> Atom -> Bool
canMemoAtom Atom
a
    Con
_ -> Bool
True

  canMemoAtom :: Atom -> Bool
  canMemoAtom :: Atom -> Bool
canMemoAtom (AVar Var
_) = Bool
False
  canMemoAtom (ABase BaseTy
b) = BaseTy -> Bool
canMemoBase BaseTy
b

  canMemoBase :: BaseTy -> Bool
  canMemoBase :: BaseTy -> Bool
canMemoBase = \case
    BaseTy
Gen -> Bool
False
    BaseTy
P -> Bool
False
    BaseTy
_ -> Bool
True

-- 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 a b. Sem r (a -> b) -> Sem r a -> Sem r b
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 a b. Sem r (a -> b) -> Sem r a -> Sem r b
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 a b. Sem r (a -> b) -> Sem r a -> Sem r b
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 a b. Sem r (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Core -> Sem r Core
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Core
CUnit
compileDTerm (DTTyOp Type
_ TyOp
op Type
ty) = Core -> Sem r Core
forall a. a -> Sem r a
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 a. a -> Sem r a
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)]
forall a b. Coercible a b => a -> b
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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Prim -> Sem r Core
compilePrim (Type
argTy :->: Type
_) (PrimUOp UOp
uop) = Core -> Sem r Core
forall a. a -> Sem r a
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo (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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo (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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo (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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 (TySet Type
_ :->: Type
_) Prim
PrimAbs =
  Core -> Sem r Core
forall a. a -> Sem r a
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
"setSize")
compilePrim (TyBag Type
_ :->: Type
_) Prim
PrimAbs =
  Core -> Sem r Core
forall a. a -> Sem r a
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
"bagSize")
compilePrim (TyList Type
_ :->: Type
_) Prim
PrimAbs =
  Core -> Sem r Core
forall a. a -> Sem r a
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
"length")
compilePrim Type
_ Prim
PrimAbs = Core -> Sem r Core
forall a. a -> Sem r a
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 (TySet Type
_ :->: Type
_) Prim
PrimPower = Core -> Sem r Core
forall a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prim
PrimList, Prim
PrimBag, Prim
PrimSet] = Core -> Sem r Core
forall a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 (Type
_ :->: TyBag Type
_) Prim
PrimUC2B = Core -> Sem r Core
forall a. a -> Sem r a
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
OUnsafeCountsToBag
compilePrim Type
ty Prim
PrimUC2B = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
compilePrimErr Prim
PrimUC2B Type
ty
compilePrim (TyMap Type
_ Type
_ :->: Type
_) Prim
PrimMapToSet = Core -> Sem r Core
forall a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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
_ Prim
PrimRandom = Core -> Sem r Core
forall a. a -> Sem r a
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
ORandom
compilePrim Type
_ Prim
PrimSeed = Core -> Sem r Core
forall a. a -> Sem r a
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
OSeed
compilePrim (Type
_ :*: TyList Type
_ :->: Type
_) Prim
PrimEach =
  Core -> Sem r Core
forall a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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
compilePrim Type
ty Prim
PrimMin = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
desugaredPrimErr Prim
PrimMin Type
ty
compilePrim Type
ty Prim
PrimMax = Prim -> Type -> Sem r Core
forall a. Prim -> Type -> a
desugaredPrimErr Prim
PrimMax Type
ty

compilePrimErr :: Prim -> Type -> a
compilePrimErr :: forall a. 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

desugaredPrimErr :: Prim -> Type -> a
desugaredPrimErr :: forall a. Prim -> Type -> a
desugaredPrimErr 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
" at type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", should have been desugared away"

------------------------------------------------------------
-- 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 :: [(* -> *) -> * -> *]).
Member Fresh r =>
[DBranch] -> Sem r Core
compileCase [] = Core -> Sem r Core
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo ([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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo ([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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DBranch -> Sem r Core
compileBranch DBranch
b = do
  (Telescope (Guard_ DS)
gs, DTerm
e) <- DBranch -> Sem r (Telescope (Guard_ DS), 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 <- [Guard_ DS] -> Name Core -> Core -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Guard_ DS] -> Name Core -> Core -> Sem r Core
compileGuards (Telescope (Guard_ DS) -> [Guard_ DS]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope (Guard_ DS)
gs) Name Core
k Core
c
  Core -> Sem r Core
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Core -> Sem r Core) -> Core -> Sem r Core
forall a b. (a -> b) -> a -> b
$ ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo ([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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Guard_ DS] -> Name Core -> Core -> Sem r Core
compileGuards [] Name Core
_ Core
e = Core -> Sem r Core
forall a. a -> Sem r a
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) Pattern_ DS
p : [Guard_ DS]
gs) Name Core
k Core
e = do
  Core
e' <- [Guard_ DS] -> Name Core -> Core -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Guard_ DS] -> Name Core -> Core -> Sem r Core
compileGuards [Guard_ DS]
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
  Pattern_ DS -> Core -> Name Core -> Core -> Sem r Core
forall (r :: [(* -> *) -> * -> *]).
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 :: [(* -> *) -> * -> *]).
Member Fresh r =>
Pattern_ DS -> Core -> Name Core -> Core -> Sem r Core
compileMatch (DPVar Type
_ Name DTerm
x) Core
s Name Core
_ Core
e = Core -> Sem r Core
forall a. a -> Sem r a
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 (ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name DTerm -> Name Core
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 = Core -> Sem r Core
forall a. a -> Sem r a
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 (ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo ([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 Pattern_ DS
DPUnit Core
s Name Core
_ Core
e = Core -> Sem r Core
forall a. a -> Sem r a
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 (ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo ([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 a. a -> Sem r a
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
      ( ShouldMemo -> Bind [Name Core] Core -> Core
CAbs
          ShouldMemo
NoMemo
          ( [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
                      (ShouldMemo -> Bind [Name Core] Core -> Core
CAbs ShouldMemo
NoMemo ([Name Core] -> Core -> Bind [Name Core] Core
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name DTerm -> Name Core
forall a b. Coercible a b => a -> b
coerce Name DTerm
x1, Name DTerm -> Name Core
forall a b. Coercible a b => a -> b
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 a. a -> Sem r a
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
forall a b. Coercible a b => a -> b
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 a. a -> Sem r a
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
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 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
      , UOp
Not UOp -> Op -> (UOp, Op)
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 BOp -> [BOp] -> Bool
forall a. Eq a => a -> [a] -> 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
      ]

-- 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" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
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" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
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" ModuleName -> Name Core -> QName Core
forall a. ModuleName -> Name a -> QName a
.- String -> Name Core
forall a. String -> Name a
string2Name String
"listCP")
-- 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
      , BOp
And BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OAnd
      , BOp
Or BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OOr
      , BOp
Impl BOp -> Op -> (BOp, Op)
forall a b. a -> b -> (a, b)
==> Op
OImpl
      ]

-- Should 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
_ (Should BOp
op) = Op -> Core
CConst (BOp -> Type -> Op
OShould BOp
op 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)