58774fe · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

@@ -12,6 +12,7 @@ New in 0.9.13:

12* New (first class) nested record update/access syntax:

13 record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val

14 record { a->b->c } x -- accesses field, equivalent to c (b (a x))

15+* The banner at startup can be suppressed by adding :set nobanner to the initialisation script.

15

16

16Internal changes

17Internal changes

17

18

libs/prelude/Prelude/Bool.idr+5

@@ -2,6 +2,8 @@ module Prelude.Bool

2

3import Builtins

4

5+import Prelude.Uninhabited

6+

5||| Boolean Data Type

7||| Boolean Data Type

6data Bool = False | True

8data Bool = False | True

7

9

@@ -16,6 +18,9 @@ boolElim False t e = e

16||| Defines a predicate on Bool which guarantees that the value is true.

18||| Defines a predicate on Bool which guarantees that the value is true.

17data so : Bool -> Type where oh : so True

19data so : Bool -> Type where oh : so True

18

20

21+instance Uninhabited (so False) where

22+ uninhabited oh impossible

23+

19-- Syntactic sugar for boolean elimination.

24-- Syntactic sugar for boolean elimination.

20syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

25syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

21

26

src/IRTS/CodegenJavaScript.hs+77−27

@@ -740,21 +740,44 @@ removeIDs js =

740 JSReturn (JSApp (JSIdent fun) args)

741 )])

742 | Just pos <- lookup fun ids

743− , pos < length args = args !! pos

743+ , pos < length args = removeIDCall ids (args !! pos)

744

745 removeIDCall ids (JSNew _ [JSFunction [] (

746 JSReturn (JSApp (JSIdent fun) args)

747 )])

748 | Just pos <- lookup fun ids

749− , pos < length args = args !! pos

749+ , pos < length args = removeIDCall ids (args !! pos)

750

751 removeIDCall ids js@(JSApp id@(JSIdent fun) args)

752 | Just pos <- lookup fun ids

753− , pos < length args = args !! pos

753+ , pos < length args = removeIDCall ids (args !! pos)

754

755 removeIDCall ids js = transformJS (removeIDCall ids) js

756

757

758+inlineFunction :: String -> [String] -> JS -> JS -> JS

759+inlineFunction fun args body js = inline' js

760+ where

761+ inline' :: JS -> JS

762+ inline' (JSApp (JSIdent name) vals)

763+ | name == fun =

764+ let (js, phs) = insertPlaceHolders args body in

765+ inline' $ foldr (uncurry jsSubst) js (zip phs vals)

766+

767+ inline' js = transformJS inline' js

768+

769+ insertPlaceHolders :: [String] -> JS -> (JS, [JS])

770+ insertPlaceHolders args body = insertPlaceHolders' args body []

771+ where

772+ insertPlaceHolders' :: [String] -> JS -> [JS] -> (JS, [JS])

773+ insertPlaceHolders' (a:as) body ph

774+ | (body', ph') <- insertPlaceHolders' as body ph =

775+ let phvar = JSIdent $ "__PH_" ++ show (length ph') in

776+ (jsSubst (JSIdent a) phvar body', phvar : ph')

777+

778+ insertPlaceHolders' [] body ph = (body, ph)

779+

780+

758inlineFunctions :: [JS] -> [JS]

781inlineFunctions :: [JS] -> [JS]

759inlineFunctions js =

782inlineFunctions js =

760 inlineHelper ([], js)

783 inlineHelper ([], js)

@@ -766,7 +789,7 @@ inlineFunctions js =

766 | Just new <- inlineAble (

789 | Just new <- inlineAble (

767 countAll fun front + countAll fun back

790 countAll fun front + countAll fun back

768 ) fun args body =

791 ) fun args body =

769− let f = map (inline fun args new) in

792+ let f = map (inlineFunction fun args new) in

770 inlineHelper (f front, f back)

793 inlineHelper (f front, f back)

771

794

772 inlineHelper (front, next:back) = inlineHelper (front ++ [next], back)

795 inlineHelper (front, next:back) = inlineHelper (front ++ [next], back)

@@ -783,29 +806,6 @@ inlineFunctions js =

783 inlineAble _ _ _ _ = Nothing

806 inlineAble _ _ _ _ = Nothing

784

807

785

808

786− inline :: String -> [String] -> JS -> JS -> JS

787− inline fun args body js = inline' js

788− where

789− inline' :: JS -> JS

790− inline' (JSApp (JSIdent name) vals)

791− | name == fun =

792− let (js, phs) = insertPlaceHolders args body in

793− inline' $ foldr (uncurry jsSubst) js (zip phs vals)

794−

795− inline' js = transformJS inline' js

796−

797− insertPlaceHolders :: [String] -> JS -> (JS, [JS])

798− insertPlaceHolders args body = insertPlaceHolders' args body []

799− where

800− insertPlaceHolders' :: [String] -> JS -> [JS] -> (JS, [JS])

801− insertPlaceHolders' (a:as) body ph

802− | (body', ph') <- insertPlaceHolders' as body ph =

803− let phvar = JSIdent $ "__PH_" ++ show (length ph') in

804− (jsSubst (JSIdent a) phvar body', phvar : ph')

805−

806− insertPlaceHolders' [] body ph = (body, ph)

807−

808−

809 nonRecur :: String -> JS -> Bool

810 nonRecur name body = countInvokations name body == 0

811

@@ -1416,6 +1416,54 @@ evalCons js =

1416 match js = transformJS match js

1417

1418

1419+elimConds :: [JS] -> [JS]

1420+elimConds js =

1421+ let (conds, rest) = partition isCond js in

1422+ foldl' eraseCond rest conds

1423+ where

1424+ isCond :: JS -> Bool

1425+ isCond (JSAlloc

1426+ fun (Just (JSFunction args (JSCond

1427+ [ (JSBinOp "==" (JSNum (JSInt tag)) _, JSReturn (JSIdent _))

1428+ , (JSNoop, JSReturn (JSIdent _))

1429+ ]))

1430+ )) = True

1431+

1432+ isCond (JSAlloc

1433+ fun (Just (JSFunction args (JSCond

1434+ [ (JSBinOp "==" _ (JSNum (JSInt tag)), JSReturn (JSIdent _))

1435+ , (JSNoop, JSReturn (JSIdent _))

1436+ ]))

1437+ )) = True

1438+

1439+ isCond _ = False

1440+

1441+

1442+ eraseCond :: [JS] -> JS -> [JS]

1443+ eraseCond js (JSAlloc

1444+ fun (Just (JSFunction args (JSCond

1445+ [ (c, JSReturn t)

1446+ , (_, JSReturn f)

1447+ ])

1448+ )

1449+ )) = map (inlineFunction fun args (JSTernary c t f)) js

1450+

1451+

1452+removeUselessCons :: [JS] -> [JS]

1453+removeUselessCons js =

1454+ let (cons, rest) = partition isUseless js in

1455+ foldl' eraseCon rest cons

1456+ where

1457+ isUseless :: JS -> Bool

1458+ isUseless (JSAlloc fun (Just JSNull)) = True

1459+ isUseless (JSAlloc fun (Just (JSIdent _))) = True

1460+ isUseless _ = False

1461+

1462+

1463+ eraseCon :: [JS] -> JS -> [JS]

1464+ eraseCon js (JSAlloc fun (Just val)) = map (jsSubst (JSIdent fun) val) js

1465+

1466+

1419getGlobalCons :: JS -> [(String, JS)]

1467getGlobalCons :: JS -> [(String, JS)]

1420getGlobalCons js = foldJS match (++) [] js

1468getGlobalCons js = foldJS match (++) [] js

1421 where

1469 where

@@ -1517,6 +1565,8 @@ codegenJS_all target definitions includes filename outputType = do

1517 , extractLocalConstructors

1565 , extractLocalConstructors

1518 , unfoldLookupTable

1566 , unfoldLookupTable

1519 , evalCons

1567 , evalCons

1568+ , elimConds

1569+ , removeUselessCons

1520 ]

1570 ]

