1122194 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

1122194Edmund Smith9 years ago

CHANGELOG.md+7−4

compare with master

unifiedsplit

@@ -1,13 +1,16 @@

2## Tool Updates

4−+ New javascript code generator that uses an higher level intermediate

4++ New JavaScript code generator that uses an higher level intermediate

5 representation.

6−

7++ Various optimizations of the novel JavaScript code generator to make

8+ its results fast.

7+ Names are now annotated with their representations over the IDE

10+ Names are now annotated with their representations over the IDE

8 protocol, which allows IDEs to provide commands that work on special

11 protocol, which allows IDEs to provide commands that work on special

9− names that don't have syntax, such as case block names

12+ names that don't have syntax, such as case block names.

10−

13+

12# New in 1.0

15# New in 1.0

docs/tutorial/miscellany.rst+28−1

@@ -14,7 +14,7 @@ In this section we discuss a variety of additional features:

14+ code generation; and

15+ the universe hierarchy.

17−Auto implicit arguments

17+Implicit arguments

18=======================

20We have already seen implicit arguments, which allows arguments to be

@@ -23,6 +23,9 @@ omitted when they can be inferred by the type checker, e.g.

23.. code-block:: idris

25 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

26+

27+Auto implicit arguments

28+------------------------

27In other situations, it may be possible to infer arguments not by type

30In other situations, it may be possible to infer arguments not by type

28checking but by searching the context for an appropriate value, or

31checking but by searching the context for an appropriate value, or

@@ -66,6 +69,30 @@ In the case that a proof is not found, it can be provided explicitly as normal:

66.. code-block:: idris

69.. code-block:: idris

68 head xs {p = ?headProof}

71 head xs {p = ?headProof}

72+

73+Default implicit arguments

74+---------------------------

75+

76+Besides having Idris automatically find a value of a given type, sometimes we

77+want to have an implicit argument with a specific default value. In Idris, we can

78+do this using the ``default`` annotation. While this is primarily intended to assist

79+in automatically constructing a proof where auto fails, or finds an unhelpful value,

80+it might be easier to first consider a simpler case, not involving proofs.

81+

82+If we want to compute the n'th fibonacci number (and defining the 0th fibonacci

83+number as 0), we could write:

84+

85+.. code-block:: idris

86+

87+ fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat

88+ fibonacci {lag} Z = lag

89+ fibonacci {lag} {lead} (S Z) = fibonacci {lag=lead} {lead=lag+lead} n

90+

91+After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,

92+and will return the 5th fibonacci number. Note that while this works, this is not the

93+intended use of the ``default`` annotation. It is included here for illustrative purposes

94+only. Usually, ``default`` is used to provide things like a custom proof search script.

95+

70Implicit conversions

97Implicit conversions

71====================

98====================

libs/base/Data/Bits.idr+9−4

@@ -19,8 +19,8 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)

19 l2x = log2NZ (S x) SIsNotZ

21||| Gets the lowest n for which "8 * 2 ^ n" is larger than or equal to the input.

22−||| For example, `nextBytes 10 = 16`.

22+||| For example, `nextBytes 10 = 1`.

23−||| Like with nextPow2, the result is not rounded up, so `nextBytes 16 = 16`.

23+||| Like with nextPow2, the result is not rounded up, so `nextBytes 16 = 1`.

24public export

25nextBytes : Nat -> Nat

26nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))

@@ -368,6 +368,7 @@ complement' {n=n} x with (nextBytes n)

368 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad

369 | _ = assert_unreachable

370

371+||| Reverse all the bits in the argument.

371complement : %static {n : Nat} -> Bits n -> Bits n

372complement : %static {n : Nat} -> Bits n -> Bits n

