Permalink
Browse files

added case ty-rule

  • Loading branch information...
1 parent ec0d569 commit 9e8bd87f0ff25f2d8409ad285cf7b1fe5fe0a1a9 @rubendg rubendg committed Jul 8, 2011
Showing with 4 additions and 5 deletions.
  1. +3 −4 doc/main.tex
  2. +1 −1 src/APA2/AG/Infer.ag
View
@@ -252,13 +252,12 @@ \subsection{Type System}
} \\
~&~\\
$ [$\emph{t-case}$] $& \inference{
- & \Gamma, C |- e_0 : [\tau]^\varphi
- & \sigma = gen(\tau_r)
- & \Gamma[f \mapsto (\sigma, \varphi_r)],C |- e_2 : \tau_2^{\varphi_2}
+ & \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>\ e_2 : \tau_2^{ \varphi_3}
+ \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
@@ -539,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

0 comments on commit 9e8bd87

Please sign in to comment.