module Disco.Desugar
(
runDesugar
, desugarDefn, desugarTerm, desugarProperty
, desugarBranch, desugarGuards
)
where
import Control.Monad.Cont
import Data.Bool (bool)
import Data.Coerce
import Data.Maybe (fromMaybe, isJust)
import Disco.AST.Desugared
import Disco.AST.Surface
import Disco.AST.Typed
import Disco.Module
import Disco.Names
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Typecheck (containerTy)
import Disco.Types
import Disco.Effects.Fresh
import Polysemy (Member, Sem, run)
import Unbound.Generics.LocallyNameless (Bind, Name, bind,
embed, name2String,
string2Name, unembed,
unrebind)
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)
runDesugar :: Sem '[Fresh] a -> a
runDesugar :: Sem '[Fresh] a -> a
runDesugar = Sem '[] a -> a
forall a. Sem '[] a -> a
run (Sem '[] a -> a)
-> (Sem '[Fresh] a -> Sem '[] a) -> Sem '[Fresh] a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem '[Fresh] a -> Sem '[] a
forall (r :: [(* -> *) -> * -> *]) a. Sem (Fresh : r) a -> Sem r a
runFresh1
atVar :: Type -> Name ATerm -> ATerm
atVar :: Type -> Name ATerm -> ATerm
atVar Type
ty Name ATerm
x = Type -> QName ATerm -> ATerm
ATVar Type
ty (NameProvenance -> Name ATerm -> QName ATerm
forall a. NameProvenance -> Name a -> QName a
QName NameProvenance
LocalName Name ATerm
x)
tapp :: ATerm -> ATerm -> ATerm
tapp :: ATerm -> ATerm -> ATerm
tapp ATerm
t1 ATerm
t2 = Type -> ATerm -> ATerm -> ATerm
ATApp Type
resTy ATerm
t1 ATerm
t2
where
resTy :: Type
resTy = case ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t1 of
(Type
_ :->: Type
r) -> Type
r
Type
ty -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! Got non-function type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in tapp"
mkBin :: Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin :: Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
resTy BOp
bop ATerm
t1 ATerm
t2
= ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t1 Type -> Type -> Type
:*: ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t2 Type -> Type -> Type
:->: Type
resTy) (BOp -> Prim
PrimBOp BOp
bop)) (ATerm -> ATerm -> ATerm
mkPair ATerm
t1 ATerm
t2)
mkUn :: Type -> UOp -> ATerm -> ATerm
mkUn :: Type -> UOp -> ATerm -> ATerm
mkUn Type
resTy UOp
uop ATerm
t = ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t Type -> Type -> Type
:->: Type
resTy) (UOp -> Prim
PrimUOp UOp
uop)) ATerm
t
mkPair :: ATerm -> ATerm -> ATerm
mkPair :: ATerm -> ATerm -> ATerm
mkPair ATerm
t1 ATerm
t2 = [ATerm] -> ATerm
mkTup [ATerm
t1,ATerm
t2]
mkTup :: [ATerm] -> ATerm
mkTup :: [ATerm] -> ATerm
mkTup [ATerm]
ts = Type -> [ATerm] -> ATerm
ATTup ((Type -> Type -> Type) -> [Type] -> Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
(:*:) ((ATerm -> Type) -> [ATerm] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ATerm -> Type
forall t. HasType t => t -> Type
getType [ATerm]
ts)) [ATerm]
ts
tapps :: ATerm -> [ATerm] -> ATerm
tapps :: ATerm -> [ATerm] -> ATerm
tapps ATerm
t [ATerm]
ts = ATerm -> ATerm -> ATerm
tapp ATerm
t ([ATerm] -> ATerm
mkTup [ATerm]
ts)
infixr 2 ||.
(||.) :: ATerm -> ATerm -> ATerm
||. :: ATerm -> ATerm -> ATerm
(||.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Or
infixl 6 -., +.
(-.) :: ATerm -> ATerm -> ATerm
ATerm
at1 -. :: ATerm -> ATerm -> ATerm
-. ATerm
at2 = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at1) BOp
Sub ATerm
at1 ATerm
at2
(+.) :: ATerm -> ATerm -> ATerm
ATerm
at1 +. :: ATerm -> ATerm -> ATerm
+. ATerm
at2 = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at1) BOp
Add ATerm
at1 ATerm
at2
infixl 7 /.
(/.) :: ATerm -> ATerm -> ATerm
ATerm
at1 /. :: ATerm -> ATerm -> ATerm
/. ATerm
at2 = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at1) BOp
Div ATerm
at1 ATerm
at2
infix 4 <., >=.
(<.) :: ATerm -> ATerm -> ATerm
<. :: ATerm -> ATerm -> ATerm
(<.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Lt
(>=.) :: ATerm -> ATerm -> ATerm
>=. :: ATerm -> ATerm -> ATerm
(>=.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Geq
(|.) :: ATerm -> ATerm -> ATerm
|. :: ATerm -> ATerm -> ATerm
(|.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Divides
infix 4 ==.
(==.) :: ATerm -> ATerm -> ATerm
==. :: ATerm -> ATerm -> ATerm
(==.) = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
Eq
tnot :: ATerm -> ATerm
tnot :: ATerm -> ATerm
tnot = ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim (Type
TyBool Type -> Type -> Type
:->: Type
TyBool) (UOp -> Prim
PrimUOp UOp
Not))
(<==.) :: ATerm -> [AGuard] -> ABranch
ATerm
t <==. :: ATerm -> [AGuard] -> ABranch
<==. [AGuard]
gs = Telescope AGuard -> ATerm -> ABranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([AGuard] -> Telescope AGuard
forall b. Alpha b => [b] -> Telescope b
toTelescope [AGuard]
gs) ATerm
t
fls :: ATerm
fls :: ATerm
fls = Type -> Bool -> ATerm
ATBool Type
TyBool Bool
False
tru :: ATerm
tru :: ATerm
tru = Type -> Bool -> ATerm
ATBool Type
TyBool Bool
True
tif :: ATerm -> AGuard
tif :: ATerm -> AGuard
tif ATerm
t = Embed ATerm -> AGuard
AGBool (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
ATerm
t)
ctrNil :: Container -> Type -> ATerm
ctrNil :: Container -> Type -> ATerm
ctrNil Container
ctr Type
ty = Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> ATerm
ATContainer (Container -> Type -> Type
containerTy Container
ctr Type
ty) Container
ctr [] Maybe (Ellipsis ATerm)
forall a. Maybe a
Nothing
ctrSingleton :: Container -> ATerm -> ATerm
ctrSingleton :: Container -> ATerm -> ATerm
ctrSingleton Container
ctr ATerm
t = Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> ATerm
ATContainer (Container -> Type -> Type
containerTy Container
ctr (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t)) Container
ctr [(ATerm
t, Maybe ATerm
forall a. Maybe a
Nothing)] Maybe (Ellipsis ATerm)
forall a. Maybe a
Nothing
dtVar :: Type -> Name DTerm -> DTerm
dtVar :: Type -> Name DTerm -> DTerm
dtVar Type
ty Name DTerm
x = Type -> QName DTerm -> DTerm
DTVar Type
ty (NameProvenance -> Name DTerm -> QName DTerm
forall a. NameProvenance -> Name a -> QName a
QName NameProvenance
LocalName Name DTerm
x)
dtapp :: DTerm -> DTerm -> DTerm
dtapp :: DTerm -> DTerm -> DTerm
dtapp DTerm
t1 DTerm
t2 = Type -> DTerm -> DTerm -> DTerm
DTApp Type
resTy DTerm
t1 DTerm
t2
where
resTy :: Type
resTy = case DTerm -> Type
forall t. HasType t => t -> Type
getType DTerm
t1 of
(Type
_ :->: Type
r) -> Type
r
Type
ty -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! Got non-function type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in dtapp"
dtbin :: Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin :: Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
resTy Prim
p DTerm
dt1 DTerm
dt2
= DTerm -> DTerm -> DTerm
dtapp (Type -> Prim -> DTerm
DTPrim (DTerm -> Type
forall t. HasType t => t -> Type
getType DTerm
dt1 Type -> Type -> Type
:*: DTerm -> Type
forall t. HasType t => t -> Type
getType DTerm
dt2 Type -> Type -> Type
:->: Type
resTy) Prim
p) (DTerm -> DTerm -> DTerm
mkDTPair DTerm
dt1 DTerm
dt2)
mkDTPair :: DTerm -> DTerm -> DTerm
mkDTPair :: DTerm -> DTerm -> DTerm
mkDTPair DTerm
dt1 DTerm
dt2 = Type -> DTerm -> DTerm -> DTerm
DTPair (DTerm -> Type
forall t. HasType t => t -> Type
getType DTerm
dt1 Type -> Type -> Type
:*: DTerm -> Type
forall t. HasType t => t -> Type
getType DTerm
dt2) DTerm
dt1 DTerm
dt2
desugarDefn :: Member Fresh r => Defn -> Sem r DTerm
desugarDefn :: Defn -> Sem r DTerm
desugarDefn (Defn Name ATerm
_ [Type]
patTys Type
bodyTy [Clause]
def) =
Quantifier -> Type -> [Clause] -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Quantifier -> Type -> [Clause] -> Sem r DTerm
desugarAbs Quantifier
Lam ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(:->:) Type
bodyTy [Type]
patTys) [Clause]
def
desugarAbs :: Member Fresh r => Quantifier -> Type -> [Clause] -> Sem r DTerm
desugarAbs :: Quantifier -> Type -> [Clause] -> Sem r DTerm
desugarAbs Quantifier
Lam Type
ty [cl :: Clause
cl@(Clause -> ([APattern], ATerm)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> ([APVar Type
_ Name ATerm
_], ATerm
_))] = do
([APattern]
ps, ATerm
at) <- Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Clause
cl
DTerm
d <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
at
DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
Lam Type
ty (Name DTerm -> DTerm -> Bind (Name DTerm) DTerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (APattern -> Name DTerm
forall b. Coercible b (Name ATerm) => APattern -> b
getVar ([APattern] -> APattern
forall a. [a] -> a
head [APattern]
ps)) DTerm
d)
where
getVar :: APattern -> b
getVar (APVar Type
_ Name ATerm
x) = Name ATerm -> b
coerce Name ATerm
x
desugarAbs Quantifier
quant Type
overallTy [Clause]
body = do
[([APattern], ATerm)]
clausePairs <- [Clause] -> Sem r [([APattern], ATerm)]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[Clause] -> Sem r [([APattern], ATerm)]
unbindClauses [Clause]
body
let ([[APattern]]
pats, [ATerm]
bodies) = [([APattern], ATerm)] -> ([[APattern]], [ATerm])
forall a b. [(a, b)] -> ([a], [b])
unzip [([APattern], ATerm)]
clausePairs
let patTys :: [Type]
patTys = (APattern -> Type) -> [APattern] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map APattern -> Type
forall t. HasType t => t -> Type
getType ([[APattern]] -> [APattern]
forall a. [a] -> a
head [[APattern]]
pats)
let bodyTy :: Type
bodyTy = ATerm -> Type
forall t. HasType t => t -> Type
getType ([ATerm] -> ATerm
forall a. [a] -> a
head [ATerm]
bodies)
[Name ATerm]
args <- (APattern -> Int -> Sem r (Name ATerm))
-> [APattern] -> [Int] -> Sem r [Name ATerm]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\APattern
_ Int
i -> Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name ([Char]
"arg" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i))) ([[APattern]] -> [APattern]
forall a. [a] -> a
head [[APattern]]
pats) [Int
0 :: Int ..]
let branches :: [ABranch]
branches = (ATerm -> [APattern] -> ABranch)
-> [ATerm] -> [[APattern]] -> [ABranch]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ([(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch
mkBranch ([Name ATerm] -> [Type] -> [(Name ATerm, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name ATerm]
args [Type]
patTys)) [ATerm]
bodies [[APattern]]
pats
DTerm
dcase <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> [ABranch] -> ATerm
ATCase Type
bodyTy [ABranch]
branches
DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Quantifier -> Type -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkAbs Quantifier
quant Type
overallTy [Type]
patTys ([Name ATerm] -> [Name ATerm]
coerce [Name ATerm]
args) DTerm
dcase
where
mkBranch :: [(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch
mkBranch :: [(Name ATerm, Type)] -> ATerm -> [APattern] -> ABranch
mkBranch [(Name ATerm, Type)]
xs ATerm
b [APattern]
ps = Telescope AGuard -> ATerm -> ABranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([(Name ATerm, Type)] -> [APattern] -> Telescope AGuard
mkGuards [(Name ATerm, Type)]
xs [APattern]
ps) ATerm
b
mkGuards :: [(Name ATerm, Type)] -> [APattern] -> Telescope AGuard
mkGuards :: [(Name ATerm, Type)] -> [APattern] -> Telescope AGuard
mkGuards [(Name ATerm, Type)]
xs [APattern]
ps = [AGuard] -> Telescope AGuard
forall b. Alpha b => [b] -> Telescope b
toTelescope ([AGuard] -> Telescope AGuard) -> [AGuard] -> Telescope AGuard
forall a b. (a -> b) -> a -> b
$ (Embed ATerm -> APattern -> AGuard)
-> [Embed ATerm] -> [APattern] -> [AGuard]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Embed ATerm -> APattern -> AGuard
AGPat (((Name ATerm, Type) -> Embed ATerm)
-> [(Name ATerm, Type)] -> [Embed ATerm]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name ATerm
x,Type
ty) -> Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name ATerm -> ATerm
atVar Type
ty Name ATerm
x)) [(Name ATerm, Type)]
xs) [APattern]
ps
unbindClauses :: Member Fresh r => [Clause] -> Sem r [([APattern], ATerm)]
unbindClauses :: [Clause] -> Sem r [([APattern], ATerm)]
unbindClauses [Clause
c] | Quantifier
quant Quantifier -> [Quantifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Quantifier
All, Quantifier
Ex] = do
([APattern]
ps, ATerm
t) <- Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Clause -> Sem r ([APattern], ATerm)
liftClause Clause
c
[([APattern], ATerm)] -> Sem r [([APattern], ATerm)]
forall (m :: * -> *) a. Monad m => a -> m a
return [([APattern]
ps, [APattern] -> ATerm -> ATerm
addDbgInfo [APattern]
ps ATerm
t)]
unbindClauses [Clause]
cs = (Clause -> Sem r ([APattern], ATerm))
-> [Clause] -> Sem r [([APattern], ATerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind [Clause]
cs
liftClause :: Member Fresh r => Bind [APattern] ATerm -> Sem r ([APattern], ATerm)
liftClause :: Clause -> Sem r ([APattern], ATerm)
liftClause Clause
c = Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Clause
c Sem r ([APattern], ATerm)
-> (([APattern], ATerm) -> Sem r ([APattern], ATerm))
-> Sem r ([APattern], ATerm)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
([APattern]
ps, ATAbs Quantifier
q Type
_ Clause
c') | Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
quant -> do
([APattern]
ps', ATerm
b) <- Clause -> Sem r ([APattern], ATerm)
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Clause -> Sem r ([APattern], ATerm)
liftClause Clause
c'
([APattern], ATerm) -> Sem r ([APattern], ATerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ([APattern]
ps [APattern] -> [APattern] -> [APattern]
forall a. [a] -> [a] -> [a]
++ [APattern]
ps', ATerm
b)
([APattern]
ps, ATerm
b) -> ([APattern], ATerm) -> Sem r ([APattern], ATerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ([APattern]
ps, ATerm
b)
addDbgInfo :: [APattern] -> ATerm -> ATerm
addDbgInfo :: [APattern] -> ATerm -> ATerm
addDbgInfo [APattern]
ps ATerm
t = [([Char], Type, Name ATerm)] -> ATerm -> ATerm
ATTest (((Name ATerm, Type) -> ([Char], Type, Name ATerm))
-> [(Name ATerm, Type)] -> [([Char], Type, Name ATerm)]
forall a b. (a -> b) -> [a] -> [b]
map (Name ATerm, Type) -> ([Char], Type, Name ATerm)
forall a b. (Name a, b) -> ([Char], b, Name a)
withName ([(Name ATerm, Type)] -> [([Char], Type, Name ATerm)])
-> [(Name ATerm, Type)] -> [([Char], Type, Name ATerm)]
forall a b. (a -> b) -> a -> b
$ (APattern -> [(Name ATerm, Type)])
-> [APattern] -> [(Name ATerm, Type)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap APattern -> [(Name ATerm, Type)]
varsBound [APattern]
ps) ATerm
t
where withName :: (Name a, b) -> ([Char], b, Name a)
withName (Name a
n, b
ty) = (Name a -> [Char]
forall a. Name a -> [Char]
name2String Name a
n, b
ty, Name a
n)
desugarCList2B :: Member Fresh r => Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B :: Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B Prim
p Type
ty Type
cts Type
b = do
Name ATerm
c <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"c")
DTerm
body <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim (Type -> Type
TyBag Type
cts Type -> Type -> Type
:->: Type -> Type
TyBag Type
b) Prim
p)
(ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim (Type -> Type
TyList Type
cts Type -> Type -> Type
:->: Type -> Type
TyBag Type
cts) Prim
PrimBag)
(Type -> Name ATerm -> ATerm
atVar (Type -> Type
TyList Type
cts) Name ATerm
c)
)
DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda Type
ty [Name ATerm
c] DTerm
body
desugarTerm :: Member Fresh r => ATerm -> Sem r DTerm
desugarTerm :: ATerm -> Sem r DTerm
desugarTerm (ATVar Type
ty QName ATerm
x) = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> QName DTerm -> DTerm
DTVar Type
ty (QName ATerm -> QName DTerm
coerce QName ATerm
x)
desugarTerm (ATPrim (Type
ty1 :->: Type
resTy) (PrimUOp UOp
uop))
| Type -> Type -> UOp -> Bool
uopDesugars Type
ty1 Type
resTy UOp
uop = Type -> Type -> UOp -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp Type
ty1 Type
resTy UOp
uop
desugarTerm (ATPrim (Type
ty1 :*: Type
ty2 :->: Type
resTy) (PrimBOp BOp
bop))
| Type -> Type -> Type -> BOp -> Bool
bopDesugars Type
ty1 Type
ty2 Type
resTy BOp
bop = Type -> Type -> Type -> BOp -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> Type -> Type -> BOp -> Sem r DTerm
desugarPrimBOp Type
ty1 Type
ty2 Type
resTy BOp
bop
desugarTerm (ATPrim ty :: Type
ty@(TyList Type
cts :->: TyBag Type
b) Prim
PrimC2B) = Prim -> Type -> Type -> Type -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B Prim
PrimC2B Type
ty Type
cts Type
b
desugarTerm (ATPrim ty :: Type
ty@(TyList Type
cts :->: TyBag Type
b) Prim
PrimUC2B) = Prim -> Type -> Type -> Type -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Prim -> Type -> Type -> Type -> Sem r DTerm
desugarCList2B Prim
PrimUC2B Type
ty Type
cts Type
b
desugarTerm (ATPrim Type
ty Prim
x) = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> Prim -> DTerm
DTPrim Type
ty Prim
x
desugarTerm ATerm
ATUnit = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return DTerm
DTUnit
desugarTerm (ATBool Type
ty Bool
b) = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> Bool -> DTerm
DTBool Type
ty Bool
b
desugarTerm (ATChar Char
c) = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Char -> DTerm
DTChar Char
c
desugarTerm (ATString [Char]
cs) =
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer (Type -> Type
TyList Type
TyC) Container
ListContainer ((Char -> (ATerm, Maybe ATerm)) -> [Char] -> [(ATerm, Maybe ATerm)]
forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> (Char -> ATerm
ATChar Char
c, Maybe ATerm
forall a. Maybe a
Nothing)) [Char]
cs) Maybe (Ellipsis ATerm)
forall a. Maybe a
Nothing
desugarTerm (ATAbs Quantifier
q Type
ty Clause
lam) = Quantifier -> Type -> [Clause] -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Quantifier -> Type -> [Clause] -> Sem r DTerm
desugarAbs Quantifier
q Type
ty [Clause
lam]
desugarTerm (ATApp Type
resTy (ATPrim Type
_ (PrimUOp UOp
uop)) ATerm
t)
| Type -> Type -> UOp -> Bool
uopDesugars (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t) Type
resTy UOp
uop = Type -> UOp -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> UOp -> ATerm -> Sem r DTerm
desugarUnApp Type
resTy UOp
uop ATerm
t
desugarTerm (ATApp Type
resTy (ATPrim Type
_ (PrimBOp BOp
bop)) (ATTup Type
_ [ATerm
t1,ATerm
t2]))
| Type -> Type -> Type -> BOp -> Bool
bopDesugars (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t1) (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t2) Type
resTy BOp
bop = Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
desugarBinApp Type
resTy BOp
bop ATerm
t1 ATerm
t2
desugarTerm (ATApp Type
ty ATerm
t1 ATerm
t2) =
Type -> DTerm -> DTerm -> DTerm
DTApp Type
ty (DTerm -> DTerm -> DTerm) -> Sem r DTerm -> Sem r (DTerm -> DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t1 Sem r (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t2
desugarTerm (ATTup Type
ty [ATerm]
ts) = Type -> [ATerm] -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> [ATerm] -> Sem r DTerm
desugarTuples Type
ty [ATerm]
ts
desugarTerm (ATNat Type
ty Integer
n) = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> Integer -> DTerm
DTNat Type
ty Integer
n
desugarTerm (ATRat Rational
r) = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Rational -> DTerm
DTRat Rational
r
desugarTerm (ATTyOp Type
ty TyOp
op Type
t) = DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> TyOp -> Type -> DTerm
DTTyOp Type
ty TyOp
op Type
t
desugarTerm (ATChain Type
_ ATerm
t1 [ALink]
links) = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ ATerm -> [ALink] -> ATerm
expandChain ATerm
t1 [ALink]
links
desugarTerm (ATContainer Type
ty Container
c [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell) = Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer Type
ty Container
c [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell
desugarTerm (ATContainerComp Type
_ Container
ctr Bind (Telescope AQual) ATerm
bqt) = do
(Telescope AQual
qs, ATerm
t) <- Bind (Telescope AQual) ATerm -> Sem r (Telescope AQual, ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope AQual) ATerm
bqt
Container -> ATerm -> Telescope AQual -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope AQual -> Sem r DTerm
desugarComp Container
ctr ATerm
t Telescope AQual
qs
desugarTerm (ATLet Type
_ Bind (Telescope ABinding) ATerm
t) = do
(Telescope ABinding
bs, ATerm
t2) <- Bind (Telescope ABinding) ATerm
-> Sem r (Telescope ABinding, ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope ABinding) ATerm
t
[ABinding] -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[ABinding] -> ATerm -> Sem r DTerm
desugarLet (Telescope ABinding -> [ABinding]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope ABinding
bs) ATerm
t2
desugarTerm (ATCase Type
ty [ABranch]
bs) = Type -> [DBranch] -> DTerm
DTCase Type
ty ([DBranch] -> DTerm) -> Sem r [DBranch] -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ABranch -> Sem r DBranch) -> [ABranch] -> Sem r [DBranch]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ABranch -> Sem r DBranch
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ABranch -> Sem r DBranch
desugarBranch [ABranch]
bs
desugarTerm (ATTest [([Char], Type, Name ATerm)]
info ATerm
t) = [([Char], Type, Name DTerm)] -> DTerm -> DTerm
DTTest ([([Char], Type, Name ATerm)] -> [([Char], Type, Name DTerm)]
coerce [([Char], Type, Name ATerm)]
info) (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
desugarProperty :: Member Fresh r => AProperty -> Sem r DTerm
desugarProperty :: ATerm -> Sem r DTerm
desugarProperty ATerm
p = [([Char], Type, Name DTerm)] -> DTerm -> DTerm
DTTest [] (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
p
uopDesugars :: Type -> Type -> UOp -> Bool
uopDesugars :: Type -> Type -> UOp -> Bool
uopDesugars Type
_ Type
_ UOp
uop = UOp
uop UOp -> UOp -> Bool
forall a. Eq a => a -> a -> Bool
== UOp
Not
desugarPrimUOp :: Member Fresh r => Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp :: Type -> Type -> UOp -> Sem r DTerm
desugarPrimUOp Type
argTy Type
resTy UOp
op = do
Name ATerm
x <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"arg")
DTerm
body <- Type -> UOp -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> UOp -> ATerm -> Sem r DTerm
desugarUnApp Type
resTy UOp
op (Type -> Name ATerm -> ATerm
atVar Type
argTy Name ATerm
x)
DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda (Type
argTy Type -> Type -> Type
:->: Type
resTy) [Name ATerm
x] DTerm
body
bopDesugars :: Type -> Type -> Type -> BOp -> Bool
bopDesugars :: Type -> Type -> Type -> BOp -> Bool
bopDesugars Type
_ Type
TyN Type
_ BOp
Choose = Bool
True
bopDesugars Type
_ Type
_ Type
_ BOp
bop = BOp
bop BOp -> [BOp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`
[ BOp
And, BOp
Or, BOp
Impl, BOp
Iff
, BOp
Neq, BOp
Gt, BOp
Leq, BOp
Geq, BOp
Min, BOp
Max
, BOp
IDiv
, BOp
Sub, BOp
SSub
, BOp
Inter, BOp
Diff, BOp
Union, BOp
Subset
]
desugarPrimBOp :: Member Fresh r => Type -> Type -> Type -> BOp -> Sem r DTerm
desugarPrimBOp :: Type -> Type -> Type -> BOp -> Sem r DTerm
desugarPrimBOp Type
ty1 Type
ty2 Type
resTy BOp
op = do
Name ATerm
p <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"pair1")
Name ATerm
x <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"arg1")
Name ATerm
y <- Name ATerm -> Sem r (Name ATerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name ATerm
forall a. [Char] -> Name a
string2Name [Char]
"arg2")
let argsTy :: Type
argsTy = Type
ty1 Type -> Type -> Type
:*: Type
ty2
DTerm
body <- Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
desugarBinApp Type
resTy BOp
op (Type -> Name ATerm -> ATerm
atVar Type
ty1 Name ATerm
x) (Type -> Name ATerm -> ATerm
atVar Type
ty2 Name ATerm
y)
DTerm -> Sem r DTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (DTerm -> Sem r DTerm) -> DTerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda (Type
argsTy Type -> Type -> Type
:->: Type
resTy) [Name ATerm
p] (DTerm -> DTerm) -> DTerm -> DTerm
forall a b. (a -> b) -> a -> b
$
Type -> [DBranch] -> DTerm
DTCase Type
resTy
[ Telescope DGuard -> DTerm -> DBranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind
([DGuard] -> Telescope DGuard
forall b. Alpha b => [b] -> Telescope b
toTelescope [Embed DTerm -> DPattern -> DGuard
DGPat (Embedded (Embed DTerm) -> Embed DTerm
forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name DTerm -> DTerm
dtVar Type
argsTy (Name ATerm -> Name DTerm
coerce Name ATerm
p))) (Type -> Name DTerm -> Name DTerm -> DPattern
DPPair Type
argsTy (Name ATerm -> Name DTerm
coerce Name ATerm
x) (Name ATerm -> Name DTerm
coerce Name ATerm
y))])
DTerm
body
]
desugarUnApp :: Member Fresh r => Type -> UOp -> ATerm -> Sem r DTerm
desugarUnApp :: Type -> UOp -> ATerm -> Sem r DTerm
desugarUnApp Type
_ UOp
Not ATerm
t = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
Type -> [ABranch] -> ATerm
ATCase Type
TyBool
[ ATerm
fls ATerm -> [AGuard] -> ABranch
<==. [Embed ATerm -> AGuard
AGBool (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
ATerm
t)]
, ATerm
tru ATerm -> [AGuard] -> ABranch
<==. []
]
desugarUnApp Type
ty UOp
uop ATerm
t = [Char] -> Sem r DTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> Sem r DTerm) -> [Char] -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! desugarUnApp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ UOp -> [Char]
forall a. Show a => a -> [Char]
show UOp
uop [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ATerm -> [Char]
forall a. Show a => a -> [Char]
show ATerm
t
desugarBinApp :: Member Fresh r => Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
desugarBinApp :: Type -> BOp -> ATerm -> ATerm -> Sem r DTerm
desugarBinApp Type
_ BOp
And ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
Type -> [ABranch] -> ATerm
ATCase Type
TyBool
[ ATerm
t2 ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif ATerm
t1]
, ATerm
fls ATerm -> [AGuard] -> ABranch
<==. []
]
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
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
desugarBinApp Type
_ BOp
Or ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
Type -> [ABranch] -> ATerm
ATCase Type
TyBool
[ ATerm
tru ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif ATerm
t1]
, ATerm
t2 ATerm -> [AGuard] -> ABranch
<==. []
]
desugarBinApp Type
_ BOp
Neq ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ ATerm -> ATerm
tnot (ATerm
t1 ATerm -> ATerm -> ATerm
==. ATerm
t2)
desugarBinApp Type
_ BOp
Gt ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ ATerm
t2 ATerm -> ATerm -> ATerm
<. ATerm
t1
desugarBinApp Type
_ BOp
Leq ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ ATerm -> ATerm
tnot (ATerm
t2 ATerm -> ATerm -> ATerm
<. ATerm
t1)
desugarBinApp Type
_ BOp
Geq ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ ATerm -> ATerm
tnot (ATerm
t1 ATerm -> ATerm -> ATerm
<. ATerm
t2)
desugarBinApp Type
ty BOp
Min ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
Type -> [ABranch] -> ATerm
ATCase Type
ty
[ ATerm
t1 ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif (ATerm
t1 ATerm -> ATerm -> ATerm
<. ATerm
t2)]
, ATerm
t2 ATerm -> [AGuard] -> ABranch
<==. []
]
desugarBinApp Type
ty BOp
Max ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
Type -> [ABranch] -> ATerm
ATCase Type
ty
[ ATerm
t1 ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif (ATerm
t2 ATerm -> ATerm -> ATerm
<. ATerm
t1)]
, ATerm
t2 ATerm -> [AGuard] -> ABranch
<==. []
]
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)
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
$
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
<==. []
]
desugarBinApp Type
ty BOp
op ATerm
t1 ATerm
t2
| BOp
op BOp -> [BOp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Inter, BOp
Diff, BOp
Union] =
ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
ATerm -> [ATerm] -> ATerm
tapps (Type -> Prim -> ATerm
ATPrim ((Type
TyN Type -> Type -> Type
:*: Type
TyN Type -> Type -> Type
:->: Type
TyN) Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
ty) Prim
PrimMerge)
[ Type -> Prim -> ATerm
ATPrim (Type
TyN Type -> Type -> Type
:*: Type
TyN Type -> Type -> Type
:->: Type
TyN) (Type -> BOp -> Prim
mergeOp Type
ty BOp
op)
, ATerm
t1
, ATerm
t2
]
where
mergeOp :: Type -> BOp -> Prim
mergeOp Type
_ BOp
Inter = BOp -> Prim
PrimBOp BOp
Min
mergeOp Type
_ BOp
Diff = BOp -> Prim
PrimBOp BOp
SSub
mergeOp (TySet Type
_) BOp
Union = BOp -> Prim
PrimBOp BOp
Max
mergeOp (TyBag Type
_) BOp
Union = BOp -> Prim
PrimBOp BOp
Add
mergeOp Type
_ BOp
_ = [Char] -> Prim
forall a. HasCallStack => [Char] -> a
error ([Char] -> Prim) -> [Char] -> Prim
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! mergeOp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BOp -> [Char]
forall a. Show a => a -> [Char]
show BOp
op
desugarBinApp Type
_ BOp
Subset ATerm
t1 ATerm
t2 = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$
ATerm -> [ATerm] -> ATerm
tapps (Type -> Prim -> ATerm
ATPrim (Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
TyBool) (BOp -> Prim
PrimBOp BOp
Eq))
[ ATerm -> [ATerm] -> ATerm
tapps (Type -> Prim -> ATerm
ATPrim ((Type
TyN Type -> Type -> Type
:*: Type
TyN Type -> Type -> Type
:->: Type
TyN) Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
ty) Prim
PrimMerge)
[ Type -> Prim -> ATerm
ATPrim (Type
TyN Type -> Type -> Type
:*: Type
TyN Type -> Type -> Type
:->: Type
TyN) (BOp -> Prim
PrimBOp BOp
Max)
, ATerm
t1
, ATerm
t2
]
, ATerm
t2
]
where
ty :: Type
ty = ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t1
desugarBinApp Type
ty BOp
bop ATerm
t1 ATerm
t2 = [Char] -> Sem r DTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> Sem r DTerm) -> [Char] -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! desugarBinApp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BOp -> [Char]
forall a. Show a => a -> [Char]
show BOp
bop [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ATerm -> [Char]
forall a. Show a => a -> [Char]
show ATerm
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ATerm -> [Char]
forall a. Show a => a -> [Char]
show ATerm
t2
desugarComp :: Member Fresh r => Container -> ATerm -> Telescope AQual -> Sem r DTerm
desugarComp :: Container -> ATerm -> Telescope AQual -> Sem r DTerm
desugarComp Container
ctr ATerm
t Telescope AQual
qs = Container -> ATerm -> Telescope AQual -> Sem r ATerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope AQual -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope AQual
qs Sem r ATerm -> (ATerm -> Sem r DTerm) -> Sem r DTerm
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm
expandComp :: Member Fresh r => Container -> ATerm -> Telescope AQual -> Sem r ATerm
expandComp :: Container -> ATerm -> Telescope AQual -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope AQual
TelEmpty = ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Container -> ATerm -> ATerm
ctrSingleton Container
ctr ATerm
t
expandComp Container
ctr ATerm
t (TelCons (Rebind AQual (Telescope AQual) -> (AQual, Telescope AQual)
forall p1 p2. (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind -> (AQual
q,Telescope AQual
qs)))
= case AQual
q of
AQBind Name ATerm
x (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
lst) -> do
ATerm
tqs <- Container -> ATerm -> Telescope AQual -> Sem r ATerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope AQual -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope AQual
qs
let c :: Type -> Type
c = Container -> Type -> Type
containerTy Container
ctr
tTy :: Type
tTy = ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t
xTy :: Type
xTy = case ATerm -> Type
forall t. HasType t => t -> Type
getType Embedded (Embed ATerm)
ATerm
lst of
TyContainer Atom
_ Type
e -> Type
e
Type
_ -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible! Not a container in expandComp"
joinTy :: Type
joinTy = Type -> Type
c (Type -> Type
c Type
tTy) Type -> Type -> Type
:->: Type -> Type
c Type
tTy
mapTy :: Type
mapTy = (Type
xTy Type -> Type -> Type
:->: Type -> Type
c Type
tTy) Type -> Type -> Type
:*: Type -> Type
c Type
xTy Type -> Type -> Type
:->: Type -> Type
c (Type -> Type
c Type
tTy)
ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ ATerm -> ATerm -> ATerm
tapp (Type -> Prim -> ATerm
ATPrim Type
joinTy Prim
PrimJoin) (ATerm -> ATerm) -> ATerm -> ATerm
forall a b. (a -> b) -> a -> b
$
ATerm -> ATerm -> ATerm
tapp
(Type -> Prim -> ATerm
ATPrim Type
mapTy Prim
PrimEach)
(ATerm -> ATerm -> ATerm
mkPair
(Quantifier -> Type -> Clause -> ATerm
ATAbs Quantifier
Lam (Type
xTy Type -> Type -> Type
:->: Type -> Type
c Type
tTy) ([APattern] -> ATerm -> Clause
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Type -> Name ATerm -> APattern
APVar Type
xTy Name ATerm
x] ATerm
tqs))
Embedded (Embed ATerm)
ATerm
lst
)
AQGuard (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
g) -> do
ATerm
tqs <- Container -> ATerm -> Telescope AQual -> Sem r ATerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Container -> ATerm -> Telescope AQual -> Sem r ATerm
expandComp Container
ctr ATerm
t Telescope AQual
qs
ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Type -> [ABranch] -> ATerm
ATCase (Container -> Type -> Type
containerTy Container
ctr (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t))
[ ATerm
tqs ATerm -> [AGuard] -> ABranch
<==. [ATerm -> AGuard
tif Embedded (Embed ATerm)
ATerm
g]
, Container -> Type -> ATerm
ctrNil Container
ctr (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t) ATerm -> [AGuard] -> ABranch
<==. []
]
desugarLet :: Member Fresh r => [ABinding] -> ATerm -> Sem r DTerm
desugarLet :: [ABinding] -> ATerm -> Sem r DTerm
desugarLet [] ATerm
t = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
desugarLet ((ABinding Maybe (Embed PolyType)
_ Name ATerm
x (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
t1)) : [ABinding]
ls) ATerm
t =
DTerm -> DTerm -> DTerm
dtapp
(DTerm -> DTerm -> DTerm) -> Sem r DTerm -> Sem r (DTerm -> DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
Lam (ATerm -> Type
forall t. HasType t => t -> Type
getType Embedded (Embed ATerm)
ATerm
t1 Type -> Type -> Type
:->: ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t)
(Bind (Name DTerm) DTerm -> DTerm)
-> Sem r (Bind (Name DTerm) DTerm) -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name DTerm -> DTerm -> Bind (Name DTerm) DTerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Name ATerm -> Name DTerm
coerce Name ATerm
x) (DTerm -> Bind (Name DTerm) DTerm)
-> Sem r DTerm -> Sem r (Bind (Name DTerm) DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ABinding] -> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
[ABinding] -> ATerm -> Sem r DTerm
desugarLet [ABinding]
ls ATerm
t)
)
Sem r (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
ATerm
t1
mkLambda :: Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda :: Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda Type
funty [Name ATerm]
args DTerm
c = Type -> [Name ATerm] -> DTerm
go Type
funty [Name ATerm]
args
where
go :: Type -> [Name ATerm] -> DTerm
go Type
_ [] = DTerm
c
go ty :: Type
ty@(Type
_ :->: Type
ty2) (Name ATerm
x:[Name ATerm]
xs) = Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
Lam Type
ty (Name DTerm -> DTerm -> Bind (Name DTerm) DTerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Name ATerm -> Name DTerm
coerce Name ATerm
x) (Type -> [Name ATerm] -> DTerm
go Type
ty2 [Name ATerm]
xs))
go Type
ty [Name ATerm]
as = [Char] -> DTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> DTerm) -> [Char] -> DTerm
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! mkLambda.go " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Name ATerm] -> [Char]
forall a. Show a => a -> [Char]
show [Name ATerm]
as
mkQuant :: Quantifier -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkQuant :: Quantifier -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkQuant Quantifier
q [Type]
argtys [Name ATerm]
args DTerm
c = ((Name ATerm, Type) -> DTerm -> DTerm)
-> DTerm -> [(Name ATerm, Type)] -> DTerm
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name ATerm, Type) -> DTerm -> DTerm
quantify DTerm
c ([Name ATerm] -> [Type] -> [(Name ATerm, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name ATerm]
args [Type]
argtys)
where
quantify :: (Name ATerm, Type) -> DTerm -> DTerm
quantify (Name ATerm
x, Type
ty) DTerm
body = Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs Quantifier
q Type
ty (Name DTerm -> DTerm -> Bind (Name DTerm) DTerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Name ATerm -> Name DTerm
coerce Name ATerm
x) DTerm
body)
mkAbs :: Quantifier -> Type -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkAbs :: Quantifier -> Type -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkAbs Quantifier
Lam Type
funty [Type]
_ [Name ATerm]
args DTerm
c = Type -> [Name ATerm] -> DTerm -> DTerm
mkLambda Type
funty [Name ATerm]
args DTerm
c
mkAbs Quantifier
q Type
_ [Type]
argtys [Name ATerm]
args DTerm
c = Quantifier -> [Type] -> [Name ATerm] -> DTerm -> DTerm
mkQuant Quantifier
q [Type]
argtys [Name ATerm]
args DTerm
c
desugarTuples :: Member Fresh r => Type -> [ATerm] -> Sem r DTerm
desugarTuples :: Type -> [ATerm] -> Sem r DTerm
desugarTuples Type
_ [ATerm
t] = ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
desugarTuples ty :: Type
ty@(Type
_ :*: Type
ty2) (ATerm
t:[ATerm]
ts) = Type -> DTerm -> DTerm -> DTerm
DTPair Type
ty (DTerm -> DTerm -> DTerm) -> Sem r DTerm -> Sem r (DTerm -> DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t Sem r (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> [ATerm] -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> [ATerm] -> Sem r DTerm
desugarTuples Type
ty2 [ATerm]
ts
desugarTuples Type
ty [ATerm]
ats
= [Char] -> Sem r DTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> Sem r DTerm) -> [Char] -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! desugarTuples " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ATerm] -> [Char]
forall a. Show a => a -> [Char]
show [ATerm]
ats
expandChain :: ATerm -> [ALink] -> ATerm
expandChain :: ATerm -> [ALink] -> ATerm
expandChain ATerm
_ [] = [Char] -> ATerm
forall a. HasCallStack => [Char] -> a
error [Char]
"Can't happen! expandChain _ []"
expandChain ATerm
t1 [ATLink BOp
op ATerm
t2] = Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
op ATerm
t1 ATerm
t2
expandChain ATerm
t1 (ATLink BOp
op ATerm
t2 : [ALink]
links) =
Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
And
(Type -> BOp -> ATerm -> ATerm -> ATerm
mkBin Type
TyBool BOp
op ATerm
t1 ATerm
t2)
(ATerm -> [ALink] -> ATerm
expandChain ATerm
t2 [ALink]
links)
desugarBranch :: Member Fresh r => ABranch -> Sem r DBranch
desugarBranch :: ABranch -> Sem r DBranch
desugarBranch ABranch
b = do
(Telescope AGuard
ags, ATerm
at) <- ABranch -> Sem r (Telescope AGuard, ATerm)
forall (r :: [(* -> *) -> * -> *]) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind ABranch
b
Telescope DGuard
dgs <- Telescope AGuard -> Sem r (Telescope DGuard)
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Telescope AGuard -> Sem r (Telescope DGuard)
desugarGuards Telescope AGuard
ags
DTerm
d <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
at
DBranch -> Sem r DBranch
forall (m :: * -> *) a. Monad m => a -> m a
return (DBranch -> Sem r DBranch) -> DBranch -> Sem r DBranch
forall a b. (a -> b) -> a -> b
$ Telescope DGuard -> DTerm -> DBranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope DGuard
dgs DTerm
d
desugarGuards :: Member Fresh r => Telescope AGuard -> Sem r (Telescope DGuard)
desugarGuards :: Telescope AGuard -> Sem r (Telescope DGuard)
desugarGuards = ([[DGuard]] -> Telescope DGuard)
-> Sem r [[DGuard]] -> Sem r (Telescope DGuard)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([DGuard] -> Telescope DGuard
forall b. Alpha b => [b] -> Telescope b
toTelescope ([DGuard] -> Telescope DGuard)
-> ([[DGuard]] -> [DGuard]) -> [[DGuard]] -> Telescope DGuard
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[DGuard]] -> [DGuard]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) (Sem r [[DGuard]] -> Sem r (Telescope DGuard))
-> (Telescope AGuard -> Sem r [[DGuard]])
-> Telescope AGuard
-> Sem r (Telescope DGuard)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AGuard -> Sem r [DGuard]) -> [AGuard] -> Sem r [[DGuard]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM AGuard -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [DGuard]
desugarGuard ([AGuard] -> Sem r [[DGuard]])
-> (Telescope AGuard -> [AGuard])
-> Telescope AGuard
-> Sem r [[DGuard]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope AGuard -> [AGuard]
forall b. Alpha b => Telescope b -> [b]
fromTelescope
where
desugarGuard :: Member Fresh r => AGuard -> Sem r [DGuard]
desugarGuard :: AGuard -> Sem r [DGuard]
desugarGuard (AGBool (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at)) = do
DTerm
dt <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
ATerm
at
DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (Type -> Side -> APattern -> APattern
APInj Type
TyBool Side
R APattern
APUnit)
desugarGuard (AGLet (ABinding Maybe (Embed PolyType)
_ Name ATerm
x (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at))) = do
DTerm
dt <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
ATerm
at
DTerm -> Name DTerm -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Name DTerm -> Sem r [DGuard]
varMatch DTerm
dt (Name ATerm -> Name DTerm
coerce Name ATerm
x)
desugarGuard (AGPat (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at) APattern
p) = do
DTerm
dt <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm Embedded (Embed ATerm)
ATerm
at
DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt APattern
p
desugarMatch :: Member Fresh r => DTerm -> APattern -> Sem r [DGuard]
desugarMatch :: DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (APVar Type
ty Name ATerm
x) = DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt (Type -> Name DTerm -> DPattern
DPVar Type
ty (Name ATerm -> Name DTerm
coerce Name ATerm
x))
desugarMatch DTerm
_ (APWild Type
_) = [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return []
desugarMatch DTerm
dt APattern
APUnit = DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt DPattern
DPUnit
desugarMatch DTerm
dt (APBool Bool
b) = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (Type -> Side -> APattern -> APattern
APInj Type
TyBool (Side -> Side -> Bool -> Side
forall a. a -> a -> Bool -> a
bool Side
L Side
R Bool
b) APattern
APUnit)
desugarMatch DTerm
dt (APNat Type
ty Integer
n) = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch (Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
TyBool (BOp -> Prim
PrimBOp BOp
Eq) DTerm
dt (Type -> Integer -> DTerm
DTNat Type
ty Integer
n)) (Bool -> APattern
APBool Bool
True)
desugarMatch DTerm
dt (APChar Char
c) = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch (Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
TyBool (BOp -> Prim
PrimBOp BOp
Eq) DTerm
dt (Char -> DTerm
DTChar Char
c)) (Bool -> APattern
APBool Bool
True)
desugarMatch DTerm
dt (APString [Char]
s) = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (Type -> [APattern] -> APattern
APList (Type -> Type
TyList Type
TyC) ((Char -> APattern) -> [Char] -> [APattern]
forall a b. (a -> b) -> [a] -> [b]
map Char -> APattern
APChar [Char]
s))
desugarMatch DTerm
dt (APTup Type
tupTy [APattern]
pat) = Type -> DTerm -> [APattern] -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> DTerm -> [APattern] -> Sem r [DGuard]
desugarTuplePats Type
tupTy DTerm
dt [APattern]
pat
where
desugarTuplePats :: Member Fresh r => Type -> DTerm -> [APattern] -> Sem r [DGuard]
desugarTuplePats :: Type -> DTerm -> [APattern] -> Sem r [DGuard]
desugarTuplePats Type
_ DTerm
_ [] = [Char] -> Sem r [DGuard]
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible! desugarTuplePats []"
desugarTuplePats Type
_ DTerm
t [APattern
p] = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
t APattern
p
desugarTuplePats ty :: Type
ty@(Type
_ :*: Type
ty2) DTerm
t (APattern
p:[APattern]
ps) = do
(Name DTerm
x1,[DGuard]
gs1) <- APattern -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
APattern -> Sem r (Name DTerm, [DGuard])
varForPat APattern
p
(Name DTerm
x2,[DGuard]
gs2) <- case [APattern]
ps of
[APVar Type
_ Name ATerm
px2] -> (Name DTerm, [DGuard]) -> Sem r (Name DTerm, [DGuard])
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ATerm -> Name DTerm
coerce Name ATerm
px2, [])
[APattern]
_ -> do
Name DTerm
x <- Name DTerm -> Sem r (Name DTerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name DTerm
forall a. [Char] -> Name a
string2Name [Char]
"x")
(Name DTerm
x,) ([DGuard] -> (Name DTerm, [DGuard]))
-> Sem r [DGuard] -> Sem r (Name DTerm, [DGuard])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> DTerm -> [APattern] -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type -> DTerm -> [APattern] -> Sem r [DGuard]
desugarTuplePats Type
ty2 (Type -> Name DTerm -> DTerm
dtVar Type
ty2 Name DTerm
x) [APattern]
ps
([[DGuard]] -> [DGuard]) -> Sem r [[DGuard]] -> Sem r [DGuard]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[DGuard]] -> [DGuard]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Sem r [[DGuard]] -> Sem r [DGuard])
-> ([Sem r [DGuard]] -> Sem r [[DGuard]])
-> [Sem r [DGuard]]
-> Sem r [DGuard]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r [DGuard]] -> Sem r [[DGuard]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Sem r [DGuard]] -> Sem r [DGuard])
-> [Sem r [DGuard]] -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$
[ DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
t (DPattern -> Sem r [DGuard]) -> DPattern -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$ Type -> Name DTerm -> Name DTerm -> DPattern
DPPair Type
ty Name DTerm
x1 Name DTerm
x2
, [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs1
, [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs2
]
desugarTuplePats Type
ty DTerm
_ [APattern]
_
= [Char] -> Sem r [DGuard]
forall a. HasCallStack => [Char] -> a
error ([Char] -> Sem r [DGuard]) -> [Char] -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! desugarTuplePats with non-pair type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty
desugarMatch DTerm
dt (APInj Type
ty Side
s APattern
p) = do
(Name DTerm
x,[DGuard]
gs) <- APattern -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
APattern -> Sem r (Name DTerm, [DGuard])
varForPat APattern
p
([[DGuard]] -> [DGuard]) -> Sem r [[DGuard]] -> Sem r [DGuard]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[DGuard]] -> [DGuard]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Sem r [[DGuard]] -> Sem r [DGuard])
-> ([Sem r [DGuard]] -> Sem r [[DGuard]])
-> [Sem r [DGuard]]
-> Sem r [DGuard]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r [DGuard]] -> Sem r [[DGuard]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Sem r [DGuard]] -> Sem r [DGuard])
-> [Sem r [DGuard]] -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$
[ DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt (DPattern -> Sem r [DGuard]) -> DPattern -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$ Type -> Side -> Name DTerm -> DPattern
DPInj Type
ty Side
s Name DTerm
x
, [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs
]
desugarMatch DTerm
dt (APCons Type
ty APattern
p1 APattern
p2) = do
Name DTerm
y <- Name DTerm -> Sem r (Name DTerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name DTerm
forall a. [Char] -> Name a
string2Name [Char]
"y")
(Name DTerm
x1, [DGuard]
gs1) <- APattern -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
APattern -> Sem r (Name DTerm, [DGuard])
varForPat APattern
p1
(Name DTerm
x2, [DGuard]
gs2) <- APattern -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
APattern -> Sem r (Name DTerm, [DGuard])
varForPat APattern
p2
let eltTy :: Type
eltTy = APattern -> Type
forall t. HasType t => t -> Type
getType APattern
p1
unrolledTy :: Type
unrolledTy = Type
eltTy Type -> Type -> Type
:*: Type
ty
([[DGuard]] -> [DGuard]) -> Sem r [[DGuard]] -> Sem r [DGuard]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[DGuard]] -> [DGuard]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Sem r [[DGuard]] -> Sem r [DGuard])
-> ([Sem r [DGuard]] -> Sem r [[DGuard]])
-> [Sem r [DGuard]]
-> Sem r [DGuard]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r [DGuard]] -> Sem r [[DGuard]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Sem r [DGuard]] -> Sem r [DGuard])
-> [Sem r [DGuard]] -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$
[ DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt (Type -> Side -> Name DTerm -> DPattern
DPInj Type
ty Side
R Name DTerm
y)
, DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch (Type -> Name DTerm -> DTerm
dtVar Type
unrolledTy Name DTerm
y) (Type -> Name DTerm -> Name DTerm -> DPattern
DPPair Type
unrolledTy Name DTerm
x1 Name DTerm
x2)
, [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs1
, [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [DGuard]
gs2
]
desugarMatch DTerm
dt (APList Type
ty []) = DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (Type -> Side -> APattern -> APattern
APInj Type
ty Side
L APattern
APUnit)
desugarMatch DTerm
dt (APList Type
ty [APattern]
ps) =
DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
dt (APattern -> Sem r [DGuard]) -> APattern -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$ (APattern -> APattern -> APattern)
-> APattern -> [APattern] -> APattern
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> APattern -> APattern -> APattern
APCons Type
ty) (Type -> [APattern] -> APattern
APList Type
ty []) [APattern]
ps
desugarMatch DTerm
dt (APAdd Type
ty Side
_ APattern
p ATerm
t) = (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
posRestrict ATerm -> ATerm -> ATerm
(-.) DTerm
dt Type
ty APattern
p ATerm
t
where
posRestrict :: Type -> Maybe (ATerm -> ATerm -> ATerm)
posRestrict Type
plusty
| Type
plusty Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type
TyN, Type
TyF] = (ATerm -> ATerm -> ATerm) -> Maybe (ATerm -> ATerm -> ATerm)
forall a. a -> Maybe a
Just ATerm -> ATerm -> ATerm
(>=.)
| Bool
otherwise = Maybe (ATerm -> ATerm -> ATerm)
forall a. Maybe a
Nothing
desugarMatch DTerm
dt (APMul Type
ty Side
_ APattern
p ATerm
t) = (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
intRestrict ATerm -> ATerm -> ATerm
(/.) DTerm
dt Type
ty APattern
p ATerm
t
where
intRestrict :: Type -> Maybe (ATerm -> ATerm -> ATerm)
intRestrict Type
plusty
| Type
plusty Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type
TyN, Type
TyZ] = (ATerm -> ATerm -> ATerm) -> Maybe (ATerm -> ATerm -> ATerm)
forall a. a -> Maybe a
Just ((ATerm -> ATerm -> ATerm) -> ATerm -> ATerm -> ATerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip ATerm -> ATerm -> ATerm
(|.))
| Bool
otherwise = Maybe (ATerm -> ATerm -> ATerm)
forall a. Maybe a
Nothing
desugarMatch DTerm
dt (APSub Type
ty APattern
p ATerm
t) = (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
(Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
arithBinMatch (Maybe (ATerm -> ATerm -> ATerm)
-> Type -> Maybe (ATerm -> ATerm -> ATerm)
forall a b. a -> b -> a
const Maybe (ATerm -> ATerm -> ATerm)
forall a. Maybe a
Nothing) ATerm -> ATerm -> ATerm
(+.) DTerm
dt Type
ty APattern
p ATerm
t
desugarMatch DTerm
dt (APFrac Type
_ APattern
p APattern
q)
= DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch
(DTerm -> DTerm -> DTerm
dtapp (Type -> Prim -> DTerm
DTPrim (Type
TyQ Type -> Type -> Type
:->: Type
TyZ Type -> Type -> Type
:*: Type
TyN) Prim
PrimFrac) DTerm
dt)
(Type -> [APattern] -> APattern
APTup (Type
TyZ Type -> Type -> Type
:*: Type
TyN) [APattern
p, APattern
q])
desugarMatch DTerm
dt (APNeg Type
ty APattern
p) = do
(Name DTerm
x0, [DGuard]
g1) <- DTerm -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [DGuard])
varFor DTerm
dt
[DGuard]
g2 <- AGuard -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [DGuard]
desugarGuard (AGuard -> Sem r [DGuard]) -> AGuard -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$ Embed ATerm -> AGuard
AGBool (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name ATerm -> ATerm
atVar Type
ty (Name DTerm -> Name ATerm
coerce Name DTerm
x0) ATerm -> ATerm -> ATerm
<. Type -> Integer -> ATerm
ATNat Type
ty Integer
0))
DTerm
neg <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm) -> ATerm -> Sem r DTerm
forall a b. (a -> b) -> a -> b
$ Type -> UOp -> ATerm -> ATerm
mkUn Type
ty UOp
Neg (Type -> Name ATerm -> ATerm
atVar Type
ty (Name DTerm -> Name ATerm
coerce Name DTerm
x0))
[DGuard]
g3 <- DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
neg APattern
p
[DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DGuard]
g1 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
g2 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
g3)
mkMatch :: Member Fresh r => DTerm -> DPattern -> Sem r [DGuard]
mkMatch :: DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt DPattern
dp = [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return [Embed DTerm -> DPattern -> DGuard
DGPat (Embedded (Embed DTerm) -> Embed DTerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed DTerm)
DTerm
dt) DPattern
dp]
varMatch :: Member Fresh r => DTerm -> Name DTerm -> Sem r [DGuard]
varMatch :: DTerm -> Name DTerm -> Sem r [DGuard]
varMatch DTerm
dt Name DTerm
x = DTerm -> DPattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> DPattern -> Sem r [DGuard]
mkMatch DTerm
dt (Type -> Name DTerm -> DPattern
DPVar (DTerm -> Type
forall t. HasType t => t -> Type
getType DTerm
dt) Name DTerm
x)
varFor :: Member Fresh r => DTerm -> Sem r (Name DTerm, [DGuard])
varFor :: DTerm -> Sem r (Name DTerm, [DGuard])
varFor (DTVar Type
_ (QName NameProvenance
_ Name DTerm
x)) = (Name DTerm, [DGuard]) -> Sem r (Name DTerm, [DGuard])
forall (m :: * -> *) a. Monad m => a -> m a
return (Name DTerm
x, [])
varFor DTerm
dt = do
Name DTerm
x <- Name DTerm -> Sem r (Name DTerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name DTerm
forall a. [Char] -> Name a
string2Name [Char]
"x")
[DGuard]
g <- DTerm -> Name DTerm -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Name DTerm -> Sem r [DGuard]
varMatch DTerm
dt Name DTerm
x
(Name DTerm, [DGuard]) -> Sem r (Name DTerm, [DGuard])
forall (m :: * -> *) a. Monad m => a -> m a
return (Name DTerm
x, [DGuard]
g)
varForPat :: Member Fresh r => APattern -> Sem r (Name DTerm, [DGuard])
varForPat :: APattern -> Sem r (Name DTerm, [DGuard])
varForPat (APVar Type
_ Name ATerm
x) = (Name DTerm, [DGuard]) -> Sem r (Name DTerm, [DGuard])
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ATerm -> Name DTerm
coerce Name ATerm
x, [])
varForPat APattern
p = do
Name DTerm
x <- Name DTerm -> Sem r (Name DTerm)
forall (r :: [(* -> *) -> * -> *]) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh ([Char] -> Name DTerm
forall a. [Char] -> Name a
string2Name [Char]
"px")
(Name DTerm
x,) ([DGuard] -> (Name DTerm, [DGuard]))
-> Sem r [DGuard] -> Sem r (Name DTerm, [DGuard])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch (Type -> Name DTerm -> DTerm
dtVar (APattern -> Type
forall t. HasType t => t -> Type
getType APattern
p) Name DTerm
x) APattern
p
arithBinMatch
:: Member Fresh r
=> (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm -> Type -> APattern -> ATerm -> Sem r [DGuard]
arithBinMatch :: (Type -> Maybe (ATerm -> ATerm -> ATerm))
-> (ATerm -> ATerm -> ATerm)
-> DTerm
-> Type
-> APattern
-> ATerm
-> Sem r [DGuard]
arithBinMatch Type -> Maybe (ATerm -> ATerm -> ATerm)
restrict ATerm -> ATerm -> ATerm
inverse DTerm
dt Type
ty APattern
p ATerm
t = do
(Name DTerm
x0, [DGuard]
g1) <- DTerm -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [DGuard])
varFor DTerm
dt
DTerm
t' <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
(Name DTerm
v, [DGuard]
g2) <- DTerm -> Sem r (Name DTerm, [DGuard])
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> Sem r (Name DTerm, [DGuard])
varFor DTerm
t'
[DGuard]
g3 <- case Type -> Maybe (ATerm -> ATerm -> ATerm)
restrict Type
ty of
Maybe (ATerm -> ATerm -> ATerm)
Nothing -> [DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Just ATerm -> ATerm -> ATerm
cmp ->
AGuard -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
AGuard -> Sem r [DGuard]
desugarGuard (AGuard -> Sem r [DGuard]) -> AGuard -> Sem r [DGuard]
forall a b. (a -> b) -> a -> b
$
Embed ATerm -> AGuard
AGBool (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed (Type -> Name ATerm -> ATerm
atVar Type
ty (Name DTerm -> Name ATerm
coerce Name DTerm
x0) ATerm -> ATerm -> ATerm
`cmp` Type -> Name ATerm -> ATerm
atVar (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t) (Name DTerm -> Name ATerm
coerce Name DTerm
v)))
DTerm
inv <- ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (Type -> Name ATerm -> ATerm
atVar Type
ty (Name DTerm -> Name ATerm
coerce Name DTerm
x0) ATerm -> ATerm -> ATerm
`inverse` Type -> Name ATerm -> ATerm
atVar (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
t) (Name DTerm -> Name ATerm
coerce Name DTerm
v))
[DGuard]
g4 <- DTerm -> APattern -> Sem r [DGuard]
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
DTerm -> APattern -> Sem r [DGuard]
desugarMatch DTerm
inv APattern
p
[DGuard] -> Sem r [DGuard]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DGuard]
g1 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
g2 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
g3 [DGuard] -> [DGuard] -> [DGuard]
forall a. [a] -> [a] -> [a]
++ [DGuard]
g4)
desugarContainer :: Member Fresh r => Type -> Container -> [(ATerm, Maybe ATerm)] -> Maybe (Ellipsis ATerm) -> Sem r DTerm
desugarContainer :: Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer Type
ty Container
ListContainer [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
Nothing =
(DTerm -> DTerm -> DTerm) -> DTerm -> [DTerm] -> DTerm
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
ty (BOp -> Prim
PrimBOp BOp
Cons)) (Type -> DTerm
DTNil Type
ty) ([DTerm] -> DTerm) -> Sem r [DTerm] -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ATerm, Maybe ATerm) -> Sem r DTerm)
-> [(ATerm, Maybe ATerm)] -> Sem r [DTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r DTerm)
-> ((ATerm, Maybe ATerm) -> ATerm)
-> (ATerm, Maybe ATerm)
-> Sem r DTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm, Maybe ATerm) -> ATerm
forall a b. (a, b) -> a
fst) [(ATerm, Maybe ATerm)]
es
desugarContainer ty :: Type
ty@(TyList Type
_) Container
ListContainer [(ATerm, Maybe ATerm)]
es (Just (Until ATerm
t)) =
Type -> Prim -> DTerm -> DTerm -> DTerm
dtbin Type
ty Prim
PrimUntil
(DTerm -> DTerm -> DTerm) -> Sem r DTerm -> Sem r (DTerm -> DTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ATerm -> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
ATerm -> Sem r DTerm
desugarTerm ATerm
t
Sem r (DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer Type
ty Container
ListContainer [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
forall a. Maybe a
Nothing
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
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
]
desugarContainer Type
ty Container
_ [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell =
DTerm -> DTerm -> DTerm
dtapp (Type -> Prim -> DTerm
DTPrim (Type -> Type
TyList Type
eltTy Type -> Type -> Type
:->: Type
ty) Prim
conv)
(DTerm -> DTerm) -> Sem r DTerm -> Sem r DTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
forall (r :: [(* -> *) -> * -> *]).
Member Fresh r =>
Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> Sem r DTerm
desugarContainer (Type -> Type
TyList Type
eltTy) Container
ListContainer [(ATerm, Maybe ATerm)]
es Maybe (Ellipsis ATerm)
mell
where
(Prim
conv, Type
eltTy) = case Type
ty of
TyBag Type
e -> (Prim
PrimBag, Type
e)
TySet Type
e -> (Prim
PrimSet, Type
e)
Type
_ -> [Char] -> (Prim, Type)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (Prim, Type)) -> [Char] -> (Prim, Type)
forall a b. (a -> b) -> a -> b
$ [Char]
"Impossible! Non-container type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
ty [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in desugarContainer"