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

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

-- |
-- Module      :  Disco.Desugar
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Desugaring the typechecked surface language to a (still typed)
-- simpler language.
module Disco.Desugar (
  -- * Running desugaring computations
  runDesugar,

  -- * Programs, terms, and properties
  desugarDefn,
  desugarTerm,
  desugarProperty,

  -- * Case expressions and patterns
  desugarBranch,
  desugarGuards,
)
where

import Control.Monad.Cont
import Data.Bool (bool)
import Data.Coerce
import Data.Maybe (fromMaybe, isJust)

import Disco.AST.Desugared
import Disco.AST.Surface
import Disco.AST.Typed
import Disco.Module
import Disco.Names
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Typecheck (containerTy)
import Disco.Types

import Disco.Effects.Fresh
import Polysemy (Member, Sem, run)
import Unbound.Generics.LocallyNameless (
  Bind,
  Name,
  bind,
  embed,
  name2String,
  string2Name,
  unembed,
  unrebind,
 )
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)

------------------------------------------------------------
-- Running desugaring computations
------------------------------------------------------------

-- | Run a desugaring computation.
runDesugar :: Sem '[Fresh] a -> a
runDesugar :: forall a. Sem '[Fresh] a -> a
runDesugar = forall a. Sem '[] a -> a
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: [(* -> *) -> * -> *]) a. Sem (Fresh : r) a -> Sem r a
runFresh1

-- Using runFresh1 is a bit of a hack; that way we won't
-- ever pick a name with #0 (which is what is generated by default
-- by string2Name), hence won't conflict with any existing free
-- variables which came from the parser.

------------------------------------------------------------
-- ATerm DSL
------------------------------------------------------------

-- A tiny DSL for building certain ATerms, which is helpful for
-- writing desugaring rules.

-- Make a local ATVar.
atVar :: Type -> Name ATerm -> ATerm
atVar :: Type -> Name ATerm -> ATerm
atVar Type
ty Name ATerm
x = Type -> QName ATerm -> ATerm
ATVar Type
ty (forall a. NameProvenance -> Name a -> QName a
QName NameProvenance
LocalName Name ATerm
x)

tapp :: ATerm -> ATerm -> ATerm
tapp :: ATerm -> ATerm -> ATerm
tapp ATerm
t1 ATerm
t2 = Type -> ATerm -> ATerm -> ATerm
ATApp Type
resTy ATerm
t1 ATerm
t2
 where
  resTy :: Type
resTy = case forall t. HasType t => t -> Type
getType ATerm
t1 of
    (Type
_ :->: Type
r) -> Type
r
    Type
ty -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! Got non-function type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty forall a. [a] -> [a] -> [a]
++ String
" in tapp"

mkBin :: Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin :: Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
resTy BOp
bop ATerm
t1 ATerm
t2 =
  ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim (forall t. HasType t => t -> Type
getType ATerm
t1 Type -> Type -> Type
:*: forall t. HasType t => t -> Type
getType ATerm
t2 Type -> Type -> Type
:->: Type
resTy) (BOp -> Prim
PrimBOp BOp
bop)) (ATerm -> ATerm -> ATerm
mkPair ATerm
t1 ATerm
t2)

mkUn :: Type -> UOp -> ATerm -> ATerm
mkUn :: Type -> UOp -> ATerm -> ATerm
mkUn Type
resTy UOp
uop ATerm
t = ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim (forall t. HasType t => t -> Type
getType ATerm
t Type -> Type -> Type
:->: Type
resTy) (UOp -> Prim
PrimUOp UOp
uop)) ATerm
t

mkPair :: ATerm -> ATerm -> ATerm
mkPair :: ATerm -> ATerm -> ATerm
mkPair ATerm
t1 ATerm
t2 = [ATerm] -> ATerm
mkTup [ATerm
t1, ATerm
t2]

mkTup :: [ATerm] -> ATerm
mkTup :: [ATerm] -> ATerm
mkTup [ATerm]
ts = Type -> [ATerm] -> ATerm
ATTup (forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
(:*:) (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasType t => t -> Type
getType [ATerm]
ts)) [ATerm]
ts

tapps :: ATerm -> [ATerm] -> ATerm
tapps :: ATerm -> [ATerm] -> ATerm
tapps ATerm
t [ATerm]
ts = ATerm -> ATerm -> ATerm
tapp ATerm
t ([ATerm] -> ATerm
mkTup [ATerm]
ts)

