{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-}
{-# OPTIONS_GHC -fno-warn-x-data-list-nonempty-unzip #-}

{-# HLINT ignore "Functor law" #-}

-- |
-- 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 (zipWithM)
import Data.Bool (bool)
import Data.Coerce
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Maybe (fromMaybe, isJust)
import Disco.AST.Desugared
import Disco.AST.Surface
import Disco.AST.Typed
import Disco.Effects.Fresh
import Disco.Module
import Disco.Names
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Typecheck (containerTy)
import Disco.Types
import Polysemy (Member, Sem, run)
import Unbound.Generics.LocallyNameless (
  Bind,
  Name,
  bind,
  embed,
  name2String,
  string2Name,
  unembed,
  unrebind,
 )
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)

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

-- | Run a desugaring computation.
runDesugar :: Sem '[Fresh] a -> a
runDesugar :: forall a. Sem '[Fresh] a -> a
runDesugar = 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 -> String -> Type
forall a. HasCallStack => String -> a
error (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ String
"Impossible! Got non-function type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 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 a. (a -> a -> a) -> [a] -> a
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 -> String -> Type
forall a. HasCallStack => String -> a
error (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ String
"Impossible! Got non-function type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Defn -> Sem r DTerm
desugarDefn (Defn Name ATerm
_ [Type]
patTys Type
bodyTy NonEmpty (Bind [Pattern_ TY] ATerm)
def) =
  Quantifier
-> Type -> NonEmpty (Bind [Pattern_ TY] ATerm) -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Quantifier
-> Type -> NonEmpty (Bind [Pattern_ TY] ATerm) -> Sem r DTerm
desugarAbs Quantifier
Lam ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(:->:) Type
bodyTy [Type]
patTys) NonEmpty (Bind [Pattern_ TY] ATerm)
def

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

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

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

  -- Create lambdas and one big case.  Recursively desugar the case to
  -- deal with arithmetic patterns.
  let branches :: NonEmpty ABranch
branches = (ATerm -> [Pattern_ TY] -> ABranch)
-> NonEmpty ATerm -> NonEmpty [Pattern_ TY] -> NonEmpty ABranch
forall a b c.
(a -> b -> c) -> NonEmpty a -> NonEmpty b -> NonEmpty c
NE.zipWith ([(Name ATerm, Type)] -> ATerm -> [Pattern_ TY] -> ABranch
mkBranch ([Name ATerm] -> [Type] -> [(Name ATerm, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name ATerm]
args [Type]
patTys)) NonEmpty ATerm
bodies NonEmpty [Pattern_ TY]
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 (NonEmpty ABranch -> [ABranch]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty ABranch
branches)
  DTerm -> Sem r DTerm
forall a. a -> Sem r a
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]
forall a b. Coercible a b => a -> b
coerce [Name ATerm]
args) DTerm
dcase
 where
  mkBranch :: [(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch
  mkBranch :: [(Name ATerm, Type)] -> ATerm -> [Pattern_ TY] -> ABranch
mkBranch [(Name ATerm, Type)]
xs ATerm
b [Pattern_ TY]
ps = Telescope AGuard -> ATerm -> ABranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([(Name ATerm, Type)] -> [Pattern_ TY] -> Telescope AGuard
mkGuards [(Name ATerm, Type)]
xs [Pattern_ TY]
ps) ATerm
b

  mkGuards :: [(Name ATerm, Type)] -> [APattern] -> Telescope AGuard
  mkGuards :: [(Name ATerm, Type)] -> [Pattern_ TY] -> Telescope AGuard
mkGuards [(Name ATerm, Type)]
xs [Pattern_ TY]
ps = [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 -> Pattern_ TY -> AGuard)
-> [Embed ATerm] -> [Pattern_ TY] -> [AGuard]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Embed ATerm -> Pattern_ TY -> 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) [Pattern_ TY]
ps

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

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

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

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

-- | Desugar the application of a "bag from counts" primitive on a
--   list, either a safe or unsafe variant.
desugarCList2B :: Member Fresh r => Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B Prim
p Type
ty Type
cts Type
b = do
  Name ATerm
c <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name ATerm
forall a. String -> Name a
string2Name String
"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 a. a -> Sem r a
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 the @min@ and @max@ functions into conditional expressions.
desugarMinMax :: Member Fresh r => Prim -> Type -> Sem r DTerm
desugarMinMax :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Prim -> Type -> Sem r DTerm
desugarMinMax Prim
m Type
ty = do
  Name ATerm
p <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name ATerm
forall a. String -> Name a
string2Name String
"p")
  Name ATerm
a <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name ATerm
forall a. String -> Name a
string2Name String
"a")
  Name ATerm
