Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Comparing changes

Choose two branches to see what's changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
base fork: toothbrush/apa-proj2
base: 728d9ba10d
...
head fork: toothbrush/apa-proj2
compare: b8776d3e6c
Checking mergeability… Don't worry, you can still create the pull request.
  • 6 commits
  • 2 files changed
  • 0 commit comments
  • 1 contributor
Showing with 39 additions and 26 deletions.
  1. +34 −17 doc/main.tex
  2. +5 −9 src/APA2/AG/Infer.ag
View
51 doc/main.tex
@@ -16,7 +16,7 @@
% things for the semantic package
\reservestyle{\command}{\textbf}
-\command{let,in,:,case,of,if,then,else}
+\command{let,in,:,case,of,if,then,else,letrec,nil,cons,false,true,[]}
\mathlig{-->}{\longrightarrow}
\newcommand{\tyrel}{\sqsubseteq}
% end semantic
@@ -165,20 +165,20 @@ \subsection{Type System}
~&~\\
$ [$\emph{t-true}$] $& \inference{}
{
- {\Gamma},C |- True : Bool^{\varphi}
+ {\Gamma},C |- \<true>\ : Bool^{\varphi}
} \\
~&~\\
$ [$\emph{t-false}$] $& \inference{}
{
- {\Gamma},C |- False : Bool^{\varphi}
+ {\Gamma},C |- \<false>\ : Bool^{\varphi}
} \\
~&~\\
$ [$\emph{t-nil}$] $& \inference{
- {\Gamma},C |- Nil : \tau^{\varphi_1}
+ {\Gamma},C |- \<nil>\ : \tau^{\varphi_1}
& C |- \varphi \sqsupseteq \pi
}
{
- {\Gamma},C |- Nil_\pi : [\tau^{\varphi_1}]^{\varphi}
+ {\Gamma},C |- \<nil>_\pi : [\tau^{\varphi_1}]^{\varphi}
} \\
~&~\\
$ [$\emph{t-cons}$] $& \inference{
@@ -188,7 +188,7 @@ \subsection{Type System}
& C |- \varphi \sqsupseteq \pi
}
{
- {\Gamma},C |- Cons_\pi\ e_1\ e_2 : [\tau^{\varphi_1}]^{\varphi}
+ {\Gamma},C |- \<cons>_\pi\ e_1\ e_2 : [\tau^{\varphi_1}]^{\varphi}
} \\
~&~\\
$ [$\emph{t-var}$] $& \inference{
@@ -214,9 +214,8 @@ \subsection{Type System}
\Gamma, C |- e_0 : Bool^{\varphi_0}
& \Gamma, C |- e_1 : \tau^{\varphi_1}
& \Gamma, C |- e_2 : \tau^{\varphi_2}
- & C |- \varphi_0 \tyrel \varphi
- & C |- \varphi_1 \tyrel \varphi
- & C |- \varphi_2 \tyrel \varphi
+ & C |- \varphi \sqsupseteq \varphi_1
+ & C |- \varphi \sqsupseteq \varphi_2
}
{
\Gamma,C|- \<if>\: e_0\: \<then>\: e_1\: \<else>\: e_2 : \tau^{\varphi}
@@ -225,22 +224,40 @@ \subsection{Type System}
$ [$\emph{t-bin-op}$] $& \inference{ % what about all the annotated simple vars?
\Gamma, C |- e_1 : \tau_{1\oplus}^{\varphi_1}
& \Gamma, C |- e_2 : \tau_{2\oplus}^{\varphi_2}
- & C |- \varphi_1 \tyrel \varphi
- & C |- \varphi_2 \tyrel \varphi
+ & C |- \varphi \sqsupseteq \varphi_1
+ & C |- \varphi \sqsupseteq \varphi_2
}
{
\Gamma, C|- e_1 \oplus e_2 : \tau_{\oplus}^\varphi
} \\
~&~\\
-% todo do we need rules for case statements involving head and tail of lists??
$ [$\emph{t-let}$] $& \inference{
- \Gamma, C' |- e_1 : \tau_1^{\varphi_1}
- & (C'',\sigma) = gen(C', \tau_1)
- & \Gamma[x \mapsto (\sigma, \varphi_1)],C\cup C'' |- e_2 : \tau_2^{\varphi_2}
- & C\cup C'' |- \varphi_2 \tyrel \varphi_3
+ \Gamma, C |- e_1 : \tau_1^{\varphi_1}
+ & \sigma = gen(\tau_1)
+ & \Gamma[x \mapsto (\sigma, \varphi_1)],C |- e_2 : \tau_2^{\varphi_2}
+ & C |- \varphi_3 \sqsupseteq \varphi_2
}
{
- \Gamma,C\cup C'' |- \<let>\: x = e_1\: \<in>\: e_2 : \tau_2^{\varphi_3}
+ \Gamma,C |- \<let>\: x = e_1\: \<in>\: e_2 : \tau_2^{\varphi_3}
+ } \\
+~&~\\
+ $ [$\emph{t-letrec}$] $& \inference{
+ & \Gamma[f \mapsto (\tau_x^{\varphi_x} -> \tau_r^{\varphi_r}, \varphi), x \mapsto (\tau_x, \varphi_x)],C |- e_1 : \tau_r^{\varphi_r}
+ & \sigma = gen(\tau_r)
+ & \Gamma[f \mapsto (\sigma, \varphi_r)],C |- e_2 : \tau_2^{\varphi_2}
+ & C |- \varphi_3 \sqsupseteq \varphi_2
+ }
+ {
+ \Gamma,C |- \<letrec>\: f\ x = e_1\: \<in>\: e_2 : \tau_2^{ \varphi_3}
+ } \\
+~&~\\
+ $ [$\emph{t-case}$] $& \inference{
+ & \Gamma, C |- e_0 : [\tau_0]^\varphi
+ & C |- \varphi_3 \sqsupseteq \varphi_1
+ & C |- \varphi_3 \sqsupseteq \varphi_2
+ }
+ {
+ \Gamma,C |- \<case>\:\ e_0\ \<of>\ \{ pat : \tau_0 \hookrightarrow e_1 : \tau_1^{\varphi_1} ; pat : \tau_0 \hookrightarrow e_2 : \tau_1^{\varphi_2} \} : \tau_2^{ \varphi_3}
} \\
~&~\\
% $ [$\emph{t-app}$] $& \inference{
View
14 src/APA2/AG/Infer.ag
@@ -452,11 +452,9 @@ SEM MH
loc.substitution = @loc.theta2 `dot` @loc.theta1
loc.constraints =
- let c1 = @e1.constraints
- c2 = @e2.constraints
- c3 = @loc.betaf' <:? @e2.annotation
- cs = c1 `DS.union` c2 `DS.union` c3
- in applySubst @loc.theta2 cs
+ let cs = @e1.constraints `DS.union` @e2.constraints `DS.union`
+ (@loc.betaf' <:? @e2.annotation)
+ in applySubst @loc.substitution cs
loc.annotation = @loc.betaf'
@@ -505,12 +503,10 @@ SEM MH
loc.theta1 = unify @e1.ty (applySubst @loc.theta0 @loc.alphar')
loc.theta2 = unifyAnn (applySubst @loc.theta1 @e1.annotation) (applySubst @loc.theta1 @loc.betar')
- loc.theta = @loc.theta2 `dot` @loc.theta1 `dot` @loc.theta0
+ loc.substitution = @loc.theta2 `dot` @loc.theta1 `dot` @loc.theta0
loc.ty = @e2.ty
- loc.substitution = @loc.theta
-
loc.constraints =
let cs = @e1.constraints `DS.union` @e2.constraints `DS.union`
(@loc.betaf' <:? @e2.annotation)
@@ -543,7 +539,7 @@ SEM MH
let newEnv = applySubst @loc.substitution @lhs.typeEnvironment
in case @x of
Just _ -> let ty = Arr @loc.alphax' @loc.betax' @e1.ty @e1.annotation
- ty' = applySubst @loc.theta ty
+ ty' = applySubst @loc.substitution ty
genTy = snd $ generalise newEnv @e1.annotation ty' @e1.constraints
in DM.insert @f genTy newEnv
Nothing -> DM.insert @f (QualSig $ Ty @loc.alphar') newEnv -- not sure about this

No commit comments for this range

Something went wrong with that request. Please try again.