infixr 2 ||.
(||.) :: ATerm -> ATerm -> ATerm
||. :: ATerm -> ATerm -> ATerm
(||.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Or

infixl 6 -., +.
(-.) :: ATerm -> ATerm -> ATerm
ATerm
at1 -. :: ATerm -> ATerm -> ATerm
-. ATerm
at2 = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin (forall t. HasType t => t -> Type
getType ATerm
at1) BOp
Sub ATerm
at1 ATerm
at2

(+.) :: ATerm -> ATerm -> ATerm
ATerm
at1 +. :: ATerm -> ATerm -> ATerm
+. ATerm
at2 = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin (forall t. HasType t => t -> Type
getType ATerm
at1) BOp
Add ATerm
at1 ATerm
at2

infixl 7 /.
(/.) :: ATerm -> ATerm -> ATerm
ATerm
at1 /. :: ATerm -> ATerm -> ATerm
/. ATerm
at2 = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin (forall t. HasType t => t -> Type
getType ATerm
at1) BOp
Div ATerm
at1 ATerm
at2

infix 4 <., >=.
(<.) :: ATerm -> ATerm -> ATerm
<. :: ATerm -> ATerm -> ATerm
(<.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Lt

(>=.) :: ATerm -> ATerm -> ATerm
>=. :: ATerm -> ATerm -> ATerm
(>=.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Geq

(|.) :: ATerm -> ATerm -> ATerm
|. :: ATerm -> ATerm -> ATerm
(|.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Divides

infix 4 ==.
(==.) :: ATerm -> ATerm -> ATerm
==. :: ATerm -> ATerm -> ATerm
(==.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Eq

tnot :: ATerm -> ATerm
tnot :: ATerm -> ATerm
tnot = ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim (Type
TyBool Type -> Type -> Type
:->: Type
TyBool) (UOp -> Prim
PrimUOp UOp
Not))

(<==.) :: ATerm -> [AGuard] -> ABranch
ATerm
t <==. :: ATerm -> [AGuard] -> ABranch
<==. [AGuard]
gs = forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (forall b. Alpha b => [b] -> Telescope b
toTelescope [AGuard]
gs) ATerm
t

fls :: ATerm
fls :: ATerm
fls = Type -> Bool -> ATerm
ATBool Type
TyBool Bool
False

tru :: ATerm
tru :: ATerm
tru = Type -> Bool -> ATerm
ATBool Type
TyBool Bool
True

tif :: ATerm -> AGuard
tif :: ATerm -> AGuard
tif ATerm
t = Embed ATerm -> AGuard
AGBool (forall e. IsEmbed e => Embedded e -> e
embed ATerm
t)

ctrNil :: Container -> Type -> ATerm
ctrNil :: Container -> Type -> ATerm
ctrNil Container
ctr Type
ty = Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> ATerm
ATContainer (Container -> Type -> Type
containerTy Container
ctr Type
ty) Container
ctr [] forall a. Maybe a
Nothing

ctrSingleton :: Container -> ATerm -> ATerm
ctrSingleton :: Container -> ATerm -> ATerm
ctrSingleton Container
ctr ATerm
t = Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> ATerm
ATContainer (Container -> Type -> Type
containerTy Container
ctr (forall t. HasType t => t -> Type
getType ATerm
t)) Container
ctr [(ATerm
t, forall a. Maybe a
Nothing)] forall a. Maybe a
Nothing

------------------------------------------------------------
-- Making DTerms
------------------------------------------------------------

dtVar :: Type -> Name DTerm -> DTerm
dtVar :: Type -> Name DTerm -> DTerm
dtVar Type
ty Name DTerm
x = Type -> QName DTerm -> DTerm
DTVar Type
ty (forall a. NameProvenance -> Name a -> QName a
QName NameProvenance
LocalName Name DTerm
x)

dtapp :: DTerm -> DTerm -> DTerm
dtapp :: DTerm -> DTerm -> DTerm
dtapp DTerm
t1 DTerm
t2 = Type -> DTerm -> DTerm -> DTerm
DTApp Type
resTy DTerm
t1 DTerm
t2
 where
  resTy :: Type
resTy = case forall t. HasType t => t -> Type
getType DTerm
t1 of
    (Type
_ :->: Type
r) -> Type
r
    Type
ty -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! Got non-function type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty forall a. [a] -> [a] -> [a]
++ String
" in dtapp"

dtbin :: Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin :: Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
resTy Prim
p DTerm
dt1 DTerm
dt2 =
  DTerm -> DTerm -> DTerm
dtapp (Type -> Prim -> DTerm
DTPrim (forall t. HasType t => t -> Type
getType DTerm
dt1 Type -> Type -> Type
:*: forall t. HasType t => t -> Type
getType DTerm
dt2 Type -> Type -> Type
:->: Type
resTy) Prim
p) (DTerm -> DTerm -> DTerm
mkDTPair DTerm
dt1 DTerm
dt2)

mkDTPair :: DTerm -> DTerm -> DTerm
mkDTPair :: DTerm -> DTerm -> DTerm
mkDTPair DTerm
dt1 DTerm
dt2 = Type -> DTerm -> DTerm -> DTerm
DTPair (forall t. HasType t => t -> Type
getType DTerm
dt1 Type -> Type -> Type
:*: forall t. HasType t => t -> Type
getType DTerm
dt2) DTerm
dt1 DTerm
dt2

------------------------------------------------------------
-- Definition desugaring
------------------------------------------------------------

-- | Desugar a definition (consisting of a collection of pattern
--   clauses with bodies) into a core language term.
desugarDefn :: Member Fresh r => Defn -> Sem r DTerm
desugarDefn :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Defn -> Sem r DTerm
desugarDefn (Defn Name ATerm
_ [Type]
patTys Type
bodyTy [Bind [Pattern_ TY] ATerm]
def) =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Quantifier -> Type -> [Bind [Pattern_ TY] ATerm] -> Sem r DTerm
desugarAbs Quantifier
Lam (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(:->:) Type
bodyTy [Type]
patTys) [Bind [Pattern_ TY] ATerm]
def

------------------------------------------------------------
-- Abstraction desugaring
------------------------------------------------------------

-- | Desugar an abstraction -- that is, a collection of clauses
--   with their corresponding patterns. Definitions are abstractions
--   (which happen to be named), and source-level lambdas are also
--   abstractions (which happen to have only one clause).
desugarAbs :: Member Fresh r => Quantifier -> Type -> [Clause] -> Sem r DTerm
-- Special case for compiling a single lambda with no pattern matching directly to a lambda
desugarAbs :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Quantifier -> Type -> [Bind [Pattern_ TY] ATerm] -> Sem r DTerm
desugarAbs Quantifier
Lam Type
ty [cl :: Bind [Pattern_ TY] ATerm
cl@(forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> ([APVar Type
_ Name ATerm
_], ATerm
_))] = do
  ([Pattern_ TY]
ps, ATerm
at) <- forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Pattern_ TY] ATerm
cl
  DTerm
d <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
at
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
Lam Type
ty (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (forall {b}. Coercible b (Name ATerm) => Pattern_ TY -> b
getVar (forall a. [a] -> a
head [Pattern_ TY]
ps)) DTerm
d)
 where
  getVar :: Pattern_ TY -> b
getVar (APVar Type
_ Name ATerm
x) = coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x
-- General case
desugarAbs Quantifier
quant Type
overallTy [Bind [Pattern_ TY] ATerm]
body = do
  [([Pattern_ TY], ATerm)]
clausePairs <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Bind [Pattern_ TY] ATerm] -> Sem r [([Pattern_ TY], ATerm)]
unbindClauses [Bind [Pattern_ TY] ATerm]
body
  let ([[Pattern_ TY]]
pats, [ATerm]
bodies) = forall a b. [(a, b)] -> ([a], [b])
unzip [([Pattern_ TY], ATerm)]
clausePairs
  let patTys :: [Type]
patTys = forall a b. (a -> b) -> [a] -> [b]
map forall t. HasType t => t -> Type
getType (forall a. [a] -> a
head [[Pattern_ TY]]
pats)
  let bodyTy :: Type
bodyTy = forall t. HasType t => t -> Type
getType (forall a. [a] -> a
head [ATerm]
bodies)

  -- generate dummy variables for lambdas
  [Name ATerm]
args <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Pattern_ TY
_ Int
i -> forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name (String
"arg" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i))) (forall a. [a] -> a
head [[Pattern_ TY]]
pats) [Int
0 :: Int ..]

  -- Create lambdas and one big case.  Recursively desugar the case to
  -- deal with arithmetic patterns.
  let branches :: [ABranch]
branches = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ([(Name ATerm, Type)] -> ATerm -> [Pattern_ TY] -> ABranch
mkBranch (forall a b. [a] -> [b] -> [(a, b)]
zip [Name ATerm]
args [Type]
patTys)) [ATerm]
bodies [[Pattern_ TY]]
pats
  DTerm
dcase <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ Type -> [ABranch] -> ATerm
ATCase Type
bodyTy [ABranch]
branches
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Quantifier -> Type -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkAbs Quantifier
quant Type
overallTy [Type]
patTys (coerce :: forall a b. Coercible a b => a -> b
coerce [Name ATerm]
args) DTerm
dcase
 where
  mkBranch :: [(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch
  mkBranch :: [(Name ATerm, Type)] -> ATerm -> [Pattern_ TY] -> ABranch
mkBranch [(Name ATerm, Type)]
xs ATerm
b [Pattern_ TY]
ps = forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([(Name ATerm, Type)] -> [Pattern_ TY] -> Telescope AGuard
mkGuards [(Name ATerm, Type)]
xs [Pattern_ TY]
ps) ATerm
b

  mkGuards :: [(Name ATerm, Type)] -> [APattern] -> Telescope AGuard
  mkGuards :: [(Name ATerm, Type)] -> [Pattern_ TY] -> Telescope AGuard
mkGuards [(Name ATerm, Type)]
xs [Pattern_ TY]
ps = forall b. Alpha b => [b] -> Telescope b
toTelescope forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Embed ATerm -> Pattern_ TY -> AGuard
AGPat (forall a b. (a -> b) -> [a] -> [b]
map (\(Name ATerm
x, Type
ty) -> forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name ATerm -> ATerm
atVar Type
ty Name ATerm
x)) [(Name ATerm, Type)]
xs) [Pattern_ TY]
ps

  -- To make searches fairer, we lift up directly nested abstractions
  -- with the same quantifier when there's only a single clause. That
  -- way, we generate a chain of abstractions followed by a case, instead
  -- of a bunch of alternating abstractions and cases.
  unbindClauses :: Member Fresh r => [Clause] -> Sem r [([APattern], ATerm)]
  unbindClauses :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Bind [Pattern_ TY] ATerm] -> Sem r [([Pattern_ TY], ATerm)]
unbindClauses [Bind [Pattern_ TY] ATerm
c] | Quantifier
quant forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Quantifier
All, Quantifier
Ex] = do
    ([Pattern_ TY]
ps, ATerm
t) <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Bind [Pattern_ TY] ATerm -> Sem r ([Pattern_ TY], ATerm)
liftClause Bind [Pattern_ TY] ATerm
c
    forall (m :: * -> *) a. Monad m => a -> m a
return [([Pattern_ TY]
ps, [Pattern_ TY] -> ATerm -> ATerm
addDbgInfo [Pattern_ TY]
ps ATerm
t)]
  unbindClauses [Bind [Pattern_ TY] ATerm]
cs = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind [Bind [Pattern_ TY] ATerm]
cs

  liftClause :: Member Fresh r => Bind [APattern] ATerm -> Sem r ([APattern], ATerm)
  liftClause :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Bind [Pattern_ TY] ATerm -> Sem r ([Pattern_ TY], ATerm)
liftClause Bind [Pattern_ TY] ATerm
c =
    forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Pattern_ TY] ATerm
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      ([Pattern_ TY]
ps, ATAbs Quantifier
q Type
_ Bind [Pattern_ TY] ATerm
c') | Quantifier
q forall a. Eq a => a -> a -> Bool
== Quantifier
quant -> do
        ([Pattern_ TY]
ps', ATerm
b) <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Bind [Pattern_ TY] ATerm -> Sem r ([Pattern_ TY], ATerm)
liftClause Bind [Pattern_ TY] ATerm
c'
        forall (m :: * -> *) a. Monad m => a -> m a
return ([Pattern_ TY]
ps forall a. [a] -> [a] -> [a]
++ [Pattern_ TY]
ps', ATerm
b)
      ([Pattern_ TY]
ps, ATerm
b) -> forall (m :: * -> *) a. Monad m => a -> m a
return ([Pattern_ TY]
ps, ATerm
b)

  -- Wrap a term in a test frame to report the values of all variables
  -- bound in the patterns.
  addDbgInfo :: [APattern] -> ATerm -> ATerm
  addDbgInfo :: [Pattern_ TY] -> ATerm -> ATerm
addDbgInfo [Pattern_ TY]
ps ATerm
t = [(String, Type, Name ATerm)] -> ATerm -> ATerm
ATTest (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b}. (Name a, b) -> (String, b, Name a)
withName forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern_ TY -> [(Name ATerm, Type)]
varsBound [Pattern_ TY]
ps) ATerm
t
   where
    withName :: (Name a, b) -> (String, b, Name a)
