{-|
Module      : Idris.DSL
Description : Code to deal with DSL blocks.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# 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

-- | Replace DSL-bound variable in a term
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
-- For every arg which is an AppBind, lift it out
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))]