370939b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

Conflicts: src/Idris/Elab/Term.hs

commit370939baddd7a72405a36e0289bfe23485410a7a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 16 Apr 2015, 11:38 (12 years ago) parent3ed4dcf 72f4386

56 files changed+1356−3824

compare with master

unifiedsplit

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.

libs/base/Data/Bits.idr+5−10

@@ -4,21 +4,16 @@ import Data.Fin

55%default total

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/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

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

88 Raise : a -> sig (Exception a) b

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

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/Language/Reflection/Elab.idrnew file+149

@@ -0,0 +1,149 @@

1+module Language.Reflection.Elab

3+import Builtins

4+import Prelude.Applicative

5+import Prelude.Functor

6+import Prelude.List

7+import Prelude.Maybe

8+import Prelude.Monad

9+import Language.Reflection

10+

11+data Arg : Type where

12+ Explicit : TTName -> Raw -> Arg

13+ Implicit : TTName -> Raw -> Arg

14+ Constraint : TTName -> Raw -> Arg

15+

16+data TyDecl : Type where

17+ Declare : TTName -> List Arg -> Raw -> TyDecl

18+

19+data FunClause : Type where

20+ MkFunClause : (lhs, rhs : Raw) -> FunClause

21+ MkImpossibleClause : (lhs : Raw) -> FunClause

22+

23+data FunDefn : Type where

24+ DefineFun : TTName -> List FunClause -> FunDefn

25+

26+abstract

27+data Elab : Type -> Type where

28+ -- obligatory control stuff

29+ prim__PureElab : a -> Elab a

30+ prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b

31+

32+ prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a

33+ prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a

34+

35+ prim__Env : Elab (List (TTName, Binder TT))

36+ prim__Goal : Elab (TTName, TT)

37+ prim__Holes : Elab (List TTName)

38+ prim__Guess : Elab (Maybe TT)

39+

40+ prim__SourceLocation : Elab SourceLocation

41+

42+ prim__Forget : TT -> Elab Raw

43+

44+ prim__Gensym : String -> Elab TTName

45+

46+ prim__Solve : Elab ()

47+ prim__Fill : Raw -> Elab ()

48+ prim__Focus : TTName -> Elab ()

49+ prim__Unfocus : TTName -> Elab ()

50+ prim__Attack : Elab ()

51+

52+ prim__Rewrite : Raw -> Elab ()

53+

54+ prim__Claim : TTName -> Raw -> Elab ()

55+ prim__Intro : Maybe TTName -> Elab ()

56+

57+ prim__DeclareType : TyDecl -> Elab ()

58+ prim__DefineFunction : FunDefn -> Elab ()

59+

60+ prim__Debug : {a : Type} -> Maybe String -> Elab a

61+

62+

63+-------------

64+-- Public API

65+-------------

66+%access public

67+

68+instance Functor Elab where

69+ map f t = prim__BindElab t (\x => prim__PureElab (f x))

70+

71+instance Applicative Elab where

72+ pure x = prim__PureElab x

73+ f <*> x = prim__BindElab f $ \g =>

74+ prim__BindElab x $ \y =>

75+ prim__PureElab $ g y

76+

77+instance Alternative Elab where

78+ empty = prim__Fail [TextPart "empty"]

79+ x <|> y = prim__Try x y

80+

81+instance Monad Elab where

82+ x >>= f = prim__BindElab x f

83+

84+fail : List ErrorReportPart -> Elab a

85+fail err = prim__Fail err

86+

87+getEnv : Elab (List (TTName, Binder TT))

88+getEnv = prim__Env

89+

90+getGoal : Elab (TTName, TT)

91+getGoal = prim__Goal

92+

93+getHoles : Elab (List TTName)

94+getHoles = prim__Holes

95+

96+getGuess : Elab (Maybe TT)

97+getGuess = prim__Guess

98+

99+forgetTypes : TT -> Elab Raw

100+forgetTypes tt = prim__Forget tt

101+

102+gensym : (hint : String) -> Elab TTName

103+gensym hint = prim__Gensym hint

104+

105+solve : Elab ()

106+solve = prim__Solve

107+

108+fill : Raw -> Elab ()

109+fill tm = prim__Fill tm

110+

111+focus : (hole : TTName) -> Elab ()

112+focus hole = prim__Focus hole

113+

114+unfocus : TTName -> Elab ()

115+unfocus hole = prim__Unfocus hole

116+

117+attack : Elab ()

118+attack = prim__Attack

119+

120+claim : TTName -> Raw -> Elab ()

121+claim n ty = prim__Claim n ty

122+

123+intro : Maybe TTName -> Elab ()

124+intro n = prim__Intro n

125+

126+||| Find out the present source context for the tactic script

127+getSourceLocation : Elab SourceLocation

128+getSourceLocation = prim__SourceLocation

129+

130+||| Attempt to solve the current goal with the source code location

131+sourceLocation : Elab ()

132+sourceLocation = do loc <- getSourceLocation

133+ fill (quote loc)

134+ solve

135+

136+rewriteWith : Raw -> Elab ()

137+rewriteWith rule = prim__Rewrite rule

138+

139+declareType : TyDecl -> Elab ()

140+declareType decl = prim__DeclareType decl

141+

142+defineFunction : FunDefn -> Elab ()

143+defineFunction defun = prim__DefineFunction defun

144+

145+debug : Elab a

146+debug = prim__Debug Nothing

147+

148+debugMessage : String -> Elab a

149+debugMessage msg = prim__Debug (Just msg)

libs/prelude/Language/Reflection/Tactical.idrdeleted−138

@@ -1,138 +0,0 @@

1−module Language.Reflection.Tactical

2−

3−import Builtins

4−import Prelude.Applicative

5−import Prelude.Functor

6−import Prelude.List

7−import Prelude.Maybe

8−import Prelude.Monad

9−import Language.Reflection

10−

11−data Arg : Type where

12− Explicit : TTName -> Raw -> Arg

13− Implicit : TTName -> Raw -> Arg

14− Constraint : TTName -> Raw -> Arg

15−

16−data TyDecl : Type where

17− Declare : TTName -> List Arg -> Raw -> TyDecl

18−

19−abstract

20−data Tactical : Type -> Type where

21− -- obligatory control stuff

22− prim__PureTactical : a -> Tactical a

23− prim__BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b

24−

25− prim__Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a

26− prim__Fail : {a : Type} -> List ErrorReportPart -> Tactical a

27−

28− prim__Env : Tactical (List (TTName, Binder TT))

29− prim__Goal : Tactical (TTName, TT)

30− prim__Holes : Tactical (List TTName)

31− prim__Guess : Tactical (Maybe TT)

32−

33− prim__SourceLocation : Tactical SourceLocation

34−

35− prim__Forget : TT -> Tactical Raw

36−

37− prim__Gensym : String -> Tactical TTName

38−

39− prim__Solve : Tactical ()

40− prim__Fill : Raw -> Tactical ()

41− prim__Focus : TTName -> Tactical ()

42− prim__Unfocus : TTName -> Tactical ()

43− prim__Attack : Tactical ()

44−

45− prim__Rewrite : Raw -> Tactical ()

46−

47− prim__Claim : TTName -> Raw -> Tactical ()

48− prim__Intro : Maybe TTName -> Tactical ()

49−

50− prim__DeclareType : TyDecl -> Tactical ()

51−

52− prim__Debug : {a : Type} -> Maybe String -> Tactical a

53−

54−

55−-------------

56−-- Public API

57−-------------

58−%access public

59−

60−instance Functor Tactical where

61− map f t = prim__BindTactical t (\x => prim__PureTactical (f x))

62−

63−instance Applicative Tactical where

64− pure x = prim__PureTactical x

65− f <*> x = prim__BindTactical f $ \g =>

66− prim__BindTactical x $ \y =>

67− prim__PureTactical $ g y

68−

69−instance Alternative Tactical where

70− empty = prim__Fail [TextPart "empty"]

71− x <|> y = prim__Try x y

72−

73−instance Monad Tactical where

74− x >>= f = prim__BindTactical x f

75−

76−fail : List ErrorReportPart -> Tactical a

77−fail err = prim__Fail err

78−

79−getEnv : Tactical (List (TTName, Binder TT))

80−getEnv = prim__Env

81−

82−getGoal : Tactical (TTName, TT)

83−getGoal = prim__Goal

84−

85−getHoles : Tactical (List TTName)

86−getHoles = prim__Holes

87−

88−getGuess : Tactical (Maybe TT)

89−getGuess = prim__Guess

90−

91−forgetTypes : TT -> Tactical Raw

92−forgetTypes tt = prim__Forget tt

93−

94−gensym : (hint : String) -> Tactical TTName

95−gensym hint = prim__Gensym hint

96−

97−solve : Tactical ()

98−solve = prim__Solve

99−

100−fill : Raw -> Tactical ()

101−fill tm = prim__Fill tm

102−

103−focus : (hole : TTName) -> Tactical ()

104−focus hole = prim__Focus hole

105−

106−unfocus : TTName -> Tactical ()

107−unfocus hole = prim__Unfocus hole

108−

109−attack : Tactical ()

110−attack = prim__Attack

111−

112−claim : TTName -> Raw -> Tactical ()

113−claim n ty = prim__Claim n ty

114−

115−intro : Maybe TTName -> Tactical ()

116−intro n = prim__Intro n

117−

118−||| Find out the present source context for the tactic script

119−getSourceLocation : Tactical SourceLocation

120−getSourceLocation = prim__SourceLocation

121−

122−||| Attempt to solve the current goal with the source code location

123−sourceLocation : Tactical ()

124−sourceLocation = do loc <- getSourceLocation

125− fill (quote loc)

126− solve

127−

128−rewriteWith : Raw -> Tactical ()

129−rewriteWith rule = prim__Rewrite rule

130−

131−declareType : TyDecl -> Tactical ()

132−declareType decl = prim__DeclareType decl

133−

134−debug : Tactical a

135−debug = prim__Debug Nothing

136−

137−debugMessage : String -> Tactical a

138−debugMessage msg = prim__Debug (Just msg)

libs/prelude/Prelude.idr+9−7

@@ -135,7 +135,7 @@ instance Show a => Show (Maybe a) where

135135 show (Just x) = "Just " ++ show x

136136

137137instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

138− show (y ** prf) = show y ++ " ** " ++ show prf

138+ show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

139139

140140---- Functor instances

141141

@@ -245,8 +245,8 @@ natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc

245245total natEnumFromTo : Nat -> Nat -> List Nat

246246natEnumFromTo n m = map (plus n) (natRange ((S m) - n))

247247total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat

248−natEnumFromThenTo _ Z _ = []

249−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)))

250250

251251class Enum a where

252252 total pred : a -> a

@@ -285,7 +285,7 @@ instance Enum Integer where

285285 go [] = []

286286 go (x :: xs) = n + cast x :: go xs

287287 enumFromThenTo _ 0 _ = []

288− 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)))

289289 where go : List Nat -> List Integer

290290 go [] = []

291291 go (x :: xs) = n + (cast x * inc) :: go xs

@@ -305,7 +305,7 @@ instance Enum Int where

305305 go acc (S k) m = go (m :: acc) k (m - 1)

306306 enumFromThen n inc = n :: enumFromThen (inc + n) inc

307307 enumFromThenTo _ 0 _ = []

308− 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)))

309309 where go : List Nat -> List Int

310310 go [] = []

311311 go (x :: xs) = n + (cast x * inc) :: go xs

@@ -349,7 +349,7 @@ partial

349349printLn : Show a => a -> IO' ffi ()

350350printLn x = putStrLn (show x)

351351

352−||| Read one line of input from stdin

352+||| Read one line of input from stdin, without the trailing newline

353353partial

354354getLine : IO' ffi String

355355getLine = prim_read

@@ -548,5 +548,7 @@ readFile fn = do h <- openFile fn Read

548548 readFile' h contents =

549549 do x <- feof h

550550 if not x then do l <- fread h

551− readFile' h (contents ++ l)

551+ case contents of

552+ "" => readFile' h l

553+ _ => readFile' h (contents ++ "\n" ++ l)

552554 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--------------------------------------------------------------------------------

libs/prelude/prelude.ipkg+1−1

@@ -10,7 +10,7 @@ modules = Builtins, Prelude, IO,

1010 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

1111 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,

1212

13− Language.Reflection, Language.Reflection.Errors, Language.Reflection.Tactical,

13+ Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,

1414

1515 Decidable.Equality

1616

rts/idris_rts.c+5−2

@@ -504,17 +504,20 @@ VAL idris_strlen(VM* vm, VAL l) {

504504}

505505