withName (Name a
n, b
ty) = (forall a. Name a -> String
name2String Name a
n, b
ty, Name a
n)

------------------------------------------------------------
-- Term desugaring
------------------------------------------------------------

-- | Desugar the application of a "bag from counts" primitive on a
--   list, either a safe or unsafe variant.
desugarCList2B :: Member Fresh r => Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B Prim
p Type
ty Type
cts Type
b = do
  Name ATerm
c <- forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"c")
  DTerm
body <-
    forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
      ATerm -> ATerm -> ATerm
tapp
        (Type -> Prim -> ATerm
ATPrim (Type -> Type
TyBag Type
cts Type -> Type -> Type
:->: Type -> Type
TyBag Type
b) Prim
p)
        ( ATerm -> ATerm -> ATerm
tapp
            (Type -> Prim -> ATerm
ATPrim (Type -> Type
TyList Type
cts Type -> Type -> Type
:->: Type -> Type
TyBag Type
cts) Prim
PrimBag)
            (Type -> Name ATerm -> ATerm
atVar (Type -> Type
TyList Type
cts) Name ATerm
c)
        )
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda Type
ty [Name ATerm
c] DTerm
body

-- | Desugar a typechecked term.
desugarTerm :: Member Fresh r => ATerm -> Sem r DTerm
desugarTerm :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATVar Type
ty QName ATerm
x) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> QName DTerm -> DTerm
DTVar Type
ty (coerce :: forall a b. Coercible a b => a -> b
coerce QName ATerm
x)
desugarTerm (ATPrim (Type
ty1 :->: Type
resTy) (PrimUOp UOp
uop))
  | Type -> Type -> UOp -> Bool
uopDesugars Type
ty1 Type
resTy UOp
uop = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp Type
ty1 Type
resTy UOp
uop
desugarTerm (ATPrim (Type
ty1 :*: Type
ty2 :->: Type
resTy) (PrimBOp BOp
bop))
  | Type -> Type -> Type -> BOp -> Bool
bopDesugars Type
ty1 Type
ty2 Type
resTy BOp
bop = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Type -> Type -> BOp -> Sem r DTerm
desugarPrimBOp Type
ty1 Type
ty2 Type
resTy BOp
bop
desugarTerm (ATPrim ty :: Type
ty@(TyList Type
cts :->: TyBag Type
b) Prim
PrimC2B) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B Prim
PrimC2B Type
ty Type
cts Type
b
desugarTerm (ATPrim ty :: Type
ty@(TyList Type
cts :->: TyBag Type
b) Prim
PrimUC2B) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B Prim
PrimUC2B Type
ty Type
cts Type
b
desugarTerm (ATPrim Type
ty Prim
x) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Prim -> DTerm
DTPrim Type
ty Prim
x
desugarTerm ATerm
ATUnit = forall (m :: * -> *) a. Monad m => a -> m a
return DTerm
DTUnit
desugarTerm (ATBool Type
ty Bool
b) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Bool -> DTerm
DTBool Type
ty Bool
b
desugarTerm (ATChar Char
c) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Char -> DTerm
DTChar Char
c
desugarTerm (ATString String
cs) =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer (Type -> Type
TyList Type
TyC) Container
ListContainer (forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> (Char -> ATerm
ATChar Char
c, forall a. Maybe a
Nothing)) String
cs) forall a. Maybe a
Nothing
desugarTerm (ATAbs Quantifier
q Type
ty Bind [Pattern_ TY] ATerm
lam) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Quantifier -> Type -> [Bind [Pattern_ TY] ATerm] -> Sem r DTerm
desugarAbs Quantifier
q Type
ty [Bind [Pattern_ TY] ATerm
lam]
-- Special cases for fully applied operators
desugarTerm (ATApp Type
resTy (ATPrim Type
_ (PrimUOp UOp
uop)) ATerm
t)
  | Type -> Type -> UOp -> Bool
uopDesugars (forall t. HasType t => t -> Type
getType ATerm
t) Type
resTy UOp
uop = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> UOp -> ATerm -> Sem r DTerm
desugarUnApp Type
resTy UOp
uop ATerm
t
desugarTerm (ATApp Type
resTy (ATPrim Type
_ (PrimBOp BOp
bop)) (ATTup Type
_ [ATerm
t1, ATerm
t2]))
  | Type -> Type -> Type -> BOp -> Bool
bopDesugars (forall t. HasType t => t -> Type
getType ATerm
t1) (forall t. HasType t => t -> Type
getType ATerm
t2) Type
resTy BOp
bop = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
desugarBinApp Type
resTy BOp
bop ATerm
t1 ATerm
t2
desugarTerm (ATApp Type
ty ATerm
t1 ATerm
t2) =
  Type -> DTerm -> DTerm -> DTerm
DTApp Type
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t2
desugarTerm (ATTup Type
ty [ATerm]
ts) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> [ATerm] -> Sem r DTerm
desugarTuples Type
ty [ATerm]
ts
desugarTerm (ATNat Type
ty Integer
n) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Integer -> DTerm
DTNat Type
ty Integer
n
desugarTerm (ATRat Rational
r) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Rational -> DTerm
DTRat Rational
r
desugarTerm (ATTyOp Type
ty TyOp
op Type
t) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> TyOp -> Type -> DTerm
DTTyOp Type
ty TyOp
op Type
t
desugarTerm (ATChain Type
_ ATerm
t1 [Link_ TY]
links) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ ATerm -> [Link_ TY] -> ATerm
expandChain ATerm
t1 [Link_ TY]
links
desugarTerm (ATContainer Type
ty Container
c [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer Type
ty Container
c [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell
desugarTerm (ATContainerComp Type
_ Container
ctr Bind (Telescope (Qual_ TY)) ATerm
bqt) = do
  (Telescope (Qual_ TY)
qs, ATerm
t) <- forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope (Qual_ TY)) ATerm
bqt
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r DTerm
desugarComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs
desugarTerm (ATLet Type
_ Bind (Telescope (Binding_ TY)) ATerm
t) = do
  (Telescope (Binding_ TY)
bs, ATerm
t2) <- forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope (Binding_ TY)) ATerm
t
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Binding_ TY] -> ATerm -> Sem r DTerm
desugarLet (forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope (Binding_ TY)
bs) ATerm
t2
desugarTerm (ATCase Type
ty [ABranch]
bs) = Type -> [DBranch] -> DTerm
DTCase Type
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ABranch -> Sem r DBranch
desugarBranch [ABranch]
bs
desugarTerm (ATTest [(String, Type, Name ATerm)]
info ATerm
t) = [(String, Type, Name DTerm)] -> DTerm -> DTerm
DTTest (coerce :: forall a b. Coercible a b => a -> b
coerce [(String, Type, Name ATerm)]
info) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t

-- | Desugar a property by wrapping its corresponding term in a test
--   frame to catch its exceptions & convert booleans to props.
desugarProperty :: Member Fresh r => AProperty -> Sem r DTerm
desugarProperty :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarProperty ATerm
p = [(String, Type, Name DTerm)] -> DTerm -> DTerm
DTTest [] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
p

------------------------------------------------------------
-- Desugaring operators
------------------------------------------------------------

-- | Test whether a given unary operator is one that needs to be
--   desugared, given the type of the argument and result.
uopDesugars :: Type -> Type -> UOp -> Bool
-- uopDesugars _ (TyFin _) Neg = True
uopDesugars :: Type -> Type -> UOp -> Bool
uopDesugars Type
TyProp Type
TyProp UOp
Not = Bool
False
uopDesugars Type
_ Type
_ UOp
uop = UOp
uop forall a. Eq a => a -> a -> Bool
== UOp
Not

desugarPrimUOp :: Member Fresh r => Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp Type
argTy Type
resTy UOp
op = do
  Name ATerm
x <- forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"arg")
  DTerm
