04b4cc0 · Idris-dev · git.iko.soy

contribs/gtksourceview-2.0-language-spec/idris.langdeleted−254

@@ -1,254 +0,0 @@

1−<?xml version="1.0" encoding="UTF-8"?>

2−<!--

3−

4− Author: Dominic Mulligan

6−

7− Lexemes taken from src/Idris/Parser.hs.

8−

9− Based on the gtksourceview-2.0 Haskell style by:

10−

11− Authors: Duncan Coutts, Anders Carlsson

14−

15− This library is free software; you can redistribute it and/or

16− modify it under the terms of the GNU Library General Public

17− License as published by the Free Software Foundation; either

18− version 2 of the License, or (at your option) any later version.

19−

20− This library is distributed in the hope that it will be useful,

21− but WITHOUT ANY WARRANTY; without even the implied warranty of

22− MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU

23− Library General Public License for more details.

24−

25− You should have received a copy of the GNU Library General Public

26− License along with this library; if not, write to the

27− Free Software Foundation, Inc., 59 Temple Place - Suite 330,

28− Boston, MA 02111-1307, USA.

29−

30−-->

31−<language id="idris" _name="Idris" version="2.0" _section="Sources">

32− <metadata>

33− <property name="mimetypes">text/x-idris</property>

34− <property name="globs">*.idr</property>

35− </metadata>

36−

37− <styles>

38− <style id="preprocessor" _name="Preprocessor" map-to="def:preprocessor"/>

39− <style id="comment" _name="Comment" map-to="def:comment"/>

40− <style id="variable" _name="Variable" />

41− <style id="symbol" _name="Symbol" />

42− <style id="keyword" _name="Keyword" map-to="def:keyword"/>

43− <style id="tactic" _name="Tactic" map-to="def:keyword"/>

44− <style id="type" _name="Data Type" map-to="def:type"/>

45− <style id="string" _name="String" map-to="def:string"/>

46− <style id="character" _name="Character" map-to="def:character"/>

47− <style id="char-escape" _name="Escaped Character" map-to="def:special-char"/>

48− <style id="decimal" _name="Decimal" map-to="def:decimal"/>

49− <style id="float" _name="Float" map-to="def:floating-point"/>

50− </styles>

51−

52− <definitions>