b <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name ATerm
forall a. String -> Name a
string2Name String
"b")
  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
$
      Type -> [ABranch] -> ATerm
ATCase
        Type
ty
        [ 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 [Embed ATerm -> Pattern_ TY -> AGuard
AGPat (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name ATerm -> ATerm
atVar Type
ty Name ATerm
p)) (Type -> [Pattern_ TY] -> Pattern_ TY
APTup (Type
ty Type -> Type -> Type
:*: Type
ty) [Type -> Name ATerm -> Pattern_ TY
APVar Type
ty Name ATerm
a, Type -> Name ATerm -> Pattern_ TY
APVar Type
ty Name ATerm
b])])
            (ATerm -> ABranch) -> ATerm -> ABranch
forall a b. (a -> b) -> a -> b
$ Type -> [ABranch] -> ATerm
ATCase
              Type
ty
              [ Type -> Name ATerm -> ATerm
atVar Type
ty (if Prim
m Prim -> Prim -> Bool
forall a. Eq a => a -> a -> Bool
== Prim
PrimMin then Name ATerm
a else Name ATerm
b) ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif (Type -> Name ATerm -> ATerm
atVar Type
ty Name ATerm
a ATerm -> ATerm -> ATerm
<. Type -> Name ATerm -> ATerm
atVar Type
ty Name ATerm
b)]
              , Type -> Name ATerm -> ATerm
atVar Type
ty (if Prim
m Prim -> Prim -> Bool
forall a. Eq a => a -> a -> Bool
== Prim
PrimMin then Name ATerm
b else Name ATerm
a) ATerm -> [AGuard] -> ABranch
<==. []
              ]
        ]
  DTerm -> Sem r DTerm
forall a. a -> Sem r a
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 Type -> Type -> Type
:*: Type
ty) Type -> Type -> Type
:->: Type
ty) [Name ATerm
p] DTerm
body

-- | Desugar a typechecked term.
desugarTerm :: Member Fresh r => ATerm -> Sem r DTerm
desugarTerm :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATVar Type
ty QName ATerm
x) = DTerm -> Sem r DTerm
forall a. a -> Sem r a
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
forall a b. Coercible a b => a -> b
coerce QName ATerm
x)
desugarTerm (ATPrim (Type
ty1 :->: Type
resTy) (PrimUOp UOp
uop))
  | Type -> Type -> UOp -> Bool
uopDesugars Type
ty1 Type
resTy UOp
uop = 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
_ :->: Type
ty) Prim
PrimMin) = Prim -> Type -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Prim -> Type -> Sem r DTerm
desugarMinMax Prim
PrimMin Type
ty
desugarTerm (ATPrim (Type
_ :->: Type
ty) Prim
PrimMax) = Prim -> Type -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Prim -> Type -> Sem r DTerm
desugarMinMax Prim
PrimMax Type
ty
desugarTerm (ATPrim Type
ty Prim
x) = DTerm -> Sem r DTerm
forall a. a -> Sem r a
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return DTerm
DTUnit
desugarTerm (ATBool Type
ty Bool
b) = DTerm -> Sem r DTerm
forall a. a -> Sem r a
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 a. a -> Sem r a
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 String
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)) -> String -> [(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)) String
cs) Maybe (Ellipsis ATerm)
forall a. Maybe a
Nothing
desugarTerm (ATAbs Quantifier
q Type
ty Bind [Pattern_ TY] ATerm
lam) = Quantifier
-> Type -> NonEmpty (Bind [Pattern_ TY] ATerm) -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Quantifier
-> Type -> NonEmpty (Bind [Pattern_ TY] ATerm) -> Sem r DTerm
desugarAbs Quantifier
q Type
ty (Bind [Pattern_ TY] ATerm -> NonEmpty (Bind [Pattern_ TY] ATerm)
forall a. a -> NonEmpty a
NE.singleton Bind [Pattern_ TY] ATerm
lam)
-- Special cases for fully applied operators
desugarTerm (ATApp Type
resTy (ATPrim Type
_ (PrimUOp UOp
uop)) ATerm
t)
  | Type -> Type -> UOp -> Bool