body <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> UOp -> ATerm -> Sem r DTerm
desugarUnApp Type
resTy UOp
op (Type -> Name ATerm -> ATerm
atVar Type
argTy Name ATerm
x)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda (Type
argTy Type -> Type -> Type
:->: Type
resTy) [Name ATerm
x] DTerm
body

-- | Test whether a given binary operator is one that needs to be
--   desugared, given the two types of the arguments and the type of the result.
bopDesugars :: Type -> Type -> Type -> BOp -> Bool
bopDesugars :: Type -> Type -> Type -> BOp -> Bool
bopDesugars Type
_ Type
TyN Type
_ BOp
Choose = Bool
True
-- bopDesugars _   _   (TyFin _) bop | bop `elem` [Add, Mul] = True

-- And, Or, Impl for Props don't desugar because they are primitive
-- Prop constructors.  On the other hand, logical operations on Bool
-- can desugar in terms of more primitive conditional expressions.
bopDesugars Type
_ Type
_ Type
TyProp BOp
bop | BOp
bop forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
And, BOp
Or, BOp
Impl] = Bool
False
bopDesugars Type
_ Type
_ Type
_ BOp
bop =
  BOp
bop
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ BOp
And
           , BOp
Or
           , BOp
Impl
           , BOp
Iff
           , BOp
Neq
           , BOp
Gt
           , BOp
Leq
           , BOp
Geq
           , BOp
Min
           , BOp
Max
           , BOp
IDiv
           , BOp
Sub
           , BOp
SSub
           , BOp
Inter
           , BOp
Diff
           , BOp
Union
           , BOp
Subset
           ]

-- | Desugar a primitive binary operator at the given type.
desugarPrimBOp :: Member Fresh r => Type -> Type -> Type -> BOp -> Sem r DTerm
desugarPrimBOp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Type -> Type -> BOp -> Sem r DTerm
desugarPrimBOp Type
ty1 Type
ty2 Type
resTy BOp
op = do
  Name ATerm
p <- forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"pair1")
  Name ATerm
x <- forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"arg1")
  Name ATerm
y <- forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"arg2")
  let argsTy :: Type
argsTy = Type
ty1 Type -> Type -> Type
:*: Type
ty2
  DTerm
body <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
desugarBinApp Type
resTy BOp
op (Type -> Name ATerm -> ATerm
atVar Type
ty1 Name ATerm
x) (Type -> Name ATerm -> ATerm
atVar Type
ty2 Name ATerm
y)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda (Type
argsTy Type -> Type -> Type
:->: Type
resTy) [Name ATerm
p] forall a b. (a -> b) -> a -> b
$
      Type -> [DBranch] -> DTerm
DTCase
        Type
resTy
        [ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind
            (forall b. Alpha b => [b] -> Telescope b
toTelescope [Embed DTerm -> Pattern_ DS -> Guard_ DS
DGPat (forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name DTerm -> DTerm
dtVar Type
argsTy (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
p))) (Type -> Name DTerm -> Name DTerm -> Pattern_ DS
DPPair Type
argsTy (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x) (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
y))])
            DTerm
body
        ]

-- | Desugar a saturated application of a unary operator.
--   The first argument is the type of the result.
desugarUnApp :: Member Fresh r => Type -> UOp -> ATerm -> Sem r DTerm
-- Desugar negation on TyFin to a negation on TyZ followed by a mod.
-- See the comments below re: Add and Mul on TyFin.
-- desugarUnApp (TyFin n) Neg t =
--   desugarTerm $ mkBin (TyFin n) Mod (mkUn TyZ Neg t) (ATNat TyN n)

-- XXX This should be turned into a standard library definition.
-- not t ==> {? false if t, true otherwise ?}
desugarUnApp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> UOp -> ATerm -> Sem r DTerm
desugarUnApp Type
_ UOp
Not ATerm
t =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
    Type -> [ABranch] -> ATerm
ATCase
      Type
TyBool
      [ ATerm
fls ATerm -> [AGuard] -> ABranch
<==. [Embed ATerm -> AGuard
AGBool (forall e. IsEmbed e => Embedded e -> e
embed ATerm
t)]
      , ATerm
tru ATerm -> [AGuard] -> ABranch
<==. []
      ]
desugarUnApp Type
ty UOp
uop ATerm
t = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! desugarUnApp " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UOp
uop forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ATerm
t

-- | Desugar a saturated application of a binary operator.
--   The first argument is the type of the result.
desugarBinApp :: Member Fresh r => Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
-- Implies, and, or should all be turned into a standard library
-- definition.  This will require first (1) adding support for
-- modules/a standard library, including (2) the ability to define
-- infix operators.

-- t1 and t2 ==> {? t2 if t1, false otherwise ?}
desugarBinApp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
desugarBinApp Type
_ BOp
And ATerm
t1 ATerm
t2 =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
    Type -> [ABranch] -> ATerm
ATCase
      Type
TyBool
      [ ATerm
t2 ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif ATerm
t1]
      , ATerm
fls ATerm -> [AGuard] -> ABranch
<==. []
      ]
-- (t1 implies t2) ==> (not t1 or t2)
desugarBinApp Type
_ BOp
Impl ATerm
t1 ATerm
t2 = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ ATerm -> ATerm
tnot ATerm
t1 ATerm -> ATerm -> ATerm
||. ATerm
t2
-- (t1 iff t2) ==> (t1 == t2)
desugarBinApp Type
_ BOp
Iff ATerm
t1 ATerm
t2 = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ ATerm
t1 ATerm -> ATerm -> ATerm
==. ATerm
t2
-- t1 or t2 ==> {? true if t1, t2 otherwise ?})
desugarBinApp Type
_ BOp
Or ATerm
t1 ATerm
t2 =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
    Type -> [ABranch] -> ATerm
ATCase
      Type
TyBool
      [ ATerm
tru ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif ATerm
t1]
      , ATerm
t2 ATerm -> [AGuard] -> ABranch
<==. []
      ]
desugarBinApp Type
_ BOp
Neq ATerm
t1 ATerm
t2 = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ ATerm -> ATerm
tnot (ATerm
t1 ATerm -> ATerm -> ATerm
==. ATerm
t2)
desugarBinApp Type
_ BOp
Gt ATerm
t1 ATerm
t2 = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ ATerm
t2 ATerm -> ATerm -> ATerm
<. ATerm
t1
desugarBinApp Type
_ BOp
Leq ATerm
t1 ATerm
t2 = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ ATerm -> ATerm
tnot (ATerm
t2 ATerm -> ATerm -> ATerm
<. ATerm
t1)
desugarBinApp Type
_ BOp
Geq ATerm
t1 ATerm
t2 = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ ATerm -> ATerm
tnot (ATerm
t1 ATerm -> ATerm -> ATerm
<. ATerm
t2)
-- XXX sharing!
desugarBinApp Type
ty BOp
Min ATerm
t1 ATerm
t2 =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
    Type -> [ABranch] -> ATerm
ATCase
      Type
ty
      [ ATerm
t1 ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif (ATerm
t1 ATerm -> ATerm -> ATerm
<. ATerm
t2)]
      , ATerm
t2 ATerm -> [AGuard] -> ABranch
<==. []
      ]
desugarBinApp Type
ty BOp
Max ATerm
t1 ATerm
t2 =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
    Type -> [ABranch] -> ATerm
ATCase
      Type
ty
      [ ATerm
t1 ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif (ATerm
t2 ATerm -> ATerm -> ATerm
<. ATerm
t1)]
      , ATerm
t2 ATerm -> [AGuard] -> ABranch
<==. []
      ]
-- t1 // t2 ==> floor (t1 / t2)
desugarBinApp Type
resTy BOp
IDiv ATerm
t1 ATerm
t2 =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
    Type -> ATerm -> ATerm -> ATerm
ATApp Type
resTy (Type -> Prim -> ATerm
ATPrim (forall t. HasType t => t -> Type
getType ATerm
t1 Type -> Type -> Type
:->: Type
resTy) Prim
PrimFloor) (Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin (forall t. HasType t => t -> Type
getType ATerm
t1) BOp
Div ATerm
t1 ATerm
t2)
-- Desugar normal binomial coefficient (n choose k) to a multinomial
-- coefficient with a singleton list, (n choose [k]).
-- Note this will only be called when (getType t2 == TyN); see bopDesugars.
desugarBinApp Type
_ BOp
Choose ATerm
t1 ATerm
t2 =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyN BOp
Choose ATerm
t1 (Container -> ATerm -> ATerm
ctrSingleton Container
ListContainer ATerm
t2)
desugarBinApp Type
ty BOp
Sub ATerm
t1 ATerm
t2 = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
ty BOp
Add ATerm
t1 (Type -> UOp -> ATerm -> ATerm
mkUn Type
ty UOp
Neg ATerm
t2)
desugarBinApp Type
ty BOp
SSub ATerm
t1 ATerm
t2 =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
    -- t1 -. t2 ==> {? 0 if t1 < t2, t1 - t2 otherwise ?}
    Type -> [ABranch] -> ATerm