1521

1571

1522 functions :: [String]

1572 functions :: [String]

src/Idris/AbsSyntax.hs+3−1

@@ -947,6 +947,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

947 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r

948 bnames _ = []

949

950+-- | Expands parameters defined in parameter and where blocks inside of declarations

950expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

951expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

951 = PData doc argDocs syn fc co (expandPData pd)

952 = PData doc argDocs syn fc co (expandPData pd)

952 where

953 where

@@ -972,11 +973,12 @@ expandParamsD rhs ist dec ps ns (PParams f params pds)

972-- (map (expandParamsD ist dec ps ns) pds)

973-- (map (expandParamsD ist dec ps ns) pds)

973expandParamsD rhs ist dec ps ns (PMutual f pds)

974expandParamsD rhs ist dec ps ns (PMutual f pds)

974 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

975 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

975−expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)

976+expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)

976 = PClass doc info f

977 = PClass doc info f

977 (map (expandParams dec ps ns []) cs)

978 (map (expandParams dec ps ns []) cs)

978 n

979 n

979 (map (mapsnd (expandParams dec ps ns [])) params)

980 (map (mapsnd (expandParams dec ps ns [])) params)

981+ pDocs

980 (map (expandParamsD rhs ist dec ps ns) decls)

982 (map (expandParamsD rhs ist dec ps ns) decls)

981expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)

983expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)

982 = PInstance info f

984 = PInstance info f

src/Idris/AbsSyntaxTree.hs+38−11

@@ -31,6 +31,7 @@ import qualified Data.Map as M

31import Data.Either

32import qualified Data.Set as S

33import Data.Word (Word)

34+import Data.Maybe (fromMaybe)

34

35

35import Debug.Trace

36import Debug.Trace

36

37

@@ -487,6 +488,7 @@ data PDecl' t

487 [t] -- constraints

488 [t] -- constraints

488 Name

489 Name

489 [(Name, t)] -- parameters

490 [(Name, t)] -- parameters

491+ [(Name, Docstring)] -- parameter docstrings

490 [PDecl' t] -- declarations

492 [PDecl' t] -- declarations

491 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

493 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

492 -- class name, parameters, method declarations

494 -- class name, parameters, method declarations

@@ -569,7 +571,7 @@ declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

569declared (PParams _ _ ds) = concatMap declared ds

571declared (PParams _ _ ds) = concatMap declared ds

570declared (PNamespace _ ds) = concatMap declared ds

572declared (PNamespace _ ds) = concatMap declared ds

571declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

573declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

572−declared (PClass _ _ _ _ n _ ms) = n : concatMap declared ms

574+declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

573declared (PInstance _ _ _ _ _ _ _ _) = []

575declared (PInstance _ _ _ _ _ _ _ _) = []

574declared (PDSL n _) = [n]

576declared (PDSL n _) = [n]

575declared (PSyntax _ _) = []

577declared (PSyntax _ _) = []

@@ -588,7 +590,7 @@ tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

588tldeclared (PParams _ _ ds) = []

590tldeclared (PParams _ _ ds) = []

589tldeclared (PMutual _ ds) = concatMap tldeclared ds

591tldeclared (PMutual _ ds) = concatMap tldeclared ds

590tldeclared (PNamespace _ ds) = concatMap tldeclared ds

592tldeclared (PNamespace _ ds) = concatMap tldeclared ds

591−tldeclared (PClass _ _ _ _ n _ ms) = concatMap tldeclared ms

593+tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

592tldeclared (PInstance _ _ _ _ _ _ _ _) = []

594tldeclared (PInstance _ _ _ _ _ _ _ _) = []

593tldeclared _ = []

595tldeclared _ = []

594

596

@@ -604,7 +606,7 @@ defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

604defined (PParams _ _ ds) = concatMap defined ds

606defined (PParams _ _ ds) = concatMap defined ds

605defined (PNamespace _ ds) = concatMap defined ds

607defined (PNamespace _ ds) = concatMap defined ds

606defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

608defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

607−defined (PClass _ _ _ _ n _ ms) = n : concatMap defined ms

609+defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

608defined (PInstance _ _ _ _ _ _ _ _) = []

610defined (PInstance _ _ _ _ _ _ _ _) = []

609defined (PDSL n _) = [n]

611defined (PDSL n _) = [n]

610defined (PSyntax _ _) = []

612defined (PSyntax _ _) = []

@@ -1065,7 +1067,7 @@ eqOpts = []

1065elimName = sUN "__Elim"

1067elimName = sUN "__Elim"

1066elimMethElimTy = sUN "__elimTy"

1068elimMethElimTy = sUN "__elimTy"

1067elimMethElim = sUN "elim"

1069elimMethElim = sUN "elim"

1068−elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1070+elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)] []