372complement (MkBits x) = MkBits (complement' x)

373complement (MkBits x) = MkBits (complement' x)

373

374

@@ -386,6 +387,7 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

386 | (S (S (S _)), S (S (S _))) = believe_me x

387 | (S (S (S _)), S (S (S _))) = believe_me x

387 | _ = assert_unreachable

388 | _ = assert_unreachable

388

389

390+||| Extend the bitstring with zeros, leaving the first n bits unchanged.

389zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)

391zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)

390zeroExtend (MkBits x) = MkBits (zext' x)

392zeroExtend (MkBits x) = MkBits (zext' x)

391

393

@@ -418,7 +420,7 @@ bitsToInt' {n=n} x with (nextBytes n)

418bitsToInt : %static {n : Nat} -> Bits n -> Integer

420bitsToInt : %static {n : Nat} -> Bits n -> Integer

419bitsToInt (MkBits x) = bitsToInt' x

421bitsToInt (MkBits x) = bitsToInt' x

420

422

421−-- Zero out the high bits of a truncated bitstring

423+||| Zero out the high bits of a truncated bitstring

422zeroUnused : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)

424zeroUnused : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)

423zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)

425zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)

424

426

@@ -474,10 +476,13 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))

474 | (S (S (S _)), S (S (S _))) = believe_me x

476 | (S (S (S _)), S (S (S _))) = believe_me x

475 | _ = assert_unreachable

477 | _ = assert_unreachable

476

478

479+||| Truncate the high bits of a bitstring.

477truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n

480truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n

