{-# LANGUAGE PatternGuards #-}
module Idris.DSL (debindApp, desugar) where
import Idris.AbsSyntax
import Idris.Core.TT
import Control.Monad.State.Strict
import Data.Generics.Uniplate.Data (transform)
debindApp :: SyntaxInfo -> PTerm -> PTerm
debindApp :: SyntaxInfo -> PTerm -> PTerm
debindApp SyntaxInfo
syn PTerm
t = PTerm -> PTerm -> PTerm
debind (forall t. DSL' t -> t
dsl_bind (SyntaxInfo -> DSL
dsl_info SyntaxInfo
syn)) PTerm
t
dslify :: SyntaxInfo -> IState -> PTerm -> PTerm
dslify :: SyntaxInfo -> IState -> PTerm -> PTerm
dslify SyntaxInfo
syn IState
i = forall on. Uniplate on => (on -> on) -> on -> on
transform PTerm -> PTerm
dslifyApp
where
dslifyApp :: PTerm -> PTerm
dslifyApp (PApp FC
fc (PRef FC
_ [FC]
_ Name
f) [PArg
a])
| [DSL
d] <- forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
f (IState -> Ctxt DSL
idris_dsls IState
i)
= SyntaxInfo -> IState -> PTerm -> PTerm
desugar (SyntaxInfo
syn { dsl_info :: DSL
dsl_info = DSL
d }) IState
i (forall t. PArg' t -> t
getTm PArg
a)
dslifyApp PTerm
t = PTerm
t
desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
t = let t' :: PTerm
t' = DSL -> PTerm -> PTerm
expandSugar (SyntaxInfo -> DSL
dsl_info SyntaxInfo
syn) PTerm
t
in SyntaxInfo -> IState -> PTerm -> PTerm
dslify SyntaxInfo
syn IState
i PTerm
t'
mkTTName :: FC -> Name -> PTerm
mkTTName :: FC -> Name -> PTerm
mkTTName FC
fc Name
n =
let mkList :: FC -> [Text] -> PTerm
mkList FC
fc [] = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Nil") [String
"List", String
"Prelude"])
mkList FC
fc (Text
x:[Text]
xs) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> [String] -> Name
sNS (String -> Name
sUN String
"::") [String
"List", String
"Prelude"]))
[ forall {t}. t -> PArg' t
pexp (Text -> PTerm
stringC Text
x)
, forall {t}. t -> PArg' t
pexp (FC -> [Text] -> PTerm
mkList FC
fc [Text]
xs)]
stringC :: Text -> PTerm
stringC = FC -> Const -> PTerm
PConstant FC
fc forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Const
Str forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
str
intC :: Int -> PTerm
intC = FC -> Const -> PTerm
PConstant FC
fc forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I
reflm :: String -> Name
reflm String
n = Name -> [String] -> Name
sNS (String -> Name
sUN String
n) [String
"Reflection", String
"Language"]
in case Name
n of
UN Text
nm -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
reflm String
"UN")) [ forall {t}. t -> PArg' t
pexp (Text -> PTerm
stringC Text
nm)]
NS Name
nm [Text]
ns -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
reflm String
"NS")) [ forall {t}. t -> PArg' t
pexp (FC -> Name -> PTerm
mkTTName FC
fc Name
nm)
, forall {t}. t -> PArg' t
pexp (FC -> [Text] -> PTerm
mkList FC
fc [Text]
ns)]
MN Int
i Text
nm -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
reflm String
"MN")) [ forall {t}. t -> PArg' t
pexp (Int -> PTerm
intC Int
i)
, forall {t}. t -> PArg' t
pexp (Text -> PTerm
stringC Text
nm)]
Name
_ -> forall a. HasCallStack => String -> a
error String
"Invalid name from user syntax for DSL name"
expandSugar :: DSL -> PTerm -> PTerm
expandSugar :: DSL -> PTerm -> PTerm
expandSugar DSL
dsl (PLam FC
fc Name
n FC
nfc PTerm
ty PTerm
tm)
| Just PTerm
lam <- forall t. DSL' t -> Maybe t
dsl_lambda DSL
dsl
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
lam [ forall {t}. t -> PArg' t
pexp (FC -> Name -> PTerm
mkTTName FC
fc Name
n)
, forall {t}. t -> PArg' t
pexp (DSL -> PTerm -> PTerm
expandSugar DSL
dsl (DSL -> Name -> PTerm -> Int -> PTerm
var DSL
dsl Name
n PTerm
tm Int
0))]
expandSugar DSL
dsl (PLam FC
fc Name
n FC
nfc PTerm
ty PTerm
tm) = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
ty) (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
tm)
expandSugar DSL
dsl (PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
v PTerm
tm)
| Just PTerm
letb <- forall t. DSL' t -> Maybe t
dsl_let DSL
dsl
= FC -> PTerm -> [PArg] -> PTerm
PApp (String -> FC
fileFC String
"(dsl)") PTerm
letb [ forall {t}. t -> PArg' t
pexp (FC -> Name -> PTerm
mkTTName FC
fc Name
n)
, forall {t}. t -> PArg' t
pexp (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
v)
, forall {t}. t -> PArg' t
pexp (DSL -> PTerm -> PTerm
expandSugar DSL
dsl (DSL -> Name -> PTerm -> Int -> PTerm
var DSL
dsl Name
n PTerm
tm Int
0))]
expandSugar DSL
dsl (PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
v PTerm
tm) = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
ty) (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
v) (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
tm)
expandSugar DSL
dsl (PPi Plicity
p Name
n FC
fc PTerm
ty PTerm
tm)
| Just PTerm
pi <- forall t. DSL' t -> Maybe t
dsl_pi DSL
dsl
= FC -> PTerm -> [PArg] -> PTerm
PApp (String -> FC
fileFC String
"(dsl)") PTerm
pi [ forall {t}. t -> PArg' t
pexp (FC -> Name -> PTerm
mkTTName (String -> FC
fileFC String
"(dsl)") Name
n)
, forall {t}. t -> PArg' t
pexp (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
ty)
, forall {t}. t -> PArg' t
pexp (DSL -> PTerm -> PTerm
expandSugar DSL
dsl (DSL -> Name -> PTerm -> Int -> PTerm
var DSL
dsl Name
n PTerm
tm Int
0))]
expandSugar DSL
dsl (PPi Plicity
p Name
n FC
fc PTerm
ty PTerm
tm) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
ty) (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
tm)
expandSugar DSL
dsl (PApp FC
fc PTerm
t [PArg]
args) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t)
(forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DSL -> PTerm -> PTerm
expandSugar DSL
dsl)) [PArg]
args)
expandSugar DSL
dsl (PWithApp FC
fc PTerm
t PTerm
arg) = FC -> PTerm -> PTerm -> PTerm
PWithApp FC
fc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t)
(DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
arg)
expandSugar DSL
dsl (PAppBind FC
fc PTerm
t [PArg]
args) = FC -> PTerm -> [PArg] -> PTerm
PAppBind FC
fc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t)
(forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DSL -> PTerm -> PTerm
expandSugar DSL
dsl)) [PArg]
args)
expandSugar DSL
dsl (PCase FC
fc PTerm
s [(PTerm, PTerm)]
opts) = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
s)
(forall a b. (a -> b) -> [a] -> [b]
map (forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
pmap (DSL -> PTerm -> PTerm
expandSugar DSL
dsl)) [(PTerm, PTerm)]
opts)
expandSugar DSL
dsl (PIfThenElse FC
fc PTerm
c PTerm
t PTerm
f) =
FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
NoFC [] (String -> Name
sUN String
"ifThenElse"))
[ forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
0 [] (Int -> String -> Name
sMN Int
0 String
"condition") forall a b. (a -> b) -> a -> b
$ DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
c
, forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
0 [] (Int -> String -> Name
sMN Int
0 String
"whenTrue") forall a b. (a -> b) -> a -> b
$ DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t
, forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
0 [] (Int -> String -> Name
sMN Int
0 String
"whenFalse") forall a b. (a -> b) -> a -> b
$ DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
f
]
expandSugar DSL
dsl (PPair FC
fc [FC]
hls PunInfo
p PTerm
l PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc [FC]
hls PunInfo
p (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
l) (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
r)
expandSugar DSL
dsl (PDPair FC
fc [FC]
hls PunInfo
p PTerm
l PTerm
t PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
fc [FC]
hls PunInfo
p (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
l) (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t)
(DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
r)
expandSugar DSL
dsl (PAlternative [(Name, Name)]
ms PAltType
a [PTerm]
as) = [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [(Name, Name)]
ms PAltType
a (forall a b. (a -> b) -> [a] -> [b]
map (DSL -> PTerm -> PTerm
expandSugar DSL
dsl) [PTerm]
as)
expandSugar DSL
dsl (PHidden PTerm
t) = PTerm -> PTerm
PHidden (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t)
expandSugar DSL
dsl (PNoImplicits PTerm
t) = PTerm -> PTerm
PNoImplicits (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t)
expandSugar DSL
dsl (PUnifyLog PTerm
t) = PTerm -> PTerm
PUnifyLog (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t)
expandSugar DSL
dsl (PDisamb [[Text]]
ns PTerm
t) = [[Text]] -> PTerm -> PTerm
PDisamb [[Text]]
ns (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t)
expandSugar DSL
dsl (PRewrite FC
fc Maybe Name
by PTerm
r PTerm
t Maybe PTerm
ty)
= FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm
PRewrite FC
fc Maybe Name
by PTerm
r (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
t) Maybe PTerm
ty
expandSugar DSL
dsl (PGoal FC
fc PTerm
r Name
n PTerm
sc)
= FC -> PTerm -> Name -> PTerm -> PTerm
PGoal FC
fc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
r) Name
n (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
sc)
expandSugar DSL
dsl (PDoBlock [PDo]
ds)
= DSL -> PTerm -> PTerm
expandSugar DSL
dsl forall a b. (a -> b) -> a -> b
$ PTerm -> PTerm -> PTerm
debind (forall t. DSL' t -> t
dsl_bind DSL
dsl) (PTerm -> [PDo] -> PTerm
block (forall t. DSL' t -> t
dsl_bind DSL
dsl) [PDo]
ds)
where
block :: PTerm -> [PDo] -> PTerm
block PTerm
b [DoExp FC
fc PTerm
tm] = PTerm
tm
block PTerm
b [PDo
a] = Err -> PTerm
PElabError (forall t. String -> Err' t
Msg String
"Last statement in do block must be an expression")
block PTerm
b (DoBind FC
fc Name
n FC
nfc PTerm
tm : [PDo]
rest)
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
b [forall {t}. t -> PArg' t
pexp PTerm
tm, forall {t}. t -> PArg' t
pexp (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc PTerm
Placeholder (PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest))]
block PTerm
b (DoBindP FC
fc PTerm
p PTerm
tm [(PTerm, PTerm)]
alts : [PDo]
rest)
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
b [forall {t}. t -> PArg' t
pexp PTerm
tm, forall {t}. t -> PArg' t
pexp (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN Int
0 String
"__bpat") FC
NoFC PTerm
Placeholder
(FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN Int
0 String
"__bpat"))
((PTerm
p, PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest) forall a. a -> [a] -> [a]
: [(PTerm, PTerm)]
alts)))]
block PTerm
b (DoLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
tm : [PDo]
rest)
= FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
tm (PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest)
block PTerm
b (DoLetP FC
fc PTerm
p PTerm
tm [(PTerm, PTerm)]
alts : [PDo]
rest)
= FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc PTerm
tm ((PTerm
p, PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest) forall a. a -> [a] -> [a]
: [(PTerm, PTerm)]
alts)
block PTerm
b (DoRewrite FC
fc PTerm
h : [PDo]
rest)
= FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm
PRewrite FC
fc forall a. Maybe a
Nothing PTerm
h (PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest) forall a. Maybe a
Nothing
block PTerm
b (DoExp FC
fc PTerm
tm : [PDo]
rest)
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
b
[forall {t}. t -> PArg' t
pexp PTerm
tm,
forall {t}. t -> PArg' t
pexp (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN Int
0 String
"__bindx") FC
NoFC (PTerm -> PTerm
mkTy PTerm
tm) (PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest))]
where mkTy :: PTerm -> PTerm
mkTy (PCase FC
_ PTerm
_ [(PTerm, PTerm)]
_) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
unitTy
mkTy (PMetavar FC
_ Name
_) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
unitTy
mkTy PTerm
_ = PTerm
Placeholder
block PTerm
b [PDo]
_ = Err -> PTerm
PElabError (forall t. String -> Err' t
Msg String
"Invalid statement in do block")
expandSugar DSL
dsl (PIdiom FC
fc PTerm
e) = DSL -> PTerm -> PTerm
expandSugar DSL
dsl forall a b. (a -> b) -> a -> b
$ PTerm -> PTerm -> FC -> PTerm -> PTerm
unIdiom (forall t. DSL' t -> t
dsl_apply DSL
dsl) (forall t. DSL' t -> t
dsl_pure DSL
dsl) FC
fc PTerm
e
expandSugar DSL
dsl (PRunElab FC
fc PTerm
tm [String]
ns) = FC -> PTerm -> [String] -> PTerm
PRunElab FC
fc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
tm) [String]
ns
expandSugar DSL
dsl (PConstSugar FC
fc PTerm
tm) = FC -> PTerm -> PTerm
PConstSugar FC
fc (DSL -> PTerm -> PTerm
expandSugar DSL
dsl PTerm
tm)
expandSugar DSL
dsl PTerm
t = PTerm
t
var :: DSL -> Name -> PTerm -> Int -> PTerm
var :: DSL -> Name -> PTerm -> Int -> PTerm
var DSL
dsl Name
n PTerm
t Int
i = forall {t}. (Eq t, Num t) => t -> PTerm -> PTerm
v' Int
i PTerm
t where
v' :: t -> PTerm -> PTerm
v' t
i (PRef FC
fc [FC]
hl Name
x) | Name
x forall a. Eq a => a -> a -> Bool
== Name
n =
case forall t. DSL' t -> Maybe t
dsl_var DSL
dsl of
Maybe PTerm
Nothing -> Err -> PTerm
PElabError (forall t. String -> Err' t
Msg String
"No 'variable' defined in dsl")
Just PTerm
v -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
v [forall {t}. t -> PArg' t
pexp (forall {t}. (Eq t, Num t) => FC -> t -> PTerm
mkVar FC
fc t
i)]
v' t
i (PLam FC
fc Name
n FC
nfc PTerm
ty PTerm
sc)
| Maybe PTerm
Nothing <- forall t. DSL' t -> Maybe t
dsl_lambda DSL
dsl
= FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc PTerm
ty (t -> PTerm -> PTerm
v' t
i PTerm
sc)
| Bool
otherwise = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc (t -> PTerm -> PTerm
v' t
i PTerm
ty) (t -> PTerm -> PTerm
v' (t
i forall a. Num a => a -> a -> a
+ t
1) PTerm
sc)
v' t
i (PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
val PTerm
sc)
| Maybe PTerm
Nothing <- forall t. DSL' t -> Maybe t
dsl_let DSL
dsl
= FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc (t -> PTerm -> PTerm
v' t
i PTerm
ty) (t -> PTerm -> PTerm
v' t
i PTerm
val) (t -> PTerm -> PTerm
v' t
i PTerm
sc)
| Bool
otherwise = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc (t -> PTerm -> PTerm
v' t
i PTerm
ty) (t -> PTerm -> PTerm
v' t
i PTerm
val) (t -> PTerm -> PTerm
v' (t
i forall a. Num a => a -> a -> a
+ t
1) PTerm
sc)
v' t
i (PPi Plicity
p Name
n FC
fc PTerm
ty PTerm
sc)
| Maybe PTerm
Nothing <- forall t. DSL' t -> Maybe t
dsl_pi DSL
dsl
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc (t -> PTerm -> PTerm
v' t
i PTerm
ty) (t -> PTerm -> PTerm
v' t
i PTerm
sc)
| Bool
otherwise = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc (t -> PTerm -> PTerm
v' t
i PTerm
ty) (t -> PTerm -> PTerm
v' (t
iforall a. Num a => a -> a -> a
+t
1) PTerm
sc)
v' t
i (PTyped PTerm
l PTerm
r) = PTerm -> PTerm -> PTerm
PTyped (t -> PTerm -> PTerm
v' t
i PTerm
l) (t -> PTerm -> PTerm
v' t
i PTerm
r)
v' t
i (PApp FC
f PTerm
x [PArg]
as) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
f (t -> PTerm -> PTerm
v' t
i PTerm
x) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> PTerm -> PTerm
v' t
i)) [PArg]
as)
v' t
i (PWithApp FC
f PTerm
x PTerm
a) = FC -> PTerm -> PTerm -> PTerm
PWithApp FC
f (t -> PTerm -> PTerm
v' t
i PTerm
x) (t -> PTerm -> PTerm
v' t
i PTerm
a)
v' t
i (PCase FC
f PTerm
t [(PTerm, PTerm)]
as) = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
f (t -> PTerm -> PTerm
v' t
i PTerm
t) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
pmap (t -> PTerm -> PTerm
v' t
i)) [(PTerm, PTerm)]
as)
v' t
i (PPair FC
f [FC]
hls PunInfo
p PTerm
l PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
f [FC]
hls PunInfo
p (t -> PTerm -> PTerm
v' t
i PTerm
l) (t -> PTerm -> PTerm
v' t
i PTerm
r)
v' t
i (PDPair FC
f [FC]
hls PunInfo
p PTerm
l PTerm
t PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
f [FC]
hls PunInfo
p (t -> PTerm -> PTerm
v' t
i PTerm
l) (t -> PTerm -> PTerm
v' t
i PTerm
t) (t -> PTerm -> PTerm
v' t
i PTerm
r)
v' t
i (PAlternative [(Name, Name)]
ms PAltType
a [PTerm]
as) = [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [(Name, Name)]
ms PAltType
a forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (t -> PTerm -> PTerm
v' t
i) [PTerm]
as
v' t
i (PHidden PTerm
t) = PTerm -> PTerm
PHidden (t -> PTerm -> PTerm
v' t
i PTerm
t)
v' t
i (PIdiom FC
f PTerm
t) = FC -> PTerm -> PTerm
PIdiom FC
f (t -> PTerm -> PTerm
v' t
i PTerm
t)
v' t
i (PDoBlock [PDo]
ds) = [PDo] -> PTerm
PDoBlock (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> PTerm -> PTerm
v' t
i)) [PDo]
ds)
v' t
i (PNoImplicits PTerm
t) = PTerm -> PTerm
PNoImplicits (t -> PTerm -> PTerm
v' t
i PTerm
t)
v' t
i PTerm
t = PTerm
t
mkVar :: FC -> t -> PTerm
mkVar FC
fc t
0 = case forall t. DSL' t -> Maybe t
index_first DSL
dsl of
Maybe PTerm
Nothing -> Err -> PTerm
PElabError (forall t. String -> Err' t
Msg String
"No index_first defined")
Just PTerm
f -> FC -> PTerm -> PTerm
setFC FC
fc PTerm
f
mkVar FC
fc t
n = case forall t. DSL' t -> Maybe t
index_next DSL
dsl of
Maybe PTerm
Nothing -> Err -> PTerm
PElabError (forall t. String -> Err' t
Msg String
"No index_next defined")
Just PTerm
f -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f [forall {t}. t -> PArg' t
pexp (FC -> t -> PTerm
mkVar FC
fc (t
nforall a. Num a => a -> a -> a
-t
1))]
setFC :: FC -> PTerm -> PTerm
setFC FC
fc (PRef FC
_ [FC]
_ Name
n) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n
setFC FC
fc (PApp FC
_ PTerm
f [PArg]
xs) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> PTerm -> PTerm
setFC FC
fc PTerm
f) (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FC -> PTerm -> PTerm
setFC FC
fc)) [PArg]
xs)
setFC FC
fc PTerm
t = PTerm
t
unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
unIdiom PTerm
ap PTerm
pure FC
fc e :: PTerm
e@(PApp FC
_ PTerm
_ [PArg]
_) = (PTerm, [PArg]) -> PTerm
mkap (PTerm -> (PTerm, [PArg])
getFn PTerm
e)
where
getFn :: PTerm -> (PTerm, [PArg])
getFn (PApp FC
fc PTerm
f [PArg]
args) = (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
pure [forall {t}. t -> PArg' t
pexp PTerm
f], [PArg]
args)
getFn PTerm
f = (PTerm
f, [])
mkap :: (PTerm, [PArg]) -> PTerm
mkap (PTerm
f, []) = PTerm
f
mkap (PTerm
f, PArg
a:[PArg]
as) = (PTerm, [PArg]) -> PTerm
mkap (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
ap [forall {t}. t -> PArg' t
pexp PTerm
f, PArg
a], [PArg]
as)
unIdiom PTerm
ap PTerm
pure FC
fc PTerm
e = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
pure [forall {t}. t -> PArg' t
pexp PTerm
e]
debind :: PTerm -> PTerm -> PTerm
debind :: PTerm -> PTerm -> PTerm
debind PTerm
b PTerm
tm = let (PTerm
tm', ([(Name, FC, PTerm)]
bs, Int
_)) = forall s a. State s a -> s -> (a, s)
runState (PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
tm) ([], Int
0) in
[(Name, FC, PTerm)] -> PTerm -> PTerm
bindAll (forall a. [a] -> [a]
reverse [(Name, FC, PTerm)]
bs) PTerm
tm'
where
db' :: PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' :: PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' (PAppBind FC
_ (PApp FC
fc PTerm
t [PArg]
args) [])
= PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' (FC -> PTerm -> [PArg] -> PTerm
PAppBind FC
fc PTerm
t [PArg]
args)
db' (PAppBind FC
fc PTerm
t [PArg]
args)
= do [PArg]
args' <- [PArg] -> StateT ([(Name, FC, PTerm)], Int) Identity [PArg]
dbs [PArg]
args
([(Name, FC, PTerm)]
bs, Int
n) <- forall s (m :: * -> *). MonadState s m => m s
get
let nm :: Name
nm = String -> Name
sUN (String
"_bindApp" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n)
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
nm, FC
fc, FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
t [PArg]
args') forall a. a -> [a] -> [a]
: [(Name, FC, PTerm)]
bs, Int
nforall a. Num a => a -> a -> a
+Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
nm)
db' (PApp FC
fc PTerm
t [PArg]
args)
= do PTerm
t' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
t
[PArg]
args' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PArg -> StateT ([(Name, FC, PTerm)], Int) Identity PArg
dbArg [PArg]
args
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
t' [PArg]
args')
db' (PWithApp FC
fc PTerm
t PTerm
arg)
= do PTerm
t' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
t
PTerm
arg' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
arg
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm -> PTerm
PWithApp FC
fc PTerm
t' PTerm
arg')
db' (PLam FC
fc Name
n FC
nfc PTerm
ty PTerm
sc) = forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc PTerm
ty (PTerm -> PTerm -> PTerm
debind PTerm
b PTerm
sc))
db' (PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
v PTerm
sc)
= do PTerm
v' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
v
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
v' (PTerm -> PTerm -> PTerm
debind PTerm
b PTerm
sc))
db' (PCase FC
fc PTerm
s [(PTerm, PTerm)]
opts) = do PTerm
s' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
s
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc PTerm
s' (forall a b. (a -> b) -> [a] -> [b]
map (forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
pmap (PTerm -> PTerm -> PTerm
debind PTerm
b)) [(PTerm, PTerm)]
opts))
db' (PPair FC
fc [FC]
hls PunInfo
p PTerm
l PTerm
r) = do PTerm
l' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
l
PTerm
r' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
r
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc [FC]
hls PunInfo
p PTerm
l' PTerm
r')
db' (PDPair FC
fc [FC]
hls PunInfo
p PTerm
l PTerm
t PTerm
r) = do PTerm
l' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
l
PTerm
r' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
r
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
fc [FC]
hls PunInfo
p PTerm
l' PTerm
t PTerm
r')
db' (PRunElab FC
fc PTerm
t [String]
ns) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\PTerm
tm -> FC -> PTerm -> [String] -> PTerm
PRunElab FC
fc PTerm
tm [String]
ns) (PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
t)
db' (PConstSugar FC
fc PTerm
tm) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (FC -> PTerm -> PTerm
PConstSugar FC
fc) (PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
tm)
db' PTerm
t = forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
t
dbArg :: PArg -> StateT ([(Name, FC, PTerm)], Int) Identity PArg
dbArg PArg
a = do PTerm
t' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' (forall t. PArg' t -> t
getTm PArg
a)
forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
a { getTm :: PTerm
getTm = PTerm
t' })
dbs :: [PArg] -> StateT ([(Name, FC, PTerm)], Int) Identity [PArg]
dbs [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
dbs (PArg
a : [PArg]
as) = do let t :: PTerm
t = forall t. PArg' t -> t
getTm PArg
a
PTerm
t' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
t
[PArg]
as' <- [PArg] -> StateT ([(Name, FC, PTerm)], Int) Identity [PArg]
dbs [PArg]
as
forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
a { getTm :: PTerm
getTm = PTerm
t' } forall a. a -> [a] -> [a]
: [PArg]
as')
bindAll :: [(Name, FC, PTerm)] -> PTerm -> PTerm
bindAll [] PTerm
tm = PTerm
tm
bindAll ((Name
n, FC
fc, PTerm
t) : [(Name, FC, PTerm)]
bs) PTerm
tm
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
b [forall {t}. t -> PArg' t
pexp PTerm
t, forall {t}. t -> PArg' t
pexp (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
NoFC PTerm
Placeholder ([(Name, FC, PTerm)] -> PTerm -> PTerm
bindAll [(Name, FC, PTerm)]
bs PTerm
tm))]