ATCase
      Type
ty
      [ Type -> Integer -> ATerm
ATNat Type
ty Integer
0 ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif (ATerm
t1 ATerm -> ATerm -> ATerm
<. ATerm
t2)]
      , Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
ty BOp
Sub ATerm
t1 ATerm
t2 ATerm -> [AGuard] -> ABranch
<==. []
      -- NOTE, the above is slightly bogus since the whole point of SSub is
      -- because we can't subtract naturals.  However, this will
      -- immediately desugar to a DTerm.  When we write a linting
      -- typechecker for DTerms we should allow subtraction on TyN!
      ]
-- Addition and multiplication on TyFin just desugar to the operation
-- followed by a call to mod.
-- desugarBinApp (TyFin n) op t1 t2
--   | op `elem` [Add, Mul] = desugarTerm $
--       mkBin (TyFin n) Mod
--         (mkBin TyN op t1 t2)
--         (ATNat TyN n)
-- Note the typing of this is a bit funny: t1 and t2 presumably
-- have type (TyFin n), and now we are saying that applying 'op'
-- to them results in TyN, then applying 'mod' results in a TyFin
-- n again.  Using TyN as the intermediate result is necessary so
-- we don't fall into an infinite desugaring loop, and intuitively
-- makes sense because the idea is that we first do the operation
-- as a normal operation in "natural land" and then do a mod.
--
-- We will have to think carefully about how the linting
-- typechecker for DTerms should treat TyN and TyFin.  Probably
-- something like this will work: TyFin is a subtype of TyN, and
-- TyN can be turned into TyFin with mod.  (We don't want such
-- typing rules in the surface disco language itself because
-- implicit coercions from TyFin -> N don't commute with
-- operations like addition and multiplication, e.g. 3+3 yields 1
-- if we add them in Z5 and then coerce to Nat, but 6 if we first
-- coerce both and then add.

-- Intersection, difference, and union all desugar to an application
-- of 'merge' with an appropriate combining operation.
desugarBinApp Type
ty BOp
op ATerm
t1 ATerm
t2
  | BOp
op forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Inter, BOp
Diff, BOp
Union] =
      forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
        ATerm -> [ATerm] -> ATerm
tapps
          (Type -> Prim -> ATerm
ATPrim ((Type
TyN Type -> Type -> Type
:*: Type
TyN Type -> Type -> Type
:->: Type
TyN) Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
ty) Prim
PrimMerge)
          [ Type -> Prim -> ATerm
ATPrim (Type
TyN Type -> Type -> Type
:*: Type
TyN Type -> Type -> Type
:->: Type
TyN) (Type -> BOp -> Prim
mergeOp Type
ty BOp
op)
          , ATerm
t1
          , ATerm
t2
          ]
 where
  mergeOp :: Type -> BOp -> Prim
mergeOp Type
_ BOp
Inter = BOp -> Prim
PrimBOp BOp
Min
  mergeOp Type
_ BOp
Diff = BOp -> Prim
PrimBOp BOp
SSub
  mergeOp (TySet Type
_) BOp
Union = BOp -> Prim
PrimBOp BOp
Max
  mergeOp (TyBag Type
_) BOp
Union = BOp -> Prim
PrimBOp BOp
Add
  mergeOp Type
_ BOp
_ = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! mergeOp " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BOp
op

-- A ⊆ B  <==>  (A ⊔ B = B)
--   where ⊔ denotes 'merge max'.
--   Note it is NOT union, since this doesn't work for bags.
--   e.g.  bag [1] union bag [1,2] =  bag [1,1,2] /= bag [1,2].
desugarBinApp Type
_ BOp
Subset ATerm
t1 ATerm
t2 =
  forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$
    ATerm -> [ATerm] -> ATerm
tapps
      (Type -> Prim -> ATerm
ATPrim (Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
TyBool) (BOp -> Prim
PrimBOp BOp
Eq))
      [ ATerm -> [ATerm] -> ATerm
tapps
          (Type -> Prim -> ATerm
ATPrim ((Type
TyN Type -> Type -> Type
:*: Type
TyN Type -> Type -> Type
:->: Type
TyN) Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
ty) Prim
PrimMerge)
          [ Type -> Prim -> ATerm
ATPrim (Type
TyN Type -> Type -> Type
:*: Type
TyN Type -> Type -> Type
:->: Type
TyN) (BOp -> Prim
PrimBOp BOp
Max)
          , ATerm
t1
          , ATerm
t2
          ]
      , ATerm
t2 -- XXX sharing
      ]
 where
  ty :: Type
ty = forall t. HasType t => t -> Type
getType ATerm
t1
desugarBinApp Type
ty BOp
bop ATerm
t1 ATerm
t2 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! desugarBinApp " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BOp
bop forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ATerm
t1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ATerm
t2

------------------------------------------------------------
-- Desugaring other stuff
------------------------------------------------------------

-- | Desugar a container comprehension.  First translate it into an
--   expanded ATerm and then recursively desugar that.
desugarComp :: Member Fresh r => Container -> ATerm -> Telescope AQual -> Sem r DTerm
desugarComp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r DTerm
desugarComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm

-- | Expand a container comprehension into an equivalent ATerm.
expandComp :: Member Fresh r => Container -> ATerm -> Telescope AQual -> Sem r ATerm
-- [ t | ] = [ t ]
expandComp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope (Qual_ TY)
TelEmpty = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Container -> ATerm -> ATerm
ctrSingleton Container
ctr ATerm
t
-- [ t | q, qs ] = ...
expandComp Container
ctr ATerm
t (TelCons (forall p1 p2. (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind -> (Qual_ TY
q, Telescope (Qual_ TY)
qs))) =
  case Qual_ TY
q of
    -- [ t | x in l, qs ] = join (map (\x -> [t | qs]) l)
    AQBind Name ATerm
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
lst) -> do
      ATerm
tqs <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs
      let c :: Type -> Type
c = Container -> Type -> Type
containerTy Container
ctr
          tTy :: Type
tTy = forall t. HasType t => t -> Type
getType ATerm
t
          xTy :: Type
xTy = case forall t. HasType t => t -> Type
getType Embedded (Embed ATerm)
lst of
            TyContainer Atom
_ Type
e -> Type
e
            Type
_ -> forall a. HasCallStack => String -> a
error String
"Impossible! Not a container in expandComp"
          joinTy :: Type
joinTy = Type -> Type
c (Type -> Type
c Type
tTy) Type -> Type -> Type
:->: Type -> Type
c Type
tTy
          mapTy :: Type
mapTy = (Type
xTy Type -> Type -> Type
:->: Type -> Type
c Type
tTy) Type -> Type -> Type
:*: Type -> Type
c Type
xTy Type -> Type -> Type
:->: Type -> Type
c (Type -> Type
c Type
tTy)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim Type
joinTy Prim
PrimJoin) forall a b. (a -> b) -> a -> b
$
          ATerm -> ATerm -> ATerm
tapp
            (Type -> Prim -> ATerm
ATPrim Type
mapTy Prim
PrimEach)
            ( ATerm -> ATerm -> ATerm
mkPair
                (Quantifier -> Type -> Bind [Pattern_ TY] ATerm -> ATerm
ATAbs Quantifier
Lam (Type
xTy Type -> Type -> Type
:->: Type -> Type
c Type
tTy) (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Type -> Name ATerm -> Pattern_ TY
APVar Type
xTy Name ATerm
x] ATerm
tqs))
                Embedded (Embed ATerm)
lst
            )

    -- [ t | g, qs ] = if g then [ t | qs ] else []
    AQGuard (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
g) -> do
      ATerm
tqs <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        Type -> [ABranch] -> ATerm
ATCase
          (Container -> Type -> Type
containerTy Container
ctr (forall t. HasType t => t -> Type
getType ATerm
t))
          [ ATerm
tqs ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif Embedded (Embed ATerm)
g]
          , Container -> Type -> ATerm
ctrNil Container
ctr (forall t. HasType t => t -> Type
getType ATerm
t) ATerm -> [AGuard] -> ABranch
<==. []
          ]

