{-|
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 syn :: SyntaxInfo
syn t :: PTerm
t = PTerm -> PTerm -> PTerm
debind (DSL' PTerm -> PTerm
forall t. DSL' t -> t
dsl_bind (SyntaxInfo -> DSL' PTerm
dsl_info SyntaxInfo
syn)) PTerm
t

dslify :: SyntaxInfo -> IState -> PTerm -> PTerm
dslify :: SyntaxInfo -> IState -> PTerm -> PTerm
dslify syn :: SyntaxInfo
syn i :: IState
i = (PTerm -> PTerm) -> PTerm -> PTerm
forall on. Uniplate on => (on -> on) -> on -> on
transform PTerm -> PTerm
dslifyApp
  where
    dslifyApp :: PTerm -> PTerm
dslifyApp (PApp fc :: FC
fc (PRef _ _ f :: Name
f) [a :: PArg
a])
        | [d :: DSL' PTerm
d] <- Name -> Ctxt (DSL' PTerm) -> [DSL' PTerm]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
f (IState -> Ctxt (DSL' PTerm)
idris_dsls IState
i)
            = SyntaxInfo -> IState -> PTerm -> PTerm
desugar (SyntaxInfo
syn { dsl_info :: DSL' PTerm
dsl_info = DSL' PTerm
d }) IState
i (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
a)
    dslifyApp t :: PTerm
t = PTerm
t

desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
desugar syn :: SyntaxInfo
syn i :: IState
i t :: PTerm
t = let t' :: PTerm
t' = DSL' PTerm -> PTerm -> PTerm
expandSugar (SyntaxInfo -> DSL' PTerm
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
fc n :: Name
n =
    let mkList :: FC -> [Text] -> PTerm
mkList fc :: FC
fc []     = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> [String] -> Name
sNS (String -> Name
sUN "Nil") ["List", "Prelude"])
        mkList fc :: FC
fc (x :: Text
x:xs :: [Text]
xs) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> [String] -> Name
sNS (String -> Name
sUN "::") ["List", "Prelude"]))
                                   [ PTerm -> PArg
forall t. t -> PArg' t
pexp (Text -> PTerm
stringC Text
x)
                                   , PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> [Text] -> PTerm
mkList FC
fc [Text]
xs)]
        stringC :: Text -> PTerm
stringC = FC -> Const -> PTerm
PConstant FC
fc (Const -> PTerm) -> (Text -> Const) -> Text -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Const
Str (String -> Const) -> (Text -> String) -> Text -> Const
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
str
        intC :: Int -> PTerm
intC = FC -> Const -> PTerm
PConstant FC
fc (Const -> PTerm) -> (Int -> Const) -> Int -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I
        reflm :: String -> Name
reflm n :: String
n = Name -> [String] -> Name
sNS (String -> Name
sUN String
n) ["Reflection", "Language"]
    in case Name
n of
         UN nm :: Text
nm     -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
reflm "UN")) [ PTerm -> PArg
forall t. t -> PArg' t
pexp (Text -> PTerm
stringC Text
nm)]
         NS nm :: Name
nm ns :: [Text]
ns  -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
reflm "NS")) [ PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> Name -> PTerm
mkTTName FC
fc Name
nm)
                                                        , PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> [Text] -> PTerm
mkList FC
fc [Text]
ns)]
         MN i :: Int
i nm :: Text
nm   -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
reflm "MN")) [ PTerm -> PArg
forall t. t -> PArg' t
pexp (Int -> PTerm
intC Int
i)
                                                        , PTerm -> PArg
forall t. t -> PArg' t
pexp (Text -> PTerm
stringC Text
nm)]
         _ -> String -> PTerm
forall a. HasCallStack => String -> a
error "Invalid name from user syntax for DSL name"

expandSugar :: DSL -> PTerm -> PTerm
expandSugar :: DSL' PTerm -> PTerm -> PTerm
expandSugar dsl :: DSL' PTerm
dsl (PLam fc :: FC
fc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty tm :: PTerm
tm)
    | Just lam :: PTerm