506506VAL idris_readStr(VM* vm, FILE* h) {

507+ VAL ret;

507508 char *buffer = NULL;

508509 size_t n = 0;

509510 ssize_t len;

510511 len = getline(&buffer, &n, h);

512+ strtok(buffer, "\n");

511513

512514 if (len <= 0) {

513− return MKSTR(vm, "");

515+ ret = MKSTR(vm, "");

514516 } else {

515− return MKSTR(vm, buffer);

517+ ret = MKSTR(vm, buffer);

516518 }

517519 free(buffer);

520+ return ret;

518521}

519522

520523VAL idris_strHead(VM* vm, VAL str) {

src/Idris/AbsSyntax.hs+4−4

@@ -1011,7 +1011,7 @@ expandParams dec ps ns infs tm = en tm

10111011 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

10121012 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

10131013 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

1014− en (PRunTactics fc tm) = PRunTactics fc (en tm)

1014+ en (PRunElab fc tm) = PRunElab fc (en tm)

10151015 en t = t

10161016

10171017 nselem x [] = False

@@ -1485,7 +1485,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

14851485 imps top env (PHidden tm) = imps False env tm

14861486 imps top env (PUnifyLog tm) = imps False env tm

14871487 imps top env (PNoImplicits tm) = imps False env tm

1488− imps top env (PRunTactics fc tm) = imps False env tm

1488+ imps top env (PRunElab fc tm) = imps False env tm

14891489 imps top env _ = return ()

14901490

14911491 pibind using [] sc = sc

@@ -1612,7 +1612,7 @@ addImpl' inpat env infns imp_meths ist ptm

16121612 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

16131613 (fmap (ai True env ds) g)

16141614 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

1615− ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm)

1615+ ai qq env ds (PRunElab fc tm) = PRunElab fc (ai False env ds tm)

16161616 ai qq env ds tm = tm

16171617

16181618 handleErr (Left err) = PElabError err

@@ -2149,5 +2149,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

21492149 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

21502150 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

21512151 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

2152− mkUniq (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts)

2152+ mkUniq (PRunElab fc ts) = liftM (PRunElab fc ) (mkUniq ts)

21532153 mkUniq t = return t

src/Idris/AbsSyntaxTree.hs+20−7

@@ -645,11 +645,16 @@ deriving instance Binary PDecl'

645645deriving instance NFData PDecl'

646646!-}

647647

648−-- For elaborator state

648+-- | A set of instructions for things that need to happen in IState

649+-- after a term elaboration when there's been reflected elaboration.

650+data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

651+ | RClausesInstrs Name [([Name], Term, Term)]

652+

653+-- | For elaborator state

649654data EState = EState {

650655 case_decls :: [PDecl],

651656 delayed_elab :: [Elab' EState ()],

652− new_tyDecls :: [(Name, FC, [PArg], Type)]

657+ new_tyDecls :: [RDeclInstructions]

653658 }

654659

655660initEState :: EState

@@ -821,7 +826,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

821826 | PNoImplicits PTerm -- ^ never run implicit converions on the term

822827 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

823828 | PUnquote PTerm -- ^ ~Term

824− | PRunTactics FC PTerm -- ^ %runTactics tm - New-style proof script

829+ | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script

825830 deriving (Eq, Data, Typeable)

826831

827832

@@ -1428,16 +1433,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

14281433 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

14291434 prettySe p bnd (PLam fc n ty sc) =

14301435 bracket p startPrec . group . align . hang 2 $

1431− text "\\" <> bindingOf n False <+> text "=>" <$>

1436+ text "\\" <> prettyBindingOf n False <+> text "=>" <$>

14321437 prettySe startPrec ((n, False):bnd) sc

14331438 prettySe p bnd (PLet fc n ty v sc) =

14341439 bracket p startPrec . group . align $

1435− kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>

1440+ kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>

14361441 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)

14371442 prettySe p bnd (PPi (Exp l s _) n ty sc)

14381443 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

14391444 bracket p startPrec . group $

1440− enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>

1445+ enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>

14411446 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc

14421447 | otherwise =

14431448 bracket p startPrec . group $

@@ -1450,7 +1455,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

14501455 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)

14511456 | ppopt_impl ppo =

14521457 bracket p startPrec $

1453− lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

1458+ lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

14541459 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc

14551460 | otherwise = prettySe startPrec ((n, True):bnd) sc

14561461 where

@@ -1607,6 +1612,14 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

16071612

16081613 prettySe p bnd _ = text "missing pretty-printer for term"

16091614

1615+ prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation

1616+ prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))

1617+ where display (UN n) = T.unpack n

1618+ display (MN _ n) = T.unpack n

1619+ -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings

1620+ display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n

1621+ display n = show n

1622+

16101623 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

16111624 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm

16121625 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

src/Idris/Core/TT.hs+4−3

@@ -117,9 +117,6 @@ data ErrorReportPart = TextPart String

117117 deriving (Show, Eq, Data, Typeable)

118118

119119

120−-- Please remember to keep Err synchronised with

121−-- Language.Reflection.Errors.Err in the stdlib!

122−

123120data Provenance = ExpectedType

124121 | TooManyArgs Term

125122 | InferredVal

@@ -131,6 +128,10 @@ deriving instance NFData Err

131128deriving instance Binary Err

132129!-}

133130

131+

132+-- NB: Please remember to keep Err synchronised with

133+-- Language.Reflection.Errors.Err in the stdlib!

134+

134135-- | Idris errors. Used as exceptions in the compiler, but reported to users

135136-- if they reach the top level.

136137data Err' t

src/Idris/DSL.hs+2−2

@@ -108,7 +108,7 @@ expandDo dsl (PDoBlock ds)

108108 block b _ = PElabError (Msg "Invalid statement in do block")

109109

110110expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

111−expandDo dsl (PRunTactics fc tm) = PRunTactics fc $ expandDo dsl tm

111+expandDo dsl (PRunElab fc tm) = PRunElab fc $ expandDo dsl tm

112112expandDo dsl t = t

113113

114114-- | Replace DSL-bound variable in a term

@@ -195,7 +195,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

195195 db' (PDPair fc p l t r) = do l' <- db' l

196196 r' <- db' r

197197 return (PDPair fc p l' t r')

198− db' (PRunTactics fc t) = fmap (PRunTactics fc) (db' t)

198+ db' (PRunElab fc t) = fmap (PRunElab fc) (db' t)

199199 db' t = return t

200200

201201 dbArg a = do t' <- db' (getTm a)

src/Idris/DeepSeq.hs+1−1

@@ -243,7 +243,7 @@ instance NFData PTerm where

243243 rnf (PNoImplicits x1) = rnf x1 `seq` ()

244244 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

245245 rnf (PUnquote x1) = rnf x1 `seq` ()

246− rnf (PRunTactics x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

246+ rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

247247

248248instance (NFData t) => NFData (PTactic' t) where

249249 rnf (Intro x1) = rnf x1 `seq` ()

src/Idris/Elab/Term.hs+71−864

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

1−{-# LANGUAGE PatternGuards, ViewPatterns #-}

1+{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}

22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

33module Idris.Elab.Term where

@@ -10,6 +10,7 @@ import Idris.Error

1010import Idris.ProofSearch

1111import Idris.Output (pshow)

1212

13+import Idris.Core.CaseTree (SC, SC'(STerm))

1314import Idris.Core.Elaborate hiding (Tactic(..))

1415import Idris.Core.TT

1516import Idris.Core.Evaluate

@@ -35,6 +36,7 @@ import Debug.Trace

3536data ElabMode = ETyDecl | ELHS | ERHS

3637 deriving Eq

3738

39+

3840data ElabResult =

3941 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

4042 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]

@@ -43,23 +45,28 @@ data ElabResult =

4345 -- ^ Deferred declarations as the meaning of case blocks

4446 , resultContext :: Context

4547 -- ^ The potentially extended context from new definitions

46− , resultTyDecls :: [(Name, FC, [PArg], Type)]

48+ , resultTyDecls :: [RDeclInstructions]

4749 -- ^ Meta-info about the new type declarations

4850 }

4951

50−processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()

52+processTacticDecls :: [RDeclInstructions] -> Idris ()

5153processTacticDecls info =

52− forM_ info $ \(n, fc, impls, ty) ->

53− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

54− logLvl 3 $ " It has impls " ++ show impls

55− updateIState $ \i -> i { idris_implicits =

56− addDef n impls (idris_implicits i) }

57− addIBC (IBCImp n)

58− ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]

59− addIBC (IBCDef n)

60− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

61− addDeferred ds'

62−

54+ forM_ info $ \case

55+ RTyDeclInstrs n fc impls ty ->

56+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

57+ logLvl 3 $ " It has impls " ++ show impls

58+ updateIState $ \i -> i { idris_implicits =

59+ addDef n impls (idris_implicits i) }

60+ addIBC (IBCImp n)

61+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]

62+ addIBC (IBCDef n)

63+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

64+ addDeferred ds'

65+ RClausesInstrs n cs ->

66+ do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n

67+ solveDeferred n

68+ updateIState $ \i -> i { idris_patdefs = addDef n (cs, []) $ idris_patdefs i } -- TODO: missing clauses

69+ addIBC (IBCDef n)

6370

6471-- Using the elaborator, convert a term in raw syntax to a fully

6572-- elaborated, typechecked term.

@@ -213,7 +220,7 @@ goal_polymorphic =

213220

214221-- | Returns the set of declarations we need to add to complete the

215222-- definition (most likely case blocks to elaborate) as well as

216−-- declarations resulting from user tactic scripts (%runTactics)

223+-- declarations resulting from user tactic scripts (%runElab)

217224elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

218225 ElabD ()

219226elab ist info emode opts fn tm

@@ -1098,11 +1105,11 @@ elab ist info emode opts fn tm

10981105 delayElab $ do focus h

10991106 dotterm

11001107 elab' ina fc t

1101− elab' ina fc (PRunTactics fc' tm) =

1108+ elab' ina fc (PRunElab fc' tm) =

11021109 do attack

11031110 n <- getNameFrom (sMN 0 "tacticScript")

11041111 n' <- getNameFrom (sMN 0 "tacticExpr")

1105− let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)

1112+ let scriptTy = RApp (Var (sNS (sUN "Elab") ["Elab", "Reflection", "Language"])) (Var unitTy)

11061113 claim n scriptTy

11071114 movelast n

11081115 letbind n' scriptTy (Var n)

@@ -1592,8 +1599,6 @@ case_ ind autoSolve ist fn tm = do

15921599 else casetac (forget val)

15931600 when autoSolve solveAll

15941601

1595−tacN :: String -> Name

1596−tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

15971602

15981603runTactical :: FC -> Env -> Term -> ElabD ()

15991604runTactical fc env tm = do tm' <- eval tm

@@ -1605,6 +1610,45 @@ runTactical fc env tm = do tm' <- eval tm

16051610

16061611 returnUnit = fmap fst $ get_type_val (Var unitCon)

16071612

1613+ patvars :: [Name] -> Term -> ([Name], Term)

1614+ patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)

1615+ patvars ns tm = (ns, tm)

1616+

1617+ pullVars :: (Term, Term) -> ([Name], Term, Term)

1618+ pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs

1619+

1620+ defineFunction :: RFunDefn -> ElabD ()

1621+ defineFunction (RDefineFun n clauses) =

1622+ do ctxt <- get_context

1623+ ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt

1624+ let info = CaseInfo True True False -- TODO document and figure out

1625+ clauses' <- forM clauses (\case

1626+ RMkFunClause lhs rhs ->

1627+ do lhs' <- fmap fst . lift $ check ctxt [] lhs

1628+ rhs' <- fmap fst . lift $ check ctxt [] rhs

1629+ return $ Right (lhs', rhs')

1630+ RMkImpossibleClause lhs ->

1631+ do lhs' <- fmap fst . lift $ check ctxt [] lhs

1632+ return $ Left lhs')

