4d2185b · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -434,7 +434,7 @@ Library

434

435 Build-depends: base >=4 && <5

436 , Cabal

437− , annotated-wl-pprint

437+ , annotated-wl-pprint >= 0.5.3

438 , ansi-terminal

439 , ansi-wl-pprint

440 , binary

src/Idris/AbsSyntax.hs+27−1

@@ -397,6 +397,31 @@ ihPrintResult h s = do i <- getIState

397 let good = SexpList [SymbolAtom "ok", toSExp s] in

398 runIO $ hPutStrLn h $ convSExp "return" good n

399

400+ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

401+ihPrintTermWithType h tm ty = do ist <- getIState

402+ let output = tm <+> colon <+> ty

403+ case idris_outputmode ist of

404+ RawOutput -> runIO .

405+ hPutStrLn h .

406+ displayDecorated (consoleDecorate ist) .

407+ renderCompact $ output

408+ IdeSlave n -> let (str, spans) = displaySpans (fmap (fancifyAnnots ist) (renderCompact output))

409+ good = [SymbolAtom "ok", toSExp str, toSExp spans]

410+ in runIO . hPutStrLn h $ convSExp "return" good n

411+

412+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

413+fancifyAnnots ist annot@(AnnName n _ _) =

414+ do let ctxt = tt_ctxt ist

415+ case () of

416+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing

417+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing

418+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing

419+ _ | otherwise -> annot

420+fancifyAnnots _ annot = annot

421+

422+type1Doc :: Doc OutputAnnotation

423+type1Doc = (annotate AnnConstType $ text "Type 1")

424+

400ihPrintError :: Handle -> String -> Idris ()

425ihPrintError :: Handle -> String -> Idris ()

401ihPrintError h s = do i <- getIState

426ihPrintError h s = do i <- getIState

402 case idris_outputmode i of

427 case idris_outputmode i of

@@ -429,7 +454,8 @@ iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

429iputGoal g = do i <- getIState

454iputGoal g = do i <- getIState

430 case idris_outputmode i of

455 case idris_outputmode i of

431 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

456 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

432− IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" (displayS g "") n

457+ IdeSlave n -> runIO . putStrLn $

458+ convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n

433

459

434isetPrompt :: String -> Idris ()

460isetPrompt :: String -> Idris ()

435isetPrompt p = do i <- getIState

461isetPrompt p = do i <- getIState

src/Idris/Delaborate.hs+5−5

@@ -50,8 +50,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

50 | Just n' <- lookup n env = PRef un n'

51 | otherwise

52 = case lookup n (idris_metavars ist) of

53− Just (Just _, mi, _) -> mkMVApp (dens n) []

53+ Just (Just _, mi, _) -> mkMVApp n []

54− _ -> PRef un (dens n)

54+ _ -> PRef un n

55 de env _ (Bind n (Lam ty) sc)

56 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

57 de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)

@@ -96,9 +96,9 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

96 deFn env (P _ n _) args | not mvs

97 = case lookup n (idris_metavars ist) of

98 Just (Just _, mi, _) ->

99− mkMVApp (dens n) (drop mi (map (de env []) args))

99+ mkMVApp n (drop mi (map (de env []) args))

100− _ -> mkPApp (dens n) (map (de env []) args)

100+ _ -> mkPApp n (map (de env []) args)

101− | otherwise = mkPApp (dens n) (map (de env []) args)

101+ | otherwise = mkPApp n (map (de env []) args)

102 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

103

104 mkMVApp n []

src/Idris/IdeSlave.hs+17

@@ -69,6 +69,23 @@ instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where

69instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where

70 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]

71

72+instance SExpable NameOutput where

73+ toSExp TypeOutput = SymbolAtom "type"

74+ toSExp FunOutput = SymbolAtom "function"

75+ toSExp DataOutput = SymbolAtom "data"

76+

77+instance SExpable OutputAnnotation where

78+ toSExp (AnnName n Nothing _) = toSExp [(SymbolAtom "name", StringAtom (show n)),

79+ (SymbolAtom "implicit", BoolAtom False)]

80+ toSExp (AnnName n (Just ty) _) = toSExp [(SymbolAtom "name", StringAtom (show n)),

81+ (SymbolAtom "decor", toSExp ty),

82+ (SymbolAtom "implicit", BoolAtom False)]

83+ toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

84+ (SymbolAtom "decor", SymbolAtom "bound"),

85+ (SymbolAtom "implicit", BoolAtom imp)]

86+ toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]

87+ toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]

88+

72escape :: String -> String

89escape :: String -> String

73escape = concatMap escapeChar

90escape = concatMap escapeChar

74 where

91 where

src/Idris/REPL.hs+11−6

@@ -448,8 +448,11 @@ process h fn (Eval t)

448 ist <- getIState

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

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

451− ihPrintResult h (showTm ist (delab ist tm') ++ " : " ++

451+ let imp = opt_showimp (idris_options ist)

452+ tmDoc = prettyImp imp (delab ist tm')

452− showTm ist (delab ist ty'))

453+ tyDoc = prettyImp imp (delab ist ty')

454+ ihPrintTermWithType h tmDoc tyDoc

455+

453process h fn (ExecVal t)

456process h fn (ExecVal t)

454 = do ctxt <- getContext

457 = do ctxt <- getContext

455 ist <- getIState

458 ist <- getIState

@@ -497,11 +500,13 @@ process h fn (Check t)

497 = do (tm, ty) <- elabVal toplevel False t

500 = do (tm, ty) <- elabVal toplevel False t

498 ctxt <- getContext

501 ctxt <- getContext

499 ist <- getIState

502 ist <- getIState

503+ let imp = opt_showimp (idris_options ist)

500− let ty' = normaliseC ctxt [] ty

504+ ty' = normaliseC ctxt [] ty

501 case tm of

505 case tm of

502− TType _ -> ihPrintResult h ("Type : Type 1")

506+ TType _ ->

503− _ -> ihPrintResult h (showTm ist (delab ist tm) ++ " : " ++

507+ ihPrintTermWithType h (prettyImp imp PType) type1Doc

508+ _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))

504− showTm ist (delab ist ty))

509+ (prettyImp imp (delab ist ty))

505

510

506process h fn (DocStr n)

511process h fn (DocStr n)

507 = do i <- getIState

512 = do i <- getIState