on master help sign in
Merge branch 'master' into cabal_stuff
commit5c6c22f8a6c994a7a8e454f8631772859207ff87 authorNiklas Larsson <metaniklas@gmail.com> dateTue 1 Aug 2017, 16:30 (9 years ago) parent596987270f172c
59 files changed+1031−168
CHANGELOG.md+4−1 idris.cabal+8−10 libs/contrib/Text/PrettyPrint/WL.idr+18 libs/contrib/Text/PrettyPrint/WL/Characters.idr+103 libs/contrib/Text/PrettyPrint/WL/Combinators.idr+259 libs/contrib/Text/PrettyPrint/WL/Core.idr+225 libs/contrib/contrib.ipkg+5 scripts/runidris+18 scripts/runidris-node+18 src/IRTS/CodegenC.hs+234−115 src/IRTS/Compiler.hs+1−1 src/IRTS/Defunctionalise.hs+1−1 src/IRTS/Lang.hs+2−1 src/IRTS/Portable.hs+1−1 src/IRTS/Simplified.hs+1 src/Idris/AbsSyntax.hs+1−1 src/Idris/AbsSyntaxTree.hs+10−1 src/Idris/Apropos.hs+1 src/Idris/CaseSplit.hs+1−1 src/Idris/Chaser.hs+2 src/Idris/Core/Binary.hs+2 src/Idris/Core/CaseTree.hs+2−2 src/Idris/Core/DeepSeq.hs+2−1 src/Idris/Core/ProofState.hs+2−1 src/Idris/Core/TT.hs+4−2 src/Idris/Core/Typecheck.hs+2−2 src/Idris/Core/Unify.hs+1−1 src/Idris/Core/WHNF.hs+1−1 src/Idris/Coverage.hs+1−1 src/Idris/DSL.hs+2 src/Idris/DataOpts.hs+1−1 src/Idris/Docstrings.hs+2−1 src/Idris/Elab/Quasiquote.hs+1 src/Idris/Elab/Utils.hs+7−6 src/Idris/Error.hs+1 src/Idris/IBC.hs+9−2 src/Idris/IdrisDoc.hs+1 src/Idris/Output.hs+1 src/Idris/Package/Parser.hs+1−1 src/Idris/Parser.hs+7−2 src/Idris/Parser/Expr.hs+7 src/Idris/Parser/Helpers.hs+3−2 src/Idris/Parser/Ops.hs+2−1 src/Idris/PartialEval.hs+1−1 src/Idris/Prover.hs+1 src/Idris/REPL.hs+1−1 src/Util/Pretty.hs+3 stack-shell.nix+1−1 stack.yaml+1−1 test/basic009/expected+1−1 test/basic018/expected+4−2 test/interactive017/TestMod.idr+5 test/interactive017/expected+7 test/interactive017/run+9 test/interactive017/shebang-args.idr+6 test/interactive017/shebang-import.idr+6 test/interactive017/shebang-node.idr+4 test/interactive017/shebang.idr+4 test/regression002/expected+2−1
CHANGELOG.md+4−1
@@ -1,7 +1,10 @@
1−# New in 1.0.1
1+# New in 1.1.0
22
33## Library Updates
44
5++ Added `Text.PrettyPrint.WL` an implementation of the Wadler-Leijen
6+ Pretty-Print algorithm. Useful for those wishing to pretty print
7+ things.
58+ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries
69 for implementing total lexical analysers and parsers.
710+ New instances:
idris.cabal+8−10
@@ -1,5 +1,5 @@
11Name: idris
2−Version: 1.0
2+Version: 1.1.0
33License: BSD3
44License-file: LICENSE
55Author: Edwin Brady
@@ -40,7 +40,7 @@ Description: Idris is a general purpose language with full dependent types.
4040 .
4141 * Hugs style interactive environment
4242
43−Cabal-Version: >= 1.8.1
43+Cabal-Version: >= 1.18
4444
4545Build-type: Custom
4646
@@ -302,14 +302,6 @@ Library
302302 , fsnotify >= 0.2 && < 2.2
303303 , async < 2.2
304304
305− Extensions: MultiParamTypeClasses
306− , DeriveFoldable
307− , DeriveTraversable
308− , FunctionalDependencies
309− , FlexibleContexts
310− , FlexibleInstances
311− , TemplateHaskell
312−
313305 ghc-prof-options: -auto-all -caf-all
314306
315307 if os(linux)
@@ -347,6 +339,7 @@ Executable idris
347339 , haskeline >= 0.7
348340 , transformers
349341
342+ Default-Language: Haskell2010
350343 ghc-prof-options: -auto-all -caf-all
351344 ghc-options: -threaded -rtsopts -funbox-strict-fields -with-rtsopts=-I0
352345
@@ -372,6 +365,8 @@ Test-suite regression-and-feature-tests
372365 , bytestring
373366 , transformers
374367
368+
369+ Default-Language: Haskell2010
375370 ghc-prof-options: -auto-all -caf-all
376371 ghc-options: -threaded -rtsopts -with-rtsopts=-N -funbox-strict-fields
377372
@@ -385,6 +380,7 @@ Executable idris-codegen-c
385380 , haskeline >= 0.7
386381 , transformers
387382
383+ Default-Language: Haskell2010
388384 ghc-prof-options: -auto-all -caf-all
389385 ghc-options: -threaded -rtsopts -funbox-strict-fields
390386
@@ -398,6 +394,7 @@ Executable idris-codegen-javascript
398394 , haskeline >= 0.7
399395 , transformers
400396
397+ Default-Language: Haskell2010
401398 ghc-prof-options: -auto-all -caf-all
402399 ghc-options: -threaded -rtsopts -funbox-strict-fields
403400
@@ -411,5 +408,6 @@ Executable idris-codegen-node
411408 , haskeline >= 0.7
412409 , transformers
413410
411+ Default-Language: Haskell2010
414412 ghc-prof-options: -auto-all -caf-all
415413 ghc-options: -threaded -rtsopts -funbox-strict-fields
libs/contrib/Text/PrettyPrint/WL.idrnew file+18
@@ -0,0 +1,18 @@
1+||| A revised Idris port of the Wadler-Leijen pretty-printer.
2+|||
3+||| This port of the Wadler-Leijen Pretty-Printer is based upon the
4+||| port originally created by Shayan Najd [1]. We have changed the
5+||| render function to be total using a technique based on
6+||| continuations proposed by gallais [2], and fix minor errors in the
7+||| original Idris port.
8+|||
9+||| [1] https://github.com/shayan-najd/wl-pprint
10+||| [2] https://gallais.github.io/blog/termination-tricks.html
11+module Text.PrettyPrint.WL
12+
13+import public Text.PrettyPrint.WL.Core
14+import public Text.PrettyPrint.WL.Characters
15+import public Text.PrettyPrint.WL.Combinators
16+
17+%default total
18+%access export
libs/contrib/Text/PrettyPrint/WL/Characters.idrnew file+103
@@ -0,0 +1,103 @@
1+||| Commonly used characters
2+module Text.PrettyPrint.WL.Characters
3+
4+import Text.PrettyPrint.WL.Core
5+
6+%default total
7+%access export
8+
9+lparen : Doc
10+lparen = char '('
11+
12+rparen : Doc
13+rparen = char ')'
14+
15+langle : Doc
16+langle = char '<'
17+
18+rangle : Doc
19+rangle = char '>'
20+
21+lbrace : Doc
22+lbrace = char '{'
23+
24+rbrace : Doc
25+rbrace = char '}'
26+
27+lbracket : Doc
28+lbracket = char '['
29+
30+rbracket : Doc
31+rbracket = char ']'
32+
33+squote : Doc
34+squote = char '\''
35+
36+dquote : Doc
37+dquote = char '"'
38+
39+semi : Doc
40+semi = char ';'
41+
42+colon : Doc
43+colon = char ':'
44+
45+comma : Doc
46+comma = char ','
47+
48+space : Doc
49+space = char ' '
50+
51+dot : Doc
52+dot = char '.'
53+
54+backslash : Doc
55+backslash = char '\\'
56+
57+forwardslash : Doc
58+forwardslash = char '/'
59+
60+equals : Doc
61+equals = char '='
62+
63+pipe : Doc
64+pipe = char '|'
65+
66+bang : Doc
67+bang = char '!'
68+
69+tick : Doc
70+tick = char '`'
71+
72+tilda : Doc
73+tilda = char '~'
74+
75+hash : Doc
76+hash = char '#'
77+
78+asterix : Doc
79+asterix = char '*'
80+
81+ampersand : Doc
82+ampersand = char '&'
83+
84+dash : Doc
85+dash = char '-'
86+
87+question : Doc
88+question = char '?'
89+
90+dollar : Doc
91+dollar = char '$'
92+
93+pound : Doc
94+pound = char '£'
95+
96+euro : Doc
97+euro = char '€'
98+
99+caret : Doc
100+caret = char '^'
101+
102+percent : Doc
103+percent = char '%'
libs/contrib/Text/PrettyPrint/WL/Combinators.idrnew file+259
@@ -0,0 +1,259 @@
1+||| Common combinators.
2+module Text.PrettyPrint.WL.Combinators
3+
4+import Text.PrettyPrint.WL.Core
5+import Text.PrettyPrint.WL.Characters
6+
7+%default total
8+%access export
9+
10+-- --------------------------------------------------- [ Alignment Combinators ]
11+
12+||| The document `(align x)` renders document `x` with the nesting
13+||| level set to the current column. It is used for example to
14+||| implement 'hang'.
15+align : Doc -> Doc
16+align d = column (\k => nesting (\i => nest (k - i) d))
17+
18+||| The hang combinator implements hanging indentation. The document
19+||| `(hang i x)` renders document `x` with a nesting level set to the
20+||| current column plus `i`.
21+hang : Int -> Doc -> Doc
22+hang i d = align (nest i d)
23+
24+||| The document `(indent i x)` indents document `x` with `i` spaces.
25+indent : Int -> Doc -> Doc
26+indent i d = hang i (text (spaces i) <+> d)
27+
28+-- -------------------------------------------------- [ High-Level Combinators ]
29+
30+||| The document `softLine` behaves like `space` if the resulting
31+||| output fits the page, otherwise it behaves like `line`.
32+softLine : Doc
33+softLine = group line
34+
35+||| The document `softbreak` behaves like `empty` if the resulting
36+||| output fits the page, otherwise it behaves like 'line'.
37+softBreak : Doc
38+softBreak = group breakLine
39+
40+infixr 5 |/|, |//|, |$|, |$$|
41+infixr 6 |+|, |++|
42+
43+private
44+concatDoc : Doc -> Doc -> Doc -> Doc
45+concatDoc sep x y = x `beside` (sep `beside` y)
46+
47+||| The document `(x |+| y)` concatenates document `x` and document
48+||| `y`. It is an associative operation having 'empty' as a left and
49+||| right unit.
50+(|+|) : Doc -> Doc -> Doc
51+(|+|) = (<+>)
52+
53+||| The document `(x |++| y)` concatenates document `x` and `y` with a
54+||| `space` in between.
55+(|++|) : Doc -> Doc -> Doc
56+(|++|) = concatDoc space
57+
58+||| The document `(x |/| y)` concatenates document `x` and `y` with a
59+||| 'softline' in between. This effectively puts `x` and `y` either
60+||| next to each other (with a `space` in between) or underneath each
61+||| other.
62+(|/|) : Doc -> Doc -> Doc
63+(|/|) = concatDoc softLine
64+
65+||| The document `(x |//| y)` concatenates document `x` and `y` with
66+||| a 'softbreak' in between. This effectively puts `x` and `y` either
67+||| right next to each other or underneath each other.
68+(|//|) : Doc -> Doc -> Doc
69+(|//|) = concatDoc softBreak
70+
71+||| The document `(x |$| y)` concatenates document `x` and `y` with a
72+||| `line` in between.
73+(|$|) : Doc -> Doc -> Doc
74+(|$|) = concatDoc line
75+
76+||| The document `(x |$$| y)` concatenates document `x` and `y` with
77+||| a `linebreak` in between.
78+(|$$|) : Doc -> Doc -> Doc
79+(|$$|) = concatDoc breakLine
80+
81+||| The document `(vsep xs)` concatenates all documents `xs`
82+||| vertically with `(|$|)`. If a 'group' undoes the line breaks
83+||| inserted by `vsep`, all documents are separated with a space.
84+vsep : List Doc -> Doc
85+vsep = fold (|$|)
86+
87+||| The document `(sep xs)` concatenates all documents `xs` either
88+||| horizontally with `(|++|)`, if it fits the page, or vertically with
89+||| `(|$|)`.
90+sep : List Doc -> Doc
91+sep = group . vsep
92+
93+
94+||| The document `(fillSep xs)` concatenates documents `xs`
95+||| horizontally with `(|++|)` as long as its fits the page, than
96+||| inserts a `line` and continues doing that for all documents in
97+||| `xs`.
98+fillSep : List Doc -> Doc
99+fillSep = fold (|/|)
100+
101+||| The document `(hsep xs)` concatenates all documents `xs`
102+||| horizontally with `(|++|)`.
103+hsep : List Doc -> Doc
104+hsep = fold (|++|)
105+
106+||| The document `(hcat xs)` concatenates all documents `xs`
107+||| horizontally with `(|+|)`.
108+hcat : List Doc -> Doc
109+hcat = fold (<+>)
110+
111+||| The document `(vcat xs)` concatenates all documents `xs`
112+||| vertically with `(|$$|)`. If a `group` undoes the line breaks
113+||| inserted by `vcat`, all documents are directly concatenated.
114+vcat : List Doc -> Doc
115+vcat = fold (|$$|)
116+
117+||| The document `(cat xs)` concatenates all documents `xs` either
118+||| horizontally with `(|+|)`, if it fits the page, or vertically with
119+||| `(|$$|)`.
120+cat : List Doc -> Doc
121+cat = group . vcat
122+
123+||| The document `(fillCat xs)` concatenates documents `xs`
124+||| horizontally with `(|+|)` as long as its fits the page, than inserts
125+||| a `linebreak` and continues doing that for all documents in `xs`.
126+fillCat : List Doc -> Doc
127+fillCat = fold (|//|)
128+
129+||| The document `(enclose l r x)` encloses document `x` between
130+||| documents `l` and `r` using `(|+|)`.
131+enclose : Doc -> Doc -> Doc -> Doc
132+enclose l r x = concatDoc x l r
133+
134+squotes : Doc -> Doc
135+squotes = enclose squote squote
136+
137+dquotes : Doc -> Doc
138+dquotes = enclose dquote dquote
139+
140+braces : Doc -> Doc
141+braces = enclose lbrace rbrace
142+
143+parens : Doc -> Doc
144+parens = enclose lparen rparen
145+
146+angles : Doc -> Doc
147+angles = enclose langle rangle
148+
149+brackets : Doc -> Doc
150+brackets = enclose lbracket rbracket
151+
152+-- ----------------------------------------------------- [ Lists, Sets, Tuples ]
153+
154+||| The document `(encloseSep l r sep xs)` concatenates the documents
155+||| `xs` separated by `sep` and encloses the resulting document by `l`
156+||| and `r`. The documents are rendered horizontally if that fits the
157+||| page. Otherwise they are aligned vertically. All separators are put
158+||| in front of the elements.
159+encloseSep : (l : Doc)
160+ -> (r : Doc)
161+ -> (sep : Doc)
162+ -> (xs : List Doc)
163+ -> Doc
164+encloseSep l r s [] = l <+> r
165+encloseSep l r s [x] = l <+> x <+> r
166+encloseSep l r s xs = align (cat (zipWith (<+>) (l :: replicate (length xs) s) xs) <+> r)
167+
168+||| The document `(list xs)` comma separates the documents `xs` and
169+||| encloses them in square brackets. The documents are rendered
170+||| horizontally if that fits the page. Otherwise they are aligned
171+||| vertically. All comma separators are put in front of the
172+||| elements.
173+list : List Doc -> Doc
174+list = encloseSep lbracket rbracket comma
175+
176+||| The document `(tupled xs)` comma separates the documents `xs`
177+||| and encloses them in parenthesis. The documents are rendered
178+||| horizontally if that fits the page. Otherwise they are aligned
179+||| vertically. All comma separators are put in front of the
180+||| elements.
181+tupled : List Doc -> Doc
182+tupled = encloseSep lparen rparen comma
183+
184+||| The document `(set xs)` separates the documents `xs` with
185+||| commas and encloses them in braces. The documents are
186+||| rendered horizontally if that fits the page. Otherwise they are
187+||| aligned vertically. All comma's are put in front of the
188+||| elements.
189+set : List Doc -> Doc
190+set = encloseSep lbrace rbrace comma
191+
192+||| The document `(semiBraces xs)` separates the documents `xs` with
193+||| semi-colon and encloses them in braces. The documents are
194+||| rendered horizontally if that fits the page. Otherwise they are
195+||| aligned vertically. All semi-colons's are put in front of the
196+||| elements.
197+semiBrace : List Doc -> Doc
198+semiBrace = encloseSep lbrace rbrace semi
199+
200+||| `(punctuate p xs)` concatenates all documents in `xs` with
201+||| document `p` except for the last document.
202+punctuate : Doc -> List Doc -> List Doc
203+punctuate p [] = []
204+punctuate p [x] = [x]
205+punctuate p (x :: xs) = (x <+> p) :: punctuate p xs
206+
207+-- ------------------------------------------------------------------- [ Fills ]
208+
209+width : Doc -> (Int -> Doc) -> Doc
210+width doc f = column (\k => doc <+> column (\k' => f (k' - k)))
211+
212+||| The document `(fillBreak i x)` first renders document `x`. It
213+||| than appends `space`s until the width is equal to `i`. If the
214+||| width of `x` is already larger than `i`, the nesting level is
215+||| increased by `i` and a `line` is appended.
216+fillBreak : (i : Int) -> (x : Doc) -> Doc
217+fillBreak f x =
218+ width x (\w => if (w > f)
219+ then nest f breakLine
220+ else text (spaces (f - w)))
221+
222+||| The document `(fill i x)` renders document `x`. It than appends
223+||| `space`s until the width is equal to `i`. If the width of `x` is
224+||| already larger, nothing is appended. This combinator is quite
225+||| useful in practice to output a list of bindings.
226+fill : (i : Int) -> (x : Doc) -> Doc
227+fill f d =
228+ width d (\w => if (w >= f)
229+ then empty
230+ else text (spaces (f - w)))
231+
232+-- -------------------------------------------------------------- [ Primatives ]
233+
234+||| The document `(literal s)` concatenates all characters in `s`
235+||| using `line` for newline characters and `char` for all other
236+||| characters. It is used instead of 'text' whenever the text contains
237+||| newline characters.
238+literal : (str : String) -> Doc
239+literal str = mkLiteral (unpack str)
240+ where
241+ mkLiteral : List Char -> Doc
242+ mkLiteral Nil = empty
243+ mkLiteral ('\n':: ss) = line <+> mkLiteral ss
244+ mkLiteral (c :: ss) = char c <+> mkLiteral ss
245+
246+bool : Bool -> Doc
247+bool b = text (show b)
248+
249+nat : Nat -> Doc
250+nat n = text (show n)
251+
252+int : Int -> Doc
253+int i = text (show i)
254+
255+integer : Integer -> Doc
256+integer i = text (show i)
257+
258+double : Double -> Doc
259+double d = text (show d)
libs/contrib/Text/PrettyPrint/WL/Core.idrnew file+225
@@ -0,0 +1,225 @@
1+||| Core definitions and primitives.
2+module Text.PrettyPrint.WL.Core
3+
4+%default total
5+%access export
6+
7+-- -------------------------------------------------------------------- [ Core ]
8+
9+||| The abstract data type `Doc` represents pretty documents.
10+|||
11+data Doc : Type where
12+ Empty : Doc
13+ Chara : (c : Char) -> Doc
14+ Text : (len : Int) -> (str : String) -> Doc
15+ Line : (undone : Bool) -> Doc
16+
17+ Cat : (x : Doc) -> (y : Doc) -> Doc
18+ Nest : (lvl : Int) -> (x : Doc) -> Doc
19+ Union : (x : Doc) -> (y : Doc) -> Doc
20+
21+ Column : (f : Int -> Doc) -> Doc
22+ Nesting : (f : Int -> Doc) -> Doc
23+
24+-- -------------------------------------------------------------- [ Primitives ]
25+
26+||| The empty document is, indeed, empty.
27+empty : Doc
28+empty = Empty
29+
30+||| The `line` document advances to the next line and indents to the
31+||| current nesting level. Document `line` behaves like `(text " ")`
32+||| if the line break is undone by 'group'.
33+line : Doc
34+line = Line False
35+
36+||| The document `(char c)` contains the literal character `c`. If the
37+||| character is a newline (`'\n'`) the function returns a line
38+||| document. Ideally, the function 'line' should be used for line
39+||| breaks.
40+char : (c : Char) -> Doc
41+char '\n' = line
42+char c = Chara c
43+
44+||| The document `(text s)` contains the literal string `s`. The
45+||| string shouldn't contain any newline (`'\n'`) characters. If the
46+||| string contains newline characters, the function 'literal' should be
47+||| used.
48+text : (str : String) -> Doc
49+text "" = empty
50+text str = Text (cast $ length str) str
51+
52+||| The `breakLine` document advances to the next line and indents to
53+||| the current nesting level. Document `breakLine` behaves like
54+||| 'empty' if the line break is undone by 'group'.
55+breakLine : Doc
56+breakLine = Line True
57+
58+||| Horizontal concatenation of documents
59+beside : Doc -> Doc -> Doc
60+beside = Cat
61+
62+||| The document `(nest lvl x)` renders document `x` with the current
63+||| indentation level increased by lvl.
64+nest : (lvl : Int)
65+ -> (x : Doc)
66+ -> Doc
67+nest = Nest
68+
69+column : (f : Int -> Doc) -> Doc
70+column = Column
71+
72+nesting : (f : Int -> Doc) -> Doc
73+nesting = Nesting
74+
75+private %inline
76+flatten : Doc -> Doc
77+flatten (Line break) = if break then Empty else Text 1 " "
78+
79+flatten (Cat x y) = Cat (flatten x) (flatten y)
80+flatten (Nest lvl x) = Nest lvl (flatten x)
81+flatten (Union x _) = flatten x
82+flatten (Column f) = Column (\i => flatten $ f i)
83+flatten (Nesting f) = Nesting (\i => flatten $ f i)
84+
85+flatten other = other
86+
87+||| The `group` combinator is used to specify alternative
88+||| layouts. The document `(group x)` undoes all line breaks in
89+||| document `x`. The resulting line is added to the current line if
90+||| that fits the page. Otherwise, the document `x` is rendered without
91+||| any changes.
92+group : Doc -> Doc
93+group x = Union (flatten x) x
94+
95+Semigroup Doc where
96+ (<+>) x y = beside x y
97+
98+Monoid Doc where
99+ neutral = empty
100+
101+fold : (f : Doc -> Doc -> Doc) -> (ds : List Doc) -> Doc
102+fold _ Nil = empty
103+fold f (x::xs) = foldl f x xs
104+
105+-- --------------------------------------------------------------- [ Renderers ]
106+
107+namespace PrettyDoc
108+
109+ ||| The data type `PrettyDoc` represents rendered documents and is
110+ ||| used by the display functions.
111+ data PrettyDoc : Type where
112+ Empty : PrettyDoc
113+ Chara : (c : Char) -> (rest : PrettyDoc) -> PrettyDoc
114+ Text : (len : Int) -> (str : String) -> (rest : PrettyDoc) -> PrettyDoc
115+ Line : (lvl : Int) -> (rest : PrettyDoc) -> PrettyDoc
116+
117+||| Helper function to construct spaces.
118+spaces : (n : Int) -> String
119+spaces n = if n <= 0 then "" else pack $ replicate (cast n) ' '
120+
121+private
122+indentation : Int -> String
123+indentation n = spaces n
124+
125+||| `(showPrettyDoc doc)` takes the output `PrettyDoc` from a
126+||| rendering function and transforms it to a String for printing.
127+showPrettyDoc : (doc : PrettyDoc) -> String
128+showPrettyDoc doc = showPrettyDocS doc ""
129+ where
130+ showPrettyDocS : (doc : PrettyDoc) -> (acc : String) -> String
131+ showPrettyDocS Empty = id
132+ showPrettyDocS (Chara c rest) = strCons c . showPrettyDocS rest
133+ showPrettyDocS (Text len str rest) = (str ++) . showPrettyDocS rest
134+ showPrettyDocS (Line lvl rest) = (('\n' `strCons` indentation lvl) ++) . showPrettyDocS rest
135+
136+private
137+fits : (w : Int) -> (x : PrettyDoc) -> Bool
138+fits w Empty = if w < 0 then False else True
139+fits w (Chara c rest) = if w < 0 then False else fits (w - 1) rest
140+
141+fits w (Text len str rest) = if w < 0 then False else fits (w - len) rest
142+
143+fits w (Line _ _) = if w < 0 then False else True
144+
145+
146+||| Use the Wadler-Leijen algorithm to pretty print the `doc`.
147+||| The algorithm uses a page width of `width` and a ribbon
148+||| width of `(ribbonfrac * width)` characters. The ribbon width is
149+||| the maximal amount of non-indentation characters on a line. The
150+||| parameter `ribbonfrac` should be between `0.0` and `1.0`. If it is
151+||| lower or higher, the ribbon width will be 0 or `width`
152+||| respectively.
153+render : (rfrac : Double)
154+ -> (width : Int)
155+ -> (doc : Doc)
156+ -> PrettyDoc
157+render rfrac w doc = best w 0 0 doc (const Empty)
158+ where
159+ rwidth : Int
160+ rwidth = max 0 $ min w (cast (cast w * rfrac))
161+
162+ nicest : (lvl : Int)
163+ -> (col : Int)
164+ -> (x : PrettyDoc)
165+ -> (y : PrettyDoc)
166+ -> PrettyDoc
167+ nicest n k x y =
168+ let width = min (w - k) (rwidth - k + n)
169+ in if fits width x then x else y
170+
171+ best : (lvl : Int)
172+ -> (col : Int)
173+ -> (curr : Int)
174+ -> (doc : Doc)
175+ -> (k : Int -> PrettyDoc)
176+ -> PrettyDoc
177+ best lvl col curr Empty k = k col
178+ best lvl col curr (Chara c) k = Chara c $ k (col + 1)
179+ best lvl col curr (Text len str) k = Text len str $ k (col + len)
180+ best lvl col curr (Line undone) k = Line curr $ k curr
181+
182+ best lvl col curr (Cat x y) k =
183+ best lvl col curr x (\curr' => best lvl curr' curr y k)
184+
185+ best lvl col curr (Nest x y) k = best lvl col (curr+x) y k
186+
187+ best lvl col curr (Union x y) k =
188+ nicest lvl col (best lvl col curr x k)
189+ (best lvl col curr y k)
190+
191+ best lvl col curr (Column f) k = best lvl col curr (f col) k
192+ best lvl col curr (Nesting f) k = best lvl col curr (f curr) k
193+
194+||| Print the document to a string using the given ribbon fraction
195+||| and page width.
196+toString : (rfrac : Double)
197+ -> (width : Int)
198+ -> (doc : Doc)
199+ -> String
200+toString rfrac width doc = showPrettyDoc (render rfrac width doc)
201+
202+writeDoc : (fname : String)
203+ -> (rfrac : Double)
204+ -> (width : Int)
205+ -> (doc : Doc)
206+ -> IO (Either FileError ())
207+writeDoc fname rfrac width doc = writeFile fname $ toString rfrac width doc
208+
209+namespace Default
210+
211+ ||| Render the document with a default ribbon fraction of 0.4 and page width of 120 characters.
212+ render : (doc : Doc) -> PrettyDoc
213+ render = render 0.4 120
214+
215+ ||| Print the document to a string using a default ribbon fraction
216+ ||| of 0.4 and page width of 120 characters.
217+ toString : (doc : Doc) -> String
218+ toString = toString 0.4 120
219+
220+ ||| Write the doc to `fname` using a default ribbon fraction of 0.4
221+ ||| and page width of 120 characters.
222+ writeDoc : (fname : String)
223+ -> (doc : Doc)
224+ -> IO (Either FileError ())
225+ writeDoc fname doc = writeFile fname $ Default.toString doc
libs/contrib/contrib.ipkg+5
@@ -32,4 +32,9 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
3232
3333 Text.Lexer, Text.Parser,
3434
35+ Text.PrettyPrint.WL,
36+ Text.PrettyPrint.WL.Core,
37+ Text.PrettyPrint.WL.Characters,
38+ Text.PrettyPrint.WL.Combinators,
39+
3540 Data.Fin.Extra
scripts/runidrisnew file+18
@@ -0,0 +1,18 @@
1+#!/bin/sh
2+
3+# This is a script that runs an idris program, suitable for use
4+# in a shebang line. We cache the executables by naming them after
5+# the SHA hash of the idris source and looking for it before
6+# compiling
7+RUNIDRIS_DIR="${TEMP:-/tmp}/runidris"
8+if [ ! -d $RUNIDRIS_DIR ]; then
9+ mkdir $RUNIDRIS_DIR
10+ chmod 700 $RUNIDRIS_DIR
11+fi
12+TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`"
13+FP="$RUNIDRIS_DIR/$TEMP_NAME"
14+if [ ! -e $FP ]; then
15+ "${IDRIS:-idris}" $1 --ibcsubdir "$RUNIDRIS_DIR" -i "." -o $FP
16+fi
17+shift
18+"$FP" "$@"
scripts/runidris-nodenew file+18
@@ -0,0 +1,18 @@
1+#!/bin/sh
2+
3+# This is a script that runs an idris program, suitable for use
4+# in a shebang line. We cache the executables by naming them after
5+# the SHA hash of the idris source and looking for it before
6+# compiling. This is the node version.
7+RUNIDRIS_DIR="${TEMP:-/tmp}/runidris-node"
8+if [ ! -d $RUNIDRIS_DIR ]; then
9+ mkdir $RUNIDRIS_DIR
10+ chmod 700 $RUNIDRIS_DIR
11+fi
12+TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`.js"
13+FP="$RUNIDRIS_DIR/$TEMP_NAME"
14+if [ ! -e $FP ]; then
15+ "${IDRIS:-idris}" --codegen node --ibcsubdir "$RUNIDRIS_DIR" -i "." $1 -o $FP
16+fi
17+shift
18+node "$FP" "$@"
src/IRTS/CodegenC.hs+234−115
@@ -5,9 +5,11 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleContexts #-}
9+
810module IRTS.CodegenC (codegenC) where
911
10−import Idris.AbsSyntax
12+import Idris.AbsSyntax hiding (getBC)
1113import Idris.Core.TT
1214import IRTS.Bytecode
1315import IRTS.CodegenCommon
@@ -19,10 +21,12 @@ import IRTS.System
1921import Util.System
2022
2123import Control.Monad
24+import Control.Monad
25+import Control.Monad.RWS
2226import Data.Bits
2327import Data.Char
24−import Data.List (intercalate, nubBy)
25−import Debug.Trace
28+import Data.List (find, intercalate, nubBy, partition)
29+import qualified Data.Text as T
2630import Numeric
2731import System.Directory
2832import System.Exit
@@ -30,6 +34,8 @@ import System.FilePath ((<.>), (</>))
3034import System.IO
3135import System.Process
3236
37+import Debug.Trace
38+
3339codegenC :: CodeGenerator
3440codegenC ci = do codegenC' (simpleDecls ci)
3541 (outputFile ci)
@@ -64,7 +70,9 @@ codegenC' defs out exec incs objs libs flags exports iface dbg
6470 let bc = map toBC defs
6571 let wrappers = genWrappers bc
6672 let h = concatMap toDecl (map fst bc)
67− let cc = concatMap (uncurry toC) bc
73+ let (state, cc) = execRWS (generateSrc bc) 0
74+ (CS { fnName = Nothing,
75+ level = 1 })
6876 let hi = concatMap ifaceC (concatMap getExp exports)
6977 d <- getIdrisCRTSDir
7078 mprog <- readFile (d </> "idris_main" <.> "c")
@@ -134,12 +142,17 @@ creg Tmp = "REG1"
134142toDecl :: Name -> String
135143toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"
136144
137−toC :: Name -> [BC] -> String
138−toC f code
139− = -- "/* " ++ show code ++ "*/\n\n" ++
140− "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" ++
141− indent 1 ++ "INITFRAME;\n" ++
142− concatMap (bcc 1) code ++ "}\n\n"
145+generateSrc :: [(Name, [BC])] -> RWS Int String CState ()
146+generateSrc bc = mapM_ toC bc
147+
148+toC :: (Name, [BC]) -> RWS Int String CState ()
149+toC (f, code) = do
150+ modify (\s -> s { fnName = Just f })
151+ s <- get
152+ tell $ "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n"
153+ tell $ indent (level s) ++ "INITFRAME;\n"
154+ bcc code
155+ tell $ "}\n\n"
143156
144157showCStr :: String -> String
145158showCStr s = '"' : foldr ((++) . showChar) "\"" s
@@ -175,10 +188,22 @@ showCStr s = '"' : foldr ((++) . showChar) "\"" s
175188 2 -> s
176189 _ -> error $ "Can't happen: String of invalid length " ++ show s
177190
178−bcc :: Int -> BC -> String
179−bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
180−bcc i (ASSIGNCONST l c)
181− = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"
191+data CState = CS {
192+ fnName :: Maybe Name,
193+ level :: Int
194+}
195+
196+
197+bcc :: [BC] -> RWS Int String CState ()
198+bcc [] = return ()
199+bcc ((ASSIGN l r):xs) = do
200+ i <- get
201+ tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
202+ bcc xs
203+bcc ((ASSIGNCONST l c):xs) = do
204+ i <- get
205+ tell $ indent (level i) ++ creg l ++ " = " ++ mkConst c ++ ";\n"
206+ bcc xs
182207 where
183208 mkConst (I i) = "MKINT(" ++ show i ++ ")"
184209 mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"
@@ -196,16 +221,21 @@ bcc i (ASSIGNCONST l c)
196221 mkConst c | isTypeConst c = "MKINT(42424242)"
197222 mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented"
198223
199−bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
200−bcc i (MKCON l loc tag []) | tag < 256
201− = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
202−bcc i (MKCON l loc tag args)
203− = indent i ++ alloc loc tag ++
204− indent i ++ setArgs 0 args ++ "\n" ++
205− indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
206−
207−-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++
208−-- show (length args) ++ concatMap showArg args ++ ");\n"
224+bcc ((UPDATE l r):xs) = do
225+ i <- get
226+ tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
227+ bcc xs
228+bcc ((MKCON l loc tag []):xs) | tag < 256 = do
229+ i <- get
230+ tell $ indent (level i) ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
231+ bcc xs
232+bcc ((MKCON l loc tag args):xs) = do
233+ i <- get
234+ let tab = indent (level i)
235+ tell $ tab ++ alloc loc tag ++
236+ tab ++ setArgs 0 args ++ "\n" ++
237+ tab ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
238+ bcc xs
209239 where showArg r = ", " ++ creg r
210240 setArgs i [] = ""
211241 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++
@@ -217,52 +247,94 @@ bcc i (MKCON l loc tag args)
217247 = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++
218248 show (length args) ++ ");\n"
219249
220−bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++
221− ", " ++ show a ++ ");\n"
222−bcc i (PROJECTINTO r t idx)
223− = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"
224−bcc i (CASE True r code def)
225− | length code < 4 = showCase i def code
250+bcc ((PROJECT l loc a):xs) = do
251+ i <- get
252+ tell $ indent (level i) ++ "PROJECT(vm, " ++ creg l ++ ", "
253+ ++ show loc ++ ", " ++ show a ++ ");\n"
254+ bcc xs
255+bcc ((PROJECTINTO r t idx):xs) = do
256+ i <- get
257+ tell $ indent (level i) ++ creg r ++ " = GETARG(" ++ creg t
258+ ++ ", " ++ show idx ++ ");\n"
259+ bcc xs
260+bcc ((CASE True r code def):xs)
261+ | length code < 4 = do
262+ showCases def code
263+ bcc xs
226264 where
227− showCode :: Int -> [BC] -> String
228− showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++
229− indent i ++ "}\n"
230−
231− showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String
232− showCase i Nothing [(t, c)] = indent i ++ showCode i c
233− showCase i (Just def) [] = indent i ++ showCode i def
234− showCase i def ((t, c) : cs)
235− = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c
236− ++ indent i ++ "else\n" ++ showCase i def cs
237−
238−bcc i (CASE safe r code def)
239− = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++
240− concatMap (showCase i) code ++
241− showDef i def ++
242− indent i ++ "}\n"
265+ showCode bc = do
266+ w <- getBC bc xs
267+ i <- get
268+ tell $ "{\n" ++ w ++ indent (level i) ++ "}\n"
269+
270+ showCases Nothing [(t, c)] = do
271+ i <- get
272+ tell $ indent (level i)
273+ showCode c
274+ showCases (Just def) [] = do
275+ i <- get
276+ tell $ indent (level i)
277+ showCode def
278+ showCases def ((t, c) : cs) = do
279+ i <- get
280+ tell $ indent (level i) ++ "if (CTAG(" ++ creg r ++ ") == "
281+ ++ show t ++ ") "
282+ showCode c
283+ tell $ indent (level i) ++ "else\n"
284+ showCases def cs
285+
286+bcc ((CASE safe r code def):xs) = do
287+ i <- get
288+ tell $ indent (level i) ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n"
289+ mapM showCase code
290+ showDef def
291+ tell $ indent (level i) ++ "}\n"
292+ bcc xs
243293 where
244294 ctag True = "CTAG"
245295 ctag False = "TAG"
246296
247− showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
248− ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"
249− showDef i Nothing = ""
250− showDef i (Just c) = indent i ++ "default:\n"
251− ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"
252−bcc i (CONSTCASE r code def)
297+ showCase (t, bc) = do
298+ w <- getBC bc xs
299+ is <- get
300+ let i = level is
301+ tell $ indent i ++ "case " ++ show t ++ ":\n"
302+ ++ w ++ indent (i + 1) ++ "break;\n"
303+ showDef Nothing = return $ ()
304+ showDef (Just c) = do
305+ w <- getBC c xs
306+ is <- get
307+ let i = level is
308+ tell $ indent i ++ "default:\n" ++ w ++ indent (i + 1) ++ "break;\n"
309+
310+bcc ((CONSTCASE r code def):xs)
253311 | intConsts code
254−-- = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" ++
255−-- concatMap (showCase i) code ++
256−-- showDef i def ++
257−-- indent i ++ "}\n"
258− = concatMap (iCase (creg r)) code ++
259− indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
312+ = do
313+ is <- get
314+ let i = level is
315+ codes <- mapM getCode code
316+ defs <- showDefS def
317+ tell $ concatMap (iCase i (creg r)) codes
318+ tell $ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
319+ bcc xs
260320 | strConsts code
261− = concatMap (strCase ("GETSTR(" ++ creg r ++ ")")) code ++
262− indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
321+ = do
322+ is <- get
323+ let i = level is
324+ codes <- mapM getCode code
325+ defs <- showDefS def
326+ tell $ concatMap (strCase i ("GETSTR(" ++ creg r ++ ")")) codes
327+ ++ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
328+ bcc xs
263329 | bigintConsts code
264− = concatMap (biCase (creg r)) code ++
265− indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
330+ = do
331+ is <- get
332+ let i = level is
333+ codes <- mapM getCode code
334+ defs <- showDefS def
335+ tell $ concatMap (biCase i (creg r)) codes ++
336+ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
337+ bcc xs
266338 | otherwise = error $ "Can't happen: Can't compile const case " ++ show code
267339 where
268340 intConsts ((I _, _ ) : _) = True
@@ -279,72 +351,119 @@ bcc i (CONSTCASE r code def)
279351 strConsts ((Str _, _ ) : _) = True
280352 strConsts _ = False
281353
282− strCase sv (s, bc) =
354+ getCode (x, code) = do
355+ c <- getBC code xs
356+ return (x, c)
357+
358+ strCase i sv (s, bc) =
283359 indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++
284− concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
285− biCase bv (BI b, bc) =
360+ bc ++ indent i ++ "} else\n"
361+ biCase i bv (BI b, bc) =
286362 indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"
287− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
288− iCase v (I b, bc) =
363+ ++ bc ++ indent i ++ "} else\n"
364+ iCase i v (I b, bc) =
289365 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"
290− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
291− iCase v (Ch b, bc) =
366+ ++ bc ++ indent i ++ "} else\n"
367+ iCase i v (Ch b, bc) =
292368 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"
293− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
294− iCase v (B8 w, bc) =
369+ ++ bc ++ indent i ++ "} else\n"
370+ iCase i v (B8 w, bc) =
295371 indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
296− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
297− iCase v (B16 w, bc) =
372+ ++ bc ++ indent i ++ "} else\n"
373+ iCase i v (B16 w, bc) =
298374 indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
299− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
300− iCase v (B32 w, bc) =
375+ ++ bc ++ indent i ++ "} else\n"
376+ iCase i v (B32 w, bc) =
301377 indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
302− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
303− iCase v (B64 w, bc) =
378+ ++ bc ++ indent i ++ "} else\n"
379+ iCase i v (B64 w, bc) =
304380 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
305− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
306− showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
307− ++ concatMap (bcc (i+1)) bc ++
308− indent (i + 1) ++ "break;\n"
309− showDef i Nothing = ""
310− showDef i (Just c) = indent i ++ "default:\n"
311− ++ concatMap (bcc (i+1)) c ++
312− indent (i + 1) ++ "break;\n"
313− showDefS i Nothing = ""
314− showDefS i (Just c) = concatMap (bcc (i+1)) c
315−
316−bcc i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"
317−bcc i (TAILCALL n) = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"
318−bcc i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"
319−bcc i REBASE = indent i ++ "REBASE;\n"
320−bcc i (RESERVE 0) = ""
321−bcc i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"
322−bcc i (ADDTOP 0) = ""
323−bcc i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"
324−bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"
325−bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"
326−bcc i STOREOLD = indent i ++ "STOREOLD;\n"
327−bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"
328−bcc i (FOREIGNCALL l rty (FStr fn@('&':name)) [])
329− = indent i ++
330− c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
331−bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"
332− = indent i ++
333− c_irts (toFType rty) (creg l ++ " = ")
381+ ++ bc ++ indent i ++ "} else\n"
382+
383+ showDefS Nothing = return ""
384+ showDefS (Just c) = getBC c xs
385+
386+bcc (CALL n:xs) = do
387+ i <- get
388+ tell $ indent (level i) ++ "CALL(" ++ cname n ++ ");\n"
389+ bcc xs
390+bcc (TAILCALL n:xs) = do
391+ i <- get
392+ tell $ indent (level i) ++ "TAILCALL(" ++ cname n ++ ");\n"
393+ bcc xs
394+bcc ((SLIDE n):xs) = do
395+ i <- get
396+ tell $ indent (level i) ++ "SLIDE(vm, " ++ show n ++ ");\n"
397+ bcc xs
398+bcc (REBASE:xs) = do
399+ i <- get
400+ tell $ indent (level i)++ "REBASE;\n"
401+ bcc xs
402+bcc ((RESERVE 0):xs) = bcc xs
403+bcc ((RESERVE n):xs) = do
404+ i <- get
405+ tell $ indent (level i) ++ "RESERVE(" ++ show n ++ ");\n"
406+ bcc xs
407+bcc ((ADDTOP 0):xs) = bcc xs
408+bcc ((ADDTOP n):xs) = do
409+ i <- get
410+ tell $ indent (level i) ++ "ADDTOP(" ++ show n ++ ");\n"
411+ bcc xs
412+bcc ((TOPBASE n):xs) = do
413+ i <- get
414+ tell $ indent (level i) ++ "TOPBASE(" ++ show n ++ ");\n"
415+ bcc xs
416+bcc ((BASETOP n):xs) = do
417+ i <- get
418+ tell $ indent (level i) ++ "BASETOP(" ++ show n ++ ");\n"
419+ bcc xs
420+bcc (STOREOLD:xs) = do
421+ i <- get
422+ tell $ indent (level i) ++ "STOREOLD;\n"
423+ bcc xs
424+bcc ((OP l fn args):xs) = do
425+ i <- get
426+ tell $ indent (level i) ++ doOp (creg l ++ " = ") fn args ++ ";\n"
427+ bcc xs
428+bcc ((FOREIGNCALL l rty (FStr fn@('&':name)) []):xs) = do
429+ i <- get
430+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
431+ bcc xs
432+bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%wrapper"
433+ = do
434+ i <- get
435+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
334436 ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"
335−bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"
336− = indent i ++ c_irts (toFType rty) (creg l ++ " = ")
437+ bcc zs
438+bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%dynamic"
439+ = do
440+ i <- get
441+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
337442 ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++
338443 "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"
339−bcc i (FOREIGNCALL l rty (FStr fn) args)
340− = indent i ++
341− c_irts (toFType rty) (creg l ++ " = ")
342− (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
343−bcc i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."
344−bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
345−bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
444+ bcc zs
445+bcc ((FOREIGNCALL l rty (FStr fn) args):xs) = do
446+ i <- get
447+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
448+ (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
449+ bcc xs
450+bcc ((FOREIGNCALL l rty _ args):_) = error "Foreign Function calls cannot be partially applied, without being inlined."
451+bcc ((NULL r):xs) = do
452+ i <- get
453+ tell $ indent (level i) ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
454+ bcc xs
455+bcc ((ERROR str):xs) = do
456+ i <- get
457+ tell $ indent (level i) ++ "fprintf(stderr, "
458+ ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
459+ bcc xs
346460-- bcc i c = error (show c) -- indent i ++ "// not done yet\n"
347461
462+getBC code xs = do
463+ i <- get
464+ let (a, s, w) = runRWS (bcc code) 0 (i { level = level i + 1 })
465+ return w
466+
348467fcall (t, arg) = irts_c (toFType t) (creg arg)
349468-- Deconstruct the Foreign type in the defunctionalised expression and build
350469-- a foreign type description for c_irts and irts_c
src/IRTS/Compiler.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances #-}
8+{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances #-}
99
1010module IRTS.Compiler(compile, generate) where
1111
src/IRTS/Defunctionalise.hs+1−1
@@ -19,7 +19,7 @@ To defunctionalise:
19198. Add explicit EVAL to case, primitives, and foreign calls
2020
2121-}
22−{-# LANGUAGE PatternGuards #-}
22+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
2323module IRTS.Defunctionalise(module IRTS.Defunctionalise
2424 , module IRTS.Lang
2525 ) where
src/IRTS/Lang.hs+2−1
@@ -5,7 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
8+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, FlexibleContexts,
9+ PatternGuards #-}
910
1011module IRTS.Lang where
1112
src/IRTS/Portable.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE OverloadedStrings #-}
8+{-# LANGUAGE FlexibleInstances, OverloadedStrings, TypeSynonymInstances #-}
99module IRTS.Portable (writePortable) where
1010
1111import Idris.Core.CaseTree
src/IRTS/Simplified.hs+1
@@ -5,6 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleContexts #-}
89module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
910
1011import Idris.Core.CaseTree
src/Idris/AbsSyntax.hs+1−1
@@ -6,7 +6,7 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE DeriveFunctor, PatternGuards #-}
9+{-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternGuards #-}
1010
1111module Idris.AbsSyntax(
1212 module Idris.AbsSyntax
src/Idris/AbsSyntaxTree.hs+10−1
@@ -6,7 +6,9 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
9+{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric,
10+ DeriveTraversable, FlexibleContexts, FlexibleInstances,
11+ MultiParamTypeClasses, PatternGuards, TypeSynonymInstances #-}
1012
1113module Idris.AbsSyntaxTree where
1214
@@ -1047,6 +1049,7 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
10471049 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
10481050 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
10491051 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1052+ mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
10501053mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
10511054mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
10521055mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
@@ -1171,6 +1174,7 @@ data PDo' t = DoExp FC t
11711174 | DoBindP FC t t [(t,t)]
11721175 | DoLet FC Name FC t t -- ^ second FC is precise name location
11731176 | DoLetP FC t t
1177+ | DoRewrite FC t -- rewrite in do block
11741178 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
11751179{-!
11761180deriving instance Binary PDo'
@@ -1182,6 +1186,7 @@ instance Sized a => Sized (PDo' a) where
11821186 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
11831187 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
11841188 size (DoLetP fc l r) = 1 + size fc + size l + size r
1189+ size (DoRewrite fc h) = 1 + size fc + size h
11851190
11861191type PDo = PDo' PTerm
11871192
@@ -1277,6 +1282,7 @@ highestFC (PDoBlock lines) =
12771282 getDoFC (DoBindP fc l r alts) = fc
12781283 getDoFC (DoLet fc nm nfc l r) = fc
12791284 getDoFC (DoLetP fc l r) = fc
1285+ getDoFC (DoRewrite fc h) = fc
12801286
12811287highestFC (PIdiom fc _) = Just fc
12821288highestFC (PMetavar fc _) = Just fc
@@ -1951,6 +1957,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
19511957 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
19521958 text "no pretty printer for pattern-matching do binding" :
19531959 ppdo bnd dos
1960+ ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab
1961+ text "no pretty printer for pattern-matching do binding" :
1962+ ppdo bnd dos
19541963 ppdo _ [] = []
19551964 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
19561965 prettySe d p bnd (PElabError s) = pretty s
src/Idris/Apropos.hs+1
@@ -5,6 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleInstances #-}
89module Idris.Apropos (apropos, aproposModules) where
910
1011import Idris.AbsSyntax
src/Idris/CaseSplit.hs+1−1
@@ -17,7 +17,7 @@ Always take the "more specific" argument when there is a discrepancy, i.e.
1717names over '_', patterns over names, etc.
1818-}
1919
20−{-# LANGUAGE PatternGuards #-}
20+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
2121
2222module Idris.CaseSplit(
2323 splitOnLine, replaceSplits
src/Idris/Chaser.hs+2
@@ -5,6 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleContexts #-}
9+
810module Idris.Chaser(
911 buildTree, getImports
1012 , getModuleFiles
src/Idris/Core/Binary.hs+2
@@ -5,6 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleInstances #-}
9+
810{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
911module Idris.Core.Binary where
1012
src/Idris/Core/CaseTree.hs+2−2
@@ -18,8 +18,8 @@ allows casing on arbitrary terms, here we choose to maintain the distinction
1818in order to allow for better optimisation opportunities.
1919
2020-}
21−{-# LANGUAGE DeriveFunctor, DeriveGeneric, PatternGuards, TypeSynonymInstances
22− #-}
21+{-# LANGUAGE DeriveFunctor, DeriveGeneric, FlexibleContexts, FlexibleInstances,
22+ PatternGuards, TypeSynonymInstances #-}
2323
2424module Idris.Core.CaseTree (
2525 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo
src/Idris/Core/DeepSeq.hs+2−1
@@ -5,7 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE BangPatterns, CPP, ViewPatterns #-}
8+{-# LANGUAGE BangPatterns, CPP, FlexibleInstances, TypeSynonymInstances,
9+ ViewPatterns #-}
910{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1011
1112module Idris.Core.DeepSeq where
src/Idris/Core/ProofState.hs+2−1
@@ -10,7 +10,8 @@ proofs, and some high level commands for introducing new theorems,
1010evaluation/checking inside the proof system, etc.
1111-}
1212
13−{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}
13+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
14+ PatternGuards #-}
1415module Idris.Core.ProofState(
1516 ProofState(..), newProof, envAtFocus, goalAtFocus
1617 , Tactic(..), Goal(..), processTactic, nowElaboratingPS
src/Idris/Core/TT.hs+4−2
@@ -22,8 +22,10 @@ TT is the core language of Idris. The language has:
2222 * We have a simple collection of tactics which we use to elaborate source
2323 programs with implicit syntax into fully explicit terms.
2424-}
25−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, FlexibleContexts,
26− FunctionalDependencies, MultiParamTypeClasses, PatternGuards #-}
25+{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric,
26+ DeriveTraversable, FlexibleContexts, FlexibleInstances,
27+ FunctionalDependencies, MultiParamTypeClasses, PatternGuards,
28+ TypeSynonymInstances #-}
2729{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2830module Idris.Core.TT(
2931 AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)
src/Idris/Core/Typecheck.hs+2−2
@@ -6,8 +6,8 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,
10− PatternGuards #-}
9+{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances,
10+ MultiParamTypeClasses, PatternGuards #-}
1111
1212module Idris.Core.Typecheck where
1313
src/Idris/Core/Unify.hs+1−1
@@ -11,7 +11,7 @@ Returns a list of hole names paired with the term which solves them, and
1111a list of things which need to be injective.
1212
1313-}
14−{-# LANGUAGE PatternGuards #-}
14+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
1515
1616module Idris.Core.Unify(
1717 match_unify, unify
src/Idris/Core/WHNF.hs+1−1
@@ -6,7 +6,7 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE PatternGuards #-}
9+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
1010{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1111module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where
1212
src/Idris/Coverage.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
99module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,
1010 mkPatTm) where
1111
src/Idris/DSL.hs+2
@@ -109,6 +109,8 @@ expandSugar dsl (PDoBlock ds)
109109 = PLet fc n nfc ty tm (block b rest)
110110 block b (DoLetP fc p tm : rest)
111111 = PCase fc tm [(p, block b rest)]
112+ block b (DoRewrite fc h : rest)
113+ = PRewrite fc Nothing h (block b rest) Nothing
112114 block b (DoExp fc tm : rest)
113115 = PApp fc b
114116 [pexp tm,
src/Idris/DataOpts.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleInstances, PatternGuards #-}
99
1010module Idris.DataOpts(applyOpts) where
1111
src/Idris/Docstrings.hs+2−1
@@ -6,7 +6,8 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE DeriveFunctor, DeriveGeneric, ScopedTypeVariables #-}
9+{-# LANGUAGE DeriveFoldable, DeriveFunctor, DeriveGeneric, DeriveTraversable,
10+ ScopedTypeVariables #-}
1011{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1112module Idris.Docstrings (
1213 Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring
src/Idris/Elab/Quasiquote.hs+1
@@ -75,6 +75,7 @@ extractDoUnquotes d (DoLet fc n nfc v b)
7575 (b', ex2) <- extractUnquotes d b
7676 return (DoLet fc n nfc v' b', ex1 ++ ex2)
7777extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
78+extractDoUnquotes d (DoRewrite fc h) = fail "Rewrites in Do block cannot be quasiquoted"
7879
7980
8081extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
src/Idris/Elab/Utils.hs+7−6
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
99module Idris.Elab.Utils where
1010
1111import Idris.AbsSyntax
@@ -449,9 +449,12 @@ displayWarnings est
449449 = mapM_ displayImpWarning (implicit_warnings est)
450450 where
451451 displayImpWarning :: (FC, Name) -> Idris ()
452− displayImpWarning (fc, n) =
453− iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"
454− ++ "\tDid you mean to refer to " ++ show n ++ "?"
452+ displayImpWarning (fc, n) = do
453+ ist <- getIState
454+ let msg = show (nsroot n)
455+ ++ " is bound as an implicit\n"
456+ ++ "\tDid you mean to refer to " ++ show n ++ "?"
457+ iWarn fc (pprintErr ist (Msg msg))
455458
456459propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
457460propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)
@@ -767,5 +770,3 @@ isPlausible ist var env n ty
767770 collectConstraints env tcs t
768771 | (V i, _) <- unApply t = (Just (env !! i), tcs)
769772 | otherwise = (Nothing, tcs)
770−
771−
src/Idris/Error.hs+1
@@ -138,6 +138,7 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
138138 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
139139 wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
140140 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
141+ wStep (DoRewrite _ h) = warnDisamb ist h
141142warnDisamb ist (PIdiom _ x) = warnDisamb ist x
142143warnDisamb ist (PMetavar _ _) = return ()
143144warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
src/Idris/IBC.hs+9−2
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE TypeSynonymInstances #-}
8+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
99{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1010
1111module Idris.IBC (loadIBC, loadPkgIndex,
@@ -48,7 +48,7 @@ import System.Directory
4848import System.FilePath
4949
5050ibcVersion :: Word16
51−ibcVersion = 160
51+ibcVersion = 161
5252
5353-- | When IBC is being loaded - we'll load different things (and omit
5454-- different structures/definitions) depending on which phase we're in.
@@ -2293,6 +2293,9 @@ instance (Binary t) => Binary (PDo' t) where
22932293 put x1
22942294 put x2
22952295 put x3
2296+ DoRewrite x1 x2 -> do putWord8 5
2297+ put x1
2298+ put x2
22962299 get
22972300 = do i <- getWord8
22982301 case i of
@@ -2319,6 +2322,10 @@ instance (Binary t) => Binary (PDo' t) where
23192322 x2 <- get
23202323 x3 <- get
23212324 return (DoLetP x1 x2 x3)
2325+ 5 -> do
2326+ x1 <- get
2327+ x2 <- get
2328+ return (DoRewrite x1 x2)
23222329 _ -> error "Corrupted binary data for PDo'"
23232330
23242331
src/Idris/IdrisDoc.hs+1
@@ -344,6 +344,7 @@ extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps
344344 in concatMap extract (p1 : p2 : ps')
345345extractPDo (DoLet _ n _ p1 p2) = n : concatMap extract [p1, p2]
346346extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]
347+extractPDo (DoRewrite _ p) = extract p
347348
348349-- | Helper function for extractPTermNames
349350extractPTactic :: PTactic -> [Name]
src/Idris/Output.hs+1
@@ -6,6 +6,7 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9+{-# LANGUAGE FlexibleInstances #-}
910{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1011
1112module Idris.Output where
src/Idris/Package/Parser.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE CPP, ConstraintKinds #-}
8+{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}
99module Idris.Package.Parser where
1010
1111import Idris.AbsSyntaxTree
src/Idris/Parser.hs+7−2
@@ -5,7 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}
8+{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
9+ PatternGuards #-}
910{-# OPTIONS_GHC -O0 #-}
1011module Idris.Parser(module Idris.Parser,
1112 module Idris.Parser.Expr,
@@ -1569,7 +1570,8 @@ parseImports fname input
15691570 [ImportInfo],
15701571 Maybe Delta),
15711572 [(FC, OutputAnnotation)], IState)
1572− imports = do whiteSpace
1573+ imports = do optional shebang
1574+ whiteSpace
15731575 (mdoc, mname, annots) <- moduleHeader
15741576 ps_exp <- many import_
15751577 mrk <- mark
@@ -1594,6 +1596,9 @@ parseImports fname input
15941596 (fc, AnnNamespace ns (Just path)) : addPath annots path
15951597 addPath (annot:annots) path = annot : addPath annots path
15961598
1599+ shebang :: IdrisParser ()
1600+ shebang = string "#!" *> many (satisfy $ not . isEol) *> eol *> pure ()
1601+
15971602-- | There should be a better way of doing this...
15981603findFC :: Doc -> (FC, String)
15991604findFC x = let s = show (plain x) in findFC' s
src/Idris/Parser/Expr.hs+7
@@ -234,6 +234,7 @@ updateSynMatch = update
234234 = DoBindP fc (update ns i) (update ns t)
235235 (map (\(l,r) -> (update ns l, update ns r)) ts)
236236 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
237+ upd ns (DoRewrite fc h) = DoRewrite fc (update ns h)
237238 update ns (PIdiom fc t) = PIdiom fc $ update ns t
238239 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)
239240 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
@@ -1343,6 +1344,7 @@ doBlock syn
13431344Do ::=
13441345 'let' Name TypeSig'? '=' Expr
13451346 | 'let' Expr' '=' Expr
1347+ | 'rewrite Expr
13461348 | Name '<-' Expr
13471349 | Expr' '<-' Expr
13481350 | Expr
@@ -1367,6 +1369,11 @@ do_ syn
13671369 sc <- expr syn
13681370 highlightP kw AnnKeyword
13691371 return (DoLetP fc i sc))
1372+ <|> try (do kw <- reservedFC "rewrite"
1373+ fc <- getFC
1374+ sc <- expr syn
1375+ highlightP kw AnnKeyword
1376+ return (DoRewrite fc sc))
13701377 <|> try (do (i, ifc) <- name
13711378 symbol "<-"
13721379 fc <- getFC
src/Idris/Parser/Helpers.hs+3−2
@@ -5,8 +5,9 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE CPP, ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards,
9− StandaloneDeriving #-}
8+{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances,
9+ GeneralizedNewtypeDeriving, PatternGuards, StandaloneDeriving,
10+ TypeSynonymInstances #-}
1011module Idris.Parser.Helpers where
1112
1213import Idris.AbsSyntax
src/Idris/Parser/Ops.hs+2−1
@@ -5,7 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}
8+{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
9+ PatternGuards #-}
910module Idris.Parser.Ops where
1011
1112import Idris.AbsSyntax
src/Idris/PartialEval.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
99
1010module Idris.PartialEval(
1111 partial_eval, getSpecApps, specType
src/Idris/Prover.hs+1
@@ -350,6 +350,7 @@ elabloop info fn d prompt prf e prev h env
350350 Success (Right cmd') ->
351351 case cmd' of
352352 DoLetP {} -> ifail "Pattern-matching let not supported here"
353+ DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"
353354 DoBindP {} -> ifail "Pattern-matching <- not supported here"
354355 DoLet fc i ifc Placeholder expr ->
355356 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
src/Idris/REPL.hs+1−1
@@ -5,7 +5,7 @@ License : BSD3
55Maintainer : The Idris Community.
66-}
77
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
99
1010module Idris.REPL
1111 ( idemodeStart
src/Util/Pretty.hs+3
@@ -5,6 +5,9 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+
9+{-# LANGUAGE MultiParamTypeClasses #-}
10+
811module Util.Pretty (
912 module Text.PrettyPrint.Annotated.Leijen
1013 , Sized(..)
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_18.ghc;
5+ resolver = haskell.packages.lts-9_0.ghc;
66
77 native_libs = [
88 libffi
stack.yaml+1−1
@@ -1,4 +1,4 @@
1−resolver: lts-8.18
1+resolver: lts-9.0
22
33packages:
44 - location: .
test/basic009/expected+1−1
@@ -1,5 +1,5 @@
11MAIN-PASS
2−Faulty.idr:6:9-12:WARNING: num is bound as an implicit
2+Faulty.idr:6:9-12:num is bound as an implicit
33 Did you mean to refer to A.num?
44Faulty.idr:7:7:When checking right hand side of fault with expected type
55 num = 0
test/basic018/expected+4−2
@@ -1,6 +1,8 @@
1−basic018.idr:7:12-17:WARNING: thing is bound as an implicit
1+basic018.idr:7:12-17:
2+thing is bound as an implicit
23 Did you mean to refer to Main.thing?
3−basic018.idr:12:8-13:WARNING: thing is bound as an implicit
4+basic018.idr:12:8-13:
5+thing is bound as an implicit
46 Did you mean to refer to Main.thing?
57basic018.idr:13:6:When checking right hand side of test with expected type
68 thing = S 41
test/interactive017/TestMod.idrnew file+5
@@ -0,0 +1,5 @@
1+module TestMod
2+
3+export
4+test : IO ()
5+test = putStrLn "Hello from a module"
test/interactive017/expectednew file+7
@@ -0,0 +1,7 @@
1+hello from C
2+hello from C
3+hello from node
4+hello from node
5+Hello ["aaa"]
6+Hello ["bbb", "aaa"]
7+Hello from a module
test/interactive017/runnew file+9
@@ -0,0 +1,9 @@
1+#!/bin/sh
2+PATH="../../scripts:$PATH"
3+./shebang.idr
4+./shebang.idr
5+./shebang-node.idr
6+./shebang-node.idr
7+./shebang-args.idr aaa
8+./shebang-args.idr bbb aaa
9+./shebang-import.idr
test/interactive017/shebang-args.idrnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env runidris
2+
3+main : IO ()
4+main = do
5+ args <- getArgs
6+ putStrLn $ "Hello " ++ (show $ drop 1 args)
test/interactive017/shebang-import.idrnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env runidris
2+
3+import TestMod
4+
5+main : IO ()
6+main = TestMod.test
test/interactive017/shebang-node.idrnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env runidris-node
2+
3+main : IO ()
4+main = putStrLn "hello from node"
test/interactive017/shebang.idrnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env runidris
2+
3+main : IO ()
4+main = putStrLn "hello from C"
test/regression002/expected+2−1
@@ -110,7 +110,8 @@ reg068.idr:1:6:Main.nat has a name which may be implicitly bound.
110110This is likely to lead to problems!
111111reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
112112This is likely to lead to problems!
113−reg068.idr:2:8-11:WARNING: nat is bound as an implicit
113+reg068.idr:2:8-11:
114+nat is bound as an implicit
114115 Did you mean to refer to Main.nat?
115116reg068.idr:2:6:When checking constructor Main.ze:
116117Type level variable nat is not Main.nat