e46603a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'upstream/master' into error-reflection

e46603aDavid Raymond Christiansen13 years ago

idris.cabal+2

compare with master

unifiedsplit

@@ -437,6 +437,7 @@ Library

437

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

439 , Cabal

440+ , annotated-wl-pprint >= 0.5.3

440 , ansi-terminal

441 , ansi-terminal

441 , ansi-wl-pprint

442 , ansi-wl-pprint

442 , binary

443 , binary

@@ -466,6 +467,7 @@ Library

466 , zlib

467 , zlib

467 Extensions: MultiParamTypeClasses

468 Extensions: MultiParamTypeClasses

468 , FunctionalDependencies

469 , FunctionalDependencies

470+ , FlexibleContexts

469 , FlexibleInstances

471 , FlexibleInstances

470 , TemplateHaskell

472 , TemplateHaskell

471

473

libs/prelude/Prelude/Vect.idr+26

@@ -99,6 +99,32 @@ unzip : Vect n (a, b) -> (Vect n a, Vect n b)

99unzip [] = ([], [])

100unzip ((l, r)::xs) with (unzip xs)

101 | (lefts, rights) = (l::lefts, r::rights)

102+

103+--------------------------------------------------------------------------------

104+-- Equality

105+--------------------------------------------------------------------------------

106+

107+instance (Eq a) => Eq (Vect n a) where

108+ (==) [] [] = True

109+ (==) (x::xs) (y::ys) =

110+ if x == y then

111+ xs == ys

112+ else

113+ False

114+

115+

116+--------------------------------------------------------------------------------

117+-- Order

118+--------------------------------------------------------------------------------

119+

120+instance Ord a => Ord (Vect n a) where

121+ compare [] [] = EQ

122+ compare (x::xs) (y::ys) =

123+ if x /= y then

124+ compare x y

125+ else

126+ compare xs ys

127+

102

128

103--------------------------------------------------------------------------------

129--------------------------------------------------------------------------------

104-- Maps

130-- Maps

main/Main.hs+12−14

@@ -89,18 +89,16 @@ usagemsg = usagemsghdr ++ "\n" ++

89 map (\x -> '-') usagemsghdr ++ "\n" ++

90 "idris [OPTIONS] [FILE]\n\n" ++

91 "Common flags:\n" ++

92− "\t --install=IPKG Install Package\n" ++

92+ "\t --install=IPKG Install package\n" ++

93− "\t --clean=IPKG Clean Package\n" ++

93+ "\t --clean=IPKG Clean package\n" ++

94− "\t --build=IPKG Build Package\n" ++

94+ "\t --build=IPKG Build package\n" ++

95− "\t --exec=EXPR Execute as Idris\n" ++

95+ "\t --exec=EXPR Execute as idris\n" ++

96 "\t --libdir Display library directory\n" ++

97 "\t --link Display link directory\n" ++

98 "\t --include Display the includes directory\n" ++

99 "\t --nobanner Suppress the banner\n" ++

100− "\t --color Force colored output\n" ++

101− "\t --colour Force coloured output\n" ++

100+ "\t --color, --colour Force coloured output\n" ++

102− "\t --nocolor Disable colored output\n" ++

103− "\t --nocolour Disable coloured output\n" ++

101+ "\t --nocolor, --nocolour Disable coloured output\n" ++

104 "\t --errorcontent Undocumented\n" ++

102 "\t --errorcontent Undocumented\n" ++

105 "\t --nocoverage Undocumented\n" ++

103 "\t --nocoverage Undocumented\n" ++

106 "\t -o --output=FILE Specify output file\n" ++

104 "\t -o --output=FILE Specify output file\n" ++

@@ -118,22 +116,22 @@ usagemsg = usagemsghdr ++ "\n" ++

118 "\t -i --idrispath=DIR Add directory to the list of import paths\n" ++

116 "\t -i --idrispath=DIR Add directory to the list of import paths\n" ++

119 "\t --package=ITEM Undocumented\n" ++

117 "\t --package=ITEM Undocumented\n" ++

120 "\t --ibcsubdir=FILE Write IBC files into sub directory\n" ++

118 "\t --ibcsubdir=FILE Write IBC files into sub directory\n" ++

121− "\t --codegen=TARGET Select code generator: C, Java, bytecode," ++

119+ "\t --codegen=TARGET Select code generator: C, Java, bytecode,\n" ++

122 "\t javascript, node, or llvm\n" ++

120 "\t javascript, node, or llvm\n" ++

123 "\t --mvn Create a maven project (for Java codegen)\n" ++

121 "\t --mvn Create a maven project (for Java codegen)\n" ++

124− "\t --cpu=CPU Select tartget CPU e.g. corei& or cortex-m3" ++

122+ "\t --cpu=CPU Select tartget CPU e.g. corei7 or cortex-m3\n" ++

125 "\t (for LLVM codegen)\n" ++

123 "\t (for LLVM codegen)\n" ++

126 "\t --target=TRIPLE Select target triple (for llvm codegen)\n" ++

124 "\t --target=TRIPLE Select target triple (for llvm codegen)\n" ++

127 "\t -S --codegenonly Do no further compilation of code generator output\n" ++

125 "\t -S --codegenonly Do no further compilation of code generator output\n" ++

128− "\t -c --compileonly Compile to object fules rather than an executable\n" ++

126+ "\t -c --compileonly Compile to object files rather than an executable\n" ++

129− "\t -X --extension=ITEM undocumented\n" ++

127+ "\t -X --extension=ITEM Undocumented\n" ++

130 "\t --dumpdefuns Undocumented\n" ++

128 "\t --dumpdefuns Undocumented\n" ++

131 "\t --dumpcases Undocumented\n" ++

129 "\t --dumpcases Undocumented\n" ++

132− "\t --log=LEVEL --loglevel Type Debugging log level\n" ++

130+ "\t --log=LEVEL --loglevel Debugging log level\n" ++

133 "\t --ideslave Undocumented\n" ++

131 "\t --ideslave Undocumented\n" ++

134 "\t --client Undocumented\n" ++

132 "\t --client Undocumented\n" ++

135 "\t -h --help Display help message\n" ++

133 "\t -h --help Display help message\n" ++

136 "\t -v --version Print version information\n" ++

134 "\t -v --version Print version information\n" ++

137− "\t -V --Verbose Loud verbosity\n" ++

135+ "\t -V --verbose Loud verbosity\n" ++

138 "\t -q --quiet Quiet verbosity\n"

136 "\t -q --quiet Quiet verbosity\n"

139

137

src/IRTS/CodegenJavaScript.hs+254−56

@@ -258,20 +258,8 @@ jsSubst var new (JSIdent old)

258jsSubst var new (JSArray fields) =

259 JSArray (map (jsSubst var new) fields)

260

261−jsSubst var new (JSNew con [tag, vals]) =

261+jsSubst var new (JSNew con vals) =

262− JSNew con [tag, jsSubst var new vals]

263−

264−jsSubst var new (JSNew con [JSFunction [] (JSReturn (JSApp fun vars))]) =

265− JSNew con [JSFunction [] (

266− JSReturn $ JSApp (jsSubst var new fun) (map (jsSubst var new) vars)

262+ JSNew con $ map (jsSubst var new) vals

267− )]

268−

269−jsSubst var new (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

270− JSReturn (JSApp fun args)

271− )]) =

272− JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

273− JSReturn $ JSApp (jsSubst var new fun) (map (jsSubst var new) args)

274− )]

275

263

276jsSubst var new (JSApp (JSProj (JSFunction args body) "apply") vals)

264jsSubst var new (JSApp (JSProj (JSFunction args body) "apply") vals)

277 | var `notElem` args =

265 | var `notElem` args =

@@ -283,9 +271,6 @@ jsSubst var new (JSApp (JSProj (JSFunction args body) "apply") vals)

283 map (jsSubst var new) vals

271 map (jsSubst var new) vals

284 )

272 )

285

273

286−jsSubst var new (JSApp (JSProj obj field) args) =

287− JSApp (JSProj (jsSubst var new obj) field) $ map (jsSubst var new) args

288−

289jsSubst var new (JSApp (JSFunction [arg] body) vals)

274jsSubst var new (JSApp (JSFunction [arg] body) vals)

290 | var /= arg =

275 | var /= arg =

291 JSApp (JSFunction [arg] (

276 JSApp (JSFunction [arg] (

@@ -296,6 +281,12 @@ jsSubst var new (JSApp (JSFunction [arg] body) vals)

296 body

281 body

297 )) $ map (jsSubst var new) vals

282 )) $ map (jsSubst var new) vals

298

283

284+jsSubst var new (JSApp lhs rhs) =

285+ JSApp (jsSubst var new lhs) (map (jsSubst var new) rhs)

286+

287+jsSubst var new (JSFunction [] body) =

288+ JSFunction [] (jsSubst var new body)

289+

299jsSubst var new (JSReturn ret) =

290jsSubst var new (JSReturn ret) =

300 JSReturn $ jsSubst var new ret

291 JSReturn $ jsSubst var new ret

301

292

@@ -317,9 +308,64 @@ jsSubst var new (JSCond conds) =

317jsSubst var new (JSAssign lhs rhs) =

308jsSubst var new (JSAssign lhs rhs) =

318 JSAssign (jsSubst var new lhs) (jsSubst var new rhs)

309 JSAssign (jsSubst var new lhs) (jsSubst var new rhs)

319

310

311+jsSubst var new (JSAlloc val (Just js)) =

312+ JSAlloc val (Just (jsSubst var new js))

313+

320jsSubst _ _ js = js

314jsSubst _ _ js = js

321

315

322

316

317+removeAllocations :: JS -> JS

318+removeAllocations (JSSeq body) =

319+ let opt = removeHelper (map removeAllocations body) in

320+ case opt of

321+ [ret] -> ret

322+ _ -> JSSeq opt

323+ where

324+ removeHelper :: [JS] -> [JS]

325+ removeHelper [js] = [js]

326+ removeHelper ((JSAlloc name (Just val@(JSIdent _))):js) =

327+ map (jsSubst name val) (removeHelper js)

328+ removeHelper (j:js) = j : removeHelper js

329+

330+removeAllocations (JSFunction args body) =

331+ JSFunction args $ removeAllocations body

332+

333+removeAllocations (JSReturn ret) =

334+ JSReturn $ removeAllocations ret

335+

336+removeAllocations (JSApp fun args) =

337+ JSApp (removeAllocations fun) (map removeAllocations args)

338+

339+removeAllocations (JSNew con args) =

340+ JSNew con $ map removeAllocations args

341+

342+removeAllocations (JSOp op lhs rhs) =

343+ JSOp op (removeAllocations lhs) (removeAllocations rhs)

344+

345+removeAllocations (JSProj obj field) =

346+ JSProj (removeAllocations obj) field

347+

348+removeAllocations (JSArray vals) =

349+ JSArray $ map removeAllocations vals

350+

351+removeAllocations (JSAssign lhs rhs) =

352+ JSAssign (removeAllocations lhs) (removeAllocations rhs)

353+

354+removeAllocations (JSAlloc name (Just val)) =

355+ JSAlloc name $ Just (removeAllocations val)

356+

357+removeAllocations (JSIndex val idx) =

358+ JSIndex (removeAllocations val) (removeAllocations idx)

359+

360+removeAllocations (JSCond conds) =

361+ JSCond $ map (removeAllocations *** removeAllocations) conds

362+

363+removeAllocations (JSTernary c t f) =

364+ JSTernary (removeAllocations c) (removeAllocations t) (removeAllocations f)

365+

366+removeAllocations js = js

367+

368+

323isJSConstant :: JS -> Bool

369isJSConstant :: JS -> Bool

324isJSConstant js

370isJSConstant js

325 | JSString _ <- js = True

371 | JSString _ <- js = True

@@ -386,13 +432,9 @@ inlineJS (JSApp (JSFunction [arg] (JSReturn ret)) [val])

386 JSOp op (jsSubst arg opt lhs) $

432 JSOp op (jsSubst arg opt lhs) $

387 (jsSubst arg opt rhs)

433 (jsSubst arg opt rhs)

388

434

389− | JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

435+ | JSApp (JSIdent fun) args <- ret

390− JSReturn (JSApp fun args)

391− )] <- ret

392 , opt <- inlineJS val =

436 , opt <- inlineJS val =

393− JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

394− JSReturn $ JSApp (jsSubst arg opt fun) (map (jsSubst arg opt) args)

437+ JSApp (JSIdent fun) $ map (jsSubst arg opt) args

395− )]

396

438

397inlineJS (JSApp fun args) =

439inlineJS (JSApp fun args) =

398 JSApp (inlineJS fun) (map inlineJS args)

440 JSApp (inlineJS fun) (map inlineJS args)

@@ -438,6 +480,62 @@ reduceJS js = reduceLoop [] ([], js)

438funName :: JS -> String

480funName :: JS -> String

439funName (JSAlloc fun _) = fun

481funName (JSAlloc fun _) = fun

440

482

483+

484+deadEvalApplyCases :: [JS] -> [JS]

485+deadEvalApplyCases js =

486+ let tags = sort $ nub $ concatMap (getTags) js in

487+ map (removeHelper tags) js

488+ where

489+ getTags :: JS -> [Int]

490+ getTags (JSNew "__IDRRT__Con" [JSNum (JSInt tag), args]) =

491+ tag : getTags args

492+

493+ getTags (JSNew _ args) = concatMap getTags args

494+

495+ getTags (JSFunction _ body) = getTags body

496+

497+ getTags (JSReturn ret) = getTags ret

498+

499+ getTags (JSApp lhs rhs) = getTags lhs ++ concatMap getTags rhs

500+

501+ getTags (JSSeq seq) = concatMap getTags seq

502+

503+ getTags (JSOp _ lhs rhs) = getTags lhs ++ getTags rhs

504+

505+ getTags (JSProj obj _) = getTags obj

506+

507+ getTags (JSArray vals) = concatMap getTags vals

508+

509+ getTags (JSAssign lhs rhs) = getTags lhs ++ getTags rhs

510+

511+ getTags (JSAlloc _ (Just val)) = getTags val

512+

513+ getTags (JSCond conds) =

514+ concatMap (uncurry (++)) $ map (getTags *** getTags) conds

515+