1069 [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1071 [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1070 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1072 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1071

1073

@@ -1126,19 +1128,24 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1126 colour UnderlineText = IdrisColour Nothing True True False False

1128 colour UnderlineText = IdrisColour Nothing True True False False

1127 colour ItalicText = IdrisColour Nothing True False False True

1129 colour ItalicText = IdrisColour Nothing True False False True

1128

1130

1129−-- | Pretty-print a high-level closed Idris term

1131+-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1130prettyImp :: Bool -- ^^ whether to show implicits

1132prettyImp :: Bool -- ^^ whether to show implicits

1131 -> PTerm -- ^^ the term to pretty-print

1133 -> PTerm -- ^^ the term to pretty-print

1132 -> Doc OutputAnnotation

1134 -> Doc OutputAnnotation

1133−prettyImp impl = pprintPTerm impl [] []

1135+prettyImp impl = pprintPTerm impl [] [] []

1134

1136

1137+-- | Do the right thing for rendering a term in an IState

1138+prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1139+prettyIst ist = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist)

1140+

1135−-- | Pretty-print a high-level Idris term in some bindings context

1141+-- | Pretty-print a high-level Idris term in some bindings context with infix info

1136pprintPTerm :: Bool -- ^^ whether to show implicits

1142pprintPTerm :: Bool -- ^^ whether to show implicits

1137 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1143 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1138 -> [Name] -- ^^ names to always show in pi, even if not used

1144 -> [Name] -- ^^ names to always show in pi, even if not used

1145+ -> [FixDecl] -- ^^ Fixity declarations

1139 -> PTerm -- ^^ the term to pretty-print

1146 -> PTerm -- ^^ the term to pretty-print

1140 -> Doc OutputAnnotation

1147 -> Doc OutputAnnotation

1141−pprintPTerm impl bnd docArgs = prettySe 10 bnd

1148+pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1142 where

1149 where

1143 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1150 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1144 prettySe p bnd (PQuote r) =

1151 prettySe p bnd (PQuote r) =

@@ -1203,13 +1210,23 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1203 case getExps args of

1210 case getExps args of

1204 [] -> enclose lparen rparen opName

1211 [] -> enclose lparen rparen opName

1205 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

1212 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

1213+ [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1206− [l,r] -> bracket p 1 $ inFix l r

1214+ in bracket p precedence $ inFix l r

1207 (l:r:rest) -> bracket p 1 $

1215 (l:r:rest) -> bracket p 1 $

1208 enclose lparen rparen (inFix l r) <+>

1216 enclose lparen rparen (inFix l r) <+>

1209 align (group (vsep (map (prettyArgSe bnd) rest)))

1217 align (group (vsep (map (prettyArgSe bnd) rest)))

1210 where opName = prettyName impl bnd op

1218 where opName = prettyName impl bnd op

1219+ f = getFixity (opStr op)

1220+ left l = case f of

1221+ Nothing -> prettySe (-1) bnd l

1222+ Just (Infixl p') -> prettySe p' bnd l

1223+ Just f' -> prettySe (prec f'-1) bnd l

1224+ right r = case f of

1225+ Nothing -> prettySe (-1) bnd r

1226+ Just (Infixr p') -> prettySe p' bnd r

1227+ Just f' -> prettySe (prec f'-1) bnd r

1211 inFix l r = align . group $

1228 inFix l r = align . group $

1212− (prettySe 1 bnd l <+> opName) <$> group (prettySe 0 bnd r)

1229+ (left l <+> opName) <$> group (right r)

1213 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1230 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1214 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1231 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1215 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1232 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

@@ -1314,6 +1331,10 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1314 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1331 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1315 annName n = annotate (AnnName n Nothing Nothing Nothing)

1332 annName n = annotate (AnnName n Nothing Nothing Nothing)

1316

1333

1334+ opStr :: Name -> String

1335+ opStr (NS n _) = opStr n

1336+ opStr (UN n) = T.unpack n

1337+

1317 basename :: Name -> Name

1338 basename :: Name -> Name

1318 basename (NS n _) = basename n

1339 basename (NS n _) = basename n

1319 basename n = n

1340 basename n = n

@@ -1367,6 +1388,12 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1367

1388

1368 kwd = annotate AnnKeyword . text

1389 kwd = annotate AnnKeyword . text

1369

1390

1391+ fixities :: M.Map String Fixity

1392+ fixities = M.fromList [(s, f) | (Fix f s) <- infixes]

1393+

1394+ getFixity :: String -> Maybe Fixity

1395+ getFixity = flip M.lookup fixities

1396+

1370-- | Pretty-printer helper for the binding site of a name

1397-- | Pretty-printer helper for the binding site of a name

1371bindingOf :: Name -- ^^ the bound name

1398bindingOf :: Name -- ^^ the bound name

1372 -> Bool -- ^^ whether the name is implicit

1399 -> Bool -- ^^ whether the name is implicit

@@ -1419,7 +1446,7 @@ showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

1419showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1446showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1420showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1447showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1421showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1448showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1422−showDeclImp i (PClass _ _ _ cs n ps ds)

1449+showDeclImp i (PClass _ _ _ cs n ps _ ds)

1423 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds

1450 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds

1424showDeclImp i (PInstance _ _ cs n _ t _ ds)

1451showDeclImp i (PInstance _ _ cs n _ t _ ds)

1425 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds

1452 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds

src/Idris/CaseSplit.hs+4−1

@@ -22,6 +22,7 @@ import Idris.Core.Evaluate

22

23import Data.Maybe

24import Data.Char

25+import Data.List (isPrefixOf, isSuffixOf)

25import Control.Monad

26import Control.Monad

26import Control.Monad.State.Strict

27import Control.Monad.State.Strict

27

28

@@ -299,7 +300,9 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

299 else c : updatePat (not (isAlphaNum c)) n tm rest

300 else c : updatePat (not (isAlphaNum c)) n tm rest

300 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest

301 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest

301

302

302− addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"

303+ addBrackets tm | ' ' `elem` tm

304+ , not (isPrefixOf "(" tm)

305+ , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"

303 | otherwise = tm

306 | otherwise = tm

304

307

305getUniq nm i

308getUniq nm i

src/Idris/Chaser.hs+1−1

@@ -82,7 +82,7 @@ buildTree built fp = btree [] fp

82 iLOG $ "CHASING " ++ show file

83 ibcsd <- valIBCSubDir i

84 ids <- allImportDirs

85− fp <- runIO $ findImport ids ibcsd file

85+ fp <- findImport ids ibcsd file

86 iLOG $ "Found " ++ show fp

87 mt <- runIO $ getIModTime fp

88 if (file `elem` built)

src/Idris/Completion.hs+1

@@ -112,6 +112,7 @@ completeOption = completeWord Nothing " \t" completeOpt

112 , "showimplicits"

113 , "originalerrors"

114 , "autosolve"

115+ , "nobanner"

115 ]

116 ]

116

117

117completeConsoleWidth :: CompletionFunc Idris

118completeConsoleWidth :: CompletionFunc Idris

src/Idris/Core/Execute.hs+13−1

@@ -220,7 +220,7 @@ execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)

220-- Special cases arising from not having access to the C RTS in the interpreter

221execApp env ctxt (EP _ fp _) (_:fn:str:_:rest)

222 | fp == mkfprim,

223− Just (FFun "putStr" _ _) <- foreignFromTT fn

223+ Just (FFun "putStr" _ _) <- foreignFromTT fn

224 = case str of

225 EConstant (Str arg) -> do execIO (putStr arg)

226 execApp env ctxt ioUnit rest

@@ -228,6 +228,18 @@ execApp env ctxt (EP _ fp _) (_:fn:str:_:rest)

228 "The argument to putStr should be a constant string, but it was " ++

229 show str ++

230 ". Are all cases covered?"

231+execApp env ctxt (EP _ fp _) (_:fn:ch:_:rest)

232+ | fp == mkfprim,

233+ Just (FFun "putchar" _ _) <- foreignFromTT fn

234+ = case ch of

235+ EConstant (Ch c) -> do execIO (putChar c)

236+ execApp env ctxt ioUnit rest

237+ EConstant (I i) -> do execIO (putChar (toEnum i))

238+ execApp env ctxt ioUnit rest

239+ _ -> execFail . Msg $

240+ "The argument to putchar should be a constant character, but it was " ++

241+ show str ++

242+ ". Are all cases covered?"

231execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)

243execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)

232 | fp == mkfprim,

244 | fp == mkfprim,

233 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

245 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

src/Idris/DeepSeq.hs+2−2

@@ -143,10 +143,10 @@ instance (NFData t) => NFData (PDecl' t) where

143 rnf x2 `seq`

144 rnf x3 `seq`

145 rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

146− rnf (PClass x1 x2 x3 x4 x5 x6 x7)

146+ rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7)

147 = rnf x1 `seq`

148 rnf x2 `seq`

149− rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

149+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

150 rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

151 = rnf x1 `seq`

152 rnf x2 `seq`

src/Idris/Delaborate.hs+1−1

@@ -138,7 +138,7 @@ pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

138pprintTerm ist = pprintTerm' ist []

139

140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

141−pprintTerm' ist bnd tm = pprintPTerm (opt_showimp (idris_options ist)) bnd [] tm

141+pprintTerm' ist bnd = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist)

142

143pprintErr :: IState -> Err -> Doc OutputAnnotation

144pprintErr i err = pprintErr' i (fmap (errReverse i) err)

src/Idris/Docs.hs+40−23

@@ -1,5 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Docs where

2+module Idris.Docs (pprintDocs, getDocs, FunDoc(..), Docs (..)) where

3

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

@@ -34,11 +34,11 @@ data Docs = FunDoc FunDoc

34showDoc d | nullDocstring d = empty

35 | otherwise = text " -- " <> renderDocstring d

36

37−pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

37+pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

38−pprintFD imp (FD n doc args ty f)

38+pprintFD ist (FD n doc args ty f)

