module Idris.ParseData where
import Prelude hiding (pi)
import Text.Trifecta.Delta
import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)
import Text.Parser.LookAhead
import Text.Parser.Expression
import qualified Text.Parser.Token as Tok
import qualified Text.Parser.Char as Chr
import qualified Text.Parser.Token.Highlight as Hi
import Idris.AbsSyntax
import Idris.ParseHelpers
import Idris.ParseOps
import Idris.ParseExpr
import Idris.DSL
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Docstrings
import Control.Applicative
import Control.Monad
import Control.Monad.State.Strict
import Data.Maybe
import qualified Data.List.Split as Spl
import Data.List
import Data.Monoid
import Data.Char
import qualified Data.HashSet as HS
import qualified Data.Text as T
import qualified Data.ByteString.UTF8 as UTF8
import Debug.Trace
record :: SyntaxInfo -> IdrisParser PDecl
record syn = do (doc, argDocs, acc, opts) <- try (do
(doc, argDocs) <- option noDocs docComment
ist <- get
let doc' = annotCode (tryFullExpr syn ist) doc
argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
| (n, d) <- argDocs ]
acc <- optional accessibility
opts <- dataOpts []
reserved "record"
return (doc', argDocs', acc, opts))
fc <- getFC
tyn_in <- fnName
lchar ':'
ty <- typeExpr (allowImp syn)
let tyn = expandNS syn tyn_in
reserved "where"
(cdoc, cargDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)
accData acc tyn [cn]
let rsyn = syn { syn_namespace = show (nsroot tyn) :
syn_namespace syn }
let fns = getRecNames rsyn cty
mapM_ (\n -> addAcc n acc) fns
return $ PRecord doc rsyn fc tyn ty opts cdoc cn cty
<?> "record type declaration"
where
getRecNames :: SyntaxInfo -> PTerm -> [Name]
getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
++ getRecNames syn sc
getRecNames _ _ = []
toFreeze :: Maybe Accessibility -> Maybe Accessibility
toFreeze (Just Frozen) = Just Hidden
toFreeze x = x
dataI :: IdrisParser DataOpts
dataI = do reserved "data"; return []
<|> do reserved "codata"; return [Codata]
dataOpts :: DataOpts -> IdrisParser DataOpts
dataOpts opts
= do reserved "%elim"; dataOpts (DefaultEliminator : DefaultCaseFun : opts)
<|> do reserved "%case"; dataOpts (DefaultCaseFun : opts)
<|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
<|> return opts
<?> "data options"
data_ :: SyntaxInfo -> IdrisParser PDecl
data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
(doc, argDocs) <- option noDocs docComment
pushIndent
acc <- optional accessibility
elim <- dataOpts []
co <- dataI
ist <- get
let dataOpts = combineDataOpts (elim ++ co)
doc' = annotCode (tryFullExpr syn ist) doc
argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
| (n, d) <- argDocs ]
return (doc', argDocs', acc, dataOpts))
fc <- getFC
tyn_in <- fnName
(do try (lchar ':')
popIndent
ty <- typeExpr (allowImp syn)
let tyn = expandNS syn tyn_in
option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do
reserved "where"
cons <- indentedBlock (constructor syn)
accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons)
return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do
args <- many name
let ty = bindArgs (map (const PType) args) PType
let tyn = expandNS syn tyn_in
option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do
try (lchar '=') <|> do reserved "where"
let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "
let n = show tyn_in ++ " "
let s = kw ++ n
let as = concat (intersperse " " $ map show args) ++ " "
let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
let ss = concat (intersperse " -> " $ map (const "Type") args)
let fix1 = s ++ as ++ " = ..."
let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")
terminator
let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
cons' <- mapM (\ (doc, argDocs, x, cargs, cfc, fs) ->
do let cty = bindArgs cargs conty
return (doc, argDocs, x, cty, cfc, fs)) cons
accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons')
return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons')))
<?> "data type declaration"
where
mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
mkPApp fc t [] = t
mkPApp fc t xs = PApp fc t (map pexp xs)
bindArgs :: [PTerm] -> PTerm -> PTerm
bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs
combineDataOpts :: DataOpts -> DataOpts
combineDataOpts opts = if Codata `elem` opts
then delete DefaultEliminator opts
else opts
constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name])
constructor syn
= do (doc, argDocs) <- option noDocs docComment
cn_in <- fnName; fc <- getFC
let cn = expandNS syn cn_in
lchar ':'
fs <- option [] (do lchar '%'; reserved "erase"
sepBy1 name (lchar ','))
ty <- typeExpr (allowImp syn)
ist <- get
let doc' = annotCode (tryFullExpr syn ist) doc
argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
| (n, d) <- argDocs ]
return (doc', argDocs', cn, ty, fc, fs)
<?> "constructor"
simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, [PTerm], FC, [Name])
simpleConstructor syn
= do (doc, _) <- option noDocs (try docComment)
ist <- get
let doc' = annotCode (tryFullExpr syn ist) doc
cn_in <- fnName
let cn = expandNS syn cn_in
fc <- getFC
args <- many (do notEndApp
simpleExpr syn)
return (doc', [], cn, args, fc, [])
<?> "constructor"
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl syn = do reserved "dsl"
n <- fnName
bs <- indentedBlock (overload syn)
let dsl = mkDSL bs (dsl_info syn)
checkDSL dsl
i <- get
put (i { idris_dsls = addDef n dsl (idris_dsls i) })
return (PDSL n dsl)
<?> "dsl block declaration"
where mkDSL :: [(String, PTerm)] -> DSL -> DSL
mkDSL bs dsl = let var = lookup "variable" bs
first = lookup "index_first" bs
next = lookup "index_next" bs
leto = lookup "let" bs
lambda = lookup "lambda" bs
pi = lookup "pi" bs in
initDSL { dsl_var = var,
index_first = first,
index_next = next,
dsl_lambda = lambda,
dsl_let = leto,
dsl_pi = pi }
checkDSL :: DSL -> IdrisParser ()
checkDSL dsl = return ()
overload :: SyntaxInfo -> IdrisParser (String, PTerm)
overload syn = do o <- identifier <|> do reserved "let"
return "let"
if o `notElem` overloadable
then fail $ show o ++ " is not an overloading"
else do
lchar '='
t <- expr syn
return (o, t)
<?> "dsl overload declaratioN"
where overloadable = ["let","lambda","pi","index_first","index_next","variable"]