disco-0.2: src/Disco/Compile.hs
-- |
-- 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 desugarThing = run . runFresh . (compileDTerm <=< desugarThing)
-- | Compile a typechecked term ('ATerm') directly to a 'Core' term,
-- by desugaring and then compiling.
compileTerm :: ATerm -> Core
compileTerm = compileThing desugarTerm
-- | Compile a typechecked property ('AProperty') directly to a 'Core' term,
-- by desugaring and then compilling.
compileProperty :: AProperty -> Core
compileProperty = compileThing 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 defs = run . runFresh $ do
let vars = Ctx.keysSet 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 = S.unions . map (\(x, body) -> S.map (,x) (setOf (fvQ @Defn @ATerm) body)) . Ctx.assocs $ 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 = G.topsort (G.condensation (G.mkGraph vars deps))
concat <$> mapM (compileDefnGroup . Ctx.assocs . Ctx.restrictKeys defs) 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 [(f, 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)
| f `S.member` setOf fvQ defn =
return . (: []) $
(fT, CForce (CProj L (CDelay (bind [qname fL] [substQC fT (CForce (CVar fL)) cdefn]))))
-- A non-recursive definition just compiles simply.
| otherwise =
return [(fT, cdefn)]
where
fT, fL :: QName Core
fT = coerce f
fL = localName (coerce (qname f))
cdefn = compileThing desugarDefn 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 defs = do
grp :: QName Core <- freshQ "__grp"
let (vars, bodies) = unzip defs
varsT, varsL :: [QName Core]
varsT = coerce vars
varsL = map (localName . qname) varsT
forceVars :: [(QName Core, Core)]
forceVars = zipWith (\t l -> (t, CForce (CVar l))) varsT varsL
bodies' :: [Core]
bodies' = map (substsQC forceVars . compileThing desugarDefn) bodies
return $
(grp, CDelay (bind (map qname varsL) bodies'))
: zip varsT (for [0 ..] $ CForce . flip proj (CVar grp))
where
proj :: Int -> Core -> Core
proj 0 = CProj L
proj n = proj (n - 1) . CProj R
------------------------------------------------------------
-- Compiling terms
------------------------------------------------------------
-- | Compile a typechecked, desugared 'DTerm' to an untyped 'Core'
-- term.
compileDTerm :: Member Fresh r => DTerm -> Sem r Core
compileDTerm (DTVar _ x) = return $ CVar (coerce x)
compileDTerm (DTPrim ty x) = compilePrim ty x
compileDTerm DTUnit = return CUnit
compileDTerm (DTBool _ b) = return $ CInj (bool L R b) CUnit
compileDTerm (DTChar c) = return $ CNum (toInteger (fromEnum c) % 1)
compileDTerm (DTNat _ n) = return $ CNum (n % 1) -- compileNat ty n
compileDTerm (DTRat r) = return $ CNum r
compileDTerm term@(DTAbs q _ _) = do
(xs, tys, body) <- unbindDeep term
cbody <- compileDTerm body
case q of
Lam -> return $ abstract (canMemo tys) xs cbody
Ex -> return $ quantify (OExists tys) (abstract NoMemo xs cbody)
All -> return $ quantify (OForall tys) (abstract NoMemo xs cbody)
where
-- Gather nested abstractions with the same quantifier.
unbindDeep :: Member Fresh r => DTerm -> Sem r ([Name DTerm], [Type], DTerm)
unbindDeep (DTAbs q' ty l) | q == q' = do
(name, inner) <- unbind l
(ns, tys, body) <- unbindDeep inner
return (name : ns, ty : tys, body)
unbindDeep t = return ([], [], t)
abstract :: ShouldMemo -> [Name DTerm] -> Core -> Core
abstract m xs body = CAbs m (bind (map coerce xs) body)
quantify :: Op -> Core -> Core
quantify op = CApp (CConst 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 tys
| all canMemoTy tys = Memo
| otherwise = NoMemo
canMemoTy :: Type -> Bool
canMemoTy (TyAtom a) = canMemoAtom a
-- Anti-higher order while allowing for curried functions.
canMemoTy (TyCon CArr tys@(t : _)) = case t of
TyCon CArr _ -> False
_ -> all canMemoTy tys
canMemoTy (TyCon c tys) = canMemoCon c && all canMemoTy tys
canMemoCon :: Con -> Bool
canMemoCon = \case
CArr -> False
CUser _ -> False
CGraph -> False
CMap -> False
CContainer a -> canMemoAtom a
_ -> True
canMemoAtom :: Atom -> Bool
canMemoAtom (AVar _) = False
canMemoAtom (ABase b) = canMemoBase b
canMemoBase :: BaseTy -> Bool
canMemoBase = \case
Gen -> False
P -> False
_ -> True
-- Special case for Cons, which compiles to a constructor application
-- rather than a function application.
compileDTerm (DTApp _ (DTPrim _ (PrimBOp Cons)) (DTPair _ t1 t2)) =
CInj R <$> (CPair <$> compileDTerm t1 <*> compileDTerm t2)
-- Special cases for left and right, which also compile to constructor applications.
compileDTerm (DTApp _ (DTPrim _ PrimLeft) t) =
CInj L <$> compileDTerm t
compileDTerm (DTApp _ (DTPrim _ PrimRight) t) =
CInj R <$> compileDTerm t
compileDTerm (DTApp _ t1 t2) = CApp <$> compileDTerm t1 <*> compileDTerm t2
compileDTerm (DTPair _ t1 t2) =
CPair <$> compileDTerm t1 <*> compileDTerm t2
compileDTerm (DTCase _ bs) = CApp <$> compileCase bs <*> pure CUnit
compileDTerm (DTTyOp _ op ty) = return $ CApp (CConst (tyOps ! op)) (CType ty)
where
tyOps =
M.fromList
[ Enumerate ==> OEnum
, Count ==> OCount
]
compileDTerm (DTNil _) = return $ CInj L CUnit
compileDTerm (DTTest info t) = CTest (coerce info) <$> compileDTerm 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 (argTy :->: _) (PrimUOp uop) = return $ compileUOp argTy uop
compilePrim ty p@(PrimUOp _) = compilePrimErr p 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 _ (PrimBOp Cons) = do
hd <- fresh (string2Name "hd")
tl <- fresh (string2Name "tl")
return $ CAbs NoMemo $ bind [hd, tl] $ CInj R (CPair (CVar (localName hd)) (CVar (localName tl)))
compilePrim _ PrimLeft = do
a <- fresh (string2Name "a")
return $ CAbs NoMemo $ bind [a] $ CInj L (CVar (localName a))
compilePrim _ PrimRight = do
a <- fresh (string2Name "a")
return $ CAbs NoMemo $ bind [a] $ CInj R (CVar (localName a))
compilePrim (ty1 :*: ty2 :->: resTy) (PrimBOp bop) = return $ compileBOp ty1 ty2 resTy bop
compilePrim ty p@(PrimBOp _) = compilePrimErr p ty
compilePrim _ PrimSqrt = return $ CConst OSqrt
compilePrim _ PrimFloor = return $ CConst OFloor
compilePrim _ PrimCeil = return $ CConst OCeil
compilePrim (TySet _ :->: _) PrimAbs =
return $
CVar (Named Stdlib "container" .- string2Name "setSize")
compilePrim (TyBag _ :->: _) PrimAbs =
return $
CVar (Named Stdlib "container" .- string2Name "bagSize")
compilePrim (TyList _ :->: _) PrimAbs =
return $
CVar (Named Stdlib "list" .- string2Name "length")
compilePrim _ PrimAbs = return $ CConst OAbs
compilePrim (TySet _ :->: _) PrimPower = return $ CConst OPower
compilePrim (TyBag _ :->: _) PrimPower = return $ CConst OPower
compilePrim ty PrimPower = compilePrimErr PrimPower ty
compilePrim (TySet _ :->: _) PrimList = return $ CConst OSetToList
compilePrim (TyBag _ :->: _) PrimSet = return $ CConst OBagToSet
compilePrim (TyBag _ :->: _) PrimList = return $ CConst OBagToList
compilePrim (TyList _ :->: _) PrimSet = return $ CConst OListToSet
compilePrim (TyList _ :->: _) PrimBag = return $ CConst OListToBag
compilePrim _ p | p `elem` [PrimList, PrimBag, PrimSet] = return $ CConst OId
compilePrim ty PrimList = compilePrimErr PrimList ty
compilePrim ty PrimBag = compilePrimErr PrimBag ty
compilePrim ty PrimSet = compilePrimErr PrimSet ty
compilePrim _ PrimB2C = return $ CConst OBagToCounts
compilePrim (_ :->: TyBag _) PrimC2B = return $ CConst OCountsToBag
compilePrim ty PrimC2B = compilePrimErr PrimC2B ty
compilePrim (_ :->: TyBag _) PrimUC2B = return $ CConst OUnsafeCountsToBag
compilePrim ty PrimUC2B = compilePrimErr PrimUC2B ty
compilePrim (TyMap _ _ :->: _) PrimMapToSet = return $ CConst OMapToSet
compilePrim (_ :->: TyMap _ _) PrimSetToMap = return $ CConst OSetToMap
compilePrim ty PrimMapToSet = compilePrimErr PrimMapToSet ty
compilePrim ty PrimSetToMap = compilePrimErr PrimSetToMap ty
compilePrim _ PrimSummary = return $ CConst OSummary
compilePrim (_ :->: TyGraph _) PrimVertex = return $ CConst OVertex
compilePrim (TyGraph _) PrimEmptyGraph = return $ CConst OEmptyGraph
compilePrim (_ :->: TyGraph _) PrimOverlay = return $ CConst OOverlay
compilePrim (_ :->: TyGraph _) PrimConnect = return $ CConst OConnect
compilePrim ty PrimVertex = compilePrimErr PrimVertex ty
compilePrim ty PrimEmptyGraph = compilePrimErr PrimEmptyGraph ty
compilePrim ty PrimOverlay = compilePrimErr PrimOverlay ty
compilePrim ty PrimConnect = compilePrimErr PrimConnect ty
compilePrim _ PrimInsert = return $ CConst OInsert
compilePrim _ PrimLookup = return $ CConst OLookup
compilePrim _ PrimRandom = return $ CConst ORandom
compilePrim _ PrimSeed = return $ CConst OSeed
compilePrim (_ :*: TyList _ :->: _) PrimEach =
return $
CVar (Named Stdlib "list" .- string2Name "eachlist")
compilePrim (_ :*: TyBag _ :->: TyBag _) PrimEach = return $ CConst OEachBag
compilePrim (_ :*: TySet _ :->: TySet _) PrimEach = return $ CConst OEachSet
compilePrim ty PrimEach = compilePrimErr PrimEach ty
compilePrim (_ :*: _ :*: TyList _ :->: _) PrimReduce =
return $ CVar (Named Stdlib "list" .- string2Name "foldr")
compilePrim (_ :*: _ :*: TyBag _ :->: _) PrimReduce =
return $
CVar (Named Stdlib "container" .- string2Name "reducebag")
compilePrim (_ :*: _ :*: TySet _ :->: _) PrimReduce =
return $
CVar (Named Stdlib "container" .- string2Name "reduceset")
compilePrim ty PrimReduce = compilePrimErr PrimReduce ty
compilePrim (_ :*: TyList _ :->: _) PrimFilter =
return $
CVar (Named Stdlib "list" .- string2Name "filterlist")
compilePrim (_ :*: TyBag _ :->: _) PrimFilter = return $ CConst OFilterBag
compilePrim (_ :*: TySet _ :->: _) PrimFilter = return $ CConst OFilterBag
compilePrim ty PrimFilter = compilePrimErr PrimFilter ty
compilePrim (_ :->: TyList _) PrimJoin =
return $
CVar (Named Stdlib "list" .- string2Name "concat")
compilePrim (_ :->: TyBag _) PrimJoin = return $ CConst OBagUnions
compilePrim (_ :->: TySet _) PrimJoin =
return $
CVar (Named Stdlib "container" .- string2Name "unions")
compilePrim ty PrimJoin = compilePrimErr PrimJoin ty
compilePrim (_ :*: TyBag _ :*: _ :->: _) PrimMerge = return $ CConst OMerge
compilePrim (_ :*: TySet _ :*: _ :->: _) PrimMerge = return $ CConst OMerge
compilePrim ty PrimMerge = compilePrimErr PrimMerge ty
compilePrim _ PrimIsPrime = return $ CConst OIsPrime
compilePrim _ PrimFactor = return $ CConst OFactor
compilePrim _ PrimFrac = return $ CConst OFrac
compilePrim _ PrimCrash = return $ CConst OCrash
compilePrim _ PrimUntil = return $ CConst OUntil
compilePrim _ PrimHolds = return $ CConst OHolds
compilePrim _ PrimLookupSeq = return $ CConst OLookupSeq
compilePrim _ PrimExtendSeq = return $ CConst OExtendSeq
compilePrim ty PrimMin = desugaredPrimErr PrimMin ty
compilePrim ty PrimMax = desugaredPrimErr PrimMax ty
compilePrimErr :: Prim -> Type -> a
compilePrimErr p ty = error $ "Impossible! compilePrim " ++ show p ++ " on bad type " ++ show ty
desugaredPrimErr :: Prim -> Type -> a
desugaredPrimErr p ty = error $ "Impossible! compilePrim " ++ show p ++ " at type " ++ show ty ++ ", 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 [] = return $ CAbs NoMemo (bind [string2Name "_"] (CConst OMatchErr))
-- empty case ==> λ _ . error
compileCase (b : bs) = do
c1 <- compileBranch b
c2 <- compileCase bs
return $ CAbs NoMemo (bind [string2Name "_"] (CApp c1 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 b = do
(gs, e) <- unbind b
c <- compileDTerm e
k <- fresh (string2Name "k") -- Fresh name for the failure continuation
bc <- compileGuards (fromTelescope gs) k c
return $ CAbs NoMemo (bind [k] 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 [] _ e = return e
compileGuards (DGPat (unembed -> s) p : gs) k e = do
e' <- compileGuards gs k e
s' <- compileDTerm s
compileMatch p s' k 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 (DPVar _ x) s _ e = return $ CApp (CAbs NoMemo (bind [coerce x] e)) 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 _) s _ e = return $ CApp (CAbs NoMemo (bind [string2Name "_"] e)) s
compileMatch DPUnit s _ e = return $ CApp (CAbs NoMemo (bind [string2Name "_"] e)) s
compileMatch (DPPair _ x1 x2) s _ e = do
y <- fresh (string2Name "y")
-- {? e when s is (x1,x2) ?} ==> (\y. (\x1.\x2. e) (fst y) (snd y)) s
return $
CApp
( CAbs
NoMemo
( bind
[y]
( CApp
( CApp
(CAbs NoMemo (bind [coerce x1, coerce x2] e))
(CProj L (CVar (localName y)))
)
(CProj R (CVar (localName y)))
)
)
)
s
compileMatch (DPInj _ L x) s k e =
-- {? e when s is left(x) ?} ==> case s of {left x -> e; right _ -> k unit}
return $ CCase s (bind (coerce x) e) (bind (string2Name "_") (CApp (CVar (localName k)) CUnit))
compileMatch (DPInj _ R x) s k e =
-- {? e when s is right(x) ?} ==> case s of {left _ -> k unit; right x -> e}
return $ CCase s (bind (string2Name "_") (CApp (CVar (localName k)) CUnit)) (bind (coerce x) e)
------------------------------------------------------------
-- Unary and binary operators
------------------------------------------------------------
-- | Compile a unary operator.
compileUOp ::
-- | Type of the operator argument
Type ->
UOp ->
Core
compileUOp _ op = CConst (coreUOps ! op)
where
-- Just look up the corresponding core operator.
coreUOps =
M.fromList
[ Neg ==> ONeg
, Fact ==> OFact
, Not ==> 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 (TyGraph _) (TyGraph _) (TyGraph _) op
| op `elem` [Add, Mul] =
CConst (regularOps ! op)
where
regularOps =
M.fromList
[ Add ==> OOverlay
, Mul ==> OConnect
]
-- The Cartesian product operator just compiles to library function calls.
compileBOp (TySet _) _ _ CartProd =
CVar (Named Stdlib "container" .- string2Name "setCP")
compileBOp (TyBag _) _ _ CartProd =
CVar (Named Stdlib "container" .- string2Name "bagCP")
compileBOp (TyList _) _ _ CartProd =
CVar (Named Stdlib "list" .- string2Name "listCP")
-- Some regular arithmetic operations that just translate straightforwardly.
compileBOp _ _ _ op
| op `M.member` regularOps = CConst (regularOps ! op)
where
regularOps =
M.fromList
[ Add ==> OAdd
, Mul ==> OMul
, Div ==> ODiv
, Exp ==> OExp
, Mod ==> OMod
, Divides ==> ODivides
, Choose ==> OMultinom
, Eq ==> OEq
, Lt ==> OLt
, And ==> OAnd
, Or ==> OOr
, Impl ==> 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 ty _ _ (Should op) = CConst (OShould op ty)
compileBOp _ty (TyList _) _ Elem = CConst OListElem
compileBOp _ty _ _ Elem = CConst OBagElem
compileBOp ty1 ty2 resTy op =
error $ "Impossible! missing case in compileBOp: " ++ show (ty1, ty2, resTy, op)