{-|
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
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 (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 SyntaxInfo
syn 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 (PRef FC
_ [FC]
_ Name
f) [PArg
a])
        | [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 = d }) IState
i (PArg -> PTerm
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 -> 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 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"]))
                                   [ 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 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")) [ PTerm -> PArg
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")) [ 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 Int
i Text
nm   -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
reflm String
"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)]
         Name
_ -> String -> PTerm
forall a. HasCallStack => String -> a
error String
"Invalid name from user syntax for DSL name"

expandSugar :: DSL -> PTerm -> PTerm
expandSugar :: DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl (PLam FC
fc Name
n FC
nfc PTerm
ty PTerm
tm)
    | Just 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 Int
0))]
expandSugar DSL' PTerm
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 -> PTerm
expandSugar DSL' PTerm
dsl PTerm
ty) (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
tm)
expandSugar DSL' PTerm
dsl (PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
v PTerm
tm)
    | Just 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 String
"(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 Int
0))]
expandSugar DSL' PTerm
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 -> 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' PTerm
dsl (PPi Plicity
p Name
n FC
fc PTerm
ty PTerm
tm)
    | Just 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 String
"(dsl)") PTerm
pi [ PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> Name -> PTerm
mkTTName (String -> FC
fileFC String
"(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 Int
0))]
expandSugar DSL' PTerm
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 -> PTerm
expandSugar DSL' PTerm
dsl PTerm
ty) (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
tm)
expandSugar DSL' PTerm
dsl (PApp FC
fc PTerm
t [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 a b. (a -> b) -> PArg' a -> PArg' b
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' PTerm
dsl (PWithApp FC
fc PTerm
t 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' PTerm
dsl (PAppBind FC
fc PTerm
t [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 a b. (a -> b) -> PArg' a -> PArg' b
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' PTerm
dsl (PCase FC
fc PTerm
s [(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' PTerm
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"))
       [ Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
0 [] (Int -> String -> Name
sMN Int
0 String
"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 Int
0 [] (Int -> String -> Name
sMN Int
0 String
"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 Int
0 [] (Int -> String -> Name
sMN Int
0 String
"whenFalse") (PTerm -> PArg) -> PTerm -> PArg
forall a b. (a -> b) -> a -> b
$ DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
f
       ]
expandSugar DSL' PTerm
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 -> PTerm
expandSugar DSL' PTerm
dsl PTerm
l) (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
r)
expandSugar DSL' PTerm
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 -> 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' PTerm
dsl (PAlternative [(Name, Name)]
ms PAltType
a [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' PTerm
dsl (PHidden PTerm
t) = PTerm -> PTerm
PHidden (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
expandSugar DSL' PTerm
dsl (PNoImplicits PTerm
t) = PTerm -> PTerm
PNoImplicits (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
expandSugar DSL' PTerm
dsl (PUnifyLog PTerm
t) = PTerm -> PTerm
PUnifyLog (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
expandSugar DSL' PTerm
dsl (PDisamb [[Text]]
ns PTerm
t) = [[Text]] -> PTerm -> PTerm
PDisamb [[Text]]
ns (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t)
expandSugar DSL' PTerm
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 -> PTerm
expandSugar DSL' PTerm
dsl PTerm
t) Maybe PTerm
ty
expandSugar DSL' PTerm
dsl (PGoal FC
fc PTerm
r Name
n 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' PTerm
dsl (PDoBlock [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 PTerm
b [DoExp FC
fc PTerm
tm] = PTerm
tm
    block PTerm
b [PDo
a] = Err -> PTerm
PElabError (String -> Err
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 [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 PTerm
b (DoBindP FC
fc PTerm
p PTerm
tm [(PTerm, PTerm)]
alts : [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 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) (PTerm, PTerm) -> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
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) (PTerm, PTerm) -> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
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 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 PTerm
b (DoExp FC
fc PTerm
tm : [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 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 (String -> Err
forall t. String -> Err' t
Msg String
"Invalid statement in do block")

expandSugar DSL' PTerm
dsl (PIdiom FC
fc 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' PTerm
dsl (PRunElab FC
fc PTerm
tm [String]
ns) = FC -> PTerm -> [String] -> PTerm
PRunElab FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
tm) [String]
ns
expandSugar DSL' PTerm
dsl (PConstSugar FC
fc PTerm
tm) = FC -> PTerm -> PTerm
PConstSugar FC
fc (DSL' PTerm -> PTerm -> PTerm
expandSugar DSL' PTerm
dsl PTerm
tm)
expandSugar DSL' PTerm
dsl 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' PTerm
dsl Name
n PTerm
t Int
i = Int -> PTerm -> PTerm
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 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
            Maybe PTerm
Nothing -> Err -> PTerm
PElabError (String -> Err
forall t. String -> Err' t
Msg String
"No 'variable' defined in dsl")
            Just PTerm
v -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
v [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> t -> PTerm
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 <- 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 (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 t -> t -> t
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 <- 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 (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 t -> t -> t
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 <- 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 (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
it -> t -> t
forall 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) ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((PTerm -> PTerm) -> PArg -> PArg
forall a b. (a -> b) -> PArg' a -> PArg' b
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) (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
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 (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 ([PTerm] -> PTerm) -> [PTerm] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PTerm -> PTerm) -> [PTerm] -> [PTerm]
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 ((PDo -> PDo) -> [PDo] -> [PDo]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PDo -> PDo
forall a b. (a -> b) -> PDo' a -> PDo' b
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 DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
index_first DSL' PTerm
dsl of
                   Maybe PTerm
Nothing -> Err -> PTerm
PElabError (String -> Err
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 DSL' PTerm -> Maybe PTerm
forall t. DSL' t -> Maybe t
index_next DSL' PTerm
dsl of
                   Maybe PTerm
Nothing -> Err -> PTerm
PElabError (String -> Err
forall t. String -> Err' t
Msg String
"No index_next defined")
                   Just 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
-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) ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PArg -> PArg
forall a b. (a -> b) -> PArg' a -> PArg' b
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 [PTerm -> PArg
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 [PTerm -> PArg
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 [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 PTerm
b PTerm
tm = let (PTerm
tm', ([(Name, FC, PTerm)]
bs, Int
_)) = 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) ([], Int
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 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) <- 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 (String
"_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
+Int
1)
             PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
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' <- (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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM PArg -> StateT ([(Name, FC, PTerm)], Int) Identity PArg
dbArg [PArg]
args
              PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
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
              PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
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) = PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
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
             PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
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
                               PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
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 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
                                  PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
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
                                     PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
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) = (PTerm -> PTerm)
-> State ([(Name, FC, PTerm)], Int) PTerm
-> State ([(Name, FC, PTerm)], Int) PTerm
forall a b.
(a -> b)
-> StateT ([(Name, FC, PTerm)], Int) Identity a
-> StateT ([(Name, FC, PTerm)], Int) Identity b
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) = (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' PTerm
t = PTerm -> State ([(Name, FC, PTerm)], Int) PTerm
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
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' (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
a)
                 PArg -> StateT ([(Name, FC, PTerm)], Int) Identity PArg
forall a. a -> StateT ([(Name, FC, PTerm)], Int) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
a { getTm = t' })

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