{-# 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 info :: ElabInfo
info what :: ElabWhat
what doc :: Docstring (Either Err PTerm)
doc rsyn :: SyntaxInfo
rsyn fc :: FC
fc opts :: DataOpts
opts tyn :: Name
tyn nfc :: FC
nfc params :: [(Name, FC, Plicity, PTerm)]
params paramDocs :: [(Name, Docstring (Either Err PTerm))]
paramDocs fields :: [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fields cname :: Maybe (Name, FC)
cname cdoc :: Docstring (Either Err PTerm)
cdoc csyn :: SyntaxInfo
csyn
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 (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 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Data constructor: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
dconTy
Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ (String -> String -> String) -> String -> [String] -> String
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
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse "\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
ETypes -> Name -> FC -> PTerm -> PData' PTerm
forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tyn FC
NoFC PTerm
tycon
_ -> 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) | (n :: Name
n, _, _, pt :: PTerm
pt) <- [(Name, FC, Plicity, PTerm)]
params]
let projections :: [Name]
projections = [Name
n | (n :: Name
n, _, _, _, _) <- [(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 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 [] (\(_, cnfc :: 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) | (fn :: Name
fn, ffc :: FC
ffc, _, _, _) <- [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
fieldsWithName]
where
generateTyConType :: [(Name, FC, Plicity, PTerm)] -> PTerm
generateTyConType :: [(Name, FC, Plicity, PTerm)] -> PTerm
generateTyConType ((n :: Name
n, nfc :: FC
nfc, p :: Plicity
p, t :: PTerm
t) : rest :: [(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 n :: Name
n) = Name -> Idris Name
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 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 0 ("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 n :: Name
n = do IState
i <- Idris IState
getIState
case Name -> Context -> Maybe (Name, Type)
lookupTyNameExact Name
n (IState -> Context
tt_ctxt IState
i) of
Just _ -> Name -> Idris Name
uniqueName (Name -> Name
nextName Name
n)
Nothing -> Name -> Idris Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
generateDConType :: [(Name, FC, Plicity, PTerm)] -> [(Name, FC, Plicity, PTerm, a)] -> PTerm
generateDConType :: [(Name, FC, Plicity, PTerm)]
-> [(Name, FC, Plicity, PTerm, a)] -> PTerm
generateDConType ((n :: Name
n, nfc :: FC
nfc, _, t :: PTerm
t) : ps :: [(Name, FC, Plicity, PTerm)]
ps) as :: [(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 [] ((n :: Name
n, _, p :: Plicity
p, t :: PTerm
t, _) : as :: [(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) | (n :: Name
n, _, p :: Plicity
p, _) <- [(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 ((n :: Name
n, fc :: FC
fc, p :: Plicity
p, t :: PTerm
t) : rest :: [(Name, FC, Plicity, PTerm)]
rest) docs :: [(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 d' :: Docstring (Either Err PTerm)
d' -> Docstring a
d
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 _ _ = []
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 ((n :: Name
n, _, _, _, (Just d :: Docstring (Either Err PTerm)
d)) : rest :: [(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 (_ : rest :: [(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 ns :: [Name]
ns ((n :: Maybe (Name, FC)
n, p :: Plicity
p, t :: PTerm
t, d :: Maybe (Docstring (Either Err PTerm))
d) : rest :: [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
rest)
= let nn :: (Name, FC)
nn = case Maybe (Name, FC)
n of
Just n' :: (Name, FC)
n' -> (Name, FC)
n'
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 _ _ = []
baseName :: (Name, FC)
baseName = (String -> Name
sUN "__pi_arg", FC
NoFC)
newName :: [Name] -> (Name, FC) -> (Name, FC)
newName :: [Name] -> (Name, FC) -> (Name, FC)
newName ns :: [Name]
ns (n :: Name
n, nfc :: FC
nfc)
| Name
n Name -> [Name] -> 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 ((n :: Name
n, nfc :: FC
nfc, p :: Plicity
p, t :: PTerm
t, d :: Maybe (Docstring (Either Err PTerm))
d) : rest :: [(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 info :: ElabInfo
info rsyn :: SyntaxInfo
rsyn fc :: FC
fc tyn :: Name
tyn params :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
params fields :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fields dconName :: Name
dconName target :: PTerm
target
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Fields: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
fieldNames
Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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
Type
ttConsTy <-
case Name -> Context -> Maybe Type
lookupTyExact Name
dconName (IState -> Context
tt_ctxt IState
i) of
Just as :: Type
as -> Type -> StateT IState (ExceptT Err IO) Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
as
Nothing -> TC Type -> StateT IState (ExceptT Err IO) Type
forall a. TC a -> Idris a
tclift (TC Type -> StateT IState (ExceptT Err IO) Type)
-> TC Type -> StateT IState (ExceptT Err IO) Type
forall a b. (a -> b) -> a -> b
$ Err -> TC Type
forall a. Err -> TC a
tfail (Err -> TC Type) -> Err -> TC Type
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating "record " Name
tyn Maybe Type
forall a. Maybe a
Nothing (String -> Err
forall t. String -> Err' t
InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))
let constructorArgs :: [(Name, Type)]
constructorArgs = Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getArgTys Type
ttConsTy
Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Cons args: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, Type)] -> String
forall a. Show a => a -> String
show [(Name, Type)]
constructorArgs
Int -> String -> Idris ()
logElab 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Free fields: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, Type)] -> String
forall a. Show a => a -> String
show (((Name, Type) -> Bool) -> [(Name, Type)] -> [(Name, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((Name, Type) -> Bool) -> (Name, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Bool
forall a. (Name, a) -> Bool
isFieldOrParam') [(Name, Type)]
constructorArgs)
let freeFieldsForElab :: [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
freeFieldsForElab = ((Name, Type)
-> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm)))
-> [(Name, Type)]
-> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))]
forall a b. (a -> b) -> [a] -> [b]
map (IState
-> (Name, Type)
-> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))
freeField IState
i) (((Name, Type) -> Bool) -> [(Name, Type)] -> [(Name, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((Name, Type) -> Bool) -> (Name, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Bool
forall a. (Name, a) -> Bool
isFieldOrParam') [(Name, Type)]
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) | (n :: Name
n, _, _, t :: PTerm
t, d :: 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) | (n :: Name
n, nfc :: FC
nfc, p :: Plicity
p, t :: PTerm
t, d :: 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) | ((n :: Name
n, n' :: Name
n', p :: Plicity
p, t :: PTerm
t, d :: Docstring (Either Err PTerm)
d), i :: 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) [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 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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) | ((n :: Name
n, n' :: Name
n', p :: Plicity
p, t :: PTerm
t, d :: Docstring (Either Err PTerm)
d), i :: 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) [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 p :: Plicity
p n :: 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 | (n :: Name
n, _, _, _, _) <- [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
fields]
paramNames :: [Name]
paramNames :: [Name]
paramNames = [Name -> Name
nsroot Name
n | (n :: Name
n, _, _, _, _) <- [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
params]
isFieldOrParam :: Name -> Bool
isFieldOrParam :: Name -> Bool
isFieldOrParam n :: Name
n = Name
n Name -> [Name] -> 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' :: (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, Type)
-> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))
freeField i :: IState
i arg :: (Name, Type)
arg = let nameInCons :: Name
nameInCons = (Name, Type) -> Name
forall a b. (a, b) -> a
fst (Name, Type)
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, Type) -> Name
forall a b. (a, b) -> a
fst (Name, Type)
arg)
plicity :: Plicity
plicity = Plicity
impl
fieldType :: PTerm
fieldType = IState -> Type -> PTerm
delab IState
i ((Name, Type) -> Type
forall a b. (a, b) -> b
snd (Name, Type)
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 n :: Text
n) = String -> Name
sUN ("free_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
freeName (MN i :: Int
i n :: Text
n) = Int -> String -> Name
sMN Int
i ("free_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
freeName (NS n :: Name
n s :: [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
freeName Name
n) [Text]
s
freeName n :: Name
n = Name
n
paramName :: Name -> Name
paramName :: Name -> Name
paramName (UN n :: Text
n) = String -> Name
sUN ("param_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
paramName (MN i :: Int
i n :: Text
n) = Int -> String -> Name
sMN Int
i ("param_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
paramName (NS n :: Name
n s :: [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
paramName Name
n) [Text]
s
paramName n :: 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 cn :: Name
cn paramnames :: [Name]
paramnames fs :: [(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) | (n :: Name
n, _, p :: Plicity
p, _, _, _) <- [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs]
elab :: (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)
-> Idris ()
elab = \(n :: Name
n, n' :: Name
n', p :: Plicity
p, t :: PTerm
t, doc :: Docstring (Either Err PTerm)
doc, i :: Int
i) ->
do let t' :: PTerm
t' = [(Name, Name)] -> PTerm -> PTerm
projectInType [(Name
m, Name
m') | (m :: Name
m, m' :: Name
m', _, _, _, _) <- [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs
, Bool -> Bool
not (Name
m Name -> [Name] -> 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 cn :: Name
cn paramnames :: [Name]
paramnames fs :: [(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) | (n :: Name
n, _, p :: Plicity
p, _, _, _) <- [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)]
fs]
elab :: (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)
-> Idris ()
elab = \(n :: Name
n, n' :: Name
n', p :: Plicity
p, t :: PTerm
t, doc :: Docstring (Either Err PTerm)
doc, i :: 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 n :: Name
n = Name
n Name -> [Name] -> 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) | (n :: Name
n, _, _, t :: PTerm
t, _) <- [(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 n :: Name
n t :: 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 (\x :: 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 info :: ElabInfo
info cname :: Name
cname paramnames :: [Name]
paramnames pname :: Name
pname plicity :: Plicity
plicity projTy :: PTerm
projTy pdoc :: Docstring (Either Err PTerm)
pdoc psyn :: SyntaxInfo
psyn fc :: FC
fc targetTy :: PTerm
targetTy cn :: Name
cn phArgs :: [PArg]
phArgs fnames :: [Name]
fnames index :: Int
index
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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
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 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs
let rhs :: PTerm
rhs = PTerm
generateRhs
Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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
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 [] t :: PTerm
t = PTerm
t
bindParams (n :: Name
n : ns :: [Name]
ns) ty :: 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 0 (_ : rest :: [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 i :: Int
i (x :: PArg
x : rest :: [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
-1) [PArg]
rest)
lhsArgs _ [] = []
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 info :: ElabInfo
info cname :: Name
cname paramnames :: [Name]
paramnames pname :: Name
pname plicity :: Plicity
plicity pty :: PTerm
pty pdoc :: Docstring (Either Err PTerm)
pdoc psyn :: SyntaxInfo
psyn fc :: FC
fc sty :: PTerm
sty cn :: Name
cn args :: [PArg]
args fnames :: [Name]
fnames i :: Int
i optional :: Bool
optional
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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
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 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs
let rhs :: PTerm
rhs = PTerm
generateRhs
Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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
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
err -> Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 [] t :: PTerm
t = PTerm
t
bindParams (n :: Name
n : ns :: [Name]
ns) ty :: 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 n :: Text
n) = String -> Name
sUN ("set_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
set_name (MN i :: Int
i n :: Text
n) = Int -> String -> Name
sMN Int
i ("set_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
set_name (NS n :: Name
n s :: [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
set_name Name
n) [Text]
s
set_name n :: 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 0 (_ : rest :: [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 i :: Int
i (x :: PArg
x : rest :: [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
-1) [PArg]
rest)
newArgs _ [] = []
in_name :: Name -> Name
in_name :: Name -> Name
in_name (UN n :: Text
n) = Int -> String -> Name
sMN 0 (Text -> String
str Text
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_in")
in_name (MN i :: Int
i n :: Text
n) = Int -> String -> Name
sMN Int
i (Text -> String
str Text
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_in")
in_name (NS n :: Name
n s :: [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
in_name Name
n) [Text]
s
in_name n :: Name
n = Name
n
asArg :: Plicity -> Name -> PTerm -> PArg
asArg :: Plicity -> Name -> PTerm -> PArg
asArg (Imp os :: [ArgOpt]
os _ _ _ _ _) n :: Name
n t :: PTerm
t = Int -> Bool -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
PImp 0 Bool
False [ArgOpt]
os Name
n PTerm
t
asArg (Exp os :: [ArgOpt]
os _ _ _) n :: Name
n t :: PTerm
t = Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp 0 [ArgOpt]
os Name
n PTerm
t
asArg (Constraint os :: [ArgOpt]
os _ _) n :: Name
n t :: PTerm
t = Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PConstraint 0 [ArgOpt]
os Name
n PTerm
t
asArg (TacImp os :: [ArgOpt]
os _ s :: PTerm
s _) n :: Name
n t :: PTerm
t = Int -> [ArgOpt] -> Name -> PTerm -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> t -> PArg' t
PTacImplicit 0 [ArgOpt]
os Name
n PTerm
s PTerm
t
recName :: Name
recName :: Name
recName = Int -> String -> Name
sMN 0 "rec"
recRef :: PTerm
recRef = FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] Name
recName
projectInType :: [(Name, Name)] -> PTerm -> PTerm
projectInType :: [(Name, Name)] -> PTerm -> PTerm
projectInType xs :: [(Name, Name)]
xs = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
st
where
st :: PTerm -> PTerm
st :: PTerm -> PTerm
st (PRef fc :: FC
fc hls :: [FC]
hls n :: Name
n)
| Just pn :: 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 t :: PTerm
t = PTerm
t
asPRefArg :: Plicity -> Name -> PArg
asPRefArg :: Plicity -> Name -> PArg
asPRefArg p :: Plicity
p n :: 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)