lam <- DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
dsl_lambda DSL' PTerm
dsl
        = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
lam [ PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> Name -> PTerm
mkTTName FC
fc Name
n)
                      , PTerm -> PArg
forall t. t -> PArg' t
pexp (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl (DSL' PTerm -> Name -> PTerm -> Int -> PTerm
var DSL' PTerm
dsl Name
n PTerm
tm 0))]
expandSugar dsl :: DSL' PTerm
dsl (PLam fc :: FC
fc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty tm :: PTerm
tm) = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
ty) (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
tm)
expandSugar dsl :: DSL' PTerm
dsl (PLet fc :: FC
fc rc :: RigCount
rc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty v :: PTerm
v tm :: PTerm
tm)
    | Just letb :: PTerm
letb <- DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
dsl_let DSL' PTerm
dsl
        = FC -> PTerm -> [PArg] -> PTerm
PApp (String -> FC
fileFC "(dsl)") PTerm
letb [ PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> Name -> PTerm
mkTTName FC
fc Name
n)
                                     , PTerm -> PArg
forall t. t -> PArg' t
pexp (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
v)
                                     , PTerm -> PArg
forall t. t -> PArg' t
pexp (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl (DSL' PTerm -> Name -> PTerm -> Int -> PTerm
var DSL' PTerm
dsl Name
n PTerm
tm 0))]
expandSugar dsl :: DSL' PTerm
dsl (PLet fc :: FC
fc rc :: RigCount
rc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty v :: PTerm
v tm :: PTerm
tm) = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
ty) (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
v) (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
tm)
expandSugar dsl :: DSL' PTerm
dsl (PPi p :: Plicity
p n :: Name
n fc :: FC
fc ty :: PTerm
ty tm :: PTerm
tm)
    | Just pi :: PTerm
pi <- DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
dsl_pi DSL' PTerm
dsl
        = FC -> PTerm -> [PArg] -> PTerm
PApp (String -> FC
fileFC "(dsl)") PTerm
pi [ PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> Name -> PTerm
mkTTName (String -> FC
fileFC "(dsl)") Name
n)
                                   , PTerm -> PArg
forall t. t -> PArg' t
pexp (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
ty)
                                   , PTerm -> PArg
forall t. t -> PArg' t
pexp (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl (DSL' PTerm -> Name -> PTerm -> Int -> PTerm
var DSL' PTerm
dsl Name
n PTerm
tm 0))]
expandSugar dsl :: DSL' PTerm
dsl (PPi p :: Plicity
p n :: Name
n fc :: FC
fc ty :: PTerm
ty tm :: PTerm
tm) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
ty) (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
tm)
expandSugar dsl :: DSL' PTerm
dsl (PApp fc :: FC
fc t :: PTerm
t args :: [PArg]
args) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
                                        ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PArg -> PArg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl)) [PArg]
args)
expandSugar dsl :: DSL' PTerm
dsl (PWithApp fc :: FC
fc t :: PTerm
t arg :: PTerm
arg) = FC -> PTerm -> PTerm -> PTerm
PWithApp FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
                                                  (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
arg)
expandSugar dsl :: DSL' PTerm
dsl (PAppBind fc :: FC
fc t :: PTerm
t args :: [PArg]
args) = FC -> PTerm -> [PArg] -> PTerm
PAppBind FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
                                                ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PArg -> PArg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl)) [PArg]
args)
expandSugar dsl :: DSL' PTerm
dsl (PCase fc :: FC
fc s :: PTerm
s opts :: [(PTerm, PTerm)]
opts) = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
s)
                                        (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> (PTerm, PTerm) -> (PTerm, PTerm)
forall t b. (t -> b) -> (t, t) -> (b, b)
pmap (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl)) [(PTerm, PTerm)]
opts)
expandSugar dsl :: DSL' PTerm
dsl (PIfThenElse fc :: FC
fc c :: PTerm
c t :: PTerm
t f :: PTerm
f) =
  FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
