git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
370939bEdwin Brady
contribs/gtksourceview-2.0-language-spec/idris.langdeleted−254
compare with master
unifiedsplit
@@ -1,254 +0,0 @@
1−<?xml version="1.0" encoding="UTF-8"?>
2−<!--
3−
4− Author: Dominic Mulligan
5− Copyright (C) 2012 Dominic Mulligan <dominic.p.mulligan@gmail.com>
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
12− Copyright (C) 2004, 2007 Duncan Coutts <duncan@haskell.org>
13− Copyright (C) 2004 Anders Carlsson <andersca@gnome.org>
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">[!#$%&amp;*+./&gt;=&lt;?@:\\^|~-]</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>(?&lt;!\%{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>(?&lt;!\%{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>-&gt;</keyword>
97− <keyword>@</keyword>
98− <keyword>~</keyword>
99− <keyword>=&gt;</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\\"\'&amp;] | # 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.
6− * Copyright 2012. All rights reserved.
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.
6− * Copyright 2012. All rights reserved.
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",
6− "match": "\\b(if|then|else|do|let|in|data|codata|record|dsl|import)\\b"
7−
8− },
9− { "name": "keyword.control.idris",
10− "match": "\\b(impossible|case|of|total|partial|mutual|infix|infixl|infixr)\\b"
11−
12− },
13− { "name": "keyword.control.idris",
14− "match": "\\b(where|with|syntax|proof|postulate|using|namespace|class|instance)\\b"
15−
16− },
17− { "name": "keyword.control.idris",
18− "match": "\\b(public|private|abstract|implicit)\\b"
19−
20− },
21− { "name": "keyword.other.idris",
22− "match": "\\b(Type|Int|Integer|Float|Char|String|Ptr|Bits8|Bits16|Bits32|Bits64)\\b"
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>
15− <string>\b(if|then|else|do|let|in|data|codata|record|dsl|import)\b</string>
16− <key>name</key>
17− <string>keyword.control.idris</string>
18− </dict>
19− <dict>
20− <key>match</key>
21− <string>\b(impossible|case|of|total|partial|mutual|infix|infixl|infixr)\b</string>
22− <key>name</key>
23− <string>keyword.control.idris</string>
24− </dict>
25− <dict>
26− <key>match</key>
27− <string>\b(where|with|syntax|proof|postulate|using|namespace|class|instance)\b</string>
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>
39− <string>\b(Type|Int|Integer|Float|Char|String|Ptr|Bits8|Bits16|Bits32|Bits64)\b</string>
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
1+CABALFLAGS += -f LLVM -f FFI -f curses --disable-documentation --disable-profiling --disable-library-profiling
2−
docs/tutorial/introduction.rst+10−10
@@ -25,11 +25,12 @@ lists of a given length [1]_, ``Vect n a``, where ``a`` is the element
25type and ``n`` is the length of the list and can be an arbitrary term.
25type and ``n`` is the length of the list and can be an arbitrary term.
26
26
27When types can contain values, and where those values describe
27When types can contain values, and where those values describe
28−properties (e.g. the length of a list) the type of a function can
28+properties, for example the length of a list, the type of a function
29−begin to describe its own properties. For example, concatenating two
29+can begin to describe its own properties. Take for example the
30+concatenatation of two lists. This operation has the property that the
30−lists has the property that the resulting list’s length is the sum of
31+resulting list's length is the sum of the lengths of the two input
31−the lengths of the two input lists. We can therefore give the
32+lists. We can therefore give the following type to the ``app``
32−following type to the ``app`` function, which concatenates vectors:
33+function, which concatenates vectors:
33
34
34.. code-block:: idris
35.. code-block:: idris
35
36
@@ -58,11 +59,10 @@ Example Code
58============
59============
59
60
60This tutorial includes some example code, which has been tested with
61This tutorial includes some example code, which has been tested with
61−Idris version . The files are available in the Idris
62+against Idris. These files are available with the Idris distribution,
62−distribution, and provided along side the tutorial source, so that you
63−can try them out easily, under ``tutorial/examples``. However, it is
63+so that you can try them out easily. They can be found under
64−strongly recommended that you can type them in yourself, rather than
64+``samples``. It is, however, strongly recommended that you type
65−simply loading and reading them.
65+them in yourself, rather than simply loading and reading them.
66
66
67.. [1]
67.. [1]
68 Typically, and perhaps confusingly, referred to in the dependently
68 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
10are to be imported, and a collection of declarations and definitions of
10are to be imported, and a collection of declarations and definitions of
11types, classes and functions. For example, the listing below gives a
11types, classes and functions. For example, the listing below gives a
12module which defines a binary tree type ``BTree`` (in a file
12module which defines a binary tree type ``BTree`` (in a file
13−``btree.idr``):
13+``Btree.idr``):
14
14
15.. code-block:: idris
15.. code-block:: idris
16
16
17− module btree
17+ module Btree
18
18
19 data BTree a = Leaf
19 data BTree a = Leaf
20 | Node (BTree a) a (BTree a)
20 | Node (BTree a) a (BTree a)
@@ -40,23 +40,24 @@ Then, this gives a main program (in a file
40
40
41 module Main
41 module Main
42
42
43− import btree
43+ import Btree
44
44
45 main : IO ()
45 main : IO ()
46 main = do let t = toTree [1,8,2,7,9,3]
46 main = do let t = toTree [1,8,2,7,9,3]
47 print (btree.toList t)
47 print (btree.toList t)
48
48
49
49
50+
50The same names can be defined in multiple modules. This is possible
51The same names can be defined in multiple modules. This is possible
51because in practice names are *qualified* with the name of the module.
52because in practice names are *qualified* with the name of the module.
52The names defined in the ``btree`` module are, in full:
53The names defined in the ``btree`` module are, in full:
53
54
54−+ ``btree.BTree``
55++ ``Btree.BTree``
55−+ ``btree.Leaf``
56++ ``Btree.Leaf``
56−+ ``btree.Node``
57++ ``Btree.Node``
57−+ ``btree.insert``
58++ ``Btree.insert``
58−+ ``btree.toList``
59++ ``Btree.toList``
59−+ ``btree.toTree``
60++ ``Btree.toTree``
60
61
61If names are otherwise unambiguous, there is no need to give the fully
62If names are otherwise unambiguous, there is no need to give the fully
62qualified name. Names can be disambiguated either by giving an explicit
63qualified name. Names can be disambiguated either by giving an explicit
@@ -103,7 +104,7 @@ functions to be exported as ``abstract``, as we see below:
103
104
104.. code-block:: idris
105.. code-block:: idris
105
106
106− module btree
107+ module Btree
107
108
108 abstract data BTree a = Leaf
109 abstract data BTree a = Leaf
109 | Node (BTree a) a (BTree a)
110 | Node (BTree a) a (BTree a)
@@ -137,7 +138,8 @@ the ``public`` modifier on an ``import``. For example:
137
138
138 module A
139 module A
139
140
141+ import B
140− import B import public C
142+ import public C
141
143
142 public a : AType a = ...
144 public a : AType a = ...
143
145
@@ -154,7 +156,7 @@ wish to overload names within the same module:
154
156
155.. code-block:: idris
157.. code-block:: idris
156
158
157− module foo
159+ module Foo
158
160
159 namespace x
161 namespace x
160 test : Int -> Int
162 test : Int -> Int
docs/tutorial/starting.rst+9−13
@@ -10,12 +10,9 @@ Prerequisites
10Before installing Idris, you will need to make sure you have all
10Before installing Idris, you will need to make sure you have all
11of the necessary libraries and tools. You will need:
11of the necessary libraries and tools. You will need:
12
12
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
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.
15− date.
16
14
17−- The *GNU Multiple Precision Arithmetic Library* (GMP) is available
15+- The *GNU Multiple Precision Arithmetic Library* (GMP) is available from MacPorts/Homebrew and all major Linux distributions.
18− from MacPorts/Homebrew and all major Linux distributions.
19
16
20Downloading and Installing
17Downloading and Installing
21==========================
18==========================
@@ -33,7 +30,7 @@ development version you can find it, as well as build intructions, on
33GitHub at: https://github.com/idris-lang/Idris-dev.
30GitHub at: https://github.com/idris-lang/Idris-dev.
34
31
35To check that installation has succeeded, and to write your first
32To 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
37following text:
34following text:
38
35
39.. code-block:: idris
36.. code-block:: idris
@@ -55,18 +52,17 @@ create an executable called ``hello``, which you can run:
55 $ ./hello
52 $ ./hello
56 Hello world
53 Hello world
57
54
58−Note that the ``$`` indicates the shell prompt! Should the Idris
55+Please note that the dollar sign ``$`` indicates the shell prompt!
59−executable not be found please ensure that you have added
56+Should the Idris executable not be found please ensure that you have
60−``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X
57+added ``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS
61−users may find they need to use ``~/Library/Haskell/bin``
58+X users may find they need to add ``~/Library/Haskell/bin``
62instead. Some useful options to the Idris command are:
59instead. Some useful options to the Idris command are:
63
60
64- ``-o prog`` to compile to an executable called ``prog``.
61- ``-o prog`` to compile to an executable called ``prog``.
65
62
66−- ``--check`` type check the file and its dependencies without
63+- ``--check`` type check the file and its dependencies without starting the interactive environment.
67− starting the interactive environment.
68
64
69−- ``--help`` display usage summary and command line options
65+- ``--help`` display usage summary and command line options.
70
66
71The Interactive Environment
67The Interactive Environment
72===========================
68===========================
docs/tutorial/typesfuns.rst+37−33
@@ -12,13 +12,13 @@ Idris defines several primitive types: ``Int``, ``Integer`` and
12manipulation, and ``Ptr`` which represents foreign pointers. There are
12manipulation, and ``Ptr`` which represents foreign pointers. There are
13also several data types declared in the library, including ``Bool``,
13also several data types declared in the library, including ``Bool``,
14with values ``True`` and ``False``. We can declare some constants with
14with 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
16into the Idris interactive environment by typing ``idris
16into the Idris interactive environment by typing ``idris
17−prims.idr``:
17+Prims.idr``:
18
18
19.. code-block:: idris
19.. code-block:: idris
20
20
21− module prims
21+ module Prims
22
22
23 x : Int
23 x : Int
24 x = 42
24 x = 42
@@ -33,17 +33,18 @@ prims.idr``:
33 quux = False
33 quux = False
34
34
35An Idris file consists of an optional module declaration (here
35An Idris file consists of an optional module declaration (here
36−``module prims``) followed by an optional list of imports (none here,
36+``module Prims``) followed by an optional list of imports and a
37+collection of declarations and definitions. In this example no imports
37−however Idris programs can consist of several modules, and the
38+have been specified. However Idris programs can consist of several
38−definitions in each module each have their own namespace, as we will
39+modules and the definitions in each module each have their own
39−discuss in Section :ref:`sect-namespaces`) and a collection of
40+namespace. This is discussed further in Section
40−declarations and definitions. The order of definitions is significant
41+:ref:`sect-namespaces`). When writing Idris programs both the order in
42+definitions are given and indentation are significant. Functions and
41−— functions and data types must be defined before use. Each definition
43+data types must be defined before use, incidently each definition must
42−must have a type declaration, for example see ``x : Int``, ``foo :
44+have a type declaration, for example see ``x : Int``, ``foo :
43−String``, from the above listing. Indentation is significant — a new
45+String``, from the above listing. New declarations must begin at the
44−declaration begins at the same level of indentation as the preceding
46+same level of indentation as the preceding declaration.
45−declaration. Alternatively, declarations may be terminated with a
47+Alternatively, a semicolon ``;`` can be used to terminate declarations.
46−semicolon.
47
48
48A library module ``prelude`` is automatically imported by every
49A library module ``prelude`` is automatically imported by every
49Idris program, including facilities for IO, arithmetic, data
50Idris program, including facilities for IO, arithmetic, data
@@ -63,7 +64,7 @@ All of the usual arithmetic and comparison operators are defined for
63the primitive types. They are overloaded using type classes, as we
64the primitive types. They are overloaded using type classes, as we
64will discuss in Section :ref:`sect-classes` and can be extended to
65will discuss in Section :ref:`sect-classes` and can be extended to
65work on user defined types. Boolean expressions can be tested with the
66work on user defined types. Boolean expressions can be tested with the
66−``if...then...else`` construct:
67+``if...then...else`` construct, for example:
67
68
68::
69::
69
70
@@ -73,9 +74,9 @@ work on user defined types. Boolean expressions can be tested with the
73Data Types
74Data Types
74==========
75==========
75
76
76−Data types are declared in a similar way to Haskell data types, with a
77+Data types are declared in a similar way and with similar syntax to
77−similar syntax. Natural numbers and lists, for example, can be
78+Haskell. Natural numbers and lists, for example, can be declared as
78−declared as follows:
79+follows:
79
80
80.. code-block:: idris
81.. code-block:: idris
81
82
@@ -193,11 +194,13 @@ does not need to be visible globally:
193Indentation is significant — functions in the ``where`` block must be
194Indentation is significant — functions in the ``where`` block must be
194indented further than the outer function.
195indented further than the outer function.
195
196
197+.. note:: Scope
198+
196−**Scope:** Any names which are visible in the outer scope are also
199+ Any names which are visible in the outer scope are also visible in
197−visible in the ``where`` clause (unless they have been redefined, such
200+ the ``where`` clause (unless they have been redefined, such as ``xs``
198−as ``xs`` here). A name which appears only in the type will be in scope
201+ here). A name which appears only in the type will be in scope in the
199−in the ``where`` clause if it is a *parameter* to one of the types,
202+ ``where`` clause if it is a *parameter* to one of the types, i.e. it
200−i.e. it is fixed across the entire structure.
203+ is fixed across the entire structure.
201
204
202As well as functions, ``where`` blocks can include local data
205As well as functions, ``where`` blocks can include local data
203declarations, such as the following where ``MyLT`` is not accessible
206declarations, such as the following where ``MyLT`` is not accessible
@@ -306,16 +309,17 @@ following:
306 $ idris vbroken.idr --check
309 $ idris vbroken.idr --check
307 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
310 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
308 When elaborating an application of constructor Vect.:::
311 When elaborating an application of constructor Vect.:::
309− Can't unify
312+ Can't unify
310− Vect (k + k) a
313+ Vect (k + k) a (Type of xs ++ xs)
311− with
314+ with
312− Vect (plus k m) a
315+ Vect (plus k m) a (Expected type)
313−
316+
314− Specifically:
317+ Specifically:
315− Can't unify
318+ Can't unify
316− plus k k
319+ plus k k
317− with
320+ with
318− plus k m
321+ plus k m
322+
319
323
320This error message suggests that there is a length mismatch between
324This error message suggests that there is a length mismatch between
321two vectors — we needed a vector of length ``k + m``, but provided a
325two vectors — we needed a vector of length ``k + m``, but provided a
docs/tutorial/views.rst+2−2
@@ -83,8 +83,8 @@ rule:
83The value of the result of ``parity k`` affects the form of ``k``,
83The value of the result of ``parity k`` affects the form of ``k``,
84because the result of ``parity k`` depends on ``k``. So, as well as
84because the result of ``parity k`` depends on ``k``. So, as well as
85the patterns for the result of the intermediate computation (``Even``
85the patterns for the result of the intermediate computation (``Even``
86−and ``odd``) right of the ``\mid``, we also write how the results
86+and ``odd``) right of the ``|``, we also write how the results
87−affect the other patterns left of the :math:`\mid`. Note that there is
87+affect the other patterns left of the ``|``. Note that there is
88a function in the patterns (``+``) and repeated occurrences of
88a function in the patterns (``+``) and repeated occurrences of
89``j``—this is allowed because another argument has determined the form
89``j``—this is allowed because another argument has determined the form
90of these patterns.
90of these patterns.
libs/base/Data/Bits.idr+5−10
@@ -4,21 +4,16 @@ import Data.Fin
4
4
5%default total
5%default total
6
6
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−
12nextPow2 : Nat -> Nat
7nextPow2 : Nat -> Nat
13nextPow2 Z = Z
8nextPow2 Z = Z
14−nextPow2 x = if x == (2 `power` l2x)
9+nextPow2 (S x) = if (S x) == (2 `power` l2x)
15− then l2x
10+ then l2x
16− else S l2x
11+ else S l2x
17 where
12 where
18− l2x = log2 x
13+ l2x = log2NZ (S x) SIsNotZ
19
14
20nextBytes : Nat -> Nat
15nextBytes : Nat -> Nat
21−nextBytes bits = (nextPow2 (bits `divCeil` 8))
16+nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
22
17
23machineTy : Nat -> Type
18machineTy : Nat -> Type
24machineTy Z = Bits8
19machineTy Z = Bits8
libs/contrib/Network/Cgi.idr+1−1
@@ -108,7 +108,7 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
108 | _ = Nothing
108 | _ = Nothing
109
109
110getContent : Int -> IO String
110getContent : Int -> IO String
111−getContent x = getC (toNat x) "" where
111+getContent x = getC (cast x) "" where
112 getC : Nat -> String -> IO String
112 getC : Nat -> String -> IO String
113 getC Z acc = return $ reverse acc
113 getC Z acc = return $ reverse acc
114 getC (S k) acc = do x <- getChar
114 getC (S k) acc = do x <- getChar
libs/effects/Effect/Exception.idr+3−3
@@ -4,7 +4,7 @@ import Effects
4import System
4import System
5import Control.IOExcept
5import Control.IOExcept
6
6
7−data Exception : Type -> Effect where
7+data Exception : Type -> Effect where
8 Raise : a -> sig (Exception a) b
8 Raise : a -> sig (Exception a) b
9
9
10instance Handler (Exception a) Maybe where
10instance Handler (Exception a) Maybe where
@@ -14,7 +14,7 @@ instance Handler (Exception a) List where
14 handle _ (Raise e) k = []
14 handle _ (Raise e) k = []
15
15
16instance Show a => Handler (Exception a) IO where
16instance Show a => Handler (Exception a) IO where
17− handle _ (Raise e) k = do print e
17+ handle _ (Raise e) k = do printLn e
18 believe_me (exit 1)
18 believe_me (exit 1)
19
19
20instance Handler (Exception a) (IOExcept a) where
20instance Handler (Exception a) (IOExcept a) where
@@ -26,5 +26,5 @@ instance Handler (Exception a) (Either a) where
26EXCEPTION : Type -> EFFECT
26EXCEPTION : Type -> EFFECT
27EXCEPTION t = MkEff () (Exception t)
27EXCEPTION t = MkEff () (Exception t)
28
28
29−raise : a -> Eff b [EXCEPTION a]
29+raise : a -> Eff b [EXCEPTION a]
30raise err = call $ Raise err
30raise err = call $ Raise err
libs/effects/Effect/StdIO.idr+18−7
@@ -9,8 +9,8 @@ import Control.IOExcept
9
9
10||| The internal representation of StdIO effects
10||| The internal representation of StdIO effects
11data StdIO : Effect where
11data StdIO : Effect where
12− PutStr : String -> sig StdIO ()
12+ PutStr : String -> sig StdIO ()
13− GetStr : sig StdIO String
13+ GetStr : sig StdIO String
14 PutCh : Char -> sig StdIO ()
14 PutCh : Char -> sig StdIO ()
15 GetCh : sig StdIO Char
15 GetCh : sig StdIO Char
16
16
@@ -22,13 +22,13 @@ data StdIO : Effect where
22instance Handler StdIO IO where
22instance Handler StdIO IO where
23 handle () (PutStr s) k = do putStr s; k () ()
23 handle () (PutStr s) k = do putStr s; k () ()
24 handle () GetStr k = do x <- getLine; k x ()
24 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 () ()
26 handle () GetCh k = do x <- getChar; k x ()
26 handle () GetCh k = do x <- getChar; k x ()
27
27
28instance Handler StdIO (IOExcept a) where
28instance Handler StdIO (IOExcept a) where
29 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
29 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
30 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()
30 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 () ()
32 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
32 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
33
33
34-------------------------------------------------------------
34-------------------------------------------------------------
@@ -42,13 +42,17 @@ STDIO = MkEff () StdIO
42putStr : String -> Eff () [STDIO]
42putStr : String -> Eff () [STDIO]
43putStr s = call $ PutStr s
43putStr s = call $ PutStr s
44
44
45+||| Write a string to standard output, terminating with a newline.
46+putStrLn : String -> Eff () [STDIO]
47+putStrLn s = putStr (s ++ "\n")
48+
45||| Write a character to standard output.
49||| Write a character to standard output.
46putChar : Char -> Eff () [STDIO]
50putChar : Char -> Eff () [STDIO]
47putChar c = call $ PutCh c
51putChar c = call $ PutCh c
48
52
49−||| Write a string to standard output, terminating with a newline.
53+||| Write a character to standard output, terminating with a newline.
50−putStrLn : String -> Eff () [STDIO]
54+putCharLn : Char -> Eff () [STDIO]
51−putStrLn s = putStr (s ++ "\n")
55+putCharLn c = putStrLn (singleton c)
52
56
53||| Read a string from standard input.
57||| Read a string from standard input.
54getStr : Eff String [STDIO]
58getStr : Eff String [STDIO]
@@ -58,3 +62,10 @@ getStr = call $ GetStr
58getChar : Eff Char [STDIO]
62getChar : Eff Char [STDIO]
59getChar = call $ GetCh
63getChar = call $ GetCh
60
64
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
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+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
135 show (Just x) = "Just " ++ show x
135 show (Just x) = "Just " ++ show x
136
136
137instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
137instance (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 ++ ")"
139
139
140---- Functor instances
140---- Functor instances
141
141
@@ -245,8 +245,8 @@ natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
245total natEnumFromTo : Nat -> Nat -> List Nat
245total natEnumFromTo : Nat -> Nat -> List Nat
246natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
246natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
247total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
247total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
248−natEnumFromThenTo _ Z _ = []
248+natEnumFromThenTo _ Z _ = []
249−natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
249+natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (m - n) (S inc) SIsNotZ)))
250
250
251class Enum a where
251class Enum a where
252 total pred : a -> a
252 total pred : a -> a
@@ -285,7 +285,7 @@ instance Enum Integer where
285 go [] = []
285 go [] = []
286 go (x :: xs) = n + cast x :: go xs
286 go (x :: xs) = n + cast x :: go xs
287 enumFromThenTo _ 0 _ = []
287 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)))
289 where go : List Nat -> List Integer
289 where go : List Nat -> List Integer
290 go [] = []
290 go [] = []
291 go (x :: xs) = n + (cast x * inc) :: go xs
291 go (x :: xs) = n + (cast x * inc) :: go xs
@@ -305,7 +305,7 @@ instance Enum Int where
305 go acc (S k) m = go (m :: acc) k (m - 1)
305 go acc (S k) m = go (m :: acc) k (m - 1)
306 enumFromThen n inc = n :: enumFromThen (inc + n) inc
306 enumFromThen n inc = n :: enumFromThen (inc + n) inc
307 enumFromThenTo _ 0 _ = []
307 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)))
309 where go : List Nat -> List Int
309 where go : List Nat -> List Int
310 go [] = []
310 go [] = []
311 go (x :: xs) = n + (cast x * inc) :: go xs
311 go (x :: xs) = n + (cast x * inc) :: go xs
@@ -349,7 +349,7 @@ partial
349printLn : Show a => a -> IO' ffi ()
349printLn : Show a => a -> IO' ffi ()
350printLn x = putStrLn (show x)
350printLn x = putStrLn (show x)
351
351
352−||| Read one line of input from stdin
352+||| Read one line of input from stdin, without the trailing newline
353partial
353partial
354getLine : IO' ffi String
354getLine : IO' ffi String
355getLine = prim_read
355getLine = prim_read
@@ -548,5 +548,7 @@ readFile fn = do h <- openFile fn Read
548 readFile' h contents =
548 readFile' h contents =
549 do x <- feof h
549 do x <- feof h
550 if not x then do l <- fread h
550 if not x then do l <- fread h
551+ case contents of
552+ "" => readFile' h l
551− readFile' h (contents ++ l)
553+ _ => readFile' h (contents ++ "\n" ++ l)
552 else return contents
554 else return contents
libs/prelude/Prelude/Classes.idr+24−12
@@ -315,10 +315,12 @@ class Integral a where
315
315
316-- ---------------------------------------------------------------- [ Integers ]
316-- ---------------------------------------------------------------- [ Integers ]
317divBigInt : Integer -> Integer -> Integer
317divBigInt : Integer -> Integer -> Integer
318+divBigInt x y = case y == 0 of
318−divBigInt = prim__sdivBigInt
319+ False => prim__sdivBigInt x y
319
320
320modBigInt : Integer -> Integer -> Integer
321modBigInt : Integer -> Integer -> Integer
322+modBigInt x y = case y == 0 of
321−modBigInt = prim__sremBigInt
323+ False => prim__sremBigInt x y
322
324
323instance Integral Integer where
325instance Integral Integer where
324 div = divBigInt
326 div = divBigInt
@@ -327,10 +329,12 @@ instance Integral Integer where
327-- --------------------------------------------------------------------- [ Int ]
329-- --------------------------------------------------------------------- [ Int ]
328
330
329divInt : Int -> Int -> Int
331divInt : Int -> Int -> Int
332+divInt x y = case y == 0 of
330−divInt = prim__sdivInt
333+ False => prim__sdivInt x y
331
334
332modInt : Int -> Int -> Int
335modInt : Int -> Int -> Int
336+modInt x y = case y == 0 of
333−modInt = prim__sremInt
337+ False => prim__sremInt x y
334
338
335instance Integral Int where
339instance Integral Int where
336 div = divInt
340 div = divInt
@@ -338,10 +342,12 @@ instance Integral Int where
338
342
339-- ------------------------------------------------------------------- [ Bits8 ]
343-- ------------------------------------------------------------------- [ Bits8 ]
340divB8 : Bits8 -> Bits8 -> Bits8
344divB8 : Bits8 -> Bits8 -> Bits8
345+divB8 x y = case y == 0 of
341−divB8 = prim__sdivB8
346+ False => prim__sdivB8 x y
342
347
343modB8 : Bits8 -> Bits8 -> Bits8
348modB8 : Bits8 -> Bits8 -> Bits8
349+modB8 x y = case y == 0 of
344−modB8 = prim__sremB8
350+ False => prim__sremB8 x y
345
351
346instance Integral Bits8 where
352instance Integral Bits8 where
347 div = divB8
353 div = divB8
@@ -349,10 +355,12 @@ instance Integral Bits8 where
349
355
350-- ------------------------------------------------------------------ [ Bits16 ]
356-- ------------------------------------------------------------------ [ Bits16 ]
351divB16 : Bits16 -> Bits16 -> Bits16
357divB16 : Bits16 -> Bits16 -> Bits16
358+divB16 x y = case y == 0 of
352−divB16 = prim__sdivB16
359+ False => prim__sdivB16 x y
353
360
354modB16 : Bits16 -> Bits16 -> Bits16
361modB16 : Bits16 -> Bits16 -> Bits16
362+modB16 x y = case y == 0 of
355−modB16 = prim__sremB16
363+ False => prim__sremB16 x y
356
364
357instance Integral Bits16 where
365instance Integral Bits16 where
358 div = divB16
366 div = divB16
@@ -360,10 +368,12 @@ instance Integral Bits16 where
360
368
361-- ------------------------------------------------------------------ [ Bits32 ]
369-- ------------------------------------------------------------------ [ Bits32 ]
362divB32 : Bits32 -> Bits32 -> Bits32
370divB32 : Bits32 -> Bits32 -> Bits32
371+divB32 x y = case y == 0 of
363−divB32 = prim__sdivB32
372+ False => prim__sdivB32 x y
364
373
365modB32 : Bits32 -> Bits32 -> Bits32
374modB32 : Bits32 -> Bits32 -> Bits32
375+modB32 x y = case y == 0 of
366−modB32 = prim__sremB32
376+ False => prim__sremB32 x y
367
377
368instance Integral Bits32 where
378instance Integral Bits32 where
369 div = divB32
379 div = divB32
@@ -371,10 +381,12 @@ instance Integral Bits32 where
371
381
372-- ------------------------------------------------------------------ [ Bits64 ]
382-- ------------------------------------------------------------------ [ Bits64 ]
373divB64 : Bits64 -> Bits64 -> Bits64
383divB64 : Bits64 -> Bits64 -> Bits64
384+divB64 x y = case y == 0 of
374−divB64 = prim__sdivB64
385+ False => prim__sdivB64 x y
375
386
376modB64 : Bits64 -> Bits64 -> Bits64
387modB64 : Bits64 -> Bits64 -> Bits64
388+modB64 x y = case y == 0 of
377−modB64 = prim__sremB64
389+ False => prim__sremB64 x y
378
390
379instance Integral Bits64 where
391instance Integral Bits64 where
380 div = divB64
392 div = divB64
libs/prelude/Prelude/List.idr+14−6
@@ -309,13 +309,12 @@ mapMaybe f (x::xs) =
309-- Folds
309-- Folds
310--------------------------------------------------------------------------------
310--------------------------------------------------------------------------------
311
311
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−
317instance Foldable List where
312instance 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
319
318
320--------------------------------------------------------------------------------
319--------------------------------------------------------------------------------
321-- Special folds
320-- Special folds
@@ -809,6 +808,15 @@ hasAnyByNilFalse p (x::xs) =
809hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
808hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
810hasAnyNilFalse l = ?hasAnyNilFalseBody
809hasAnyNilFalse l = ?hasAnyNilFalseBody
811
810
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+
812
820
813--------------------------------------------------------------------------------
821--------------------------------------------------------------------------------
814-- Proofs
822-- Proofs
libs/prelude/Prelude/Nat.idr+36−17
@@ -288,10 +288,12 @@ fact (S n) = (S n) * fact n
288-- Division and modulus
288-- Division and modulus
289--------------------------------------------------------------------------------
289--------------------------------------------------------------------------------
290
290
291−total
291+SIsNotZ : {x: Nat} -> (S x = Z) -> Void
292+SIsNotZ Refl impossible
293+
292−modNat : Nat -> Nat -> Nat
294+modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
293−modNat left Z = left
295+modNatNZ left Z p = void (p Refl)
294−modNat left (S right) = mod' left left right
296+modNatNZ left (S right) _ = mod' left left right
295 where
297 where
296 total mod' : Nat -> Nat -> Nat -> Nat
298 total mod' : Nat -> Nat -> Nat -> Nat
297 mod' Z centre right = centre
299 mod' Z centre right = centre
@@ -301,10 +303,13 @@ modNat left (S right) = mod' left left right
301 else
303 else
302 mod' left (centre - (S right)) right
304 mod' left (centre - (S right)) right
303
305
304−total
306+partial
307+modNat : Nat -> Nat -> Nat
308+modNat left (S right) = modNatNZ left (S right) SIsNotZ
309+
305−divNat : Nat -> Nat -> Nat
310+divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
306−divNat left Z = S left -- div by zero
311+divNatNZ left Z p = void (p Refl)
307−divNat left (S right) = div' left left right
312+divNatNZ left (S right) _ = div' left left right
308 where
313 where
309 total div' : Nat -> Nat -> Nat -> Nat
314 total div' : Nat -> Nat -> Nat -> Nat
310 div' Z centre right = Z
315 div' Z centre right = Z
@@ -314,23 +319,42 @@ divNat left (S right) = div' left left right
314 else
319 else
315 S (div' left (centre - (S right)) right)
320 S (div' left (centre - (S right)) right)
316
321
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+
317instance Integral Nat where
335instance Integral Nat where
318 div = divNat
336 div = divNat
319 mod = modNat
337 mod = modNat
320
338
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
321log2 : Nat -> Nat
345log2 : Nat -> Nat
322−log2 Z = Z
346+log2 (S n) = log2NZ (S n) SIsNotZ
323−log2 (S Z) = Z
324−log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
325
347
326--------------------------------------------------------------------------------
348--------------------------------------------------------------------------------
327-- GCD and LCM
349-- GCD and LCM
328--------------------------------------------------------------------------------
350--------------------------------------------------------------------------------
351+partial
329gcd : Nat -> Nat -> Nat
352gcd : Nat -> Nat -> Nat
330gcd a Z = a
353gcd a Z = a
331gcd a b = assert_total (gcd b (a `modNat` b))
354gcd a b = assert_total (gcd b (a `modNat` b))
332
355
356+partial
333−total lcm : Nat -> Nat -> Nat
357+lcm : Nat -> Nat -> Nat
334lcm _ Z = Z
358lcm _ Z = Z
335lcm Z _ = Z
359lcm Z _ = Z
336lcm x y = divNat (x * y) (gcd x y)
360lcm x y = divNat (x * y) (gcd x y)
@@ -724,11 +748,6 @@ total sucMinR : (l : Nat) -> minimum l (S l) = l
724sucMinR Z = Refl
748sucMinR Z = Refl
725sucMinR (S l) = cong (sucMinR l)
749sucMinR (S l) = cong (sucMinR l)
726
750
727−-- div and mod
728−total modZeroZero : (n : Nat) -> mod 0 n = Z
729−modZeroZero Z = Refl
730−modZeroZero (S n) = Refl
731−
732--------------------------------------------------------------------------------
751--------------------------------------------------------------------------------
733-- Proofs
752-- Proofs
734--------------------------------------------------------------------------------
753--------------------------------------------------------------------------------
libs/prelude/prelude.ipkg+1−1
@@ -10,7 +10,7 @@ modules = Builtins, Prelude, IO,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
12
12
13− Language.Reflection, Language.Reflection.Errors, Language.Reflection.Tactical,
13+ Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
14
14
15 Decidable.Equality
15 Decidable.Equality
16
16
rts/idris_rts.c+5−2
@@ -504,17 +504,20 @@ VAL idris_strlen(VM* vm, VAL l) {
504}
504}
505
505
506VAL idris_readStr(VM* vm, FILE* h) {
506VAL idris_readStr(VM* vm, FILE* h) {
507+ VAL ret;
507 char *buffer = NULL;
508 char *buffer = NULL;
508 size_t n = 0;
509 size_t n = 0;
509 ssize_t len;
510 ssize_t len;
510 len = getline(&buffer, &n, h);
511 len = getline(&buffer, &n, h);
512+ strtok(buffer, "\n");
511
513
512 if (len <= 0) {
514 if (len <= 0) {
513− return MKSTR(vm, "");
515+ ret = MKSTR(vm, "");
514 } else {
516 } else {
515− return MKSTR(vm, buffer);
517+ ret = MKSTR(vm, buffer);
516 }
518 }
517 free(buffer);
519 free(buffer);
520+ return ret;
518}
521}
519
522
520VAL idris_strHead(VM* vm, VAL str) {
523VAL idris_strHead(VM* vm, VAL str) {
src/Idris/AbsSyntax.hs+4−4
@@ -1011,7 +1011,7 @@ expandParams dec ps ns infs tm = en tm
1011 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1011 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1012 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1012 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1013 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1013 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)
1015 en t = t
1015 en t = t
1016
1016
1017 nselem x [] = False
1017 nselem x [] = False
@@ -1485,7 +1485,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1485 imps top env (PHidden tm) = imps False env tm
1485 imps top env (PHidden tm) = imps False env tm
1486 imps top env (PUnifyLog tm) = imps False env tm
1486 imps top env (PUnifyLog tm) = imps False env tm
1487 imps top env (PNoImplicits tm) = imps False env tm
1487 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
1489 imps top env _ = return ()
1489 imps top env _ = return ()
1490
1490
1491 pibind using [] sc = sc
1491 pibind using [] sc = sc
@@ -1612,7 +1612,7 @@ addImpl' inpat env infns imp_meths ist ptm
1612 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1612 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1613 (fmap (ai True env ds) g)
1613 (fmap (ai True env ds) g)
1614 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1614 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)
1616 ai qq env ds tm = tm
1616 ai qq env ds tm = tm
1617
1617
1618 handleErr (Left err) = PElabError err
1618 handleErr (Left err) = PElabError err
@@ -2149,5 +2149,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
2149 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2149 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
2150 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2150 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
2151 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2151 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)
2153 mkUniq t = return t
2153 mkUniq t = return t
src/Idris/AbsSyntaxTree.hs+20−7
@@ -645,11 +645,16 @@ deriving instance Binary PDecl'
645deriving instance NFData PDecl'
645deriving instance NFData PDecl'
646!-}
646!-}
647
647
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+
648−-- For elaborator state
653+-- | For elaborator state
649data EState = EState {
654data EState = EState {
650 case_decls :: [PDecl],
655 case_decls :: [PDecl],
651 delayed_elab :: [Elab' EState ()],
656 delayed_elab :: [Elab' EState ()],
652− new_tyDecls :: [(Name, FC, [PArg], Type)]
657+ new_tyDecls :: [RDeclInstructions]
653 }
658 }
654
659
655initEState :: EState
660initEState :: EState
@@ -821,7 +826,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
821 | PNoImplicits PTerm -- ^ never run implicit converions on the term
826 | PNoImplicits PTerm -- ^ never run implicit converions on the term
822 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
827 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
823 | PUnquote PTerm -- ^ ~Term
828 | PUnquote PTerm -- ^ ~Term
824− | PRunTactics FC PTerm -- ^ %runTactics tm - New-style proof script
829+ | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script
825 deriving (Eq, Data, Typeable)
830 deriving (Eq, Data, Typeable)
826
831
827
832
@@ -1428,16 +1433,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1428 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1433 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1429 prettySe p bnd (PLam fc n ty sc) =
1434 prettySe p bnd (PLam fc n ty sc) =
1430 bracket p startPrec . group . align . hang 2 $
1435 bracket p startPrec . group . align . hang 2 $
1431− text "\\" <> bindingOf n False <+> text "=>" <$>
1436+ text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1432 prettySe startPrec ((n, False):bnd) sc
1437 prettySe startPrec ((n, False):bnd) sc
1433 prettySe p bnd (PLet fc n ty v sc) =
1438 prettySe p bnd (PLet fc n ty v sc) =
1434 bracket p startPrec . group . align $
1439 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) </>
1436 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1441 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1437 prettySe p bnd (PPi (Exp l s _) n ty sc)
1442 prettySe p bnd (PPi (Exp l s _) n ty sc)
1438 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1443 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1439 bracket p startPrec . group $
1444 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) <+>
1441 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1446 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1442 | otherwise =
1447 | otherwise =
1443 bracket p startPrec . group $
1448 bracket p startPrec . group $
@@ -1450,7 +1455,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1450 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1455 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1451 | ppopt_impl ppo =
1456 | ppopt_impl ppo =
1452 bracket p startPrec $
1457 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 <+>
1454 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1459 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1455 | otherwise = prettySe startPrec ((n, True):bnd) sc
1460 | otherwise = prettySe startPrec ((n, True):bnd) sc
1456 where
1461 where
@@ -1607,6 +1612,14 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1607
1612
1608 prettySe p bnd _ = text "missing pretty-printer for term"
1613 prettySe p bnd _ = text "missing pretty-printer for term"
1609
1614
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+
1610 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1623 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1611 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1624 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1612 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1625 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
src/Idris/Core/TT.hs+4−3
@@ -117,9 +117,6 @@ data ErrorReportPart = TextPart String
117 deriving (Show, Eq, Data, Typeable)
117 deriving (Show, Eq, Data, Typeable)
118
118
119
119
120−-- Please remember to keep Err synchronised with
121−-- Language.Reflection.Errors.Err in the stdlib!
122−
123data Provenance = ExpectedType
120data Provenance = ExpectedType
124 | TooManyArgs Term
121 | TooManyArgs Term
125 | InferredVal
122 | InferredVal
@@ -131,6 +128,10 @@ deriving instance NFData Err
131deriving instance Binary Err
128deriving instance Binary Err
132!-}
129!-}
133
130
131+
132+-- NB: Please remember to keep Err synchronised with
133+-- Language.Reflection.Errors.Err in the stdlib!
134+
134-- | Idris errors. Used as exceptions in the compiler, but reported to users
135-- | Idris errors. Used as exceptions in the compiler, but reported to users
135-- if they reach the top level.
136-- if they reach the top level.
136data Err' t
137data Err' t
src/Idris/DSL.hs+2−2
@@ -108,7 +108,7 @@ expandDo dsl (PDoBlock ds)
108 block b _ = PElabError (Msg "Invalid statement in do block")
108 block b _ = PElabError (Msg "Invalid statement in do block")
109
109
110expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
110expandDo 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
112expandDo dsl t = t
112expandDo dsl t = t
113
113
114-- | Replace DSL-bound variable in a term
114-- | Replace DSL-bound variable in a term
@@ -195,7 +195,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
195 db' (PDPair fc p l t r) = do l' <- db' l
195 db' (PDPair fc p l t r) = do l' <- db' l
196 r' <- db' r
196 r' <- db' r
197 return (PDPair fc p l' t r')
197 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)
199 db' t = return t
199 db' t = return t
200
200
201 dbArg a = do t' <- db' (getTm a)
201 dbArg a = do t' <- db' (getTm a)
src/Idris/DeepSeq.hs+1−1
@@ -243,7 +243,7 @@ instance NFData PTerm where
243 rnf (PNoImplicits x1) = rnf x1 `seq` ()
243 rnf (PNoImplicits x1) = rnf x1 `seq` ()
244 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
244 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
245 rnf (PUnquote x1) = rnf x1 `seq` ()
245 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` ()
247
247
248instance (NFData t) => NFData (PTactic' t) where
248instance (NFData t) => NFData (PTactic' t) where
249 rnf (Intro x1) = rnf x1 `seq` ()
249 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 #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.Elab.Term where
3module Idris.Elab.Term where
4
4
@@ -10,6 +10,7 @@ import Idris.Error
10import Idris.ProofSearch
10import Idris.ProofSearch
11import Idris.Output (pshow)
11import Idris.Output (pshow)
12
12
13+import Idris.Core.CaseTree (SC, SC'(STerm))
13import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.TT
15import Idris.Core.TT
15import Idris.Core.Evaluate
16import Idris.Core.Evaluate
@@ -35,6 +36,7 @@ import Debug.Trace
35data ElabMode = ETyDecl | ELHS | ERHS
36data ElabMode = ETyDecl | ELHS | ERHS
36 deriving Eq
37 deriving Eq
37
38
39+
38data ElabResult =
40data ElabResult =
39 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
41 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
40 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
42 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
@@ -43,23 +45,28 @@ data ElabResult =
43 -- ^ Deferred declarations as the meaning of case blocks
45 -- ^ Deferred declarations as the meaning of case blocks
44 , resultContext :: Context
46 , resultContext :: Context
45 -- ^ The potentially extended context from new definitions
47 -- ^ The potentially extended context from new definitions
46− , resultTyDecls :: [(Name, FC, [PArg], Type)]
48+ , resultTyDecls :: [RDeclInstructions]
47 -- ^ Meta-info about the new type declarations
49 -- ^ Meta-info about the new type declarations
48 }
50 }
49
51
50−processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()
52+processTacticDecls :: [RDeclInstructions] -> Idris ()
51processTacticDecls info =
53processTacticDecls info =
52− forM_ info $ \(n, fc, impls, ty) ->
54+ forM_ info $ \case
55+ RTyDeclInstrs n fc impls ty ->
53− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
56+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
54− logLvl 3 $ " It has impls " ++ show impls
57+ logLvl 3 $ " It has impls " ++ show impls
55− updateIState $ \i -> i { idris_implicits =
58+ updateIState $ \i -> i { idris_implicits =
56− addDef n impls (idris_implicits i) }
59+ addDef n impls (idris_implicits i) }
57− addIBC (IBCImp n)
60+ addIBC (IBCImp n)
58− ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]
61+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]
59− addIBC (IBCDef n)
62+ addIBC (IBCDef n)
60− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
63+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
61− addDeferred ds'
64+ addDeferred ds'
62−
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)
63
70
64-- Using the elaborator, convert a term in raw syntax to a fully
71-- Using the elaborator, convert a term in raw syntax to a fully
65-- elaborated, typechecked term.
72-- elaborated, typechecked term.
@@ -213,7 +220,7 @@ goal_polymorphic =
213
220
214-- | Returns the set of declarations we need to add to complete the
221-- | Returns the set of declarations we need to add to complete the
215-- definition (most likely case blocks to elaborate) as well as
222-- 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)
217elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
224elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
218 ElabD ()
225 ElabD ()
219elab ist info emode opts fn tm
226elab ist info emode opts fn tm
@@ -1098,11 +1105,11 @@ elab ist info emode opts fn tm
1098 delayElab $ do focus h
1105 delayElab $ do focus h
1099 dotterm
1106 dotterm
1100 elab' ina fc t
1107 elab' ina fc t
1101− elab' ina fc (PRunTactics fc' tm) =
1108+ elab' ina fc (PRunElab fc' tm) =
1102 do attack
1109 do attack
1103 n <- getNameFrom (sMN 0 "tacticScript")
1110 n <- getNameFrom (sMN 0 "tacticScript")
1104 n' <- getNameFrom (sMN 0 "tacticExpr")
1111 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)
1106 claim n scriptTy
1113 claim n scriptTy
1107 movelast n
1114 movelast n
1108 letbind n' scriptTy (Var n)
1115 letbind n' scriptTy (Var n)
@@ -1592,8 +1599,6 @@ case_ ind autoSolve ist fn tm = do
1592 else casetac (forget val)
1599 else casetac (forget val)
1593 when autoSolve solveAll
1600 when autoSolve solveAll
1594
1601
1595−tacN :: String -> Name
1596−tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1597
1602
1598runTactical :: FC -> Env -> Term -> ElabD ()
1603runTactical :: FC -> Env -> Term -> ElabD ()
1599runTactical fc env tm = do tm' <- eval tm
1604runTactical fc env tm = do tm' <- eval tm
@@ -1605,6 +1610,45 @@ runTactical fc env tm = do tm' <- eval tm
1605
1610
1606 returnUnit = fmap fst $ get_type_val (Var unitCon)
1611 returnUnit = fmap fst $ get_type_val (Var unitCon)
1607
1612
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+
1608 -- | Do a step in the reflected elaborator monad. The input is the
1652 -- | Do a step in the reflected elaborator monad. The input is the
1609 -- step, the output is the (reflected) term returned.
1653 -- step, the output is the (reflected) term returned.
1610 runTacTm :: Term -> ElabD Term
1654 runTacTm :: Term -> ElabD Term
@@ -1643,9 +1687,9 @@ runTactical fc env tm = do tm' <- eval tm
1643 = do errs' <- eval errs
1687 = do errs' <- eval errs
1644 parts <- reifyReportParts errs'
1688 parts <- reifyReportParts errs'
1645 lift . tfail $ ReflectionError [parts] (Msg "")
1689 lift . tfail $ ReflectionError [parts] (Msg "")
1646− | n == tacN "prim__PureTactical", [_a, tm] <- args
1690+ | n == tacN "prim__PureElab", [_a, tm] <- args
1647 = return tm
1691 = return tm
1648− | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1692+ | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args
1649 = do first' <- eval first
1693 = do first' <- eval first
1650 res <- runTacTm first'
1694 res <- runTacTm first'
1651 next <- eval (App Complete andThen res)
1695 next <- eval (App Complete andThen res)
@@ -1672,7 +1716,7 @@ runTactical fc env tm = do tm' <- eval tm
1672 returnUnit
1716 returnUnit
1673 | n == tacN "prim__Forget", [tt] <- args
1717 | n == tacN "prim__Forget", [tt] <- args
1674 = do tt' <- reifyTT tt
1718 = do tt' <- reifyTT tt
1675− fmap fst . get_type_val $ reflect tt'
1719+ fmap fst . get_type_val . reflectRaw $ forget tt'
1676 | n == tacN "prim__Attack", [] <- args
1720 | n == tacN "prim__Attack", [] <- args
1677 = do attack
1721 = do attack
1678 returnUnit
1722 returnUnit
@@ -1713,10 +1757,14 @@ runTactical fc env tm = do tm' <- eval tm
1713 let decl = TyDecl Ref checked
1757 let decl = TyDecl Ref checked
1714 ctxt' = addCtxtDef n decl ctxt
1758 ctxt' = addCtxtDef n decl ctxt
1715 set_context ctxt'
1759 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) :
1717 new_tyDecls e }
1761 new_tyDecls e }
1718 aux <- getAux
1762 aux <- getAux
1719 returnUnit
1763 returnUnit
1764+ | n == tacN "prim__DefineFunction", [decl] <- args
1765+ = do defn <- reifyFunDefn decl
1766+ defineFunction defn
1767+ returnUnit
1720 | n == tacN "prim__Debug", [ty, msg] <- args
1768 | n == tacN "prim__Debug", [ty, msg] <- args
1721 = do let msg' = fromTTMaybe msg
1769 = do let msg' = fromTTMaybe msg
1722 case msg' of
1770 case msg' of
@@ -1978,781 +2026,6 @@ runTac autoSolve ist perhapsFC fn tac
1978 runReflected t = do t' <- reify ist t
2026 runReflected t = do t' <- reify ist t
1979 runTac autoSolve ist perhapsFC fn t'
2027 runTac autoSolve ist perhapsFC fn t'
1980
2028
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−
2756elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2029elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2757elaboratingArgErr [] err = err
2030elaboratingArgErr [] err = err
2758elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
2031elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
@@ -2823,70 +2096,4 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2823 [] -> e
2096 [] -> e
2824 parts -> ReflectionError errorparts e
2097 parts -> ReflectionError errorparts e
2825
2098
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−
2892solveAll = try (do solve; solveAll) (return ())
2099solveAll = try (do solve; solveAll) (return ())
src/Idris/ElabQuasiquote.hs+2−2
@@ -170,8 +170,8 @@ extractUnquotes n (PUnquote tm)
170 return (PRef (fileFC "(unquote)") n, [(n, tm)])
170 return (PRef (fileFC "(unquote)") n, [(n, tm)])
171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
172 extractUnquotes (n-1) tm
172 extractUnquotes (n-1) tm
173−extractUnquotes n (PRunTactics fc tm)
173+extractUnquotes n (PRunElab fc tm)
174− = fmap (\(tm', ex) -> (PRunTactics fc tm', ex)) $ extractUnquotes n tm
174+ = fmap (\(tm', ex) -> (PRunElab fc tm', ex)) $ extractUnquotes n tm
175extractUnquotes n x = return (x, []) -- no subterms!
175extractUnquotes n x = return (x, []) -- no subterms!
176
176
177
177
src/Idris/Error.hs+1−1
@@ -148,4 +148,4 @@ warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
148warnDisamb ist (PUnquote tm) = warnDisamb ist tm
148warnDisamb ist (PUnquote tm) = warnDisamb ist tm
149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
150warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
150warnDisamb 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
1674 put x2
1674 put x2
1675 PUniverse x1 -> do putWord8 38
1675 PUniverse x1 -> do putWord8 38
1676 put x1
1676 put x1
1677− PRunTactics x1 x2 -> do putWord8 39
1677+ PRunElab x1 x2 -> do putWord8 39
1678− put x1
1678+ put x1
1679− put x2
1679+ put x2
1680 PAs x1 x2 x3 -> do putWord8 40
1680 PAs x1 x2 x3 -> do putWord8 40
1681 put x1
1681 put x1
1682 put x2
1682 put x2
@@ -1809,7 +1809,7 @@ instance Binary PTerm where
1809 return (PUniverse x1)
1809 return (PUniverse x1)
1810 39 -> do x1 <- get
1810 39 -> do x1 <- get
1811 x2 <- get
1811 x2 <- get
1812− return (PRunTactics x1 x2)
1812+ return (PRunElab x1 x2)
1813 40 -> do x1 <- get
1813 40 -> do x1 <- get
1814 x2 <- get
1814 x2 <- get
1815 x3 <- get
1815 x3 <- get
src/Idris/IdrisDoc.hs+1−1
@@ -321,7 +321,7 @@ extractPTermNames (PCoerced p) = extract p
321extractPTermNames (PDisamb _ p) = extract p
321extractPTermNames (PDisamb _ p) = extract p
322extractPTermNames (PUnifyLog p) = extract p
322extractPTermNames (PUnifyLog p) = extract p
323extractPTermNames (PNoImplicits p) = extract p
323extractPTermNames (PNoImplicits p) = extract p
324−extractPTermNames (PRunTactics _ p) = extract p
324+extractPTermNames (PRunElab _ p) = extract p
325extractPTermNames _ = []
325extractPTermNames _ = []
326
326
327-- | Shorter name for extractPTermNames
327-- | Shorter name for extractPTermNames
src/Idris/ParseExpr.hs+9−9
@@ -220,7 +220,7 @@ InternalExpr ::=
220internalExpr :: SyntaxInfo -> IdrisParser PTerm
220internalExpr :: SyntaxInfo -> IdrisParser PTerm
221internalExpr syn =
221internalExpr syn =
222 unifyLog syn
222 unifyLog syn
223− <|> runTactics syn
223+ <|> runElab syn
224 <|> disamb syn
224 <|> disamb syn
225 <|> noImplicits syn
225 <|> noImplicits syn
226 <|> recordType syn
226 <|> recordType syn
@@ -497,16 +497,16 @@ unifyLog syn = do try (lchar '%' *> reserved "unifyLog")
497
497
498{- | Parses a new-style tactics expression
498{- | Parses a new-style tactics expression
499RunTactics ::=
499RunTactics ::=
500− '%' 'runTactics' SimpleExpr
500+ '%' 'runElab' SimpleExpr
501 ;
501 ;
502-}
502-}
503−runTactics :: SyntaxInfo -> IdrisParser PTerm
503+runElab :: SyntaxInfo -> IdrisParser PTerm
504−runTactics syn = do try (lchar '%' *> reserved "runTactics")
504+runElab syn = do try (lchar '%' *> reserved "runElab")
505− fc <- getFC
505+ fc <- getFC
506− tm <- simpleExpr syn
506+ tm <- simpleExpr syn
507− i <- get
507+ i <- get
508− return $ PRunTactics fc tm
508+ return $ PRunElab fc tm
509− <?> "new-style tactics expression"
509+ <?> "new-style tactics expression"
510
510
511{- | Parses a disambiguation expression
511{- | Parses a disambiguation expression
512Disamb ::=
512Disamb ::=
src/Idris/Reflection.hs+883−3
@@ -1,10 +1,22 @@
1−{-|
1+{-| Code related to Idris's reflection system. This module contains
2−Handy tools for doing reflection.
2+quoters and unquoters along with some supporting datatypes.
3-}
3-}
4+{-# LANGUAGE PatternGuards #-}
5+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4module Idris.Reflection where
6module Idris.Reflection where
5
7
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)
6import Idris.Core.TT
15import Idris.Core.TT
16+
7−import Idris.AbsSyntaxTree (PArg'(..), PArg, PTerm(Placeholder))
17+import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),
18+ PTerm(..), initEState, pairCon, pairTy)
19+import Idris.Delaborate (delab)
8
20
9data RArg = RExplicit { argName :: Name, argTy :: Raw }
21data RArg = RExplicit { argName :: Name, argTy :: Raw }
10 | RImplicit { argName :: Name, argTy :: Raw }
22 | RImplicit { argName :: Name, argTy :: Raw }
@@ -16,3 +28,871 @@ rArgToPArg :: RArg -> PArg
16rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
28rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
17rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
29rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
18rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder
30rArgToPArg (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 @@
1foo
1foo
2−
test/effects001/expected+1−1
@@ -1,4 +1,4 @@
1−["HELLO!!!\n", "WORLD!!!\n", ""]
1+["HELLO!!!", "WORLD!!!", ""]
23
23
315
315
4Answer: 99
4Answer: 99
test/io001/expected+1
@@ -13,4 +13,5 @@ World!
133
133
144
144
15Last line
15Last line
16+
16---
17---
test/io001/test004.idr+1−1
@@ -13,7 +13,7 @@ dumpFile fn = do { h <- openFile fn Read
13 x <- feof h
13 x <- feof h
14 return (not x) })
14 return (not x) })
15 (do { l <- fread h
15 (do { l <- fread h
16− putStr l })
16+ putStrLn l })
17 closeFile h }
17 closeFile h }
18
18
19main : IO ()
19main : IO ()
test/runtest.pl+3−2
@@ -10,10 +10,11 @@ my @idrOpts = ();
10
10
11sub sandbox_path {
11sub sandbox_path {
12 my ($test_dir,) = @_;
12 my ($test_dir,) = @_;
13− my $sandbox = abs_path("$test_dir/../../.cabal-sandbox/bin");
13+ my $sandbox = "$test_dir/../../.cabal-sandbox/bin";
14
14
15 if ( -d $sandbox ) {
15 if ( -d $sandbox ) {
16− return "PATH=\"$sandbox:$PATH\"";
16+ my $sandbox_abs = abs_path($sandbox);
17+ return "PATH=\"$sandbox_abs:$PATH\"";
17 } else {
18 } else {
18 return "";
19 return "";
19 }
20 }
test/tactics001/Tactics.idr+10−10
@@ -1,6 +1,6 @@
1module Tactics
1module Tactics
2
2
3−import Language.Reflection.Tactical
3+import Language.Reflection.Elab
4
4
5import Data.Vect
5import Data.Vect
6
6
@@ -18,24 +18,24 @@ refl t x = RApp (RApp (Var (UN "Refl")) t) x
18plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
18plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
19plusZeroRightNeutralNew Z = Refl
19plusZeroRightNeutralNew Z = Refl
20plusZeroRightNeutralNew (S k) =
20plusZeroRightNeutralNew (S k) =
21− %runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
21+ %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
22− fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
22+ fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
23− solve)
23+ solve)
24
24
25plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
25plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
26plusSuccRightSuccNew Z k = Refl
26plusSuccRightSuccNew Z k = Refl
27plusSuccRightSuccNew (S j) k =
27plusSuccRightSuccNew (S j) k =
28− %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
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")))))
29+ fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
30− solve)
30+ solve)
31
31
32-- Test that side effects in new tactics work
32-- Test that side effects in new tactics work
33
33
34mkDecl : ()
34mkDecl : ()
35−mkDecl = %runTactics (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
35+mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
36 [Implicit (UN "z") `(Nat)]
36 [Implicit (UN "z") `(Nat)]
37 `(Vect ~(Var (UN "z")) ())
37 `(Vect ~(Var (UN "z")) ())
38− fill `(() : ())
38+ fill `(() : ())
39− solve)
39+ solve)
40
40
41repUnit = pure ()
41repUnit = pure ()