uopDesugars (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 a b. Sem r (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 [Link_ TY]
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 -> [Link_ TY] -> ATerm
expandChain ATerm
t1 [Link_ TY]
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 (Qual_ TY)) ATerm
bqt) = do
  (Telescope (Qual_ TY)
qs, ATerm
t) <- Bind (Telescope (Qual_ TY)) ATerm
-> Sem r (Telescope (Qual_ TY), ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope (Qual_ TY)) ATerm
bqt
  Container -> ATerm -> Telescope (Qual_ TY) -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r DTerm
desugarComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs
desugarTerm (ATLet Type
_ Bind (Telescope (Binding_ TY)) ATerm
t) = do
  (Telescope (Binding_ TY)
bs, ATerm
t2) <- Bind (Telescope (Binding_ TY)) ATerm
-> Sem r (Telescope (Binding_ TY), ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope (Binding_ TY)) ATerm
t
  [Binding_ TY] -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Binding_ TY] -> ATerm -> Sem r DTerm
desugarLet (Telescope (Binding_ TY) -> [Binding_ TY]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope (Binding_ TY)
bs) ATerm
t2
desugarTerm (ATCase Type
ty [ABranch]
bs) = Type -> [DBranch] -> DTerm
DTCase Type
ty ([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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ABranch -> Sem r DBranch
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ABranch -> Sem r DBranch
desugarBranch [ABranch]
bs
desugarTerm (ATTest [(String, Type, Name ATerm)]
info ATerm
t) = [(String, Type, Name DTerm)] -> DTerm -> DTerm
DTTest ([(String, Type, Name ATerm)] -> [(String, Type, Name DTerm)]
forall a b. Coercible a b => a -> b
coerce [(String, 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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarProperty ATerm
p = [(String, 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 (Type -> ATerm -> ATerm
forall t. HasType t => Type -> t -> t
setType Type
TyProp ATerm
p)

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

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

desugarPrimUOp :: Member Fresh r => Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp Type
argTy Type
resTy UOp
op = do
  Name ATerm
x <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name ATerm
forall a. String -> Name a
string2Name String
"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 a. a -> Sem r a
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

-- Eq and Lt at type Prop desugar into ShouldEq, ShouldLt .
bopDesugars Type
_ Type
_ Type
TyProp BOp
bop | BOp
bop BOp -> [BOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Eq, BOp
Neq, BOp
Lt, BOp
Gt, BOp
Leq, BOp
Geq, BOp
Divides] = Bool
True
bopDesugars Type
_ Type
_ Type
_ BOp
bop =
  BOp
bop
    BOp -> [BOp] -> Bool
forall a. Eq a => a -> [a] -> 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
IDiv
           , BOp
Sub
           , BOp
SSub
           , BOp
Inter
           , BOp
Diff
           , BOp
Union
           , BOp
Subset
           ]

-- | Desugar a primitive binary operator at the given type.
desugarPrimBOp :: Member Fresh r => Type -> Type -> Type -> BOp -> Sem r DTerm
desugarPrimBOp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Type -> Type -> BOp -> Sem r DTerm
desugarPrimBOp Type
ty1 Type
ty2 Type
resTy BOp
op = do
  Name ATerm
p <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name ATerm
forall a. String -> Name a
string2Name String
"pair1")
  Name ATerm
x <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name ATerm
forall a. String -> Name a
string2Name String
"arg1")
  Name ATerm
y <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (String -> Name ATerm
forall a. String -> Name a
string2Name String
"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 a. a -> Sem r a
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 (Guard_ DS) -> DTerm -> DBranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind
            ([Guard_ DS] -> Telescope (Guard_ DS)
forall b. Alpha b => [b] -> Telescope b
toTelescope [Embed DTerm -> Pattern_ DS -> Guard_ DS
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
forall a b. Coercible a b => a -> b
coerce Name ATerm
p))) (Type -> Name DTerm -> Name DTerm -> Pattern_ DS
DPPair Type
argsTy (Name ATerm -> Name DTerm
forall a b. Coercible a b => a -> b
coerce Name ATerm
x) (Name ATerm -> Name DTerm
forall a b. Coercible a b => a -> b
coerce Name ATerm
y))])
            DTerm
body
        ]

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

-- XXX This should be turned into a standard library definition.
-- not t ==> {? false if t, true otherwise ?}
desugarUnApp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> UOp -> ATerm -> Sem r DTerm
desugarUnApp Type
_ UOp
Not ATerm
t =
  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 = String -> Sem r DTerm
forall a. HasCallStack => String -> a
error (String -> Sem r DTerm) -> String -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ String
"Impossible! desugarUnApp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UOp -> String
forall a. Show a => a -> String
show UOp
uop String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ATerm -> String
forall a. Show a => a -> String
show ATerm
t

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

-- And, Or, Impl at type Prop are primitive Prop constructors so don't
-- desugar; but we push the Prop type down so we properly desugar
-- their arguments.
desugarBinApp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
desugarBinApp Type
TyProp BOp
b ATerm
t1 ATerm
t2 | BOp
b BOp -> [BOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
And, BOp
Or, BOp
Impl] = do
  DTerm
d1 <- 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
forall t. HasType t => Type -> t -> t
setType Type
TyProp ATerm
t1
  DTerm
d2 <- 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
forall t. HasType t => Type -> t -> t
setType Type
TyProp ATerm
t2
  DTerm -> Sem r DTerm
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
TyProp (BOp -> Prim
PrimBOp BOp
b) DTerm
d1 DTerm
d2

-- t1 and t2 ==> {? t2 if t1, false otherwise ?}
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
TyProp BOp
op ATerm
t1 ATerm
t2
  | BOp
op BOp -> [BOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Eq, BOp
Neq, BOp
Lt, BOp
Gt, BOp
Leq, BOp
Geq, BOp
Divides] = 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
TyProp (BOp -> BOp
Should BOp
op) ATerm
t1 ATerm
t2
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)
-- 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 a. Eq a => a -> [a] -> 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 = Prim
PrimMin
  mergeOp Type