1633+ let clauses'' = map (\case Right c -> pullVars c

1634+ Left lhs -> let (ns, lhs') = patvars [] lhs'

1635+ in (ns, lhs', Impossible))

1636+ clauses'

1637+ set_context $

1638+ addCasedef n (const [])

1639+ info False (STerm Erased)

1640+ True False -- TODO what are these?

1641+ [] [] -- TODO argument types, inaccessible types

1642+ clauses'

1643+ clauses''

1644+ clauses''

1645+ clauses''

1646+ clauses''

1647+ ty

1648+ ctxt

1649+ updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}

1650+ return ()

1651+

16081652 -- | Do a step in the reflected elaborator monad. The input is the

16091653 -- step, the output is the (reflected) term returned.

16101654 runTacTm :: Term -> ElabD Term

@@ -1643,9 +1687,9 @@ runTactical fc env tm = do tm' <- eval tm

16431687 = do errs' <- eval errs

16441688 parts <- reifyReportParts errs'

16451689 lift . tfail $ ReflectionError [parts] (Msg "")

1646− | n == tacN "prim__PureTactical", [_a, tm] <- args

1690+ | n == tacN "prim__PureElab", [_a, tm] <- args

16471691 = return tm

1648− | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1692+ | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args

16491693 = do first' <- eval first

16501694 res <- runTacTm first'

16511695 next <- eval (App Complete andThen res)

@@ -1672,7 +1716,7 @@ runTactical fc env tm = do tm' <- eval tm

16721716 returnUnit

16731717 | n == tacN "prim__Forget", [tt] <- args

16741718 = do tt' <- reifyTT tt

1675− fmap fst . get_type_val $ reflect tt'

1719+ fmap fst . get_type_val . reflectRaw $ forget tt'

16761720 | n == tacN "prim__Attack", [] <- args

16771721 = do attack

16781722 returnUnit

@@ -1713,10 +1757,14 @@ runTactical fc env tm = do tm' <- eval tm

17131757 let decl = TyDecl Ref checked

17141758 ctxt' = addCtxtDef n decl ctxt

17151759 set_context ctxt'

1716− updateAux $ \e -> e { new_tyDecls = (n, fc, map rArgToPArg args, checked) :

1760+ updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rArgToPArg args) checked) :

17171761 new_tyDecls e }

17181762 aux <- getAux

17191763 returnUnit

1764+ | n == tacN "prim__DefineFunction", [decl] <- args

1765+ = do defn <- reifyFunDefn decl

1766+ defineFunction defn

1767+ returnUnit

17201768 | n == tacN "prim__Debug", [ty, msg] <- args

17211769 = do let msg' = fromTTMaybe msg

17221770 case msg' of

@@ -1978,781 +2026,6 @@ runTac autoSolve ist perhapsFC fn tac

19782026 runReflected t = do t' <- reify ist t

19792027 runTac autoSolve ist perhapsFC fn t'

19802028

1981−-- | Prefix a name with the "Language.Reflection" namespace

1982−reflm :: String -> Name

1983−reflm n = sNS (sUN n) ["Reflection", "Language"]

1984−

1985−

1986−-- | Reify tactics from their reflected representation

1987−reify :: IState -> Term -> ElabD PTactic

1988−reify _ (P _ n _) | n == reflm "Intros" = return Intros

1989−reify _ (P _ n _) | n == reflm "Trivial" = return Trivial

1990−reify _ (P _ n _) | n == reflm "Instance" = return TCInstance

1991−reify _ (P _ n _) | n == reflm "Solve" = return Solve

1992−reify _ (P _ n _) | n == reflm "Compute" = return Compute

1993−reify _ (P _ n _) | n == reflm "Skip" = return Skip

1994−reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC

1995−reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus

1996−reify ist t@(App _ _ _)

1997− | (P _ f _, args) <- unApply t = reifyApp ist f args

1998−reify _ t = fail ("Unknown tactic " ++ show t)

1999−

2000−reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

2001−reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)

2002−reifyApp _ t [Constant (I i)]

2003− | t == reflm "Search" = return (ProofSearch True True i Nothing [])

2004−reifyApp _ t [x]

2005− | t == reflm "Refine" = do n <- reifyTTName x

2006− return $ Refine n []

2007−reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n

2008− goal <- reifyTT ty

2009− return $ Claim n' (delab ist goal)

2010−reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)

2011−reifyApp ist t [Constant (Str n), x]

2012− | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

2013−reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)

2014−reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')

2015−reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')

2016−reifyApp ist t [t']

2017− | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

2018−reifyApp ist t [t']

2019− | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')

2020−reifyApp ist t [t']

2021− | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')

2022−reifyApp _ t [t']

2023− | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')

2024−reifyApp ist t [t']

2025− | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')

2026−reifyApp ist t [x]

2027− | t == reflm "Focus" = liftM Focus (reifyTTName x)

2028−reifyApp ist t [t']

2029− | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')

2030−reifyApp ist t [n, t']

2031− | t == reflm "LetTac" = do n' <- reifyTTName n

2032− t'' <- reifyTT t'

2033− return $ LetTac n' (delab ist t')

2034−reifyApp ist t [n, tt', t']

2035− | t == reflm "LetTacTy" = do n' <- reifyTTName n

2036− tt'' <- reifyTT tt'

2037− t'' <- reifyTT t'

2038− return $ LetTacTy n' (delab ist tt'') (delab ist t'')

2039−reifyApp ist t [errs]

2040− | t == reflm "Fail" = fmap TFail (reifyReportParts errs)

2041−reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

2042−

2043−reifyReportParts :: Term -> ElabD [ErrorReportPart]

2044−reifyReportParts errs =

2045− case unList errs of

2046− Nothing -> fail "Failed to reify errors"

2047− Just errs' ->

2048− let parts = mapM reifyReportPart errs' in

2049− case parts of

2050− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err

2051− Right errs'' ->

2052− return errs''

2053−

2054−-- | Reify terms from their reflected representation

2055−reifyTT :: Term -> ElabD Term

2056−reifyTT t@(App _ _ _)

2057− | (P _ f _, args) <- unApply t = reifyTTApp f args

2058−reifyTT t@(P _ n _)

2059− | n == reflm "Erased" = return $ Erased

2060−reifyTT t@(P _ n _)

2061− | n == reflm "Impossible" = return $ Impossible

2062−reifyTT t = fail ("Unknown reflection term: " ++ show t)

2063−

2064−reifyTTApp :: Name -> [Term] -> ElabD Term

2065−reifyTTApp t [nt, n, x]

2066− | t == reflm "P" = do nt' <- reifyTTNameType nt

2067− n' <- reifyTTName n

2068− x' <- reifyTT x

2069− return $ P nt' n' x'

2070−reifyTTApp t [Constant (I i)]

2071− | t == reflm "V" = return $ V i

2072−reifyTTApp t [n, b, x]

2073− | t == reflm "Bind" = do n' <- reifyTTName n

2074− b' <- reifyTTBinder reifyTT (reflm "TT") b

2075− x' <- reifyTT x

2076− return $ Bind n' b' x'

2077−reifyTTApp t [f, x]

2078− | t == reflm "App" = do f' <- reifyTT f

2079− x' <- reifyTT x

2080− return $ App Complete f' x'

2081−reifyTTApp t [c]

2082− | t == reflm "TConst" = liftM Constant (reifyTTConst c)

2083−reifyTTApp t [t', Constant (I i)]

2084− | t == reflm "Proj" = do t'' <- reifyTT t'

2085− return $ Proj t'' i

2086−reifyTTApp t [tt]

2087− | t == reflm "TType" = liftM TType (reifyTTUExp tt)

2088−reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

2089−

2090−-- | Reify raw terms from their reflected representation

2091−reifyRaw :: Term -> ElabD Raw

2092−reifyRaw t@(App _ _ _)

2093− | (P _ f _, args) <- unApply t = reifyRawApp f args

2094−reifyRaw t@(P _ n _)

2095− | n == reflm "RType" = return $ RType

2096−reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)

2097−

2098−reifyRawApp :: Name -> [Term] -> ElabD Raw

2099−reifyRawApp t [n]

2100− | t == reflm "Var" = liftM Var (reifyTTName n)

2101−reifyRawApp t [n, b, x]

2102− | t == reflm "RBind" = do n' <- reifyTTName n

2103− b' <- reifyTTBinder reifyRaw (reflm "Raw") b

2104− x' <- reifyRaw x

2105− return $ RBind n' b' x'

2106−reifyRawApp t [f, x]

2107− | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)

2108−reifyRawApp t [t']

2109− | t == reflm "RForce" = liftM RForce (reifyRaw t')

2110−reifyRawApp t [c]

2111− | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)

2112−reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))

2113−

2114−reifyTTName :: Term -> ElabD Name

2115−reifyTTName t

2116− | (P _ f _, args) <- unApply t = reifyTTNameApp f args

2117−reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

2118−

2119−reifyTTNameApp :: Name -> [Term] -> ElabD Name

2120−reifyTTNameApp t [Constant (Str n)]

2121− | t == reflm "UN" = return $ sUN n

2122−reifyTTNameApp t [n, ns]

2123− | t == reflm "NS" = do n' <- reifyTTName n

2124− ns' <- reifyTTNamespace ns

2125− return $ sNS n' ns'

2126−reifyTTNameApp t [Constant (I i), Constant (Str n)]

2127− | t == reflm "MN" = return $ sMN i n

2128−reifyTTNameApp t []

2129− | t == reflm "NErased" = return NErased

2130−reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

2131−

2132−reifyTTNamespace :: Term -> ElabD [String]

2133−reifyTTNamespace t@(App _ _ _)

2134− = case unApply t of

2135− (P _ f _, [Constant StrType])

2136− | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []

2137− (P _ f _, [Constant StrType, Constant (Str n), ns])

2138− | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)

2139− _ -> fail ("Unknown reflection namespace arg: " ++ show t)

2140−reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

2141−

2142−reifyTTNameType :: Term -> ElabD NameType

2143−reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound

2144−reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

2145−reifyTTNameType t@(App _ _ _)

2146− = case unApply t of

2147− (P _ f _, [Constant (I tag), Constant (I num)])

2148− | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!

2149− | f == reflm "TCon" -> return $ TCon tag num

2150− _ -> fail ("Unknown reflection name type: " ++ show t)

2151−reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

2152−

2153−reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)

2154−reifyTTBinder reificator binderType t@(App _ _ _)

2155− = case unApply t of

2156− (P _ f _, bt:args) | forget bt == Var binderType

2157− -> reifyTTBinderApp reificator f args

2158− _ -> fail ("Mismatching binder reflection: " ++ show t)

2159−reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)

2160−

2161−reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

2162−reifyTTBinderApp reif f [t]

2163− | f == reflm "Lam" = liftM Lam (reif t)

2164−reifyTTBinderApp reif f [t, k]

2165− | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)

2166−reifyTTBinderApp reif f [x, y]

2167− | f == reflm "Let" = liftM2 Let (reif x) (reif y)

2168−reifyTTBinderApp reif f [x, y]

2169− | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)

2170−reifyTTBinderApp reif f [t]

2171− | f == reflm "Hole" = liftM Hole (reif t)

2172−reifyTTBinderApp reif f [t]

2173− | f == reflm "GHole" = liftM (GHole 0) (reif t)

2174−reifyTTBinderApp reif f [x, y]

2175− | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

2176−reifyTTBinderApp reif f [t]

2177− | f == reflm "PVar" = liftM PVar (reif t)

2178−reifyTTBinderApp reif f [t]

2179− | f == reflm "PVTy" = liftM PVTy (reif t)

2180−reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

2181−

2182−reifyTTConst :: Term -> ElabD Const

2183−reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

2184−reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType

2185−reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

2186−reifyTTConst t@(App _ _ _)

2187− | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg

2188−reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

2189−

2190−reifyTTConstApp :: Name -> Term -> ElabD Const

2191−reifyTTConstApp f aty

2192− | f == reflm "AType" = fmap AType (reifyArithTy aty)

2193−reifyTTConstApp f (Constant c@(I _))

2194− | f == reflm "I" = return $ c

2195−reifyTTConstApp f (Constant c@(BI _))

2196− | f == reflm "BI" = return $ c

2197−reifyTTConstApp f (Constant c@(Fl _))

2198− | f == reflm "Fl" = return $ c

2199−reifyTTConstApp f (Constant c@(I _))

2200− | f == reflm "Ch" = return $ c

2201−reifyTTConstApp f (Constant c@(Str _))

2202− | f == reflm "Str" = return $ c

2203−reifyTTConstApp f (Constant c@(B8 _))

2204− | f == reflm "B8" = return $ c

2205−reifyTTConstApp f (Constant c@(B16 _))

2206− | f == reflm "B16" = return $ c

2207−reifyTTConstApp f (Constant c@(B32 _))

2208− | f == reflm "B32" = return $ c

2209−reifyTTConstApp f (Constant c@(B64 _))

2210− | f == reflm "B64" = return $ c

2211−reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

2212−

2213−reifyArithTy :: Term -> ElabD ArithTy

2214−reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

2215−reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat

2216−reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

2217−

2218−reifyNativeTy :: Term -> ElabD NativeTy

2219−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

2220−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

2221−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

2222−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

2223−reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x

2224−