516+ getTags (JSTernary c t f) = getTags c ++ getTags t ++ getTags f

517+

518+ getTags js = []

519+ removeHelper :: [Int] -> JS -> JS

520+ removeHelper tags (JSAlloc fun (Just (

521+ JSApp (JSFunction [] (JSSeq seq)) []))

522+ ) =

523+ (JSAlloc fun (Just (

524+ JSApp (JSFunction [] (JSSeq $ remover tags seq)) []))

525+ )

526+

527+ removeHelper _ js = js

528+

529+ remover :: [Int] -> [JS] -> [JS]

530+ remover tags (

531+ j@(JSAssign ((JSIndex (JSIdent "t") (JSNum (JSInt tag)))) _):js

532+ )

533+ | tag `notElem` tags = remover tags js

534+

535+ remover tags (j:js) = j : remover tags js

536+ remover _ [] = []

537+

538+

441initConstructors :: [JS] -> [JS]

539initConstructors :: [JS] -> [JS]

442initConstructors js =

540initConstructors js =

443 let tags = nub $ sort $ concat (map getTags js) in

541 let tags = nub $ sort $ concat (map getTags js) in

@@ -592,6 +690,92 @@ removeIDs js =

592

690

593 removeIDCall _ js = js

691 removeIDCall _ js = js

594

692

693+inlineFunctions :: [JS] -> [JS]

694+inlineFunctions js =

695+ let funs = collectFunctions js

696+ occurences = map ((id . fst) &&& countAll js) funs in

697+ removeDeadFunctions occurences js

698+ where

699+ removeDeadFunctions :: [(String, (Int, JS))] -> [JS] -> [JS]

700+ removeDeadFunctions _ [] = []

701+ removeDeadFunctions funOccur ((JSAlloc fun (Just (JSFunction _ _))):js)

702+ | Just (o, _) <- lookup fun funOccur

703+ , o == 0 = removeDeadFunctions funOccur js

704+

705+ removeDeadFunctions funOccur (j:js) = j : removeDeadFunctions funOccur js

706+

707+

708+ collectFunctions :: [JS] -> [(String, JS)]

709+ collectFunctions js =

710+ catMaybes $ map collectHelper js

711+

712+

713+ collectHelper :: JS -> Maybe (String, JS)

714+ collectHelper (JSAlloc fun (Just js@(JSFunction _ body)))

715+ | fun /= "main" && nonRecur fun body = Just (fun, js)

716+ collectHelper _ = Nothing

717+

718+

719+ nonRecur :: String -> JS -> Bool

720+ nonRecur name body = countInvokations name body == 0

721+

722+

723+ countAll :: [JS] -> (String, JS) -> (Int, JS)

724+ countAll js (name, fun) = (sum $ map (countInvokations name) js, fun)

725+

726+

727+ countInvokations :: String -> JS -> Int

728+ countInvokations name (JSApp (JSIdent ident) args)

729+ | name == ident = 1 + (sum $ map (countInvokations name) args)

730+ | otherwise = sum $ map (countInvokations name) args

731+

732+ countInvokations name (JSApp lhs rhs) =

733+ countInvokations name lhs + (sum $ map (countInvokations name) rhs)

734+

735+ countInvokations name (JSFunction _ body) =

736+ countInvokations name body

737+

738+ countInvokations name (JSSeq seq) =

739+ sum $ map (countInvokations name) seq

740+

741+ countInvokations name (JSReturn ret) =

742+ countInvokations name ret

743+

744+ countInvokations name (JSNew _ args) =

745+ sum $ map (countInvokations name) args

746+

747+ countInvokations name (JSOp _ lhs rhs) =

748+ countInvokations name lhs + countInvokations name rhs

749+

750+ countInvokations name (JSProj obj _) =

751+ countInvokations name obj

752+

753+ countInvokations name (JSArray vals) =

754+ sum $ map (countInvokations name) vals

755+

756+ countInvokations name (JSAssign _ rhs) =

757+ countInvokations name rhs

758+

759+ countInvokations name (JSAlloc _ (Just js)) =

760+ countInvokations name js

761+

762+ countInvokations name (JSIndex lhs rhs) =

763+ countInvokations name lhs + countInvokations name rhs

764+

765+ countInvokations name (JSCond conds) =

766+ sum $ map (uncurry (+)) (

767+ map (countInvokations name *** countInvokations name) conds

768+ )

769+

770+ countInvokations name (JSTernary c t f) =

771+ sum $ [ countInvokations name c

772+ , countInvokations name t

773+ , countInvokations name f

774+ ]

775+

776+ countInvokations _ _ = 0

777+

778+

595reduceConstant :: JS -> JS

779reduceConstant :: JS -> JS

596reduceConstant (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

780reduceConstant (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

597 JSReturn (JSApp (JSIdent "__IDR__mEVAL0") [JSNum num])

781 JSReturn (JSApp (JSIdent "__IDR__mEVAL0") [JSNum num])

@@ -736,7 +920,7 @@ codegenJavaScript target definitions filename outputType = do

736 intercalate "\n" $ [ jsbn

920 intercalate "\n" $ [ jsbn

737 , idrRuntime

921 , idrRuntime

738 , tgtRuntime

922 , tgtRuntime

739− ] ++ functions ++ [mainLoop, invokeLoop]

923+ ] ++ functions

740 )

924 )

741

925