NoFC [] (String -> Name
sUN "ifThenElse"))
       [ Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp 0 [] (Int -> String -> Name
sMN 0 "condition") (PTerm -> PArg) -> PTerm -> PArg
forall a b. (a -> b) -> a -> b
$ DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
c
       , Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp 0 [] (Int -> String -> Name
sMN 0 "whenTrue") (PTerm -> PArg) -> PTerm -> PArg
forall a b. (a -> b) -> a -> b
$ DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t
       , Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp 0 [] (Int -> String -> Name
sMN 0 "whenFalse") (PTerm -> PArg) -> PTerm -> PArg
forall a b. (a -> b) -> a -> b
$ DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
f
       ]
expandSugar dsl :: DSL' PTerm
dsl (PPair fc :: FC
fc hls :: [FC]
hls p :: PunInfo
p l :: PTerm
l r :: PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc [FC]
hls PunInfo
p (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
l) (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
r)
expandSugar dsl :: DSL' PTerm
dsl (PDPair fc :: FC
fc hls :: [FC]
hls p :: PunInfo
p l :: PTerm
l t :: PTerm
t r :: PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
fc [FC]
hls PunInfo
p (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
l) (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
                                                          (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
r)
expandSugar dsl :: DSL' PTerm
dsl (PAlternative ms :: [(Name, Name)]
ms a :: PAltType
a as :: [PTerm]
as) = [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [(Name, Name)]
ms PAltType
a ((PTerm -> PTerm) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl) [PTerm]
as)
expandSugar dsl :: DSL' PTerm
dsl (PHidden t :: PTerm
t) = PTerm -> PTerm
PHidden (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
expandSugar dsl :: DSL' PTerm
dsl (PNoImplicits t :: PTerm
t) = PTerm -> PTerm
PNoImplicits (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
expandSugar dsl :: DSL' PTerm
dsl (PUnifyLog t :: PTerm
t) = PTerm -> PTerm
PUnifyLog (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
expandSugar dsl :: DSL' PTerm
dsl (PDisamb ns :: [[Text]]
ns t :: PTerm
t) = [[Text]] -> PTerm -> PTerm
PDisamb [[Text]]
ns (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
expandSugar dsl :: DSL' PTerm
dsl (PRewrite fc :: FC
fc by :: Maybe Name
by r :: PTerm
r t :: PTerm
t ty :: Maybe PTerm
ty)
    = FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm
PRewrite FC
fc Maybe Name
by PTerm
r (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t) Maybe PTerm
ty
expandSugar dsl :: DSL' PTerm
dsl (PGoal fc :: FC
fc r :: PTerm
r n :: Name
n sc :: PTerm
sc)
    = FC -> PTerm -> Name -> PTerm -> PTerm
PGoal FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
r) Name
n (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
sc)
expandSugar dsl :: DSL' PTerm
dsl (PDoBlock ds :: [PDo]
ds)
    = DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ PTerm -> PTerm -> PTerm
debind (DSL' PTerm -> PTerm
forall t. DSL' t -> t
dsl_bind DSL' PTerm
dsl) (PTerm -> [PDo] -> PTerm
block (DSL' PTerm -> PTerm
forall t. DSL' t -> t
dsl_bind DSL' PTerm
dsl) [PDo]
ds)
  where
    block :: PTerm -> [PDo] -> PTerm
block b :: PTerm
b [DoExp fc :: FC
fc tm :: PTerm
tm] = PTerm
tm
    block b :: PTerm
b [a :: PDo
a] = Err -> PTerm
PElabError (String -> Err
forall t. String -> Err' t
Msg "Last statement in do block must be an expression")
    block b :: PTerm
b (DoBind fc :: FC
fc n :: Name
n nfc :: FC
nfc tm :: PTerm
tm : rest :: [PDo]
rest)
        = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
b [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
tm, PTerm -> PArg
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 b :: PTerm
b (DoBindP fc :: FC
fc p :: PTerm
p tm :: PTerm
tm alts :: [(PTerm, PTerm)]
alts : rest :: [PDo]
rest)
        = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
b [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
tm, PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN 0 "__bpat") FC
NoFC PTerm
Placeholder
                                   (FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN 0 "__bpat"))
                                             ((PTerm
p, PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest) (PTerm, PTerm) -> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a. a -> [a] -> [a]
: [(PTerm, PTerm)]
alts)))]
    block b :: PTerm
b (DoLet fc :: FC
fc rc :: RigCount
rc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty tm :: PTerm
tm : rest :: [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 b :: PTerm
b (DoLetP fc :: FC
fc p :: PTerm
p tm :: PTerm
tm alts :: [(PTerm, PTerm)]
alts : rest :: [PDo]
rest)
        = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc PTerm
tm ((PTerm
p, PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest) (PTerm, PTerm) -> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a. a -> [a] -> [a]
: [(PTerm, PTerm)]
alts)
    block b :: PTerm
b (DoRewrite fc :: FC
fc h :: PTerm
h : rest :: [PDo]
rest)
        = FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm
PRewrite FC
fc Maybe Name
forall a. Maybe a
Nothing PTerm
h (PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest) Maybe PTerm
forall a. Maybe a
Nothing
    block b :: PTerm
b (DoExp fc :: FC
fc tm :: PTerm
tm : rest :: [PDo]
rest)
        = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
b
            [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
tm,
             PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN 0 "__bindx") FC
NoFC (PTerm -> PTerm
mkTy PTerm
tm) (PTerm -> [PDo] -> PTerm
block PTerm
b [PDo]
rest))]
        where mkTy :: PTerm -> PTerm
mkTy (PCase _ _ _) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
unitTy
              mkTy (PMetavar _ _) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
unitTy
              mkTy _ = PTerm
Placeholder
    block b :: PTerm
b _ = Err -> PTerm
PElabError (String -> Err
forall t. String -> Err' t
Msg "Invalid statement in do block")

expandSugar dsl :: DSL' PTerm
dsl (PIdiom fc :: FC
fc e :: PTerm
e) = DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ PTerm -> PTerm -> FC -> PTerm -> PTerm
unIdiom (DSL' PTerm -> PTerm
forall t. DSL' t -> t
dsl_apply DSL' PTerm
dsl) (DSL' PTerm -> PTerm
forall t. DSL' t -> t
dsl_pure DSL' PTerm
dsl) FC
fc PTerm
e
expandSugar dsl :: DSL' PTerm
dsl (PRunElab fc :: FC
fc tm :: PTerm
tm ns :: [String]
ns) = FC -> PTerm -> [String] -> PTerm
PRunElab FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
tm) [String]
ns
expandSugar dsl :: DSL' PTerm
dsl (PConstSugar fc :: FC
fc tm :: PTerm
tm) = FC -> PTerm -> PTerm
PConstSugar FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
tm)
expandSugar dsl :: DSL' PTerm
dsl t :: PTerm
t = PTerm
t

-- | Replace DSL-bound variable in a term
var :: DSL -> Name -> PTerm -> Int -> PTerm
var :: DSL' PTerm -> Name -> PTerm -> Int -> PTerm
var dsl :: DSL' PTerm
dsl n :: Name
n t :: PTerm
t i :: Int
i = Int -> PTerm -> PTerm
forall a. (Eq a, Num a) => a -> PTerm -> PTerm
v' Int
i PTerm
t where
    v' :: a -> PTerm -> PTerm
v' i :: a
i (PRef fc :: FC
fc hl :: [FC]
hl x :: Name
x) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n =
        case DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
dsl_var DSL' PTerm
dsl of
            Nothing -> Err -> PTerm
PElabError (String -> Err
forall t. String -> Err' t
Msg "No 'variable' defined in dsl")
            Just v :: PTerm
v -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
v [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> a -> PTerm
forall t. (Eq t, Num t) => FC -> t -> PTerm
mkVar FC
fc a
i)]
    v' i :: a
