-----------------------------------------------------------------------------
-- |
-- 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 :: Sem '[Fresh] a -> a
runDesugar = Sem '[] a -> a
forall a. Sem '[] a -> a
run (Sem '[] a -> a)
-> (Sem '[Fresh] a -> Sem '[] a) -> Sem '[Fresh] a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem '[Fresh] a -> Sem '[] a
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 (NameProvenance -> Name ATerm -> QName ATerm
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 ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t1 of
      (Type
_ :->: Type
r) -> Type
r
      Type
ty         -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! Got non-function type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" 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 (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t1 Type -> Type -> Type
:*: ATerm -> 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 (ATerm -> Type
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 ((Type -> Type -> Type) -> [Type] -> Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
(:*:) ((ATerm -> Type) -> [ATerm] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ATerm -> Type
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 (ATerm -> Type
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 (ATerm -> Type
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 (ATerm -> Type
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 = Telescope AGuard -> ATerm -> ABranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([AGuard] -> Telescope AGuard
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 (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
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 [] Maybe (Ellipsis ATerm)
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 (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t)) Container
ctr [(ATerm
t, Maybe ATerm
forall a. Maybe a
Nothing)] Maybe (Ellipsis ATerm)
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 (NameProvenance -> Name DTerm -> QName DTerm
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 DTerm -> Type
forall t. HasType t => t -> Type
getType DTerm
t1 of
      (Type
_ :->: Type
r) -> Type
r
      Type
ty         -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! Got non-function type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" 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 (DTerm -> Type
forall t. HasType t => t -> Type
getType DTerm
dt1 Type -> Type -> Type
:*: DTerm -> 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 (DTerm -> Type
forall t. HasType t => t -> Type
getType DTerm
dt1 Type -> Type -> Type
:*: DTerm -> 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 :: Defn -> Sem r DTerm
desugarDefn (Defn Name ATerm
_ [Type]
patTys Type
bodyTy [Clause]
def) =
  Quantifier -> Type -> [Clause] -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Quantifier -> Type -> [Clause] -> Sem r DTerm
desugarAbs Quantifier
Lam ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(:->:) Type
bodyTy [Type]
patTys) [Clause]
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 :: Quantifier -> Type -> [Clause] -> Sem r DTerm
desugarAbs Quantifier
Lam Type
ty [cl :: Clause
cl@(Clause -> ([APattern], ATerm)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> ([APVar Type
_ Name ATerm
_], ATerm
_))] = do
  ([APattern]
ps, ATerm
at) <- Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Clause
cl
  DTerm
d <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
at
  DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
Lam Type
ty (Name DTerm -> DTerm -> Bind (Name DTerm) DTerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (APattern -> Name DTerm
forall b. Coercible b (Name ATerm) => APattern -> b
getVar ([APattern] -> APattern
forall a. [a] -> a
head [APattern]
ps)) DTerm
d)
  where
    getVar :: APattern -> b
getVar (APVar Type
_ Name ATerm
x) = Name ATerm -> b
coerce Name ATerm
x
-- General case
desugarAbs Quantifier
quant Type
overallTy [Clause]
body = do
  [([APattern], ATerm)]
clausePairs <- [Clause] -> Sem r [([APattern], ATerm)]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Clause] -> Sem r [([APattern], ATerm)]
unbindClauses [Clause]
body
  let ([[APattern]]
pats, [ATerm]
bodies) = [([APattern], ATerm)] -> ([[APattern]], [ATerm])
forall a b. [(a, b)] -> ([a], [b])
unzip [([APattern], ATerm)]
clausePairs
  let patTys :: [Type]
patTys = (APattern -> Type) -> [APattern] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map APattern -> Type
forall t. HasType t => t -> Type
getType ([[APattern]] -> [APattern]
forall a. [a] -> a
head [[APattern]]
pats)
  let bodyTy :: Type
bodyTy = ATerm -> Type
forall t. HasType t => t -> Type
getType ([ATerm] -> ATerm
forall a. [a] -> a
head [ATerm]
bodies)

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

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

  where
    mkBranch :: [(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch
    mkBranch :: [(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch
mkBranch [(Name ATerm, Type)]
xs ATerm
b [APattern]
ps = Telescope AGuard -> ATerm -> ABranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([(Name ATerm, Type)] -> [APattern] -> Telescope AGuard
mkGuards [(Name ATerm, Type)]
xs [APattern]
ps) ATerm
b

    mkGuards :: [(Name ATerm, Type)] -> [APattern] -> Telescope AGuard
    mkGuards :: [(Name ATerm, Type)] -> [APattern] -> Telescope AGuard
mkGuards [(Name ATerm, Type)]
xs [APattern]
ps = [AGuard] -> Telescope AGuard
forall b. Alpha b => [b] -> Telescope b
toTelescope ([AGuard] -> Telescope AGuard) -> [AGuard] -> Telescope AGuard
forall a b. (a -> b) -> a -> b
$ (Embed ATerm -> APattern -> AGuard)
-> [Embed ATerm] -> [APattern] -> [AGuard]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Embed ATerm -> APattern -> AGuard
AGPat (((Name ATerm, Type) -> Embed ATerm)
-> [(Name ATerm, Type)] -> [Embed ATerm]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name ATerm
x,Type
ty) -> Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name ATerm -> ATerm
atVar Type
ty Name ATerm
x)) [(Name ATerm, Type)]
xs) [APattern]
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 :: [Clause] -> Sem r [([APattern], ATerm)]
unbindClauses [Clause
c] | Quantifier
quant Quantifier -> [Quantifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Quantifier
All, Quantifier
Ex] = do
      ([APattern]
ps, ATerm
t) <- Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Clause -> Sem r ([APattern], ATerm)
liftClause Clause
c
      [([APattern], ATerm)] -> Sem r [([APattern], ATerm)]
forall (m :: * -> *) a. Monad m => a -> m a
return [([APattern]
ps, [APattern] -> ATerm -> ATerm
addDbgInfo [APattern]
ps ATerm
t)]
    unbindClauses [Clause]
cs  = (Clause -> Sem r ([APattern], ATerm))
-> [Clause] -> Sem r [([APattern], ATerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind [Clause]
cs

    liftClause :: Member Fresh r => Bind [APattern] ATerm -> Sem r ([APattern], ATerm)
    liftClause :: Clause -> Sem r ([APattern], ATerm)
liftClause Clause
c = Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Clause
c Sem r ([APattern], ATerm)
-> (([APattern], ATerm) -> Sem r ([APattern], ATerm))
-> Sem r ([APattern], ATerm)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      ([APattern]
ps, ATAbs Quantifier
q Type
_ Clause
c') | Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
quant -> do
        ([APattern]
ps', ATerm
b) <- Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Clause -> Sem r ([APattern], ATerm)
liftClause Clause
c'
        ([APattern], ATerm) -> Sem r ([APattern], ATerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ([APattern]
ps [APattern] -> [APattern] -> [APattern]
forall a. [a] -> [a] -> [a]
++ [APattern]
ps', ATerm
b)
      ([APattern]
ps, ATerm
b) -> ([APattern], ATerm) -> Sem r ([APattern], ATerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ([APattern]
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 :: [APattern] -> ATerm -> ATerm
addDbgInfo [APattern]
ps ATerm
t = [([Char], Type, Name ATerm)] -> ATerm -> ATerm
ATTest (((Name ATerm, Type) -> ([Char], Type, Name ATerm))
-> [(Name ATerm, Type)] -> [([Char], Type, Name ATerm)]
forall a b. (a -> b) -> [a] -> [b]
map (Name ATerm, Type) -> ([Char], Type, Name ATerm)
forall a b. (Name a, b) -> ([Char], b, Name a)
withName ([(Name ATerm, Type)] -> [([Char], Type, Name ATerm)])
-> [(Name ATerm, Type)] -> [([Char], Type, Name ATerm)]
forall a b. (a -> b) -> a -> b
$ (APattern -> [(Name ATerm, Type)])
-> [APattern] -> [(Name ATerm, Type)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap APattern -> [(Name ATerm, Type)]
varsBound [APattern]
ps) ATerm
t
      where withName :: (Name a, b) -> ([Char], b, Name a)
withName (Name a
n, b
ty) = (Name a -> [Char]
forall a. Name a -> [Char]
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 :: Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B Prim
p Type
ty Type
cts Type
b = do
  Name ATerm
c <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"c")
  DTerm
body <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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)
      )
  DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
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 :: ATerm -> Sem r DTerm
desugarTerm (ATVar Type
ty QName ATerm
x) = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> QName DTerm -> DTerm
DTVar Type
ty (QName ATerm -> QName DTerm
coerce QName ATerm
x)
desugarTerm (ATPrim (Type
ty1 :->: Type
resTy) (PrimUOp UOp
uop))
  | Type -> Type -> UOp -> Bool
uopDesugars Type
ty1 Type
resTy UOp
uop = Type -> Type -> UOp -> Sem r DTerm
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 = Type -> Type -> Type -> BOp -> Sem r DTerm
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) = Prim -> Type -> Type -> Type -> Sem r DTerm
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) = Prim -> Type -> Type -> Type -> Sem r DTerm
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)        = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> Prim -> DTerm
DTPrim Type
ty Prim
x
desugarTerm ATerm
ATUnit               = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return DTerm
DTUnit
desugarTerm (ATBool Type
ty Bool
b)        = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> Bool -> DTerm
DTBool Type
ty Bool
b
desugarTerm (ATChar Char
c)           = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Char -> DTerm
DTChar Char
c
desugarTerm (ATString [Char]
cs)        =
  Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer (Type -> Type
TyList Type
TyC) Container
ListContainer ((Char -> (ATerm, Maybe ATerm)) -> [Char] -> [(ATerm, Maybe ATerm)]
forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> (Char -> ATerm
ATChar Char
c, Maybe ATerm
forall a. Maybe a
Nothing)) [Char]
cs) Maybe (Ellipsis ATerm)
forall a. Maybe a
Nothing
desugarTerm (ATAbs Quantifier
q Type
ty Clause
lam)     = Quantifier -> Type -> [Clause] -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Quantifier -> Type -> [Clause] -> Sem r DTerm
desugarAbs Quantifier
q Type
ty [Clause
lam]

-- Special cases for fully applied operators
desugarTerm (ATApp Type
resTy (ATPrim Type
_ (PrimUOp UOp
uop)) ATerm
t)
  | Type -> Type -> UOp -> Bool
uopDesugars (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t) Type
resTy UOp
uop = Type -> UOp -> ATerm -> Sem r DTerm
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 (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t1) (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t2) Type
resTy BOp
bop = Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
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 (DTerm -> DTerm -> DTerm) -> Sem r DTerm -> Sem r (DTerm -> DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t1 Sem r (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t2
desugarTerm (ATTup Type
ty [ATerm]
ts)        = Type -> [ATerm] -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> [ATerm] -> Sem r DTerm
desugarTuples Type
ty [ATerm]
ts
desugarTerm (ATNat Type
ty Integer
n)         = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> Integer -> DTerm
DTNat Type
ty Integer
n
desugarTerm (ATRat Rational
r)            = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Rational -> DTerm
DTRat Rational
r

desugarTerm (ATTyOp Type
ty TyOp
op Type
t)      = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> TyOp -> Type -> DTerm
DTTyOp Type
ty TyOp
op Type
t

desugarTerm (ATChain Type
_ ATerm
t1 [ALink]
links)  = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ ATerm -> [ALink] -> ATerm
expandChain ATerm
t1 [ALink]
links

desugarTerm (ATContainer Type
ty Container
c [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell) = Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
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 AQual) ATerm
bqt) = do
  (Telescope AQual
qs, ATerm
t) <- Bind (Telescope AQual) ATerm -> Sem r (Telescope AQual, ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope AQual) ATerm
bqt
  Container -> ATerm -> Telescope AQual -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope AQual -> Sem r DTerm
desugarComp Container
ctr ATerm
t Telescope AQual
qs

desugarTerm (ATLet Type
_ Bind (Telescope ABinding) ATerm
t) = do
  (Telescope ABinding
bs, ATerm
t2) <- Bind (Telescope ABinding) ATerm
-> Sem r (Telescope ABinding, ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope ABinding) ATerm
t
  [ABinding] -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[ABinding] -> ATerm -> Sem r DTerm
desugarLet (Telescope ABinding -> [ABinding]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope ABinding
bs) ATerm
t2

desugarTerm (ATCase Type
ty [ABranch]
bs) = Type -> [DBranch] -> DTerm
DTCase Type
ty ([DBranch] -> DTerm) -> Sem r [DBranch] -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ABranch -> Sem r DBranch) -> [ABranch] -> Sem r [DBranch]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ABranch -> Sem r DBranch
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ABranch -> Sem r DBranch
desugarBranch [ABranch]
bs

desugarTerm (ATTest [([Char], Type, Name ATerm)]
info ATerm
t) = [([Char], Type, Name DTerm)] -> DTerm -> DTerm
DTTest ([([Char], Type, Name ATerm)] -> [([Char], Type, Name DTerm)]
coerce [([Char], Type, Name ATerm)]
info) (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
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 :: ATerm -> Sem r DTerm
desugarProperty ATerm
p = [([Char], Type, Name DTerm)] -> DTerm -> DTerm
DTTest [] (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
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
_ Type
_         UOp
uop = UOp
uop UOp -> UOp -> Bool
forall a. Eq a => a -> a -> Bool
== UOp
Not

desugarPrimUOp :: Member Fresh r => Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp :: Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp Type
argTy Type
resTy UOp
op = do
  Name ATerm
x <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"arg")
  DTerm
body <- Type -> UOp -> ATerm -> Sem r DTerm
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)
  DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
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
bopDesugars Type
_   Type
_   Type
_ BOp
bop = BOp
bop BOp -> [BOp] -> Bool
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 :: Type -> Type -> Type -> BOp -> Sem r DTerm
desugarPrimBOp Type
ty1 Type
ty2 Type
resTy BOp
op = do
  Name ATerm
p <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"pair1")
  Name ATerm
x <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"arg1")
  Name ATerm
y <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"arg2")
  let argsTy :: Type
argsTy = Type
ty1 Type -> Type -> Type
:*: Type
ty2
  DTerm
body <- Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
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)
  DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda (Type
argsTy Type -> Type -> Type
:->: Type
resTy) [Name ATerm
p] (DTerm -> DTerm) -> DTerm -> DTerm
forall a b. (a -> b) -> a -> b
$
    Type -> [DBranch] -> DTerm
DTCase Type
resTy
    [ Telescope DGuard -> DTerm -> DBranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind
        ([DGuard] -> Telescope DGuard
forall b. Alpha b => [b] -> Telescope b
toTelescope [Embed DTerm -> DPattern -> DGuard
DGPat (Embedded (Embed DTerm) -> Embed DTerm
forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name DTerm -> DTerm
dtVar Type
argsTy (Name ATerm -> Name DTerm
coerce Name ATerm
p))) (Type -> Name DTerm -> Name DTerm -> DPattern
DPPair Type
argsTy (Name ATerm -> Name DTerm
coerce Name ATerm
x) (Name ATerm -> Name DTerm
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 :: Type -> UOp -> ATerm -> Sem r DTerm
desugarUnApp Type
_ UOp
Not ATerm
t = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
  Type -> [ABranch] -> ATerm
ATCase Type
TyBool
    [ ATerm
fls ATerm -> [AGuard] -> ABranch
<==. [Embed ATerm -> AGuard
AGBool (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
ATerm
t)]
    , ATerm
tru ATerm -> [AGuard] -> ABranch
<==. []
    ]

desugarUnApp Type
ty UOp
uop ATerm
t = [Char] -> Sem r DTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> Sem r DTerm) -> [Char] -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! desugarUnApp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ UOp -> [Char]
forall a. Show a => a -> [Char]
show UOp
uop [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ATerm -> [Char]
forall a. Show a => a -> [Char]
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 :: Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
desugarBinApp Type
_ BOp
And ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ ATerm
t2 ATerm -> ATerm -> ATerm
<. ATerm
t1
desugarBinApp Type
_ BOp
Leq ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
  Type -> ATerm -> ATerm -> ATerm
ATApp Type
resTy (Type -> Prim -> ATerm
ATPrim (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t1 Type -> Type -> Type
:->: Type
resTy) Prim
PrimFloor) (Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin (ATerm -> Type
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
  = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 BOp -> [BOp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Inter, BOp
Diff, BOp
Union] =
    ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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
_     = [Char] -> Prim
forall a. HasCallStack => [Char] -> a
error ([Char] -> Prim) -> [Char] -> Prim
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! mergeOp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BOp -> [Char]
forall a. Show a => a -> [Char]
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 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
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 = ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t1

desugarBinApp Type
ty BOp
bop ATerm
t1 ATerm
t2 = [Char] -> Sem r DTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> Sem r DTerm) -> [Char] -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! desugarBinApp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BOp -> [Char]
forall a. Show a => a -> [Char]
show BOp
bop [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ATerm -> [Char]
forall a. Show a => a -> [Char]
show ATerm
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ATerm -> [Char]
forall a. Show a => a -> [Char]
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 :: Container -> ATerm -> Telescope AQual -> Sem r DTerm
desugarComp Container
ctr ATerm
t Telescope AQual
qs = Container -> ATerm -> Telescope AQual -> Sem r ATerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope AQual -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope AQual
qs Sem r ATerm -> (ATerm -> Sem r DTerm) -> Sem r DTerm
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ATerm -> Sem r DTerm
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 :: Container -> ATerm -> Telescope AQual -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope AQual
TelEmpty = ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Container -> ATerm -> ATerm
ctrSingleton Container
ctr ATerm
t

-- [ t | q, qs ] = ...
expandComp Container
ctr ATerm
t (TelCons (Rebind AQual (Telescope AQual) -> (AQual, Telescope AQual)
forall p1 p2. (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind -> (AQual
q,Telescope AQual
qs)))
  = case AQual
q of
      -- [ t | x in l, qs ] = join (map (\x -> [t | qs]) l)
      AQBind Name ATerm
x (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
lst) -> do
        ATerm
tqs <- Container -> ATerm -> Telescope AQual -> Sem r ATerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope AQual -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope AQual
qs
        let c :: Type -> Type
c      = Container -> Type -> Type
containerTy Container
ctr
            tTy :: Type
tTy    = ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t
            xTy :: Type
xTy    = case ATerm -> Type
forall t. HasType t => t -> Type
getType Embedded (Embed ATerm)
ATerm
lst of
                       TyContainer Atom
_ Type
e -> Type
e
                       Type
_ -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"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)
        ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim Type
joinTy Prim
PrimJoin) (ATerm -> ATerm) -> ATerm -> ATerm
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 -> Clause -> ATerm
ATAbs Quantifier
Lam (Type
xTy Type -> Type -> Type
:->: Type -> Type
c Type
tTy) ([APattern] -> ATerm -> Clause
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Type -> Name ATerm -> APattern
APVar Type
xTy Name ATerm
x] ATerm
tqs))
              Embedded (Embed ATerm)
ATerm
lst
            )

      -- [ t | g, qs ] = if g then [ t | qs ] else []
      AQGuard (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
g)    -> do
        ATerm
tqs <- Container -> ATerm -> Telescope AQual -> Sem r ATerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope AQual -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope AQual
qs
        ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Type -> [ABranch] -> ATerm
ATCase (Container -> Type -> Type
containerTy Container
ctr (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t))
          [ ATerm
tqs                    ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif Embedded (Embed ATerm)
ATerm
g]
          , Container -> Type -> ATerm
ctrNil Container
ctr (ATerm -> Type
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 :: [ABinding] -> ATerm -> Sem r DTerm
desugarLet [] ATerm
t = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
desugarLet ((ABinding Maybe (Embed PolyType)
_ Name ATerm
x (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
t1)) : [ABinding]
ls) ATerm
t =
  DTerm -> DTerm -> DTerm
dtapp
    (DTerm -> DTerm -> DTerm) -> Sem r DTerm -> Sem r (DTerm -> DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
Lam (ATerm -> Type
forall t. HasType t => t -> Type
getType Embedded (Embed ATerm)
ATerm
t1 Type -> Type -> Type
:->: ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t)
          (Bind (Name DTerm) DTerm -> DTerm)
-> Sem r (Bind (Name DTerm) DTerm) -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name DTerm -> DTerm -> Bind (Name DTerm) DTerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Name ATerm -> Name DTerm
coerce Name ATerm
x) (DTerm -> Bind (Name DTerm) DTerm)
-> Sem r DTerm -> Sem r (Bind (Name DTerm) DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ABinding] -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[ABinding] -> ATerm -> Sem r DTerm
desugarLet [ABinding]
ls ATerm
t)
        )
    Sem r (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
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 (Name DTerm -> DTerm -> Bind (Name DTerm) DTerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Name ATerm -> Name DTerm
coerce Name ATerm
x) (Type -> [Name ATerm] -> DTerm
go Type
ty2 [Name ATerm]
xs))
    go Type
ty [Name ATerm]
as = [Char] -> DTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> DTerm) -> [Char] -> DTerm
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! mkLambda.go " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Name ATerm] -> [Char]
forall a. Show a => a -> [Char]
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 = ((Name ATerm, Type) -> DTerm -> DTerm)
-> DTerm -> [(Name ATerm, Type)] -> DTerm
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name ATerm, Type) -> DTerm -> DTerm
quantify DTerm
c ([Name ATerm] -> [Type] -> [(Name ATerm, Type)]
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 (Name DTerm -> DTerm -> Bind (Name DTerm) DTerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Name ATerm -> Name DTerm
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 :: Type -> [ATerm] -> Sem r DTerm
desugarTuples Type
_ [ATerm
t]                    = ATerm -> Sem r DTerm
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 (DTerm -> DTerm -> DTerm) -> Sem r DTerm -> Sem r (DTerm -> DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t Sem r (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> [ATerm] -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> [ATerm] -> Sem r DTerm
desugarTuples Type
ty2 [ATerm]
ts
desugarTuples Type
ty [ATerm]
ats
  = [Char] -> Sem r DTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> Sem r DTerm) -> [Char] -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! desugarTuples " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ATerm] -> [Char]
forall a. Show a => a -> [Char]
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 -> [ALink] -> ATerm
expandChain ATerm
_ [] = [Char] -> ATerm
forall a. HasCallStack => [Char] -> a
error [Char]
"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 : [ALink]
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 -> [ALink] -> ATerm
expandChain ATerm
t2 [ALink]
links)

-- | Desugar a branch of a case expression.
desugarBranch :: Member Fresh r => ABranch -> Sem r DBranch
desugarBranch :: ABranch -> Sem r DBranch
desugarBranch ABranch
b = do
  (Telescope AGuard
ags, ATerm
at) <- ABranch -> Sem r (Telescope AGuard, ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind ABranch
b
  Telescope DGuard
dgs <- Telescope AGuard -> Sem r (Telescope DGuard)
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Telescope AGuard -> Sem r (Telescope DGuard)
desugarGuards Telescope AGuard
ags
  DTerm
d   <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
at
  DBranch -> Sem r DBranch
forall (m :: * -> *) a. Monad m => a -> m a
return (DBranch -> Sem r DBranch) -> DBranch -> Sem r DBranch
forall a b. (a -> b) -> a -> b
$ Telescope DGuard -> DTerm -> DBranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope DGuard
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 :: Telescope AGuard -> Sem r (Telescope DGuard)
desugarGuards = ([[DGuard]] -> Telescope DGuard)
-> Sem r [[DGuard]] -> Sem r (Telescope DGuard)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([DGuard] -> Telescope DGuard
forall b. Alpha b => [b] -> Telescope b
toTelescope ([DGuard] -> Telescope DGuard)
-> ([[DGuard]] -> [DGuard]) -> [[DGuard]] -> Telescope DGuard
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[DGuard]] -> [DGuard]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) (Sem r [[DGuard]] -> Sem r (Telescope DGuard))
-> (Telescope AGuard -> Sem r [[DGuard]])
-> Telescope AGuard
-> Sem r (Telescope DGuard)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AGuard -> Sem r [DGuard]) -> [AGuard] -> Sem r [[DGuard]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM AGuard -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [DGuard]
desugarGuard ([AGuard] -> Sem r [[DGuard]])
-> (Telescope AGuard -> [AGuard])
-> Telescope AGuard
-> Sem r [[DGuard]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope AGuard -> [AGuard]
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 :: AGuard -> Sem r [DGuard]
desugarGuard (AGBool (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at)) = do
      DTerm
dt <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
ATerm
at
      DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (Type -> Side -> APattern -> APattern
APInj Type
TyBool Side
R APattern
APUnit)

    -- 'let x = t' is desugared to 'when t is x'.
    desugarGuard (AGLet (ABinding Maybe (Embed PolyType)
_ Name ATerm
x (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at))) = do
      DTerm
dt <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
ATerm
at
      DTerm -> Name DTerm -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Name DTerm -> Sem r [DGuard]
varMatch DTerm
dt (Name ATerm -> Name DTerm
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 (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at) APattern
p) = do
      DTerm
dt <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
ATerm
at
      DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt APattern
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 :: DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (APVar Type
ty Name ATerm
x)      = DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt (Type -> Name DTerm -> DPattern
DPVar Type
ty (Name ATerm -> Name DTerm
coerce Name ATerm
x))
    desugarMatch DTerm
_  (APWild Type
_)        = [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    desugarMatch DTerm
dt APattern
APUnit            = DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt DPattern
DPUnit
    desugarMatch DTerm
dt (APBool Bool
b)        = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (Type -> Side -> APattern -> APattern
APInj Type
TyBool (Side -> Side -> Bool -> Side
forall a. a -> a -> Bool -> a
bool Side
L Side
R Bool
b) APattern
APUnit)
    desugarMatch DTerm
dt (APNat Type
ty Integer
n)      = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
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 -> APattern
APBool Bool
True)
    desugarMatch DTerm
dt (APChar Char
c)        = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch (Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
TyBool (BOp -> Prim
PrimBOp BOp
Eq) DTerm
dt (Char -> DTerm
DTChar Char
c)) (Bool -> APattern
APBool Bool
True)
    desugarMatch DTerm
dt (APString [Char]
s)      = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (Type -> [APattern] -> APattern
APList (Type -> Type
TyList Type
TyC) ((Char -> APattern) -> [Char] -> [APattern]
forall a b. (a -> b) -> [a] -> [b]
map Char -> APattern
APChar [Char]
s))
    desugarMatch DTerm
dt (APTup Type
tupTy [APattern]
pat) = Type -> DTerm -> [APattern] -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> DTerm -> [APattern] -> Sem r [DGuard]
desugarTuplePats Type
tupTy DTerm
dt [APattern]
pat
      where
        desugarTuplePats :: Member Fresh r => Type -> DTerm -> [APattern] -> Sem r [DGuard]
        desugarTuplePats :: Type -> DTerm -> [APattern] -> Sem r [DGuard]
desugarTuplePats Type
_ DTerm
_  [] = [Char] -> Sem r [DGuard]
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible! desugarTuplePats []"
        desugarTuplePats Type
_ DTerm
t [APattern
p] = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
t APattern
p
        desugarTuplePats ty :: Type
ty@(Type
_ :*: Type
ty2) DTerm
t (APattern
p:[APattern]
ps) = do
          (Name DTerm
x1,[DGuard]
gs1) <- APattern -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
APattern -> Sem r (Name DTerm, [DGuard])
varForPat APattern
p
          (Name DTerm
x2,[DGuard]
gs2) <- case [APattern]
ps of
            [APVar Type
_ Name ATerm
px2] -> (Name DTerm, [DGuard]) -> Sem r (Name DTerm, [DGuard])
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ATerm -> Name DTerm
coerce Name ATerm
px2, [])
            [APattern]
_             -> do
              Name DTerm
x <- Name DTerm -> Sem r (Name DTerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name DTerm
forall a. [Char] -> Name a
string2Name [Char]
"x")
              (Name DTerm
x,) ([DGuard] -> (Name DTerm, [DGuard]))
-> Sem r [DGuard] -> Sem r (Name DTerm, [DGuard])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> DTerm -> [APattern] -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> DTerm -> [APattern] -> Sem r [DGuard]
desugarTuplePats Type
ty2 (Type -> Name DTerm -> DTerm
dtVar Type
ty2 Name DTerm
x) [APattern]
ps
          ([[DGuard]] -> [DGuard]) -> Sem r [[DGuard]] -> Sem r [DGuard]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[DGuard]] -> [DGuard]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Sem r [[DGuard]] -> Sem r [DGuard])
-> ([Sem r [DGuard]] -> Sem r [[DGuard]])
-> [Sem r [DGuard]]
-> Sem r [DGuard]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r [DGuard]] -> Sem r [[DGuard]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Sem r [DGuard]] -> Sem r [DGuard])
-> [Sem r [DGuard]] -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$
            [ DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
t (DPattern -> Sem r [DGuard]) -> DPattern -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$ Type -> Name DTerm -> Name DTerm -> DPattern
DPPair Type
ty Name DTerm
x1 Name DTerm
x2
            , [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs1
            , [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs2
            ]
        desugarTuplePats Type
ty DTerm
_ [APattern]
_
          = [Char] -> Sem r [DGuard]
forall a. HasCallStack => [Char] -> a
error ([Char] -> Sem r [DGuard]) -> [Char] -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! desugarTuplePats with non-pair type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty

    desugarMatch DTerm
dt (APInj Type
ty Side
s APattern
p) = do
      (Name DTerm
x,[DGuard]
gs) <- APattern -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
APattern -> Sem r (Name DTerm, [DGuard])
varForPat APattern
p
      ([[DGuard]] -> [DGuard]) -> Sem r [[DGuard]] -> Sem r [DGuard]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[DGuard]] -> [DGuard]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Sem r [[DGuard]] -> Sem r [DGuard])
-> ([Sem r [DGuard]] -> Sem r [[DGuard]])
-> [Sem r [DGuard]]
-> Sem r [DGuard]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r [DGuard]] -> Sem r [[DGuard]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Sem r [DGuard]] -> Sem r [DGuard])
-> [Sem r [DGuard]] -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$
        [ DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt (DPattern -> Sem r [DGuard]) -> DPattern -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$ Type -> Side -> Name DTerm -> DPattern
DPInj Type
ty Side
s Name DTerm
x
        , [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs
        ]

    desugarMatch DTerm
dt (APCons Type
ty APattern
p1 APattern
p2) = do
      Name DTerm
y <- Name DTerm -> Sem r (Name DTerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name DTerm
forall a. [Char] -> Name a
string2Name [Char]
"y")
      (Name DTerm
x1, [DGuard]
gs1) <- APattern -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
APattern -> Sem r (Name DTerm, [DGuard])
varForPat APattern
p1
      (Name DTerm
x2, [DGuard]
gs2) <- APattern -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
APattern -> Sem r (Name DTerm, [DGuard])
varForPat APattern
p2

      let eltTy :: Type
eltTy = APattern -> Type
forall t. HasType t => t -> Type
getType APattern
p1
          unrolledTy :: Type
unrolledTy = Type
eltTy Type -> Type -> Type
:*: Type
ty
      ([[DGuard]] -> [DGuard]) -> Sem r [[DGuard]] -> Sem r [DGuard]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[DGuard]] -> [DGuard]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Sem r [[DGuard]] -> Sem r [DGuard])
-> ([Sem r [DGuard]] -> Sem r [[DGuard]])
-> [Sem r [DGuard]]
-> Sem r [DGuard]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r [DGuard]] -> Sem r [[DGuard]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Sem r [DGuard]] -> Sem r [DGuard])
-> [Sem r [DGuard]] -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$
        [ DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt (Type -> Side -> Name DTerm -> DPattern
DPInj Type
ty Side
R Name DTerm
y)
        , DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch (Type -> Name DTerm -> DTerm
dtVar Type
unrolledTy Name DTerm
y) (Type -> Name DTerm -> Name DTerm -> DPattern
DPPair Type
unrolledTy Name DTerm
x1 Name DTerm
x2)
        , [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs1
        , [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs2
        ]

    desugarMatch DTerm
dt (APList Type
ty []) = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (Type -> Side -> APattern -> APattern
APInj Type
ty Side
L APattern
APUnit)
    desugarMatch DTerm
dt (APList Type
ty [APattern]
ps) =
      DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (APattern -> Sem r [DGuard]) -> APattern -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$ (APattern -> APattern -> APattern)
-> APattern -> [APattern] -> APattern
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> APattern -> APattern -> APattern
APCons Type
ty) (Type -> [APattern] -> APattern
APList Type
ty []) [APattern]
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
_ APattern
p ATerm
t) = (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
posRestrict ATerm -> ATerm -> ATerm
(-.) DTerm
dt Type
ty APattern
p ATerm
t
      where
        posRestrict :: Type -> Maybe (ATerm -> ATerm -> ATerm)
posRestrict Type
plusty
          | Type
plusty Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type
TyN, Type
TyF] = (ATerm -> ATerm -> ATerm) -> Maybe (ATerm -> ATerm -> ATerm)
forall a. a -> Maybe a
Just ATerm -> ATerm -> ATerm
(>=.)
          | Bool