-- | Desugar a let into applications of a chain of nested lambdas.
--   /e.g./
--
--     @let x = s, y = t in q@
--
--   desugars to
--
--     @(\x. (\y. q) t) s@
desugarLet :: Member Fresh r => [ABinding] -> ATerm -> Sem r DTerm
desugarLet :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Binding_ TY] -> ATerm -> Sem r DTerm
desugarLet [] ATerm
t = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
desugarLet ((ABinding Maybe (Embed PolyType)
_ Name ATerm
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
t1)) : [Binding_ TY]
ls) ATerm
t =
  DTerm -> DTerm -> DTerm
dtapp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
Lam (forall t. HasType t => t -> Type
getType Embedded (Embed ATerm)
t1 Type -> Type -> Type
:->: forall t. HasType t => t -> Type
getType ATerm
t)
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Binding_ TY] -> ATerm -> Sem r DTerm
desugarLet [Binding_ TY]
ls ATerm
t)
        )
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
t1

-- | Desugar a lambda from a list of argument names and types and the
--   desugared @DTerm@ expression for its body. It will be desugared
--   to a chain of one-argument lambdas. /e.g./
--
--     @\x y z. q@
--
--   desugars to
--
--     @\x. \y. \z. q@
mkLambda :: Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda :: Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda Type
funty [Name ATerm]
args DTerm
c = Type -> [Name ATerm] -> DTerm
go Type
funty [Name ATerm]
args
 where
  go :: Type -> [Name ATerm] -> DTerm
go Type
_ [] = DTerm
c
  go ty :: Type
ty@(Type
_ :->: Type
ty2) (Name ATerm
x : [Name ATerm]
xs) = Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
Lam Type
ty (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x) (Type -> [Name ATerm] -> DTerm
go Type
ty2 [Name ATerm]
xs))
  go Type
ty [Name ATerm]
as = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! mkLambda.go " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name ATerm]
as

mkQuant :: Quantifier -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkQuant :: Quantifier -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkQuant Quantifier
q [Type]
argtys [Name ATerm]
args DTerm
c = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name ATerm, Type) -> DTerm -> DTerm
quantify DTerm
c (forall a b. [a] -> [b] -> [(a, b)]
zip [Name ATerm]
args [Type]
argtys)
 where
  quantify :: (Name ATerm, Type) -> DTerm -> DTerm
quantify (Name ATerm
x, Type
ty) DTerm
body = Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
q Type
ty (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x) DTerm
body)

mkAbs :: Quantifier -> Type -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkAbs :: Quantifier -> Type -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkAbs Quantifier
Lam Type
funty [Type]
_ [Name ATerm]
args DTerm
c = Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda Type
funty [Name ATerm]
args DTerm
c
mkAbs Quantifier
q Type
_ [Type]
argtys [Name ATerm]
args DTerm
c = Quantifier -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkQuant Quantifier
q [Type]
argtys [Name ATerm]
args DTerm
c

-- | Desugar a tuple to nested pairs, /e.g./ @(a,b,c,d) ==> (a,(b,(c,d)))@.a
desugarTuples :: Member Fresh r => Type -> [ATerm] -> Sem r DTerm
desugarTuples :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> [ATerm] -> Sem r DTerm
desugarTuples Type
_ [ATerm
t] = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
desugarTuples ty :: Type
ty@(Type
_ :*: Type
ty2) (ATerm
t : [ATerm]
ts) = Type -> DTerm -> DTerm -> DTerm
DTPair Type
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> [ATerm] -> Sem r DTerm
desugarTuples Type
ty2 [ATerm]
ts
desugarTuples Type
ty [ATerm]
ats =
  forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! desugarTuples " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [ATerm]
ats

-- | Expand a chain of comparisons into a sequence of binary
--   comparisons combined with @and@.  Note we only expand it into
--   another 'ATerm' (which will be recursively desugared), because
--   @and@ itself also gets desugared.
--
--   For example, @a < b <= c > d@ becomes @a < b and b <= c and c > d@.
expandChain :: ATerm -> [ALink] -> ATerm
expandChain :: ATerm -> [Link_ TY] -> ATerm
expandChain ATerm
_ [] = forall a. HasCallStack => String -> a
error String
"Can't happen! expandChain _ []"
expandChain ATerm
t1 [ATLink BOp
op ATerm
t2] = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
op ATerm
t1 ATerm
t2
expandChain ATerm
t1 (ATLink BOp
op ATerm
t2 : [Link_ TY]
links) =
  Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin
    Type
TyBool
    BOp
And
    (Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
op ATerm
t1 ATerm
t2)
    (ATerm -> [Link_ TY] -> ATerm
expandChain ATerm
t2 [Link_ TY]
links)

-- | Desugar a branch of a case expression.
desugarBranch :: Member Fresh r => ABranch -> Sem r DBranch
desugarBranch :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ABranch -> Sem r DBranch
desugarBranch ABranch
b = do
  (Telescope AGuard
ags, ATerm
at) <- forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind ABranch
b
  Telescope (Guard_ DS)
dgs <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Telescope AGuard -> Sem r (Telescope (Guard_ DS))
desugarGuards Telescope AGuard
ags
  DTerm
d <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
at
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope (Guard_ DS)
dgs DTerm
d

-- | Desugar the list of guards in one branch of a case expression.
--   Pattern guards essentially remain as they are; boolean guards get
--   turned into pattern guards which match against @true@.
desugarGuards :: Member Fresh r => Telescope AGuard -> Sem r (Telescope DGuard)
desugarGuards :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Telescope AGuard -> Sem r (Telescope (Guard_ DS))
desugarGuards = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall b. Alpha b => [b] -> Telescope b
toTelescope forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [Guard_ DS]
desugarGuard forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. Alpha b => Telescope b -> [b]
fromTelescope
 where
  desugarGuard :: Member Fresh r => AGuard -> Sem r [DGuard]

  -- A Boolean guard is desugared to a pattern-match on @true = right(unit)@.
  desugarGuard :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [Guard_ DS]
desugarGuard (AGBool (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at)) = do
    DTerm
dt <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
at
    forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt (Type -> Side -> Pattern_ TY -> Pattern_ TY
APInj Type
TyBool Side
R Pattern_ TY
APUnit)

  -- 'let x = t' is desugared to 'when t is x'.
  desugarGuard (AGLet (ABinding Maybe (Embed PolyType)
_ Name ATerm
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at))) = do
    DTerm
dt <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
at
    forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Name DTerm -> Sem r [Guard_ DS]
varMatch DTerm
dt (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x)

  -- Desugaring 'when t is p' is the most complex case; we have to
  -- break down the pattern and match it incrementally.
  desugarGuard (AGPat (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at) Pattern_ TY
p) = do
    DTerm
dt <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
at
    forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt Pattern_ TY
p

  -- Desugar a guard of the form 'when dt is p'.  An entire match is
  -- the right unit to desugar --- as opposed to, say, writing a
  -- function to desugar a pattern --- since a match may desugar to
  -- multiple matches, and on recursive calls we need to know what
  -- term/variable should be bound to the pattern.
  --
  -- A match may desugar to multiple matches for two reasons:
  --
  --   1. Nested patterns 'explode' into a 'telescope' matching one
  --   constructor at a time, for example, 'when t is (x,y,3)'
  --   becomes 'when t is (x,x0) when x0 is (y,x1) when x1 is 3'.
  --   This makes the order of matching explicit and enables lazy
  --   matching without requiring special support from the
  --   interpreter other than WHNF reduction.
  --
  --   2. Matches against arithmetic patterns desugar to a
  --   combination of matching, computation, and boolean checks.
  --   For example, 'when t is (y+1)' becomes 'when t is x0 if x0 >=
  --   1 let y = x0-1'.
  desugarMatch :: Member Fresh r => DTerm -> APattern -> Sem r [DGuard]
  desugarMatch :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt (APVar Type
ty Name ATerm
x) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch DTerm
dt (Type -> Name DTerm -> Pattern_ DS
DPVar Type
ty (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x))
  desugarMatch DTerm
_ (APWild Type
_) = forall (m :: * -> *) a. Monad m => a -> m a
return []
  desugarMatch DTerm
dt Pattern_ TY
APUnit = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch DTerm
dt Pattern_ DS
DPUnit
  desugarMatch DTerm
dt (APBool Bool
b) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt (Type -> Side -> Pattern_ TY -> Pattern_ TY
APInj Type
TyBool (forall a. a -> a -> Bool -> a
bool Side
L Side
R Bool
b) Pattern_ TY
APUnit)
  desugarMatch DTerm
