ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
Code Issues Projects Releases Wiki Activity

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

Browse Source 
Conflicts:
	src/Idris/Elab/Term.hs
This commit is contained in:
Edwin Brady 2015-04-16 11:38:37 +01:00
commit 370939badd
56 changed files with 1355 additions and 3823 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

254
contribs/gtksourceview-2.0-language-spec/idris.lang
View File

@ -1,254 +0,0 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Author: Dominic Mulligan
Copyright (C) 2012 Dominic Mulligan <dominic.p.mulligan@gmail.com>
Lexemes taken from src/Idris/Parser.hs.
Based on the gtksourceview-2.0 Haskell style by:
Authors: Duncan Coutts, Anders Carlsson
Copyright (C) 2004, 2007 Duncan Coutts <duncan@haskell.org>
Copyright (C) 2004 Anders Carlsson <andersca@gnome.org>
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Library General Public
License as published by the Free Software Foundation; either
version 2 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Library General Public License for more details.
You should have received a copy of the GNU Library General Public
License along with this library; if not, write to the
Free Software Foundation, Inc., 59 Temple Place - Suite 330,
Boston, MA 02111-1307, USA.
-->
<language id="idris" _name="Idris" version="2.0" _section="Sources">
<metadata>
<property name="mimetypes">text/x-idris</property>
<property name="globs">*.idr</property>
</metadata>
<styles>
<style id="preprocessor" _name="Preprocessor" map-to="def:preprocessor"/>
<style id="comment" _name="Comment" map-to="def:comment"/>
<style id="variable" _name="Variable" />
<style id="symbol" _name="Symbol" />
<style id="keyword" _name="Keyword" map-to="def:keyword"/>
<style id="tactic" _name="Tactic" map-to="def:keyword"/>
<style id="type" _name="Data Type" map-to="def:type"/>
<style id="string" _name="String" map-to="def:string"/>
<style id="character" _name="Character" map-to="def:character"/>
<style id="char-escape" _name="Escaped Character" map-to="def:special-char"/>
<style id="decimal" _name="Decimal" map-to="def:decimal"/>
<style id="float" _name="Float" map-to="def:floating-point"/>
</styles>
<definitions>
<define-regex id="symbolchar">[!#$%&amp;*+./&gt;=&lt;?@:\\^|~-]</define-regex>
<context id="line-comment" style-ref="comment" end-at-line-end="true" class="comment" class-disabled="no-spell-check">
<start>(?&lt;!\%{symbolchar})--+(?!\%{symbolchar})</start>
<include>
<context ref="def:in-comment"/>
<context ref="haddock:line-paragraph"/>
<context ref="haddock:directive"/>
</include>
</context>
<context id="block-comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
<start>\{-</start>
<end>-\}</end>
<include>
<context ref="def:in-comment"/>
<context ref="haddock:block-paragraph"/>
<context ref="haddock:directive"/>
<context ref="block-comment"/>
</include>
</context>
<context id="variable" style-ref="variable">
<match>\b[a-z_][0-9a-zA-Z_'#]*</match>
</context>
<context id="type-or-constructor" style-ref="type">
<match>\b[A-Z][0-9a-zA-Z._'#]*</match>
</context>
<context id="symbol" style-ref="symbol" extend-parent="false">
<match>\%{symbolchar}+</match>
</context>
<context id="keysymbol" style-ref="keyword">
<prefix>(?&lt;!\%{symbolchar})</prefix>
<suffix>(?!\%{symbolchar})</suffix>
<keyword>\.</keyword>
<keyword>:</keyword>
<keyword>%</keyword>
<keyword>=</keyword>
<keyword>\|</keyword>
<keyword>\</keyword>
<keyword>-&gt;</keyword>
<keyword>@</keyword>
<keyword>~</keyword>
<keyword>=&gt;</keyword>
<keyword>\(\)</keyword>
<keyword>\_\|\_</keyword>
<keyword>\*\*</keyword>
</context>
<define-regex id="escaped-character" extended="true">
\\( # leading backslash
[abfnrtv\\"\'&amp;] | # escaped character
[0-9]+ | # decimal digits
o[0-7]+ | # 'o' followed by octal digits
x[0-9A-Fa-f]+ | # 'x' followed by hex digits
\^[A-Z@\[\\\]^_] | # control character codes
NUL | SOH | STX | ETX | EOT | ENQ | ACK |
BEL | BS | HT | LF | VT | FF | CR | SO |
SI | DLE | DC1 | DC2 | DC3 | DC4 | NAK |
SYN | ETB | CAN | EM | SUB | ESC | FS | GS |
RS | US | SP | DEL # control char names
)
</define-regex>
<context id="string" style-ref="string" end-at-line-end="true" class="string" class-disabled="no-spell-check">
<start>"</start>
<end>"</end>
<include>
<context ref="def:line-continue"/>
<context style-ref="char-escape">
<match>\%{escaped-character}</match>
</context>
</include>
</context>
<context id="char" style-ref="character" end-at-line-end="true">
<start>'</start>
<end>'</end>
<include>
<context style-ref="char-escape" once-only="true">
<match>\%{escaped-character}</match>
</context>
<context once-only="true" extend-parent="false">
<match>.</match>
</context>
<context style-ref="def:error" extend-parent="false">
<match>.</match>
</context>
</include>
</context>
<context id="float" style-ref="float">
<match extended="true">
[0-9]+ \. [0-9]+ ([eE][+-]?[0-9]+)?
| [0-9]+ [eE][+-]?[0-9]+
</match>
</context>
<context id="decimal" style-ref="decimal">
<match>[0-9]+</match>
</context>
<context id="keyword" style-ref="keyword">
<keyword>Set</keyword>
<keyword>case</keyword>
<keyword>class</keyword>
<keyword>data</keyword>
<keyword>default</keyword>
<keyword>do</keyword>
<keyword>record</keyword>
<keyword>foreign</keyword>
<keyword>lib</keyword>
<keyword>link</keyword>
<keyword>include</keyword>
<keyword>hide</keyword>
<keyword>freeze</keyword>
<keyword>access</keyword>
<keyword>logging</keyword>
<keyword>abstract</keyword>
<keyword>public</keyword>
<keyword>private</keyword>
<keyword>namespace</keyword>
<keyword>syntax</keyword>
<keyword>term</keyword>
<keyword>pattern</keyword>
<keyword>params</keyword>
<keyword>import</keyword>
<keyword>using</keyword>
<keyword>in</keyword>
<keyword>infix</keyword>
<keyword>infixl</keyword>
<keyword>infixr</keyword>
<keyword>prefix</keyword>
<keyword>instance</keyword>
<keyword>let</keyword>
<keyword>module</keyword>
<keyword>of</keyword>
<keyword>if</keyword>
<keyword>else</keyword>
<keyword>then</keyword>
<keyword>where</keyword>
<keyword>with</keyword>
<keyword>type</keyword>
<keyword>proof</keyword>
<keyword>tactics</keyword>
<keyword>static</keyword>
<keyword>impossible</keyword>
<keyword>total</keyword>
<keyword>assert_total</keyword>
</context>
<context id="tactic" style-ref="tactic">
<keyword>rewrite</keyword>
<keyword>exact</keyword>
<keyword>intros</keyword>
<keyword>intro</keyword>
<keyword>refine</keyword>
<keyword>trivial</keyword>
<keyword>focus</keyword>
<keyword>try</keyword>
<keyword>compute</keyword>
<keyword>solve</keyword>
<keyword>attack</keyword>
<keyword>Refl</keyword>
<keyword>state</keyword>
<keyword>term</keyword>
<keyword>undo</keyword>
<keyword>qed</keyword>
<keyword>abandon</keyword>
</context>
<context id="body">
<include>
<context ref="line-comment"/>
<context ref="block-comment"/>
<context ref="keyword"/>
<context ref="tactic" />
<context ref="variable"/>
<context ref="type-or-constructor"/>
<context ref="keysymbol"/>
<context ref="symbol"/>
<context ref="string"/>
<context ref="char"/>
<context ref="float"/>
<context ref="decimal"/>
</include>
</context>
<context id="idris" class="no-spell-check">
<include>
<context ref="c:if0-comment"/>
<context ref="c:include"/>
<context ref="c:preprocessor"/>
<context ref="body"/>
</include>
</context>
</definitions>
</language>

100
contribs/idriscasesplit.vim
View File

@ -1,100 +0,0 @@
function IdrisReload()
let file = expand("%")
let tc = system("idris --client :l " . file)
if (! (tc is ""))
echo tc
endif
return tc
endfunction
function IdrisShowType()
w
let word = expand("<cword>")
let tc = IdrisReload()
if (! (tc is ""))
echo tc
else
let ty = system("idris --client :t " . word)
echo ty
endif
return tc
endfunction
function IdrisCaseSplit()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let tc = IdrisReload()
if (tc is "")
let fn = "idris --client :cs! " . cline . " " . word
let result = system(fn)
if (! (result is ""))
echo result
else
e
call winrestview(view)
endif
endif
endfunction
function IdrisMakeWith()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let tc = IdrisReload()
if (tc is "")
let fn = "idris --client :mw! " . cline . " " . word
let result = system(fn)
if (! (result is ""))
echo result
else
e
call winrestview(view)
call search("_")
endif
endif
endfunction
function IdrisAddClause()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let tc = IdrisReload()
if (tc is "")
let fn = "idris --client :ac! " . cline . " " . word
let result = system(fn)
if (! (result is ""))
echo result
else
e
call winrestview(view)
call search(word)
endif
endif
endfunction
function IdrisEval()
let tc = IdrisReload()
if (tc is "")
let expr = input ("Expression: ")
let fn = "idris --client '" . expr . "'"
let result = system(fn)
echo result
endif
echo ""
endfunction
map <LocalLeader>t :call IdrisShowType()<ENTER>
map <LocalLeader>r :call IdrisReload()<ENTER>
map <LocalLeader>c :call IdrisCaseSplit()<ENTER>
map <LocalLeader>d ?:<ENTER>b:call IdrisAddClause()<ENTER>w
map <LocalLeader>w 0:call IdrisMakeWith()<ENTER>
map <LocalLeader>e :call IdrisEval()<ENTER>

159
contribs/idrislang.sty
View File

@ -1,159 +0,0 @@
%% --------------------------------------------------- [ Idris Styling Package ]
%%
%% A set of LaTeX macros and styling for working with Idris in LaTeX
%%
%% + Provides a listings bindings:
%% + idris :: default ascii
%% + literateidris :: convert ascii maths to math symbols.
%% + Defines a `numbers', `default', and `stdout' listings style.
%% + default :: Uses TT font for code and SF font for comments,
%% and indented by parident.
%% + numbers :: default but with numbers.
%% + beamer :: default minus parindent
%% + stdout :: for formatting stdout.
%% + Defines a `code' environment for typesetting idris.
%% + \begin{code}[...] ... \end{code}
%% + Defines an input command for externally defined idris files.
%% + \inputIdrisListing[...]{file.idr}
%% + Provides definitions (from Idris Compiler) for pretty-printing Idris
%% code using Fancy Verbatim and colour commands.
%% + Sets commandchars for latex commands.
%% + Defines commands typesetting the name Idris.
%% + \Idris{}
%% + \idris{}
%%
%% Options:
%% - literate :: turn on literate idris for code environments.
%%
%% ----------------------------------------------------------- [ Begin Package ]
\ProvidesPackage{idrislang}
\RequirePackage{ifthen}
\RequirePackage{xcolor}
\RequirePackage{fancyvrb}
\RequirePackage{listings}
\RequirePackage{xspace}
\RequirePackage{textcomp}
\RequirePackage{setspace}
%% ----------------------------------------------------------------- [ Options ]
\newboolean{literate}
\setboolean{literate}{false}
\DeclareOption{literate}{%
\setboolean{literate}{true}
}
\ProcessOptions\relax
%% ---------------------------------------------------------------- [ Commands ]
\newcommand{\Idris}{\textsc{Idris}\xspace}
\newcommand{\idris}{\textsc{Idris}\xspace}
\newcommand{\IdrisLineSpacing}{\singlespacing}
%% ---------------------------------------------------------- [ Color Commands ]
\newcommand{\IdrisData}[1]{\textcolor{red}{#1}}
\newcommand{\IdrisType}[1]{\textcolor{blue}{#1}}
\newcommand{\IdrisBound}[1]{\textcolor{magenta}{#1}}
\newcommand{\IdrisFunction}[1]{\textcolor{green}{#1}}
\newcommand{\IdrisKeyword}[1]{{\underline{#1}}}
\newcommand{\IdrisImplicit}[1]{{\itshape \IdrisBound{#1}}}
\fvset{commandchars=\\\{\}}
%% --------------------------------------------------- [ Define Idris Listings ]
\lstdefinelanguage{idris}{%
sensitive,%
%% ----------------------------------------------------------- [ Default Style ]
xleftmargin=1.5em,
tabsize=2,
upquote=true,
basicstyle=\ttfamily,
flexiblecolumns=false,
commentstyle=\footnotesize\sffamily,
%% ---------------------------------------------------------------- [ Keywords ]
%% From Idris Parser and idris-mode and vimscript
keywords={%
abstract, attack, case, compute, do, dsl, else, exact, focus, if,
import, in, infix, infixl, infixr, instance, intros, module,
mutual, namespace, of, let, parameters, partial, pattern, prefix,
private, public, refine, rewrite, solve, syntax, term, then,
total, trivial, try, using, where, with
},
%% ------------------------------------------------------- [ Prelude Functions ]
morekeywords={%
class, data, instance, record, dsl, postulate, default,
lambda, variable, index_first, index_next
},
%% ---------------------------------------------------------------- [ Comments ]
morecomment=[l]--,%
morecomment=[n]{\{-}{-\}}
}[keywords,comments,strings]%
%% ---------------------------------------- [ Define Idris with Literate Stuff ]
\lstdefinelanguage{literateidris}[]{idris}{
literate= {+}{{$+$}}1
{/}{{$/$}}1
{*}{{$*$}}1
{=}{{$=$}}1
{>}{{$>$}}1
{<}{{$<$}}1
{\\}{{$\lambda$}}1
{\\\\}{{\char`\\\char`\\}}1
{->}{{$\rightarrow$}}2
{>=}{{$\geq$}}2
{<-}{{$\leftarrow$}}2
{<=}{{$\leq$}}2
{=>}{{$\Rightarrow$}}2
{==}{{$\equiv$}}2
{\ .}{{$\circ$}}2
{\ .\ }{{$\circ$}}2
{>>}{{>>}}2
{>>=}{{>>=}}2
{|}{{$\mid$}}1,
}
%% -------------------------------------------------- [ Default Listings Style ]
\lstdefinestyle{default}{%
basicstyle=\ttfamily\normalsize,
}
\lstdefinestyle{numbers}{%
numbers=left,
numbersep=10pt,
numberstyle=\footnotesize\sffamily,
frame=leftline
}
\lstdefinestyle{stdout}{%
xleftmargin=\parindent,
tabsize=2,
basicstyle=\ttfamily\normalsize,
showstringspaces=false,
escapechar=^
}
\lstdefinestyle{beamer}{%
basicstyle=\ttfamily\normalsize,
escapechar=^
}
%% ------------------------------------------------------ [ A Code Environment ]
%% Replicate the existence of literate haskell code environments,
%% option to make pretty with numbers.
\lstnewenvironment{code}[1][]
{\ifthenelse{\boolean{literate}}{%
\lstset{language=literateidris}}{%
\lstset{language=idris}}
\IdrisLineSpacing{}
}{}
%% ---------------------------------------------------------- [ Input Listings ]
%% Command to add externally defined Idris code to the document.
\newcommand{\inputIdrisListing}[2][]{%
\begingroup
\ifthenelse{\boolean{literate}}{%
\lstset{language=literateidris}}{%
\lstset{language=idris}}
\lstinputlisting[#1]{#2}
\endgroup
}
\endinput
%% --------------------------------------------------------------------- [ EOF ]

15
contribs/lib/SQLite3/Makefile
View File

@ -1,15 +0,0 @@
# This makefile compiles the project
#
.PHONY: all
sqltest : testunit.idr Sqlite3.idr sqlite3api.o
idris testunit.idr -o sqltest
sqlite3api.o : sqlite3api.c
gcc -I . -c sqlite3api.c
sqlite3api.so: sqlite3api.c
gcc -I . -fPIC -o sqlite3api.so -shared sqlite3api.c
all : sqltest sqlite3api.o

278
contribs/lib/SQLite3/Sqlexpr.idr
View File

@ -1,278 +0,0 @@
module Sqlexpr
import Prelude.List
-----------------------------------------------------------------------------
-- |
-- Module : sqlexpr
-- Copyright : (c) The University of St Andrews, 2012
--
-- Implementations for SQLite query data type.
--
-----------------------------------------------------------------------------
-----------------------------------------------------------
-- | SQL data type
-----------------------------------------------------------
data Value = VInt Int
| VStr String
| VFloat Float
| VCol String
| VNULL
--Perhaps could extend this by adding
-- a dot operator to allow mapping
-- between table and column and
-- comparing different table columns.
data Cond = Equals Value Value
| MkGT Value Value
| MkGTE Value Value
| MkLT Value Value
| MkLTE Value Value
| MkNULL Value
data SelVar = Cols (List String)
| ALL
data ColType = CInt String -- parsed as string "int"
| Varchar String
mutual
data Clause = MkCond Cond
| AND Clause Clause
| OR Clause Clause
| Empty
| MkSQL SQL
data condClause = SET Clause
| WHERE condClause Clause
data Constr = NOTNULL
| UNIQUE Constr
| None
| PRIMARYKEY
| FOREIGNKEY
| CHECK
| DEFAULT
data SQL = SELECT SelVar SQL Clause
| TBL (List String)
| INSERT SQL (List Value)
| INSERTC SQL (List Value) (List Value)
| UPDATE SQL condClause
| CREATE SQL (List (Value, ColType , Constr))
-- remember to remove these funcs later
-- foldr1 : (a -> a -> a) -> List a -> a
-- foldr1 f [x] = x
-- foldr1 f (x::xs) = f x (foldr1 f xs)
-- unwords' : List (List Char) -> List Char
-- unwords' [] = []
-- unwords' ws = (foldr1 addSpace ws)
-- where
-- addSpace : List Char -> List Char -> List Char
-- addSpace w s = w ++ (' ' :: s)
--
--
-- unwords : List String -> String
-- unwords = pack . unwords' . map unpack
-----------------------------------------------------------
-- | This function replaces values with question mark
-- following by an index number. It then puts the value
-- replaced, in the list.
-----------------------------------------------------------
valString : List (Maybe (Int, Value)) -> Value -> (String, List (Maybe (Int, Value)))
valString xs (VInt x) = ("?" ++ show (cast (length xs) + 1), xs ++ [Just (cast ((length xs) + 1), (VInt x))])
valString xs (VStr x) = ("?" ++ show (cast (length xs) + 1), xs ++ [Just (cast ((length xs) + 1), (VStr x))])
valString xs (VFloat x) = ("?" ++ show (cast (length xs) + 1), xs ++ [Just (cast ((length xs) + 1), (VFloat x))])
valString xs (VCol n) = (n, xs)
-----------------------------------------------------------
-- | This function calls valString on a list of Values
-- and separates the values by commas.
-----------------------------------------------------------
listVal : List (Maybe (Int, Value)) -> List Value -> (String, List (Maybe (Int, Value)))
listVal xs [] = ("", xs)
listVal xs (v::vs) = let (str, newxs) = (valString xs v) in
let (str', newxs') = listVal newxs vs in
(unwords (intersperse "," (words (str) ++ words (str'))), newxs')
-----------------------------------------------------------
-- | Parses the type of column to be created.
-----------------------------------------------------------
getColType : List (Maybe (Int, Value)) -> ColType -> (String, List (Maybe (Int, Value)))
getColType xs (CInt x) = ("int", xs)
getColType xs (Varchar str) = ("varchar(255)", xs)
-----------------------------------------------------------
-- | CREATE Constraints
-----------------------------------------------------------
getConstr : List (Maybe (Int, Value)) -> Constr -> (String, List (Maybe (Int, Value)))
getConstr xs (NOTNULL) = ("NOT NULL", xs)
getConstr xs (UNIQUE constr) = ("NOT NULL UNIQUE", xs)
getConstr xs (PRIMARYKEY) = ("PRIMARY KEY", xs)
getConstr xs (FOREIGNKEY) = ("FOREIGN KEY", xs)
getConstr xs (CHECK) = ("CHECK", xs)
getConstr xs (DEFAULT) = ("DEFAULT", xs)
getConstr xs (None) = ("", xs)
putBrackets : String -> String
putBrackets str = "(" ++ str ++ ")"
-----------------------------------------------------------
-- | Used to detect a complex type in a nested SQLite query
-- This function is used for bracketing the nested queries.
-----------------------------------------------------------
complexType : SQL -> Bool
complexType (TBL tbl) = False
complexType (SELECT vars sql c) = True
-----------------------------------------------------------
-- | Used in CREATE
-----------------------------------------------------------
listValType : List (Maybe (Int, Value)) -> List (Value, ColType , Constr) -> (String, List (Maybe (Int, Value)))
listValType xs [] = ("", xs)
listValType xs ((val, types, constr) :: vs) =
let (str , newxs) = valString xs val in
let (str' , newxs') = getColType newxs types in
let (str'', newxs'') = getConstr newxs' constr in
let (finalstr, finalxs) = listValType newxs'' vs in
(unwords (intersperse " " (words str ++ words str' ++ words str'' ++ words finalstr)) , finalxs)
-----------------------------------------------------------
-- | Evaluates a conditional WHERE clause
-----------------------------------------------------------
evalCond : List (Maybe (Int, Value)) -> Cond -> (String, List (Maybe (Int, Value)))
evalCond xs (Equals val1 val2) = let (restring , newxs ) = valString xs val1 in
let (restring2, newxs') = valString newxs val2 in
(restring ++ " = " ++ restring2, newxs')
evalCond xs (MkGT val1 val2) = let (restring , newxs ) = valString xs val1 in
let (restring2, newxs') = valString newxs val2 in
(restring ++ " > " ++ restring2, newxs')
evalCond xs (MkGTE val1 val2) = let (restring , newxs ) = valString xs val1 in
let (restring2, newxs') = valString newxs val2 in
(restring ++ " >= " ++ restring2, newxs')
evalCond xs (MkLT val1 val2) = let (restring , newxs ) = valString xs val1 in
let (restring2, newxs') = valString newxs val2 in
(restring ++ " < " ++ restring2, newxs')
evalCond xs (MkLTE val1 val2) = let (restring , newxs ) = valString xs val1 in
let (restring2, newxs') = valString newxs val2 in
(restring ++ " =< " ++ restring2, newxs')
evalCond xs (MkNULL val) = let (restring , newxs ) = valString xs val in
(restring ++ " IS NULL " , newxs)
-----------------------------------------------------------
-- | Evaluates clauses
-- Supports WHERE Clause
-- WHERE Clause And Another-Clause
-- WHERE Clause Or Another-Clause
-----------------------------------------------------------
clauseString : List (Maybe (Int, Value)) -> Clause -> (String, List (Maybe (Int, Value)))
clauseString xs (Empty) = ("" , []) -- No condition
clauseString xs (MkCond cond') = let (condstr, newxs) = evalCond xs cond' in
(condstr , newxs)
clauseString xs (AND c1 c2) = let (clausestr, newxs) = clauseString xs c1 in
let (clausestr2, newxs') = clauseString newxs c2 in
(clausestr ++ " AND " ++ clausestr2 , newxs')
clauseString xs (OR c1 c2) = let (clausestr, newxs) = clauseString xs c1 in
let (clausestr2, newxs') = clauseString newxs c2 in
(clausestr ++ " OR " ++ clausestr2 , newxs')
-----------------------------------------------------------
-- | Evaluates conditional clauses.
-----------------------------------------------------------
condClauseStr : List (Maybe (Int, Value)) -> condClause -> (String, List (Maybe (Int, Value)))
condClauseStr xs (SET setcl) = let (condstr, newxs) = clauseString xs setcl in
(" SET " ++ condstr, newxs)
condClauseStr xs (WHERE setcl1 setcl2) = let (condstr, newxs) = condClauseStr xs setcl1 in
let (condstr', newxs') = clauseString newxs setcl2 in
( condstr ++ " WHERE " ++ condstr', newxs')
-----------------------------------------------------------
-- | Evaluates queries by calling the other functions
-- on each part of the query
-----------------------------------------------------------
evalSQL : List (Maybe (Int, Value)) -> SQL -> (String, List (Maybe (Int, Value)))
-- SELECT data from tbl1 where num > (SELECT num from tbl1 where num = 24)
-- evalSQL [] ((SELECT ALL)(TBL "tbl")(MkSQL ((SELECT ALL) (TBL "tbl")(MkCond (VCol "))))
-- NTBF
--clauseString xs (MkSQL sql) = (evalSQL xs sql)
-- Separate list of tables
-- For complex type, return list returned by evalSQL
-- And add brackets
evalSQL xs (TBL tbl) = (unwords (intersperse "," ( tbl)), xs)
evalSQL xs (SELECT vars sql' c) =
let (sqlstring, newxs) = evalSQL xs sql' in
let (csstring, newxs') = clauseString newxs c in
case c of
Empty => case vars of
ALL => if complexType sql'
then ("SELECT " ++ "*" ++ " FROM " ++
putBrackets sqlstring ++ csstring, newxs)
else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring ++
csstring, newxs')
Cols selvar => if complexType sql'
then ("SELECT " ++ unwords selvar ++
" FROM " ++ putBrackets sqlstring ++ csstring, newxs)
else ("SELECT " ++ unwords selvar ++ " FROM " ++ sqlstring ++
csstring, newxs')
_ => case vars of
ALL => if complexType sql'
then ("SELECT " ++ "*" ++ " FROM " ++
" WHERE " ++ csstring, newxs)
else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring
++ " WHERE " ++ csstring, newxs')
Cols selvar => if complexType sql'
then ("SELECT " ++ (unwords selvar) ++ " FROM " ++
putBrackets sqlstring ++ " WHERE " ++
csstring , newxs)
else ("SELECT " ++ (unwords selvar) ++ " FROM " ++ sqlstring ++
" WHERE " ++ csstring, newxs')
evalSQL xs (INSERT sql vals) = let (tblname, newvals) = evalSQL xs sql in
let (str, newxs ) = listVal newvals vals in
("INSERT INTO " ++ tblname ++ " VALUES (" ++ str ++ ")", newxs)
evalSQL xs (INSERTC sql cols vals) = let (tblname, newvals) = evalSQL xs sql in
let (strcol, newcol) = listVal newvals cols in
let (strval, newcolval) = listVal newcol vals in
("INSERT INTO " ++ tblname ++ "(" ++ strcol ++ ")" ++ "VALUES (" ++ strval ++ ")", newcolval)
evalSQL xs (UPDATE sql cl) = let (tblname, newxs) = evalSQL xs sql in
let (csstring, newxs') = condClauseStr newxs cl in
("UPDATE " ++ tblname ++ csstring, newxs')
evalSQL xs (CREATE sql details) = let (sqlstring, newxs) = evalSQL xs sql in
let (csstring, newxs') = listValType newxs details in
("CREATE TABLE " ++ sqlstring ++ "(" ++ csstring ++ ")", newxs')

419
contribs/lib/SQLite3/Sqlite3.idr
View File

@ -1,419 +0,0 @@
module Sqlite3
import public Sqlexpr
%lib C "sqlite3"
-- %link C "sqlite3.o"
-- %include C "sqlite3.h"
%link C "sqlite3api.o"
%include C "sqlite3api.h"
-----------------------------------------------------------------------------
-- |
-- Module : sqlite3
-- Copyright : (c) The University of St Andrews, 2012
--
-- Library built on top of FFI supporting basic SQLite C/C++ Interface
-- functions.
--
-----------------------------------------------------------------------------
-- | The types supported by Idris returned by the database functions.
data DBVal = DBInt Int
| DBText String
| DBFloat Float
| DBNull
-- Database pointer
data DBPointer = MkDBPointer Ptr
-- Table pointer
data TBPointer = MkTBPointer Ptr
-- Statement pointer
data StmtPtr = MkStmtPtr Ptr
Table : Type
Table = List (List DBVal)
-- ForMap used in to_list_v1
forM : Applicative f => List a -> (a -> f b) -> f (List b)
forM xs f = (sequence (map f xs))
-- Neater error handling done using DB
data DB a = MkDB (IO (Either String a))
instance Functor DB where
map f (MkDB action) = MkDB (do res <- action
return (map f res))
instance Applicative DB where
pure = MkDB . return . Right
(MkDB f) <*> (MkDB x) = MkDB (do f' <- f
case f' of
Left err => return (Left err)
Right op => x >>= (return . map op))
instance Monad DB where
(MkDB l) >>= k = MkDB (do c <- l
case c of
Left err => return (Left err)
Right v => case k v of
MkDB k' => k')
--return x = MkDB (return (Right x))
fail : String -> DB a
fail err = MkDB (return (Left err))
liftIO : IO a -> DB a
liftIO f = MkDB (do f' <- f
return (Right f'))
ioError : String -> IO a
ioError err = do putStrLn err
return (believe_me ())
runDB : DB a -> IO a
runDB (MkDB f) = do f' <- f
case f' of
Right v => return v
Left str => ioError str
-----------------------------------------------------------------------------
-- | Opens an SQLite database file as specified by the String name argument.
-----------------------------------------------------------------------------
open_db : String -> DB DBPointer
open_db name = do x <- liftIO (foreign FFI_C "sqlite3_open_idr" (String -> IO Ptr) name)
return (MkDBPointer x)
-----------------------------------------------------------------------------
-- | Destructor for the DBPointer.
-----------------------------------------------------------------------------
close_db : DBPointer -> DB Int
close_db (MkDBPointer pointer) = liftIO (foreign FFI_C "sqlite3_close_idr" (Ptr -> IO Int) pointer)
-----------------------------------------------------------------------------
-- | Wrapper around prepare, step and finalize.
-----------------------------------------------------------------------------
exec_db : DBPointer -> String -> DB Int
exec_db (MkDBPointer pointer) stmt = do
x <- liftIO (foreign FFI_C "sqlite3_exec_idr" (Ptr -> String -> IO Int) pointer stmt)
if (x == 1)
then fail "Could not execute."
else return x
-----------------------------------------------------------------------------
-- | Executes a prepared query. Use of this version is recommended.
-----------------------------------------------------------------------------
exec_db_v2 : StmtPtr -> DB Int
exec_db_v2 (MkStmtPtr pointer) = do
x <- liftIO (foreign FFI_C "exec_db" (Ptr -> IO Int) pointer)
if (x == 21)
then fail "No data returned."
else return x
-----------------------------------------------------------------------------
-- | Returns the error stored in the buffer by exec_db function.
-- This function can only be used with exec_db and get_table.
-- Only these functions store any occured error in the buffer array.
-----------------------------------------------------------------------------
get_error : DBPointer -> IO String
get_error (MkDBPointer pointer) = foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer
-----------------------------------------------------------------------------
-- | Compiles the query inot a byte-code program in order to execute it.
-- Returns a pointer to a Statement pointer on a successful call.
-- Returns a null pointer on a failure.
-----------------------------------------------------------------------------
prepare_db : DBPointer -> String -> DB StmtPtr
prepare_db (MkDBPointer pointer) cmd = do
result <- liftIO (foreign FFI_C "sqlite3_prepare_idr" (Ptr -> String -> IO Ptr) pointer cmd)
flag <- liftIO (nullPtr result)
if flag
then fail "Error occured while preparing"
else return (MkStmtPtr result)
-----------------------------------------------------------------------------
-- | Returns the error stored in the buffer by exec_db function.
-- This function can only be used with exec_db and get_table.
-- Only these functions store any occured error in the buffer array.
-----------------------------------------------------------------------------
step_db : StmtPtr -> DB Int
step_db (MkStmtPtr pointer)= do
x <- liftIO (foreign FFI_C "sqlite3_step_idr" (Ptr -> IO Int) pointer)
if (x == 101)
then fail "SQLITE_DONE"
else return x
-----------------------------------------------------------------------------
-- | Deletes a prepared statement. This function must be called after
-- prepare function.
-----------------------------------------------------------------------------
finalize_db : StmtPtr -> DB Int
finalize_db (MkStmtPtr pointer) = do
x <- liftIO (foreign FFI_C "sqlite3_finalize_idr" (Ptr -> IO Int) pointer)
if (x /= 0)
then fail "Could not finalize"
else return x
-----------------------------------------------------------------------------
-- | Resets a prepared statement pointer back to its initial state.
-----------------------------------------------------------------------------
reset_db : StmtPtr -> DB Int
reset_db (MkStmtPtr pointer) = do
x <- liftIO (foreign FFI_C "sqlite3_reset_idr" (Ptr -> IO Int) pointer)
if (x /= 0)
then fail "Could not reset"
else return x
-----------------------------------------------------------------------------
-- | These routines obtain column information.
-----------------------------------------------------------------------------
column_count : DBPointer -> IO (Either String Int)
column_count (MkDBPointer pointer) = do
x <- foreign FFI_C "sqlite3_column_count_idr" (Ptr -> IO Int) pointer
return $ if (x == 0)
then Left "No Data"
else (Right x)
column_name : DBPointer -> Int -> IO String
column_name (MkDBPointer pointer) iCol =
foreign FFI_C "sqlite3_column_name_idr" (Ptr -> Int -> IO String) pointer iCol
column_decltype : DBPointer -> Int -> IO String
column_decltype (MkDBPointer pointer) iCol =
foreign FFI_C "sqlite3_column_decltype_idr" (Ptr -> Int -> IO String) pointer iCol
column_bytes : DBPointer -> Int -> IO Int
column_bytes (MkDBPointer pointer) iCol =
foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO Int) pointer iCol
column_blob : DBPointer -> Int -> IO String
column_blob (MkDBPointer pointer) iCol =
foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO String) pointer iCol
column_text : DBPointer -> Int -> IO String
column_text (MkDBPointer pointer) iCol =
foreign FFI_C "sqlite3_column_text_idr" (Ptr -> Int -> IO String) pointer iCol
column_Int : DBPointer -> Int -> IO Int
column_Int (MkDBPointer pointer) iCol =
foreign FFI_C "sqlite3_column_int_idr" (Ptr -> Int -> IO Int) pointer iCol
-----------------------------------------------------------------------------
-- | These routines support some of SQLite backup functions.
-----------------------------------------------------------------------------
backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer
backup_init (MkDBPointer des_pointer) destName (MkDBPointer src_pointer) srcName =
do x <- foreign FFI_C "sqlite3_backup_init_idr" (Ptr -> String -> Ptr -> String -> IO Ptr)
des_pointer destName src_pointer srcName
return (MkDBPointer x)
backup_step : DBPointer -> Int -> IO Int
backup_step (MkDBPointer pointer) nPage =
foreign FFI_C "sqlite3_backup_step_idr" (Ptr -> Int -> IO Int) pointer nPage
backup_finish : DBPointer -> IO Int
backup_finish (MkDBPointer pointer) =
foreign FFI_C "sqlite3_backup_finish_idr" (Ptr -> IO Int) pointer
backup_remaining : DBPointer -> IO Int
backup_remaining (MkDBPointer pointer) =
foreign FFI_C "sqlite3_backup_remaining_idr" (Ptr -> IO Int) pointer
-----------------------------------------------------------------------------
-- | Use of this interface is not recommended.
-- This function returns a result table. The functions num_row and num_col
-- are used to obtain the number of rows and columns.
-- These functions can be used to print the resulting table.
-----------------------------------------------------------------------------
get_table : DBPointer -> String -> DB TBPointer
get_table (MkDBPointer pointer) name = do
x <- liftIO(foreign FFI_C "sqlite3_get_table_idr" (Ptr -> String -> IO Ptr) pointer name)
flag <- liftIO (nullPtr x)
if flag
then do x <- liftIO(get_error_table pointer) ; fail x
else return (MkTBPointer x)
where
get_error_table : Ptr-> IO String
get_error_table pointer = do x <- foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer
return x
free_table : TBPointer -> IO ()
free_table (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_free_table_idr" (Ptr -> IO ()) pointer
return ()
-----------------------------------------------------------------------------
-- | This version of these function obtain the row and column number
-- from the Table struct. These functions are only used with get_table.
-----------------------------------------------------------------------------
num_row : TBPointer -> IO Int
num_row (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row" (Ptr -> IO Int) pointer
return x
num_col : TBPointer -> IO Int
num_col (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col" (Ptr -> IO Int) pointer
return x
-----------------------------------------------------------------------------
-- | This version of these function obtain the row and column number
-- from the Database struct.
-----------------------------------------------------------------------------
num_row_v2 : DBPointer -> IO Int
num_row_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row_v2" (Ptr -> IO Int) pointer
return x
num_col_v2 : DBPointer -> IO Int
num_col_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col_v2" (Ptr -> IO Int) pointer
return x
-----------------------------------------------------------------------------
-- | This function prints the result of a query by checking the type
-- of each value returned, it then calls the appropriate function.
-- Ther result is one of the DBVal variants.
-----------------------------------------------------------------------------
get_data : DBPointer -> Int -> Int -> IO DBVal
get_data (MkDBPointer pointer) row col = do
ty <- get_data_type pointer row col
helper ty
where get_data_type : Ptr ->Int -> Int -> IO Int
get_data_type pointer row col =
foreign FFI_C "sqlite3_get_data_type" (Ptr -> Int -> Int -> IO Int) pointer row col
get_data_val_int : Ptr -> Int -> IO Int
get_data_val_int pointer col =
foreign FFI_C "sqlite3_get_val_int" (Ptr -> Int -> IO Int) pointer col
get_data_val_text : Ptr -> Int -> IO String
get_data_val_text pointer col =
foreign FFI_C "sqlite3_get_val_text" (Ptr -> Int -> IO String) pointer col
get_data_val_float : Ptr -> Int -> IO Float
get_data_val_float pointer col =
foreign FFI_C "sqlite3_get_float" (Ptr -> Int -> IO Float) pointer col
helper : Int -> IO DBVal
helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)
helper 2 = do i <- get_data_val_float pointer col ; return (DBFloat i)
helper 3 = do i <- get_data_val_text pointer col; return (DBText i)
helper _ = return DBNull
-----------------------------------------------------------------------------
-- | This function makes use of get_data to get all the result.
-----------------------------------------------------------------------------
toList_v1 : DBPointer -> DB Table
toList_v1 db = do nbR <- liftIO (num_row_v2 db)
nmC <- liftIO (num_col_v2 db)
res <- liftIO $ forM [0..(nbR-1)] $ \ i =>
forM [0..(nmC-1)] $ \ j => get_data db i j
return (the (List (List DBVal)) res)
strcat : String -> String-> String
strcat str1 str2 = str1 ++ str2
-----------------------------------------------------------------------------
-- | This version of toList retunrs result from get_table
-- This could be removed if not needed in the future.
-----------------------------------------------------------------------------
--toList_v2 : String -> String -> DBPointer -> DB Table
--toList_v2 name stmt x = do
-- ptr <- (get_table x (stmt))
-- nbR <- liftIO (num_row ptr)
-- nmC <- liftIO (num_col ptr)
-- res <- forM [0..(nbR-1)] (\ i =>
-- forM [0..(nmC-1)] (\ j =>
-- liftIO(get_data x name i j)
--
-- )
-- )
-- liftIO (free_table ptr)
-- return res
-----------------------------------------------------------------------------
-- | These routines support binding the types supported by Idris.
-- These return a pointer to statement pointer since we want to allow
-- binding multiple values by implementing a recursive function.
-----------------------------------------------------------------------------
bind_int : StmtPtr -> Int -> Int -> DB StmtPtr
bind_int (MkStmtPtr pointer) indexval val = do
x <- liftIO (foreign FFI_C "sqlite3_bind_int_idr" (Ptr -> Int -> Int -> IO Ptr) pointer indexval val)
flag <- liftIO (nullPtr x)
if flag
then fail "Could not bind int."
else return (MkStmtPtr x)
bind_float : StmtPtr -> Int -> Float -> DB StmtPtr
bind_float (MkStmtPtr pointer) indexval val = do
x <- liftIO (foreign FFI_C "sqlite3_bind_float_idr" (Ptr -> Int -> Float -> IO Ptr) pointer indexval val)
flag <- liftIO (nullPtr x)
if flag
then fail "Could not bind float."
else return (MkStmtPtr x)
bind_text : StmtPtr -> String -> Int -> Int -> DB StmtPtr
bind_text (MkStmtPtr pointer) text indexval lengthval = do
x <- liftIO (foreign FFI_C "sqlite3_bind_text_idr" (Ptr -> String -> Int -> Int -> IO Ptr)
pointer text indexval lengthval)
flag <- liftIO(nullPtr x)
if flag
then fail "Could not bind text."
else return (MkStmtPtr x)
bind_null : StmtPtr -> Int -> DB StmtPtr
bind_null (MkStmtPtr pointer) indexval = do
x <- liftIO (foreign FFI_C "sqlite3_bind_null_idr" (Ptr -> Int -> IO Ptr) pointer indexval)
flag <- liftIO (nullPtr x)
if flag
then fail "Could not bind null."
else return (MkStmtPtr x)
-----------------------------------------------------------------------------
-- | String Length
-----------------------------------------------------------------------------
strlen : String -> DB Int
strlen str = liftIO (foreign FFI_C "strLength" (String -> IO Int) str)
instance Show DBVal where
show (DBInt i) = "Int val: " ++ show i ++ "\n"
show (DBText i) = "Text val: " ++ show i ++ "\n"
show (DBFloat i) = "Float val: " ++ show i ++ "\n"
show (DBNull ) = "NULL"
-----------------------------------------------------------------------------
-- | Multi bind a list of values.
-----------------------------------------------------------------------------
bindMulti : StmtPtr-> List (Maybe (Int, Value)) -> DB StmtPtr
bindMulti pointer [] = return pointer
bindMulti pointer (Nothing :: vs) = bindMulti pointer vs
bindMulti pointer ((Just (indexs, (VInt i)))::vs) =
do x <- bind_int pointer indexs i
bindMulti x vs
bindMulti pointer ((Just (indexs, (VStr s)))::vs) =
do len <- strlen s
x <- bind_text pointer s indexs len
bindMulti x vs
bindMulti pointer ((Just (indexs, (VFloat f)))::vs) =
do x <- bind_float pointer indexs f
bindMulti x vs

BIN
contribs/lib/SQLite3/newdb.db
View File

Binary file not shown.

BIN
contribs/lib/SQLite3/somedb.db
View File

Binary file not shown.

157
contribs/lib/SQLite3/sqlite3.tex
View File

@ -1,157 +0,0 @@
\documentclass[11pt]{article}
\topmargin -1.5cm
\oddsidemargin -0.04cm
\evensidemargin -0.04cm
\textwidth 16.59cm
\textheight 21.94cm
%\pagestyle{empty}
\parskip 7.2pt
\parindent 0pt
\begin{document}
\section{Introduction}
\label{Introduction}
This document provides overview on how the Idris library for SQLite3 works. The code base is written on top of the
SQLite3 C/C++ Interface.
This library supports some features of the low-level library, implemented in a higher level basis.
The library allows making use of queries as data types. The aim of this library is to avoid
SQL injections which are the most common security issues.
To avoid this we have defined a datatype which describes queries.
The queries are written using these data types and parsed as quoted string
while replacing values with \emph{indexed question mark} to be binded with the prepared statement.
This prevents the user from preparing the queries inappropriately by not allowing to pass
any types of values directly to the prepare function. However this is a design choice, the library
does not prevent the user from passing a String directly to the prepare function.
\section{Using the library}
\label{Using the library}
Simple examples have been provided in the \emph{testunit.idr} file.
To open a database, use the open\_db function which takes the filename as a string.
This function implements the sqlite3\_open function.
This function returns a pointer to the database which can be used by other function
to access the database object.
Whether or not an error occurs when it is opened,
resources should be released by passing it to close\_db when it is no longer required.
A query can then be builts using the supported data types.
The library supports limited number of queries at the moment. The supported sql commands are :
\newline
\textbf{SELECT,}
\textbf{INSERT,}
\textbf{UPDATE,}
\textbf{CREATE}
\subsection{Creating Queries}
\label{Creating Queries}
To create a query, use the evalSQL function which takes an empty list and the SQL query.
The routine evaluates the expression recrusively by dividing it into smaller parts,
filling up the list with the received values. For instance the following is a valid query:
let sql = evalSQL [ ] ((SELECT ALL)(TBL ["tbl1"]) (MkCond (MkNULL (VCol "data"))))
\newline
\newline{This will be parsed as :}
\b{“SELECT * FROM tbl1 WHERE data IS NULL “}
The evaluator returns a string and a list of indexed values.
The string part of the query could be parsed to prepare.
\emph{evalSQL} parses the query as a string replacing values with \emph{?} and an index starting from one,
storing them in the list given to it as an argument.
For example:
evalSQL [ ] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL ["tbl1"])
\newline (MkCond(Equals(VCol "num")(VInt 2))))Empty))
is passed to prepare as :
SELECT * FROM tbl1 WHERE data = ?1 AND num = ?2 OR num = ?3
and returns the list as follows:
\newline{(Just (1, VStr "data0")) ,(Just (2, VInt 1)) , (Just (3, VInt 2))}
The values in the list are binded to the statement using bindMulti function.
This function takes the statement pointer returned by prepare and the list returned by evalSQL
and binds the values by calling the appropriate functions.
The function exec\_db\_v2 executes the statement.
Note that the other version of exec\_db implements the sqlite3\_exec() interface which is a wrapper
around sqlite3\_prepare\_v2(), sqlite3\_step(), and sqlite3\_finalize(),
without having to use a lot of code, though the use of this function is not recommended in this case.
The functions finalize\_db and close\_db must be called to clean up the open resources.
To print the result, the function toList\_v1 can be used which takes a DBPointer and returns
the resulting table.
\subsection{More Examples}
\label{More Examples}
Nested expressions are also supported. You could write queries such as :
evalSQL [ ] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL ["tbl1"]) (MkCond (Equals (VCol "num")(VInt 2)))) Empty)
Parsed as :
SELECT data FROM (SELECT num data FROM tbl1 WHERE num = ?1)
Note that in this example, the inner query must include the same column as the outer one otherwise this query will not validate.
\subsection{SQL Data Type}
\label{SQL Data Type}
The SQL Data Types describe the queries that are supported by the library.
The implementation of these datatypes is similar to defining a grammar.
Data type Value consists of Int, String and Float.
The data type can be extended to further support queries.
The evaulator function makes use of smaller function to evaulate parts of the query.
For instance given a SELECT qeury, it calls \emph{evalSQL} to obtain the list of tables,
and clauseString to evaluate the rest of the expression which could include a WHERE clause or could be Empty.
\section{Evaluating Queries}
\label{Evaluating Queries}
The method used here is a divide and conquer manner which divides the query into smaller
parts and deals with each part and puts the results together to return a String representation
of the query and a list of values.
However this could result to a slow type checking process since it needs to go through all
the possibilities to type check. Maybe this can be improved?
\subsection{evalSQL Function}
\label{evalSQL Function}
This is a recursive evaluator which makes a call to itself.
An SQL could consist of a SELECT ALL or Columns followed by another SQL
which could be a nested query or just the name of the table(s).
It then call the appropriate functions to evaluate the query.
It returns the well-quoted String expression and a list of indexed values which are passed to the bind function.
\section{Pointers passed to Idris functions}
\label{Pointers passed to Idris functions}
The library uses FFI. In order to make the pointers passed to each function more explicit,
we have defined them as data types. For instance open\_db takes a String and returns a DBPointer
(Database Pointer) and prepare\_db
takes a DBPointer and returns a StmtPtr(Statemenet Pointer).
Error handling is done using the \emph {DB a} data type which
is either \emph {IO String} indicating an error or \emph{ IO a}.
To test the functions in main, you need to use runDB :
\begin{center}
\centering runDB : DB a $\rightarrow$ IO a
\end{center}
More examples on how to use the functions can be found in \emph{testunit.idr}
\section{Using the C Functions}
\label{Using the C Functions}
The library includes some wrapper functions such as get\_table
and exec\_db. Using these functions mixed with prepare, step or finalize
inappropriately could cause segmentation faults.
Perhaps these functions could be removed from the library if no longer required in the future
since the main purpose of this library is to make use of data types.
However these functionalities could be implemented internally without calling
the C Interface wrapper functions.
\section{Further improving the library}
\label{Further improving the library}
There are many features that could be added to this library. These include adding more useful SQL Commands,
extending the SQL datatype to support more complex queries and possibly improving \emph{evalSQL}
for a faster performance.
Another useful thing to implement is the dot operator(.) which is the member access operator to yield
the value of a field in a table. This enables comparing values in different tables and constructing
more complex queries.
\end{document}

543
contribs/lib/SQLite3/sqlite3api.c
View File

@ -1,543 +0,0 @@
/*
* sqlite3api.c
*
*
* Created by Melissa Farinaz MOZIFIAN on 22/06/2012.
* Copyright 2012. All rights reserved.
*
*/
#include "sqlite3api.h"
// buffer used for storing queries
// Used in high-level functions.
static char sql_query_buffer[2000];
// array used to store the string
//value obtain by get_val_text
unsigned char* array;
/*
open an SQLite database file as
specified by the filename argument.
Returns pointer to DB struct on success
Null on failure.
*/
void* sqlite3_open_idr(const char *filename){
sqlite3 *db;
int res =sqlite3_open(filename,&db);
if(res != SQLITE_OK){
printf("Error occured while opening the databse.");
return NULL;
}
DBinfo *dbi = malloc(sizeof(DBinfo));
dbi->db_ptr = db;
return dbi;
}
/*
Frees the resource and returns 0 on success
*/
int sqlite3_close_idr(void* db){
DBinfo* dbi =(DBinfo*) db;
int res =sqlite3_close(dbi->db_ptr);
if (res == SQLITE_OK){
free(dbi);
return 0;
}
else {
return res;
}
}
/*
SQLite wrapper around sqlite3_prepare_v2(),
sqlite3_step(), and sqlite3_finalize().
This version of exec cannot be used with prepare.
For executing queries, must use the exec_db function.
*/
int sqlite3_exec_idr(void* db, const char *sql)
{
DBinfo* dbi =(DBinfo*) db;
char* err;
int rc;
rc = sqlite3_exec(dbi->db_ptr,sql,NULL, NULL, &err);
if (rc != SQLITE_OK && err != NULL) {
strncpy(dbi->buffer, err, sizeof(dbi->buffer));
sqlite3_free(err);
}
return rc;
}
/*
Gets the error store in the buffer
in the struct. Some certain functions
have the feature to store errors in a buffer.
*/
char* sqlite3_get_error(void* db) {
DBinfo* dbi =(DBinfo*) db;
return dbi->buffer;
}
/*
Compiles the query into a byte-code program
Returns a pointer to the sqlite3_stmt pointer
and stores it in the struct.
*/
void* sqlite3_prepare_idr(void *db,const char *zSql){
sqlite3_stmt* stmt;
const char *tail;
DBinfo* dbi =(DBinfo*) db;
int rec = sqlite3_prepare_v2(dbi->db_ptr,zSql,-1,&stmt,&tail);
dbi ->ppStmt =stmt;
dbi ->Ptr_tail = tail;
if(rec != SQLITE_OK){
return NULL;
}
return dbi;
}
/*
Another wrapper interface that is preserved
for backwards compatibility.
Use of this interface is not recommended.
This was mainly used for testing within the
library.
*/
void* sqlite3_get_table_idr(void* db,
const char *sql){
DBinfo* dbi =(DBinfo*) db;
char* err;
Table* tbl = malloc(sizeof(Table));
tbl->database = dbi;
int res = sqlite3_get_table(dbi->db_ptr,sql,&tbl->table_data,&tbl->num_row,&tbl->num_col,&err);
int array_size = sizeof(&tbl->table_data);
if( res != SQLITE_OK && err != NULL){
strncpy(dbi->buffer, err, sizeof(dbi->buffer));
sqlite3_free(err);
return NULL;
}
tbl -> data_size = array_size;
return tbl;
}
/*
This function executes queries.
This can be used after preparing a query
In case of error or library misuse
it returns 1.
It also calls step in order to obtain
the row and column number and stores them
in the struct. The row number is needed
later on in get_data_type function.
*/
int exec_db(void*p){
DBinfo* dbi =(DBinfo*) p;
int rc, col, row_counter;
const char* col_name;
rc = sqlite3_step(dbi->ppStmt);
if( rc == SQLITE_DONE){
return rc;
}
if(rc == SQLITE_ERROR && rc == SQLITE_MISUSE){
return 1;
}
row_counter =0;
while (rc == SQLITE_ROW) {
rc = sqlite3_step(dbi->ppStmt);
row_counter++;
}
col = sqlite3_column_count(dbi->ppStmt);
dbi->row_count = row_counter;
dbi->col_count = col;
return rc;
}
/*
Returns row number from DB Struct
*/
int sqlite3_get_num_row_v2(void* p){
DBinfo* dbi =(DBinfo*) p;
int row_number =dbi->row_count;
return row_number;
}
/*
Returns column number from DB Struct
*/
int sqlite3_get_num_col_v2(void* p){
DBinfo* dbi =(DBinfo*) p;
int col_number =dbi-> col_count;
return col_number;
}
/*
Another way of obtaining row number
Thought this function gets the value
from Table struct. The value is stored
in the struct after calling get_table.
Using this version is not recommended
unless used with get_table
*/
int sqlite3_get_num_row(void* p){
Table* tbl =(Table*) p;
int row_number =tbl->num_row;
return row_number;
}
/*
Another way of obtaining column number
Thought this function gets the value
from Table struct. The value is stored
in the struct after calling get_table.
Using this version is not recommended
unless used with get_table
*/
int sqlite3_get_num_col(void* p){
Table* tbl =(Table*) p;
int col_number =tbl-> num_col;
return col_number;
}
/*
This routine returns the type of value
and must be called after prepare and exec.
Since exec steps through database to obtain
row number, this function calls reset to
set the pointer to its initial state
and then calls sqlite3_column_type
to get the type
*/
int sqlite3_get_data_type(void* p, int nRow, int nCol){
DBinfo* dbi =(DBinfo*) p;
int rc, type, row_counter;
const char* char_int;
rc = sqlite3_reset(dbi->ppStmt);
rc = sqlite3_step(dbi->ppStmt);
row_counter =0;
while (rc == SQLITE_ROW && row_counter < nRow) {
rc = sqlite3_step(dbi->ppStmt);
row_counter++;
}
type =sqlite3_column_type(dbi->ppStmt, nCol);
return type;
}
/*
Obtains the integer value in a given column
*/
int sqlite3_get_val_int(void* p, int nCol){
DBinfo* dbi =(DBinfo*) p;
int val, col;
val =sqlite3_column_int(dbi->ppStmt, nCol);
return val;
}
/*
Obtains the text value
Need to allocate memory to store the string
Use GC_malloc since Boehm garbage collector
frees the resources .
*/
const unsigned char* sqlite3_get_val_text(void* p,int nCol){
DBinfo* dbi =(DBinfo*) p;
int rc,i, val, counter;
const unsigned char* text_val;
array =(unsigned char *) malloc(1000*sizeof(char));
text_val =sqlite3_column_text(dbi->ppStmt, nCol);
memcpy(array, text_val, strlen(text_val));
return array;
}
float sqlite3_get_float(void* p, int nCol){
DBinfo* dbi =(DBinfo*) p;
double double_val;
double_val =sqlite3_column_double(dbi->ppStmt, nCol);
float float_val =(float)double_val;
return float_val;
}
/*
frees the pointer returned by get_table.
*/
void sqlite3_free_table_idr(void* db){
Table* tbl =(Table*) db;
sqlite3_free_table(tbl->table_data);
free(tbl);
}
int sqlite3_step_idr(void* db){
DBinfo* dbi =(DBinfo*) db;
int rc =sqlite3_step(dbi->ppStmt);
return rc;
}
/*
Binds integer. This returns a pointer
because of the implementation of BindMulti
which binds multiple values
*/
void* sqlite3_bind_int_idr(void* p,int index, int val){
DBinfo* dbi =(DBinfo*) p;
int rc;
rc =sqlite3_bind_int(dbi->ppStmt,index,val);
if(rc != SQLITE_OK){
return NULL;
}
return dbi;
}
void* sqlite3_bind_float_idr(void* p,int index, float val){
DBinfo* dbi =(DBinfo*) p;
int rc;
double res =(float)val;
rc =sqlite3_bind_double(dbi->ppStmt,index,res);
if(rc != SQLITE_OK){
return NULL;
}
return dbi;
}
void* sqlite3_bind_null_idr(void* p,int index){
DBinfo* dbi =(DBinfo*) p;
int rc;
rc =sqlite3_bind_null(dbi->ppStmt,index);
if(rc != SQLITE_OK){
return NULL;
}
return dbi;
}
void* sqlite3_bind_text_idr(void* p,const char* text, int index,int length){
DBinfo* dbi =(DBinfo*) p;
int rc;
rc =sqlite3_bind_text(dbi->ppStmt,index,text,length,SQLITE_STATIC);
if(rc != SQLITE_OK){
return NULL;
}
return dbi;
}
/*
Used for testing column count function.
This function prepares query and by passing
select all, gets the count for column number
Could be used for testing. Not recommended to
be used with prepare and exec
*/
int sqlite3_column_count_idr(void* db, const char* tbl_name){
DBinfo* dbi =(DBinfo*) db;
sqlite3_stmt* stmt;
const char *tail;
int rc;
strcpy(sql_query_buffer, "select * from ");
strcat(sql_query_buffer, tbl_name);
rc = sqlite3_prepare_v2(dbi->db_ptr, sql_query_buffer, -1, &stmt, &tail);
if(rc != SQLITE_OK){
fprintf(stderr, "SQL Prepare error");
return rc;
}
printf("Prepare successful %d\n", rc);
rc =sqlite3_column_count(stmt);
if(rc == 0){
fprintf(stderr, "SQL column count error\n");
return rc;
}
sqlite3_finalize(stmt);
// rc = actual column count
return rc;
}
int sqlite3_data_count_idr(void* db){
DBinfo* dbi =(DBinfo*) db;
int rc = sqlite3_data_count(dbi->ppStmt);
return rc;
}
/*
Must be called after prepare to clean up
the resources.
*/
int sqlite3_finalize_idr(void* db){
DBinfo* dbi=(DBinfo*) db;
int rc =sqlite3_finalize(dbi->ppStmt);
return rc;
}
int sqlite3_complete_idr(const char *sql){
int rc = sqlite3_complete(sql);
return rc;
}
/*
Resets a prepared statement pointer
to its initial state
*/
int sqlite3_reset_idr(void* db){
DBinfo* dbi=(DBinfo*) db;
int rc = sqlite3_reset(dbi-> ppStmt);
return rc;
}
/*
The following routines may be used to
obtain column related information.
*/
const char *sqlite3_column_name_idr(void* db, int N){
DBinfo* dbi=(DBinfo*) db;
const char *name = sqlite3_column_name(dbi->ppStmt, N);
return name;
}
const char *sqlite3_column_decltype_idr(void* db,int n){
DBinfo* dbi=(DBinfo*) db;
const char *dectype = sqlite3_column_decltype(dbi->ppStmt, n);
return dectype;
}
int sqlite3_column_bytes_idr(void* db, int n){
DBinfo* dbi=(DBinfo*) db;
int res = sqlite3_column_bytes(dbi->ppStmt, n);
return res;
}
const void *sqlite3_column_blob_idr(void* db, int iCol){
DBinfo* dbi=(DBinfo*) db;
const void* data =sqlite3_column_blob(dbi-> ppStmt, iCol);
return data;
}
const unsigned char *sqlite3_column_text_idr(void* db, int iCol){
DBinfo* dbi=(DBinfo*) db;
const unsigned char* col_text =sqlite3_column_text(dbi->ppStmt, iCol);
return col_text;
}
int sqlite3_column_int_idr(void* db, int iCol){
DBinfo* dbi=(DBinfo*) db;
int res =sqlite3_column_int(dbi-> ppStmt, iCol);
return res;
}
/*
Some back up functions
*/
void* sqlite3_backup_init_idr(void* pDest,
const char *zDestName,
void* pSource,
const char *zSourceName
){
DBinfo* dbi=(DBinfo*) pDest;
DBbackup* dbi2=(DBbackup*) pSource;
void* res = sqlite3_backup_init(dbi->db_ptr,zDestName,
dbi2->source_ptr,zSourceName);
if(res == NULL){
printf("Error number in initializing backup : %d\n", sqlite3_errcode(dbi->db_ptr));
}
dbi2->backup = res;
return dbi2;
}
int sqlite3_backup_step_idr(void *backup, int nPage){
DBbackup* dbi=(DBbackup*) backup;
int res = sqlite3_backup_step(dbi->backup, nPage);
return res;
}
int sqlite3_backup_finish_idr(void *backup){
DBbackup* dbi=(DBbackup*) backup;
int res = sqlite3_backup_finish(dbi->backup);
return res;
}
int sqlite3_backup_remaining_idr(void *backup){
DBbackup* dbi=(DBbackup*) backup;
int res = sqlite3_backup_remaining(dbi->backup);
return res;
}
int sqlite3_backup_pagecount_idr(void *backup){
DBbackup* dbi=(DBbackup*) backup;
int res =sqlite3_backup_pagecount(dbi-> backup);
return res;
}
/*
Get the length of string
Need this in Idris since length will not
work on Strings.
*/
int strLength(const char * str){
int length = strlen(str);
return length;
}

130
contribs/lib/SQLite3/sqlite3api.h
View File

@ -1,130 +0,0 @@
/*
* sqlite3api.h
*
*
* Created by Melissa Farinaz MOZIFIAN on 22/06/2012.
* Copyright 2012. All rights reserved.
*
*/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <sqlite3.h>
#include <ctype.h>
#include <gc.h>
typedef struct {
sqlite3 *db_ptr; // database pointer
sqlite3_stmt *ppStmt; // statement pointer
char buffer[1000]; // bufer to store errors returned by certain functions
const char *Ptr_tail;
sqlite3_value *value;
int row_count; // row number store by exec function
int col_count;
} DBinfo;
// struct used for backup functions
typedef struct {
sqlite3 *source_ptr;
sqlite3_backup *backup;
}DBbackup ;
// Table struct used by get_table function
// stores row and column
// returned by get_table
typedef struct {
int num_row;
int num_col;
char** table_data;
int data_size;
int* data_type;
DBinfo* database;
}Table;
void* sqlite3_open_idr(const char *filename);
int exec_db(void*p);
int sqlite3_close_idr(void* db);
int sqlite3_exec_idr(void*, const char *sql);
char* sqlite3_get_error(void* db);
const unsigned char* sqlite3_get_val_text(void* p,int nCol);
void* sqlite3_get_table_idr(void* db, const char *sql);
void sqlite3_free_table_idr(void* db);
int sqlite3_get_num_col(void* p);
int sqlite3_get_num_row(void* p);
int sqlite3_get_num_row_v2(void* p);
int sqlite3_get_num_col_v2(void* p);
int sqlite3_get_data_type(void* p, int nRow, int nCol);
int sqlite3_get_val_int(void* p,int nCo);
float sqlite3_get_float(void* p, int nCol);
void* sqlite3_prepare_idr(
void *db, /* Database handle */
const char *zSql /* SQL statement, UTF-8 encoded */
);
int sqlite3_step_idr(void* stmt);
void* sqlite3_bind_float_idr(void* p,int index, float val);
void* sqlite3_bind_int_idr(void* p,int index , int val);
void* sqlite3_bind_null_idr(void* p,int index);
void* sqlite3_bind_text_idr(void* p,const char* text, int index,int length);
int sqlite3_column_count_idr(void* stmt, const char* tbl_name);
int sqlite3_data_count_idr(void* stmt);
int sqlite3_reset_idr(void* stmt);
int sqlite3_finalize_idr(void* stmt);
int sqlite3_complete_idr(const char *sql);
const char *sqlite3_column_decltype_idr(void* stmt,int n);
const char *sqlite3_column_name_idr(void* stmt, int N);
int sqlite3_column_bytes_idr(void* stmt, int n);
int sqlite3_column_bytes_idr(void* stmt, int n);
const void *sqlite3_column_blob_idr(void* stmt, int iCol);
const unsigned char *sqlite3_column_text_idr(void* stmt, int iCol);
int sqlite3_column_int_idr(void* stmt, int iCol);
void* sqlite3_backup_init_idr(void* pDestm,
const char *zDestName,
void* pSource,
const char *zSourceName
);
int sqlite3_backup_finish_idr(void *backup);
int sqlite3_backup_step_idr(void *backup, int nPage);
int sqlite3_backup_remaining_idr(void *backup);
int sqlite3_backup_pagecount_idr(void *backup);
int strLength(const char * str);

BIN
contribs/lib/SQLite3/students.db
View File

Binary file not shown.

140
contribs/lib/SQLite3/testunit.idr
View File

@ -1,140 +0,0 @@
module Main
import Sqlite3
testexpr : DB()
testexpr = do db <- open_db "somedb.db"
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))))))
let x = (fst sql) -- get the string
let list = (snd sql) -- list of vals
liftIO(printLn x) -- use liftIO to turn this into DB type
stmt <- (prepare_db db x) -- prepare the statement
bindMulti stmt list -- bind the values in the list
exec_db_v2 stmt -- execute the prepared query
res <- toList_v1 db -- toList_v1 to get the result
liftIO(printLn res) -- print the result
finalize_db stmt -- Statment pointer must be finalized in the end
close_db db -- close the datbase
return ()
testupdate : DB()
testupdate = do db <- open_db "somedb.db"
let sql = (evalSQL [] (UPDATE (TBL ["tbl1"]) (WHERE (SET (MkCond (Equals(VCol "data") (VStr "data600"))) ) (MkCond (Equals (VCol "num") (VInt 2))) ) ))
let x = (fst sql)
let list = (snd sql)
liftIO(printLn x)
stmt <- (prepare_db db x)
bindMulti stmt list
exec_db_v2 stmt
finalize_db stmt
close_db db
return ()
testInsert : DB()
testInsert = do db <- open_db "somedb.db"
let sql = (evalSQL [] (INSERT (TBL ["tbl1"]) [(VInt 3),(VStr "ham")]))
let x = (fst sql)
let list = (snd sql)
liftIO(printLn x)
stmt <- (prepare_db db x)
bindMulti stmt list
exec_db_v2 stmt
finalize_db stmt
close_db db
return ()
testNull : DB()
testNull = do db <- open_db "somedb.db"
let sql = (evalSQL [] ((SELECT ALL)(TBL ["tbl1"]) (MkCond (MkNULL (VCol "data")))))
let x = (fst sql)
let list = (snd sql)
liftIO(printLn x)
stmt <- (prepare_db db x)
bindMulti stmt list
exec_db_v2 stmt
res <- toList_v1 db
liftIO(printLn res)
finalize_db stmt
close_db db
return ()
testInsertWithCond : DB()
testInsertWithCond = do db <- open_db "somedb.db"
let sql = (evalSQL [] (INSERTC (TBL ["tbl1"]) [(VCol "data"),(VCol "num")] [(VInt 30),(VStr "inserthere")]))
let x = (fst sql)
let list = (snd sql)
liftIO(printLn x)
stmt <- (prepare_db db x)
bindMulti stmt list
exec_db_v2 stmt
finalize_db stmt
close_db db
return ()
-- Nested queries need to have the same column as the outer queries.
testNestedSel1 : DB()
testNestedSel1 = do db <- open_db "somedb.db"
let sql = (evalSQL [] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL ["tbl1"]) (MkCond (MkGT (VCol "num")(VInt 2))))Empty))
let x = (fst sql)
let list = (snd sql)
liftIO(printLn x)
stmt <- (prepare_db db x)
bindMulti stmt list
exec_db_v2 stmt
res <- toList_v1 db
liftIO(printLn res)
finalize_db stmt
close_db db
return ()
-- Testing Create Table
testCreateTable : DB ()
testCreateTable = do db <- open_db "somedb.db"
let sql = (evalSQL [] (CREATE (TBL ["mynewtbl"]) [ ((VCol "col"),(CInt "int"),(None)) ] ) )
let x = (fst sql)
let list = (snd sql)
liftIO(printLn x)
stmt <- (prepare_db db x)
bindMulti stmt list
exec_db_v2 stmt
finalize_db stmt
close_db db
return ()
-- This may be a bit slow
testMultiTable : DB ()
testMultiTable = do db <- open_db "somedb.db"
let sql = (evalSQL [] ((SELECT ALL )(TBL ["mytable","tbl1"]) (Empty) ) )
let x = (fst sql)
let list = (snd sql)
liftIO(printLn x)
stmt <- (prepare_db db x)
bindMulti stmt list
exec_db_v2 stmt
res <- toList_v1 db
liftIO(printLn res)
finalize_db stmt
close_db db
return ()
testSelAll : DB ()
testSelAll = do db <- open_db "somedb.db"
let sql = (evalSQL [] ((SELECT ALL )(TBL ["tbl1"]) (Empty) ) )
let x = (fst sql)
let list = (snd sql)
liftIO(printLn x)
stmt <- (prepare_db db x)
bindMulti stmt list
exec_db_v2 stmt
res <- toList_v1 db
liftIO(printLn res)
finalize_db stmt
close_db db
return ()
main : IO ()
main = do x <- runDB (testMultiTable) -- runDB : DB a -> IO a
--y <- runDB (testNestedSel1)
return ()

190
contribs/lib/SimpleParser/SimpleParser.idr
View File

@ -1,190 +0,0 @@
{-
Simple monadic parser module, based heavily on that by
Graham Hutton.
-}
module SimpleParser
import Prelude
import Prelude.Monad
import Prelude.Applicative
import Prelude.List
import Builtins
%access public
--------------------------------------------------------------------------------
-- The monad of parsers
--------------------------------------------------------------------------------
data Parser a = P (String -> Either String (a, String))
parse : Parser a -> String -> Either String (a, String)
parse (P p) inp = p inp
instance Functor Parser where
map f p = P (\inp => case parse p inp of
Left err => Left err
Right (v, rest) => Right ((f v), rest))
instance Applicative Parser where
pure v = P (\inp => Right (v, inp))
a <*> b = P (\inp => do (f, rest) <- parse a inp
(x, rest') <- parse b rest
pure ((f x), rest'))
instance Monad Parser where
p >>= f = P (\inp => case parse p inp of
Left err => Left err
Right (v,rest) => parse (f v) rest)
instance Alternative Parser where
empty = P (const (Left "empty"))
p <|> q = P (\inp => case parse p inp of
Left msg => parse q inp
Right (v,out) => Right (v,out))
--------------------------------------------------------------------------------
-- Basic parsers
--------------------------------------------------------------------------------
failure : String -> Parser a
failure msg = P (\inp => Left msg)
item : Parser Char
item = P (\inp => case choose (inp == "") of
Left _ => Left "Error! Parsing empty list."
Right p => Right (strHead' inp p, strTail' inp p))
--------------------------------------------------------------------------------
-- Derived primitives
--------------------------------------------------------------------------------
sat : (Char -> Bool) -> Parser Char
sat p = do x <- item
guard (p x)
pure x
oneof : List Char -> Parser Char
oneof xs = sat (\x => elem x xs)
digit : Parser Char
digit = sat isDigit
lower : Parser Char
lower = sat isLower
upper : Parser Char
upper = sat isUpper
letter : Parser Char
letter = sat isAlpha
alphanum : Parser Char
alphanum = sat isAlphaNum
char : Char -> Parser Char
char x = sat (== x)
string : String -> Parser String
string s = map pack (traverse char (unpack s))
mutual
many1 : Parser a -> Parser (List a)
many1 p = [| p :: many p |]
many : Parser a -> Parser (List a)
many p = lazy (many1 p) <|> pure []
bool : Parser Bool
bool = parseTrue <|> parseFalse
where parseTrue : Parser Bool
parseTrue = do oneof ['T', 't']
string "rue"
pure True
parseFalse = do oneof ['F', 'f']
string "alse"
pure False
ident : Parser String
ident = map pack xs
where xs : Parser (List Char)
xs = [| letter :: many1 alphanum |]
nat : Parser Int
nat = do xs <- many digit
pure (cast (cast xs))
int : Parser Int
int = neg <|> nat
where neg : Parser Int
neg = do char '-'
n <- nat
pure (-n)
space : Parser ()
space = do many (sat isSpace)
pure ()
--------------------------------------------------------------------------------
-- Ignoring spacing
--------------------------------------------------------------------------------
token : Parser a -> Parser a
token p = space $> p <$ space
identifier : Parser String
identifier = token ident
natural : Parser Int
natural = token nat
integer : Parser Int
integer = token int
symbol : String -> Parser String
symbol xs = token (string xs)
strToken : Parser String
strToken = map pack (token (many1 alphanum))
--------------------------------------------------------------------------------
-- combinators
--------------------------------------------------------------------------------
optional : Parser a -> Parser (Maybe a)
optional p = map Just p <|> pure Nothing
sepBy1 : Parser a -> Parser b -> Parser (List a)
sepBy1 p s = [| p :: many (s $> p) |]
sepBy : Parser a -> Parser b -> Parser (List a)
sepBy p s = sepBy1 p s <|> pure Nil
manyTil : Parser a -> Parser b -> Parser (List a)
manyTil p e = (e $> pure Nil) <|> lazy [| p :: manyTil p e |] <|> pure Nil
--------------------------------------------------------------------------------
-- Expressions
--------------------------------------------------------------------------------
expr : Parser Int
factor : Parser Int
term : Parser Int
expr = do t <- term
map (t+) (symbol "+" $> expr) <|> pure t
factor = (symbol "(" $> expr <$ symbol ")") <|> natural
term = do f <- factor
map (f*) (symbol "*" $> term) <|> pure f
eval : String -> Maybe Int
eval xs = case (parse expr xs) of
Right (n,rest) => if rest == "" then Just n else Nothing
Left msg => Nothing

4
contribs/lib/SimpleParser/simpleparser.ipkg
View File

@ -1,4 +0,0 @@
package simpleparser
opts = "-i ../lib"
modules = SimpleParser

31
contribs/tool-support/completion/idris.bash
View File

@ -1,31 +0,0 @@
_idris() {
local cur prev words opts LIBRARIES TARGETS
_init_completion || return
opts=$(_parse_help "$1")
LIBRARIES="effects"
TARGETS="C Java bytecode javascript node"
case "${prev}" in
-o)
_filedir
;;
-i|--ibcsubdir)
_filedir -d
;;
-p)
COMPREPLY=( $(compgen -W "${LIBRARIES}" -- ${cur}))
;;
--target)
COMPREPLY=( $(compgen -W "${TARGETS}" -- ${cur}))
;;
esac
if [[ $cur == -* ]]; then
COMPREPLY=($(compgen -W "${opts}" -- ${cur}))
return
fi
_filedir '@(idr)'
} &&
complete -o default -F _idris idris

70
contribs/tool-support/sublime-text/Idris/Idris.JSON-tmLanguage
View File

@ -1,70 +0,0 @@
{ "name": "Idris",
"scopeName": "source.idris",
"fileTypes": ["idr"],
"patterns": [
{ "name": "keyword.control.idris",
"match": "\\b(if|then|else|do|let|in|data|codata|record|dsl|import)\\b"
},
{ "name": "keyword.control.idris",
"match": "\\b(impossible|case|of|total|partial|mutual|infix|infixl|infixr)\\b"
},
{ "name": "keyword.control.idris",
"match": "\\b(where|with|syntax|proof|postulate|using|namespace|class|instance)\\b"
},
{ "name": "keyword.control.idris",
"match": "\\b(public|private|abstract|implicit)\\b"
},
{ "name": "keyword.other.idris",
"match": "\\b(Type|Int|Integer|Float|Char|String|Ptr|Bits8|Bits16|Bits32|Bits64)\\b"
},
{ "name": "constant.numeric.idris",
"match": "\\b(S|O)\\b"
},
{ "match": "\\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\\b",
"name": "constant.numeric.idris",
"comment": "integers"
},
{
"match": "\\b([0-9]+\\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\\b",
"name": "constant.numeric.float.idris",
"comment": "floats"
},
{
"name": "comment.line.idris",
"match": "(--).*$\n?",
"comment": "Line comment"
},
{ "name": "comment.block.idris",
"begin": "\\{-",
"end": "-\\}",
"comment": "Block comment"
},
{
"name": "string.quoted.idris",
"begin": "\"",
"beginCaptures": {
"0": { "name": "punctuation.definition.string.begin.idris"}
},
"end": "\"",
"endCaptures": {
"0": { "name": "punctuation.definition.string.end.idris"}
},
"patterns": [
{ "name": "constant.character.escape.idris",
"match": "\\\\\""
}
]
}
],
"repository": {
},
"uuid": "4dd16092-ffa5-4ba4-8075-e5da9f368a72"
}

126
contribs/tool-support/sublime-text/Idris/Idris.tmLanguage
View File

@ -1,126 +0,0 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE plist PUBLIC "-//Apple Computer//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
<plist version="1.0">
<dict>
<key>fileTypes</key>
<array>
<string>idr</string>
</array>
<key>name</key>
<string>Idris</string>
<key>patterns</key>
<array>
<dict>
<key>match</key>
<string>\b(if|then|else|do|let|in|data|codata|record|dsl|import)\b</string>
<key>name</key>
<string>keyword.control.idris</string>
</dict>
<dict>
<key>match</key>
<string>\b(impossible|case|of|total|partial|mutual|infix|infixl|infixr)\b</string>
<key>name</key>
<string>keyword.control.idris</string>
</dict>
<dict>
<key>match</key>
<string>\b(where|with|syntax|proof|postulate|using|namespace|class|instance)\b</string>
<key>name</key>
<string>keyword.control.idris</string>
</dict>
<dict>
<key>match</key>
<string>\b(public|private|abstract|implicit)\b</string>
<key>name</key>
<string>keyword.control.idris</string>
</dict>
<dict>
<key>match</key>
<string>\b(Type|Int|Integer|Float|Char|String|Ptr|Bits8|Bits16|Bits32|Bits64)\b</string>
<key>name</key>
<string>keyword.other.idris</string>
</dict>
<dict>
<key>match</key>
<string>\b(S|O)\b</string>
<key>name</key>
<string>constant.numeric.idris</string>
</dict>
<dict>
<key>comment</key>
<string>integers</string>
<key>match</key>
<string>\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\b</string>
<key>name</key>
<string>constant.numeric.idris</string>
</dict>
<dict>
<key>comment</key>
<string>floats</string>
<key>match</key>
<string>\b([0-9]+\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\b</string>
<key>name</key>
<string>constant.numeric.float.idris</string>
</dict>
<dict>
<key>comment</key>
<string>Line comment</string>
<key>match</key>
<string>(--).*$
?</string>
<key>name</key>
<string>comment.line.idris</string>
</dict>
<dict>
<key>begin</key>
<string>\{-</string>
<key>comment</key>
<string>Block comment</string>
<key>end</key>
<string>-\}</string>
<key>name</key>
<string>comment.block.idris</string>
</dict>
<dict>
<key>begin</key>
<string>"</string>
<key>beginCaptures</key>
<dict>
<key>0</key>
<dict>
<key>name</key>
<string>punctuation.definition.string.begin.idris</string>
</dict>
</dict>
<key>end</key>
<string>"</string>
<key>endCaptures</key>
<dict>
<key>0</key>
<dict>
<key>name</key>
<string>punctuation.definition.string.end.idris</string>
</dict>
</dict>
<key>name</key>
<string>string.quoted.idris</string>
<key>patterns</key>
<array>
<dict>
<key>match</key>
<string>\\"</string>
<key>name</key>
<string>constant.character.escape.idris</string>
</dict>
</array>
</dict>
</array>
<key>repository</key>
<dict>
</dict>
<key>scopeName</key>
<string>source.idris</string>
<key>uuid</key>
<string>4dd16092-ffa5-4ba4-8075-e5da9f368a72</string>
</dict>
</plist>

5
contribs/tool-support/sublime-text/Idris/idris.sublime-build
View File

@ -1,5 +0,0 @@
{
"cmd": ["idris", "$file"],
"file_regex": "^(...*?):([0-9]*):?([0-9]*)",
"selector": "source.idris"
}

11
contribs/tool-support/sublime-text/README.md
View File

@ -1,11 +0,0 @@
#### Idris support for Sublime Text 2
To install, copy the Idris directory to Sublime Text's Packages directory.
To build a new Idris.tmLanguage file from the Idris.JSON-tmLanguage file, Sublime Text needs to have the AAAPackageDev package installed.
Syntax Definitions tutorial: https://sublime-text-unofficial-documentation.readthedocs.org/en/latest/extensibility/syntaxdefs.html
Syntax Definitions reference: https://sublime-text-unofficial-documentation.readthedocs.org/en/latest/reference/syntaxdefs.html
Most used scopes: http://manual.macromates.com/en/language_grammars#naming_conventions

3
custom.mk-alldeps
View File

@ -1,2 +1 @@
CABALFLAGS += -f LLVM -f FFI -f curses CABALFLAGS += -f LLVM -f FFI -f curses --disable-documentation --disable-profiling --disable-library-profiling

20
docs/tutorial/introduction.rst
View File

@ -25,11 +25,12 @@ lists of a given length [1]_, ``Vect n a``, where ``a`` is the element
type and ``n`` is the length of the list and can be an arbitrary term. type and ``n`` is the length of the list and can be an arbitrary term.
When types can contain values, and where those values describe When types can contain values, and where those values describe
properties (e.g. the length of a list) the type of a function can properties, for example the length of a list, the type of a function
begin to describe its own properties. For example, concatenating two can begin to describe its own properties. Take for example the
lists has the property that the resulting list’s length is the sum of concatenatation of two lists. This operation has the property that the
the lengths of the two input lists. We can therefore give the resulting list's length is the sum of the lengths of the two input
following type to the ``app`` function, which concatenates vectors: lists. We can therefore give the following type to the ``app``
function, which concatenates vectors:
.. code-block:: idris .. code-block:: idris
@ -58,11 +59,10 @@ Example Code
============ ============
This tutorial includes some example code, which has been tested with This tutorial includes some example code, which has been tested with
Idris version . The files are available in the Idris against Idris. These files are available with the Idris distribution,
distribution, and provided along side the tutorial source, so that you so that you can try them out easily. They can be found under
can try them out easily, under ``tutorial/examples``. However, it is ``samples``. It is, however, strongly recommended that you type
strongly recommended that you can type them in yourself, rather than them in yourself, rather than simply loading and reading them.
simply loading and reading them.
.. [1] .. [1]
Typically, and perhaps confusingly, referred to in the dependently Typically, and perhaps confusingly, referred to in the dependently

26
docs/tutorial/modules.rst
View File

@ -10,11 +10,11 @@ module, a list of ``import`` statements giving the other modules which
are to be imported, and a collection of declarations and definitions of are to be imported, and a collection of declarations and definitions of
types, classes and functions. For example, the listing below gives a types, classes and functions. For example, the listing below gives a
module which defines a binary tree type ``BTree`` (in a file module which defines a binary tree type ``BTree`` (in a file
``btree.idr``): ``Btree.idr``):
.. code-block:: idris .. code-block:: idris
module btree module Btree
data BTree a = Leaf data BTree a = Leaf
| Node (BTree a) a (BTree a) | Node (BTree a) a (BTree a)
@ -40,23 +40,24 @@ Then, this gives a main program (in a file
module Main module Main
import btree import Btree
main : IO () main : IO ()
main = do let t = toTree [1,8,2,7,9,3] main = do let t = toTree [1,8,2,7,9,3]
print (btree.toList t) print (btree.toList t)
The same names can be defined in multiple modules. This is possible The same names can be defined in multiple modules. This is possible
because in practice names are *qualified* with the name of the module. because in practice names are *qualified* with the name of the module.
The names defined in the ``btree`` module are, in full: The names defined in the ``btree`` module are, in full:
+ ``btree.BTree`` + ``Btree.BTree``
+ ``btree.Leaf`` + ``Btree.Leaf``
+ ``btree.Node`` + ``Btree.Node``
+ ``btree.insert`` + ``Btree.insert``
+ ``btree.toList`` + ``Btree.toList``
+ ``btree.toTree`` + ``Btree.toTree``
If names are otherwise unambiguous, there is no need to give the fully If names are otherwise unambiguous, there is no need to give the fully
qualified name. Names can be disambiguated either by giving an explicit qualified name. Names can be disambiguated either by giving an explicit
@ -103,7 +104,7 @@ functions to be exported as ``abstract``, as we see below:
.. code-block:: idris .. code-block:: idris
module btree module Btree
abstract data BTree a = Leaf abstract data BTree a = Leaf
| Node (BTree a) a (BTree a) | Node (BTree a) a (BTree a)
@ -137,7 +138,8 @@ the ``public`` modifier on an ``import``. For example:
module A module A
import B import public C import B
import public C
public a : AType a = ... public a : AType a = ...
@ -154,7 +156,7 @@ wish to overload names within the same module:
.. code-block:: idris .. code-block:: idris
module foo module Foo
namespace x namespace x
test : Int -> Int test : Int -> Int

22
docs/tutorial/starting.rst
View File

@ -10,12 +10,9 @@ Prerequisites
Before installing Idris, you will need to make sure you have all Before installing Idris, you will need to make sure you have all
of the necessary libraries and tools. You will need: of the necessary libraries and tools. You will need:
- A fairly recent Haskell platform. Version 2013.2.0.0 should be - A fairly recent Haskell platform. Version ``2013.2.0.0`` should be sufficiently recent, though it is better to be completely up to date.
sufficiently recent, though it is better to be completely up to
date.
- The *GNU Multiple Precision Arithmetic Library* (GMP) is available - The *GNU Multiple Precision Arithmetic Library* (GMP) is available from MacPorts/Homebrew and all major Linux distributions.
from MacPorts/Homebrew and all major Linux distributions.
Downloading and Installing Downloading and Installing
========================== ==========================
@ -33,7 +30,7 @@ development version you can find it, as well as build intructions, on
GitHub at: https://github.com/idris-lang/Idris-dev. GitHub at: https://github.com/idris-lang/Idris-dev.
To check that installation has succeeded, and to write your first To check that installation has succeeded, and to write your first
Idris program, create a file called “``hello.idr``” containing the Idris program, create a file called ``hello.idr`` containing the
following text: following text:
.. code-block:: idris .. code-block:: idris
@ -55,18 +52,17 @@ create an executable called ``hello``, which you can run:
$ ./hello $ ./hello
Hello world Hello world
Note that the ``$`` indicates the shell prompt! Should the Idris Please note that the dollar sign ``$`` indicates the shell prompt!
executable not be found please ensure that you have added Should the Idris executable not be found please ensure that you have
``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X added ``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS
users may find they need to use ``~/Library/Haskell/bin`` X users may find they need to add ``~/Library/Haskell/bin``
instead. Some useful options to the Idris command are: instead. Some useful options to the Idris command are:
- ``-o prog`` to compile to an executable called ``prog``. - ``-o prog`` to compile to an executable called ``prog``.
- ``--check`` type check the file and its dependencies without - ``--check`` type check the file and its dependencies without starting the interactive environment.
starting the interactive environment.
- ``--help`` display usage summary and command line options - ``--help`` display usage summary and command line options.
The Interactive Environment The Interactive Environment
=========================== ===========================

68
docs/tutorial/typesfuns.rst
View File

@ -12,13 +12,13 @@ Idris defines several primitive types: ``Int``, ``Integer`` and
manipulation, and ``Ptr`` which represents foreign pointers. There are manipulation, and ``Ptr`` which represents foreign pointers. There are
also several data types declared in the library, including ``Bool``, also several data types declared in the library, including ``Bool``,
with values ``True`` and ``False``. We can declare some constants with with values ``True`` and ``False``. We can declare some constants with
these types. Enter the following into a file ``prims.idr`` and load it these types. Enter the following into a file ``Prims.idr`` and load it
into the Idris interactive environment by typing ``idris into the Idris interactive environment by typing ``idris
prims.idr``: Prims.idr``:
.. code-block:: idris .. code-block:: idris
module prims module Prims
x : Int x : Int
x = 42 x = 42
@ -33,17 +33,18 @@ prims.idr``:
quux = False quux = False
An Idris file consists of an optional module declaration (here An Idris file consists of an optional module declaration (here
``module prims``) followed by an optional list of imports (none here, ``module Prims``) followed by an optional list of imports and a
however Idris programs can consist of several modules, and the collection of declarations and definitions. In this example no imports
definitions in each module each have their own namespace, as we will have been specified. However Idris programs can consist of several
discuss in Section :ref:`sect-namespaces`) and a collection of modules and the definitions in each module each have their own
declarations and definitions. The order of definitions is significant namespace. This is discussed further in Section
— functions and data types must be defined before use. Each definition :ref:`sect-namespaces`). When writing Idris programs both the order in
must have a type declaration, for example see ``x : Int``, ``foo : definitions are given and indentation are significant. Functions and
String``, from the above listing. Indentation is significant — a new data types must be defined before use, incidently each definition must
declaration begins at the same level of indentation as the preceding have a type declaration, for example see ``x : Int``, ``foo :
declaration. Alternatively, declarations may be terminated with a String``, from the above listing. New declarations must begin at the
semicolon. same level of indentation as the preceding declaration.
Alternatively, a semicolon ``;`` can be used to terminate declarations.
A library module ``prelude`` is automatically imported by every A library module ``prelude`` is automatically imported by every
Idris program, including facilities for IO, arithmetic, data Idris program, including facilities for IO, arithmetic, data
@ -63,7 +64,7 @@ All of the usual arithmetic and comparison operators are defined for
the primitive types. They are overloaded using type classes, as we the primitive types. They are overloaded using type classes, as we
will discuss in Section :ref:`sect-classes` and can be extended to will discuss in Section :ref:`sect-classes` and can be extended to
work on user defined types. Boolean expressions can be tested with the work on user defined types. Boolean expressions can be tested with the
``if...then...else`` construct: ``if...then...else`` construct, for example:
:: ::
@ -73,9 +74,9 @@ work on user defined types. Boolean expressions can be tested with the
Data Types Data Types
========== ==========
Data types are declared in a similar way to Haskell data types, with a Data types are declared in a similar way and with similar syntax to
similar syntax. Natural numbers and lists, for example, can be Haskell. Natural numbers and lists, for example, can be declared as
declared as follows: follows:
.. code-block:: idris .. code-block:: idris
@ -193,11 +194,13 @@ does not need to be visible globally:
Indentation is significant — functions in the ``where`` block must be Indentation is significant — functions in the ``where`` block must be
indented further than the outer function. indented further than the outer function.
**Scope:** Any names which are visible in the outer scope are also .. note:: Scope
visible in the ``where`` clause (unless they have been redefined, such
as ``xs`` here). A name which appears only in the type will be in scope Any names which are visible in the outer scope are also visible in
in the ``where`` clause if it is a *parameter* to one of the types, the ``where`` clause (unless they have been redefined, such as ``xs``
i.e. it is fixed across the entire structure. here). A name which appears only in the type will be in scope in the
``where`` clause if it is a *parameter* to one of the types, i.e. it
is fixed across the entire structure.
As well as functions, ``where`` blocks can include local data As well as functions, ``where`` blocks can include local data
declarations, such as the following where ``MyLT`` is not accessible declarations, such as the following where ``MyLT`` is not accessible
@ -306,16 +309,17 @@ following:
$ idris vbroken.idr --check $ idris vbroken.idr --check
vbroken.idr:9:23:When elaborating right hand side of Vect.++: vbroken.idr:9:23:When elaborating right hand side of Vect.++:
When elaborating an application of constructor Vect.::: When elaborating an application of constructor Vect.:::
Can't unify Can't unify
Vect (k + k) a Vect (k + k) a (Type of xs ++ xs)
with with
Vect (plus k m) a Vect (plus k m) a (Expected type)
Specifically:
Can't unify
plus k k
with
plus k m
Specifically:
Can't unify
plus k k
with
plus k m
This error message suggests that there is a length mismatch between This error message suggests that there is a length mismatch between
two vectors — we needed a vector of length ``k + m``, but provided a two vectors — we needed a vector of length ``k + m``, but provided a

4
docs/tutorial/views.rst
View File

@ -83,8 +83,8 @@ rule:
The value of the result of ``parity k`` affects the form of ``k``, The value of the result of ``parity k`` affects the form of ``k``,
because the result of ``parity k`` depends on ``k``. So, as well as because the result of ``parity k`` depends on ``k``. So, as well as
the patterns for the result of the intermediate computation (``Even`` the patterns for the result of the intermediate computation (``Even``
and ``odd``) right of the ``\mid``, we also write how the results and ``odd``) right of the ``|``, we also write how the results
affect the other patterns left of the :math:`\mid`. Note that there is affect the other patterns left of the ``|``. Note that there is
a function in the patterns (``+``) and repeated occurrences of a function in the patterns (``+``) and repeated occurrences of
``j``—this is allowed because another argument has determined the form ``j``—this is allowed because another argument has determined the form
of these patterns. of these patterns.

15
libs/base/Data/Bits.idr
View File

@ -4,21 +4,16 @@ import Data.Fin
%default total %default total
divCeil : Nat -> Nat -> Nat
divCeil x y = case x `mod` y of
Z => x `div` y
S _ => S (x `div` y)
nextPow2 : Nat -> Nat nextPow2 : Nat -> Nat
nextPow2 Z = Z nextPow2 Z = Z
nextPow2 x = if x == (2 `power` l2x) nextPow2 (S x) = if (S x) == (2 `power` l2x)
then l2x then l2x
else S l2x else S l2x
where where
l2x = log2 x l2x = log2NZ (S x) SIsNotZ
nextBytes : Nat -> Nat nextBytes : Nat -> Nat
nextBytes bits = (nextPow2 (bits `divCeil` 8)) nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
machineTy : Nat -> Type machineTy : Nat -> Type
machineTy Z = Bits8 machineTy Z = Bits8

2
libs/contrib/Network/Cgi.idr
View File

@ -108,7 +108,7 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
| _ = Nothing | _ = Nothing
getContent : Int -> IO String getContent : Int -> IO String
getContent x = getC (toNat x) "" where getContent x = getC (cast x) "" where
getC : Nat -> String -> IO String getC : Nat -> String -> IO String
getC Z acc = return $ reverse acc getC Z acc = return $ reverse acc
getC (S k) acc = do x <- getChar getC (S k) acc = do x <- getChar

6
libs/effects/Effect/Exception.idr
View File

@ -4,7 +4,7 @@ import Effects
import System import System
import Control.IOExcept import Control.IOExcept
data Exception : Type -> Effect where data Exception : Type -> Effect where
Raise : a -> sig (Exception a) b Raise : a -> sig (Exception a) b
instance Handler (Exception a) Maybe where instance Handler (Exception a) Maybe where
@ -14,7 +14,7 @@ instance Handler (Exception a) List where
handle _ (Raise e) k = [] handle _ (Raise e) k = []
instance Show a => Handler (Exception a) IO where instance Show a => Handler (Exception a) IO where
handle _ (Raise e) k = do print e handle _ (Raise e) k = do printLn e
believe_me (exit 1) believe_me (exit 1)
instance Handler (Exception a) (IOExcept a) where instance Handler (Exception a) (IOExcept a) where
@ -26,5 +26,5 @@ instance Handler (Exception a) (Either a) where
EXCEPTION : Type -> EFFECT EXCEPTION : Type -> EFFECT
EXCEPTION t = MkEff () (Exception t) EXCEPTION t = MkEff () (Exception t)
raise : a -> Eff b [EXCEPTION a] raise : a -> Eff b [EXCEPTION a]
raise err = call $ Raise err raise err = call $ Raise err

25
libs/effects/Effect/StdIO.idr
View File

@ -9,8 +9,8 @@ import Control.IOExcept
||| The internal representation of StdIO effects ||| The internal representation of StdIO effects
data StdIO : Effect where data StdIO : Effect where
PutStr : String -> sig StdIO () PutStr : String -> sig StdIO ()
GetStr : sig StdIO String GetStr : sig StdIO String
PutCh : Char -> sig StdIO () PutCh : Char -> sig StdIO ()
GetCh : sig StdIO Char GetCh : sig StdIO Char
@ -22,13 +22,13 @@ data StdIO : Effect where
instance Handler StdIO IO where instance Handler StdIO IO where
handle () (PutStr s) k = do putStr s; k () () handle () (PutStr s) k = do putStr s; k () ()
handle () GetStr k = do x <- getLine; k x () handle () GetStr k = do x <- getLine; k x ()
handle () (PutCh c) k = do putChar c; k () () handle () (PutCh c) k = do putChar c; k () ()
handle () GetCh k = do x <- getChar; k x () handle () GetCh k = do x <- getChar; k x ()
instance Handler StdIO (IOExcept a) where instance Handler StdIO (IOExcept a) where
handle () (PutStr s) k = do ioe_lift $ putStr s; k () () handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
handle () GetStr k = do x <- ioe_lift $ getLine; k x () handle () GetStr k = do x <- ioe_lift $ getLine; k x ()
handle () (PutCh c) k = do ioe_lift $ putChar c; k () () handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
handle () GetCh k = do x <- ioe_lift $ getChar; k x () handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
------------------------------------------------------------- -------------------------------------------------------------
@ -42,13 +42,17 @@ STDIO = MkEff () StdIO
putStr : String -> Eff () [STDIO] putStr : String -> Eff () [STDIO]
putStr s = call $ PutStr s putStr s = call $ PutStr s
||| Write a string to standard output, terminating with a newline.
putStrLn : String -> Eff () [STDIO]
putStrLn s = putStr (s ++ "\n")
||| Write a character to standard output. ||| Write a character to standard output.
putChar : Char -> Eff () [STDIO] putChar : Char -> Eff () [STDIO]
putChar c = call $ PutCh c putChar c = call $ PutCh c
||| Write a string to standard output, terminating with a newline. ||| Write a character to standard output, terminating with a newline.
putStrLn : String -> Eff () [STDIO] putCharLn : Char -> Eff () [STDIO]
putStrLn s = putStr (s ++ "\n") putCharLn c = putStrLn (singleton c)
||| Read a string from standard input. ||| Read a string from standard input.
getStr : Eff String [STDIO] getStr : Eff String [STDIO]
@ -58,3 +62,10 @@ getStr = call $ GetStr
getChar : Eff Char [STDIO] getChar : Eff Char [STDIO]
getChar = call $ GetCh getChar = call $ GetCh
||| Given a parameter `a` 'show' `a` to standard output.
print : Show a => a -> Eff () [STDIO]
print a = putStr (show a)
||| Given a parameter `a` 'show' `a` to a standard output, terminating with a newline
printLn : Show a => a -> Eff () [STDIO]
printLn a = putStrLn (show a)

149
libs/prelude/Language/Reflection/Elab.idr Normal file
View File

@ -0,0 +1,149 @@
module Language.Reflection.Elab
import Builtins
import Prelude.Applicative
import Prelude.Functor
import Prelude.List
import Prelude.Maybe
import Prelude.Monad
import Language.Reflection
data Arg : Type where
Explicit : TTName -> Raw -> Arg
Implicit : TTName -> Raw -> Arg
Constraint : TTName -> Raw -> Arg
data TyDecl : Type where
Declare : TTName -> List Arg -> Raw -> TyDecl
data FunClause : Type where
MkFunClause : (lhs, rhs : Raw) -> FunClause
MkImpossibleClause : (lhs : Raw) -> FunClause
data FunDefn : Type where
DefineFun : TTName -> List FunClause -> FunDefn
abstract
data Elab : Type -> Type where
-- obligatory control stuff
prim__PureElab : a -> Elab a
prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
prim__Env : Elab (List (TTName, Binder TT))
prim__Goal : Elab (TTName, TT)
prim__Holes : Elab (List TTName)
prim__Guess : Elab (Maybe TT)
prim__SourceLocation : Elab SourceLocation
prim__Forget : TT -> Elab Raw
prim__Gensym : String -> Elab TTName
prim__Solve : Elab ()
prim__Fill : Raw -> Elab ()
prim__Focus : TTName -> Elab ()
prim__Unfocus : TTName -> Elab ()
prim__Attack : Elab ()
prim__Rewrite : Raw -> Elab ()
prim__Claim : TTName -> Raw -> Elab ()
prim__Intro : Maybe TTName -> Elab ()
prim__DeclareType : TyDecl -> Elab ()
prim__DefineFunction : FunDefn -> Elab ()
prim__Debug : {a : Type} -> Maybe String -> Elab a
-------------
-- Public API
-------------
%access public
instance Functor Elab where
map f t = prim__BindElab t (\x => prim__PureElab (f x))
instance Applicative Elab where
pure x = prim__PureElab x
f <*> x = prim__BindElab f $ \g =>
prim__BindElab x $ \y =>
prim__PureElab $ g y
instance Alternative Elab where
empty = prim__Fail [TextPart "empty"]
x <|> y = prim__Try x y
instance Monad Elab where
x >>= f = prim__BindElab x f
fail : List ErrorReportPart -> Elab a
fail err = prim__Fail err
getEnv : Elab (List (TTName, Binder TT))
getEnv = prim__Env
getGoal : Elab (TTName, TT)
getGoal = prim__Goal
getHoles : Elab (List TTName)
getHoles = prim__Holes
getGuess : Elab (Maybe TT)
getGuess = prim__Guess
forgetTypes : TT -> Elab Raw
forgetTypes tt = prim__Forget tt
gensym : (hint : String) -> Elab TTName
gensym hint = prim__Gensym hint
solve : Elab ()
solve = prim__Solve
fill : Raw -> Elab ()
fill tm = prim__Fill tm
focus : (hole : TTName) -> Elab ()
focus hole = prim__Focus hole
unfocus : TTName -> Elab ()
unfocus hole = prim__Unfocus hole
attack : Elab ()
attack = prim__Attack
claim : TTName -> Raw -> Elab ()
claim n ty = prim__Claim n ty
intro : Maybe TTName -> Elab ()
intro n = prim__Intro n
||| Find out the present source context for the tactic script
getSourceLocation : Elab SourceLocation
getSourceLocation = prim__SourceLocation
||| Attempt to solve the current goal with the source code location
sourceLocation : Elab ()
sourceLocation = do loc <- getSourceLocation
fill (quote loc)
solve
rewriteWith : Raw -> Elab ()
rewriteWith rule = prim__Rewrite rule
declareType : TyDecl -> Elab ()
declareType decl = prim__DeclareType decl
defineFunction : FunDefn -> Elab ()
defineFunction defun = prim__DefineFunction defun
debug : Elab a
debug = prim__Debug Nothing
debugMessage : String -> Elab a
debugMessage msg = prim__Debug (Just msg)

138
libs/prelude/Language/Reflection/Tactical.idr
View File

@ -1,138 +0,0 @@
module Language.Reflection.Tactical
import Builtins
import Prelude.Applicative
import Prelude.Functor
import Prelude.List
import Prelude.Maybe
import Prelude.Monad
import Language.Reflection
data Arg : Type where
Explicit : TTName -> Raw -> Arg
Implicit : TTName -> Raw -> Arg
Constraint : TTName -> Raw -> Arg
data TyDecl : Type where
Declare : TTName -> List Arg -> Raw -> TyDecl
abstract
data Tactical : Type -> Type where
-- obligatory control stuff
prim__PureTactical : a -> Tactical a
prim__BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b
prim__Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a
prim__Fail : {a : Type} -> List ErrorReportPart -> Tactical a
prim__Env : Tactical (List (TTName, Binder TT))
prim__Goal : Tactical (TTName, TT)
prim__Holes : Tactical (List TTName)
prim__Guess : Tactical (Maybe TT)
prim__SourceLocation : Tactical SourceLocation
prim__Forget : TT -> Tactical Raw
prim__Gensym : String -> Tactical TTName
prim__Solve : Tactical ()
prim__Fill : Raw -> Tactical ()
prim__Focus : TTName -> Tactical ()
prim__Unfocus : TTName -> Tactical ()
prim__Attack : Tactical ()
prim__Rewrite : Raw -> Tactical ()
prim__Claim : TTName -> Raw -> Tactical ()
prim__Intro : Maybe TTName -> Tactical ()
prim__DeclareType : TyDecl -> Tactical ()
prim__Debug : {a : Type} -> Maybe String -> Tactical a
-------------
-- Public API
-------------
%access public
instance Functor Tactical where
map f t = prim__BindTactical t (\x => prim__PureTactical (f x))
instance Applicative Tactical where
pure x = prim__PureTactical x
f <*> x = prim__BindTactical f $ \g =>
prim__BindTactical x $ \y =>
prim__PureTactical $ g y
instance Alternative Tactical where
empty = prim__Fail [TextPart "empty"]
x <|> y = prim__Try x y
instance Monad Tactical where
x >>= f = prim__BindTactical x f
fail : List ErrorReportPart -> Tactical a
fail err = prim__Fail err
getEnv : Tactical (List (TTName, Binder TT))
getEnv = prim__Env
getGoal : Tactical (TTName, TT)
getGoal = prim__Goal
getHoles : Tactical (List TTName)
getHoles = prim__Holes
getGuess : Tactical (Maybe TT)
getGuess = prim__Guess
forgetTypes : TT -> Tactical Raw
forgetTypes tt = prim__Forget tt
gensym : (hint : String) -> Tactical TTName
gensym hint = prim__Gensym hint
solve : Tactical ()
solve = prim__Solve
fill : Raw -> Tactical ()
fill tm = prim__Fill tm
focus : (hole : TTName) -> Tactical ()
focus hole = prim__Focus hole
unfocus : TTName -> Tactical ()
unfocus hole = prim__Unfocus hole
attack : Tactical ()
attack = prim__Attack
claim : TTName -> Raw -> Tactical ()
claim n ty = prim__Claim n ty
intro : Maybe TTName -> Tactical ()
intro n = prim__Intro n
||| Find out the present source context for the tactic script
getSourceLocation : Tactical SourceLocation
getSourceLocation = prim__SourceLocation
||| Attempt to solve the current goal with the source code location
sourceLocation : Tactical ()
sourceLocation = do loc <- getSourceLocation
fill (quote loc)
solve
rewriteWith : Raw -> Tactical ()
rewriteWith rule = prim__Rewrite rule
declareType : TyDecl -> Tactical ()
declareType decl = prim__DeclareType decl
debug : Tactical a
debug = prim__Debug Nothing
debugMessage : String -> Tactical a
debugMessage msg = prim__Debug (Just msg)

16
libs/prelude/Prelude.idr
View File

@ -135,7 +135,7 @@ instance Show a => Show (Maybe a) where
show (Just x) = "Just " ++ show x show (Just x) = "Just " ++ show x
instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
show (y ** prf) = show y ++ " ** " ++ show prf show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
---- Functor instances ---- Functor instances
@ -245,8 +245,8 @@ natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
total natEnumFromTo : Nat -> Nat -> List Nat total natEnumFromTo : Nat -> Nat -> List Nat
natEnumFromTo n m = map (plus n) (natRange ((S m) - n)) natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
natEnumFromThenTo _ Z _ = [] natEnumFromThenTo _ Z _ = []
natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc))) natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (m - n) (S inc) SIsNotZ)))
class Enum a where class Enum a where
total pred : a -> a total pred : a -> a
@ -285,7 +285,7 @@ instance Enum Integer where
go [] = [] go [] = []
go (x :: xs) = n + cast x :: go xs go (x :: xs) = n + cast x :: go xs
enumFromThenTo _ 0 _ = [] enumFromThenTo _ 0 _ = []
enumFromThenTo n inc m = go (natRange (S (fromInteger (abs (m - n)) `div` fromInteger (abs inc)))) enumFromThenTo n inc m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs inc) - 1))) SIsNotZ)))
where go : List Nat -> List Integer where go : List Nat -> List Integer
go [] = [] go [] = []
go (x :: xs) = n + (cast x * inc) :: go xs go (x :: xs) = n + (cast x * inc) :: go xs
@ -305,7 +305,7 @@ instance Enum Int where
go acc (S k) m = go (m :: acc) k (m - 1) go acc (S k) m = go (m :: acc) k (m - 1)
enumFromThen n inc = n :: enumFromThen (inc + n) inc enumFromThen n inc = n :: enumFromThen (inc + n) inc
enumFromThenTo _ 0 _ = [] enumFromThenTo _ 0 _ = []
enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc)))) enumFromThenTo n inc m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs inc) - 1))) SIsNotZ)))
where go : List Nat -> List Int where go : List Nat -> List Int
go [] = [] go [] = []
go (x :: xs) = n + (cast x * inc) :: go xs go (x :: xs) = n + (cast x * inc) :: go xs
@ -349,7 +349,7 @@ partial
printLn : Show a => a -> IO' ffi () printLn : Show a => a -> IO' ffi ()
printLn x = putStrLn (show x) printLn x = putStrLn (show x)
||| Read one line of input from stdin ||| Read one line of input from stdin, without the trailing newline
partial partial
getLine : IO' ffi String getLine : IO' ffi String
getLine = prim_read getLine = prim_read
@ -548,5 +548,7 @@ readFile fn = do h <- openFile fn Read
readFile' h contents = readFile' h contents =
do x <- feof h do x <- feof h
if not x then do l <- fread h if not x then do l <- fread h
readFile' h (contents ++ l) case contents of
"" => readFile' h l
_ => readFile' h (contents ++ "\n" ++ l)
else return contents else return contents

36
libs/prelude/Prelude/Classes.idr
View File

@ -315,10 +315,12 @@ class Integral a where
-- ---------------------------------------------------------------- [ Integers ] -- ---------------------------------------------------------------- [ Integers ]
divBigInt : Integer -> Integer -> Integer divBigInt : Integer -> Integer -> Integer
divBigInt = prim__sdivBigInt divBigInt x y = case y == 0 of
False => prim__sdivBigInt x y
modBigInt : Integer -> Integer -> Integer modBigInt : Integer -> Integer -> Integer
modBigInt = prim__sremBigInt modBigInt x y = case y == 0 of
False => prim__sremBigInt x y
instance Integral Integer where instance Integral Integer where
div = divBigInt div = divBigInt
@ -327,10 +329,12 @@ instance Integral Integer where
-- --------------------------------------------------------------------- [ Int ] -- --------------------------------------------------------------------- [ Int ]
divInt : Int -> Int -> Int divInt : Int -> Int -> Int
divInt = prim__sdivInt divInt x y = case y == 0 of
False => prim__sdivInt x y
modInt : Int -> Int -> Int modInt : Int -> Int -> Int
modInt = prim__sremInt modInt x y = case y == 0 of
False => prim__sremInt x y
instance Integral Int where instance Integral Int where
div = divInt div = divInt
@ -338,10 +342,12 @@ instance Integral Int where
-- ------------------------------------------------------------------- [ Bits8 ] -- ------------------------------------------------------------------- [ Bits8 ]
divB8 : Bits8 -> Bits8 -> Bits8 divB8 : Bits8 -> Bits8 -> Bits8
divB8 = prim__sdivB8 divB8 x y = case y == 0 of
False => prim__sdivB8 x y
modB8 : Bits8 -> Bits8 -> Bits8 modB8 : Bits8 -> Bits8 -> Bits8
modB8 = prim__sremB8 modB8 x y = case y == 0 of
False => prim__sremB8 x y
instance Integral Bits8 where instance Integral Bits8 where
div = divB8 div = divB8
@ -349,10 +355,12 @@ instance Integral Bits8 where
-- ------------------------------------------------------------------ [ Bits16 ] -- ------------------------------------------------------------------ [ Bits16 ]
divB16 : Bits16 -> Bits16 -> Bits16 divB16 : Bits16 -> Bits16 -> Bits16
divB16 = prim__sdivB16 divB16 x y = case y == 0 of
False => prim__sdivB16 x y
modB16 : Bits16 -> Bits16 -> Bits16 modB16 : Bits16 -> Bits16 -> Bits16
modB16 = prim__sremB16 modB16 x y = case y == 0 of
False => prim__sremB16 x y
instance Integral Bits16 where instance Integral Bits16 where
div = divB16 div = divB16
@ -360,10 +368,12 @@ instance Integral Bits16 where
-- ------------------------------------------------------------------ [ Bits32 ] -- ------------------------------------------------------------------ [ Bits32 ]
divB32 : Bits32 -> Bits32 -> Bits32 divB32 : Bits32 -> Bits32 -> Bits32
divB32 = prim__sdivB32 divB32 x y = case y == 0 of
False => prim__sdivB32 x y
modB32 : Bits32 -> Bits32 -> Bits32 modB32 : Bits32 -> Bits32 -> Bits32
modB32 = prim__sremB32 modB32 x y = case y == 0 of
False => prim__sremB32 x y
instance Integral Bits32 where instance Integral Bits32 where
div = divB32 div = divB32
@ -371,10 +381,12 @@ instance Integral Bits32 where
-- ------------------------------------------------------------------ [ Bits64 ] -- ------------------------------------------------------------------ [ Bits64 ]
divB64 : Bits64 -> Bits64 -> Bits64 divB64 : Bits64 -> Bits64 -> Bits64
divB64 = prim__sdivB64 divB64 x y = case y == 0 of
False => prim__sdivB64 x y
modB64 : Bits64 -> Bits64 -> Bits64 modB64 : Bits64 -> Bits64 -> Bits64
modB64 = prim__sremB64 modB64 x y = case y == 0 of
False => prim__sremB64 x y
instance Integral Bits64 where instance Integral Bits64 where
div = divB64 div = divB64

20
libs/prelude/Prelude/List.idr
View File

@ -309,13 +309,12 @@ mapMaybe f (x::xs) =
-- Folds -- Folds
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
||| A tail recursive right fold on Lists.
total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc
foldrImpl f e go [] = go e
foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
instance Foldable List where instance Foldable List where
foldr f e xs = foldrImpl f e id xs foldr c n [] = n
foldr c n (x::xs) = c x (foldr c n xs)
foldl f q [] = q
foldl f q (x::xs) = foldl f (f q x) xs
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- Special folds -- Special folds
@ -809,6 +808,15 @@ hasAnyByNilFalse p (x::xs) =
hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
hasAnyNilFalse l = ?hasAnyNilFalseBody hasAnyNilFalse l = ?hasAnyNilFalseBody
foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z
||| The definition of foldl works the same as the default definition
||| in terms of foldr
foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs
foldlMatchesFoldr f q [] = Refl
foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- Proofs -- Proofs

53
libs/prelude/Prelude/Nat.idr
View File

@ -288,10 +288,12 @@ fact (S n) = (S n) * fact n
-- Division and modulus -- Division and modulus
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
total SIsNotZ : {x: Nat} -> (S x = Z) -> Void
modNat : Nat -> Nat -> Nat SIsNotZ Refl impossible
modNat left Z = left
modNat left (S right) = mod' left left right modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
modNatNZ left Z p = void (p Refl)
modNatNZ left (S right) _ = mod' left left right
where where
total mod' : Nat -> Nat -> Nat -> Nat total mod' : Nat -> Nat -> Nat -> Nat
mod' Z centre right = centre mod' Z centre right = centre
@ -301,10 +303,13 @@ modNat left (S right) = mod' left left right
else else
mod' left (centre - (S right)) right mod' left (centre - (S right)) right
total partial
divNat : Nat -> Nat -> Nat modNat : Nat -> Nat -> Nat
divNat left Z = S left -- div by zero modNat left (S right) = modNatNZ left (S right) SIsNotZ
divNat left (S right) = div' left left right
divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
divNatNZ left Z p = void (p Refl)
divNatNZ left (S right) _ = div' left left right
where where
total div' : Nat -> Nat -> Nat -> Nat total div' : Nat -> Nat -> Nat -> Nat
div' Z centre right = Z div' Z centre right = Z
@ -314,23 +319,42 @@ divNat left (S right) = div' left left right
else else
S (div' left (centre - (S right)) right) S (div' left (centre - (S right)) right)
partial
divNat : Nat -> Nat -> Nat
divNat left (S right) = divNatNZ left (S right) SIsNotZ
divCeilNZ : Nat -> (y: Nat) -> Not (y = 0) -> Nat
divCeilNZ x y p = case (modNatNZ x y p) of
Z => divNatNZ x y p
S _ => S (divNatNZ x y p)
partial
divCeil : Nat -> Nat -> Nat
divCeil x (S y) = divCeilNZ x (S y) SIsNotZ
instance Integral Nat where instance Integral Nat where
div = divNat div = divNat
mod = modNat mod = modNat
log2NZ : (x: Nat) -> Not (x = Z) -> Nat
log2NZ Z p = void (p Refl)
log2NZ (S Z) _ = Z
log2NZ (S (S n)) _ = S (log2NZ (assert_smaller (S (S n)) (S (divNatNZ n 2 SIsNotZ))) SIsNotZ)
partial
log2 : Nat -> Nat log2 : Nat -> Nat
log2 Z = Z log2 (S n) = log2NZ (S n) SIsNotZ
log2 (S Z) = Z
log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- GCD and LCM -- GCD and LCM
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
partial
gcd : Nat -> Nat -> Nat gcd : Nat -> Nat -> Nat
gcd a Z = a gcd a Z = a
gcd a b = assert_total (gcd b (a `modNat` b)) gcd a b = assert_total (gcd b (a `modNat` b))
total lcm : Nat -> Nat -> Nat partial
lcm : Nat -> Nat -> Nat
lcm _ Z = Z lcm _ Z = Z
lcm Z _ = Z lcm Z _ = Z
lcm x y = divNat (x * y) (gcd x y) lcm x y = divNat (x * y) (gcd x y)
@ -724,11 +748,6 @@ total sucMinR : (l : Nat) -> minimum l (S l) = l
sucMinR Z = Refl sucMinR Z = Refl
sucMinR (S l) = cong (sucMinR l) sucMinR (S l) = cong (sucMinR l)
-- div and mod
total modZeroZero : (n : Nat) -> mod 0 n = Z
modZeroZero Z = Refl
modZeroZero (S n) = Refl
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- Proofs -- Proofs
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------

2
libs/prelude/prelude.ipkg
View File

@ -10,7 +10,7 @@ modules = Builtins, Prelude, IO,
Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream, Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers, Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
Language.Reflection, Language.Reflection.Errors, Language.Reflection.Tactical, Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
Decidable.Equality Decidable.Equality

7
rts/idris_rts.c
View File

@ -504,17 +504,20 @@ VAL idris_strlen(VM* vm, VAL l) {
} }
VAL idris_readStr(VM* vm, FILE* h) { VAL idris_readStr(VM* vm, FILE* h) {
VAL ret;
char *buffer = NULL; char *buffer = NULL;
size_t n = 0; size_t n = 0;
ssize_t len; ssize_t len;
len = getline(&buffer, &n, h); len = getline(&buffer, &n, h);
strtok(buffer, "\n");
if (len <= 0) { if (len <= 0) {
return MKSTR(vm, ""); ret = MKSTR(vm, "");
} else { } else {
return MKSTR(vm, buffer); ret = MKSTR(vm, buffer);
} }
free(buffer); free(buffer);
return ret;
} }
VAL idris_strHead(VM* vm, VAL str) { VAL idris_strHead(VM* vm, VAL str) {

8
src/Idris/AbsSyntax.hs
View File

@ -1011,7 +1011,7 @@ expandParams dec ps ns infs tm = en tm
en (PApp fc f as) = PApp fc (en f) (map (fmap en) as) en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as) en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
en (PCase fc c os) = PCase fc (en c) (map (pmap en) os) en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
en (PRunTactics fc tm) = PRunTactics fc (en tm) en (PRunElab fc tm) = PRunElab fc (en tm)
en t = t en t = t
nselem x [] = False nselem x [] = False
@ -1485,7 +1485,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
imps top env (PHidden tm) = imps False env tm imps top env (PHidden tm) = imps False env tm
imps top env (PUnifyLog tm) = imps False env tm imps top env (PUnifyLog tm) = imps False env tm
imps top env (PNoImplicits tm) = imps False env tm imps top env (PNoImplicits tm) = imps False env tm
imps top env (PRunTactics fc tm) = imps False env tm imps top env (PRunElab fc tm) = imps False env tm
imps top env _ = return () imps top env _ = return ()
pibind using [] sc = sc pibind using [] sc = sc
@ -1612,7 +1612,7 @@ addImpl' inpat env infns imp_meths ist ptm
ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm) ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
(fmap (ai True env ds) g) (fmap (ai True env ds) g)
ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm) ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm) ai qq env ds (PRunElab fc tm) = PRunElab fc (ai False env ds tm)
ai qq env ds tm = tm ai qq env ds tm = tm
handleErr (Left err) = PElabError err handleErr (Left err) = PElabError err
@ -2149,5 +2149,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t) mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts) mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts) mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
mkUniq (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts) mkUniq (PRunElab fc ts) = liftM (PRunElab fc ) (mkUniq ts)
mkUniq t = return t mkUniq t = return t

27
src/Idris/AbsSyntaxTree.hs
View File

@ -645,11 +645,16 @@ deriving instance Binary PDecl'
deriving instance NFData PDecl' deriving instance NFData PDecl'
!-} !-}
-- For elaborator state -- | A set of instructions for things that need to happen in IState
-- after a term elaboration when there's been reflected elaboration.
data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
| RClausesInstrs Name [([Name], Term, Term)]
-- | For elaborator state
data EState = EState { data EState = EState {
case_decls :: [PDecl], case_decls :: [PDecl],
delayed_elab :: [Elab' EState ()], delayed_elab :: [Elab' EState ()],
new_tyDecls :: [(Name, FC, [PArg], Type)] new_tyDecls :: [RDeclInstructions]
} }
initEState :: EState initEState :: EState
@ -821,7 +826,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
| PNoImplicits PTerm -- ^ never run implicit converions on the term | PNoImplicits PTerm -- ^ never run implicit converions on the term
| PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term]) | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
| PUnquote PTerm -- ^ ~Term | PUnquote PTerm -- ^ ~Term
| PRunTactics FC PTerm -- ^ %runTactics tm - New-style proof script | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script
deriving (Eq, Data, Typeable) deriving (Eq, Data, Typeable)
@ -1428,16 +1433,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
prettySe p bnd (PLam fc n ty sc) = prettySe p bnd (PLam fc n ty sc) =
bracket p startPrec . group . align . hang 2 $ bracket p startPrec . group . align . hang 2 $
text "\\" <> bindingOf n False <+> text "=>" <$> text "\\" <> prettyBindingOf n False <+> text "=>" <$>
prettySe startPrec ((n, False):bnd) sc prettySe startPrec ((n, False):bnd) sc
prettySe p bnd (PLet fc n ty v sc) = prettySe p bnd (PLet fc n ty v sc) =
bracket p startPrec . group . align $ bracket p startPrec . group . align $
kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </> kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc) kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
prettySe p bnd (PPi (Exp l s _) n ty sc) prettySe p bnd (PPi (Exp l s _) n ty sc)
| n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs = | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
bracket p startPrec . group $ bracket p startPrec . group $
enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+> enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
| otherwise = | otherwise =
bracket p startPrec . group $ bracket p startPrec . group $
@ -1450,7 +1455,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
prettySe p bnd (PPi (Imp l s _ fa) n ty sc) prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
| ppopt_impl ppo = | ppopt_impl ppo =
bracket p startPrec $ bracket p startPrec $
lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+> lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
st <> text "->" </> prettySe startPrec ((n, True):bnd) sc st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
| otherwise = prettySe startPrec ((n, True):bnd) sc | otherwise = prettySe startPrec ((n, True):bnd) sc
where where
@ -1607,6 +1612,14 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
prettySe p bnd _ = text "missing pretty-printer for term" prettySe p bnd _ = text "missing pretty-printer for term"
prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
where display (UN n) = T.unpack n
display (MN _ n) = T.unpack n
-- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
display n = show n
prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm) prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

7
src/Idris/Core/TT.hs
View File

@ -117,9 +117,6 @@ data ErrorReportPart = TextPart String
deriving (Show, Eq, Data, Typeable) deriving (Show, Eq, Data, Typeable)
-- Please remember to keep Err synchronised with
-- Language.Reflection.Errors.Err in the stdlib!
data Provenance = ExpectedType data Provenance = ExpectedType
| TooManyArgs Term | TooManyArgs Term
| InferredVal | InferredVal
@ -131,6 +128,10 @@ deriving instance NFData Err
deriving instance Binary Err deriving instance Binary Err
!-} !-}
-- NB: Please remember to keep Err synchronised with
-- Language.Reflection.Errors.Err in the stdlib!
-- | Idris errors. Used as exceptions in the compiler, but reported to users -- | Idris errors. Used as exceptions in the compiler, but reported to users
-- if they reach the top level. -- if they reach the top level.
data Err' t data Err' t

4
src/Idris/DSL.hs
View File

@ -108,7 +108,7 @@ expandDo dsl (PDoBlock ds)
block b _ = PElabError (Msg "Invalid statement in do block") block b _ = PElabError (Msg "Invalid statement in do block")
expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
expandDo dsl (PRunTactics fc tm) = PRunTactics fc $ expandDo dsl tm expandDo dsl (PRunElab fc tm) = PRunElab fc $ expandDo dsl tm
expandDo dsl t = t expandDo dsl t = t
-- | Replace DSL-bound variable in a term -- | Replace DSL-bound variable in a term
@ -195,7 +195,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
db' (PDPair fc p l t r) = do l' <- db' l db' (PDPair fc p l t r) = do l' <- db' l
r' <- db' r r' <- db' r
return (PDPair fc p l' t r') return (PDPair fc p l' t r')
db' (PRunTactics fc t) = fmap (PRunTactics fc) (db' t) db' (PRunElab fc t) = fmap (PRunElab fc) (db' t)
db' t = return t db' t = return t
dbArg a = do t' <- db' (getTm a) dbArg a = do t' <- db' (getTm a)

2
src/Idris/DeepSeq.hs
View File

@ -243,7 +243,7 @@ instance NFData PTerm where
rnf (PNoImplicits x1) = rnf x1 `seq` () rnf (PNoImplicits x1) = rnf x1 `seq` ()
rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` () rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
rnf (PUnquote x1) = rnf x1 `seq` () rnf (PUnquote x1) = rnf x1 `seq` ()
rnf (PRunTactics x1 x2) = rnf x1 `seq` rnf x2 `seq` () rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
instance (NFData t) => NFData (PTactic' t) where instance (NFData t) => NFData (PTactic' t) where
rnf (Intro x1) = rnf x1 `seq` () rnf (Intro x1) = rnf x1 `seq` ()

935
src/Idris/Elab/Term.hs
View File

File diff suppressed because it is too large Load Diff

4
src/Idris/ElabQuasiquote.hs
View File

@ -170,8 +170,8 @@ extractUnquotes n (PUnquote tm)
return (PRef (fileFC "(unquote)") n, [(n, tm)]) return (PRef (fileFC "(unquote)") n, [(n, tm)])
| otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $ | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
extractUnquotes (n-1) tm extractUnquotes (n-1) tm
extractUnquotes n (PRunTactics fc tm) extractUnquotes n (PRunElab fc tm)
= fmap (\(tm', ex) -> (PRunTactics fc tm', ex)) $ extractUnquotes n tm = fmap (\(tm', ex) -> (PRunElab fc tm', ex)) $ extractUnquotes n tm
extractUnquotes n x = return (x, []) -- no subterms! extractUnquotes n x = return (x, []) -- no subterms!

2
src/Idris/Error.hs
View File

@ -148,4 +148,4 @@ warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
warnDisamb ist (PUnquote tm) = warnDisamb ist tm warnDisamb ist (PUnquote tm) = warnDisamb ist tm
warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
warnDisamb ist (PRunTactics _ tm) = warnDisamb ist tm warnDisamb ist (PRunElab _ tm) = warnDisamb ist tm

8
src/Idris/IBC.hs
View File

@ -1674,9 +1674,9 @@ instance Binary PTerm where
put x2 put x2
PUniverse x1 -> do putWord8 38 PUniverse x1 -> do putWord8 38
put x1 put x1
PRunTactics x1 x2 -> do putWord8 39 PRunElab x1 x2 -> do putWord8 39
put x1 put x1
put x2 put x2
PAs x1 x2 x3 -> do putWord8 40 PAs x1 x2 x3 -> do putWord8 40
put x1 put x1
put x2 put x2
@ -1809,7 +1809,7 @@ instance Binary PTerm where
return (PUniverse x1) return (PUniverse x1)
39 -> do x1 <- get 39 -> do x1 <- get
x2 <- get x2 <- get
return (PRunTactics x1 x2) return (PRunElab x1 x2)
40 -> do x1 <- get 40 -> do x1 <- get
x2 <- get x2 <- get
x3 <- get x3 <- get

2
src/Idris/IdrisDoc.hs
View File

@ -321,7 +321,7 @@ extractPTermNames (PCoerced p) = extract p
extractPTermNames (PDisamb _ p) = extract p extractPTermNames (PDisamb _ p) = extract p
extractPTermNames (PUnifyLog p) = extract p extractPTermNames (PUnifyLog p) = extract p
extractPTermNames (PNoImplicits p) = extract p extractPTermNames (PNoImplicits p) = extract p
extractPTermNames (PRunTactics _ p) = extract p extractPTermNames (PRunElab _ p) = extract p
extractPTermNames _ = [] extractPTermNames _ = []
-- | Shorter name for extractPTermNames -- | Shorter name for extractPTermNames

18
src/Idris/ParseExpr.hs
View File

@ -220,7 +220,7 @@ InternalExpr ::=
internalExpr :: SyntaxInfo -> IdrisParser PTerm internalExpr :: SyntaxInfo -> IdrisParser PTerm
internalExpr syn = internalExpr syn =
unifyLog syn unifyLog syn
<|> runTactics syn <|> runElab syn
<|> disamb syn <|> disamb syn
<|> noImplicits syn <|> noImplicits syn
<|> recordType syn <|> recordType syn
@ -497,16 +497,16 @@ unifyLog syn = do try (lchar '%' *> reserved "unifyLog")
{- | Parses a new-style tactics expression {- | Parses a new-style tactics expression
RunTactics ::= RunTactics ::=
'%' 'runTactics' SimpleExpr '%' 'runElab' SimpleExpr
; ;
-} -}
runTactics :: SyntaxInfo -> IdrisParser PTerm runElab :: SyntaxInfo -> IdrisParser PTerm
runTactics syn = do try (lchar '%' *> reserved "runTactics") runElab syn = do try (lchar '%' *> reserved "runElab")
fc <- getFC fc <- getFC
tm <- simpleExpr syn tm <- simpleExpr syn
i <- get i <- get
return $ PRunTactics fc tm return $ PRunElab fc tm
<?> "new-style tactics expression" <?> "new-style tactics expression"
{- | Parses a disambiguation expression {- | Parses a disambiguation expression
Disamb ::= Disamb ::=

886
src/Idris/Reflection.hs
View File

@ -1,10 +1,22 @@
{-| {-| Code related to Idris's reflection system. This module contains
Handy tools for doing reflection. quoters and unquoters along with some supporting datatypes.
-} -}
{-# LANGUAGE PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Idris.Reflection where module Idris.Reflection where
import Control.Monad (liftM, liftM2)
import Data.List ((\\))
import qualified Data.Text as T
import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
movelast, runElab, solve)
import Idris.Core.Evaluate (initContext)
import Idris.Core.TT import Idris.Core.TT
import Idris.AbsSyntaxTree (PArg'(..), PArg, PTerm(Placeholder))
import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),
PTerm(..), initEState, pairCon, pairTy)
import Idris.Delaborate (delab)
data RArg = RExplicit { argName :: Name, argTy :: Raw } data RArg = RExplicit { argName :: Name, argTy :: Raw }
| RImplicit { argName :: Name, argTy :: Raw } | RImplicit { argName :: Name, argTy :: Raw }
@ -16,3 +28,871 @@ rArgToPArg :: RArg -> PArg
rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder
data RFunClause = RMkFunClause Raw Raw
| RMkImpossibleClause Raw
deriving Show
data RFunDefn = RDefineFun Name [RFunClause] deriving Show
-- | Prefix a name with the "Language.Reflection" namespace
reflm :: String -> Name
reflm n = sNS (sUN n) ["Reflection", "Language"]
-- | Prefix a name with the "Language.Reflection.Elab" namespace
tacN :: String -> Name
tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]
-- | Reify tactics from their reflected representation
reify :: IState -> Term -> ElabD PTactic
reify _ (P _ n _) | n == reflm "Intros" = return Intros
reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
reify _ (P _ n _) | n == reflm "Solve" = return Solve
reify _ (P _ n _) | n == reflm "Compute" = return Compute
reify _ (P _ n _) | n == reflm "Skip" = return Skip
reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
reify ist t@(App _ _ _)
| (P _ f _, args) <- unApply t = reifyApp ist f args
reify _ t = fail ("Unknown tactic " ++ show t)
reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
reifyApp _ t [Constant (I i)]
| t == reflm "Search" = return (ProofSearch True True i Nothing [])
reifyApp _ t [x]
| t == reflm "Refine" = do n <- reifyTTName x
return $ Refine n []
reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
goal <- reifyTT ty
return $ Claim n' (delab ist goal)
reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
reifyApp ist t [Constant (Str n), x]
| t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
reifyApp ist t [t']
| t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
reifyApp ist t [t']
| t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
reifyApp ist t [t']
| t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
reifyApp _ t [t']
| t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
reifyApp ist t [t']
| t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
reifyApp ist t [x]
| t == reflm "Focus" = liftM Focus (reifyTTName x)
reifyApp ist t [t']
| t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
reifyApp ist t [n, t']
| t == reflm "LetTac" = do n' <- reifyTTName n
t'' <- reifyTT t'
return $ LetTac n' (delab ist t')
reifyApp ist t [n, tt', t']
| t == reflm "LetTacTy" = do n' <- reifyTTName n
tt'' <- reifyTT tt'
t'' <- reifyTT t'
return $ LetTacTy n' (delab ist tt'') (delab ist t'')
reifyApp ist t [errs]
| t == reflm "Fail" = fmap TFail (reifyReportParts errs)
reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
reifyReportParts :: Term -> ElabD [ErrorReportPart]
reifyReportParts errs =
case unList errs of
Nothing -> fail "Failed to reify errors"
Just errs' ->
let parts = mapM reifyReportPart errs' in
case parts of
Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
Right errs'' ->
return errs''
-- | Reify terms from their reflected representation
reifyTT :: Term -> ElabD Term
reifyTT t@(App _ _ _)
| (P _ f _, args) <- unApply t = reifyTTApp f args
reifyTT t@(P _ n _)
| n == reflm "Erased" = return $ Erased
reifyTT t@(P _ n _)
| n == reflm "Impossible" = return $ Impossible
reifyTT t = fail ("Unknown reflection term: " ++ show t)
reifyTTApp :: Name -> [Term] -> ElabD Term
reifyTTApp t [nt, n, x]
| t == reflm "P" = do nt' <- reifyTTNameType nt
n' <- reifyTTName n
x' <- reifyTT x
return $ P nt' n' x'
reifyTTApp t [Constant (I i)]
| t == reflm "V" = return $ V i
reifyTTApp t [n, b, x]
| t == reflm "Bind" = do n' <- reifyTTName n
b' <- reifyTTBinder reifyTT (reflm "TT") b
x' <- reifyTT x
return $ Bind n' b' x'
reifyTTApp t [f, x]
| t == reflm "App" = do f' <- reifyTT f
x' <- reifyTT x
return $ App Complete f' x'
reifyTTApp t [c]
| t == reflm "TConst" = liftM Constant (reifyTTConst c)
reifyTTApp t [t', Constant (I i)]
| t == reflm "Proj" = do t'' <- reifyTT t'
return $ Proj t'' i
reifyTTApp t [tt]
| t == reflm "TType" = liftM TType (reifyTTUExp tt)
reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
-- | Reify raw terms from their reflected representation
reifyRaw :: Term -> ElabD Raw
reifyRaw t@(App _ _ _)
| (P _ f _, args) <- unApply t = reifyRawApp f args
reifyRaw t@(P _ n _)
| n == reflm "RType" = return $ RType
reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
reifyRawApp :: Name -> [Term] -> ElabD Raw
reifyRawApp t [n]
| t == reflm "Var" = liftM Var (reifyTTName n)
reifyRawApp t [n, b, x]
| t == reflm "RBind" = do n' <- reifyTTName n
b' <- reifyTTBinder reifyRaw (reflm "Raw") b
x' <- reifyRaw x
return $ RBind n' b' x'
reifyRawApp t [f, x]
| t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
reifyRawApp t [t']
| t == reflm "RForce" = liftM RForce (reifyRaw t')
reifyRawApp t [c]
| t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
reifyTTName :: Term -> ElabD Name
reifyTTName t
| (P _ f _, args) <- unApply t = reifyTTNameApp f args
reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
reifyTTNameApp :: Name -> [Term] -> ElabD Name
reifyTTNameApp t [Constant (Str n)]
| t == reflm "UN" = return $ sUN n
reifyTTNameApp t [n, ns]
| t == reflm "NS" = do n' <- reifyTTName n
ns' <- reifyTTNamespace ns
return $ sNS n' ns'
reifyTTNameApp t [Constant (I i), Constant (Str n)]
| t == reflm "MN" = return $ sMN i n
reifyTTNameApp t []
| t == reflm "NErased" = return NErased
reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
reifyTTNamespace :: Term -> ElabD [String]
reifyTTNamespace t@(App _ _ _)
= case unApply t of
(P _ f _, [Constant StrType])
| f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
(P _ f _, [Constant StrType, Constant (Str n), ns])
| f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
_ -> fail ("Unknown reflection namespace arg: " ++ show t)
reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
reifyTTNameType :: Term -> ElabD NameType
reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
reifyTTNameType t@(App _ _ _)
= case unApply t of
(P _ f _, [Constant (I tag), Constant (I num)])
| f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!
| f == reflm "TCon" -> return $ TCon tag num
_ -> fail ("Unknown reflection name type: " ++ show t)
reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder reificator binderType t@(App _ _ _)
= case unApply t of
(P _ f _, bt:args) | forget bt == Var binderType
-> reifyTTBinderApp reificator f args
_ -> fail ("Mismatching binder reflection: " ++ show t)
reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
reifyTTBinderApp reif f [t]
| f == reflm "Lam" = liftM Lam (reif t)
reifyTTBinderApp reif f [t, k]
| f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
reifyTTBinderApp reif f [x, y]
| f == reflm "Let" = liftM2 Let (reif x) (reif y)
reifyTTBinderApp reif f [x, y]
| f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
reifyTTBinderApp reif f [t]
| f == reflm "Hole" = liftM Hole (reif t)
reifyTTBinderApp reif f [t]
| f == reflm "GHole" = liftM (GHole 0) (reif t)
reifyTTBinderApp reif f [x, y]
| f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
reifyTTBinderApp reif f [t]
| f == reflm "PVar" = liftM PVar (reif t)
reifyTTBinderApp reif f [t]
| f == reflm "PVTy" = liftM PVTy (reif t)
reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
reifyTTConst :: Term -> ElabD Const
reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
reifyTTConst t@(App _ _ _)
| (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
reifyTTConstApp :: Name -> Term -> ElabD Const
reifyTTConstApp f aty
| f == reflm "AType" = fmap AType (reifyArithTy aty)
reifyTTConstApp f (Constant c@(I _))
| f == reflm "I" = return $ c
reifyTTConstApp f (Constant c@(BI _))
| f == reflm "BI" = return $ c
reifyTTConstApp f (Constant c@(Fl _))
| f == reflm "Fl" = return $ c
reifyTTConstApp f (Constant c@(I _))
| f == reflm "Ch" = return $ c
reifyTTConstApp f (Constant c@(Str _))
| f == reflm "Str" = return $ c
reifyTTConstApp f (Constant c@(B8 _))
| f == reflm "B8" = return $ c
reifyTTConstApp f (Constant c@(B16 _))
| f == reflm "B16" = return $ c
reifyTTConstApp f (Constant c@(B32 _))
| f == reflm "B32" = return $ c
reifyTTConstApp f (Constant c@(B64 _))
| f == reflm "B64" = return $ c
reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
reifyArithTy :: Term -> ElabD ArithTy
reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
reifyNativeTy :: Term -> ElabD NativeTy
reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
reifyIntTy :: Term -> ElabD IntTy
reifyIntTy (App _ (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
reifyTTUExp :: Term -> ElabD UExp
reifyTTUExp t@(App _ _ _)
= case unApply t of
(P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
(P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
_ -> fail ("Unknown reflection type universe expression: " ++ show t)
reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
-- | Create a reflected call to a named function/constructor
reflCall :: String -> [Raw] -> Raw
reflCall funName args
= raw_apply (Var (reflm funName)) args
-- | Lift a term into its Language.Reflection.TT representation
reflect :: Term -> Raw
reflect = reflectTTQuote []
-- | Lift a term into its Language.Reflection.Raw representation
reflectRaw :: Raw -> Raw
reflectRaw = reflectRawQuote []
claimTT :: Name -> ElabD Name
claimTT n = do n' <- getNameFrom n
claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
return n'
-- | Convert a reflected term to a more suitable form for pattern-matching.
-- In particular, the less-interesting bits are elaborated to _ patterns. This
-- happens to NameTypes, universe levels, names that are bound but not used,
-- and the type annotation field of the P constructor.
reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
reflectTTQuotePattern unq (P _ n _)
| n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
do fill (Var n) ; solve
| otherwise =
do tyannot <- claimTT (sMN 0 "pTyAnnot")
movelast tyannot -- use a _ pattern here
nt <- getNameFrom (sMN 0 "nt")
claim nt (Var (reflm "NameType"))
movelast nt -- use a _ pattern here
n' <- getNameFrom (sMN 0 "n")
claim n' (Var (reflm "TTName"))
fill $ reflCall "P" [Var nt, Var n', Var tyannot]
solve
focus n'; reflectNameQuotePattern n
reflectTTQuotePattern unq (V n)
= do fill $ reflCall "V" [RConstant (I n)]
solve
reflectTTQuotePattern unq (Bind n b x)
= do x' <- claimTT (sMN 0 "sc")
movelast x'
b' <- getNameFrom (sMN 0 "binder")
claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
(Var (sNS (sUN "TT") ["Reflection", "Language"])))
if n `elem` freeNames x
then do fill $ reflCall "Bind"
[reflectName n,
Var b',
Var x']
solve
else do any <- getNameFrom (sMN 0 "anyName")
claim any (Var (reflm "TTName"))
movelast any
fill $ reflCall "Bind"
[Var any,
Var b',
Var x']
solve
focus x'; reflectTTQuotePattern unq x
focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
reflectTTQuotePattern unq (App _ f x)
= do f' <- claimTT (sMN 0 "f"); movelast f'
x' <- claimTT (sMN 0 "x"); movelast x'
fill $ reflCall "App" [Var f', Var x']
solve
focus f'; reflectTTQuotePattern unq f
focus x'; reflectTTQuotePattern unq x
reflectTTQuotePattern unq (Constant c)
= do fill $ reflCall "TConst" [reflectConstant c]
solve
reflectTTQuotePattern unq (Proj t i)
= do t' <- claimTT (sMN 0 "t"); movelast t'
fill $ reflCall "Proj" [Var t', RConstant (I i)]
solve
focus t'; reflectTTQuotePattern unq t
reflectTTQuotePattern unq (Erased)
= do erased <- claimTT (sMN 0 "erased")
movelast erased
fill $ (Var erased)
solve
reflectTTQuotePattern unq (Impossible)
= do fill $ Var (reflm "Impossible")
solve
reflectTTQuotePattern unq (TType exp)
= do ue <- getNameFrom (sMN 0 "uexp")
claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
movelast ue
fill $ reflCall "TType" [Var ue]
solve
reflectTTQuotePattern unq (UType u)
= do uH <- getNameFrom (sMN 0 "someUniv")
claim uH (Var (reflm "Universe"))
movelast uH
fill $ reflCall "UType" [Var uH]
solve
focus uH
fill (Var (reflm (case u of
NullType -> "NullType"
UniqueType -> "UniqueType"
AllTypes -> "AllTypes")))
solve
reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
reflectRawQuotePattern unq (Var n)
-- the unquoted names already have types, just use them
| n `elem` unq = do fill (Var n); solve
| otherwise = do fill (reflCall "Var" [reflectName n]); solve
reflectRawQuotePattern unq (RBind n b sc) =
do scH <- getNameFrom (sMN 0 "sc")
claim scH (Var (reflm "Raw"))
movelast scH
bH <- getNameFrom (sMN 0 "binder")
claim bH (RApp (Var (reflm "Binder"))
(Var (reflm "Raw")))
if n `elem` freeNamesR sc
then do fill $ reflCall "RBind" [reflectName n,
Var bH,
Var scH]
solve
else do any <- getNameFrom (sMN 0 "anyName")
claim any (Var (reflm "TTName"))
movelast any
fill $ reflCall "RBind" [Var any, Var bH, Var scH]
solve
focus scH; reflectRawQuotePattern unq sc
focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
where freeNamesR (Var n) = [n]
freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
freeNamesR body \\ [n],
freeNamesR t]
freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
(freeNamesR body \\ [n])
freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
freeNamesR RType = []
freeNamesR (RUType _) = []
freeNamesR (RForce r) = freeNamesR r
freeNamesR (RConstant _) = []
reflectRawQuotePattern unq (RApp f x) =
do fH <- getNameFrom (sMN 0 "f")
claim fH (Var (reflm "Raw"))
movelast fH
xH <- getNameFrom (sMN 0 "x")
claim xH (Var (reflm "Raw"))
movelast xH
fill $ reflCall "RApp" [Var fH, Var xH]
solve
focus fH; reflectRawQuotePattern unq f
focus xH; reflectRawQuotePattern unq x
reflectRawQuotePattern unq RType =
do fill (Var (reflm "RType"))
solve
reflectRawQuotePattern unq (RUType univ) =
do uH <- getNameFrom (sMN 0 "universe")
claim uH (Var (reflm "Universe"))
movelast uH
fill $ reflCall "RUType" [Var uH]
solve
focus uH; fill (reflectUniverse univ); solve
reflectRawQuotePattern unq (RForce r) =
do rH <- getNameFrom (sMN 0 "raw")
claim rH (Var (reflm "Raw"))
movelast rH
fill $ reflCall "RForce" [Var rH]
solve
focus rH; reflectRawQuotePattern unq r
reflectRawQuotePattern unq (RConstant c) =
do cH <- getNameFrom (sMN 0 "const")
claim cH (Var (reflm "Constant"))
movelast cH
fill (reflCall "RConstant" [Var cH]); solve
focus cH
fill (reflectConstant c); solve
reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
reflectBinderQuotePattern q unq (Lam t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
solve
focus t'; q unq t
reflectBinderQuotePattern q unq (Pi _ t k)
= do t' <- claimTT (sMN 0 "ty") ; movelast t'
k' <- claimTT (sMN 0 "k"); movelast k';
fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
solve
focus t'; q unq t
reflectBinderQuotePattern q unq (Let x y)
= do x' <- claimTT (sMN 0 "ty"); movelast x';
y' <- claimTT (sMN 0 "v"); movelast y';
fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
solve
focus x'; q unq x
focus y'; q unq y
reflectBinderQuotePattern q unq (NLet x y)
= do x' <- claimTT (sMN 0 "ty"); movelast x'
y' <- claimTT (sMN 0 "v"); movelast y'
fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
solve
focus x'; q unq x
focus y'; q unq y
reflectBinderQuotePattern q unq (Hole t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
solve
focus t'; q unq t
reflectBinderQuotePattern q unq (GHole _ t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
solve
focus t'; q unq t
reflectBinderQuotePattern q unq (Guess x y)
= do x' <- claimTT (sMN 0 "ty"); movelast x'
y' <- claimTT (sMN 0 "v"); movelast y'
fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
solve
focus x'; q unq x
focus y'; q unq y
reflectBinderQuotePattern q unq (PVar t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
solve
focus t'; q unq t
reflectBinderQuotePattern q unq (PVTy t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
solve
focus t'; q unq t
reflectUniverse :: Universe -> Raw
reflectUniverse u =
(Var (reflm (case u of
NullType -> "NullType"
UniqueType -> "UniqueType"
AllTypes -> "AllTypes")))
-- | Create a reflected TT term, but leave refs to the provided name intact
reflectTTQuote :: [Name] -> Term -> Raw
reflectTTQuote unq (P nt n t)
| n `elem` unq = Var n
| otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
reflectTTQuote unq (V n)
= reflCall "V" [RConstant (I n)]
reflectTTQuote unq (Bind n b x)
= reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
reflectTTQuote unq (App _ f x)
= reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
reflectTTQuote unq (Constant c)
= reflCall "TConst" [reflectConstant c]
reflectTTQuote unq (Proj t i)
= reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
reflectTTQuote unq (Erased) = Var (reflm "Erased")
reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
reflectRawQuote :: [Name] -> Raw -> Raw
reflectRawQuote unq (Var n)
| n `elem` unq = Var n
| otherwise = reflCall "Var" [reflectName n]
reflectRawQuote unq (RBind n b r) =
reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
reflectRawQuote unq (RApp f x) =
reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
reflectRawQuote unq RType = Var (reflm "RType")
reflectRawQuote unq (RUType u) =
reflCall "RUType" [reflectUniverse u]
reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
reflectNameType :: NameType -> Raw
reflectNameType (Bound) = Var (reflm "Bound")
reflectNameType (Ref) = Var (reflm "Ref")
reflectNameType (DCon x y _)
= reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!
reflectNameType (TCon x y)
= reflCall "TCon" [RConstant (I x), RConstant (I y)]
reflectName :: Name -> Raw
reflectName (UN s)
= reflCall "UN" [RConstant (Str (str s))]
reflectName (NS n ns)
= reflCall "NS" [ reflectName n
, foldr (\ n s ->
raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
[ RConstant StrType, RConstant (Str n), s ])
( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
[ RConstant StrType ])
(map str ns)
]
reflectName (MN i n)
= reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
reflectName (NErased) = Var (reflm "NErased")
reflectName n = Var (reflm "NErased") -- special name, not yet implemented
-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
-- MNs corresponding to will care about the string but not the number. All
-- others become _.
reflectNameQuotePattern :: Name -> ElabD ()
reflectNameQuotePattern n@(UN s)
= do fill $ reflectName n
solve
reflectNameQuotePattern n@(NS _ _)
= do fill $ reflectName n
solve
reflectNameQuotePattern (MN _ n)
= do i <- getNameFrom (sMN 0 "mnCounter")
claim i (RConstant (AType (ATInt ITNative)))
movelast i
fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
solve
reflectNameQuotePattern _ -- for all other names, match any
= do nameHole <- getNameFrom (sMN 0 "name")
claim nameHole (Var (reflm "TTName"))
movelast nameHole
fill (Var nameHole)
solve
reflectBinder :: Binder Term -> Raw
reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
reflectBinderQuote q ty unq (Lam t)
= reflCall "Lam" [Var ty, q unq t]
reflectBinderQuote q ty unq (Pi _ t k)
= reflCall "Pi" [Var ty, q unq t, q unq k]
reflectBinderQuote q ty unq (Let x y)
= reflCall "Let" [Var ty, q unq x, q unq y]
reflectBinderQuote q ty unq (NLet x y)
= reflCall "NLet" [Var ty, q unq x, q unq y]
reflectBinderQuote q ty unq (Hole t)
= reflCall "Hole" [Var ty, q unq t]
reflectBinderQuote q ty unq (GHole _ t)
= reflCall "GHole" [Var ty, q unq t]
reflectBinderQuote q ty unq (Guess x y)
= reflCall "Guess" [Var ty, q unq x, q unq y]
reflectBinderQuote q ty unq (PVar t)
= reflCall "PVar" [Var ty, q unq t]
reflectBinderQuote q ty unq (PVTy t)
= reflCall "PVTy" [Var ty, q unq t]
mkList :: Raw -> [Raw] -> Raw
mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
x)
(mkList ty xs)
reflectConstant :: Const -> Raw
reflectConstant c@(I _) = reflCall "I" [RConstant c]
reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
reflectConstant StrType = Var (reflm "StrType")
reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
reflectConstant VoidType = Var (reflm "VoidType")
reflectConstant Forgot = Var (reflm "Forgot")
reflectConstant WorldType = Var (reflm "WorldType")
reflectConstant TheWorld = Var (reflm "TheWorld")
reflectUExp :: UExp -> Raw
reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
-- | Reflect the environment of a proof into a List (TTName, Binder TT)
reflectEnv :: Env -> Raw
reflectEnv = foldr consToEnvList emptyEnvList
where
consToEnvList :: (Name, Binder Term) -> Raw -> Raw
consToEnvList (n, b) l
= raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
[ envTupleType
, raw_apply (Var pairCon) [ (Var $ reflm "TTName")
, (RApp (Var $ reflm "Binder")
(Var $ reflm "TT"))
, reflectName n
, reflectBinder b
]
, l
]
emptyEnvList :: Raw
emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
[envTupleType]
-- | Reflect an error into the internal datatype of Idris -- TODO
rawBool :: Bool -> Raw
rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
rawNil :: Raw -> Raw
rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
rawCons :: Raw -> Raw -> Raw -> Raw
rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
rawList :: Raw -> [Raw] -> Raw
rawList ty = foldr (rawCons ty) (rawNil ty)
rawPairTy :: Raw -> Raw -> Raw
rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
reflectCtxt :: [(Name, Type)] -> Raw
reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
(map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
(reflectName n, reflect t)))
ctxt)
reflectErr :: Err -> Raw
reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
raw_apply (Var $ reflErrName "CantUnify")
[ rawBool b
, reflect t1
, reflect t2
, reflectErr e
, reflectCtxt ctxt
, RConstant (I i)]
reflectErr (InfiniteUnify n tm ctxt) =
raw_apply (Var $ reflErrName "InfiniteUnify")
[ reflectName n
, reflect tm
, reflectCtxt ctxt
]
reflectErr (CantConvert t t' ctxt) =
raw_apply (Var $ reflErrName "CantConvert")
[ reflect t
, reflect t'
, reflectCtxt ctxt
]
reflectErr (CantSolveGoal t ctxt) =
raw_apply (Var $ reflErrName "CantSolveGoal")
[ reflect t
, reflectCtxt ctxt
]
reflectErr (UnifyScope n n' t ctxt) =
raw_apply (Var $ reflErrName "UnifyScope")
[ reflectName n
, reflectName n'
, reflect t
, reflectCtxt ctxt
]
reflectErr (CantInferType str) =
raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
reflectErr (NonFunctionType t t') =
raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
reflectErr (NotEquality t t') =
raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
reflectErr (NotInjective t1 t2 t3) =
raw_apply (Var $ reflErrName "NotInjective")
[ reflect t1
, reflect t2
, reflect t3
]
reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
reflectErr (CantResolveAlts ss) =
raw_apply (Var $ reflErrName "CantResolveAlts")
[rawList (Var $ reflm "TTName") (map reflectName ss)]
reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
reflectErr (NoEliminator str t)
= raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),
reflect t]
reflectErr UniverseError = Var $ reflErrName "UniverseError"
reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
reflectErr (ProviderError str) =
raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
reflectErr (LoadingFailed str err) =
raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
-- | Reflect a file context
reflectFC :: FC -> Raw
reflectFC fc = raw_apply (Var (reflm "FileLoc"))
[ RConstant (Str (fc_fname fc))
, raw_apply (Var pairCon) $
[intTy, intTy] ++
map (RConstant . I)
[ fst (fc_start fc)
, snd (fc_start fc)
]
, raw_apply (Var pairCon) $
[intTy, intTy] ++
map (RConstant . I)
[ fst (fc_end fc)
, snd (fc_end fc)
]
]
where intTy = RConstant (AType (ATInt ITNative))
fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
| just == txt "Just" = Just tm
fromTTMaybe x = Nothing
reflErrName :: String -> Name
reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
-- | Attempt to reify a report part from TT to the internal
-- representation. Not in Idris or ElabD monads because it should be usable
-- from either.
reifyReportPart :: Term -> Either Err ErrorReportPart
reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
Right (TextPart msg)
reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
| n == reflm "NamePart" =
case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of
Error e -> Left . InternalMsg $
"could not reify name term " ++
show ttn ++
" when reflecting an error:" ++ show e
OK (n', _)-> Right $ NamePart n'
reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
| n == reflm "TermPart" =
case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of
Error e -> Left . InternalMsg $
"could not reify reflected term " ++
show tm ++
" when reflecting an error:" ++ show e
OK (tm', _) -> Right $ TermPart tm'
reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
| n == reflm "SubReport" =
case unList tm of
Just xs -> do subParts <- mapM reifyReportPart xs
Right (SubReport subParts)
Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
reifyTyDecl :: Term -> ElabD RTyDecl
reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
| n == tacN "Declare" =
do tyN' <- reifyTTName tyN
args' <- case unList args of
Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
Just xs -> mapM reifyRArg xs
ret' <- reifyRaw ret
return $ RDeclare tyN' args' ret'
where reifyRArg :: Term -> ElabD RArg
reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)
| n == tacN "Explicit" = liftM2 RExplicit
(reifyTTName argN)
(reifyRaw argTy)
| n == tacN "Implicit" = liftM2 RImplicit
(reifyTTName argN)
(reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
(reifyTTName argN)
(reifyRaw argTy)
reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
reifyFunDefn :: Term -> ElabD RFunDefn
reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)
| n == tacN "DefineFun" =
do fnN' <- reifyTTName fnN
clauses' <- case unList clauses of
Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
Just cs -> mapM reifyC cs
return $ RDefineFun fnN' clauses'
where reifyC :: Term -> ElabD RFunClause
reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)
| n == tacN "MkFunClause" = liftM2 RMkFunClause
(reifyRaw lhs)
(reifyRaw rhs)
reifyC (App _ (P (DCon _ _ _) n _) lhs)
| n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
envTupleType :: Raw
envTupleType
= raw_apply (Var pairTy) [ (Var $ reflm "TTName")
, (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
]

1
test/dsl002/expected
View File

@ -1,2 +1 @@
foo foo

2
test/effects001/expected
View File

@ -1,4 +1,4 @@
["HELLO!!!\n", "WORLD!!!\n", ""] ["HELLO!!!", "WORLD!!!", ""]
3 3
15 15
Answer: 99 Answer: 99

1
test/io001/expected
View File

@ -13,4 +13,5 @@ World!
3 3
4 4
Last line Last line
--- ---

2
test/io001/test004.idr
View File

@ -13,7 +13,7 @@ dumpFile fn = do { h <- openFile fn Read
x <- feof h x <- feof h
return (not x) }) return (not x) })
(do { l <- fread h (do { l <- fread h
putStr l }) putStrLn l })
closeFile h } closeFile h }
main : IO () main : IO ()

5
test/runtest.pl
View File

@ -10,10 +10,11 @@ my @idrOpts = ();
sub sandbox_path { sub sandbox_path {
my ($test_dir,) = @_; my ($test_dir,) = @_;
my $sandbox = abs_path("$test_dir/../../.cabal-sandbox/bin"); my $sandbox = "$test_dir/../../.cabal-sandbox/bin";
if ( -d $sandbox ) { if ( -d $sandbox ) {
return "PATH=\"$sandbox:$PATH\""; my $sandbox_abs = abs_path($sandbox);
return "PATH=\"$sandbox_abs:$PATH\"";
} else { } else {
return ""; return "";
} }

20
test/tactics001/Tactics.idr
View File

@ -1,6 +1,6 @@
module Tactics module Tactics
import Language.Reflection.Tactical import Language.Reflection.Elab
import Data.Vect import Data.Vect
@ -18,24 +18,24 @@ refl t x = RApp (RApp (Var (UN "Refl")) t) x
plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
plusZeroRightNeutralNew Z = Refl plusZeroRightNeutralNew Z = Refl
plusZeroRightNeutralNew (S k) = plusZeroRightNeutralNew (S k) =
%runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k")) %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
fill $ refl `(Nat : Type) `(S ~(Var (UN "k"))) fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
solve) solve)
plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k) plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
plusSuccRightSuccNew Z k = Refl plusSuccRightSuccNew Z k = Refl
plusSuccRightSuccNew (S j) k = plusSuccRightSuccNew (S j) k =
%runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k"))) %runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k"))))) fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
solve) solve)
-- Test that side effects in new tactics work -- Test that side effects in new tactics work
mkDecl : () mkDecl : ()
mkDecl = %runTactics (do declareType $ Declare (NS (UN "repUnit") ["Tactics"]) mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
[Implicit (UN "z") `(Nat)] [Implicit (UN "z") `(Nat)]
`(Vect ~(Var (UN "z")) ()) `(Vect ~(Var (UN "z")) ())
fill `(() : ()) fill `(() : ())
solve) solve)
repUnit = pure () repUnit = pure ()