_ BOp
Diff = BOp -> Prim
PrimBOp BOp
SSub
  mergeOp (TySet Type
_) BOp
Union = Prim
PrimMax
  mergeOp (TyBag Type
_) BOp
Union = BOp -> Prim
PrimBOp BOp
Add
  mergeOp Type
_ BOp
_ = String -> Prim
forall a. HasCallStack => String -> a
error (String -> Prim) -> String -> Prim
forall a b. (a -> b) -> a -> b
$ String
"Impossible! mergeOp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BOp -> String
forall a. Show a => a -> String
show BOp
op

-- A ⊆ B  <==>  (A ⊔ B = B)
--   where ⊔ denotes 'merge max'.
--   Note it is NOT union, since this doesn't work for bags.
--   e.g.  bag [1] union bag [1,2] =  bag [1,1,2] /= bag [1,2].
desugarBinApp Type
_ BOp
Subset ATerm
t1 ATerm
t2 =
  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) Prim
PrimMax
          , 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 = String -> Sem r DTerm
forall a. HasCallStack => String -> a
error (String -> Sem r DTerm) -> String -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ String
"Impossible! desugarBinApp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BOp -> String
forall a. Show a => a -> String
show BOp
bop String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ATerm -> String
forall a. Show a => a -> String
show ATerm
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ATerm -> String
forall a. Show a => a -> String
show ATerm
t2

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

-- | Desugar a container comprehension.  First translate it into an
--   expanded ATerm and then recursively desugar that.
desugarComp :: Member Fresh r => Container -> ATerm -> Telescope AQual -> Sem r DTerm
desugarComp :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r DTerm
desugarComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs = Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs Sem r ATerm -> (ATerm -> Sem r DTerm) -> Sem r DTerm
forall a b. Sem r a -> (a -> Sem r b) -> Sem r b
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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope (Qual_ TY)
TelEmpty = ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 (Qual_ TY) (Telescope (Qual_ TY))
-> (Qual_ TY, Telescope (Qual_ TY))
forall p1 p2. (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind -> (Qual_ TY
q, Telescope (Qual_ TY)
qs))) =
  case Qual_ TY
q of
    -- [ t | x in l, qs ] = join (map (\x -> [t | qs]) l)
    AQBind Name ATerm
x (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
lst) -> do
      ATerm
tqs <- Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs
      let c :: Type -> Type
c = Container -> Type -> Type
containerTy Container
ctr
          tTy :: Type
tTy = 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
_ -> String -> Type
forall a. HasCallStack => String -> a
error String
"Impossible! Not a container in expandComp"
          joinTy :: Type
joinTy = Type -> Type
c (Type -> Type
c Type
tTy) Type -> Type -> Type
:->: Type -> Type
c Type
tTy
          mapTy :: Type
mapTy = (Type
xTy Type -> Type -> Type
:->: Type -> Type
c Type
tTy) Type -> Type -> Type
:*: Type -> Type
c Type
xTy Type -> Type -> Type
:->: Type -> Type
c (Type -> Type
c Type
tTy)
      ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 -> Bind [Pattern_ TY] ATerm -> ATerm
ATAbs Quantifier
Lam (Type
xTy Type -> Type -> Type
:->: Type -> Type
c Type
tTy) ([Pattern_ TY] -> ATerm -> Bind [Pattern_ TY] ATerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Type -> Name ATerm -> Pattern_ TY
APVar Type
xTy Name ATerm
x] ATerm
tqs))
                Embedded (Embed ATerm)
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 (Qual_ TY) -> Sem r ATerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope (Qual_ TY) -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope (Qual_ TY)
qs
      ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Binding_ TY] -> 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)) : [Binding_ TY]
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
forall a b. Coercible a b => a -> b
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
<$> [Binding_ TY] -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Binding_ TY] -> ATerm -> Sem r DTerm
desugarLet [Binding_ TY]
ls ATerm
t)
        )
    Sem r (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall a b. Sem r (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
forall a b. Coercible a b => a -> b
coerce Name ATerm
x) (Type -> [Name ATerm] -> DTerm
go Type
ty2 [Name ATerm]
xs))
  go Type
ty [Name ATerm]
as = String -> DTerm
forall a. HasCallStack => String -> a
error (String -> DTerm) -> String -> DTerm
forall a b. (a -> b) -> a -> b
$ String
"Impossible! mkLambda.go " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name ATerm] -> String
forall a. Show a => a -> String
show [Name ATerm]
as

mkQuant :: Quantifier -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkQuant :: Quantifier -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkQuant Quantifier
q [Type]
argtys [Name ATerm]
args DTerm
c = ((Name ATerm, Type) -> DTerm -> DTerm)
-> DTerm -> [(Name ATerm, Type)] -> DTerm
forall a b. (a -> b -> b) -> b -> [a] -> b
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
forall a b. Coercible a b => a -> b
coerce Name ATerm
x) DTerm
body)

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

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

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

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

-- | Desugar the list of guards in one branch of a case expression.
--   Pattern guards essentially remain as they are; boolean guards get
--   turned into pattern guards which match against @true@.
desugarGuards :: Member Fresh r => Telescope AGuard -> Sem r (Telescope DGuard)
desugarGuards :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Telescope AGuard -> Sem r (Telescope (Guard_ DS))
desugarGuards = ([[Guard_ DS]] -> Telescope (Guard_ DS))
-> Sem r [[Guard_ DS]] -> Sem r (Telescope (Guard_ DS))
forall a b. (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Guard_ DS] -> Telescope (Guard_ DS)
forall b. Alpha b => [b] -> Telescope b
toTelescope ([Guard_ DS] -> Telescope (Guard_ DS))
-> ([[Guard_ DS]] -> [Guard_ DS])
-> [[Guard_ DS]]
-> Telescope (Guard_ DS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Guard_ DS]] -> [Guard_ DS]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) (Sem r [[Guard_ DS]] -> Sem r (Telescope (Guard_ DS)))
-> (Telescope AGuard -> Sem r [[Guard_ DS]])
-> Telescope AGuard
-> Sem r (Telescope (Guard_ DS))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AGuard -> Sem r [Guard_ DS]) -> [AGuard] -> Sem r [[Guard_ DS]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM AGuard -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [Guard_ DS]
desugarGuard ([AGuard] -> Sem r [[Guard_ DS]])
-> (Telescope AGuard -> [AGuard])
-> Telescope AGuard
-> Sem r [[Guard_ DS]]
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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [Guard_ DS]
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 -> Pattern_ TY -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt (Type -> Side -> Pattern_ TY -> Pattern_ TY
APInj Type
TyBool Side
R Pattern_ TY
APUnit)

  -- 'let x = t' is desugared to 'when t is x'.
  desugarGuard (AGLet (ABinding Maybe (Embed PolyType)
_ Name ATerm
x (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 [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Name DTerm -> Sem r [Guard_ DS]
varMatch DTerm
dt (Name ATerm -> Name DTerm
forall a b. Coercible a b => a -> b
coerce Name ATerm
x)

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

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

    let eltTy :: Type
eltTy = Pattern_ TY -> Type
forall t. HasType t => t -> Type
getType Pattern_ TY
p1
        unrolledTy :: Type
unrolledTy = Type
eltTy Type -> Type -> Type
:*: Type
ty
    ([[Guard_ DS]] -> [Guard_ DS])
-> Sem r [[Guard_ DS]] -> Sem r [Guard_ DS]
forall a b. (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Guard_ DS]] -> [Guard_ DS]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Sem r [[Guard_ DS]] -> Sem r [Guard_ DS])
-> ([Sem r [Guard_ DS]] -> Sem r [[Guard_ DS]])
-> [Sem r [Guard_ DS]]
-> Sem r [Guard_ DS]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r [Guard_ DS]] -> Sem r [[Guard_ DS]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Sem r [Guard_ DS]] -> Sem r [Guard_ DS])
-> [Sem r [Guard_ DS]] -> Sem r [Guard_ DS]
forall a b. (a -> b) -> a -> b
$
      [ DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch DTerm
dt (Type -> Side -> Name DTerm -> Pattern_ DS
DPInj Type
ty Side
R Name DTerm
y)
      , DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch (Type -> Name DTerm -> DTerm
dtVar Type
unrolledTy Name DTerm
y) (Type -> Name DTerm -> Name DTerm -> Pattern_ DS
DPPair Type
unrolledTy Name DTerm
x1 Name DTerm
x2)
      , [Guard_ DS] -> Sem r [Guard_ DS]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [Guard_ DS]
gs1
      , [Guard_ DS] -> Sem r [Guard_ DS]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [Guard_ DS]
gs2
      ]
  desugarMatch DTerm
dt (APList Type
ty []) = DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt (Type -> Side -> Pattern_ TY -> Pattern_ TY
APInj Type
ty Side
L Pattern_ TY
APUnit)
  desugarMatch DTerm
dt (APList Type
ty [Pattern_ TY]
ps) =
    DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
dt (Pattern_ TY -> Sem r [Guard_ DS])
-> Pattern_ TY -> Sem r [Guard_ DS]
forall a b. (a -> b) -> a -> b
$ (Pattern_ TY -> Pattern_ TY -> Pattern_ TY)
-> Pattern_ TY -> [Pattern_ TY] -> Pattern_ TY
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Pattern_ TY -> Pattern_ TY -> Pattern_ TY
APCons Type
ty) (Type -> [Pattern_ TY] -> Pattern_ TY
APList Type
ty []) [Pattern_ TY]
ps
  -- when dt is (p + t) ==> when dt is x0; let v = t; [if x0 >= v]; when x0-v is p
  desugarMatch DTerm
dt (APAdd Type
ty Side
_ Pattern_ TY
p ATerm
t) = (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
posRestrict ATerm -> ATerm -> ATerm
(-.) DTerm
dt Type
ty Pattern_ TY
p ATerm
t
   where
    posRestrict :: Type -> Maybe (ATerm -> ATerm -> ATerm)
posRestrict Type
plusty
      | Type
plusty Type -> [Type] -> Bool
forall a. Eq a => a -> [a] -> 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
_ Pattern_ TY
p ATerm
t) = (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
intRestrict ATerm -> ATerm -> ATerm
(/.) DTerm
dt Type
ty Pattern_ TY
p ATerm
t
   where
    intRestrict :: Type -> Maybe (ATerm -> ATerm -> ATerm)
intRestrict Type
plusty
      | Type
plusty Type -> [Type] -> Bool
forall a. Eq a => a -> [a] -> 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 Pattern_ TY
p ATerm
t) = (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> Pattern_ TY
-> ATerm
-> Sem r [Guard_ DS]
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 Pattern_ TY
p ATerm
t
  -- when dt is (p/q) ==> when $frac(dt) is (p, q)
  desugarMatch DTerm
dt (APFrac Type
_ Pattern_ TY
p Pattern_ TY
q) =
    DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch
      (DTerm -> DTerm -> DTerm
dtapp (Type -> Prim -> DTerm
DTPrim (Type
TyQ Type -> Type -> Type
:->: Type
TyZ Type -> Type -> Type
:*: Type
TyN) Prim
PrimFrac) DTerm
dt)
      (Type -> [Pattern_ TY] -> Pattern_ TY
APTup (Type
TyZ Type -> Type -> Type
:*: Type
TyN) [Pattern_ TY
p, Pattern_ TY
q])
  -- when dt is (-p) ==> when dt is x0; if x0 < 0; when -x0 is p
  desugarMatch DTerm
dt (APNeg Type
ty Pattern_ TY
p) = do
    -- when dt is x0
    (Name DTerm
x0, [Guard_ DS]
g1) <- DTerm -> Sem r (Name DTerm, [Guard_ DS])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [Guard_ DS])
varFor DTerm
dt

    -- if x0 < 0
    [Guard_ DS]
