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

CHANGELOG+1

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

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

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

1414 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.

1516

1617Internal changes

1718

libs/prelude/Prelude/Bool.idr+5

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

22

33import Builtins

44

5+import Prelude.Uninhabited

6+

57||| Boolean Data Type

68data Bool = False | True

79

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

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

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

1820

21+instance Uninhabited (so False) where

22+ uninhabited oh impossible

23+

1924-- Syntactic sugar for boolean elimination.

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

2126

src/IRTS/CodegenJavaScript.hs+77−27

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

740740 JSReturn (JSApp (JSIdent fun) args)

741741 )])

742742 | Just pos <- lookup fun ids

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

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

744744

745745 removeIDCall ids (JSNew _ [JSFunction [] (

746746 JSReturn (JSApp (JSIdent fun) args)

747747 )])

748748 | Just pos <- lookup fun ids

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

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

750750

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

752752 | Just pos <- lookup fun ids

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

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

754754

755755 removeIDCall ids js = transformJS (removeIDCall ids) js

756756

757757

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+

758781inlineFunctions :: [JS] -> [JS]

759782inlineFunctions js =

760783 inlineHelper ([], js)

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

766789 | Just new <- inlineAble (

767790 countAll fun front + countAll fun back

768791 ) fun args body =

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

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

770793 inlineHelper (f front, f back)

771794

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

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

783806 inlineAble _ _ _ _ = Nothing

784807

785808

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−

809809 nonRecur :: String -> JS -> Bool

810810 nonRecur name body = countInvokations name body == 0

811811

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

14161416 match js = transformJS match js

14171417

14181418

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+

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

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

14211469 where

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

15171565 , extractLocalConstructors

15181566 , unfoldLookupTable

15191567 , evalCons

1568+ , elimConds

1569+ , removeUselessCons

15201570 ]

15211571

15221572 functions :: [String]

src/Idris/AbsSyntax.hs+3−1

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

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

948948 bnames _ = []

949949

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

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

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

952953 where

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

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

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

974975 = 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)

976977 = PClass doc info f

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

978979 n

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

981+ pDocs

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

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

982984 = PInstance info f

src/Idris/AbsSyntaxTree.hs+38−11

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

3131import Data.Either

3232import qualified Data.Set as S

3333import Data.Word (Word)

34+import Data.Maybe (fromMaybe)

3435

3536import Debug.Trace

3637

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

487488 [t] -- constraints

488489 Name

489490 [(Name, t)] -- parameters

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

490492 [PDecl' t] -- declarations

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

492494 -- class name, parameters, method declarations

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

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

570572declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

574576declared (PDSL n _) = [n]

575577declared (PSyntax _ _) = []

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

588590tldeclared (PParams _ _ ds) = []

589591tldeclared (PMutual _ ds) = concatMap tldeclared ds

590592tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

593595tldeclared _ = []

594596

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

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

605607defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

609611defined (PDSL n _) = [n]

610612defined (PSyntax _ _) = []

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

10651067elimName = sUN "__Elim"

10661068elimMethElimTy = sUN "__elimTy"

10671069elimMethElim = 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)] []

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

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

10711073

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

11261128 colour UnderlineText = IdrisColour Nothing True True False False

11271129 colour ItalicText = IdrisColour Nothing True False False True

11281130

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

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

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

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

11321134 -> Doc OutputAnnotation

1133−prettyImp impl = pprintPTerm impl [] []

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

11341136

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

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+

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

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

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

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

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

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

11401147 -> Doc OutputAnnotation

1141−pprintPTerm impl bnd docArgs = prettySe 10 bnd

1148+pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

11421149 where

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

11441151 prettySe p bnd (PQuote r) =

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

12031210 case getExps args of

12041211 [] -> enclose lparen rparen opName

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

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

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

1214+ in bracket p precedence $ inFix l r

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

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

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

12101218 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

12111228 inFix l r = align . group $

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

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

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

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

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

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

13141331 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

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

13161333

1334+ opStr :: Name -> String

1335+ opStr (NS n _) = opStr n

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

1337+

13171338 basename :: Name -> Name

13181339 basename (NS n _) = basename n

13191340 basename n = n

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

13671388