otherwise                = Maybe (ATerm -> ATerm -> ATerm)
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
_ APattern
p ATerm
t) = (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
intRestrict ATerm -> ATerm -> ATerm
(/.) DTerm
dt Type
ty APattern
p ATerm
t
      where
        intRestrict :: Type -> Maybe (ATerm -> ATerm -> ATerm)
intRestrict Type
plusty
          | Type
plusty Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type
TyN, Type
TyZ] = (ATerm -> ATerm -> ATerm) -> Maybe (ATerm -> ATerm -> ATerm)
forall a. a -> Maybe a
Just ((ATerm -> ATerm -> ATerm) -> ATerm -> ATerm -> ATerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip ATerm -> ATerm -> ATerm
(|.))
          | Bool
otherwise                = Maybe (ATerm -> ATerm -> ATerm)
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 APattern
p ATerm
t)  = (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
arithBinMatch (Maybe (ATerm -> ATerm -> ATerm)
-> Type -> Maybe (ATerm -> ATerm -> ATerm)
forall a b. a -> b -> a
const Maybe (ATerm -> ATerm -> ATerm)
forall a. Maybe a
Nothing) ATerm -> ATerm -> ATerm
(+.) DTerm
dt Type
ty APattern
p ATerm
t

    -- when dt is (p/q) ==> when $frac(dt) is (p, q)
    desugarMatch DTerm
dt (APFrac Type
_ APattern
p APattern
q)
      = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
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 -> [APattern] -> APattern
APTup (Type
TyZ Type -> Type -> Type
:*: Type
TyN) [APattern
p, APattern
q])

    -- when dt is (-p) ==> when dt is x0; if x0 < 0; when -x0 is p
    desugarMatch DTerm