478truncate (MkBits x) = MkBits (zeroUnused (trunc' x))

481truncate (MkBits x) = MkBits (zeroUnused (trunc' x))

479

482

483+||| Create a bitstring of length n with the bit given as an argument set to one

484+||| and all other bits set to zero.

480−bitAt : %static {n : Nat} -> Fin n -> Bits n

485+bitAt : %static {n : Nat} -> (at : Fin n) -> Bits n

481bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)

486bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)

482

487

483getBit : %static {n : Nat} -> Fin n -> Bits n -> Bool

488getBit : %static {n : Nat} -> Fin n -> Bits n -> Bool

libs/contrib/Data/SortedSet.idr+3

@@ -29,6 +29,7 @@ export

29toList : SortedSet k -> List k

30toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)

32+export

32Foldable SortedSet where

33Foldable SortedSet where

33 foldr f e xs = foldr f e (Data.SortedSet.toList xs)

34 foldr f e xs = foldr f e (Data.SortedSet.toList xs)

@@ -52,8 +53,10 @@ export

52intersection : (x, y : SortedSet k) -> SortedSet k

53intersection : (x, y : SortedSet k) -> SortedSet k

53intersection x y = difference x (difference x y)

54intersection x y = difference x (difference x y)

56+export

55Ord k => Semigroup (SortedSet k) where

57Ord k => Semigroup (SortedSet k) where

56 (<+>) = union

58 (<+>) = union

60+export

58Ord k => Monoid (SortedSet k) where

61Ord k => Monoid (SortedSet k) where

59 neutral = empty

62 neutral = empty

src/IRTS/JavaScript/Codegen.hs+47−36

@@ -71,6 +71,15 @@ getIncludes l = do

71 incs <- mapM getInclude l

72 return $ T.intercalate "\n\n" incs

74+includeLibs :: [String] -> String

75+includeLibs =

76+ let

77+ repl '\\' = '_'

78+ repl '/' = '_'

79+ repl c = c

80+ in

81+ concatMap (\lib -> "var " ++ (repl <$> lib) ++ " = require(\"" ++ lib ++"\");\n")

82+

74isYes :: Maybe String -> Bool

83isYes :: Maybe String -> Bool

75isYes (Just "Y") = True

84isYes (Just "Y") = True

76isYes (Just "y") = True

85isYes (Just "y") = True

@@ -80,12 +89,7 @@ isYes _ = False

80codegenJs :: CGConf -> CodeGenerator

89codegenJs :: CGConf -> CodeGenerator

81codegenJs conf ci =

90codegenJs conf ci =

82 do

91 do

83− optim <- isYes <$> lookupEnv "IDRISJS_OPTIM"

84 debug <- isYes <$> lookupEnv "IDRISJS_DEBUG"

92 debug <- isYes <$> lookupEnv "IDRISJS_DEBUG"

85− if debug then

86− if optim then putStrLn "compiling width idris-js optimizations"

87− else putStrLn "compiling widthout idris-js optimizations"

88− else pure ()

89 let defs = Map.fromList $ liftDecls ci

93 let defs = Map.fromList $ liftDecls ci

90 let used = Map.elems $ removeDeadCode defs [sMN 0 "runMain"]

94 let used = Map.elems $ removeDeadCode defs [sMN 0 "runMain"]

91 if debug then

95 if debug then

@@ -105,15 +109,20 @@ codegenJs conf ci =

105 extraRT <- TIO.readFile $ path </> (extraRunTime conf)

109 extraRT <- TIO.readFile $ path </> (extraRunTime conf)

106

110

107 includes <- getIncludes $ includes ci

111 includes <- getIncludes $ includes ci

112+ let libs = T.pack $ includeLibs $ compileLibs ci

108 TIO.writeFile (outputFile ci) $ T.concat [ header conf

113 TIO.writeFile (outputFile ci) $ T.concat [ header conf

109 , "\"use strict\";\n\n"

114 , "\"use strict\";\n\n"

110 , "(function(){\n\n"

115 , "(function(){\n\n"

116+ -- rts

111 , runtimeCommon, "\n"

117 , runtimeCommon, "\n"

112 , extraRT, "\n"

118 , extraRT, "\n"

113 , jsbn, "\n"

119 , jsbn, "\n"

120+ -- external libraries

121+ , includes, "\n"

122+ , libs, "\n"

123+ -- user code

114 , doPartials (partialApplications stats), "\n"

124 , doPartials (partialApplications stats), "\n"

115 , doHiddenClasses (hiddenClasses stats), "\n"

125 , doHiddenClasses (hiddenClasses stats), "\n"

116− , includes, "\n"

117 , out, "\n"

126 , out, "\n"

118 , jsName (sMN 0 "runMain"), "();\n"

127 , jsName (sMN 0 "runMain"), "();\n"

119 , "}.call(this))"

128 , "}.call(this))"

@@ -135,6 +144,7 @@ doHiddenClasses :: Set HiddenClass -> Text

135doHiddenClasses x =

144doHiddenClasses x =

136 T.intercalate "\n" (map f $ Set.toList x)

145 T.intercalate "\n" (map f $ Set.toList x)

137 where

146 where

147+ f p@(HiddenClass n id 0) = jsStmt2Text $ JsDecConst (jsNameHiddenClass p) $ JsObj [("type", JsInt id)]

138 f p@(HiddenClass n id arity) =

148 f p@(HiddenClass n id arity) =

139 let vars = map dataPartName $ take arity [1..]

149 let vars = map dataPartName $ take arity [1..]

140 in jsStmt2Text $

150 in jsStmt2Text $

@@ -349,27 +359,9 @@ cgBody' rt (LApp tailcall (LV (Glob fn)) args) =

349 let ((y1,y2), y3) = tailCallOptimRefreshArgs (zip argN argVals) Set.empty

359 let ((y1,y2), y3) = tailCallOptimRefreshArgs (zip argN argVals) Set.empty

350 addUsedArgsTailCallOptim y3

360 addUsedArgsTailCallOptim y3

351 pure (preDecs, y1 `JsSeq` y2)

361 pure (preDecs, y1 `JsSeq` y2)

352− _ ->

362+ _ -> do

353− do

363+ app <- formApp fn argVals

354− argsFn <- getArgList fn

355− case argsFn of

356− Nothing -> do

357− fn' <- cgName fn

358− pure (preDecs, addRT rt $ jsCurryApp fn' argVals )

359− Just agFn ->

360− do

361− let lenAgFn = length agFn

362− let lenArgs = length args

363− case compare lenAgFn lenArgs of

364− EQ ->

365− pure (preDecs, addRT rt $ jsAppN fname argVals)

364+ pure (preDecs, addRT rt app)

366− LT ->

367− pure (preDecs, addRT rt $ jsCurryApp (jsAppN fname (take lenAgFn argVals)) (drop lenAgFn argVals) )

368− GT ->

369− do

370− let part = Partial fn lenArgs lenAgFn

371− addPartial part

372− pure (preDecs, addRT rt $ jsAppN (jsNamePartial part) argVals )

373

365

374cgBody' rt (LForce (LLazyApp n args)) = cgBody rt (LApp False (LV (Glob n)) args)

366cgBody' rt (LForce (LLazyApp n args)) = cgBody rt (LApp False (LV (Glob n)) args)

375cgBody' rt (LLazyApp n args) =

367cgBody' rt (LLazyApp n args) =

@@ -447,18 +439,36 @@ altHasNoProj :: LAlt -> Bool

447altHasNoProj (LConCase _ _ args _) = args == []

439altHasNoProj (LConCase _ _ args _) = args == []

448altHasNoProj _ = True

440altHasNoProj _ = True

449

441

442+formApp :: Name -> [JsExpr] -> State CGBodyState JsExpr

443+formApp fn argVals = case specialCall fn of

444+ Just (arity, g) | arity == length argVals -> pure $ g argVals

445+ _ -> do

446+ argsFn <- getArgList fn

447+ fname <- cgName fn

448+ case argsFn of

449+ Nothing -> pure $ jsCurryApp fname argVals

450+ Just agFn -> do

451+ let lenAgFn = length agFn

452+ let lenArgs = length argVals

453+ case compare lenAgFn lenArgs of

454+ EQ -> pure $ JsApp fname argVals

455+ LT -> pure $ jsCurryApp (JsApp fname (take lenAgFn argVals)) (drop lenAgFn argVals)

456+ GT -> do

457+ let part = Partial fn lenArgs lenAgFn

458+ addPartial part

459+ pure $ jsAppN (jsNamePartial part) argVals

460+

450formCon :: Name -> [JsExpr] -> State CGBodyState JsExpr

461formCon :: Name -> [JsExpr] -> State CGBodyState JsExpr

451formCon n args = do

462formCon n args = do

452 case specialCased n of

463 case specialCased n of

453 Just (ctor, test, match) -> pure $ ctor args

464 Just (ctor, test, match) -> pure $ ctor args

454 Nothing -> do

465 Nothing -> do

455 (conId, arity) <- getConsId n

466 (conId, arity) <- getConsId n

456− if (arity > 0)

457− then do

458− let hc = HiddenClass n conId arity

467+ let hc = HiddenClass n conId arity

459− addHiddenClass hc

468+ addHiddenClass hc

469+ pure $ if (arity > 0)

460− pure $ JsNew (JsVar $ jsNameHiddenClass hc) args

470+ then JsNew (JsVar $ jsNameHiddenClass hc) args

461− else pure $ JsInt conId

471+ else JsVar $ jsNameHiddenClass hc

462

472

463formConTest :: Name -> JsExpr -> State CGBodyState JsExpr

473formConTest :: Name -> JsExpr -> State CGBodyState JsExpr

464formConTest n x = do

474formConTest n x = do

@@ -466,9 +476,10 @@ formConTest n x = do

466 Just (ctor, test, match) -> pure $ test x

476 Just (ctor, test, match) -> pure $ test x

467 Nothing -> do

477 Nothing -> do

468 (conId, arity) <- getConsId n

478 (conId, arity) <- getConsId n

479+ pure $ JsBinOp "===" (JsProp x (T.pack "type")) (JsInt conId)

469− if (arity > 0)

480+ -- if (arity > 0)

470− then pure $ JsBinOp "===" (JsProp x (T.pack "type")) (JsInt conId)

481+ -- then pure $ JsBinOp "===" (JsProp x (T.pack "type")) (JsInt conId)

471− else pure $ JsBinOp "===" x (JsInt conId)

482+ -- else pure $ JsBinOp "===" x (JsInt conId)

472

483

473formProj :: Name -> JsExpr -> Int -> JsExpr

484formProj :: Name -> JsExpr -> Int -> JsExpr

474formProj n v i =

485formProj n v i =

src/IRTS/JavaScript/PrimOp.hs+5−5

@@ -37,7 +37,7 @@ primDB =

37 Map.fromList [

38 item (LPlus ATFloat) False PTAny $ binop "+"

39 , item (LPlus (ATInt ITChar)) False PTAny $ JsForeign "String.fromCharCode(%0.charCodeAt(0) + %1.charCodeAt(0))"

40− , item (LPlus (ATInt ITNative)) False PTAny $ JsForeign "%0+%1|0"

40+ , item (LPlus (ATInt ITNative)) False PTAny $ binop "+"

41 , item (LPlus (ATInt (ITFixed IT8))) False PTAny $ JsForeign "%0 + %1 & 0xFF"

42 , item (LPlus (ATInt (ITFixed IT16))) False PTAny $ JsForeign "%0 + %1 & 0xFFFF"

43 , item (LPlus (ATInt (ITFixed IT32))) False PTAny $ JsForeign "%0+%1|0"

@@ -46,7 +46,7 @@ primDB =

46 \[l, r] -> JsForeign "%0.add(%1).and(new $JSRTS.jsbn.BigInteger(%2))" [l,r, JsStr $ show 0xFFFFFFFFFFFFFFFF]

47 , item (LMinus ATFloat) False PTAny $ binop "-"

48 , item (LMinus (ATInt ITChar)) False PTAny $ JsForeign "String.fromCharCode(%0.charCodeAt(0) - %1.charCodeAt(0))"

49− , item (LMinus (ATInt ITNative)) False PTAny $ JsForeign "%0-%1|0"

49+ , item (LMinus (ATInt ITNative)) False PTAny $ binop "-"

50 , item (LMinus (ATInt (ITFixed IT8))) False PTAny $ JsForeign "%0 - %1 & 0xFF"

51 , item (LMinus (ATInt (ITFixed IT16))) False PTAny $ JsForeign "%0 - %1 & 0xFFFF"

52 , item (LMinus (ATInt (ITFixed IT32))) False PTAny $ JsForeign "%0-%1|0"

@@ -55,7 +55,7 @@ primDB =

55 \[l, r] -> JsForeign "%0.subtract(%1).and(new $JSRTS.jsbn.BigInteger(%2))" [l,r, JsStr $ show 0xFFFFFFFFFFFFFFFF]

56 , item (LTimes ATFloat) False PTAny $ binop "*"

57 , item (LTimes (ATInt ITChar)) False PTAny $ JsForeign "String.fromCharCode(%0.charCodeAt(0) * %1.charCodeAt(0))"

58− , item (LTimes (ATInt ITNative)) False PTAny $ JsForeign "%0*%1|0"

58+ , item (LTimes (ATInt ITNative)) False PTAny $ binop "*"

59 , item (LTimes (ATInt (ITFixed IT8))) False PTAny $ JsForeign "%0 * %1 & 0xFF"

60 , item (LTimes (ATInt (ITFixed IT16))) False PTAny $ JsForeign "%0 * %1 & 0xFFFF"

61 , item (LTimes (ATInt (ITFixed IT32))) False PTAny $ JsForeign "%0*%1|0"

@@ -71,14 +71,14 @@ primDB =

71 , item (LSDiv (ATInt (ITFixed IT16))) False PTAny $ JsForeign "%0 / %1"

72 , item (LSDiv (ATInt (ITFixed IT32))) False PTAny $ JsForeign "%0 / %1 |0"

73 , item (LSDiv (ATInt (ITFixed IT64))) True PTAny $ JsForeign "%0.divide(%1)"

74− , item (LSDiv (ATInt ITNative)) False PTAny $ JsForeign "%0/%1|0"

74+ , item (LSDiv (ATInt ITNative)) False PTAny $ JsForeign "%0/%1|0" -- we need "|0" in this

75 , item (LSDiv (ATInt ITBig)) True PTAny $ method "divide"

76 , item (LURem (ITFixed IT8)) False PTAny $ JsForeign "%0 % %1"

77 , item (LURem (ITFixed IT16)) False PTAny $ JsForeign "%0 % %1"

78 , item (LURem (ITFixed IT32)) False PTAny $ JsForeign "(%0>>>0) % (%1>>>0) |0"

79 , item (LURem (ITFixed IT64)) True PTAny $ method "remainder"

80 , item (LSRem ATFloat) False PTAny $ binop "%"

81− , item (LSRem (ATInt ITNative)) False PTAny $ JsForeign "%0 % %1 |0"

81+ , item (LSRem (ATInt ITNative)) False PTAny $ binop "%"

82 , item (LSRem (ATInt (ITFixed IT8))) False PTAny $ JsForeign "%0 % %1"

83 , item (LSRem (ATInt (ITFixed IT16))) False PTAny $ JsForeign "%0 % %1"

84 , item (LSRem (ATInt (ITFixed IT32))) False PTAny $ JsForeign "%0 % %1 |0"

test/README.md+1−1

@@ -132,7 +132,7 @@ for the compatible backends are:

132

133- `ANY`: choose this if your test will work with any code generator

134- `C_CG`: choose this to only test against the C code generator

135−- `JS_CG`: choose this to only test against the Node code generator

135+- `NODE_CG`: choose this to only test against the Node code generator

136- `NONE`: choose this if you don't want your test to be run with multiple code

137generators (mainly for tests that only perform type checking)

138

test/TestData.hs+1

@@ -127,6 +127,7 @@ testFamiliesData = [

127 , ( 7, C_CG )

128 , ( 8, C_CG )

129 , ( 9, C_CG )

130+ , ( 10, NODE_CG )

130 ]),

131 ]),

131 ("folding", "Folding",

132 ("folding", "Folding",

132 [ ( 1, ANY )]),

133 [ ( 1, ANY )]),

test/ffi010/expectednew file+3

@@ -0,0 +1,3 @@

1+start

2+olare

3+end

test/ffi010/ffi010.idrnew file+43

@@ -0,0 +1,43 @@

2+%inline

3+public export

4+jscall : (fname : String) -> (ty : Type) ->

5+ {auto fty : FTy FFI_JS [] ty} -> ty

6+jscall fname ty = foreign FFI_JS fname ty

8+export

9+data ServiceM : Type -> Type where

10+ PureServ : a -> ServiceM a

11+

12+

13+get_jsio : ServiceM a -> JS_IO (Either String a)

14+get_jsio (PureServ x) = do

15+ pure $ Right x

16+

17+export

18+mytst : String -> ServiceM String

19+mytst x = PureServ $ "end"

20+

21+call_fn : (String -> JS_IO String) -> String -> JS_IO String

22+call_fn f x = jscall

23+ "%0(%1)"

24+ ((JsFn (String -> JS_IO String)) -> String -> JS_IO String)

25+ (MkJsFn f)

26+ x

27+

28+mytstJs : String -> JS_IO String

29+mytstJs x = do

30+ r <- get_jsio $ mytst "arst"

31+ case r of

32+ Right k => pure k

33+

34+tst2 : JS_IO String

35+tst2 = call_fn mytstJs "inputmytst"

36+

37+export

38+main : JS_IO ()

39+main = do

40+ putStrLn' "start"

41+ r <- tst2

42+ putStrLn' "olare"

43+ putStrLn' r

test/ffi010/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ ffi010.idr -o ffi010

3+./ffi010

4+rm -f ffi010 *.ibc