diff options
| author | aarne <aarne@cs.chalmers.se> | 2008-06-26 21:05:01 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2008-06-26 21:05:01 +0000 |
| commit | fb1d9b7d2c3c8261fc5a2ce3698e6749458b207a (patch) | |
| tree | 466adc81f2c6ac803d20804863927c076e2b243a /transfer | |
| parent | 33eb6d899fef48f2d38a92bc0fab66ff585be553 (diff) | |
removed transfer from gf3
Diffstat (limited to 'transfer')
33 files changed, 0 insertions, 2515 deletions
diff --git a/transfer/Makefile b/transfer/Makefile deleted file mode 100644 index 1ef8da644..000000000 --- a/transfer/Makefile +++ /dev/null @@ -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 diff --git a/transfer/README b/transfer/README deleted file mode 100644 index 5a764ca07..000000000 --- a/transfer/README +++ /dev/null @@ -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" - diff --git a/transfer/TODO b/transfer/TODO deleted file mode 100644 index 6ad3a3428..000000000 --- a/transfer/TODO +++ /dev/null @@ -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 diff --git a/transfer/compile_all.sh b/transfer/compile_all.sh deleted file mode 100644 index d229d4dec..000000000 --- a/transfer/compile_all.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sh - -for f in lib/*.tra examples/*.tra; do - ./transferc -ilib $f; -done diff --git a/transfer/doc/Makefile b/transfer/doc/Makefile deleted file mode 100644 index 02f0bec10..000000000 --- a/transfer/doc/Makefile +++ /dev/null @@ -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 diff --git a/transfer/doc/mathpartir.sty b/transfer/doc/mathpartir.sty deleted file mode 100644 index 549596797..000000000 --- a/transfer/doc/mathpartir.sty +++ /dev/null @@ -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 diff --git a/transfer/doc/typesystem.tex b/transfer/doc/typesystem.tex deleted file mode 100644 index fb26b064c..000000000 --- a/transfer/doc/typesystem.tex +++ /dev/null @@ -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} diff --git a/transfer/examples/aggregation/Abstract.gf b/transfer/examples/aggregation/Abstract.gf deleted file mode 100644 index 9d8b31d0d..000000000 --- a/transfer/examples/aggregation/Abstract.gf +++ /dev/null @@ -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 ; - -} diff --git a/transfer/examples/aggregation/English.gf b/transfer/examples/aggregation/English.gf deleted file mode 100644 index 53199787b..000000000 --- a/transfer/examples/aggregation/English.gf +++ /dev/null @@ -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} ; - -} diff --git a/transfer/examples/aggregation/aggregate.tra b/transfer/examples/aggregation/aggregate.tra deleted file mode 100644 index b71ccfef2..000000000 --- a/transfer/examples/aggregation/aggregate.tra +++ /dev/null @@ -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 --} diff --git a/transfer/examples/aggregation/tree.tra b/transfer/examples/aggregation/tree.tra deleted file mode 100644 index 5515efa21..000000000 --- a/transfer/examples/aggregation/tree.tra +++ /dev/null @@ -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 ; diff --git a/transfer/examples/disjpatt.tra b/transfer/examples/disjpatt.tra deleted file mode 100644 index 740e08a7b..000000000 --- a/transfer/examples/disjpatt.tra +++ /dev/null @@ -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
\ No newline at end of file diff --git a/transfer/examples/exp.tra b/transfer/examples/exp.tra deleted file mode 100644 index e54b82055..000000000 --- a/transfer/examples/exp.tra +++ /dev/null @@ -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)))
\ No newline at end of file diff --git a/transfer/examples/fib.tra b/transfer/examples/fib.tra deleted file mode 100644 index 43e533b1f..000000000 --- a/transfer/examples/fib.tra +++ /dev/null @@ -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)
\ No newline at end of file diff --git a/transfer/examples/layout.tra b/transfer/examples/layout.tra deleted file mode 100644 index 8c2d9aa3f..000000000 --- a/transfer/examples/layout.tra +++ /dev/null @@ -1,9 +0,0 @@ -x : Apa -x = let x = y - in case y of - f -> q - _ -> a - -f = apa - -g = bepa
\ No newline at end of file diff --git a/transfer/examples/list.tra b/transfer/examples/list.tra deleted file mode 100644 index 253c29e02..000000000 --- a/transfer/examples/list.tra +++ /dev/null @@ -1,6 +0,0 @@ -import prelude - -l1 = append ? [1,2,3,5,6] [3] -l2 = 2 :: l1 - -main = rec { x = length ? l2; y = l2} diff --git a/transfer/examples/numerals.tra b/transfer/examples/numerals.tra deleted file mode 100644 index 2c2718130..000000000 --- a/transfer/examples/numerals.tra +++ /dev/null @@ -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) - diff --git a/transfer/examples/reflexive/Abstract.gf b/transfer/examples/reflexive/Abstract.gf deleted file mode 100644 index 0426defdc..000000000 --- a/transfer/examples/reflexive/Abstract.gf +++ /dev/null @@ -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 ; - -} diff --git a/transfer/examples/reflexive/English.gf b/transfer/examples/reflexive/English.gf deleted file mode 100644 index 73fa00e91..000000000 --- a/transfer/examples/reflexive/English.gf +++ /dev/null @@ -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} ; - -} diff --git a/transfer/examples/reflexive/reflexive.tra b/transfer/examples/reflexive/reflexive.tra deleted file mode 100644 index 8d28f0db0..000000000 --- a/transfer/examples/reflexive/reflexive.tra +++ /dev/null @@ -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 - --}
\ No newline at end of file diff --git a/transfer/examples/reflexive/tree.tra b/transfer/examples/reflexive/tree.tra deleted file mode 100644 index 7bef5e019..000000000 --- a/transfer/examples/reflexive/tree.tra +++ /dev/null @@ -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 ; diff --git a/transfer/examples/stoneage.tra b/transfer/examples/stoneage.tra deleted file mode 100644 index e48c519e6..000000000 --- a/transfer/examples/stoneage.tra +++ /dev/null @@ -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
\ No newline at end of file diff --git a/transfer/examples/test.tra b/transfer/examples/test.tra deleted file mode 100644 index bfd303ee5..000000000 --- a/transfer/examples/test.tra +++ /dev/null @@ -1,4 +0,0 @@ -import nat -import fib - -main = (\x -> (\x -> \x -> x) 1 x) 5 diff --git a/transfer/examples/tricky-type-checking.tra b/transfer/examples/tricky-type-checking.tra deleted file mode 100644 index ad69c33db..000000000 --- a/transfer/examples/tricky-type-checking.tra +++ /dev/null @@ -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 diff --git a/transfer/examples/widesnake.tra b/transfer/examples/widesnake.tra deleted file mode 100644 index f68ed9013..000000000 --- a/transfer/examples/widesnake.tra +++ /dev/null @@ -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 diff --git a/transfer/lib/bintree.tra b/transfer/lib/bintree.tra deleted file mode 100644 index 0dd21f184..000000000 --- a/transfer/lib/bintree.tra +++ /dev/null @@ -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 - diff --git a/transfer/lib/bool.tra b/transfer/lib/bool.tra deleted file mode 100644 index 2639422b7..000000000 --- a/transfer/lib/bool.tra +++ /dev/null @@ -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 - diff --git a/transfer/lib/collection.tra b/transfer/lib/collection.tra deleted file mode 100644 index 59b71a5e9..000000000 --- a/transfer/lib/collection.tra +++ /dev/null @@ -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 - -- ... diff --git a/transfer/lib/nat.tra b/transfer/lib/nat.tra deleted file mode 100644 index b13a809ed..000000000 --- a/transfer/lib/nat.tra +++ /dev/null @@ -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)) diff --git a/transfer/lib/prelude.tra b/transfer/lib/prelude.tra deleted file mode 100644 index 054058db4..000000000 --- a/transfer/lib/prelude.tra +++ /dev/null @@ -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) --} - diff --git a/transfer/lib/vector.tra b/transfer/lib/vector.tra deleted file mode 100644 index 2eda35167..000000000 --- a/transfer/lib/vector.tra +++ /dev/null @@ -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) diff --git a/transfer/transferc.hs b/transfer/transferc.hs deleted file mode 100644 index 7a88d8e3a..000000000 --- a/transfer/transferc.hs +++ /dev/null @@ -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>" diff --git a/transfer/trci.hs b/transfer/trci.hs deleted file mode 100644 index 3cfd02bd6..000000000 --- a/transfer/trci.hs +++ /dev/null @@ -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 |