{-# 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
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
-> 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
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
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
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
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
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)
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
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
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
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
-> Name
-> PTerm
-> 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
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."))
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)
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)
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]
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]
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..]]
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
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..]]
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
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
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
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
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)
plicity :: Plicity
plicity = Plicity
impl
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)
doc :: Docstring a
doc = Docstring a
forall a. Docstring a
emptyDocstring
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
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) ->
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
, 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
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
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
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)
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)))
elabProjection :: ElabInfo
-> Name
-> [Name]
-> Name
-> Plicity
-> PTerm
-> (Docstring (Either Err PTerm))
-> SyntaxInfo
-> FC -> PTerm
-> Name
-> [PArg]
-> [Name]
-> Int
-> 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
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)
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
_ [] = []
pname_in :: Name
pname_in :: Name
pname_in = Name
rootname
rootname :: Name
rootname :: Name
rootname = Name -> Name
nsroot Name
cname
generateRhs :: PTerm
generateRhs :: PTerm
generateRhs = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
pname_in
elabUpdate :: ElabInfo
-> Name
-> [Name]
-> Name
-> Plicity
-> PTerm
-> (Docstring (Either Err PTerm))
-> SyntaxInfo
-> FC -> PTerm
-> Name
-> [PArg]
-> [Name]
-> Int
-> Bool
-> 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)
where
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)
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
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
pname_in :: Name
pname_in :: Name
pname_in = Name -> Name
in_name Name
rootname
rootname :: Name
rootname :: Name
rootname = Name -> Name
nsroot Name
pname
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
_ [] = []
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
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
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
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)