742 setPermissions filename (emptyPermissions { readable = True

926 setPermissions filename (emptyPermissions { readable = True

@@ -749,10 +933,21 @@ codegenJavaScript target definitions filename outputType = do

749

933

750 functions :: [String]

934 functions :: [String]

751 functions =

935 functions =

752− map compileJS $ initConstructors (map reduceConstants ((reduceJS . removeIDs) $ map (optimizeJS . translateDeclaration) def))

936+ let translated =

753−

937+ concatMap translateDeclaration def ++ [mainLoop, invokeLoop]

938+

939+ optimized = map optimizeJS translated

940+ idsRemoved = removeIDs optimized

941+ reduced = reduceJS idsRemoved

942+ constRemoved = map reduceConstants reduced

943+ constrInit = initConstructors constRemoved

944+ removeAlloc = map removeAllocations constrInit

945+ deadElim = deadEvalApplyCases removeAlloc

946+ js = inlineFunctions deadElim in

947+ map compileJS js

948+

754− mainLoop :: String

949+ mainLoop :: JS

755− mainLoop = compileJS $

950+ mainLoop =

756 JSAlloc "main" $ Just $ JSFunction [] (

951 JSAlloc "main" $ Just $ JSFunction [] (

757 case target of

952 case target of

758 Node -> mainFun

953 Node -> mainFun

@@ -769,8 +964,8 @@ codegenJavaScript target definitions filename outputType = do

769 runMain :: String

964 runMain :: String

770 runMain = idrNamespace ++ translateName (sMN 0 "runMain")

965 runMain = idrNamespace ++ translateName (sMN 0 "runMain")

771

966

772− invokeLoop :: String

967+ invokeLoop :: JS

773− invokeLoop = compileJS $ jsCall "main" []

968+ invokeLoop = jsCall "main" []

774

969

775translateIdentifier :: String -> String

970translateIdentifier :: String -> String

776translateIdentifier =

971translateIdentifier =

@@ -876,7 +1071,7 @@ translateConstant (BI i) = jsBigInt $ JSString (show i)

876translateConstant c =

1071translateConstant c =

877 JSError $ "Unimplemented Constant: " ++ show c

1072 JSError $ "Unimplemented Constant: " ++ show c

878

1073

879−translateDeclaration :: (String, SDecl) -> JS

1074+translateDeclaration :: (String, SDecl) -> [JS]

880translateDeclaration (path, SFun name params stackSize body)

1075translateDeclaration (path, SFun name params stackSize body)

881 | (MN _ ap) <- name

1076 | (MN _ ap) <- name

882 , (SLet var val next) <- body

1077 , (SLet var val next) <- body

@@ -884,37 +1079,40 @@ translateDeclaration (path, SFun name params stackSize body)

884 , ap == txt "APPLY" =

1079 , ap == txt "APPLY" =

885 let lvar = translateVariableName var

1080 let lvar = translateVariableName var

886 lookup = "[" ++ lvar ++ ".tag](fn0,arg0," ++ lvar ++ ")" in

1081 lookup = "[" ++ lvar ++ ".tag](fn0,arg0," ++ lvar ++ ")" in

887− JSSeq [ lookupTable [(var, "chk")] var cases

1082+ [ lookupTable [(var, "chk")] var cases

888− , jsDecl $ JSFunction ["fn0", "arg0"] (

1083+ , jsDecl $ JSFunction ["fn0", "arg0"] (

889− JSSeq [ JSAlloc "__var_0" (Just $ JSIdent "fn0")

1084+ JSSeq [ JSAlloc "__var_0" (Just $ JSIdent "fn0")

890− , JSAlloc (translateVariableName var) (

1085+ , JSAlloc (translateVariableName var) (

891− Just $ translateExpression val

1086+ Just $ translateExpression val

892− )

1087+ )

893− , JSReturn $ (JSTernary (

1088+ , JSReturn $ (JSTernary (

894− (JSVar var `jsInstanceOf` jsCon) `jsAnd`

1089+ (JSVar var `jsInstanceOf` jsCon) `jsAnd`

895− (hasProp lookupTableName (translateVariableName var))

1090+ (hasProp lookupTableName (translateVariableName var))

896− ) (JSIdent $

1091+ ) (JSIdent $

897− lookupTableName ++ lookup

1092+ lookupTableName ++ lookup

898− ) JSNull

1093+ ) JSNull

899− )

1094+ )

900− ]

1095+ ]

901− )

1096+ )

902− ]

1097+ ]

903

1098

904 | (MN _ ev) <- name

1099 | (MN _ ev) <- name

905 , (SChkCase var cases) <- body

1100 , (SChkCase var cases) <- body

906 , ev == txt "EVAL" =

1101 , ev == txt "EVAL" =

907− JSSeq [ lookupTable [] var cases

1102+ [ lookupTable [] var cases

908− , jsDecl $ JSFunction ["arg0"] (JSReturn $

1103+ , jsDecl $ JSFunction ["arg0"] (JSReturn $

909− JSTernary (

1104+ JSTernary (

910− (JSIdent "arg0" `jsInstanceOf` jsCon) `jsAnd`

1105+ (JSIdent "arg0" `jsInstanceOf` jsCon) `jsAnd`

911− (hasProp lookupTableName "arg0")

1106+ (hasProp lookupTableName "arg0")

1107+ ) (JSApp

912− ) (JSRaw $ lookupTableName ++ "[arg0.tag](arg0)") (JSIdent "arg0")

1108+ (JSIndex (JSIdent lookupTableName) (JSProj (JSIdent "arg0") "tag"))

1109+ [JSIdent "arg0"]

1110+ ) (JSIdent "arg0")

913− )

1111+ )

914− ]

1112+ ]

915 | otherwise =

1113 | otherwise =

916 let fun = translateExpression body in

1114 let fun = translateExpression body in

917− jsDecl $ jsFun fun

1115+ [jsDecl $ jsFun fun]

918

1116

919 where

1117 where

920 hasProp :: String -> String -> JS

1118 hasProp :: String -> String -> JS

src/Idris/AbsSyntax.hs+56−89

@@ -417,6 +417,55 @@ ihPrintResult h s = do i <- getIState

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

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

419

420+-- | Write a pretty-printed term to the console with semantic coloring

421+consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

422+consoleDisplayAnnotated h output = do ist <- getIState

423+ runIO . hPutStrLn h .

424+ displayDecorated (consoleDecorate ist) .

425+ renderCompact $ output

426+

427+-- | Write pretty-printed output to IDESlave with semantic annotations

428+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

429+ideSlaveReturnAnnotated n h out = do ist <- getIState

430+ let (str, spans) = displaySpans .

431+ renderCompact .

432+ fmap (fancifyAnnots ist) $

433+ out

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

435+ runIO . hPutStrLn h $ convSExp "return" good n

436+

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

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

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

440+ case idris_outputmode ist of

441+ RawOutput -> consoleDisplayAnnotated h output

442+ IdeSlave n -> ideSlaveReturnAnnotated n h output

443+

444+-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

445+ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()

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

447+ihPrintFunTypes h n overloads = do imp <- impShow

448+ ist <- getIState

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

450+ case idris_outputmode ist of

451+ RawOutput -> consoleDisplayAnnotated h output

452+ IdeSlave n -> ideSlaveReturnAnnotated n h output

453+ where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)

454+ ppOverload imp n tm = fullName n <+> colon <+> prettyImp imp tm

455+

456+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

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

458+ do let ctxt = tt_ctxt ist

459+ case () of

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

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

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

463+ _ | otherwise -> annot

464+fancifyAnnots _ annot = annot

465+

466+type1Doc :: Doc OutputAnnotation

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

468+

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

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

421ihPrintError h s = do i <- getIState

470ihPrintError h s = do i <- getIState

422 case idris_outputmode i of

471 case idris_outputmode i of

@@ -445,11 +494,12 @@ ideslavePutSExp cmd info = do i <- getIState

445 _ -> return ()

494 _ -> return ()

446

495

447-- this needs some typing magic and more structured output towards emacs

496-- this needs some typing magic and more structured output towards emacs

448−iputGoal :: String -> Idris ()

497+iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

449−iputGoal s = do i <- getIState

498+iputGoal g = do i <- getIState

450 case idris_outputmode i of

499 case idris_outputmode i of

451− RawOutput -> runIO $ putStrLn s

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

452− IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n

501+ IdeSlave n -> runIO . putStrLn $

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

453

503

454isetPrompt :: String -> Idris ()

504isetPrompt :: String -> Idris ()

455isetPrompt p = do i <- getIState

505isetPrompt p = do i <- getIState

@@ -722,90 +772,6 @@ setTypeCase t = do i <- getIState

722 putIState $ i { idris_options = opt' }

772 putIState $ i { idris_options = opt' }

723

773

724

774

725−-- For inferring types of things

726−

727−bi = fileFC "builtin"

728−

729−inferTy = sMN 0 "__Infer"

730−inferCon = sMN 0 "__infer"

731−inferDecl = PDatadecl inferTy

732− PType

733− [("", inferCon, PPi impl (sMN 0 "iType") PType (

734− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

735− (PRef bi inferTy)), bi, [])]

736−inferOpts = []

737−

738−infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

739−infP = P (TCon 6 0) inferTy (TType (UVal 0))

740−

741−getInferTerm, getInferType :: Term -> Term

742−getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

743−getInferTerm (App (App _ _) tm) = tm

744−getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

745−

746−getInferType (Bind n b sc) = Bind n b $ getInferType sc

747−getInferType (App (App _ ty) _) = ty

748−

749−-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class

750−

751−primNames = [unitTy, unitCon,

752− falseTy, pairTy, pairCon,

753− eqTy, eqCon, inferTy, inferCon]

754−

755−unitTy = sMN 0 "__Unit"

756−unitCon = sMN 0 "__II"

757−unitDecl = PDatadecl unitTy PType

758− [("", unitCon, PRef bi unitTy, bi, [])]

759−unitOpts = [DefaultEliminator]

760−

761−falseTy = sMN 0 "__False"

762−falseDecl = PDatadecl falseTy PType []

763−falseOpts = []

764−

765−pairTy = sMN 0 "__Pair"

766−pairCon = sMN 0 "__MkPair"

767−pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

768− [("", pairCon, PPi impl (n "A") PType (

769− PPi impl (n "B") PType (

770− PPi expl (n "a") (PRef bi (n "A")) (

771− PPi expl (n "b") (PRef bi (n "B"))

772− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

773− pexp (PRef bi (n "B"))])))), bi, [])]

774− where n a = sMN 0 a

775−pairOpts = []

776−

777−eqTy = sUN "="

778−eqCon = sUN "refl"

779−eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

780− (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

781− PType)

782− [("", eqCon, PPi impl (n "A") PType (

783− PPi impl (n "x") (PRef bi (n "A"))

784− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

785− pimp (n "B") Placeholder False,

786− pexp (PRef bi (n "x")),

787− pexp (PRef bi (n "x"))])), bi, [])]

788− where n a = sMN 0 a

789−eqOpts = []

790−

791−elimName = sUN "__Elim"

792−elimMethElimTy = sUN "__elimTy"

793−elimMethElim = sUN "elim"

794−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

795− [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

796− PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

797−

798−-- Defined in builtins.idr

799−sigmaTy = sUN "Exists"

800−existsCon = sUN "Ex_intro"

801−

802−piBind :: [(Name, PTerm)] -> PTerm -> PTerm

803−piBind = piBindp expl

804−

805−piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

806−piBindp p [] t = t

807−piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

808−

809-- Dealing with parameters

775-- Dealing with parameters

810

776

811expandParams :: (Name -> Name) -> [(Name, PTerm)] ->

777expandParams :: (Name -> Name) -> [(Name, PTerm)] ->

@@ -1472,7 +1438,7 @@ mkPApp fc a f as = let rest = drop a as in

1472-- FIXME: It's possible that this really has to happen after elaboration

1438-- FIXME: It's possible that this really has to happen after elaboration

1473

1439

1474findStatics :: IState -> PTerm -> (PTerm, [Bool])

1440findStatics :: IState -> PTerm -> (PTerm, [Bool])

1475−findStatics ist tm = trace (showImp Nothing True False tm) $

1441+findStatics ist tm = trace (show tm) $

1476 let (ns, ss) = fs tm in

1442 let (ns, ss) = fs tm in

1477 runState (pos ns ss tm) []

1443 runState (pos ns ss tm) []

1478 where fs (PPi p n t sc)

1444 where fs (PPi p n t sc)

@@ -1756,3 +1722,4 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1756 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

1722 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

1757 mkUniq t = return t

1723 mkUniq t = return t

1758

1724

1725+

src/Idris/AbsSyntaxTree.hs+361−351

@@ -32,6 +32,8 @@ import Data.Word (Word)

33import Debug.Trace

35+import Text.PrettyPrint.Annotated.Leijen

36+

35data IOption = IOption { opt_logLevel :: Int,

37data IOption = IOption { opt_logLevel :: Int,

36 opt_typecase :: Bool,

38 opt_typecase :: Bool,

37 opt_typeintype :: Bool,

39 opt_typeintype :: Bool,

@@ -916,275 +918,440 @@ expandNS syn n = case syn_namespace syn of

916 xs -> sNS n xs

918 xs -> sNS n xs

917

919

918

920

919−--- Pretty printing declarations and terms

921+-- For inferring types of things

920

922

921−instance Show PTerm where

923+bi = fileFC "builtin"

922− show tm = showImp Nothing False False tm

923

924

924−instance Pretty PTerm where

925+inferTy = sMN 0 "__Infer"

925− pretty = prettyImp False

926+inferCon = sMN 0 "__infer"

927+inferDecl = PDatadecl inferTy

928+ PType

929+ [("", inferCon, PPi impl (sMN 0 "iType") PType (

930+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

931+ (PRef bi inferTy)), bi, [])]

932+inferOpts = []

926

933

927−instance Show PDecl where

934+infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

928− show d = showDeclImp False d

935+infP = P (TCon 6 0) inferTy (TType (UVal 0))

929

936

930−instance Show PClause where

937+getInferTerm, getInferType :: Term -> Term

931− show c = showCImp True c

938+getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

939+getInferTerm (App (App _ _) tm) = tm

940+getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

932

941

933−instance Show PData where

942+getInferType (Bind n b sc) = Bind n b $ getInferType sc

934− show d = showDImp False d

943+getInferType (App (App _ ty) _) = ty

935

944

936−showDecls :: Bool -> [PDecl] -> String

937−showDecls _ [] = ""

938−showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds

939

945

940−showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

941−showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t

942−showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)

943−showDeclImp _ (PData _ _ _ _ d) = showDImp True d

944−showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"

945−showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"

946−showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn

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

948− = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds

949−showDeclImp i (PInstance _ _ cs n _ t _ ds)

950− = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds

951−showDeclImp _ _ = "..."

952−-- showDeclImp (PImport i) = "import " ++ i

953

946

947+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class

954

948

955−showCImp :: Bool -> PClause -> String

949+primNames = [unitTy, unitCon,

956−showCImp impl (PClause _ n l ws r w)

950+ falseTy, pairTy, pairCon,

957− = showImp Nothing impl False l ++ showWs ws ++ " = " ++ showImp Nothing impl False r

951+ eqTy, eqCon, inferTy, inferCon]

958− ++ " where " ++ show w

959− where

960− showWs [] = ""

961− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs

962−showCImp impl (PWith _ n l ws r w)

963− = showImp Nothing impl False l ++ showWs ws ++ " with " ++ showImp Nothing impl False r

964− ++ " { " ++ show w ++ " } "

965− where

966− showWs [] = ""

967− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs

968

952

953+unitTy = sMN 0 "__Unit"

954+unitCon = sMN 0 "__II"

955+unitDecl = PDatadecl unitTy PType

956+ [("", unitCon, PRef bi unitTy, bi, [])]

957+unitOpts = [DefaultEliminator]

969

958

970−showDImp :: Bool -> PData -> String

959+falseTy = sMN 0 "__False"

971−showDImp impl (PDatadecl n ty cons)

960+falseDecl = PDatadecl falseTy PType []

972− = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"

961+falseOpts = []

973− ++ showSep "\n\t| "

974− (map (\ (_, n, t, _, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)

975

962

976−getImps :: [PArg] -> [(Name, PTerm)]

963+pairTy = sMN 0 "__Pair"

977−getImps [] = []

964+pairCon = sMN 0 "__MkPair"

978−getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs

965+pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

979−getImps (_ : xs) = getImps xs

966+ [("", pairCon, PPi impl (n "A") PType (

967+ PPi impl (n "B") PType (

968+ PPi expl (n "a") (PRef bi (n "A")) (

969+ PPi expl (n "b") (PRef bi (n "B"))

970+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

971+ pexp (PRef bi (n "B"))])))), bi, [])]

972+ where n a = sMN 0 a

973+pairOpts = []

980

974

981−getExps :: [PArg] -> [PTerm]

975+eqTy = sUN "="

982−getExps [] = []

976+eqCon = sUN "refl"

983−getExps (PExp _ _ tm _ : xs) = tm : getExps xs

977+eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

984−getExps (_ : xs) = getExps xs

978+ (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

979+ PType)

980+ [("", eqCon, PPi impl (n "A") PType (

981+ PPi impl (n "x") (PRef bi (n "A"))

982+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

983+ pimp (n "B") Placeholder False,

984+ pexp (PRef bi (n "x")),

985+ pexp (PRef bi (n "x"))])), bi, [])]

986+ where n a = sMN 0 a

987+eqOpts = []

985

988

986−getConsts :: [PArg] -> [PTerm]

989+elimName = sUN "__Elim"

987−getConsts [] = []

990+elimMethElimTy = sUN "__elimTy"

988−getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs

991+elimMethElim = sUN "elim"

989−getConsts (_ : xs) = getConsts xs

992+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

993+ [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

994+ PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

995+

996+-- Defined in builtins.idr

997+sigmaTy = sUN "Exists"

998+existsCon = sUN "Ex_intro"

999+

1000+piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1001+piBind = piBindp expl

1002+

1003+piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

1004+piBindp p [] t = t

1005+piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

990

1006

991−getAll :: [PArg] -> [PTerm]

992−getAll = map getTm

993

1007

1008+-- Pretty-printing declarations and terms

1009+

1010+instance Show PTerm where

1011+ showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm

1012+

1013+instance Show PDecl where

1014+ showsPrec _ d = (displayS . renderCompact . showDeclImp False) d

1015+

1016+instance Show PClause where

1017+ showsPrec _ c = (displayS . renderCompact . showCImp True) c

1018+

1019+instance Show PData where

1020+ showsPrec _ d = (displayS . renderCompact . showDImp False) d

1021+

1022+instance Pretty PTerm OutputAnnotation where

1023+ pretty = prettyImp False

1024+

1025+-- | Colourise annotations according to an Idris state. It ignores the names

1026+-- in the annotation, as there's no good way to show extended information on a

1027+-- terminal.

1028+consoleDecorate :: IState -> OutputAnnotation -> String -> String

1029+consoleDecorate ist _ | not (idris_colourRepl ist) = id

1030+consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist

1031+ in colouriseData theme

1032+consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist

1033+ in colouriseType theme

1034+consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1035+consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1036+consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist

1037+ theme = idris_colourTheme ist

1038+ in case () of

1039+ _ | isDConName n ctxt -> colouriseData theme

1040+ _ | isFnName n ctxt -> colouriseFun theme

1041+ _ | isTConName n ctxt -> colouriseType theme

1042+ _ | otherwise -> id -- don't colourise unknown names

1043+consoleDecorate ist (AnnFC _) = id

1044+

994−-- | Pretty-print a high-level Idris term

1045+-- | Pretty-print a high-level closed Idris term

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

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

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

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

997− -> Doc

1048+ -> Doc OutputAnnotation

998−prettyImp impl = prettySe 10

1049+prettyImp impl = pprintPTerm impl []

1050+

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

1052+pprintPTerm :: Bool -- ^^ whether to show implicits

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

1054+ -> PTerm -- ^^ the term to pretty-print

1055+ -> Doc OutputAnnotation

1056+pprintPTerm impl bnd = prettySe 10 bnd

999 where

1057 where

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

1000− prettySe p (PQuote r) =

1059+ prettySe p bnd (PQuote r) =

1001 if size r > breakingSize then

1060 if size r > breakingSize then

1002− text "![" $$ pretty r <> text "]"

1061+ text "![" <> line <> pretty r <> text "]"

1003 else

1062 else

1004 text "![" <> pretty r <> text "]"

1063 text "![" <> pretty r <> text "]"

1005− prettySe p (PPatvar fc n) = pretty n

1064+ prettySe p bnd (PPatvar fc n) = pretty n

1006− prettySe p (PRef fc n) =

1065+ prettySe p bnd e

1007− if impl then

1066+ | Just str <- slist p bnd e = str

1008− pretty n

1067+ | Just n <- snat p e = annotate AnnConstData (text (show n))

1009− else

1068+ prettySe p bnd (PRef fc n) = prettyName impl bnd n

1010− prettyBasic n

1011− where

1012− prettyBasic n@(UN _) = pretty n

1013− prettyBasic (MN _ s) = text (str s)

1014− prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map (text.str) $ reverse s))) <> prettyBasic n

1015− prettyBasic (SN sn) = text (show sn)

1016− prettySe p (PLam n ty sc) =

1069+ prettySe p bnd (PLam n ty sc) =

1017 bracket p 2 $

1070 bracket p 2 $

1018 if size sc > breakingSize then

1071 if size sc > breakingSize then

1019− text "λ" <> pretty n <+> text "=>" $+$ pretty sc

1072+ text "\\" <> bindingOf n False <+> text "=>" <> line <> prettySe 10 ((n, False):bnd) sc

1020 else

1073 else

1021− text "λ" <> pretty n <+> text "=>" <+> pretty sc

1074+ text "\\" <> bindingOf n False <+> text "=>" <+> prettySe 10 ((n, False):bnd) sc

1022− prettySe p (PLet n ty v sc) =

1075+ prettySe p bnd (PLet n ty v sc) =

1023 bracket p 2 $

1076 bracket p 2 $

1024 if size sc > breakingSize then

1077 if size sc > breakingSize then

1025− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$

1078+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>

1026− nest nestingSize (prettySe 10 sc)

1079+ nest nestingSize (prettySe 10 ((n, False):bnd) sc)

1027 else

1080 else

1028− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>

1081+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>

1029− prettySe 10 sc

1082+ prettySe 10 ((n, False):bnd) sc

1030− prettySe p (PPi (Exp l s _ _) n ty sc)

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

1031 | n `elem` allNamesIn sc || impl =

1084 | n `elem` allNamesIn sc || impl =

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

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

1033 bracket p 2 $

1086 bracket p 2 $

1034 if size sc > breakingSize then

1087 if size sc > breakingSize then

1035− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

1088+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1036− st <+> text "->" $+$ prettySe 10 sc

1089+ st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc

1037 else

1090 else

1038− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

1091+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1039− st <+> text "->" <+> prettySe 10 sc

1092+ st <> text "->" <+> prettySe 10 ((n, False):bnd) sc

1040 | otherwise =

1093 | otherwise =

1041 bracket p 2 $

1094 bracket p 2 $

1042 if size sc > breakingSize then

1095 if size sc > breakingSize then

1043− prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc

1096+ prettySe 0 bnd ty <+> st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc

1044 else

1097 else

1045− prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc

1098+ prettySe 0 bnd ty <+> st <> text "->" <+> prettySe 10 ((n, False):bnd) sc

1046 where

1099 where

1047 st =

1100 st =

1048 case s of

1101 case s of

1049− Static -> text "[static]"

1102+ Static -> text "[static]" <> space

1050 _ -> empty

1103 _ -> empty

1051− prettySe p (PPi (Imp l s _ _) n ty sc)

1104+ prettySe p bnd (PPi (Imp l s _ _) n ty sc)

1052 | impl =

1105 | impl =

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

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

1054 bracket p 2 $

1107 bracket p 2 $

1055 if size sc > breakingSize then

1108 if size sc > breakingSize then

1056− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1109+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1057− st <+> text "->" <+> prettySe 10 sc

1110+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc

1058 else

1111 else

1059− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1112+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1060− st <+> text "->" <+> prettySe 10 sc

1113+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc

1061− | otherwise = prettySe 10 sc

1114+ | otherwise = prettySe 10 ((n, True):bnd) sc

1062 where

1115 where

1063 st =

1116 st =

1064 case s of

1117 case s of

1065− Static -> text $ "[static]"

1118+ Static -> text "[static]" <> space

1066 _ -> empty

1119 _ -> empty

1067− prettySe p (PPi (Constraint _ _ _) n ty sc) =

1120+ prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1068 bracket p 2 $

1121 bracket p 2 $

1069 if size sc > breakingSize then

1122 if size sc > breakingSize then

1070− prettySe 10 ty <+> text "=>" <+> prettySe 10 sc

1123+ prettySe 10 bnd ty <+> text "=>" <+> prettySe 10 ((n, True):bnd) sc

1071 else

1124 else

1072− prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc

1125+ prettySe 10 bnd ty <+> text "=>" <> line <> prettySe 10 ((n, True):bnd) sc

1073− prettySe p (PPi (TacImp _ _ s _) n ty sc) =

1126+ prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =

1074 bracket p 2 $

1127 bracket p 2 $

1075 if size sc > breakingSize then

1128 if size sc > breakingSize then

1076− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

1129+ lbrace <> text "tacimp" <+> bindingOf n True <+> colon <+> prettySe 10 bnd ty <>

1077− rbrace <+> text "->" $+$ prettySe 10 sc

1130+ rbrace <+> text "->" <> line <> prettySe 10 ((n, True):bnd) sc

1078 else

1131 else

1079− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

1132+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1080− rbrace <+> text "->" <+> prettySe 10 sc

1133+ rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc

1081− prettySe p (PApp _ (PRef _ f) [])

1134+ prettySe p bnd (PApp _ (PRef _ f) [])

1082− | not impl = pretty f

1135+ | not impl = prettyName impl bnd f

1083− prettySe p (PAppBind _ (PRef _ f) [])

1136+ prettySe p bnd (PAppBind _ (PRef _ f) [])

1084− | not impl = text "!" <+> pretty f

1137+ | not impl = text "!" <> prettyName impl bnd f

1085− prettySe p (PApp _ (PRef _ op@(UN nm)) args)

1138+ prettySe p bnd (PApp _ (PRef _ op) args)

1139+ | UN nm <- basename op

1086− | not (tnull nm) &&

1140+ , not (tnull nm) &&

1087 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =

1141 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =

1088 let [l, r] = getExps args in

1142 let [l, r] = getExps args in

1089 bracket p 1 $

1143 bracket p 1 $

1090 if size r > breakingSize then

1144 if size r > breakingSize then

1091− prettySe 1 l <+> pretty op $+$ prettySe 0 r

1145+ prettySe 1 bnd l <+> prettyName impl bnd op <> line <> prettySe 0 bnd r

1092 else

1146 else

1093− prettySe 1 l <+> pretty op <+> prettySe 0 r

1147+ prettySe 1 bnd l <+> prettyName impl bnd op <+> prettySe 0 bnd r

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

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

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

1094− prettySe p (PApp _ f as) =

1151+ prettySe p bnd (PApp _ f as) =

1095− let args = getExps as in

1152+ let args = getExps as

1153+ fp = prettySe 1 bnd f

1154+ in

1096 bracket p 1 $

1155 bracket p 1 $

1097− prettySe 1 f <+>

1098− if impl then

1156+ hsep (if impl

1099− foldl' fS empty as

1100− -- foldr (<+>) empty $ map prettyArgS as

1157+ then fp : map (prettyArgS bnd) as

1101− else

1102− foldl' fSe empty args

1103− -- foldr (<+>) empty $ map prettyArgSe args

1158+ else fp : map (prettyArgSe bnd) args)

1159+ prettySe p bnd (PCase _ scr opts) =

1160+ text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody

1104 where

1161 where

1105− fS l r =

1106− if size r > breakingSize then

1107− l $+$ nest nestingSize (prettyArgS r)

1108− else

1109− l <+> prettyArgS r

1110−

1111− fSe l r =

1112− if size r > breakingSize then

1113− l $+$ nest nestingSize (prettyArgSe r)

1114− else

1115− l <+> prettyArgSe r

1116− prettySe p (PCase _ scr opts) =

1117− text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody

1118− where

1119− prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts

1162+ prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts

1120−

1163+

1121− sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r

1164+ sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r

1122− prettySe p (PHidden tm) = text "." <> prettySe 0 tm

1165+ prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1123− prettySe p (PRefl _ _) = text "refl"

1166+ prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"

1124− prettySe p (PResolveTC _) = text "resolvetc"

1167+ prettySe p bnd (PResolveTC _) = text "resolvetc"

1125− prettySe p (PTrue _) = text "()"

1168+ prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1126− prettySe p (PFalse _) = text "_|_"

1169+ prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"

1127− prettySe p (PEq _ l r) =

1170+ prettySe p bnd (PEq _ l r) =

1128 bracket p 2 $

1171 bracket p 2 $

1129 if size r > breakingSize then

1172 if size r > breakingSize then

1130− prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)