2225−reifyIntTy :: Term -> ElabD IntTy

2226−reifyIntTy (App _ (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)

2227−reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative

2228−reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig

2229−reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar

2230−reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

2231−

2232−reifyTTUExp :: Term -> ElabD UExp

2233−reifyTTUExp t@(App _ _ _)

2234− = case unApply t of

2235− (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

2236− (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

2237− _ -> fail ("Unknown reflection type universe expression: " ++ show t)

2238−reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

2239−

2240−-- | Create a reflected call to a named function/constructor

2241−reflCall :: String -> [Raw] -> Raw

2242−reflCall funName args

2243− = raw_apply (Var (reflm funName)) args

2244−

2245−-- | Lift a term into its Language.Reflection.TT representation

2246−reflect :: Term -> Raw

2247−reflect = reflectTTQuote []

2248−

2249−-- | Lift a term into its Language.Reflection.Raw representation

2250−reflectRaw :: Raw -> Raw

2251−reflectRaw = reflectRawQuote []

2252−

2253−claimTT :: Name -> ElabD Name

2254−claimTT n = do n' <- getNameFrom n

2255− claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))

2256− return n'

2257−

2258−-- | Convert a reflected term to a more suitable form for pattern-matching.

2259−-- In particular, the less-interesting bits are elaborated to _ patterns. This

2260−-- happens to NameTypes, universe levels, names that are bound but not used,

2261−-- and the type annotation field of the P constructor.

2262−reflectTTQuotePattern :: [Name] -> Term -> ElabD ()

2263−reflectTTQuotePattern unq (P _ n _)

2264− | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them

2265− do fill (Var n) ; solve

2266− | otherwise =

2267− do tyannot <- claimTT (sMN 0 "pTyAnnot")

2268− movelast tyannot -- use a _ pattern here

2269− nt <- getNameFrom (sMN 0 "nt")

2270− claim nt (Var (reflm "NameType"))

2271− movelast nt -- use a _ pattern here

2272− n' <- getNameFrom (sMN 0 "n")

2273− claim n' (Var (reflm "TTName"))

2274− fill $ reflCall "P" [Var nt, Var n', Var tyannot]

2275− solve

2276− focus n'; reflectNameQuotePattern n

2277−reflectTTQuotePattern unq (V n)

2278− = do fill $ reflCall "V" [RConstant (I n)]

2279− solve

2280−reflectTTQuotePattern unq (Bind n b x)

2281− = do x' <- claimTT (sMN 0 "sc")

2282− movelast x'

2283− b' <- getNameFrom (sMN 0 "binder")

2284− claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))

2285− (Var (sNS (sUN "TT") ["Reflection", "Language"])))

2286− if n `elem` freeNames x

2287− then do fill $ reflCall "Bind"

2288− [reflectName n,

2289− Var b',

2290− Var x']

2291− solve

2292− else do any <- getNameFrom (sMN 0 "anyName")

2293− claim any (Var (reflm "TTName"))

2294− movelast any

2295− fill $ reflCall "Bind"

2296− [Var any,

2297− Var b',

2298− Var x']

2299− solve

2300− focus x'; reflectTTQuotePattern unq x

2301− focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b

2302−reflectTTQuotePattern unq (App _ f x)

2303− = do f' <- claimTT (sMN 0 "f"); movelast f'

2304− x' <- claimTT (sMN 0 "x"); movelast x'

2305− fill $ reflCall "App" [Var f', Var x']

2306− solve

2307− focus f'; reflectTTQuotePattern unq f

2308− focus x'; reflectTTQuotePattern unq x

2309−reflectTTQuotePattern unq (Constant c)

2310− = do fill $ reflCall "TConst" [reflectConstant c]

2311− solve

2312−reflectTTQuotePattern unq (Proj t i)

2313− = do t' <- claimTT (sMN 0 "t"); movelast t'

2314− fill $ reflCall "Proj" [Var t', RConstant (I i)]

2315− solve

2316− focus t'; reflectTTQuotePattern unq t

2317−reflectTTQuotePattern unq (Erased)

2318− = do erased <- claimTT (sMN 0 "erased")

2319− movelast erased

2320− fill $ (Var erased)

2321− solve

2322−reflectTTQuotePattern unq (Impossible)

2323− = do fill $ Var (reflm "Impossible")

2324− solve

2325−reflectTTQuotePattern unq (TType exp)

2326− = do ue <- getNameFrom (sMN 0 "uexp")

2327− claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))

2328− movelast ue

2329− fill $ reflCall "TType" [Var ue]

2330− solve

2331−reflectTTQuotePattern unq (UType u)

2332− = do uH <- getNameFrom (sMN 0 "someUniv")

2333− claim uH (Var (reflm "Universe"))

2334− movelast uH

2335− fill $ reflCall "UType" [Var uH]

2336− solve

2337− focus uH

2338− fill (Var (reflm (case u of

2339− NullType -> "NullType"

2340− UniqueType -> "UniqueType"

2341− AllTypes -> "AllTypes")))

2342− solve

2343−

2344−reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()

2345−reflectRawQuotePattern unq (Var n)

2346− -- the unquoted names already have types, just use them

2347− | n `elem` unq = do fill (Var n); solve

2348− | otherwise = do fill (reflCall "Var" [reflectName n]); solve

2349−reflectRawQuotePattern unq (RBind n b sc) =

2350− do scH <- getNameFrom (sMN 0 "sc")

2351− claim scH (Var (reflm "Raw"))

2352− movelast scH

2353− bH <- getNameFrom (sMN 0 "binder")

2354− claim bH (RApp (Var (reflm "Binder"))

2355− (Var (reflm "Raw")))

2356− if n `elem` freeNamesR sc

2357− then do fill $ reflCall "RBind" [reflectName n,

2358− Var bH,

2359− Var scH]

2360− solve

2361− else do any <- getNameFrom (sMN 0 "anyName")

2362− claim any (Var (reflm "TTName"))

2363− movelast any

2364− fill $ reflCall "RBind" [Var any, Var bH, Var scH]

2365− solve

2366− focus scH; reflectRawQuotePattern unq sc

2367− focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b

2368− where freeNamesR (Var n) = [n]

2369− freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,

2370− freeNamesR body \\ [n],

2371− freeNamesR t]

2372− freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++

2373− (freeNamesR body \\ [n])

2374− freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x

2375− freeNamesR RType = []

2376− freeNamesR (RUType _) = []

2377− freeNamesR (RForce r) = freeNamesR r

2378− freeNamesR (RConstant _) = []

2379−reflectRawQuotePattern unq (RApp f x) =

2380− do fH <- getNameFrom (sMN 0 "f")

2381− claim fH (Var (reflm "Raw"))

2382− movelast fH

2383− xH <- getNameFrom (sMN 0 "x")

2384− claim xH (Var (reflm "Raw"))

2385− movelast xH

2386− fill $ reflCall "RApp" [Var fH, Var xH]

2387− solve

2388− focus fH; reflectRawQuotePattern unq f

2389− focus xH; reflectRawQuotePattern unq x

2390−reflectRawQuotePattern unq RType =

2391− do fill (Var (reflm "RType"))

2392− solve

2393−reflectRawQuotePattern unq (RUType univ) =

2394− do uH <- getNameFrom (sMN 0 "universe")

2395− claim uH (Var (reflm "Universe"))

2396− movelast uH

2397− fill $ reflCall "RUType" [Var uH]

2398− solve

2399− focus uH; fill (reflectUniverse univ); solve

2400−reflectRawQuotePattern unq (RForce r) =

2401− do rH <- getNameFrom (sMN 0 "raw")

2402− claim rH (Var (reflm "Raw"))

2403− movelast rH

2404− fill $ reflCall "RForce" [Var rH]

2405− solve

2406− focus rH; reflectRawQuotePattern unq r

2407−reflectRawQuotePattern unq (RConstant c) =

2408− do cH <- getNameFrom (sMN 0 "const")

2409− claim cH (Var (reflm "Constant"))

2410− movelast cH

2411− fill (reflCall "RConstant" [Var cH]); solve

2412− focus cH

2413− fill (reflectConstant c); solve

2414−

2415−reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()

2416−reflectBinderQuotePattern q unq (Lam t)

2417− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2418− fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

2419− solve

2420− focus t'; q unq t

2421−reflectBinderQuotePattern q unq (Pi _ t k)

2422− = do t' <- claimTT (sMN 0 "ty") ; movelast t'

2423− k' <- claimTT (sMN 0 "k"); movelast k';

2424− fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

2425− solve

2426− focus t'; q unq t

2427−reflectBinderQuotePattern q unq (Let x y)

2428− = do x' <- claimTT (sMN 0 "ty"); movelast x';

2429− y' <- claimTT (sMN 0 "v"); movelast y';

2430− fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']

2431− solve

2432− focus x'; q unq x

2433− focus y'; q unq y

2434−reflectBinderQuotePattern q unq (NLet x y)

2435− = do x' <- claimTT (sMN 0 "ty"); movelast x'

2436− y' <- claimTT (sMN 0 "v"); movelast y'

2437− fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']

2438− solve

2439− focus x'; q unq x

2440− focus y'; q unq y

2441−reflectBinderQuotePattern q unq (Hole t)

2442− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2443− fill $ reflCall "Hole" [Var (reflm "TT"), Var t']

2444− solve

2445− focus t'; q unq t

2446−reflectBinderQuotePattern q unq (GHole _ t)

2447− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2448− fill $ reflCall "GHole" [Var (reflm "TT"), Var t']

2449− solve

2450− focus t'; q unq t

2451−reflectBinderQuotePattern q unq (Guess x y)

2452− = do x' <- claimTT (sMN 0 "ty"); movelast x'

2453− y' <- claimTT (sMN 0 "v"); movelast y'

2454− fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']

2455− solve

2456− focus x'; q unq x

2457− focus y'; q unq y

2458−reflectBinderQuotePattern q unq (PVar t)

2459− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2460− fill $ reflCall "PVar" [Var (reflm "TT"), Var t']

2461− solve

2462− focus t'; q unq t

2463−reflectBinderQuotePattern q unq (PVTy t)

2464− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2465− fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']

2466− solve

2467− focus t'; q unq t

2468−

2469−reflectUniverse :: Universe -> Raw

2470−reflectUniverse u =

2471− (Var (reflm (case u of

2472− NullType -> "NullType"

2473− UniqueType -> "UniqueType"

2474− AllTypes -> "AllTypes")))

2475−

2476−-- | Create a reflected TT term, but leave refs to the provided name intact

2477−reflectTTQuote :: [Name] -> Term -> Raw

2478−reflectTTQuote unq (P nt n t)

2479− | n `elem` unq = Var n

2480− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]

2481−reflectTTQuote unq (V n)

2482− = reflCall "V" [RConstant (I n)]

2483−reflectTTQuote unq (Bind n b x)

2484− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

2485−reflectTTQuote unq (App _ f x)

2486− = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2487−reflectTTQuote unq (Constant c)

2488− = reflCall "TConst" [reflectConstant c]

2489−reflectTTQuote unq (Proj t i)

2490− = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]

2491−reflectTTQuote unq (Erased) = Var (reflm "Erased")

2492−reflectTTQuote unq (Impossible) = Var (reflm "Impossible")

2493−reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

2494−reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]

2495−

2496−reflectRawQuote :: [Name] -> Raw -> Raw

2497−reflectRawQuote unq (Var n)

2498− | n `elem` unq = Var n

2499− | otherwise = reflCall "Var" [reflectName n]

2500−reflectRawQuote unq (RBind n b r) =

2501− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]

2502−reflectRawQuote unq (RApp f x) =

2503− reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2504−reflectRawQuote unq RType = Var (reflm "RType")

2505−reflectRawQuote unq (RUType u) =

2506− reflCall "RUType" [reflectUniverse u]

2507−reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]

2508−reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]

2509−

2510−reflectNameType :: NameType -> Raw

2511−reflectNameType (Bound) = Var (reflm "Bound")

2512−reflectNameType (Ref) = Var (reflm "Ref")

2513−reflectNameType (DCon x y _)

2514− = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!

2515−reflectNameType (TCon x y)

2516− = reflCall "TCon" [RConstant (I x), RConstant (I y)]

2517−

2518−reflectName :: Name -> Raw

2519−reflectName (UN s)

2520− = reflCall "UN" [RConstant (Str (str s))]

2521−reflectName (NS n ns)

2522− = reflCall "NS" [ reflectName n

2523− , foldr (\ n s ->

2524− raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )

2525− [ RConstant StrType, RConstant (Str n), s ])

2526− ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )

2527− [ RConstant StrType ])

2528− (map str ns)

2529− ]

2530−reflectName (MN i n)

2531− = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]

2532−reflectName (NErased) = Var (reflm "NErased")

2533−reflectName n = Var (reflm "NErased") -- special name, not yet implemented

2534−

2535−-- | Elaborate a name to a pattern. This means that NS and UN will be intact.

2536−-- MNs corresponding to will care about the string but not the number. All

2537−-- others become _.

2538−reflectNameQuotePattern :: Name -> ElabD ()

2539−reflectNameQuotePattern n@(UN s)

2540− = do fill $ reflectName n

2541− solve

2542−reflectNameQuotePattern n@(NS _ _)

2543− = do fill $ reflectName n

2544− solve

2545−reflectNameQuotePattern (MN _ n)

2546− = do i <- getNameFrom (sMN 0 "mnCounter")

2547− claim i (RConstant (AType (ATInt ITNative)))

2548− movelast i

2549− fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]

2550− solve

2551−reflectNameQuotePattern _ -- for all other names, match any

2552− = do nameHole <- getNameFrom (sMN 0 "name")

2553− claim nameHole (Var (reflm "TTName"))

2554− movelast nameHole

2555− fill (Var nameHole)

2556− solve

2557−

2558−reflectBinder :: Binder Term -> Raw

2559−reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

2560−

2561−reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

2562−reflectBinderQuote q ty unq (Lam t)

2563− = reflCall "Lam" [Var ty, q unq t]

2564−reflectBinderQuote q ty unq (Pi _ t k)

2565− = reflCall "Pi" [Var ty, q unq t, q unq k]

2566−reflectBinderQuote q ty unq (Let x y)

2567− = reflCall "Let" [Var ty, q unq x, q unq y]

2568−reflectBinderQuote q ty unq (NLet x y)

2569− = reflCall "NLet" [Var ty, q unq x, q unq y]

2570−reflectBinderQuote q ty unq (Hole t)

2571− = reflCall "Hole" [Var ty, q unq t]

2572−reflectBinderQuote q ty unq (GHole _ t)

2573− = reflCall "GHole" [Var ty, q unq t]

2574−reflectBinderQuote q ty unq (Guess x y)

2575− = reflCall "Guess" [Var ty, q unq x, q unq y]

2576−reflectBinderQuote q ty unq (PVar t)

2577− = reflCall "PVar" [Var ty, q unq t]

2578−reflectBinderQuote q ty unq (PVTy t)

2579− = reflCall "PVTy" [Var ty, q unq t]

2580−

2581−mkList :: Raw -> [Raw] -> Raw

2582−mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

2583−mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)

2584− x)

2585− (mkList ty xs)

2586−

2587−reflectConstant :: Const -> Raw

2588−reflectConstant c@(I _) = reflCall "I" [RConstant c]

2589−reflectConstant c@(BI _) = reflCall "BI" [RConstant c]

2590−reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]

2591−reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]

2592−reflectConstant c@(Str _) = reflCall "Str" [RConstant c]

2593−reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]

2594−reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]

2595−reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]

2596−reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]

2597−reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]

2598−reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]

2599−reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]

2600−reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]

2601−reflectConstant StrType = Var (reflm "StrType")

2602−reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]

2603−reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]

2604−reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]

2605−reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]

2606−reflectConstant VoidType = Var (reflm "VoidType")

2607−reflectConstant Forgot = Var (reflm "Forgot")

2608−reflectConstant WorldType = Var (reflm "WorldType")

2609−reflectConstant TheWorld = Var (reflm "TheWorld")

2610−

2611−reflectUExp :: UExp -> Raw

2612−reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]

2613−reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

2614−

2615−-- | Reflect the environment of a proof into a List (TTName, Binder TT)

2616−reflectEnv :: Env -> Raw

2617−reflectEnv = foldr consToEnvList emptyEnvList

2618− where

2619− consToEnvList :: (Name, Binder Term) -> Raw -> Raw

2620− consToEnvList (n, b) l

2621− = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))

2622− [ envTupleType

2623− , raw_apply (Var pairCon) [ (Var $ reflm "TTName")

2624− , (RApp (Var $ reflm "Binder")

2625− (Var $ reflm "TT"))

2626− , reflectName n

2627− , reflectBinder b

2628− ]

2629− , l

2630− ]

2631−

2632− emptyEnvList :: Raw

2633− emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))

2634− [envTupleType]

2635−

2636−-- | Reflect an error into the internal datatype of Idris -- TODO

2637−rawBool :: Bool -> Raw

2638−rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])

2639−rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])

2640−

2641−rawNil :: Raw -> Raw

2642−rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]

2643−

2644−rawCons :: Raw -> Raw -> Raw -> Raw

2645−rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]

2646−

2647−rawList :: Raw -> [Raw] -> Raw

2648−rawList ty = foldr (rawCons ty) (rawNil ty)

2649−

2650−rawPairTy :: Raw -> Raw -> Raw

2651−rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]

2652−

2653−rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

2654−rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]

2655−

2656−reflectCtxt :: [(Name, Type)] -> Raw

2657−reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))

2658− (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")

2659− (reflectName n, reflect t)))

2660− ctxt)

2661−

2662−reflectErr :: Err -> Raw

2663−reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]

2664−reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]

2665−reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =

2666− raw_apply (Var $ reflErrName "CantUnify")

2667− [ rawBool b

2668− , reflect t1

2669− , reflect t2

2670− , reflectErr e

2671− , reflectCtxt ctxt

2672− , RConstant (I i)]

2673−reflectErr (InfiniteUnify n tm ctxt) =

2674− raw_apply (Var $ reflErrName "InfiniteUnify")

2675− [ reflectName n

2676− , reflect tm

2677− , reflectCtxt ctxt

2678− ]

2679−reflectErr (CantConvert t t' ctxt) =

2680− raw_apply (Var $ reflErrName "CantConvert")

2681− [ reflect t

2682− , reflect t'

2683− , reflectCtxt ctxt

2684− ]

2685−reflectErr (CantSolveGoal t ctxt) =

2686− raw_apply (Var $ reflErrName "CantSolveGoal")

2687− [ reflect t

2688− , reflectCtxt ctxt

2689− ]

2690−reflectErr (UnifyScope n n' t ctxt) =

2691− raw_apply (Var $ reflErrName "UnifyScope")

2692− [ reflectName n

2693− , reflectName n'

2694− , reflect t

2695− , reflectCtxt ctxt

2696− ]

2697−reflectErr (CantInferType str) =

2698− raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]

2699−reflectErr (NonFunctionType t t') =

2700− raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']

2701−reflectErr (NotEquality t t') =

2702− raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']

2703−reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]

2704−reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]

2705−reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]

2706−reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]

2707−reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]

2708−reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]

2709−reflectErr (NotInjective t1 t2 t3) =

2710− raw_apply (Var $ reflErrName "NotInjective")

2711− [ reflect t1

2712− , reflect t2

2713− , reflect t3

2714− ]

2715−reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2716−reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]

2717−reflectErr (CantResolveAlts ss) =

2718− raw_apply (Var $ reflErrName "CantResolveAlts")

2719− [rawList (Var $ reflm "TTName") (map reflectName ss)]

2720−reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2721−reflectErr (NoEliminator str t)

2722− = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

2723− reflect t]

2724−reflectErr UniverseError = Var $ reflErrName "UniverseError"

2725−reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2726−reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

2727−reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

2728−reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

2729−reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]

2730−reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]

2731−reflectErr (ProviderError str) =

2732− raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

2733−reflectErr (LoadingFailed str err) =

2734− raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

2735−reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

2736−

2737−-- | Reflect a file context

2738−reflectFC :: FC -> Raw

2739−reflectFC fc = raw_apply (Var (reflm "FileLoc"))

2740− [ RConstant (Str (fc_fname fc))

2741− , raw_apply (Var pairCon) $

2742− [intTy, intTy] ++

2743− map (RConstant . I)

2744− [ fst (fc_start fc)

2745− , snd (fc_start fc)

2746− ]

2747− , raw_apply (Var pairCon) $

2748− [intTy, intTy] ++

2749− map (RConstant . I)

2750− [ fst (fc_end fc)

2751− , snd (fc_end fc)

2752− ]

2753− ]

2754− where intTy = RConstant (AType (ATInt ITNative))

2755−

27562029elaboratingArgErr :: [(Name, Name)] -> Err -> Err

27572030elaboratingArgErr [] err = err

27582031elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

@@ -2823,70 +2096,4 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

28232096 [] -> e

28242097 parts -> ReflectionError errorparts e

28252098

2826−fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

2827−fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

2828− | just == txt "Just" = Just tm

2829−fromTTMaybe x = Nothing

2830−

2831−reflErrName :: String -> Name

2832−reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

2833−

2834−-- | Attempt to reify a report part from TT to the internal

2835−-- representation. Not in Idris or ElabD monads because it should be usable

2836−-- from either.

2837−reifyReportPart :: Term -> Either Err ErrorReportPart

2838−reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

2839− Right (TextPart msg)

2840−reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

2841− | n == reflm "NamePart" =

2842− case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2843− Error e -> Left . InternalMsg $

2844− "could not reify name term " ++

2845− show ttn ++

2846− " when reflecting an error:" ++ show e

2847− OK (n', _)-> Right $ NamePart n'

2848−reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

2849− | n == reflm "TermPart" =

2850− case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of

2851− Error e -> Left . InternalMsg $

2852− "could not reify reflected term " ++

2853− show tm ++

2854− " when reflecting an error:" ++ show e

2855− OK (tm', _) -> Right $ TermPart tm'

2856−reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

2857− | n == reflm "SubReport" =

2858− case unList tm of

2859− Just xs -> do subParts <- mapM reifyReportPart xs

2860− Right (SubReport subParts)

2861− Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2862−reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2863−

2864−reifyTyDecl :: Term -> ElabD RTyDecl

2865−reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)

2866− | n == tacN "Declare" =

2867− do tyN' <- reifyTTName tyN

2868− args' <- case unList args of

2869− Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

2870− Just xs -> mapM reifyRArg xs

2871− ret' <- reifyRaw ret

2872− return $ RDeclare tyN' args' ret'

2873− where reifyRArg :: Term -> ElabD RArg

2874− reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)

2875− | n == tacN "Explicit" = liftM2 RExplicit

2876− (reifyTTName argN)

2877− (reifyRaw argTy)

2878− | n == tacN "Implicit" = liftM2 RImplicit

2879− (reifyTTName argN)

2880− (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint

2881− (reifyTTName argN)

2882− (reifyRaw argTy)

2883− reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

2884−reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

2885−

2886−envTupleType :: Raw

2887−envTupleType

2888− = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

2889− , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))

2890− ]

2891−

28922099solveAll = try (do solve; solveAll) (return ())

src/Idris/ElabQuasiquote.hs+2−2

@@ -170,8 +170,8 @@ extractUnquotes n (PUnquote tm)

170170 return (PRef (fileFC "(unquote)") n, [(n, tm)])

171171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $

172172 extractUnquotes (n-1) tm

173−extractUnquotes n (PRunTactics fc tm)

174− = fmap (\(tm', ex) -> (PRunTactics fc tm', ex)) $ extractUnquotes n tm

173+extractUnquotes n (PRunElab fc tm)

174+ = fmap (\(tm', ex) -> (PRunElab fc tm', ex)) $ extractUnquotes n tm

175175extractUnquotes n x = return (x, []) -- no subterms!

176176

177177

src/Idris/Error.hs+1−1

@@ -148,4 +148,4 @@ warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>

148148warnDisamb ist (PUnquote tm) = warnDisamb ist tm

149149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm

150150warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm

151−warnDisamb ist (PRunTactics _ tm) = warnDisamb ist tm

151+warnDisamb ist (PRunElab _ tm) = warnDisamb ist tm

src/Idris/IBC.hs+4−4

@@ -1674,9 +1674,9 @@ instance Binary PTerm where

16741674 put x2

16751675 PUniverse x1 -> do putWord8 38

16761676 put x1

1677− PRunTactics x1 x2 -> do putWord8 39

1678− put x1

1679− put x2

1677+ PRunElab x1 x2 -> do putWord8 39

1678+ put x1

1679+ put x2

16801680 PAs x1 x2 x3 -> do putWord8 40

16811681 put x1

16821682 put x2

@@ -1809,7 +1809,7 @@ instance Binary PTerm where

18091809 return (PUniverse x1)

18101810 39 -> do x1 <- get

18111811 x2 <- get

1812− return (PRunTactics x1 x2)

1812+ return (PRunElab x1 x2)

