Skip to content
Snippets Groups Projects
Commit f71a732a authored by Richard Eisenberg's avatar Richard Eisenberg
Browse files

Typeset relevant rules from TVIP

parent 25cae14e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
grammar.ott
+ 1
− 3
View file @ f71a732a
......@@ -123,7 +123,7 @@ G {{ tex \Gamma }}, Gt {{ tex \Gamma_t }} :: 'TyEnv_' ::= {{ com Type environmen
| tv : type :: :: TyVar {{ com Type variable binding }}
| < tv : type > :: M :: TyVars
{{ tex \overline{ [[tv]] : [[type]] } }}
| ( G ) :: :: Parens {{ com Grouping }}
| ( G ) :: M :: Parens {{ com Grouping }}
{{ tex [[G]] }}
| Giminus_one :: M :: GIHack
......@@ -178,7 +178,6 @@ terminals :: 'terminals_' ::=
| ftv :: :: ftv {{ tex \mathit{ftv}\! }}
| # :: :: fresh {{ tex \mathrel{\#} }}
| @ :: :: at {{ tex \at }}
| isTV :: :: isTV {{ tex \mathit{isInternalTypeVar}\! }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Formulae %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -195,7 +194,6 @@ formula :: formula_ ::=
| obj1 = obj2 :: :: objeq
| < formula > :: :: overline
{{ tex \overline{[[formula]]} }}
| isTV ( t ) :: :: isTV
% | x : t \in G :: :: ctx_in
% {{ tex [[x]] : [[t]] \in [[G]] }}
......
haskell.mng
+ 23
− 1
View file @ f71a732a
......@@ -3,6 +3,7 @@
\usepackage[supertabular,implicitLineBreakHack]{ottalt}
\usepackage[dvipsnames]{xcolor}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{fullpage}
\inputott{ott.tex}
......@@ -14,10 +15,31 @@
\newcommand{\varid}[1]{\textcolor{Sepia}{\id{#1}}}
\renewcommand\ottaltinferrule[4]{
\inferrule*[narrower=0.3,right=#1,#2]
{#3}
{#4}
}
\begin{document}
\section{Metavariables}
\ottmetavars
\section{Grammar}
\nonterms{prog,CL,v,e,p,sg,Q,tv,theta,t,G}
\drules
\section{Typing rules}
\drules[E]{$[[G |- e : t]]$}{Expressions}{VarCon,Eq,App,Abs,Case,Let}
Abstract judgments $[[G ||- Q]]$ denotes entailment and $[[G ||- sg1 <= sg2]]$ denotes
subtyping ($[[sg1]]$ is more general than $[[sg2]]$).
\drules[P]{$[[G |-p p : sg => G']]$}{Patterns}{Var,Con,Syn,Sig}
\drules[Ps]{$[[G |-p* </ pi : sgi // i /> => G']]$}{Pattern sequences}{PatSeq}
\end{document}
rules.ott
+ 37
− 63
View file @ f71a732a
......@@ -9,30 +9,27 @@ by
isTyVar ( a )
defn
G |- e : t :: :: Ty :: '' {{ com Expression typing }}
G |- e : t :: :: Ty :: 'E_' {{ 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
-------------------------- :: VarCon
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)
% (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
G |- e1 : t1 -> t2
G |- e2 : t2
--------------------------------- :: App
G |- e1 e2 : t2
......@@ -40,29 +37,17 @@ 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 |- e : u
ftv(t) (= dom(G)
--------------------------------- :: Case
G |- case e of {</ pi -> ei // i />} : t
G |- e : u // cs = ftv(u)
G, x : forall cs.u |- e2 : t
sg = forall cs. Q => u
ftv(sg) (= dom(G)
G, <c : type>, Q |- e : u
G, x : sg |- 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
......@@ -75,25 +60,18 @@ by
defn
G |-p p : sg => G' :: :: Pat :: 'Pat' {{ com Pattern typing }}
G |-p p : sg => G' :: :: Pat :: 'P_' {{ 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' = 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)
</ 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 />
......@@ -104,29 +82,25 @@ 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)
</ cl // l /> = ftv(</ t'j // j />) \ dom(G)
</ aj // j /> # dom(G)
G' = G,(</ aj : type // j />),(</ cl : type // l />),(</ cl ~ t''l // l />),(</ ui ~ ti // i />),Q
</ G' ||- t'j ~ aj // j /> // </ isTV(t''l) // l />
</ G' ||- t'j ~ aj // j />
G' |-p* </ pk : sgk // k /> => G''
-------------------------------- :: ConTyApp
-------------------------------- :: Con
G |-p K </ @ t'j // j /> </ pk // k /> : T </ ti // i /> => G''
ftv(sg') = emptyset // G ||- sg <= sg' // G |-p p : sg' => G'
cs = ftv(sg') \ dom(G)
G' = G, <c : type>, < c ~ t >
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 ~ t >
< isTV(t) >
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 }}
G |-p* </ pi : sgi // i /> => G' :: :: PatSeq :: 'Ps_' {{ com Pattern squence typing }}
by
% help, how do I typeset that with G_{i-1}
......@@ -135,11 +109,11 @@ by
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
% 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
% G, c : type |-sb* e <= [a |-> c]sg
% --------------------------------- :: SB_DTyAbs
% G |-sb* \ @c . e <= forall a. sg
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment