Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Merge branch 'master' of github.com:toothbrush/apa-proj2

  • Loading branch information...
commit 1fb2a9fb484a3e6fd485e8863ce414288b660bcf 2 parents 3dbb5c6 + 553f089
Ruben de Gooijer rubendg authored
8 doc/main.tex
View
@@ -247,9 +247,11 @@ \subsection{Type System}
} \\
~&~\\
$ [$\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}
+ & \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
}
{
42 src/APA2/AG/DataTypes.ag
View
@@ -129,8 +129,9 @@ tyAnn :: (Show a1, Show a) => a -> a1 -> [Char]
tyAnn t a = "(" ++ show t ++ (colonOpt $ show a) ++ ")"
tyAnnCont :: Show a => Map AnnVar SAnn -> a -> AnnVar -> [Char]
-tyAnnCont con t a = "(" ++ show t ++ (colonOpt $ a `from` con)
+tyAnnCont con t a = "" ++ show t ++ (colonOpt $ a `from` con) ++ ""
+colonOpt :: String -> String
colonOpt [] = ""
colonOpt xs = " : " ++ xs
@@ -140,18 +141,20 @@ instance Show SAnn where
show (AnnEmpty) = "" -- really "{}"
instance Show Ty where
- show (TyVar a) = a
- show (Arr t a t' a') = tyAnn t a ++ " ➔ " ++ tyAnn t' a'
- show Nat = "Nat"
- show Bool = "Bool"
- show (List t an) = "(List " ++ show t ++ ") " ++ (colonOpt $ show an)
+ show = tyLayout DM.empty
tyLayout :: Map AnnVar SAnn -> Ty -> String
-tyLayout _ (TyVar a) = a -- we probably don't want to see this here.
-tyLayout con (Arr t a t' a') = tyAnnCont con t ((fromSAnn a) `from` con) ++ " ➔ " ++ tyAnnCont con t' ((fromSAnn a') `from` con)
+tyLayout _ (TyVar a) = a
+tyLayout con (Arr t@(TyVar _) a t'@(TyVar _) a') = tyAnnCont con t ((fromSAnn a) `from` con) ++ " ➔ " ++ tyAnnCont con t' ((fromSAnn a') `from` con)
+tyLayout con (Arr t@(TyVar _) a t' a') = tyAnnCont con t ((fromSAnn a) `from` con) ++ " ➔ (" ++ tyAnnCont con t' ((fromSAnn a') `from` con) ++ ")"
+tyLayout con (Arr t a t'@(TyVar _) a') = "(" ++ tyAnnCont con t ((fromSAnn a) `from` con) ++ ") ➔ " ++ tyAnnCont con t' ((fromSAnn a') `from` con)
+tyLayout con (Arr t a t' a') = "(" ++ tyAnnCont con t ((fromSAnn a) `from` con) ++ ") ➔ (" ++ tyAnnCont con t' ((fromSAnn a') `from` con) ++ ")"
tyLayout _ Nat = "Nat"
tyLayout _ Bool = "Bool"
-tyLayout con (List t an) = "((List " ++ tyLayout con t ++ ") " ++ (colonOpt $ (fromSAnn an) `from` con) ++ ")"
+tyLayout con (List t an) = "List " ++ case t of
+ TyVar _ -> inner
+ _ -> "(" ++ inner ++ ")"
+ where inner = tyLayout con t ++ "" ++ (colonOpt $ fromSAnn an `from` con)
from :: AnnVar -> Map AnnVar SAnn -> String
from ann con = show $ DM.findWithDefault (AnnVar ann) ann con
@@ -179,25 +182,4 @@ ppMap :: (Show b) => Map String b -> String
ppMap x = let f (a, b) = a ++ " == " ++ show b
l = map f $ M.toList x
in "{\n" ++ intercalate "\n" l ++ "\n}"
-
-{-
-instance Show Ty where
- show (TyVar a) = "TyVar \"" ++ a ++ "\""
- show (Arr t a t' a') = "Arr ("++show t++") ("++show a++") ("++show t'++") ("++show a'++")"
- show Nat = "Nat"
- show Bool = "Bool"
- show (List t an) = "List (" ++ show t ++ ") (" ++ show an ++ ")"
-
-instance Show SAnn where
- show (AnnVar var) = "AnnVar (\""++var++"\")"
- show (AnnSet ps) = "{" ++ intercalate ", " (toList ps) ++ "}"
- show (AnnEmpty) = "{}"
-
-instance Show SimpleSubstitution where
- show Identity = "Identity"
- show (TySub v t) = "TySub (\"" ++ v ++ "\") (" ++ show t ++ ")"
- show (AnnSub a a') = "AnnSub (" ++ show a ++ ") (" ++ show a' ++ ")"
- show (Dot s s') = "Dot (" ++ show s ++ ") (" ++ show s' ++ ")"
--}
-
}
4 src/APA2/AG/Infer.ag
View
@@ -73,6 +73,7 @@ SEM MH
lhs.expressions = [(@loc.ty,@copy)]
| Nil
+ lhs.annotDict = DM.singleton ("L" ++ show @loc.ppoint) @loc.copy
loc.alpha : UNIQUEREF counter
loc.betaf1 : UNIQUEREF counter
loc.betaf2 : UNIQUEREF counter
@@ -113,6 +114,9 @@ SEM MH
loc.betaf1' = freshAnnVar @loc.betaf1
loc.betaf2' = freshAnnVar @loc.betaf2
+ lhs.annotDict = DM.singleton ("L" ++ show @loc.ppoint) @loc.copy
+ `DM.union` @e1.annotDict
+ `DM.union` @e2.annotDict
loc.pi = mkProgramPoint "L" @loc.ppoint
loc.listTy = List @e1.ty @e1.annotation
2  src/Components.hs
View
@@ -82,7 +82,7 @@ analysisResult tm =
putStrLn "Type of full program:\n"
let solved = worklist constraints
let ty' = applySubst (solutionSubst constraints) (applySubst subst ty)
- putStrLn $ ("("++ tyLayout solved ty' ++ ") :::: " ++ ((fromSAnn annotation) `from` solved))
+ putStrLn (tyLayout solved ty' ++ " :::: " ++ (fromSAnn annotation `from` solved))
putStrLn "\nMapping of program points to code: \n"
putStrLn (ppMap annots)
putStrLn "\nAnalysis result for all sub-expressions: \n"
Please sign in to comment.
Something went wrong with that request. Please try again.