i (PLam fc :: FC
fc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty sc :: PTerm
sc)
        | Maybe PTerm
Nothing <- DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
dsl_lambda DSL' PTerm
dsl
            = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc PTerm
ty (a -> PTerm -> PTerm
v' a
i PTerm
sc)
        | Bool
otherwise = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc (a -> PTerm -> PTerm
v' a
i PTerm
ty) (a -> PTerm -> PTerm
v' (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) PTerm
sc)
    v' i :: a
i (PLet fc :: FC
fc rc :: RigCount
rc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty val :: PTerm
val sc :: PTerm
sc)
        | Maybe PTerm
Nothing <- DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
dsl_let DSL' PTerm
dsl
            = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc (a -> PTerm -> PTerm
v' a
i PTerm
ty) (a -> PTerm -> PTerm
v' a
i PTerm
val) (a -> PTerm -> PTerm
v' a
i PTerm
sc)
        | Bool
otherwise = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc (a -> PTerm -> PTerm
v' a
i PTerm
ty) (a -> PTerm -> PTerm
v' a
i PTerm
val) (a -> PTerm -> PTerm
v' (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) PTerm
sc)
    v' i :: a
i (PPi p :: Plicity
p n :: Name
n fc :: FC
fc ty :: PTerm
ty sc :: PTerm
sc)
        | Maybe PTerm
