20fbc08 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' into semantic-pprint

20fbc08David Raymond Christiansen13 years ago

CHANGELOG+3

compare with master

unifiedsplit

@@ -26,6 +26,9 @@ New in 0.9.11:

26 be total, e.g "assert_total (tail (x :: xs))".

27* Terminal width is automatically detected if Idris is compiled with curses

28 support. If curses is not available, automatic mode assumes 80 columns.

29+* Changed argument order for Prelude.Either.either.

30+* Experimental 'neweffects' library, intended to replace 'effects' in the

31+ next release.

30Internal changes

33Internal changes

libs/neweffects/Effect/File.idr+1−1

@@ -12,7 +12,7 @@ openOK m False = ()

13data FileIO : Effect where

14 Open : String -> (m : Mode) ->

15− {() ==> if result then OpenFile m else ()} FileIO Bool

15+ {() ==> {res} if res then OpenFile m else ()} FileIO Bool

16 Close : {OpenFile m ==> ()} FileIO ()

18 ReadLine : {OpenFile Read} FileIO String

libs/neweffects/Effects.idr+2

@@ -22,6 +22,8 @@ class Handler (e : Effect) (m : Type -> Type) where

22-- A bit of syntactic sugar ('syntax' is not very flexible so we only go

23-- up to a small number of parameters...)

25+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]

26+ = eff inst (\b => outst)

25syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)

27syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)

26syntax "{" [inst] "}" [eff] = eff inst (\result => inst)

28syntax "{" [inst] "}" [eff] = eff inst (\result => inst)

libs/prelude/Prelude/Either.idr+4−4

@@ -29,9 +29,9 @@ choose : (b : Bool) -> Either (so b) (so (not b))

29choose True = Left oh

30choose False = Right oh

32−either : Either a b -> (a -> c) -> (b -> c) -> c

32+either : (a -> c) -> (b -> c) -> Either a b -> c

33−either (Left x) l r = l x

33+either l r (Left x) = l x

34−either (Right x) l r = r x

34+either l r (Right x) = r x

36lefts : List (Either a b) -> List a

37lefts [] = []

@@ -84,4 +84,4 @@ leftInjective refl = refl

85total rightInjective : {a : Type} -> {x : b} -> {y : b}

86 -> (Right {a = a} x = Right {a = a} y) -> (x = y)

87−rightInjective refl = refl

87+rightInjective refl = refl

mkpkg.shnew file+17

@@ -0,0 +1,17 @@

1+#!/bin/sh

3+echo "Building version-$VERSION\n\n"

4+echo "Have you: set the release flag, checked the demos and the tutorial?"

5+read $foo

7+git tag version-$VERSION -a

9+VERSION=$1

10+

11+cabal sdist

12+

13+cabal configure --prefix=/usr/local

14+cabal build

15+cabal copy --destdir=/tmp/idris-pkg/

16+pkgbuild --id org.idris-lang --root /tmp/idris-pkg/ idris-$VERSION.pkg

17+

src/IRTS/CodegenJavaScript.hs+135−134

@@ -262,6 +262,43 @@ jsError :: String -> JS

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

263

264

265+foldJS :: (JS -> a) -> (a -> a -> a) -> a -> JS -> a

266+foldJS tr add acc js =

267+ fold js

268+ where

269+ fold js

270+ | JSFunction args body <- js =

271+ add (tr js) (fold body)

272+ | JSSeq seq <- js =

273+ add (tr js) $ foldl' add acc (map fold seq)

274+ | JSReturn ret <- js =

275+ add (tr js) (fold ret)

276+ | JSApp lhs rhs <- js =

277+ add (tr js) $ add (fold lhs) (foldl' add acc $ map fold rhs)

278+ | JSNew _ args <- js =

279+ add (tr js) $ foldl' add acc $ map fold args

280+ | JSOp _ lhs rhs <- js =

281+ add (tr js) $ add (fold lhs) (fold rhs)

282+ | JSProj obj _ <- js =

283+ add (tr js) (fold obj)

284+ | JSArray vals <- js =

285+ add (tr js) $ foldl' add acc $ map fold vals

286+ | JSAssign lhs rhs <- js =

287+ add (tr js) $ add (fold lhs) (fold rhs)

288+ | JSIndex lhs rhs <- js =

289+ add (tr js) $ add (fold lhs) (fold rhs)

290+ | JSAlloc _ val <- js =

291+ add (tr js) $ fromMaybe acc $ fmap fold val

292+ | JSTernary c t f <- js =

293+ add (tr js) $ add (fold c) (add (fold t) (fold f))

294+ | JSParens val <- js =

295+ add (tr js) $ fold val

296+ | JSCond conds <- js =

297+ add (tr js) $ foldl' add acc $ map (uncurry add . (fold *** fold)) conds

298+ | otherwise =

299+ tr js

300+

301+

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

302transformJS :: (JS -> JS) -> JS -> JS

266transformJS tr js =

303transformJS tr js =

267 transformHelper js

304 transformHelper js

@@ -348,6 +385,7 @@ isJSConstant js

348 | JSChar _ <- js = True

385 | JSChar _ <- js = True

349 | JSNum _ <- js = True

386 | JSNum _ <- js = True

350 | JSType _ <- js = True

387 | JSType _ <- js = True

388+ | JSNull <- js = True

351

389

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

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

353 | otherwise = False

391 | otherwise = False

@@ -449,37 +487,11 @@ deadEvalApplyCases js =

449 map (removeHelper tags) js

487 map (removeHelper tags) js

450 where

488 where

451 getTags :: JS -> [Int]

489 getTags :: JS -> [Int]

490+ getTags = foldJS match (++) []

491+ where

492+ match js

452− getTags (JSNew "__IDRRT__Con" [JSNum (JSInt tag), args]) =

493+ | JSNew "__IDRRT__Con" [JSNum (JSInt tag), _] <- js = [tag]

453− tag : getTags args

494+ | otherwise = []

454−

455− getTags (JSNew _ args) = concatMap getTags args

456−

457− getTags (JSFunction _ body) = getTags body

458−

459− getTags (JSReturn ret) = getTags ret

460−

461− getTags (JSApp lhs rhs) = getTags lhs ++ concatMap getTags rhs

462−

463− getTags (JSSeq seq) = concatMap getTags seq

464−

465− getTags (JSOp _ lhs rhs) = getTags lhs ++ getTags rhs

466−

467− getTags (JSProj obj _) = getTags obj

468−

469− getTags (JSArray vals) = concatMap getTags vals

470−

471− getTags (JSAssign lhs rhs) = getTags lhs ++ getTags rhs

472−

473− getTags (JSAlloc _ (Just val)) = getTags val

474−

475− getTags (JSCond conds) =

476− concatMap (uncurry (++)) $ map (getTags *** getTags) conds

477−

478− getTags (JSTernary c t f) = getTags c ++ getTags t ++ getTags f

479−

480− getTags (JSParens js) = getTags js

481−

482− getTags js = []

483

495

484

496

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

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

@@ -509,36 +521,11 @@ initConstructors js =

509 map createConstant tags ++ replaceConstructors tags js

521 map createConstant tags ++ replaceConstructors tags js

510 where

522 where

511 getTags :: JS -> [Int]

523 getTags :: JS -> [Int]

524+ getTags = foldJS match (++) []

525+ where

526+ match js

512− getTags (JSNew "__IDRRT__Con" [JSNum (JSInt tag), JSArray []]) = [tag]

527+ | JSNew "__IDRRT__Con" [JSNum (JSInt tag), JSArray []] <- js = [tag]

513−

528+ | otherwise = []

514− getTags (JSNew _ args) = concatMap getTags args

515−

516− getTags (JSFunction _ body) = getTags body

517−

518− getTags (JSReturn ret) = getTags ret

519−

520− getTags (JSApp lhs rhs) = getTags lhs ++ concatMap getTags rhs

521−

522− getTags (JSSeq seq) = concatMap getTags seq

523−

524− getTags (JSOp _ lhs rhs) = getTags lhs ++ getTags rhs

525−

526− getTags (JSProj obj _) = getTags obj

527−

528− getTags (JSArray vals) = concatMap getTags vals

529−

530− getTags (JSAssign lhs rhs) = getTags lhs ++ getTags rhs

531−

532− getTags (JSAlloc _ (Just val)) = getTags val

533−

534− getTags (JSCond conds) =

535− concatMap (uncurry (++)) $ map (getTags *** getTags) conds

536−

537− getTags (JSTernary c t f) = getTags c ++ getTags t ++ getTags f

538−

539− getTags (JSParens js) = getTags js

540−

541− getTags js = []

542

529

543

530

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

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

@@ -597,91 +584,104 @@ removeIDs js =

597

584

598inlineFunctions :: [JS] -> [JS]

585inlineFunctions :: [JS] -> [JS]

599inlineFunctions js =

586inlineFunctions js =

600− let funs = collectFunctions js

587+ inlineHelper ([], js)

601− occurences = map ((id . fst) &&& countAll js) funs in

588+ where

602− removeDeadFunctions occurences js

589+ inlineHelper :: ([JS], [JS]) -> [JS]

590+ inlineHelper (front , (JSAlloc fun (Just (JSFunction args body))):back)

591+ | countAll fun front + countAll fun back == 0 =

592+ inlineHelper (front, back)

593+ | Just new <- inlineAble (

594+ countAll fun front + countAll fun back

595+ ) fun args body =

596+ let f = map (inline fun args new) in

597+ inlineHelper (f front, f back)

598+

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

600+ inlineHelper (front, []) = front

601+

602+

603+ inlineAble :: Int -> String -> [String] -> JS -> Maybe JS

604+ inlineAble 1 fun args body

605+ | nonRecur fun body =

606+ inlineAble' body

607+ where

608+ inlineAble' :: JS -> Maybe JS

609+ inlineAble' (

610+ JSReturn js@(JSNew "__IDRRT__Con" [JSNum _, JSArray vals])

611+ )

612+ | and $ map (\x -> isJSIdent x || isJSConstant x) vals = Just js

613+

614+ inlineAble' (

615+ JSReturn js@(JSNew "__IDRRT__Cont" [JSFunction [] (

616+ JSReturn (JSApp (JSIdent _) args)

617+ )])

618+ )

619+ | and $ map (\x -> isJSIdent x || isJSConstant x) args = Just js

620+

621+ inlineAble' (

622+ JSReturn js@(JSIndex (JSProj (JSApp (JSIdent _) args) "vars") _)

623+ )

624+ | and $ map (\x -> isJSIdent x || isJSConstant x) args = Just js

625+

626+ inlineAble' _ = Nothing

627+

628+ isJSIdent js

629+ | JSIdent _ <- js = True

630+ | otherwise = False

631+

632+ inlineAble _ _ _ _ = Nothing

633+

634+

635+ inline :: String -> [String] -> JS -> JS -> JS

636+ inline fun args body js = inline' js

603 where

637 where

604− removeDeadFunctions :: [(String, (Int, JS))] -> [JS] -> [JS]

638+ inline' :: JS -> JS

605− removeDeadFunctions _ [] = []

639+ inline' (JSApp (JSIdent name) vals)

606− removeDeadFunctions funOccur ((JSAlloc fun (Just (JSFunction _ _))):js)

640+ | name == fun =

607− | Just (o, _) <- lookup fun funOccur

641+ let (js, phs) = insertPlaceHolders args body in

608− , o == 0 = removeDeadFunctions funOccur js

642+ inline' $ foldr (uncurry jsSubst) js (zip phs vals)

609−

610− removeDeadFunctions funOccur (j:js) = j : removeDeadFunctions funOccur js

611−

612−

613− collectFunctions :: [JS] -> [(String, JS)]

614− collectFunctions js =

615− catMaybes $ map collectHelper js

616−

617−

618− collectHelper :: JS -> Maybe (String, JS)

619− collectHelper (JSAlloc fun (Just js@(JSFunction _ body)))

620− | fun /= "main" && nonRecur fun body = Just (fun, js)

621− collectHelper _ = Nothing

622−

623−

624− nonRecur :: String -> JS -> Bool

625− nonRecur name body = countInvokations name body == 0

626

643

644+ inline' js = transformJS inline' js

627

645

628− countAll :: [JS] -> (String, JS) -> (Int, JS)

646+ insertPlaceHolders :: [String] -> JS -> (JS, [JS])

629− countAll js (name, fun) = (sum $ map (countInvokations name) js, fun)

647+ insertPlaceHolders args body = insertPlaceHolders' args body []

630−

648+ where

631−

649+ insertPlaceHolders' :: [String] -> JS -> [JS] -> (JS, [JS])

632− countInvokations :: String -> JS -> Int

650+ insertPlaceHolders' (a:as) body ph

633− countInvokations name (JSApp (JSIdent ident) args)

651+ | (body', ph') <- insertPlaceHolders' as body ph =

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

