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

toothbrush · Jul 8, 2011 · 475f2cc · 475f2cc
2 parents 9b258fd + 0194cea
commit 475f2cc
Show file tree

Hide file tree

Showing 23 changed files with 18 additions and 84 deletions.
diff --git a/doc/main.tex b/doc/main.tex
@@ -174,8 +174,7 @@ \subsection{Type System}
         } \\
 ~&~\\
         $ [$\emph{t-nil}$] $& \inference{
-        {\Gamma},C |- \<nil>\ : \tau^{\varphi_1}
-        & C |- \varphi \sqsupseteq \pi
+        C |- \varphi \sqsupseteq \pi
         }
         {
         {\Gamma},C |- \<nil>_\pi : [\tau^{\varphi_1}]^{\varphi}

diff --git a/examples/app.hm b/examples/app.hm
diff --git a/examples/assignment.hm b/examples/assignment.hm
diff --git a/examples/case-list.hm b/examples/case-list.hm
diff --git a/examples/case.hm b/examples/case.hm
diff --git a/examples/conditional.hm b/examples/conditional.hm
diff --git a/examples/const.hm b/examples/const.hm
diff --git a/examples/generalise-test.hm b/examples/generalise-test.hm
diff --git a/examples/identity.hm b/examples/identity.hm
diff --git a/examples/inf.hm b/examples/inf.hm
diff --git a/examples/letidid.hm b/examples/letidid.hm
diff --git a/examples/list-fn.hm b/examples/list-fn.hm
diff --git a/examples/list.hm b/examples/list.hm
diff --git a/examples/poisoning-case.hm b/examples/poisoning-case.hm
diff --git a/examples/poisoning.hm b/examples/poisoning.hm
diff --git a/examples/recursion.hm b/examples/recursion.hm
diff --git a/examples/recursion2.hm b/examples/recursion2.hm
diff --git a/examples/singleton.hm b/examples/singleton.hm
diff --git a/examples/slide.hm b/examples/slide.hm
diff --git a/examples/tuple.hm b/examples/tuple.hm
diff --git a/src/APA2/AG/DataTypes.ag b/src/APA2/AG/DataTypes.ag
@@ -126,11 +126,12 @@ instance Show Qual where
   show (Qual c q) = show c ++ " => " ++ show q
 
 tyAnn :: (Show a1, Show a) => a -> a1 -> [Char]
-tyAnn t a = "(" ++ show t ++ ":" ++ show a ++ ")"
+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) ++ ")"
 
+colonOpt :: String -> String
 colonOpt []   = ""
 colonOpt xs   = " : " ++ xs
 
@@ -147,7 +148,7 @@ instance Show Ty where
   show (List t an)  = "(List " ++ show t ++ ") " ++ (colonOpt $ show an)
 
 tyLayout :: Map AnnVar SAnn -> Ty -> String
-tyLayout _   (TyVar a)       = "" -- a - we probably don't want to see this here. 
+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 _   Nat             = "Nat"
 tyLayout _   Bool            = "Bool"

diff --git a/src/APA2/AG/Infer.ag b/src/APA2/AG/Infer.ag
@@ -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

diff --git a/src/Components.hs b/src/Components.hs
@@ -46,38 +46,31 @@ debugFile fl = do
 debugInference :: MH -> IO ()
 debugInference tm =
   do
-    let (ty, annotation, subst, constraints, exprs, debug, annots) = w tm
-    putStrLn ("Program: \n    " ++ show tm)
-    print tm 
-    putStrLn ""
+    let (_, annotation, subst, constraints, _, debug, annots) = w tm
     putStrLn "Substitution:"
     print subst
     putStrLn ""
-    putStrLn "Ty:"
-    let solved = worklist constraints
-    let ty' = applySubst (solutionSubst constraints) (applySubst subst ty)
-    putStrLn $ ("("++ tyLayout solved ty' ++ ") :::: " ++  ((fromSAnn annotation) `from` solved))
-    putStrLn ""
     putStrLn "Top level annotation: "
     print annotation
+    putStrLn ""
+    let solved = worklist constraints
     let ppoint = DM.findWithDefault (AnnVar "the empty set") (fromSAnn annotation) solved
     putStr $ "... which maps to: " ++ show ppoint ++ "\n"
     putStr $ DS.fold (\x->(++) (
         x ++ " is in fact \"" ++ show (annots DM.! x) ++ "\"\n"
         ) ) ""
         (toSet ppoint)
-    putStrLn "Annotation dictionary:"
-    putStrLn (ppMap annots)
     putStrLn ""
     putStrLn "Constraints: "
     print (DS.toList constraints)
-    putStrLn "\nNew_Constraints: "
-    printAnalysis solved
-    putStrLn ""
-    putStrLn "Expressions: "
-    printExpressions solved (applySubst (solutionSubst constraints) (applySubst subst exprs))
     putStrLn ""
+    putStrLn "\nNew_Constraints (after solving): "
+    printAnalysis solved
+    putStrLn "DEBUG OUTPUT ACCUMULATED IN AG:"
     putStrLn debug
+    putStr   horiz
+    putStrLn "DEBUG OUTPUT FINISHED. NORMAL OUTPUT TO FOLLOW: \n"
+    analysisResult tm
 
 -- | Prints an analysis result
 analysisResult :: MH -> IO ()
@@ -105,7 +98,7 @@ solutionSubst cs =
 
 -- | Prints a list of expressions
 --   Don't print the whole program again, this happens earlier.
---printExpressions :: Show a => [(a, MH)] -> IO ()
+printExpressions :: Map AnnVar SAnn -> [(Ty, MH)] -> IO ()
 printExpressions _   []        = putStr "\n"
 printExpressions con (_:exprs) = mapM_ (\(a,e) -> case e of 
                                                     CaseAlt _ _ -> putStr ""