Type variables in patterns – figure source code

.gitignore

tyvars-in-pats-haskell18.pdf
tyvars-in-pats-haskell18-*.pdf

## Richard's ott setup
tyvars-in-pats-haskell18.tex
tyvars-in-pats-haskell18-*.tex
tyvars-in-pats-haskell18.lhs
tyvars-in-pats-haskell18.hs
ott.tex
ottdump.pdf

## Core latex/pdflatex auxiliary files:
*.aux
*.lof
*.log
*.lot
*.fls
*.out
*.toc
*.ptb
*.fot
*.cb
*.cb2
.*.lb

## Intermediate documents:
*.dvi
*.xdv
*-converted-to.*
# these rules might exclude image files for figures etc.
# *.ps
# *.eps
# *.pdf

## Generated if empty string is given at "Please type another file name for output:"
.pdf

## Bibliography auxiliary files (bibtex/biblatex/biber):
*.bbl
*.bcf
*.blg
*-blx.aux
*-blx.bib
*.run.xml

## Build tool auxiliary files:
*.fdb_latexmk
*.synctex
*.synctex(busy)
*.synctex.gz
*.synctex.gz(busy)
*.pdfsync

## Auxiliary and intermediate files from other packages:
# algorithms
*.alg
*.loa
*.cut

# achemso
acs-*.bib

# amsthm
*.thm

# beamer
*.nav
*.pre
*.snm
*.vrb

# changes
*.soc

# cprotect
*.cpt

# elsarticle (documentclass of Elsevier journals)
*.spl

# endnotes
*.ent

# fixme
*.lox

# feynmf/feynmp
*.mf
*.mp
*.t[1-9]
*.t[1-9][0-9]
*.tfm

#(r)(e)ledmac/(r)(e)ledpar
*.end
*.?end
*.[1-9]
*.[1-9][0-9]
*.[1-9][0-9][0-9]
*.[1-9]R
*.[1-9][0-9]R
*.[1-9][0-9][0-9]R
*.eledsec[1-9]
*.eledsec[1-9]R
*.eledsec[1-9][0-9]
*.eledsec[1-9][0-9]R
*.eledsec[1-9][0-9][0-9]
*.eledsec[1-9][0-9][0-9]R

# glossaries
*.acn
*.acr
*.glg
*.glo
*.gls
*.glsdefs

# gnuplottex
*-gnuplottex-*

# gregoriotex
*.gaux
*.gtex

# htlatex
*.4ct
*.4tc
*.idv
*.lg
*.trc
*.xref

# hyperref
*.brf

# knitr
*-concordance.tex
# TODO Comment the next line if you want to keep your tikz graphics files
*.tikz
*-tikzDictionary

# listings
*.lol

# makeidx
*.idx
*.ilg
*.ind
*.ist

# minitoc
*.maf
*.mlf
*.mlt
*.mtc[0-9]*
*.slf[0-9]*
*.slt[0-9]*
*.stc[0-9]*

# minted
_minted*
*.pyg

# morewrites
*.mw

# nomencl
*.nlg
*.nlo
*.nls

# pax
*.pax

# pdfpcnotes
*.pdfpc

# sagetex
*.sagetex.sage
*.sagetex.py
*.sagetex.scmd

# scrwfile
*.wrt

# sympy
*.sout
*.sympy
sympy-plots-for-*.tex/

# pdfcomment
*.upa
*.upb

# pythontex
*.pytxcode
pythontex-files-*/

# thmtools
*.loe

# TikZ & PGF
*.dpth
*.md5
*.auxlock

# todonotes
*.tdo

# easy-todo
*.lod

# xmpincl
*.xmpi

# xindy
*.xdy

# xypic precompiled matrices
*.xyc

# endfloat
*.ttt
*.fff

# Latexian
TSWLatexianTemp*

## Editors:
# WinEdt
*.bak
*.sav

# Texpad
.texpadtmp

# Kile
*.backup

# KBibTeX
*~[0-9]*

