git.iko.soy/Idris-dev
on master help sign in
Fixes #1233 by spinning out content into separate repositories:
ea0ea47Jan de Muijnck-Hughes
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