38484ff · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

38484ffRui Barreiro9 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

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

78 incs <- mapM getInclude l

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

81+includeLibs :: [String] -> String

82+includeLibs =

83+ let

84+ repl '\\' = '_'

85+ repl '/' = '_'

86+ repl c = c

87+ in

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

89+

81isYes :: Maybe String -> Bool

90isYes :: Maybe String -> Bool

82isYes (Just "Y") = True

91isYes (Just "Y") = True

83isYes (Just "y") = True

92isYes (Just "y") = True

@@ -87,12 +96,7 @@ isYes _ = False

87codegenJs :: CGConf -> CodeGenerator

96codegenJs :: CGConf -> CodeGenerator

88codegenJs conf ci =

97codegenJs conf ci =

89 do

98 do

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

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

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

92− if debug then

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

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

95− else pure ()

96 let defs = Map.fromList $ liftDecls ci

100 let defs = Map.fromList $ liftDecls ci

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

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

98 if debug then

102 if debug then

@@ -112,15 +116,20 @@ codegenJs conf ci =

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

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

113

117

114 includes <- getIncludes $ includes ci

118 includes <- getIncludes $ includes ci

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

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

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

116 , "\"use strict\";\n\n"

121 , "\"use strict\";\n\n"

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

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

123+ -- rts

118 , runtimeCommon, "\n"

124 , runtimeCommon, "\n"

119 , extraRT, "\n"

125 , extraRT, "\n"

120 , jsbn, "\n"

126 , jsbn, "\n"

127+ -- external libraries

128+ , includes, "\n"

129+ , libs, "\n"

130+ -- user code

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

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

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

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

123− , includes, "\n"

124 , out, "\n"

133 , out, "\n"

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

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

126 , "}.call(this))"

135 , "}.call(this))"

@@ -142,6 +151,7 @@ doHiddenClasses :: Set HiddenClass -> Text

142doHiddenClasses x =

151doHiddenClasses x =

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

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

144 where

153 where

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

145 f p@(HiddenClass n id arity) =

155 f p@(HiddenClass n id arity) =

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

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

147 in jsStmt2Text $

157 in jsStmt2Text $

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

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

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

357 addUsedArgsTailCallOptim y3

367 addUsedArgsTailCallOptim y3

358 pure (preDecs, y1 `JsSeq` y2)

368 pure (preDecs, y1 `JsSeq` y2)

359− _ ->

369+ _ -> do

360− do

370+ app <- formApp fn argVals

361− argsFn <- getArgList fn

362− case argsFn of

363− Nothing -> do

364− fn' <- cgName fn

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

366− Just agFn ->

367− do

368− let lenAgFn = length agFn

369− let lenArgs = length args

370− case compare lenAgFn lenArgs of

371− EQ ->

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

371+ pure (preDecs, addRT rt app)

373− LT ->

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

375− GT ->

376− do

377− let part = Partial fn lenArgs lenAgFn

378− addPartial part

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

380

372

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

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

382cgBody' rt (LLazyApp n args) =

374cgBody' rt (LLazyApp n args) =

@@ -454,18 +446,36 @@ altHasNoProj :: LAlt -> Bool

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

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

455altHasNoProj _ = True

447altHasNoProj _ = True

456

448

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

450+formApp fn argVals = case specialCall fn of

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

452+ _ -> do

453+ argsFn <- getArgList fn

454+ fname <- cgName fn

455+ case argsFn of

456+ Nothing -> pure $ jsCurryApp fname argVals

457+ Just agFn -> do

458+ let lenAgFn = length agFn

459+ let lenArgs = length argVals

460+ case compare lenAgFn lenArgs of

461+ EQ -> pure $ JsApp fname argVals

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

463+ GT -> do

464+ let part = Partial fn lenArgs lenAgFn

465+ addPartial part

466+ pure $ jsAppN (jsNamePartial part) argVals

467+

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

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

458formCon n args = do

469formCon n args = do

459 case specialCased n of

470 case specialCased n of

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

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

461 Nothing -> do

472 Nothing -> do

462 (conId, arity) <- getConsId n

473 (conId, arity) <- getConsId n

463− if (arity > 0)

464− then do

465− let hc = HiddenClass n conId arity

474+ let hc = HiddenClass n conId arity

466− addHiddenClass hc

475+ addHiddenClass hc

476+ pure $ if (arity > 0)

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

477+ then JsNew (JsVar $ jsNameHiddenClass hc) args

468− else pure $ JsInt conId

478+ else JsVar $ jsNameHiddenClass hc

469

479

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

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

471formConTest n x = do

481formConTest n x = do

@@ -473,9 +483,10 @@ formConTest n x = do

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

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

474 Nothing -> do

484 Nothing -> do

475 (conId, arity) <- getConsId n

485 (conId, arity) <- getConsId n

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

476− if (arity > 0)

487+ -- if (arity > 0)

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

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

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

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

479

490

480formProj :: Name -> JsExpr -> Int -> JsExpr

491formProj :: Name -> JsExpr -> Int -> JsExpr

481formProj n v i =

492formProj 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