dt (APNeg Type
ty APattern
p) = do

      -- when dt is x0
      (Name DTerm
x0, [DGuard]
g1) <- DTerm -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [DGuard])
varFor DTerm
dt

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

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

      [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DGuard]
g1 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
g2 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
g3)

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

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

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

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

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

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

      [DGuard]
g3 <- case Type -> Maybe (ATerm -> ATerm -> ATerm)
restrict Type
ty of
        Maybe (ATerm -> ATerm -> ATerm)
Nothing -> [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return []

        -- if x0 `cmp` v
        Just ATerm -> ATerm -> ATerm
cmp ->
          AGuard -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [DGuard]
desugarGuard (AGuard -> Sem r [DGuard]) -> AGuard -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$
            Embed ATerm -> AGuard
AGBool (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name ATerm -> ATerm
atVar Type
ty (Name DTerm -> Name ATerm
coerce Name DTerm
x0) ATerm -> ATerm -> ATerm
`cmp` Type -> Name ATerm -> ATerm
atVar (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t) (Name DTerm -> Name ATerm
coerce Name DTerm
v)))

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

      [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DGuard]
g1 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
g2 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
g3 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
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 :: Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer Type
ty Container
ListContainer [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
Nothing =
  (DTerm -> DTerm -> DTerm) -> DTerm -> [DTerm] -> DTerm
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) ([DTerm] -> DTerm) -> Sem r [DTerm] -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ATerm, Maybe ATerm) -> Sem r DTerm)
-> [(ATerm, Maybe ATerm)] -> Sem r [DTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm)
-> ((ATerm, Maybe ATerm) -> ATerm)
-> (ATerm, Maybe ATerm)
-> Sem r DTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm, Maybe ATerm) -> ATerm
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
    (DTerm -> DTerm -> DTerm) -> Sem r DTerm -> Sem r (DTerm -> DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
    Sem r (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
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)
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
  | ((ATerm, Maybe ATerm) -> Bool) -> [(ATerm, Maybe ATerm)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe ATerm -> Bool
forall a. Maybe a -> Bool
isJust (Maybe ATerm -> Bool)
-> ((ATerm, Maybe ATerm) -> Maybe ATerm)
-> (ATerm, Maybe ATerm)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm, Maybe ATerm) -> Maybe ATerm
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)
      (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
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, ATerm -> Maybe ATerm -> ATerm
forall a. a -> Maybe a -> a
fromMaybe (Type -> Integer -> ATerm
ATNat Type
TyN Integer
1) Maybe ATerm
n], Maybe ATerm
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)
    (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
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
_       -> [Char] -> (Prim, Type)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (Prim, Type)) -> [Char] -> (Prim, Type)
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! Non-container type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in desugarContainer"