39 = nest 4 (prettyName imp [] n <+> colon <+>

40 pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args

41− , not (T.isPrefixOf (T.pack "__") n') ] ty <$>

41+ , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

42 renderDocstring doc <$>

43 maybe empty (\f -> text (show f) <> line) f <>

44 let argshow = showArgs args [] in

@@ -46,21 +46,23 @@ pprintFD imp (FD n doc args ty f)

46 then nest 4 $ text "Arguments:" <$> vsep argshow

47 else empty)

48

49+ where imp = opt_showimp (idris_options ist)

50+ infixes = idris_infixes ist

49− where showArgs ((n, ty, Exp {}, Just d):args) bnd

51+ showArgs ((n, ty, Exp {}, Just d):args) bnd

50 = bindingOf n False <+> colon <+>

52 = bindingOf n False <+> colon <+>

51− pprintPTerm imp bnd [] ty <>

53+ pprintPTerm imp bnd [] infixes ty <>

52 showDoc d <> line

54 showDoc d <> line

53 :

55 :

54 showArgs args ((n, False):bnd)

56 showArgs args ((n, False):bnd)

55 showArgs ((n, ty, Constraint {}, Just d):args) bnd

57 showArgs ((n, ty, Constraint {}, Just d):args) bnd

56 = text "Class constraint" <+>

58 = text "Class constraint" <+>

57− pprintPTerm imp bnd [] ty <> showDoc d <> line

59+ pprintPTerm imp bnd [] infixes ty <> showDoc d <> line

58 :

60 :

59 showArgs args ((n, True):bnd)

61 showArgs args ((n, True):bnd)

60 showArgs ((n, ty, Imp {}, Just d):args) bnd

62 showArgs ((n, ty, Imp {}, Just d):args) bnd

61 = text "(implicit)" <+>

63 = text "(implicit)" <+>

62 bindingOf n True <+> colon <+>

64 bindingOf n True <+> colon <+>

63− pprintPTerm imp bnd [] ty <>

65+ pprintPTerm imp bnd [] infixes ty <>

64 showDoc d <> line

66 showDoc d <> line

65 :

67 :

66 showArgs args ((n, True):bnd)

68 showArgs args ((n, True):bnd)

@@ -68,20 +70,20 @@ pprintFD imp (FD n doc args ty f)

68 showArgs [] _ = []

70 showArgs [] _ = []

69

71

70

72

71−pprintDocs :: Bool -> Docs -> Doc OutputAnnotation

73+pprintDocs :: IState -> Docs -> Doc OutputAnnotation

72−pprintDocs imp (FunDoc d) = pprintFD imp d

74+pprintDocs ist (FunDoc d) = pprintFD ist d

73−pprintDocs imp (DataDoc t args)

75+pprintDocs ist (DataDoc t args)

74− = text "Data type" <+> pprintFD imp t <$>

76+ = text "Data type" <+> pprintFD ist t <$>

75 nest 4 (text "Constructors:" <> line <>

77 nest 4 (text "Constructors:" <> line <>

76− vsep (map (pprintFD imp) args))

78+ vsep (map (pprintFD ist) args))

77−pprintDocs imp (ClassDoc n doc meths params instances)

79+pprintDocs ist (ClassDoc n doc meths params instances)

78 = nest 4 (text "Type class" <+> prettyName imp [] n <>

80 = nest 4 (text "Type class" <+> prettyName imp [] n <>

79 if nullDocstring doc then empty else line <> renderDocstring doc)

81 if nullDocstring doc then empty else line <> renderDocstring doc)

80 <> line <$>

82 <> line <$>

81 nest 4 (text "Parameters:" <$> prettyParameters)

83 nest 4 (text "Parameters:" <$> prettyParameters)

82 <> line <$>

84 <> line <$>

83 nest 4 (text "Methods:" <$>

85 nest 4 (text "Methods:" <$>

84− vsep (map (pprintFD imp) meths))

86+ vsep (map (pprintFD ist) meths))

85 <$>

87 <$>

86 nest 4 (text "Instances:" <$>

88 nest 4 (text "Instances:" <$>

87 vsep (if null instances' then [text "<no instances>"]

89 vsep (if null instances' then [text "<no instances>"]

@@ -89,16 +91,32 @@ pprintDocs imp (ClassDoc n doc meths params instances)

89 <>

91 <>

90 if null subclasses then empty

92 if null subclasses then empty

91 else line <$> nest 4 (text "Subclasses:" <$>

93 else line <$> nest 4 (text "Subclasses:" <$>

92− vsep (map (dumpInstance . remConstraint) subclasses))

94+ vsep (map (dumpInstance . prettifySubclasses) subclasses))

93 where

95 where

94− params' = map (\x -> (fst x, False)) params

96+ params' = zip pNames (repeat False)

97+

98+ pNames = map fst params

99+

100+ imp = opt_showimp (idris_options ist)

101+ infixes = idris_infixes ist

95

102

96 dumpInstance :: PTerm -> Doc OutputAnnotation

103 dumpInstance :: PTerm -> Doc OutputAnnotation

97− dumpInstance = pprintPTerm imp params' []

104+ dumpInstance = pprintPTerm imp params' [] infixes

105+

106+ prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm

107+ prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)

108+ prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args

109+ prettifySubclasses tm = tm

110+

111+ safeHead _ (y:_) = y

112+ safeHead x [] = x

113+

114+ updateArgs (p:ps) ((PExp prty opts _ ref):as) = (PExp prty opts p (updateRef p ref)) : updateArgs ps as

115+ updateArgs ps (a:as) = a : updateArgs ps as

116+ updateArgs _ _ = []

98

117

99− remConstraint (PPi (Constraint _ _) _ tm _) = tm

118+ updateRef nm (PRef fc _) = PRef fc nm

100− remConstraint (PPi x y z pt) = PPi x y z (remConstraint pt)

119+ updateRef _ pt = pt

101− remConstraint p = p

102

120

103 hasConstraint (PPi (Constraint _ _) _ _ _) = True

121 hasConstraint (PPi (Constraint _ _) _ _ _) = True

104 hasConstraint (PPi _ _ _ pt) = hasConstraint pt

122 hasConstraint (PPi _ _ _ pt) = hasConstraint pt

@@ -107,7 +125,7 @@ pprintDocs imp (ClassDoc n doc meths params instances)

107 (subclasses, instances') = partition hasConstraint instances

125 (subclasses, instances') = partition hasConstraint instances

108

126

109 prettyParameters = if any (isJust . snd) params

127 prettyParameters = if any (isJust . snd) params

110− then vsep (map (\(n,md) -> prettyName False params' n <+> maybe empty showDoc md) params)

128+ then vsep (map (\(nm,md) -> prettyName False params' nm <+> maybe empty showDoc md) params)

111 else hsep (punctuate comma (map (prettyName False params' . fst) params))

129 else hsep (punctuate comma (map (prettyName False params' . fst) params))

112

130

113getDocs :: Name -> Idris Docs

131getDocs :: Name -> Idris Docs

@@ -129,7 +147,6 @@ docData n ti

129docClass :: Name -> ClassInfo -> Idris Docs

147docClass :: Name -> ClassInfo -> Idris Docs

130docClass n ci

148docClass n ci

131 = do i <- getIState

149 = do i <- getIState

132− ctxt <- getContext

133 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

150 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

134 docstr = maybe emptyDocstring fst docStrings

151 docstr = maybe emptyDocstring fst docStrings

135 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

152 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

src/Idris/ElabDecls.hs+13−11

@@ -365,12 +365,13 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

365

366type EliminatorState = StateT (Map.Map String Int) Idris

367

368−-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

368+-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

369elabEliminator :: [Int] -> Name -> PTerm ->

370 [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->

371 ElabInfo -> EliminatorState ()

372elabEliminator paramPos n ty cons info = do

373 elimLog $ "Elaborating eliminator"

374+ put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

374 let (cnstrs, _) = splitPi ty

375 let (cnstrs, _) = splitPi ty

375 let (splittedTy@(pms, idxs)) = splitPms cnstrs

376 let (splittedTy@(pms, idxs)) = splitPms cnstrs

376 generalParams <- namePis False pms

377 generalParams <- namePis False pms

@@ -389,13 +390,14 @@ elabEliminator paramPos n ty cons info = do

389 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

390 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

390 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

391 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

391 let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy

392 let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy

393+ elimLog elimSig

392 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

394 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

393 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

395 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

394 elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef

396 elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef

395 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

397 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

396 -- Do not elaborate clauses if there aren't any

398 -- Do not elaborate clauses if there aren't any

397 case eliminatorClauses of

399 case eliminatorClauses of

398− [] -> return ()

400+ [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type

399 _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())

401 _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())

400 where elimLog :: String -> EliminatorState ()

402 where elimLog :: String -> EliminatorState ()

401 elimLog s = State.lift (logLvl 2 s)

403 elimLog s = State.lift (logLvl 2 s)

@@ -458,9 +460,9 @@ elabEliminator paramPos n ty cons info = do

458 freshName key = do

460 freshName key = do

459 nameMap <- get

461 nameMap <- get

460 let i = fromMaybe 0 (Map.lookup key nameMap)

462 let i = fromMaybe 0 (Map.lookup key nameMap)

461− let name = key ++ show i

463+ let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)

462 put $ Map.insert key (i+1) nameMap

464 put $ Map.insert key (i+1) nameMap

463− return (sUN name)

465+ return name

464

466

465 scrutineeName :: Name

467 scrutineeName :: Name

466 scrutineeName = sUN "scrutinee"

468 scrutineeName = sUN "scrutinee"

@@ -553,7 +555,7 @@ elabEliminator paramPos n ty cons info = do

553 let cons' = replaceParams paramPos generalParameters ty

555 let cons' = replaceParams paramPos generalParameters ty

554 let (args, resTy) = splitPi cons'

556 let (args, resTy) = splitPi cons'

555 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

557 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

556− consArgs <- namePis True args

558+ consArgs <- namePis False args

557 let recArgs = findRecArgs consArgs

559 let recArgs = findRecArgs consArgs

558 let recMotives = map applyRecMotive recArgs

560 let recMotives = map applyRecMotive recArgs

559 let (_, consIdxs) = splitArgPms resTy

561 let (_, consIdxs) = splitArgPms resTy

@@ -592,7 +594,7 @@ elabEliminator paramPos n ty cons info = do

592 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

594 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

593 let (_, generalIdxs') = splitArgPms resTy

595 let (_, generalIdxs') = splitArgPms resTy

594 let generalIdxs = map pexp generalIdxs'

596 let generalIdxs = map pexp generalIdxs'

595− consArgs <- namePis True args

597+ consArgs <- namePis False args

596 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

598 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

597 let recArgs = findRecArgs consArgs

599 let recArgs = findRecArgs consArgs

598 let recElims = map applyRecElim recArgs

600 let recElims = map applyRecElim recArgs

@@ -1834,8 +1836,8 @@ data MArgTy = IA | EA | CA deriving Show

1834

1836

1835elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

1837elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

1836 FC -> [PTerm] ->

1838 FC -> [PTerm] ->

1837− Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1839+ Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()

1838−elabClass info syn doc fc constraints tn ps ds

1840+elabClass info syn doc fc constraints tn ps pDocs ds

1839 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

1841 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

1840 let tty = pibind ps PType

1842 let tty = pibind ps PType

1841 let constraint = PApp fc (PRef fc tn)

1843 let constraint = PApp fc (PRef fc tn)

@@ -1862,7 +1864,7 @@ elabClass info syn doc fc constraints tn ps ds

1862 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

1864 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

1863 let ddecl = PDatadecl tn tty cons

1865 let ddecl = PDatadecl tn tty cons

1864 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1866 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1865− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl

1867+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

1866 -- for each constraint, build a top level function to chase it

1868 -- for each constraint, build a top level function to chase it

1867 logLvl 5 $ "Building functions"

1869 logLvl 5 $ "Building functions"

1868 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

1870 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

@@ -2344,10 +2346,10 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

2344 ninfo = case namespace info of

2346 ninfo = case namespace info of

2345 Nothing -> info { namespace = Just [n] }

2347 Nothing -> info { namespace = Just [n] }

2346 Just ns -> info { namespace = Just (n:ns) }

2348 Just ns -> info { namespace = Just (n:ns) }

2347−elabDecl' what info (PClass doc s f cs n ps ds)

2349+elabDecl' what info (PClass doc s f cs n ps pdocs ds)

2348 | what /= EDefns

2350 | what /= EDefns

2349 = do iLOG $ "Elaborating class " ++ show n

2351 = do iLOG $ "Elaborating class " ++ show n

2350− elabClass info (s { syn_params = [] }) doc f cs n ps ds

2352+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

2351elabDecl' what info (PInstance s f cs n ps t expn ds)

2353elabDecl' what info (PInstance s f cs n ps t expn ds)

2352 = do iLOG $ "Elaborating instance " ++ show n

2354 = do iLOG $ "Elaborating instance " ++ show n

2353 elabInstance info s what f cs n ps t expn ds

2355 elabInstance info s what f cs n ps t expn ds

src/Idris/IBC.hs+6−4

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

30import Util.Zlib (decompressEither)

31

32ibcVersion :: Word8

33−ibcVersion = 68

33+ibcVersion = 69

34

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

@@ -300,7 +300,7 @@ pImports fs

300 = do mapM_ (\f -> do i <- getIState

301 ibcsd <- valIBCSubDir i

302 ids <- allImportDirs

303− fp <- runIO $ findImport ids ibcsd f

303+ fp <- findImport ids ibcsd f

304 if (f `elem` imported i)

305 then iLOG $ "Already read " ++ f

306 else do putIState (i { imported = f : imported i })

@@ -1436,7 +1436,7 @@ instance (Binary t) => Binary (PDecl' t) where

1436 put x7

1437 put x8

1438 put x9

1439− PClass x1 x2 x3 x4 x5 x6 x7

1439+ PClass x1 x2 x3 x4 x5 x6 x7 x8

1440 -> do putWord8 7

1441 put x1

1442 put x2

@@ -1445,6 +1445,7 @@ instance (Binary t) => Binary (PDecl' t) where

1445 put x5

1446 put x6

1447 put x7

1448+ put x8

1448 PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8

1449 PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8

1449 put x1

1450 put x1

1450 put x2

1451 put x2

@@ -1523,7 +1524,8 @@ instance (Binary t) => Binary (PDecl' t) where

1523 x5 <- get

1524 x5 <- get

1524 x6 <- get

1525 x6 <- get

1525 x7 <- get

1526 x7 <- get

1527+ x8 <- get

1526− return (PClass x1 x2 x3 x4 x5 x6 x7)

1528+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8)

1527 8 -> do x1 <- get

1529 8 -> do x1 <- get

1528 x2 <- get

1530 x2 <- get

1529 x3 <- get

1531 x3 <- get

src/Idris/IdrisDoc.hs+2−2

@@ -457,7 +457,7 @@ genTypeHeader ist (FD n _ args ftype _) = do

457

458 where

459 htmlSignature = displayDecorated decorator $ renderCompact signature

460− signature = pprintPTerm False [] names ftype

460+ signature = pprintPTerm False [] names (idris_infixes ist) ftype

461 names = [ n | (n@(UN n'), _, _, _) <- args,

462 not (T.isPrefixOf (txt "__") n') ]

463

@@ -656,4 +656,4 @@ copyDependencies :: FilePath -- ^ The base directory to which

656 -> IO ()

657copyDependencies dir =

658 do styles <- getDataFileName $ "idrisdoc" </> "styles.css"

659− copyFile styles (dir </> "styles.css")

659+ copyFile styles (dir </> "styles.css")

src/Idris/Imports.hs+7−6

@@ -1,6 +1,7 @@

1module Idris.Imports where

2

3import Idris.AbsSyntax

4+import Idris.Error

4

5

5import Idris.Core.TT

6import Idris.Core.TT

6import Paths_idris

7import Paths_idris

@@ -43,15 +44,15 @@ ibcPathWithFallback ibcsd fp = do let ibcp = ibcPath ibcsd True fp

43ibcPathNoFallback :: FilePath -> FilePath -> FilePath

44ibcPathNoFallback :: FilePath -> FilePath -> FilePath

44ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp

45ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp

45

46

46−findImport :: [FilePath] -> FilePath -> FilePath -> IO IFileType

47+findImport :: [FilePath] -> FilePath -> FilePath -> Idris IFileType

47−findImport [] ibcsd fp = fail $ "Can't find import " ++ fp

48+findImport [] ibcsd fp = ierror . Msg $ "Can't find import " ++ fp

48findImport (d:ds) ibcsd fp = do let fp_full = d </> fp

49findImport (d:ds) ibcsd fp = do let fp_full = d </> fp

49− ibcp <- ibcPathWithFallback ibcsd fp_full

50+ ibcp <- runIO $ ibcPathWithFallback ibcsd fp_full

50 let idrp = srcPath fp_full

51 let idrp = srcPath fp_full

51 let lidrp = lsrcPath fp_full

52 let lidrp = lsrcPath fp_full

52− ibc <- doesFileExist ibcp

53+ ibc <- runIO $ doesFileExist ibcp

53− idr <- doesFileExist idrp

54+ idr <- runIO $ doesFileExist idrp

54− lidr <- doesFileExist lidrp

55+ lidr <- runIO $ doesFileExist lidrp

55-- when idr $ putStrLn $ idrp ++ " ok"

56-- when idr $ putStrLn $ idrp ++ " ok"

56-- when lidr $ putStrLn $ lidrp ++ " ok"

57-- when lidr $ putStrLn $ lidrp ++ " ok"

57-- when ibc $ putStrLn $ ibcp ++ " ok"

58-- when ibc $ putStrLn $ ibcp ++ " ok"

src/Idris/Output.hs+9−5

@@ -23,7 +23,9 @@ ihWarn h fc err = do i <- getIState

23 case idris_outputmode i of

24 RawOutput ->

25 do err' <- iRender . fmap (fancifyAnnots i) $

26+ if fc_fname fc /= ""

26− text (show fc) <> colon <//> err

27+ then text (show fc) <> colon <//> err

28+ else err

27 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

29 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

28 IdeSlave n ->

30 IdeSlave n ->

29 do err' <- iRender . fmap (fancifyAnnots i) $ err

31 do err' <- iRender . fmap (fancifyAnnots i) $ err

@@ -78,7 +80,7 @@ ideSlaveReturnAnnotated n h out = do ist <- getIState

78

80

79ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

81ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

80ihPrintTermWithType h tm ty = do ist <- getIState

82ihPrintTermWithType h tm ty = do ist <- getIState

81− let output = tm <+> colon <+> ty

83+ let output = tm <+> colon <+> align ty

82 case idris_outputmode ist of

84 case idris_outputmode ist of

83 RawOutput -> consoleDisplayAnnotated h output

85 RawOutput -> consoleDisplayAnnotated h output

84 IdeSlave n -> ideSlaveReturnAnnotated n h output

86 IdeSlave n -> ideSlaveReturnAnnotated n h output

@@ -88,12 +90,14 @@ ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris

88ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

90ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

89ihPrintFunTypes h bnd n overloads = do imp <- impShow

91ihPrintFunTypes h bnd n overloads = do imp <- impShow

90 ist <- getIState

92 ist <- getIState

93+ let infixes = idris_infixes ist

91− let output = vsep (map (uncurry (ppOverload imp)) overloads)

94+ let output = vsep (map (uncurry (ppOverload imp infixes)) overloads)

92 case idris_outputmode ist of

95 case idris_outputmode ist of

93 RawOutput -> consoleDisplayAnnotated h output

96 RawOutput -> consoleDisplayAnnotated h output

94 IdeSlave n -> ideSlaveReturnAnnotated n h output

97 IdeSlave n -> ideSlaveReturnAnnotated n h output

95 where fullName n = prettyName True bnd n

98 where fullName n = prettyName True bnd n

99+ ppOverload imp infixes n tm =

96− ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)

100+ fullName n <+> colon <+> align (pprintPTerm imp bnd [] infixes tm)

97

101

98ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

102ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

99ihRenderResult h d = do ist <- getIState

103ihRenderResult h d = do ist <- getIState

@@ -119,7 +123,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

119 out = displayS . renderPretty 1.0 50 $ renderDocstring o

123 out = displayS . renderPretty 1.0 50 $ renderDocstring o

120 return (out "")

124 return (out "")

121 getTy :: IState -> Name -> String -- fails if name not already extant!

125 getTy :: IState -> Name -> String -- fails if name not already extant!

122− getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] $

126+ getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist) $

123 delabTy ist n

127 delabTy ist n

124 in (displayS . renderPretty 1.0 50 $ theTy) ""

128 in (displayS . renderPretty 1.0 50 $ theTy) ""

125fancifyAnnots _ annot = annot

129fancifyAnnots _ annot = annot

src/Idris/ParseHelpers.hs+2−2

@@ -566,8 +566,8 @@ collect (c@(PClauses _ o _ _) : ds)

566collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

567collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

568collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

569−collect (PClass doc f s cs n ps ds : ds')

569+collect (PClass doc f s cs n ps pdocs ds : ds')

570− = PClass doc f s cs n ps (collect ds) : collect ds'

570+ = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

571collect (PInstance f s cs n ps t en ds : ds')

572 = PInstance f s cs n ps t en (collect ds) : collect ds'

573collect (d : ds) = d : collect ds

src/Idris/Parser.hs+8−7

@@ -574,7 +574,7 @@ class_ syn = do (doc, acc) <- try (do

574 cs <- many carg

575 ds <- option [] (classBlock syn)

576 accData acc n (concatMap declared ds)

577− return [PClass (fst doc) syn fc cons n cs ds]

577+ return [PClass (fst doc) syn fc cons n cs (snd doc) ds]

578 <?> "type-class declaration"

579 where

580 carg :: IdrisParser (Name, PTerm)

@@ -1158,8 +1158,7 @@ loadModule outh f

1158 = idrisCatch (loadModule' outh f)

1159 (\e -> do setErrSpan (getErrSpan e)

1160 ist <- getIState

1161− msg <- showErr e

1161+ ihWarn outh (getErrSpan e) $ pprintErr ist e

1162− ihputStrLn outh msg

1163 return "")

1162 return "")

1164

1163

1165{- | Load idris module -}

1164{- | Load idris module -}

@@ -1169,7 +1168,7 @@ loadModule' outh f

1169 let file = takeWhile (/= ' ') f

1168 let file = takeWhile (/= ' ') f

1170 ibcsd <- valIBCSubDir i

1169 ibcsd <- valIBCSubDir i

1171 ids <- allImportDirs

1170 ids <- allImportDirs

1172− fp <- liftIO $ findImport ids ibcsd file

1171+ fp <- findImport ids ibcsd file

1173 if file `elem` imported i

1172 if file `elem` imported i

1174 then iLOG $ "Already read " ++ file

1173 then iLOG $ "Already read " ++ file

1175 else do putIState (i { imported = file : imported i })

1174 else do putIState (i { imported = file : imported i })

@@ -1206,7 +1205,9 @@ loadSource' h lidr r

1206 = idrisCatch (loadSource h lidr r)

1205 = idrisCatch (loadSource h lidr r)

1207 (\e -> do setErrSpan (getErrSpan e)

1206 (\e -> do setErrSpan (getErrSpan e)

1208 ist <- getIState

1207 ist <- getIState

1208+ case e of

1209+ At f e' -> ihWarn h f (pprintErr ist e')

1209− ihRenderError h (pprintErr ist e))

1210+ _ -> ihWarn h (getErrSpan e) (pprintErr ist e))

1210

1211

1211{- | Load Idris source code-}

1212{- | Load Idris source code-}

1212loadSource :: Handle -> Bool -> FilePath -> Idris ()

1213loadSource :: Handle -> Bool -> FilePath -> Idris ()

@@ -1219,7 +1220,7 @@ loadSource h lidr f

1219 (mname, imports, pos) <- parseImports f file

1220 (mname, imports, pos) <- parseImports f file

1220 ids <- allImportDirs

1221 ids <- allImportDirs

1221 ibcsd <- valIBCSubDir i

1222 ibcsd <- valIBCSubDir i

1222− mapM_ (\f -> do fp <- runIO $ findImport ids ibcsd f

1223+ mapM_ (\f -> do fp <- findImport ids ibcsd f

1223 case fp of

1224 case fp of

1224 LIDR fn -> ifail $ "No ibc for " ++ f

1225 LIDR fn -> ifail $ "No ibc for " ++ f

1225 IDR fn -> ifail $ "No ibc for " ++ f

1226 IDR fn -> ifail $ "No ibc for " ++ f

@@ -1309,7 +1310,7 @@ loadSource h lidr f

1309 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1310 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1310 case x of

1311 case x of

1311 PClauses _ _ _ _ -> r

1312 PClauses _ _ _ _ -> r

1312− PClass _ _ _ _ _ _ _ -> r

1313+ PClass _ _ _ _ _ _ _ _ -> r

1313 PInstance _ _ _ _ _ _ _ _ -> r

1314 PInstance _ _ _ _ _ _ _ _ -> r

1314 _ -> x

1315 _ -> x

1315

1316

src/Idris/Prover.hs+13−11

@@ -112,7 +112,7 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

112 where

113 showImplicits = opt_showimp (idris_options ist)

114

115− tPretty bnd t = pprintPTerm showImplicits bnd [] $ delab ist t

115+ tPretty bnd t = pprintPTerm showImplicits bnd [] (idris_infixes ist) $ delab ist t

116

117 assumptionNames :: Env -> [Name]

118 assumptionNames = map fst

@@ -237,15 +237,16 @@ ploop fn d prompt prf e h

237 ctxt' = envCtxt env ctxt

238 putIState ist { tt_ctxt = ctxt' }

239 (tm, ty) <- elabVal toplevel False t

240− let imp = opt_showimp (idris_options ist)

240+ let imp = opt_showimp (idris_options ist)

241− ty' = normaliseC ctxt [] ty

241+ ty' = normaliseC ctxt [] ty

242− h = idris_outh ist

242+ h = idris_outh ist

243+ infixes = idris_infixes ist

243 case tm of

244 case tm of

244 TType _ ->

245 TType _ ->

245 ihPrintTermWithType h (prettyImp imp PType) type1Doc

246 ihPrintTermWithType h (prettyImp imp PType) type1Doc

246 _ -> let bnd = map (\x -> (fst x, False)) env in

247 _ -> let bnd = map (\x -> (fst x, False)) env in

247− ihPrintTermWithType h (pprintPTerm imp bnd [] (delab ist tm))

248+ ihPrintTermWithType h (pprintPTerm imp bnd [] infixes (delab ist tm))

248− (pprintPTerm imp bnd [] (delab ist ty))

249+ (pprintPTerm imp bnd [] infixes (delab ist ty))

249 putIState ist

250 putIState ist

250 return (False, e, False, prf))

251 return (False, e, False, prf))

251 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

252 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

@@ -259,11 +260,12 @@ ploop fn d prompt prf e h

259 bnd = map (\x -> (fst x, False)) env

260 bnd = map (\x -> (fst x, False)) env

260 putIState ist'

261 putIState ist'

261 (tm, ty) <- elabVal toplevel False t

262 (tm, ty) <- elabVal toplevel False t

262− let tm' = force (normaliseAll ctxt' env tm)

263+ let tm' = force (normaliseAll ctxt' env tm)

263− ty' = force (normaliseAll ctxt' env ty)

264+ ty' = force (normaliseAll ctxt' env ty)

264− imp = opt_showimp (idris_options ist')

265+ imp = opt_showimp (idris_options ist')

266+ infixes = idris_infixes ist

265− tmDoc = pprintPTerm imp bnd [] (delab ist' tm')

267+ tmDoc = pprintPTerm imp bnd [] infixes (delab ist' tm')

266− tyDoc = pprintPTerm imp bnd [] (delab ist' ty')

268+ tyDoc = pprintPTerm imp bnd [] infixes (delab ist' ty')

267 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

268 putIState ist

270 putIState ist

269 return (False, e, False, prf))

271 return (False, e, False, prf))

src/Idris/REPL.hs+38−30

@@ -327,8 +327,9 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

327 -> ([(String, String, SpanList OutputAnnotation)],

328 (String, SpanList OutputAnnotation))

329 sexpGoal ist cols imp ns ([], concl) =

330+ let infixes = idris_infixes ist

330− let concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

331+ concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

331− pprintPTerm imp (zip ns (repeat False)) [] concl

332+ pprintPTerm imp (zip ns (repeat False)) [] infixes concl

332 in ([], concl')

333 in ([], concl')

333 sexpGoal ist cols imp ns ((n, t):ps, concl) =

334 sexpGoal ist cols imp ns ((n, t):ps, concl) =

334 let n' = case n of

335 let n' = case n of

@@ -337,7 +338,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

337 | otherwise -> str nm

338 | otherwise -> str nm

338 _ -> "_"

339 _ -> "_"

339 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

340 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

340− pprintPTerm imp (zip ns (repeat False)) [] t

341+ pprintPTerm imp (zip ns (repeat False)) [] (idris_infixes ist) t

341 rest = sexpGoal ist cols imp (n:ns) (ps, concl)

342 rest = sexpGoal ist cols imp (n:ns) (ps, concl)

342 in ((n', t', spans) : fst rest, snd rest)

343 in ((n', t', spans) : fst rest, snd rest)

343runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

344runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

@@ -562,21 +563,19 @@ process h fn (Eval t)

562 ist <- getIState

563 ist <- getIState

563 logLvl 3 $ "Raw: " ++ show (tm', ty')

564 logLvl 3 $ "Raw: " ++ show (tm', ty')

564 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

565 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

565− let imp = opt_showimp (idris_options ist)

566− tmDoc = prettyImp imp (delab ist tm')

566+ let tmDoc = prettyIst ist (delab ist tm')

567− tyDoc = prettyImp imp (delab ist ty')

567+ tyDoc = prettyIst ist (delab ist ty')

568 ihPrintTermWithType h tmDoc tyDoc

569

570process h fn (ExecVal t)

571 = do ctxt <- getContext

572 ist <- getIState

573− let imp = opt_showimp (idris_options ist)

574 (tm, ty) <- elabVal toplevel False t

573 (tm, ty) <- elabVal toplevel False t

575-- let tm' = normaliseAll ctxt [] tm

574-- let tm' = normaliseAll ctxt [] tm

576 let ty' = normaliseAll ctxt [] ty

575 let ty' = normaliseAll ctxt [] ty

577 res <- execute tm

576 res <- execute tm

578− let (resOut, tyOut) = (prettyImp imp (delab ist res),

577+ let (resOut, tyOut) = (prettyIst ist (delab ist res),

579− prettyImp imp (delab ist ty'))

578+ prettyIst ist (delab ist ty'))

580 ihPrintTermWithType h resOut tyOut

579 ihPrintTermWithType h resOut tyOut

581

580

582process h fn (Check (PRef _ n))

581process h fn (Check (PRef _ n))

@@ -611,7 +610,7 @@ process h fn (Check (PRef _ n))

611 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

610 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

612 align (tPretty bnd ist g)

611 align (tPretty bnd ist g)

613

612

614− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t

613+ tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist) t

615

614

616

615

617process h fn (Check t)

616process h fn (Check t)

@@ -622,19 +621,18 @@ process h fn (Check t)

622 ty' = normaliseC ctxt [] ty

621 ty' = normaliseC ctxt [] ty

623 case tm of

622 case tm of

624 TType _ ->

623 TType _ ->

625− ihPrintTermWithType h (prettyImp imp PType) type1Doc

624+ ihPrintTermWithType h (prettyIst ist PType) type1Doc

626− _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))

625+ _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))

627− (prettyImp imp (delab ist ty))

626+ (prettyIst ist (delab ist ty))

628

627

629process h fn (DocStr n)

628process h fn (DocStr n)

630− = do i <- getIState

629+ = do ist <- getIState

631− let imp = opt_showimp (idris_options i)

632− case lookupCtxtName n (idris_docstrings i) of

630+ case lookupCtxtName n (idris_docstrings ist) of

633 [] -> iPrintError $ "No documentation for " ++ show n

631 [] -> iPrintError $ "No documentation for " ++ show n

634− ns -> do toShow <- mapM (showDoc imp) ns

632+ ns -> do toShow <- mapM (showDoc ist) ns

635 ihRenderResult h (vsep toShow)

633 ihRenderResult h (vsep toShow)

636− where showDoc imp (n, d) = do doc <- getDocs n

634+ where showDoc ist (n, d) = do doc <- getDocs n

637− return $ pprintDocs imp doc

635+ return $ pprintDocs ist doc

638process h fn Universes

636process h fn Universes

639 = do i <- getIState

637 = do i <- getIState

640 let cs = idris_constraints i

638 let cs = idris_constraints i

@@ -826,9 +824,11 @@ process h fn (DoProofSearch updatefile rec l n hints)

826 (tm, ty) <- elabVal toplevel False (PRef fc mn)

824 (tm, ty) <- elabVal toplevel False (PRef fc mn)

827 ctxt <- getContext

825 ctxt <- getContext

828 i <- getIState

826 i <- getIState

827+ return . flip displayS "" . renderPretty 1.0 80 $

828+ pprintPTerm False [] [] (idris_infixes i)

829− return $ show (stripNS

829+ (stripNS

830− (dropCtxt envlen

830+ (dropCtxt envlen

831− (delab i (specialise ctxt [] [(mn, 1)] tm)))))

831+ (delab i (specialise ctxt [] [(mn, 1)] tm)))))

832 (\e -> return ("?" ++ show n))

833 if updatefile then

834 do let fb = fn ++ "~"

@@ -1031,6 +1031,8 @@ process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

1031process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

1032process h fn (SetOpt AutoSolve) = setAutoSolve True

1033process h fn (UnsetOpt AutoSolve) = setAutoSolve False

1034+process h fn (SetOpt NoBanner) = setNoBanner True

1035+process h fn (UnsetOpt NoBanner) = setNoBanner False

1034

1036

1035process h fn (SetOpt _) = iPrintError "Not a valid option"

1037process h fn (SetOpt _) = iPrintError "Not a valid option"

1036process h fn (UnsetOpt _) = iPrintError "Not a valid option"

1038process h fn (UnsetOpt _) = iPrintError "Not a valid option"

@@ -1051,15 +1053,14 @@ process h fn (SetConsoleWidth w) = setWidth w

1051

1053

1052process h fn (Apropos a) =

1054process h fn (Apropos a) =

1053 do ist <- getIState

1055 do ist <- getIState

1054− let impl = opt_showimp (idris_options ist)

1055 let names = apropos ist (T.pack a)

1056 let names = apropos ist (T.pack a)

1056 let aproposInfo = [ (n,

1057 let aproposInfo = [ (n,

1057 delabTy ist n,

1058 delabTy ist n,

1058 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1059 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1059 | n <- sort names, isUN n ]

1060 | n <- sort names, isUN n ]

1060− ihRenderResult h $ vsep (map (renderApropos impl) aproposInfo)

1061+ ihRenderResult h $ vsep (map (renderApropos ist) aproposInfo)

1061− where renderApropos impl (name, ty, docs) =

1062+ where renderApropos ist (name, ty, docs) =

1062− prettyName True [] name <+> colon <+> align (prettyImp impl ty) <$>

1063+ prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

1063 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1064 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1064 isUN (UN _) = True

1065 isUN (UN _) = True

1065 isUN (NS n _) = isUN n

1066 isUN (NS n _) = isUN n

@@ -1258,11 +1259,11 @@ loadInputs h inputs

1258 idris_patdefs = patdefs }))

1259 idris_patdefs = patdefs }))

1259 (\e -> do i <- getIState

1260 (\e -> do i <- getIState

1260 case e of

1261 case e of

1261− At f _ -> do setErrSpan f

1262+ At f e' -> do setErrSpan f

1262− ihRenderError stdout $ pprintErr i e

1263+ ihWarn stdout f $ pprintErr i e'

1263 ProgramLineComment -> return () -- fail elsewhere

1264 ProgramLineComment -> return () -- fail elsewhere

1264 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1265 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1265− iputStrLn (pshow i e))

1266+ ihWarn stdout emptyFC $ pprintErr i e)

1266 where -- load all files, stop if any fail

1267 where -- load all files, stop if any fail

1267 tryLoad :: Bool -> [IFileType] -> Idris ()

1268 tryLoad :: Bool -> [IFileType] -> Idris ()

1268 tryLoad keepstate [] = return ()

1269 tryLoad keepstate [] = return ()

@@ -1353,6 +1354,7 @@ idrisMain opts =

1353 setVerbose verbose

1354 setVerbose verbose

1354 setCmdLine opts

1355 setCmdLine opts

1355 setOutputTy outty

1356 setOutputTy outty

1357+ setNoBanner nobanner

1356 setCodegen cgn

1358 setCodegen cgn

1357 setTargetTriple trpl

1359 setTargetTriple trpl

1358 setTargetCPU tcpu

1360 setTargetCPU tcpu

@@ -1367,6 +1369,8 @@ idrisMain opts =

1367 (d:_) -> setIBCSubDir d

1369 (d:_) -> setIBCSubDir d

1368 setImportDirs importdirs

1370 setImportDirs importdirs

1369

1371

1372+ setNoBanner nobanner

1373+

1370 when (not (NoBasePkgs `elem` opts)) $ do

1374 when (not (NoBasePkgs `elem` opts)) $ do

1371 addPkgDir "prelude"

1375 addPkgDir "prelude"

1372 addPkgDir "base"

1376 addPkgDir "base"

@@ -1376,6 +1380,11 @@ idrisMain opts =

1376 return ()

1380 return ()

1377 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"

1381 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"

1378 return ()

1382 return ()

1383+

1384+ when (runrepl && not idesl) initScript

1385+

1386+ nobanner <- getNoBanner

1387+

1379 when (runrepl &&

1388 when (runrepl &&

1380 not quiet &&

1389 not quiet &&

1381 not idesl &&

1390 not idesl &&

@@ -1426,7 +1435,6 @@ idrisMain opts =

1426

1435

1427 when (runrepl && not idesl) $ do

1436 when (runrepl && not idesl) $ do

1428-- clearOrigPats

1437-- clearOrigPats

1429− initScript

1430 startServer orig inputs

1438 startServer orig inputs

1431 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1439 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1432 when (idesl) $ ideslaveStart orig inputs

1440 when (idesl) $ ideslaveStart orig inputs

src/Idris/REPLParser.hs+1

@@ -119,6 +119,7 @@ pOption = do discard (P.symbol "errorcontext"); return ErrContext

119 <|> do discard (P.symbol "showimplicits"); return ShowImpl

120 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

121 <|> do discard (P.symbol "autosolve"); return AutoSolve

122+ <|> do discard (P.symbol "nobanner") ; return NoBanner

122

123

123codegenOption :: P.IdrisParser Codegen

124codegenOption :: P.IdrisParser Codegen

124codegenOption = do discard (P.symbol "javascript"); return ViaJavaScript

125codegenOption = do discard (P.symbol "javascript"); return ViaJavaScript

test/interactive001/expected+1−1

@@ -4,7 +4,7 @@ isElem x (y :: xs) = ?isElem_rhs_3

4

5 localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1

6

7−f x :: (map f xs)

7+f x :: map f xs

8isElem2 x (y :: ys) with (_)

9 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs

10 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3

test/interactive003/expected+2−2

@@ -1,5 +1,5 @@

1Type checking ./interactive003.idr

2ys

3−x :: (app xs ys)

3+x :: app xs ys

4[]

5−f x y :: (vzipWith f xs ys)

5+f x y :: vzipWith f xs ys