Nothing <- DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
dsl_pi DSL' PTerm
dsl
            = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc (a -> PTerm -> PTerm
v' a
i PTerm
ty) (a -> PTerm -> PTerm
v' a
i PTerm
sc)
        | Bool
otherwise = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc (a -> PTerm -> PTerm
v' a
i PTerm
ty) (a -> PTerm -> PTerm
v' (a
ia -> a -> a
forall a. Num a => a -> a -> a
+1) PTerm
sc)
    v' i :: a
i (PTyped l :: PTerm
l r :: PTerm
r)    = PTerm -> PTerm -> PTerm
PTyped (a -> PTerm -> PTerm
v' a
i PTerm
l) (a -> PTerm -> PTerm
v' a
i PTerm
r)
    v' i :: a
i (PApp f :: FC
f x :: PTerm
x as :: [PArg]
as)   = FC -> PTerm -> [PArg] -> PTerm
PApp FC
f (a -> PTerm -> PTerm
v' a
i PTerm
x) ((PArg -> PArg) -> [PArg] -> [PArg]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((PTerm -> PTerm) -> PArg -> PArg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> PTerm -> PTerm
v' a
i)) [PArg]
as)
    v' i :: a
i (PWithApp f :: FC
f x :: PTerm
x a :: PTerm
a) = FC -> PTerm -> PTerm -> PTerm
PWithApp FC
f (a -> PTerm -> PTerm
v' a
i PTerm
x) (a -> PTerm -> PTerm
v' a
i PTerm
a)
    v' i :: a
i (PCase f :: FC
f t :: PTerm
t as :: [(PTerm, PTerm)]
as)  = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
f (a -> PTerm -> PTerm
v' a
i PTerm
t) (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((PTerm -> PTerm) -> (PTerm, PTerm) -> (PTerm, PTerm)
forall t b. (t -> b) -> (t, t) -> (b, b)
pmap (a -> PTerm -> PTerm
v' a
i)) [(PTerm, PTerm)]
as)
    v' i :: a