# auto folder when using emacs and auctex
./auto/*
*.el

# expex forward references with \gathertags
*-tags.tex

# standalone packages
*.sta

# Haskell
*.hi
*.o

grammar.ott

%% The Stitch language

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Metavariables  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

metavar x, y, z, f, g, h::= {{ com Term variables }}
metavar a, b ::=            {{ com Type varaibles (internal) }}
metavar c ::=               {{ com Type variables (user-specified) }}
metavar K {{ tex \mathrm K }}  ::= {{ com Data constructors }}
metavar P {{ tex \mathrm P }}  ::= {{ com Pattern synonyms }}
metavar T {{ tex \mathrm T }}  ::= {{ com Type constructors }}
indexvar i, j, k, l, n ::=  {{ com Index variables }}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Grammar  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

grammar

prog :: 'Prog_' ::= {{ com Programs }}
| empty                   ::  :: Empty
| f = e , prog            ::  :: Bind
| f '::' sg '=' e , prog  ::  :: TypedBind

v {{ tex \nu }} :: 'Atom_' ::= {{ com Atoms }}
| x       :: :: Var
| K       :: :: DataCon

e :: 'Expr_' ::= {{ com Expressions }}
| v       :: :: Atom
| P       :: :: PatSyn
| \ x . e :: :: Lam
| \ @ c . e :: :: TyLam
| e1 e2   :: :: App
| case e of { alts } :: :: Case
| ( e )   :: M :: Parens
| let  x '::' sg  = e1 in e2  ::  :: Let
  {{ tex \keyword{let}\ [[x]] [[::]] [[sg]] = [[e1]]\ \keyword{in}\ [[e2]] }}

alts {{ tex \overline{\ottnt{p} \to \ottnt{e} } }} :: 'Alts_' ::= {{ com Case alternatives }}
| </ pi -> ei // i /> :: :: Patterns

p :: 'Pat_' ::= {{ com Patterns }}
| _               :: :: Underscore
| x               :: :: Var
| p '::' sg       :: :: Sig
| K ps            :: :: DataCon
| K atts ps       :: :: DataConWithTyApp
| P atts ps       :: :: PatSyn
| ( p )                       :: M :: Parens

ps {{ tex \overline{\ottnt{p} } }} :: 'Pats_' ::= {{ com Lists of patterns }}
| </ pi // i />   :: :: List

atts {{ tex \overline{\at \tau} }} :: 'AtTypes_' ::= {{ com Lists of visible type patterns }}
| @ t1 ... @ ti   ::  :: List

sg {{ tex \sigma }} :: 'SigTy_' ::= {{ com Type schemes }}
| forall as . Q => sg ::   :: ForallQTy
  {{ tex [[forall]] [[as]].\,[[Q]] [[=>]] [[sg]] }}
| forall as . sg      :: M :: ForallTy
  {{ tex [[forall]] [[as]].\,[[sg]] }}
| t                             ::   :: MonoTy
| [ </ ai |-> ti // i /> ] sg   :: M :: Subst
| theta ( sg )                  :: M :: SubstVar

tvs {{ tex \overline{\ottnt{tv} } }}, as {{ tex \overline{\ottmv{a} } }}, bs {{ tex \overline{\ottmv{b} } }}, cs {{ tex \overline{\ottmv{c} } }} :: 'Vars_' ::= {{ com Lists of variables }}
| </ ai // i />   :: :: List
| </ ci // i />   :: :: UserList
| as bs           :: :: Concat

Q, Qr {{ tex Q_r }}, Qp {{ tex Q_p }} :: 'Constraint_' ::= {{ com Constraints }}
| empty                      ::  :: Empty
| Q1 /\ Q2                   ::  :: Conj
| t1 ~ t2                  ::  :: Eq
| [ </ ai |-> ti // i /> ] Q :: M :: Subst
| theta Q                  :: M :: SubstVar
  {{ tex [[theta]] [[Q]] }}
| ( Q )                     :: M :: Parens
| < Q >                     :: M :: Many
  {{ tex \overline{[[Q]]} }}

tv :: 'TyVar_' ::= {{ com Any type variable }}
| a                          ::   :: Var
| c                          ::   :: ExplVar

theta {{ tex \theta }} :: 'Subst_' ::= {{ com Type substitution }}
| [ </ tvi |-> ti // i /> ]   :: :: SubstList
| [< tv |-> t >]              :: :: Overline
  {{ tex [\overline{[[tv]] [[|->]] [[t]]}] }}
| theta1 theta2              :: :: Concat

t {{ tex \tau }}, u {{ tex \upsilon }} :: 'Ty_' ::= {{ com Monotypes }}
| a                              ::   :: Var
| c                              ::   :: ExplVar
| sg -> t                        ::   :: Fun
| sgs -> t                       :: M :: Funs
| T ts                           ::   :: ConApp
| theta t                        :: M :: Subst
  {{ tex [[theta]] [[t]] }}
| ( t )                          :: M :: Parens
| Int                            :: M :: Int
  {{ tex \conid{Int} }}

ts {{ tex \overline{\tau} }} :: 'Tys_' ::= {{ com Lists of monotypes }}
| </ ti // i />               :: :: List
| as                          :: :: Vars

sgs {{ tex \overline{\sigma} }} :: 'Sigmas_' ::= {{ com Lists of polytypes }}
| </ sgi // , // i />              ::  :: List

G {{ tex \Gamma }} :: 'TyEnv_' ::= {{ com Type environments }}
| G1 , .. , Gn                 :: :: Empty
| v : sg                       :: :: Var
| P : sg                       :: :: PatSyn
| Q                            :: :: Constraint
| tv : type                    :: :: TyVar
| < tv : type >                :: :: TyVars
  {{ tex \overline{ [[tv]] : [[type]] } }}
| ( G )                        :: MS :: Parens {{ tex [[G]] }}
| Giminus_one                  :: M  :: GIHack

kbind :: 'KBind_' ::= {{ com Data constructor binding }}
| K : sg                 :: :: DataCon

obj :: 'SynObj' ::= {{ com Syntactic object }}
| sgs :: :: TypeScheme
| Q  :: :: Constraint
| G  :: :: Context

% This is less typed that it could be
tvexpr :: 'TyVarExpr_' ::= {{ com Type variable set expressions }}
| emptyset                  :: :: Emptyset
| ftv ( obj ) :: :: FTV {{ com Free type variables }}
| dom( G )                     :: :: CtxtDmo
  {{ tex \mathit{dom} ([[G]]) }}
| tvexpr \ tvexpr'    :: :: subtract
  {{ tex [[tvexpr]] \mathop{\backslash} [[tvexpr']] }}
| as                        :: :: VarListNoBraces

tvrel  :: 'TyVarRel_' ::= {{ com Type variable set relation }}
| tvexpr (= tvexpr'         :: :: subset
| tvexpr = tvexpr'         :: :: eq
| tvexpr # tvexpr'              :: :: fresh


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Terminals  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

terminals :: 'terminals_' ::=
| \                              ::   :: Lam        {{ tex \lambda }}
| ->                             ::   :: Arrow      {{ tex \to }}
| =>                             ::   :: ThickArrow {{ tex \Rightarrow }}
| <=                             ::   :: LE         {{ tex \le }}
| |->                            ::   :: Mapsto     {{ tex \mapsto }}
| empty                          ::   :: empty      {{ tex \epsilon }}
| emptyset                       ::   :: emptyset   {{ tex \emptyset }}
| forall                         ::   :: Forall     {{ tex \forall }}
| /\                             ::   :: And        {{ tex \wedge }}
| ~                              ::   :: Eq         {{ tex \sim }}
| |-                             ::   :: VDash1     {{ tex \vdash }}
| ||-                            ::   :: VDash2     {{ tex \Vdash }}
| |-p                            ::   :: VDashp     {{ tex \vdash_{\!\mathsf p} }}
| |-p*                           ::   :: VDashpstar {{ tex \vdash_{\!\mathsf p}^{\!\ast} }}
| |-sb*                          ::   :: VDashsbstar {{ tex \vdash_{\!\mathsf sb}^{\!\ast} }}
| :=                             ::   :: Def        {{ tex \coloneqq }}
| in                             ::   :: In         {{ tex \in }}
| '//'                           ::   :: spacer     {{ tex \; }}
| type                           ::   :: type       {{ tex \ast }}
| (=                             ::   :: subseteq   {{ tex \subseteq }}
| without                        ::   :: setminus   {{ tex \setminus }}
| Giminus_one                    ::   :: Giminus_one {{ tex \Gamma_{i-1} }}
| ftv                            ::   :: ftv        {{ tex \mathit{ftv}\! }}
| #                              ::   :: fresh      {{ tex \mathrel{\#} }}
| @                              ::   :: at         {{ tex \at }}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

formula :: formula_ ::=
|  judgement                       ::   :: judgement
|  formula1 '//' .. '//' formulan            ::   :: dots
|  ( v : sg ) in G                   ::   :: ctxtlookup
|  ( P : sg ) in G                   ::   :: patsynlookup
|  theta1 = theta2                   ::   :: substdef
|  G = G'                           ::   :: ctxtdef
|  tvrel                             ::   :: tvrel
|  obj1 = obj2                       ::   :: objeq

% | x : t \in G                      ::   :: ctx_in
%   {{ tex [[x]] : [[t]] \in [[G]] }}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Defined functions  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% funs
% Util ::=
%
% fun
% result ( op ) :: t :: arith_result
%   {{ tex [[result]]([[op]]) }}
%
% by
% result(+) === Int
% result(-) === Int
% result(*) === Int
% result(/) === Int
% result(\%) === Int
% result(>) === Bool
% result(>=) === Bool
% result(<) === Bool
% result(<=) === Bool
% result(==) === Bool
%
% fun
% e1 [ e2 / x ] :: e :: theta
%
% by

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Subrules  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

subrules

tv <:: t

Makefile

PAPER = tyvars-in-pats-haskell18

TEX_FILES =

GHC = ghc

OTT_FILES = grammar.ott rules.ott
OTT_OPTS = -tex_show_meta false -tex_wrap false -picky_multiple_parses false
OTT_TEX = ott.tex

BIB_FILES =
FMT_FILES = rae.fmt

GHC_OPTIONS = -dcore-lint -Wall

all: ott

#all: $(PAPER).pdf $(PAPER)-submission.pdf $(PAPER)-preprint.pdf $(PAPER)-body.pdf $(PAPER)-appendix.pdf

ott: ottdump.pdf


%.lhs: %.mng $(OTT_FILES)
	rm -f $@
	ott $(OTT_OPTS) -tex_filter $< $@ $(OTT_FILES)
	chmod -w $@

%.tex: %.lhs $(FMT_FILES)
	rm -f $@
	lhs2TeX -o $@ $<
	chmod -w $@

$(PAPER)-submission.tex: $(PAPER).lhs
$(PAPER)-preprint.tex: $(PAPER).lhs

$(PAPER)-body.pdf: $(PAPER)-submission.pdf
	pdftk $< cat 1-12 output $@

$(PAPER)-appendix.pdf: $(PAPER)-submission.pdf
	pdftk $< cat 13-END output $@

%.pdf: %.tex $(BIB_FILES) $(OTT_TEX)
	latexmk -pdf -interaction=nonstopmode -halt-on-error $<

%.o: %.hs
	$(GHC) $(GHC_OPTIONS) -c $<

%.hs: %.lhs $(FMT_FILES)
	rm -f $@
	lhs2TeX --newcode -o $@ $<
	chmod -w $@

ott.tex: $(OTT_FILES)
	rm -f $@
	ott $(OTT_OPTS) -o $@ $^
	chmod -w $@

code: $(PAPER).o

clean:
	rm -f *.aux *.log *.bbl *.blg *.ptb *~
	rm -f *.fdb_latexmk *.fls *.out
	rm -f comment.cut *.o *.hi
	rm -f $(PAPER).tex $(PAPER).pdf $(OTT_TEX) $(PAPER).hs $(PAPER).lhs ottdump.pdf

.PHONY: all ott clean code
.SECONDARY:

ottdump.tex

\documentclass{article}

\usepackage[dvipsnames]{xcolor}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{mathtools}
\usepackage{supertabular}

\newcommand{\syntaxcolor}[2]{\textcolor{#1}{#2}}
\newcommand{\keyword}[1]{\syntaxcolor{BlueViolet}{\textbf{#1}}}
\newcommand{\id}[1]{\textsf{\textsl{#1}}}
\newcommand{\varid}[1]{\syntaxcolor{Sepia}{\id{#1}}}
\newcommand{\conid}[1]{\syntaxcolor{OliveGreen}{\id{#1}}}
\newcommand{\tick}{\text{\textquoteright}}
\newcommand{\at}{@}

\title{Type variables in patterns}

\input{ott}

\renewcommand{\ottusedrule}[1]{\[#1\]\vspace{1ex}}

\begin{document}

\ottall

\end{document}

rae.fmt

%include polycode.fmt

%format (at x) = "@" x

%if style == poly
%format ! = "\mathop{}\tick"
%format nil = "\tick" []
%format !: = "\mathop{\tick{:}}"
%format !:~> = "\mathop{\tick{{:}{\rightsquigarrow}}}"
%format !-> = "\mathop{\tick{\to}}"
%format !=> = "\mathop{\tick{\Rightarrow}}"
%format !++ = "\mathop{\tick{" ++ "}}"
%format :~> = "\mathop{{:}{\rightsquigarrow}}"
%format :~: = "\mathop{{:}{\sim}{:}}"
%format :~~: = "\mathop{{:}{\approx}{:}}"
%subst conid a = "\conid{" a "}"
%subst varid a = "\varid{" a "}"
%subst keyword a = "\keyword{" a "}"
%format ^^ = "\;"
%format ^^^ = "\,"
%format ## = "\!"
%format (FromNat x) = x
%format BOX = "\square"
%format ~ = "\,\sim\,"
%format qquad = "\qquad"
%format com = "\text{-}\text{-}"
%format bang = "!"
%format family = "\keyword{family}"
%format pattern = "\keyword{pattern}"
%format COMPLETE = "\keyword{complete}"
%format RULES = "\keyword{rules}"
%format NOINLINE = "\keyword{noinline}"
%format LANGUAGE = "\keyword{language}"
%format /~ = "\not\sim"
%format * = "\star"
%format \* = "*"
%format =-> = "\mapsto"
%format dollar = $
%format ~> = "\twoheadrightarrow"
%format th_d_open = "[\id{d}|\;"
%format th_d_close = |]
   % the above one is unnecessary, but included for completeness
%format ghci = "\lambda\!"
%format /\ = "\Lambda"
%format |> = "\triangleright"
%format pi = "\Pi"
%format tau = "\tau"
%format taus = "\overline\tau"
%format upsilon = "\upsilon"
%format upsilons = "\overline\upsilon"
%format sigma = "\sigma"
%format alpha = "\alpha"
%format alphas = "\overline\alpha"
%format beta = "\beta"
%format <$> = "\mathop{{\langle}{\$}{\rangle}}"
%format <*> = "\mathop{{\langle}{*}{\rangle}}"
%format ^ = "\string^"
%format bottom = "\bot"
%format prag_begin = "\{-{\#}"
%format prag_end = "{\#}{-}\}"
%format k1
%format k2

% suppress some built-in formatting of lhs2TeX:
%format not = "\varid{not}"
%format == = "\mathop{==}"
%format /= = "\mathop{{/}{=}}"
%format && = "\mathop{\&\&}"
%format undefined = "\varid{undefined}"

%else
%format KK = k
%format ^^ =
%format ^^^ =
%format ## =
%format qquad =
%format com = --
%format \* = *
%format ! = "TICK "
%format !: = TICK :
%format !:~> = TICK :~>
%format nil = TICK []
%format dollar = $
%format begin_comment = "{-"
%format end_comment = "-}"
%format th_d_open = "[d|"
%format prag_begin = "{-#"
%format prag_end = "#-}"
%format ... = "undefined"
%endif

%if False
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% forall.fmt
%
% *EXPERIMENTAL*
% Semi-automatic formatting of the . as either function
% composition (normally) or a period (when used after a
% forall).
%
% Permission is granted to include this file (or parts of this file) 
% literally into other documents, regardless of the conditions or 
% license applying to these documents.
%
% Andres Loeh, November 2005, ver 1.1
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%endif
%if not lhs2tex_forall_fmt_read
%let lhs2tex_forall_fmt_read = True
%include lhs2TeX.fmt
%
%if style /= newcode
%
% First, let's redefine the forall, and the dot.
%
%format forall    = forall_ "\hsforall "
%format exists    = exists_ "\hsexists "
%format .         = "\hsdot{" `comp_` "}{" period_ "}"
%format `comp_`   = "\circ "
%format period_   = ".\,"
%format forall_   = "\keyword{$\forall$}\!\! "
%format exists_   = "\keyword{$\exists$}\!\! "
%
% This is made in such a way that after a forall, the next
% dot will be printed as a period, otherwise the formatting
% of `comp_` is used. By redefining `comp_`, as suitable
% composition operator can be chosen. Similarly, period_
% is used for the period.
%
\ReadOnlyOnce{forall.fmt}%
\makeatletter

% The HaskellResetHook is a list to which things can
% be added that reset the Haskell state to the beginning.
% This is to recover from states where the hacked intelligence
% is not sufficient.

\let\HaskellResetHook\empty
\newcommand*{\AtHaskellReset}[1]{%
  \g@@addto@@macro\HaskellResetHook{#1}}
\newcommand*{\HaskellReset}{\HaskellResetHook}

\global\let\hsforallread\empty
\global\let\hsexistsread\empty

\newcommand\hsforall{\global\let\hsdot=\hsperiodonce}
\newcommand\hsexists{\global\let\hsdot=\hsperiodonce}
\newcommand*\hsperiodonce[2]{#2\global\let\hsdot=\hscompose}
\newcommand*\hscompose[2]{#1}

\AtHaskellReset{\global\let\hsdot=\hscompose}

% In the beginning, we should reset Haskell once.
\HaskellReset

\makeatother
\EndFmtInput
%endif
%endif

rules.ott

defns
Ty :: '' ::=

defn
isTyVar ( t ) :: :: IsTyVar :: '' {{ com Type variable check }}
by

----------- :: IsTyVar
isTyVar ( a )

defn
G |- e : t :: :: Ty :: '' {{ com Expression typing }}
by

(v : forall tvs . u) in G
------------ :: VarCon
G |- v : [<tv |-> t>]u

(v : forall as . Q => u) in G
G ||- [< a |-> t >]Q
-------------------------- :: VarConQ
G |- v : [< a |-> t >] u

(P : forall as. Qr => forall bs. Qp => u) in G
theta = [< a |-> t >][< b |-> t' >]
G ||- theta(Qr /\ Qp)
------------------------ :: Syn
G |- P : theta(u)

G |- e : t1
G ||- t1 ~ t2
--------------------------------- :: Eq
G |- e : t2

G |- e1 : t1 -> t2 //   G |- e2 : t2
--------------------------------- :: App
G |- e1 e2 : t2

G, (x : t1) |- e : t2
--------------------------------- :: Abs
G |- \x.e : t1 -> t2

G |- e : u  //  </ G |-p pi : u => Gi'  // Gi' |- ei : t // i />
--------------------------------- :: Case
G |- case e of {</ pi -> ei // i />} : t

</ G |-p pi : u => Gi'  // Gi' |- ei : t // i />
G |- e : u  //  ftv(t) (= dom(G)
--------------------------------- :: CaseTv
G |- case e of {</ pi -> ei // i />} : t

G |- e : u // cs = ftv(u)
G, x : forall cs.u |- e2 : t
----------------------------- :: Let
G |- let x :: u = e in e2 : t

G, <a : type> |- e : [<c |-> a>]u
cs = ftv(u)      // as # dom(G)
G, x : forall cs.u |- e2 : t
----------------------------- :: LetTv
G |- let x :: u = e in e2 : t

sg = forall cs. Q => u  // ftv(sg) (= dom(G)
G, <c : type>, Q  |- e : u  // G, x : sg |- e2 : t
----------------------------- :: LetForall
G |- let x :: sg = e in e2 : t

defn
G ||- Q'         :: :: ConImpl :: 'ConImpl_' {{ com Constraint implication }}
by

defn
G ||- sg <= sg'  :: :: Subtype :: 'SubType_' {{ com Subtyping relation}}
by


defn
G |-p p : sg => G' :: :: Pat :: 'Pat' {{ com Pattern typing }}
by

-------------------------------- :: Var
G |-p x : sg => G, (x : sg)

(K : forall </ ai // i /> . </ sgk // k /> -> T </ ai // i />) in G     //      G |-p* </ pk : [</ ai |-> ti // i />]sgk // k /> => G'
-------------------------------- :: Con98
G |-p K </ pk // k /> : T </ ti // i /> => G'

(K : forall as. Q  => </ sgi // i /> -> T </ uj // j />) in G   // as # dom(G)
G, < a : type >, (</ uj ~ tj // j />), Q |-p* </ pi : sgi // i /> => G'
-------------------------------- :: Con
G |-p K </ pi // i /> : T </ tj // j /> => G'

(P : forall </ ai // i />. Qr => forall </ bj // j />. Qp => </ sgk // k /> -> u) in G
G' = G, (</ ai : type // i />), (</ ai ~ u'i // i />)  // </ ai // i /> # dom(G)
G' ||- (u ~ t) /\ Qr
</ cl // l /> = ftv(</ t'i // i />,</ t''j // j />) \ dom(G)  // </ bj // j /> # dom(G)
G'' = G',(</ bj : type // j />),(</ cl : type // l />),(</ cl ~ b'l // l />),Qp
</ G'' ||- t'i ~ ai // i />
</ G'' ||- t''j ~ bj // j />
G'' |-p* </ pk : theta(sgk) // k /> => G'''
-------------------------------- :: Syn
G |-p P </ @ t'i // i /> </ @ t''j // j /> </ pk // k /> : t => G'''



(K : forall </ aj // j /> . Q  => </ sgk // k /> -> T </ ui // i />) in G
</ cl // l /> = ftv(</ t'j // j />) \ dom(G)  //  </ aj // j /> # dom(G)
G' = G,(</ aj : type // j />),(</ cl : type // l />),(</ cl ~ bl // l />),(</ ui ~ ti // i />),Q
</ G' ||- t'j ~ aj // j />
G' |-p* </ pk : sgk // k /> => G''
-------------------------------- :: ConTyApp
G |-p K </ @ t'j // j /> </ pk // k /> : T </ ti // i /> => G''



ftv(sg') = emptyset //  G ||- sg <= sg'  //  G |-p p : sg' => G'
-------------------------------- :: Sig
G |-p (p :: sg') : sg => G'

cs = ftv(sg') \ dom(G)  //  G' = G, <c : type>, < c ~ b >
G' ||- sg <= sg'  //  G' |-p p : sg' => G''
-------------------------------- :: SigTv
G |-p (p :: sg') : sg => G''



defn
G |-p* </ pi : sgi // i />  => G' :: :: PatSeq :: '' {{ com Pattern squence typing }}
by

% help, how do I typeset that with G_{i-1}
</ Giminus_one |-p  pi : sgi => Gi  // i IN 1 .. n />
----------------------------- :: PatSeq
G0 |-p*  </ pi : sgi // i IN 1 .. n />  => Gn


defn
G |-sb* e <= sg :: :: Check :: '' {{ com Checking against specified polytypes }}
  {{ tex [[G]] [[|-sb*]] [[e]] \Leftarrow [[sg]] }}
by

G, c : type |-sb* e <= [a |-> c]sg
--------------------------------- :: SB_DTyAbs
G |-sb* \ @c . e <= forall a. sg