652+ let phvar = JSIdent $ "__PH_" ++ show (length ph') in

635− | otherwise = sum $ map (countInvokations name) args

653+ (jsSubst (JSIdent a) phvar body', phvar : ph')

636−

637− countInvokations name (JSApp lhs rhs) =

638− countInvokations name lhs + (sum $ map (countInvokations name) rhs)

639−

640− countInvokations name (JSFunction _ body) =

641− countInvokations name body

642−

643− countInvokations name (JSSeq seq) =

644− sum $ map (countInvokations name) seq

645−

646− countInvokations name (JSReturn ret) =

647− countInvokations name ret

648−

649− countInvokations name (JSNew _ args) =

650− sum $ map (countInvokations name) args

651

654

652− countInvokations name (JSOp _ lhs rhs) =

655+ insertPlaceHolders' [] body ph = (body, ph)

653− countInvokations name lhs + countInvokations name rhs

654

656

655− countInvokations name (JSProj obj _) =

656− countInvokations name obj

657

658− countInvokations name (JSArray vals) =

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

659− sum $ map (countInvokations name) vals

659+ nonRecur name body = countInvokations name body == 0

660

661− countInvokations name (JSAssign _ rhs) =

662− countInvokations name rhs

663

661

664− countInvokations name (JSAlloc _ (Just js)) =

662+ countAll :: String -> [JS] -> Int

665− countInvokations name js

663+ countAll name js = sum $ map (countInvokations name) js

666

664

667− countInvokations name (JSIndex lhs rhs) =

668− countInvokations name lhs + countInvokations name rhs

669

665

670− countInvokations name (JSCond conds) =

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

671− sum $ map (uncurry (+)) (

667+ countInvokations name = foldJS match (+) 0

672− map (countInvokations name *** countInvokations name) conds

668+ where

673− )

669+ match :: JS -> Int

670+ match js

671+ | JSApp (JSIdent ident) _ <- js

672+ , name == ident = 1

673+ | otherwise = 0

674

675− countInvokations name (JSTernary c t f) =

676− sum $ [ countInvokations name c

677− , countInvokations name t

678− , countInvokations name f

679− ]

680

675

681− countInvokations name (JSParens js) =

676+reduceContinuations :: JS -> JS

682− countInvokations name js

677+reduceContinuations = transformJS reduceHelper

678+ where

679+ reduceHelper :: JS -> JS

680+ reduceHelper (JSNew "__IDRRT__Cont" [JSFunction [] (

681+ JSReturn js@(JSNew "__IDRRT__Cont" [JSFunction [] body])

682+ )]) = js

683

684− countInvokations _ _ = 0

684+ reduceHelper js = transformJS reduceHelper js

685

686

687reduceConstant :: JS -> JS

@@ -866,11 +866,12 @@ codegenJavaScript target definitions filename outputType = do

866 , initConstructors

867 , map removeAllocations

868 , elimDeadLoop

869− , inlineFunctions

870 , map elimDuplicateEvals

869 , map elimDuplicateEvals

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

870 , map (optimizeEvalTailcalls ("__IDR__mEVAL0", "__IDRRT__EVALTC"))

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

871 , map (optimizeEvalTailcalls ("__IDR__mAPPLY0", "__IDRRT__APPLYTC"))

873 , map removeInstanceChecks

872 , map removeInstanceChecks

873+ , inlineFunctions

874+ , map reduceContinuations

874 ]

875 ]

875

876

877

src/Idris/ElabTerm.hs+6−6

@@ -171,9 +171,9 @@ elab ist info pattern opts fn tm

171 -> ElabD ()

172 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

173 elab' ina PType = do apply RType []; solve

174− elab' (_,_,inty) (PConstant c)

174+-- elab' (_,_,inty) (PConstant c)

175− | constType c && pattern && not reflect && not inty

175+-- | constType c && pattern && not reflect && not inty

176− = lift $ tfail (Msg "Typecase is not allowed")

176+-- = lift $ tfail (Msg "Typecase is not allowed")

177 elab' ina (PConstant c) = do apply (RConstant c) []; solve

178 elab' ina (PQuote r) = do fill r; solve

179 elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))

@@ -245,9 +245,9 @@ elab ist info pattern opts fn tm

245 trySeq' deferr (x : xs)

246 = try' (elab' ina x) (trySeq' deferr xs) True

247 elab' ina (PPatvar fc n) | pattern = patvar n

248− elab' (_, _, inty) (PRef fc f)

248+-- elab' (_, _, inty) (PRef fc f)

249− | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty

249+-- | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty

250− = lift $ tfail (Msg "Typecase is not allowed")

250+-- = lift $ tfail (Msg "Typecase is not allowed")

251 elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)

252 = do ctxt <- get_context

253 let defined = case lookupTy n ctxt of

test/dsl002/Resimp.idr+2−2

@@ -135,9 +135,9 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

135 interp env (Lift io) k

136 = k env io

137 interp env (Check x left right) k =

138− either (envLookup x env)

139− (\a => interp (envUpdate x a env) left k)

138+ either (\a => interp (envUpdate x a env) left k)

140 (\b => interp (envUpdate x b env) right k)

139 (\b => interp (envUpdate x b env) right k)

140+ (envLookup x env)

141 interp env (While test body) k

142 = interp env test

143 (\env', result =>