i (PPair f :: FC
f hls :: [FC]
hls p :: PunInfo
p l :: PTerm
l r :: PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
f [FC]
hls PunInfo
p (a -> PTerm -> PTerm
v' a
i PTerm
l) (a -> PTerm -> PTerm
v' a
i PTerm
r)
    v' i :: a
i (PDPair f :: FC
f hls :: [FC]
hls p :: PunInfo
p l :: PTerm
l t :: PTerm
t r :: PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
f [FC]
hls PunInfo
p (a -> PTerm -> PTerm
v' a
i PTerm
l) (a -> PTerm -> PTerm
v' a
i PTerm
t) (a -> PTerm -> PTerm
v' a
i PTerm
r)
    v' i :: a
i (PAlternative ms :: [(Name, Name)]
ms a :: PAltType
a as :: [PTerm]
as) = [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [(Name, Name)]
ms PAltType
a ([PTerm] -> PTerm) -> [PTerm] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PTerm -> PTerm) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (a -> PTerm -> PTerm
v' a
i) [PTerm]
as
    v' i :: a
i (PHidden t :: PTerm
t)     = PTerm -> PTerm
PHidden (a -> PTerm -> PTerm
v' a
i PTerm
t)
    v' i :: a
i (PIdiom f :: FC
f t :: PTerm
t)    = FC -> PTerm -> PTerm
PIdiom FC
f (a -> PTerm -> PTerm
v' a
i PTerm
t)
    v' i :: a
i (PDoBlock ds :: [PDo]
ds)   = [PDo] -> PTerm
PDoBlock ((PDo -> PDo) -> [PDo] -> [PDo]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PDo -> PDo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> PTerm -> PTerm
v' a
i)) [PDo]
ds)
    v' i :: a
i (PNoImplicits t :: PTerm
t) = PTerm -> PTerm
PNoImplicits (a -> PTerm -> PTerm
v' a
i PTerm
t)
    v' i :: a
i t :: PTerm
t = PTerm
t

    mkVar :: FC -> t -> PTerm
mkVar fc :: FC
fc 0 = case DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
index_first DSL' PTerm
dsl of
                   Nothing -> Err -> PTerm
PElabError (String -> Err
forall t. String -> Err' t
Msg "No index_first defined")
                   Just f :: PTerm
f  -> FC -> PTerm -> PTerm
setFC FC
fc PTerm
f
    mkVar fc :: FC
fc n :: t
n = case DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
index_next DSL' PTerm
dsl of
                   Nothing -> Err -> PTerm
PElabError (String -> Err
forall t. String -> Err' t
Msg "No index_next defined")
                   Just f :: PTerm
f -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> t -> PTerm
mkVar FC
fc (t
nt -> t -> t
forall a. Num a => a -> a -> a
-1))]

    setFC :: FC -> PTerm -> PTerm
setFC fc :: FC
fc (PRef _ _ n :: Name
n) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n
    setFC fc :: FC
fc (PApp _ f :: PTerm
f xs :: [PArg]
xs) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> PTerm -> PTerm
setFC FC
fc PTerm
f) ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PArg -> PArg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FC -> PTerm -> PTerm
setFC FC
fc)) [PArg]
xs)
    setFC fc :: FC
fc t :: PTerm
t = PTerm
t

unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
unIdiom ap :: PTerm
ap pure :: PTerm
pure fc :: FC
fc e :: PTerm
e@(PApp _ _ _) = (PTerm, [PArg]) -> PTerm
mkap (PTerm -> (PTerm, [PArg])
getFn PTerm
e)
  where
    getFn :: PTerm -> (PTerm, [PArg])
getFn (PApp fc :: FC
fc f :: PTerm
f args :: [PArg]
args) = (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
pure [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
f], [PArg]
args)
    getFn f :: PTerm
f = (PTerm
f, [])

    mkap :: (PTerm, [PArg]) -> PTerm
mkap (f :: PTerm
f, [])   = PTerm
f
    mkap (f :: PTerm
f, a :: PArg
a:as :: [PArg]
as) = (PTerm, [PArg]) -> PTerm
mkap (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
ap [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
f, PArg
a], [PArg]
as)

unIdiom ap :: PTerm
ap pure :: PTerm
pure fc :: FC
fc e :: PTerm
e = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
pure [PTerm -> PArg
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 b :: PTerm
b tm :: PTerm
tm = let (tm' :: PTerm
tm', (bs :: [(Name, FC, PTerm)]
bs, _)) = State ([(Name, FC, PTerm)], Int) PTerm
-> ([(Name, FC, PTerm)], Int)
-> (PTerm, ([(Name, FC, PTerm)], Int))
forall s a. State s a -> s -> (a, s)
runState (PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
tm) ([], 0) in
                  [(Name, FC, PTerm)] -> PTerm -> PTerm