13681389 kwd = annotate AnnKeyword . text

13691390

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+

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

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

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

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

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

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

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

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

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

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

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

14251452 = 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

2222

2323import Data.Maybe

2424import Data.Char

25+import Data.List (isPrefixOf, isSuffixOf)

2526import Control.Monad

2627import Control.Monad.State.Strict

2728

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

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

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

301302

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

303+ addBrackets tm | ' ' `elem` tm

304+ , not (isPrefixOf "(" tm)

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

303306 | otherwise = tm

304307

305308getUniq nm i

src/Idris/Chaser.hs+1−1

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

8282 iLOG $ "CHASING " ++ show file

8383 ibcsd <- valIBCSubDir i

8484 ids <- allImportDirs

85− fp <- runIO $ findImport ids ibcsd file

85+ fp <- findImport ids ibcsd file

8686 iLOG $ "Found " ++ show fp

8787 mt <- runIO $ getIModTime fp

8888 if (file `elem` built)

src/Idris/Completion.hs+1

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

112112 , "showimplicits"

113113 , "originalerrors"

114114 , "autosolve"

115+ , "nobanner"

115116 ]

116117

117118completeConsoleWidth :: CompletionFunc Idris

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

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

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

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

222222 | fp == mkfprim,

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

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

224224 = case str of

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

226226 execApp env ctxt ioUnit rest

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

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

229229 show str ++

230230 ". 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?"

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

232244 | fp == mkfprim,

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

src/Idris/DeepSeq.hs+2−2

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

143143 rnf x2 `seq`

144144 rnf x3 `seq`

145145 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)

147147 = rnf x1 `seq`