1173+ prettySe 10 bnd l <+> eq <$> nest nestingSize (prettySe 10 bnd r)

1131 else

1174 else

1132− prettySe 10 l <+> text "=" <+> prettySe 10 r

1175+ prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r

1176+ where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")

1133− prettySe p (PRewrite _ l r _) =

1177+ prettySe p bnd (PRewrite _ l r _) =

1134 bracket p 2 $

1178 bracket p 2 $

1135 if size r > breakingSize then

1179 if size r > breakingSize then

1136− text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)

1180+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <> nest nestingSize (prettySe 10 bnd r)

1137 else

1181 else

1138− text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r

1182+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1139− prettySe p (PTyped l r) =

1183+ prettySe p bnd (PTyped l r) =

1140− lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen

1184+ lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen

1141− prettySe p (PPair _ l r) =

1185+ prettySe p bnd (PPair _ l r) =

1142 if size r > breakingSize then

1186 if size r > breakingSize then

1143− lparen <> prettySe 10 l <> text "," $+$

1187+ lparen <> prettySe 10 bnd l <> text "," <>

1144− prettySe 10 r <> rparen

1188+ line <> prettySe 10 bnd r <> rparen

1145 else

1189 else

1146− lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen

1190+ lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen

1147− prettySe p (PDPair _ l t r) =

1191+ prettySe p bnd (PDPair _ l t r) =

1148 if size r > breakingSize then

1192 if size r > breakingSize then

1149− lparen <> prettySe 10 l <+> text "**" $+$

1193+ lparen <> prettySe 10 bnd l <+> text "**" <>

1150− prettySe 10 r <> rparen

1194+ line <> prettySe 10 bnd r <> rparen

1151 else

1195 else

1152− lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen

1196+ lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1153− prettySe p (PAlternative a as) =

1197+ prettySe p bnd (PAlternative a as) =

1154 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1198 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1155 where

1199 where

1156 prettyAs =

1200 prettyAs =

1157− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as

1201+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1158− prettySe p PType = text "Type"

1202+ prettySe p bnd PType = annotate AnnConstType $ text "Type"

1159− prettySe p (PConstant c) = pretty c

1203+ prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))

1204+ where annot (AType _) = AnnConstType

1205+ annot StrType = AnnConstType

1206+ annot PtrType = AnnConstType

1207+ annot VoidType = AnnConstType

1208+ annot _ = AnnConstData

1160 -- XXX: add pretty for tactics

1209 -- XXX: add pretty for tactics

1161− prettySe p (PProof ts) =

1210+ prettySe p bnd (PProof ts) =

1162− text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace

1211+ text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1163− prettySe p (PTactics ts) =

1212+ prettySe p bnd (PTactics ts) =

1164− text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace

1213+ text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1165− prettySe p (PMetavar n) = text "?" <> pretty n

1214+ prettySe p bnd (PMetavar n) = text "?" <> pretty n

1166− prettySe p (PReturn f) = text "return"

1215+ prettySe p bnd (PReturn f) = text "return"

1167− prettySe p PImpossible = text "impossible"

1216+ prettySe p bnd PImpossible = text "impossible"

1168− prettySe p Placeholder = text "_"

1217+ prettySe p bnd Placeholder = text "_"

1169− prettySe p (PDoBlock _) = text "do block pretty not implemented"

1218+ prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

1170− prettySe p (PElabError s) = pretty s

1219+ prettySe p bnd (PElabError s) = pretty s

1171−

1220+

1172− prettySe p _ = text "test"

1221+ prettySe p bnd _ = text "test"

1173−

1222+

1174− prettyArgS (PImp _ _ _ n tm _) = prettyArgSi (n, tm)

1223+ prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)

1175− prettyArgS (PExp _ _ tm _) = prettyArgSe tm

1224+ prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm

1176− prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm

1225+ prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm

1177− prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)

1226+ prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)

1178−

1227+

1179− prettyArgSe arg = prettySe 0 arg

1228+ prettyArgSe bnd arg = prettySe 0 bnd arg

1180− prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace

1229+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1181− prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace

1230+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1182− prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace

1231+ prettyArgSti bnd (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1232+

1233+ basename :: Name -> Name

1234+ basename (NS n _) = basename n

1235+ basename n = n

1236+

1237+ slist' p bnd (PApp _ (PRef _ nil) _)

1238+ | not impl && nsroot nil == sUN "Nil" = Just []

1239+ slist' p bnd (PApp _ (PRef _ cons) args)

1240+ | nsroot cons == sUN "::",

1241+ (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1242+ all isImp imps,

1243+ Just tl' <- slist' p bnd tl

1244+ = Just (hd:tl')

1245+ where

1246+ isImp (PImp {}) = True

1247+ isImp _ = False

1248+ slist' _ _ _ = Nothing

1249+

1250+ slist p bnd e | Just es <- slist' p bnd e = Just $

1251+ case es of [] -> annotate AnnConstData $ text "[]"

1252+ [x] -> enclose left

1253+ right

1254+ (prettySe p bnd x)

1255+ xs -> (enclose left right . hsep . punctuate comma . map (prettySe p bnd)) xs

1256+ where left = (annotate AnnConstData (text "["))

1257+ right = (annotate AnnConstData (text "]"))

1258+ comma = (annotate AnnConstData (text ","))

1259+ slist _ _ _ = Nothing

1260+

1261+ natns = "Prelude.Nat."

1262+

1263+ snat p (PRef _ z)

1264+ | show z == (natns++"Z") || show z == "Z" = Just 0

1265+ snat p (PApp _ s [PExp {getTm=n}])

1266+ | show s == (natns++"S") || show s == "S",

1267+ Just n' <- snat p n

1268+ = Just $ 1 + n'

1269+ snat _ _ = Nothing

1183

1270

1184 bracket outer inner doc

1271 bracket outer inner doc

1185 | inner > outer = lparen <> doc <> rparen

1272 | inner > outer = lparen <> doc <> rparen

1186 | otherwise = doc

1273 | otherwise = doc

1187

1274

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

1276+bindingOf :: Name -- ^^ the bound name

1277+ -> Bool -- ^^ whether the name is implicit

1278+ -> Doc OutputAnnotation

1279+bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))

1280+

1281+-- | Pretty-printer helper for names that attaches the correct annotations

1282+prettyName :: Bool -- ^^ whether to show namespaces

1283+ -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit

1284+ -> Name -- ^^ the name to pprint

1285+ -> Doc OutputAnnotation

1286+prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))

1287+ | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))

1288+ where strName (UN n) = T.unpack n

1289+ strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1290+ | otherwise = strName n

1291+ strName (MN i s) = T.unpack s

1292+ strName other = show other

1293+

1294+

1295+showCImp :: Bool -> PClause -> Doc OutputAnnotation

1296+showCImp impl (PClause _ n l ws r w)

1297+ = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r

1298+ <+> text "where" <+> text (show w)

1299+ where

1300+ showWs [] = empty

1301+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1302+showCImp impl (PWith _ n l ws r w)

1303+ = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r

1304+ <+> braces (text (show w))

1305+ where

1306+ showWs [] = empty

1307+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1308+

1309+

1310+showDImp :: Bool -> PData -> Doc OutputAnnotation

1311+showDImp impl (PDatadecl n ty cons)