53− <define-regex id="symbolchar">[!#$%&*+./>=<?@:\\^|~-]</define-regex>

54−

55− <context id="line-comment" style-ref="comment" end-at-line-end="true" class="comment" class-disabled="no-spell-check">

56− <start>(?<!\%{symbolchar})--+(?!\%{symbolchar})</start>

57− <include>

58− <context ref="def:in-comment"/>

59− <context ref="haddock:line-paragraph"/>

60− <context ref="haddock:directive"/>

61− </include>

62− </context>

63−

64− <context id="block-comment" style-ref="comment" class="comment" class-disabled="no-spell-check">

65− <start>\{-</start>

66− <end>-\}</end>

67− <include>

68− <context ref="def:in-comment"/>

69− <context ref="haddock:block-paragraph"/>

70− <context ref="haddock:directive"/>

71− <context ref="block-comment"/>

72− </include>

73− </context>

74−

75− <context id="variable" style-ref="variable">

76− <match>\b[a-z_][0-9a-zA-Z_'#]*</match>

77− </context>

78−

79− <context id="type-or-constructor" style-ref="type">

80− <match>\b[A-Z][0-9a-zA-Z._'#]*</match>

81− </context>

82−

83− <context id="symbol" style-ref="symbol" extend-parent="false">

84− <match>\%{symbolchar}+</match>

85− </context>

86−

87− <context id="keysymbol" style-ref="keyword">

88− <prefix>(?<!\%{symbolchar})</prefix>

89− <suffix>(?!\%{symbolchar})</suffix>

90− <keyword>\.</keyword>

91− <keyword>:</keyword>

92− <keyword>%</keyword>

93− <keyword>=</keyword>

94− <keyword>\|</keyword>

95− <keyword>\</keyword>

96− <keyword>-></keyword>

97− <keyword>@</keyword>

98− <keyword>~</keyword>

99− <keyword>=></keyword>

100− <keyword></keyword>

101− <keyword>\_\|\_</keyword>

102− <keyword>\*\*</keyword>

103− </context>

104−

105− <define-regex id="escaped-character" extended="true">

106− \\( # leading backslash

107− [abfnrtv\\"\'&] | # escaped character

108− [0-9]+ | # decimal digits

109− o[0-7]+ | # 'o' followed by octal digits

110− x[0-9A-Fa-f]+ | # 'x' followed by hex digits

111− \^[A-Z@\[\\\]^_] | # control character codes

112− NUL | SOH | STX | ETX | EOT | ENQ | ACK |

113− BEL | BS | HT | LF | VT | FF | CR | SO |

114− SI | DLE | DC1 | DC2 | DC3 | DC4 | NAK |

115− SYN | ETB | CAN | EM | SUB | ESC | FS | GS |

116− RS | US | SP | DEL # control char names

117− )

118− </define-regex>

119−

120− <context id="string" style-ref="string" end-at-line-end="true" class="string" class-disabled="no-spell-check">

121− <start>"</start>

122− <end>"</end>

123− <include>

124− <context ref="def:line-continue"/>

125− <context style-ref="char-escape">

126− <match>\%{escaped-character}</match>

127− </context>

128− </include>

129− </context>

130−

131− <context id="char" style-ref="character" end-at-line-end="true">

132− <start>'</start>

133− <end>'</end>

134− <include>

135− <context style-ref="char-escape" once-only="true">

136− <match>\%{escaped-character}</match>

137− </context>

138− <context once-only="true" extend-parent="false">

139− <match>.</match>

140− </context>

141− <context style-ref="def:error" extend-parent="false">

142− <match>.</match>

143− </context>

144− </include>

145− </context>

146−

147− <context id="float" style-ref="float">

148− <match extended="true">

149− [0-9]+ \. [0-9]+ ([eE][+-]?[0-9]+)?

150− | [0-9]+ [eE][+-]?[0-9]+

151− </match>

152− </context>

153−

154− <context id="decimal" style-ref="decimal">

155− <match>[0-9]+</match>

156− </context>

157−

158− <context id="keyword" style-ref="keyword">

159− <keyword>Set</keyword>

160− <keyword>case</keyword>

161− <keyword>class</keyword>

162− <keyword>data</keyword>

163− <keyword>default</keyword>

164− <keyword>do</keyword>

165− <keyword>record</keyword>

166− <keyword>foreign</keyword>

167− <keyword>lib</keyword>

168− <keyword>link</keyword>

169− <keyword>include</keyword>

170− <keyword>hide</keyword>

171− <keyword>freeze</keyword>

172− <keyword>access</keyword>

173− <keyword>logging</keyword>

174− <keyword>abstract</keyword>

175− <keyword>public</keyword>

176− <keyword>private</keyword>

177− <keyword>namespace</keyword>

178− <keyword>syntax</keyword>

179− <keyword>term</keyword>

180− <keyword>pattern</keyword>

181− <keyword>params</keyword>

182− <keyword>import</keyword>

183− <keyword>using</keyword>

184− <keyword>in</keyword>

185− <keyword>infix</keyword>

186− <keyword>infixl</keyword>

187− <keyword>infixr</keyword>

188− <keyword>prefix</keyword>

189− <keyword>instance</keyword>

190− <keyword>let</keyword>

191− <keyword>module</keyword>

192− <keyword>of</keyword>

193− <keyword>if</keyword>

194− <keyword>else</keyword>

195− <keyword>then</keyword>

196− <keyword>where</keyword>

197− <keyword>with</keyword>

198− <keyword>type</keyword>

199− <keyword>proof</keyword>

200− <keyword>tactics</keyword>

201− <keyword>static</keyword>

202− <keyword>impossible</keyword>

203− <keyword>total</keyword>

204− <keyword>assert_total</keyword>

205− </context>

206−

207− <context id="tactic" style-ref="tactic">

208− <keyword>rewrite</keyword>

209− <keyword>exact</keyword>

210− <keyword>intros</keyword>

211− <keyword>intro</keyword>

212− <keyword>refine</keyword>

213− <keyword>trivial</keyword>

214− <keyword>focus</keyword>

215− <keyword>try</keyword>

216− <keyword>compute</keyword>

217− <keyword>solve</keyword>

218− <keyword>attack</keyword>

219− <keyword>Refl</keyword>

220− <keyword>state</keyword>

221− <keyword>term</keyword>

222− <keyword>undo</keyword>

223− <keyword>qed</keyword>

224− <keyword>abandon</keyword>

225− </context>

226−

227− <context id="body">

228− <include>

229− <context ref="line-comment"/>

230− <context ref="block-comment"/>

231− <context ref="keyword"/>

232− <context ref="tactic" />

233− <context ref="variable"/>

234− <context ref="type-or-constructor"/>

235− <context ref="keysymbol"/>

236− <context ref="symbol"/>

237− <context ref="string"/>

238− <context ref="char"/>

239− <context ref="float"/>

240− <context ref="decimal"/>

241− </include>

242− </context>

243−

244− <context id="idris" class="no-spell-check">

245− <include>

246− <context ref="c:if0-comment"/>

247− <context ref="c:include"/>

248− <context ref="c:preprocessor"/>

249− <context ref="body"/>

250− </include>

251− </context>

252−

253− </definitions>

254−</language>

contribs/idriscasesplit.vimdeleted−100

@@ -1,100 +0,0 @@

1−function IdrisReload()

2− let file = expand("%")

3− let tc = system("idris --client :l " . file)

4− if (! (tc is ""))

5− echo tc

6− endif

7− return tc

8−endfunction

9−

10−function IdrisShowType()

11− w

12− let word = expand("<cword>")

13− let tc = IdrisReload()

14− if (! (tc is ""))

15− echo tc

16− else

17− let ty = system("idris --client :t " . word)

18− echo ty

19− endif

20− return tc

21−endfunction

22−

23−function IdrisCaseSplit()

24− let view = winsaveview()

25− w

26− let cline = line(".")

27− let word = expand("<cword>")

28− let tc = IdrisReload()

29−

30− if (tc is "")

31− let fn = "idris --client :cs! " . cline . " " . word

32− let result = system(fn)

33− if (! (result is ""))

34− echo result

35− else

36− e

37− call winrestview(view)

38− endif

39− endif

40−endfunction

41−

42−function IdrisMakeWith()

43− let view = winsaveview()

44− w

45− let cline = line(".")

46− let word = expand("<cword>")

47− let tc = IdrisReload()

48−

49− if (tc is "")

50− let fn = "idris --client :mw! " . cline . " " . word

51− let result = system(fn)

52− if (! (result is ""))

53− echo result

54− else

55− e

56− call winrestview(view)

57− call search("_")

58− endif

59− endif

60−endfunction

61−

62−function IdrisAddClause()

63− let view = winsaveview()

64− w

65− let cline = line(".")

66− let word = expand("<cword>")

67− let tc = IdrisReload()

68−

69− if (tc is "")

70− let fn = "idris --client :ac! " . cline . " " . word

71− let result = system(fn)

72− if (! (result is ""))

73− echo result

74− else

75− e

76− call winrestview(view)

77− call search(word)

78−

79− endif

80− endif

81−endfunction

82−

83−function IdrisEval()

84− let tc = IdrisReload()

85− if (tc is "")

86− let expr = input ("Expression: ")

87− let fn = "idris --client '" . expr . "'"

88− let result = system(fn)

89− echo result

90− endif

91− echo ""

92−endfunction

93−

94−map <LocalLeader>t :call IdrisShowType()<ENTER>

95−map <LocalLeader>r :call IdrisReload()<ENTER>

96−map <LocalLeader>c :call IdrisCaseSplit()<ENTER>

97−map <LocalLeader>d ?:<ENTER>b:call IdrisAddClause()<ENTER>w

98−map <LocalLeader>w 0:call IdrisMakeWith()<ENTER>

99−map <LocalLeader>e :call IdrisEval()<ENTER>

100−

contribs/idrislang.stydeleted−159

@@ -1,159 +0,0 @@

1−%% --------------------------------------------------- [ Idris Styling Package ]

2−%%

3−%% A set of LaTeX macros and styling for working with Idris in LaTeX

4−%%

5−%% + Provides a listings bindings:

6−%% + idris :: default ascii

7−%% + literateidris :: convert ascii maths to math symbols.

8−%% + Defines a `numbers', `default', and `stdout' listings style.

9−%% + default :: Uses TT font for code and SF font for comments,

10−%% and indented by parident.

11−%% + numbers :: default but with numbers.

12−%% + beamer :: default minus parindent

13−%% + stdout :: for formatting stdout.

14−%% + Defines a `code' environment for typesetting idris.

15−%% + \begin{code}[...] ... \end{code}

16−%% + Defines an input command for externally defined idris files.

17−%% + \inputIdrisListing[...]{file.idr}

18−%% + Provides definitions (from Idris Compiler) for pretty-printing Idris

19−%% code using Fancy Verbatim and colour commands.

20−%% + Sets commandchars for latex commands.

21−%% + Defines commands typesetting the name Idris.

22−%% + \Idris{}

23−%% + \idris{}

24−%%

25−%% Options:

26−%% - literate :: turn on literate idris for code environments.

27−%%

28−%% ----------------------------------------------------------- [ Begin Package ]

29−\ProvidesPackage{idrislang}

30−

31−\RequirePackage{ifthen}

32−\RequirePackage{xcolor}

33−\RequirePackage{fancyvrb}

34−\RequirePackage{listings}

35−\RequirePackage{xspace}

36−\RequirePackage{textcomp}

37−\RequirePackage{setspace}

38−%% ----------------------------------------------------------------- [ Options ]

39−\newboolean{literate}

40−\setboolean{literate}{false}

41−

42−\DeclareOption{literate}{%

43− \setboolean{literate}{true}

44−}

45−

46−\ProcessOptions\relax

47−

48−%% ---------------------------------------------------------------- [ Commands ]

49−\newcommand{\Idris}{\textsc{Idris}\xspace}

50−\newcommand{\idris}{\textsc{Idris}\xspace}

51−\newcommand{\IdrisLineSpacing}{\singlespacing}

52−%% ---------------------------------------------------------- [ Color Commands ]

53−\newcommand{\IdrisData}[1]{\textcolor{red}{#1}}

54−\newcommand{\IdrisType}[1]{\textcolor{blue}{#1}}

55−\newcommand{\IdrisBound}[1]{\textcolor{magenta}{#1}}

56−\newcommand{\IdrisFunction}[1]{\textcolor{green}{#1}}

57−\newcommand{\IdrisKeyword}[1]{{\underline{#1}}}

58−\newcommand{\IdrisImplicit}[1]{{\itshape \IdrisBound{#1}}}

59−

60−\fvset{commandchars=\\\{\}}

61−

62−%% --------------------------------------------------- [ Define Idris Listings ]

63−\lstdefinelanguage{idris}{%

64− sensitive,%

65−%% ----------------------------------------------------------- [ Default Style ]

66− xleftmargin=1.5em,

67− tabsize=2,

68− upquote=true,

69− basicstyle=\ttfamily,

70− flexiblecolumns=false,

71− commentstyle=\footnotesize\sffamily,

72−%% ---------------------------------------------------------------- [ Keywords ]

73−%% From Idris Parser and idris-mode and vimscript

74− keywords={%

75− abstract, attack, case, compute, do, dsl, else, exact, focus, if,

76− import, in, infix, infixl, infixr, instance, intros, module,

77− mutual, namespace, of, let, parameters, partial, pattern, prefix,

78− private, public, refine, rewrite, solve, syntax, term, then,

79− total, trivial, try, using, where, with

80−},

81−%% ------------------------------------------------------- [ Prelude Functions ]

82− morekeywords={%

83− class, data, instance, record, dsl, postulate, default,

84− lambda, variable, index_first, index_next

85− },

86−%% ---------------------------------------------------------------- [ Comments ]

87− morecomment=[l]--,%

88− morecomment=[n]{\{-}{-\}}

89−}[keywords,comments,strings]%

90−

91−%% ---------------------------------------- [ Define Idris with Literate Stuff ]

92−\lstdefinelanguage{literateidris}[]{idris}{

93− literate= {+}{{$+$}}1

94− {/}{{$/$}}1

95− {*}{{$*$}}1

96− {=}{{$=$}}1

97− {>}{{$>$}}1

98− {<}{{$<$}}1

99− {\\}{{$\lambda$}}1

100− {\\\\}{{\char`\\\char`\\}}1

101− {->}{{$\rightarrow$}}2

102− {>=}{{$\geq$}}2

103− {<-}{{$\leftarrow$}}2

104− {<=}{{$\leq$}}2

105− {=>}{{$\Rightarrow$}}2

106− {==}{{$\equiv$}}2

107− {\ .}{{$\circ$}}2

108− {\ .\ }{{$\circ$}}2

109− {>>}{{>>}}2

110− {>>=}{{>>=}}2

111− {|}{{$\mid$}}1,

112−}

113−%% -------------------------------------------------- [ Default Listings Style ]

114−

115−\lstdefinestyle{default}{%

116− basicstyle=\ttfamily\normalsize,

117−}

118−

119−\lstdefinestyle{numbers}{%

120− numbers=left,

121− numbersep=10pt,

122− numberstyle=\footnotesize\sffamily,

123− frame=leftline

124−}

125−

126−\lstdefinestyle{stdout}{%

127− xleftmargin=\parindent,

128− tabsize=2,

129− basicstyle=\ttfamily\normalsize,

130− showstringspaces=false,

131− escapechar=^

132−}

133−

134−\lstdefinestyle{beamer}{%

135− basicstyle=\ttfamily\normalsize,

136− escapechar=^

137−}

138−

139−%% ------------------------------------------------------ [ A Code Environment ]

140−%% Replicate the existence of literate haskell code environments,

141−%% option to make pretty with numbers.

142−\lstnewenvironment{code}[1][]

143− {\ifthenelse{\boolean{literate}}{%

144− \lstset{language=literateidris}}{%

145− \lstset{language=idris}}

146− \IdrisLineSpacing{}

147− }{}

148−%% ---------------------------------------------------------- [ Input Listings ]

149−%% Command to add externally defined Idris code to the document.

150−\newcommand{\inputIdrisListing}[2][]{%

151−\begingroup

152− \ifthenelse{\boolean{literate}}{%

153− \lstset{language=literateidris}}{%

154− \lstset{language=idris}}

155− \lstinputlisting[#1]{#2}

156−\endgroup

157−}

158−\endinput

159−%% --------------------------------------------------------------------- [ EOF ]

contribs/lib/SQLite3/Makefiledeleted−15

@@ -1,15 +0,0 @@

1−# This makefile compiles the project

2−#

3−

4−.PHONY: all

5−

6−sqltest : testunit.idr Sqlite3.idr sqlite3api.o

7− idris testunit.idr -o sqltest

8−

9−sqlite3api.o : sqlite3api.c

10− gcc -I . -c sqlite3api.c

11−

12−sqlite3api.so: sqlite3api.c

13− gcc -I . -fPIC -o sqlite3api.so -shared sqlite3api.c

14−

15−all : sqltest sqlite3api.o

contribs/lib/SQLite3/Sqlexpr.idrdeleted−278

@@ -1,278 +0,0 @@

1−module Sqlexpr

2−import Prelude.List

3−

4−-----------------------------------------------------------------------------

5−-- |

6−-- Module : sqlexpr

7−-- Copyright : (c) The University of St Andrews, 2012

8−--

9−-- Implementations for SQLite query data type.

10−--

11−-----------------------------------------------------------------------------

12−

13−

14−-----------------------------------------------------------

15−-- | SQL data type

16−-----------------------------------------------------------

17−

18−data Value = VInt Int

19− | VStr String

20− | VFloat Float

21− | VCol String

22− | VNULL

23−

24−--Perhaps could extend this by adding

25−-- a dot operator to allow mapping

26−-- between table and column and

27−-- comparing different table columns.

28−

29−data Cond = Equals Value Value

30− | MkGT Value Value

31− | MkGTE Value Value

32− | MkLT Value Value

33− | MkLTE Value Value

34− | MkNULL Value

35−

36−data SelVar = Cols (List String)

37− | ALL

38−

39−data ColType = CInt String -- parsed as string "int"

40− | Varchar String

41−

42−

43−

44−mutual

45− data Clause = MkCond Cond

46− | AND Clause Clause

47− | OR Clause Clause

48− | Empty

49− | MkSQL SQL

50−

51− data condClause = SET Clause

52− | WHERE condClause Clause

53−

54− data Constr = NOTNULL

55− | UNIQUE Constr

56− | None

57− | PRIMARYKEY

58− | FOREIGNKEY

59− | CHECK

60− | DEFAULT

61−

62−

63− data SQL = SELECT SelVar SQL Clause

64− | TBL (List String)

65− | INSERT SQL (List Value)

66− | INSERTC SQL (List Value) (List Value)

67− | UPDATE SQL condClause

68− | CREATE SQL (List (Value, ColType , Constr))

69−

70−-- remember to remove these funcs later

71−-- foldr1 : (a -> a -> a) -> List a -> a

72−-- foldr1 f [x] = x

73−-- foldr1 f (x::xs) = f x (foldr1 f xs)

74−

75−

76−-- unwords' : List (List Char) -> List Char

77−-- unwords' [] = []

78−-- unwords' ws = (foldr1 addSpace ws)

79−-- where

80−-- addSpace : List Char -> List Char -> List Char

81−-- addSpace w s = w ++ (' ' :: s)

82−--

83−--

84−-- unwords : List String -> String

85−-- unwords = pack . unwords' . map unpack

86−

87−-----------------------------------------------------------

88−-- | This function replaces values with question mark

89−-- following by an index number. It then puts the value

90−-- replaced, in the list.

91−-----------------------------------------------------------

92−

93−valString : List (Maybe (Int, Value)) -> Value -> (String, List (Maybe (Int, Value)))

94−valString xs (VInt x) = ("?" ++ show (cast (length xs) + 1), xs ++ [Just (cast ((length xs) + 1), (VInt x))])

95−valString xs (VStr x) = ("?" ++ show (cast (length xs) + 1), xs ++ [Just (cast ((length xs) + 1), (VStr x))])

96−valString xs (VFloat x) = ("?" ++ show (cast (length xs) + 1), xs ++ [Just (cast ((length xs) + 1), (VFloat x))])

97−valString xs (VCol n) = (n, xs)

98−

99−-----------------------------------------------------------

100−-- | This function calls valString on a list of Values

101−-- and separates the values by commas.

102−-----------------------------------------------------------

103−

104−listVal : List (Maybe (Int, Value)) -> List Value -> (String, List (Maybe (Int, Value)))

105−listVal xs [] = ("", xs)

106−listVal xs (v::vs) = let (str, newxs) = (valString xs v) in

107− let (str', newxs') = listVal newxs vs in

108− (unwords (intersperse "," (words (str) ++ words (str'))), newxs')

109−

110−-----------------------------------------------------------

111−-- | Parses the type of column to be created.

112−-----------------------------------------------------------

113−

114−getColType : List (Maybe (Int, Value)) -> ColType -> (String, List (Maybe (Int, Value)))

115−getColType xs (CInt x) = ("int", xs)

116−getColType xs (Varchar str) = ("varchar(255)", xs)

117−

118−-----------------------------------------------------------

119−-- | CREATE Constraints

120−-----------------------------------------------------------

121−

122−getConstr : List (Maybe (Int, Value)) -> Constr -> (String, List (Maybe (Int, Value)))

123−getConstr xs (NOTNULL) = ("NOT NULL", xs)

124−getConstr xs (UNIQUE constr) = ("NOT NULL UNIQUE", xs)

125−getConstr xs (PRIMARYKEY) = ("PRIMARY KEY", xs)

126−getConstr xs (FOREIGNKEY) = ("FOREIGN KEY", xs)

127−getConstr xs (CHECK) = ("CHECK", xs)

128−getConstr xs (DEFAULT) = ("DEFAULT", xs)

129−getConstr xs (None) = ("", xs)

130−

131−putBrackets : String -> String

132−putBrackets str = "(" ++ str ++ ")"

133−

134−-----------------------------------------------------------

135−-- | Used to detect a complex type in a nested SQLite query

136−-- This function is used for bracketing the nested queries.

137−-----------------------------------------------------------

138−complexType : SQL -> Bool

139−complexType (TBL tbl) = False

140−complexType (SELECT vars sql c) = True

141−

142−-----------------------------------------------------------

143−-- | Used in CREATE

144−-----------------------------------------------------------

145−

146−listValType : List (Maybe (Int, Value)) -> List (Value, ColType , Constr) -> (String, List (Maybe (Int, Value)))

147−listValType xs [] = ("", xs)

148−listValType xs ((val, types, constr) :: vs) =

149− let (str , newxs) = valString xs val in

150− let (str' , newxs') = getColType newxs types in

151− let (str'', newxs'') = getConstr newxs' constr in

152− let (finalstr, finalxs) = listValType newxs'' vs in

153− (unwords (intersperse " " (words str ++ words str' ++ words str'' ++ words finalstr)) , finalxs)

154−

155−

156−-----------------------------------------------------------

157−-- | Evaluates a conditional WHERE clause

158−-----------------------------------------------------------

159−

160−evalCond : List (Maybe (Int, Value)) -> Cond -> (String, List (Maybe (Int, Value)))

161−evalCond xs (Equals val1 val2) = let (restring , newxs ) = valString xs val1 in

162− let (restring2, newxs') = valString newxs val2 in

163− (restring ++ " = " ++ restring2, newxs')

164−

165−evalCond xs (MkGT val1 val2) = let (restring , newxs ) = valString xs val1 in

166− let (restring2, newxs') = valString newxs val2 in

167− (restring ++ " > " ++ restring2, newxs')

168−

169−evalCond xs (MkGTE val1 val2) = let (restring , newxs ) = valString xs val1 in

170− let (restring2, newxs') = valString newxs val2 in

171− (restring ++ " >= " ++ restring2, newxs')

172−

173−evalCond xs (MkLT val1 val2) = let (restring , newxs ) = valString xs val1 in

174− let (restring2, newxs') = valString newxs val2 in

175− (restring ++ " < " ++ restring2, newxs')

176−

177−evalCond xs (MkLTE val1 val2) = let (restring , newxs ) = valString xs val1 in

178− let (restring2, newxs') = valString newxs val2 in

179− (restring ++ " =< " ++ restring2, newxs')

180−

181−evalCond xs (MkNULL val) = let (restring , newxs ) = valString xs val in

182− (restring ++ " IS NULL " , newxs)

183−

184−

185−-----------------------------------------------------------

186−-- | Evaluates clauses

187−-- Supports WHERE Clause

188−-- WHERE Clause And Another-Clause

189−-- WHERE Clause Or Another-Clause

190−-----------------------------------------------------------

191−clauseString : List (Maybe (Int, Value)) -> Clause -> (String, List (Maybe (Int, Value)))

192−

193−clauseString xs (Empty) = ("" , []) -- No condition

194−clauseString xs (MkCond cond') = let (condstr, newxs) = evalCond xs cond' in

195− (condstr , newxs)

196−

197−clauseString xs (AND c1 c2) = let (clausestr, newxs) = clauseString xs c1 in

198− let (clausestr2, newxs') = clauseString newxs c2 in

199− (clausestr ++ " AND " ++ clausestr2 , newxs')

200−

201−clauseString xs (OR c1 c2) = let (clausestr, newxs) = clauseString xs c1 in

202− let (clausestr2, newxs') = clauseString newxs c2 in

203− (clausestr ++ " OR " ++ clausestr2 , newxs')

204−

205−

206−-----------------------------------------------------------

207−-- | Evaluates conditional clauses.

208−-----------------------------------------------------------

209−

210−condClauseStr : List (Maybe (Int, Value)) -> condClause -> (String, List (Maybe (Int, Value)))

211−condClauseStr xs (SET setcl) = let (condstr, newxs) = clauseString xs setcl in

212− (" SET " ++ condstr, newxs)

213−

214−condClauseStr xs (WHERE setcl1 setcl2) = let (condstr, newxs) = condClauseStr xs setcl1 in

215− let (condstr', newxs') = clauseString newxs setcl2 in

216− ( condstr ++ " WHERE " ++ condstr', newxs')

217−

218−

219−-----------------------------------------------------------

220−-- | Evaluates queries by calling the other functions

221−-- on each part of the query

222−-----------------------------------------------------------

223−evalSQL : List (Maybe (Int, Value)) -> SQL -> (String, List (Maybe (Int, Value)))

224−-- SELECT data from tbl1 where num > (SELECT num from tbl1 where num = 24)

225−-- evalSQL [] ((SELECT ALL)(TBL "tbl")(MkSQL ((SELECT ALL) (TBL "tbl")(MkCond (VCol "))))

226−-- NTBF

227−--clauseString xs (MkSQL sql) = (evalSQL xs sql)

228−

229−-- Separate list of tables

230−-- For complex type, return list returned by evalSQL

231−-- And add brackets

232−evalSQL xs (TBL tbl) = (unwords (intersperse "," ( tbl)), xs)

233−evalSQL xs (SELECT vars sql' c) =

234− let (sqlstring, newxs) = evalSQL xs sql' in

235− let (csstring, newxs') = clauseString newxs c in

236− case c of

237− Empty => case vars of

238− ALL => if complexType sql'

239− then ("SELECT " ++ "*" ++ " FROM " ++

240− putBrackets sqlstring ++ csstring, newxs)

241− else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring ++

242− csstring, newxs')

243− Cols selvar => if complexType sql'

244− then ("SELECT " ++ unwords selvar ++

245− " FROM " ++ putBrackets sqlstring ++ csstring, newxs)

246− else ("SELECT " ++ unwords selvar ++ " FROM " ++ sqlstring ++

247− csstring, newxs')

248− _ => case vars of

249− ALL => if complexType sql'

250− then ("SELECT " ++ "*" ++ " FROM " ++

251− " WHERE " ++ csstring, newxs)

252− else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring

253− ++ " WHERE " ++ csstring, newxs')

254− Cols selvar => if complexType sql'

255− then ("SELECT " ++ (unwords selvar) ++ " FROM " ++

256− putBrackets sqlstring ++ " WHERE " ++

257− csstring , newxs)

258− else ("SELECT " ++ (unwords selvar) ++ " FROM " ++ sqlstring ++

259− " WHERE " ++ csstring, newxs')

260−

261−

262−evalSQL xs (INSERT sql vals) = let (tblname, newvals) = evalSQL xs sql in

263− let (str, newxs ) = listVal newvals vals in

264− ("INSERT INTO " ++ tblname ++ " VALUES (" ++ str ++ ")", newxs)

265−

266−evalSQL xs (INSERTC sql cols vals) = let (tblname, newvals) = evalSQL xs sql in

267− let (strcol, newcol) = listVal newvals cols in

268− let (strval, newcolval) = listVal newcol vals in

269− ("INSERT INTO " ++ tblname ++ "(" ++ strcol ++ ")" ++ "VALUES (" ++ strval ++ ")", newcolval)

270−

271−

272−evalSQL xs (UPDATE sql cl) = let (tblname, newxs) = evalSQL xs sql in

273− let (csstring, newxs') = condClauseStr newxs cl in

274− ("UPDATE " ++ tblname ++ csstring, newxs')

275−

276−evalSQL xs (CREATE sql details) = let (sqlstring, newxs) = evalSQL xs sql in

277− let (csstring, newxs') = listValType newxs details in

278− ("CREATE TABLE " ++ sqlstring ++ "(" ++ csstring ++ ")", newxs')

contribs/lib/SQLite3/Sqlite3.idrdeleted−419

@@ -1,419 +0,0 @@

1−module Sqlite3

2−import public Sqlexpr

3−

4−%lib C "sqlite3"

5−-- %link C "sqlite3.o"

6−-- %include C "sqlite3.h"

7−%link C "sqlite3api.o"

8−%include C "sqlite3api.h"

9−

10−-----------------------------------------------------------------------------

11−-- |

12−-- Module : sqlite3

13−-- Copyright : (c) The University of St Andrews, 2012

14−--

15−-- Library built on top of FFI supporting basic SQLite C/C++ Interface

16−-- functions.

17−--

18−-----------------------------------------------------------------------------

19−

20−-- | The types supported by Idris returned by the database functions.

21−

22−data DBVal = DBInt Int

23− | DBText String

24− | DBFloat Float

25− | DBNull

26−

27−-- Database pointer

28−data DBPointer = MkDBPointer Ptr

29−-- Table pointer

30−data TBPointer = MkTBPointer Ptr

31−-- Statement pointer

32−data StmtPtr = MkStmtPtr Ptr

33−

34−Table : Type

35−Table = List (List DBVal)

36−

37−-- ForMap used in to_list_v1

38−forM : Applicative f => List a -> (a -> f b) -> f (List b)

39−forM xs f = (sequence (map f xs))

40−

41−-- Neater error handling done using DB

42−data DB a = MkDB (IO (Either String a))

43−

44−instance Functor DB where

45− map f (MkDB action) = MkDB (do res <- action

46− return (map f res))

47−

48−

49−instance Applicative DB where

50− pure = MkDB . return . Right

51− (MkDB f) <*> (MkDB x) = MkDB (do f' <- f

52− case f' of

53− Left err => return (Left err)

54− Right op => x >>= (return . map op))

55−

56−

57−instance Monad DB where

58− (MkDB l) >>= k = MkDB (do c <- l

59− case c of

60− Left err => return (Left err)

61− Right v => case k v of

62− MkDB k' => k')

63− --return x = MkDB (return (Right x))

64−

65−fail : String -> DB a

66−fail err = MkDB (return (Left err))

67−

68−liftIO : IO a -> DB a

69−liftIO f = MkDB (do f' <- f

70− return (Right f'))

71−

72−ioError : String -> IO a

73−ioError err = do putStrLn err

74− return (believe_me ())

75−

76−runDB : DB a -> IO a

77−runDB (MkDB f) = do f' <- f

78− case f' of

79− Right v => return v

80− Left str => ioError str

81−

82−-----------------------------------------------------------------------------

83−-- | Opens an SQLite database file as specified by the String name argument.

84−-----------------------------------------------------------------------------

85−

86−open_db : String -> DB DBPointer

87−open_db name = do x <- liftIO (foreign FFI_C "sqlite3_open_idr" (String -> IO Ptr) name)

88− return (MkDBPointer x)

89−

90−-----------------------------------------------------------------------------

91−-- | Destructor for the DBPointer.

92−-----------------------------------------------------------------------------

93−

94−close_db : DBPointer -> DB Int

95−close_db (MkDBPointer pointer) = liftIO (foreign FFI_C "sqlite3_close_idr" (Ptr -> IO Int) pointer)

96−

97−-----------------------------------------------------------------------------

98−-- | Wrapper around prepare, step and finalize.

99−-----------------------------------------------------------------------------

100−

101−exec_db : DBPointer -> String -> DB Int

102−exec_db (MkDBPointer pointer) stmt = do

103− x <- liftIO (foreign FFI_C "sqlite3_exec_idr" (Ptr -> String -> IO Int) pointer stmt)

104− if (x == 1)

105− then fail "Could not execute."

106− else return x

107−

108−-----------------------------------------------------------------------------

109−-- | Executes a prepared query. Use of this version is recommended.

110−-----------------------------------------------------------------------------

111−

112−exec_db_v2 : StmtPtr -> DB Int

113−exec_db_v2 (MkStmtPtr pointer) = do

114− x <- liftIO (foreign FFI_C "exec_db" (Ptr -> IO Int) pointer)

115− if (x == 21)

116− then fail "No data returned."

117− else return x

118−

119−-----------------------------------------------------------------------------

120−-- | Returns the error stored in the buffer by exec_db function.

121−-- This function can only be used with exec_db and get_table.

122−-- Only these functions store any occured error in the buffer array.

123−-----------------------------------------------------------------------------

124−

125−get_error : DBPointer -> IO String

126−get_error (MkDBPointer pointer) = foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer

127−

128−-----------------------------------------------------------------------------

129−-- | Compiles the query inot a byte-code program in order to execute it.

130−-- Returns a pointer to a Statement pointer on a successful call.

131−-- Returns a null pointer on a failure.

132−-----------------------------------------------------------------------------

133−

134−prepare_db : DBPointer -> String -> DB StmtPtr

135−prepare_db (MkDBPointer pointer) cmd = do

136− result <- liftIO (foreign FFI_C "sqlite3_prepare_idr" (Ptr -> String -> IO Ptr) pointer cmd)

137− flag <- liftIO (nullPtr result)

138− if flag

139− then fail "Error occured while preparing"

140− else return (MkStmtPtr result)

141−

142−-----------------------------------------------------------------------------

143−-- | Returns the error stored in the buffer by exec_db function.

144−-- This function can only be used with exec_db and get_table.

145−-- Only these functions store any occured error in the buffer array.

146−-----------------------------------------------------------------------------

147−

148−step_db : StmtPtr -> DB Int

149−step_db (MkStmtPtr pointer)= do

150− x <- liftIO (foreign FFI_C "sqlite3_step_idr" (Ptr -> IO Int) pointer)

151− if (x == 101)

152− then fail "SQLITE_DONE"

153− else return x

154−

155−-----------------------------------------------------------------------------

156−-- | Deletes a prepared statement. This function must be called after

157−-- prepare function.

158−-----------------------------------------------------------------------------

159−

160−finalize_db : StmtPtr -> DB Int

161−finalize_db (MkStmtPtr pointer) = do

162− x <- liftIO (foreign FFI_C "sqlite3_finalize_idr" (Ptr -> IO Int) pointer)

163− if (x /= 0)

164− then fail "Could not finalize"

165− else return x

166−

167−-----------------------------------------------------------------------------

168−-- | Resets a prepared statement pointer back to its initial state.

169−-----------------------------------------------------------------------------

170−

171−reset_db : StmtPtr -> DB Int

172−reset_db (MkStmtPtr pointer) = do

173− x <- liftIO (foreign FFI_C "sqlite3_reset_idr" (Ptr -> IO Int) pointer)

174− if (x /= 0)

175− then fail "Could not reset"

176− else return x

177−

178−-----------------------------------------------------------------------------

179−-- | These routines obtain column information.

180−-----------------------------------------------------------------------------

181−

182−column_count : DBPointer -> IO (Either String Int)

183−column_count (MkDBPointer pointer) = do

184− x <- foreign FFI_C "sqlite3_column_count_idr" (Ptr -> IO Int) pointer

185− return $ if (x == 0)

186− then Left "No Data"

187− else (Right x)

188−

189−column_name : DBPointer -> Int -> IO String

190−column_name (MkDBPointer pointer) iCol =

191− foreign FFI_C "sqlite3_column_name_idr" (Ptr -> Int -> IO String) pointer iCol

192−

193−column_decltype : DBPointer -> Int -> IO String

194−column_decltype (MkDBPointer pointer) iCol =

195− foreign FFI_C "sqlite3_column_decltype_idr" (Ptr -> Int -> IO String) pointer iCol

196−

197−column_bytes : DBPointer -> Int -> IO Int

198−column_bytes (MkDBPointer pointer) iCol =

199− foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO Int) pointer iCol

200−

201−column_blob : DBPointer -> Int -> IO String

202−column_blob (MkDBPointer pointer) iCol =

203− foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO String) pointer iCol

204−

205−column_text : DBPointer -> Int -> IO String

206−column_text (MkDBPointer pointer) iCol =

207− foreign FFI_C "sqlite3_column_text_idr" (Ptr -> Int -> IO String) pointer iCol

208−

209−column_Int : DBPointer -> Int -> IO Int

210−column_Int (MkDBPointer pointer) iCol =

211− foreign FFI_C "sqlite3_column_int_idr" (Ptr -> Int -> IO Int) pointer iCol

212−

213−-----------------------------------------------------------------------------

214−-- | These routines support some of SQLite backup functions.

215−-----------------------------------------------------------------------------

216−

217−backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer

218−backup_init (MkDBPointer des_pointer) destName (MkDBPointer src_pointer) srcName =

219− do x <- foreign FFI_C "sqlite3_backup_init_idr" (Ptr -> String -> Ptr -> String -> IO Ptr)

220− des_pointer destName src_pointer srcName

221− return (MkDBPointer x)

222−

223−backup_step : DBPointer -> Int -> IO Int

224−backup_step (MkDBPointer pointer) nPage =

225− foreign FFI_C "sqlite3_backup_step_idr" (Ptr -> Int -> IO Int) pointer nPage

226−

227−backup_finish : DBPointer -> IO Int

228−backup_finish (MkDBPointer pointer) =

229− foreign FFI_C "sqlite3_backup_finish_idr" (Ptr -> IO Int) pointer

230−

231−backup_remaining : DBPointer -> IO Int

232−backup_remaining (MkDBPointer pointer) =

233− foreign FFI_C "sqlite3_backup_remaining_idr" (Ptr -> IO Int) pointer

234−

235−-----------------------------------------------------------------------------

236−-- | Use of this interface is not recommended.

237−-- This function returns a result table. The functions num_row and num_col

238−-- are used to obtain the number of rows and columns.

239−-- These functions can be used to print the resulting table.

240−-----------------------------------------------------------------------------

241−

242−get_table : DBPointer -> String -> DB TBPointer

243−get_table (MkDBPointer pointer) name = do

244− x <- liftIO(foreign FFI_C "sqlite3_get_table_idr" (Ptr -> String -> IO Ptr) pointer name)

245− flag <- liftIO (nullPtr x)

246− if flag

247− then do x <- liftIO(get_error_table pointer) ; fail x

248− else return (MkTBPointer x)

249− where

250− get_error_table : Ptr-> IO String

251− get_error_table pointer = do x <- foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer

252− return x

253−

254−free_table : TBPointer -> IO ()

255−free_table (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_free_table_idr" (Ptr -> IO ()) pointer

256− return ()

257−

258−-----------------------------------------------------------------------------

259−-- | This version of these function obtain the row and column number

260−-- from the Table struct. These functions are only used with get_table.

261−-----------------------------------------------------------------------------

262−

263−num_row : TBPointer -> IO Int

264−num_row (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row" (Ptr -> IO Int) pointer

265− return x

266−

267−num_col : TBPointer -> IO Int

268−num_col (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col" (Ptr -> IO Int) pointer

269− return x

270−

271−-----------------------------------------------------------------------------

272−-- | This version of these function obtain the row and column number

273−-- from the Database struct.

274−-----------------------------------------------------------------------------

275−

276−num_row_v2 : DBPointer -> IO Int

277−num_row_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row_v2" (Ptr -> IO Int) pointer

278− return x

279−

280−num_col_v2 : DBPointer -> IO Int

281−num_col_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col_v2" (Ptr -> IO Int) pointer

282− return x

283−

284−-----------------------------------------------------------------------------

285−-- | This function prints the result of a query by checking the type

286−-- of each value returned, it then calls the appropriate function.

287−-- Ther result is one of the DBVal variants.

288−-----------------------------------------------------------------------------

289−

290−get_data : DBPointer -> Int -> Int -> IO DBVal

291−get_data (MkDBPointer pointer) row col = do

292− ty <- get_data_type pointer row col

293− helper ty

294− where get_data_type : Ptr ->Int -> Int -> IO Int

295− get_data_type pointer row col =

296− foreign FFI_C "sqlite3_get_data_type" (Ptr -> Int -> Int -> IO Int) pointer row col

297− get_data_val_int : Ptr -> Int -> IO Int

298− get_data_val_int pointer col =

299− foreign FFI_C "sqlite3_get_val_int" (Ptr -> Int -> IO Int) pointer col

300−

301− get_data_val_text : Ptr -> Int -> IO String

302− get_data_val_text pointer col =

303− foreign FFI_C "sqlite3_get_val_text" (Ptr -> Int -> IO String) pointer col

304−

305− get_data_val_float : Ptr -> Int -> IO Float

306− get_data_val_float pointer col =

307− foreign FFI_C "sqlite3_get_float" (Ptr -> Int -> IO Float) pointer col

308−

309− helper : Int -> IO DBVal

310− helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)

311− helper 2 = do i <- get_data_val_float pointer col ; return (DBFloat i)

312− helper 3 = do i <- get_data_val_text pointer col; return (DBText i)

313− helper _ = return DBNull

314−

315−-----------------------------------------------------------------------------

316−-- | This function makes use of get_data to get all the result.

317−-----------------------------------------------------------------------------

318−

319−toList_v1 : DBPointer -> DB Table

320−toList_v1 db = do nbR <- liftIO (num_row_v2 db)

321− nmC <- liftIO (num_col_v2 db)

322− res <- liftIO $ forM [0..(nbR-1)] $ \ i =>

323− forM [0..(nmC-1)] $ \ j => get_data db i j

324− return (the (List (List DBVal)) res)

325−

326−strcat : String -> String-> String

327−strcat str1 str2 = str1 ++ str2

328−

329−-----------------------------------------------------------------------------

330−-- | This version of toList retunrs result from get_table

331−-- This could be removed if not needed in the future.

332−-----------------------------------------------------------------------------

333−

334−--toList_v2 : String -> String -> DBPointer -> DB Table

335−--toList_v2 name stmt x = do

336−-- ptr <- (get_table x (stmt))

337−-- nbR <- liftIO (num_row ptr)

338−-- nmC <- liftIO (num_col ptr)

339−-- res <- forM [0..(nbR-1)] (\ i =>

340−-- forM [0..(nmC-1)] (\ j =>

341−-- liftIO(get_data x name i j)

342−--

343−-- )

344−-- )

345−-- liftIO (free_table ptr)

346−-- return res

347−

348−

349−-----------------------------------------------------------------------------

350−-- | These routines support binding the types supported by Idris.

351−-- These return a pointer to statement pointer since we want to allow

352−-- binding multiple values by implementing a recursive function.

353−-----------------------------------------------------------------------------

354−

355−bind_int : StmtPtr -> Int -> Int -> DB StmtPtr

356−bind_int (MkStmtPtr pointer) indexval val = do

357− x <- liftIO (foreign FFI_C "sqlite3_bind_int_idr" (Ptr -> Int -> Int -> IO Ptr) pointer indexval val)

358− flag <- liftIO (nullPtr x)

359− if flag

360− then fail "Could not bind int."

361− else return (MkStmtPtr x)

362−

363−

364−bind_float : StmtPtr -> Int -> Float -> DB StmtPtr

365−bind_float (MkStmtPtr pointer) indexval val = do

366− x <- liftIO (foreign FFI_C "sqlite3_bind_float_idr" (Ptr -> Int -> Float -> IO Ptr) pointer indexval val)

367− flag <- liftIO (nullPtr x)

368− if flag

369− then fail "Could not bind float."

370− else return (MkStmtPtr x)

371−

372−bind_text : StmtPtr -> String -> Int -> Int -> DB StmtPtr

373−bind_text (MkStmtPtr pointer) text indexval lengthval = do

374− x <- liftIO (foreign FFI_C "sqlite3_bind_text_idr" (Ptr -> String -> Int -> Int -> IO Ptr)

375− pointer text indexval lengthval)

376− flag <- liftIO(nullPtr x)

377− if flag

378− then fail "Could not bind text."

379− else return (MkStmtPtr x)

380−

381−bind_null : StmtPtr -> Int -> DB StmtPtr

382−bind_null (MkStmtPtr pointer) indexval = do

383− x <- liftIO (foreign FFI_C "sqlite3_bind_null_idr" (Ptr -> Int -> IO Ptr) pointer indexval)

384− flag <- liftIO (nullPtr x)

385− if flag

386− then fail "Could not bind null."

387− else return (MkStmtPtr x)

388−

389−-----------------------------------------------------------------------------

390−-- | String Length

391−-----------------------------------------------------------------------------

392−

393−strlen : String -> DB Int

394−strlen str = liftIO (foreign FFI_C "strLength" (String -> IO Int) str)

395−

396−instance Show DBVal where

397− show (DBInt i) = "Int val: " ++ show i ++ "\n"

398− show (DBText i) = "Text val: " ++ show i ++ "\n"

399− show (DBFloat i) = "Float val: " ++ show i ++ "\n"

400− show (DBNull ) = "NULL"

401−

402−-----------------------------------------------------------------------------

403−-- | Multi bind a list of values.

404−-----------------------------------------------------------------------------

405−

406−bindMulti : StmtPtr-> List (Maybe (Int, Value)) -> DB StmtPtr

407−bindMulti pointer [] = return pointer

408−bindMulti pointer (Nothing :: vs) = bindMulti pointer vs

409−bindMulti pointer ((Just (indexs, (VInt i)))::vs) =

410− do x <- bind_int pointer indexs i

411− bindMulti x vs

412−bindMulti pointer ((Just (indexs, (VStr s)))::vs) =

413− do len <- strlen s

414− x <- bind_text pointer s indexs len

415− bindMulti x vs

416−bindMulti pointer ((Just (indexs, (VFloat f)))::vs) =

417− do x <- bind_float pointer indexs f

418− bindMulti x vs

419−

contribs/lib/SQLite3/newdb.dbdeleted

Binary file not shown.

contribs/lib/SQLite3/somedb.dbdeleted

Binary file not shown.

contribs/lib/SQLite3/sqlite3.texdeleted−157

@@ -1,157 +0,0 @@

1− \documentclass[11pt]{article}

2− \topmargin -1.5cm

3− \oddsidemargin -0.04cm

4− \evensidemargin -0.04cm

5− \textwidth 16.59cm

6− \textheight 21.94cm

7− %\pagestyle{empty}

8− \parskip 7.2pt

9− \parindent 0pt

10−

11− \begin{document}

12− \section{Introduction}

13−\label{Introduction}

14−This document provides overview on how the Idris library for SQLite3 works. The code base is written on top of the

15−SQLite3 C/C++ Interface.

16−This library supports some features of the low-level library, implemented in a higher level basis.

17−The library allows making use of queries as data types. The aim of this library is to avoid

18−SQL injections which are the most common security issues.

19−To avoid this we have defined a datatype which describes queries.

20−The queries are written using these data types and parsed as quoted string

21−while replacing values with \emph{indexed question mark} to be binded with the prepared statement.

22−This prevents the user from preparing the queries inappropriately by not allowing to pass

23−any types of values directly to the prepare function. However this is a design choice, the library

24−does not prevent the user from passing a String directly to the prepare function.

25−

26−\section{Using the library}

27−\label{Using the library}

28−Simple examples have been provided in the \emph{testunit.idr} file.

29−To open a database, use the open\_db function which takes the filename as a string.

30−This function implements the sqlite3\_open function.

31−This function returns a pointer to the database which can be used by other function

32−to access the database object.

33−Whether or not an error occurs when it is opened,

34−resources should be released by passing it to close\_db when it is no longer required.

35−A query can then be builts using the supported data types.

36−The library supports limited number of queries at the moment. The supported sql commands are :

37−\newline

38−

39−\textbf{SELECT,}

40−\textbf{INSERT,}

41−\textbf{UPDATE,}

42−\textbf{CREATE}

43−

44−\subsection{Creating Queries}

45−\label{Creating Queries}

46−

47−To create a query, use the evalSQL function which takes an empty list and the SQL query.

48−The routine evaluates the expression recrusively by dividing it into smaller parts,

49−filling up the list with the received values. For instance the following is a valid query:

50−

51−let sql = evalSQL [ ] ((SELECT ALL)(TBL ["tbl1"]) (MkCond (MkNULL (VCol "data"))))

52−\newline

53−\newline{This will be parsed as :}

54−\b{“SELECT * FROM tbl1 WHERE data IS NULL “}

55−

56−The evaluator returns a string and a list of indexed values.

57−The string part of the query could be parsed to prepare.

58−\emph{evalSQL} parses the query as a string replacing values with \emph{?} and an index starting from one,

59−storing them in the list given to it as an argument.

60−For example:

61−

62−

63−evalSQL [ ] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL ["tbl1"])

64−\newline (MkCond(Equals(VCol "num")(VInt 2))))Empty))

65−

66−is passed to prepare as :

67−

68−SELECT * FROM tbl1 WHERE data = ?1 AND num = ?2 OR num = ?3

69−

70−and returns the list as follows:

71−\newline{(Just (1, VStr "data0")) ,(Just (2, VInt 1)) , (Just (3, VInt 2))}

72−

73−The values in the list are binded to the statement using bindMulti function.

74−This function takes the statement pointer returned by prepare and the list returned by evalSQL

75−and binds the values by calling the appropriate functions.

76−

77−The function exec\_db\_v2 executes the statement.

78−Note that the other version of exec\_db implements the sqlite3\_exec() interface which is a wrapper

79−around sqlite3\_prepare\_v2(), sqlite3\_step(), and sqlite3\_finalize(),

80−without having to use a lot of code, though the use of this function is not recommended in this case.

81−

82−The functions finalize\_db and close\_db must be called to clean up the open resources.

83−To print the result, the function toList\_v1 can be used which takes a DBPointer and returns

84−the resulting table.

85−

86−\subsection{More Examples}

87−\label{More Examples}

88−Nested expressions are also supported. You could write queries such as :

89−

90−evalSQL [ ] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL ["tbl1"]) (MkCond (Equals (VCol "num")(VInt 2)))) Empty)

91−

92−Parsed as :

93−

94−SELECT data FROM (SELECT num data FROM tbl1 WHERE num = ?1)

95−

96−Note that in this example, the inner query must include the same column as the outer one otherwise this query will not validate.

97−

98−\subsection{SQL Data Type}

99−\label{SQL Data Type}

100−The SQL Data Types describe the queries that are supported by the library.

101−The implementation of these datatypes is similar to defining a grammar.

102−Data type Value consists of Int, String and Float.

103−The data type can be extended to further support queries.

104−The evaulator function makes use of smaller function to evaulate parts of the query.

105−For instance given a SELECT qeury, it calls \emph{evalSQL} to obtain the list of tables,

106−and clauseString to evaluate the rest of the expression which could include a WHERE clause or could be Empty.

107−

108−

109−\section{Evaluating Queries}

110−\label{Evaluating Queries}

111−The method used here is a divide and conquer manner which divides the query into smaller

112−parts and deals with each part and puts the results together to return a String representation

113−of the query and a list of values.

114−However this could result to a slow type checking process since it needs to go through all

115−the possibilities to type check. Maybe this can be improved?

116−

117−\subsection{evalSQL Function}

118−\label{evalSQL Function}

119−This is a recursive evaluator which makes a call to itself.

120−An SQL could consist of a SELECT ALL or Columns followed by another SQL

121−which could be a nested query or just the name of the table(s).

122−It then call the appropriate functions to evaluate the query.

123−It returns the well-quoted String expression and a list of indexed values which are passed to the bind function.

124−\section{Pointers passed to Idris functions}

125−\label{Pointers passed to Idris functions}

126−

127−The library uses FFI. In order to make the pointers passed to each function more explicit,

128−we have defined them as data types. For instance open\_db takes a String and returns a DBPointer

129−(Database Pointer) and prepare\_db

130−takes a DBPointer and returns a StmtPtr(Statemenet Pointer).

131−Error handling is done using the \emph {DB a} data type which

132−is either \emph {IO String} indicating an error or \emph{ IO a}.

133−To test the functions in main, you need to use runDB :

134−\begin{center}

135−\centering runDB : DB a $\rightarrow$ IO a

136−\end{center}

137−More examples on how to use the functions can be found in \emph{testunit.idr}

138−

139−\section{Using the C Functions}

140−\label{Using the C Functions}

141−The library includes some wrapper functions such as get\_table

142−and exec\_db. Using these functions mixed with prepare, step or finalize

143−inappropriately could cause segmentation faults.

144−Perhaps these functions could be removed from the library if no longer required in the future

145−since the main purpose of this library is to make use of data types.

146−However these functionalities could be implemented internally without calling

147−the C Interface wrapper functions.

148−

149−\section{Further improving the library}

150−\label{Further improving the library}

151−There are many features that could be added to this library. These include adding more useful SQL Commands,

152−extending the SQL datatype to support more complex queries and possibly improving \emph{evalSQL}

153−for a faster performance.

154−Another useful thing to implement is the dot operator(.) which is the member access operator to yield

155−the value of a field in a table. This enables comparing values in different tables and constructing

156−more complex queries.

157−\end{document}

contribs/lib/SQLite3/sqlite3api.cdeleted−543

@@ -1,543 +0,0 @@

1−/*

2− * sqlite3api.c

3− *

4− *

5− * Created by Melissa Farinaz MOZIFIAN on 22/06/2012.

7− *

8− */

9−

10−

11−#include "sqlite3api.h"

12−

13−

14−// buffer used for storing queries

15−// Used in high-level functions.

16−static char sql_query_buffer[2000];

17−// array used to store the string

18−//value obtain by get_val_text

19−unsigned char* array;

20−/*

21− open an SQLite database file as

22− specified by the filename argument.

23− Returns pointer to DB struct on success

24− Null on failure.

25− */

26−void* sqlite3_open_idr(const char *filename){

27−

28− sqlite3 *db;

29− int res =sqlite3_open(filename,&db);

30−

31− if(res != SQLITE_OK){

32− printf("Error occured while opening the databse.");

33− return NULL;

34− }

35− DBinfo *dbi = malloc(sizeof(DBinfo));

36− dbi->db_ptr = db;

37− return dbi;

38−

39−}

40−/*

41− Frees the resource and returns 0 on success

42− */

43−int sqlite3_close_idr(void* db){

44−

45− DBinfo* dbi =(DBinfo*) db;

46− int res =sqlite3_close(dbi->db_ptr);

47− if (res == SQLITE_OK){

48− free(dbi);

49− return 0;

50− }

51− else {

52− return res;

53− }

54−}

55−/*

56− SQLite wrapper around sqlite3_prepare_v2(),

57− sqlite3_step(), and sqlite3_finalize().

58− This version of exec cannot be used with prepare.

59− For executing queries, must use the exec_db function.

60− */

61−int sqlite3_exec_idr(void* db, const char *sql)

62−{

63− DBinfo* dbi =(DBinfo*) db;

64− char* err;

65− int rc;

66− rc = sqlite3_exec(dbi->db_ptr,sql,NULL, NULL, &err);

67− if (rc != SQLITE_OK && err != NULL) {

68− strncpy(dbi->buffer, err, sizeof(dbi->buffer));

69− sqlite3_free(err);

70− }

71− return rc;

72−}

73−/*

74− Gets the error store in the buffer

75− in the struct. Some certain functions

76− have the feature to store errors in a buffer.

77− */

78−char* sqlite3_get_error(void* db) {

79− DBinfo* dbi =(DBinfo*) db;

80− return dbi->buffer;

81−}

82−/*

83− Compiles the query into a byte-code program

84− Returns a pointer to the sqlite3_stmt pointer

85− and stores it in the struct.

86− */

87−void* sqlite3_prepare_idr(void *db,const char *zSql){

88− sqlite3_stmt* stmt;

89− const char *tail;

90−

91− DBinfo* dbi =(DBinfo*) db;

92−

93− int rec = sqlite3_prepare_v2(dbi->db_ptr,zSql,-1,&stmt,&tail);

94− dbi ->ppStmt =stmt;

95− dbi ->Ptr_tail = tail;

96−

97− if(rec != SQLITE_OK){

98− return NULL;

99− }

100− return dbi;

101−}

102−/*

103− Another wrapper interface that is preserved

104− for backwards compatibility.

105− Use of this interface is not recommended.

106− This was mainly used for testing within the

107− library.

108− */

109−void* sqlite3_get_table_idr(void* db,

110− const char *sql){

111−

112− DBinfo* dbi =(DBinfo*) db;

113− char* err;

114−

115− Table* tbl = malloc(sizeof(Table));

116− tbl->database = dbi;

117− int res = sqlite3_get_table(dbi->db_ptr,sql,&tbl->table_data,&tbl->num_row,&tbl->num_col,&err);

118− int array_size = sizeof(&tbl->table_data);

119−

120− if( res != SQLITE_OK && err != NULL){

121− strncpy(dbi->buffer, err, sizeof(dbi->buffer));

122− sqlite3_free(err);

123− return NULL;

124− }

125− tbl -> data_size = array_size;

126− return tbl;

127−}

128−

129−/*

130− This function executes queries.

131− This can be used after preparing a query

132− In case of error or library misuse

133− it returns 1.

134− It also calls step in order to obtain

135− the row and column number and stores them

136− in the struct. The row number is needed

137− later on in get_data_type function.

138− */

139−int exec_db(void*p){

140−

141− DBinfo* dbi =(DBinfo*) p;

142− int rc, col, row_counter;

143−

144− const char* col_name;

145−

146− rc = sqlite3_step(dbi->ppStmt);

147−

148− if( rc == SQLITE_DONE){

149− return rc;

150− }

151− if(rc == SQLITE_ERROR && rc == SQLITE_MISUSE){

152− return 1;

153− }

154− row_counter =0;

155−

156− while (rc == SQLITE_ROW) {

157−

158− rc = sqlite3_step(dbi->ppStmt);

159− row_counter++;

160− }

161−

162− col = sqlite3_column_count(dbi->ppStmt);

163− dbi->row_count = row_counter;

164− dbi->col_count = col;

165− return rc;

166−}

167−/*

168− Returns row number from DB Struct

169−

170− */

171−int sqlite3_get_num_row_v2(void* p){

172−

173− DBinfo* dbi =(DBinfo*) p;

174− int row_number =dbi->row_count;

175− return row_number;

176−}

177−

178−/*

179− Returns column number from DB Struct

180− */

181−int sqlite3_get_num_col_v2(void* p){

182−

183− DBinfo* dbi =(DBinfo*) p;

184− int col_number =dbi-> col_count;

185− return col_number;

186−}

187−

188−/*

189− Another way of obtaining row number

190− Thought this function gets the value

191− from Table struct. The value is stored

192− in the struct after calling get_table.

193− Using this version is not recommended

194− unless used with get_table

195− */

196−int sqlite3_get_num_row(void* p){

197−

198− Table* tbl =(Table*) p;

199− int row_number =tbl->num_row;

200− return row_number;

201−}

202−

203−/*

204− Another way of obtaining column number

205− Thought this function gets the value

206− from Table struct. The value is stored

207− in the struct after calling get_table.

208− Using this version is not recommended

209− unless used with get_table

210− */

211−int sqlite3_get_num_col(void* p){

212−

213− Table* tbl =(Table*) p;

214− int col_number =tbl-> num_col;

215− return col_number;

216−}

217−

218−/*

219− This routine returns the type of value

220− and must be called after prepare and exec.

221− Since exec steps through database to obtain

222− row number, this function calls reset to

223− set the pointer to its initial state

224− and then calls sqlite3_column_type

225− to get the type

226−*/

227−int sqlite3_get_data_type(void* p, int nRow, int nCol){

228−

229− DBinfo* dbi =(DBinfo*) p;

230− int rc, type, row_counter;

231− const char* char_int;

232−

233− rc = sqlite3_reset(dbi->ppStmt);

234− rc = sqlite3_step(dbi->ppStmt);

235− row_counter =0;

236−

237− while (rc == SQLITE_ROW && row_counter < nRow) {

238−

239− rc = sqlite3_step(dbi->ppStmt);

240− row_counter++;

241− }

242− type =sqlite3_column_type(dbi->ppStmt, nCol);

243− return type;

244−

245−}

246−/*

247− Obtains the integer value in a given column

248−*/

249−

250−int sqlite3_get_val_int(void* p, int nCol){

251−

252− DBinfo* dbi =(DBinfo*) p;

253− int val, col;

254− val =sqlite3_column_int(dbi->ppStmt, nCol);

255− return val;

256−}

257−

258−/*

259− Obtains the text value

260− Need to allocate memory to store the string

261− Use GC_malloc since Boehm garbage collector

262− frees the resources .

263− */

264−const unsigned char* sqlite3_get_val_text(void* p,int nCol){

265−

266−

267− DBinfo* dbi =(DBinfo*) p;

268− int rc,i, val, counter;

269− const unsigned char* text_val;

270− array =(unsigned char *) malloc(1000*sizeof(char));

271− text_val =sqlite3_column_text(dbi->ppStmt, nCol);

272− memcpy(array, text_val, strlen(text_val));

273− return array;

274−

275−}

276−float sqlite3_get_float(void* p, int nCol){

277−

278− DBinfo* dbi =(DBinfo*) p;

279− double double_val;

280−

281− double_val =sqlite3_column_double(dbi->ppStmt, nCol);

282− float float_val =(float)double_val;

283− return float_val;

284−

285−}

286−/*

287− frees the pointer returned by get_table.

288− */

289−

290−void sqlite3_free_table_idr(void* db){

291− Table* tbl =(Table*) db;

292− sqlite3_free_table(tbl->table_data);

293− free(tbl);

294−}

295−int sqlite3_step_idr(void* db){

296−

297− DBinfo* dbi =(DBinfo*) db;

298− int rc =sqlite3_step(dbi->ppStmt);

299− return rc;

300−}

301−/*

302− Binds integer. This returns a pointer

303− because of the implementation of BindMulti

304− which binds multiple values

305− */

306−void* sqlite3_bind_int_idr(void* p,int index, int val){

307−

308− DBinfo* dbi =(DBinfo*) p;

309− int rc;

310−

311− rc =sqlite3_bind_int(dbi->ppStmt,index,val);

312− if(rc != SQLITE_OK){

313− return NULL;

314− }

315−

316− return dbi;

317−}

318−

319−void* sqlite3_bind_float_idr(void* p,int index, float val){

320−

321− DBinfo* dbi =(DBinfo*) p;

322− int rc;

323− double res =(float)val;

324−

325− rc =sqlite3_bind_double(dbi->ppStmt,index,res);

326−

327− if(rc != SQLITE_OK){

328− return NULL;

329− }

330− return dbi;

331−}

332−

333−void* sqlite3_bind_null_idr(void* p,int index){

334−

335− DBinfo* dbi =(DBinfo*) p;

336− int rc;

337− rc =sqlite3_bind_null(dbi->ppStmt,index);

338− if(rc != SQLITE_OK){

339− return NULL;

340− }

341−

342− return dbi;

343−}

344−

345−void* sqlite3_bind_text_idr(void* p,const char* text, int index,int length){

346−

347− DBinfo* dbi =(DBinfo*) p;

348− int rc;

349− rc =sqlite3_bind_text(dbi->ppStmt,index,text,length,SQLITE_STATIC);

350− if(rc != SQLITE_OK){

351− return NULL;

352− }

353−

354− return dbi;

355−}

356−/*

357− Used for testing column count function.

358− This function prepares query and by passing

359− select all, gets the count for column number

360− Could be used for testing. Not recommended to

361− be used with prepare and exec

362− */

363−

364−int sqlite3_column_count_idr(void* db, const char* tbl_name){

365− DBinfo* dbi =(DBinfo*) db;

366− sqlite3_stmt* stmt;

367− const char *tail;

368− int rc;

369−

370− strcpy(sql_query_buffer, "select * from ");

371− strcat(sql_query_buffer, tbl_name);

372−

373− rc = sqlite3_prepare_v2(dbi->db_ptr, sql_query_buffer, -1, &stmt, &tail);

374− if(rc != SQLITE_OK){

375− fprintf(stderr, "SQL Prepare error");

376− return rc;

377− }

378− printf("Prepare successful %d\n", rc);

379−

380− rc =sqlite3_column_count(stmt);

381− if(rc == 0){

382− fprintf(stderr, "SQL column count error\n");

383− return rc;

384− }

385− sqlite3_finalize(stmt);

386−

387− // rc = actual column count

388− return rc;

389−}

390−

391−int sqlite3_data_count_idr(void* db){

392−

393− DBinfo* dbi =(DBinfo*) db;

394− int rc = sqlite3_data_count(dbi->ppStmt);

395−

396− return rc;

397−}

398−/*

399− Must be called after prepare to clean up

400− the resources.

401− */

402−int sqlite3_finalize_idr(void* db){

403−

404− DBinfo* dbi=(DBinfo*) db;

405− int rc =sqlite3_finalize(dbi->ppStmt);

406− return rc;

407−}

408−

409−int sqlite3_complete_idr(const char *sql){

410−

411− int rc = sqlite3_complete(sql);

412− return rc;

413−}

414−

415−/*

416− Resets a prepared statement pointer

417− to its initial state

418− */

419−int sqlite3_reset_idr(void* db){

420−

421− DBinfo* dbi=(DBinfo*) db;

422− int rc = sqlite3_reset(dbi-> ppStmt);

423− return rc;

424−

425−}

426−/*

427− The following routines may be used to

428− obtain column related information.

429− */

430−const char *sqlite3_column_name_idr(void* db, int N){

431−

432− DBinfo* dbi=(DBinfo*) db;

433− const char *name = sqlite3_column_name(dbi->ppStmt, N);

434−

435− return name;

436−}

437−

438−const char *sqlite3_column_decltype_idr(void* db,int n){

439− DBinfo* dbi=(DBinfo*) db;

440− const char *dectype = sqlite3_column_decltype(dbi->ppStmt, n);

441−

442− return dectype;

443−

444−}

445−int sqlite3_column_bytes_idr(void* db, int n){

446−

447− DBinfo* dbi=(DBinfo*) db;

448− int res = sqlite3_column_bytes(dbi->ppStmt, n);

449− return res;

450−

451−

452−}

453−const void *sqlite3_column_blob_idr(void* db, int iCol){

454− DBinfo* dbi=(DBinfo*) db;

455− const void* data =sqlite3_column_blob(dbi-> ppStmt, iCol);

456− return data;

457−}

458−

459−const unsigned char *sqlite3_column_text_idr(void* db, int iCol){

460− DBinfo* dbi=(DBinfo*) db;

461− const unsigned char* col_text =sqlite3_column_text(dbi->ppStmt, iCol);

462− return col_text;

463−

464−}

465−

466−int sqlite3_column_int_idr(void* db, int iCol){

467− DBinfo* dbi=(DBinfo*) db;

468− int res =sqlite3_column_int(dbi-> ppStmt, iCol);

469− return res;

470−

471−}

472−/*

473− Some back up functions

474− */

475−

476−void* sqlite3_backup_init_idr(void* pDest,

477− const char *zDestName,

478− void* pSource,

479− const char *zSourceName

480− ){

481−

482− DBinfo* dbi=(DBinfo*) pDest;

483− DBbackup* dbi2=(DBbackup*) pSource;

484−

485− void* res = sqlite3_backup_init(dbi->db_ptr,zDestName,

486− dbi2->source_ptr,zSourceName);

487−

488− if(res == NULL){

489− printf("Error number in initializing backup : %d\n", sqlite3_errcode(dbi->db_ptr));

490− }

491−

492− dbi2->backup = res;

493− return dbi2;

494−

495−

496−}

497−

498−int sqlite3_backup_step_idr(void *backup, int nPage){

499−

500− DBbackup* dbi=(DBbackup*) backup;

501− int res = sqlite3_backup_step(dbi->backup, nPage);

502− return res;

503−

504−

505−}

506−int sqlite3_backup_finish_idr(void *backup){

507−

508− DBbackup* dbi=(DBbackup*) backup;

509− int res = sqlite3_backup_finish(dbi->backup);

510− return res;

511−

512−

513−}

514−

515−int sqlite3_backup_remaining_idr(void *backup){

516−

517− DBbackup* dbi=(DBbackup*) backup;

518− int res = sqlite3_backup_remaining(dbi->backup);

519−

520− return res;

521−}

522−

523−int sqlite3_backup_pagecount_idr(void *backup){

524−

525− DBbackup* dbi=(DBbackup*) backup;

526− int res =sqlite3_backup_pagecount(dbi-> backup);

527− return res;

528−

529−}

530−/*

531− Get the length of string

532− Need this in Idris since length will not

533− work on Strings.

534− */

535−int strLength(const char * str){

536−

537− int length = strlen(str);

538− return length;

539−

540−

541−}

542−

543−

contribs/lib/SQLite3/sqlite3api.hdeleted−130

@@ -1,130 +0,0 @@

1−/*

2− * sqlite3api.h

3− *

4− *

5− * Created by Melissa Farinaz MOZIFIAN on 22/06/2012.

7− *

8− */

9−#include <stdio.h>

10−#include <stdlib.h>

11−#include <string.h>

12−#include <sqlite3.h>

13−#include <ctype.h>

14−#include <gc.h>

15−

16−typedef struct {

17− sqlite3 *db_ptr; // database pointer

18− sqlite3_stmt *ppStmt; // statement pointer

19− char buffer[1000]; // bufer to store errors returned by certain functions

20− const char *Ptr_tail;

21− sqlite3_value *value;

22− int row_count; // row number store by exec function

23− int col_count;

24−

25−} DBinfo;

26−

27−// struct used for backup functions

28−typedef struct {

29− sqlite3 *source_ptr;

30− sqlite3_backup *backup;

31−}DBbackup ;

32−

33−// Table struct used by get_table function

34−// stores row and column

35−// returned by get_table

36−typedef struct {

37− int num_row;

38− int num_col;

39− char** table_data;

40− int data_size;

41− int* data_type;

42− DBinfo* database;

43−}Table;

44−

45−

46−void* sqlite3_open_idr(const char *filename);

47−

48−int exec_db(void*p);

49−

50−int sqlite3_close_idr(void* db);

51−

52−int sqlite3_exec_idr(void*, const char *sql);

53−

54−char* sqlite3_get_error(void* db);

55−

56−const unsigned char* sqlite3_get_val_text(void* p,int nCol);

57−

58−void* sqlite3_get_table_idr(void* db, const char *sql);

59−

60−void sqlite3_free_table_idr(void* db);

61−

62−int sqlite3_get_num_col(void* p);

63−

64−int sqlite3_get_num_row(void* p);

65−

66−int sqlite3_get_num_row_v2(void* p);

67−

68−int sqlite3_get_num_col_v2(void* p);

69−

70−int sqlite3_get_data_type(void* p, int nRow, int nCol);

71−

72−int sqlite3_get_val_int(void* p,int nCo);

73−

74−float sqlite3_get_float(void* p, int nCol);

75−

76−void* sqlite3_prepare_idr(

77− void *db, /* Database handle */

78− const char *zSql /* SQL statement, UTF-8 encoded */

79−);

80−

81−int sqlite3_step_idr(void* stmt);

82−

83−void* sqlite3_bind_float_idr(void* p,int index, float val);

84−

85−void* sqlite3_bind_int_idr(void* p,int index , int val);

86−

87−void* sqlite3_bind_null_idr(void* p,int index);

88−

89−void* sqlite3_bind_text_idr(void* p,const char* text, int index,int length);

90−

91−int sqlite3_column_count_idr(void* stmt, const char* tbl_name);

92−

93−int sqlite3_data_count_idr(void* stmt);

94−

95−int sqlite3_reset_idr(void* stmt);

96−

97−int sqlite3_finalize_idr(void* stmt);

98−

99−int sqlite3_complete_idr(const char *sql);

100−

101−const char *sqlite3_column_decltype_idr(void* stmt,int n);

102−

103−const char *sqlite3_column_name_idr(void* stmt, int N);

104−

105−int sqlite3_column_bytes_idr(void* stmt, int n);

106−

107−int sqlite3_column_bytes_idr(void* stmt, int n);

108−

109−const void *sqlite3_column_blob_idr(void* stmt, int iCol);

110−

111−const unsigned char *sqlite3_column_text_idr(void* stmt, int iCol);

112−

113−int sqlite3_column_int_idr(void* stmt, int iCol);

114−

115−

116−void* sqlite3_backup_init_idr(void* pDestm,

117− const char *zDestName,

118− void* pSource,

119− const char *zSourceName

120− );

121−

122−int sqlite3_backup_finish_idr(void *backup);

123−

124−int sqlite3_backup_step_idr(void *backup, int nPage);

125−

126−int sqlite3_backup_remaining_idr(void *backup);

127−

128−int sqlite3_backup_pagecount_idr(void *backup);

129−

130−int strLength(const char * str);

contribs/lib/SQLite3/students.dbdeleted

Binary file not shown.

contribs/lib/SQLite3/testunit.idrdeleted−140

@@ -1,140 +0,0 @@

1−module Main

2−import Sqlite3

3−

4−

5−testexpr : DB()

6−testexpr = do db <- open_db "somedb.db"

7− let sql = (evalSQL [] ((SELECT ALL)(TBL ["tbl1"]) (OR (AND (MkCond (Equals (VCol "data")(VStr "data0"))) (MkCond (Equals (VCol "num")(VInt 1))) ) (MkCond (Equals (VCol "num")(VInt 2))))))

8− let x = (fst sql) -- get the string

9− let list = (snd sql) -- list of vals

10− liftIO(printLn x) -- use liftIO to turn this into DB type

11− stmt <- (prepare_db db x) -- prepare the statement

12− bindMulti stmt list -- bind the values in the list

13− exec_db_v2 stmt -- execute the prepared query

14− res <- toList_v1 db -- toList_v1 to get the result

15− liftIO(printLn res) -- print the result

16− finalize_db stmt -- Statment pointer must be finalized in the end

17− close_db db -- close the datbase

18− return ()

19−

20−testupdate : DB()

21−testupdate = do db <- open_db "somedb.db"

22− let sql = (evalSQL [] (UPDATE (TBL ["tbl1"]) (WHERE (SET (MkCond (Equals(VCol "data") (VStr "data600"))) ) (MkCond (Equals (VCol "num") (VInt 2))) ) ))

23− let x = (fst sql)

24− let list = (snd sql)

25− liftIO(printLn x)

26− stmt <- (prepare_db db x)

27− bindMulti stmt list

28− exec_db_v2 stmt

29− finalize_db stmt

30− close_db db

31− return ()

32−

33−testInsert : DB()

34−testInsert = do db <- open_db "somedb.db"

35− let sql = (evalSQL [] (INSERT (TBL ["tbl1"]) [(VInt 3),(VStr "ham")]))

36− let x = (fst sql)

37− let list = (snd sql)

38− liftIO(printLn x)

39− stmt <- (prepare_db db x)

40− bindMulti stmt list

41− exec_db_v2 stmt

42− finalize_db stmt

43− close_db db

44− return ()

45−

46−testNull : DB()

47−testNull = do db <- open_db "somedb.db"

48− let sql = (evalSQL [] ((SELECT ALL)(TBL ["tbl1"]) (MkCond (MkNULL (VCol "data")))))

49− let x = (fst sql)

50− let list = (snd sql)

51− liftIO(printLn x)

52− stmt <- (prepare_db db x)

53− bindMulti stmt list

54− exec_db_v2 stmt

55− res <- toList_v1 db

56− liftIO(printLn res)

57− finalize_db stmt

58− close_db db

59− return ()

60−

61−

62−testInsertWithCond : DB()

63−testInsertWithCond = do db <- open_db "somedb.db"

64− let sql = (evalSQL [] (INSERTC (TBL ["tbl1"]) [(VCol "data"),(VCol "num")] [(VInt 30),(VStr "inserthere")]))

65− let x = (fst sql)

66− let list = (snd sql)

67− liftIO(printLn x)

68− stmt <- (prepare_db db x)

69− bindMulti stmt list

70− exec_db_v2 stmt

71− finalize_db stmt

72− close_db db

73− return ()

74−

75−-- Nested queries need to have the same column as the outer queries.

76−testNestedSel1 : DB()

77−testNestedSel1 = do db <- open_db "somedb.db"

78− let sql = (evalSQL [] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL ["tbl1"]) (MkCond (MkGT (VCol "num")(VInt 2))))Empty))

79− let x = (fst sql)

80− let list = (snd sql)

81− liftIO(printLn x)

82− stmt <- (prepare_db db x)

83− bindMulti stmt list

84− exec_db_v2 stmt

85− res <- toList_v1 db

86− liftIO(printLn res)

87− finalize_db stmt

88− close_db db

89− return ()

90−

91−-- Testing Create Table

92−testCreateTable : DB ()

93−testCreateTable = do db <- open_db "somedb.db"

94− let sql = (evalSQL [] (CREATE (TBL ["mynewtbl"]) [ ((VCol "col"),(CInt "int"),(None)) ] ) )

95− let x = (fst sql)

96− let list = (snd sql)

97− liftIO(printLn x)

98− stmt <- (prepare_db db x)

99− bindMulti stmt list

100− exec_db_v2 stmt

101− finalize_db stmt

102− close_db db

103− return ()

104−

105−-- This may be a bit slow

106−testMultiTable : DB ()

107−testMultiTable = do db <- open_db "somedb.db"

108− let sql = (evalSQL [] ((SELECT ALL )(TBL ["mytable","tbl1"]) (Empty) ) )

109− let x = (fst sql)

110− let list = (snd sql)

111− liftIO(printLn x)

112− stmt <- (prepare_db db x)

113− bindMulti stmt list

114− exec_db_v2 stmt

115− res <- toList_v1 db

116− liftIO(printLn res)

117− finalize_db stmt

118− close_db db

119− return ()

120−

121−testSelAll : DB ()

122−testSelAll = do db <- open_db "somedb.db"

123− let sql = (evalSQL [] ((SELECT ALL )(TBL ["tbl1"]) (Empty) ) )

124− let x = (fst sql)

125− let list = (snd sql)

126− liftIO(printLn x)

127− stmt <- (prepare_db db x)

128− bindMulti stmt list

129− exec_db_v2 stmt

130− res <- toList_v1 db

131− liftIO(printLn res)

132− finalize_db stmt

133− close_db db

134− return ()

135−

136−

137−main : IO ()

138−main = do x <- runDB (testMultiTable) -- runDB : DB a -> IO a

139− --y <- runDB (testNestedSel1)

140− return ()

contribs/lib/SimpleParser/SimpleParser.idrdeleted−190

@@ -1,190 +0,0 @@

1−{-

2− Simple monadic parser module, based heavily on that by

3− Graham Hutton.

4−-}

5−

6−module SimpleParser

7−

8−import Prelude

9−import Prelude.Monad

10−import Prelude.Applicative

11−import Prelude.List

12−import Builtins

13−

14−%access public

15−

16−

17−--------------------------------------------------------------------------------

18−-- The monad of parsers

19−--------------------------------------------------------------------------------

20−

21−data Parser a = P (String -> Either String (a, String))

22−

23−parse : Parser a -> String -> Either String (a, String)

24−parse (P p) inp = p inp

25−

26−instance Functor Parser where

27− map f p = P (\inp => case parse p inp of

28− Left err => Left err

29− Right (v, rest) => Right ((f v), rest))

30−

31−instance Applicative Parser where

32− pure v = P (\inp => Right (v, inp))

33− a <*> b = P (\inp => do (f, rest) <- parse a inp

34− (x, rest') <- parse b rest

35− pure ((f x), rest'))

36−

37−instance Monad Parser where

38− p >>= f = P (\inp => case parse p inp of

39− Left err => Left err

40− Right (v,rest) => parse (f v) rest)

41−

42−instance Alternative Parser where

43− empty = P (const (Left "empty"))

44− p <|> q = P (\inp => case parse p inp of

45− Left msg => parse q inp

46− Right (v,out) => Right (v,out))

47−

48−

49−--------------------------------------------------------------------------------

50−-- Basic parsers

51−--------------------------------------------------------------------------------

52−

53−failure : String -> Parser a

54−failure msg = P (\inp => Left msg)

55−

56−item : Parser Char

57−item = P (\inp => case choose (inp == "") of

58− Left _ => Left "Error! Parsing empty list."

59− Right p => Right (strHead' inp p, strTail' inp p))

60−

61−

62−--------------------------------------------------------------------------------

63−-- Derived primitives

64−--------------------------------------------------------------------------------

65−

66−sat : (Char -> Bool) -> Parser Char

67−sat p = do x <- item

68− guard (p x)

69− pure x

70−

71−oneof : List Char -> Parser Char

72−oneof xs = sat (\x => elem x xs)

73−

74−digit : Parser Char

75−digit = sat isDigit

76−

77−lower : Parser Char

78−lower = sat isLower

79−

80−upper : Parser Char

81−upper = sat isUpper

82−

83−letter : Parser Char

84−letter = sat isAlpha

85−

86−alphanum : Parser Char

87−alphanum = sat isAlphaNum

88−

89−char : Char -> Parser Char

90−char x = sat (== x)

91−

92−string : String -> Parser String

93−string s = map pack (traverse char (unpack s))

94−

95−mutual

96− many1 : Parser a -> Parser (List a)

97− many1 p = [| p :: many p |]

98−

99− many : Parser a -> Parser (List a)

100− many p = lazy (many1 p) <|> pure []

101−

102−bool : Parser Bool

103−bool = parseTrue <|> parseFalse

104− where parseTrue : Parser Bool

105− parseTrue = do oneof ['T', 't']

106− string "rue"

107− pure True

108− parseFalse = do oneof ['F', 'f']

109− string "alse"

110− pure False

111−

112−ident : Parser String

113−ident = map pack xs

114− where xs : Parser (List Char)

115− xs = [| letter :: many1 alphanum |]

116−

117−nat : Parser Int

118−nat = do xs <- many digit

119− pure (cast (cast xs))

120−

121−int : Parser Int

122−int = neg <|> nat

123− where neg : Parser Int

124− neg = do char '-'

125− n <- nat

126− pure (-n)

127−

128−space : Parser ()

129−space = do many (sat isSpace)

130− pure ()

131−

132−

133−--------------------------------------------------------------------------------

134−-- Ignoring spacing

135−--------------------------------------------------------------------------------

136−

137−token : Parser a -> Parser a

138−token p = space $> p <$ space

139−

140−identifier : Parser String

141−identifier = token ident

142−

143−natural : Parser Int

144−natural = token nat

145−

146−integer : Parser Int

147−integer = token int

148−

149−symbol : String -> Parser String

150−symbol xs = token (string xs)

151−

152−strToken : Parser String

153−strToken = map pack (token (many1 alphanum))

154−

155−--------------------------------------------------------------------------------

156−-- combinators

157−--------------------------------------------------------------------------------

158−

159−optional : Parser a -> Parser (Maybe a)

160−optional p = map Just p <|> pure Nothing

161−

162−sepBy1 : Parser a -> Parser b -> Parser (List a)

163−sepBy1 p s = [| p :: many (s $> p) |]

164−

165−sepBy : Parser a -> Parser b -> Parser (List a)

166−sepBy p s = sepBy1 p s <|> pure Nil

167−

168−manyTil : Parser a -> Parser b -> Parser (List a)

169−manyTil p e = (e $> pure Nil) <|> lazy [| p :: manyTil p e |] <|> pure Nil

170−

171−--------------------------------------------------------------------------------

172−-- Expressions

173−--------------------------------------------------------------------------------

174−

175−expr : Parser Int

176−factor : Parser Int

177−term : Parser Int

178−

179−expr = do t <- term

180− map (t+) (symbol "+" $> expr) <|> pure t

181−

182−factor = (symbol "(" $> expr <$ symbol ")") <|> natural

183−

184−term = do f <- factor

185− map (f*) (symbol "*" $> term) <|> pure f

186−

187−eval : String -> Maybe Int

188−eval xs = case (parse expr xs) of

189− Right (n,rest) => if rest == "" then Just n else Nothing

190− Left msg => Nothing

contribs/lib/SimpleParser/simpleparser.ipkgdeleted−4

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

1−package simpleparser

2−

3−opts = "-i ../lib"

4−modules = SimpleParser

contribs/tool-support/completion/idris.bashdeleted−31

@@ -1,31 +0,0 @@

1−_idris() {

2− local cur prev words opts LIBRARIES TARGETS

3− _init_completion || return

4−

5− opts=$(_parse_help "$1")

6− LIBRARIES="effects"

7− TARGETS="C Java bytecode javascript node"

8−

9− case "${prev}" in

10− -o)

11− _filedir

12− ;;

13− -i|--ibcsubdir)

14− _filedir -d

15− ;;

16− -p)

17− COMPREPLY=( $(compgen -W "${LIBRARIES}" -- ${cur}))

18− ;;

19− --target)

20− COMPREPLY=( $(compgen -W "${TARGETS}" -- ${cur}))

21− ;;

22− esac

23−

24− if [[ $cur == -* ]]; then

25− COMPREPLY=($(compgen -W "${opts}" -- ${cur}))

26− return

27− fi

28−

29− _filedir '@(idr)'

30−} &&

31−complete -o default -F _idris idris

contribs/tool-support/sublime-text/Idris/Idris.JSON-tmLanguagedeleted−70

@@ -1,70 +0,0 @@

1−{ "name": "Idris",

2− "scopeName": "source.idris",

3− "fileTypes": ["idr"],

4− "patterns": [

5− { "name": "keyword.control.idris",

7−

8− },

9− { "name": "keyword.control.idris",

11−

12− },

13− { "name": "keyword.control.idris",

15−

16− },

17− { "name": "keyword.control.idris",

18− "match": "\\b(public|private|abstract|implicit)\\b"

19−

20− },

21− { "name": "keyword.other.idris",

23− },

24− { "name": "constant.numeric.idris",

25− "match": "\\b(S|O)\\b"

26− },

27− { "match": "\\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\\b",

28− "name": "constant.numeric.idris",

29− "comment": "integers"

30− },

31− {

32− "match": "\\b([0-9]+\\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\\b",

33− "name": "constant.numeric.float.idris",

34− "comment": "floats"

35− },

36− {

37− "name": "comment.line.idris",

38− "match": "(--).*$\n?",

39− "comment": "Line comment"

40− },

41− { "name": "comment.block.idris",

42− "begin": "\\{-",

43− "end": "-\\}",

44− "comment": "Block comment"

45− },

46− {

47− "name": "string.quoted.idris",

48− "begin": "\"",

49− "beginCaptures": {

50− "0": { "name": "punctuation.definition.string.begin.idris"}

51− },

52− "end": "\"",

53− "endCaptures": {

54− "0": { "name": "punctuation.definition.string.end.idris"}

55− },

56− "patterns": [

57− { "name": "constant.character.escape.idris",

58− "match": "\\\\\""

59− }

60− ]

61−

62− }

63−

64−

65− ],

66− "repository": {

67−

68− },

69− "uuid": "4dd16092-ffa5-4ba4-8075-e5da9f368a72"

70−}

contribs/tool-support/sublime-text/Idris/Idris.tmLanguagedeleted−126

@@ -1,126 +0,0 @@

1−<?xml version="1.0" encoding="UTF-8"?>

2−<!DOCTYPE plist PUBLIC "-//Apple Computer//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">

3−<plist version="1.0">

4−<dict>

5− <key>fileTypes</key>

6− <array>

7− <string>idr</string>

8− </array>

9− <key>name</key>

10− <string>Idris</string>

11− <key>patterns</key>

12− <array>

13− <dict>

14− <key>match</key>

16− <key>name</key>

17− <string>keyword.control.idris</string>

18− </dict>

19− <dict>

20− <key>match</key>

22− <key>name</key>

23− <string>keyword.control.idris</string>

24− </dict>

25− <dict>

26− <key>match</key>

28− <key>name</key>

29− <string>keyword.control.idris</string>

30− </dict>

31− <dict>

32− <key>match</key>

33− <string>\b(public|private|abstract|implicit)\b</string>

34− <key>name</key>

35− <string>keyword.control.idris</string>

36− </dict>

37− <dict>

38− <key>match</key>

40− <key>name</key>

41− <string>keyword.other.idris</string>

42− </dict>

43− <dict>

44− <key>match</key>

45− <string>\b(S|O)\b</string>

46− <key>name</key>

47− <string>constant.numeric.idris</string>

48− </dict>

49− <dict>

50− <key>comment</key>

51− <string>integers</string>

52− <key>match</key>

53− <string>\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\b</string>

54− <key>name</key>

55− <string>constant.numeric.idris</string>

56− </dict>

57− <dict>

58− <key>comment</key>

59− <string>floats</string>

60− <key>match</key>

61− <string>\b([0-9]+\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\b</string>

62− <key>name</key>

63− <string>constant.numeric.float.idris</string>

64− </dict>

65− <dict>

66− <key>comment</key>

67− <string>Line comment</string>

68− <key>match</key>

69− <string>(--).*$

70−?</string>

71− <key>name</key>

72− <string>comment.line.idris</string>

73− </dict>

74− <dict>

75− <key>begin</key>

76− <string>\{-</string>

77− <key>comment</key>

78− <string>Block comment</string>

79− <key>end</key>

80− <string>-\}</string>

81− <key>name</key>

82− <string>comment.block.idris</string>

83− </dict>

84− <dict>

85− <key>begin</key>

86− <string>"</string>

87− <key>beginCaptures</key>

88− <dict>

89− <key>0</key>

90− <dict>

91− <key>name</key>

92− <string>punctuation.definition.string.begin.idris</string>

93− </dict>

94− </dict>

95− <key>end</key>

96− <string>"</string>

97− <key>endCaptures</key>

98− <dict>

99− <key>0</key>

100− <dict>

101− <key>name</key>

102− <string>punctuation.definition.string.end.idris</string>

103− </dict>

104− </dict>

105− <key>name</key>

106− <string>string.quoted.idris</string>

107− <key>patterns</key>

108− <array>

109− <dict>

110− <key>match</key>

111− <string>\\"</string>

112− <key>name</key>

113− <string>constant.character.escape.idris</string>

114− </dict>

115− </array>

116− </dict>

117− </array>

118− <key>repository</key>

119− <dict>

120− </dict>

121− <key>scopeName</key>

122− <string>source.idris</string>

123− <key>uuid</key>

124− <string>4dd16092-ffa5-4ba4-8075-e5da9f368a72</string>

125−</dict>

126−</plist>

contribs/tool-support/sublime-text/Idris/idris.sublime-builddeleted−5

@@ -1,5 +0,0 @@

1−{

2− "cmd": ["idris", "$file"],

3− "file_regex": "^(...*?):([0-9]*):?([0-9]*)",

4− "selector": "source.idris"

5−}

contribs/tool-support/sublime-text/README.mddeleted−11

@@ -1,11 +0,0 @@

1−#### Idris support for Sublime Text 2

2−

3−To install, copy the Idris directory to Sublime Text's Packages directory.

4−

5−To build a new Idris.tmLanguage file from the Idris.JSON-tmLanguage file, Sublime Text needs to have the AAAPackageDev package installed.

6−

7−Syntax Definitions tutorial: https://sublime-text-unofficial-documentation.readthedocs.org/en/latest/extensibility/syntaxdefs.html

8−

9−Syntax Definitions reference: https://sublime-text-unofficial-documentation.readthedocs.org/en/latest/reference/syntaxdefs.html

10−

11−Most used scopes: http://manual.macromates.com/en/language_grammars#naming_conventions

custom.mk-alldeps+1−2

@@ -1,2 +1 @@

1−CABALFLAGS += -f LLVM -f FFI -f curses

2−

1+CABALFLAGS += -f LLVM -f FFI -f curses --disable-documentation --disable-profiling --disable-library-profiling

docs/tutorial/introduction.rst+10−10

@@ -25,11 +25,12 @@ lists of a given length [1]_, ``Vect n a``, where ``a`` is the element

2525type and ``n`` is the length of the list and can be an arbitrary term.

2626

2727When types can contain values, and where those values describe

28−properties (e.g. the length of a list) the type of a function can

29−begin to describe its own properties. For example, concatenating two

30−lists has the property that the resulting list’s length is the sum of

31−the lengths of the two input lists. We can therefore give the

32−following type to the ``app`` function, which concatenates vectors:

28+properties, for example the length of a list, the type of a function

29+can begin to describe its own properties. Take for example the

30+concatenatation of two lists. This operation has the property that the

31+resulting list's length is the sum of the lengths of the two input

32+lists. We can therefore give the following type to the ``app``

33+function, which concatenates vectors:

3334

3435.. code-block:: idris

3536

@@ -58,11 +59,10 @@ Example Code

5859============

5960

6061This tutorial includes some example code, which has been tested with

61−Idris version . The files are available in the Idris

62−distribution, and provided along side the tutorial source, so that you

63−can try them out easily, under ``tutorial/examples``. However, it is

64−strongly recommended that you can type them in yourself, rather than

65−simply loading and reading them.

62+against Idris. These files are available with the Idris distribution,

63+so that you can try them out easily. They can be found under

64+``samples``. It is, however, strongly recommended that you type

65+them in yourself, rather than simply loading and reading them.

6666

6767.. [1]

6868 Typically, and perhaps confusingly, referred to in the dependently

docs/tutorial/modules.rst+14−12

@@ -10,11 +10,11 @@ module, a list of ``import`` statements giving the other modules which

1010are to be imported, and a collection of declarations and definitions of

1111types, classes and functions. For example, the listing below gives a

1212module which defines a binary tree type ``BTree`` (in a file

13−``btree.idr``):

13+``Btree.idr``):

1414

1515.. code-block:: idris

1616

17− module btree

17+ module Btree

1818

1919 data BTree a = Leaf

2020 | Node (BTree a) a (BTree a)

@@ -40,23 +40,24 @@ Then, this gives a main program (in a file

4040

4141 module Main

4242

43− import btree

43+ import Btree

4444

4545 main : IO ()

4646 main = do let t = toTree [1,8,2,7,9,3]

4747 print (btree.toList t)

4848

4949

50+

5051The same names can be defined in multiple modules. This is possible

5152because in practice names are *qualified* with the name of the module.

5253The names defined in the ``btree`` module are, in full:

5354

54−+ ``btree.BTree``

55−+ ``btree.Leaf``

56−+ ``btree.Node``

57−+ ``btree.insert``

58−+ ``btree.toList``

59−+ ``btree.toTree``

55++ ``Btree.BTree``

56++ ``Btree.Leaf``

57++ ``Btree.Node``

58++ ``Btree.insert``

59++ ``Btree.toList``

60++ ``Btree.toTree``

6061

6162If names are otherwise unambiguous, there is no need to give the fully

6263qualified name. Names can be disambiguated either by giving an explicit

@@ -103,7 +104,7 @@ functions to be exported as ``abstract``, as we see below:

103104

104105.. code-block:: idris

105106

106− module btree

107+ module Btree

107108

108109 abstract data BTree a = Leaf

109110 | Node (BTree a) a (BTree a)

@@ -137,7 +138,8 @@ the ``public`` modifier on an ``import``. For example:

137138

138139 module A

139140

140− import B import public C

141+ import B

142+ import public C

141143

142144 public a : AType a = ...

143145

@@ -154,7 +156,7 @@ wish to overload names within the same module:

154156

155157.. code-block:: idris

156158

157− module foo

159+ module Foo

158160

159161 namespace x

160162 test : Int -> Int

docs/tutorial/starting.rst+9−13

@@ -10,12 +10,9 @@ Prerequisites

1010Before installing Idris, you will need to make sure you have all

1111of the necessary libraries and tools. You will need:

1212

13−- A fairly recent Haskell platform. Version 2013.2.0.0 should be

14− sufficiently recent, though it is better to be completely up to

15− date.

13+- A fairly recent Haskell platform. Version ``2013.2.0.0`` should be sufficiently recent, though it is better to be completely up to date.

1614

17−- The *GNU Multiple Precision Arithmetic Library* (GMP) is available

18− from MacPorts/Homebrew and all major Linux distributions.

15+- The *GNU Multiple Precision Arithmetic Library* (GMP) is available from MacPorts/Homebrew and all major Linux distributions.

1916

2017Downloading and Installing

2118==========================

@@ -33,7 +30,7 @@ development version you can find it, as well as build intructions, on

3330GitHub at: https://github.com/idris-lang/Idris-dev.

3431

3532To check that installation has succeeded, and to write your first

36−Idris program, create a file called “``hello.idr``” containing the

33+Idris program, create a file called ``hello.idr`` containing the

3734following text:

3835

3936.. code-block:: idris

@@ -55,18 +52,17 @@ create an executable called ``hello``, which you can run:

5552 $ ./hello

5653 Hello world

5754

58−Note that the ``$`` indicates the shell prompt! Should the Idris

59−executable not be found please ensure that you have added

60−``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X

61−users may find they need to use ``~/Library/Haskell/bin``

55+Please note that the dollar sign ``$`` indicates the shell prompt!

56+Should the Idris executable not be found please ensure that you have

57+added ``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS

58+X users may find they need to add ``~/Library/Haskell/bin``

6259instead. Some useful options to the Idris command are:

6360

6461- ``-o prog`` to compile to an executable called ``prog``.

6562

66−- ``--check`` type check the file and its dependencies without

67− starting the interactive environment.

63+- ``--check`` type check the file and its dependencies without starting the interactive environment.

6864

69−- ``--help`` display usage summary and command line options

65+- ``--help`` display usage summary and command line options.

7066

7167The Interactive Environment

7268===========================

docs/tutorial/typesfuns.rst+37−33

@@ -12,13 +12,13 @@ Idris defines several primitive types: ``Int``, ``Integer`` and

1212manipulation, and ``Ptr`` which represents foreign pointers. There are

1313also several data types declared in the library, including ``Bool``,

1414with values ``True`` and ``False``. We can declare some constants with

15−these types. Enter the following into a file ``prims.idr`` and load it

15+these types. Enter the following into a file ``Prims.idr`` and load it

1616into the Idris interactive environment by typing ``idris

17−prims.idr``:

17+Prims.idr``:

1818

1919.. code-block:: idris

2020

21− module prims

21+ module Prims

2222

2323 x : Int

2424 x = 42

@@ -33,17 +33,18 @@ prims.idr``:

3333 quux = False

3434

3535An Idris file consists of an optional module declaration (here

36−``module prims``) followed by an optional list of imports (none here,

37−however Idris programs can consist of several modules, and the

38−definitions in each module each have their own namespace, as we will

39−discuss in Section :ref:`sect-namespaces`) and a collection of

40−declarations and definitions. The order of definitions is significant

41−— functions and data types must be defined before use. Each definition

42−must have a type declaration, for example see ``x : Int``, ``foo :

43−String``, from the above listing. Indentation is significant — a new

44−declaration begins at the same level of indentation as the preceding

45−declaration. Alternatively, declarations may be terminated with a

46−semicolon.

36+``module Prims``) followed by an optional list of imports and a

37+collection of declarations and definitions. In this example no imports

38+have been specified. However Idris programs can consist of several

39+modules and the definitions in each module each have their own

40+namespace. This is discussed further in Section

41+:ref:`sect-namespaces`). When writing Idris programs both the order in

42+definitions are given and indentation are significant. Functions and

43+data types must be defined before use, incidently each definition must

44+have a type declaration, for example see ``x : Int``, ``foo :

45+String``, from the above listing. New declarations must begin at the

46+same level of indentation as the preceding declaration.

47+Alternatively, a semicolon ``;`` can be used to terminate declarations.

4748

4849A library module ``prelude`` is automatically imported by every

4950Idris program, including facilities for IO, arithmetic, data

@@ -63,7 +64,7 @@ All of the usual arithmetic and comparison operators are defined for

6364the primitive types. They are overloaded using type classes, as we

6465will discuss in Section :ref:`sect-classes` and can be extended to

6566work on user defined types. Boolean expressions can be tested with the

66−``if...then...else`` construct:

67+``if...then...else`` construct, for example:

6768

6869::

6970

@@ -73,9 +74,9 @@ work on user defined types. Boolean expressions can be tested with the

7374Data Types

7475==========

7576

76−Data types are declared in a similar way to Haskell data types, with a

77−similar syntax. Natural numbers and lists, for example, can be

78−declared as follows:

77+Data types are declared in a similar way and with similar syntax to

78+Haskell. Natural numbers and lists, for example, can be declared as

79+follows:

7980

8081.. code-block:: idris

8182

@@ -193,11 +194,13 @@ does not need to be visible globally:

193194Indentation is significant — functions in the ``where`` block must be

194195indented further than the outer function.

195196

196−**Scope:** Any names which are visible in the outer scope are also

197−visible in the ``where`` clause (unless they have been redefined, such

198−as ``xs`` here). A name which appears only in the type will be in scope

199−in the ``where`` clause if it is a *parameter* to one of the types,

200−i.e. it is fixed across the entire structure.

197+.. note:: Scope

198+

199+ Any names which are visible in the outer scope are also visible in

200+ the ``where`` clause (unless they have been redefined, such as ``xs``

201+ here). A name which appears only in the type will be in scope in the

202+ ``where`` clause if it is a *parameter* to one of the types, i.e. it

203+ is fixed across the entire structure.

201204

202205As well as functions, ``where`` blocks can include local data

203206declarations, such as the following where ``MyLT`` is not accessible

@@ -306,16 +309,17 @@ following:

306309 $ idris vbroken.idr --check

307310 vbroken.idr:9:23:When elaborating right hand side of Vect.++:

308311 When elaborating an application of constructor Vect.:::

309− Can't unify

310− Vect (k + k) a

311− with

312− Vect (plus k m) a

313−

314− Specifically:

315− Can't unify

316− plus k k

317− with

318− plus k m

312+ Can't unify

313+ Vect (k + k) a (Type of xs ++ xs)

314+ with

315+ Vect (plus k m) a (Expected type)

316+

317+ Specifically:

318+ Can't unify

319+ plus k k

320+ with

321+ plus k m

322+

319323

320324This error message suggests that there is a length mismatch between

321325two vectors — we needed a vector of length ``k + m``, but provided a

docs/tutorial/views.rst+2−2

@@ -83,8 +83,8 @@ rule:

8383The value of the result of ``parity k`` affects the form of ``k``,

8484because the result of ``parity k`` depends on ``k``. So, as well as

8585the patterns for the result of the intermediate computation (``Even``

86−and ``odd``) right of the ``\mid``, we also write how the results

87−affect the other patterns left of the :math:`\mid`. Note that there is

86+and ``odd``) right of the ``|``, we also write how the results

87+affect the other patterns left of the ``|``. Note that there is

8888a function in the patterns (``+``) and repeated occurrences of

8989``j``—this is allowed because another argument has determined the form

9090of these patterns.

idris.cabal+5−1

@@ -346,6 +346,10 @@ Extra-source-files:

346346 test/basic013/*.idr

347347 test/basic013/expected

348348

349+ test/bignum001/run

350+ test/bignum001/*.idr

351+ test/bignum001/expected

352+

349353 test/delab001/*.idr

350354 test/delab001/run

351355 test/delab001/expected

@@ -730,6 +734,7 @@ Library

730734 , Idris.Elab.Provider

731735 , Idris.Elab.Transform

732736 , Idris.Elab.Value

737+ , Idris.Elab.Term

733738

734739 , Idris.AbsSyntax

735740 , Idris.AbsSyntaxTree

@@ -748,7 +753,6 @@ Library

748753 , Idris.Docstrings

749754 , Idris.ElabDecls

750755 , Idris.ElabQuasiquote

751− , Idris.ElabTerm

752756 , Idris.Erasure

753757 , Idris.Error

754758 , Idris.ErrReverse

libs/base/Data/Bits.idr+5−10

@@ -4,21 +4,16 @@ import Data.Fin

44

55%default total

66

7−divCeil : Nat -> Nat -> Nat

8−divCeil x y = case x `mod` y of

9− Z => x `div` y

10− S _ => S (x `div` y)

11−

127nextPow2 : Nat -> Nat

138nextPow2 Z = Z

14−nextPow2 x = if x == (2 `power` l2x)

15− then l2x

16− else S l2x

9+nextPow2 (S x) = if (S x) == (2 `power` l2x)

10+ then l2x

11+ else S l2x

1712 where

18− l2x = log2 x

13+ l2x = log2NZ (S x) SIsNotZ

1914

2015nextBytes : Nat -> Nat

21−nextBytes bits = (nextPow2 (bits `divCeil` 8))

16+nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))

2217

2318machineTy : Nat -> Type

2419machineTy Z = Bits8

libs/contrib/Data/SortedMap.idr+64−53

@@ -2,72 +2,73 @@ module Data.SortedMap

22

33-- TODO: write merge and split

44

5−data Tree : Nat -> Type -> Type -> Type where

6− Leaf : k -> v -> Tree Z k v

7− Branch2 : Tree n k v -> k -> Tree n k v -> Tree (S n) k v

8− Branch3 : Tree n k v -> k -> Tree n k v -> k -> Tree n k v -> Tree (S n) k v

5+private

6+data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where

7+ Leaf : k -> v -> Tree Z k v o

8+ Branch2 : Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o

9+ Branch3 : Tree n k v o -> k -> Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o

910

1011branch4 :

11− Tree n k v -> k ->

12− Tree n k v -> k ->

13− Tree n k v -> k ->

14− Tree n k v ->

15− Tree (S (S n)) k v

12+ Tree n k v o -> k ->

13+ Tree n k v o -> k ->

14+ Tree n k v o -> k ->

15+ Tree n k v o ->

16+ Tree (S (S n)) k v o

1617branch4 a b c d e f g =

1718 Branch2 (Branch2 a b c) d (Branch2 e f g)

1819

1920branch5 :

20− Tree n k v -> k ->

21− Tree n k v -> k ->

22− Tree n k v -> k ->

23− Tree n k v -> k ->

24− Tree n k v ->

25− Tree (S (S n)) k v

21+ Tree n k v o -> k ->

22+ Tree n k v o -> k ->

23+ Tree n k v o -> k ->

24+ Tree n k v o -> k ->

25+ Tree n k v o ->

26+ Tree (S (S n)) k v o

2627branch5 a b c d e f g h i =

2728 Branch2 (Branch2 a b c) d (Branch3 e f g h i)

2829

2930branch6 :

30− Tree n k v -> k ->

31− Tree n k v -> k ->

32− Tree n k v -> k ->

33− Tree n k v -> k ->

34− Tree n k v -> k ->

35− Tree n k v ->

36− Tree (S (S n)) k v

31+ Tree n k v o -> k ->

32+ Tree n k v o -> k ->

33+ Tree n k v o -> k ->

34+ Tree n k v o -> k ->

35+ Tree n k v o -> k ->

36+ Tree n k v o ->

37+ Tree (S (S n)) k v o

3738branch6 a b c d e f g h i j k =

3839 Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)

3940

4041branch7 :

41− Tree n k v -> k ->

42− Tree n k v -> k ->

43− Tree n k v -> k ->

44− Tree n k v -> k ->

45− Tree n k v -> k ->

46− Tree n k v -> k ->

47− Tree n k v ->

48− Tree (S (S n)) k v

42+ Tree n k v o -> k ->

43+ Tree n k v o -> k ->

44+ Tree n k v o -> k ->

45+ Tree n k v o -> k ->

46+ Tree n k v o -> k ->

47+ Tree n k v o -> k ->

48+ Tree n k v o ->

49+ Tree (S (S n)) k v o

4950branch7 a b c d e f g h i j k l m =

5051 Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)

5152

52−merge1 : Tree n k v -> k -> Tree (S n) k v -> k -> Tree (S n) k v -> Tree (S (S n)) k v

53+merge1 : Tree n k v o -> k -> Tree (S n) k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o

5354merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i

5455merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k

5556merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k

5657merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

5758

58−merge2 : Tree (S n) k v -> k -> Tree n k v -> k -> Tree (S n) k v -> Tree (S (S n)) k v

59+merge2 : Tree (S n) k v o -> k -> Tree n k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o

5960merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i

6061merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k

6162merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k

6263merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

6364

64−merge3 : Tree (S n) k v -> k -> Tree (S n) k v -> k -> Tree n k v -> Tree (S (S n)) k v

65+merge3 : Tree (S n) k v o -> k -> Tree (S n) k v o -> k -> Tree n k v o -> Tree (S (S n)) k v o

6566merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i

6667merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k

6768merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k

6869merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m

6970

70−treeLookup : Ord k => k -> Tree n k v -> Maybe v

71+treeLookup : k -> Tree n k v o -> Maybe v

7172treeLookup k (Leaf k' v) =

7273 if k == k' then

7374 Just v

@@ -86,7 +87,7 @@ treeLookup k (Branch3 t1 k1 t2 k2 t3) =

8687 else

8788 treeLookup k t3

8889

89−treeInsert' : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree n k v, k, Tree n k v)

90+treeInsert' : k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree n k v o, k, Tree n k v o)

9091treeInsert' k v (Leaf k' v') =

9192 case compare k k' of

9293 LT => Right (Leaf k v, k, Leaf k' v')

@@ -116,17 +117,17 @@ treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =

116117 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')

117118 Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)

118119

119−treeInsert : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree (S n) k v)

120+treeInsert : k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree (S n) k v o)

120121treeInsert k v t =

121122 case treeInsert' k v t of

122123 Left t' => Left t'

123124 Right (a, b, c) => Right (Branch2 a b c)

124125

125−delType : Nat -> Type -> Type -> Type

126−delType Z k v = ()

127−delType (S n) k v = Tree n k v

126+delType : Nat -> (k : Type) -> Type -> Ord k -> Type

127+delType Z k v o = ()

128+delType (S n) k v o = Tree n k v o

128129

129−treeDelete : Ord k => k -> Tree n k v -> Either (Tree n k v) (delType n k v)

130+treeDelete : k -> Tree n k v o -> Either (Tree n k v o) (delType n k v o)

130131treeDelete k (Leaf k' v) =

131132 if k == k' then

132133 Right ()

@@ -183,33 +184,38 @@ treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =

183184 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')

184185 Right t3' => Left (merge3 t1 k1 t2 k2 t3')

185186

186−treeToList : Tree n k v -> List (k, v)

187+treeToList : Tree n k v o -> List (k, v)

187188treeToList = treeToList' (:: [])

188189 where

189− treeToList' : ((k, v) -> List (k, v)) -> Tree n k v -> List (k, v)

190+ treeToList' : ((k, v) -> List (k, v)) -> Tree n k v o -> List (k, v)

190191 treeToList' cont (Leaf k v) = cont (k, v)

191192 treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1

192193 treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1

193194

195+abstract

194196data SortedMap : Type -> Type -> Type where

195− Empty : SortedMap k v

196− M : (n:Nat) -> Tree n k v -> SortedMap k v

197+ Empty : Ord k => SortedMap k v

198+ M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v

197199

198−empty : SortedMap k v

200+public

201+empty : Ord k => SortedMap k v

199202empty = Empty

200203

201−lookup : Ord k => k -> SortedMap k v -> Maybe v

204+public

205+lookup : k -> SortedMap k v -> Maybe v

202206lookup _ Empty = Nothing

203207lookup k (M _ t) = treeLookup k t

204208

205−insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v

209+public

210+insert : k -> v -> SortedMap k v -> SortedMap k v

206211insert k v Empty = M Z (Leaf k v)

207212insert k v (M _ t) =

208213 case treeInsert k v t of

209214 Left t' => (M _ t')

210215 Right t' => (M _ t')

211216

212−delete : Ord k => k -> SortedMap k v -> SortedMap k v

217+public

218+delete : k -> SortedMap k v -> SortedMap k v

213219delete _ Empty = Empty

214220delete k (M Z t) =

215221 case treeDelete k t of

@@ -220,18 +226,23 @@ delete k (M (S _) t) =

220226 Left t' => (M _ t')

221227 Right t' => (M _ t')

222228

229+public

223230fromList : Ord k => List (k, v) -> SortedMap k v

224231fromList l = foldl (flip (uncurry insert)) empty l

225232

233+public

226234toList : SortedMap k v -> List (k, v)

227235toList Empty = []

228236toList (M _ t) = treeToList t

229237

230−instance Functor (Tree n k) where

231− map f (Leaf k v) = Leaf k (f v)

232− map f (Branch2 t1 k t2) = Branch2 (map f t1) k (map f t2)

233− map f (Branch3 t1 k1 t2 k2 t3) = Branch3 (map f t1) k1 (map f t2) k2 (map f t3)

238+public

239+treeMap : (a -> b) -> Tree n k a o -> Tree n k b o

240+treeMap f (Leaf k v) = Leaf k (f v)

241+treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)

242+treeMap f (Branch3 t1 k1 t2 k2 t3)

243+ = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)

234244

235245instance Functor (SortedMap k) where

236246 map _ Empty = Empty

237− map f (M n t) = M _ (map f t)

247+ map f (M n t) = M _ (treeMap f t)

248+

libs/contrib/Data/SortedSet.idr+11−4

@@ -4,23 +4,30 @@ import Data.SortedMap

44

55-- TODO: add intersection, union, difference

66

7+abstract

78data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())

89

9−empty : SortedSet k

10+public

11+empty : Ord k => SortedSet k

1012empty = SetWrapper Data.SortedMap.empty

1113

12−insert : Ord k => k -> SortedSet k -> SortedSet k

14+public

15+insert : k -> SortedSet k -> SortedSet k

1316insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)

1417

15−delete : Ord k => k -> SortedSet k -> SortedSet k

18+public

19+delete : k -> SortedSet k -> SortedSet k

1620delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)

1721

18−contains : Ord k => k -> SortedSet k -> Bool

22+public

23+contains : k -> SortedSet k -> Bool

1924contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)

2025

26+public

2127fromList : Ord k => List k -> SortedSet k

2228fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))

2329

30+public

2431toList : SortedSet k -> List k

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

2633

libs/contrib/Network/Cgi.idr+1−1

@@ -108,7 +108,7 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)

108108 | _ = Nothing

109109

110110getContent : Int -> IO String

111−getContent x = getC (toNat x) "" where

111+getContent x = getC (cast x) "" where

112112 getC : Nat -> String -> IO String

113113 getC Z acc = return $ reverse acc

114114 getC (S k) acc = do x <- getChar

libs/effects/Effect/Exception.idr+3−3

@@ -4,7 +4,7 @@ import Effects

44import System

55import Control.IOExcept

66

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

88 Raise : a -> sig (Exception a) b

99

1010instance Handler (Exception a) Maybe where

@@ -14,7 +14,7 @@ instance Handler (Exception a) List where

1414 handle _ (Raise e) k = []

1515

1616instance Show a => Handler (Exception a) IO where

17− handle _ (Raise e) k = do print e

17+ handle _ (Raise e) k = do printLn e

1818 believe_me (exit 1)

1919

2020instance Handler (Exception a) (IOExcept a) where

@@ -26,5 +26,5 @@ instance Handler (Exception a) (Either a) where

2626EXCEPTION : Type -> EFFECT

2727EXCEPTION t = MkEff () (Exception t)

2828

29−raise : a -> Eff b [EXCEPTION a]

29+raise : a -> Eff b [EXCEPTION a]

3030raise err = call $ Raise err

libs/effects/Effect/StdIO.idr+18−7

@@ -9,8 +9,8 @@ import Control.IOExcept

99

1010||| The internal representation of StdIO effects

1111data StdIO : Effect where

12− PutStr : String -> sig StdIO ()

13− GetStr : sig StdIO String

12+ PutStr : String -> sig StdIO ()

13+ GetStr : sig StdIO String

1414 PutCh : Char -> sig StdIO ()

1515 GetCh : sig StdIO Char

1616

@@ -22,13 +22,13 @@ data StdIO : Effect where

2222instance Handler StdIO IO where

2323 handle () (PutStr s) k = do putStr s; k () ()

2424 handle () GetStr k = do x <- getLine; k x ()

25− handle () (PutCh c) k = do putChar c; k () ()

25+ handle () (PutCh c) k = do putChar c; k () ()

2626 handle () GetCh k = do x <- getChar; k x ()

2727

2828instance Handler StdIO (IOExcept a) where

2929 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()

3030 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()

31− handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

31+ handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

3232 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()

3333

3434-------------------------------------------------------------

@@ -42,13 +42,17 @@ STDIO = MkEff () StdIO

4242putStr : String -> Eff () [STDIO]

4343putStr s = call $ PutStr s

4444

45+||| Write a string to standard output, terminating with a newline.

46+putStrLn : String -> Eff () [STDIO]

47+putStrLn s = putStr (s ++ "\n")

48+

4549||| Write a character to standard output.

4650putChar : Char -> Eff () [STDIO]

4751putChar c = call $ PutCh c

4852

49−||| Write a string to standard output, terminating with a newline.

50−putStrLn : String -> Eff () [STDIO]

51−putStrLn s = putStr (s ++ "\n")

53+||| Write a character to standard output, terminating with a newline.

54+putCharLn : Char -> Eff () [STDIO]

55+putCharLn c = putStrLn (singleton c)

5256

5357||| Read a string from standard input.

5458getStr : Eff String [STDIO]

@@ -58,3 +62,10 @@ getStr = call $ GetStr

5862getChar : Eff Char [STDIO]

5963getChar = call $ GetCh

6064

65+||| Given a parameter `a` 'show' `a` to standard output.

66+print : Show a => a -> Eff () [STDIO]

67+print a = putStr (show a)

68+

69+||| Given a parameter `a` 'show' `a` to a standard output, terminating with a newline

70+printLn : Show a => a -> Eff () [STDIO]

71+printLn a = putStrLn (show a)

libs/prelude/Prelude.idr+11−6

@@ -134,6 +134,9 @@ instance Show a => Show (Maybe a) where

134134 show Nothing = "Nothing"

135135 show (Just x) = "Just " ++ show x

136136

137+instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

138+ show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

139+

137140---- Functor instances

138141

139142instance Functor PrimIO where

@@ -242,8 +245,8 @@ natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc

242245total natEnumFromTo : Nat -> Nat -> List Nat

243246natEnumFromTo n m = map (plus n) (natRange ((S m) - n))

244247total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat

245−natEnumFromThenTo _ Z _ = []

246−natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))

248+natEnumFromThenTo _ Z _ = []

249+natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (m - n) (S inc) SIsNotZ)))

247250

248251class Enum a where

249252 total pred : a -> a

@@ -282,7 +285,7 @@ instance Enum Integer where

282285 go [] = []

283286 go (x :: xs) = n + cast x :: go xs

284287 enumFromThenTo _ 0 _ = []

285− enumFromThenTo n inc m = go (natRange (S (fromInteger (abs (m - n)) `div` fromInteger (abs inc))))

288+ enumFromThenTo n inc m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs inc) - 1))) SIsNotZ)))

286289 where go : List Nat -> List Integer

287290 go [] = []

288291 go (x :: xs) = n + (cast x * inc) :: go xs

@@ -302,7 +305,7 @@ instance Enum Int where

302305 go acc (S k) m = go (m :: acc) k (m - 1)

303306 enumFromThen n inc = n :: enumFromThen (inc + n) inc

304307 enumFromThenTo _ 0 _ = []

305− enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))

308+ enumFromThenTo n inc m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs inc) - 1))) SIsNotZ)))

306309 where go : List Nat -> List Int

307310 go [] = []

308311 go (x :: xs) = n + (cast x * inc) :: go xs

@@ -346,7 +349,7 @@ partial

346349printLn : Show a => a -> IO' ffi ()

347350printLn x = putStrLn (show x)

348351

349−||| Read one line of input from stdin

352+||| Read one line of input from stdin, without the trailing newline

350353partial

351354getLine : IO' ffi String

352355getLine = prim_read

@@ -545,5 +548,7 @@ readFile fn = do h <- openFile fn Read

545548 readFile' h contents =

546549 do x <- feof h

547550 if not x then do l <- fread h

548− readFile' h (contents ++ l)

551+ case contents of

552+ "" => readFile' h l

553+ _ => readFile' h (contents ++ "\n" ++ l)

549554 else return contents

libs/prelude/Prelude/Classes.idr+24−12

@@ -315,10 +315,12 @@ class Integral a where

315315

316316-- ---------------------------------------------------------------- [ Integers ]

317317divBigInt : Integer -> Integer -> Integer

318−divBigInt = prim__sdivBigInt

318+divBigInt x y = case y == 0 of

319+ False => prim__sdivBigInt x y

319320

320321modBigInt : Integer -> Integer -> Integer

321−modBigInt = prim__sremBigInt

322+modBigInt x y = case y == 0 of

323+ False => prim__sremBigInt x y

322324

323325instance Integral Integer where

324326 div = divBigInt

@@ -327,10 +329,12 @@ instance Integral Integer where

327329-- --------------------------------------------------------------------- [ Int ]

328330

329331divInt : Int -> Int -> Int

330−divInt = prim__sdivInt

332+divInt x y = case y == 0 of

333+ False => prim__sdivInt x y

331334

332335modInt : Int -> Int -> Int

333−modInt = prim__sremInt

336+modInt x y = case y == 0 of

337+ False => prim__sremInt x y

334338

335339instance Integral Int where

336340 div = divInt

@@ -338,10 +342,12 @@ instance Integral Int where

338342

339343-- ------------------------------------------------------------------- [ Bits8 ]

340344divB8 : Bits8 -> Bits8 -> Bits8

341−divB8 = prim__sdivB8

345+divB8 x y = case y == 0 of

346+ False => prim__sdivB8 x y

342347

343348modB8 : Bits8 -> Bits8 -> Bits8

344−modB8 = prim__sremB8

349+modB8 x y = case y == 0 of

350+ False => prim__sremB8 x y

345351

346352instance Integral Bits8 where

347353 div = divB8

@@ -349,10 +355,12 @@ instance Integral Bits8 where

349355

350356-- ------------------------------------------------------------------ [ Bits16 ]

351357divB16 : Bits16 -> Bits16 -> Bits16

352−divB16 = prim__sdivB16

358+divB16 x y = case y == 0 of

359+ False => prim__sdivB16 x y

353360

354361modB16 : Bits16 -> Bits16 -> Bits16

355−modB16 = prim__sremB16

362+modB16 x y = case y == 0 of

363+ False => prim__sremB16 x y

356364

357365instance Integral Bits16 where

358366 div = divB16

@@ -360,10 +368,12 @@ instance Integral Bits16 where

360368

361369-- ------------------------------------------------------------------ [ Bits32 ]

362370divB32 : Bits32 -> Bits32 -> Bits32

363−divB32 = prim__sdivB32

371+divB32 x y = case y == 0 of

372+ False => prim__sdivB32 x y

364373

365374modB32 : Bits32 -> Bits32 -> Bits32

366−modB32 = prim__sremB32

375+modB32 x y = case y == 0 of

376+ False => prim__sremB32 x y

367377

368378instance Integral Bits32 where

369379 div = divB32

@@ -371,10 +381,12 @@ instance Integral Bits32 where

371381

372382-- ------------------------------------------------------------------ [ Bits64 ]

373383divB64 : Bits64 -> Bits64 -> Bits64

374−divB64 = prim__sdivB64

384+divB64 x y = case y == 0 of

385+ False => prim__sdivB64 x y

375386

376387modB64 : Bits64 -> Bits64 -> Bits64

377−modB64 = prim__sremB64

388+modB64 x y = case y == 0 of

389+ False => prim__sremB64 x y

378390

379391instance Integral Bits64 where

380392 div = divB64

libs/prelude/Prelude/List.idr+14−6

@@ -309,13 +309,12 @@ mapMaybe f (x::xs) =

309309-- Folds

310310--------------------------------------------------------------------------------

311311

312−||| A tail recursive right fold on Lists.

313−total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc

314−foldrImpl f e go [] = go e

315−foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs

316−

317312instance Foldable List where

318− foldr f e xs = foldrImpl f e id xs

313+ foldr c n [] = n

314+ foldr c n (x::xs) = c x (foldr c n xs)

315+

316+ foldl f q [] = q

317+ foldl f q (x::xs) = foldl f (f q x) xs

319318

320319--------------------------------------------------------------------------------

321320-- Special folds

@@ -809,6 +808,15 @@ hasAnyByNilFalse p (x::xs) =

809808hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False

810809hasAnyNilFalse l = ?hasAnyNilFalseBody

811810

811+foldlAsFoldr : (b -> a -> b) -> b -> List a -> b

812+foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z

813+

814+||| The definition of foldl works the same as the default definition

815+||| in terms of foldr

816+foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs

817+foldlMatchesFoldr f q [] = Refl

818+foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs

819+

812820

813821--------------------------------------------------------------------------------

814822-- Proofs

libs/prelude/Prelude/Nat.idr+36−17

@@ -288,10 +288,12 @@ fact (S n) = (S n) * fact n

288288-- Division and modulus

289289--------------------------------------------------------------------------------

290290

291−total

292−modNat : Nat -> Nat -> Nat

293−modNat left Z = left

294−modNat left (S right) = mod' left left right

291+SIsNotZ : {x: Nat} -> (S x = Z) -> Void

292+SIsNotZ Refl impossible

293+

294+modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat

295+modNatNZ left Z p = void (p Refl)

296+modNatNZ left (S right) _ = mod' left left right

295297 where

296298 total mod' : Nat -> Nat -> Nat -> Nat

297299 mod' Z centre right = centre

@@ -301,10 +303,13 @@ modNat left (S right) = mod' left left right

301303 else

302304 mod' left (centre - (S right)) right

303305

304−total

305−divNat : Nat -> Nat -> Nat

306−divNat left Z = S left -- div by zero

307−divNat left (S right) = div' left left right

306+partial

307+modNat : Nat -> Nat -> Nat

308+modNat left (S right) = modNatNZ left (S right) SIsNotZ

309+

310+divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat

311+divNatNZ left Z p = void (p Refl)

312+divNatNZ left (S right) _ = div' left left right

308313 where

309314 total div' : Nat -> Nat -> Nat -> Nat

310315 div' Z centre right = Z

@@ -314,23 +319,42 @@ divNat left (S right) = div' left left right

314319 else

315320 S (div' left (centre - (S right)) right)

316321

322+partial

323+divNat : Nat -> Nat -> Nat

324+divNat left (S right) = divNatNZ left (S right) SIsNotZ

325+

326+divCeilNZ : Nat -> (y: Nat) -> Not (y = 0) -> Nat

327+divCeilNZ x y p = case (modNatNZ x y p) of

328+ Z => divNatNZ x y p

329+ S _ => S (divNatNZ x y p)

330+

331+partial

332+divCeil : Nat -> Nat -> Nat

333+divCeil x (S y) = divCeilNZ x (S y) SIsNotZ

334+

317335instance Integral Nat where

318336 div = divNat

319337 mod = modNat

320338

339+log2NZ : (x: Nat) -> Not (x = Z) -> Nat

340+log2NZ Z p = void (p Refl)

341+log2NZ (S Z) _ = Z

342+log2NZ (S (S n)) _ = S (log2NZ (assert_smaller (S (S n)) (S (divNatNZ n 2 SIsNotZ))) SIsNotZ)

343+

344+partial

321345log2 : Nat -> Nat

322−log2 Z = Z

323−log2 (S Z) = Z

324−log2 n = S (log2 (assert_smaller n (n `divNat` 2)))

346+log2 (S n) = log2NZ (S n) SIsNotZ

325347

326348--------------------------------------------------------------------------------

327349-- GCD and LCM

328350--------------------------------------------------------------------------------

351+partial

329352gcd : Nat -> Nat -> Nat

330353gcd a Z = a

331354gcd a b = assert_total (gcd b (a `modNat` b))

332355

333−total lcm : Nat -> Nat -> Nat

356+partial

357+lcm : Nat -> Nat -> Nat

334358lcm _ Z = Z

335359lcm Z _ = Z

336360lcm x y = divNat (x * y) (gcd x y)

@@ -724,11 +748,6 @@ total sucMinR : (l : Nat) -> minimum l (S l) = l

724748sucMinR Z = Refl

725749sucMinR (S l) = cong (sucMinR l)

726750

727−-- div and mod

728−total modZeroZero : (n : Nat) -> mod 0 n = Z

729−modZeroZero Z = Refl

730−modZeroZero (S n) = Refl

731−

732751--------------------------------------------------------------------------------

733752-- Proofs

734753--------------------------------------------------------------------------------

rts/idris_gc.c+7

@@ -53,6 +53,13 @@ VAL copy(VM* vm, VAL x) {

5353 break;

5454 case FWD:

5555 return x->info.ptr;

56+ case RAWDATA:

57+ {

58+ size_t size = x->info.size + sizeof(Closure);

59+ cl = allocate(size, 0);

60+ memcpy(cl, x, size);

61+ }

62+ break;

5663 default:

5764 break;

5865 }

rts/idris_rts.c+16−3

@@ -143,7 +143,10 @@ int space(VM* vm, size_t size) {

143143}

144144

145145void* idris_alloc(size_t size) {

146− return allocate(size, 0);

146+ Closure* cl = (Closure*) allocate(sizeof(Closure)+size, 0);

147+ SETTY(cl, RAWDATA);

148+ cl->info.size = size;

149+ return (void*)cl+sizeof(Closure);

147150}

148151

149152void* idris_realloc(void* old, size_t old_size, size_t size) {

@@ -501,17 +504,20 @@ VAL idris_strlen(VM* vm, VAL l) {

501504}

502505

503506VAL idris_readStr(VM* vm, FILE* h) {

507+ VAL ret;

504508 char *buffer = NULL;

505509 size_t n = 0;

506510 ssize_t len;

507511 len = getline(&buffer, &n, h);

512+ strtok(buffer, "\n");

508513

509514 if (len <= 0) {

510− return MKSTR(vm, "");

515+ ret = MKSTR(vm, "");

511516 } else {

512− return MKSTR(vm, buffer);

517+ ret = MKSTR(vm, buffer);

513518 }

514519 free(buffer);

520+ return ret;

515521}

516522

517523VAL idris_strHead(VM* vm, VAL str) {

@@ -712,6 +718,13 @@ VAL doCopyTo(VM* vm, VAL x) {

712718 case BITS64:

713719 cl = idris_b64CopyForGC(vm, x);

714720 break;

721+ case RAWDATA:

722+ {

723+ size_t size = x->info.size + sizeof(Closure);

724+ cl = allocate(size, 0);

725+ memcpy(cl, x, size);

726+ }

727+ break;

715728 default:

716729 assert(0); // We're in trouble if this happens...

717730 }

rts/idris_rts.h+2−1

@@ -26,7 +26,7 @@

2626typedef enum {

2727 CON, INT, BIGINT, FLOAT, STRING, STROFFSET,

2828 BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD,

29− MANAGEDPTR

29+ MANAGEDPTR, RAWDATA

3030} ClosureType;

3131

3232typedef struct Closure *VAL;

@@ -76,6 +76,7 @@ typedef struct Closure {

7676 __m128i* bits128p;

7777 Buffer* buf;

7878 ManagedPtr* mptr;

79+ size_t size;

7980 } info;

8081} Closure;

8182

src/IRTS/Compiler.hs+3−3

@@ -235,7 +235,7 @@ data VarInfo = VI

235235type Vars = M.Map Name VarInfo

236236

237237irTerm :: Vars -> [Name] -> Term -> Idris LExp

238−irTerm vs env tm@(App f a) = do

238+irTerm vs env tm@(App _ f a) = do

239239 ist <- getIState

240240 case unApply tm of

241241 (P _ (UN m) _, args)

@@ -297,8 +297,8 @@ irTerm vs env tm@(App f a) = do

297297

298298 -- This case is here until we get more general inlining. It's just

299299 -- a really common case, and the laziness hurts...

300− (P _ (NS (UN be) [b,p]) _, [_,x,(App (App (App (P _ (UN d) _) _) _) t),

301− (App (App (App (P _ (UN d') _) _) _) e)])

300+ (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),

301+ (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])

302302 | be == txt "boolElim"

303303 , d == txt "Delay"

304304 , d' == txt "Delay"

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1258,14 +1258,14 @@ infP = P (TCon 6 0) inferTy (TType (UVal 0))

12581258

12591259getInferTerm, getInferType :: Term -> Term

12601260getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

1261−getInferTerm (App (App _ _) tm) = tm

1261+getInferTerm (App _ (App _ _ _) tm) = tm

12621262getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

12631263

12641264getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

12651265 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))

12661266 toTy (PVar t) = PVTy t

12671267 toTy b = b

1268−getInferType (App (App _ ty) _) = ty

1268+getInferType (App _ (App _ _ ty) _) = ty

12691269

12701270

12711271

src/Idris/Apropos.hs+1−1

@@ -77,7 +77,7 @@ instance Apropos (TT Name) where

7777 isApropos str (P (DCon _ _ _) n ty) = isApropos str n || isApropos str ty

7878 isApropos str (P Bound _ ty) = isApropos str ty

7979 isApropos str (Bind n b tm) = isApropos str b || isApropos str tm

80− isApropos str (App t1 t2) = isApropos str t1 || isApropos str t2

80+ isApropos str (App _ t1 t2) = isApropos str t1 || isApropos str t2

8181 isApropos str (Constant const) = isApropos str const

8282 isApropos str _ = False

8383

src/Idris/CaseSplit.hs+1−1

@@ -10,13 +10,13 @@ module Idris.CaseSplit(splitOnLine, replaceSplits,

1010import Idris.AbsSyntax

1111import Idris.AbsSyntaxTree (Idris, IState, PTerm)

1212import Idris.ElabDecls

13−import Idris.ElabTerm

1413import Idris.Delaborate

1514import Idris.Parser

1615import Idris.Error

1716import Idris.Output

1817

1918import Idris.Elab.Value

19+import Idris.Elab.Term

2020

2121import Idris.Core.TT

2222import Idris.Core.Typecheck

src/Idris/Core/Binary.hs+4−4

@@ -555,9 +555,9 @@ instance {- (Binary n) => -} Binary (TT Name) where

555555 put x1

556556 put x2

557557 put x3

558− App x1 x2 -> do putWord8 3

559− put x1

560− put x2

558+ App _ x1 x2 -> do putWord8 3

559+ put x1

560+ put x2

561561 Constant x1 -> do putWord8 4

562562 put x1

563563 Proj x1 x2 -> do putWord8 5

@@ -584,7 +584,7 @@ instance {- (Binary n) => -} Binary (TT Name) where

584584 return (Bind x1 x2 x3)

585585 3 -> do x1 <- get

586586 x2 <- get

587− return (App x1 x2)

587+ return (App Complete x1 x2)

588588 4 -> do x1 <- get

589589 return (Constant x1)

590590 5 -> do x1 <- get

src/Idris/Core/CaseTree.hs+8−8

@@ -130,7 +130,7 @@ namesUsed sc = nub $ nu' [] sc where

130130

131131 nut ps (P _ n _) | n `elem` ps = []

132132 | otherwise = [n]

133− nut ps (App f a) = nut ps f ++ nut ps a

133+ nut ps (App _ f a) = nut ps f ++ nut ps a

134134 nut ps (Proj t _) = nut ps t

135135 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

136136 nut ps (Bind n b sc) = nut (n:ps) sc

@@ -154,7 +154,7 @@ findCalls sc topargs = nub $ nu' topargs sc where

154154

155155 nut ps (P Ref n _) | n `elem` ps = []

156156 | otherwise = [(n, [])] -- tmp

157− nut ps fn@(App f a)

157+ nut ps fn@(App _ f a)

158158 | (P Ref n _, args) <- unApply fn

159159 = if n `elem` ps then nut ps f ++ nut ps a

160160 else [(n, map argNames args)] ++ concatMap (nut ps) args

@@ -175,8 +175,8 @@ directUse (P _ n _) = [n]

175175directUse (Bind n (Let t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])

176176 ++ directUse t

177177directUse (Bind n b sc) = nub $ directUse (binderTy b) ++ (directUse sc \\ [n])

178−directUse fn@(App f a)

179− | (P Ref (UN pfk) _, [App e w]) <- unApply fn,

178+directUse fn@(App _ f a)

179+ | (P Ref (UN pfk) _, [App _ e w]) <- unApply fn,

180180 pfk == txt "prim_fork"

181181 = directUse e ++ directUse w -- HACK so that fork works

182182 | (P Ref (UN fce) _, [_, _, a]) <- unApply fn,

@@ -336,7 +336,7 @@ data Pat = PCon Bool Name Int [Pat]

336336

337337toPats :: Bool -> Bool -> Term -> [Pat]

338338toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where

339− getArgs (App f a) = a : getArgs f

339+ getArgs (App _ f a) = a : getArgs f

340340 getArgs _ = []

341341

342342toPat :: Bool -> Bool -> [Term] -> [Pat]

@@ -361,7 +361,7 @@ toPat reflect tc = map $ toPat' []

361361 = PSuc $ toPat' [] p

362362

363363 toPat' [] (P Bound n ty) = PV n ty

364− toPat' args (App f a) = toPat' (a : args) f

364+ toPat' args (App _ f a) = toPat' (a : args) f

365365 toPat' [] (Constant x) | isTypeConst x = PTyPat

366366 | otherwise = PConst x

367367

@@ -638,7 +638,7 @@ depatt ns tm = dp [] tm

638638 dpa ms x (SucCase n sc) = SucCase n (dp ms sc)

639639 dpa ms x (DefaultCase sc) = DefaultCase (dp ms sc)

640640

641− applyMaps ms f@(App _ _)

641+ applyMaps ms f@(App _ _ _)

642642 | (P nt cn pty, args) <- unApply f

643643 = let args' = map (applyMaps ms) args in

644644 applyMap ms nt cn pty args'

@@ -651,7 +651,7 @@ depatt ns tm = dp [] tm

651651 same n (P _ n' _) = n == n'

652652 same _ _ = False

653653

654− applyMaps ms (App f a) = App (applyMaps ms f) (applyMaps ms a)

654+ applyMaps ms (App s f a) = App s (applyMaps ms f) (applyMaps ms a)

655655 applyMaps ms t = t

656656

657657-- FIXME: Do this for SucCase too

src/Idris/Core/DeepSeq.hs+1−1

@@ -160,7 +160,7 @@ instance (NFData n) => NFData (TT n) where

160160 rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

161161 rnf (V x1) = rnf x1 `seq` ()

162162 rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

163− rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

163+ rnf (App x1 x2 x3) = rnf x2 `seq` rnf x3 `seq` ()

164164 rnf (Constant x1) = rnf x1 `seq` ()

165165 rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

166166 rnf Erased = ()

src/Idris/Core/Elaborate.hs+3−3

@@ -258,7 +258,7 @@ checkInjective (tm, l, r) = do ctxt <- get_context

258258 else lift $ tfail (NotInjective tm l r)

259259 where isInj ctxt (P _ n _)

260260 | isConName n ctxt = True

261− isInj ctxt (App f a) = isInj ctxt f

261+ isInj ctxt (App _ f a) = isInj ctxt f

262262 isInj ctxt (Constant _) = True

263263 isInj ctxt (TType _) = True

264264 isInj ctxt (Bind _ (Pi _ _ _) sc) = True

@@ -431,7 +431,7 @@ dotterm = do ES (p, a) s m <- get

431431 where foB (Guess t v) = union (findOuter h env t) (findOuter h (n:env) v)

432432 foB (Let t v) = union (findOuter h env t) (findOuter h env v)

433433 foB b = findOuter h env (binderTy b)

434− findOuter h env (App f a)

434+ findOuter h env (App _ f a)

435435 = union (findOuter h env f) (findOuter h env a)

436436 findOuter h env _ = []

437437

@@ -541,7 +541,7 @@ prepare_apply fn imps =

541541 | n `elem` hs = let n' = uniqueName n hs in

542542 Bind n' (fmap (rebind hs) t) (rebind (n':hs) sc)

543543 | otherwise = Bind n (fmap (rebind hs) t) (rebind (n:hs) sc)

544− rebind hs (App f a) = App (rebind hs f) (rebind hs a)

544+ rebind hs (App s f a) = App s (rebind hs f) (rebind hs a)

545545 rebind hs t = t

546546

547547apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

src/Idris/Core/Evaluate.hs+11−11

@@ -285,7 +285,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

285285 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

286286 -- block reduction immediately under codata (and not forced)

287287 ev ntimes stk top env

288− (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

288+ (App _ (App _ (App _ d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

289289 | dly == txt "Delay" && lco == txt "LazyCodata" && not (simpl || atRepl)

290290 = do let (f, _) = unApply arg

291291 let ntimes' = case f of

@@ -299,11 +299,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

299299 when spec $ setBlock False

300300 evApply ntimes' stk top env [l',t',arg'] d'

301301 -- Treat "assert_total" specially, as long as it's defined!

302− ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)

302+ ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)

303303 | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl) ctxt,

304304 at == txt "assert_total" && not simpl

305305 = ev ntimes (n : stk) top env arg

306− ev ntimes stk top env (App f a)

306+ ev ntimes stk top env (App _ f a)

307307 = do f' <- ev ntimes stk False env f

308308 a' <- ev ntimes stk False env a

309309 evApply ntimes stk top env [a'] f'

@@ -434,7 +434,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

434434 Just (altmap, sc) -> evTree ntimes stk top env altmap sc

435435 _ -> return Nothing

436436

437− conHeaded tm@(App _ _)

437+ conHeaded tm@(App _ _ _)

438438 | (P (DCon _ _ _) _ _, args) <- unApply tm = True

439439 conHeaded t = False

440440

@@ -540,7 +540,7 @@ instance Quote Value where

540540 v' <- quote i v

541541 let sc'' = pToV (sMN vd "vlet") (addBinder sc')

542542 return (Bind n (Let t' v') sc'')

543− quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

543+ quote i (VApp f a) = liftM2 (App MaybeHoles) (quote i f) (quote i a)

544544 quote i (VType u) = return $ TType u

545545 quote i (VUType u) = return $ UType u

546546 quote i VErased = return $ Erased

@@ -576,13 +576,13 @@ convEq ctxt holes topx topy = ceq [] topx topy where

576576 | x `elem` holes || y `elem` holes = return True

577577 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

578578 | otherwise = sameDefs ps x y

579− ceq ps x (Bind n (Lam t) (App y (V 0)))

579+ ceq ps x (Bind n (Lam t) (App _ y (V 0)))

580580 = ceq ps x (substV (P Bound n t) y)

581− ceq ps (Bind n (Lam t) (App x (V 0))) y

581+ ceq ps (Bind n (Lam t) (App _ x (V 0))) y

582582 = ceq ps (substV (P Bound n t) x) y

583− ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))

583+ ceq ps x (Bind n (Lam t) (App _ y (P Bound n' _)))

584584 | n == n' = ceq ps x y

585− ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

585+ ceq ps (Bind n (Lam t) (App _ x (P Bound n' _))) y

586586 | n == n' = ceq ps x y

587587

588588 ceq ps (Bind n (PVar t) sc) y = ceq ps sc y

@@ -604,7 +604,7 @@ convEq ctxt holes topx topy = ceq [] topx topy where

604604 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

605605 ceqB ps (Pi i v t) (Pi i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

606606 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

607− ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

607+ ceq ps (App _ fx ax) (App _ fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

608608 ceq ps (Constant x) (Constant y) = return (x == y)

609609 ceq ps (TType x) (TType y) = do (v, cs) <- get

610610 put (v, ULE x y : cs)

@@ -1085,5 +1085,5 @@ uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name

10851085uniqueBindersCtxt ctxt ns (Bind n b sc)

10861086 = let n' = uniqueNameCtxt ctxt n ns in

10871087 Bind n' (fmap (uniqueBindersCtxt ctxt (n':ns)) b) (uniqueBindersCtxt ctxt ns sc)

1088−uniqueBindersCtxt ctxt ns (App f a) = App (uniqueBindersCtxt ctxt ns f) (uniqueBindersCtxt ctxt ns a)

1088+uniqueBindersCtxt ctxt ns (App s f a) = App s (uniqueBindersCtxt ctxt ns f) (uniqueBindersCtxt ctxt ns a)

10891089uniqueBindersCtxt ctxt ns t = t

src/Idris/Core/Execute.hs+2−2

@@ -103,7 +103,7 @@ toTT (EBind n b body) = do n' <- newN n

103103 return n'

104104toTT (EApp e1 e2) = do e1' <- toTT e1

105105 e2' <- toTT e2

106− return $ App e1' e2'

106+ return $ App Complete e1' e2'

107107toTT (EType u) = return $ TType u

108108toTT (EUType u) = return $ UType u

109109toTT EErased = return Erased

@@ -192,7 +192,7 @@ doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

192192doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)

193193 return $

194194 EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)

195−doExec env ctxt a@(App _ _) =

195+doExec env ctxt a@(App _ _ _) =

196196 do let (f, args) = unApply a

197197 f' <- doExec env ctxt f

198198 args' <- case f' of

src/Idris/Core/ProofState.hs+34−11

@@ -328,7 +328,7 @@ computeLet ctxt n tm = cl [] tm where

328328 | n' == n = let v' = normalise ctxt env v in

329329 Bind n' (Let t v') sc

330330 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)

331− cl env (App f a) = App (cl env f) (cl env a)

331+ cl env (App s f a) = App s (cl env f) (cl env a)

332332 cl env t = t

333333

334334attack :: RunTactic

@@ -551,13 +551,36 @@ solve ctxt env (Bind x (Guess ty val) sc)

551551 recents = x : recents ps,

552552 instances = instances ps \\ [x],

553553 dotted = dropUnified dropdots (dotted ps) })

554− let tm' = subst x val sc in

555− return tm'

554+ let (locked, did) = tryLock (holes ps \\ [x]) (updsubst x val sc) in

555+ return locked

556556 where dropUnified ddots [] = []

557557 dropUnified ddots ((x, es) : ds)

558558 | x `elem` ddots || any (\e -> e `elem` ddots) es

559559 = dropUnified ddots ds

560560 | otherwise = (x, es) : dropUnified ddots ds

561+

562+ tryLock :: [Name] -> Term -> (Term, Bool)

563+ tryLock hs tm@(App Complete _ _) = (tm, True)

564+ tryLock hs tm@(App s f a) =

565+ let (f', fl) = tryLock hs f

566+ (a', al) = tryLock hs a in

567+ if fl && al then (App Complete f' a', True)

568+ else (App s f' a', False)

569+ tryLock hs t@(P _ n _) = (t, not $ n `elem` hs)

570+ tryLock hs t@(Bind n (Hole _) sc) = (t, False)

571+ tryLock hs t@(Bind n (Guess _ _) sc) = (t, False)

572+ tryLock hs t@(Bind n (Let ty val) sc)

573+ = let (ty', tyl) = tryLock hs ty

574+ (val', vall) = tryLock hs val

575+ (sc', scl) = tryLock hs sc in

576+ (Bind n (Let ty' val') sc', tyl && vall && scl)

577+ tryLock hs t@(Bind n b sc)

578+ = let (bt', btl) = tryLock hs (binderTy b)

579+ (val', vall) = tryLock hs val

580+ (sc', scl) = tryLock hs sc in

581+ (Bind n (b { binderTy = bt' }) sc', btl && scl)

582+ tryLock hs t = (t, True)

583+

561584solve _ _ h@(Bind x t sc)

562585 = do ps <- get

563586 case findType x sc of

@@ -581,7 +604,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

581604 (tyv, tyt) <- lift $ check ctxt env ty

582605-- ns <- lift $ unify ctxt env tyv t'

583606 case t' of

584− Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in

607+ Bind y (Pi _ s _) t -> let t' = updsubst y (P Bound n s) t in

585608 do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)

586609 ps <- get

587610 let (uh, uns) = unified ps

@@ -600,7 +623,7 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

600623 _ -> hnf ctxt env t

601624 case t' of

602625 Bind y (Pi _ s _) t -> -- trace ("in type " ++ show t') $

603− let t' = subst y (P Bound n s) t in

626+ let t' = updsubst y (P Bound n s) t in

604627 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

605628 _ -> lift $ tfail $ CantIntroduce t'

606629intro n ctxt env _ = fail "Can't introduce here."

@@ -623,7 +646,7 @@ patvar n ctxt env (Bind x (Hole t) sc) =

623646 (notunified ps),

624647 injective = addInj n x (injective ps)

625648 })

626− return $ Bind n (PVar t) (subst x (P Bound n t) sc)

649+ return $ Bind n (PVar t) (updsubst x (P Bound n t) sc)

627650 where addInj n x ps | x `elem` ps = n : ps

628651 | otherwise = ps

629652patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm

@@ -638,7 +661,7 @@ letbind n ty val ctxt env _ = fail "Can't let bind here"

638661

639662expandLet :: Name -> Term -> RunTactic

640663expandLet n v ctxt env tm =

641− return $ subst n v tm

664+ return $ updsubst n v tm

642665

643666rewrite :: Raw -> RunTactic

644667rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

@@ -661,9 +684,9 @@ rewrite _ _ _ _ = fail "Can't rewrite here"

661684-- an x, and put \x : lt in front

662685mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name

663686mkP lt l r ty | l == ty = lt

664−mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f

665− a' = if (r /= a) then mkP lt l r a else a in

666− App f' a'

687+mkP lt l r (App s f a) = let f' = if (r /= f) then mkP lt l r f else f

688+ a' = if (r /= a) then mkP lt l r a else a in

689+ App s f' a'

667690mkP lt l r (Bind n b sc)

668691 = let b' = mkPB b

669692 sc' = if (r /= sc) then mkP lt l r sc else sc in

@@ -750,7 +773,7 @@ patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

750773 x@(Bind y (PVTy s) t) -> x

751774 _ -> hnf ctxt env t

752775 case t' of

753− Bind y (PVTy s) t -> let t' = subst y (P Bound n s) t in

776+ Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in

754777 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))

755778 _ -> fail "Nothing to pattern bind"

756779patbind n ctxt env _ = fail "Can't pattern bind here"

src/Idris/Core/ProofTerm.hs+68−20

@@ -7,7 +7,7 @@ evaluation/checking inside the proof system, etc.

77

88module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,

99 updateSolved, updateSolvedTerm, updateSolvedTerm',

10− bound_in, bound_in_term, refocus,

10+ bound_in, bound_in_term, refocus, updsubst,

1111 Hole, RunTactic',

1212 goal, atHole) where

1313

@@ -21,8 +21,8 @@ import Debug.Trace

2121

2222-- | A zipper over terms, in order to efficiently update proof terms.

2323data TermPath = Top

24− | AppL TermPath Term

25− | AppR Term TermPath

24+ | AppL (AppStatus Name) TermPath Term

25+ | AppR (AppStatus Name) Term TermPath

2626 | InBind Name BinderPath Term

2727 | InScope Name (Binder Term) TermPath

2828 deriving Show

@@ -39,8 +39,8 @@ data BinderPath = Binder (Binder TermPath)

3939-- words, "graft" one term path into another.

4040replaceTop :: TermPath -> TermPath -> TermPath

4141replaceTop p Top = p

42−replaceTop p (AppL l t) = AppL (replaceTop p l) t

43−replaceTop p (AppR t r) = AppR t (replaceTop p r)

42+replaceTop p (AppL s l t) = AppL s (replaceTop p l) t

43+replaceTop p (AppR s t r) = AppR s t (replaceTop p r)

4444replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc

4545 where

4646 replaceTopB p (Binder b) = Binder (fmap (replaceTop p) b)

@@ -53,8 +53,8 @@ replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)

5353-- | Build a term from a zipper, given something to put in the hole.

5454rebuildTerm :: Term -> TermPath -> Term

5555rebuildTerm tm Top = tm

56−rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a

57−rebuildTerm tm (AppR f p) = App f (rebuildTerm tm p)

56+rebuildTerm tm (AppL s p a) = App s (rebuildTerm tm p) a

57+rebuildTerm tm (AppR s f p) = App s f (rebuildTerm tm p)

5858rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)

5959rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc

6060

@@ -73,9 +73,10 @@ findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)

7373findHole n env t = fh' env Top t where

7474 fh' env path tm@(Bind x h sc)

7575 | hole h && n == x = Just (path, env, tm)

76− fh' env path (App f a)

77− | Just (p, env', tm) <- fh' env path a = Just (AppR f p, env', tm)

78− | Just (p, env', tm) <- fh' env path f = Just (AppL p a, env', tm)

76+ fh' env path (App Complete _ _) = Nothing

77+ fh' env path (App s f a)

78+ | Just (p, env', tm) <- fh' env path a = Just (AppR s f p, env', tm)

79+ | Just (p, env', tm) <- fh' env path f = Just (AppL s p a, env', tm)

7980 fh' env path (Bind x b sc)

8081 | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)

8182 | Just (p, env', tm) <- fh' ((x,b):env) path sc = Just (InScope x b p, env', tm)

@@ -156,19 +157,20 @@ updateSolvedTerm' xs x = updateSolved' xs x where

156157 updateSolved' xs (Bind n (Hole ty) t)

157158 | Just v <- lookup n xs

158159 = case xs of

159− [_] -> (subst n v t, True) -- some may be Vs! Can't assume

160+ [_] -> (updsubst n v t, True) -- some may be Vs! Can't assume

160161 -- explicit names

161162 _ -> let (t', _) = updateSolved' xs t in

162− (subst n v t', True)

163+ (updsubst n v t', True)

163164 updateSolved' xs tm@(Bind n b t)

164165 | otherwise = let (t', ut) = updateSolved' xs t

165166 (b', ub) = updateSolvedB' xs b in

166167 if ut || ub then (Bind n b' t', True)

167168 else (tm, False)

168− updateSolved' xs t@(App f a)

169+ updateSolved' xs t@(App Complete f a) = (t, False)

170+ updateSolved' xs t@(App s f a)

169171 = let (f', uf) = updateSolved' xs f

170172 (a', ua) = updateSolved' xs a in

171− if uf || ua then (App f' a', True)

173+ if uf || ua then (App s f' a', True)

172174 else (t, False)

173175 updateSolved' xs t@(P _ n@(MN _ _) _)

174176 | Just v <- lookup n xs = (v, True)

@@ -189,7 +191,7 @@ updateSolvedTerm' xs x = updateSolved' xs x where

189191 if u then (b { binderTy = ty' }, u) else (b, False)

190192

191193 noneOf ns (P _ n _) | n `elem` ns = False

192− noneOf ns (App f a) = noneOf ns a && noneOf ns f

194+ noneOf ns (App s f a) = noneOf ns a && noneOf ns f

193195 noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t

194196 noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b

195197 where

@@ -198,6 +200,49 @@ updateSolvedTerm' xs x = updateSolved' xs x where

198200 noneOfB ns b = noneOf ns (binderTy b)

199201 noneOf ns _ = True

200202

203+-- | As 'subst', in TT, but takes advantage of knowing not to substitute

204+-- under Complete applications.

205+updsubst :: Eq n => n {-^ The id to replace -} ->

206+ TT n {-^ The replacement term -} ->

207+ TT n {-^ The term to replace in -} ->

208+ TT n

209+-- subst n v tm = instantiate v (pToV n tm)

210+updsubst n v tm = fst $ subst' 0 tm

211+ where

212+ -- keep track of updates to save allocations - this is a big win on

213+ -- large terms in particular

214+ -- ('Maybe' would be neater here, but >>= is not the right combinator.

215+ -- Feel free to tidy up, as long as it still saves allocating when no

216+ -- substitution happens...)

217+ subst' i (V x) | i == x = (v, True)

218+ subst' i (P _ x _) | n == x = (v, True)

219+ subst' i t@(P nt x ty)

220+ = let (ty', ut) = subst' i ty in

221+ if ut then (P nt x ty', True) else (t, False)

222+ subst' i t@(Bind x b sc) | x /= n

223+ = let (b', ub) = substB' i b

224+ (sc', usc) = subst' (i+1) sc in

225+ if ub || usc then (Bind x b' sc', True) else (t, False)

226+ subst' i t@(App Complete f a) = (t, False)

227+ subst' i t@(App s f a) = let (f', uf) = subst' i f

228+ (a', ua) = subst' i a in

229+ if uf || ua then (App s f' a', True) else (t, False)

230+ subst' i t@(Proj x idx) = let (x', u) = subst' i x in

231+ if u then (Proj x' idx, u) else (t, False)

232+ subst' i t = (t, False)

233+

234+ substB' i b@(Let t v) = let (t', ut) = subst' i t

235+ (v', uv) = subst' i v in

236+ if ut || uv then (Let t' v', True)

237+ else (b, False)

238+ substB' i b@(Guess t v) = let (t', ut) = subst' i t

239+ (v', uv) = subst' i v in

240+ if ut || uv then (Guess t' v', True)

241+ else (b, False)

242+ substB' i b = let (ty', u) = subst' i (binderTy b) in

243+ if u then (b { binderTy = ty' }, u) else (b, False)

244+

245+

201246-- | Apply solutions to an environment.

202247updateEnv :: [(Name, Term)] -> Env -> Env

203248updateEnv [] e = e

@@ -208,8 +253,10 @@ updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns e

208253updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath

209254updateSolvedPath [] t = t

210255updateSolvedPath ns Top = Top

211−updateSolvedPath ns (AppL p r) = AppL (updateSolvedPath ns p) (updateSolvedTerm ns r)

212−updateSolvedPath ns (AppR l p) = AppR (updateSolvedTerm ns l) (updateSolvedPath ns p)

256+updateSolvedPath ns t@(AppL Complete _ _) = t

257+updateSolvedPath ns t@(AppR Complete _ _) = t

258+updateSolvedPath ns (AppL s p r) = AppL s (updateSolvedPath ns p) (updateSolvedTerm ns r)

259+updateSolvedPath ns (AppR s l p) = AppR s (updateSolvedTerm ns l) (updateSolvedPath ns p)

213260updateSolvedPath ns (InBind n b sc)

214261 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)

215262 where

@@ -246,7 +293,8 @@ goal h pt@(PT path env sub ups)

246293 g env (Bind n b sc) | hole b && same h n = return $ GD env b

247294 | otherwise

248295 = g ((n, b):env) sc `mplus` gb env b

249− g env (App f a) = g env a `mplus` g env f

296+ g env (App Complete f a) = fail "Can't find hole"

297+ g env (App _ f a) = g env a `mplus` g env f

250298 g env t = fail "Can't find hole"

251299

252300 gb env (Let t v) = g env v `mplus` g env t

@@ -291,7 +339,7 @@ atHole h f c e pt -- @(PT path env sub)

291339 if u then return (Bind n b sc', True)

292340 else do (b', u) <- atHb f c env b

293341 return (Bind n b' sc', u)

294− atH tac c env (App f a) = ulift2 tac c env App f a

342+ atH tac c env (App s f a) = ulift2 tac c env (App s) f a

295343 atH tac c env t = return (t, False)

296344

297345 atHb f c env (Let t v) = ulift2 f c env Let t v

@@ -308,6 +356,6 @@ bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc

308356 bi (Let t v) = bound_in_term t ++ bound_in_term v

309357 bi (Guess t v) = bound_in_term t ++ bound_in_term v

310358 bi b = bound_in_term (binderTy b)

311−bound_in_term (App f a) = bound_in_term f ++ bound_in_term a

359+bound_in_term (App _ f a) = bound_in_term f ++ bound_in_term a

312360bound_in_term _ = []

313361

src/Idris/Core/TT.hs+45−40

@@ -808,6 +808,11 @@ instance Eq NameType where

808808 TCon _ a == TCon _ b = (a == b) -- ignore tag

809809 _ == _ = False

810810

811+data AppStatus n = Complete

812+ | MaybeHoles

813+ | Holes [n]

814+ deriving (Eq, Ord, Functor, Data, Typeable, Show)

815+

811816-- | Terms in the core language. The type parameter is the type of

812817-- identifiers used for bindings and explicit named references;

813818-- usually we use @TT 'Name'@.

@@ -816,7 +821,7 @@ data TT n = P NameType n (TT n) -- ^ named references with type

816821 -- Pure Type Systems Formalized)

817822 | V !Int -- ^ a resolved de Bruijn-indexed variable

818823 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding

819− | App !(TT n) (TT n) -- ^ function, function type, arg

824+ | App (AppStatus n) !(TT n) (TT n) -- ^ function, function type, arg

820825 | Constant Const -- ^ constant

821826 | Proj (TT n) !Int -- ^ argument projection; runtime only

822827 -- (-1) is a special case for 'subtract one from BI'

@@ -852,7 +857,7 @@ instance TermSize (TT Name) where

852857 termsize n (Bind n' b sc)

853858 = let rn = if n == n' then sMN 0 "noname" else n in

854859 termsize rn sc

855− termsize n (App f a) = termsize n f + termsize n a

860+ termsize n (App _ f a) = termsize n f + termsize n a

856861 termsize n (Proj t i) = termsize n t

857862 termsize n _ = 1

858863

@@ -860,7 +865,7 @@ instance Sized a => Sized (TT a) where

860865 size (P name n trm) = 1 + size name + size n + size trm

861866 size (V v) = 1

862867 size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy

863− size (App l r) = 1 + size l + size r

868+ size (App _ l r) = 1 + size l + size r

864869 size (Constant c) = size c

865870 size Erased = 1

866871 size (TType u) = 1 + size u

@@ -881,8 +886,8 @@ instance Eq n => Eq (TT n) where

881886 (==) (P xt x _) (P yt y _) = x == y

882887 (==) (V x) (V y) = x == y

883888 (==) (Bind _ xb xs) (Bind _ yb ys) = xs == ys && xb == yb

884− (==) (App fx ax) (App fy ay) = ax == ay && fx == fy

885− (==) (TType _) (TType _) = True -- deal with constraints later

889+ (==) (App _ fx ax) (App _ fy ay) = ax == ay && fx == fy

890+ (==) (TType _) (TType _) = True -- deal with constraints later

886891 (==) (Constant x) (Constant y) = x == y

887892 (==) (Proj x i) (Proj y j) = x == y && i == j

888893 (==) Erased _ = True

@@ -898,15 +903,15 @@ isInjective :: TT n -> Bool

898903isInjective (P (DCon _ _ _) _ _) = True

899904isInjective (P (TCon _ _) _ _) = True

900905isInjective (Constant _) = True

901−isInjective (TType x) = True

906+isInjective (TType x) = True

902907isInjective (Bind _ (Pi _ _ _) sc) = True

903−isInjective (App f a) = isInjective f

908+isInjective (App _ f a) = isInjective f

904909isInjective _ = False

905910

906911-- | Count the number of instances of a de Bruijn index in a term

907912vinstances :: Int -> TT n -> Int

908913vinstances i (V x) | i == x = 1

909−vinstances i (App f a) = vinstances i f + vinstances i a

914+vinstances i (App _ f a) = vinstances i f + vinstances i a

910915vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc

911916 where instancesB (Let t v) = vinstances i v

912917 instancesB _ = 0

@@ -918,7 +923,7 @@ instantiate e = subst 0 where

918923 subst i (P nt x ty) = P nt x (subst i ty)

919924 subst i (V x) | i == x = e

920925 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

921− subst i (App f a) = App (subst i f) (subst i a)

926+ subst i (App s f a) = App s (subst i f) (subst i a)

922927 subst i (Proj x idx) = Proj (subst i x) idx

923928 subst i t = t

924929

@@ -931,7 +936,7 @@ substV x tm = dropV 0 (instantiate x tm) where

931936 dropV i (V x) | x > i = V (x - 1)

932937 | otherwise = V x

933938 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

934− dropV i (App f a) = App (dropV i f) (dropV i a)

939+ dropV i (App s f a) = App s (dropV i f) (dropV i a)

935940 dropV i (Proj x idx) = Proj (dropV i x) idx

936941 dropV i t = t

937942

@@ -942,7 +947,7 @@ explicitNames (Bind x b sc) = let b' = fmap explicitNames b in

942947 Bind x b'

943948 (explicitNames (instantiate

944949 (P Bound x (binderTy b')) sc))

945−explicitNames (App f a) = App (explicitNames f) (explicitNames a)

950+explicitNames (App s f a) = App s (explicitNames f) (explicitNames a)

946951explicitNames (Proj x idx) = Proj (explicitNames x) idx

947952explicitNames t = t

948953

@@ -956,7 +961,7 @@ pToV' n i (Bind x b sc)

956961-- resolve names from the *outer* scope which may happen to have the same id.

957962 | n == x = Bind x (fmap (pToV' n i) b) sc

958963 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)

959−pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

964+pToV' n i (App s f a) = App s (pToV' n i f) (pToV' n i a)

960965pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

961966pToV' n i t = t

962967

@@ -967,7 +972,7 @@ addBinder t = ab 0 t

967972 ab top (V i) | i >= top = V (i + 1)

968973 | otherwise = V i

969974 ab top (Bind x b sc) = Bind x (fmap (ab top) b) (ab (top + 1) sc)

970− ab top (App f a) = App (ab top f) (ab top a)

975+ ab top (App s f a) = App s (ab top f) (ab top a)

971976 ab top (Proj t idx) = Proj (ab top t) idx

972977 ab top t = t

973978

@@ -986,14 +991,14 @@ vToP = vToP' [] where

986991 P Bound n (binderTy b)

987992 vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in

988993 Bind n b' (vToP' ((n, b'):env) sc)

989− vToP' env (App f a) = App (vToP' env f) (vToP' env a)

994+ vToP' env (App s f a) = App s (vToP' env f) (vToP' env a)

990995 vToP' env t = t

991996

992997-- | Replace every non-free reference to the name of a binding in

993998-- the given term with a de Bruijn index.

994999finalise :: Eq n => TT n -> TT n

9951000finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))

996−finalise (App f a) = App (finalise f) (finalise a)

1001+finalise (App s f a) = App s (finalise f) (finalise a)

9971002finalise t = t

9981003

9991004-- Once we've finished checking everything about a term we no longer need

@@ -1001,7 +1006,7 @@ finalise t = t

10011006

10021007pEraseType :: TT n -> TT n

10031008pEraseType (P nt t _) = P nt t Erased

1004−pEraseType (App f a) = App (pEraseType f) (pEraseType a)

1009+pEraseType (App s f a) = App s (pEraseType f) (pEraseType a)

10051010pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)

10061011pEraseType t = t

10071012

@@ -1028,9 +1033,9 @@ subst n v tm = fst $ subst' 0 tm

10281033 = let (b', ub) = substB' i b

10291034 (sc', usc) = subst' (i+1) sc in

10301035 if ub || usc then (Bind x b' sc', True) else (t, False)

1031− subst' i t@(App f a) = let (f', uf) = subst' i f

1032− (a', ua) = subst' i a in

1033− if uf || ua then (App f' a', True) else (t, False)

1036+ subst' i t@(App s f a) = let (f', uf) = subst' i f

1037+ (a', ua) = subst' i a in

1038+ if uf || ua then (App s f' a', True) else (t, False)

10341039 subst' i t@(Proj x idx) = let (x', u) = subst' i x in

10351040 if u then (Proj x' idx, u) else (t, False)

10361041 subst' i t = (t, False)

@@ -1055,7 +1060,7 @@ psubst n v tm = s' 0 tm where

10551060 s' i (P _ x _) | n == x = v

10561061 s' i (Bind x b sc) | n == x = Bind x (fmap (s' i) b) sc

10571062 | otherwise = Bind x (fmap (s' i) b) (s' (i+1) sc)

1058− s' i (App f a) = App (s' i f) (s' i a)

1063+ s' i (App st f a) = App st (s' i f) (s' i a)

10591064 s' i (Proj t idx) = Proj (s' i t) idx

10601065 s' i t = t

10611066

@@ -1073,7 +1078,7 @@ substTerm :: Eq n => TT n {-^ Old term -} ->

10731078 -> TT n

10741079substTerm old new = st where

10751080 st t | t == old = new

1076− st (App f a) = App (st f) (st a)

1081+ st (App s f a) = App s (st f) (st a)

10771082 st (Bind x b sc) = Bind x (fmap st b) (st sc)

10781083 st t = t

10791084

@@ -1087,7 +1092,7 @@ occurrences n t = execState (no' 0 t) 0

10871092 where noB' i (Let t v) = do no' i t; no' i v

10881093 noB' i (Guess t v) = do no' i t; no' i v

10891094 noB' i b = no' i (binderTy b)

1090− no' i (App f a) = do no' i f; no' i a

1095+ no' i (App _ f a) = do no' i f; no' i a

10911096 no' i (Proj x _) = no' i x

10921097 no' i _ = return ()

10931098

@@ -1101,7 +1106,7 @@ noOccurrence n t = no' 0 t

11011106 where noB' i (Let t v) = no' i t && no' i v

11021107 noB' i (Guess t v) = no' i t && no' i v

11031108 noB' i b = no' i (binderTy b)

1104− no' i (App f a) = no' i f && no' i a

1109+ no' i (App _ f a) = no' i f && no' i a

11051110 no' i (Proj x _) = no' i x

11061111 no' i _ = True

11071112

@@ -1113,7 +1118,7 @@ freeNames t = nub $ freeNames' t

11131118 freeNames' (Bind n (Let t v) sc) = freeNames' v ++ (freeNames' sc \\ [n])

11141119 ++ freeNames' t

11151120 freeNames' (Bind n b sc) = freeNames' (binderTy b) ++ (freeNames' sc \\ [n])

1116− freeNames' (App f a) = freeNames' f ++ freeNames' a

1121+ freeNames' (App _ f a) = freeNames' f ++ freeNames' a

11171122 freeNames' (Proj x i) = freeNames' x

11181123 freeNames' _ = []

11191124

@@ -1125,14 +1130,14 @@ arity _ = 0

11251130-- | Deconstruct an application; returns the function and a list of arguments

11261131unApply :: TT n -> (TT n, [TT n])

11271132unApply t = ua [] t where

1128− ua args (App f a) = ua (a:args) f

1133+ ua args (App _ f a) = ua (a:args) f

11291134 ua args t = (t, args)

11301135

11311136-- | Returns a term representing the application of the first argument

11321137-- (a function) to every element of the second argument.

11331138mkApp :: TT n -> [TT n] -> TT n

11341139mkApp f [] = f

1135−mkApp f (a:as) = mkApp (App f a) as

1140+mkApp f (a:as) = mkApp (App MaybeHoles f a) as

11361141

11371142unList :: Term -> Maybe [Term]

11381143unList tm = case unApply tm of

@@ -1173,7 +1178,7 @@ safeForgetEnv env (Bind n b sc)

11731178 (safeForgetEnv env v)

11741179 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)

11751180 Just $ fmap (\_ -> ty') b

1176−safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

1181+safeForgetEnv env (App _ f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

11771182safeForgetEnv env (Constant c) = Just $ RConstant c

11781183safeForgetEnv env (TType i) = Just RType

11791184safeForgetEnv env (UType u) = Just $ RUType u

@@ -1226,7 +1231,7 @@ uniqueBinders ns = ubSet (fromList ns) where

12261231 = let n' = uniqueNameSet n ns

12271232 ns' = insert n' ns in

12281233 Bind n' (fmap (ubSet ns') b) (ubSet ns' sc)

1229− ubSet ns (App f a) = App (ubSet ns f) (ubSet ns a)

1234+ ubSet ns (App s f a) = App s (ubSet ns f) (ubSet ns a)

12301235 ubSet ns t = t

12311236

12321237

@@ -1319,7 +1324,7 @@ prettyEnv env t = prettyEnv' env t False

13191324 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

13201325 prettySe p env (Bind n b sc) debug =

13211326 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

1322− prettySe p env (App f a) debug =

1327+ prettySe p env (App _ f a) debug =

13231328 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug

13241329 prettySe p env (Proj x i) debug =

13251330 prettySe 1 env x debug <+> text ("!" ++ show i)

@@ -1363,7 +1368,7 @@ showEnv' env t dbg = se 10 env t where

13631368 where arrow (TType _) = " -> "

13641369 arrow u = " [" ++ show u ++ "] -> "

13651370 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

1366− se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

1371+ se p env (App _ f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

13671372 se p env (Proj x i) = se 1 env x ++ "!" ++ show i

13681373 se p env (Constant c) = show c

13691374 se p env Erased = "[__]"

@@ -1388,9 +1393,9 @@ showEnv' env t dbg = se 10 env t where

13881393 bracket outer inner str | inner > outer = "(" ++ str ++ ")"

13891394 | otherwise = str

13901395

1391−-- | Check whether a term has any holes in it - impure if so

1396+-- | Check whether a term has any hole bindings in it - impure if so

13921397pureTerm :: TT Name -> Bool

1393−pureTerm (App f a) = pureTerm f && pureTerm a

1398+pureTerm (App _ f a) = pureTerm f && pureTerm a

13941399pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where

13951400 pureBinder (Hole _) = False

13961401 pureBinder (Guess _ _) = False

@@ -1406,7 +1411,7 @@ pureTerm _ = True

14061411weakenTm :: Int -> TT n -> TT n

14071412weakenTm i t = wk i 0 t

14081413 where wk i min (V x) | x >= min = V (i + x)

1409− wk i m (App f a) = App (wk i m f) (wk i m a)

1414+ wk i m (App s f a) = App s (wk i m f) (wk i m a)

14101415 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)

14111416 wk i m t = t

14121417 wkb i m t = fmap (wk i m) t

@@ -1431,7 +1436,7 @@ weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))

14311436orderPats :: Term -> Term

14321437orderPats tm = op [] tm

14331438 where

1434− op [] (App f a) = App f (op [] a) -- for Infer terms

1439+ op [] (App s f a) = App s f (op [] a) -- for Infer terms

14351440

14361441 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc

14371442 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc

@@ -1456,7 +1461,7 @@ refsIn (Bind n b t) = nub $ nb b ++ refsIn t

14561461 where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)

14571462 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)

14581463 nb t = refsIn (binderTy t)

1459−refsIn (App f a) = nub (refsIn f ++ refsIn a)

1464+refsIn (App s f a) = nub (refsIn f ++ refsIn a)

14601465refsIn _ = []

14611466

14621467-- Make sure all the pattern bindings are as far out as possible

@@ -1493,9 +1498,9 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

14931498 return (Bind n (Hole t') sc')

14941499

14951500

1496− getPats (App f a) = do f' <- getPats f

1497− a' <- getPats a

1498− return (App f' a')

1501+ getPats (App s f a) = do f' <- getPats f

1502+ a' <- getPats a

1503+ return (App s f' a')

14991504 getPats t = return t

15001505

15011506allTTNames :: Eq n => TT n -> [n]

@@ -1505,7 +1510,7 @@ allTTNames = nub . allNamesIn

15051510 where nb (Let t v) = allNamesIn t ++ allNamesIn v

15061511 nb (Guess t v) = allNamesIn t ++ allNamesIn v

15071512 nb t = allNamesIn (binderTy t)

1508− allNamesIn (App f a) = allNamesIn f ++ allNamesIn a

1513+ allNamesIn (App _ f a) = allNamesIn f ++ allNamesIn a

15091514 allNamesIn _ = []

15101515

15111516

@@ -1528,7 +1533,7 @@ pprintTT bound tm = pp startPrec bound tm

15281533 | otherwise = text ("{{{V" ++ show i ++ "}}}")

15291534 pp p bound (Bind n b sc) = ppb p bound n b $

15301535 pp startPrec (n:bound) sc

1531− pp p bound (App tm1 tm2) =

1536+ pp p bound (App _ tm1 tm2) =

15321537 bracket p appPrec . group . hang 2 $

15331538 pp appPrec bound tm1 <> line <>

15341539 pp (appPrec + 1) bound tm2

src/Idris/Core/Typecheck.hs+8−5

@@ -77,6 +77,9 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

7777 smaller _ (UType u) = UType u

7878 smaller x _ = x

7979

80+ astate | holes = MaybeHoles

81+ | otherwise = Complete

82+

8083 chk :: Type -> -- uniqueness level

8184 Env -> Raw -> StateT UCs TC (Term, Type)

8285 chk u env (Var n)

@@ -101,13 +104,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

101104 put (v+1, ULT (UVar v) v' : cs)

102105 let apty = simplify initContext env

103106 (Bind x (Let (TType v') (TType (UVar v))) t)

104− return (App fv (TType (UVar v)), apty)

107+ return (App Complete fv (TType (UVar v)), apty)

105108 Bind x (Pi i s k) t ->

106109 do (av, aty) <- chk u env RType

107110 convertsC ctxt env aty s

108111 let apty = simplify initContext env

109112 (Bind x (Let aty av) t)

110− return (App fv av, apty)

113+ return (App astate fv av, apty)

111114 t -> lift $ tfail $ NonFunctionType fv fty

112115 chk u env ap@(RApp f a)

113116 = do (fv, fty) <- chk u env f

@@ -123,7 +126,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

123126 do convertsC ctxt env aty s

124127 let apty = simplify initContext env

125128 (Bind x (Let aty av) t)

126− return (App fv av, apty)

129+ return (App astate fv av, apty)

127130 t -> lift $ tfail $ NonFunctionType fv fty

128131 chk u env RType

129132 | holes = return (TType (UVal 0), TType (UVal 0))

@@ -298,7 +301,7 @@ checkUnique borrowed ctxt env tm

298301 chkBinders env (P _ n _) = chkName n

299302 -- 'lending' a unique or nulltype variable doesn't count as a use,

300303 -- but we still can't lend something that's already been used.

301− chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)

304+ chkBinders env (App _ (App _ (P _ (NS (UN lend) [owner]) _) t) a)

302305 | isVar a && owner == txt "Ownership" &&

303306 (lend == txt "lend" || lend == txt "Read")

304307 = do chkBinders env t -- Check the type normally

@@ -307,7 +310,7 @@ checkUnique borrowed ctxt env tm

307310 put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)

308311 chkBinders env a

309312 put st -- Reset the old state after checking the argument

310− chkBinders env (App f a) = do chkBinders env f; chkBinders env a

313+ chkBinders env (App _ f a) = do chkBinders env f; chkBinders env a

311314 chkBinders env (Bind n b t)

312315 = do chkBinderName env n b

313316 st <- get

src/Idris/Core/Unify.hs+33−35

@@ -96,22 +96,22 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

9696 -- but it scares me. However, matching is never guaranteed to give a unique

9797 -- answer, merely a valid one, so perhaps we're okay.

9898 -- In other words: it may vanish without warning some day :)

99− un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)

99+ un names x tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a)

100100 | (P (TCon _ _) _ _, _) <- unApply x,

101101 holeIn env f || f `elem` holes

102102 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

103103 checkCycle names (f, Bind n' (Lam t) x)

104− un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

104+ un names tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a) x

105105 | (P (TCon _ _) _ _, _) <- unApply x,

106106 holeIn env f || f `elem` holes

107107 = let n' = uniqueName fn (map fst env) in

108108 checkCycle names (f, Bind n' (Lam t) x)

109− un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)

109+ un names x tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a)

110110 | (P (DCon _ _ _) _ _, _) <- unApply x,

111111 holeIn env f || f `elem` holes

112112 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

113113 checkCycle names (f, Bind n' (Lam t) x)

114− un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

114+ un names tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a) x

115115 | (P (DCon _ _ _) _ _, _) <- unApply x,

116116 holeIn env f || f `elem` holes

117117 = let n' = uniqueName fn (map fst env) in

@@ -135,7 +135,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

135135 = do h1 <- uB bnames bx by

136136 h2 <- un (((x, y), binderTy bx) : bnames) sx sy

137137 combine bnames h1 h2

138− un names (App fx ax) (App fy ay)

138+ un names (App _ fx ax) (App _ fy ay)

139139 = do hf <- un names fx fy

140140 ha <- un names ax ay

141141 combine names hf ha

@@ -218,7 +218,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

218218 bind i ns tm

219219 | i < 0 = tm

220220 | otherwise = let ((x,y),ty) = ns!!i in

221− App (Bind y (Lam ty) (bind (i-1) ns tm))

221+ App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))

222222 (P Bound x ty)

223223

224224renameBinders env (x, t) = (x, renameBindersTm env t)

@@ -233,12 +233,12 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

233233 (uniqueBinders (n':env) (rename n n' sc))

234234 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

235235 (uniqueBinders (n:env) sc)

236− uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)

236+ uniqueBinders env (App s f a) = App s (uniqueBinders env f) (uniqueBinders env a)

237237 uniqueBinders env t = t

238238

239239 rename n n' (P nt x ty) | n == x = P nt n' ty

240240 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)

241− rename n n' (App f a) = App (rename n n' f) (rename n n' a)

241+ rename n n' (App s f a) = App s (rename n n' f) (rename n n' a)

242242 rename n n' t = t

243243

244244 explicitHole (Bind n (Hole ty) sc)

@@ -280,7 +280,7 @@ expandLets env (x, tm) = (x, doSubst (reverse env) tm)

280280

281281hasv :: TT Name -> Bool

282282hasv (V x) = True

283−hasv (App f a) = hasv f || hasv a

283+hasv (App _ f a) = hasv f || hasv a

284284hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

285285hasv _ = False

286286

@@ -315,14 +315,12 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

315315

316316 injective (P (DCon _ _ _) _ _) = True

317317 injective (P (TCon _ _) _ _) = True

318−-- injective (App f (P _ _ _)) = injective f

319−-- injective (App f (Constant _)) = injective f

320− injective (App f a) = injective f -- && injective a

318+ injective (App _ f a) = injective f -- && injective a

321319 injective _ = False

322320

323321-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK

324322 injectiveVar (P _ n _) = n `elem` inj

325− injectiveVar (App f a) = injectiveVar f -- && injective a

323+ injectiveVar (App _ f a) = injectiveVar f -- && injective a

326324 injectiveVar _ = False

327325

328326 injectiveApp x = injective x || injectiveVar x

@@ -426,18 +424,18 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

426424 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y

427425 un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy

428426

429− un' fn bnames appx@(App _ _) appy@(App _ _)

427+ un' fn bnames appx@(App _ _ _) appy@(App _ _ _)

430428 = unApp fn bnames appx appy

431429-- = uplus (unApp fn bnames appx appy)

432430-- (unifyTmpFail appx appy) -- take the whole lot

433431

434− un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))

432+ un' fn bnames x (Bind n (Lam t) (App _ y (P Bound n' _)))

435433 | n == n' = un' False bnames x y

436− un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

434+ un' fn bnames (Bind n (Lam t) (App _ x (P Bound n' _))) y

437435 | n == n' = un' False bnames x y

438− un' fn bnames x (Bind n (Lam t) (App y (V 0)))

436+ un' fn bnames x (Bind n (Lam t) (App _ y (V 0)))

439437 = un' False bnames x y

440− un' fn bnames (Bind n (Lam t) (App x (V 0))) y

438+ un' fn bnames (Bind n (Lam t) (App _ x (V 0))) y

441439 = un' False bnames x y

442440-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

443441-- = un' False ((x,y):bnames) sx sy

@@ -447,14 +445,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

447445 -- f D unifies with t -> D. This is dubious, but it helps with type

448446 -- class resolution for type classes over functions.

449447

450− un' fn bnames (App f x) (Bind n (Pi i t k) y)

448+ un' fn bnames (App _ f x) (Bind n (Pi i t k) y)

451449 | noOccurrence n y && injectiveApp f

452450 = do ux <- un' False bnames x y

453451 uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

454452 (Bind n (Pi i t k) (V 1)))

455453 combine bnames ux uf

456454

457− un' fn bnames (Bind n (Pi i t k) y) (App f x)

455+ un' fn bnames (Bind n (Pi i t k) y) (App _ f x)

458456 | noOccurrence n y && injectiveApp f

459457 = do ux <- un' False bnames y x

460458 uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

@@ -481,7 +479,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

481479 else do put (UI s ((x, y, True, env, err, from, Unify) : f))

482480 return [] -- lift $ tfail err

483481

484− unApp fn bnames appx@(App fx ax) appy@(App fy ay)

482+ unApp fn bnames appx@(App _ fx ax) appy@(App _ fy ay)

485483 -- shortcut for the common case where we just want to check the

486484 -- arguments are correct

487485 | (injectiveApp fx && fx == fy)

@@ -545,7 +543,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

545543 rigid (P (TCon _ _) _ _) = True

546544 rigid t@(P Ref _ _) = inenv t || globmetavar t

547545 rigid (Constant _) = True

548− rigid (App f a) = rigid f && rigid a

546+ rigid (App _ f a) = rigid f && rigid a

549547 rigid t = not (metavar t) || globmetavar t

550548

551549 globmetavar t = case unApply t of

@@ -636,7 +634,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

636634 bind i ns tm

637635 | i < 0 = tm

638636 | otherwise = let ((x,y),ty) = ns!!i in

639− App (Bind y (Lam ty) (bind (i-1) ns tm))

637+ App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))

640638 (P Bound x ty)

641639

642640 combineArgs bnames args = ca [] args where

@@ -658,16 +656,16 @@ boundVs :: Int -> Term -> [Int]

658656boundVs i (V j) | j < i = []

659657 | otherwise = [j]

660658boundVs i (Bind n b sc) = boundVs (i + 1) sc

661−boundVs i (App f x) = let fs = boundVs i f

662− xs = boundVs i x in

663− nub (fs ++ xs)

659+boundVs i (App _ f x) = let fs = boundVs i f

660+ xs = boundVs i x in

661+ nub (fs ++ xs)

664662boundVs i _ = []

665663

666664highV :: Int -> Term -> Int

667665highV i (V j) | j > i = j

668666 | otherwise = i

669667highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]

670−highV i (App f x) = max (highV i f) (highV i x)

668+highV i (App _ f x) = max (highV i f) (highV i x)

671669highV i _ = i

672670

673671envPos x i [] = 0

@@ -683,9 +681,9 @@ envPos x i ((y, _) : ys) | x == y = i

683681--

684682-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722

685683--

686−recoverable t@(App _ _) _

684+recoverable t@(App _ _ _) _

687685 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

688−recoverable _ t@(App _ _)

686+recoverable _ t@(App _ _ _)

689687 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

690688recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y

691689recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

@@ -696,13 +694,13 @@ recoverable (Constant _) (P (TCon _ _) y _) = False

696694recoverable (P (TCon _ _) x _) (Constant _) = False

697695recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False

698696recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False

699−recoverable p@(Constant _) (App f a) = recoverable p f

700−recoverable (App f a) p@(Constant _) = recoverable f p

701−recoverable p@(P _ n _) (App f a) = recoverable p f

702−recoverable (App f a) p@(P _ _ _) = recoverable f p

703−recoverable (App f a) (App f' a')

697+recoverable p@(Constant _) (App _ f a) = recoverable p f

698+recoverable (App _ f a) p@(Constant _) = recoverable f p

699+recoverable p@(P _ n _) (App _ f a) = recoverable p f

700+recoverable (App _ f a) p@(P _ _ _) = recoverable f p

701+recoverable (App _ f a) (App _ f' a')

704702 | f == f' = recoverable a a'

705−recoverable (App f a) (App f' a')

703+recoverable (App _ f a) (App _ f' a')

706704 = recoverable f f' -- && recoverable a a'

707705recoverable f (Bind _ (Pi _ _ _) sc)

708706 | (P (DCon _ _ _) _ _, _) <- unApply f = False

src/Idris/Coverage.hs+13−13

@@ -147,9 +147,9 @@ recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

147147 where -- different notion of recoverable than in unification, since we

148148 -- have no metavars -- just looking to see if a constructor is failing

149149 -- to unify with a function that may be reduced later

150− checkRec (App f a) p@(P _ _ _) = checkRec f p

151− checkRec p@(P _ _ _) (App f a) = checkRec p f

152− checkRec fa@(App _ _) fa'@(App _ _)

150+ checkRec (App _ f a) p@(P _ _ _) = checkRec f p

151+ checkRec p@(P _ _ _) (App _ f a) = checkRec p f

152+ checkRec fa@(App _ _ _) fa'@(App _ _ _)

153153 | (f, as) <- unApply fa,

154154 (f', as') <- unApply fa'

155155 = if (length as /= length as')

@@ -364,7 +364,7 @@ calcProd i fc topn pats

364364 prodRec n done (_, _, tm) = prod n done False (delazy' True tm)

365365

366366 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool

367− prod n done ok ap@(App _ _)

367+ prod n done ok ap@(App _ _ _)

368368 | (P nt f _, args) <- unApply ap

369369 = do recOK <- checkProdRec (n:done) f

370370 let ctxt = tt_ctxt i

@@ -376,8 +376,8 @@ calcProd i fc topn pats

376376 return (and (ok : argsprod) )

377377 else do argsprod <- mapM (prod n done co) args

378378 return (and argsprod)

379− prod n done ok (App f a) = liftM2 (&&) (prod n done False f)

380− (prod n done False a)

379+ prod n done ok (App _ f a) = liftM2 (&&) (prod n done False f)

380+ (prod n done False a)

381381 prod n done ok (Bind _ (Let t v) sc)

382382 = liftM2 (&&) (prod n done False v) (prod n done False v)

383383 prod n done ok (Bind _ b sc) = prod n done ok sc

@@ -414,7 +414,7 @@ calcTotality fc n pats

414414 = case lookupTotal fn (tt_ctxt i) of

415415 [Partial _] -> return (Partial (Other [fn]))

416416 _ -> Nothing

417− checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)

417+ checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)

418418 checkLHS _ _ = Nothing

419419

420420checkTotality :: [Name] -> FC -> Name -> Idris Totality

@@ -522,14 +522,14 @@ buildSCG (_, n) = do

522522 x -> error $ "buildSCG: " ++ show (n, x)

523523

524524delazy = delazy' False -- not lazy codata

525−delazy' all t@(App f a)

525+delazy' all t@(App _ f a)

526526 | (P _ (UN l) _, [_, _, arg]) <- unApply t,

527527 l == txt "Force" = delazy' all arg

528528 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,

529529 l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg

530530 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,

531531 l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg

532−delazy' all (App f a) = App (delazy' all f) (delazy' all a)

532+delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)

533533delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)

534534delazy' all t = t

535535

@@ -543,7 +543,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

543543 (f, pargs) = unApply (dePat lhs') in

544544 findCalls Toplevel (dePat rhs') (patvars lhs') pargs

545545

546− findCalls guarded ap@(App f a) pvs pargs

546+ findCalls guarded ap@(App _ f a) pvs pargs

547547 -- under a call to "assert_total", don't do any checking, just believe

548548 -- that it is total.

549549 | (P _ (UN at) _, [_, _]) <- unApply ap,

@@ -564,7 +564,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

564564 else Unguarded in

565565 mkChange n args pargs ++

566566 concatMap (\x -> findCalls nguarded x pvs pargs) args

567− findCalls guarded (App f a) pvs pargs

567+ findCalls guarded (App _ f a) pvs pargs

568568 = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs

569569 findCalls guarded (Bind n (Let t v) e) pvs pargs

570570 = findCalls Unguarded t pvs pargs ++

@@ -606,13 +606,13 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

606606 smaller (Just tyn) a (t, Just tyt)

607607 | a == t = isInductive (fst (unApply (getRetTy tyn)))

608608 (fst (unApply (getRetTy tyt)))

609− smaller ty a (ap@(App f s), _)

609+ smaller ty a (ap@(App _ f s), _)

610610 | (P (DCon _ _ _) n _, args) <- unApply ap

611611 = let tyn = getType n in

612612 any (smaller (ty `mplus` Just tyn) a)

613613 (zip args (map toJust (getArgTys tyn)))

614614 -- check higher order recursive arguments

615− smaller ty (App f s) a = smaller ty f a

615+ smaller ty (App _ f s) a = smaller ty f a

616616 smaller _ _ _ = False

617617

618618 toJust (n, t) = Just t

src/Idris/DataOpts.hs+6−6

@@ -63,21 +63,21 @@ instance Optimisable (TT Name) where

6363 applyOpts (P _ (NS (UN fn) mod) _)

6464 | fn == txt "mult" && mod == prel

6565 = return (P Ref (sUN "prim__mulBigInt") Erased)

66− applyOpts (App (P _ (NS (UN fn) mod) _) x)

66+ applyOpts (App _ (P _ (NS (UN fn) mod) _) x)

6767 | fn == txt "fromIntegerNat" && mod == prel

6868 = applyOpts x

6969 applyOpts (P _ (NS (UN fn) mod) _)

7070 | fn == txt "fromIntegerNat" && mod == prel

71− = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

71+ = return (App Complete (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

7272 applyOpts (P _ (NS (UN fn) mod) _)

7373 | fn == txt "toIntegerNat" && mod == prel

74− = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

74+ = return (App Complete (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

7575 applyOpts c@(P (DCon t arity uniq) n _)

7676 = return $ applyDataOptRT n t arity uniq []

77− applyOpts t@(App f a)

77+ applyOpts t@(App s f a)

7878 | (c@(P (DCon t arity uniq) n _), args) <- unApply t

7979 = applyDataOptRT n t arity uniq <$> mapM applyOpts args

80− | otherwise = App <$> applyOpts f <*> applyOpts a

80+ | otherwise = App s <$> applyOpts f <*> applyOpts a

8181 applyOpts (Bind n b t) = Bind n <$> applyOpts b <*> applyOpts t

8282 applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i

8383 applyOpts t = return t

@@ -103,6 +103,6 @@ applyDataOptRT n tag arity uniq args

103103 = Constant (BI 0)

104104 doOpts (NS (UN s) [nat, prelude]) [k]

105105 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"

106− = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

106+ = App Complete (App Complete (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

107107

108108 doOpts n args = mkApp (P (DCon tag arity uniq) n Erased) args

src/Idris/Delaborate.hs+6−6

@@ -49,7 +49,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

4949 where

5050 un = fileFC "(val)"

5151

52− de env _ (App f a) = deFn env f [a]

52+ de env _ (App _ f a) = deFn env f [a]

5353 de env _ (V i) | i < length env = PRef un (snd (env!!i))

5454 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))

5555 de env _ (P _ n _) | n == unitTy = PTrue un IsType

@@ -103,7 +103,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

103103 _ -> ns

104104 dens n = n

105105

106− deFn env (App f a) args = deFn env f (a:args)

106+ deFn env (App _ f a) args = deFn env f (a:args)

107107 deFn env (P _ n _) [l,r]

108108 | n == pairTy = PPair un IsType (de env [] l) (de env [] r)

109109 | n == eqCon = PRefl un (de env [] r)

@@ -163,7 +163,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

163163 | otherwise = tm

164164 nonVar [] = error "Tried to delaborate empty case list"

165165 nonVar [x] = x

166− nonVar (x@(App _ _) : _) = x

166+ nonVar (x@(App _ _ _) : _) = x

167167 nonVar (x@(P (DCon _ _ _) _ _) : _) = x

168168 nonVar (x:xs) = nonVar xs

169169-- | How far to indent sub-errors

@@ -256,9 +256,9 @@ pprintErr' i (CantConvert x_in y_in env) =

256256 y)) <>

257257 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

258258 where flagUnique (Bind n (Pi i t k@(UType u)) sc)

259− = App (P Ref (sUN (show u)) Erased)

259+ = App Complete (P Ref (sUN (show u)) Erased)

260260 (Bind n (Pi i (flagUnique t) k) (flagUnique sc))

261− flagUnique (App f a) = App (flagUnique f) (flagUnique a)

261+ flagUnique (App s f a) = App s (flagUnique f) (flagUnique a)

262262 flagUnique (Bind n b sc) = Bind n (fmap flagUnique b) (flagUnique sc)

263263 flagUnique t = t

264264pprintErr' i (CantSolveGoal x env) =

@@ -423,7 +423,7 @@ renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

423423

424424 rename :: [(Name, Name)] -> Term -> Term

425425 rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t

426− rename ns (App f a) = App (rename ns f) (rename ns a)

426+ rename ns (App s f a) = App s (rename ns f) (rename ns a)

427427 rename ns (Bind x b sc)

428428 = let b' = fmap (rename ns) b

429429 sc' = rename ns sc in

src/Idris/Elab/Class.hs+1−1

@@ -7,7 +7,7 @@ import Idris.DSL

77import Idris.Error

88import Idris.Delaborate

99import Idris.Imports

10−import Idris.ElabTerm

10+import Idris.Elab.Term

1111import Idris.Coverage

1212import Idris.DataOpts

1313import Idris.Providers

src/Idris/Elab/Clause.hs+6−5

@@ -7,7 +7,7 @@ import Idris.DSL

77import Idris.Error

88import Idris.Delaborate

99import Idris.Imports

10−import Idris.ElabTerm

10+import Idris.Elab.Term

1111import Idris.Coverage

1212import Idris.DataOpts

1313import Idris.Providers

@@ -433,7 +433,7 @@ elabPE info fc caller r =

433433 showArg _ = ""

434434

435435 qshow (Bind _ _ _) = "fn"

436− qshow (App f a) = qshow f ++ qshow a

436+ qshow (App _ f a) = qshow f ++ qshow a

437437 qshow (P _ n _) = show n

438438 qshow (Constant c) = show c

439439 qshow _ = ""

@@ -465,6 +465,7 @@ checkPossible info fc tcgen fname lhs_in

465465 else return (validCoverageCase ctxt err ||

466466 recoverableCoverage ctxt err)

467467

468+

468469propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

469470propagateParams i ps t tm@(PApp _ (PRef fc n) args)

470471 = PApp fc (PRef fc n) (addP t args)

@@ -700,14 +701,14 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

700701 -- Find the variable names which appear under a 'Ownership.Read' so that

701702 -- we know they can't be used on the RHS

702703 borrowedNames :: [Name] -> Term -> [Name]

703− borrowedNames env (App (App (P _ (NS (UN lend) [owner]) _) _) arg)

704+ borrowedNames env (App _ (App _ (P _ (NS (UN lend) [owner]) _) _) arg)

704705 | owner == txt "Ownership" &&

705706 (lend == txt "lend" || lend == txt "Read") = getVs arg

706707 where

707708 getVs (V i) = [env!!i]

708− getVs (App f a) = nub $ getVs f ++ getVs a

709+ getVs (App _ f a) = nub $ getVs f ++ getVs a

709710 getVs _ = []

710− borrowedNames env (App f a) = nub $ borrowedNames env f ++ borrowedNames env a

711+ borrowedNames env (App _ f a) = nub $ borrowedNames env f ++ borrowedNames env a

711712 borrowedNames env (Bind n b sc) = nub $ borrowedB b ++ borrowedNames (n:env) sc

712713 where borrowedB (Let t v) = nub $ borrowedNames env t ++ borrowedNames env v

713714 borrowedB b = borrowedNames env (binderTy b)

src/Idris/Elab/Data.hs+2−2

@@ -7,7 +7,7 @@ import Idris.DSL

77import Idris.Error

88import Idris.Delaborate

99import Idris.Imports

10−import Idris.ElabTerm

10+import Idris.Elab.Term

1111import Idris.Coverage

1212import Idris.DataOpts

1313import Idris.Providers

@@ -174,7 +174,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

174174 update ((n, _) : as) (_ : args) = (n, Nothing) : update as args

175175

176176 getDataApp :: Type -> [[Maybe Name]]

177− getDataApp f@(App _ _)

177+ getDataApp f@(App _ _ _)

178178 | (P _ d _, args) <- unApply f

179179 = if (d == n) then [mParam args args] else []

180180 getDataApp (Bind n (Pi _ t _) sc)

src/Idris/Elab/Instance.hs+2−2

@@ -7,7 +7,6 @@ import Idris.DSL

77import Idris.Error

88import Idris.Delaborate

99import Idris.Imports

10−import Idris.ElabTerm

1110import Idris.Coverage

1211import Idris.DataOpts

1312import Idris.Providers

@@ -21,6 +20,7 @@ import IRTS.Lang

2120import Idris.Elab.Type

2221import Idris.Elab.Data

2322import Idris.Elab.Utils

23+import Idris.Elab.Term

2424

2525import Idris.Core.TT

2626import Idris.Core.Elaborate hiding (Tactic(..))

@@ -317,7 +317,7 @@ checkInjectiveArgs fc n ds (Just ty)

317317

318318 isInj i (P Bound n _) = True

319319 isInj i (P _ n _) = isConName n (tt_ctxt i)

320− isInj i (App f a) = isInj i f && isInj i a

320+ isInj i (App _ f a) = isInj i f && isInj i a

321321 isInj i (V _) = True

322322 isInj i (Bind n b sc) = isInj i sc

323323 isInj _ _ = True

src/Idris/Elab/Provider.hs+3−3

@@ -7,7 +7,6 @@ import Idris.DSL

77import Idris.Error

88import Idris.Delaborate

99import Idris.Imports

10−import Idris.ElabTerm

1110import Idris.Coverage

1211import Idris.DataOpts

1312import Idris.Providers

@@ -22,6 +21,7 @@ import Idris.Elab.Type

2221import Idris.Elab.Clause

2322import Idris.Elab.Value

2423import Idris.Elab.Utils

24+import Idris.Elab.Term

2525

2626import Idris.Core.TT

2727import Idris.Core.Elaborate hiding (Tactic(..))

@@ -111,8 +111,8 @@ elabProvider doc info syn fc what n

111111 -- (MkFFI C_FFI) (Providers.Provider ty) in hopes of better

112112 -- error messages with less normalisation

113113 providerOf :: Type -> Type

114− providerOf ty = App (P Ref (sUN "IO") Erased) $

115− App (P Ref (sNS (sUN "Provider") ["Providers", "Prelude"]) Erased)

114+ providerOf ty = App Complete (P Ref (sUN "IO") Erased) $

115+ App Complete (P Ref (sNS (sUN "Provider") ["Providers", "Prelude"]) Erased)

116116 ty

117117

118118 isProviderOf :: Context -> TT Name -> TT Name -> Bool

src/Idris/Elab/Record.hs+1−1

@@ -7,7 +7,7 @@ import Idris.DSL

77import Idris.Error

88import Idris.Delaborate

99import Idris.Imports

10−import Idris.ElabTerm

10+import Idris.Elab.Term

1111import Idris.Coverage

1212import Idris.DataOpts

1313import Idris.Providers

src/Idris/ElabTerm.hs → src/Idris/Elab/Term.hsrenamed+29−20

@@ -1,6 +1,6 @@

11{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}

22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.ElabTerm where

3+module Idris.Elab.Term where

44

55import Idris.AbsSyntax

66import Idris.AbsSyntaxTree

@@ -252,9 +252,7 @@ elab ist info emode opts fn tm

252252 -- normally correct to call elabE - the ones that don't are desugarings

253253 -- typically

254254 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()

255− elabE ina fc' t =

256− --do g <- goal

257− --trace ("Elaborating " ++ show t ++ " : " ++ show g) $

255+ elabE ina fc' t =

258256 do solved <- get_recents

259257 as <- get_autos

260258 -- If any of the autos use variables which have recently been solved,

@@ -420,7 +418,7 @@ elab ist info emode opts fn tm

420418 [pimp (sMN 0 "a") t False,

421419 pimp (sMN 0 "P") Placeholder True,

422420 pexp l, pexp r])

423− elab' ina fc (PAlternative True as)

421+ elab' ina fc (PAlternative True as)

424422 = do hnf_compute

425423 ty <- goal

426424 ctxt <- get_context

@@ -957,7 +955,7 @@ elab ist info emode opts fn tm

957955 _ -> n

958956

959957 inApp (P _ n _) = [n]

960− inApp (App f a) = inApp f ++ inApp a

958+ inApp (App _ f a) = inApp f ++ inApp a

961959 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc

962960 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc

963961 inApp (Bind n b sc) = inApp sc

@@ -1368,7 +1366,7 @@ pruneByType _ t _ as = as

13681366

13691367findInstances :: IState -> Term -> [Name]

13701368findInstances ist t

1371− | (P _ n _, _) <- unApply t

1369+ | (P _ n _, _) <- unApply (getRetTy t)

13721370 = case lookupCtxt n (idris_classes ist) of

13731371 [CI _ _ _ _ _ ins _] -> filter accessible ins

13741372 _ -> []

@@ -1419,17 +1417,17 @@ resTC' tcs defaultOn topholes depth topg fn ist

14191417 = do compute

14201418 g <- goal

14211419 let argsok = tcArgsOK g topholes

1422−-- trace (show (g,hs,argsok,topholes)) $

14231420 if not argsok -- && not mvok)

14241421 then lift $ tfail $ CantResolve True topg

14251422 else do

14261423 ptm <- get_term

14271424 ulog <- getUnifyLog

14281425 hs <- get_holes

1429− traceWhen ulog ("Resolving class " ++ show g) $

1426+ env <- get_env

1427+ traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env) $

14301428 try' (trivial' ist)

14311429 (do t <- goal

1432− let (tc, ttypes) = unApply t

1430+ let (tc, ttypes) = unApply (getRetTy t)

14331431 scopeOnly <- needsDefault t tc ttypes

14341432 let stk = elab_stack ist

14351433 let insts_in = findInstances ist t

@@ -1439,10 +1437,10 @@ resTC' tcs defaultOn topholes depth topg fn ist

14391437 let depth' = if scopeOnly then 2 else depth

14401438 blunderbuss t depth' stk (stk ++ insts)) True

14411439 where

1442− tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1440+ tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn

14431441 = True

14441442 tcArgsOK ty hs -- if any arguments are metavariables, postpone

1445− = let (f, as) = unApply ty in

1443+ = let (f, as) = unApply (getRetTy ty) in

14461444 case f of

14471445 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

14481446 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

@@ -1459,7 +1457,7 @@ resTC' tcs defaultOn topholes depth topg fn ist

14591457 isMeta _ _ = False

14601458

14611459 notHole hs (P _ n _, c)

1462− | (P _ cn _, _) <- unApply c,

1460+ | (P _ cn _, _) <- unApply (getRetTy c),

14631461 n `elem` hs && isConName cn (tt_ctxt ist) = False

14641462 | Constant _ <- c = not (n `elem` hs)

14651463 notHole _ _ = True

@@ -1500,11 +1498,22 @@ resTC' tcs defaultOn topholes depth topg fn ist

15001498 _ -> blunderbuss t d stk ns)

15011499 | otherwise = blunderbuss t d stk ns

15021500

1501+ introImps = do g <- goal

1502+ case g of

1503+ (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing

1504+ num <- introImps

1505+ return (num + 1)

1506+ _ -> return 0

1507+

1508+ solven 0 = return ()

1509+ solven n = do solve; solven (n - 1)

1510+

15031511 resolve n depth

15041512 | depth == 0 = fail $ "Can't resolve type class"

15051513 | otherwise

1506− = do t <- goal

1507− let (tc, ttypes) = unApply t

1514+ = do lams <- introImps

1515+ t <- goal

1516+ let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

15081517-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

15091518-- else do

15101519 -- if there's a hole in the goal, don't even try

@@ -1516,14 +1525,15 @@ resTC' tcs defaultOn topholes depth topg fn ist

15161525 tm <- get_term

15171526 args <- map snd <$> try' (apply (Var n) imps)

15181527 (match_apply (Var n) imps) True

1528+ solven lams -- close any implicit lambdas we introduced

15191529 ps' <- get_probs

15201530 when (length ps < length ps' || unrecoverable ps') $

15211531 fail "Can't apply type class"

15221532-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

15231533 mapM_ (\ (_,n) -> do focus n

15241534 t' <- goal

1525− let (tc', ttype) = unApply t'

1526− let got = fst (unApply t)

1535+ let (tc', ttype) = unApply (getRetTy t')

1536+ let got = fst (unApply (getRetTy t))

15271537 let depth' = if tc' `elem` tcs

15281538 then depth - 1 else depth

15291539 resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

@@ -1551,7 +1561,7 @@ collectDeferred top (Bind n b t) = do b' <- cdb b

15511561 cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)

15521562 cdb b = do ty' <- collectDeferred top (binderTy b)

15531563 return (b { binderTy = ty' })

1554−collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)

1564+collectDeferred top (App s f a) = liftM2 (App s) (collectDeferred top f) (collectDeferred top a)

15551565collectDeferred top t = return t

15561566

15571567case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

@@ -1687,7 +1697,7 @@ runTactical fc env tm = do tm' <- eval tm

16871697 | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args

16881698 = do first' <- eval first

16891699 res <- runTacTm first'

1690− next <- eval (App andThen res)

1700+ next <- eval (App Complete andThen res)

16911701 runTacTm next

16921702 | n == tacN "prim__Try", [_a, first, alt] <- args

16931703 = do first' <- eval first

@@ -2022,7 +2032,6 @@ runTac autoSolve ist perhapsFC fn tac

20222032 runReflected t = do t' <- reify ist t

20232033 runTac autoSolve ist perhapsFC fn t'

20242034

2025−

20262035elaboratingArgErr :: [(Name, Name)] -> Err -> Err

20272036elaboratingArgErr [] err = err

20282037elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

src/Idris/Elab/Transform.hs+1−1

@@ -7,7 +7,6 @@ import Idris.DSL

77import Idris.Error

88import Idris.Delaborate

99import Idris.Imports

10−import Idris.ElabTerm

1110import Idris.Coverage

1211import Idris.DataOpts

1312import Idris.Providers

@@ -19,6 +18,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)

1918import IRTS.Lang

2019

2120import Idris.Elab.Utils

21+import Idris.Elab.Term

2222

2323import Idris.Core.TT

2424import Idris.Core.Elaborate hiding (Tactic(..))

src/Idris/Elab/Type.hs+3−3

@@ -8,7 +8,7 @@ import Idris.DSL

88import Idris.Error

99import Idris.Delaborate

1010import Idris.Imports

11−import Idris.ElabTerm

11+import Idris.Elab.Term

1212import Idris.Coverage

1313import Idris.DataOpts

1414import Idris.Providers

@@ -215,8 +215,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

215215 errrep = txt "ErrorReportPart"

216216

217217 tyIsHandler (Bind _ (Pi _ (P _ (NS (UN e) ns1) _) _)

218− (App (P _ (NS (UN m) ns2) _)

219− (App (P _ (NS (UN l) ns3) _)

218+ (App _ (P _ (NS (UN m) ns2) _)

219+ (App _ (P _ (NS (UN l) ns3) _)

220220 (P _ (NS (UN r) ns4) _))))

221221 | e == err && m == maybe && l == lst && r == errrep

222222 , ns1 == map txt ["Errors","Reflection","Language"]

src/Idris/Elab/Utils.hs+3−3

@@ -171,7 +171,7 @@ getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi _ t _) sc)

171171 _ -> []

172172getFixedInType i env (_ : is) (Bind n (Pi _ t _) sc)

173173 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

174−getFixedInType i env is tm@(App f a)

174+getFixedInType i env is tm@(App _ f a)

175175 | (P _ tn _, args) <- unApply tm

176176 = case lookupCtxt tn (idris_datatypes i) of

177177 [t] -> nub $ paramNames args env (param_pos t) ++

@@ -186,7 +186,7 @@ getFixedInType i _ _ _ = []

186186getFlexInType i env ps (Bind n (Pi _ t _) sc)

187187 = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++

188188 getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)

189−getFlexInType i env ps tm@(App f a)

189+getFlexInType i env ps tm@(App _ f a)

190190 | (P _ tn _, args) <- unApply tm

191191 = case lookupCtxt tn (idris_datatypes i) of

192192 [t] -> nub $ paramNames args env [x | x <- [0..length args],

@@ -232,7 +232,7 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

232232 _ -> False in

233233 do getUniqB env us b

234234 getUniq ((n,b):env) ((n, uniq):us) sc

235− getUniq env us (App f a) = do getUniq env us f; getUniq env us a

235+ getUniq env us (App _ f a) = do getUniq env us f; getUniq env us a

236236 getUniq env us (V i)

237237 | i < length us = if snd (us!!i) then use (fst (us!!i)) else return ()

238238 getUniq env us (P _ n _)

src/Idris/Elab/Value.hs+1−1

@@ -8,7 +8,6 @@ import Idris.DSL

88import Idris.Error

99import Idris.Delaborate

1010import Idris.Imports

11−import Idris.ElabTerm

1211import Idris.Coverage

1312import Idris.DataOpts

1413import Idris.Providers

@@ -20,6 +19,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)

2019import IRTS.Lang

2120

2221import Idris.Elab.Utils

22+import Idris.Elab.Term

2323

2424import Idris.Core.TT

2525import Idris.Core.Elaborate hiding (Tactic(..))

src/Idris/ElabDecls.hs+1−1

@@ -9,7 +9,7 @@ import Idris.DSL

99import Idris.Error

1010import Idris.Delaborate

1111import Idris.Imports

12−import Idris.ElabTerm

12+import Idris.Elab.Term

1313import Idris.Coverage

1414import Idris.DataOpts

1515import Idris.Providers

src/Idris/Erasure.hs+6−6

@@ -279,7 +279,7 @@ buildDepMap ci used externs ctx startNames

279279

280280 etaExpand :: [Name] -> Term -> Term

281281 etaExpand [] t = t

282− etaExpand (n : ns) t = etaExpand ns (App t (P Ref n Erased))

282+ etaExpand (n : ns) t = etaExpand ns (App Complete t (P Ref n Erased))

283283

284284 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps

285285 getDepsSC fn es vs ImpossibleCase = M.empty

@@ -370,7 +370,7 @@ buildDepMap ci used externs ctx startNames

370370 var t cd = getDepsTerm vs bs cd t

371371

372372 -- applications may add items to Cond

373− getDepsTerm vs bs cd app@(App _ _)

373+ getDepsTerm vs bs cd app@(App _ _ _)

374374 | (fun, args) <- unApply app = case fun of

375375 -- instance constructors -> create metamethod deps

376376 P (DCon _ _ _) ctorName@(SN (InstanceCtorN className)) _

@@ -418,8 +418,8 @@ buildDepMap ci used externs ctx startNames

418418 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

419419

420420 -- and we interpret applied lets as lambdas

421− Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')

422− Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')

421+ Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')

422+ Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')

423423

424424 Proj t i

425425 -> error $ "cannot[0] analyse projection !" ++ show i ++ " of " ++ show t

@@ -493,9 +493,9 @@ buildDepMap ci used externs ctx startNames

493493 -- convert applications of lambdas to lets

494494 -- Note that this transformation preserves de bruijn numbering

495495 lamToLet :: [Term] -> Term -> Term

496− lamToLet xs (App f x) = lamToLet (x:xs) f

496+ lamToLet xs (App _ f x) = lamToLet (x:xs) f

497497 lamToLet (x:xs) (Bind n (Lam ty) t) = Bind n (Let ty x) (lamToLet xs t)

498− lamToLet (x:xs) t = App (lamToLet xs t) x

498+ lamToLet (x:xs) t = App Complete (lamToLet xs t) x

499499 lamToLet [] t = t

500500

501501 -- split "\x_i -> T(x_i)" into [x_i] and T

src/Idris/ErrReverse.hs+7−7

@@ -35,9 +35,9 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

3535

3636 matchTerm ns l r t

3737 | Just nmap <- match ns l t = substNames nmap r

38− matchTerm ns l r (App f a) = let f' = matchTerm ns l r f

39− a' = matchTerm ns l r a in

40− App f' a'

38+ matchTerm ns l r (App s f a) = let f' = matchTerm ns l r f

39+ a' = matchTerm ns l r a in

40+ App s f' a'

4141 matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b

4242 sc' = matchTerm ns l r sc in

4343 Bind n b' sc'

@@ -54,16 +54,16 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

5454 Just ((x, t) : xs')

5555

5656 match' ns (P Ref n _) t | n `elem` ns = Just [(n, t)]

57− match' ns (App f a) (App f' a') = do fs <- match' ns f f'

58− as <- match' ns a a'

59− Just (fs ++ as)

57+ match' ns (App _ f a) (App _ f' a') = do fs <- match' ns f f'

58+ as <- match' ns a a'

59+ Just (fs ++ as)

6060 -- no matching Binds, for now...

6161 match' ns x y = if x == y then Just [] else Nothing

6262

6363 -- if the term under a lambda is huge, there's no much point in showing

6464 -- it as it won't be very enlightening.

6565

66− elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)

66+ elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)

6767 elideLambdas (Bind n (Lam t) sc)

6868 | size sc > 200 = P Ref (sUN "...") Erased

6969 elideLambdas (Bind n b sc)

src/Idris/IBC.hs+1−1

@@ -501,7 +501,7 @@ pDefs reexp syms ds

501501

502502 update (P t n ty) = do n' <- getSymbol n

503503 return $ P t n' ty

504− update (App f a) = liftM2 App (update f) (update a)

504+ update (App s f a) = liftM2 (App s) (update f) (update a)

505505 update (Bind n b sc) = do b' <- updateB b

506506 sc' <- update sc

507507 return $ Bind n b' sc'

src/Idris/Inliner.hs+1−1

@@ -21,7 +21,7 @@ inlineDef ist ds = map (\ (ns, lhs, rhs) -> (ns, lhs, inlineTerm ist rhs)) ds

2121inlineTerm :: IState -> Term -> Term

2222inlineTerm ist tm = inl tm where

2323 inl orig@(P _ n _) = inlApp n [] orig

24− inl orig@(App f a)

24+ inl orig@(App _ f a)

2525 | (P _ fn _, args) <- unApply orig = inlApp fn args orig

2626 inl (Bind n (Let t v) sc) = Bind n (Let t (inl v)) (inl sc)

2727 inl (Bind n b sc) = Bind n b (inl sc)

src/Idris/Interactive.hs+2−2

@@ -12,12 +12,12 @@ import Idris.Core.Evaluate

1212import Idris.CaseSplit

1313import Idris.AbsSyntax

1414import Idris.ElabDecls

15−import Idris.ElabTerm

1615import Idris.Error

1716import Idris.Delaborate

1817import Idris.Output

1918import Idris.IdeMode hiding (IdeModeCommand(..))

2019import Idris.Elab.Value

20+import Idris.Elab.Term

2121

2222import Util.Pretty

2323import Util.System

@@ -322,7 +322,7 @@ makeLemma fn updatefile l n

322322 guessImps ctxt _ = []

323323

324324 guarded ctxt n (P _ n' _) | n == n' = True

325− guarded ctxt n ap@(App _ _)

325+ guarded ctxt n ap@(App _ _ _)

326326 | (P _ f _, args) <- unApply ap,

327327 isConName f ctxt = any (guarded ctxt n) args

328328-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows

src/Idris/ParseExpr.hs+2−2

@@ -966,9 +966,9 @@ constraintList1 syn = try (do lchar '('

966966 return [(defname, t)])

967967 <?> "type constraint list"

968968 where nexpr = try (do n <- name; lchar ':'

969− e <- expr' (disallowImp syn)

969+ e <- expr syn

970970 return (n, e))

971− <|> do e <- expr' (disallowImp syn)

971+ <|> do e <- expr syn

972972 return (defname, e)

973973 defname = sMN 0 "constrarg"

974974

src/Idris/Parser.hs+1−1

@@ -25,8 +25,8 @@ import Idris.Imports

2525import Idris.Delaborate

2626import Idris.Error

2727import Idris.Elab.Value

28+import Idris.Elab.Term

2829import Idris.ElabDecls

29−import Idris.ElabTerm

3030import Idris.Coverage

3131import Idris.IBC

3232import Idris.Unlit

src/Idris/PartialEval.hs+2−2

@@ -146,7 +146,7 @@ mkPE_TyDecl ist args ty = mkty args ty

146146 = do nm <- get

147147 put (nm + 1)

148148 return (P Bound (sMN nm "spec") Erased)

149− gen (App f a) = App <$> gen f <*> gen a

149+ gen (App s f a) = App s <$> gen f <*> gen a

150150 gen tm = return tm

151151

152152-- | Checks if a given argument is a type class constraint argument

@@ -291,7 +291,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

291291

292292 -- if we have a *defined* function that has static arguments,

293293 -- it will become a specialised application

294− ga env tm@(App f a) | (P _ n _, args) <- unApply tm,

294+ ga env tm@(App _ f a) | (P _ n _, args) <- unApply tm,

295295 n `notElem` map fst (idris_metavars ist) =

296296 ga env f ++ ga env a ++

297297 case (lookupCtxtExact n (idris_statics ist),

src/Idris/ProofSearch.hs+1−1

@@ -128,7 +128,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

128128 toUN t@(P nt (MN i n) ty)

129129 | ('_':xs) <- str n = t

130130 | otherwise = P nt (UN n) ty

131− toUN (App f a) = App (toUN f) (toUN a)

131+ toUN (App s f a) = App s (toUN f) (toUN a)

132132 toUN t = t

133133

134134 -- psRec counts depth and the local variable applications we're under

src/Idris/Prover.hs+1−1

@@ -9,13 +9,13 @@ import Idris.Core.Typecheck

99

1010import Idris.Elab.Utils

1111import Idris.Elab.Value

12+import Idris.Elab.Term

1213

1314import Idris.AbsSyntax

1415import Idris.AbsSyntaxTree

1516import Idris.Delaborate

1617import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)

1718import Idris.ElabDecls

18−import Idris.ElabTerm

1919import Idris.Parser hiding (params)

2020import Idris.Error

2121import Idris.DataOpts

src/Idris/REPL.hs+1−1

@@ -8,7 +8,6 @@ import Idris.ASTUtils

88import Idris.Apropos (apropos, aproposModules)

99import Idris.REPLParser

1010import Idris.ElabDecls

11−import Idris.ElabTerm

1211import Idris.Erasure

1312import Idris.Error

1413import Idris.ErrReverse

@@ -39,6 +38,7 @@ import Idris.Elab.Type

3938import Idris.Elab.Clause

4039import Idris.Elab.Data

4140import Idris.Elab.Value

41+import Idris.Elab.Term

4242

4343import Version_idris (gitHash)

4444import Util.System

src/Idris/Reflection.hs+23−23

@@ -53,7 +53,7 @@ reify _ (P _ n _) | n == reflm "Compute" = return Compute

5353reify _ (P _ n _) | n == reflm "Skip" = return Skip

5454reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC

5555reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus

56−reify ist t@(App _ _)

56+reify ist t@(App _ _ _)

5757 | (P _ f _, args) <- unApply t = reifyApp ist f args

5858reify _ t = fail ("Unknown tactic " ++ show t)

5959

@@ -113,7 +113,7 @@ reifyReportParts errs =

113113

114114-- | Reify terms from their reflected representation

115115reifyTT :: Term -> ElabD Term

116−reifyTT t@(App _ _)

116+reifyTT t@(App _ _ _)

117117 | (P _ f _, args) <- unApply t = reifyTTApp f args

118118reifyTT t@(P _ n _)

119119 | n == reflm "Erased" = return $ Erased

@@ -137,7 +137,7 @@ reifyTTApp t [n, b, x]

137137reifyTTApp t [f, x]

138138 | t == reflm "App" = do f' <- reifyTT f

139139 x' <- reifyTT x

140− return $ App f' x'

140+ return $ App Complete f' x'

141141reifyTTApp t [c]

142142 | t == reflm "TConst" = liftM Constant (reifyTTConst c)

143143reifyTTApp t [t', Constant (I i)]

@@ -149,7 +149,7 @@ reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

149149

150150-- | Reify raw terms from their reflected representation

151151reifyRaw :: Term -> ElabD Raw

152−reifyRaw t@(App _ _)

152+reifyRaw t@(App _ _ _)

153153 | (P _ f _, args) <- unApply t = reifyRawApp f args

154154reifyRaw t@(P _ n _)

155155 | n == reflm "RType" = return $ RType

@@ -190,7 +190,7 @@ reifyTTNameApp t []

190190reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

191191

192192reifyTTNamespace :: Term -> ElabD [String]

193−reifyTTNamespace t@(App _ _)

193+reifyTTNamespace t@(App _ _ _)

194194 = case unApply t of

195195 (P _ f _, [Constant StrType])

196196 | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []

@@ -202,7 +202,7 @@ reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

202202reifyTTNameType :: Term -> ElabD NameType

203203reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound

204204reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

205−reifyTTNameType t@(App _ _)

205+reifyTTNameType t@(App _ _ _)

206206 = case unApply t of

207207 (P _ f _, [Constant (I tag), Constant (I num)])

208208 | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!

@@ -211,7 +211,7 @@ reifyTTNameType t@(App _ _)

211211reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

212212

213213reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)

214−reifyTTBinder reificator binderType t@(App _ _)

214+reifyTTBinder reificator binderType t@(App _ _ _)

215215 = case unApply t of

216216 (P _ f _, bt:args) | forget bt == Var binderType

217217 -> reifyTTBinderApp reificator f args

@@ -243,7 +243,7 @@ reifyTTConst :: Term -> ElabD Const

243243reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

244244reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType

245245reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

246−reifyTTConst t@(App _ _)

246+reifyTTConst t@(App _ _ _)

247247 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg

248248reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

249249

@@ -271,7 +271,7 @@ reifyTTConstApp f (Constant c@(B64 _))

271271reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

272272

273273reifyArithTy :: Term -> ElabD ArithTy

274−reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

274+reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

275275reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat

276276reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

277277

@@ -283,14 +283,14 @@ reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

283283reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x

284284

285285reifyIntTy :: Term -> ElabD IntTy

286−reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)

286+reifyIntTy (App _ (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)

287287reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative

288288reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig

289289reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar

290290reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

291291

292292reifyTTUExp :: Term -> ElabD UExp

293−reifyTTUExp t@(App _ _)

293+reifyTTUExp t@(App _ _ _)

294294 = case unApply t of

295295 (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

296296 (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

@@ -359,7 +359,7 @@ reflectTTQuotePattern unq (Bind n b x)

359359 solve

360360 focus x'; reflectTTQuotePattern unq x

361361 focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b

362−reflectTTQuotePattern unq (App f x)

362+reflectTTQuotePattern unq (App _ f x)

363363 = do f' <- claimTT (sMN 0 "f"); movelast f'

364364 x' <- claimTT (sMN 0 "x"); movelast x'

365365 fill $ reflCall "App" [Var f', Var x']

@@ -542,7 +542,7 @@ reflectTTQuote unq (V n)

542542 = reflCall "V" [RConstant (I n)]

543543reflectTTQuote unq (Bind n b x)

544544 = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

545−reflectTTQuote unq (App f x)

545+reflectTTQuote unq (App _ f x)

546546 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

547547reflectTTQuote unq (Constant c)

548548 = reflCall "TConst" [reflectConstant c]

@@ -814,7 +814,7 @@ reflectFC fc = raw_apply (Var (reflm "FileLoc"))

814814 where intTy = RConstant (AType (ATInt ITNative))

815815

816816fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

817−fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

817+fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

818818 | just == txt "Just" = Just tm

819819fromTTMaybe x = Nothing

820820

@@ -825,9 +825,9 @@ reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

825825-- representation. Not in Idris or ElabD monads because it should be usable

826826-- from either.

827827reifyReportPart :: Term -> Either Err ErrorReportPart

828−reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

828+reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

829829 Right (TextPart msg)

830−reifyReportPart (App (P (DCon _ _ _) n _) ttn)

830+reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

831831 | n == reflm "NamePart" =

832832 case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of

833833 Error e -> Left . InternalMsg $

@@ -835,7 +835,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) ttn)

835835 show ttn ++

836836 " when reflecting an error:" ++ show e

837837 OK (n', _)-> Right $ NamePart n'

838−reifyReportPart (App (P (DCon _ _ _) n _) tm)

838+reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

839839 | n == reflm "TermPart" =

840840 case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of

841841 Error e -> Left . InternalMsg $

@@ -843,7 +843,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

843843 show tm ++

844844 " when reflecting an error:" ++ show e

845845 OK (tm', _) -> Right $ TermPart tm'

846−reifyReportPart (App (P (DCon _ _ _) n _) tm)

846+reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

847847 | n == reflm "SubReport" =

848848 case unList tm of

849849 Just xs -> do subParts <- mapM reifyReportPart xs

@@ -852,7 +852,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

852852reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

853853

854854reifyTyDecl :: Term -> ElabD RTyDecl

855−reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

855+reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)

856856 | n == tacN "Declare" =

857857 do tyN' <- reifyTTName tyN

858858 args' <- case unList args of

@@ -861,7 +861,7 @@ reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

861861 ret' <- reifyRaw ret

862862 return $ RDeclare tyN' args' ret'

863863 where reifyRArg :: Term -> ElabD RArg

864− reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)

864+ reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)

865865 | n == tacN "Explicit" = liftM2 RExplicit

866866 (reifyTTName argN)

867867 (reifyRaw argTy)

@@ -874,7 +874,7 @@ reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

874874reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

875875

876876reifyFunDefn :: Term -> ElabD RFunDefn

877−reifyFunDefn (App (App (P _ n _) fnN) clauses)

877+reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)

878878 | n == tacN "DefineFun" =

879879 do fnN' <- reifyTTName fnN

880880 clauses' <- case unList clauses of

@@ -882,11 +882,11 @@ reifyFunDefn (App (App (P _ n _) fnN) clauses)

882882 Just cs -> mapM reifyC cs

883883 return $ RDefineFun fnN' clauses'

884884 where reifyC :: Term -> ElabD RFunClause

885− reifyC (App (App (P (DCon _ _ _) n _) lhs) rhs)

885+ reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)

886886 | n == tacN "MkFunClause" = liftM2 RMkFunClause

887887 (reifyRaw lhs)

888888 (reifyRaw rhs)

889− reifyC (App (P (DCon _ _ _) n _) lhs)

889+ reifyC (App _ (P (DCon _ _ _) n _) lhs)

890890 | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs

891891 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

892892reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

src/Idris/Transforms.hs+8−8

@@ -39,21 +39,21 @@ applyTransRulesWith rules tm

3939 = finalise $ applyAll rules emptyContext (vToP tm)

4040

4141applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term

42−applyAll extra ts ap@(App f a)

42+applyAll extra ts ap@(App s f a)

4343 | (P _ fn ty, args) <- unApply ap

4444 = let rules = case lookupCtxtExact fn ts of

4545 Just r -> extra ++ r

4646 Nothing -> extra

47− ap' = App (applyAll extra ts f) (applyAll extra ts a) in

47+ ap' = App s (applyAll extra ts f) (applyAll extra ts a) in

4848 case rules of

4949 [] -> ap'

5050 rs -> case applyFnRules rs ap of

51− Just tm'@(App f' a') ->

52− App (applyAll extra ts f')

53− (applyAll extra ts a')

51+ Just tm'@(App s f' a') ->

52+ App s (applyAll extra ts f')

53+ (applyAll extra ts a')

5454 Just tm' -> tm'

55− _ -> App (applyAll extra ts f)

56− (applyAll extra ts a)

55+ _ -> App s (applyAll extra ts f)

56+ (applyAll extra ts a)

5757applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)

5858 (applyAll extra ts sc)

5959applyAll extra ts t = t

@@ -94,7 +94,7 @@ matchTerm lhs tm = matchVars [] lhs tm

9494 doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]

9595 doMatch ns (P _ n _) tm

9696 | n `elem` ns = return [(n, tm)]

97− doMatch ns (App f a) (App f' a')

97+ doMatch ns (App _ f a) (App _ f' a')

9898 = do fm <- doMatch ns f f'

9999 am <- doMatch ns a a'

100100 return (fm ++ am)

src/Idris/TypeSearch.hs+7−6

@@ -104,9 +104,9 @@ typeFromDef (def, _, _, _) = get def where

104104-- Replace all occurences of `Lazy' s t` with `t` in a type

105105unLazy :: Type -> Type

106106unLazy typ = case typ of

107− App (App (P _ lazy _) _) ty | lazy == sUN "Lazy'" -> unLazy ty

107+ App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Lazy'" -> unLazy ty

108108 Bind name binder ty -> Bind name (fmap unLazy binder) (unLazy ty)

109− App t1 t2 -> App (unLazy t1) (unLazy t2)

109+ App s t1 t2 -> App s (unLazy t1) (unLazy t2)

110110 Proj ty i -> Proj (unLazy ty) i

111111 _ -> typ

112112

@@ -146,7 +146,7 @@ usedVars = f True where

146146 Let t v -> f b t `M.union` f b v

147147 Guess t v -> f b t `M.union` f b v

148148 bind -> f b (binderTy bind)

149− f b (App t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2

149+ f b (App _ t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2

150150 f b (Proj t _) = f b t

151151 f _ (V _) = error "unexpected! run vToP first"

152152 f _ _ = M.empty

@@ -307,13 +307,14 @@ subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss

307307-- recalls the number of flips that have been made

308308flipEqualities :: Type -> [(Int, Type)]

309309flipEqualities t = case t of

310− eq1@(App (App (App (App eq@(P _ eqty _) tyL) tyR) valL) valR) | eqty == eqTy ->

311− [(0, eq1), (1, App (App (App (App eq tyR) tyL) valR) valL)]

310+ eq1@(App _ (App _ (App _ (App _ eq@(P _ eqty _) tyL) tyR) valL) valR) | eqty == eqTy ->

311+ [(0, eq1), (1, app (app (app (app eq tyR) tyL) valR) valL)]

312312 Bind n binder sc -> (\bind' (j, sc') -> (fst (binderTy bind') + j, Bind n (fmap snd bind') sc'))

313313 <$> traverse flipEqualities binder <*> flipEqualities sc

314− App f x -> (\(i, f') (j, x') -> (i + j, App f' x'))

314+ App _ f x -> (\(i, f') (j, x') -> (i + j, app f' x'))

315315 <$> flipEqualities f <*> flipEqualities x

316316 t' -> [(0, t')]

317+ where app = App Complete

317318

318319--DONT run vToP first!

319320-- | Try to match two types together in a unification-like procedure.

src/Idris/WhoCalls.hs+2−2

@@ -13,7 +13,7 @@ occurs :: Name -> Term -> Bool

1313occurs n (P Bound _ _) = False

1414occurs n (P _ n' _) = n == n'

1515occurs n (Bind _ b sc) = occursBinder n b || occurs n sc

16−occurs n (App t1 t2) = occurs n t1 || occurs n t2

16+occurs n (App _ t1 t2) = occurs n t1 || occurs n t2

1717occurs n (Proj t _) = occurs n t

1818occurs n _ = False

1919

@@ -21,7 +21,7 @@ names :: Term -> [Name]

2121names (P Bound _ _) = []

2222names (P _ n _) = [n]

2323names (Bind _ b sc) = namesBinder b ++ names sc

24−names (App t1 t2) = names t1 ++ names t2

24+names (App _ t1 t2) = names t1 ++ names t2

2525names (Proj t _) = names t

2626names _ = []

2727

test/README+1

@@ -1,6 +1,7 @@

11Tests are categorised as follows:

22

33basic: Basic language features, some complete programs

4+bignum: Bignums and GMP

45dsl: Embedded DSLs and features to support DSL development

56effects: Effects package

67error: Error messages and error reflection

test/bignum001/bignum001.idrnew file+17

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

1+module Main

2+

3+fac : Integer -> Integer

4+fac 0 = 1

5+fac n = n*fac(n-1)

6+

7+binomial : Integer -> Integer -> Integer

8+binomial n k = divBigInt (fac n) ((fac k)*(fac (n-k)))

9+

10+sumBinomials : Integer -> Integer

11+sumBinomials n = foldr (+) 0 (map (\k=>binomial n k) [0..n])

12+

13+main : IO ()

14+main = do

15+ if sumBinomials 1000 - pow 2 1000 == 0

16+ then putStrLn "OK"

17+ else putStrLn "ERROR"

test/bignum001/expectednew file+1

@@ -0,0 +1 @@

1+OK

test/bignum001/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ bignum001.idr -o bignum001

3+./bignum001

4+rm -f bignum001 *.ibc

test/dsl002/expected−1

@@ -1,2 +1 @@

11foo

2−

test/effects001/expected+1−1

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

1−["HELLO!!!\n", "WORLD!!!\n", ""]

1+["HELLO!!!", "WORLD!!!", ""]

223

3315

44Answer: 99

test/folding002/expected+2−2

@@ -1,2 +1,2 @@

1−500000500000

2−500000500000

1+5000050000

2+5000050000

test/folding002/folding002.idr+1−1

@@ -5,7 +5,7 @@ addAll : (Foldable t, Num a) => t a -> a

55addAll = foldr (+) 0

66

77n : Integer

8−n = 1000000

8+n = 100000

99

1010numbersList : List Integer

1111numbersList = numbersList' n []

test/io001/expected+1

@@ -13,4 +13,5 @@ World!

13133

14144

1515Last line

16+

1617---

test/io001/test004.idr+1−1

@@ -13,7 +13,7 @@ dumpFile fn = do { h <- openFile fn Read

1313 x <- feof h

1414 return (not x) })

1515 (do { l <- fread h

16− putStr l })

16+ putStrLn l })

1717 closeFile h }

1818

1919main : IO ()

test/runtest.pl+3−2

@@ -10,10 +10,11 @@ my @idrOpts = ();

1010

1111sub sandbox_path {

1212 my ($test_dir,) = @_;

13− my $sandbox = abs_path("$test_dir/../../.cabal-sandbox/bin");

13+ my $sandbox = "$test_dir/../../.cabal-sandbox/bin";

1414

1515 if ( -d $sandbox ) {

16− return "PATH=\"$sandbox:$PATH\"";

16+ my $sandbox_abs = abs_path($sandbox);

17+ return "PATH=\"$sandbox_abs:$PATH\"";

1718 } else {

1819 return "";

1920 }