148148 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` ()

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

151151 = rnf x1 `seq`

152152 rnf x2 `seq`

src/Idris/Delaborate.hs+1−1

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

138138pprintTerm ist = pprintTerm' ist []

139139

140140pprintTerm' :: 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)

142142

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

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

src/Idris/Docs.hs+40−23

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

11{-# LANGUAGE PatternGuards #-}

2−module Idris.Docs where

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

33

44import Idris.AbsSyntax

55import Idris.AbsSyntaxTree

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

3434showDoc d | nullDocstring d = empty

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

3636

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

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

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

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

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

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

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

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

4242 renderDocstring doc <$>

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

4444 let argshow = showArgs args [] in

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

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

4747 else empty)

4848

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

49+ where imp = opt_showimp (idris_options ist)

50+ infixes = idris_infixes ist

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

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

51− pprintPTerm imp bnd [] ty <>

53+ pprintPTerm imp bnd [] infixes ty <>

5254 showDoc d <> line

5355 :

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

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

5658 = text "Class constraint" <+>

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

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

5860 :

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

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

6163 = text "(implicit)" <+>

6264 bindingOf n True <+> colon <+>

63− pprintPTerm imp bnd [] ty <>

65+ pprintPTerm imp bnd [] infixes ty <>

6466 showDoc d <> line

6567 :

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

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

6870 showArgs [] _ = []

6971

7072

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

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

73−pprintDocs imp (DataDoc t args)

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

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

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

75+pprintDocs ist (DataDoc t args)

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

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

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

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

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

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

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

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

8082 <> line <$>

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

8284 <> line <$>

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

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

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

8587 <$>

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

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

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

8991 <>

9092 if null subclasses then empty

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

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

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

9395 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

95102

96103 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 _ _ = []

98117

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

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

101− remConstraint p = p

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

119+ updateRef _ pt = pt

102120

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

104122 hasConstraint (PPi _ _ _ pt) = hasConstraint pt

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

107125 (subclasses, instances') = partition hasConstraint instances

108126

109127 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)

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

112130

113131getDocs :: Name -> Idris Docs

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

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

130148docClass n ci

131149 = do i <- getIState

132− ctxt <- getContext

133150 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

134151 docstr = maybe emptyDocstring fst docStrings

135152 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)

365365

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

367367

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)

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

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

371371 ElabInfo -> EliminatorState ()

372372elabEliminator paramPos n ty cons info = do

373373 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))

374375 let (cnstrs, _) = splitPi ty

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

376377 generalParams <- namePis False pms

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

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

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

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

393+ elimLog elimSig

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

393395 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

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

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

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

397399 case eliminatorClauses of

398− [] -> return ()

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

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

400402 where elimLog :: String -> EliminatorState ()

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

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

458460 freshName key = do

459461 nameMap <- get

460462 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)

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

463− return (sUN name)

465+ return name

464466

465467 scrutineeName :: Name

466468 scrutineeName = sUN "scrutinee"

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

553555 let cons' = replaceParams paramPos generalParameters ty

554556 let (args, resTy) = splitPi cons'

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

556− consArgs <- namePis True args

558+ consArgs <- namePis False args

557559 let recArgs = findRecArgs consArgs

558560 let recMotives = map applyRecMotive recArgs

559561 let (_, consIdxs) = splitArgPms resTy

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

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

593595 let (_, generalIdxs') = splitArgPms resTy

594596 let generalIdxs = map pexp generalIdxs'

595− consArgs <- namePis True args

597+ consArgs <- namePis False args

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

597599 let recArgs = findRecArgs consArgs

598600 let recElims = map applyRecElim recArgs

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

18341836

18351837elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

18361838 FC -> [PTerm] ->

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

1838−elabClass info syn doc fc constraints tn ps ds

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

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

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

18401842 let tty = pibind ps PType

18411843 let constraint = PApp fc (PRef fc tn)

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

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

18631865 let ddecl = PDatadecl tn tty cons

18641866 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

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

18671869 logLvl 5 $ "Building functions"

18681870 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

23442346 ninfo = case namespace info of

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

23462348 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)

23482350 | what /= EDefns

23492351 = 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

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

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

23532355 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)

3030import Util.Zlib (decompressEither)

3131

3232ibcVersion :: Word8

33−ibcVersion = 68

33+ibcVersion = 69

3434

3535data IBCFile = IBCFile { ver :: Word8,

3636 sourcefile :: FilePath,

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

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

301301 ibcsd <- valIBCSubDir i

302302 ids <- allImportDirs

303− fp <- runIO $ findImport ids ibcsd f

303+ fp <- findImport ids ibcsd f

304304 if (f `elem` imported i)

305305 then iLOG $ "Already read " ++ f

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

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

14361436 put x7

14371437 put x8

14381438 put x9

1439− PClass x1 x2 x3 x4 x5 x6 x7

1439+ PClass x1 x2 x3 x4 x5 x6 x7 x8

14401440 -> do putWord8 7

14411441 put x1

14421442 put x2

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

14451445 put x5

14461446 put x6

14471447 put x7

1448+ put x8

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

14491450 put x1

14501451 put x2

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

15231524 x5 <- get

15241525 x6 <- get

15251526 x7 <- get

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

1527+ x8 <- get

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

15271529 8 -> do x1 <- get

15281530 x2 <- get

15291531 x3 <- get

src/Idris/IdrisDoc.hs+2−2

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

457457

458458 where

459459 htmlSignature = displayDecorated decorator $ renderCompact signature

460− signature = pprintPTerm False [] names ftype

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

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

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

463463

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

656656 -> IO ()

657657copyDependencies dir =

658658 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 @@

11module Idris.Imports where

22

33import Idris.AbsSyntax

4+import Idris.Error

45

56import Idris.Core.TT

67import Paths_idris

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

4344ibcPathNoFallback :: FilePath -> FilePath -> FilePath

4445ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp

4546

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

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

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

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

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

49− ibcp <- ibcPathWithFallback ibcsd fp_full

50+ ibcp <- runIO $ ibcPathWithFallback ibcsd fp_full

5051 let idrp = srcPath fp_full

5152 let lidrp = lsrcPath fp_full

52− ibc <- doesFileExist ibcp

53− idr <- doesFileExist idrp

54− lidr <- doesFileExist lidrp

53+ ibc <- runIO $ doesFileExist ibcp

54+ idr <- runIO $ doesFileExist idrp

55+ lidr <- runIO $ doesFileExist lidrp

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

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

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

src/Idris/Output.hs+9−5

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

2323 case idris_outputmode i of

2424 RawOutput ->

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

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

26+ if fc_fname fc /= ""

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

28+ else err

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

2830 IdeSlave n ->

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

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

7880

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

8082ihPrintTermWithType h tm ty = do ist <- getIState

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

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

8284 case idris_outputmode ist of

8385 RawOutput -> consoleDisplayAnnotated h output

8486 IdeSlave n -> ideSlaveReturnAnnotated n h output

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

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

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

9092 ist <- getIState

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

93+ let infixes = idris_infixes ist

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

9295 case idris_outputmode ist of

9396 RawOutput -> consoleDisplayAnnotated h output

9497 IdeSlave n -> ideSlaveReturnAnnotated n h output

9598 where fullName n = prettyName True bnd n

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

99+ ppOverload imp infixes n tm =

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

97101

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

99103ihRenderResult h d = do ist <- getIState

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

119123 out = displayS . renderPretty 1.0 50 $ renderDocstring o

120124 return (out "")

121125 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) $

123127 delabTy ist n

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

125129fancifyAnnots _ annot = annot

src/Idris/ParseHelpers.hs+2−2

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

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

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

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

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

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

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

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

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

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

573573collect (d : ds) = d : collect ds

src/Idris/Parser.hs+8−7

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

574574 cs <- many carg

575575 ds <- option [] (classBlock syn)

576576 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]

578578 <?> "type-class declaration"

579579 where

580580 carg :: IdrisParser (Name, PTerm)

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

11581158 = idrisCatch (loadModule' outh f)

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

11601160 ist <- getIState

1161− msg <- showErr e

1162− ihputStrLn outh msg

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

11631162 return "")

11641163

11651164{- | Load idris module -}

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

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

11701169 ibcsd <- valIBCSubDir i

11711170 ids <- allImportDirs

1172− fp <- liftIO $ findImport ids ibcsd file

1171+ fp <- findImport ids ibcsd file

11731172 if file `elem` imported i

11741173 then iLOG $ "Already read " ++ file

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

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

12061205 = idrisCatch (loadSource h lidr r)

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

12081207 ist <- getIState

1209− ihRenderError h (pprintErr ist e))

1208+ case e of

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

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

12101211

12111212{- | Load Idris source code-}

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

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

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

12201221 ids <- allImportDirs

12211222 ibcsd <- valIBCSubDir i

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

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

12231224 case fp of

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

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

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

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

13101311 case x of

13111312 PClauses _ _ _ _ -> r

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

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

13131314 PInstance _ _ _ _ _ _ _ _ -> r

13141315 _ -> x

13151316

src/Idris/Prover.hs+13−11

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

112112 where

113113 showImplicits = opt_showimp (idris_options ist)

114114

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

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

116116

117117 assumptionNames :: Env -> [Name]

118118 assumptionNames = map fst

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

237237 ctxt' = envCtxt env ctxt

238238 putIState ist { tt_ctxt = ctxt' }

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

240− let imp = opt_showimp (idris_options ist)

241− ty' = normaliseC ctxt [] ty

242− h = idris_outh ist

240+ let imp = opt_showimp (idris_options ist)

241+ ty' = normaliseC ctxt [] ty

242+ h = idris_outh ist

243+ infixes = idris_infixes ist

243244 case tm of

244245 TType _ ->

245246 ihPrintTermWithType h (prettyImp imp PType) type1Doc

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

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

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

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

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

249250 putIState ist

250251 return (False, e, False, prf))

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

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

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

260261 putIState ist'

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

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

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

264− imp = opt_showimp (idris_options ist')

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

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

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

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

265+ imp = opt_showimp (idris_options ist')

266+ infixes = idris_infixes ist

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

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

267269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

268270 putIState ist

269271 return (False, e, False, prf))

src/Idris/REPL.hs+38−30

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

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

328328 (String, SpanList OutputAnnotation))

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

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

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

330+ let infixes = idris_infixes ist

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

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

332333 in ([], concl')

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

334335 let n' = case n of

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

337338 | otherwise -> str nm

338339 _ -> "_"

339340 (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

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

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

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

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

562563 ist <- getIState

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

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

565− let imp = opt_showimp (idris_options ist)

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

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

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

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

568568 ihPrintTermWithType h tmDoc tyDoc

569569

570570process h fn (ExecVal t)

571571 = do ctxt <- getContext

572572 ist <- getIState

573− let imp = opt_showimp (idris_options ist)

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

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

576575 let ty' = normaliseAll ctxt [] ty

577576 res <- execute tm

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

579− prettyImp imp (delab ist ty'))

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

578+ prettyIst ist (delab ist ty'))

580579 ihPrintTermWithType h resOut tyOut

581580

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

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

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

612611 align (tPretty bnd ist g)

613612

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

615614

616615

617616process h fn (Check t)

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

622621 ty' = normaliseC ctxt [] ty

623622 case tm of

624623 TType _ ->

625− ihPrintTermWithType h (prettyImp imp PType) type1Doc

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

627− (prettyImp imp (delab ist ty))

624+ ihPrintTermWithType h (prettyIst ist PType) type1Doc

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

626+ (prettyIst ist (delab ist ty))

628627

629628process h fn (DocStr n)

630− = do i <- getIState

631− let imp = opt_showimp (idris_options i)

632− case lookupCtxtName n (idris_docstrings i) of

629+ = do ist <- getIState

630+ case lookupCtxtName n (idris_docstrings ist) of

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

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

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

635633 ihRenderResult h (vsep toShow)

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

637− return $ pprintDocs imp doc

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

635+ return $ pprintDocs ist doc

638636process h fn Universes

639637 = do i <- getIState

640638 let cs = idris_constraints i

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

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

827825 ctxt <- getContext

828826 i <- getIState

829− return $ show (stripNS

830− (dropCtxt envlen

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

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

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

829+ (stripNS

830+ (dropCtxt envlen

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

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

833833 if updatefile then

834834 do let fb = fn ++ "~"

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

10311031process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

10321032process h fn (SetOpt AutoSolve) = setAutoSolve True

10331033process h fn (UnsetOpt AutoSolve) = setAutoSolve False

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

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

10341036

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

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

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

10511053

10521054process h fn (Apropos a) =

10531055 do ist <- getIState

1054− let impl = opt_showimp (idris_options ist)

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

10561057 let aproposInfo = [ (n,

10571058 delabTy ist n,

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

10591060 | n <- sort names, isUN n ]

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

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

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

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

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

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

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

10641065 isUN (UN _) = True

10651066 isUN (NS n _) = isUN n

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

12581259 idris_patdefs = patdefs }))

12591260 (\e -> do i <- getIState

12601261 case e of

1261− At f _ -> do setErrSpan f

1262− ihRenderError stdout $ pprintErr i e

1262+ At f e' -> do setErrSpan f

1263+ ihWarn stdout f $ pprintErr i e'

12631264 ProgramLineComment -> return () -- fail elsewhere

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

1265− iputStrLn (pshow i e))

1266+ ihWarn stdout emptyFC $ pprintErr i e)

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

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

12681269 tryLoad keepstate [] = return ()

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

13531354 setVerbose verbose

13541355 setCmdLine opts

13551356 setOutputTy outty

1357+ setNoBanner nobanner

13561358 setCodegen cgn

13571359 setTargetTriple trpl

13581360 setTargetCPU tcpu

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

13671369 (d:_) -> setIBCSubDir d

13681370 setImportDirs importdirs

13691371

1372+ setNoBanner nobanner

1373+

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

13711375 addPkgDir "prelude"

13721376 addPkgDir "base"

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

13761380 return ()

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

13781382 return ()

1383+

1384+ when (runrepl && not idesl) initScript

1385+

1386+ nobanner <- getNoBanner

1387+

13791388 when (runrepl &&

13801389 not quiet &&

13811390 not idesl &&

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

14261435

14271436 when (runrepl && not idesl) $ do

14281437-- clearOrigPats

1429− initScript

14301438 startServer orig inputs

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

14321440 when (idesl) $ ideslaveStart orig inputs

src/Idris/REPLParser.hs+1

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

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

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

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

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

122123

123124codegenOption :: P.IdrisParser Codegen

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

test/interactive001/expected+1−1

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

44

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

66

7−f x :: (map f xs)

7+f x :: map f xs

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

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

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

test/interactive003/expected+2−2

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

11Type checking ./interactive003.idr

22ys

3−x :: (app xs ys)

3+x :: app xs ys

44[]

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

5+f x y :: vzipWith f xs ys