b1f049b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

commitb1f049b5c9329e63bad8f3416fa2e54f0cc9c340 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 1 Feb 2014, 17:15 (13 years ago) parent889d848 eb363b7

11 files changed+331−545

compare with master

unifiedsplit

.gitignore+2−4 CHANGELOG+4 src/IRTS/CodegenJavaScript.hs+206−393 src/Idris/AbsSyntax.hs+27−4 src/Idris/AbsSyntaxTree.hs+46−78 src/Idris/Core/ProofState.hs+6−21 src/Idris/Core/TT.hs+2−10 src/Idris/Parser.hs+2−2 src/Idris/Prover.hs+13−10 src/Idris/REPL.hs+22−18 src/Util/Pretty.hs+1−5

.gitignore+2−4

@@ -15,10 +15,8 @@ cabal.sandbox.config

1515*.tix

1616custom.mk

1717test/output

18−test/test???/output

19−test/reg???/output

20−test/test???/*.exe

21−test/reg???/*.exe

18+test/*[0-9][0-9][0-9]/output

19+test/*[0-9][0-9][0-9]/*.exe

2220tutorial/*.aux

2321tutorial/*.bbl

2422tutorial/*.blg

CHANGELOG+4

@@ -14,6 +14,10 @@ New in 0.9.11:

1414 strings that it emits, which can be used by clients to implement

1515 semantic highlighting like that of the REPL. This has been implemented

1616 in the Emacs mode and the IRC bot, which can serve as examples.

17+* New expression form: with NAME EXPR privileges the namespace NAME

18+ when disambiguating overloaded names. For example, it is possible to

19+ write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",

20+ because the Vect constructors are defined in a namespace called Vect.

1721

1822Internal changes

1923

src/IRTS/CodegenJavaScript.hs+206−393

@@ -24,8 +24,10 @@ idrNamespace = "__IDR__"

2424idrRTNamespace = "__IDRRT__"

2525idrLTNamespace = "__IDRLT__"

2626

27+

2728data JSTarget = Node | JavaScript deriving Eq

2829

30+

2931data JSType = JSIntTy

3032 | JSStringTy

3133 | JSIntegerTy

@@ -35,16 +37,19 @@ data JSType = JSIntTy

3537 | JSForgotTy

3638 deriving Eq

3739

40+

3841data JSInteger = JSBigZero

3942 | JSBigOne

4043 | JSBigInt Integer

4144 deriving Eq

4245

46+

4347data JSNum = JSInt Int

4448 | JSFloat Double

4549 | JSInteger JSInteger

4650 deriving Eq

4751

52+

4853data JS = JSRaw String

4954 | JSIdent String

5055 | JSFunction [String] JS

@@ -62,7 +67,6 @@ data JS = JSRaw String

6267 | JSTrue

6368 | JSFalse

6469 | JSArray [JS]

65− | JSObject [(String, JS)]

6670 | JSString String

6771 | JSChar String

6872 | JSNum JSNum

@@ -71,8 +75,10 @@ data JS = JSRaw String

7175 | JSIndex JS JS

7276 | JSCond [(JS, JS)]

7377 | JSTernary JS JS JS

78+ | JSParens JS

7479 deriving Eq

7580

81+

7682compileJS :: JS -> String

7783compileJS (JSRaw code) =

7884 code

@@ -114,7 +120,7 @@ compileJS (JSNew name args) =

114120 "new " ++ name ++ "(" ++ intercalate "," (map compileJS args) ++ ")"

115121

116122compileJS (JSError exc) =

117− "(function(){throw '" ++ exc ++ "';})()"

123+ "throw new Error(\"" ++ exc ++ "\")"

118124

119125compileJS (JSOp op lhs rhs) =

120126 compileJS lhs ++ " " ++ op ++ " " ++ compileJS rhs

@@ -145,12 +151,6 @@ compileJS JSFalse =

145151compileJS (JSArray elems) =

146152 "[" ++ intercalate "," (map compileJS elems) ++ "]"

147153

148−compileJS (JSObject fields) =

149− "{" ++ intercalate ",\n" (map compileField fields) ++ "}"

150− where

151− compileField :: (String, JS) -> String

152− compileField (name, val) = '\'' : name ++ "' : " ++ compileJS val

153−

154154compileJS (JSString str) =

155155 show str

156156

@@ -174,19 +174,15 @@ compileJS (JSIndex lhs rhs) =

174174 compileJS lhs ++ "[" ++ compileJS rhs ++ "]"

175175

176176compileJS (JSCond branches) =

177− intercalate " else " $ map createIfBlock (eliminateDeadBranches branches)

177+ intercalate " else " $ map createIfBlock branches

178178 where

179− eliminateDeadBranches (e@(JSTrue, _):_) = [e]

180− eliminateDeadBranches (x:xs) = x : eliminateDeadBranches xs

181− eliminateDeadBranches [] = []

182−

183179 createIfBlock (JSTrue, e) =

184180 "{\n"

185− ++ "return " ++ compileJS e

181+ ++ compileJS e

186182 ++ ";\n}"

187183 createIfBlock (cond, e) =

188184 "if (" ++ compileJS cond ++") {\n"

189− ++ "return " ++ compileJS e

185+ ++ compileJS e

190186 ++ ";\n}"

191187

192188compileJS (JSTernary cond true false) =

@@ -195,48 +191,64 @@ compileJS (JSTernary cond true false) =

195191 f = compileJS false in

196192 "(" ++ c ++ ")?(" ++ t ++ "):(" ++ f ++ ")"

197193

194+compileJS (JSParens js) =

195+ "(" ++ compileJS js ++ ")"

196+

197+

198198jsTailcall :: JS -> JS

199199jsTailcall call =

200200 jsCall (idrRTNamespace ++ "tailcall") [

201201 JSFunction [] (JSReturn call)

202202 ]

203203

204+

204205jsCall :: String -> [JS] -> JS

205206jsCall fun = JSApp (JSIdent fun)

206207

208+

207209jsMeth :: JS -> String -> [JS] -> JS

208210jsMeth obj meth =

209211 JSApp (JSProj obj meth)

210212

213+

211214jsInstanceOf :: JS -> JS -> JS

212215jsInstanceOf = JSOp "instanceof"

213216

217+

214218jsEq :: JS -> JS -> JS

215219jsEq = JSOp "=="

216220

221+

217222jsAnd :: JS -> JS -> JS

218223jsAnd = JSOp "&&"

219224

225+

220226jsType :: JS

221227jsType = JSIdent $ idrRTNamespace ++ "Type"

222228

229+

223230jsCon :: JS

224231jsCon = JSIdent $ idrRTNamespace ++ "Con"

225232

233+

226234jsTag :: JS -> JS

227235jsTag obj = JSProj obj "tag"

228236

237+

229238jsTypeTag :: JS -> JS

230239jsTypeTag obj = JSProj obj "type"

231240

241+

232242jsBigInt :: JS -> JS

233243jsBigInt (JSString "0") = JSNum $ JSInteger JSBigZero

234244jsBigInt (JSString "1") = JSNum $ JSInteger JSBigOne

235245jsBigInt val = JSApp (JSIdent $ idrRTNamespace ++ "bigInt") [val]

236246

247+

237248jsVar :: Int -> String

238249jsVar = ("__var_" ++) . show

239250

251+

240252jsLet :: String -> JS -> JS -> JS

241253jsLet name value body =

242254 JSApp (

@@ -246,6 +258,33 @@ jsLet name value body =

246258 ) [value]

247259

248260

261+jsError :: String -> JS

262+jsError err = JSApp (JSFunction [] (JSError err)) []

263+

264+

265+transformJS :: (JS -> JS) -> JS -> JS

266+transformJS tr js =

267+ transformHelper js

268+ where

269+ transformHelper :: JS -> JS

270+ transformHelper js

271+ | JSFunction args body <- js = JSFunction args $ tr body

272+ | JSSeq seq <- js = JSSeq $ map tr seq

273+ | JSReturn ret <- js = JSReturn $ tr ret

274+ | JSApp lhs rhs <- js = JSApp (tr lhs) $ map tr rhs

275+ | JSNew con args <- js = JSNew con $ map tr args

276+ | JSOp op lhs rhs <- js = JSOp op (tr lhs) (tr rhs)

277+ | JSProj obj field <- js = JSProj (tr obj) field

278+ | JSArray vals <- js = JSArray $ map tr vals

279+ | JSAssign lhs rhs <- js = JSAssign (tr lhs) (tr rhs)

280+ | JSAlloc var val <- js = JSAlloc var $ fmap tr val

281+ | JSIndex lhs rhs <- js = JSIndex (tr lhs) (tr rhs)

282+ | JSCond conds <- js = JSCond $ map (tr *** tr) conds

283+ | JSTernary c t f <- js = JSTernary (tr c) (tr t) (tr f)

284+ | JSParens val <- js = JSParens $ tr val

285+ | otherwise = js

286+

287+

249288jsSubst :: JS -> JS -> JS -> JS

250289jsSubst var new old

251290 | var == old = new

@@ -284,37 +323,7 @@ jsSubst (JSIdent var) new (JSApp (JSFunction [arg] body) vals)

284323 body

285324 )) $ map (jsSubst (JSIdent var) new) vals

286325

287−jsSubst var new (JSApp lhs rhs) =

288− JSApp (jsSubst var new lhs) (map (jsSubst var new) rhs)

289−

290−jsSubst var new (JSFunction [] body) =

291− JSFunction [] (jsSubst var new body)

292−

293−jsSubst var new (JSReturn ret) =

294− JSReturn $ jsSubst var new ret

295−

296−jsSubst var new (JSProj obj field) =

297− JSProj (jsSubst var new obj) field

298−

299−jsSubst var new (JSSeq body) =

300− JSSeq $ map (jsSubst var new) body

301−

302−jsSubst var new (JSOp op lhs rhs) =

303− JSOp op (jsSubst var new lhs) (jsSubst var new rhs)

304−

305−jsSubst var new (JSIndex obj field) =

306− JSIndex (jsSubst var new obj) (jsSubst var new field)

307−

308−jsSubst var new (JSCond conds) =

309− JSCond (map ((jsSubst var new) *** (jsSubst var new)) conds)

310−

311−jsSubst var new (JSAssign lhs rhs) =

312− JSAssign (jsSubst var new lhs) (jsSubst var new rhs)

313−

314−jsSubst var new (JSAlloc val (Just js)) =

315− JSAlloc val (Just (jsSubst var new js))

316−

317−jsSubst _ _ js = js

326+jsSubst var new js = transformJS (jsSubst var new) js

318327

319328

320329removeAllocations :: JS -> JS

@@ -330,43 +339,7 @@ removeAllocations (JSSeq body) =

330339 map (jsSubst (JSIdent name) val) (removeHelper js)

331340 removeHelper (j:js) = j : removeHelper js

332341

333−removeAllocations (JSFunction args body) =

334− JSFunction args $ removeAllocations body

335−

336−removeAllocations (JSReturn ret) =

337− JSReturn $ removeAllocations ret

338−

339−removeAllocations (JSApp fun args) =

340− JSApp (removeAllocations fun) (map removeAllocations args)

341−

342−removeAllocations (JSNew con args) =

343− JSNew con $ map removeAllocations args

344−

345−removeAllocations (JSOp op lhs rhs) =

346− JSOp op (removeAllocations lhs) (removeAllocations rhs)

347−

348−removeAllocations (JSProj obj field) =

349− JSProj (removeAllocations obj) field

350−

351−removeAllocations (JSArray vals) =

352− JSArray $ map removeAllocations vals

353−

354−removeAllocations (JSAssign lhs rhs) =

355− JSAssign (removeAllocations lhs) (removeAllocations rhs)

356−

357−removeAllocations (JSAlloc name (Just val)) =

358− JSAlloc name $ Just (removeAllocations val)

359−

360−removeAllocations (JSIndex val idx) =

361− JSIndex (removeAllocations val) (removeAllocations idx)

362−

363−removeAllocations (JSCond conds) =

364− JSCond $ map (removeAllocations *** removeAllocations) conds

365−

366−removeAllocations (JSTernary c t f) =

367− JSTernary (removeAllocations c) (removeAllocations t) (removeAllocations f)

368−

369−removeAllocations js = js

342+removeAllocations js = transformJS removeAllocations js

370343

371344

372345isJSConstant :: JS -> Bool

@@ -379,20 +352,23 @@ isJSConstant js

379352 | JSApp (JSIdent "__IDRRT__bigInt") _ <- js = True

380353 | otherwise = False

381354

355+

382356inlineJS :: JS -> JS

357+inlineJS (JSReturn (JSApp (JSFunction [] err@(JSError _)) [])) = err

383358inlineJS (JSReturn (JSApp (JSFunction ["cse"] body) [val@(JSVar _)])) =

384359 inlineJS $ jsSubst (JSIdent "cse") val body

385360

361+

386362inlineJS (JSReturn (JSApp (JSFunction [arg] cond@(JSCond _)) [val])) =

387− JSSeq [ JSAlloc arg (Just (inlineJS val))

388− , inlineJS cond

389− ]

363+ inlineJS $ JSSeq [ JSAlloc arg (Just val)

364+ , cond

365+ ]

390366

391367inlineJS (JSApp (JSProj (JSFunction args (JSReturn body)) "apply") [

392368 JSThis,JSProj var "vars"

393369 ])

394370 | var /= JSIdent "cse" =

395− inlineApply args body 0

371+ inlineJS $ inlineApply args body 0

396372 where

397373 inlineApply [] body _ = inlineJS body

398374 inlineApply (a:as) body n =

@@ -411,94 +387,62 @@ inlineJS (JSApp (JSIdent "__IDRRT__tailcall") [

411387inlineJS (JSApp (JSFunction [arg] (JSReturn ret)) [val])

412388 | JSNew con [tag, vals] <- ret

413389 , opt <- inlineJS val =

414− JSNew con [tag, jsSubst (JSIdent arg) opt vals]

390+ inlineJS $ JSNew con [tag, inlineJS $ jsSubst (JSIdent arg) opt vals]

415391

416392 | JSNew con [JSFunction [] (JSReturn (JSApp fun vars))] <- ret

417393 , opt <- inlineJS val =

418− JSNew con [JSFunction [] (

394+ inlineJS $ JSNew con [JSFunction [] (

419395 JSReturn (

420396 JSApp (

421− jsSubst (JSIdent arg) opt fun

397+ inlineJS $ jsSubst (JSIdent arg) opt fun

422398 ) (

423− map (jsSubst (JSIdent arg) opt) vars

399+ map (inlineJS . jsSubst (JSIdent arg) opt) vars

424400 )

425401 )

426402 )]

427403

428404 | JSApp (JSProj obj field) args <- ret

429405 , opt <- inlineJS val =

430− JSApp (

431− JSProj (jsSubst (JSIdent arg) opt obj) field

406+ inlineJS $ JSApp (

407+ inlineJS $ JSProj (jsSubst (JSIdent arg) opt obj) field

432408 ) (

433− map (jsSubst (JSIdent arg) opt) args

409+ map (inlineJS . jsSubst (JSIdent arg) opt) args

434410 )

435411

436412 | JSIndex (JSProj obj field) idx <- ret

437413 , opt <- inlineJS val =

438− JSIndex (JSProj (

439− jsSubst (JSIdent arg) opt obj

414+ inlineJS $ JSIndex (JSProj (

415+ inlineJS $ jsSubst (JSIdent arg) opt obj

440416 ) field

441− ) (jsSubst (JSIdent arg) opt idx)

417+ ) (inlineJS $ jsSubst (JSIdent arg) opt idx)

442418

443419 | JSOp op lhs rhs <- ret

444420 , opt <- inlineJS val =

445− JSOp op (jsSubst (JSIdent arg) opt lhs) $

446− (jsSubst (JSIdent arg) opt rhs)

421+ inlineJS $ JSOp op (inlineJS $ jsSubst (JSIdent arg) opt lhs) $

422+ (inlineJS $ jsSubst (JSIdent arg) opt rhs)

447423

448424 | JSApp (JSIdent fun) args <- ret

449425 , opt <- inlineJS val =

450− JSApp (JSIdent fun) $ map (jsSubst (JSIdent arg) opt) args

451−

452−inlineJS (JSApp fun args) =

453− JSApp (inlineJS fun) (map inlineJS args)

454−

455−inlineJS (JSNew con args) =

456− JSNew con $ map inlineJS args

457−

458−inlineJS (JSArray fields) =

459− JSArray (map inlineJS fields)

426+ inlineJS $ JSApp (JSIdent fun) $ map (inlineJS . jsSubst (JSIdent arg) opt) args

460427

461−inlineJS (JSAssign lhs rhs) =

462− JSAssign (inlineJS lhs) (inlineJS rhs)

428+inlineJS js = transformJS inlineJS js

463429

464−inlineJS (JSSeq seq) =

465− JSSeq (map inlineJS seq)

466−

467−inlineJS (JSFunction args body) =

468− JSFunction args (inlineJS body)

469−

470−inlineJS (JSProj (JSFunction args body) field) =

471− JSProj (JSFunction args (inlineJS body)) field

472−

473−inlineJS (JSReturn js) =

474− JSReturn $ inlineJS js

475−

476−inlineJS (JSAlloc name (Just js)) =

477− JSAlloc name (Just $ inlineJS js)

478−

479−inlineJS (JSCond cases) =

480− JSCond (map (second inlineJS) cases)

481−

482−inlineJS (JSObject fields) =

483− JSObject (map (second inlineJS) fields)

484−

485−inlineJS (JSOp op lhs rhs) =

486− JSOp op (inlineJS lhs) (inlineJS rhs)

487−

488−inlineJS js = js

489430

490431reduceJS :: [JS] -> [JS]

491432reduceJS js = reduceLoop [] ([], js)

492433

434+

493435funName :: JS -> String

494436funName (JSAlloc fun _) = fun

495437

438+

496439elimDeadLoop :: [JS] -> [JS]

497440elimDeadLoop js

498441 | ret <- deadEvalApplyCases js

499442 , ret /= js = elimDeadLoop ret

500443 | otherwise = js

501444

445+

502446deadEvalApplyCases :: [JS] -> [JS]

503447deadEvalApplyCases js =

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

@@ -533,7 +477,11 @@ deadEvalApplyCases js =

533477

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

535479

480+ getTags (JSParens js) = getTags js

481+

536482 getTags js = []

483+

484+

537485 removeHelper :: [Int] -> JS -> JS

538486 removeHelper tags (JSAlloc fun (Just (

539487 JSApp (JSFunction [] (JSSeq seq)) []))

@@ -544,6 +492,7 @@ deadEvalApplyCases js =

544492

545493 removeHelper _ js = js

546494

495+

547496 remover :: [Int] -> [JS] -> [JS]

548497 remover tags (

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

@@ -587,8 +536,11 @@ initConstructors js =

587536

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

589538

539+ getTags (JSParens js) = getTags js

540+

590541 getTags js = []

591542

543+

592544 replaceConstructors :: [Int] -> [JS] -> [JS]

593545 replaceConstructors tags js = map (replaceHelper tags) js

594546 where

@@ -596,47 +548,8 @@ initConstructors js =

596548 replaceHelper tags (JSNew "__IDRRT__Con" [JSNum (JSInt tag), JSArray []])

597549 | tag `elem` tags = JSIdent ("__IDRCTR__" ++ show tag)

598550

599− replaceHelper tags (JSNew con args) =

600− JSNew con $ map (replaceHelper tags) args

601−

602− replaceHelper tags (JSFunction fun body) =

603− JSFunction fun (replaceHelper tags body)

604−

605− replaceHelper tags (JSReturn ret) =

606− JSReturn (replaceHelper tags ret)

607−

608− replaceHelper tags (JSApp lhs rhs) =

609− JSApp (replaceHelper tags lhs) (map (replaceHelper tags) rhs)

610−

611− replaceHelper tags (JSSeq seq) =

612− JSSeq $ map (replaceHelper tags) seq

613−

614− replaceHelper tags (JSOp op lhs rhs) =

615− JSOp op (replaceHelper tags lhs) (replaceHelper tags rhs)

616−

617− replaceHelper tags (JSProj obj field) =

618− JSProj (replaceHelper tags obj) field

619−

620− replaceHelper tags (JSArray vals) =

621− JSArray $ map (replaceHelper tags) vals

551+ replaceHelper tags js = transformJS (replaceHelper tags) js

622552

623− replaceHelper tags (JSAssign lhs rhs) =

624− JSAssign (replaceHelper tags lhs) (replaceHelper tags rhs)

625−

626− replaceHelper tags (JSAlloc var (Just val)) =

627− JSAlloc var $ Just (replaceHelper tags val)

628−

629− replaceHelper tags (JSCond conds) =

630− JSCond (map ((replaceHelper tags) *** (replaceHelper tags)) conds)

631−

632− replaceHelper tags (JSTernary c t f) =

633− JSTernary (replaceHelper tags c) (

634− replaceHelper tags t

635− ) (

636− replaceHelper tags f

637− )

638−

639− replaceHelper tags js = js

640553

641554 createConstant :: Int -> JS

642555 createConstant tag =

@@ -644,6 +557,7 @@ initConstructors js =

644557 JSNew (idrRTNamespace ++ "Con") [JSNum (JSInt tag), JSArray []]

645558 ))

646559

560+

647561removeIDs :: [JS] -> [JS]

648562removeIDs js =

649563 case partition isID js of

@@ -655,10 +569,12 @@ removeIDs js =

655569

656570 isID _ = False

657571

572+

658573 idFor :: JS -> (String, Int)

659574 idFor (JSAlloc fun (Just (JSFunction _ (JSSeq body))))

660575 | JSReturn (JSVar (Loc pos)) <- last body = (fun, pos)

661576

577+

662578 removeIDCall :: [(String, Int)] -> JS -> JS

663579 removeIDCall ids (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

664580 JSReturn (JSApp (JSIdent fun) args)

@@ -676,37 +592,8 @@ removeIDs js =

676592 | Just pos <- lookup fun ids

677593 , pos < length args = args !! pos

678594

679− removeIDCall ids (JSAlloc fun (Just body)) =

680− JSAlloc fun (Just $ removeIDCall ids body)

681−

682− removeIDCall ids (JSReturn js) =

683− JSReturn $ removeIDCall ids js

684−

685− removeIDCall ids (JSSeq js) =

686− JSSeq $ map (removeIDCall ids) js

687−

688− removeIDCall ids (JSNew con args) =

689− JSNew con $ map (removeIDCall ids) args

690−

691− removeIDCall ids (JSFunction args body) =

692− JSFunction args $ removeIDCall ids body

595+ removeIDCall ids js = transformJS (removeIDCall ids) js

693596

694− removeIDCall ids (JSApp fun args) =

695− JSApp (removeIDCall ids fun) $ map (removeIDCall ids) args

696−

697− removeIDCall ids (JSProj obj field) =

698− JSProj (removeIDCall ids obj) field

699−

700− removeIDCall ids (JSCond conds) =

701− JSCond $ map (removeIDCall ids *** removeIDCall ids) conds

702−

703− removeIDCall ids (JSAssign lhs rhs) =

704− JSAssign (removeIDCall ids lhs) (removeIDCall ids rhs)

705−

706− removeIDCall ids (JSArray fields) =

707− JSArray $ map (removeIDCall ids) fields

708−

709− removeIDCall _ js = js

710597

711598inlineFunctions :: [JS] -> [JS]

712599inlineFunctions js =

@@ -791,42 +678,39 @@ inlineFunctions js =

791678 , countInvokations name f

792679 ]

793680

681+ countInvokations name (JSParens js) =

682+ countInvokations name js

683+

794684 countInvokations _ _ = 0

795685

796686

797687reduceConstant :: JS -> JS

798−reduceConstant (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

799− JSReturn (JSApp (JSIdent "__IDR__mEVAL0") [JSNum num])

800− )]) = JSNum num

801−

802−reduceConstant (JSReturn ret) =

803− JSReturn (reduceConstant ret)

804−

805−reduceConstant (JSApp fun args) =

806− JSApp (reduceConstant fun) (map reduceConstant args)

807−

808−reduceConstant (JSArray fields) =

809− JSArray (map reduceConstant fields)

810−

811−reduceConstant (JSAlloc name (Just val)) =

812− JSAlloc name $ Just (reduceConstant val)

813−

814−reduceConstant (JSNew con args) =

815− JSNew con (map reduceConstant args)

688+reduceConstant

689+ (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

690+ JSReturn (JSApp (JSIdent "__IDR__mEVAL0") [val])

691+ )])

692+ | JSNum num <- val = val

693+ | JSOp op lhs rhs <- val =

694+ JSParens $ JSOp op (reduceConstant lhs) (reduceConstant rhs)

695+

696+ | JSApp (JSProj lhs op) [rhs] <- val

697+ , op `elem` [ "subtract"

698+ , "add"

699+ , "multiply"

700+ , "divide"

701+ , "mod"

702+ , "equals"

703+ , "lesser"

704+ , "lesserOrEquals"

705+ , "greater"

706+ , "greaterOrEquals"

707+ ] = val

708+

709+reduceConstant (JSApp ident [(JSParens js)]) =

710+ JSApp ident [reduceConstant js]

711+

712+reduceConstant js = transformJS reduceConstant js

816713

817−reduceConstant (JSProj obj field) =

818− JSProj (reduceConstant obj) field

819−

820−reduceConstant (JSCond conds) =

821− JSCond $ map (reduceConstant *** reduceConstant) conds

822−

823−reduceConstant (JSSeq seq) =

824− JSSeq $ map reduceConstant seq

825−

826−reduceConstant (JSFunction args body) =

827− JSFunction args (reduceConstant body)

828−

829−reduceConstant js = js

830714

831715reduceConstants :: JS -> JS

832716reduceConstants js

@@ -848,6 +732,7 @@ elimDuplicateEvals (JSAlloc fun (Just (JSFunction args (JSSeq seq)))) =

848732

849733elimDuplicateEvals js = js

850734

735+

851736optimizeEvalTailcalls :: (String, String) -> JS -> JS

852737optimizeEvalTailcalls (fun, tc) js =

853738 optHelper js

@@ -858,106 +743,28 @@ optimizeEvalTailcalls (fun, tc) js =

858743 ])

859744 | n == fun = JSApp (JSIdent tc) $ map optHelper args

860745

861− optHelper (JSFunction args body) =

862− JSFunction args $ optHelper body

863−

864− optHelper (JSSeq seq) =

865− JSSeq $ map optHelper seq

866−

867− optHelper (JSReturn ret) =

868− JSReturn $ optHelper ret

869−

870− optHelper (JSApp lhs rhs) =

871− JSApp (optHelper lhs) (map optHelper rhs)

872−

873− optHelper (JSNew con args) =

874− JSNew con $ map optHelper args

875−

876− optHelper (JSOp op lhs rhs) =

877− JSOp op (optHelper lhs) (optHelper rhs)

878−

879− optHelper (JSProj obj field) =

880− JSProj (optHelper obj) field

881−

882− optHelper (JSArray vals) =

883− JSArray $ map optHelper vals

884−

885− optHelper (JSAssign lhs rhs) =

886− JSAssign (optHelper lhs) (optHelper rhs)

887−

888− optHelper (JSAlloc var (Just val)) =

889− JSAlloc var (Just $ optHelper val)

890−

891− optHelper (JSIndex lhs rhs) =

892− JSIndex (optHelper lhs) (optHelper rhs)

893−

894− optHelper (JSCond conds) =

895− JSCond $ map (optHelper *** optHelper) conds

896−

897− optHelper (JSTernary c t f) =

898− JSTernary (

899− optHelper c

900− ) (

901− optHelper t

902− ) (

903− optHelper f

904− )

905−

906− optHelper js = js

746+ optHelper js = transformJS optHelper js

907747

908748

909749removeInstanceChecks :: JS -> JS

910750removeInstanceChecks (JSCond conds) =

911− JSCond $ map (removeHelper *** removeInstanceChecks) conds

751+ JSCond $ eliminateDeadBranches $ map (

752+ removeHelper *** removeInstanceChecks

753+ ) conds

912754 where

913755 removeHelper (

914756 JSOp "&&" (JSOp "instanceof" _ (JSIdent "__IDRRT__Con")) check

915757 ) = removeHelper check

916758 removeHelper js = js

917759

918−removeInstanceChecks (JSFunction args body) =

919− JSFunction args $ removeInstanceChecks body

920−

921−removeInstanceChecks (JSSeq seq) =

922− JSSeq $ map removeInstanceChecks seq

923−

924−removeInstanceChecks (JSReturn ret) =

925− JSReturn $ removeInstanceChecks ret

926−

927−removeInstanceChecks (JSApp lhs rhs) =

928− JSApp (removeInstanceChecks lhs) $ map removeInstanceChecks rhs

929760

930−removeInstanceChecks (JSNew con args) =

931− JSNew con $ map removeInstanceChecks args

932−

933−removeInstanceChecks (JSOp op lhs rhs) =

934− JSOp op (removeInstanceChecks lhs) (removeInstanceChecks rhs)

935−

936−removeInstanceChecks (JSProj obj field) =

937− JSProj (removeInstanceChecks obj) field

938−

939−removeInstanceChecks (JSArray vals) =

940− JSArray $ map removeInstanceChecks vals

941−

942−removeInstanceChecks (JSAssign lhs rhs) =

943− JSAssign (removeInstanceChecks lhs) (removeInstanceChecks rhs)

944−

945−removeInstanceChecks (JSAlloc var (Just val)) =

946− JSAlloc var (Just $ removeInstanceChecks val)

947−

948−removeInstanceChecks (JSIndex lhs rhs) =

949− JSIndex (removeInstanceChecks lhs) (removeInstanceChecks rhs)

761+ eliminateDeadBranches (e@(JSTrue, _):_) = [e]

762+ eliminateDeadBranches [(_, js)] = [(JSTrue, js)]

763+ eliminateDeadBranches (x:xs) = x : eliminateDeadBranches xs

764+ eliminateDeadBranches [] = []

950765

951−removeInstanceChecks (JSTernary c t f) =

952− JSTernary (

953− removeInstanceChecks c

954− ) (

955− removeInstanceChecks t

956− ) (

957− removeInstanceChecks f

958− )

766+removeInstanceChecks js = transformJS removeInstanceChecks js

959767

960−removeInstanceChecks js = js

961768

962769reduceLoop :: [String] -> ([JS], [JS]) -> [JS]

963770reduceLoop reduced (cons, program) =

@@ -974,13 +781,15 @@ reduceLoop reduced (cons, program) =

974781 reducable $ last body

975782 | otherwise = False

976783 where reducable :: JS -> Bool

977− reducable (JSReturn js) = reducable js

978− reducable (JSNew _ args) = and $ map reducable args

979− reducable (JSArray fields) = and $ map reducable fields

980− reducable (JSNum _) = True

981− reducable JSNull = True

982− reducable (JSIdent _) = True

983− reducable _ = False

784+ reducable js

785+ | JSReturn ret <- js = reducable ret

786+ | JSNew _ args <- js = and $ map reducable args

787+ | JSArray fields <- js = and $ map reducable fields

788+ | JSNum _ <- js = True

789+ | JSNull <- js = True

790+ | JSIdent _ <- js = True

791+ | otherwise = False

792+

984793

985794 reduce :: JS -> JS

986795 reduce (JSAlloc fun (Just (JSFunction _ (JSSeq body))))

@@ -988,6 +797,7 @@ reduceLoop reduced (cons, program) =

988797

989798 reduce js = js

990799

800+

991801 reduceCall :: [String] -> JS -> JS

992802 reduceCall funs (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

993803 JSReturn (JSApp id@(JSIdent ret) _)

@@ -997,43 +807,8 @@ reduceLoop reduced (cons, program) =

997807 reduceCall funs js@(JSApp id@(JSIdent fun) _)

998808 | fun `elem` funs = id

999809

1000− reduceCall funs (JSAlloc fun (Just body)) =

1001− JSAlloc fun (Just $ reduceCall funs body)

1002−

1003− reduceCall funs (JSReturn js) =

1004− JSReturn $ reduceCall funs js

810+ reduceCall funs js = transformJS (reduceCall funs) js

1005811

1006− reduceCall funs (JSSeq js) =

1007− JSSeq $ map (reduceCall funs) js

1008−

1009− reduceCall funs (JSNew con args) =

1010− JSNew con $ map (reduceCall funs) args

1011−

1012− reduceCall funs (JSFunction args body) =

1013− JSFunction args $ reduceCall funs body

1014−

1015− reduceCall funs (JSApp fun args) =

1016− JSApp (reduceCall funs fun) $ map (reduceCall funs) args

1017−

1018− reduceCall funs (JSProj obj field) =

1019− JSProj (reduceCall funs obj) field

1020−

1021− reduceCall funs (JSIndex obj idx) =

1022− JSIndex (reduceCall funs obj) (reduceCall funs idx)

1023−

1024− reduceCall funs (JSOp op rhs lhs) =

1025− JSOp op (reduceCall funs rhs) (reduceCall funs lhs)

1026−

1027− reduceCall funs (JSCond conds) =

1028− JSCond $ map (reduceCall funs *** reduceCall funs) conds

1029−

1030− reduceCall funs (JSAssign lhs rhs) =

1031− JSAssign (reduceCall funs lhs) (reduceCall funs rhs)

1032−

1033− reduceCall funs (JSArray fields) =

1034− JSArray $ map (reduceCall funs) fields

1035−

1036− reduceCall _ js = js

1037812

1038813optimizeJS :: JS -> JS

1039814optimizeJS = inlineLoop

@@ -1043,6 +818,7 @@ optimizeJS = inlineLoop

1043818 , opt /= js = inlineLoop opt

1044819 | otherwise = js

1045820

821+

1046822codegenJavaScript

1047823 :: JSTarget

1048824 -> [(Name, SDecl)]

@@ -1074,25 +850,29 @@ codegenJavaScript target definitions filename outputType = do

1074850 def :: [(String, SDecl)]

1075851 def = map (first translateNamespace) definitions

1076852

853+

1077854 functions :: [String]

1078− functions =

1079− let translated =

1080− concatMap translateDeclaration def ++ [mainLoop, invokeLoop]

1081−

1082− optimized = map optimizeJS translated

1083− idsRemoved = removeIDs optimized

1084− reduced = reduceJS idsRemoved

1085− constRemoved = map reduceConstants reduced

1086− constrInit = initConstructors constRemoved

1087− removeAlloc = map removeAllocations constrInit

1088− deadElim = elimDeadLoop removeAlloc

1089− inlined = inlineFunctions deadElim

1090− elimDup = map elimDuplicateEvals inlined

1091− evalTC = map (optimizeEvalTailcalls ("__IDR__mEVAL0", "__IDRRT__EVALTC")) elimDup

1092− applyTC = map (optimizeEvalTailcalls ("__IDR__mAPPLY0", "__IDRRT__APPLYTC")) evalTC

1093− remChecks = map removeInstanceChecks applyTC

1094− js = remChecks in

1095− map compileJS js

855+ functions = translate >>> optimize >>> compile $ def

856+ where

857+ translate p = concatMap translateDeclaration p ++ [mainLoop, invokeLoop]

858+ optimize p = foldl' (flip ($)) p opt

859+ compile = map compileJS

860+

861+ opt =

862+ [ map optimizeJS

863+ , removeIDs

864+ , reduceJS

865+ , map reduceConstants

866+ , initConstructors

867+ , map removeAllocations

868+ , elimDeadLoop

869+ , inlineFunctions

870+ , map elimDuplicateEvals

871+ , map (optimizeEvalTailcalls ("__IDR__mEVAL0", "__IDRRT__EVALTC"))

872+ , map (optimizeEvalTailcalls ("__IDR__mAPPLY0", "__IDRRT__APPLYTC"))

873+ , map removeInstanceChecks

874+ ]

875+

1096876

1097877 mainLoop :: JS

1098878 mainLoop =

@@ -1109,12 +889,15 @@ codegenJavaScript target definitions filename outputType = do

1109889 mainFun :: JS

1110890 mainFun = jsTailcall $ jsCall runMain []

1111891

892+

1112893 runMain :: String

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

1114895

896+

1115897 invokeLoop :: JS

1116898 invokeLoop = jsCall "main" []

1117899

900+

1118901translateIdentifier :: String -> String

1119902translateIdentifier =

1120903 replaceReserved . concatMap replaceBadChars

@@ -1128,6 +911,8 @@ translateIdentifier =

1128911 replaceReserved s

1129912 | s `elem` reserved = '_' : s

1130913 | otherwise = s

914+

915+

1131916 reserved = [ "break"

1132917 , "case"

1133918 , "catch"

@@ -1173,6 +958,7 @@ translateIdentifier =

1173958 , "yield"

1174959 ]

1175960

961+

1176962translateNamespace :: Name -> String

1177963translateNamespace (UN _) = idrNamespace

1178964translateNamespace (NS _ ns) = idrNamespace ++ concatMap (translateIdentifier . str) ns

@@ -1180,6 +966,7 @@ translateNamespace (MN _ _) = idrNamespace

1180966translateNamespace (SN name) = idrNamespace ++ translateSpecialName name

1181967translateNamespace NErased = idrNamespace

1182968

969+

1183970translateName :: Name -> String

1184971translateName (UN name) = 'u' : translateIdentifier (str name)

1185972translateName (NS name _) = 'n' : translateName name

@@ -1187,6 +974,7 @@ translateName (MN i name) = 'm' : translateIdentifier (str name) ++ show i

1187974translateName (SN name) = 's' : translateSpecialName name

1188975translateName NErased = "e"

1189976

977+

1190978translateSpecialName :: SpecialName -> String

1191979translateSpecialName name

1192980 | WhereN i m n <- name =

@@ -1200,6 +988,7 @@ translateSpecialName name

1200988 | CaseN n <- name =

1201989 'c' : translateName n

1202990

991+

1203992translateConstant :: Const -> JS

1204993translateConstant (I i) = JSNum (JSInt i)

1205994translateConstant (Fl f) = JSNum (JSFloat f)

@@ -1217,7 +1006,8 @@ translateConstant PtrType = JSType JSPtrTy

12171006translateConstant Forgot = JSType JSForgotTy

12181007translateConstant (BI i) = jsBigInt $ JSString (show i)

12191008translateConstant c =

1220− JSError $ "Unimplemented Constant: " ++ show c

1009+ jsError $ "Unimplemented Constant: " ++ show c

1010+

12211011

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

12231013translateDeclaration (path, SFun name params stackSize body)

@@ -1267,17 +1057,22 @@ translateDeclaration (path, SFun name params stackSize body)

12671057 hasProp table var =

12681058 JSIndex (JSIdent table) (JSProj (JSIdent var) "tag")

12691059

1060+

12701061 caseFun :: [(LVar, String)] -> LVar -> SAlt -> JS

12711062 caseFun aux var cse =

1272− jsFunAux aux (translateCase (Just (translateVariableName var)) cse)

1063+ let (JSReturn c) = translateCase (Just (translateVariableName var)) cse in

1064+ jsFunAux aux c

1065+

12731066

12741067 getTag :: SAlt -> Maybe Int

12751068 getTag (SConCase _ tag _ _ _) = Just tag

12761069 getTag _ = Nothing

12771070

1071+

12781072 lookupTableName :: String

12791073 lookupTableName = idrLTNamespace ++ translateName name

12801074

1075+

12811076 lookupTable :: [(LVar, String)] -> LVar -> [SAlt] -> JS

12821077 lookupTable aux var cases =

12831078 JSAlloc lookupTableName $ Just (

@@ -1296,16 +1091,20 @@ translateDeclaration (path, SFun name params stackSize body)

12961091 JSAssign (JSIndex (JSIdent "t") (JSNum $ JSInt tag)) fun

12971092 ) entries

12981093

1094+

12991095 lookupEntry :: [(LVar, String)] -> LVar -> SAlt -> Maybe (Int, JS)

13001096 lookupEntry aux var alt = do

13011097 tag <- getTag alt

13021098 return (tag, caseFun aux var alt)

13031099

1100+

13041101 jsDecl :: JS -> JS

13051102 jsDecl = JSAlloc (path ++ translateName name) . Just

13061103

1104+

13071105 jsFun body = jsFunAux [] body

13081106

1107+

13091108 jsFunAux :: [(LVar, String)] -> JS -> JS

13101109 jsFunAux aux body =

13111110 JSFunction (p ++ map snd aux) (

@@ -1318,17 +1117,21 @@ translateDeclaration (path, SFun name params stackSize body)

13181117 assignVar :: Int -> String -> JS

13191118 assignVar n s = JSAlloc (jsVar n) (Just $ JSIdent s)

13201119

1120+

13211121 assignAux :: (LVar, String) -> JS

13221122 assignAux (Loc var, val) =

13231123 JSAlloc (jsVar var) (Just $ JSIdent val)

13241124

1125+

13251126 p :: [String]

13261127 p = map translateName params

13271128

1129+

13281130translateVariableName :: LVar -> String

13291131translateVariableName (Loc i) =

13301132 jsVar i

13311133

1134+

13321135translateExpression :: SExp -> JS

13331136translateExpression (SLet name value body) =

13341137 jsLet (translateVariableName name) (

@@ -1504,11 +1307,12 @@ translateExpression (SOp op vars)

15041307 translateBinaryOp :: String -> LVar -> LVar -> JS

15051308 translateBinaryOp f lhs rhs = JSOp f (JSVar lhs) (JSVar rhs)

15061309

1310+

15071311 invokeMeth :: LVar -> String -> [LVar] -> JS

15081312 invokeMeth obj meth args = jsMeth (JSVar obj) meth (map JSVar args)

15091313

15101314translateExpression (SError msg) =

1511− JSError msg

1315+ jsError msg

15121316

15131317translateExpression (SForeign _ _ "putStr" [(FString, var)]) =

15141318 jsCall (idrRTNamespace ++ "print") [JSVar var]

@@ -1534,6 +1338,7 @@ translateExpression patterncase

15341338 JSCond $ map (expandCase param . translateCaseCond param) cases

15351339 )) [JSVar var]

15361340

1341+

15371342 expandCase :: String -> (Cond, JS) -> (JS, JS)

15381343 expandCase _ (RawCond cond, branch) = (cond, branch)

15391344 expandCase _ (CaseCond DefaultCase, branch) = (JSTrue , branch)

@@ -1562,14 +1367,16 @@ translateExpression (SProj var i) =

15621367translateExpression SNothing = JSNull

15631368

15641369translateExpression e =

1565− JSError $ "Not yet implemented: " ++ filter (/= '\'') (show e)

1370+ jsError $ "Not yet implemented: " ++ filter (/= '\'') (show e)

1371+

15661372

15671373data FFI = FFICode Char | FFIArg Int | FFIError String

15681374

1375+

15691376ffi :: String -> [String] -> JS

15701377ffi code args = let parsed = ffiParse code in

15711378 case ffiError parsed of

1572− Just err -> JSError err

1379+ Just err -> jsError err

15731380 Nothing -> JSRaw $ renderFFI parsed args

15741381 where

15751382 ffiParse :: String -> [FFI]

@@ -1583,11 +1390,13 @@ ffi code args = let parsed = ffiParse code in

15831390 [FFIError "Invalid positional argument"]

15841391 ffiParse (s:ss) = FFICode s : ffiParse ss

15851392

1393+

15861394 ffiError :: [FFI] -> Maybe String

15871395 ffiError [] = Nothing

15881396 ffiError ((FFIError s):xs) = Just s

15891397 ffiError (x:xs) = ffiError xs

15901398

1399+

15911400 renderFFI :: [FFI] -> [String] -> String

15921401 renderFFI [] _ = ""

15931402 renderFFI ((FFICode c) : fs) args = c : renderFFI fs args

@@ -1595,14 +1404,17 @@ ffi code args = let parsed = ffiParse code in

15951404 | i < length args && i >= 0 = args !! i ++ renderFFI fs args

15961405 | otherwise = "Argument index out of bounds"

15971406

1407+

15981408data CaseType = ConCase Int

15991409 | TypeCase JSType

16001410 | DefaultCase

16011411 deriving Eq

16021412

1413+

16031414data Cond = CaseCond CaseType

16041415 | RawCond JS

16051416

1417+

16061418translateCaseCond :: String -> SAlt -> (Cond, JS)

16071419translateCaseCond _ cse@(SDefaultCase _) =

16081420 (CaseCond DefaultCase, translateCase Nothing cse)

@@ -1630,11 +1442,12 @@ translateCaseCond var cse@(SConstCase cst _) =

16301442translateCaseCond var cse@(SConCase _ tag _ _ _) =

16311443 (CaseCond $ ConCase tag, translateCase (Just var) cse)

16321444

1445+

16331446translateCase :: Maybe String -> SAlt -> JS

1634−translateCase _ (SDefaultCase e) = translateExpression e

1635−translateCase _ (SConstCase _ e) = translateExpression e

1447+translateCase _ (SDefaultCase e) = JSReturn $ translateExpression e

1448+translateCase _ (SConstCase _ e) = JSReturn $ translateExpression e

16361449translateCase (Just var) (SConCase a _ _ vars e) =

16371450 let params = map jsVar [a .. (a + length vars)] in

1638− jsMeth (JSFunction params (JSReturn $ translateExpression e)) "apply" [

1451+ JSReturn $ jsMeth (JSFunction params (JSReturn $ translateExpression e)) "apply" [

16391452 JSThis, JSProj (JSIdent var) "vars"

16401453 ]

src/Idris/AbsSyntax.hs+27−4

@@ -407,6 +407,21 @@ getUndefined :: Idris [Name]

407407getUndefined = do i <- getIState

408408 return (map fst (idris_metavars i) \\ primDefs)

409409

410+getWidth :: Idris ConsoleWidth

411+getWidth = fmap idris_consolewidth getIState

412+

413+setWidth :: ConsoleWidth -> Idris ()

414+setWidth w = do ist <- getIState

415+ put ist { idris_consolewidth = w }

416+

417+iRender :: Doc a -> Idris (SimpleDoc a)

418+iRender d = do w <- getWidth

419+ return $ case w of

420+ InfinitelyWide -> renderPretty 1.0 1000000000 d

421+ ColsWide n -> if n < 1

422+ then renderPretty 1.0 1000000000 d

423+ else renderPretty 0.5 n d

424+

410425ihPrintResult :: Handle -> String -> Idris ()

411426ihPrintResult h s = do i <- getIState

412427 case idris_outputmode i of

@@ -420,15 +435,17 @@ ihPrintResult h s = do i <- getIState

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

421436consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

422437consoleDisplayAnnotated h output = do ist <- getIState

438+ rendered <- iRender $ output

423439 runIO . hPutStrLn h .

424− displayDecorated (consoleDecorate ist) .

425− renderCompact $ output

440+ displayDecorated (consoleDecorate ist) $

441+ rendered

442+

426443

427444-- | Write pretty-printed output to IDESlave with semantic annotations

428445ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

429446ideSlaveReturnAnnotated n h out = do ist <- getIState

430447 let (str, spans) = displaySpans .

431− renderCompact .

448+ renderPretty 0.8 80 .

432449 fmap (fancifyAnnots ist) $

433450 out

434451 good = [SymbolAtom "ok", toSExp str, toSExp spans]

@@ -451,7 +468,13 @@ ihPrintFunTypes h n overloads = do imp <- impShow

451468 RawOutput -> consoleDisplayAnnotated h output

452469 IdeSlave n -> ideSlaveReturnAnnotated n h output

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

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

471+ ppOverload imp n tm = fullName n <+> colon <+> align (prettyImp imp tm)

472+

473+ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

474+ihRenderResult h d = do ist <- getIState

475+ case idris_outputmode ist of

476+ RawOutput -> consoleDisplayAnnotated h d

477+ IdeSlave n -> ideSlaveReturnAnnotated n h d

455478

456479fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

457480fancifyAnnots ist annot@(AnnName n _ _) =

src/Idris/AbsSyntaxTree.hs+46−78

@@ -22,7 +22,7 @@ import System.IO

2222import Control.Monad.Trans.State.Strict

2323import Control.Monad.Trans.Error

2424

25−import Data.List

25+import Data.List hiding (group)

2626import Data.Char

2727import qualified Data.Map as M

2828import qualified Data.Text as T

@@ -83,6 +83,10 @@ data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord

8383-- | The output mode in use

8484data OutputMode = RawOutput | IdeSlave Integer deriving Show

8585

86+-- | How wide is the console?

87+data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

88+ | ColsWide Int -- ^ Must be positive

89+

8690-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

8791-- without typechecking).

8892-- This will include all the functions and data declarations, plus fixity declarations

@@ -144,8 +148,8 @@ data IState = IState {

144148 idris_errorhandlers :: [Name], -- ^ Global error handlers

145149 idris_nameIdx :: (Int, Ctxt (Int, Name)),

146150 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

147− module_aliases :: M.Map [T.Text] [T.Text]

148−

151+ module_aliases :: M.Map [T.Text] [T.Text],

152+ idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?

149153 }

150154

151155data SizeChange = Smaller | Same | Bigger | Unknown

@@ -215,6 +219,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

215219 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

216220 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

217221 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

222+ (ColsWide 80)

218223

219224-- | The monad for the main REPL - reading and processing files and updating

220225-- global state (hence the IO inner monad).

@@ -691,7 +696,6 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

691696deriving instance Binary PTactic'

692697deriving instance NFData PTactic'

693698!-}

694−

695699instance Sized a => Sized (PTactic' a) where

696700 size (Intro nms) = 1 + size nms

697701 size Intros = 1

@@ -1010,17 +1014,20 @@ piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

10101014

10111015-- Pretty-printing declarations and terms

10121016

1017+-- These "show" instances render to an absurdly wide screen because inserted line breaks

1018+-- could interfere with interactive editing, which calls "show".

1019+

10131020instance Show PTerm where

1014− showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm

1021+ showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp False) tm

10151022

10161023instance Show PDecl where

1017− showsPrec _ d = (displayS . renderCompact . showDeclImp False) d

1024+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp False) d

10181025

10191026instance Show PClause where

1020− showsPrec _ c = (displayS . renderCompact . showCImp True) c

1027+ showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp True) c

10211028

10221029instance Show PData where

1023− showsPrec _ d = (displayS . renderCompact . showDImp False) d

1030+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp False) d

10241031

10251032instance Pretty PTerm OutputAnnotation where

10261033 pretty = prettyImp False

@@ -1060,9 +1067,6 @@ pprintPTerm impl bnd = prettySe 10 bnd

10601067 where

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

10621069 prettySe p bnd (PQuote r) =

1063− if size r > breakingSize then

1064− text "![" <> line <> pretty r <> text "]"

1065− else

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

10671071 prettySe p bnd (PPatvar fc n) = pretty n

10681072 prettySe p bnd e

@@ -1070,35 +1074,23 @@ pprintPTerm impl bnd = prettySe 10 bnd

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

10711075 prettySe p bnd (PRef fc n) = prettyName impl bnd n

10721076 prettySe p bnd (PLam n ty sc) =

1073− bracket p 2 $

1074− if size sc > breakingSize then

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

1076− else

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

1077+ bracket p 2 . group . hang 2 $

1078+ text "\\" <> bindingOf n False <+> text "=>" <$>

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

10781080 prettySe p bnd (PLet n ty v sc) =

10791081 bracket p 2 $

1080− if size sc > breakingSize then

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

1082− nest nestingSize (prettySe 10 ((n, False):bnd) sc)

1083− else

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

1085− prettySe 10 ((n, False):bnd) sc

1082+ text "let" <+> bindingOf n False <+> text "=" </>

1083+ prettySe 10 bnd v <+> text "in" </>

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

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

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

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

1089− bracket p 2 $

1090− if size sc > breakingSize then

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

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

1093− else

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

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

1088+ bracket p 2 . group $

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

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

10961091 | otherwise =

1097− bracket p 2 $

1098− if size sc > breakingSize then

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

1100− else

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

1092+ bracket p 2 . group $

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

11021094 where

11031095 st =

11041096 case s of

@@ -1108,12 +1100,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

11081100 | impl =

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

11101102 bracket p 2 $

1111− if size sc > breakingSize then

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

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

1114− else

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

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

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

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

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

11181106 where

11191107 st =

@@ -1122,18 +1110,11 @@ pprintPTerm impl bnd = prettySe 10 bnd

11221110 _ -> empty

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

11241112 bracket p 2 $

1125− if size sc > breakingSize then

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

1127− else

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

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

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

11301115 bracket p 2 $

1131− if size sc > breakingSize then

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

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

1134− else

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

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

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

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

11371118 prettySe p bnd (PApp _ (PRef _ f) [])

11381119 | not impl = prettyName impl bnd f

11391120 prettySe p bnd (PAppBind _ (PRef _ f) [])

@@ -1143,11 +1124,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

11431124 , not (tnull nm) &&

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

11451126 let [l, r] = getExps args in

1146− bracket p 1 $

1147− if size r > breakingSize then

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

1149− else

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

1127+ bracket p 1 . align . group $

1128+ (prettySe 1 bnd l <+> prettyName impl bnd op) <$> group (prettySe 0 bnd r)

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

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

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

@@ -1155,10 +1133,14 @@ pprintPTerm impl bnd = prettySe 10 bnd

11551133 let args = getExps as

11561134 fp = prettySe 1 bnd f

11571135 in

1158− bracket p 1 $

1159− hsep (if impl

1160− then fp : map (prettyArgS bnd) as

1161− else fp : map (prettyArgSe bnd) args)

1136+ bracket p 1 . group $

1137+ if impl

1138+ then if null as

1139+ then fp

1140+ else fp <+> align (vsep (map (prettyArgS bnd) as))

1141+ else if null args

1142+ then fp

1143+ else fp <+> align (vsep (map (prettyArgSe bnd) args))

11621144 prettySe p bnd (PCase _ scr opts) =

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

11641146 where

@@ -1171,32 +1153,18 @@ pprintPTerm impl bnd = prettySe 10 bnd

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

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

11731155 prettySe p bnd (PEq _ l r) =

1174− bracket p 2 $

1175− if size r > breakingSize then

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

1177− else

1178− prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r

1156+ bracket p 2 . align . group $

1157+ prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

11791158 where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")

11801159 prettySe p bnd (PRewrite _ l r _) =

11811160 bracket p 2 $

1182− if size r > breakingSize then

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

1184− else

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

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

11861162 prettySe p bnd (PTyped l r) =

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

11881164 prettySe p bnd (PPair _ l r) =

1189− if size r > breakingSize then

1190− lparen <> prettySe 10 bnd l <> text "," <>

1191− line <> prettySe 10 bnd r <> rparen

1192− else

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

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

11941166 prettySe p bnd (PDPair _ l t r) =

1195− if size r > breakingSize then

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

1197− line <> prettySe 10 bnd r <> rparen

1198− else

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

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

12001168 prettySe p bnd (PAlternative a as) =

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

12021170 where

src/Idris/Core/ProofState.hs+6−21

@@ -115,10 +115,7 @@ instance Show ProofState where

115115

116116instance Pretty ProofState OutputAnnotation where

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

118− if size nm > breakingSize then

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

120− else

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

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

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

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

124121 let wkEnv = premises g in

@@ -128,29 +125,17 @@ instance Pretty ProofState OutputAnnotation where

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

129126 where

130127 prettyGoal ps (Guess t v) =

131− if size v > breakingSize then

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

133− nest nestingSize (prettyEnv ps v)

134− else

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

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

136129 prettyGoal ps b = prettyEnv ps $ binderTy b

137130

138131 prettyPs env [] = empty

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

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

141− if size v > breakingSize then

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

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

144− nest nestingSize (prettyPs env bs)

145− else

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

147− nest nestingSize (prettyPs env bs))

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

135+ nest nestingSize (prettyPs env bs))

148136 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) <+>

153− nest nestingSize (prettyPs env bs))

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

138+ nest nestingSize (prettyPs env bs))

154139

155140same Nothing n = True

156141same (Just x) n = x == n

src/Idris/Core/TT.hs+2−10

@@ -191,13 +191,8 @@ instance Show Err where

191191instance Pretty Err OutputAnnotation where

192192 pretty (Msg m) = text m

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

194− if size l + size r > breakingSize then

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

196− nest nestingSize (pretty l <+> text "and" <+> pretty r) <+>

197− nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

198− else

199194 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

200− nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

195+ nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

201196 pretty (ProviderError msg) = text msg

202197 pretty err@(LoadingFailed _ _) = text (show err)

203198 pretty _ = text "Error"

@@ -210,10 +205,7 @@ type TC = TC' Err

210205instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where

211206 pretty (OK ok) = pretty ok

212207 pretty (Error err) =

213− if size err > breakingSize then

214− text "Error" <+> colon <+> (nest nestingSize $ pretty err)

215− else

216− text "Error" <+> colon <+> pretty err

208+ text "Error" <+> colon <+> pretty err

217209

218210instance Show a => Show (TC a) where

219211 show (OK x) = show x

src/Idris/Parser.hs+2−2

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

561561 doc <- option "" (docComment '|')

562562 acc <- optional accessibility

563563 return (doc, acc))

564− reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name

564+ reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

565565 let n = expandNS syn n_in

566566 cs <- many carg

567567 ds <- option [] (classBlock syn)

@@ -591,7 +591,7 @@ instance_ :: SyntaxInfo -> IdrisParser [PDecl]

591591instance_ syn = do reserved "instance"; fc <- getFC

592592 en <- optional instanceName

593593 cs <- constraintList syn

594− cn <- name

594+ cn <- fnName

595595 args <- many (simpleExpr syn)

596596 let sc = PApp fc (PRef fc cn) (map pexp args)

597597 let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc

src/Idris/Prover.hs+13−10

@@ -89,18 +89,21 @@ elabStep st e = do case runStateT e st of

8989

9090dumpState :: IState -> ProofState -> Idris ()

9191dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

92− iputGoal . renderPretty 0.7 breakingSize $

93− prettyName False [] nm <> colon <+> text "No more goals."

92+ do rendered <- iRender $ prettyName False [] nm <> colon <+> text "No more goals."

93+ iputGoal rendered

9494dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

9595 let OK ty = goalAtFocus ps

9696 let OK env = envAtFocus ps

97− iputGoal . renderPretty 0.7 breakingSize $

98− prettyOtherGoals hs <> line <>

99− prettyAssumptions env <> line <>

100− prettyGoal (zip (assumptionNames env) (repeat False)) ty

97+ let state = prettyOtherGoals hs <> line <>

98+ prettyAssumptions env <> line <>

99+ prettyGoal (zip (assumptionNames env) (repeat False)) ty

100+ rendered <- iRender state

101+ iputGoal rendered

102+

101103 where

102− -- XXX

103− tPretty bnd t = pprintPTerm True bnd $ delab ist t

104+ showImplicits = opt_showimp (idris_options ist)

105+

106+ tPretty bnd t = pprintPTerm showImplicits bnd $ delab ist t

104107

105108 assumptionNames :: Env -> [Name]

106109 assumptionNames = map fst

@@ -113,14 +116,14 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = d

113116 nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>

114117 tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)

115118 prettyPs bnd ((n, b) : bs) =

116− line <> bindingOf n False <+> colon <+> tPretty bnd (binderTy b) <> prettyPs ((n, False):bnd) bs

119+ line <> bindingOf n False <+> colon <+> align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs

117120

118121 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

119122 prettyG bnd b = tPretty bnd $ binderTy b

120123

121124 prettyGoal bnd ty =

122125 text "---------- Goal: ----------" <$$>

123− bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)

126+ bindingOf h False <+> colon <+> align (prettyG bnd ty)

124127

125128 prettyAssumptions env =

126129 if length env == 0 then

src/Idris/REPL.hs+22−18

@@ -14,7 +14,7 @@ import Idris.Parser

1414import Idris.Primitives

1515import Idris.Coverage

1616import Idris.UnusedArgs

17−import Idris.Docs

17+import Idris.Docs hiding (Doc)

1818import Idris.Help

1919import Idris.Completion

2020import qualified Idris.IdeSlave as IdeSlave

@@ -30,6 +30,7 @@ import Version_idris (gitHash)

3030import Util.System

3131import Util.DynamicLinker

3232import Util.Net (listenOnLocalhost)

33+import Util.Pretty hiding ((</>))

3334

3435import Idris.Core.Evaluate

3536import Idris.Core.Execute (execute)

@@ -470,32 +471,35 @@ process h fn (Check (PRef _ n))

470471 = do ctxt <- getContext

471472 ist <- getIState

472473 imp <- impShow

473− c <- colourise

474474 case lookupNames n ctxt of

475475 ts@(t:_) ->

476476 case lookup t (idris_metavars ist) of

477− Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)

477+ Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

478+ showMetavarInfo imp ist n i

478479 Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)

479480 [] -> ihPrintError h $ "No such variable " ++ show n

480481 where

481− showMetavarInfo c imp ist n i

482+ showMetavarInfo imp ist n i

482483 = case lookupTy n (tt_ctxt ist) of

483− (ty:_) -> putTy c imp ist i (delab ist ty)

484− putTy c imp ist 0 sc = putGoal c imp ist sc

485− putTy c imp ist i (PPi _ n t sc)

486− = let current = " " ++

484+ (ty:_) -> putTy imp ist i [] (delab ist ty)

485+ putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

486+ putTy imp ist 0 bnd sc = putGoal imp ist bnd sc

487+ putTy imp ist i bnd (PPi _ n t sc)

488+ = let current = text " " <>

487489 (case n of

488− MN _ _ -> "_"

489− UN nm | ('_':'_':_) <- str nm -> "_"

490− _ -> showName (Just ist) [] False c n) ++

491− " : " ++ showTm ist t ++ "\n"

490+ MN _ _ -> text "_"

491+ UN nm | ('_':'_':_) <- str nm -> text "_"

492+ _ -> bindingOf n False) <+>

493+ colon <+> align (tPretty bnd ist t) <> line

492494 in

493− current ++ putTy c imp ist (i-1) sc

494− putTy c imp ist _ sc = putGoal c imp ist sc

495− putGoal c imp ist g

496− = "--------------------------------------\n" ++

497− showName (Just ist) [] False c n ++ " : " ++

498− showTm ist g

495+ current <> putTy imp ist (i-1) ((n,False):bnd) sc

496+ putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

497+ putGoal imp ist bnd g

498+ = text "--------------------------------------" <$>

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

500+ align (tPretty bnd ist g)

501+

502+ tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd t

499503

500504

501505process h fn (Check t)

src/Util/Pretty.hs+1−5

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

11module Util.Pretty (

22 module Text.PrettyPrint.Annotated.Leijen,

3− Sized(..), breakingSize, nestingSize,

3+ Sized(..), nestingSize,

44 Pretty(..)

55) where

@@ -17,10 +17,6 @@ instance (Sized a, Sized b) => Sized (a, b) where

1717instance Sized a => Sized [a] where

1818 size = sum . map size

1919

20−-- The maximum size before we break on to another line.

21−breakingSize :: Int

22−breakingSize = 15

23−

2420nestingSize :: Int

2521nestingSize = 1

2622