git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' into sized-types
commit17a2a4855191473acb42fee36bd59f5dae3fd9b5 authorMatus Tejiscak <ziman@functor.sk> dateThu 22 Jun 2017, 13:08 (9 years ago) parent5b33b6613768b9
30 files changed+742−107
compare with master
unifiedsplit
.travis.yml+4−1 CHANGELOG.md+9−2 appveyor.yml+1−1 libs/contrib/Data/SortedMap.idr+52−1 libs/contrib/Data/SortedSet.idr+4 libs/contrib/Text/Lexer.idr+238 libs/contrib/Text/Parser.idr+229 libs/contrib/contrib.ipkg+2 libs/prelude/Prelude/Cast.idr+1−1 libs/prelude/Prelude/Nat.idr+2−5 rts/idris_gc.c+1−1 rts/idris_gmp.h+2 rts/idris_main.c+1 rts/idris_rts.c+86−42 rts/idris_rts.h+20−3 src/IRTS/CodegenC.hs+18−18 src/IRTS/JavaScript/AST.hs+8−19 src/IRTS/JavaScript/PrimOp.hs+10−3 src/Idris/Interactive.hs+5−7 stack-shell.nix+1−1 stack.yaml+1−1 test/TestData.hs+3−1 test/interactive015/expected+6 test/interactive015/input+2 test/interactive015/run+8 test/interactive015/src/interactive015.idr+4 test/interactive016/expected+7 test/interactive016/input+2 test/interactive016/run+8 test/interactive016/src/interactive016.idr+7
.travis.yml+4−1
@@ -1,3 +1,4 @@
1+dist: trusty
12sudo: false
23
34language: c
@@ -153,7 +154,9 @@ script:
153154 - echo -en 'travis_fold:end:script.tests\\r'
154155###
155156 - echo 'Benchmarks...' && echo -en 'travis_fold:start:script.benchmarks\\r'
156− - cd benchmarks && ./build.pl && ./run.pl && cd ..
157+ - if [[ "$TESTS" == "test_c" ]]; then
158+ cd benchmarks && ./build.pl && ./run.pl && cd ..;
159+ fi
157160 - echo -en 'travis_fold:end:script.benchmarks\\r'
158161###
159162# EOF
CHANGELOG.md+9−2
@@ -1,5 +1,13 @@
1+# New in 1.0.1
2+
13## Library Updates
24
5++ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries
6+ for implementing total lexical analysers and parsers.
7+
8++ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
9+ most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
10+
311+ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
412 mapping from `a` to natural numbers. For example, there is an implementation
513 `Sized (List a)` where `size = length`.
@@ -15,8 +23,7 @@
1523+ New JavaScript code generator that uses an higher level intermediate
1624 representation.
1725
18−+ Various optimizations of the novel JavaScript code generator to make
19− its results fast.
26++ Various optimizations of the new JavaScript code generator.
2027
2128+ Names are now annotated with their representations over the IDE
2229 protocol, which allows IDEs to provide commands that work on special
appveyor.yml+1−1
@@ -1,7 +1,7 @@
11version: 1.0.{build}
22init:
33- ps: >-
4− choco install cabal
4+ choco install cabal --no-progress
55
66 mkdir C:\ghc
77
libs/contrib/Data/SortedMap.idr+52−1
@@ -1,6 +1,6 @@
11module Data.SortedMap
22
3−-- TODO: write merge and split
3+-- TODO: write split
44
55private
66data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
@@ -214,6 +214,10 @@ insert k v (M _ t) =
214214 Left t' => (M _ t')
215215 Right t' => (M _ t')
216216
217+export
218+insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v
219+insertFrom = flip $ foldl $ flip $ uncurry insert
220+
217221export
218222delete : k -> SortedMap k v -> SortedMap k v
219223delete _ Empty = Empty
@@ -235,6 +239,16 @@ toList : SortedMap k v -> List (k, v)
235239toList Empty = []
236240toList (M _ t) = treeToList t
237241
242+||| Gets the keys of the map.
243+export
244+keys : SortedMap k v -> List k
245+keys = map fst . toList
246+
247+||| Gets the values of the map. Could contain duplicates.
248+export
249+values : SortedMap k v -> List v
250+values = map snd . toList
251+
238252treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
239253treeMap f (Leaf k v) = Leaf k (f v)
240254treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
@@ -245,3 +259,40 @@ export
245259implementation Functor (SortedMap k) where
246260 map _ Empty = Empty
247261 map f (M n t) = M _ (treeMap f t)
262+
263+||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
264+||| Uses the ordering of the first map given.
265+export
266+mergeWith : (v -> v -> v) -> SortedMap k v -> SortedMap k v -> SortedMap k v
267+mergeWith f x y = insertFrom inserted x where
268+ inserted : List (k, v)
269+ inserted = do
270+ (k, v) <- toList y
271+ let v' = (maybe id f $ lookup k x) v
272+ pure (k, v')
273+
274+||| Merge two maps using the Semigroup (and by extension, Monoid) operation.
275+||| Uses mergeWith internally, so the ordering of the left map is kept.
276+export
277+merge : Semigroup v => SortedMap k v -> SortedMap k v -> SortedMap k v
278+merge = mergeWith (<+>)
279+
280+||| Left-biased merge, also keeps the ordering specified by the left map.
281+export
282+mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v
283+mergeLeft = mergeWith const
284+
285+-- TODO: is this the right variant of merge to use for this? I think it is, but
286+-- I could also see the advantages of using `mergeLeft`. The current approach is
287+-- strictly more powerful I believe, because `mergeLeft` can be emulated with
288+-- the `First` monoid. However, this does require more code to do the same
289+-- thing.
290+export
291+Semigroup v => Semigroup (SortedMap k v) where
292+ (<+>) = merge
293+
294+||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
295+||| However, semantically, it should be equal.
296+export
297+(Ord k, Semigroup v) => Monoid (SortedMap k v) where
298+ neutral = empty
libs/contrib/Data/SortedSet.idr+4
@@ -60,3 +60,7 @@ Ord k => Semigroup (SortedSet k) where
6060export
6161Ord k => Monoid (SortedSet k) where
6262 neutral = empty
63+
64+export
65+keySet : SortedMap k v -> SortedSet k
66+keySet = SetWrapper . map (const ())
libs/contrib/Text/Lexer.idrnew file+238
@@ -0,0 +1,238 @@
1+module Text.Lexer
2+
3+%default total
4+
5+||| A language of token recognisers.
6+||| The `consumes` flag is True is the recogniser is guaranteed to consume
7+||| at least one character
8+export
9+data Recognise : (consumes : Bool) -> Type where
10+ Empty : Recognise False
11+ Fail : Recognise c
12+ Pred : (Char -> Bool) -> Recognise True
13+ SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
14+ SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
15+ Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)
16+
17+||| A token recogniser. Guaranteed to consume at least one character.
18+public export
19+Lexer : Type
20+Lexer = Recognise True
21+
22+public export
23+inf : Bool -> Type -> Type
24+inf True t = Inf t
25+inf False t = t
26+
27+||| Sequence two recognisers. If either consumes a character, the sequence
28+||| is guaranteed to consume a character.
29+export %inline
30+(<+>) : {c1 : Bool} ->
31+ Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
32+(<+>) {c1 = False} = SeqEmpty
33+(<+>) {c1 = True} = SeqEat
34+
35+||| Alternative recognisers. If both consume, the combination is guaranteed
36+||| to consumer a character.
37+export
38+(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
39+(<|>) = Alt
40+
41+||| Recognise a specific character
42+export
43+is : Char -> Lexer
44+is x = Pred (==x)
45+
46+||| Recognise anything but the given character
47+export
48+isNot : Char -> Lexer
49+isNot x = Pred (/=x)
50+
51+||| Recognise a sequence of at least one sub-lexers
52+export
53+some : Lexer -> Lexer
54+some l = l <+> (some l <|> Empty)
55+
56+||| Recognise a sequence of at zero or more sub-lexers. This is not
57+||| guaranteed to consume input
58+export
59+many : Lexer -> Recognise False
60+many l = some l <|> Empty
61+
62+||| Recognise any character
63+export
64+any : Lexer
65+any = Pred (const True)
66+
67+||| Recognise no input (doesn't consume any input)
68+export
69+empty : Recognise False
70+empty = Empty
71+
72+||| Recognise a character that matches a predicate
73+export
74+pred : (Char -> Bool) -> Lexer
75+pred = Pred
76+
77+||| Recognise any of the characters in the given string
78+export
79+oneOf : String -> Lexer
80+oneOf cs = pred (\x => x `elem` unpack cs)
81+
82+data StrLen : Type where
83+ MkStrLen : String -> Nat -> StrLen
84+
85+getString : StrLen -> String
86+getString (MkStrLen str n) = str
87+
88+strIndex : StrLen -> Nat -> Maybe Char
89+strIndex (MkStrLen str len) i
90+ = if i >= len then Nothing
91+ else Just (assert_total (prim__strIndex str (cast i)))
92+
93+mkStr : String -> StrLen
94+mkStr str = MkStrLen str (length str)
95+
96+strTail : Nat -> StrLen -> StrLen
97+strTail start (MkStrLen str len)
98+ = MkStrLen (substr start len str) (minus len start)
99+
100+-- If the string is recognised, returns the index at which the token
101+-- ends
102+scan : Recognise c -> Nat -> StrLen -> Maybe Nat
103+scan Empty idx str = pure idx
104+scan Fail idx str = Nothing
105+scan (Pred f) idx str
106+ = do c <- strIndex str idx
107+ if f c
108+ then Just (idx + 1)
109+ else Nothing
110+scan (SeqEat r1 r2) idx str
111+ = do idx' <- scan r1 idx str
112+ -- TODO: Can we prove totality instead by showing idx has increased?
113+ assert_total (scan r2 idx' str)
114+scan (SeqEmpty r1 r2) idx str
115+ = do idx' <- scan r1 idx str
116+ scan r2 idx' str
117+scan (Alt r1 r2) idx str
118+ = case scan r1 idx str of
119+ Nothing => scan r2 idx str
120+ Just idx => Just idx
121+
122+takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
123+takeToken lex str
124+ = do i <- scan lex 0 str -- i must be > 0 if successful
125+ pure (substr 0 i (getString str), strTail i str)
126+
127+||| Recognise a digit 0-9
128+export
129+digits : Lexer
130+digits = some (Pred isDigit)
131+
132+||| Recognise a specific string
133+export
134+exact : String -> Lexer
135+exact str with (unpack str)
136+ exact str | [] = Fail -- Not allowed, Lexer has to consume
137+ exact str | (x :: xs)
138+ = foldl SeqEmpty (is x) (map is xs)
139+
140+||| Recognise a whitespace character
141+export
142+space : Lexer
143+space = some (pred isSpace)
144+
145+||| Recognise a non-alphanumeric, non-whitespace character
146+export
147+symbol : Lexer
148+symbol = some (pred (\x => not (isAlphaNum x) && not (isSpace x)))
149+
150+strChar : Lexer
151+strChar = (is '\\' <+> any) <|> isNot '"'
152+
153+||| Recognise a string literal, including escaped characters.
154+||| (Note: doesn't yet handle escape sequences such as \123)
155+export
156+stringLit : Lexer
157+stringLit = is '"' <+> many strChar <+> is '"'
158+
159+||| Recognise a character literal, including escaped characters.
160+||| (Note: doesn't yet handle escape sequences such as \123)
161+export
162+charLit : Lexer
163+charLit = is '\'' <+> strChar <+> is '\''
164+
165+||| Recognise an integer literal (possibly with a '-' prefix)
166+export
167+intLit : Lexer
168+intLit = (is '-' <|> Empty) <+> digits
169+
170+||| A mapping from lexers to the tokens they produce.
171+||| This is a list of pairs `(Lexer, String -> tokenType)`
172+||| For each Lexer in the list, if a substring in the input matches, run
173+||| the associated function to produce a token of type `tokenType`
174+public export
175+TokenMap : (tokenType : Type) -> Type
176+TokenMap tokenType = List (Lexer, String -> tokenType)
177+
178+||| A token, and the line and column where it was in the input
179+public export
180+record TokenData a where
181+ constructor MkToken
182+ line : Int
183+ col : Int
184+ tok : a
185+
186+fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
187+fspanEnd k p "" = (k, "")
188+fspanEnd k p xxs
189+ = assert_total $
190+ let x = prim__strHead xxs
191+ xs = prim__strTail xxs in
192+ if p x then fspanEnd (S k) p xs
193+ else (k, xxs)
194+
195+-- Faster version of 'span' from the prelude (avoids unpacking)
196+export
197+fspan : (Char -> Bool) -> String -> (String, String)
198+fspan p xs
199+ = let (end, rest) = fspanEnd 0 p xs in
200+ (substr 0 end xs, rest)
201+
202+tokenise : (line : Int) -> (col : Int) ->
203+ List (TokenData a) -> TokenMap a ->
204+ StrLen -> (List (TokenData a), (Int, Int, StrLen))
205+tokenise line col acc tmap str
206+ = case getFirstToken tmap str of
207+ Just (tok, line', col', rest) =>
208+ -- assert total because getFirstToken must consume something
209+ assert_total (tokenise line' col' (tok :: acc) tmap rest)
210+ Nothing => (reverse acc, (line, col, str))
211+ where
212+ countNLs : List Char -> Nat
213+ countNLs str = List.length (filter (== '\n') str)
214+
215+ getCols : String -> Int -> Int
216+ getCols x c
217+ = case fspan (/= '\n') (reverse x) of
218+ (incol, "") => c + cast (length incol)
219+ (incol, _) => cast (length incol)
220+
221+ getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)
222+ getFirstToken [] str = Nothing
223+ getFirstToken ((lex, fn) :: ts) str
224+ = case takeToken lex str of
225+ Just (tok, rest) => Just (MkToken line col (fn tok),
226+ line + cast (countNLs (unpack tok)),
227+ getCols tok col, rest)
228+ Nothing => getFirstToken ts str
229+
230+||| Given a mapping from lexers to token generating functions (the
231+||| TokenMap a) and an input string, return a list of recognised tokens,
232+||| and the line, column, and remainder of the input at the first point in the
233+||| string where there are no recognised tokens.
234+export
235+lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
236+lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
237+ (ts, (l, c, getString str'))
238+
libs/contrib/Text/Parser.idrnew file+229
@@ -0,0 +1,229 @@
1+module Text.Parser
2+
3+%default total
4+
5+-- TODO: Add some primitives for helping with error messages.
6+-- e.g. perhaps set a string to state what we're currently trying to
7+-- parse, or to say what the next expected token is in words
8+
9+||| Description of a language's grammar. The `tok` parameter is the type
10+||| of tokens, and the `consumes` flag is True if the language is guaranteed
11+||| to be non-empty - that is, successfully parsing the language is guaranteed
12+||| to consume some input.
13+export
14+data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
15+ Empty : (val : ty) -> Grammar tok False ty
16+ Terminal : (tok -> Maybe a) -> Grammar tok True a
17+ NextIs : (tok -> Bool) -> Grammar tok False tok
18+ EOF : Grammar tok False ()
19+
20+ Fail : String -> Grammar tok c ty
21+ Commit : Grammar tok False ()
22+
23+ SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
24+ Grammar tok True b
25+ SeqEmpty : {c1, c2 : Bool} ->
26+ Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
27+ Grammar tok (c1 || c2) b
28+ Alt : {c1, c2 : Bool} ->
29+ Grammar tok c1 ty -> Grammar tok c2 ty ->
30+ Grammar tok (c1 && c2) ty
31+
32+public export
33+inf : Bool -> Type -> Type
34+inf True t = Inf t
35+inf False t = t
36+
37+||| Sequence two grammars. If either consumes some input, the sequence is
38+||| guaranteed to consume some input. If the first one consumes input, the
39+||| second is allowed to be recursive (because it means some input has been
40+||| consumed and therefore the input is smaller)
41+export %inline
42+(>>=) : {c1 : Bool} ->
43+ Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->
44+ Grammar tok (c1 || c2) b
45+(>>=) {c1 = False} = SeqEmpty
46+(>>=) {c1 = True} = SeqEat
47+
48+||| Give two alternative grammars. If both consume, the combination is
49+||| guaranteed to consume.
50+export
51+(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
52+ Grammar tok (c1 && c2) ty
53+(<|>) = Alt
54+
55+export
56+pure : (val : ty) -> Grammar tok False ty
57+pure = Empty
58+
59+||| Check whether the next token satisfies a predicate
60+export
61+nextIs : (tok -> Bool) -> Grammar tok False tok
62+nextIs = NextIs
63+
64+||| Look at the next token in the input
65+export
66+peek : Grammar tok False tok
67+peek = nextIs (const True)
68+
69+||| Succeeds if running the predicate on the next token returns Just x,
70+||| returning x. Otherwise fails.
71+export
72+terminal : (tok -> Maybe a) -> Grammar tok True a
73+terminal = Terminal
74+
75+||| Always fail with a message
76+export
77+fail : String -> Grammar tok c ty
78+fail = Fail
79+
80+||| Succeed if the input is empty
81+export
82+eof : Grammar tok False ()
83+eof = EOF
84+
85+||| Commit to an alternative; if the current branch of an alternative
86+||| fails to parse, no more branches will be tried
87+export
88+commit : Grammar tok False ()
89+commit = Commit
90+
91+data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
92+ Failure : {xs : List tok} ->
93+ (committed : Bool) ->
94+ (err : String) -> (rest : List tok) -> ParseResult xs c ty
95+ EmptyRes : (committed : Bool) ->
96+ (val : ty) -> (more : List tok) -> ParseResult more False ty
97+ NonEmptyRes : (committed : Bool) ->
98+ (val : ty) -> (more : List tok) ->
99+ ParseResult (x :: xs ++ more) c ty
100+
101+weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
102+ ParseResult xs c ty -> ParseResult xs (whatever && c) ty
103+weakenRes (Failure com msg ts) = Failure com msg ts
104+weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs
105+weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
106+weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
107+
108+shorter : (more : List tok) -> .(ys : List tok) ->
109+ LTE (S (length more)) (S (length (ys ++ more)))
110+shorter more [] = lteRefl
111+shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
112+
113+doParse : {c : Bool} ->
114+ (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
115+ ParseResult xs c ty
116+doParse com xs act with (smallerAcc xs)
117+ doParse com xs (Empty val) | sml = EmptyRes com val xs
118+ doParse com [] (Fail str) | sml = Failure com str []
119+ doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)
120+ doParse com xs Commit | sml = EmptyRes True () xs
121+
122+ doParse com [] (Terminal f) | sml = Failure com "End of input" []
123+ doParse com (x :: xs) (Terminal f) | sml
124+ = maybe
125+ (Failure com "Unrecognised token" (x :: xs))
126+ (\a => NonEmptyRes com {xs=[]} a xs)
127+ (f x)
128+ doParse com [] EOF | sml = EmptyRes com () []
129+ doParse com (x :: xs) EOF | sml
130+ = Failure com "Expected end of input" (x :: xs)
131+ doParse com [] (NextIs f) | sml = Failure com "End of input" []
132+ doParse com (x :: xs) (NextIs f) | sml
133+ = if f x
134+ then EmptyRes com x (x :: xs)
135+ else Failure com "Unrecognised token" (x :: xs)
136+ doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
137+ doParse com xs (Alt x y) | sml | Failure com' msg ts
138+ = if com' -- If the alternative had committed, don't try the
139+ -- other branch (and reset commit flag)
140+ then Failure com msg ts
141+ else weakenRes (doParse False xs y | sml)
142+ -- Successfully parsed the first option, so use the outer commit flag
143+ doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
144+ = EmptyRes com val xs
145+ doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
146+ = NonEmptyRes com val more
147+ doParse com xs (SeqEmpty act next) | (Access morerec)
148+ = case doParse com xs act | Access morerec of
149+ Failure com msg ts => Failure com msg ts
150+ EmptyRes com val xs =>
151+ case doParse com xs (next val) | (Access morerec) of
152+ Failure com' msg ts => Failure com' msg ts
153+ EmptyRes com' val xs => EmptyRes com' val xs
154+ NonEmptyRes com' val more => NonEmptyRes com' val more
155+ NonEmptyRes {x} {xs=ys} com val more =>
156+ case (doParse com more (next val) | morerec _ (shorter more ys)) of
157+ Failure com' msg ts => Failure com' msg ts
158+ EmptyRes com' val _ => NonEmptyRes com' val more
159+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
160+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
161+ NonEmptyRes com' val more'
162+ doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
163+ doParse com xs (SeqEat act next) | sml | Failure com' msg ts
164+ = Failure com' msg ts
165+ doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
166+ = case doParse com' more (next val) | morerec _ (shorter more ys) of
167+ Failure com' msg ts => Failure com' msg ts
168+ EmptyRes com' val _ => NonEmptyRes com' val more
169+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
170+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
171+ NonEmptyRes com' val more'
172+ -- This next line is not strictly necessary, but it stops the coverage
173+ -- checker taking a really long time and eating lots of memory...
174+ doParse _ _ _ | sml = Failure True "Help the coverage checker!" []
175+
176+public export
177+data ParseError tok = Error String (List tok)
178+
179+||| Parse a list of tokens according to the given grammar. If successful,
180+||| returns a pair of the parse result and the unparsed tokens (the remaining
181+||| input).
182+export
183+parse : (xs : List tok) -> (act : Grammar tok c ty) ->
184+ Either (ParseError tok) (ty, List tok)
185+parse xs act
186+ = case doParse False xs act of
187+ Failure _ msg ts => Left (Error msg ts)
188+ EmptyRes _ val rest => pure (val, rest)
189+ NonEmptyRes _ val rest => pure (val, rest)
190+
191+||| Parse one or more things
192+export
193+some : Grammar tok True a ->
194+ Grammar tok True (List a)
195+some p = do x <- p
196+ (do xs <- some p
197+ pure (x :: xs)) <|> pure [x]
198+
199+||| Parse zero or more things (may match the empty input)
200+export
201+many : Grammar tok True a ->
202+ Grammar tok False (List a)
203+many p = some p
204+ <|> pure []
205+
206+||| Parse one or more things, separated by another thing
207+export
208+sepBy1 : Grammar tok True () -> Grammar tok True a ->
209+ Grammar tok True (List a)
210+sepBy1 sep p = do x <- p
211+ (do sep
212+ xs <- sepBy1 sep p
213+ pure (x :: xs)) <|> pure [x]
214+
215+||| Parse zero or more things, separated by another thing. May
216+||| match the empty input.
217+export
218+sepBy : Grammar tok True () -> Grammar tok True a ->
219+ Grammar tok False (List a)
220+sepBy sep p = sepBy1 sep p <|> pure []
221+
222+||| Optionally parse a thing, with a default value if the grammar doesn't
223+||| match. May match the empty input.
224+export
225+optional : Grammar tok True a -> (ifNothing : a) ->
226+ Grammar tok False a
227+optional p def = p <|> pure def
228+
229+
libs/contrib/contrib.ipkg+2
@@ -30,4 +30,6 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
3030
3131 System.Concurrency.Process,
3232
33+ Text.Lexer, Text.Parser,
34+
3335 Data.Fin.Extra
libs/prelude/Prelude/Cast.idr+1−1
@@ -7,7 +7,7 @@ import public Builtins
77
88||| Interface for transforming an instance of a data type to another type.
99interface Cast from to where
10− ||| Perform a cast operation.
10+ ||| Perform a (potentially lossy!) cast operation.
1111 |||
1212 ||| @orig The original type.
1313 cast : (orig : from) -> to
libs/prelude/Prelude/Nat.idr+2−5
@@ -191,13 +191,10 @@ maximum Z m = m
191191maximum (S n) Z = S n
192192maximum (S n) (S m) = S (maximum n m)
193193
194−||| Tail recursive cast Nat to Int
194+||| Cast Nat to Int
195195||| Note that this can overflow
196196toIntNat : Nat -> Int
197−toIntNat n = toIntNat' n 0 where
198− toIntNat' : Nat -> Int -> Int
199− toIntNat' Z x = x
200− toIntNat' (S n) x = toIntNat' n (x + 1)
197+toIntNat n = prim__truncBigInt_Int (toIntegerNat n)
201198
202199(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
203200(-) m n {smaller} = minus m n
rts/idris_gc.c+1−1
@@ -24,7 +24,7 @@ VAL copy(VM* vm, VAL x) {
2424 cl = MKFLOATc(vm, x->info.f);
2525 break;
2626 case CT_STRING:
27− cl = MKSTRc(vm, x->info.str);
27+ cl = MKSTRclen(vm, x->info.str.str, x->info.str.len);
2828 break;
2929 case CT_STROFFSET:
3030 cl = MKSTROFFc(vm, x->info.str_offset);
rts/idris_gmp.h+2
@@ -7,6 +7,8 @@
77#include "mini-gmp.h"
88#endif
99
10+#include "idris_rts.h"
11+
1012// Set memory allocation functions
1113void init_gmpalloc(void);
1214
rts/idris_main.c+1
@@ -3,6 +3,7 @@
33#include "idris_rts.h"
44#include "idris_stats.h"
55
6+void _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);
67#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)
78#include <Windows.h>
89int win32_get_argv_utf8(int *argc_ptr, char ***argv_ptr)
rts/idris_rts.c+86−42
@@ -285,19 +285,27 @@ VAL MKSTR(VM* vm, const char* str) {
285285 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
286286 sizeof(char)*len, 0);
287287 SETTY(cl, CT_STRING);
288− cl -> info.str = (char*)cl + sizeof(Closure);
288+ cl->info.str.str = (char*)cl + sizeof(Closure);
289289 if (str == NULL) {
290− cl->info.str = NULL;
290+ cl->info.str.str = NULL;
291291 } else {
292− strcpy(cl -> info.str, str);
292+ strcpy(cl->info.str.str, str);
293293 }
294+ cl->info.str.len = len > 0 ? len : 0;
294295 return cl;
295296}
296297
297298char* GETSTROFF(VAL stroff) {
298299 // Assume STROFF
299300 StrOffset* root = stroff->info.str_offset;
300− return (root->str->info.str + root->offset);
301+ return (root->str->info.str.str + root->offset);
302+}
303+
304+size_t GETSTROFFLEN(VAL stroff) {
305+ // Assume STROFF
306+ // we're working in char* here so no worries about utf8 char length
307+ StrOffset* root = stroff->info.str_offset;
308+ return (root->str->info.str.len - root->offset);
301309}
302310
303311VAL MKCDATA(VM* vm, CHeapItem * item) {
@@ -342,12 +350,26 @@ VAL MKFLOATc(VM* vm, double val) {
342350}
343351
344352VAL MKSTRc(VM* vm, char* str) {
353+ int len = strlen(str);
354+
355+ Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
356+ sizeof(char)*len+1, 1);
357+ SETTY(cl, CT_STRING);
358+ cl -> info.str.str = (char*)cl + sizeof(Closure);
359+
360+ strcpy(cl->info.str.str, str);
361+ cl->info.str.len = len;
362+ return cl;
363+}
364+
365+VAL MKSTRclen(VM* vm, char* str, int len) {
345366 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
346− sizeof(char)*strlen(str)+1, 1);
367+ sizeof(char)*len+1, 1);
347368 SETTY(cl, CT_STRING);
348− cl -> info.str = (char*)cl + sizeof(Closure);
369+ cl -> info.str.str = (char*)cl + sizeof(Closure);
349370
350− strcpy(cl -> info.str, str);
371+ strcpy(cl->info.str.str, str);
372+ cl->info.str.len = len;
351373 return cl;
352374}
353375
@@ -397,6 +419,13 @@ VAL MKB64(VM* vm, uint64_t bits64) {
397419 return cl;
398420}
399421
422+void idris_trace(VM* vm, const char* func, int line) {
423+ printf("At %s:%d\n", func, line);
424+ dumpStack(vm);
425+ puts("");
426+ fflush(stdout);
427+}
428+
400429void dumpStack(VM* vm) {
401430 int i = 0;
402431 VAL* root;
@@ -404,7 +433,8 @@ void dumpStack(VM* vm) {
404433 for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {
405434 printf("%d: ", i);
406435 dumpVal(*root);
407− if (*root >= (VAL)(vm->heap.heap) && *root < (VAL)(vm->heap.end)) { printf("OK"); }
436+ if (*root >= (VAL)(vm->heap.heap) && *root < (VAL)(vm->heap.end)) { printf(" OK"); }
437+ if (root == vm->valstack_base) { printf(" <--- base"); }
408438 printf("\n");
409439 }
410440 printf("RET: ");
@@ -428,7 +458,7 @@ void dumpVal(VAL v) {
428458 printf("] ");
429459 break;
430460 case CT_STRING:
431− printf("STR[%s]", v->info.str);
461+ printf("STR[%s]", v->info.str.str);
432462 break;
433463 case CT_FWD:
434464 printf("CT_FWD ");
@@ -490,8 +520,9 @@ VAL idris_castIntStr(VM* vm, VAL i) {
490520 int x = (int) GETINT(i);
491521 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*16, 0);
492522 SETTY(cl, CT_STRING);
493− cl -> info.str = (char*)cl + sizeof(Closure);
494− sprintf(cl -> info.str, "%d", x);
523+ cl->info.str.str = (char*)cl + sizeof(Closure);
524+ sprintf(cl->info.str.str, "%d", x);
525+ cl->info.str.len = strlen(cl->info.str.str);
495526 return cl;
496527}
497528
@@ -503,32 +534,33 @@ VAL idris_castBitsStr(VM* vm, VAL i) {
503534 case CT_BITS8:
504535 // max length 8 bit unsigned int str 3 chars (256)
505536 cl = allocate(sizeof(Closure) + sizeof(char)*4, 0);
506− cl->info.str = (char*)cl + sizeof(Closure);
507− sprintf(cl->info.str, "%" PRIu8, (uint8_t)i->info.bits8);
537+ cl->info.str.str = (char*)cl + sizeof(Closure);
538+ sprintf(cl->info.str.str, "%" PRIu8, (uint8_t)i->info.bits8);
508539 break;
509540 case CT_BITS16:
510541 // max length 16 bit unsigned int str 5 chars (65,535)
511542 cl = allocate(sizeof(Closure) + sizeof(char)*6, 0);
512− cl->info.str = (char*)cl + sizeof(Closure);
513− sprintf(cl->info.str, "%" PRIu16, (uint16_t)i->info.bits16);
543+ cl->info.str.str = (char*)cl + sizeof(Closure);
544+ sprintf(cl->info.str.str, "%" PRIu16, (uint16_t)i->info.bits16);
514545 break;
515546 case CT_BITS32:
516547 // max length 32 bit unsigned int str 10 chars (4,294,967,295)
517548 cl = allocate(sizeof(Closure) + sizeof(char)*11, 0);
518− cl->info.str = (char*)cl + sizeof(Closure);
519− sprintf(cl->info.str, "%" PRIu32, (uint32_t)i->info.bits32);
549+ cl->info.str.str = (char*)cl + sizeof(Closure);
550+ sprintf(cl->info.str.str, "%" PRIu32, (uint32_t)i->info.bits32);
520551 break;
521552 case CT_BITS64:
522553 // max length 64 bit unsigned int str 20 chars (18,446,744,073,709,551,615)
523554 cl = allocate(sizeof(Closure) + sizeof(char)*21, 0);
524− cl->info.str = (char*)cl + sizeof(Closure);
525− sprintf(cl->info.str, "%" PRIu64, (uint64_t)i->info.bits64);
555+ cl->info.str.str = (char*)cl + sizeof(Closure);
556+ sprintf(cl->info.str.str, "%" PRIu64, (uint64_t)i->info.bits64);
526557 break;
527558 default:
528559 fprintf(stderr, "Fatal Error: ClosureType %d, not an integer type", ty);
529560 exit(EXIT_FAILURE);
530561 }
531562
563+ cl->info.str.len = strlen(cl->info.str.str);
532564 SETTY(cl, CT_STRING);
533565 return cl;
534566}
@@ -545,8 +577,10 @@ VAL idris_castStrInt(VM* vm, VAL i) {
545577VAL idris_castFloatStr(VM* vm, VAL i) {
546578 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);
547579 SETTY(cl, CT_STRING);
548− cl -> info.str = (char*)cl + sizeof(Closure);
549− snprintf(cl -> info.str, 32, "%.16g", GETFLOAT(i));
580+ cl->info.str.str = (char*)cl + sizeof(Closure);
581+ snprintf(cl->info.str.str, 32, "%.16g", GETFLOAT(i));
582+
583+ cl->info.str.len = strlen(cl->info.str.str);
550584 return cl;
551585}
552586
@@ -559,11 +593,13 @@ VAL idris_concat(VM* vm, VAL l, VAL r) {
559593 char *ls = GETSTR(l);
560594 // dumpVal(l);
561595 // printf("\n");
562− Closure* cl = allocate(sizeof(Closure) + strlen(ls) + strlen(rs) + 1, 0);
596+ Closure* cl = allocate(sizeof(Closure) + GETSTRLEN(l) + GETSTRLEN(r) + 1, 0);
563597 SETTY(cl, CT_STRING);
564− cl -> info.str = (char*)cl + sizeof(Closure);
565− strcpy(cl -> info.str, ls);
566− strcat(cl -> info.str, rs);
598+ cl->info.str.str = (char*)cl + sizeof(Closure);
599+ strcpy(cl->info.str.str, ls);
600+ strcat(cl->info.str.str, rs);
601+
602+ cl->info.str.len = GETSTRLEN(l) + GETSTRLEN(r);
567603 return cl;
568604}
569605
@@ -670,21 +706,26 @@ VAL idris_strTail(VM* vm, VAL str) {
670706VAL idris_strCons(VM* vm, VAL x, VAL xs) {
671707 char *xstr = GETSTR(xs);
672708 int xval = GETINT(x);
709+ int xlen = GETSTRLEN(xs);
710+
673711 if ((xval & 0x80) == 0) { // ASCII char
674712 Closure* cl = allocate(sizeof(Closure) +
675− strlen(xstr) + 2, 0);
713+ xlen + 2, 0);
676714 SETTY(cl, CT_STRING);
677− cl -> info.str = (char*)cl + sizeof(Closure);
678− cl -> info.str[0] = (char)(GETINT(x));
679− strcpy(cl -> info.str+1, xstr);
715+ cl->info.str.str = (char*)cl + sizeof(Closure);
716+ cl->info.str.str[0] = (char)(GETINT(x));
717+ strcpy(cl->info.str.str+1, xstr);
718+ cl->info.str.len = xlen + 1;
680719 return cl;
681720 } else {
682721 char *init = idris_utf8_fromChar(xval);
683− Closure* cl = allocate(sizeof(Closure) + strlen(init) + strlen(xstr) + 1, 0);
722+ int newlen = strlen(init) + xlen;
723+ Closure* cl = allocate(sizeof(Closure) + newlen + 1, 0);
684724 SETTY(cl, CT_STRING);
685− cl -> info.str = (char*)cl + sizeof(Closure);
686− strcpy(cl -> info.str, init);
687− strcat(cl -> info.str, xstr);
725+ cl->info.str.str = (char*)cl + sizeof(Closure);
726+ strcpy(cl->info.str.str, init);
727+ strcat(cl->info.str.str, xstr);
728+ cl->info.str.len = newlen;
688729 free(init);
689730 return cl;
690731 }
@@ -701,7 +742,7 @@ VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {
701742 char* str_val = GETSTR(str);
702743
703744 // If the substring is a suffix, use idris_strShift to avoid reallocating
704− if (offset_val + length_val >= strlen(str_val)) {
745+ if (offset_val + length_val >= GETSTRLEN(str)) {
705746 return idris_strShift(vm, str, offset_val);
706747 }
707748 else {
@@ -709,20 +750,23 @@ VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {
709750 char *end = idris_utf8_advance(start, length_val);
710751 Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);
711752 SETTY(newstr, CT_STRING);
712− newstr -> info.str = (char*)newstr + sizeof(Closure);
713− memcpy(newstr -> info.str, start, end - start);
714− *(newstr -> info.str + (end - start) + 1) = '\0';
753+ newstr->info.str.str = (char*)newstr + sizeof(Closure);
754+ memcpy(newstr->info.str.str, start, end - start);
755+ *(newstr->info.str.str + (end - start) + 1) = '\0';
756+ newstr->info.str.len = strlen(newstr->info.str.str);
715757 return newstr;
716758 }
717759}
718760
719761VAL idris_strRev(VM* vm, VAL str) {
720762 char *xstr = GETSTR(str);
721− Closure* cl = allocate(sizeof(Closure) +
722− strlen(xstr) + 1, 0);
763+ int xlen = GETSTRLEN(str);
764+
765+ Closure* cl = allocate(sizeof(Closure) + xlen + 1, 0);
723766 SETTY(cl, CT_STRING);
724− cl->info.str = (char*)cl + sizeof(Closure);
725− idris_utf8_rev(xstr, cl->info.str);
767+ cl->info.str.str = (char*)cl + sizeof(Closure);
768+ cl->info.str.len = xlen;
769+ idris_utf8_rev(xstr, cl->info.str.str);
726770 return cl;
727771}
728772
@@ -832,7 +876,7 @@ VAL doCopyTo(VM* vm, VAL x) {
832876 cl = MKFLOATc(vm, x->info.f);
833877 break;
834878 case CT_STRING:
835− cl = MKSTRc(vm, x->info.str);
879+ cl = MKSTRc(vm, x->info.str.str);
836880 break;
837881 case CT_BIGINT:
838882 cl = MKBIGMc(vm, x->info.ptr);
rts/idris_rts.h+20−3
@@ -42,6 +42,11 @@ typedef struct {
4242 size_t offset;
4343} StrOffset;
4444
45+typedef struct {
46+ char* str;
47+ size_t len; // Cached strlen (we do 'strlen' a lot)
48+} String;
49+
4550// A foreign pointer, managed by the idris GC
4651typedef struct {
4752 size_t size;
@@ -59,7 +64,7 @@ typedef struct Closure {
5964 con c;
6065 int i;
6166 double f;
62− char* str;
67+ String str;
6368 StrOffset* str_offset;
6469 void* ptr;
6570 uint8_t bits8;
@@ -182,7 +187,8 @@ typedef void(*func)(VM*, VAL*);
182187#define ALIGN(__p, __alignment) ((__p + __alignment - 1) & ~(__alignment - 1))
183188
184189// Retrieving values
185−#define GETSTR(x) (ISSTR(x) ? (((VAL)(x))->info.str) : GETSTROFF(x))
190+#define GETSTR(x) (ISSTR(x) ? (((VAL)(x))->info.str.str) : GETSTROFF(x))
191+#define GETSTRLEN(x) (ISSTR(x) ? (((VAL)(x))->info.str.len) : GETSTROFFLEN(x))
186192#define GETPTR(x) (((VAL)(x))->info.ptr)
187193#define GETMPTR(x) (((VAL)(x))->info.mptr->data)
188194#define GETFLOAT(x) (((VAL)(x))->info.f)
@@ -229,7 +235,15 @@ typedef intptr_t i_int;
229235
230236// Stack management
231237
232−#define INITFRAME VAL* myoldbase
238+#ifdef IDRIS_TRACE
239+#define TRACE idris_trace(vm, __FUNCTION__, __LINE__);
240+#else
241+#define TRACE
242+#endif
243+
244+#define INITFRAME TRACE\
245+ VAL* myoldbase
246+
233247#define REBASE vm->valstack_base = oldbase
234248#define RESERVE(x) if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \
235249 else { memset(vm->valstack_top, 0, (x)*sizeof(VAL)); }
@@ -255,11 +269,13 @@ VAL MKCDATA(VM* vm, CHeapItem * item);
255269VAL MKFLOATc(VM* vm, double val);
256270VAL MKSTROFFc(VM* vm, StrOffset* off);
257271VAL MKSTRc(VM* vm, char* str);
272+VAL MKSTRclen(VM* vm, char* str, int len);
258273VAL MKPTRc(VM* vm, void* ptr);
259274VAL MKMPTRc(VM* vm, void* ptr, size_t size);
260275VAL MKCDATAc(VM* vm, CHeapItem * item);
261276
262277char* GETSTROFF(VAL stroff);
278+size_t GETSTROFFLEN(VAL stroff);
263279
264280// #define SETTAG(x, a) (x)->info.c.tag = (a)
265281#define SETARG(x, i, a) ((x)->info.c.args)[i] = ((VAL)(a))
@@ -340,6 +356,7 @@ VM* idris_getSender(Msg* msg);
340356int idris_getChannel(Msg* msg);
341357void idris_freeMsg(Msg* msg);
342358
359+void idris_trace(VM* vm, const char* func, int line);
343360void dumpVal(VAL r);
344361void dumpStack(VM* vm);
345362
src/IRTS/CodegenC.hs+18−18
@@ -151,29 +151,29 @@ showCStr s = '"' : foldr ((++) . showChar) "\"" s
151151 -- Note: we need the double quotes around the codes because otherwise
152152 -- "\n3" would get encoded as "\x0a3", which is incorrect.
153153 -- Instead, we opt for "\x0a""3" and let the C compiler deal with it.
154− | ord c < 0x10 = "\"\"\\x0" ++ showHex (ord c) "\"\""
155− | ord c < 0x20 = "\"\"\\x" ++ showHex (ord c) "\"\""
154+ | ord c < 0x20 = showUTF8 (ord c)
156155 | ord c < 0x7f = [c] -- 0x7f = \DEL
157156 | otherwise = showHexes (utf8bytes (ord c))
158157
158+ showUTF8 c = "\"\"\\x" ++ pad (showHex c "") ++ "\"\""
159+ showHexes = foldr ((++) . showUTF8) ""
160+
159161 utf8bytes :: Int -> [Int]
160− utf8bytes x = let (h : bytes) = split [] x in
161− headHex h (length bytes) : map toHex bytes
162+ utf8bytes x
163+ | x <= 0x7f = [x]
164+ | x <= 0x7ff = let (y : ys) = split [] 2 x in (y .|. 0xc0) : map (.|. 0x80) ys
165+ | x <= 0xffff = let (y : ys) = split [] 3 x in (y .|. 0xe0) : map (.|. 0x80) ys
166+ | x <= 0x10ffff = let (y : ys) = split [] 4 x in (y .|. 0xf0) : map (.|. 0x80) ys
167+ | otherwise = error $ "Invalid Unicode code point U+" ++ showHex x ""
162168 where
163− split acc 0 = acc
164− split acc x = let xbits = x .&. 0x3f
165− xrest = shiftR x 6 in
166− split (xbits : acc) xrest
167−
168− headHex h 1 = h + 0xc0
169− headHex h 2 = h + 0xe0
170− headHex h 3 = h + 0xf0
171− headHex h n = error "Can't happen: Invalid UTF8 character"
172−
173− toHex i = i + 0x80
174−
175− showHexes = foldr ((++) . showUTF8) ""
176− showUTF8 c = "\"\"\\x" ++ showHex c "\"\""
169+ split acc 1 x = x : acc
170+ split acc i x = split (x .&. 0x3f : acc) (i - 1) (shiftR x 6)
171+
172+ pad :: String -> String
173+ pad s = case length s of
174+ 1 -> "0" ++ s
175+ 2 -> s
176+ _ -> error $ "Can't happen: String of invalid length " ++ show s
177177
178178bcc :: Int -> BC -> String
179179bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
src/IRTS/JavaScript/AST.hs+8−19
@@ -99,35 +99,24 @@ data JsExpr
9999
100100translateChar :: Char -> String
101101translateChar ch
102− | '\a' <- ch = "\\u0007"
103102 | '\b' <- ch = "\\b"
104103 | '\f' <- ch = "\\f"
105104 | '\n' <- ch = "\\n"
106105 | '\r' <- ch = "\\r"
107106 | '\t' <- ch = "\\t"
108107 | '\v' <- ch = "\\v"
109− | '\SO' <- ch = "\\u000E"
110− | '\DEL' <- ch = "\\u007F"
111108 | '\\' <- ch = "\\\\"
112109 | '\"' <- ch = "\\\""
113110 | '\'' <- ch = "\\\'"
114− | ch `elem` asciiTab = "\\u" ++ fill (showHex (ord ch) "")
115− | ord ch > 255 = "\\u" ++ fill (showHex (ord ch) "")
116− | otherwise = [ch]
111+ | ord ch < 0x20 = "\\x" ++ pad 2 (showHex (ord ch) "")
112+ | ord ch < 0x7f = [ch] -- 0x7f '\DEL'
113+ | ord ch <= 0xff = "\\x" ++ pad 2 (showHex (ord ch) "")
114+ | ord ch <= 0xffff = "\\u" ++ pad 4 (showHex (ord ch) "")
115+ | ord ch <= 0x10ffff = "\\u{" ++ showHex (ord ch) "}"
116+ | otherwise = error $ "Invalid Unicode code point U+" ++ showHex (ord ch) ""
117117 where
118− fill :: String -> String
119− fill s = case length s of
120− 1 -> "000" ++ s
121− 2 -> "00" ++ s
122− 3 -> "0" ++ s
123− _ -> s
124−
125− asciiTab =
126− ['\NUL', '\SOH', '\STX', '\ETX', '\EOT', '\ENQ', '\ACK', '\BEL',
127− '\BS', '\HT', '\LF', '\VT', '\FF', '\CR', '\SO', '\SI',
128− '\DLE', '\DC1', '\DC2', '\DC3', '\DC4', '\NAK', '\SYN', '\ETB',
129− '\CAN', '\EM', '\SUB', '\ESC', '\FS', '\GS', '\RS', '\US']
130−
118+ pad :: Int -> String -> String
119+ pad n s = replicate (n - length s) '0' ++ s
131120
132121indent :: Text -> Text
133122indent x =
src/IRTS/JavaScript/PrimOp.hs+10−3
@@ -28,7 +28,7 @@ import IRTS.Lang
2828data JsPrimTy = PTBool | PTAny deriving (Eq, Ord)
2929
3030type PrimF = [JsExpr] -> JsExpr
31−type PrimDec = (Bool, JsPrimTy, PrimF)
31+type PrimDec = (Bool, JsPrimTy, PrimF) -- the bool indicates if bigint library is used or not
3232
3333deriving instance Ord PrimFn
3434
@@ -177,15 +177,22 @@ primDB =
177177 , item (LZExt (ITFixed IT16) ITNative) False PTAny $ head
178178 , item (LZExt (ITFixed IT32) ITNative) False PTAny $ head
179179 , item (LZExt ITNative ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"
180+ , item (LZExt (ITFixed IT8) ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"
181+ , item (LZExt (ITFixed IT16) ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"
182+ , item (LZExt (ITFixed IT32) ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"
183+ , item (LZExt (ITFixed IT64) ITBig) True PTAny $ head
180184 , item (LTrunc ITBig ITNative) True PTAny $ JsForeign "%0.intValue()|0"
185+ , item (LTrunc ITBig (ITFixed IT8)) True PTAny $ JsForeign "%0.intValue() & 0xFF"
186+ , item (LTrunc ITBig (ITFixed IT16)) True PTAny $ JsForeign "%0.intValue() & 0xFFFF"
187+ , item (LTrunc ITBig (ITFixed IT32)) True PTAny $ JsForeign "%0.intValue() & 0xFFFFFFFF"
188+ , item (LTrunc ITBig (ITFixed IT64)) True PTAny $
189+ \[x] -> JsForeign "%0.and(new $JSRTS.jsbn.BigInteger(%1))" [x, JsStr $ show 0xFFFFFFFFFFFFFFFF]
181190 , item (LTrunc (ITFixed IT16) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"
182191 , item (LTrunc (ITFixed IT32) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"
183192 , item (LTrunc (ITFixed IT64) (ITFixed IT8)) True PTAny $ JsForeign "%0.intValue() & 0xFF"
184193 , item (LTrunc (ITFixed IT32) (ITFixed IT16)) False PTAny $ JsForeign "%0 & 0xFFFF"
185194 , item (LTrunc (ITFixed IT64) (ITFixed IT16)) True PTAny $ JsForeign "%0.intValue() & 0xFFFF"
186195 , item (LTrunc (ITFixed IT64) (ITFixed IT32)) True PTAny $ JsForeign "%0.intValue() & 0xFFFFFFFF"
187− , item (LTrunc ITBig (ITFixed IT64)) True PTAny $
188− \[x] -> JsForeign "%0.and(new $JSRTS.jsbn.BigInteger(%1))" [x, JsStr $ show 0xFFFFFFFFFFFFFFFF]
189196 , item LStrConcat False PTAny $ binop "+"
190197 , item LStrLt False PTBool $ binop "<"
191198 , item LStrEq False PTBool $ binop "=="
src/Idris/Interactive.hs+5−7
@@ -111,7 +111,7 @@ addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
111111addMissing fn updatefile l n
112112 = do src <- runIO $ readSource fn
113113 let (before, tyline : later) = splitAt (l-1) (lines src)
114− let indent = getIndent 0 (show n) tyline
114+ let indent = getIndent tyline
115115 i <- getIState
116116 cl <- getInternalApp fn l
117117 let n' = getAppName cl
@@ -124,9 +124,9 @@ addMissing fn updatefile l n
124124 if updatefile
125125 then do let fb = fn ++ "~"
126126 runIO $ writeSource fb (unlines (before ++ nonblank)
127− ++ extras ++
128− (if null extras then ""
129− else "\n" ++ unlines rest))
127+ ++ extras
128+ ++ (if null extras then "" else "\n")
129+ ++ unlines rest)
130130 runIO $ copyFile fb fn
131131 else iPrintResult extras
132132 where showPat = show . stripNS
@@ -155,9 +155,7 @@ addMissing fn updatefile l n
155155 "\n" ++ rest))
156156 showNew nm i _ [] = return ""
157157
158− getIndent i n [] = 0
159− getIndent i n xs | take (length n) xs == n = i
160− getIndent i n (x : xs) = getIndent (i + 1) n xs
158+ getIndent s = length (takeWhile isSpace s)
161159
162160
163161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
stack-shell.nix+1−1
@@ -2,7 +2,7 @@ with (import <nixpkgs> {});
22
33let
44 # MUST match resolver in stack.yaml
5− resolver = haskell.packages.lts-8_06.ghc;
5+ resolver = haskell.packages.lts-8_18.ghc;
66
77 native_libs = [
88 libffi
stack.yaml+1−1
@@ -1,4 +1,4 @@
1−resolver: lts-8.06
1+resolver: lts-8.18
22
33packages:
44 - location: .
test/TestData.hs+3−1
@@ -155,7 +155,9 @@ testFamiliesData = [
155155 ( 11, ANY ),
156156 ( 12, ANY ),
157157 ( 13, ANY ),
158− ( 14, C_CG )]),
158+ ( 14, C_CG ),
159+ ( 15, ANY ),
160+ ( 16, ANY )]),
159161 ("interfaces", "Interfaces",
160162 [ ( 1, ANY ),
161163 ( 2, ANY ),
test/interactive015/expectednew file+6
@@ -0,0 +1,6 @@
1+test (Just x) = ?Nothing_rhs_1
2+
3+test : Maybe a -> Bool
4+test Nothing = False
5+test (Just x) = ?Nothing_rhs_1
6+
test/interactive015/inputnew file+2
@@ -0,0 +1,2 @@
1+:addmissing 3 Nothing
2+:addmissing! 3 Nothing
test/interactive015/runnew file+8
@@ -0,0 +1,8 @@
1+#!/usr/bin/env bash
2+
3+cp src/interactive015.idr .
4+${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input
5+
6+cat interactive015.idr
7+
8+rm -f *.ibc interactive015.idr
test/interactive015/src/interactive015.idrnew file+4
@@ -0,0 +1,4 @@
1+
2+test : Maybe a -> Bool
3+test Nothing = False
4+
test/interactive016/expectednew file+7
@@ -0,0 +1,7 @@
1+
2+test : Maybe a -> Bool
3+test Nothing = False
4+test (Just x) = True
5+
6+other : Int
7+other = 3
test/interactive016/inputnew file+2
@@ -0,0 +1,2 @@
1+:addmissing 3 Nothing
2+:addmissing! 3 Nothing
test/interactive016/runnew file+8
@@ -0,0 +1,8 @@
1+#!/usr/bin/env bash
2+
3+cp src/interactive016.idr .
4+${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input
5+
6+cat interactive016.idr
7+
8+rm -f *.ibc interactive016.idr
test/interactive016/src/interactive016.idrnew file+7
@@ -0,0 +1,7 @@
1+
2+test : Maybe a -> Bool
3+test Nothing = False
4+test (Just x) = True
5+
6+other : Int
7+other = 3