1312+ = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1313+ (indent 2 $ vsep (map (\ (_, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

1314+

1315+showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1316+showDecls i ds = vsep (map (showDeclImp i) ds)

1317+

1318+showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1319+showDeclImp i (PTy _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t

1320+showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1321+ indent 2 (vsep (map (showCImp i) cs))

1322+showDeclImp _ (PData _ _ _ _ d) = showDImp True d

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

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

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

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

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

1328+showDeclImp i (PInstance _ _ cs n _ t _ ds)

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

1330+showDeclImp _ _ = text "..."

1331+-- showDeclImp (PImport i) = "import " ++ i

1332+

1333+instance Show (Doc OutputAnnotation) where

1334+ show = flip (displayS . renderCompact) ""

1335+

1336+getImps :: [PArg] -> [(Name, PTerm)]

1337+getImps [] = []

1338+getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs

1339+getImps (_ : xs) = getImps xs

1340+

1341+getExps :: [PArg] -> [PTerm]

1342+getExps [] = []

1343+getExps (PExp _ _ tm _ : xs) = tm : getExps xs

1344+getExps (_ : xs) = getExps xs

1345+

1346+getConsts :: [PArg] -> [PTerm]

1347+getConsts [] = []

1348+getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs

1349+getConsts (_ : xs) = getConsts xs

1350+

1351+getAll :: [PArg] -> [PTerm]

1352+getAll = map getTm

1353+

1354+

1188-- | Show Idris name

1355-- | Show Idris name

1189showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1356showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1190 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

1357 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

@@ -1214,171 +1381,14 @@ showName ist bnd impl colour n = case ist of

1214 -- (like error messages). Thus, unknown vars are colourised as implicits.

1381 -- (like error messages). Thus, unknown vars are colourised as implicits.

1215 | otherwise -> colouriseImplicit t name

1382 | otherwise -> colouriseImplicit t name

1216

1383

1217−-- | Show Idris term

1218−showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers and colours

1384+showTm :: IState -- ^^ the Idris state, for information about identifiers and colours

1219− -> Bool -- ^^ whether to show implicits

1220− -> Bool -- ^^ whether to colourise

1221− -> PTerm -- ^^ the term to show

1385+ -> PTerm -- ^^ the term to show

1222− -> String

1386+ -> String

1223−showImp ist impl colour tm = se 10 [] tm where

1387+showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))

1224− perhapsColourise :: (ColourTheme -> String -> String) -> String -> String

1225− perhapsColourise col str = case ist of

1226− Just i -> if colour then col (idris_colourTheme i) str else str

1227− Nothing -> str

1228−

1229− se :: Int -> [(Name, Bool)] -> PTerm -> String

1230− se p bnd (PQuote r) = "![" ++ show r ++ "]"

1231− se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n

1232− se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"

1233− se p bnd e

1234− | Just str <- slist p bnd e = str

1235− | Just num <- snat p e = perhapsColourise colouriseData (show num)

1236− se p bnd (PRef fc n) = showName ist bnd impl colour n

1237− se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++

1238− (if impl then " : " ++ se 10 bnd ty else "") ++ " => "

1239− ++ se 10 ((n, False):bnd) sc

1240− se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++

1241− " = " ++ se 10 bnd v ++

1242− " in " ++ se 10 ((n, False):bnd) sc

1243− se p bnd (PPi (Exp l s _ param) n ty sc)

1244− | n `elem` allNamesIn sc || impl

1245− = bracket p 2 $

1246− (if Lazy `elem` l then "|(" else "(") ++

1247− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1248− ") " ++

1249− (if (impl && param) then "P" else "") ++

1250− st ++

1251− "-> " ++ se 10 ((n, False):bnd) sc

1252− | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc

1253− where st = case s of

1254− Static -> "[static] "

1255− _ -> ""

1256− se p bnd (PPi (Imp l s _ _) n ty sc)

1257− | impl = bracket p 2 $ (if Lazy `elem` l then "|{" else "{") ++

1258− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1259− "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

1260− | otherwise = se 10 ((n, True):bnd) sc

1261− where st = case s of

1262− Static -> "[static] "

1263− _ -> ""

1264− se p bnd (PPi (Constraint _ _ _) n ty sc)

1265− = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc

1266− se p bnd (PPi (TacImp _ _ s _) n ty sc)

1267− = bracket p 2 $

1268− "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++

1269− se 10 ((n, False):bnd) sc

1270− se p bnd (PMatchApp _ f) = "match " ++ show f

1271− se p bnd (PApp _ hd@(PRef fc f) [tm])

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

1273− f == sUN "Symbol_" = "'" ++ se 10 bnd (PRef fc (sUN str))

1274− se p bnd (PApp _ hd@(PRef _ f) [])

1275− | not impl = se p bnd hd

1276− se p bnd (PAppBind _ hd@(PRef _ f) [])

1277− | not impl = "!" ++ se p bnd hd

1278− se p bnd (PApp _ op@(PRef _ (UN nm)) args)

1279− | not (tnull nm) &&

1280− length (getExps args) == 2 && not impl && not (isAlpha (thead nm))

1281− = let [l, r] = getExps args in

1282− bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r

1283− se p bnd (PApp _ f as)

1284− = -- let args = getExps as in

1285− bracket p 1 $ se 1 bnd f ++

1286− if impl then concatMap (sArg bnd) as

1287− else concatMap (suiArg impl bnd) as

1288− se p bnd (PAppBind _ f as)

1289− = let args = getExps as in

1290− "!" ++ (bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as

1291− else concatMap (seArg bnd) args)

1292− se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)

1293− where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r

1294− se p bnd (PHidden tm) = "." ++ se 0 bnd tm

1295− se p bnd (PRefl _ t)

1296− | not impl = perhapsColourise colouriseData "refl"

1297− | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"

1298− se p bnd (PResolveTC _) = "resolvetc"

1299− se p bnd (PTrue _) = perhapsColourise colouriseType "()"

1300− se p bnd (PFalse _) = perhapsColourise colouriseType "_|_"

1301− se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ perhapsColourise colouriseType " = " ++ se 10 bnd r

1302− se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r

1303− se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"

1304− se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"

1305− se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"

1306− se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"

1307− se p bnd PType = perhapsColourise colouriseType "Type"

1308− se p bnd (PConstant c) = perhapsColourise (cfun c) (show c)

1309− where cfun (AType _) = colouriseType

1310− cfun StrType = colouriseType

1311− cfun PtrType = colouriseType

1312− cfun VoidType = colouriseType

1313− cfun _ = colouriseData

1314− se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"

1315− se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"

1316− se p bnd (PMetavar n) = "?" ++ show n

1317− se p bnd (PReturn f) = "return"

1318− se p bnd PImpossible = "impossible"

1319− se p bnd Placeholder = "_"

1320− se p bnd (PDoBlock _) = "do block show not implemented"

1321− se p bnd (PElabError s) = show s

1322− se p bnd (PCoerced t) = se p bnd t

1323− se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t

1324− se p bnd (PDisamb ns t) = "%disamb " ++ show ns ++ se p bnd t

1325− se p bnd (PNoImplicits t) = "%noimplicit " ++ se p bnd t

1326−-- se p bnd x = "Not implemented"

1327−

1328− slist' p bnd (PApp _ (PRef _ nil) _)

1329− | not impl && nsroot nil == sUN "Nil" = Just []

1330− slist' p bnd (PApp _ (PRef _ cons) args)

1331− | nsroot cons == sUN "::",

1332− (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1333− all isImp imps,

1334− Just tl' <- slist' p bnd tl

1335− = Just (hd:tl')

1336− where

1337− isImp (PImp {}) = True

1338− isImp _ = False

1339− slist' _ _ _ = Nothing

1340−

1341− slist p bnd e | Just es <- slist' p bnd e = Just $

1342− case es of [] -> "[]"

1343− [x] -> "[" ++ se p bnd x ++ "]"

1344− xs -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"

1345− slist _ _ _ = Nothing

1346−

1347− -- since Prelude is always imported, S & Z are unqualified iff they're the

1348− -- Nat ones.

1349− snat p (PRef _ o)

1350− | show o == (natns++"Z") || show o == "Z" = Just 0

1351− snat p (PApp _ s [PExp {getTm=n}])

1352− | show s == (natns++"S") || show s == "S",

1353− Just n' <- snat p n

1354− = Just $ 1 + n'

1355− snat _ _ = Nothing

1356−

1357− natns = "Prelude.Nat."

1358

1388

1359− sArg bnd (PImp _ _ _ n tm _) = siArg bnd (n, tm)

1389+-- | Show a term with implicits, no colours

1360− sArg bnd (PExp _ _ tm _) = seArg bnd tm

1390+showTmImpls :: PTerm -> String

1361− sArg bnd (PConstraint _ _ tm _) = scArg bnd tm

1391+showTmImpls = flip (displayS . renderCompact . prettyImp True) ""

1362− sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)

1363−

1364− -- show argument, implicits given by the user also shown

1365− suiArg impl bnd (PImp _ mi _ n tm _)

1366− | impl || not mi = siArg bnd (n, tm)

1367− suiArg impl bnd (PExp _ _ tm _) = seArg bnd tm

1368− suiArg impl bnd _ = ""

1369−

1370− seArg bnd arg = " " ++ se 0 bnd arg

1371− siArg bnd (n, val) =

1372− let n' = show n

1373− val' = se 10 bnd val in

1374− if (n' == val')

1375− then " {" ++ n' ++ "}"

1376− else " {" ++ n' ++ " = " ++ val' ++ "}"

1377− scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"

1378− stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"

1379−

1380− bracket outer inner str | inner > outer = "(" ++ str ++ ")"

1381− | otherwise = str

1382

1392

1383

1393

1384instance Sized PTerm where

1394instance Sized PTerm where

src/Idris/CaseSplit.hs+3−3

@@ -62,11 +62,11 @@ split n t'

62 Just ty ->

63 do let splits = findPats ist ty

64 iLOG ("New patterns " ++ showSep ", "

65− (map (showImp Nothing True False) splits))

65+ (map showTmImpls splits))

66 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

67 logLvl 4 ("Working from " ++ show t)

68 logLvl 4 ("Trying " ++ showSep "\n"

69− (map (showImp Nothing True False) newPats_in))

69+ (map (showTmImpls) newPats_in))

70 newPats <- mapM elabNewPat newPats_in

71 logLvl 3 ("Original:\n" ++ show t)

72 logLvl 3 ("Split:\n" ++

@@ -237,7 +237,7 @@ splitOnLine l n fn = do

237-- let (before, later) = splitAt (l-1) (lines inp)

238-- i <- getIState

239 cl <- getInternalApp fn l

240− logLvl 3 ("Working with " ++ showImp Nothing True False cl)

240+ logLvl 3 ("Working with " ++ showTmImpls cl)

241 tms <- split n cl

242-- iputStrLn (showSep "\n" (map show tms))

243 return tms -- "" -- not yet done...

src/Idris/Core/Elaborate.hs+1−1

@@ -24,7 +24,7 @@ import Data.Char

24import Data.List

25import Debug.Trace

27−import Util.Pretty

27+import Util.Pretty hiding (fill)

29-- I don't really want this here, but it's useful for the test shell

30data Command = Theorem Name Raw

src/Idris/Core/ProofState.hs+12−12

@@ -18,7 +18,7 @@ import Control.Applicative hiding (empty)

18import Data.List

19import Debug.Trace

21−import Util.Pretty

21+import Util.Pretty hiding (fill)

23data ProofState = PS { thname :: Name,

24 holes :: [Name], -- holes still to be solved

@@ -113,23 +113,23 @@ instance Show ProofState where

113 " =?= " ++ showEnv ps v

114 showG ps b = showEnv ps (binderTy b)

115

116−instance Pretty ProofState where

116+instance Pretty ProofState OutputAnnotation where

117 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

118 if size nm > breakingSize then

119− pretty nm <> colon $$ nest nestingSize (text " no more goals.")

119+ pretty nm <+> colon <+> nest nestingSize (text " no more goals.")

120 else

121− pretty nm <> colon <+> text " no more goals."

121+ pretty nm <+> colon <+> text " no more goals."

122 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =

123 let OK g = goal (Just h) tm in

124 let wkEnv = premises g in

125− text "Other goals" <+> colon <+> pretty hs $$

125+ text "Other goals" <+> colon <+> pretty hs <+>

126− prettyPs wkEnv (reverse wkEnv) $$

126+ prettyPs wkEnv (reverse wkEnv) <+>

127− text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$

127+ text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>

128 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)

129 where

130 prettyGoal ps (Guess t v) =

131 if size v > breakingSize then

132− prettyEnv ps t <+> text "=?=" $$

132+ prettyEnv ps t <+> text "=?=" <+>

133 nest nestingSize (prettyEnv ps v)

134 else

135 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v

@@ -139,17 +139,17 @@ instance Pretty ProofState where

139 prettyPs env ((n, Let t v):bs) =

140 nest nestingSize (pretty n <+> colon <+>

141 if size v > breakingSize then

142− prettyEnv env t <+> text "=" $$

142+ prettyEnv env t <+> text "=" <+>

143− nest nestingSize (prettyEnv env v) $$

143+ nest nestingSize (prettyEnv env v) <+>

144 nest nestingSize (prettyPs env bs)

145 else

146− prettyEnv env t <+> text "=" <+> prettyEnv env v $$

146+ prettyEnv env t <+> text "=" <+> prettyEnv env v <+>

147 nest nestingSize (prettyPs env bs))

148 prettyPs env ((n, b):bs) =

149 if size (binderTy b) > breakingSize then

150 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)

151 else

152− nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$

152+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>

153 nest nestingSize (prettyPs env bs))

154

155same Nothing n = True

src/Idris/Core/TT.hs+33−19

@@ -78,6 +78,16 @@ instance Sized FC where

78instance Show FC where

79 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c

81+-- | Output annotation for pretty-printed name - decides colour

82+data NameOutput = TypeOutput | FunOutput | DataOutput

83+

84+-- | Output annotations for pretty-printing

85+data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)

86+ | AnnBoundName Name Bool

87+ | AnnConstData

88+ | AnnConstType

89+ | AnnFC FC

90+

81-- | Used for error reflection

91-- | Used for error reflection

82data ErrorReportPart = TextPart String

92data ErrorReportPart = TextPart String

83 | NamePart Name

93 | NamePart Name

@@ -178,15 +188,15 @@ instance Show Err where

178 show (At f e) = show f ++ ":" ++ show e

188 show (At f e) = show f ++ ":" ++ show e

179 show _ = "Error"

189 show _ = "Error"

180

190

181−instance Pretty Err where

191+instance Pretty Err OutputAnnotation where

182 pretty (Msg m) = text m

192 pretty (Msg m) = text m

183 pretty (CantUnify _ l r e _ i) =

193 pretty (CantUnify _ l r e _ i) =

184 if size l + size r > breakingSize then

194 if size l + size r > breakingSize then

185− text "Cannot unify" <+> colon $$