g2 <- AGuard -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [Guard_ DS]
desugarGuard (AGuard -> Sem r [Guard_ DS]) -> AGuard -> Sem r [Guard_ DS]
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
forall a b. Coercible a b => a -> b
coerce Name DTerm
x0) ATerm -> ATerm -> ATerm
<. Type -> Integer -> ATerm
ATNat Type
ty Integer
0))

    -- when -x0 is p
    DTerm
neg <- 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
forall a b. Coercible a b => a -> b
coerce Name DTerm
x0))
    [Guard_ DS]
g3 <- DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
neg Pattern_ TY
p

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

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

  varMatch :: Member Fresh r => DTerm -> Name DTerm -> Sem r [DGuard]
  varMatch :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Name DTerm -> Sem r [Guard_ DS]
varMatch DTerm
dt Name DTerm
x = DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ DS -> Sem r [Guard_ DS]
mkMatch DTerm
dt (Type -> Name DTerm -> Pattern_ DS
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 :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [Guard_ DS])
varFor (DTVar Type
_ (QName NameProvenance
_ Name DTerm
x)) = (Name DTerm, [Guard_ DS]) -> Sem r (Name DTerm, [Guard_ DS])
forall a. a -> Sem r a
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 (String -> Name DTerm
forall a. String -> Name a
string2Name String
"x")
    [Guard_ DS]
g <- DTerm -> Name DTerm -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Name DTerm -> Sem r [Guard_ DS]
varMatch DTerm
dt Name DTerm
x
    (Name DTerm, [Guard_ DS]) -> Sem r (Name DTerm, [Guard_ DS])
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name DTerm
x, [Guard_ DS]
g)

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

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

    [Guard_ DS]
g3 <- case Type -> Maybe (ATerm -> ATerm -> ATerm)
restrict Type
ty of
      Maybe (ATerm -> ATerm -> ATerm)
Nothing -> [Guard_ DS] -> Sem r [Guard_ DS]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      -- if x0 `cmp` v
      Just ATerm -> ATerm -> ATerm
cmp ->
        AGuard -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [Guard_ DS]
desugarGuard (AGuard -> Sem r [Guard_ DS]) -> AGuard -> Sem r [Guard_ DS]
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
forall a b. Coercible a b => a -> b
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
forall a b. Coercible a b => a -> b
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
forall a b. Coercible a b => a -> b
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
forall a b. Coercible a b => a -> b
coerce Name DTerm
v))
    [Guard_ DS]
g4 <- DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Pattern_ TY -> Sem r [Guard_ DS]
desugarMatch DTerm
inv Pattern_ TY
p

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

-- | Desugar a container literal such as @[1,2,3]@ or @{1,2,3}@.
desugarContainer :: Member Fresh r => Type -> Container -> [(ATerm, Maybe ATerm)] -> Maybe (Ellipsis ATerm) -> Sem r DTerm
-- Literal list containers desugar to nested applications of cons.
desugarContainer :: forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer Type
ty Container
ListContainer [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
Nothing =
  (DTerm -> DTerm -> DTerm) -> DTerm -> [DTerm] -> DTerm
forall a b. (a -> b -> b) -> b -> [a] -> b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a b. Sem r (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
_ -> String -> (Prim, Type)
forall a. HasCallStack => String -> a
error (String -> (Prim, Type)) -> String -> (Prim, Type)
forall a b. (a -> b) -> a -> b
$ String
"Impossible! Non-container type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in desugarContainer"