dt (APNat Type
ty Integer
n) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch (Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
TyBool (BOp -> Prim
PrimBOp BOp
Eq) DTerm
dt (Type -> Integer -> DTerm
DTNat Type
ty Integer
n)) (Bool -> Pattern_ TY
APBool Bool
True)
  desugarMatch DTerm
dt (APChar Char
c) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch (Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
TyBool (BOp -> Prim
PrimBOp BOp
Eq) DTerm
dt (Char -> DTerm
DTChar Char
c)) (Bool -> Pattern_ TY
APBool Bool
True)
  desugarMatch DTerm
dt (APString String
s) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt (Type -> [Pattern_ TY] -> Pattern_ TY
APList (Type -> Type
TyList Type
TyC) (forall a b. (a -> b) -> [a] -> [b]
map Char -> Pattern_ TY
APChar String
s))
  desugarMatch DTerm
dt (APTup Type
tupTy [Pattern_ TY]
pat) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> DTerm -> [Pattern_ TY] -> Sem r [Guard_ DS]
desugarTuplePats Type
tupTy DTerm
dt [Pattern_ TY]
pat
   where
    desugarTuplePats :: Member Fresh r => Type -> DTerm -> [APattern] -> Sem r [DGuard]
    desugarTuplePats :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> DTerm -> [Pattern_ TY] -> Sem r [Guard_ DS]
desugarTuplePats Type
_ DTerm
_ [] = forall a. HasCallStack => String -> a
error String
"Impossible! desugarTuplePats []"
    desugarTuplePats Type
_ DTerm
t [Pattern_ TY
p] = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
t Pattern_ TY
p
    desugarTuplePats ty :: Type
ty@(Type
_ :*: Type
ty2) DTerm
t (Pattern_ TY
p : [Pattern_ TY]
ps) = do
      (Name DTerm
x1, [Guard_ DS]
gs1) <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Pattern_ TY -> Sem r (Name DTerm, [Guard_ DS])
varForPat Pattern_ TY
p
      (Name DTerm
x2, [Guard_ DS]
gs2) <- case [Pattern_ TY]
ps of
        [APVar Type
_ Name ATerm
px2] -> forall (m :: * -> *) a. Monad m => a -> m a
return (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
px2, [])
        [Pattern_ TY]
_ -> do
          Name DTerm
x <- forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"x")
          (Name DTerm
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> DTerm -> [Pattern_ TY] -> Sem r [Guard_ DS]
desugarTuplePats Type
ty2 (Type -> Name DTerm -> DTerm
dtVar Type
ty2 Name DTerm
x) [Pattern_ TY]
ps
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$
        [ forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch DTerm
t forall a b. (a -> b) -> a -> b
$ Type -> Name DTerm -> Name DTerm -> Pattern_ DS
DPPair Type
ty Name DTerm
x1 Name DTerm
x2
        , forall (m :: * -> *) a. Monad m => a -> m a
return [Guard_ DS]
gs1
        , forall (m :: * -> *) a. Monad m => a -> m a
return [Guard_ DS]
gs2
        ]
    desugarTuplePats Type
ty DTerm
_ [Pattern_ TY]
_ =
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! desugarTuplePats with non-pair type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty
  desugarMatch DTerm
dt (APInj Type
ty Side
s Pattern_ TY
p) = do
    (Name DTerm
x, [Guard_ DS]
gs) <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Pattern_ TY -> Sem r (Name DTerm, [Guard_ DS])
varForPat Pattern_ TY
p
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$
      [ forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch DTerm
dt forall a b. (a -> b) -> a -> b
$ Type -> Side -> Name DTerm -> Pattern_ DS
DPInj Type
ty Side
s Name DTerm
x
      , forall (m :: * -> *) a. Monad m => a -> m a
return [Guard_ DS]
gs
      ]
  desugarMatch DTerm
dt (APCons Type
ty Pattern_ TY
p1 Pattern_ TY
p2) = do
    Name DTerm
y <- forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"y")
    (Name DTerm
x1, [Guard_ DS]
gs1) <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Pattern_ TY -> Sem r (Name DTerm, [Guard_ DS])
varForPat Pattern_ TY
p1
    (Name DTerm
x2, [Guard_ DS]
gs2) <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Pattern_ TY -> Sem r (Name DTerm, [Guard_ DS])
varForPat Pattern_ TY
p2

    let eltTy :: Type
eltTy = forall t. HasType t => t -> Type
getType Pattern_ TY
p1
        unrolledTy :: Type
unrolledTy = Type
eltTy Type -> Type -> Type
:*: Type
ty
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$
      [ forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch DTerm
dt (Type -> Side -> Name DTerm -> Pattern_ DS
DPInj Type
ty Side
R Name DTerm
y)
      , forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch (Type -> Name DTerm -> DTerm
dtVar Type
unrolledTy Name DTerm
y) (Type -> Name DTerm -> Name DTerm -> Pattern_ DS
DPPair Type
unrolledTy Name DTerm
x1 Name DTerm
x2)
      , forall (m :: * -> *) a. Monad m => a -> m a
return [Guard_ DS]
gs1
      , forall (m :: * -> *) a. Monad m => a -> m a
return [Guard_ DS]
gs2
      ]
  desugarMatch DTerm
dt (APList Type
ty []) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt (Type -> Side -> Pattern_ TY -> Pattern_ TY
APInj Type
ty Side
L Pattern_ TY
APUnit)
  desugarMatch DTerm
dt (APList Type
ty [Pattern_ TY]
ps) =
    forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Pattern_ TY -> Pattern_ TY -> Pattern_ TY
APCons Type
ty) (Type -> [Pattern_ TY] -> Pattern_ TY
APList Type
ty []) [Pattern_ TY]
ps
  -- when dt is (p + t) ==> when dt is x0; let v = t; [if x0 >= v]; when x0-v is p
  desugarMatch DTerm
dt (APAdd Type
ty Side
_ Pattern_ TY
p ATerm
t) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
posRestrict ATerm -> ATerm -> ATerm
(-.) DTerm
dt Type
ty Pattern_ TY
p ATerm
t
   where
    posRestrict :: Type -> Maybe (ATerm -> ATerm -> ATerm)
posRestrict Type
plusty
      | Type
plusty forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type
TyN, Type
TyF] = forall a. a -> Maybe a
Just ATerm -> ATerm -> ATerm
(>=.)
      | Bool
otherwise = forall a. Maybe a
Nothing

  -- when dt is (p * t) ==> when dt is x0; let v = t; [if v divides x0]; when x0 / v is p
  desugarMatch DTerm
dt (APMul Type
ty Side
_ Pattern_ TY
p ATerm
t) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
intRestrict ATerm -> ATerm -> ATerm
(/.) DTerm
dt Type
ty Pattern_ TY
p ATerm
t
   where
    intRestrict :: Type -> Maybe (ATerm -> ATerm -> ATerm)
intRestrict Type
plusty
      | Type
plusty forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type
TyN, Type
TyZ] = forall a. a -> Maybe a
Just (forall a b c. (a -> b -> c) -> b -> a -> c
flip ATerm -> ATerm -> ATerm
(|.))
      | Bool
otherwise = forall a. Maybe a
Nothing

  -- when dt is (p - t) ==> when dt is x0; let v = t; when x0 + v is p
  desugarMatch DTerm
dt (APSub Type
ty Pattern_ TY
p ATerm
t) = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
arithBinMatch (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) ATerm -> ATerm -> ATerm
(+.) DTerm
dt Type
ty Pattern_ TY
p ATerm
t
  -- when dt is (p/q) ==> when $frac(dt) is (p, q)
  desugarMatch DTerm
dt (APFrac Type
_ Pattern_ TY
p Pattern_ TY
q) =
    forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch
      (DTerm -> DTerm -> DTerm
dtapp (Type -> Prim -> DTerm
DTPrim (Type
TyQ Type -> Type -> Type
:->: Type
TyZ Type -> Type -> Type
:*: Type
TyN) Prim
PrimFrac) DTerm
dt)
      (Type -> [Pattern_ TY] -> Pattern_ TY
APTup (Type
TyZ Type -> Type -> Type
:*: Type
TyN) [Pattern_ TY
p, Pattern_ TY
q])
  -- when dt is (-p) ==> when dt is x0; if x0 < 0; when -x0 is p
  desugarMatch DTerm
dt (APNeg Type
ty Pattern_ TY
p) = do
    -- when dt is x0
    (Name DTerm
x0, [Guard_ DS]
g1) <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [Guard_ DS])
varFor DTerm
dt

    -- if x0 < 0
    [Guard_ DS]