195+ text "Cannot unify" <+> colon <+>

186− nest nestingSize (pretty l <+> text "and" <+> pretty r) $$

196+ nest nestingSize (pretty l <+> text "and" <+> pretty r) <+>

187 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

197 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

188 else

198 else

189− text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$

199+ text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

190 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

200 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

191 pretty (ProviderError msg) = text msg

201 pretty (ProviderError msg) = text msg

192 pretty err@(LoadingFailed _ _) = text (show err)

202 pretty err@(LoadingFailed _ _) = text (show err)

@@ -197,11 +207,11 @@ instance Error Err where

197

207

198type TC = TC' Err

208type TC = TC' Err

199

209

200−instance (Pretty a) => Pretty (TC a) where

210+instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where

201 pretty (OK ok) = pretty ok

211 pretty (OK ok) = pretty ok

202 pretty (Error err) =

212 pretty (Error err) =

203 if size err > breakingSize then

213 if size err > breakingSize then

204− text "Error" <+> colon $$ (nest nestingSize $ pretty err)

214+ text "Error" <+> colon <+> (nest nestingSize $ pretty err)

205 else

215 else

206 text "Error" <+> colon <+> pretty err

216 text "Error" <+> colon <+> pretty err

207

217

@@ -295,11 +305,15 @@ instance Sized Name where

295 size (MN i n) = 1

305 size (MN i n) = 1

296 size _ = 1

306 size _ = 1

297

307

298−instance Pretty Name where

308+instance Pretty Name OutputAnnotation where

299− pretty (UN n) = text (T.unpack n)

309+ pretty n@(UN n') = annotate (AnnName n Nothing Nothing) $ text (T.unpack n')

300− pretty (NS n s) = pretty n

310+ pretty n@(NS un s) = annotate (AnnName n Nothing Nothing) . noAnnotate $ pretty un

311+ pretty n@(MN i s) = annotate (AnnName n Nothing Nothing) $

301− pretty (MN i s) = lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

312+ lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

302− pretty (SN s) = text (show s)

313+ pretty n@(SN s) = annotate (AnnName n Nothing Nothing) $ text (show s)

314+

315+instance Pretty [Name] OutputAnnotation where

316+ pretty = encloseSep empty empty comma . map pretty

303

317

304instance Show Name where

318instance Show Name where

305 show (UN n) = str n

319 show (UN n) = str n

@@ -418,7 +432,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

418data NativeTy = IT8 | IT16 | IT32 | IT64

432data NativeTy = IT8 | IT16 | IT32 | IT64

419 deriving (Show, Eq, Ord, Enum)

433 deriving (Show, Eq, Ord, Enum)

420

434

421−instance Pretty NativeTy where

435+instance Pretty NativeTy OutputAnnotation where

422 pretty IT8 = text "Bits8"

436 pretty IT8 = text "Bits8"

423 pretty IT16 = text "Bits16"

437 pretty IT16 = text "Bits16"

424 pretty IT32 = text "Bits32"

438 pretty IT32 = text "Bits32"

@@ -436,7 +450,7 @@ deriving instance NFData NativeTy

436deriving instance NFData ArithTy

450deriving instance NFData ArithTy

437!-}

451!-}

438

452

439−instance Pretty ArithTy where

453+instance Pretty ArithTy OutputAnnotation where

440 pretty (ATInt ITNative) = text "Int"

454 pretty (ATInt ITNative) = text "Int"

441 pretty (ATInt ITBig) = text "BigInt"

455 pretty (ATInt ITBig) = text "BigInt"

442 pretty (ATInt ITChar) = text "Char"

456 pretty (ATInt ITChar) = text "Char"

@@ -472,7 +486,7 @@ deriving instance NFData Const

472instance Sized Const where

486instance Sized Const where

473 size _ = 1

487 size _ = 1

474

488

475−instance Pretty Const where

489+instance Pretty Const OutputAnnotation where

476 pretty (I i) = text . show $ i

490 pretty (I i) = text . show $ i

477 pretty (BI i) = text . show $ i

491 pretty (BI i) = text . show $ i

478 pretty (Fl f) = text . show $ f

492 pretty (Fl f) = text . show $ f

@@ -504,7 +518,7 @@ instance Sized Raw where

504 size (RForce raw) = 1 + size raw

518 size (RForce raw) = 1 + size raw

505 size (RConstant const) = size const

519 size (RConstant const) = size const

506

520

507−instance Pretty Raw where

521+instance Pretty Raw OutputAnnotation where

508 pretty = text . show

522 pretty = text . show

509

523

510{-!

524{-!

@@ -622,7 +636,7 @@ deriving instance NFData NameType

622instance Sized NameType where

636instance Sized NameType where

623 size _ = 1

637 size _ = 1

624

638

625−instance Pretty NameType where

639+instance Pretty NameType OutputAnnotation where

626 pretty = text . show

640 pretty = text . show

627

641

628instance Eq NameType where

642instance Eq NameType where

@@ -688,7 +702,7 @@ instance Sized a => Sized (TT a) where

688 size Erased = 1

702 size Erased = 1

689 size (TType u) = 1 + size u

703 size (TType u) = 1 + size u

690

704

691−instance Pretty a => Pretty (TT a) where

705+instance Pretty a o => Pretty (TT a) o where

692 pretty _ = text "test"

706 pretty _ = text "test"

693

707

694type EnvTT n = [(n, Binder (TT n))]

708type EnvTT n = [(n, Binder (TT n))]

@@ -1043,7 +1057,7 @@ prettyEnv env t = prettyEnv' env t False

1043 prettySe p env (P nt n t) debug =

1057 prettySe p env (P nt n t) debug =

1044 pretty n <+>

1058 pretty n <+>

1045 if debug then

1059 if debug then

1046− lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack

1060+ lbracket <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbracket

1047 else

1061 else

1048 empty

1062 empty

1049 prettySe p env (V i) debug

1063 prettySe p env (V i) debug

@@ -1051,7 +1065,7 @@ prettyEnv env t = prettyEnv' env t False

1051 if debug then

1065 if debug then

1052 text . show . fst $ env!!i

1066 text . show . fst $ env!!i

1053 else

1067 else

1054− lbrack <+> text (show i) <+> rbrack

1068+ lbracket <+> text (show i) <+> rbracket

1055 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1069 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1056 prettySe p env (Bind n b@(Pi t) sc) debug

1070 prettySe p env (Bind n b@(Pi t) sc) debug

1057 | noOccurrence n sc && not debug =

1071 | noOccurrence n sc && not debug =

src/Idris/Coverage.hs+3−3

@@ -50,7 +50,7 @@ genClauses fc n xs given

50 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

51 logLvl 10 $ show argss ++ "\n" ++ show all_args

52 logLvl 10 $ "Original: \n" ++

53− showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True True)) xs)

53+ showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)

54 -- add an infinite supply of explicit arguments to update the possible

55 -- cases for (the return type may be variadic, or function type, sp

56 -- there may be more case splitting that the idris_implicits record

@@ -60,10 +60,10 @@ genClauses fc n xs given

60 _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

63− logLvl 5 $ showSep "\n" (map (showImp Nothing True False) tryclauses)

63+ logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)

64 let new = filter (noMatch i) (nub tryclauses)

65 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"

66− logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp Nothing True False) new)

66+ logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)

67-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

68 return new

69-- return (map (\t -> PClause n t [] PImpossible []) new)

src/Idris/Delaborate.hs+111−106

@@ -1,10 +1,12 @@

1{-# LANGUAGE PatternGuards #-}

3−module Idris.Delaborate where

3+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) where

5-- Convert core TT back into high level syntax, primarily for display

6-- purposes.

8+import Util.Pretty

8import Idris.AbsSyntax

10import Idris.AbsSyntax

9import Idris.Core.TT

11import Idris.Core.TT

10import Idris.Core.Evaluate

12import Idris.Core.Evaluate

@@ -33,7 +35,7 @@ delab' :: IState -> Term -> Bool -> Bool -> PTerm

33delab' i t f mvs = delabTy' i [] t f mvs

35delab' i t f mvs = delabTy' i [] t f mvs

35delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

37delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

36− -> Term

38+ -> Term

37 -> Bool -- ^ use full names

39 -> Bool -- ^ use full names

38 -> Bool -- ^ Don't treat metavariables specially

40 -> Bool -- ^ Don't treat metavariables specially

39 -> PTerm

41 -> PTerm

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

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

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

51 | otherwise

53 | otherwise

52 = case lookup n (idris_metavars ist) of

54 = case lookup n (idris_metavars ist) of

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

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

54− _ -> PRef un (dens n)

56+ _ -> PRef un n

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

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

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

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

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

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

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

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

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

97 = case lookup n (idris_metavars ist) of

99 = case lookup n (idris_metavars ist) of

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

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

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

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

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

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

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

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

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

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

103

105

104 mkMVApp n []

106 mkMVApp n []

@@ -115,108 +117,111 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

115 imp (PConstraint p l _ d) arg = PConstraint p l arg d

117 imp (PConstraint p l _ d) arg = PConstraint p l arg d

116 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

118 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

117

119

120+-- | How far to indent sub-errors

121+errorIndent :: Int

122+errorIndent = 8

118

123

119−indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where

124+-- | Actually indent a sub-error - no line at end because a newline can end

120− boxIt c text = (c:text) ++ if last text == c

125+-- multiple layers of indent

121− then ""

126+indented :: Doc a -> Doc a

122− else [c]

127+indented = nest errorIndent . (line <>)

123

128

124−pshow :: IState -> Err -> String

129+pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

125−pshow i err = pshow' i (fmap (errReverse i) err)

126−

127−pshow' i (Msg s) = s

128−pshow' i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

129− "\nThis is probably a bug, or a missing error message.\n" ++

130− "Please consider reporting at " ++ bugaddr

131−pshow' i (CantUnify _ x y e sc s)

132− = let imps = opt_showimp (idris_options i) in

130+pprintTerm ist = prettyImp (opt_showimp (idris_options ist))

133− let colour = idris_colourRepl i in

134− "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))

135− ++ "with" ++ indented (showImp (Just i) imps colour (delab i y)) ++

136−-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

137− case e of

138− Msg "" -> ""

139− _ -> "\nSpecifically:" ++