18131813 40 -> do x1 <- get

18141814 x2 <- get

18151815 x3 <- get

src/Idris/IdrisDoc.hs+1−1

@@ -321,7 +321,7 @@ extractPTermNames (PCoerced p) = extract p

321321extractPTermNames (PDisamb _ p) = extract p

322322extractPTermNames (PUnifyLog p) = extract p

323323extractPTermNames (PNoImplicits p) = extract p

324−extractPTermNames (PRunTactics _ p) = extract p

324+extractPTermNames (PRunElab _ p) = extract p

325325extractPTermNames _ = []

326326

327327-- | Shorter name for extractPTermNames

src/Idris/ParseExpr.hs+9−9

@@ -220,7 +220,7 @@ InternalExpr ::=

220220internalExpr :: SyntaxInfo -> IdrisParser PTerm

221221internalExpr syn =

222222 unifyLog syn

223− <|> runTactics syn

223+ <|> runElab syn

224224 <|> disamb syn

225225 <|> noImplicits syn

226226 <|> recordType syn

@@ -497,16 +497,16 @@ unifyLog syn = do try (lchar '%' *> reserved "unifyLog")

497497

498498{- | Parses a new-style tactics expression

499499RunTactics ::=

500− '%' 'runTactics' SimpleExpr

500+ '%' 'runElab' SimpleExpr

501501 ;

502502-}

503−runTactics :: SyntaxInfo -> IdrisParser PTerm

504−runTactics syn = do try (lchar '%' *> reserved "runTactics")

505− fc <- getFC

506− tm <- simpleExpr syn

507− i <- get

508− return $ PRunTactics fc tm

509− <?> "new-style tactics expression"

503+runElab :: SyntaxInfo -> IdrisParser PTerm

504+runElab syn = do try (lchar '%' *> reserved "runElab")

505+ fc <- getFC

506+ tm <- simpleExpr syn

507+ i <- get

508+ return $ PRunElab fc tm

509+ <?> "new-style tactics expression"

510510

511511{- | Parses a disambiguation expression

512512Disamb ::=

src/Idris/Reflection.hs+883−3

@@ -1,10 +1,22 @@

1−{-|

2−Handy tools for doing reflection.

1+{-| Code related to Idris's reflection system. This module contains

2+quoters and unquoters along with some supporting datatypes.

33-}

4+{-# LANGUAGE PatternGuards #-}

5+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

46module Idris.Reflection where

8+import Control.Monad (liftM, liftM2)

9+import Data.List ((\\))

10+import qualified Data.Text as T

11+

12+import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,

13+ movelast, runElab, solve)

14+import Idris.Core.Evaluate (initContext)

615import Idris.Core.TT

7−import Idris.AbsSyntaxTree (PArg'(..), PArg, PTerm(Placeholder))

16+

17+import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),

18+ PTerm(..), initEState, pairCon, pairTy)

19+import Idris.Delaborate (delab)

820

921data RArg = RExplicit { argName :: Name, argTy :: Raw }

1022 | RImplicit { argName :: Name, argTy :: Raw }

@@ -16,3 +28,871 @@ rArgToPArg :: RArg -> PArg

1628rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

1729rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder

1830rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder

31+

32+data RFunClause = RMkFunClause Raw Raw

33+ | RMkImpossibleClause Raw

34+ deriving Show

35+

36+data RFunDefn = RDefineFun Name [RFunClause] deriving Show

37+

38+-- | Prefix a name with the "Language.Reflection" namespace

39+reflm :: String -> Name

40+reflm n = sNS (sUN n) ["Reflection", "Language"]

41+

42+-- | Prefix a name with the "Language.Reflection.Elab" namespace

43+tacN :: String -> Name

44+tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]

45+

46+-- | Reify tactics from their reflected representation

47+reify :: IState -> Term -> ElabD PTactic

48+reify _ (P _ n _) | n == reflm "Intros" = return Intros

49+reify _ (P _ n _) | n == reflm "Trivial" = return Trivial

50+reify _ (P _ n _) | n == reflm "Instance" = return TCInstance

51+reify _ (P _ n _) | n == reflm "Solve" = return Solve

52+reify _ (P _ n _) | n == reflm "Compute" = return Compute

53+reify _ (P _ n _) | n == reflm "Skip" = return Skip

54+reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC

55+reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus

56+reify ist t@(App _ _ _)

57+ | (P _ f _, args) <- unApply t = reifyApp ist f args

58+reify _ t = fail ("Unknown tactic " ++ show t)

59+

60+reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

61+reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)

62+reifyApp _ t [Constant (I i)]

63+ | t == reflm "Search" = return (ProofSearch True True i Nothing [])

64+reifyApp _ t [x]

65+ | t == reflm "Refine" = do n <- reifyTTName x

66+ return $ Refine n []

67+reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n

68+ goal <- reifyTT ty

69+ return $ Claim n' (delab ist goal)

70+reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)

71+reifyApp ist t [Constant (Str n), x]

72+ | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

73+reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)

74+reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')

75+reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')

76+reifyApp ist t [t']

77+ | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

78+reifyApp ist t [t']

79+ | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')

80+reifyApp ist t [t']

81+ | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')

82+reifyApp _ t [t']

83+ | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')

84+reifyApp ist t [t']

85+ | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')

86+reifyApp ist t [x]

87+ | t == reflm "Focus" = liftM Focus (reifyTTName x)

88+reifyApp ist t [t']

89+ | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')

90+reifyApp ist t [n, t']

91+ | t == reflm "LetTac" = do n' <- reifyTTName n

92+ t'' <- reifyTT t'

93+ return $ LetTac n' (delab ist t')

94+reifyApp ist t [n, tt', t']

95+ | t == reflm "LetTacTy" = do n' <- reifyTTName n

96+ tt'' <- reifyTT tt'

97+ t'' <- reifyTT t'

98+ return $ LetTacTy n' (delab ist tt'') (delab ist t'')

99+reifyApp ist t [errs]

100+ | t == reflm "Fail" = fmap TFail (reifyReportParts errs)

101+reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

102+

103+reifyReportParts :: Term -> ElabD [ErrorReportPart]

104+reifyReportParts errs =

105+ case unList errs of

106+ Nothing -> fail "Failed to reify errors"

107+ Just errs' ->

108+ let parts = mapM reifyReportPart errs' in

109+ case parts of

110+ Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err

111+ Right errs'' ->

112+ return errs''

113+

114+-- | Reify terms from their reflected representation

115+reifyTT :: Term -> ElabD Term

116+reifyTT t@(App _ _ _)

117+ | (P _ f _, args) <- unApply t = reifyTTApp f args

118+reifyTT t@(P _ n _)

119+ | n == reflm "Erased" = return $ Erased

120+reifyTT t@(P _ n _)

121+ | n == reflm "Impossible" = return $ Impossible

122+reifyTT t = fail ("Unknown reflection term: " ++ show t)

123+

124+reifyTTApp :: Name -> [Term] -> ElabD Term

125+reifyTTApp t [nt, n, x]

126+ | t == reflm "P" = do nt' <- reifyTTNameType nt

127+ n' <- reifyTTName n

128+ x' <- reifyTT x

129+ return $ P nt' n' x'

130+reifyTTApp t [Constant (I i)]

131+ | t == reflm "V" = return $ V i

132+reifyTTApp t [n, b, x]

133+ | t == reflm "Bind" = do n' <- reifyTTName n

134+ b' <- reifyTTBinder reifyTT (reflm "TT") b

135+ x' <- reifyTT x

136+ return $ Bind n' b' x'

137+reifyTTApp t [f, x]

138+ | t == reflm "App" = do f' <- reifyTT f

139+ x' <- reifyTT x

140+ return $ App Complete f' x'

141+reifyTTApp t [c]

142+ | t == reflm "TConst" = liftM Constant (reifyTTConst c)

143+reifyTTApp t [t', Constant (I i)]

144+ | t == reflm "Proj" = do t'' <- reifyTT t'

145+ return $ Proj t'' i

146+reifyTTApp t [tt]

147+ | t == reflm "TType" = liftM TType (reifyTTUExp tt)

148+reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

149+

150+-- | Reify raw terms from their reflected representation

151+reifyRaw :: Term -> ElabD Raw

152+reifyRaw t@(App _ _ _)

153+ | (P _ f _, args) <- unApply t = reifyRawApp f args

154+reifyRaw t@(P _ n _)

155+ | n == reflm "RType" = return $ RType

156+reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)

157+

158+reifyRawApp :: Name -> [Term] -> ElabD Raw

159+reifyRawApp t [n]

160+ | t == reflm "Var" = liftM Var (reifyTTName n)

161+reifyRawApp t [n, b, x]

162+ | t == reflm "RBind" = do n' <- reifyTTName n

163+ b' <- reifyTTBinder reifyRaw (reflm "Raw") b

164+ x' <- reifyRaw x

165+ return $ RBind n' b' x'

166+reifyRawApp t [f, x]

167+ | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)

168+reifyRawApp t [t']

169+ | t == reflm "RForce" = liftM RForce (reifyRaw t')

170+reifyRawApp t [c]

171+ | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)

172+reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))

173+

174+reifyTTName :: Term -> ElabD Name

175+reifyTTName t

176+ | (P _ f _, args) <- unApply t = reifyTTNameApp f args

177+reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

178+

179+reifyTTNameApp :: Name -> [Term] -> ElabD Name

180+reifyTTNameApp t [Constant (Str n)]

181+ | t == reflm "UN" = return $ sUN n

182+reifyTTNameApp t [n, ns]

183+ | t == reflm "NS" = do n' <- reifyTTName n

184+ ns' <- reifyTTNamespace ns

185+ return $ sNS n' ns'

186+reifyTTNameApp t [Constant (I i), Constant (Str n)]

187+ | t == reflm "MN" = return $ sMN i n

188+reifyTTNameApp t []

189+ | t == reflm "NErased" = return NErased

190+reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

191+

192+reifyTTNamespace :: Term -> ElabD [String]

193+reifyTTNamespace t@(App _ _ _)

194+ = case unApply t of

195+ (P _ f _, [Constant StrType])

196+ | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []

197+ (P _ f _, [Constant StrType, Constant (Str n), ns])

198+ | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)

199+ _ -> fail ("Unknown reflection namespace arg: " ++ show t)

200+reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

201+

202+reifyTTNameType :: Term -> ElabD NameType

203+reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound

204+reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

205+reifyTTNameType t@(App _ _ _)

206+ = case unApply t of

207+ (P _ f _, [Constant (I tag), Constant (I num)])

208+ | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!

209+ | f == reflm "TCon" -> return $ TCon tag num

210+ _ -> fail ("Unknown reflection name type: " ++ show t)

211+reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

212+

213+reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)

214+reifyTTBinder reificator binderType t@(App _ _ _)

215+ = case unApply t of

216+ (P _ f _, bt:args) | forget bt == Var binderType

217+ -> reifyTTBinderApp reificator f args

218+ _ -> fail ("Mismatching binder reflection: " ++ show t)

219+reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)

220+

221+reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

222+reifyTTBinderApp reif f [t]

223+ | f == reflm "Lam" = liftM Lam (reif t)

224+reifyTTBinderApp reif f [t, k]

225+ | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)

226+reifyTTBinderApp reif f [x, y]

227+ | f == reflm "Let" = liftM2 Let (reif x) (reif y)

228+reifyTTBinderApp reif f [x, y]

229+ | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)

230+reifyTTBinderApp reif f [t]

231+ | f == reflm "Hole" = liftM Hole (reif t)

232+reifyTTBinderApp reif f [t]

233+ | f == reflm "GHole" = liftM (GHole 0) (reif t)

234+reifyTTBinderApp reif f [x, y]

235+ | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

236+reifyTTBinderApp reif f [t]

237+ | f == reflm "PVar" = liftM PVar (reif t)

238+reifyTTBinderApp reif f [t]

239+ | f == reflm "PVTy" = liftM PVTy (reif t)

240+reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

241+

242+reifyTTConst :: Term -> ElabD Const

243+reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

244+reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType

245+reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

246+reifyTTConst t@(App _ _ _)

247+ | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg

248+reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

249+

250+reifyTTConstApp :: Name -> Term -> ElabD Const

251+reifyTTConstApp f aty

252+ | f == reflm "AType" = fmap AType (reifyArithTy aty)

253+reifyTTConstApp f (Constant c@(I _))

254+ | f == reflm "I" = return $ c

255+reifyTTConstApp f (Constant c@(BI _))

256+ | f == reflm "BI" = return $ c

257+reifyTTConstApp f (Constant c@(Fl _))