g2 <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [Guard_ DS]
desugarGuard forall a b. (a -> b) -> a -> b
$ Embed ATerm -> AGuard
AGBool (forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name ATerm -> ATerm
atVar Type
ty (coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
x0) ATerm -> ATerm -> ATerm
<. Type -> Integer -> ATerm
ATNat Type
ty Integer
0))

    -- when -x0 is p
    DTerm
neg <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall a b. (a -> b) -> a -> b
$ Type -> UOp -> ATerm -> ATerm
mkUn Type
ty UOp
Neg (Type -> Name ATerm -> ATerm
atVar Type
ty (coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
x0))
    [Guard_ DS]
g3 <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
neg Pattern_ TY
p

    forall (m :: * -> *) a. Monad m => a -> m a
return ([Guard_ DS]
g1 forall a. [a] -> [a] -> [a]
++ [Guard_ DS]
g2 forall a. [a] -> [a] -> [a]
++ [Guard_ DS]
g3)

  mkMatch :: Member Fresh r => DTerm -> DPattern -> Sem r [DGuard]
  mkMatch :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch DTerm
dt Pattern_ DS
dp = forall (m :: * -> *) a. Monad m => a -> m a
return [Embed DTerm -> Pattern_ DS -> Guard_ DS
DGPat (forall e. IsEmbed e => Embedded e -> e
embed DTerm
dt) Pattern_ DS
dp]

  varMatch :: Member Fresh r => DTerm -> Name DTerm -> Sem r [DGuard]
  varMatch :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Name DTerm -> Sem r [Guard_ DS]
varMatch DTerm
dt Name DTerm
x = forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch DTerm
dt (Type -> Name DTerm -> Pattern_ DS
DPVar (forall t. HasType t => t -> Type
getType DTerm
dt) Name DTerm
x)

  varFor :: Member Fresh r => DTerm -> Sem r (Name DTerm, [DGuard])
  varFor :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [Guard_ DS])
varFor (DTVar Type
_ (QName NameProvenance
_ Name DTerm
x)) = forall (m :: * -> *) a. Monad m => a -> m a
return (Name DTerm
x, []) -- XXX return a name + provenance??
  varFor DTerm
dt = do
    Name DTerm
x <- forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"x")
    [Guard_ DS]
g <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Name DTerm -> Sem r [Guard_ DS]
varMatch DTerm
dt Name DTerm
x
    forall (m :: * -> *) a. Monad m => a -> m a
return (Name DTerm
x, [Guard_ DS]
g)

  varForPat :: Member Fresh r => APattern -> Sem r (Name DTerm, [DGuard])
  varForPat :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Pattern_ TY -> Sem r (Name DTerm, [Guard_ DS])
varForPat (APVar Type
_ Name ATerm
x) = forall (m :: * -> *) a. Monad m => a -> m a
return (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x, [])
  varForPat Pattern_ TY
p = do
    Name DTerm
x <- forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
"px") -- changing this from x fixed a bug and I don't know why =(
    (Name DTerm
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch (Type -> Name DTerm -> DTerm
dtVar (forall t. HasType t => t -> Type
getType Pattern_ TY
p) Name DTerm
x) Pattern_ TY
p

  arithBinMatch ::
    Member Fresh r =>
    (Type -> Maybe (ATerm -> ATerm -> ATerm)) ->
    (ATerm -> ATerm -> ATerm) ->
    DTerm ->
    Type ->
    APattern ->
    ATerm ->
    Sem r [DGuard]
  arithBinMatch :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
restrict ATerm -> ATerm -> ATerm
inverse DTerm
dt Type
ty Pattern_ TY
p ATerm
t = do
    (Name DTerm
x0, [Guard_ DS]
g1) <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [Guard_ DS])
varFor DTerm
dt

    -- let v = t
    DTerm
t' <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
    (Name DTerm
v, [Guard_ DS]
g2) <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [Guard_ DS])
varFor DTerm
t'

    [Guard_ DS]
g3 <- case Type -> Maybe (ATerm -> ATerm -> ATerm)
restrict Type
ty of
      Maybe (ATerm -> ATerm -> ATerm)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return []
      -- if x0 `cmp` v
      Just ATerm -> ATerm -> ATerm
cmp ->
        forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [Guard_ DS]
desugarGuard forall a b. (a -> b) -> a -> b
$
          Embed ATerm -> AGuard
AGBool (forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name ATerm -> ATerm
atVar Type
ty (coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
x0) ATerm -> ATerm -> ATerm
`cmp` Type -> Name ATerm -> ATerm
atVar (forall t. HasType t => t -> Type
getType ATerm
t) (coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
v)))

    -- when x0 `inverse` v is p
    DTerm
inv <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (Type -> Name ATerm -> ATerm
atVar Type
ty (coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
x0) ATerm -> ATerm -> ATerm
`inverse` Type -> Name ATerm -> ATerm
atVar (forall t. HasType t => t -> Type
getType ATerm
t) (coerce :: forall a b. Coercible a b => a -> b
coerce Name DTerm
v))
    [Guard_ DS]
g4 <- forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
inv Pattern_ TY
p

    forall (m :: * -> *) a. Monad m => a -> m a
return ([Guard_ DS]
g1 forall a. [a] -> [a] -> [a]
++ [Guard_ DS]
g2 forall a. [a] -> [a] -> [a]
++ [Guard_ DS]
g3 forall a. [a] -> [a] -> [a]
++ [Guard_ DS]
g4)

-- | Desugar a container literal such as @[1,2,3]@ or @{1,2,3}@.
desugarContainer :: Member Fresh r => Type -> Container -> [(ATerm, Maybe ATerm)] -> Maybe (Ellipsis ATerm) -> Sem r DTerm
-- Literal list containers desugar to nested applications of cons.
desugarContainer :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer Type
ty Container
ListContainer [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
Nothing =
  forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
ty (BOp -> Prim
PrimBOp BOp
Cons)) (Type -> DTerm
DTNil Type
ty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(ATerm, Maybe ATerm)]
es
-- A list container with an ellipsis @[x, y, z .. e]@ desugars to an
-- application of the primitive 'until' function.
desugarContainer ty :: Type
ty@(TyList Type
_) Container
ListContainer [(ATerm, Maybe ATerm)]
es (Just (Until ATerm
t)) =
  Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
ty Prim
PrimUntil
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer Type
ty Container
ListContainer [(ATerm, Maybe ATerm)]
es forall a. Maybe a
Nothing
-- If desugaring a bag and there are any counts specified, desugar to
-- an application of bagFromCounts to a bag of pairs (with a literal
-- value of 1 filled in for missing counts as needed).
desugarContainer (TyBag Type
eltTy) Container
BagContainer [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(ATerm, Maybe ATerm)]
es =
      DTerm -> DTerm -> DTerm
dtapp (Type -> Prim -> DTerm
DTPrim (Type -> Type
TySet (Type
eltTy Type -> Type -> Type
:*: Type
TyN) Type -> Type -> Type
:->: Type -> Type
TyBag Type
eltTy) Prim
PrimC2B)
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer (Type -> Type
TyBag (Type
eltTy Type -> Type -> Type
:*: Type
TyN)) Container
BagContainer [(ATerm, Maybe ATerm)]
counts Maybe (Ellipsis ATerm)
mell
 where
  -- turn e.g.  x # 3, y   into   (x, 3), (y, 1)
  counts :: [(ATerm, Maybe ATerm)]
counts =
    [ (Type -> [ATerm] -> ATerm
ATTup (Type
eltTy Type -> Type -> Type
:*: Type
TyN) [ATerm
t, forall a. a -> Maybe a -> a
fromMaybe (Type -> Integer -> ATerm
ATNat Type
TyN Integer
1) Maybe ATerm
n], forall a. Maybe a
Nothing)
    | (ATerm
t, Maybe ATerm
n) <- [(ATerm, Maybe ATerm)]
es
    ]

-- Other containers desugar to an application of the appropriate
-- container conversion function to the corresponding desugared list.
desugarContainer Type
ty Container
_ [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell =
  DTerm -> DTerm -> DTerm
dtapp (Type -> Prim -> DTerm
DTPrim (Type -> Type
TyList Type
eltTy Type -> Type -> Type
:->: Type
ty) Prim
conv)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer (Type -> Type
TyList Type
eltTy) Container
ListContainer [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell
 where
  (Prim
conv, Type
eltTy) = case Type
ty of
    TyBag Type
e -> (Prim
PrimBag, Type
e)
    TySet Type
e -> (Prim
PrimSet, Type
e)
    Type
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! Non-container type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty forall a. [a] -> [a] -> [a]
++ String
" in desugarContainer"