9b1746c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'upstream/master' into idrisdoc

commit9b1746c60edd70a120da2ad04d9476a1f4dc3797 authorPhilip Rasmussen <pjor@itu.dk> dateWed 26 Mar 2014, 11:40 (13 years ago) parent77eca9c 577752b

9 files changed+31−26

compare with master

unifiedsplit

idris.cabal+1 src/IRTS/CodegenC.hs+4−4 src/Idris/AbsSyntax.hs+1−1 src/Idris/AbsSyntaxTree.hs+4−3 src/Idris/Delaborate.hs+1−1 src/Idris/Docs.hs+13−10 src/Idris/Prover.hs+5−5 src/Idris/REPL.hs+1−1 test/Makefile+1−1

idris.cabal+1

@@ -541,6 +541,7 @@ Library

541541 , filepath

542542 , haskeline >= 0.7

543543 , language-java >= 0.2.6

544+ , lens >= 4.1.1

544545 , mtl

545546 , parsers >= 0.9

546547 , pretty

src/IRTS/CodegenC.hs+4−4

@@ -132,10 +132,10 @@ bcc i (ASSIGNCONST l c)

132132 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"

133133 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"

134134 mkConst (Str s) = "MKSTR(vm, " ++ showCStr s ++ ")"

135− mkConst (B8 x) = "idris_b8const(vm, " ++ show x ++ ")"

136− mkConst (B16 x) = "idris_b16const(vm, " ++ show x ++ ")"

137− mkConst (B32 x) = "idris_b32const(vm, " ++ show x ++ ")"

138− mkConst (B64 x) = "idris_b64const(vm, " ++ show x ++ ")"

135+ mkConst (B8 x) = "idris_b8const(vm, " ++ show x ++ "U)"

136+ mkConst (B16 x) = "idris_b16const(vm, " ++ show x ++ "U)"

137+ mkConst (B32 x) = "idris_b32const(vm, " ++ show x ++ "UL)"

138+ mkConst (B64 x) = "idris_b64const(vm, " ++ show x ++ "ULL)"

139139 mkConst _ = "MKINT(42424242)"

140140bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

141141bcc i (MKCON l tag args)

src/Idris/AbsSyntax.hs+1−1

@@ -567,7 +567,7 @@ ihPrintFunTypes h bnd n overloads = do imp <- impShow

567567 RawOutput -> consoleDisplayAnnotated h output

568568 IdeSlave n -> ideSlaveReturnAnnotated n h output

569569 where fullName n = prettyName True bnd n

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

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

571571

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

573573ihRenderResult h d = do ist <- getIState

src/Idris/AbsSyntaxTree.hs+4−3

@@ -1086,14 +1086,15 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

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

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

10881088 -> Doc OutputAnnotation

1089−prettyImp impl = pprintPTerm impl []

1089+prettyImp impl = pprintPTerm impl [] []

10901090

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

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

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

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

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

10951096 -> Doc OutputAnnotation

1096−pprintPTerm impl bnd = prettySe 10 bnd

1097+pprintPTerm impl bnd docArgs = prettySe 10 bnd

10971098 where

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

10991100 prettySe p bnd (PQuote r) =

@@ -1113,7 +1114,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

11131114 prettySe 10 bnd v <+> kwd "in" </>

11141115 prettySe 10 ((n, False):bnd) sc

11151116 prettySe p bnd (PPi (Exp l s _) n ty sc)

1116− | n `elem` allNamesIn sc || impl =

1117+ | n `elem` allNamesIn sc || impl || n `elem` docArgs =

11171118 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

11181119 bracket p 2 . group $

11191120 enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

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 = pprintPTerm (opt_showimp (idris_options ist))

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

142142

143143pshow :: IState -> Err -> String

144144pshow ist err = displayDecorated (consoleDecorate ist) .

src/Idris/Docs.hs+13−10

@@ -12,6 +12,7 @@ import Util.Pretty

1212

1313import Data.Maybe

1414import Data.List

15+import qualified Data.Text as T

1516

1617-- TODO: Only include names with public/abstract accessibility

1718

@@ -33,30 +34,32 @@ showDoc d | nullDocstring d = empty

3334

3435pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

3536pprintFD imp (FD n doc args ty f)

36− = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> renderDocstring doc <$>

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

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

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

40+ renderDocstring doc <$>

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

3842 let argshow = showArgs args [] in

3943 if not (null argshow)

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

4145 else empty)

4246

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

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

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

45− pprintPTerm imp bnd ty <>

46− showDoc (maybe emptyDocstring id d) <> line

49+ pprintPTerm imp bnd [] ty <>

50+ showDoc d <> line

4751 :

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

49− showArgs ((n, ty, Constraint {}, d):args) bnd

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

5054 = text "Class constraint" <+>

51− pprintPTerm imp bnd ty <> showDoc (maybe emptyDocstring id d) <> line

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

5256 :

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

54− showArgs ((n, ty, Imp {}, d):args) bnd

55− | Just d' <- d

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

5659 = text "(implicit)" <+>

5760 bindingOf n True <+> colon <+>

58− pprintPTerm imp bnd ty <>

59− showDoc d' <> line

61+ pprintPTerm imp bnd [] ty <>

62+ showDoc d <> line

6063 :

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

6265 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

src/Idris/Prover.hs+5−5

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

104104 where

105105 showImplicits = opt_showimp (idris_options ist)

106106

107− tPretty bnd t = pprintPTerm showImplicits bnd $ delab ist t

107+ tPretty bnd t = pprintPTerm showImplicits bnd [] $ delab ist t

108108

109109 assumptionNames :: Env -> [Name]

110110 assumptionNames = map fst

@@ -236,8 +236,8 @@ ploop fn d prompt prf e h

236236 TType _ ->

237237 ihPrintTermWithType h (prettyImp imp PType) type1Doc

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

239− ihPrintTermWithType h (pprintPTerm imp bnd (delab ist tm))

240− (pprintPTerm imp bnd (delab ist ty))

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

240+ (pprintPTerm imp bnd [] (delab ist ty))

241241 putIState ist

242242 return (False, e, False, prf))

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

@@ -254,8 +254,8 @@ ploop fn d prompt prf e h

254254 let tm' = force (normaliseAll ctxt' env tm)

255255 ty' = force (normaliseAll ctxt' env ty)

256256 imp = opt_showimp (idris_options ist')

257− tmDoc = pprintPTerm imp bnd (delab ist' tm')

258− tyDoc = pprintPTerm imp bnd (delab ist' ty')

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

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

259259 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

260260 putIState ist

261261 return (False, e, False, prf))

src/Idris/REPL.hs+1−1

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

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

520520 align (tPretty bnd ist g)

521521

522− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd t

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

523523

524524

525525process h fn (Check t)

test/Makefile+1−1

@@ -11,7 +11,7 @@ test_java:

1111 perl ./runtest.pl without sugar004 buffer001 --codegen Java

1212

1313test_js:

14− @perl ./runtest.pl without sugar004 reg029 io001 dsl002 io003 effects001 effects002 buffer001 bounded001 --codegen node

14+ @perl ./runtest.pl without sugar004 reg029 io001 dsl002 io003 effects001 effects002 buffer001 bounded001 folding002 --codegen node

1515

1616test_llvm:

1717 @perl ./runtest.pl without sugar004 io003 buffer001 --codegen llvm