bindAll ([(Name, FC, PTerm)] -> [(Name, FC, PTerm)]
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 _ (PApp fc :: FC
fc t :: PTerm
t args :: [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
fc t :: PTerm
t args :: [PArg]
args)
        = do [PArg]
args' <- [PArg] -> StateT ([(Name, FC, PTerm)], Int) Identity [PArg]
dbs [PArg]
args
             (bs :: [(Name, FC, PTerm)]
bs, n :: Int
n) <- StateT
  ([(Name, FC, PTerm)], Int) Identity ([(Name, FC, PTerm)], Int)
forall s (m :: * -> *). MonadState s m => m s
get
             let nm :: Name
nm = String -> Name
sUN ("_bindApp" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
             ([(Name, FC, PTerm)], Int)
-> StateT ([(Name, FC, PTerm)], Int) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
nm, FC
fc, FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
t [PArg]
args') (Name, FC, PTerm) -> [(Name, FC, PTerm)] -> [(Name, FC, PTerm)]
forall a. a -> [a] -> [a]
: [(Name, FC, PTerm)]
bs, Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1)
             PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
nm)
    db' (PApp fc :: FC
fc t :: PTerm
t args :: [PArg]
args)
         = do PTerm
t' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
t
              [PArg]
args' <- (PArg -> StateT ([(Name, FC, PTerm)], Int) Identity PArg)
-> [PArg] -> StateT ([(Name, FC, PTerm)], Int) Identity [PArg]
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
              PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
t' [PArg]
args')
    db' (PWithApp fc :: FC
fc t :: PTerm
t arg :: 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
              PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm -> PTerm
PWithApp FC
fc PTerm
t' PTerm
arg')
    db' (PLam fc :: FC
fc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty sc :: PTerm
sc) = PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
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
fc rc :: RigCount
rc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty v :: PTerm
v sc :: PTerm
sc)
        = do PTerm
v' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
v
             PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
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
fc s :: PTerm
s opts :: [(PTerm, PTerm)]
opts) = do PTerm
s' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' PTerm
s
                               PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc PTerm
s' (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> (PTerm, PTerm) -> (PTerm, PTerm)
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 :: [FC]
hls p :: PunInfo
p l :: PTerm
l r :: 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
                                  PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
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 :: [FC]
hls p :: PunInfo
p l :: PTerm
l t :: PTerm
t r :: 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
                                     PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
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
fc t :: PTerm
t ns :: [String]
ns) = (PTerm -> PTerm)
-> State ([(Name, FC, PTerm)], Int) PTerm
-> State ([(Name, FC, PTerm)], Int) PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\tm :: 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
fc tm :: PTerm
tm) = (PTerm -> PTerm)
-> State ([(Name, FC, PTerm)], Int) PTerm
-> State ([(Name, FC, PTerm)], Int) PTerm
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' t :: PTerm
t = PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
t

    dbArg :: PArg -> StateT ([(Name, FC, PTerm)], Int) Identity PArg
dbArg a :: PArg
a = do PTerm
t' <- PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
db' (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
a)
                 PArg -> StateT ([(Name, FC, PTerm)], Int) Identity PArg
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 [] = [PArg] -> StateT ([(Name, FC, PTerm)], Int) Identity [PArg]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    dbs (a :: PArg
a : as :: [PArg]
as) = do let t :: PTerm
t = PArg -> PTerm
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
                      [PArg] -> StateT ([(Name, FC, PTerm)], Int) Identity [PArg]
forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
a { getTm :: PTerm
getTm = PTerm
t' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
as')

    bindAll :: [(Name, FC, PTerm)] -> PTerm -> PTerm
bindAll [] tm :: PTerm
tm = PTerm
tm
    bindAll ((n :: Name
n, fc :: FC
fc, t :: PTerm
t) : bs :: [(Name, FC, PTerm)]
bs) tm :: PTerm
tm
       = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
b [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
t, PTerm -> PArg
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))]