258+ | f == reflm "Fl" = return $ c

259+reifyTTConstApp f (Constant c@(I _))

260+ | f == reflm "Ch" = return $ c

261+reifyTTConstApp f (Constant c@(Str _))

262+ | f == reflm "Str" = return $ c

263+reifyTTConstApp f (Constant c@(B8 _))

264+ | f == reflm "B8" = return $ c

265+reifyTTConstApp f (Constant c@(B16 _))

266+ | f == reflm "B16" = return $ c

267+reifyTTConstApp f (Constant c@(B32 _))

268+ | f == reflm "B32" = return $ c

269+reifyTTConstApp f (Constant c@(B64 _))

270+ | f == reflm "B64" = return $ c

271+reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

272+

273+reifyArithTy :: Term -> ElabD ArithTy

274+reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

275+reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat

276+reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

277+

278+reifyNativeTy :: Term -> ElabD NativeTy

279+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

280+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

281+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

282+reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

283+reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x

284+

285+reifyIntTy :: Term -> ElabD IntTy

286+reifyIntTy (App _ (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)

287+reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative

288+reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig

289+reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar

290+reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

291+

292+reifyTTUExp :: Term -> ElabD UExp

293+reifyTTUExp t@(App _ _ _)

294+ = case unApply t of

295+ (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

296+ (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

297+ _ -> fail ("Unknown reflection type universe expression: " ++ show t)

298+reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

299+

300+-- | Create a reflected call to a named function/constructor

301+reflCall :: String -> [Raw] -> Raw

302+reflCall funName args

303+ = raw_apply (Var (reflm funName)) args

304+

305+-- | Lift a term into its Language.Reflection.TT representation

306+reflect :: Term -> Raw

307+reflect = reflectTTQuote []

308+

309+-- | Lift a term into its Language.Reflection.Raw representation

310+reflectRaw :: Raw -> Raw

311+reflectRaw = reflectRawQuote []

312+

313+claimTT :: Name -> ElabD Name

314+claimTT n = do n' <- getNameFrom n

315+ claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))

316+ return n'

317+

318+-- | Convert a reflected term to a more suitable form for pattern-matching.

319+-- In particular, the less-interesting bits are elaborated to _ patterns. This

320+-- happens to NameTypes, universe levels, names that are bound but not used,

321+-- and the type annotation field of the P constructor.

322+reflectTTQuotePattern :: [Name] -> Term -> ElabD ()

323+reflectTTQuotePattern unq (P _ n _)

324+ | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them

325+ do fill (Var n) ; solve

326+ | otherwise =

327+ do tyannot <- claimTT (sMN 0 "pTyAnnot")

328+ movelast tyannot -- use a _ pattern here

329+ nt <- getNameFrom (sMN 0 "nt")

330+ claim nt (Var (reflm "NameType"))

331+ movelast nt -- use a _ pattern here

332+ n' <- getNameFrom (sMN 0 "n")

333+ claim n' (Var (reflm "TTName"))

334+ fill $ reflCall "P" [Var nt, Var n', Var tyannot]

335+ solve

336+ focus n'; reflectNameQuotePattern n

337+reflectTTQuotePattern unq (V n)

338+ = do fill $ reflCall "V" [RConstant (I n)]

339+ solve

340+reflectTTQuotePattern unq (Bind n b x)

341+ = do x' <- claimTT (sMN 0 "sc")

342+ movelast x'

343+ b' <- getNameFrom (sMN 0 "binder")

344+ claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))

345+ (Var (sNS (sUN "TT") ["Reflection", "Language"])))

346+ if n `elem` freeNames x

347+ then do fill $ reflCall "Bind"

348+ [reflectName n,

349+ Var b',

350+ Var x']

351+ solve

352+ else do any <- getNameFrom (sMN 0 "anyName")

353+ claim any (Var (reflm "TTName"))

354+ movelast any

355+ fill $ reflCall "Bind"

356+ [Var any,

357+ Var b',

358+ Var x']

359+ solve

360+ focus x'; reflectTTQuotePattern unq x

361+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b

362+reflectTTQuotePattern unq (App _ f x)

363+ = do f' <- claimTT (sMN 0 "f"); movelast f'

364+ x' <- claimTT (sMN 0 "x"); movelast x'

365+ fill $ reflCall "App" [Var f', Var x']

366+ solve

367+ focus f'; reflectTTQuotePattern unq f

368+ focus x'; reflectTTQuotePattern unq x

369+reflectTTQuotePattern unq (Constant c)

370+ = do fill $ reflCall "TConst" [reflectConstant c]

371+ solve

372+reflectTTQuotePattern unq (Proj t i)

373+ = do t' <- claimTT (sMN 0 "t"); movelast t'

374+ fill $ reflCall "Proj" [Var t', RConstant (I i)]

375+ solve

376+ focus t'; reflectTTQuotePattern unq t

377+reflectTTQuotePattern unq (Erased)

378+ = do erased <- claimTT (sMN 0 "erased")

379+ movelast erased

380+ fill $ (Var erased)

381+ solve

382+reflectTTQuotePattern unq (Impossible)

383+ = do fill $ Var (reflm "Impossible")

384+ solve

385+reflectTTQuotePattern unq (TType exp)

386+ = do ue <- getNameFrom (sMN 0 "uexp")

387+ claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))

388+ movelast ue

389+ fill $ reflCall "TType" [Var ue]

390+ solve

391+reflectTTQuotePattern unq (UType u)

392+ = do uH <- getNameFrom (sMN 0 "someUniv")

393+ claim uH (Var (reflm "Universe"))

394+ movelast uH

395+ fill $ reflCall "UType" [Var uH]

396+ solve

397+ focus uH

398+ fill (Var (reflm (case u of

399+ NullType -> "NullType"

400+ UniqueType -> "UniqueType"

401+ AllTypes -> "AllTypes")))

402+ solve

403+

404+reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()

405+reflectRawQuotePattern unq (Var n)

406+ -- the unquoted names already have types, just use them

407+ | n `elem` unq = do fill (Var n); solve

408+ | otherwise = do fill (reflCall "Var" [reflectName n]); solve

409+reflectRawQuotePattern unq (RBind n b sc) =

410+ do scH <- getNameFrom (sMN 0 "sc")

411+ claim scH (Var (reflm "Raw"))

412+ movelast scH

413+ bH <- getNameFrom (sMN 0 "binder")

414+ claim bH (RApp (Var (reflm "Binder"))

415+ (Var (reflm "Raw")))

416+ if n `elem` freeNamesR sc

417+ then do fill $ reflCall "RBind" [reflectName n,

418+ Var bH,

419+ Var scH]

420+ solve

421+ else do any <- getNameFrom (sMN 0 "anyName")

422+ claim any (Var (reflm "TTName"))

423+ movelast any

424+ fill $ reflCall "RBind" [Var any, Var bH, Var scH]

425+ solve

426+ focus scH; reflectRawQuotePattern unq sc

427+ focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b

428+ where freeNamesR (Var n) = [n]

429+ freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,

430+ freeNamesR body \\ [n],

431+ freeNamesR t]

432+ freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++

433+ (freeNamesR body \\ [n])

434+ freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x

435+ freeNamesR RType = []

436+ freeNamesR (RUType _) = []

437+ freeNamesR (RForce r) = freeNamesR r

438+ freeNamesR (RConstant _) = []

439+reflectRawQuotePattern unq (RApp f x) =

440+ do fH <- getNameFrom (sMN 0 "f")

441+ claim fH (Var (reflm "Raw"))

442+ movelast fH

443+ xH <- getNameFrom (sMN 0 "x")

444+ claim xH (Var (reflm "Raw"))

445+ movelast xH

446+ fill $ reflCall "RApp" [Var fH, Var xH]

447+ solve

448+ focus fH; reflectRawQuotePattern unq f

449+ focus xH; reflectRawQuotePattern unq x

450+reflectRawQuotePattern unq RType =

451+ do fill (Var (reflm "RType"))

452+ solve

453+reflectRawQuotePattern unq (RUType univ) =

454+ do uH <- getNameFrom (sMN 0 "universe")

455+ claim uH (Var (reflm "Universe"))

456+ movelast uH

457+ fill $ reflCall "RUType" [Var uH]

458+ solve

459+ focus uH; fill (reflectUniverse univ); solve

460+reflectRawQuotePattern unq (RForce r) =

461+ do rH <- getNameFrom (sMN 0 "raw")

462+ claim rH (Var (reflm "Raw"))

463+ movelast rH

464+ fill $ reflCall "RForce" [Var rH]

465+ solve

466+ focus rH; reflectRawQuotePattern unq r

467+reflectRawQuotePattern unq (RConstant c) =

468+ do cH <- getNameFrom (sMN 0 "const")

469+ claim cH (Var (reflm "Constant"))

470+ movelast cH

471+ fill (reflCall "RConstant" [Var cH]); solve

472+ focus cH

473+ fill (reflectConstant c); solve

474+

475+reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()

476+reflectBinderQuotePattern q unq (Lam t)

477+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

478+ fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

479+ solve

480+ focus t'; q unq t

481+reflectBinderQuotePattern q unq (Pi _ t k)

482+ = do t' <- claimTT (sMN 0 "ty") ; movelast t'

483+ k' <- claimTT (sMN 0 "k"); movelast k';

484+ fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

485+ solve

486+ focus t'; q unq t

487+reflectBinderQuotePattern q unq (Let x y)

488+ = do x' <- claimTT (sMN 0 "ty"); movelast x';

489+ y' <- claimTT (sMN 0 "v"); movelast y';

490+ fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']

491+ solve

492+ focus x'; q unq x

493+ focus y'; q unq y

494+reflectBinderQuotePattern q unq (NLet x y)

495+ = do x' <- claimTT (sMN 0 "ty"); movelast x'

496+ y' <- claimTT (sMN 0 "v"); movelast y'

497+ fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']

498+ solve

499+ focus x'; q unq x

500+ focus y'; q unq y

501+reflectBinderQuotePattern q unq (Hole t)

502+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

503+ fill $ reflCall "Hole" [Var (reflm "TT"), Var t']

504+ solve

505+ focus t'; q unq t

506+reflectBinderQuotePattern q unq (GHole _ t)

507+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

508+ fill $ reflCall "GHole" [Var (reflm "TT"), Var t']

509+ solve

510+ focus t'; q unq t

511+reflectBinderQuotePattern q unq (Guess x y)

512+ = do x' <- claimTT (sMN 0 "ty"); movelast x'

513+ y' <- claimTT (sMN 0 "v"); movelast y'

514+ fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']

515+ solve

516+ focus x'; q unq x

517+ focus y'; q unq y

518+reflectBinderQuotePattern q unq (PVar t)

519+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

520+ fill $ reflCall "PVar" [Var (reflm "TT"), Var t']

521+ solve

522+ focus t'; q unq t

523+reflectBinderQuotePattern q unq (PVTy t)

524+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

525+ fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']

526+ solve

527+ focus t'; q unq t

528+

529+reflectUniverse :: Universe -> Raw

530+reflectUniverse u =

531+ (Var (reflm (case u of

532+ NullType -> "NullType"

533+ UniqueType -> "UniqueType"

534+ AllTypes -> "AllTypes")))

535+

536+-- | Create a reflected TT term, but leave refs to the provided name intact

537+reflectTTQuote :: [Name] -> Term -> Raw

538+reflectTTQuote unq (P nt n t)

539+ | n `elem` unq = Var n

540+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]

541+reflectTTQuote unq (V n)

542+ = reflCall "V" [RConstant (I n)]

543+reflectTTQuote unq (Bind n b x)

544+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

545+reflectTTQuote unq (App _ f x)

546+ = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

547+reflectTTQuote unq (Constant c)

548+ = reflCall "TConst" [reflectConstant c]

549+reflectTTQuote unq (Proj t i)

550+ = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]

551+reflectTTQuote unq (Erased) = Var (reflm "Erased")

552+reflectTTQuote unq (Impossible) = Var (reflm "Impossible")

553+reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

554+reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]

555+

556+reflectRawQuote :: [Name] -> Raw -> Raw

557+reflectRawQuote unq (Var n)

558+ | n `elem` unq = Var n

559+ | otherwise = reflCall "Var" [reflectName n]

560+reflectRawQuote unq (RBind n b r) =

561+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]

562+reflectRawQuote unq (RApp f x) =

563+ reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

564+reflectRawQuote unq RType = Var (reflm "RType")

565+reflectRawQuote unq (RUType u) =

566+ reflCall "RUType" [reflectUniverse u]

567+reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]

568+reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]

569+

570+reflectNameType :: NameType -> Raw

