@@ -11,6 +11,7 @@ import Idris.ElabTerm
1111import Idris.Coverage
1212import Idris.IBC
1313import Idris.Unlit
14+import Idris.Providers
1415import Paths_idris
1516
1617import Core.CoreParser
@@ -339,7 +340,7 @@ pDecl syn = do notEndBlock
339340 <|> pClass syn
340341 <|> pInstance syn
341342 <|> do d <- pDSL syn; return [d]
342− <|> pDirective
343+ <|> pDirective syn
343344 <|> try (do reserved "import"; fp <- identifier
344345 fail "imports must be at the top of file")
345346
@@ -1456,34 +1457,55 @@ pWhereblock n syn
14561457 closeBlock
14571458 return (concat ds, map (\x -> (x, decoration syn x)) dns)
14581459
1459−pDirective :: IParser [PDecl]
1460−pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1461− return [PDirective (do addLib lib
1462− addIBC (IBCLib lib))])
1463− <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1464− return [PDirective (do datadir <- liftIO getDataDir
1465− o <- liftIO $ findInPath [".", datadir] obj
1466− addIBC (IBCObj o)
1467− addObjectFile o)])
1468− <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1469− return [PDirective (do addHdr hdr
1470− addIBC (IBCHeader hdr))])
1471− <|> try (do lchar '%'; reserved "hide"; n <- iName []
1472− return [PDirective (do setAccessibility n Hidden
1473− addIBC (IBCAccess n Hidden))])
1474− <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1475− return [PDirective (do setAccessibility n Frozen
1476− addIBC (IBCAccess n Frozen))])
1477− <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1478− return [PDirective (do i <- getIState
1479− putIState (i { default_access = acc }))])
1480− <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1481− i <- getState
1482− setState (i { default_total = tot } )
1483− return [PDirective (do i <- getIState
1484− putIState (i { default_total = tot }))])
1485− <|> try (do lchar '%'; reserved "logging"; i <- natural;
1486− return [PDirective (setLogLevel (fromInteger i))])
1460+pDirective :: SyntaxInfo -> IParser [PDecl]
1461+pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;
1462+ return [PDirective (do addLib lib
1463+ addIBC (IBCLib lib))])
1464+ <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1465+ return [PDirective (do datadir <- liftIO getDataDir
1466+ o <- liftIO $ findInPath [".", datadir] obj
1467+ addIBC (IBCObj o)
1468+ addObjectFile o)])
1469+ <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1470+ return [PDirective (do addHdr hdr
1471+ addIBC (IBCHeader hdr))])
1472+ <|> try (do lchar '%'; reserved "hide"; n <- iName []
1473+ return [PDirective (do setAccessibility n Hidden
1474+ addIBC (IBCAccess n Hidden))])
1475+ <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1476+ return [PDirective (do setAccessibility n Frozen
1477+ addIBC (IBCAccess n Frozen))])
1478+ <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1479+ return [PDirective (do i <- getIState
1480+ putIState (i { default_access = acc }))])
1481+ <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1482+ i <- getState
1483+ setState (i { default_total = tot } )
1484+ return [PDirective (do i <- getIState
1485+ putIState (i { default_total = tot }))])
1486+ <|> try (do lchar '%'; reserved "logging"; i <- natural;
1487+ return [PDirective (setLogLevel (fromInteger i))])
1488+ <|> try (do lchar '%'; reserved "provide";
1489+ lchar '('; n <- pfName; t <- pTSig syn; lchar ')'
1490+ fc <- pfc
1491+ -- pack into provider
1492+ let expected = providerTy fc t
1493+ reserved "with"
1494+ e <- pExpr syn
1495+ return [PDirective (do logLvl 1 $ "** Providing " ++
1496+ show n ++ " : " ++ show expected ++
1497+ " as " ++ show e
1498+ i <- getIState
1499+ (e', et) <- elabVal toplevel False e
1500+ ctxt <- getContext
1501+ ist <- get
1502+ let e'' = normaliseAll ctxt [] e'
1503+ let et' = normaliseAll ctxt [] et
1504+ logLvl 1 $ "** Elaborated: " ++ show e' ++ " :as: " ++ show et
1505+ logLvl 1 $ "** Evaluated: " ++ show e'' ++ " :as: " ++ show et'
1506+
1507+
1508+ )])
14871509
14881510pTactic :: SyntaxInfo -> IParser PTactic
14891511pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')