mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
First lot of source files and paper
This commit is contained in:
Edwin Brady
parent
6aac1a90a5
commit
dc0c198f0c
32
LICENSE
Normal file
32
LICENSE
Normal file
@ -0,0 +1,32 @@
|
||||
Copyright (c) 2006-2010 Edwin Brady
|
||||
School of Computer Science, University of St Andrews
|
||||
All rights reserved.
|
||||
|
||||
This code is derived from software written by Edwin Brady
|
||||
(eb@cs.st-andrews.ac.uk).
|
||||
|
||||
Redistribution and use in source and binary forms, with or without
|
||||
modification, are permitted provided that the following conditions
|
||||
are met:
|
||||
1. Redistributions of source code must retain the above copyright
|
||||
notice, this list of conditions and the following disclaimer.
|
||||
2. Redistributions in binary form must reproduce the above copyright
|
||||
notice, this list of conditions and the following disclaimer in the
|
||||
documentation and/or other materials provided with the distribution.
|
||||
3. None of the names of the copyright holders may be used to endorse
|
||||
or promote products derived from this software without specific
|
||||
prior written permission.
|
||||
|
||||
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
|
||||
EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
|
||||
PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
|
||||
LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
||||
CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
||||
SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
|
||||
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
|
||||
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
|
||||
OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
|
||||
IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
|
||||
*** End of disclaimer. ***
|
||||
41
impl-paper/Makefile
Normal file
41
impl-paper/Makefile
Normal file
@ -0,0 +1,41 @@
|
||||
PAPER = impldtp
|
||||
|
||||
all: ${PAPER}.pdf
|
||||
|
||||
TEXFILES = ${PAPER}.tex intro.tex conclusions.tex overview.tex
|
||||
|
||||
DIAGS =
|
||||
|
||||
SOURCES = ${TEXFILES} ${DIAGS} macros.ltx literature.bib
|
||||
|
||||
DITAA = java -jar ~/Downloads/ditaa.jar
|
||||
|
||||
${PAPER}.pdf: ${SOURCES}
|
||||
# dvipdf ${PAPER}.dvi
|
||||
pdflatex ${PAPER}
|
||||
-bibtex ${PAPER}
|
||||
-pdflatex ${PAPER}
|
||||
-pdflatex ${PAPER}
|
||||
|
||||
${PAPER}.ps: ${PAPER}.dvi
|
||||
dvips -o ${PAPER}.ps ${PAPER}
|
||||
|
||||
${PAPER}.dvi: $(SOURCES)
|
||||
-latex ${PAPER}
|
||||
-bibtex ${PAPER}
|
||||
-latex ${PAPER}
|
||||
-latex ${PAPER}
|
||||
|
||||
progress: .PHONY
|
||||
wc -w ${TEXFILES}
|
||||
|
||||
%.png : %.diag
|
||||
$(DITAA) -o -E $<
|
||||
|
||||
todropbox: .PHONY
|
||||
cp ${SOURCES} ~/Dropbox/TeX/ImplDTP/
|
||||
|
||||
fromdropbox: .PHONY
|
||||
cp ~/Dropbox/TeX/ImplDTP/* .
|
||||
|
||||
.PHONY:
|
||||
1770
impl-paper/acmtrans.bst
Normal file
1770
impl-paper/acmtrans.bst
Normal file
File diff suppressed because it is too large
Load Diff
1460
impl-paper/acmtrans2m.cls
Normal file
1460
impl-paper/acmtrans2m.cls
Normal file
File diff suppressed because it is too large
Load Diff
29
impl-paper/comments.sty
Normal file
29
impl-paper/comments.sty
Normal file
@ -0,0 +1,29 @@
|
||||
% $id$
|
||||
% KH: created comments style file to allow alternative versions of a document.
|
||||
|
||||
% \newcommand{\red}[1]{#1}
|
||||
|
||||
\usepackage{color}
|
||||
\definecolor{BrickRed}{cmyk}{0, .89, .5, 0}
|
||||
\newcommand{\red}{\color{BrickRed}}
|
||||
|
||||
\newcommand{\eucommentary}[1]{\(\spadesuit\){\red{\textbf{EC Commentary}: \emph{#1}}\(\spadesuit\)}}
|
||||
\newcommand{\euevaluation}[2]{\(\spadesuit\){\red{\textbf{Evaluation Criteria ({#1})}: \emph{#2}}\(\spadesuit\)}}
|
||||
|
||||
\newcommand{\comment}[2]{\(\spadesuit\){\bf #1: }{\rm \sf #2}\(\spadesuit\)}
|
||||
\newcommand{\draftpage}{\newpage}
|
||||
|
||||
\newcommand{\FIXME}[1]{[\textbf{FIXME}: #1]}
|
||||
|
||||
%\newcommand{\FIXME}[1]{\wibble}
|
||||
\newcommand{\nocomments}{
|
||||
\renewcommand{\eucommentary}[1]{}
|
||||
\renewcommand{\euevaluation}[2]{}
|
||||
\renewcommand{\comment}[2]{}
|
||||
\renewcommand{\draftpage}{}
|
||||
\renewcommand{\FIXME}[1]{}
|
||||
}
|
||||
|
||||
\DeclareOption{final}{\nocomments}
|
||||
\DeclareOption{draft}{}
|
||||
\ProcessOptions*
|
||||
3
impl-paper/conclusions.tex
Normal file
3
impl-paper/conclusions.tex
Normal file
@ -0,0 +1,3 @@
|
||||
\section{Related Work}
|
||||
|
||||
\section{Conclusion}
|
||||
95
impl-paper/impldtp.tex
Normal file
95
impl-paper/impldtp.tex
Normal file
@ -0,0 +1,95 @@
|
||||
%\documentclass{llncs}
|
||||
\documentclass[acmtoplas]{acmtrans2m}
|
||||
|
||||
\usepackage[draft]{comments}
|
||||
%\usepackage[final]{comments}
|
||||
% \newcommand{\comment}[2]{[#1: #2]}
|
||||
\newcommand{\khcomment}[1]{\comment{KH}{#1}}
|
||||
\newcommand{\ebcomment}[1]{\comment{EB}{#1}}
|
||||
|
||||
\usepackage{epsfig}
|
||||
\usepackage{path}
|
||||
\usepackage{url}
|
||||
\usepackage{amsmath,amssymb}
|
||||
\usepackage{fancyvrb}
|
||||
|
||||
\newenvironment{template}{\sffamily}
|
||||
|
||||
\usepackage{graphics,epsfig}
|
||||
\usepackage{stmaryrd}
|
||||
|
||||
\input{./macros.ltx}
|
||||
\input{./library.ltx}
|
||||
|
||||
\NatPackage
|
||||
\FinPackage
|
||||
|
||||
\newcounter{per}
|
||||
\setcounter{per}{1}
|
||||
|
||||
\newcommand{\Ivor}{\textsc{Ivor}}
|
||||
\newcommand{\Idris}{\textsc{Idris}}
|
||||
\newcommand{\Funl}{\textsc{Funl}}
|
||||
\newcommand{\Agda}{\textsc{Agda}}
|
||||
\newcommand{\LamPi}{$\lambda_\Pi$}
|
||||
|
||||
\newcommand{\perule}[1]{\vspace*{0.1cm}\noindent
|
||||
\begin{center}
|
||||
\fbox{
|
||||
\begin{minipage}{7.5cm}\textbf{Rule \theper:} #1\addtocounter{per}{1}
|
||||
\end{minipage}}
|
||||
\end{center}
|
||||
\vspace*{0.1cm}
|
||||
}
|
||||
|
||||
\newcommand{\mysubsubsection}[1]{
|
||||
\noindent
|
||||
\textbf{#1}
|
||||
}
|
||||
\newcommand{\hdecl}[1]{\texttt{#1}}
|
||||
|
||||
\markboth{Edwin C. Brady}{Implementation of a Practical Dependently
|
||||
Typed Functional Programming Language}
|
||||
\title{Implementation of a Practical Dependently Typed Functional
|
||||
Programming Language}
|
||||
\author{EDWIN C. BRADY\\ University of St Andrews}
|
||||
|
||||
\begin{abstract}
|
||||
I describe the implementation of a dependently typed functional
|
||||
programming language, \Idris{}. Much has been written about various
|
||||
aspects of dependently typed language implementation (e.g. checking
|
||||
dependent types, unification, optimisation) but nothing yet about how
|
||||
to bring it all together into a complete, practical, usable tool. This paper
|
||||
attempts to do so. In particular, I explain what is needed to turn
|
||||
concrete syntax with implicit arguments into fully elaborated type
|
||||
theory, using unification and a tactic engine.
|
||||
\end{abstract}
|
||||
|
||||
\category{D.3.2}{Programming Languages}{Language
|
||||
Classifications}[Applicative (functional) Languages]
|
||||
\category{D.3.4}{Programming Languages}{Processors}[Compilers]
|
||||
\terms{Languages, Verification, Performance}
|
||||
\keywords{Dependent Types, Typechecking}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\begin{bottomstuff}
|
||||
Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
|
||||
KY16 9SX
|
||||
\end{bottomstuff}
|
||||
\maketitle
|
||||
|
||||
\input{intro.tex}
|
||||
|
||||
\input{overview.tex}
|
||||
|
||||
\input{conclusions.tex}
|
||||
|
||||
\bibliographystyle{acmtrans}
|
||||
\bibliography{literature.bib}
|
||||
|
||||
\appendix
|
||||
|
||||
%\input{code}
|
||||
|
||||
\end{document}
|
||||
12
impl-paper/intro.tex
Normal file
12
impl-paper/intro.tex
Normal file
@ -0,0 +1,12 @@
|
||||
\section{Introduction}
|
||||
|
||||
This paper documents a new implementation of \Idris{}~\cite{plpv11},
|
||||
in which I attempt to learn from the mistakes of the previous
|
||||
implementation and make it nice and clean and solid. Maybe I'll keep
|
||||
it up to date as I write the code.
|
||||
|
||||
The title is deliberately a reordering of the words in my thesis
|
||||
title~\cite{brady-thesis}. Whereas that was about taking elaborated
|
||||
programs in the core type theory of \Epigram{}~\cite{view-left} and
|
||||
compiling them efficiently (i.e. making the language implementation
|
||||
practical) this paper is about making the language itself practical.
|
||||
325
impl-paper/library.ltx
Normal file
325
impl-paper/library.ltx
Normal file
@ -0,0 +1,325 @@
|
||||
%%%%%%%%%%%%%%% library file for datatypes etc.
|
||||
|
||||
%%% Identifiers
|
||||
|
||||
\newcommand{\va}{\VV{a}}
|
||||
\newcommand{\vb}{\VV{b}}
|
||||
\newcommand{\vc}{\VV{c}}
|
||||
\newcommand{\vd}{\VV{d}}
|
||||
\newcommand{\ve}{\VV{e}}
|
||||
\newcommand{\vf}{\VV{f}}
|
||||
\newcommand{\vg}{\VV{g}}
|
||||
\newcommand{\vh}{\VV{h}}
|
||||
\newcommand{\vi}{\VV{i}}
|
||||
\newcommand{\vj}{\VV{j}}
|
||||
\newcommand{\vk}{\VV{k}}
|
||||
\newcommand{\vl}{\VV{l}}
|
||||
\newcommand{\vm}{\VV{m}}
|
||||
\newcommand{\vn}{\VV{n}}
|
||||
\newcommand{\vo}{\VV{o}}
|
||||
\newcommand{\vp}{\VV{p}}
|
||||
\newcommand{\vq}{\VV{q}}
|
||||
\newcommand{\vr}{\VV{r}}
|
||||
\newcommand{\vs}{\VV{s}}
|
||||
\newcommand{\vt}{\VV{t}}
|
||||
\newcommand{\vu}{\VV{u}}
|
||||
\newcommand{\vv}{\VV{v}}
|
||||
\newcommand{\vw}{\VV{w}}
|
||||
\newcommand{\vx}{\VV{x}}
|
||||
\newcommand{\vy}{\VV{y}}
|
||||
\newcommand{\vz}{\VV{z}}
|
||||
\newcommand{\vA}{\VV{A}}
|
||||
\newcommand{\vB}{\VV{B}}
|
||||
\newcommand{\vC}{\VV{C}}
|
||||
\newcommand{\vD}{\VV{D}}
|
||||
\newcommand{\vE}{\VV{E}}
|
||||
\newcommand{\vF}{\VV{F}}
|
||||
\newcommand{\vG}{\VV{G}}
|
||||
\newcommand{\vH}{\VV{H}}
|
||||
\newcommand{\vI}{\VV{I}}
|
||||
\newcommand{\vJ}{\VV{J}}
|
||||
\newcommand{\vK}{\VV{K}}
|
||||
\newcommand{\vL}{\VV{L}}
|
||||
\newcommand{\vM}{\VV{M}}
|
||||
\newcommand{\vN}{\VV{N}}
|
||||
\newcommand{\vO}{\VV{O}}
|
||||
\newcommand{\vP}{\VV{P}}
|
||||
\newcommand{\vQ}{\VV{Q}}
|
||||
\newcommand{\vR}{\VV{R}}
|
||||
\newcommand{\vS}{\VV{S}}
|
||||
\newcommand{\vT}{\VV{T}}
|
||||
\newcommand{\vU}{\VV{U}}
|
||||
\newcommand{\vV}{\VV{V}}
|
||||
\newcommand{\vW}{\VV{W}}
|
||||
\newcommand{\vX}{\VV{X}}
|
||||
\newcommand{\vY}{\VV{Y}}
|
||||
\newcommand{\vZ}{\VV{Z}}
|
||||
\newcommand{\vas}{\VV{as}}
|
||||
\newcommand{\vbs}{\VV{bs}}
|
||||
\newcommand{\vcs}{\VV{cs}}
|
||||
\newcommand{\vds}{\VV{ds}}
|
||||
\newcommand{\ves}{\VV{es}}
|
||||
\newcommand{\vfs}{\VV{fs}}
|
||||
\newcommand{\vgs}{\VV{gs}}
|
||||
\newcommand{\vhs}{\VV{hs}}
|
||||
\newcommand{\vis}{\VV{is}}
|
||||
\newcommand{\vjs}{\VV{js}}
|
||||
\newcommand{\vks}{\VV{ks}}
|
||||
\newcommand{\vls}{\VV{ls}}
|
||||
\newcommand{\vms}{\VV{ms}}
|
||||
\newcommand{\vns}{\VV{ns}}
|
||||
\newcommand{\vos}{\VV{os}}
|
||||
\newcommand{\vps}{\VV{ps}}
|
||||
\newcommand{\vqs}{\VV{qs}}
|
||||
\newcommand{\vrs}{\VV{rs}}
|
||||
%\newcommand{\vss}{\VV{ss}}
|
||||
\newcommand{\vts}{\VV{ts}}
|
||||
\newcommand{\vus}{\VV{us}}
|
||||
\newcommand{\vvs}{\VV{vs}}
|
||||
\newcommand{\vws}{\VV{ws}}
|
||||
\newcommand{\vxs}{\VV{xs}}
|
||||
\newcommand{\vys}{\VV{ys}}
|
||||
\newcommand{\vzs}{\VV{zs}}
|
||||
|
||||
%%% Telescope Identifiers
|
||||
|
||||
\newcommand{\ta}{\vec{\VV{a}}}
|
||||
\newcommand{\tb}{\vec{\VV{b}}}
|
||||
\newcommand{\tc}{\vec{\VV{c}}}
|
||||
\newcommand{\td}{\vec{\VV{d}}}
|
||||
\newcommand{\te}{\vec{\VV{e}}}
|
||||
\newcommand{\tf}{\vec{\VV{f}}}
|
||||
\newcommand{\tg}{\vec{\VV{g}}}
|
||||
%\newcommand{\th}{\vec{\VV{h}}}
|
||||
\newcommand{\ti}{\vec{\VV{i}}}
|
||||
\newcommand{\tj}{\vec{\VV{j}}}
|
||||
\newcommand{\tk}{\vec{\VV{k}}}
|
||||
\newcommand{\tl}{\vec{\VV{l}}}
|
||||
\newcommand{\tm}{\vec{\VV{m}}}
|
||||
\newcommand{\tn}{\vec{\VV{n}}}
|
||||
%\newcommand{\to}{\vec{\VV{o}}}
|
||||
\newcommand{\tp}{\vec{\VV{p}}}
|
||||
\newcommand{\tq}{\vec{\VV{q}}}
|
||||
\newcommand{\tr}{\vec{\VV{r}}}
|
||||
\newcommand{\tts}{\vec{\VV{s}}}
|
||||
\newcommand{\ttt}{\vec{\VV{t}}}
|
||||
\newcommand{\tu}{\vec{\VV{u}}}
|
||||
%\newcommand{\tv}{\vec{\VV{v}}}
|
||||
\newcommand{\tw}{\vec{\VV{w}}}
|
||||
\newcommand{\tx}{\vec{\VV{x}}}
|
||||
\newcommand{\ty}{\vec{\VV{y}}}
|
||||
\newcommand{\tz}{\vec{\VV{z}}}
|
||||
\newcommand{\tA}{\vec{\VV{A}}}
|
||||
\newcommand{\tB}{\vec{\VV{B}}}
|
||||
\newcommand{\tC}{\vec{\VV{C}}}
|
||||
\newcommand{\tD}{\vec{\VV{D}}}
|
||||
\newcommand{\tE}{\vec{\VV{E}}}
|
||||
\newcommand{\tF}{\vec{\VV{F}}}
|
||||
\newcommand{\tG}{\vec{\VV{G}}}
|
||||
\newcommand{\tH}{\vec{\VV{H}}}
|
||||
\newcommand{\tI}{\vec{\VV{I}}}
|
||||
\newcommand{\tJ}{\vec{\VV{J}}}
|
||||
\newcommand{\tK}{\vec{\VV{K}}}
|
||||
\newcommand{\tL}{\vec{\VV{L}}}
|
||||
\newcommand{\tM}{\vec{\VV{M}}}
|
||||
\newcommand{\tN}{\vec{\VV{N}}}
|
||||
\newcommand{\tO}{\vec{\VV{O}}}
|
||||
\newcommand{\tP}{\vec{\VV{P}}}
|
||||
\newcommand{\tQ}{\vec{\VV{Q}}}
|
||||
\newcommand{\tR}{\vec{\VV{R}}}
|
||||
\newcommand{\tS}{\vec{\VV{S}}}
|
||||
\newcommand{\tT}{\vec{\VV{T}}}
|
||||
\newcommand{\tU}{\vec{\VV{U}}}
|
||||
\newcommand{\tV}{\vec{\VV{V}}}
|
||||
\newcommand{\tW}{\vec{\VV{W}}}
|
||||
\newcommand{\tX}{\vec{\VV{X}}}
|
||||
\newcommand{\tY}{\vec{\VV{Y}}}
|
||||
\newcommand{\tZ}{\vec{\VV{Z}}}
|
||||
|
||||
|
||||
|
||||
%%% Nat
|
||||
|
||||
\newcommand{\NatPackage}{
|
||||
\newcommand{\Nat}{\TC{\mathbb{N}}}
|
||||
\newcommand{\Z}{\DC{0}}
|
||||
\newcommand{\suc}{\DC{s}}
|
||||
\newcommand{\NatDecl}{
|
||||
\Data \hg
|
||||
\Axiom{\Nat\Hab\Type} \hg
|
||||
\Where \hg
|
||||
\Axiom{\Z\Hab\Nat} \hg
|
||||
\Rule{\vn\Hab\Nat}
|
||||
{\suc\:\vn\Hab\Nat}
|
||||
}}
|
||||
|
||||
%%% Bool
|
||||
|
||||
\newcommand{\BoolPackage}{
|
||||
\newcommand{\Bool}{\TC{Bool}}
|
||||
\newcommand{\true}{\DC{true}}
|
||||
\newcommand{\false}{\DC{false}}
|
||||
\newcommand{\BoolDecl}{
|
||||
\Data \hg
|
||||
\Axiom{\Bool\Hab\Type} \hg
|
||||
\Where \hg
|
||||
\Axiom{\true\Hab\Bool} \hg
|
||||
\Axiom{\false\Hab\Bool}
|
||||
}}
|
||||
|
||||
%%% So
|
||||
|
||||
\newcommand{\SoPackage}{
|
||||
\newcommand{\So}{\TC{So}}
|
||||
\newcommand{\oh}{\DC{oh}}
|
||||
\newcommand{\SoDecl}{
|
||||
\Data \hg
|
||||
\Rule{\vb\Hab\Bool}
|
||||
{\So\:\vb\Hab\Type} \hg
|
||||
\Where \hg
|
||||
\Axiom{\oh\Hab\So\:\true}
|
||||
}}
|
||||
|
||||
%%% Unit
|
||||
|
||||
\newcommand{\UnitPackage}{
|
||||
\newcommand{\Unit}{\TC{Unit}}
|
||||
\newcommand{\void}{\DC{void}}
|
||||
\newcommand{\UnitDecl}{
|
||||
\Data \hg
|
||||
\Axiom{\Unit\Hab\Type} \hg
|
||||
\Where \hg
|
||||
\Axiom{\void\Hab\Unit}
|
||||
}}
|
||||
|
||||
%%% Maybe
|
||||
|
||||
\newcommand{\MaybePackage}{
|
||||
\newcommand{\Maybe}{\TC{Maybe}}
|
||||
\newcommand{\yes}{\DC{yes}}
|
||||
\newcommand{\no}{\DC{no}}
|
||||
\newcommand{\MaybeDecl}{
|
||||
\Data \hg
|
||||
\Rule{\vA\Hab\Type}
|
||||
{\Maybe\:\vA\Hab\Type} \hg
|
||||
\Where \hg
|
||||
\Rule{\va \Hab \vA}
|
||||
{\yes\:\va\Hab\Maybe\:\vA} \hg
|
||||
\Axiom{\no\Hab\Maybe\:\vA}
|
||||
}}
|
||||
|
||||
%%% Cross
|
||||
|
||||
\newcommand{\pr}[2]{(#1\DC{,}#2)} %grrrr
|
||||
\newcommand{\CrossPackage}{
|
||||
\newcommand{\Cross}{\times}
|
||||
\newcommand{\CrossDecl}{
|
||||
\Data \hg
|
||||
\Rule{\vA,\vB\Hab\Type}
|
||||
{\vA\Cross\vB\Hab\Type} \hg
|
||||
\Where \hg
|
||||
\Rule{\va \Hab \vA \hg \vb\Hab\vB}
|
||||
{\pr{\va}{\vb}\Hab\vA\Cross\vB}
|
||||
}}
|
||||
|
||||
%%% Fin
|
||||
|
||||
\newcommand{\FinPackage}{
|
||||
\newcommand{\Fin}{\TC{Fin}}
|
||||
\newcommand{\fz}{\DC{f0}}
|
||||
\newcommand{\fs}{\DC{fs}}
|
||||
\newcommand{\FinDecl}{
|
||||
\AR{
|
||||
\Data \hg
|
||||
\Rule{\vn\Hab\Nat}
|
||||
{\Fin\:\vn\Hab\Type} \hg \\
|
||||
\Where \hg
|
||||
\begin{array}[t]{c}
|
||||
\Axiom{\fz\Hab\Fin\:(\suc\:\vn)} \hg
|
||||
\Rule{\vi\Hab\Fin\:\vn}
|
||||
{\fs\:\vi\Hab\Fin\:(\suc\:\vn)}
|
||||
\end{array}
|
||||
}
|
||||
}}
|
||||
|
||||
%%% Vect
|
||||
|
||||
\newcommand{\VectPackage}{
|
||||
\newcommand{\Vect}{\TC{Vect}}
|
||||
\newcommand{\vnil}{\varepsilon}
|
||||
\newcommand{\vcons}{\,\dcolon\,}
|
||||
\newcommand{\vsnoc}{\,\dcolon\,}
|
||||
\newcommand{\VectConsDecl}{
|
||||
\Data \hg
|
||||
\Rule{\vA \Hab \Type \hg \vn\Hab\Nat}
|
||||
{\Vect\:\vA\:\vn\Hab\Type} \hg
|
||||
\Where \hg \begin{array}[t]{c}
|
||||
\Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\
|
||||
\Rule{\vx\Hab\vA \hg \vxs\Hab \Vect\:\vA\:\vn }
|
||||
{\vx\vcons\vxs\Hab\Vect\:\vA\:(\suc\vn)}
|
||||
\end{array}
|
||||
}
|
||||
\newcommand{\VectSnocDecl}{
|
||||
\Data \hg
|
||||
\Rule{\vA \Hab \Type \hg \vn\Hab\Nat}
|
||||
{\Vect\:\vA\:\vn\Hab\Type} \hg
|
||||
\Where \hg \begin{array}[t]{c}
|
||||
\Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\
|
||||
\Rule{\vxs\Hab \Vect\:\vA\:\vn \hg \vx\Hab\vA}
|
||||
{\vxs\vsnoc\vx\Hab\Vect\:\vA\:(\suc\vn)}
|
||||
\end{array}
|
||||
}
|
||||
}
|
||||
|
||||
%%% Compare
|
||||
|
||||
%Data Compare : (x:nat)(y:nat)Type
|
||||
% = lt : (x:nat)(y:nat)(Compare x (plus (S y) x))
|
||||
% | eq : (x:nat)(Compare x x)
|
||||
% | gt : (x:nat)(y:nat)(Compare (plus (S x) y) y);
|
||||
|
||||
|
||||
\newcommand{\ComparePackage}{
|
||||
\newcommand{\Compare}{\TC{Compare}}
|
||||
\newcommand{\ltComp}{\DC{lt}}
|
||||
\newcommand{\eqComp}{\DC{eq}}
|
||||
\newcommand{\gtComp}{\DC{gt}}
|
||||
\newcommand{\CompareDecl}{
|
||||
\Data \hg
|
||||
\Rule{\vm\Hab\Nat\hg\vn\Hab\Nat}
|
||||
{\Compare\:\vm\:\vn\Hab\Type} \\
|
||||
\Where \hg\begin{array}[t]{c}
|
||||
\Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}
|
||||
{\ltComp_{\vx}\:\vy\Hab\Compare\:\vx\:(\FN{plus}\:\vx\:(\suc\:\vy))} \\
|
||||
\Rule{\vx\Hab\Nat}
|
||||
{\eqComp_{\vx}\Hab\Compare\:\vx\:\vx}\\
|
||||
\Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}
|
||||
{\gtComp_{\vy}\:\vx\Hab\Compare\:(\FN{plus}\:\vy\:(\suc\:\vx))\:\vy} \\
|
||||
\end{array}
|
||||
}
|
||||
|
||||
%Data CompareM : Type
|
||||
% = ltM : (ydiff:nat)CompareM
|
||||
% | eqM : CompareM
|
||||
% | gtM : (xdiff:nat)CompareM;
|
||||
|
||||
\newcommand{\CompareM}{\TC{Compare^-}}
|
||||
\newcommand{\ltCompM}{\DC{lt^-}}
|
||||
\newcommand{\eqCompM}{\DC{eq^-}}
|
||||
\newcommand{\gtCompM}{\DC{gt^-}}
|
||||
\newcommand{\CompareMDecl}{
|
||||
|
||||
\Data \hg
|
||||
\Axiom{\CompareM\Hab\Type} \\
|
||||
\Where \hg\begin{array}[t]{c}
|
||||
\Rule{\vy\Hab\Nat}
|
||||
{\ltCompM\:\vy\Hab\CompareM} \\
|
||||
\Axiom{\eqCompM\Hab\CompareM}\\
|
||||
\Rule{\vx\Hab\Nat}
|
||||
{\gtCompM\:\vx\Hab\CompareM} \\
|
||||
\end{array}
|
||||
}
|
||||
\newcommand{\CompareRec}{\FN{CompareRec}}
|
||||
\newcommand{\CompareRecM}{\FN{CompareRec^-}}
|
||||
|
||||
}
|
||||
3836
impl-paper/literature.bib
Normal file
3836
impl-paper/literature.bib
Normal file
File diff suppressed because it is too large
Load Diff
1060
impl-paper/macros.ltx
Normal file
1060
impl-paper/macros.ltx
Normal file
File diff suppressed because it is too large
Load Diff
11
impl-paper/overview.tex
Normal file
11
impl-paper/overview.tex
Normal file
@ -0,0 +1,11 @@
|
||||
\section{overview}
|
||||
|
||||
High level view of steps we've taken to implement this new version:
|
||||
|
||||
\begin{itemize}
|
||||
\item Syntax tree for raw and well-typed terms
|
||||
\item An evaluator for well-typed terms
|
||||
\item The important bit: a simple type checker. No unification or
|
||||
inference.
|
||||
\item The proof state and a tactic engine.
|
||||
\end{itemize}
|
||||
26
miniidris.cabal
Normal file
26
miniidris.cabal
Normal file
@ -0,0 +1,26 @@
|
||||
Name: miniidris
|
||||
Version: 0.1
|
||||
License: BSD3
|
||||
License-file: LICENSE
|
||||
Author: Edwin Brady
|
||||
Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>
|
||||
Homepage: http://www.idris-lang.org/
|
||||
|
||||
Stability: Alpha
|
||||
Category: Compilers/Interpreters, Dependent Types
|
||||
Synopsis: Dependently Typed Functional Programming Language
|
||||
Description: An experimental new version of Idris
|
||||
|
||||
Cabal-Version: >= 1.6
|
||||
Build-type: Simple
|
||||
|
||||
Executable miniidris
|
||||
Main-is: Main.hs
|
||||
hs-source-dirs: src
|
||||
Other-modules: Core, Evaluate, Typecheck, ProofState
|
||||
|
||||
Build-depends: base>=4 && <5, parsec, mtl, Cabal
|
||||
|
||||
Extensions: MultiParamTypeClasses, FunctionalDependencies,
|
||||
FlexibleInstances
|
||||
ghc-prof-options: -auto-all
|
||||
151
src/Core.hs
Normal file
151
src/Core.hs
Normal file
@ -0,0 +1,151 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
|
||||
|
||||
module Core where
|
||||
|
||||
import Control.Monad.State
|
||||
|
||||
{- The language has:
|
||||
* Full dependent types
|
||||
* A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...
|
||||
* Pattern matching letrec binding
|
||||
* (primitive types defined externally)
|
||||
|
||||
Some technical stuff:
|
||||
* Typechecker is kept as simple as possible
|
||||
- no unification, just a checker for incomplete terms.
|
||||
* We have a simple collection of tactics which we use to elaborate source
|
||||
programs with implicit syntax into fully explicit terms.
|
||||
-}
|
||||
|
||||
data Option = SetInSet
|
||||
| CheckConv
|
||||
deriving Eq
|
||||
|
||||
-- RAW TERMS ----------------------------------------------------------------
|
||||
|
||||
-- Names are hierarchies of strings, describing scope (so no danger of
|
||||
-- duplicate names, but need to be careful on lookup).
|
||||
-- Also MN for machine chosen names
|
||||
|
||||
data Name = UN [String]
|
||||
| MN Int String
|
||||
deriving (Show, Eq)
|
||||
|
||||
data Raw = Var Name
|
||||
| RBind Name (Binder Raw) Raw
|
||||
| RApp Raw Raw
|
||||
| RSet Int
|
||||
deriving Show
|
||||
|
||||
data Binder b = Lam { binderTy :: b }
|
||||
| Pi { binderTy :: b }
|
||||
| Let { binderTy :: b,
|
||||
binderVal :: b }
|
||||
| Hole { binderTy :: b}
|
||||
| Guess { binderTy :: b,
|
||||
binderVal :: b }
|
||||
| PVar { binderTy :: b }
|
||||
deriving (Show, Eq)
|
||||
|
||||
data RawFun = RawFun { rtype :: Raw,
|
||||
rval :: Raw
|
||||
}
|
||||
deriving Show
|
||||
|
||||
data RDef = RFunction RawFun
|
||||
| RConst Raw
|
||||
deriving Show
|
||||
|
||||
type RProgram = [(Name, RDef)]
|
||||
|
||||
-- WELL TYPED TERMS ---------------------------------------------------------
|
||||
|
||||
data NameType = Ref | DCon Int Int | TCon Int
|
||||
deriving (Show, Eq)
|
||||
|
||||
data TT n = P NameType n (TT n) -- embed type
|
||||
| V Int
|
||||
| Bind n (Binder (TT n)) (TT n)
|
||||
| App (TT n) (TT n) (TT n) -- function, function type, arg
|
||||
| Set Int
|
||||
deriving (Show, Eq)
|
||||
|
||||
type EnvTT n = [(n, Binder (TT n))]
|
||||
|
||||
bindEnv :: EnvTT n -> TT n -> TT n
|
||||
bindEnv [] tm = tm
|
||||
bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
|
||||
|
||||
type Term = TT Name
|
||||
type Type = Term
|
||||
|
||||
type Env = EnvTT Name
|
||||
|
||||
-- WELL TYPED TERMS AS HOAS -------------------------------------------------
|
||||
|
||||
data HTT = HP NameType Name HTT
|
||||
| HV Int
|
||||
| HBind Name (Binder HTT) (HTT -> HTT)
|
||||
| HApp HTT HTT HTT
|
||||
| HSet Int
|
||||
| HTmp Int
|
||||
|
||||
instance Show HTT where
|
||||
show h = "<<HOAS>>"
|
||||
|
||||
hoas :: [HTT] -> TT Name -> HTT
|
||||
hoas env (P nt n ty) = HP nt n (hoas env ty)
|
||||
hoas env (V i) | i < length env = env!!i
|
||||
| otherwise = HV i
|
||||
hoas env (Bind n b sc) = HBind n (hbind b) (\x -> hoas (x:env) sc)
|
||||
where hbind (Lam t) = Lam (hoas env t)
|
||||
hbind (Pi t) = Pi (hoas env t)
|
||||
hbind (Hole t) = Hole (hoas env t)
|
||||
hbind (PVar t) = PVar (hoas env t)
|
||||
hbind (Let v t) = Let (hoas env v) (hoas env t)
|
||||
hbind (Guess v t) = Guess (hoas env v) (hoas env t)
|
||||
hoas env (App f t a) = HApp (hoas env f) (hoas env t) (hoas env a)
|
||||
hoas env (Set i) = HSet i
|
||||
|
||||
-- CONTEXTS -----------------------------------------------------------------
|
||||
|
||||
data Fun = Fun Type HTT Term HTT
|
||||
deriving Show
|
||||
|
||||
data Def = Function Fun
|
||||
| Constant NameType Type HTT
|
||||
deriving Show
|
||||
|
||||
type Context = [(Name, Def)]
|
||||
|
||||
lookupTy :: Name -> Context -> Maybe Type
|
||||
lookupTy n ctxt = do def <- lookup n ctxt
|
||||
case def of
|
||||
(Function (Fun ty _ _ _)) -> return ty
|
||||
(Constant _ ty _) -> return ty
|
||||
|
||||
lookupP :: Name -> Context -> Maybe Term
|
||||
lookupP n ctxt
|
||||
= do def <- lookup n ctxt
|
||||
case def of
|
||||
(Function (Fun ty _ tm _)) -> return (P Ref n ty)
|
||||
(Constant nt ty hty) -> return (P nt n ty)
|
||||
|
||||
lookupVal :: Name -> Context -> Maybe HTT
|
||||
lookupVal n ctxt
|
||||
= do def <- lookup n ctxt
|
||||
case def of
|
||||
(Function (Fun _ _ _ htm)) -> return htm
|
||||
(Constant nt ty hty) -> return (HP nt n hty)
|
||||
|
||||
lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
|
||||
lookupTyEnv n env = li n 0 env where
|
||||
li n i [] = Nothing
|
||||
li n i ((x, b): xs)
|
||||
| n == x = Just (i, binderTy b)
|
||||
| otherwise = li n (i+1) xs
|
||||
|
||||
|
||||
x = UN ["x"]
|
||||
xt = UN ["X"]
|
||||
testtm = RBind xt (Lam (RSet 0)) (RBind x (Lam (Var xt)) (Var x))
|
||||
72
src/Evaluate.hs
Normal file
72
src/Evaluate.hs
Normal file
@ -0,0 +1,72 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
|
||||
|
||||
module Evaluate(normalise) where
|
||||
|
||||
import Debug.Trace
|
||||
import Core
|
||||
|
||||
normalise :: Context -> TT Name -> TT Name
|
||||
normalise ctxt t = quote 0 (eval ctxt (hoas [] t))
|
||||
|
||||
-- We just evaluate HOAS terms. Any de Bruijn indices will refer to higher
|
||||
-- level things, so, if we remove a binder, we need to strengthen the
|
||||
-- indices appropriately.
|
||||
|
||||
eval :: Context -> HTT -> HTT
|
||||
eval ctxt t = ev t where
|
||||
ev (HP Ref n ty)
|
||||
| Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling
|
||||
ev (HP nt n ty) = HP nt n (ev ty)
|
||||
ev (HApp f t a)
|
||||
= evSpine f [(a, t)]
|
||||
where evSpine (HApp f t a) sp = evSpine f ((a, t):sp)
|
||||
evSpine f sp = evAp f sp
|
||||
ev (HBind n (Let t v) sc) = weaken (-1) (ev (sc (weaken 1 (ev v))))
|
||||
ev (HBind n b sc)
|
||||
= HBind n (evB b) (\x -> ev (sc x))
|
||||
where evB (Lam t) = Lam (ev t)
|
||||
evB (Pi t) = Pi (ev t)
|
||||
evB (Hole t) = Hole (ev t)
|
||||
evB (Guess t v) = Guess (ev t) (ev v)
|
||||
evB (PVar t) = PVar (ev t)
|
||||
ev tm = tm -- Constructors + constants
|
||||
|
||||
-- TODO:add PE magic here - nothing is evaluated yet
|
||||
|
||||
evAp f sp = evAp' (ev f) sp
|
||||
evAp' (HBind n (Lam ty) sc) ((a, t):sp)
|
||||
= weaken (-1) (evAp' (sc (weaken 1 (ev a))) sp)
|
||||
evAp' f sp = apply f (map (\ (a, t) -> (ev a, ev t)) sp)
|
||||
|
||||
apply f [] = f
|
||||
apply f ((a, t):xs) = apply (HApp f t a) xs
|
||||
|
||||
-- Adjust de Bruijn indices across a term
|
||||
|
||||
weaken :: Int -> HTT -> HTT
|
||||
weaken w (HV i) = HV (i + w)
|
||||
weaken w (HBind n b sc)
|
||||
= HBind n (weakenB b) (\x -> weaken w (sc x))
|
||||
where weakenB (Lam t) = Lam (weaken w t)
|
||||
weakenB (Pi t) = Pi (weaken w t)
|
||||
weakenB (Let t v) = Let (weaken w t) (weaken w v)
|
||||
weakenB (Hole t) = Hole (weaken w t)
|
||||
weakenB (Guess t v) = Guess (weaken w t) (weaken w v)
|
||||
weakenB (PVar t) = PVar (weaken w t)
|
||||
weaken w (HApp f t a) = HApp (weaken w f) (weaken w t) (weaken w a)
|
||||
weaken w tm = tm
|
||||
|
||||
quote :: Int -> HTT -> TT Name
|
||||
quote env (HP nt n t) = P nt n (quote env t)
|
||||
quote env (HV i) = V i
|
||||
quote env (HBind n b sc)
|
||||
= Bind n (quoteB b) (quote (env+1) (sc (HTmp (env+1))))
|
||||
where quoteB (Lam t) = Lam (quote env t)
|
||||
quoteB (Pi t) = Pi (quote env t)
|
||||
quoteB (Let t v) = Let (quote env t) (quote env v)
|
||||
quoteB (Hole t) = Hole (quote env t)
|
||||
quoteB (Guess t v) = Guess (quote env t) (quote env v)
|
||||
quoteB (PVar t) = PVar (quote env t)
|
||||
quote env (HApp f t a) = App (quote env f) (quote env t) (quote env a)
|
||||
quote env (HSet i) = Set i
|
||||
quote env (HTmp i) = V (env-i)
|
||||
5
src/Main.hs
Normal file
5
src/Main.hs
Normal file
@ -0,0 +1,5 @@
|
||||
module Main where
|
||||
|
||||
import Typecheck
|
||||
|
||||
main = putStrLn "Nothing Happens"
|
||||
103
src/Parser.hs
Normal file
103
src/Parser.hs
Normal file
@ -0,0 +1,103 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
|
||||
|
||||
module Parser(parseTerm, parseFile, parseDef) where
|
||||
|
||||
import Core
|
||||
|
||||
import Text.ParserCombinators.Parsec
|
||||
import Text.ParserCombinators.Parsec.Expr
|
||||
import Text.ParserCombinators.Parsec.Language
|
||||
import qualified Text.ParserCombinators.Parsec.Token as PTok
|
||||
|
||||
import Debug.Trace
|
||||
|
||||
type TokenParser a = PTok.TokenParser a
|
||||
|
||||
lexer :: TokenParser ()
|
||||
lexer = PTok.makeTokenParser haskellDef
|
||||
|
||||
whiteSpace= PTok.whiteSpace lexer
|
||||
lexeme = PTok.lexeme lexer
|
||||
symbol = PTok.symbol lexer
|
||||
natural = PTok.natural lexer
|
||||
parens = PTok.parens lexer
|
||||
semi = PTok.semi lexer
|
||||
comma = PTok.comma lexer
|
||||
identifier= PTok.identifier lexer
|
||||
reserved = PTok.reserved lexer
|
||||
operator = PTok.operator lexer
|
||||
reservedOp= PTok.reservedOp lexer
|
||||
lchar = lexeme.char
|
||||
|
||||
parseFile = parse pTestFile "(input)"
|
||||
parseDef = parse pDef "(input)"
|
||||
parseTerm = parse pTerm "(input)"
|
||||
|
||||
pTestFile :: Parser RProgram
|
||||
pTestFile = many1 pDef
|
||||
|
||||
pDef :: Parser (Name, RDef)
|
||||
pDef = try (do x <- identifier; lchar ':'; ty <- pTerm
|
||||
lchar '='
|
||||
tm <- pTerm
|
||||
lchar ';'
|
||||
return (UN [x], RFunction (RawFun ty tm)))
|
||||
<|> do x <- identifier; lchar ':'; ty <- pTerm; lchar ';'
|
||||
return (UN [x], RConst ty)
|
||||
|
||||
app :: Parser (Raw -> Raw -> Raw)
|
||||
app = do whiteSpace ; return RApp
|
||||
|
||||
arrow :: Parser (Raw -> Raw -> Raw)
|
||||
arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
|
||||
|
||||
pTerm :: Parser Raw
|
||||
pTerm = try (do chainl1 pNoApp app)
|
||||
<|> pNoApp
|
||||
|
||||
pNoApp :: Parser Raw
|
||||
pNoApp = try (chainr1 pExp arrow)
|
||||
<|> pExp
|
||||
|
||||
pExp :: Parser Raw
|
||||
pExp = do lchar '\\'; x <- identifier; lchar ':'; ty <- pTerm
|
||||
symbol "=>";
|
||||
sc <- pTerm
|
||||
return (RBind (UN [x]) (Lam ty) sc)
|
||||
<|> try (do lchar '(';
|
||||
x <- identifier; lchar ':'; ty <- pTerm
|
||||
lchar ')';
|
||||
symbol "->";
|
||||
sc <- pTerm
|
||||
return (RBind (UN [x]) (Pi ty) sc))
|
||||
<|> try (do lchar '(';
|
||||
t <- pTerm
|
||||
lchar ')'
|
||||
return t)
|
||||
<|> try (do lchar '?';
|
||||
x <- identifier; lchar ':'; ty <- pTerm
|
||||
lchar '.';
|
||||
sc <- pTerm
|
||||
return (RBind (UN [x]) (Hole ty) sc))
|
||||
<|> try (do symbol "??";
|
||||
x <- identifier; lchar ':'; ty <- pTerm
|
||||
lchar '=';
|
||||
val <- pTerm
|
||||
sc <- pTerm
|
||||
return (RBind (UN [x]) (Guess ty val) sc))
|
||||
<|> try (do reserved "let";
|
||||
x <- identifier; lchar ':'; ty <- pTerm
|
||||
lchar '=';
|
||||
val <- pTerm
|
||||
sc <- pTerm
|
||||
return (RBind (UN [x]) (Let ty val) sc))
|
||||
<|> try (do lchar '_';
|
||||
x <- identifier; lchar ':'; ty <- pTerm
|
||||
lchar '.';
|
||||
sc <- pTerm
|
||||
return (RBind (UN [x]) (PVar ty) sc))
|
||||
<|> try (do reserved "Set"; i <- natural
|
||||
return (RSet (fromInteger i)))
|
||||
<|> try (do x <- identifier
|
||||
return (Var (UN [x])))
|
||||
|
||||
8
src/ProofState.hs
Normal file
8
src/ProofState.hs
Normal file
@ -0,0 +1,8 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
|
||||
|
||||
module ProofState where
|
||||
|
||||
import Typecheck
|
||||
import Evaluate
|
||||
import Core
|
||||
|
||||
11
src/Test.hs
Normal file
11
src/Test.hs
Normal file
@ -0,0 +1,11 @@
|
||||
module Test where
|
||||
|
||||
import Parser
|
||||
import Core
|
||||
import Typecheck
|
||||
|
||||
test = do f <- readFile "test.mi"
|
||||
let Right defs = parseFile f
|
||||
print defs
|
||||
let ctxt = checkProgram [] defs
|
||||
print ctxt
|
||||
134
src/Typecheck.hs
Normal file
134
src/Typecheck.hs
Normal file
@ -0,0 +1,134 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
|
||||
|
||||
module Typecheck where
|
||||
|
||||
import Control.Monad.State
|
||||
import Debug.Trace
|
||||
|
||||
import Core
|
||||
import Evaluate
|
||||
|
||||
data TC a = OK a
|
||||
| Error String -- TMP! Make this an informative data structure
|
||||
deriving Show
|
||||
|
||||
-- at some point, this instance should also carry type checking options
|
||||
-- (e.g. Set:Set)
|
||||
|
||||
instance Monad TC where
|
||||
return = OK
|
||||
x >>= k = case x of
|
||||
OK v -> k v
|
||||
Error e -> Error e
|
||||
fail = Error
|
||||
|
||||
converts :: Context -> Env -> Term -> Term -> TC ()
|
||||
converts ctxt env x y = if (normalise ctxt (bindEnv env x) ==
|
||||
normalise ctxt (bindEnv env y))
|
||||
then return ()
|
||||
else fail ("Can't convert between " ++
|
||||
show x ++ " and " ++ show y)
|
||||
|
||||
isSet :: Term -> TC ()
|
||||
isSet (Set _) = return ()
|
||||
isSet tm = fail (show tm ++ " is not a Set")
|
||||
|
||||
check :: Context -> Env -> Raw -> TC (Term, Type)
|
||||
check ctxt env (Var n)
|
||||
| Just (i, ty) <- lookupTyEnv n env = return (V i, ty)
|
||||
| Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
|
||||
| otherwise = do fail $ "No such variable " ++ show n
|
||||
check ctxt env (RApp f a)
|
||||
= do (fv, fty) <- check ctxt env f
|
||||
(av, aty) <- check ctxt env a
|
||||
let fty' = normalise ctxt fty
|
||||
case fty' of
|
||||
Bind x (Pi s) t ->
|
||||
do converts ctxt env s aty
|
||||
return (App fv fty av,
|
||||
normalise ctxt (Bind x (Let av aty) t))
|
||||
t -> fail "Can't apply a non-function type"
|
||||
check ctxt env (RSet i) = return (Set i, Set (i+1))
|
||||
check ctxt env (RBind n b sc)
|
||||
= do b' <- checkBinder b
|
||||
(scv, sct) <- check ctxt ((n, b'):env) sc
|
||||
discharge n b' scv sct
|
||||
where checkBinder (Lam t)
|
||||
= do (tv, tt) <- check ctxt env t
|
||||
let tv' = normalise ctxt tv
|
||||
let tt' = normalise ctxt tt
|
||||
isSet tt'
|
||||
return (Lam tv')
|
||||
checkBinder (Pi t)
|
||||
= do (tv, tt) <- check ctxt env t
|
||||
let tv' = normalise ctxt tv
|
||||
let tt' = normalise ctxt tt
|
||||
isSet tt'
|
||||
return (Pi tv')
|
||||
checkBinder (Let t v)
|
||||
= do (tv, tt) <- check ctxt env t
|
||||
(vv, vt) <- check ctxt env v
|
||||
let tv' = normalise ctxt tv
|
||||
let tt' = normalise ctxt tt
|
||||
converts ctxt env tv vt
|
||||
isSet tt'
|
||||
return (Let tv' vv)
|
||||
checkBinder (Hole t)
|
||||
= do (tv, tt) <- check ctxt env t
|
||||
let tv' = normalise ctxt tv
|
||||
let tt' = normalise ctxt tt
|
||||
isSet tt'
|
||||
return (Hole tv')
|
||||
checkBinder (Guess t v)
|
||||
= do (tv, tt) <- check ctxt env t
|
||||
(vv, vt) <- check ctxt env v
|
||||
let tv' = normalise ctxt tv
|
||||
let tt' = normalise ctxt tt
|
||||
converts ctxt env tv vt
|
||||
isSet tt'
|
||||
return (Guess tv' vv)
|
||||
checkBinder (PVar t)
|
||||
= do (tv, tt) <- check ctxt env t
|
||||
let tv' = normalise ctxt tv
|
||||
let tt' = normalise ctxt tt
|
||||
isSet tt'
|
||||
return (PVar tv')
|
||||
|
||||
discharge n (Lam t) scv sct
|
||||
= return (Bind n (Lam t) scv, Bind n (Pi t) sct)
|
||||
discharge n (Pi t) scv sct
|
||||
= return (Bind n (Pi t) scv, sct)
|
||||
discharge n (Let t v) scv sct
|
||||
= return (Bind n (Let t v) scv, Bind n (Let t v) sct)
|
||||
discharge n (Hole t) scv sct
|
||||
= do -- A hole can't appear in the type of its scope
|
||||
checkNotHoley 0 sct
|
||||
return (Bind n (Hole t) scv, sct)
|
||||
discharge n (Guess t v) scv sct
|
||||
= do -- A hole can't appear in the type of its scope
|
||||
checkNotHoley 0 sct
|
||||
return (Bind n (Guess t v) scv, sct)
|
||||
discharge n (PVar t) scv sct
|
||||
= return (Bind n (PVar t) scv, sct)
|
||||
|
||||
checkNotHoley i (V v)
|
||||
| v == i = fail "You can't put a hole where a hole don't belong"
|
||||
checkNotHoley i (App f t a) = do checkNotHoley i f
|
||||
checkNotHoley i t
|
||||
checkNotHoley i a
|
||||
checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
|
||||
checkNotHoley _ _ = return ()
|
||||
|
||||
checkProgram :: Context -> RProgram -> TC Context
|
||||
checkProgram ctxt [] = return ctxt
|
||||
checkProgram ctxt ((n, RConst t):xs)
|
||||
= do (t', tt') <- trace (show n) $ check ctxt [] t
|
||||
isSet tt'
|
||||
checkProgram ((n, Constant Ref t' (hoas [] t')):ctxt) xs
|
||||
checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)
|
||||
= do (ty', tyt') <- trace (show n) $ check ctxt [] ty
|
||||
(val', valt') <- check ctxt [] val
|
||||
isSet tyt'
|
||||
converts ctxt [] ty' valt'
|
||||
checkProgram ((n, Function (Fun ty' (hoas [] ty')
|
||||
val' (hoas [] val'))):ctxt) xs
|
||||
11
src/test.mi
Normal file
11
src/test.mi
Normal file
@ -0,0 +1,11 @@
|
||||
N : Set 0;
|
||||
O : N;
|
||||
S : N -> N;
|
||||
|
||||
one : N = S O;
|
||||
two : N = S one;
|
||||
three : N = S two;
|
||||
|
||||
Vect : (A:Set 0) -> (n:N) -> Set 0;
|
||||
Nil : (A:Set 0) -> (Vect A O);
|
||||
Cons : (A:Set 0) -> (k:N) -> (Vect A k) -> (Vect A (S k));
|
||||
Loading…
Reference in New Issue
Block a user