forked from GitHub/gf-core
removed transfer from gf3
This commit is contained in:
aarne
@@ -1,51 +0,0 @@
|
||||
SRCDIR=../src
|
||||
|
||||
GHC=ghc
|
||||
GHCFLAGS=-i$(SRCDIR)
|
||||
GHCOPTFLAGS=-O2
|
||||
|
||||
|
||||
.PHONY: all bnfc bnfctest doc docclean clean bnfcclean distclean
|
||||
|
||||
all: GHCFLAGS += $(GHCOPTFLAGS)
|
||||
all:
|
||||
$(GHC) $(GHCFLAGS) --make -o trci trci.hs
|
||||
$(GHC) $(GHCFLAGS) --make -o transferc transferc.hs
|
||||
|
||||
bnfc: bnfcclean
|
||||
cd $(SRCDIR) && bnfc -gadt -d -p Transfer Transfer/Core/Core.cf
|
||||
perl -i -pe 's/^import Transfer.Core.ErrM/import Transfer.ErrM/' $(SRCDIR)/Transfer/Core/*.{hs,x,y}
|
||||
-rm -f $(SRCDIR)/Transfer/Core/ErrM.hs
|
||||
cd $(SRCDIR) && alex -g Transfer/Core/Lex.x
|
||||
cd $(SRCDIR) && happy -gca Transfer/Core/Par.y
|
||||
cd $(SRCDIR) && bnfc -gadt -d -p Transfer Transfer/Syntax/Syntax.cf
|
||||
perl -i -pe 's/^import Transfer.Syntax.ErrM/import Transfer.ErrM/' $(SRCDIR)/Transfer/Syntax/*.{hs,x,y}
|
||||
-rm -f $(SRCDIR)/Transfer/Syntax/ErrM.hs
|
||||
cd $(SRCDIR) && alex -g Transfer/Syntax/Lex.x
|
||||
cd $(SRCDIR) && happy -gca Transfer/Syntax/Par.y
|
||||
|
||||
bnfctest:
|
||||
ghc $(GHCFLAGS) --make $(SRCDIR)/Transfer/Core/Test.hs -o test_core
|
||||
ghc $(GHCFLAGS) --make $(SRCDIR)/Transfer/Syntax/Test.hs -o test_syntax
|
||||
ghc $(GHCFLAGS) --make $(SRCDIR)/Transfer/Syntax/ResolveLayout.hs -o test_layout
|
||||
|
||||
doc:
|
||||
(cd $(SRCDIR)/Transfer/Core/; latex Doc.tex; dvips Doc.dvi -o Doc.ps)
|
||||
(cd $(SRCDIR)/Transfer/Syntax/; latex Doc.tex; dvips Doc.dvi -o Doc.ps)
|
||||
|
||||
docclean:
|
||||
-rm -f $(SRCDIR)/Transfer/Core/*.{log,aux,dvi,ps}
|
||||
-rm -f $(SRCDIR)/Transfer/Syntax/*.{log,aux,dvi,ps}
|
||||
|
||||
clean:
|
||||
-rm -f *.o *.hi
|
||||
find $(SRCDIR)/Transfer -name '*.o' -o -name '*.hi' | xargs rm -f
|
||||
-rm -f trci
|
||||
-rm -f transferc
|
||||
-rm -f test_core test_syntax test_layout
|
||||
|
||||
bnfcclean:
|
||||
-rm -f $(SRCDIR)/Transfer/Core/{Doc,Lex,Par,Layout,Skel,Print,Test,Abs}.*
|
||||
-rm -f $(SRCDIR)/Transfer/Syntax/{Doc,Lex,Par,Layout,Skel,Print,Test,Abs}.*
|
||||
|
||||
distclean: clean bnfcclean
|
||||
@@ -1,48 +0,0 @@
|
||||
Some features of the Transfer language:
|
||||
|
||||
* Purely functional
|
||||
* Dependent types
|
||||
* Eager evaluation
|
||||
* Generalized algebraic datatypes
|
||||
* Metavariables
|
||||
* Records with subtyping
|
||||
* Overloading by explicit dictionary passing
|
||||
* Pattern matching by case expressions
|
||||
|
||||
Additional features in the front-end language:
|
||||
|
||||
* Disjunctive patterns
|
||||
* do-notation
|
||||
* Automatic derivation of some operations on user-defined GADTs:
|
||||
- Compositional maps and folds
|
||||
- Equality
|
||||
- Ordering
|
||||
- Showing
|
||||
* Pattern equations
|
||||
* Operator syntax for common functions, most are overloaded
|
||||
|
||||
|
||||
|
||||
Differences between Transfer and Cayenne:
|
||||
|
||||
* Cayenne has a more advanced module system
|
||||
|
||||
* Cayenne has mutually recursive record fields
|
||||
|
||||
* Cayenne erases type arguments before running
|
||||
|
||||
* Transfer is eager, Cayenne is lazy
|
||||
|
||||
* Transfer has GADTs (inductive families)
|
||||
|
||||
* Transfer has metavariables
|
||||
|
||||
* Transfer has record patterns
|
||||
|
||||
* Transfer has disjunctive patterns
|
||||
|
||||
* Transfer has derivation of compositional functions
|
||||
|
||||
* Transfer has a standard library which uses a hierarchy
|
||||
of "type classes"
|
||||
|
||||
@@ -1,55 +0,0 @@
|
||||
* Improve front-end language
|
||||
|
||||
- implicit arguments?
|
||||
|
||||
- show generation
|
||||
|
||||
- ord generation
|
||||
|
||||
- better module system
|
||||
|
||||
- Negated patterns?
|
||||
|
||||
- Simplify taking many arguments of the same type: f : (A,B : Type) -> ...
|
||||
|
||||
- add record extension operator?
|
||||
|
||||
* Improve interpreter
|
||||
|
||||
- More efficient handling of constructor application
|
||||
|
||||
- Implement tail recursion.
|
||||
|
||||
* Improve the core language
|
||||
|
||||
* Add primitive types operations to core
|
||||
|
||||
- add Char type, with primitive operations:
|
||||
- Enum stuff
|
||||
|
||||
- add more primitive operations on strings:
|
||||
- make list an isntance of the collection class for strings
|
||||
|
||||
* Add more libraries
|
||||
|
||||
- Enum class
|
||||
|
||||
- Bounded class
|
||||
|
||||
- list functions
|
||||
|
||||
- a map structure
|
||||
|
||||
- collections framework?
|
||||
|
||||
- state monad
|
||||
|
||||
* Improve compilation
|
||||
|
||||
* Implement module system in interpreter
|
||||
|
||||
* Add type checker for core
|
||||
|
||||
* Add friendly type checker for front-end language
|
||||
|
||||
* Add termination checker
|
||||
@@ -1,5 +0,0 @@
|
||||
#!/bin/sh
|
||||
|
||||
for f in lib/*.tra examples/*.tra; do
|
||||
./transferc -ilib $f;
|
||||
done
|
||||
@@ -1,41 +0,0 @@
|
||||
FIGURES=
|
||||
|
||||
NAME=typesystem
|
||||
|
||||
default: pdf
|
||||
|
||||
ps: $(NAME).ps
|
||||
|
||||
pdf: $(NAME).pdf
|
||||
|
||||
%.ps: %.dvi
|
||||
dvips -f $^ > $@
|
||||
|
||||
#%.pdf: %.ps
|
||||
# ps2pdf $^
|
||||
|
||||
%.pdf: %.dvi
|
||||
dvipdfm $^
|
||||
|
||||
%.dvi: %.tex # %.bib
|
||||
latex $*
|
||||
# bibtex $*
|
||||
# latex $*
|
||||
# latex $*
|
||||
|
||||
%.ps: %.dot
|
||||
dot -Tps -o $@ $^
|
||||
|
||||
%.eps: %.ps
|
||||
ps2epsi $^ $@
|
||||
|
||||
$(NAME).dvi: $(FIGURES)
|
||||
|
||||
clean:
|
||||
-rm -f *.aux *.dvi *.log *.blg *.bbl *.toc
|
||||
|
||||
psclean: clean
|
||||
-rm -f *.pdf *.ps
|
||||
|
||||
show: $(NAME).dvi
|
||||
xdvi $(NAME).dvi
|
||||
@@ -1,390 +0,0 @@
|
||||
% Mathpartir --- Math Paragraph for Typesetting Inference Rules
|
||||
%
|
||||
% Copyright (C) 2001, 2002, 2003 Didier Rémy
|
||||
%
|
||||
% Author : Didier Remy
|
||||
% Version : 1.1.1
|
||||
% Bug Reports : to author
|
||||
% Web Site : http://pauillac.inria.fr/~remy/latex/
|
||||
%
|
||||
% WhizzyTeX is free software; you can redistribute it and/or modify
|
||||
% it under the terms of the GNU General Public License as published by
|
||||
% the Free Software Foundation; either version 2, or (at your option)
|
||||
% any later version.
|
||||
%
|
||||
% Mathpartir 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 General Public License for more details
|
||||
% (http://pauillac.inria.fr/~remy/license/GPL).
|
||||
%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% File mathpartir.sty (LaTeX macros)
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\NeedsTeXFormat{LaTeX2e}
|
||||
\ProvidesPackage{mathpartir}
|
||||
[2003/07/10 version 1.1.1 Math Paragraph for Typesetting Inference Rules]
|
||||
|
||||
%%
|
||||
|
||||
%% Identification
|
||||
%% Preliminary declarations
|
||||
|
||||
\RequirePackage {keyval}
|
||||
|
||||
%% Options
|
||||
%% More declarations
|
||||
|
||||
%% PART I: Typesetting maths in paragraphe mode
|
||||
|
||||
\newdimen \mpr@tmpdim
|
||||
|
||||
% To ensure hevea \hva compatibility, \hva should expands to nothing
|
||||
% in mathpar or in inferrule
|
||||
\let \mpr@hva \empty
|
||||
|
||||
%% normal paragraph parametters, should rather be taken dynamically
|
||||
\def \mpr@savepar {%
|
||||
\edef \MathparNormalpar
|
||||
{\noexpand \lineskiplimit \the\lineskiplimit
|
||||
\noexpand \lineskip \the\lineskip}%
|
||||
}
|
||||
|
||||
\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
|
||||
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
|
||||
\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
|
||||
\let \MathparLineskip \mpr@lineskip
|
||||
\def \mpr@paroptions {\MathparLineskip}
|
||||
\let \mpr@prebindings \relax
|
||||
|
||||
\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
|
||||
|
||||
\def \mpr@goodbreakand
|
||||
{\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
|
||||
\def \mpr@and {\hskip \mpr@andskip}
|
||||
\def \mpr@andcr {\penalty 50\mpr@and}
|
||||
\def \mpr@cr {\penalty -10000\mpr@and}
|
||||
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
|
||||
|
||||
\def \mpr@bindings {%
|
||||
\let \and \mpr@andcr
|
||||
\let \par \mpr@andcr
|
||||
\let \\\mpr@cr
|
||||
\let \eqno \mpr@eqno
|
||||
\let \hva \mpr@hva
|
||||
}
|
||||
\let \MathparBindings \mpr@bindings
|
||||
|
||||
% \@ifundefined {ignorespacesafterend}
|
||||
% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
|
||||
|
||||
\newenvironment{mathpar}[1][]
|
||||
{$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
|
||||
\vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
|
||||
\noindent $\displaystyle\fi
|
||||
\MathparBindings}
|
||||
{\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
|
||||
|
||||
% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
|
||||
% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
|
||||
|
||||
%%% HOV BOXES
|
||||
|
||||
\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
|
||||
\vbox \bgroup \tabskip 0em \let \\ \cr
|
||||
\halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
|
||||
\egroup}
|
||||
|
||||
\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
|
||||
\box0\else \mathvbox {#1}\fi}
|
||||
|
||||
|
||||
%% Part II -- operations on lists
|
||||
|
||||
\newtoks \mpr@lista
|
||||
\newtoks \mpr@listb
|
||||
|
||||
\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
|
||||
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
|
||||
|
||||
\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
|
||||
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
|
||||
|
||||
\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
|
||||
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
|
||||
|
||||
\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
|
||||
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
|
||||
|
||||
\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
|
||||
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
|
||||
|
||||
\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
|
||||
\mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
|
||||
\mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
|
||||
\def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
|
||||
\mpr@flatten \mpr@all \mpr@to \mpr@one
|
||||
\expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
|
||||
\mpr@all \mpr@stripend
|
||||
\ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
|
||||
\ifx 1\mpr@isempty
|
||||
\repeat
|
||||
}
|
||||
|
||||
%% Part III -- Type inference rules
|
||||
|
||||
\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
|
||||
\def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
|
||||
|
||||
\newif \if@premisse
|
||||
\newbox \mpr@hlist
|
||||
\newbox \mpr@vlist
|
||||
\newif \ifmpr@center \mpr@centertrue
|
||||
\def \mpr@htovlist {%
|
||||
\setbox \mpr@hlist
|
||||
\hbox {\strut
|
||||
\ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
|
||||
\unhbox \mpr@hlist}%
|
||||
\setbox \mpr@vlist
|
||||
\vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
|
||||
\else \unvbox \mpr@vlist \box \mpr@hlist
|
||||
\fi}%
|
||||
}
|
||||
% OLD version
|
||||
% \def \mpr@htovlist {%
|
||||
% \setbox \mpr@hlist
|
||||
% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
|
||||
% \setbox \mpr@vlist
|
||||
% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
|
||||
% \else \unvbox \mpr@vlist \box \mpr@hlist
|
||||
% \fi}%
|
||||
% }
|
||||
|
||||
\def \mpr@sep{2em}
|
||||
\def \mpr@blank { }
|
||||
\def \mpr@hovbox #1#2{\hbox
|
||||
\bgroup
|
||||
\ifx #1T\@premissetrue
|
||||
\else \ifx #1B\@premissefalse
|
||||
\else
|
||||
\PackageError{mathpartir}
|
||||
{Premisse orientation should either be P or B}
|
||||
{Fatal error in Package}%
|
||||
\fi \fi
|
||||
\def \@test {#2}\ifx \@test \mpr@blank\else
|
||||
\setbox \mpr@hlist \hbox {}%
|
||||
\setbox \mpr@vlist \vbox {}%
|
||||
\if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
|
||||
\let \@hvlist \empty \let \@rev \empty
|
||||
\mpr@tmpdim 0em
|
||||
\expandafter \mpr@makelist #2\mpr@to \mpr@flat
|
||||
\if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
|
||||
\def \\##1{%
|
||||
\def \@test {##1}\ifx \@test \empty
|
||||
\mpr@htovlist
|
||||
\mpr@tmpdim 0em %%% last bug fix not extensively checked
|
||||
\else
|
||||
\setbox0 \hbox{$\displaystyle {##1}$}\relax
|
||||
\advance \mpr@tmpdim by \wd0
|
||||
%\mpr@tmpdim 1.02\mpr@tmpdim
|
||||
\ifnum \mpr@tmpdim < \hsize
|
||||
\ifnum \wd\mpr@hlist > 0
|
||||
\if@premisse
|
||||
\setbox \mpr@hlist
|
||||
\hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
|
||||
\else
|
||||
\setbox \mpr@hlist
|
||||
\hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
|
||||
\fi
|
||||
\else
|
||||
\setbox \mpr@hlist \hbox {\unhbox0}%
|
||||
\fi
|
||||
\else
|
||||
\ifnum \wd \mpr@hlist > 0
|
||||
\mpr@htovlist
|
||||
\mpr@tmpdim \wd0
|
||||
\fi
|
||||
\setbox \mpr@hlist \hbox {\unhbox0}%
|
||||
\fi
|
||||
\advance \mpr@tmpdim by \mpr@sep
|
||||
\fi
|
||||
}%
|
||||
\@rev
|
||||
\mpr@htovlist
|
||||
\ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
|
||||
\fi
|
||||
\egroup
|
||||
}
|
||||
|
||||
%%% INFERENCE RULES
|
||||
|
||||
\@ifundefined{@@over}{%
|
||||
\let\@@over\over % fallback if amsmath is not loaded
|
||||
\let\@@overwithdelims\overwithdelims
|
||||
\let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
|
||||
\let\@@above\above \let\@@abovewithdelims\abovewithdelims
|
||||
}{}
|
||||
|
||||
|
||||
\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
|
||||
$\displaystyle {#1\@@over #2}$}}
|
||||
\let \mpr@fraction \mpr@@fraction
|
||||
\def \mpr@@reduce #1#2{\hbox
|
||||
{$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
|
||||
\def \mpr@@rewrite #1#2#3{\hbox
|
||||
{$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
|
||||
\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
|
||||
|
||||
\def \mpr@empty {}
|
||||
\def \mpr@inferrule
|
||||
{\bgroup
|
||||
\ifnum \linewidth<\hsize \hsize \linewidth\fi
|
||||
\mpr@rulelineskip
|
||||
\let \and \qquad
|
||||
\let \hva \mpr@hva
|
||||
\let \@rulename \mpr@empty
|
||||
\let \@rule@options \mpr@empty
|
||||
\mpr@inferrule@}
|
||||
\newcommand {\mpr@inferrule@}[3][]
|
||||
{\everymath={\displaystyle}%
|
||||
\def \@test {#2}\ifx \empty \@test
|
||||
\setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
|
||||
\else
|
||||
\def \@test {#3}\ifx \empty \@test
|
||||
\setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
|
||||
\else
|
||||
\setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
|
||||
\fi \fi
|
||||
\def \@test {#1}\ifx \@test\empty \box0
|
||||
\else \vbox
|
||||
%%% Suggestion de Francois pour les etiquettes longues
|
||||
%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
|
||||
{\hbox {\RefTirName {#1}}\box0}\fi
|
||||
\egroup}
|
||||
|
||||
\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
|
||||
|
||||
% They are two forms
|
||||
% \inferrule [label]{[premisses}{conclusions}
|
||||
% or
|
||||
% \inferrule* [options]{[premisses}{conclusions}
|
||||
%
|
||||
% Premisses and conclusions are lists of elements separated by \\
|
||||
% Each \\ produces a break, attempting horizontal breaks if possible,
|
||||
% and vertical breaks if needed.
|
||||
%
|
||||
% An empty element obtained by \\\\ produces a vertical break in all cases.
|
||||
%
|
||||
% The former rule is aligned on the fraction bar.
|
||||
% The optional label appears on top of the rule
|
||||
% The second form to be used in a derivation tree is aligned on the last
|
||||
% line of its conclusion
|
||||
%
|
||||
% The second form can be parameterized, using the key=val interface. The
|
||||
% folloiwng keys are recognized:
|
||||
%
|
||||
% width set the width of the rule to val
|
||||
% narrower set the width of the rule to val\hsize
|
||||
% before execute val at the beginning/left
|
||||
% lab put a label [Val] on top of the rule
|
||||
% lskip add negative skip on the right
|
||||
% left put a left label [Val]
|
||||
% Left put a left label [Val], ignoring its width
|
||||
% right put a right label [Val]
|
||||
% Right put a right label [Val], ignoring its width
|
||||
% leftskip skip negative space on the left-hand side
|
||||
% rightskip skip negative space on the right-hand side
|
||||
% vdots lift the rule by val and fill vertical space with dots
|
||||
% after execute val at the end/right
|
||||
%
|
||||
% Note that most options must come in this order to avoid strange
|
||||
% typesetting (in particular leftskip must preceed left and Left and
|
||||
% rightskip must follow Right or right; vdots must come last
|
||||
% or be only followed by rightskip.
|
||||
%
|
||||
|
||||
\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
|
||||
\define@key {mprset}{center}[]{\mpr@centertrue}
|
||||
\def \mprset #1{\setkeys{mprset}{#1}}
|
||||
|
||||
\newbox \mpr@right
|
||||
\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
|
||||
\define@key {mpr}{center}[]{\mpr@centertrue}
|
||||
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
|
||||
\advance \hsize by -\wd0\box0}
|
||||
\define@key {mpr}{width}{\hsize #1}
|
||||
\define@key {mpr}{sep}{\def\mpr@sep{#1}}
|
||||
\define@key {mpr}{before}{#1}
|
||||
\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
|
||||
\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
|
||||
\define@key {mpr}{narrower}{\hsize #1\hsize}
|
||||
\define@key {mpr}{leftskip}{\hskip -#1}
|
||||
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
|
||||
\define@key {mpr}{rightskip}
|
||||
{\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
|
||||
\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
|
||||
\advance \hsize by -\wd0\box0}
|
||||
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
|
||||
\advance \hsize by -\wd0\box0}
|
||||
\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
|
||||
\define@key {mpr}{right}
|
||||
{\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
|
||||
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
|
||||
\define@key {mpr}{RIGHT}
|
||||
{\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
|
||||
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
|
||||
\define@key {mpr}{Right}
|
||||
{\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
|
||||
\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
|
||||
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
|
||||
|
||||
\newdimen \rule@dimen
|
||||
\newcommand \mpr@inferstar@ [3][]{\setbox0
|
||||
\hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
|
||||
\setbox \mpr@right \hbox{}%
|
||||
$\setkeys{mpr}{#1}%
|
||||
\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
|
||||
\mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
|
||||
\box \mpr@right \mpr@vdots$}
|
||||
\setbox1 \hbox {\strut}
|
||||
\rule@dimen \dp0 \advance \rule@dimen by -\dp1
|
||||
\raise \rule@dimen \box0}
|
||||
|
||||
\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
|
||||
\newcommand \mpr@err@skipargs[3][]{}
|
||||
\def \mpr@inferstar*{\ifmmode
|
||||
\let \@do \mpr@inferstar@
|
||||
\else
|
||||
\let \@do \mpr@err@skipargs
|
||||
\PackageError {mathpartir}
|
||||
{\string\inferrule* can only be used in math mode}{}%
|
||||
\fi \@do}
|
||||
|
||||
|
||||
%%% Exports
|
||||
|
||||
% Envirnonment mathpar
|
||||
|
||||
\let \inferrule \mpr@infer
|
||||
|
||||
% make a short name \infer is not already defined
|
||||
\@ifundefined {infer}{\let \infer \mpr@infer}{}
|
||||
|
||||
\def \TirNameStyle #1{\small \textsc{#1}}
|
||||
\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
|
||||
\let \TirName \tir@name
|
||||
\let \DefTirName \TirName
|
||||
\let \RefTirName \TirName
|
||||
|
||||
%%% Other Exports
|
||||
|
||||
% \let \listcons \mpr@cons
|
||||
% \let \listsnoc \mpr@snoc
|
||||
% \let \listhead \mpr@head
|
||||
% \let \listmake \mpr@makelist
|
||||
|
||||
|
||||
|
||||
|
||||
\endinput
|
||||
@@ -1,479 +0,0 @@
|
||||
\documentclass[a4paper,11pt]{article}
|
||||
\usepackage{mathpartir}
|
||||
\usepackage{amssymb}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Transfer Type Checking}
|
||||
\author{Bj\"orn Bringert \\ \texttt{bringert@cs.chalmers.se}}
|
||||
\maketitle
|
||||
|
||||
\section{Type Checking Algorithm}
|
||||
|
||||
This is the beginnings of a type checking algorithm for the
|
||||
Transfer Core language. It is far from complete,
|
||||
and some of the rules make no sense at all at the moment.
|
||||
|
||||
\subsection{Notation}
|
||||
|
||||
$\overline{a}$ is a list of $a$s.
|
||||
|
||||
$x$ stands for variables.
|
||||
|
||||
$A$,$B$,$C$ are terms which we use for types.
|
||||
|
||||
$s$,$t$ are any terms.
|
||||
|
||||
$l$ refers to record labels.
|
||||
|
||||
$p$ refers to patterns.
|
||||
|
||||
$c$ refers to constructors.
|
||||
|
||||
$\Delta$ is a set of constructor typings.
|
||||
|
||||
$\Gamma$ is a set of variable typings.
|
||||
|
||||
$\Delta;\Gamma \vdash t \uparrow A$ means that in the
|
||||
variable typing context $\Gamma$ and the constructor
|
||||
typing context $\Delta$, the type of $t$ can be inferred
|
||||
to be $A$.
|
||||
|
||||
$\Delta;\Gamma \vdash t \downarrow A$ means that in the
|
||||
variable typing context $\Gamma$ and the constructor
|
||||
typing context $\Delta$, the type of $t$ can be
|
||||
checked to be $A$.
|
||||
|
||||
$\Delta \vdash_p p \downarrow A; \Gamma$ means that
|
||||
in the constructor typing context $\Delta$,
|
||||
the pattern $p$ can matched against a value of type
|
||||
$A$, and if the match succeeds, it will create
|
||||
variable bindings with the typings $\Gamma$.
|
||||
|
||||
$A \leq B$ means that $A$ is a subtype of of $B$.
|
||||
|
||||
$A \lesssim B$ means that $A$ is convertible
|
||||
to a subtype of $B$.
|
||||
|
||||
\subsection{Language}
|
||||
|
||||
\begin{eqnarray*}
|
||||
s,t,u & ::= & \textrm{let} \ x = s \ \textrm{in} \ t \\
|
||||
& & | \ \textrm{case} \ s \ \textrm{of} \{ \overline{p \mid t \rightarrow u} \} \\
|
||||
& & | \ \lambda x . t \\
|
||||
& & | \ (x : s) \rightarrow t \\
|
||||
& & | \ s \ t \\
|
||||
& & | \ s.l \\
|
||||
& & | \ \textrm{sig} \ \{ \overline{l : t} \} \\
|
||||
& & | \ \textrm{rec} \ \{ \overline{l = t} \} \\
|
||||
& & | \ x \\
|
||||
& & | \ Type \\
|
||||
& & | \ string \\
|
||||
& & | \ integer \\
|
||||
& & | \ double \\
|
||||
p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ | \ string \ | \ integer
|
||||
\end{eqnarray*}
|
||||
|
||||
|
||||
|
||||
\subsection{Rules}
|
||||
|
||||
\begin{figure}
|
||||
\begin{mathpar}
|
||||
|
||||
\inferrule[Type annotation]
|
||||
{ \Delta;\Gamma \vdash t \downarrow A }
|
||||
{ \Delta;\Gamma \vdash t : A \uparrow A }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Check by inferring]
|
||||
{ \Delta;\Gamma \vdash t \uparrow A' \\
|
||||
A' \lesssim A}
|
||||
{ \Delta;\Gamma \vdash t \downarrow A }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Variable]
|
||||
{ x : A \in \Gamma }
|
||||
{ \Delta;\Gamma \vdash x \uparrow A }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Constructor]
|
||||
{ c : A \in \Delta }
|
||||
{ \Delta;\Gamma \vdash c \uparrow A }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Function type]
|
||||
{ \Delta;\Gamma \vdash A \downarrow Type \\
|
||||
\Delta;\Gamma, x : A \vdash B \downarrow Type }
|
||||
{ \Delta;\Gamma \vdash (x : A) \rightarrow B \downarrow Type }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Abstraction]
|
||||
{ \Delta;\Gamma, x : A \vdash s \downarrow B }
|
||||
{ \Delta;\Gamma \vdash \lambda x. s \downarrow (x : A) \rightarrow B }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Application]
|
||||
{ \Delta;\Gamma \vdash s \uparrow (x : A) \rightarrow B \\
|
||||
\Delta;\Gamma \vdash t \downarrow A
|
||||
}
|
||||
{ \Delta;\Gamma \vdash s \ t \uparrow B [x / t] }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Local definition]
|
||||
{ \Delta;\Gamma \vdash s \uparrow A \\
|
||||
\Delta;\Gamma, x : A \vdash t \uparrow B }
|
||||
{ \Delta;\Gamma \vdash \textrm{let} \ x = s \ \textrm{in} \ t \uparrow B }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Case analysis]
|
||||
{ \Delta;\Gamma \vdash s \uparrow A \\
|
||||
B = B_1 \vee \ldots \vee B_n \\
|
||||
\Delta \vdash_p p_1 \downarrow A; \Gamma_1 \\
|
||||
\Delta;\Gamma,\Gamma_1 \vdash g_1 \downarrow Bool \\
|
||||
\Delta;\Gamma,\Gamma_1 \vdash t_1 \uparrow B_1 \\
|
||||
\ldots \\
|
||||
\Delta p_n \vdash_p A; \Gamma_n \\
|
||||
\Delta;\Gamma, \Gamma_n \vdash g_n \downarrow Bool \\
|
||||
\Delta;\Gamma, \Gamma_n \vdash t_n \uparrow B_n
|
||||
}
|
||||
{ \Delta;\Gamma \vdash \textrm{case} \ s \ \textrm{of} \ \{
|
||||
p_1 \mid g_1 \rightarrow t_1;
|
||||
\ldots;
|
||||
p_n \mid g_n \rightarrow t_n
|
||||
\} \uparrow B }
|
||||
|
||||
\end{mathpar}
|
||||
\caption{Basics.}
|
||||
\label{fig:basics}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}
|
||||
\begin{mathpar}
|
||||
|
||||
\inferrule[Record type]
|
||||
{ \Delta;\Gamma \vdash T_1 \uparrow Type \\
|
||||
\ldots \\
|
||||
\Delta;\Gamma, l_1 : T_1, \ldots, l_{n-1} : T_{n-1} \vdash T_n \uparrow Type \\
|
||||
l_1 \ldots l_n \ \textrm{different}
|
||||
}
|
||||
{ \Delta;\Gamma \vdash \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} \uparrow Type }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Record]
|
||||
{ \Delta;\Gamma \vdash t_1 \uparrow T_1 \\
|
||||
\ldots \\
|
||||
\Delta;\Gamma \vdash t_n \uparrow T_n [l_{n-1} / t_{n-1}] \ldots [l_1 / t_1] \\
|
||||
l_1 \ldots l_n \ \textrm{different} }
|
||||
{ \Delta;\Gamma \vdash \textrm{rec} \{ l_1 = t_1, \ldots, l_n = t_n \}
|
||||
\uparrow \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Record projection]
|
||||
{ \Delta;\Gamma \vdash t \downarrow \textrm{sig} \{ l : T \} }
|
||||
{ \Delta;\Gamma \vdash t . l \uparrow T }
|
||||
|
||||
\end{mathpar}
|
||||
\caption{Records.}
|
||||
\label{fig:records}
|
||||
\end{figure}
|
||||
|
||||
|
||||
\begin{figure}
|
||||
\begin{mathpar}
|
||||
|
||||
\inferrule[Variable pattern]
|
||||
{ }
|
||||
{ \Delta \vdash_p x \downarrow \ A; \{ x : A \} }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Wildcard pattern]
|
||||
{ }
|
||||
{ \Delta \vdash_p \_ \ \downarrow \ A; \{ \} }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Constructor pattern]
|
||||
{ c : (x_1 : T_1) \rightarrow \ldots \rightarrow (x_n : T_n) \rightarrow T' \in \Delta \\
|
||||
T' = T \\
|
||||
\Delta \vdash_p p_1 \downarrow T_1; \Gamma_1 \\
|
||||
\ldots \\
|
||||
\Delta \vdash_p p_n \downarrow T_n; \Gamma_n \\
|
||||
\Gamma_1 \ldots \Gamma_n \ \textrm{disjoint} \\
|
||||
\textrm{FIXME: $x_k$ can occur in $T_{k+1}$}
|
||||
}
|
||||
{ \Delta \vdash_p c \ p_1 \ldots p_n \ \downarrow \ T; \Gamma_1, \ldots, \Gamma_n }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Record pattern]
|
||||
{ \textrm{FIXME: allow more fields in type, ignore order} \\
|
||||
\textrm{FIXME: types can depend on field values} \\
|
||||
\Delta \vdash_p p_1 \ \downarrow \ T_1; \Gamma_1 \\
|
||||
\ldots \\
|
||||
\Delta \vdash_p p_n \ \downarrow \ T_n; \Gamma_n \\
|
||||
\Gamma_1 \ldots \Gamma_n \ \textrm{disjoint} \\
|
||||
l_1 \ldots l_n \ \textrm{different}
|
||||
}
|
||||
{ \Delta \vdash_p \textrm{rec} \ \{ l_1 = p_1; \ldots; l_n = p_n \} \ \downarrow \
|
||||
\textrm{sig} \ \{ l_1 : T_1; \ldots; l_n : T_n \}; \Gamma_1, \ldots, \Gamma_n }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Integer literal pattern]
|
||||
{ }
|
||||
{ \Delta \vdash_p integer \ \downarrow \ Integer; \{ \} }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[String literal pattern]
|
||||
{ }
|
||||
{ \Delta \vdash_p string \ \downarrow \ String; \{ \} }
|
||||
|
||||
\and
|
||||
|
||||
\end{mathpar}
|
||||
\caption{Type-checking patterns.}
|
||||
\label{fig:typing-patterns}
|
||||
\end{figure}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
\begin{figure}
|
||||
\begin{mathpar}
|
||||
|
||||
\inferrule[Integer type]
|
||||
{ }
|
||||
{ \Delta;\Gamma \vdash Integer \uparrow Type }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Integer literal]
|
||||
{ }
|
||||
{ \Delta;\Gamma \vdash integer \uparrow Integer }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Double type]
|
||||
{ }
|
||||
{ \Delta;\Gamma \vdash Double \uparrow Type }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Double literal]
|
||||
{ }
|
||||
{ \Delta;\Gamma \vdash double \uparrow Double }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[String type]
|
||||
{ }
|
||||
{ \Delta;\Gamma \vdash String \uparrow Type }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[String literal]
|
||||
{ }
|
||||
{ \Delta;\Gamma \vdash string \uparrow String }
|
||||
|
||||
\end{mathpar}
|
||||
\caption{Primitive types.}
|
||||
\label{fig:primitive-types}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}
|
||||
\begin{mathpar}
|
||||
|
||||
\inferrule[Subtype conversion]
|
||||
{ \vdash s \Downarrow_{wh} s' \\
|
||||
\vdash t \Downarrow_{wh} t' \\
|
||||
s' \leq t' }
|
||||
{ s \lesssim t }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Function type conversion]
|
||||
{ A_2 \lesssim A_1 \\
|
||||
B_1 [x_1/z] \lesssim B_2 [x_2/z] }
|
||||
{ (x_1 : A_1) \rightarrow B_1
|
||||
\leq (x_2 : A_2) \rightarrow B_2 }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Constructor conversion]
|
||||
{ s_1 \lesssim t_1 \\
|
||||
\ldots \\
|
||||
s_n \lesssim t_n \\
|
||||
}
|
||||
{ c \ s_1 \ldots s_n \leq c \ t_1 \ldots t_n }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Record type conversion]
|
||||
{ A_1 \lesssim B_1 \ldots A_n \lesssim B_n \\
|
||||
\textrm{FIXME: types can depend on fields} \\
|
||||
\textrm{FIXME: allow more fields on the left, ignore order} }
|
||||
{ \textrm{sig} \ \{ l_1 : A_1 \ldots l_n : A_n \}
|
||||
\leq
|
||||
\textrm{sig} \ \{ k_1 : B_1 \ldots k_m : B_m \} }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Record conversion]
|
||||
{
|
||||
\textrm{FIXME: allow more fields on the left, ignore order} \\
|
||||
s_1 \lesssim t_1 \ldots s_n \lesssim s_n
|
||||
}
|
||||
{ \textrm{rec} \ \{ l_1 = s_1 \ldots l_n = s_n \}
|
||||
\leq
|
||||
\textrm{rec} \ \{ k_1 = t_1 \ldots k_m = t_m \} }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Integer conversion]
|
||||
{ i_1 \ \textrm{integer} \\
|
||||
i_2 \ \textrm{integer} \\
|
||||
i_1 =_{integer} i_2}
|
||||
{ i_1 \leq i_2 }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[String conversion]
|
||||
{ i_1 \ \textrm{string} \\
|
||||
i_2 \ \textrm{string} \\
|
||||
i_1 =_{string} i_2}
|
||||
{ i_1 \leq i_2 }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[Double conversion]
|
||||
{ i_1 \ \textrm{double} \\
|
||||
i_2 \ \textrm{double} \\
|
||||
i_1 =_{double} i_2}
|
||||
{ i_1 \leq i_2 }
|
||||
|
||||
\end{mathpar}
|
||||
\caption{Conversion and subtyping.}
|
||||
\label{fig:conversion}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}
|
||||
\begin{mathpar}
|
||||
|
||||
\inferrule[WHNF-Let]
|
||||
{ s \Downarrow_{wh} s' \\
|
||||
\textrm{This is a weird way to evaluate a let} }
|
||||
{ \Gamma \vdash \textrm{let} \ x = s \ \textrm{in} \ t
|
||||
\Downarrow_{wh} t [x/s']
|
||||
}
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Case]
|
||||
{ \textrm{FIXME: find the right case arm} \\
|
||||
\textrm{FIXME: bind / substitute variables in RHS} }
|
||||
{ \Gamma \vdash \textrm{case} \ s \ \textrm{of} \{ \overline{p \mid t \rightarrow u} \}
|
||||
\Downarrow_{wh}
|
||||
}
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Beta]
|
||||
{ \Gamma \vdash s \Downarrow_{wh} \lambda x . s' \\
|
||||
\Gamma \vdash t \Downarrow_{wh} t' }
|
||||
{ \Gamma \vdash s \ t \Downarrow_{wh} s' [x/t'] \}
|
||||
}
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Proj]
|
||||
{ \Gamma \vdash s \Downarrow_{wh} \textrm{rec} \ \{ \ldots, l = t, \ldots \} }
|
||||
{ \Gamma \vdash s.l \Downarrow_{wh} t }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Var]
|
||||
{ x = t \in \Gamma \\
|
||||
\textrm{FIXME: there shouldn't be any free variables (but there can be functions and constructors)} }
|
||||
{ \Gamma \vdash x \Downarrow_{wh} t }
|
||||
|
||||
|
||||
% unchanged:
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Lambda]
|
||||
{ }
|
||||
{ \Gamma \vdash \lambda x . t \Downarrow_{wh} \lambda x . t }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Pi]
|
||||
{ }
|
||||
{ \Gamma \vdash (x : s) \rightarrow t \Downarrow_{wh} (x : s) \rightarrow t
|
||||
}
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Sig]
|
||||
{ }
|
||||
{ \Gamma \vdash \textrm{sig} \ \{ l_1 : A_1, \ldots, l_n : A_n \}
|
||||
\Downarrow_{wh} \textrm{sig} \ \{ l_1 : A_1, \ldots, l_n : A_n \} }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Rec]
|
||||
{ }
|
||||
{ \Gamma \vdash \textrm{rec} \ \{ l_1 = t_1, \ldots, l_n = t_n \}
|
||||
\Downarrow_{wh} \textrm{rec} \ \{ l_1 = t_1, \ldots, l_n = t_n \} }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Type]
|
||||
{ }
|
||||
{ \Gamma \vdash Type \Downarrow_{wh} Type }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-String]
|
||||
{ }
|
||||
{ \Gamma \vdash string \Downarrow_{wh} string }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Integer]
|
||||
{ }
|
||||
{ \Gamma \vdash integer \Downarrow_{wh} integer }
|
||||
|
||||
\and
|
||||
|
||||
\inferrule[WHNF-Double]
|
||||
{ }
|
||||
{ \Gamma \vdash double \Downarrow_{wh} double }
|
||||
|
||||
% FIXME: applications which are not beta redexes?
|
||||
|
||||
|
||||
|
||||
|
||||
\end{mathpar}
|
||||
\caption{Weak head normal form evaluation.}
|
||||
\label{fig:whnf-evaluation}
|
||||
\end{figure}
|
||||
|
||||
|
||||
|
||||
\end{document}
|
||||
@@ -1,24 +0,0 @@
|
||||
-- testing transfer: aggregation by def definitions. AR 12/4/2003 -- 9/10
|
||||
|
||||
-- p "Mary runs or John runs and John walks" | l -transfer=Aggregation
|
||||
-- Mary runs or John runs and walks
|
||||
-- Mary or John runs and John walks
|
||||
|
||||
-- The two results are due to ambiguity in parsing. Thus it is not spurious!
|
||||
|
||||
abstract Abstract = {
|
||||
|
||||
cat
|
||||
S ; NP ; VP ; Conj ;
|
||||
|
||||
fun
|
||||
Pred : NP -> VP -> S ;
|
||||
ConjS : Conj -> S -> S -> S ;
|
||||
ConjVP : Conj -> VP -> VP -> VP ;
|
||||
ConjNP : Conj -> NP -> NP -> NP ;
|
||||
|
||||
John, Mary, Bill : NP ;
|
||||
Walk, Run, Swim : VP ;
|
||||
And, Or : Conj ;
|
||||
|
||||
}
|
||||
@@ -1,41 +0,0 @@
|
||||
concrete English of Abstract = {
|
||||
|
||||
lincat
|
||||
VP = {s : Num => Str} ;
|
||||
NP, Conj = {s : Str ; n : Num} ;
|
||||
|
||||
lin
|
||||
Pred np vp = ss (np.s ++ vp.s ! np.n) ;
|
||||
ConjS c A B = ss (A.s ++ c.s ++ B.s) ;
|
||||
ConjVP c A B = {s = \\n => A.s ! n ++ c.s ++ B.s ! n} ;
|
||||
ConjNP c A B = {s = A.s ++ c.s ++ B.s ; n = c.n} ;
|
||||
|
||||
John = pn "John" ;
|
||||
Mary = pn "Mary" ;
|
||||
Bill = pn "Bill" ;
|
||||
Walk = vp "walk" ;
|
||||
Run = vp "run" ;
|
||||
Swim = vp "swim" ;
|
||||
|
||||
And = {s = "and" ; n = Pl} ;
|
||||
Or = pn "or" ;
|
||||
|
||||
param
|
||||
Num = Sg | Pl ;
|
||||
|
||||
oper
|
||||
vp : Str -> {s : Num => Str} = \run -> {
|
||||
s = table {
|
||||
Sg => run + "s" ;
|
||||
Pl => run
|
||||
}
|
||||
} ;
|
||||
|
||||
pn : Str -> {s : Str ; n : Num} = \bob -> {
|
||||
s = bob ;
|
||||
n = Sg
|
||||
} ;
|
||||
|
||||
ss : Str -> {s : Str} = \s -> {s = s} ;
|
||||
|
||||
}
|
||||
@@ -1,56 +0,0 @@
|
||||
import prelude
|
||||
import tree
|
||||
|
||||
|
||||
-- aggreg specialized for Tree S
|
||||
aggregS : Tree S -> Tree S
|
||||
aggregS = aggreg S
|
||||
|
||||
-- For now, here's what we have to do:
|
||||
aggreg : (A : Type) -> Tree A -> Tree A
|
||||
aggreg _ t =
|
||||
case t of
|
||||
ConjS c s1 s2 ->
|
||||
case (aggreg ? s1, aggreg ? s2) of
|
||||
(Pred np1 vp1, Pred np2 vp2) | eq NP (eq_Tree NP) np1 np2 ->
|
||||
Pred np1 (ConjVP c vp1 vp2)
|
||||
(Pred np1 vp1, Pred np2 vp2) | eq VP (eq_Tree VP) vp1 vp2 ->
|
||||
Pred (ConjNP c np1 np2) vp1
|
||||
(s1',s2') -> ConjS c s1' s2'
|
||||
_ -> composOp ? ? compos_Tree ? aggreg t
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
{-
|
||||
-- When the Transfer compiler gets meta variable inference,
|
||||
-- we can write this:
|
||||
aggreg : (A : Type) -> Tree A -> Tree A
|
||||
aggreg _ t =
|
||||
case t of
|
||||
ConjS c s1 s2 ->
|
||||
case (aggreg ? s1, aggreg ? s2) of
|
||||
(Pred np1 vp1, Pred np2 vp2) | np1 == np2 ->
|
||||
Pred np1 (ConjVP c vp1 vp2)
|
||||
(Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 ->
|
||||
Pred (ConjNP c np1 np2) vp1
|
||||
(s1',s2') -> ConjS c s1' s2'
|
||||
_ -> composOp ? ? ? ? aggreg t
|
||||
-}
|
||||
|
||||
|
||||
{-
|
||||
-- If we added idden arguments, we could write something like this:
|
||||
aggreg : (A : Type) => Tree A -> Tree A
|
||||
aggreg t =
|
||||
case t of
|
||||
ConjS c s1 s2 ->
|
||||
case (aggreg s1, aggreg s2) of
|
||||
(Pred np1 vp1, Pred np2 vp2) | np1 == np2 ->
|
||||
Pred np1 (ConjVP c vp1 vp2)
|
||||
(Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 ->
|
||||
Pred (ConjNP c np1 np2) vp1
|
||||
(s1',s2') -> ConjS c s1' s2'
|
||||
_ -> composOp aggreg t
|
||||
-}
|
||||
@@ -1,23 +0,0 @@
|
||||
import prelude ;
|
||||
data Cat : Type where {
|
||||
Conj : Cat ;
|
||||
NP : Cat ;
|
||||
S : Cat ;
|
||||
VP : Cat
|
||||
} ;
|
||||
data Tree : Cat -> Type where {
|
||||
And : Tree Conj ;
|
||||
Bill : Tree NP ;
|
||||
ConjNP : Tree Conj -> Tree NP -> Tree NP -> Tree NP ;
|
||||
ConjS : Tree Conj -> Tree S -> Tree S -> Tree S ;
|
||||
ConjVP : Tree Conj -> Tree VP -> Tree VP -> Tree VP ;
|
||||
John : Tree NP ;
|
||||
Mary : Tree NP ;
|
||||
Or : Tree Conj ;
|
||||
Pred : Tree NP -> Tree VP -> Tree S ;
|
||||
Run : Tree VP ;
|
||||
Swim : Tree VP ;
|
||||
Walk : Tree VP
|
||||
} ;
|
||||
derive Eq Tree ;
|
||||
derive Compos Tree ;
|
||||
@@ -1,24 +0,0 @@
|
||||
data Cat : Type where
|
||||
VarOrWild : Cat
|
||||
Exp : Cat
|
||||
Ident : Cat
|
||||
|
||||
data Tree : Cat -> Type where
|
||||
EAbs : Tree VarOrWild -> Tree Exp -> Tree Exp
|
||||
EPi : Tree VarOrWild -> Tree Exp -> Tree Exp -> Tree Exp
|
||||
EVar : Tree Ident -> Tree Exp
|
||||
EType : Tree Exp
|
||||
EStr : String -> Tree Exp
|
||||
EInt : Integer -> Tree Exp
|
||||
VVar : Tree Ident -> Tree VarOrWild
|
||||
VWild : Tree VarOrWild
|
||||
Ident : String -> Tree Ident
|
||||
|
||||
|
||||
f e = case e of
|
||||
EAbs (VWild || VVar _) e || EPi (VWild || VVar _) _ e -> doSomething e
|
||||
Ident i -> Ident i
|
||||
_ -> catchAll
|
||||
|
||||
|
||||
g (Ident x || EAbs (VWild || VVar _) t e) = x e
|
||||
@@ -1,33 +0,0 @@
|
||||
import prelude
|
||||
|
||||
data Cat : Type where
|
||||
Stm : Cat
|
||||
Exp : Cat
|
||||
Var : Cat
|
||||
Typ : Cat
|
||||
ListStm : Cat
|
||||
|
||||
data Tree : Cat -> Type where
|
||||
SDecl : Tree Typ -> Tree Var -> Tree Stm
|
||||
SAss : Tree Var -> Tree Exp -> Tree Stm
|
||||
SBlock : Tree ListStm -> Tree Stm
|
||||
EAdd : Tree Exp -> Tree Exp -> Tree Exp
|
||||
EStm : Tree Stm -> Tree Exp
|
||||
EVar : Tree Var -> Tree Exp
|
||||
EInt : Integer -> Tree Exp
|
||||
V : String -> Tree Var
|
||||
TInt : Tree Typ
|
||||
TFloat : Tree Typ
|
||||
|
||||
NilStm : Tree ListStm
|
||||
ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm
|
||||
|
||||
derive Compos Tree
|
||||
|
||||
rename : (String -> String) -> (C : Type) -> Tree C -> Tree C
|
||||
rename f C t = case t of
|
||||
V x -> V (f x)
|
||||
_ -> composOp ? ? compos_Tree C (rename f) t
|
||||
|
||||
|
||||
main = rename (const ? ? "apa") Stm (SAss (V "y") (EAdd (EVar (V "x")) (EInt 2)))
|
||||
@@ -1,12 +0,0 @@
|
||||
import nat
|
||||
import prelude
|
||||
|
||||
fib : Integer -> Integer
|
||||
fib 0 = 1
|
||||
fib 1 = 1
|
||||
fib n = fib (n-1) + fib (n-2)
|
||||
|
||||
fibNat : Nat -> Nat
|
||||
fibNat Zero = Succ Zero
|
||||
fibNat (Succ Zero) = Succ Zero
|
||||
fibNat (Succ (Succ n)) = plus Nat add_Nat (fibNat (Succ n)) (fibNat n)
|
||||
@@ -1,9 +0,0 @@
|
||||
x : Apa
|
||||
x = let x = y
|
||||
in case y of
|
||||
f -> q
|
||||
_ -> a
|
||||
|
||||
f = apa
|
||||
|
||||
g = bepa
|
||||
@@ -1,6 +0,0 @@
|
||||
import prelude
|
||||
|
||||
l1 = append ? [1,2,3,5,6] [3]
|
||||
l2 = 2 :: l1
|
||||
|
||||
main = rec { x = length ? l2; y = l2}
|
||||
@@ -1,94 +0,0 @@
|
||||
import prelude
|
||||
|
||||
data Cat : Type where {
|
||||
Digit : Cat ;
|
||||
Numeral : Cat ;
|
||||
Sub10 : Cat ;
|
||||
Sub100 : Cat ;
|
||||
Sub1000 : Cat ;
|
||||
Sub1000000 : Cat
|
||||
} ;
|
||||
|
||||
data Tree : (_ : Cat)-> Type where {
|
||||
n2 : Tree Digit ;
|
||||
n3 : Tree Digit ;
|
||||
n4 : Tree Digit ;
|
||||
n5 : Tree Digit ;
|
||||
n6 : Tree Digit ;
|
||||
n7 : Tree Digit ;
|
||||
n8 : Tree Digit ;
|
||||
n9 : Tree Digit ;
|
||||
num : (_ : Tree Sub1000000)-> Tree Numeral ;
|
||||
pot0 : (_ : Tree Digit)-> Tree Sub10 ;
|
||||
pot01 : Tree Sub10 ;
|
||||
pot0as1 : (_ : Tree Sub10)-> Tree Sub100 ;
|
||||
pot1 : (_ : Tree Digit)-> Tree Sub100 ;
|
||||
pot110 : Tree Sub100 ;
|
||||
pot111 : Tree Sub100 ;
|
||||
pot1as2 : (_ : Tree Sub100)-> Tree Sub1000 ;
|
||||
pot1plus : (_ : Tree Digit)-> (_ : Tree Sub10)-> Tree Sub100 ;
|
||||
pot1to19 : (_ : Tree Digit)-> Tree Sub100 ;
|
||||
pot2 : (_ : Tree Sub10)-> Tree Sub1000 ;
|
||||
pot2as3 : (_ : Tree Sub1000)-> Tree Sub1000000 ;
|
||||
pot2plus : (_ : Tree Sub10)-> (_ : Tree Sub100)-> Tree Sub1000 ;
|
||||
pot3 : (_ : Tree Sub1000)-> Tree Sub1000000 ;
|
||||
pot3plus : (_ : Tree Sub1000)-> (_ : Tree Sub1000)-> Tree Sub1000000
|
||||
}
|
||||
|
||||
derive Compos Tree
|
||||
|
||||
|
||||
data Binary_Cat : Type where {
|
||||
Bin : Binary_Cat
|
||||
} ;
|
||||
data Binary_Tree : (_ : Binary_Cat)-> Type where {
|
||||
End : Binary_Tree Bin ;
|
||||
One : (_ : Binary_Tree Bin)-> Binary_Tree Bin ;
|
||||
Zero : (_ : Binary_Tree Bin)-> Binary_Tree Bin
|
||||
}
|
||||
|
||||
|
||||
|
||||
monoid_plus_Int : Monoid Integer
|
||||
monoid_plus_Int = rec mzero = 0
|
||||
mplus = (\x -> \y -> x + y)
|
||||
|
||||
|
||||
num2int : Tree Numeral -> Integer
|
||||
num2int = tree2int ?
|
||||
|
||||
tree2int : (C : Cat) -> Tree C -> Integer
|
||||
tree2int _ n = case n of
|
||||
n2 -> 2
|
||||
n3 -> 3
|
||||
n4 -> 4
|
||||
n5 -> 5
|
||||
n6 -> 6
|
||||
n7 -> 7
|
||||
n8 -> 8
|
||||
n9 -> 9
|
||||
pot01 -> 1
|
||||
pot1 x -> 10 * tree2int ? x
|
||||
pot110 -> 10
|
||||
pot111 -> 11
|
||||
pot1plus x y -> 10 * tree2int ? x + tree2int ? y
|
||||
pot1to19 x -> 10 + tree2int ? x
|
||||
pot2 x -> 100 * tree2int ? x
|
||||
pot2as3 x -> 10 * tree2int ? x
|
||||
pot2plus x y -> 100 * tree2int ? x + tree2int ? y
|
||||
pot3 x -> 1000 * tree2int ? x
|
||||
pot3plus x y -> 1000 * tree2int ? x + tree2int ? y
|
||||
_ -> composFold ? ? compos_Tree ? monoid_plus_Int C tree2int n
|
||||
|
||||
int2bin : Integer -> Binary_Tree Bin
|
||||
int2bin = int2bin_ End
|
||||
|
||||
int2bin_ : Binary_Tree Bin -> Integer -> Binary_Tree Bin
|
||||
int2bin_ b 0 = b
|
||||
int2bin_ b n = let d = if n % 2 == 0 then Zero else One
|
||||
q = n / 2
|
||||
in int2bin_ (d b) q
|
||||
|
||||
num2bin : Tree Numeral -> Binary_Tree Bin
|
||||
num2bin n = int2bin (num2int n)
|
||||
|
||||
@@ -1,15 +0,0 @@
|
||||
abstract Abstract = {
|
||||
|
||||
cat
|
||||
S ; NP ; V2 ; Conj ;
|
||||
|
||||
fun
|
||||
PredV2 : V2 -> NP -> NP -> S ;
|
||||
ReflV2 : V2 -> NP -> S ;
|
||||
ConjNP : Conj -> NP -> NP -> NP ;
|
||||
|
||||
And, Or : Conj ;
|
||||
John, Mary, Bill : NP ;
|
||||
See, Whip : V2 ;
|
||||
|
||||
}
|
||||
@@ -1,54 +0,0 @@
|
||||
concrete English of Abstract = {
|
||||
|
||||
lincat
|
||||
S = { s : Str } ;
|
||||
V2 = {s : Num => Str} ;
|
||||
Conj = {s : Str ; n : Num} ;
|
||||
NP = {s : Str ; n : Num; g : Gender} ;
|
||||
|
||||
lin
|
||||
PredV2 v s o = ss (s.s ++ v.s ! s.n ++ o.s) ;
|
||||
ReflV2 v s = ss (s.s ++ v.s ! s.n ++ self ! s.n ! s.g) ;
|
||||
-- FIXME: what is the gender of "Mary or Bill"?
|
||||
ConjNP c A B = {s = A.s ++ c.s ++ B.s ; n = c.n; g = A.g } ;
|
||||
|
||||
John = pn Masc "John" ;
|
||||
Mary = pn Fem "Mary" ;
|
||||
Bill = pn Masc "Bill" ;
|
||||
See = regV2 "see" ;
|
||||
Whip = regV2 "whip" ;
|
||||
|
||||
And = {s = "and" ; n = Pl } ;
|
||||
Or = { s = "or"; n = Sg } ;
|
||||
|
||||
param
|
||||
Num = Sg | Pl ;
|
||||
Gender = Neutr | Masc | Fem ;
|
||||
|
||||
oper
|
||||
regV2 : Str -> {s : Num => Str} = \run -> {
|
||||
s = table {
|
||||
Sg => run + "s" ;
|
||||
Pl => run
|
||||
}
|
||||
} ;
|
||||
|
||||
self : Num => Gender => Str =
|
||||
table {
|
||||
Sg => table {
|
||||
Neutr => "itself";
|
||||
Masc => "himself";
|
||||
Fem => "herself"
|
||||
};
|
||||
Pl => \\g => "themselves"
|
||||
};
|
||||
|
||||
pn : Gender -> Str -> {s : Str ; n : Num; g : Gender} = \gen -> \bob -> {
|
||||
s = bob ;
|
||||
n = Sg ;
|
||||
g = gen
|
||||
} ;
|
||||
|
||||
ss : Str -> {s : Str} = \s -> {s = s} ;
|
||||
|
||||
}
|
||||
@@ -1,40 +0,0 @@
|
||||
{-
|
||||
|
||||
$ ../../transferc -i../../lib reflexive.tra
|
||||
|
||||
$ gf English.gf reflexive.trc
|
||||
|
||||
> p -tr "John sees John" | at -tr reflexivize_S | l
|
||||
PredV2 See John John
|
||||
ReflV2 See John
|
||||
John sees himself
|
||||
|
||||
> p -tr "John and Bill see John and Bill" | at -tr reflexivize_S | l
|
||||
PredV2 See (ConjNP And John Bill) (ConjNP And John Bill)
|
||||
ReflV2 See (ConjNP And John Bill)
|
||||
John and Bill see themselves
|
||||
|
||||
> p -tr "John sees Mary" | at -tr reflexivize_S | l
|
||||
PredV2 See John Mary
|
||||
PredV2 See John Mary
|
||||
John sees Mary
|
||||
|
||||
-}
|
||||
|
||||
import tree
|
||||
|
||||
reflexivize : (C : Cat) -> Tree C -> Tree C
|
||||
reflexivize _ (PredV2 v s o) | eq ? (eq_Tree ?) s o = ReflV2 v s
|
||||
reflexivize _ t = composOp ? ? compos_Tree ? reflexivize t
|
||||
|
||||
reflexivize_S : Tree S -> Tree S
|
||||
reflexivize_S = reflexivize S
|
||||
|
||||
{-
|
||||
With a type checker and hidden arguments we could write:
|
||||
|
||||
reflexivize : {C : Cat} -> Tree C -> Tree C
|
||||
reflexivize (PredV2 v s o) | s == o = ReflV2 v s
|
||||
reflexivize t = composOp reflexivize t
|
||||
|
||||
-}
|
||||
@@ -1,21 +0,0 @@
|
||||
import prelude ;
|
||||
data Cat : Type where {
|
||||
Conj : Cat ;
|
||||
NP : Cat ;
|
||||
S : Cat ;
|
||||
V2 : Cat
|
||||
} ;
|
||||
data Tree : Cat -> Type where {
|
||||
And : Tree Conj ;
|
||||
Bill : Tree NP ;
|
||||
ConjNP : Tree Conj -> Tree NP -> Tree NP -> Tree NP ;
|
||||
John : Tree NP ;
|
||||
Mary : Tree NP ;
|
||||
Or : Tree Conj ;
|
||||
PredV2 : Tree V2 -> Tree NP -> Tree NP -> Tree S ;
|
||||
ReflV2 : Tree V2 -> Tree NP -> Tree S ;
|
||||
See : Tree V2 ;
|
||||
Whip : Tree V2
|
||||
} ;
|
||||
derive Eq Tree ;
|
||||
derive Compos Tree ;
|
||||
@@ -1,210 +0,0 @@
|
||||
import prelude
|
||||
|
||||
data Cat : Type where {
|
||||
CN : Cat ;
|
||||
NP : Cat ;
|
||||
S : Cat
|
||||
} ;
|
||||
data Tree : (_ : Cat)-> Type where {
|
||||
A : (h_ : Tree CN)-> Tree NP ;
|
||||
All : (h_ : Tree CN)-> Tree NP ;
|
||||
Animal : Tree CN ;
|
||||
Ashes : Tree CN ;
|
||||
Back : Tree CN ;
|
||||
Bad : (h_ : Tree CN)-> Tree CN ;
|
||||
Bark : Tree CN ;
|
||||
Belly : Tree CN ;
|
||||
Big : (h_ : Tree CN)-> Tree CN ;
|
||||
Bird : Tree CN ;
|
||||
Bite : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Black : (h_ : Tree CN)-> Tree CN ;
|
||||
Blood : Tree CN ;
|
||||
Blow : (h_ : Tree NP)-> Tree S ;
|
||||
Bone : Tree CN ;
|
||||
Breast : Tree CN ;
|
||||
Breathe : (h_ : Tree NP)-> Tree S ;
|
||||
Burn : (h_ : Tree NP)-> Tree S ;
|
||||
Child : Tree CN ;
|
||||
Cloud : Tree CN ;
|
||||
Cold : (h_ : Tree CN)-> Tree CN ;
|
||||
Come : (h_ : Tree NP)-> Tree S ;
|
||||
Correct : (h_ : Tree CN)-> Tree CN ;
|
||||
Count : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Cut : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Day : Tree CN ;
|
||||
Die : (h_ : Tree NP)-> Tree S ;
|
||||
Dig : (h_ : Tree NP)-> Tree S ;
|
||||
Dirty : (h_ : Tree CN)-> Tree CN ;
|
||||
Dog : Tree CN ;
|
||||
Drink : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Dry : (h_ : Tree CN)-> Tree CN ;
|
||||
Dull : (h_ : Tree CN)-> Tree CN ;
|
||||
Dust : Tree CN ;
|
||||
Ear : Tree CN ;
|
||||
Earth : Tree CN ;
|
||||
Eat : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Egg : Tree CN ;
|
||||
Eye : Tree CN ;
|
||||
Fall : (h_ : Tree NP)-> Tree S ;
|
||||
Fat : Tree CN ;
|
||||
Father : Tree CN ;
|
||||
FatherOf : (h_ : Tree NP)-> Tree CN ;
|
||||
Fear : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Feather : Tree CN ;
|
||||
Few : (h_ : Tree CN)-> Tree NP ;
|
||||
Fight : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Fingernail : Tree CN ;
|
||||
Fire : Tree CN ;
|
||||
Fish : Tree CN ;
|
||||
Five : (h_ : Tree CN)-> Tree NP ;
|
||||
Float : (h_ : Tree NP)-> Tree S ;
|
||||
Flow : (h_ : Tree NP)-> Tree S ;
|
||||
Flower : Tree CN ;
|
||||
Fly : (h_ : Tree NP)-> Tree S ;
|
||||
Fog : Tree CN ;
|
||||
Foot : Tree CN ;
|
||||
Forest : Tree CN ;
|
||||
Four : (h_ : Tree CN)-> Tree NP ;
|
||||
Freeze : (h_ : Tree NP)-> Tree S ;
|
||||
Fruit : Tree CN ;
|
||||
Full : (h_ : Tree CN)-> Tree CN ;
|
||||
Give : (h_ : Tree NP)-> (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Good : (h_ : Tree CN)-> Tree CN ;
|
||||
Grass : Tree CN ;
|
||||
Green : (h_ : Tree CN)-> Tree CN ;
|
||||
Guts : Tree CN ;
|
||||
Hair : Tree CN ;
|
||||
Hand : Tree CN ;
|
||||
He : Tree NP ;
|
||||
Head : Tree CN ;
|
||||
Hear : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Heart : Tree CN ;
|
||||
Heavy : (h_ : Tree CN)-> Tree CN ;
|
||||
Hit : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Hold : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Horn : Tree CN ;
|
||||
Hunt : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Husband : Tree CN ;
|
||||
I : Tree NP ;
|
||||
Ice : Tree CN ;
|
||||
Kill : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Knee : Tree CN ;
|
||||
Know : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Lake : Tree CN ;
|
||||
Laugh : (h_ : Tree NP)-> Tree S ;
|
||||
Leaf : Tree CN ;
|
||||
Left : (h_ : Tree CN)-> Tree CN ;
|
||||
Leg : Tree CN ;
|
||||
Lie : (h_ : Tree NP)-> Tree S ;
|
||||
Live : (h_ : Tree NP)-> Tree S ;
|
||||
Liver : Tree CN ;
|
||||
Long : (h_ : Tree CN)-> Tree CN ;
|
||||
Louse : Tree CN ;
|
||||
Man : Tree CN ;
|
||||
Many : (h_ : Tree CN)-> Tree NP ;
|
||||
Meat : Tree CN ;
|
||||
Moon : Tree CN ;
|
||||
Mother : Tree CN ;
|
||||
MotherOf : (h_ : Tree NP)-> Tree CN ;
|
||||
Mountain : Tree CN ;
|
||||
Mouth : Tree CN ;
|
||||
Name : Tree CN ;
|
||||
Narrow : (h_ : Tree CN)-> Tree CN ;
|
||||
Near : (h_ : Tree CN)-> Tree CN ;
|
||||
Neck : Tree CN ;
|
||||
New : (h_ : Tree CN)-> Tree CN ;
|
||||
Night : Tree CN ;
|
||||
Nose : Tree CN ;
|
||||
Old : (h_ : Tree CN)-> Tree CN ;
|
||||
One : (h_ : Tree CN)-> Tree NP ;
|
||||
Other : (h_ : Tree CN)-> Tree NP ;
|
||||
Person : Tree CN ;
|
||||
Play : (h_ : Tree NP)-> Tree S ;
|
||||
Pull : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Push : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Rain : Tree CN ;
|
||||
Red : (h_ : Tree CN)-> Tree CN ;
|
||||
Right : (h_ : Tree CN)-> Tree CN ;
|
||||
River : Tree CN ;
|
||||
Road : Tree CN ;
|
||||
Root : Tree CN ;
|
||||
Rope : Tree CN ;
|
||||
Rotten : (h_ : Tree CN)-> Tree CN ;
|
||||
Round : (h_ : Tree CN)-> Tree CN ;
|
||||
Rub : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Salt : Tree CN ;
|
||||
Sand : Tree CN ;
|
||||
Scratch : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Sea : Tree CN ;
|
||||
See : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Seed : Tree CN ;
|
||||
Sew : (h_ : Tree NP)-> Tree S ;
|
||||
Sharp : (h_ : Tree CN)-> Tree CN ;
|
||||
Short : (h_ : Tree CN)-> Tree CN ;
|
||||
Sing : (h_ : Tree NP)-> Tree S ;
|
||||
Sit : (h_ : Tree NP)-> Tree S ;
|
||||
Skin : Tree CN ;
|
||||
Sky : Tree CN ;
|
||||
Sleep : (h_ : Tree NP)-> Tree S ;
|
||||
Small : (h_ : Tree CN)-> Tree CN ;
|
||||
Smell : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Smoke : Tree CN ;
|
||||
Smooth : (h_ : Tree CN)-> Tree CN ;
|
||||
Snake : Tree CN ;
|
||||
Snow : Tree CN ;
|
||||
Some_Many : (h_ : Tree CN)-> Tree NP ;
|
||||
Some_One : (h_ : Tree CN)-> Tree NP ;
|
||||
Spit : (h_ : Tree NP)-> Tree S ;
|
||||
Split : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Squeeze : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Stab : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Stand : (h_ : Tree NP)-> Tree S ;
|
||||
Star : Tree CN ;
|
||||
Stick : Tree CN ;
|
||||
Stone : Tree CN ;
|
||||
Straight : (h_ : Tree CN)-> Tree CN ;
|
||||
Suck : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Sun : Tree CN ;
|
||||
Swell : (h_ : Tree NP)-> Tree S ;
|
||||
Swim : (h_ : Tree NP)-> Tree S ;
|
||||
Tail : Tree CN ;
|
||||
That : (h_ : Tree CN)-> Tree NP ;
|
||||
The_Many : (h_ : Tree CN)-> Tree NP ;
|
||||
The_One : (h_ : Tree CN)-> Tree NP ;
|
||||
They : Tree NP ;
|
||||
Thick : (h_ : Tree CN)-> Tree CN ;
|
||||
Thin : (h_ : Tree CN)-> Tree CN ;
|
||||
Think : (h_ : Tree NP)-> Tree S ;
|
||||
This : (h_ : Tree CN)-> Tree NP ;
|
||||
Three : (h_ : Tree CN)-> Tree NP ;
|
||||
Throw : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Tie : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Tongue : Tree CN ;
|
||||
Tooth : Tree CN ;
|
||||
Tree : Tree CN ;
|
||||
Turn : (h_ : Tree NP)-> Tree S ;
|
||||
Two : (h_ : Tree CN)-> Tree NP ;
|
||||
Vomit : (h_ : Tree NP)-> Tree S ;
|
||||
Walk : (h_ : Tree NP)-> Tree S ;
|
||||
Warm : (h_ : Tree CN)-> Tree CN ;
|
||||
Wash : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Water : Tree CN ;
|
||||
We : Tree NP ;
|
||||
Wet : (h_ : Tree CN)-> Tree CN ;
|
||||
White : (h_ : Tree CN)-> Tree CN ;
|
||||
Wide : (h_ : Tree CN)-> Tree CN ;
|
||||
Wife : Tree CN ;
|
||||
Wind : Tree CN ;
|
||||
Wing : Tree CN ;
|
||||
Wipe : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ;
|
||||
Woman : Tree CN ;
|
||||
Worm : Tree CN ;
|
||||
Year : Tree CN ;
|
||||
Yellow : (h_ : Tree CN)-> Tree CN ;
|
||||
You_Many : Tree NP ;
|
||||
You_One : Tree NP
|
||||
}
|
||||
|
||||
derive Compos Tree
|
||||
|
||||
derive Eq Tree
|
||||
@@ -1,4 +0,0 @@
|
||||
import nat
|
||||
import fib
|
||||
|
||||
main = (\x -> (\x -> \x -> x) 1 x) 5
|
||||
@@ -1,37 +0,0 @@
|
||||
|
||||
--
|
||||
-- Pattern matching and inductive families.
|
||||
--
|
||||
|
||||
data Tree : Type -> Type where
|
||||
EAdd : Tree Integer -> Tree Integer -> Tree Integer
|
||||
EInt : Integer -> Tree Integer
|
||||
EFoo : (A:Type) -> A -> Tree A
|
||||
|
||||
eval : (B : Type) -> Tree B -> Tree B
|
||||
eval _ t = case t of
|
||||
EAdd x y -> EInt (x+y)
|
||||
EInt i -> EInt i
|
||||
EFoo T x -> EFoo T x
|
||||
|
||||
strip : (B : Type) -> Tree B -> B
|
||||
strip _ t = case t of
|
||||
EAdd x y -> x+y
|
||||
EInt i -> i
|
||||
EFoo _ x -> x
|
||||
|
||||
--
|
||||
-- Subtyping
|
||||
--
|
||||
|
||||
getX : { x : Integer } -> Integer
|
||||
getX r = r.x
|
||||
|
||||
getY : { y : Integer } -> Integer
|
||||
getY r = r.y
|
||||
|
||||
proj2 : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B) -> (A -> C) -> A -> (B,C)
|
||||
proj2 _ _ _ f g x = (f x, g x)
|
||||
|
||||
getXY : { x : Integer, y : Integer } -> (Integer,Integer)
|
||||
getXY r = proj2 ? ? ? getX getY r
|
||||
@@ -1,21 +0,0 @@
|
||||
import bool
|
||||
import stoneage
|
||||
|
||||
monoid_Bool : sig { zero : Bool; plus : Bool -> Bool -> Bool }
|
||||
monoid_Bool = rec
|
||||
zero = False
|
||||
plus = \x -> \y -> x && y
|
||||
|
||||
isSnake : (A : Tree) -> Tree A -> Bool
|
||||
isSnake _ x = case x of
|
||||
Snake -> True
|
||||
_ -> composFold ? ? compos_Tree Bool monoid_Bool ? isSnake x
|
||||
|
||||
wideSnake : (A : Cat) -> Tree A -> Tree A
|
||||
wideSnake _ x = case x of
|
||||
Wide y -> let y' = wideSnake ? y
|
||||
in if isSnake CN y' then Thick y' else Wide y'
|
||||
_ -> composOp ? ? compos_Tree ? wideSnake x
|
||||
|
||||
wideSnakeNP : Tree NP -> Tree NP
|
||||
wideSnakeNP = wideSnake NP
|
||||
@@ -1,22 +0,0 @@
|
||||
-- NOTE: this is unfinished and untested
|
||||
|
||||
import prelude
|
||||
|
||||
data BinTree : Type -> Type where
|
||||
Leaf : (A:Type) -> BinTree A
|
||||
Node : (A:Type) -> BinTree A -> A -> BinTree A -> BinTree A
|
||||
|
||||
contains : (A:Type) -> Ord A -> A -> BinTree A -> Bool
|
||||
contains _ _ _ (Leaf _) = False
|
||||
contains A o x (Node _ l y r)
|
||||
| x < y = contains A o x l
|
||||
| x > y = contains A o x r
|
||||
| otherwise = True
|
||||
|
||||
insert : (A:Type) -> Ord A -> A -> BinTree A -> BinTree A
|
||||
insert A o x (Leaf _) = Node A (Leaf A) x (Leaf A)
|
||||
insert A o x (Node _ l y r)
|
||||
| x < y = Node A (insert A o x l) y r
|
||||
| x > y = Node A l y (insert A o x r)
|
||||
| otherwise = Node A l x r
|
||||
|
||||
@@ -1,6 +0,0 @@
|
||||
import prelude
|
||||
|
||||
depif : (A:Type) -> (B:Type) -> (b:Bool) -> A -> B -> if Type b then A else B
|
||||
depif _ _ True x _ = x
|
||||
depif _ _ False _ y = y
|
||||
|
||||
@@ -1,77 +0,0 @@
|
||||
-- NOTE: this is unfinished and untested
|
||||
|
||||
import prelude
|
||||
import bintree
|
||||
|
||||
Collection : Type -> Type
|
||||
Collection C =
|
||||
sig
|
||||
-- types
|
||||
Elem : Type
|
||||
-- Add stuff
|
||||
zero : C
|
||||
plus : C -> C -> C
|
||||
-- Collection-specific stuff
|
||||
size : C -> Integer
|
||||
add : Elem -> C -> C
|
||||
elem : Elem -> C -> Bool
|
||||
map : (Elem -> Elem) -> C -> C
|
||||
filter : (Elem -> Bool) -> C -> C
|
||||
fromList : List Elem -> C
|
||||
toList : C -> List Elem
|
||||
|
||||
|
||||
--
|
||||
-- Collection String instance
|
||||
--
|
||||
|
||||
collection_String : Collection String
|
||||
collection_String =
|
||||
rec
|
||||
Elem = Char
|
||||
zero = ""
|
||||
plus = prim_add_String
|
||||
size = prim_length_String
|
||||
-- ...
|
||||
|
||||
|
||||
--
|
||||
-- Collection List instance
|
||||
--
|
||||
|
||||
collection_List : (A : Type) -> Collection (List A)
|
||||
collection_List A =
|
||||
rec
|
||||
Elem = A
|
||||
zero = Nil A
|
||||
plus = append A
|
||||
size = length A
|
||||
add = Cons A
|
||||
-- ...
|
||||
|
||||
--
|
||||
-- Collection Vector instance
|
||||
--
|
||||
|
||||
collection_Vector : (A : Type) -> (n : Nat) -> Collection (Vector A n)
|
||||
collection_Vector A n =
|
||||
rec
|
||||
Elem = A
|
||||
zero = Empty A
|
||||
plus = appendV A n n -- FIXME: this only works for vectors of the same length!
|
||||
-- ...
|
||||
|
||||
|
||||
--
|
||||
-- Collection BinTree instance
|
||||
--
|
||||
|
||||
collection_BinTree : (A : Type) -> Ord A -> Collection (BinTree A)
|
||||
collection_BinTree A o =
|
||||
rec
|
||||
Elem = A
|
||||
zero = Nil A
|
||||
plus = merge A o
|
||||
size = sizeBT A
|
||||
add = insert A o
|
||||
-- ...
|
||||
@@ -1,24 +0,0 @@
|
||||
import prelude
|
||||
|
||||
data Nat : Type where
|
||||
Zero : Nat
|
||||
Succ : (n:Nat) -> Nat
|
||||
|
||||
add_Nat : Add Nat
|
||||
add_Nat = rec zero = Zero
|
||||
plus = natPlus
|
||||
|
||||
natPlus : Nat -> Nat -> Nat
|
||||
natPlus Zero y = y
|
||||
natPlus (Succ x) y = Succ (natPlus x y)
|
||||
|
||||
pred : Nat -> Nat
|
||||
pred Zero = Zero
|
||||
pred (Succ n) = n
|
||||
|
||||
natToInt : Nat -> Integer
|
||||
natToInt Zero = 0
|
||||
natToInt (Succ n) = 1 + natToInt n
|
||||
|
||||
intToNat : Integer -> Nat
|
||||
intToNat n = if n == 0 then Zero else Succ (intToNat (n-1))
|
||||
@@ -1,502 +0,0 @@
|
||||
--
|
||||
-- Prelude for the transfer language.
|
||||
--
|
||||
|
||||
|
||||
--
|
||||
-- Basic functions
|
||||
--
|
||||
|
||||
const : (A:Type) -> (B:Type) -> A -> B -> A
|
||||
const _ _ x _ = x
|
||||
|
||||
id : (A:Type) -> A -> A
|
||||
id _ x = x
|
||||
|
||||
flip : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B -> C) -> B -> A -> C
|
||||
flip _ _ _ f x y = f y x
|
||||
|
||||
compose : (A:Type) -> (B:Type) -> (C:Type) -> (B -> C) -> (A -> B) -> A -> C
|
||||
compose _ _ _ f g x = f (g x)
|
||||
|
||||
otherwise : Bool
|
||||
otherwise = True
|
||||
|
||||
|
||||
--
|
||||
-- The Integer type
|
||||
--
|
||||
|
||||
-- Instances:
|
||||
|
||||
num_Integer : Num Integer
|
||||
num_Integer = rec zero = 0
|
||||
plus = prim_add_Integer
|
||||
minus = prim_sub_Integer
|
||||
one = 1
|
||||
times = prim_mul_Integer
|
||||
div = prim_div_Integer
|
||||
mod = prim_mod_Integer
|
||||
negate = prim_neg_Integer
|
||||
eq = prim_eq_Integer
|
||||
compare = prim_cmp_Integer
|
||||
|
||||
show_Integer : Show Integer
|
||||
show_Integer = rec show = prim_show_Integer
|
||||
|
||||
|
||||
--
|
||||
-- The Double type
|
||||
--
|
||||
|
||||
-- Instances:
|
||||
|
||||
num_Double : Num Double
|
||||
num_Double = rec zero = 0.0
|
||||
plus = prim_add_Double
|
||||
minus = prim_sub_Double
|
||||
one = 1.0
|
||||
times = prim_mul_Double
|
||||
div = prim_div_Double
|
||||
mod = prim_mod_Double
|
||||
negate = prim_neg_Double
|
||||
eq = prim_eq_Double
|
||||
compare = prim_cmp_Double
|
||||
|
||||
show_Double : Show Double
|
||||
show_Double = rec show = prim_show_Double
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The String type
|
||||
--
|
||||
|
||||
-- Instances:
|
||||
|
||||
add_String : Add String
|
||||
add_String = rec zero = ""
|
||||
plus = prim_add_String
|
||||
|
||||
|
||||
ord_String : Ord String
|
||||
ord_String = rec eq = prim_eq_String
|
||||
compare = prim_cmp_String
|
||||
|
||||
show_String : Show String
|
||||
show_String = rec show = prim_show_String
|
||||
|
||||
|
||||
--
|
||||
-- The Bool type
|
||||
--
|
||||
|
||||
data Bool : Type where
|
||||
True : Bool
|
||||
False : Bool
|
||||
|
||||
-- derive Show Bool
|
||||
derive Eq Bool
|
||||
-- derive Ord Bool
|
||||
|
||||
not : Bool -> Bool
|
||||
not b = if b then False else True
|
||||
|
||||
-- Instances:
|
||||
|
||||
neg_Bool : Neg Bool
|
||||
neg_Bool = rec negate = not
|
||||
|
||||
add_Bool : Add Bool
|
||||
add_Bool = rec zero = False
|
||||
plus = \x -> \y -> x || y
|
||||
|
||||
mul_Bool : Add Bool
|
||||
mul_Bool = rec one = True
|
||||
times = \x -> \y -> x && y
|
||||
|
||||
|
||||
--
|
||||
-- Tuples
|
||||
--
|
||||
|
||||
Pair : Type -> Type -> Type
|
||||
Pair A B = sig { p1 : A; p2 : B }
|
||||
|
||||
pair : (A:Type) -> (B:Type) -> A -> B -> Pair A B
|
||||
pair _ _ x y = rec { p1 = x; p2 = y }
|
||||
|
||||
fst : (A:Type) -> (B:Type) -> Pair A B -> A
|
||||
fst _ _ p = case p of Pair _ _ x _ -> x
|
||||
|
||||
snd : (A:Type) -> (B:Type) -> Pair A B -> B
|
||||
snd _ _ p = case p of Pair _ _ x _ -> x
|
||||
|
||||
{-
|
||||
|
||||
syntax:
|
||||
|
||||
(x1,...,xn) => { p1 = e1; ... ; pn = en }
|
||||
|
||||
where n >= 2 and x1,...,xn are expressions or patterns
|
||||
|
||||
-}
|
||||
|
||||
|
||||
--
|
||||
-- The List type
|
||||
--
|
||||
|
||||
data List : Type -> Type where
|
||||
Nil : (A:Type) -> List A
|
||||
Cons : (A:Type) -> A -> List A -> List A
|
||||
|
||||
foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B
|
||||
foldr _ _ _ x [] = x
|
||||
foldr A B f x (y::ys) = f y (foldr A B f x ys)
|
||||
|
||||
length : (A:Type) -> List A -> Integer
|
||||
length A = foldr A Integer (\_ -> \y -> y+1) 0
|
||||
|
||||
map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B
|
||||
map _ _ _ [] = []
|
||||
map A B f (x::xs) = f x :: map A B f xs
|
||||
|
||||
filter : (A:Type) -> (A -> Bool) -> List A -> List A
|
||||
filter _ _ [] = []
|
||||
filter A f (x::xs) | f x = x :: filter A f xs
|
||||
filter A f (x::xs) = filter A f xs
|
||||
|
||||
append : (A:Type) -> List A -> List A -> List A
|
||||
append A xs ys = foldr A (List A) (Cons A) ys xs
|
||||
|
||||
concat : (A : Type) -> List (List A) -> List A
|
||||
concat A = foldr (List A) (List A) (append A) (Nil A)
|
||||
|
||||
partition : (A : Type) -> (A -> Bool) -> List A -> Pair (List A) (List A)
|
||||
partition _ _ [] = ([],[])
|
||||
partition A p (x::xs) =
|
||||
let r = partition A p xs
|
||||
in if p x then (x :: r.p1, r.p2) else (r.p1, x :: r.p2)
|
||||
|
||||
|
||||
-- Instances:
|
||||
|
||||
add_List : (A : Type) -> Add (List A)
|
||||
add_List A = rec zero = Nil A
|
||||
plus = append A
|
||||
|
||||
|
||||
monad_List : Monad List
|
||||
monad_list = rec return = \A -> \x -> Cons A x (Nil A)
|
||||
bind = \A -> \B -> \m -> \k -> concat B (map A B k m)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Maybe type
|
||||
--
|
||||
|
||||
data Maybe : Type -> Type where
|
||||
Nothing : (A : Type) -> Maybe A
|
||||
Just : (A : Type) -> A -> Maybe A
|
||||
|
||||
-- derive Show Maybe
|
||||
derive Eq Maybe
|
||||
-- derive Ord Maybe
|
||||
|
||||
|
||||
fromMaybe : (A : Type) -> A -> Maybe A -> A
|
||||
fromMaybe _ x Nothing = x
|
||||
fromMaybe _ _ (Just x) = x
|
||||
|
||||
maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A
|
||||
maybe _ _ x _ Nothing = x
|
||||
maybe _ _ _ f (Just x) = f x
|
||||
|
||||
|
||||
-- Instances:
|
||||
|
||||
monad_Maybe : Monad Maybe
|
||||
monad_Maybe =
|
||||
rec return = Just
|
||||
bind = \A -> \B -> \m -> \k ->
|
||||
case m of
|
||||
Nothing _ -> Nothing B
|
||||
Just _ x -> k x
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Num class
|
||||
--
|
||||
|
||||
Num : Type -> Type
|
||||
Num A = sig zero : A
|
||||
plus : A -> A -> A
|
||||
minus : A -> A -> A
|
||||
one : A
|
||||
times : A -> A -> A
|
||||
div : A -> A -> A
|
||||
mod : A -> A -> A
|
||||
negate : A -> A
|
||||
eq : A -> A -> Bool
|
||||
compare : A -> A -> Ordering
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Add class
|
||||
--
|
||||
|
||||
Add : Type -> Type
|
||||
Add A = sig zero : A
|
||||
plus : A -> A -> A
|
||||
|
||||
zero : (A : Type) -> Add A -> A
|
||||
zero _ d = d.zero
|
||||
|
||||
plus : (A : Type) -> Add A -> A -> A -> A
|
||||
plus _ d = d.plus
|
||||
|
||||
sum : (A:Type) -> Add A -> List A -> A
|
||||
sum A d = foldr A A d.plus d.zero
|
||||
|
||||
|
||||
-- Operators:
|
||||
|
||||
{-
|
||||
(x + y) => (plus ? ? x y)
|
||||
-}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Sub class
|
||||
--
|
||||
|
||||
Sub : Type -> Type
|
||||
Sub = sig minus : A -> A -> A
|
||||
|
||||
minus : (A : Type) -> Sub A -> A
|
||||
minus _ d = d.minus
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Mul class
|
||||
--
|
||||
|
||||
Mul : Type -> Type
|
||||
Mul A = sig one : A
|
||||
times : A -> A -> A
|
||||
|
||||
one : (A : Type) -> Mul A -> A
|
||||
one _ d = d.one
|
||||
|
||||
times : (A : Type) -> Mul A -> A -> A -> A
|
||||
times _ d = d.times
|
||||
|
||||
product : (A:Type) -> Mul A -> List A -> A
|
||||
product A d = foldr A A d.times d.one
|
||||
|
||||
-- Operators:
|
||||
|
||||
{-
|
||||
(x * y) => (times ? ? x y)
|
||||
-}
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Div class
|
||||
--
|
||||
|
||||
Div : Type -> Type
|
||||
Div A = sig div : A -> A -> A
|
||||
mod : A -> A -> A
|
||||
|
||||
div : (A : Type) -> Div A -> A -> A -> A
|
||||
div _ d = d.div
|
||||
|
||||
mod : (A : Type) -> Div A -> A -> A -> A
|
||||
mod _ d = d.mod
|
||||
|
||||
-- Operators:
|
||||
|
||||
{-
|
||||
(x / y) => (div ? ? x y)
|
||||
(x % y) => (mod ? ? x y)
|
||||
-}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Neg class
|
||||
--
|
||||
|
||||
Neg : Type -> Type
|
||||
Neg A = sig negate : A -> A
|
||||
|
||||
negate : (A : Type) -> Neg A -> A -> A
|
||||
negate _ d = d.negate
|
||||
|
||||
-- Operators:
|
||||
|
||||
{-
|
||||
(-x) => negate ? ? x
|
||||
-}
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Eq class
|
||||
--
|
||||
|
||||
Eq : Type -> Type
|
||||
Eq A = sig eq : A -> A -> Bool
|
||||
|
||||
eq : (A : Type) -> Eq A -> A -> A -> Bool
|
||||
eq _ d = d.eq
|
||||
|
||||
neq : (A : Type) -> Eq A -> A -> A -> Bool
|
||||
neq A d x y = not (eq A d x y)
|
||||
|
||||
|
||||
-- Operators:
|
||||
|
||||
{-
|
||||
(x == y) => (eq ? ? x y)
|
||||
(x /= y) => (neq ? ? x y)
|
||||
-}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Ord class
|
||||
--
|
||||
|
||||
data Ordering : Type where
|
||||
LT : Ordering
|
||||
EQ : Ordering
|
||||
GT : Ordering
|
||||
|
||||
Ord : Type -> Type
|
||||
Ord A = sig eq : A -> A -> Bool
|
||||
compare : A -> A -> Ordering
|
||||
|
||||
compare : (A : Type) -> Ord A -> A -> A -> Ordering
|
||||
compare _ d = d.compare
|
||||
|
||||
ordOp : (Ordering -> Bool) -> (A : Type) -> Ord A -> A -> A -> Bool
|
||||
ordOp f A d x y = f (compare A d x y)
|
||||
|
||||
lt : (A : Type) -> Ord A -> A -> A -> Bool
|
||||
lt = ordOp (\o -> case o of { LT -> True; _ -> False })
|
||||
|
||||
le : (A : Type) -> Ord A -> A -> A -> Bool
|
||||
le = ordOp (\o -> case o of { GT -> False; _ -> True })
|
||||
|
||||
ge : (A : Type) -> Ord A -> A -> A -> Bool
|
||||
ge = ordOp (\o -> case o of { LT -> False; _ -> True })
|
||||
|
||||
gt : (A : Type) -> Ord A -> A -> A -> Bool
|
||||
gt = ordOp (\o -> case o of { GT -> True; _ -> False })
|
||||
|
||||
-- Operators:
|
||||
|
||||
{-
|
||||
(x < y) => (lt ? ? x y)
|
||||
(x <= y) => (le ? ? x y)
|
||||
(x >= y) => (ge ? ? x y)
|
||||
(x > y) => (gt ? ? x y)
|
||||
-}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Show class
|
||||
--
|
||||
|
||||
Show : Type -> Type
|
||||
Show A = sig show : A -> String
|
||||
|
||||
show : (A : Type) -> Show A -> A -> String
|
||||
show _ d = d.show
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Monoid class
|
||||
--
|
||||
|
||||
Monoid : Type -> Type
|
||||
Monoid A = sig mzero : A
|
||||
mplus : A -> A -> A
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Compos class
|
||||
--
|
||||
|
||||
Compos : (C : Type) -> (C -> Type) -> Type
|
||||
Compos C T = sig
|
||||
composOp : (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c
|
||||
composFold : (B : Type) -> Monoid B -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b
|
||||
|
||||
composOp : (C : Type) -> (T : C -> Type) -> (d : Compos C T)
|
||||
-> (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c
|
||||
composOp _ _ d = d.composOp
|
||||
|
||||
composFold : (C : Type) -> (T : C -> Type) -> (d : Compos C T) -> (B : Type) -> Monoid B
|
||||
-> (c : C) -> ((a : C) -> T a -> b) -> T c -> b
|
||||
composFold _ _ d = d.composFold
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--
|
||||
-- The Monad class
|
||||
--
|
||||
|
||||
Monad : (Type -> Type) -> Type
|
||||
Monad M = sig return : (A : Type) -> M A
|
||||
bind : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B
|
||||
|
||||
return : (M : Type -> Type) -> Monad M -> M A
|
||||
return _ d = d.return
|
||||
|
||||
bind : (M : Type -> Type) -> Monad M
|
||||
-> (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B
|
||||
bind _ d = d.bind
|
||||
|
||||
-- Operators:
|
||||
|
||||
{-
|
||||
(x >>= y) => bind ? ? ? ? x y
|
||||
(x >> y) => bind ? ? ? ? x (\_ -> y)
|
||||
-}
|
||||
|
||||
@@ -1,15 +0,0 @@
|
||||
-- NOTE: this is unfinished and untested
|
||||
|
||||
import nat
|
||||
|
||||
data Vector : Type -> Nat -> Type where
|
||||
Empty : (A:Type) -> Vector A Zero
|
||||
Cell : (A:Type) -> (n:Nat) -> A -> Vector A n -> Vector A (Succ n)
|
||||
|
||||
mapV : (A:Type) -> (B:Type) -> (n:Nat) -> (A -> B) -> Vector A n -> Vector B n
|
||||
mapV A B _ f (Empty _) = Empty B
|
||||
mapV A B (Succ n) f (Cell _ _ x xs) = Cell B n (f x) (mapV A B n f xs)
|
||||
|
||||
appendV : (A:Type) -> (n:Nat) -> (m:Nat) -> Vector A n -> Vector A m -> Vector A (plusNat n m)
|
||||
appendV A _ _ (Empty _) ys = ys
|
||||
appendV A (Succ n) m (Cell _ _ x xs) ys = appendV A n (Succ m) xs (Cell A m x ys)
|
||||
@@ -1,39 +0,0 @@
|
||||
module Main where
|
||||
|
||||
import Transfer.CompilerAPI
|
||||
|
||||
import Data.List (partition, isPrefixOf)
|
||||
import System.Environment
|
||||
import System.Exit
|
||||
import System.IO
|
||||
|
||||
die :: String -> IO a
|
||||
die s = do
|
||||
hPutStrLn stderr s
|
||||
exitFailure
|
||||
|
||||
getPath :: IO [String]
|
||||
getPath = do env <- getEnvironment
|
||||
return $ case lookup "TRANSFER_PATH" env of
|
||||
Nothing -> []
|
||||
Just p -> splitBy (==':') p
|
||||
|
||||
-- Modified version of a function which is originally
|
||||
-- Copyright Bryn Keller
|
||||
splitBy :: (a -> Bool) -> [a] -> [[a]]
|
||||
splitBy _ [] = []
|
||||
splitBy f list = first : splitBy f (dropWhile f rest)
|
||||
where (first, rest) = break f list
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
args <- getArgs
|
||||
let (flags,files) = partition ("-" `isPrefixOf`) args
|
||||
argPath = [ p | ('-':'i':p) <- flags ]
|
||||
envPath <- getPath
|
||||
case files of
|
||||
[f] -> do
|
||||
cf <- compileFile (argPath ++ envPath) f
|
||||
putStrLn $ "Wrote " ++ cf
|
||||
return ()
|
||||
_ -> die "Usage: transferc [-i<path> [-i<path> ... ]] <file>"
|
||||
@@ -1,37 +0,0 @@
|
||||
import Transfer.InterpreterAPI
|
||||
import Transfer.Interpreter (prEnv)
|
||||
|
||||
import Control.Monad (when)
|
||||
import Data.List (partition, isPrefixOf)
|
||||
import System.Environment (getArgs)
|
||||
import System.IO (isEOF)
|
||||
|
||||
interpretLoop :: Env -> IO ()
|
||||
interpretLoop env =
|
||||
do
|
||||
eof <- isEOF
|
||||
if eof
|
||||
then return ()
|
||||
else do
|
||||
line <- getLine
|
||||
r <- evaluateString env line
|
||||
putStrLn r
|
||||
interpretLoop env
|
||||
|
||||
runMain :: Env -> IO ()
|
||||
runMain env = do
|
||||
r <- evaluateString env "main"
|
||||
putStrLn r
|
||||
|
||||
main :: IO ()
|
||||
main = do args <- getArgs
|
||||
let (flags,files) = partition ("-" `isPrefixOf`) args
|
||||
env <- case files of
|
||||
[f] -> loadFile f
|
||||
_ -> fail "Usage: trci [-i] <file>"
|
||||
when ("-v" `elem` flags) $ do
|
||||
putStrLn "Top-level environment:"
|
||||
putStrLn (prEnv env)
|
||||
if "-i" `elem` flags
|
||||
then interpretLoop env
|
||||
else runMain env
|
||||
Reference in New Issue
Block a user