140− indented (pshow' i e) ++

141− if (opt_errContext (idris_options i)) then showSc i sc else ""

142−pshow' i (CantConvert x y env)

143− = let imps = opt_showimp (idris_options i) in

144− let colour = idris_colourRepl i in

145− "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"

146− ++ indented (showImp (Just i) imps colour (delab i y)) ++

147− if (opt_errContext (idris_options i)) then showSc i env else ""

148−pshow' i (CantSolveGoal x env)

149− = let imps = opt_showimp (idris_options i) in

150− let colour = idris_colourRepl i in

151− "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++

152− if (opt_errContext (idris_options i)) then showSc i env else ""

153−pshow' i (UnifyScope n out tm env)

154− = let imps = opt_showimp (idris_options i) in

155− let colour = idris_colourRepl i in

156− "Can't unify" ++ indented (show n) ++ "with"

157− ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++

158− indented (show out) ++ "is not in scope" ++

159− if (opt_errContext (idris_options i)) then showSc i env else ""

160−pshow' i (CantInferType t)

161− = "Can't infer type for " ++ t

162−pshow' i (NonFunctionType f ty)

163− = let imps = opt_showimp (idris_options i) in

164− let colour = idris_colourRepl i in

165− showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("

166− ++ showImp (Just i) imps colour (delab i ty) ++ ")"

167−pshow' i (NotEquality tm ty)

168− = let imps = opt_showimp (idris_options i) in

169− let colour = idris_colourRepl i in

170− showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("

171− ++ showImp (Just i) imps colour (delab i ty) ++ ")"

172−pshow' i (TooManyArguments f)

173− = "Too many arguments for " ++ show f

174−pshow' i (CantIntroduce ty)

175− = let imps = opt_showimp (idris_options i) in

176− let colour = idris_colourRepl i in

177− "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)

178−pshow' i (InfiniteUnify x tm env)

179− = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

180− " would lead to infinite value" ++

181− if (opt_errContext (idris_options i)) then showSc i env else ""

182−pshow' i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

183− " when unifying " ++ show (delab i x) ++ " and " ++

184− show (delab i y)

185−pshow' i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

186−pshow' i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

187−pshow' i (NoTypeDecl n) = "No type declaration for " ++ show n

188−pshow' i (NoSuchVariable n) = "No such variable " ++ show n

189−pshow' i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)

190−pshow' i UniverseError = "Universe inconsistency"

191−pshow' i ProgramLineComment = "Program line next to comment"

192−pshow' i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

193−pshow' i (NonCollapsiblePostulate n)

194− = "The return type of postulate " ++ show n ++ " is not collapsible"

195−pshow' i (AlreadyDefined n) = show n ++ " is already defined"

196−pshow' i (ProofSearchFail e) = pshow' i e

197−pshow' i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

198−pshow' i (At f e) = show f ++ ":" ++ pshow' i e

199−pshow' i (Elaborating s n e) = "When elaborating " ++ s ++

200− showqual i n ++ ":\n" ++ pshow' i e

201−pshow' i (ProviderError msg) = "Type provider error: " ++ msg

202−pshow' i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow' i e

203−pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in

204− concat (intersperse "\n" parts') ++

205− if (opt_origerr (idris_options i))

206− then "\nOriginal error:\n" ++ indented (pshow i orig)

207− else ""

208− where showPart :: ErrorReportPart -> String

209− showPart (TextPart str) = str

210− showPart (NamePart n) = let colour = idris_colourRepl i in

211− showName (Just i) [] False colour n

212− showPart (TermPart tm) = let colour = idris_colourRepl i

213− in showImp (Just i) False colour (delab i tm)

214− showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

215−pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

216− indented msg ++

217− indented (pshow i err) ++

218− "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

219

131

132+pshow :: IState -> Err -> String

133+pshow ist err = displayDecorated (consoleDecorate ist) .

134+ renderPretty 1.0 80 .

135+ fmap (fancifyAnnots ist) $ pprintErr ist err

136+

137+pprintErr :: IState -> Err -> Doc OutputAnnotation

138+pprintErr i err = pprintErr' i (fmap (errReverse i) err)

139+

140+pprintErr' i (Msg s) = text s

141+pprintErr' i (InternalMsg s) =

142+ vsep [ text "INTERNAL ERROR:" <+> text s,

143+ text "This is probably a bug, or a missing error message.",

144+ text ("Please consider reporting at " ++ bugaddr)

145+ ]

146+pprintErr' i (CantUnify _ x y e sc s) =

147+ text "Can't unify" <> indented (pprintTerm i (delab i x)) <$>

148+ text "with" <> indented (pprintTerm i (delab i y)) <>

149+ case e of

150+ Msg "" -> empty

151+ _ -> line <> line <> text "Specifically:" <>

152+ indented (pprintErr' i e) <>

153+ if (opt_errContext (idris_options i)) then text $ showSc i sc else empty

154+pprintErr' i (CantConvert x y env) =

155+ text "Can't convert" <> indented (pprintTerm i (delab i x)) <>

156+ text "with" <> indented (pprintTerm i (delab i y)) <>

157+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty

158+pprintErr' i (UnifyScope n out tm env) =

159+ text "Can't unify" <> indented (annName n) <+>

160+ text "with" <> indented (pprintTerm i (delab i tm)) <+>

161+ text "as" <> indented (annName out) <> text "is not in scope" <>

162+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty

163+pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t

164+pprintErr' i (NonFunctionType f ty) =

165+ pprintTerm i (delab i f) <+>

166+ text "does not have a function type" <+>

167+ parens (pprintTerm i (delab i ty))

168+pprintErr' i (NotEquality tm ty) =

169+ pprintTerm i (delab i tm) <+>

170+ text "does not have an equality type" <+>

171+ parens (pprintTerm i (delab i ty))

172+pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f

173+pprintErr' i (CantIntroduce ty) =

174+ text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)

175+pprintErr' i (InfiniteUnify x tm env) =

176+ text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>

177+ text "would lead to infinite value" <>

178+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty

179+pprintErr' i (NotInjective p x y) =

180+ text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>

181+ text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>

182+ pprintTerm i (delab i y)

183+pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

184+pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

185+ cat (punctuate comma (map text as))

186+pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

187+pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

188+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

189+pprintErr' i UniverseError = text "Universe inconsistency"

190+pprintErr' i ProgramLineComment = text "Program line next to comment"

191+pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

192+pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

193+ annName n <+> text "is not collapsible"

194+pprintErr' i (AlreadyDefined n) = annName n<+>

195+ text "is already defined"

196+pprintErr' i (ProofSearchFail e) = pprintErr' i e

197+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> pprintTerm i (delab i tm)

198+pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e

199+pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>

200+ annName' n (showqual i n) <> colon <$>

201+ pprintErr' i e

202+pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)

203+pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e

204+pprintErr' i (ReflectionError parts orig) =

205+ let parts' = map (hsep . map showPart) parts in

206+ vsep parts' <>

207+ if (opt_origerr (idris_options i))

208+ then line <> line <> text "Original error:" <$> indented (pprintErr' i orig)

209+ else empty

210+ where showPart :: ErrorReportPart -> Doc OutputAnnotation

211+ showPart (TextPart str) = text str

212+ showPart (NamePart n) = annName n

213+ showPart (TermPart tm) = pprintTerm i (delab i tm)

214+ showPart (SubReport rs) = indented . hsep . map showPart $ rs

215+pprintErr' i (ReflectionFailed msg err) =

216+ text "When attempting to perform error reflection, the following internal error occurred:" <>

217+ indented (pprintErr' i err) <>

218+ text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

219+

220+annName :: Name -> Doc OutputAnnotation

221+annName n = annName' n (show n)

222+

223+annName' :: Name -> String -> Doc OutputAnnotation

224+annName' n str = annotate (AnnName n Nothing Nothing) (text str)

220

225

221showSc i [] = ""

226showSc i [] = ""

222showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

227showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

src/Idris/ElabDecls.hs+32−32

@@ -67,12 +67,12 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

67 ctxt <- getContext

68 i <- getIState

70− logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'

70+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

71 ty' <- addUsingConstraints syn fc ty'

72 ty' <- implicit syn n ty'

74 let ty = addImpl i ty'

75− logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty

75+ logLvl 2 $ show n ++ " type " ++ showTmImpls ty

76 ((tyT, defer, is), log) <-

77 tclift $ elaborate ctxt n (TType (UVal 0)) []

78 (errAt "type of " n (erun fc (build i info False [] n ty)))

@@ -327,10 +327,10 @@ elabEliminator paramPos n ty cons info = do

327 let clauseConsElimArgs = map getPiName consTerms

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

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

330− let elimSig = "-- eliminator signature: " ++ showImp Nothing True True eliminatorTy

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

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

332 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

333− elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef

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

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

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

336 case eliminatorClauses of

@@ -815,7 +815,7 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

815 i <- getIState

816 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

817 let t = addImpl i t_in

818− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t

818+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

819 ((t', defer, is), log) <-

820 tclift $ elaborate ctxt n (TType (UVal 0)) []

821 (errAt "constructor " n (erun fc (build i info False [] n t)))

@@ -960,9 +960,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

960 missing' <- filterM (checkPossible info fc True n) missing

961 let clhs = map getLHS pdef

962 logLvl 2 $ "Must be unreachable:\n" ++

963− showSep "\n" (map (showImp Nothing True False) missing') ++

963+ showSep "\n" (map showTmImpls missing') ++

964 "\nAgainst: " ++

965− showSep "\n" (map (\t -> showImp Nothing True False (delab ist t)) (map getLHS pdef))

965+ showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))

966 -- filter out anything in missing' which is

967 -- matched by any of clhs. This might happen since

968 -- unification may force a variable to take a

@@ -1126,8 +1126,8 @@ elabPE info fc caller r =

1126 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++

1127 showSep "\n"

1128 (map (\ (lhs, rhs) ->

1129− (showImp Nothing True False lhs ++ " = " ++

1129+ (showTmImpls lhs ++ " = " ++

1130− showImp Nothing True False rhs)) pats)

1130+ showTmImpls rhs)) pats)

1131 elabType info defaultSyntax "" fc opts newnm specTy

1132 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1133 elabClauses info fc opts newnm def

@@ -1181,7 +1181,7 @@ elabValBind info aspat tm_in

1181 = do ctxt <- getContext

1182 i <- getIState

1183 let tm = addImpl i tm_in

1184− logLvl 10 (showImp Nothing True False tm)

1184+ logLvl 10 (showTmImpls tm)

1185 -- try:

1186 -- * ordinary elaboration

1187 -- * elaboration as a Type

@@ -1272,7 +1272,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1272 let params = getParamsInType i [] fn_is fn_ty

1273 let lhs = stripUnmatchable i $

1274 addImplPat i (propagateParams params (stripLinear i lhs_in))

1275− logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)

1275+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1276 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

1277

1278 ((lhs', dlhs, []), _) <-

@@ -1287,7 +1287,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1287 (clhs_c, clhsty) <- recheckC fc [] lhs_tm

1288 let clhs = normalise ctxt [] clhs_c

1289

1290− logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))

1290+ logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

1291

1292 rep <- useREPL

1293 when rep $ do

@@ -1313,10 +1313,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1313 mapM_ (elabDecl' EAll info) wbefore

1314 -- Now build the RHS, using the type of the LHS as the goal.

1315 i <- getIState -- new implicits from where block

1316− logLvl 5 (showImp Nothing True False (expandParams decorate newargs defs (defs \\ decls) rhs_in))

1316+ logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

1317 let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)

1318 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

1319− logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs

1319+ logLvl 2 $ "RHS: " ++ showTmImpls rhs

1320 ctxt <- getContext -- new context with where block added

1321 logLvl 5 "STARTING CHECK"

1322 ((rhs', defer, is), _) <-

@@ -1469,7 +1469,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1469 -- pattern bindings

1470 i <- getIState

1471 let lhs = addImplPat i (stripLinear i lhs_in)

1472− logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

1472+ logLvl 5 ("LHS: " ++ showTmImpls lhs)

1473 ((lhs', dlhs, []), _) <-

1474 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1475 (errAt "left hand side of with in " fname

@@ -1482,7 +1482,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1482 logLvl 5 ("Checked " ++ show clhs)

1483 let bargs = getPBtys lhs_tm

1484 let wval = addImplBound i (map fst bargs) wval_in

1485− logLvl 5 ("Checking " ++ showImp Nothing True False wval)

1485+ logLvl 5 ("Checking " ++ showTmImpls wval)

1486 -- Elaborate wval in this context

1487 ((wval', defer, is), _) <-

1488 tclift $ elaborate ctxt (sMN 0 "withRHS")

@@ -1546,7 +1546,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1546 (map (pexp . (PRef fc) . fst) bargs_pre ++

1547 pexp wval :

1548 (map (pexp . (PRef fc) . fst) bargs_post))

1549− logLvl 5 ("New RHS " ++ showImp Nothing True False rhs)

1549+ logLvl 5 ("New RHS " ++ showTmImpls rhs)

1550 ctxt <- getContext -- New context with block added

1551 i <- getIState

1552 ((rhs', defer, is), _) <-

@@ -1577,8 +1577,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1577 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

1578 = do i <- getIState

1579 let tm = addImplPat i tm_in

1580− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++

1580+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

1581− showImp Nothing True False toplhs)

1581+ showTmImpls toplhs)

1582 case matchClause i toplhs tm of

1583 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")

1584 Right mvars ->

@@ -1588,8 +1588,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1588 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)

1589 = do i <- getIState

1590 let tm = addImplPat i tm_in

1591− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++

1591+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

1592− showImp Nothing True False toplhs)

1592+ showTmImpls toplhs)

1593 withs' <- mapM (mkAuxC wname toplhs ns ns') withs

1594 case matchClause i toplhs tm of

1595 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")

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

1656 constraint

1657 let cons = [("", cn, cty, fc, [])]

1658 let ddecl = PDatadecl tn tty cons

1659− logLvl 5 $ "Class data " ++ showDImp True ddecl

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

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

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

1662 logLvl 5 $ "Building functions"

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

1698 getMName (PTy _ _ _ _ n _) = nsroot n

1699 tdecl allmeths (PTy doc syn _ o n t)

1700 = do t' <- implicit' syn allmeths n t

1701− logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing True False t'

1701+ logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

1702 return ( (n, (toExp (map fst ps) Exp t')),

1703 (n, (doc, o, (toExp (map fst ps) Imp t'))),

1704 (n, (syn, o, t) ) )

@@ -1735,8 +1735,8 @@ elabClass info syn doc fc constraints tn ps ds

1735 let lhs = PApp fc (PRef fc cfn) [pconst capp]

1736 let rhs = PResolveTC (fileFC "HACK")

1737 let ty = PPi constraint (sMN 0 "pc") c con

1738− iLOG (showImp Nothing True False ty)

1738+ iLOG (showTmImpls ty)

1739− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

1739+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1740 i <- getIState

1741 let conn = case con of

1742 PRef _ n -> n

@@ -1760,9 +1760,9 @@ elabClass info syn doc fc constraints tn ps ds

1760 let anames = map (\x -> sMN x "arg") [0..]

1761 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

1762 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

1763− iLOG (showImp Nothing True False ty)

1763+ iLOG (showTmImpls ty)

1764 iLOG (show (m, ty', capp, margs))

1765− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

1765+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1766 return [PTy doc syn fc o m ty',

1767 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1768

@@ -1850,7 +1850,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

1850 let wbTys = map mkTyDecl mtys

1851 let wbVals = map (decorateid (decorate ns iname)) ds'

1852 let wb = wbTys ++ wbVals

1853− logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)

1853+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)

1854 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

1855 show (concat (nub wparams))

1856 let lhs = PRef fc iname

@@ -2157,8 +2157,8 @@ elabCaseBlock info opts d@(PClauses f o n ps)

2157

2158checkInferred :: FC -> PTerm -> PTerm -> Idris ()

2159checkInferred fc inf user =

2160− do logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n\nFROM\n\n" ++

2160+ do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

2161− showImp Nothing True False user

2161+ showTmImpls user

2162 logLvl 10 $ "Checking match"

2163 i <- getIState

2164 tclift $ case matchClause' True i user inf of

@@ -2175,8 +2175,8 @@ checkInferred fc inf user =

2175inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

2176inferredDiff fc inf user =

2177 do i <- getIState

2178− logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++

2178+ logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++

2179− showImp Nothing True False user

2179+ showTmImpls user

2180 tclift $ case matchClause' True i user inf of

2181 Right vs -> return False

2182 Left (x, y) -> return True

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]

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/Parser.hs+1−1

@@ -1073,7 +1073,7 @@ loadSource h lidr f

1073 f file pos

1074 unless (null ds') $ do

1075 let ds = namespaces mname ds'

1076− logLvl 3 (showDecls True ds)

1076+ logLvl 3 (show $ showDecls True ds)

1077 i <- getIState

1078 logLvl 10 (show (toAlist (idris_implicits i)))

1079 logLvl 3 (show (idris_infixes i))

src/Idris/Prover.hs+28−23

@@ -89,47 +89,52 @@ elabStep st e = do case runStateT e st of

90dumpState :: IState -> ProofState -> Idris ()

91dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

92− iputGoal . render $ pretty nm <> colon <+> text "No more goals."

92+ iputGoal . renderPretty 0.7 breakingSize $

93+ prettyName False [] nm <> colon <+> text "No more goals."

93dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

94dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

94 let OK ty = goalAtFocus ps

95 let OK ty = goalAtFocus ps

95 let OK env = envAtFocus ps

96 let OK env = envAtFocus ps

96− iputGoal . render $

97+ iputGoal . renderPretty 0.7 breakingSize $

97− prettyOtherGoals hs $$

98+ prettyOtherGoals hs <> line <>

98− prettyAssumptions env $$

99+ prettyAssumptions env <> line <>

99− prettyGoal ty

100+ prettyGoal (zip (assumptionNames env) (repeat False)) ty

100 where

101 where

101 -- XXX

102 -- XXX

102− tPretty t = pretty $ delab ist t

103+ tPretty bnd t = pprintPTerm True bnd $ delab ist t

103

104

104− prettyPs [] = empty

105+ assumptionNames :: Env -> [Name]

105− prettyPs ((MN _ r, _) : bs)

106+ assumptionNames = map fst

106− | r == txt "rewrite_rule" = prettyPs bs

107− prettyPs ((n, Let t v) : bs) =

108− nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>

109− tPretty t $$ prettyPs bs)

110− prettyPs ((n, b) : bs) =

111− pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs

112

107

113− prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v

108+ prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation

114− prettyG b = tPretty $ binderTy b

109+ prettyPs bnd [] = empty

110+ prettyPs bnd ((n@(MN _ r), _) : bs)

111+ | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs

112+ prettyPs bnd ((n, Let t v) : bs) =

113+ nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>

114+ tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)

115+ prettyPs bnd ((n, b) : bs) =

116+ line <> bindingOf n False <+> colon <+> tPretty bnd (binderTy b) <> prettyPs ((n, False):bnd) bs

115

117

116− prettyGoal ty =

118+ prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

117− text "---------- Goal: ----------" $$

119+ prettyG bnd b = tPretty bnd $ binderTy b

118− pretty h <> colon $$ nest nestingSize (prettyG ty)

120+

121+ prettyGoal bnd ty =

122+ text "---------- Goal: ----------" <$$>

123+ bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)

119

124

120 prettyAssumptions env =

125 prettyAssumptions env =

121 if length env == 0 then

126 if length env == 0 then

122 empty

127 empty

123 else

128 else

124− text "---------- Assumptions: ----------" $$

129+ text "---------- Assumptions: ----------" <>

125− nest nestingSize (prettyPs $ reverse env)

130+ nest nestingSize (prettyPs [] $ reverse env)

126

131

127 prettyOtherGoals hs =

132 prettyOtherGoals hs =

128 if length hs == 0 then

133 if length hs == 0 then

129 empty

134 empty

130 else

135 else

131− text "---------- Other goals: ----------" $$

136+ text "---------- Other goals: ----------" <$$>

132− pretty hs

137+ nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)

133

138

134lifte :: ElabState [PDecl] -> ElabD a -> Idris a

139lifte :: ElabState [PDecl] -> ElabD a -> Idris a

135lifte st e = do (v, _) <- elabStep st e

140lifte st e = do (v, _) <- elabStep st e

src/Idris/REPL.hs+23−27

@@ -452,10 +452,11 @@ process h fn (Eval t)

452 ist <- getIState

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

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

455− imp <- impShow

455+ let imp = opt_showimp (idris_options ist)

456− c <- colourise

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

457− ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

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

458− showImp (Just ist) imp c (delab ist ty'))

458+ ihPrintTermWithType h tmDoc tyDoc

459+

459process h fn (ExecVal t)

460process h fn (ExecVal t)

460 = do ctxt <- getContext

461 = do ctxt <- getContext

461 ist <- getIState

462 ist <- getIState

@@ -463,10 +464,8 @@ process h fn (ExecVal t)

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

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

464 let ty' = normaliseAll ctxt [] ty

465 let ty' = normaliseAll ctxt [] ty

465 res <- execute tm

466 res <- execute tm

466− imp <- impShow

467+ ihPrintResult h (showTm ist (delab ist res) ++ " : " ++

467− c <- colourise

468+ showTm ist (delab ist ty'))

468− ihPrintResult h (showImp (Just ist) imp c (delab ist res) ++ " : " ++

469− showImp (Just ist) imp c (delab ist ty'))

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

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

471 = do ctxt <- getContext

470 = do ctxt <- getContext

472 ist <- getIState

471 ist <- getIState

@@ -476,9 +475,7 @@ process h fn (Check (PRef _ n))

476 ts@(t:_) ->

475 ts@(t:_) ->

477 case lookup t (idris_metavars ist) of

476 case lookup t (idris_metavars ist) of

478 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)

477 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)

479− Nothing -> ihPrintResult h $

478+ Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)

480− concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++

481− showImp (Just ist) imp c (delabTy ist n)) $ ts

482 [] -> ihPrintError h $ "No such variable " ++ show n

479 [] -> ihPrintError h $ "No such variable " ++ show n

483 where

480 where

484 showMetavarInfo c imp ist n i

481 showMetavarInfo c imp ist n i

@@ -491,27 +488,27 @@ process h fn (Check (PRef _ n))

491 MN _ _ -> "_"

488 MN _ _ -> "_"

492 UN nm | ('_':'_':_) <- str nm -> "_"

489 UN nm | ('_':'_':_) <- str nm -> "_"

493 _ -> showName (Just ist) [] False c n) ++

490 _ -> showName (Just ist) [] False c n) ++

494− " : " ++ showImp (Just ist) imp c t ++ "\n"

491+ " : " ++ showTm ist t ++ "\n"

495 in

492 in

496 current ++ putTy c imp ist (i-1) sc

493 current ++ putTy c imp ist (i-1) sc

497 putTy c imp ist _ sc = putGoal c imp ist sc

494 putTy c imp ist _ sc = putGoal c imp ist sc

498 putGoal c imp ist g

495 putGoal c imp ist g

499 = "--------------------------------------\n" ++

496 = "--------------------------------------\n" ++

500 showName (Just ist) [] False c n ++ " : " ++

497 showName (Just ist) [] False c n ++ " : " ++

501− showImp (Just ist) imp c g

498+ showTm ist g

502

499

503

500

504process h fn (Check t)

501process h fn (Check t)

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

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

506 ctxt <- getContext

503 ctxt <- getContext

507 ist <- getIState

504 ist <- getIState

508− imp <- impShow

505+ let imp = opt_showimp (idris_options ist)

509− c <- colourise

506+ ty' = normaliseC ctxt [] ty

510− let ty' = normaliseC ctxt [] ty

511 case tm of

507 case tm of

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

508+ TType _ ->

513− _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

509+ ihPrintTermWithType h (prettyImp imp PType) type1Doc

514− showImp (Just ist) imp c (delab ist ty))

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

511+ (prettyImp imp (delab ist ty))

515

512

516process h fn (DocStr n)

513process h fn (DocStr n)

517 = do i <- getIState

514 = do i <- getIState

@@ -544,9 +541,9 @@ process h fn (Defn n)

544 [t] -> iputStrLn (showTotal t i)

541 [t] -> iputStrLn (showTotal t i)

545 _ -> return ()

542 _ -> return ()

546 where printCase i (_, lhs, rhs)

543 where printCase i (_, lhs, rhs)

547− = do c <- colourise

544+ = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

548− iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++

545+ in iputStrLn (showTm i' (delab i lhs) ++ " = " ++

549− showImp (Just i) True c (delab i rhs))

546+ showTm i' (delab i rhs))

550process h fn (TotCheck n)

547process h fn (TotCheck n)

551 = do i <- getIState

548 = do i <- getIState

552 case lookupNameTotal n (tt_ctxt i) of

549 case lookupNameTotal n (tt_ctxt i) of

@@ -852,7 +849,7 @@ process h fn (TestInline t)

852 let tm' = inlineTerm ist tm

849 let tm' = inlineTerm ist tm

853 imp <- impShow

850 imp <- impShow

854 c <- colourise

851 c <- colourise

855− iPrintResult (showImp (Just ist) imp c (delab ist tm'))

852+ iPrintResult (showTm ist (delab ist tm'))

856process h fn Execute

853process h fn Execute

857 = do (m, _) <- elabVal toplevel False

854 = do (m, _) <- elabVal toplevel False

858 (PApp fc

855 (PApp fc

@@ -880,11 +877,11 @@ process h fn (Pattelab t)

880

877

881process h fn (Missing n)

878process h fn (Missing n)

882 = do i <- getIState

879 = do i <- getIState

883− c <- colourise

880+ let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

884 case lookupCtxt n (idris_patdefs i) of

881 case lookupCtxt n (idris_patdefs i) of

885 [] -> return ()

882 [] -> return ()

886 [(_, tms)] ->

883 [(_, tms)] ->

887− iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))

884+ iPrintResult (showSep "\n" (map (showTm i') tms))

888 _ -> iPrintError $ "Ambiguous name"

885 _ -> iPrintError $ "Ambiguous name"

889process h fn (DynamicLink l)

886process h fn (DynamicLink l)

890 = do i <- getIState

887 = do i <- getIState

@@ -955,9 +952,8 @@ dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t

955dumpInstance :: Name -> Idris ()

952dumpInstance :: Name -> Idris ()

956dumpInstance n = do i <- getIState

953dumpInstance n = do i <- getIState

957 ctxt <- getContext

954 ctxt <- getContext

958− imp <- impShow

959 case lookupTy n ctxt of

955 case lookupTy n ctxt of

960− ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts

956+ ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts

961

957

962showTotal :: Totality -> IState -> String

958showTotal :: Totality -> IState -> String

963showTotal t@(Partial (Other ns)) i

959showTotal t@(Partial (Other ns)) i

src/Util/Pretty.hs+5−8

@@ -1,10 +1,11 @@

1module Util.Pretty (

2− module Text.PrettyPrint.HughesPJ,

2+ module Text.PrettyPrint.Annotated.Leijen,

3 Sized(..), breakingSize, nestingSize,

4 Pretty(..)

5) where

7−import Text.PrettyPrint.HughesPJ

7+--import Text.PrettyPrint.HughesPJ

8+import Text.PrettyPrint.Annotated.Leijen

9-- A rough notion of size for pretty printing various types.

10-- A rough notion of size for pretty printing various types.

10class Sized a where

11class Sized a where

@@ -23,11 +24,7 @@ breakingSize = 15

23nestingSize :: Int

24nestingSize :: Int

24nestingSize = 1

25nestingSize = 1

26−class Pretty a where

27+class Pretty a ty where

27− pretty :: a -> Doc

28+ pretty :: a -> Doc ty

29−instance Pretty () where

30− pretty () = text "()"

32−instance Pretty a => Pretty [a] where

33− pretty l = foldr ($$) empty $ map pretty l

test/Makefile+7−1

@@ -26,7 +26,7 @@ test_js:

26 @perl ./runtest.pl reg013 --codegen node

27 @perl ./runtest.pl reg014 --codegen node

28 @perl ./runtest.pl reg015 --codegen node

29− @#perl ./runtest.pl reg016 --codegen node

29+ @perl ./runtest.pl reg016 --codegen node

30 @perl ./runtest.pl reg017 --codegen node

31 @perl ./runtest.pl reg018 --codegen node

32 @perl ./runtest.pl reg019 --codegen node

@@ -62,6 +62,12 @@ test_js:

62 @perl ./runtest.pl test029 --codegen node

63 @perl ./runtest.pl test030 --codegen node

64 @perl ./runtest.pl test031 --codegen node

65+ @perl ./runtest.pl test032 --codegen node

66+ @#perl ./runtest.pl test033 --codegen node

67+ @perl ./runtest.pl test034 --codegen node

68+ @perl ./runtest.pl test035 --codegen node

69+ @perl ./runtest.pl test036 --codegen node

70+ @perl ./runtest.pl test037 --codegen node

66test_llvm:

72test_llvm:

67 @perl ./runtest.pl test001 --codegen llvm

73 @perl ./runtest.pl test001 --codegen llvm

test/reg007/expected+6−7

@@ -1,13 +1,12 @@

1reg007.lidr:8:1:A.n is already defined

2reg007.lidr:12:9:When elaborating right hand side of hurrah:

3Can't unify

4− [92mn[0m[94m = [0m[92mlala[0m

4+ n = lala

5with

6− [91m0[0m[94m = [0m[91m1[0m

6+ 0 = 1

8Specifically:

9− Can't unify

9+ Can't unify

10− [91m1[0m

10+ 1

11− with

11+ with

12− [91m0[0m

12+ 0

13−

test/reg007/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --check $@ reg007.lidr

2+idris --nocolour --check $@ reg007.lidr

3rm -f *.ibc

test/reg010/expected+6−7

@@ -1,12 +1,11 @@

1reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst:

2Can't unify

3− P x

3+ P x

4with

5− P y

5+ P y

7Specifically:

8− Can't unify

8+ Can't unify

9− P x

9+ P x

10− with

10+ with

11− P y

11+ P y

12−

test/reg023/expected+6−7

@@ -1,12 +1,11 @@

1reg023.idr:7:5:When elaborating right hand side of bad:

2Can't unify

3− [94mNat[0m

3+ [94mNat[0m

4with

5− [92mf[0m [94mNat[0m

5+ [92mf[0m [94mNat[0m

7Specifically:

8− Can't unify

8+ Can't unify

9− [94mNat[0m

9+ [94mNat[0m

10− with

10+ with

11− [92mf[0m [94mNat[0m

11+ [92mf[0m [94mNat[0m

12−

test/test020/expected+6−7

@@ -1,14 +1,13 @@

1When elaborating right hand side of foo:

2test020a.idr:14:18:Can't unify

3− Vect n a

3+ Vect n a

4with

5− List a

5+ List a

7Specifically:

8− Can't unify

8+ Can't unify

9− Vect n a

9+ Vect n a

10− with

10+ with

11− List a

11+ List a

12−

13[3, 2, 1]

12[3, 2, 1]

14"Number 42"

13"Number 42"

test/test030/expected+6−7

@@ -1,12 +1,11 @@

1test030a.idr:12:14:When elaborating right hand side of testReflect1:

2Can't unify

3− IsJust (Just x)

3+ IsJust (Just x)

4with

5− IsJust (prove (getProof x))

5+ IsJust (prove (getProof x))

7Specifically:

8− Can't unify

8+ Can't unify

9− Just x

9+ Just x

10− with

10+ with

11− Nothing

11+ Nothing

12−

test/test037/expected+2−3

@@ -1,4 +1,3 @@

1In file ErrorReflection.idr line 78 column 5

2− When elaborating right hand side of Main.bad :

2+ When elaborating right hand side of Main.bad :

3− DSL type error: (t'(504) => t'(504)) doesn't match ()

3+ DSL type error: (t'(504) => t'(504)) doesn't match ()

4−

test/test039/expected+1−1

@@ -1,4 +1,4 @@

1FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:

2Could not prove that [] has at least two elements.

3FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

4−Could not prove that Prelude.List.tail [(Prelude.Classes.fromInteger 1)] refl has at least two elements.

4+Could not prove that tail [(fromInteger 1)] refl has at least two elements.