{-|
Module      : Idris.Elab.Record
Description : Code to elaborate records.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}
module Idris.Elab.Record(elabRecord) where

import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Docstrings
import Idris.Elab.Data
import Idris.Error
import Idris.Output (sendHighlighting)

import Control.Monad
import Data.List
import Data.Maybe
import qualified Data.Set as S

-- | Elaborate a record declaration
elabRecord :: ElabInfo
           -> ElabWhat
           -> (Docstring (Either Err PTerm))                                             -- ^ The documentation for the whole declaration
           -> SyntaxInfo
           -> FC
           -> DataOpts
           -> Name                                                                       -- ^ The name of the type being defined
           -> FC                                                                         -- ^ The precise source location of the tycon name
           -> [(Name, FC, Plicity, PTerm)]                                               -- ^ Parameters
           -> [(Name, Docstring (Either Err PTerm))]                                     -- ^ Parameter Docs
           -> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields
           -> Maybe (Name, FC)                                                           -- ^ Constructor Name
           -> (Docstring (Either Err PTerm))                                             -- ^ Constructor Doc
           -> SyntaxInfo                                                                 -- ^ Constructor SyntaxInfo
           -> Idris ()
elabRecord :: ElabInfo
-> ElabWhat
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> DataOpts
-> Name
-> FC
-> [(Name, FC, Plicity, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> Idris ()
elabRecord ElabInfo
info ElabWhat
what Docstring (Either Err PTerm)
doc SyntaxInfo
rsyn FC
fc DataOpts
opts Name
tyn FC
nfc [(Name, FC, Plicity, PTerm)]
params [(Name, Docstring (Either Err PTerm))]
paramDocs [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fields Maybe (Name, FC)
cname Docstring (Either Err PTerm)
cdoc SyntaxInfo
csyn
  = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Building data declaration for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
tyn
       -- Type constructor
       let tycon :: PTerm
tycon = [(Name, FC, Plicity, PTerm)] -> PTerm
generateTyConType [(Name, FC, Plicity, PTerm)]
params
       Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Type constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
tycon

       -- Data constructor
       Name
dconName <- Maybe Name -> Idris Name
generateDConName (((Name, FC) -> Name) -> Maybe (Name, FC) -> Maybe Name
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, FC) -> Name
forall a b. (a, b) -> a
fst Maybe (Name, FC)
cname)
       let dconTy :: PTerm
dconTy = [(Name, FC, Plicity, PTerm)]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> PTerm
forall a.
[(Name, FC, Plicity, PTerm)]
-> [(Name, FC, Plicity, PTerm, a)] -> PTerm
generateDConType [(Name, FC, Plicity, PTerm)]
params [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fieldsWithNameAndDoc
       Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Data constructor: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
dconTy

       -- Build data declaration for elaboration
       Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ (String -> String -> String) -> String -> [String] -> String
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> String -> String
forall a. [a] -> [a] -> [a]
(++) String
"" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
"\n" (((Name, Docstring (Either Err PTerm)) -> String)
-> [(Name, Docstring (Either Err PTerm))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Docstring (Either Err PTerm)) -> String
forall a. Show a => a -> String
show [(Name, Docstring (Either Err PTerm))]
dconsArgDocs)
       let datadecl :: PData' PTerm
datadecl = case ElabWhat
what of
                           ElabWhat
ETypes -> Name -> FC -> PTerm -> PData' PTerm
forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tyn FC
NoFC PTerm
tycon
                           ElabWhat
_ -> Name
-> FC
-> PTerm
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
     [Name])]
-> PData' PTerm
forall t.
Name
-> FC
-> t
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
-> PData' t
PDatadecl Name
tyn FC
NoFC PTerm
tycon [(Docstring (Either Err PTerm)
cdoc, [(Name, Docstring (Either Err PTerm))]
dconsArgDocs, Name
dconName, FC
NoFC, PTerm
dconTy, FC
fc, [])]
       ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> DataOpts
-> PData' PTerm
-> Idris ()
elabData ElabInfo
info SyntaxInfo
rsyn Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
paramDocs FC
fc DataOpts
opts PData' PTerm
datadecl

       -- Keep track of the record
       let parameters :: [(Name, PTerm)]
parameters = [(Name
n,PTerm
pt) | (Name
n, FC
_, Plicity
_, PTerm
pt) <- [(Name, FC, Plicity, PTerm)]
params]
       let projections :: [Name]
projections = [Name
n | (Name
n, FC
_, Plicity
_, PTerm
_, Maybe (Docstring (Either Err PTerm))
_) <- [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
fieldsWithName]
       Name -> RecordInfo -> Idris ()
addRecord Name
tyn ([(Name, PTerm)] -> Name -> [Name] -> RecordInfo
RI [(Name, PTerm)]
parameters Name
dconName [Name]
projections)
       IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCRecord Name
tyn)

       Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
           Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"fieldsWithName " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
-> String
forall a. Show a => a -> String
show [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
fieldsWithName
           Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"fieldsWIthNameAndDoc " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> String
forall a. Show a => a -> String
show [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fieldsWithNameAndDoc
           ElabInfo
-> SyntaxInfo
-> FC
-> Name
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> Name
-> PTerm
-> Idris ()
elabRecordFunctions ElabInfo
info SyntaxInfo
rsyn FC
fc Name
tyn [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
paramsAndDoc [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fieldsWithNameAndDoc Name
dconName PTerm
target

           Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting (Set (FC', OutputAnnotation) -> Idris ())
-> Set (FC', OutputAnnotation) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a. Ord a => [a] -> Set a
S.fromList ([(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation))
-> [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a b. (a -> b) -> a -> b
$
             [(FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
tyn Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)] [(FC', OutputAnnotation)]
-> [(FC', OutputAnnotation)] -> [(FC', OutputAnnotation)]
forall a. [a] -> [a] -> [a]
++
             [(FC', OutputAnnotation)]
-> ((Name, FC) -> [(FC', OutputAnnotation)])
-> Maybe (Name, FC)
-> [(FC', OutputAnnotation)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\(Name
_, FC
cnfc) -> [(FC -> FC'
FC' FC
cnfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
dconName Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)]) Maybe (Name, FC)
cname [(FC', OutputAnnotation)]
-> [(FC', OutputAnnotation)] -> [(FC', OutputAnnotation)]
forall a. [a] -> [a] -> [a]
++
             [(FC -> FC'
FC' FC
ffc, Name -> Bool -> OutputAnnotation
AnnBoundName Name
fn Bool
False) | (Name
fn, FC
ffc, Plicity
_, PTerm
_, Maybe (Docstring (Either Err PTerm))
_) <- [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
fieldsWithName]

  where
    -- | Generates a type constructor.
    generateTyConType :: [(Name, FC, Plicity, PTerm)] -> PTerm
    generateTyConType :: [(Name, FC, Plicity, PTerm)] -> PTerm
generateTyConType ((Name
n, FC
nfc, Plicity
p, PTerm
t) : [(Name, FC, Plicity, PTerm)]
rest) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p (Name -> Name
nsroot Name
n) FC
nfc PTerm
t ([(Name, FC, Plicity, PTerm)] -> PTerm
generateTyConType [(Name, FC, Plicity, PTerm)]
rest)
    generateTyConType [] = (FC -> PTerm
PType FC
fc)

    -- | Generates a name for the data constructor if none was specified.
    generateDConName :: Maybe Name -> Idris Name
    generateDConName :: Maybe Name -> Idris Name
generateDConName (Just Name
n) = Name -> Idris Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Idris Name) -> Name -> Idris Name
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
csyn Name
n
    generateDConName Maybe Name
Nothing  = Name -> Idris Name
uniqueName (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
csyn (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ Int -> String -> Name
sMN Int
0 (String
"Mk" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name -> String
forall a. Show a => a -> String
show (Name -> Name
nsroot Name
tyn))))
      where
        uniqueName :: Name -> Idris Name
        uniqueName :: Name -> Idris Name
uniqueName Name
n = do IState
i <- Idris IState
getIState
                          case Name -> Context -> Maybe (Name, TT Name)
lookupTyNameExact Name
n (IState -> Context
tt_ctxt IState
i) of
                            Just (Name, TT Name)
_  -> Name -> Idris Name
uniqueName (Name -> Name
nextName Name
n)
                            Maybe (Name, TT Name)
Nothing -> Name -> Idris Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n

    -- | Generates the data constructor type.
    generateDConType :: [(Name, FC, Plicity, PTerm)] -> [(Name, FC, Plicity, PTerm, a)] -> PTerm
    generateDConType :: forall a.
[(Name, FC, Plicity, PTerm)]
-> [(Name, FC, Plicity, PTerm, a)] -> PTerm
generateDConType ((Name
n, FC
nfc, Plicity
_, PTerm
t) : [(Name, FC, Plicity, PTerm)]
ps) [(Name, FC, Plicity, PTerm, a)]
as                  = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl (Name -> Name
nsroot Name
n) FC
NoFC PTerm
t ([(Name, FC, Plicity, PTerm)]
-> [(Name, FC, Plicity, PTerm, a)] -> PTerm
forall a.
[(Name, FC, Plicity, PTerm)]
-> [(Name, FC, Plicity, PTerm, a)] -> PTerm
generateDConType [(Name, FC, Plicity, PTerm)]
ps [(Name, FC, Plicity, PTerm, a)]
as)
    generateDConType []               ((Name
n, FC
_, Plicity
p, PTerm
t, a
_) : [(Name, FC, Plicity, PTerm, a)]
as) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p    (Name -> Name
nsroot Name
n) FC
NoFC PTerm
t ([(Name, FC, Plicity, PTerm)]
-> [(Name, FC, Plicity, PTerm, a)] -> PTerm
forall a.
[(Name, FC, Plicity, PTerm)]
-> [(Name, FC, Plicity, PTerm, a)] -> PTerm
generateDConType [] [(Name, FC, Plicity, PTerm, a)]
as)
    generateDConType [] [] = PTerm
target

    -- | The target for the constructor and projection functions. Also the source of the update functions.
    target :: PTerm
    target :: PTerm
target = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
tyn) ([PArg] -> PTerm) -> [PArg] -> PTerm
forall a b. (a -> b) -> a -> b
$ ((Plicity, Name) -> PArg) -> [(Plicity, Name)] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((Plicity -> Name -> PArg) -> (Plicity, Name) -> PArg
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Plicity -> Name -> PArg
asPRefArg) [(Plicity
p, Name
n) | (Name
n, FC
_, Plicity
p, PTerm
_) <- [(Name, FC, Plicity, PTerm)]
params]

    paramsAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
    paramsAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
paramsAndDoc = [(Name, FC, Plicity, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
pad [(Name, FC, Plicity, PTerm)]
params [(Name, Docstring (Either Err PTerm))]
paramDocs
      where
        pad :: [(Name, FC, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
        pad :: [(Name, FC, Plicity, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
pad ((Name
n, FC
fc, Plicity
p, PTerm
t) : [(Name, FC, Plicity, PTerm)]
rest) [(Name, Docstring (Either Err PTerm))]
docs
          = let d :: Docstring a
d = case Name
-> [(Name, Docstring (Either Err PTerm))]
-> Maybe (Docstring (Either Err PTerm))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Docstring (Either Err PTerm))]
docs of
                     Just Docstring (Either Err PTerm)
d' -> Docstring a
d
                     Maybe (Docstring (Either Err PTerm))
Nothing -> Docstring a
forall a. Docstring a
emptyDocstring
            in (Name
n, FC
fc, Plicity
p, PTerm
t, Docstring (Either Err PTerm)
forall a. Docstring a
d) (Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
forall a. a -> [a] -> [a]
: ([(Name, FC, Plicity, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
pad [(Name, FC, Plicity, PTerm)]
rest [(Name, Docstring (Either Err PTerm))]
docs)
        pad [(Name, FC, Plicity, PTerm)]
_ [(Name, Docstring (Either Err PTerm))]
_ = []

    dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]
    dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]
dconsArgDocs = [(Name, Docstring (Either Err PTerm))]
paramDocs [(Name, Docstring (Either Err PTerm))]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, Docstring (Either Err PTerm))]
forall a. [a] -> [a] -> [a]
++ ([(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
-> [(Name, Docstring (Either Err PTerm))]
dcad [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
fieldsWithName)
      where
        dcad :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Docstring (Either Err PTerm))]
        dcad :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
-> [(Name, Docstring (Either Err PTerm))]
dcad ((Name
n, FC
_, Plicity
_, PTerm
_, (Just Docstring (Either Err PTerm)
d)) : [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
rest) = ((Name -> Name
nsroot Name
n), Docstring (Either Err PTerm)
d) (Name, Docstring (Either Err PTerm))
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, Docstring (Either Err PTerm))]
forall a. a -> [a] -> [a]
: ([(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
-> [(Name, Docstring (Either Err PTerm))]
dcad [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
rest)
        dcad ((Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))
_ : [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
rest) = [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
-> [(Name, Docstring (Either Err PTerm))]
dcad [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
rest
        dcad [] = []

    fieldsWithName :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
    fieldsWithName :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
fieldsWithName = [Name]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> [(Name, FC, Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
fwn [] [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fields
      where
        fwn :: [Name] -> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
        fwn :: [Name]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> [(Name, FC, Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
fwn [Name]
ns ((Maybe (Name, FC)
n, Plicity
p, PTerm
t, Maybe (Docstring (Either Err PTerm))
d) : [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
rest)
          = let nn :: (Name, FC)
nn = case Maybe (Name, FC)
n of
                      Just (Name, FC)
n' -> (Name, FC)
n'
                      Maybe (Name, FC)
Nothing -> [Name] -> (Name, FC) -> (Name, FC)
newName [Name]
ns (Name, FC)
baseName
                withNS :: Name
withNS = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
rsyn ((Name, FC) -> Name
forall a b. (a, b) -> a
fst (Name, FC)
nn)
            in (Name
withNS, (Name, FC) -> FC
forall a b. (a, b) -> b
snd (Name, FC)
nn, Plicity
p, PTerm
t, Maybe (Docstring (Either Err PTerm))
d) (Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))
-> [(Name, FC, Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> [(Name, FC, Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
forall a. a -> [a] -> [a]
: ([Name]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> [(Name, FC, Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
fwn ((Name, FC) -> Name
forall a b. (a, b) -> a
fst (Name, FC)
nn Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
ns) [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
rest)
        fwn [Name]
_ [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
_ = []

        baseName :: (Name, FC)
baseName = (String -> Name
sUN String
"__pi_arg", FC
NoFC)

        newName :: [Name] -> (Name, FC) -> (Name, FC)
        newName :: [Name] -> (Name, FC) -> (Name, FC)
newName [Name]
ns (Name
n, FC
nfc)
          | Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ns = [Name] -> (Name, FC) -> (Name, FC)
newName [Name]
ns (Name -> Name
nextName Name
n, FC
nfc)
          | Bool
otherwise = (Name
n, FC
nfc)

    fieldsWithNameAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
    fieldsWithNameAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fieldsWithNameAndDoc = [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fwnad [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
fieldsWithName
      where
        fwnad :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
        fwnad :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fwnad ((Name
n, FC
nfc, Plicity
p, PTerm
t, Maybe (Docstring (Either Err PTerm))
d) : [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
rest)
          = let doc :: Docstring (Either Err PTerm)
doc = Docstring (Either Err PTerm)
-> Maybe (Docstring (Either Err PTerm))
-> Docstring (Either Err PTerm)
forall a. a -> Maybe a -> a
fromMaybe Docstring (Either Err PTerm)
forall a. Docstring a
emptyDocstring Maybe (Docstring (Either Err PTerm))
d
            in (Name
n, FC
nfc, Plicity
p, PTerm
t, Docstring (Either Err PTerm)
doc) (Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
forall a. a -> [a] -> [a]
: ([(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fwnad [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
rest)
        fwnad [] = []

elabRecordFunctions :: ElabInfo
                    -> SyntaxInfo
                    -> FC
                    -> Name                                                       -- ^ Record type name
                    -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Parameters
                    -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Fields
                    -> Name                                                       -- ^ Constructor Name
                    -> PTerm                                                      -- ^ Target type
                    -> Idris ()
elabRecordFunctions :: ElabInfo
-> SyntaxInfo
-> FC
-> Name
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> Name
-> PTerm
-> Idris ()
elabRecordFunctions ElabInfo
info SyntaxInfo
rsyn FC
fc Name
tyn [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
params [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fields Name
dconName PTerm
target
  = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating helper functions for record " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
tyn

       Int -> String -> Idris ()
logElab Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Fields: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
fieldNames
       Int -> String -> Idris ()
logElab Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Params: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
paramNames
       -- The elaborated constructor type for the data declaration
       IState
i <- Idris IState
getIState
       TT Name
ttConsTy <-
         case Name -> Context -> Maybe (TT Name)
lookupTyExact Name
dconName (IState -> Context
tt_ctxt IState
i) of
               Just TT Name
as -> TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
as
               Maybe (TT Name)
Nothing -> TC (TT Name) -> StateT IState (ExceptT Err IO) (TT Name)
forall a. TC a -> Idris a
tclift (TC (TT Name) -> StateT IState (ExceptT Err IO) (TT Name))
-> TC (TT Name) -> StateT IState (ExceptT Err IO) (TT Name)
forall a b. (a -> b) -> a -> b
$ Err -> TC (TT Name)
forall a. Err -> TC a
tfail (Err -> TC (TT Name)) -> Err -> TC (TT Name)
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe (TT Name) -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"record " Name
tyn Maybe (TT Name)
forall a. Maybe a
Nothing (String -> Err
forall t. String -> Err' t
InternalMsg String
"It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))

       -- The arguments to the constructor
       let constructorArgs :: [(Name, TT Name)]
constructorArgs = TT Name -> [(Name, TT Name)]
forall n. TT n -> [(n, TT n)]
getArgTys TT Name
ttConsTy
       Int -> String -> Idris ()
logElab Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Cons args: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, TT Name)] -> String
forall a. Show a => a -> String
show [(Name, TT Name)]
constructorArgs
       Int -> String -> Idris ()
logElab Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Free fields: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, TT Name)] -> String
forall a. Show a => a -> String
show (((Name, TT Name) -> Bool) -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Name, TT Name) -> Bool) -> (Name, TT Name) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, TT Name) -> Bool
forall a. (Name, a) -> Bool
isFieldOrParam') [(Name, TT Name)]
constructorArgs)
       -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.
       let freeFieldsForElab :: [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
freeFieldsForElab = ((Name, TT Name)
 -> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm)))
-> [(Name, TT Name)]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
forall a b. (a -> b) -> [a] -> [b]
map (IState
-> (Name, TT Name)
-> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))
freeField IState
i) (((Name, TT Name) -> Bool) -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Name, TT Name) -> Bool) -> (Name, TT Name) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, TT Name) -> Bool
forall a. (Name, a) -> Bool
isFieldOrParam') [(Name, TT Name)]
constructorArgs)

       -- The parameters for elaboration with their documentation
       -- Parameter functions are all prefixed with "param_".
       let paramsForElab :: [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
paramsForElab = [((Name -> Name
nsroot Name
n), (Name -> Name
paramName Name
n), Plicity
impl, PTerm
t, Docstring (Either Err PTerm)
d) | (Name
n, FC
_, Plicity
_, PTerm
t, Docstring (Either Err PTerm)
d) <- [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
params] -- zipParams i params paramDocs]

       -- The fields (written by the user) with their documentation.
       let userFieldsForElab :: [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
userFieldsForElab = [((Name -> Name
nsroot Name
n), Name
n, Plicity
p, PTerm
t, Docstring (Either Err PTerm)
d) | (Name
n, FC
nfc, Plicity
p, PTerm
t, Docstring (Either Err PTerm)
d) <- [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fields]

       -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
       let projectors :: [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
projectors = [(Name
n, Name
n', Plicity
p, PTerm
t, Docstring (Either Err PTerm)
d, Int
i) | ((Name
n, Name
n', Plicity
p, PTerm
t, Docstring (Either Err PTerm)
d), Int
i) <- [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [Int]
-> [((Name, Name, Plicity, PTerm, Docstring (Either Err PTerm)),
     Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
freeFieldsForElab [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
forall a. [a] -> [a] -> [a]
++ [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
paramsForElab [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
forall a. [a] -> [a] -> [a]
++ [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
userFieldsForElab) [Int
0..]]
       -- Build and elaborate projection functions
       Name
-> [Name]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm),
     Int)]
-> Idris ()
elabProj Name
dconName [Name]
paramNames [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
projectors

       Int -> String -> Idris ()
logElab Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Dependencies: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, [Name])] -> String
forall a. Show a => a -> String
show [(Name, [Name])]
fieldDependencies

       Int -> String -> Idris ()
logElab Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Depended on: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
dependedOn

       -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.
       let updaters :: [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
updaters = [(Name
n, Name
n', Plicity
p, PTerm
t, Docstring (Either Err PTerm)
d, Int
i) | ((Name
n, Name
n', Plicity
p, PTerm
t, Docstring (Either Err PTerm)
d), Int
i) <- [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [Int]
-> [((Name, Name, Plicity, PTerm, Docstring (Either Err PTerm)),
     Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
paramsForElab [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
forall a. [a] -> [a] -> [a]
++ [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
userFieldsForElab) [Int
0..]]
       -- Build and elaborate update functions
       Name
-> [Name]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm),
     Int)]
-> Idris ()
elabUp Name
dconName [Name]
paramNames [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
updaters
  where
    -- | Creates a PArg from a plicity and a name where the term is a Placeholder.
    placeholderArg :: Plicity -> Name -> PArg
    placeholderArg :: Plicity -> Name -> PArg
placeholderArg Plicity
p Name
n = Plicity -> Name -> PTerm -> PArg
asArg Plicity
p (Name -> Name
nsroot Name
n) PTerm
Placeholder

    -- | Root names of all fields in the current record declarations
    fieldNames :: [Name]
    fieldNames :: [Name]
fieldNames = [Name -> Name
nsroot Name
n | (Name
n, FC
_, Plicity
_, PTerm
_, Docstring (Either Err PTerm)
_) <- [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fields]

    paramNames :: [Name]
    paramNames :: [Name]
paramNames = [Name -> Name
nsroot Name
n | (Name
n, FC
_, Plicity
_, PTerm
_, Docstring (Either Err PTerm)
_) <- [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
params]

    isFieldOrParam :: Name -> Bool
    isFieldOrParam :: Name -> Bool
isFieldOrParam Name
n = Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Name]
fieldNames [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
paramNames)

    isFieldOrParam' :: (Name, a) -> Bool
    isFieldOrParam' :: forall a. (Name, a) -> Bool
isFieldOrParam' = Name -> Bool
isFieldOrParam (Name -> Bool) -> ((Name, a) -> Name) -> (Name, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, a) -> Name
forall a b. (a, b) -> a
fst

    -- Delabs the TT to PTerm
    -- This is not good.
    -- However, for machine generated implicits, there seems to be no PTerm available.
    -- Is there a better way to do this without building the setters and getters as TT?
    freeField :: IState -> (Name, TT Name) -> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))
    freeField :: IState
-> (Name, TT Name)
-> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))
freeField IState
i (Name, TT Name)
arg = let nameInCons :: Name
nameInCons = (Name, TT Name) -> Name
forall a b. (a, b) -> a
fst (Name, TT Name)
arg -- The name as it appears in the constructor
                          nameFree :: Name
nameFree = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
rsyn (Name -> Name
freeName (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ (Name, TT Name) -> Name
forall a b. (a, b) -> a
fst (Name, TT Name)
arg) -- The name prefixed with "free_"
                          plicity :: Plicity
plicity = Plicity
impl -- All free fields are implicit as they are machine generated
                          fieldType :: PTerm
fieldType = IState -> TT Name -> PTerm
delab IState
i ((Name, TT Name) -> TT Name
forall a b. (a, b) -> b
snd (Name, TT Name)
arg) -- The type of the field
                          doc :: Docstring a
doc = Docstring a
forall a. Docstring a
emptyDocstring -- No docmentation for machine generated fields
                      in (Name
nameInCons, Name
nameFree, Plicity
plicity, PTerm
fieldType, Docstring (Either Err PTerm)
forall a. Docstring a
doc)

    freeName :: Name -> Name
    freeName :: Name -> Name
freeName (UN Text
n) = String -> Name
sUN (String
"free_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
    freeName (MN Int
i Text
n) = Int -> String -> Name
sMN Int
i (String
"free_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
    freeName (NS Name
n [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
freeName Name
n) [Text]
s
    freeName Name
n = Name
n

    paramName :: Name -> Name
    paramName :: Name -> Name
paramName (UN Text
n) = String -> Name
sUN (String
"param_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
    paramName (MN Int
i Text
n) = Int -> String -> Name
sMN Int
i (String
"param_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
    paramName (NS Name
n [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
paramName Name
n) [Text]
s
    paramName Name
n = Name
n

    -- | Elaborate the projection functions.
    elabProj :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
    elabProj :: Name
-> [Name]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm),
     Int)]
-> Idris ()
elabProj Name
cn [Name]
paramnames [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs
                   = let phArgs :: [PArg]
phArgs = ((Plicity, Name) -> PArg) -> [(Plicity, Name)] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((Plicity -> Name -> PArg) -> (Plicity, Name) -> PArg
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Plicity -> Name -> PArg
placeholderArg) [(Plicity
p, Name
n) | (Name
n, Name
_, Plicity
p, PTerm
_, Docstring (Either Err PTerm)
_, Int
_) <- [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs]
                         elab :: (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)
-> Idris ()
elab = \(Name
n, Name
n', Plicity
p, PTerm
t, Docstring (Either Err PTerm)
doc, Int
i) ->
                              -- Use projections in types
                           do let t' :: PTerm
t' = [(Name, Name)] -> PTerm -> PTerm
projectInType [(Name
m, Name
m') | (Name
m, Name
m', Plicity
_, PTerm
_, Docstring (Either Err PTerm)
_, Int
_) <- [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs
                                                              -- Parameters are already in scope, so just use them
                                                              , Bool -> Bool
not (Name
m Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
paramNames)] PTerm
t
                              ElabInfo
-> Name
-> [Name]
-> Name
-> Plicity
-> PTerm
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> PTerm
-> Name
-> [PArg]
-> [Name]
-> Int
-> Idris ()
elabProjection ElabInfo
info Name
n [Name]
paramnames Name
n' Plicity
p PTerm
t' Docstring (Either Err PTerm)
doc SyntaxInfo
rsyn FC
fc PTerm
target Name
cn [PArg]
phArgs [Name]
fieldNames Int
i
                     in ((Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)
 -> Idris ())
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm),
     Int)]
-> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)
-> Idris ()
elab [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs

    -- | Elaborate the update functions.
    elabUp :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
    elabUp :: Name
-> [Name]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm),
     Int)]
-> Idris ()
elabUp Name
cn [Name]
paramnames [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs
                 = let args :: [PArg]
args = ((Plicity, Name) -> PArg) -> [(Plicity, Name)] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((Plicity -> Name -> PArg) -> (Plicity, Name) -> PArg
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Plicity -> Name -> PArg
asPRefArg) [(Plicity
p, Name
n) | (Name
n, Name
_, Plicity
p, PTerm
_, Docstring (Either Err PTerm)
_, Int
_) <- [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs]
                       elab :: (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)
-> Idris ()
elab = \(Name
n, Name
n', Plicity
p, PTerm
t, Docstring (Either Err PTerm)
doc, Int
i) -> ElabInfo
-> Name
-> [Name]
-> Name
-> Plicity
-> PTerm
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> PTerm
-> Name
-> [PArg]
-> [Name]
-> Int
-> Bool
-> Idris ()
elabUpdate ElabInfo
info Name
n [Name]
paramnames Name
n' Plicity
p PTerm
t Docstring (Either Err PTerm)
doc SyntaxInfo
rsyn FC
fc PTerm
target Name
cn [PArg]
args [Name]
fieldNames Int
i (Name -> Bool
optionalSetter Name
n)
                   in ((Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)
 -> Idris ())
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm),
     Int)]
-> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)
-> Idris ()
elab [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs

    -- | Decides whether a setter should be generated for a field or not.
    optionalSetter :: Name -> Bool
    optionalSetter :: Name -> Bool
optionalSetter Name
n = Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
dependedOn

    -- | A map from a field name to the other fields it depends on.
    fieldDependencies :: [(Name, [Name])]
    fieldDependencies :: [(Name, [Name])]
fieldDependencies = ((Name, PTerm) -> (Name, [Name]))
-> [(Name, PTerm)] -> [(Name, [Name])]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> PTerm -> (Name, [Name]))
-> (Name, PTerm) -> (Name, [Name])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> PTerm -> (Name, [Name])
fieldDep) [(Name
n, PTerm
t) | (Name
n, FC
_, Plicity
_, PTerm
t, Docstring (Either Err PTerm)
_) <- [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fields [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
forall a. [a] -> [a] -> [a]
++ [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
params]
      where
        fieldDep :: Name -> PTerm -> (Name, [Name])
        fieldDep :: Name -> PTerm -> (Name, [Name])
fieldDep Name
n PTerm
t = ((Name -> Name
nsroot Name
n), [Name]
paramNames [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
fieldNames [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` PTerm -> [Name]
allNamesIn PTerm
t)

    -- | A list of fields depended on by other fields.
    dependedOn :: [Name]
    dependedOn :: [Name]
dependedOn = [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (([Maybe [Name]] -> [[Name]]
forall a. [Maybe a] -> [a]
catMaybes ((Name -> Maybe [Name]) -> [Name] -> [Maybe [Name]]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
x -> Name -> [(Name, [Name])] -> Maybe [Name]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x [(Name, [Name])]
fieldDependencies) [Name]
fieldNames)))

-- | Creates and elaborates a projection function.
elabProjection :: ElabInfo
               -> Name                           -- ^ Name of the argument in the constructor
               -> [Name]                         -- ^ Parameter names
               -> Name                           -- ^ Projection Name
               -> Plicity                        -- ^ Projection Plicity
               -> PTerm                          -- ^ Projection Type
               -> (Docstring (Either Err PTerm)) -- ^ Projection Documentation
               -> SyntaxInfo                     -- ^ Projection SyntaxInfo
               -> FC -> PTerm                    -- ^ Projection target type
               -> Name                           -- ^ Data constructor tame
               -> [PArg]                         -- ^ Placeholder Arguments to constructor
               -> [Name]                         -- ^ All Field Names
               -> Int                            -- ^ Argument Index
               -> Idris ()
elabProjection :: ElabInfo
-> Name
-> [Name]
-> Name
-> Plicity
-> PTerm
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> PTerm
-> Name
-> [PArg]
-> [Name]
-> Int
-> Idris ()
elabProjection ElabInfo
info Name
cname [Name]
paramnames Name
pname Plicity
plicity PTerm
projTy Docstring (Either Err PTerm)
pdoc SyntaxInfo
psyn FC
fc PTerm
targetTy Name
cn [PArg]
phArgs [Name]
fnames Int
index
  = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Generating Projection for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
pname

       let ty :: PDecl
ty = PDecl
generateTy
       Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Type of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
pname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PDecl -> String
forall a. Show a => a -> String
show PDecl
ty

       let lhs :: PTerm
lhs = PTerm
generateLhs
       Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"LHS of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
pname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs
       let rhs :: PTerm
rhs = PTerm
generateRhs
       Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"RHS of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
pname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs

       ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info PDecl
ty

       let clause :: PClause' PTerm
clause = FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl] -> PClause' PTerm
forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
pname PTerm
lhs [] PTerm
rhs []
       ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info (PDecl -> Idris ()) -> PDecl -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> FnOpts -> Name -> [PClause' PTerm] -> PDecl
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc [] Name
pname [PClause' PTerm
clause]
  where
    -- | The type of the projection function.
    generateTy :: PDecl
    generateTy :: PDecl
generateTy = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
pdoc [] SyntaxInfo
psyn FC
fc [] Name
pname FC
NoFC (PTerm -> PDecl) -> PTerm -> PDecl
forall a b. (a -> b) -> a -> b
$
                   [Name] -> PTerm -> PTerm
bindParams [Name]
paramnames (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                     Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
recName FC
NoFC PTerm
targetTy PTerm
projTy

    bindParams :: [Name] -> PTerm -> PTerm
bindParams [] PTerm
t = PTerm
t
    bindParams (Name
n : [Name]
ns) PTerm
ty = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl Name
n FC
NoFC PTerm
Placeholder ([Name] -> PTerm -> PTerm
bindParams [Name]
ns PTerm
ty)

    -- | The left hand side of the projection function.
    generateLhs :: PTerm
    generateLhs :: PTerm
generateLhs = let args :: [PArg]
args = Int -> [PArg] -> [PArg]
lhsArgs Int
index [PArg]
phArgs
                  in FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pname) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
cn) [PArg]
args)]
      where
        lhsArgs :: Int -> [PArg] -> [PArg]
        lhsArgs :: Int -> [PArg] -> [PArg]
lhsArgs Int
0 (PArg
_ : [PArg]
rest) = (Plicity -> Name -> PTerm -> PArg
asArg Plicity
plicity (Name -> Name
nsroot Name
cname) (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pname_in)) PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
rest
        lhsArgs Int
i (PArg
x : [PArg]
rest) = PArg
x PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: (Int -> [PArg] -> [PArg]
lhsArgs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [PArg]
rest)
        lhsArgs Int
_ [] = []

    -- | The "_in" name. Used for the lhs.
    pname_in :: Name
    pname_in :: Name
pname_in = Name
rootname -- in_name rootname

    rootname :: Name
    rootname :: Name
rootname = Name -> Name
nsroot Name
cname

    -- | The right hand side of the projection function.
    generateRhs :: PTerm
    generateRhs :: PTerm
generateRhs = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pname_in

-- | Creates and elaborates an update function.
-- If 'optional' is true, we will not fail if we can't elaborate the update function.
elabUpdate :: ElabInfo
           -> Name                           -- ^ Name of the argument in the constructor
           -> [Name]                         -- ^ Parameter names
           -> Name                           -- ^ Field Name
           -> Plicity                        -- ^ Field Plicity
           -> PTerm                          -- ^ Field Type
           -> (Docstring (Either Err PTerm)) -- ^ Field Documentation
           -> SyntaxInfo                     -- ^ Field SyntaxInfo
           -> FC -> PTerm                    -- ^ Projection Source Type
           -> Name                           -- ^ Data Constructor Name
           -> [PArg]                         -- ^ Arguments to constructor
           -> [Name]                         -- ^ All fields
           -> Int                            -- ^ Argument Index
           -> Bool                           -- ^ Optional
           -> Idris ()
elabUpdate :: ElabInfo
-> Name
-> [Name]
-> Name
-> Plicity
-> PTerm
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> PTerm
-> Name
-> [PArg]
-> [Name]
-> Int
-> Bool
-> Idris ()
elabUpdate ElabInfo
info Name
cname [Name]
paramnames Name
pname Plicity
plicity PTerm
pty Docstring (Either Err PTerm)
pdoc SyntaxInfo
psyn FC
fc PTerm
sty Name
cn [PArg]
args [Name]
fnames Int
i Bool
optional
  = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Generating Update for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
pname

       let ty :: PDecl
ty = PDecl
generateTy
       Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Type of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
set_pname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PDecl -> String
forall a. Show a => a -> String
show PDecl
ty

       let lhs :: PTerm
lhs = PTerm
generateLhs
       Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"LHS of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
set_pname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs

       let rhs :: PTerm
rhs = PTerm
generateRhs
       Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"RHS of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
set_pname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs

       let clause :: PClause' PTerm
clause = FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl] -> PClause' PTerm
forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
set_pname PTerm
lhs [] PTerm
rhs []

       Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info PDecl
ty
                      ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info (PDecl -> Idris ()) -> PDecl -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> FnOpts -> Name -> [PClause' PTerm] -> PDecl
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc [] Name
set_pname [PClause' PTerm
clause])
         (\Err
err -> Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Could not generate update function for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
pname)
                  {-if optional
                  then logElab 1 $ "Could not generate update function for " ++ show pname
                  else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}
  where
    -- | The type of the update function.
    generateTy :: PDecl
    generateTy :: PDecl
generateTy = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
pdoc [] SyntaxInfo
psyn FC
fc [] Name
set_pname FC
NoFC (PTerm -> PDecl) -> PTerm -> PDecl
forall a b. (a -> b) -> a -> b
$
                   [Name] -> PTerm -> PTerm
bindParams [Name]
paramnames (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                     Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl (Name -> Name
nsroot Name
pname) FC
NoFC PTerm
pty (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                       Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
recName FC
NoFC PTerm
sty (PTerm -> PTerm
substInput PTerm
sty)
      where substInput :: PTerm -> PTerm
substInput = [(Name, PTerm)] -> PTerm -> PTerm
substMatches [(Name
cname, FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> Name
nsroot Name
pname))]

    bindParams :: [Name] -> PTerm -> PTerm
bindParams [] PTerm
t = PTerm
t
    bindParams (Name
n : [Name]
ns) PTerm
ty = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl Name
n FC
NoFC PTerm
Placeholder ([Name] -> PTerm -> PTerm
bindParams [Name]
ns PTerm
ty)

    -- | The "_set" name.
    set_pname :: Name
    set_pname :: Name
set_pname = Name -> Name
set_name Name
pname

    set_name :: Name -> Name
    set_name :: Name -> Name
set_name (UN Text
n) = String -> Name
sUN (String
"set_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
    set_name (MN Int
i Text
n) = Int -> String -> Name
sMN Int
i (String
"set_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
    set_name (NS Name
n [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
set_name Name
n) [Text]
s
    set_name Name
n = Name
n

    -- | The left-hand side of the update function.
    generateLhs :: PTerm
    generateLhs :: PTerm
generateLhs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
set_pname) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (PTerm -> PArg) -> PTerm -> PArg
forall a b. (a -> b) -> a -> b
$ FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pname_in, PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
constructorPattern]
      where
        constructorPattern :: PTerm
        constructorPattern :: PTerm
constructorPattern = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
cn) [PArg]
args

    -- | The "_in" name.
    pname_in :: Name
    pname_in :: Name
pname_in = Name -> Name
in_name Name
rootname

    rootname :: Name
    rootname :: Name
rootname = Name -> Name
nsroot Name
pname

    -- | The right-hand side of the update function.
    generateRhs :: PTerm
    generateRhs :: PTerm
generateRhs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
cn) (Int -> [PArg] -> [PArg]
newArgs Int
i [PArg]
args)
      where
        newArgs :: Int -> [PArg] -> [PArg]
        newArgs :: Int -> [PArg] -> [PArg]
newArgs Int
0 (PArg
_ : [PArg]
rest) = (Plicity -> Name -> PTerm -> PArg
asArg Plicity
plicity (Name -> Name
nsroot Name
cname) (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pname_in)) PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
rest
        newArgs Int
i (PArg
x : [PArg]
rest) = PArg
x PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: (Int -> [PArg] -> [PArg]
newArgs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [PArg]
rest)
        newArgs Int
_ [] = []

-- | Post-fixes a name with "_in".
in_name :: Name -> Name
in_name :: Name -> Name
in_name (UN Text
n) = Int -> String -> Name
sMN Int
0 (Text -> String
str Text
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_in")
in_name (MN Int
i Text
n) = Int -> String -> Name
sMN Int
i (Text -> String
str Text
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_in")
in_name (NS Name
n [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
in_name Name
n) [Text]
s
in_name Name
n = Name
n

-- | Creates a PArg with a given plicity, name, and term.
asArg :: Plicity -> Name -> PTerm -> PArg
asArg :: Plicity -> Name -> PTerm -> PArg
asArg (Imp [ArgOpt]
os Static
_ Bool
_ Maybe ImplicitInfo
_ Bool
_ RigCount
_) Name
n PTerm
t = Int -> Bool -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
PImp Int
0 Bool
False [ArgOpt]
os Name
n PTerm
t
asArg (Exp [ArgOpt]
os Static
_ Bool
_ RigCount
_) Name
n PTerm
t = Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
0 [ArgOpt]
os Name
n PTerm
t
asArg (Constraint [ArgOpt]
os Static
_ RigCount
_) Name
n PTerm
t = Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PConstraint Int
0 [ArgOpt]
os Name
n PTerm
t
asArg (TacImp [ArgOpt]
os Static
_ PTerm
s RigCount
_) Name
n PTerm
t = Int -> [ArgOpt] -> Name -> PTerm -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> t -> PArg' t
PTacImplicit Int
0 [ArgOpt]
os Name
n PTerm
s PTerm
t

-- | Machine name "rec".
recName :: Name
recName :: Name
recName = Int -> String -> Name
sMN Int
0 String
"rec"

recRef :: PTerm
recRef = FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] Name
recName

projectInType :: [(Name, Name)] -> PTerm -> PTerm
projectInType :: [(Name, Name)] -> PTerm -> PTerm
projectInType [(Name, Name)]
xs = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
st
  where
    st :: PTerm -> PTerm
    st :: PTerm -> PTerm
st (PRef FC
fc [FC]
hls Name
n)
      | Just Name
pn <- Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
xs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls Name
pn) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
recRef]
    st PTerm
t = PTerm
t

-- | Creates an PArg from a plicity and a name where the term is a PRef.
asPRefArg :: Plicity -> Name -> PArg
asPRefArg :: Plicity -> Name -> PArg
asPRefArg Plicity
p Name
n = Plicity -> Name -> PTerm -> PArg
asArg Plicity
p (Name -> Name
nsroot Name
n) (PTerm -> PArg) -> PTerm -> PArg
forall a b. (a -> b) -> a -> b
$ FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] (Name -> Name
nsroot Name
n)