571+reflectNameType (Bound) = Var (reflm "Bound")

572+reflectNameType (Ref) = Var (reflm "Ref")

573+reflectNameType (DCon x y _)

574+ = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!

575+reflectNameType (TCon x y)

576+ = reflCall "TCon" [RConstant (I x), RConstant (I y)]

577+

578+reflectName :: Name -> Raw

579+reflectName (UN s)

580+ = reflCall "UN" [RConstant (Str (str s))]

581+reflectName (NS n ns)

582+ = reflCall "NS" [ reflectName n

583+ , foldr (\ n s ->

584+ raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )

585+ [ RConstant StrType, RConstant (Str n), s ])

586+ ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )

587+ [ RConstant StrType ])

588+ (map str ns)

589+ ]

590+reflectName (MN i n)

591+ = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]

592+reflectName (NErased) = Var (reflm "NErased")

593+reflectName n = Var (reflm "NErased") -- special name, not yet implemented

594+

595+-- | Elaborate a name to a pattern. This means that NS and UN will be intact.

596+-- MNs corresponding to will care about the string but not the number. All

597+-- others become _.

598+reflectNameQuotePattern :: Name -> ElabD ()

599+reflectNameQuotePattern n@(UN s)

600+ = do fill $ reflectName n

601+ solve

602+reflectNameQuotePattern n@(NS _ _)

603+ = do fill $ reflectName n

604+ solve

605+reflectNameQuotePattern (MN _ n)

606+ = do i <- getNameFrom (sMN 0 "mnCounter")

607+ claim i (RConstant (AType (ATInt ITNative)))

608+ movelast i

609+ fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]

610+ solve

611+reflectNameQuotePattern _ -- for all other names, match any

612+ = do nameHole <- getNameFrom (sMN 0 "name")

613+ claim nameHole (Var (reflm "TTName"))

614+ movelast nameHole

615+ fill (Var nameHole)

616+ solve

617+

618+reflectBinder :: Binder Term -> Raw

619+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

620+

621+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

622+reflectBinderQuote q ty unq (Lam t)

623+ = reflCall "Lam" [Var ty, q unq t]

624+reflectBinderQuote q ty unq (Pi _ t k)

625+ = reflCall "Pi" [Var ty, q unq t, q unq k]

626+reflectBinderQuote q ty unq (Let x y)

627+ = reflCall "Let" [Var ty, q unq x, q unq y]

628+reflectBinderQuote q ty unq (NLet x y)

629+ = reflCall "NLet" [Var ty, q unq x, q unq y]

630+reflectBinderQuote q ty unq (Hole t)

631+ = reflCall "Hole" [Var ty, q unq t]

632+reflectBinderQuote q ty unq (GHole _ t)

633+ = reflCall "GHole" [Var ty, q unq t]

634+reflectBinderQuote q ty unq (Guess x y)

635+ = reflCall "Guess" [Var ty, q unq x, q unq y]

636+reflectBinderQuote q ty unq (PVar t)

637+ = reflCall "PVar" [Var ty, q unq t]

638+reflectBinderQuote q ty unq (PVTy t)

639+ = reflCall "PVTy" [Var ty, q unq t]

640+

641+mkList :: Raw -> [Raw] -> Raw

642+mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

643+mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)

644+ x)

645+ (mkList ty xs)

646+

647+reflectConstant :: Const -> Raw

648+reflectConstant c@(I _) = reflCall "I" [RConstant c]

649+reflectConstant c@(BI _) = reflCall "BI" [RConstant c]

650+reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]

651+reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]

652+reflectConstant c@(Str _) = reflCall "Str" [RConstant c]

653+reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]

654+reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]

655+reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]

656+reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]

657+reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]

658+reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]

659+reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]

660+reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]

661+reflectConstant StrType = Var (reflm "StrType")

662+reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]

663+reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]

664+reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]

665+reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]

666+reflectConstant VoidType = Var (reflm "VoidType")

667+reflectConstant Forgot = Var (reflm "Forgot")

668+reflectConstant WorldType = Var (reflm "WorldType")

669+reflectConstant TheWorld = Var (reflm "TheWorld")

670+

671+reflectUExp :: UExp -> Raw

672+reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]

673+reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

674+

675+-- | Reflect the environment of a proof into a List (TTName, Binder TT)

676+reflectEnv :: Env -> Raw

677+reflectEnv = foldr consToEnvList emptyEnvList

678+ where

679+ consToEnvList :: (Name, Binder Term) -> Raw -> Raw

680+ consToEnvList (n, b) l

681+ = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))

682+ [ envTupleType

683+ , raw_apply (Var pairCon) [ (Var $ reflm "TTName")

684+ , (RApp (Var $ reflm "Binder")

685+ (Var $ reflm "TT"))

686+ , reflectName n

687+ , reflectBinder b

688+ ]

689+ , l

690+ ]

691+

692+ emptyEnvList :: Raw

693+ emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))

694+ [envTupleType]

695+

696+-- | Reflect an error into the internal datatype of Idris -- TODO

697+rawBool :: Bool -> Raw

698+rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])

699+rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])

700+

701+rawNil :: Raw -> Raw

702+rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]

703+

704+rawCons :: Raw -> Raw -> Raw -> Raw

705+rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]

706+

707+rawList :: Raw -> [Raw] -> Raw

708+rawList ty = foldr (rawCons ty) (rawNil ty)

709+

710+rawPairTy :: Raw -> Raw -> Raw

711+rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]

712+

713+rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

714+rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]

715+

716+reflectCtxt :: [(Name, Type)] -> Raw

717+reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))

718+ (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")

719+ (reflectName n, reflect t)))

720+ ctxt)

721+

722+reflectErr :: Err -> Raw

723+reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]

724+reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]

725+reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =

726+ raw_apply (Var $ reflErrName "CantUnify")

727+ [ rawBool b

728+ , reflect t1

729+ , reflect t2

730+ , reflectErr e

731+ , reflectCtxt ctxt

732+ , RConstant (I i)]

733+reflectErr (InfiniteUnify n tm ctxt) =

734+ raw_apply (Var $ reflErrName "InfiniteUnify")

735+ [ reflectName n

736+ , reflect tm

737+ , reflectCtxt ctxt

738+ ]

739+reflectErr (CantConvert t t' ctxt) =

740+ raw_apply (Var $ reflErrName "CantConvert")

741+ [ reflect t

742+ , reflect t'

743+ , reflectCtxt ctxt

744+ ]

745+reflectErr (CantSolveGoal t ctxt) =

746+ raw_apply (Var $ reflErrName "CantSolveGoal")

747+ [ reflect t

748+ , reflectCtxt ctxt

749+ ]

750+reflectErr (UnifyScope n n' t ctxt) =

751+ raw_apply (Var $ reflErrName "UnifyScope")

752+ [ reflectName n

753+ , reflectName n'

754+ , reflect t

755+ , reflectCtxt ctxt

756+ ]

757+reflectErr (CantInferType str) =

758+ raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]

759+reflectErr (NonFunctionType t t') =

760+ raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']

761+reflectErr (NotEquality t t') =

762+ raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']

763+reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]

764+reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]

765+reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]

766+reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]

767+reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]

768+reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]

769+reflectErr (NotInjective t1 t2 t3) =

770+ raw_apply (Var $ reflErrName "NotInjective")

771+ [ reflect t1

772+ , reflect t2

773+ , reflect t3

774+ ]

775+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

776+reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]

777+reflectErr (CantResolveAlts ss) =

778+ raw_apply (Var $ reflErrName "CantResolveAlts")

779+ [rawList (Var $ reflm "TTName") (map reflectName ss)]

780+reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

781+reflectErr (NoEliminator str t)

782+ = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

783+ reflect t]

784+reflectErr UniverseError = Var $ reflErrName "UniverseError"

785+reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

786+reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

787+reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

788+reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

789+reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]

790+reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]

791+reflectErr (ProviderError str) =

792+ raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

793+reflectErr (LoadingFailed str err) =

794+ raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

795+reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

796+

797+-- | Reflect a file context

798+reflectFC :: FC -> Raw

799+reflectFC fc = raw_apply (Var (reflm "FileLoc"))

800+ [ RConstant (Str (fc_fname fc))

801+ , raw_apply (Var pairCon) $

802+ [intTy, intTy] ++

803+ map (RConstant . I)

804+ [ fst (fc_start fc)

805+ , snd (fc_start fc)

806+ ]

807+ , raw_apply (Var pairCon) $

808+ [intTy, intTy] ++

809+ map (RConstant . I)

810+ [ fst (fc_end fc)

811+ , snd (fc_end fc)

812+ ]

813+ ]

814+ where intTy = RConstant (AType (ATInt ITNative))

815+

816+fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

817+fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

818+ | just == txt "Just" = Just tm

819+fromTTMaybe x = Nothing

820+

821+reflErrName :: String -> Name

822+reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

823+

824+-- | Attempt to reify a report part from TT to the internal

825+-- representation. Not in Idris or ElabD monads because it should be usable

826+-- from either.

827+reifyReportPart :: Term -> Either Err ErrorReportPart

828+reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

829+ Right (TextPart msg)

830+reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

831+ | n == reflm "NamePart" =

832+ case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of

833+ Error e -> Left . InternalMsg $

834+ "could not reify name term " ++

835+ show ttn ++

836+ " when reflecting an error:" ++ show e

837+ OK (n', _)-> Right $ NamePart n'

838+reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

839+ | n == reflm "TermPart" =

840+ case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of

841+ Error e -> Left . InternalMsg $

842+ "could not reify reflected term " ++

843+ show tm ++

844+ " when reflecting an error:" ++ show e

845+ OK (tm', _) -> Right $ TermPart tm'

846+reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

847+ | n == reflm "SubReport" =

848+ case unList tm of

849+ Just xs -> do subParts <- mapM reifyReportPart xs

850+ Right (SubReport subParts)

851+ Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

852+reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

853+

854+reifyTyDecl :: Term -> ElabD RTyDecl

855+reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)

856+ | n == tacN "Declare" =

857+ do tyN' <- reifyTTName tyN

858+ args' <- case unList args of

859+ Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

860+ Just xs -> mapM reifyRArg xs

861+ ret' <- reifyRaw ret

862+ return $ RDeclare tyN' args' ret'

863+ where reifyRArg :: Term -> ElabD RArg

864+ reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)

865+ | n == tacN "Explicit" = liftM2 RExplicit

866+ (reifyTTName argN)

867+ (reifyRaw argTy)

868+ | n == tacN "Implicit" = liftM2 RImplicit

869+ (reifyTTName argN)

870+ (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint

871+ (reifyTTName argN)

872+ (reifyRaw argTy)

873+ reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

874+reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

875+

876+reifyFunDefn :: Term -> ElabD RFunDefn

877+reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)

878+ | n == tacN "DefineFun" =

879+ do fnN' <- reifyTTName fnN

880+ clauses' <- case unList clauses of

881+ Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"

882+ Just cs -> mapM reifyC cs

883+ return $ RDefineFun fnN' clauses'

884+ where reifyC :: Term -> ElabD RFunClause

885+ reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)

886+ | n == tacN "MkFunClause" = liftM2 RMkFunClause

887+ (reifyRaw lhs)

888+ (reifyRaw rhs)

889+ reifyC (App _ (P (DCon _ _ _) n _) lhs)

890+ | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs

891+ reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

892+reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

893+

894+envTupleType :: Raw

895+envTupleType

896+ = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

897+ , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))

898+ ]

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/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 }

test/tactics001/Tactics.idr+10−10

@@ -1,6 +1,6 @@

11module Tactics

3−import Language.Reflection.Tactical

3+import Language.Reflection.Elab

55import Data.Vect

@@ -18,24 +18,24 @@ refl t x = RApp (RApp (Var (UN "Refl")) t) x

1818plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n

1919plusZeroRightNeutralNew Z = Refl

2020plusZeroRightNeutralNew (S k) =

21− %runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))

22− fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))

23− solve)

21+ %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))

22+ fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))

23+ solve)

2424

2525plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)

2626plusSuccRightSuccNew Z k = Refl

2727plusSuccRightSuccNew (S j) k =

28− %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

29− fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

30− solve)

28+ %runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

29+ fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

30+ solve)

3131

3232-- Test that side effects in new tactics work

3333

3434mkDecl : ()

35−mkDecl = %runTactics (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])

35+mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])

3636 [Implicit (UN "z") `(Nat)]

3737 `(Vect ~(Var (UN "z")) ())

38− fill `(() : ())

39− solve)

38+ fill `(() : ())

39+ solve)

4040

4141repUnit = pure ()