qlang.cabal

@@ -20,7 +20,7 @@ executable qlang
                     , TypeApplications
 
 
-  build-depends:       base >=4.11 && <4.12
+  build-depends:       base
                      , containers
                      , transformers
 

src/Q/Typecheck.hs

@@ -27,11 +27,17 @@ data Value
   = VTemp Temp
   | VInt Int
   | VBool Bool
-  deriving (Eq, Ord, Show)
+  deriving (Eq, Ord)
 
 newtype Temp = Temp Int
   deriving (Eq, Ord)
 
+instance Show Value where
+  show (VTemp t) = "_"
+  show (VInt n)  = show n
+  show (VBool True) = "true"
+  show (VBool False) = "false"
+
 instance Show Temp where
   show (Temp n) = printf "t%d" n
 
@@ -47,6 +53,15 @@ data Pred x
 
 type Constraints x = Map x [Pred x]
 
+showPreds :: Show x => [Pred x] -> String
+showPreds [] = "T"
+showPreds ps = intercalate " /\\ " (show <$> ps)
+
+showConstraints :: Show x => Constraints x -> String
+showConstraints = intercalate ", " . map f . Map.toList
+  where
+    f (x, ps) = printf "%s: %s" (show x) (showPreds ps)
+
 data FunSig = FunSig
   { fnArity :: Int
   , fnPre   :: Constraints Param
@@ -54,7 +69,11 @@ data FunSig = FunSig
   deriving (Eq)
 
 data Param = RV | Arg Int
-  deriving (Eq, Ord, Show)
+  deriving (Eq, Ord)
+
+instance Show Param where
+  show RV      = "rv"
+  show (Arg i) = printf "a%d" i
 
 instance Show x => Show (Pred x) where
   show PBool = "bool"
@@ -65,7 +84,11 @@ instance Show x => Show (Pred x) where
       (if b then "" else "!")
       (show x)
   show (PFun funSig) =
-    printf "<fn, arity=%d>" (show (fnArity funSig))
+    printf "fn(%s | %s) -> %s | %s"
+      (intercalate ", " (show . Arg <$> [0..fnArity funSig - 1]))
+      (showConstraints (fnPre funSig))
+      (show RV)
+      (showConstraints (fnPost funSig))
 
 instPred :: (p -> Value) -> Pred p -> Maybe (Pred Temp)
 instPred subst PBool      = Just PBool
@@ -79,7 +102,7 @@ instPred subst (PIfBoolEq param b pred) =
                 else
                   Nothing
     VInt _ ->
-      error "impossible"
+      Nothing
 
 inst :: (p -> Value) -> Constraints p -> [(Value, Pred Temp)]
 inst subst constraints = [ (subst param, pred')
@@ -149,28 +172,25 @@ tc env (EIf e0 e1 e2) = do
   ps1 <- predsOf =<< tc env e1
   ps2 <- predsOf =<< tc env e2
 
-  let meet = ps1 `intersect` ps2
-  retT <- newTemp
-
-  addConstraintsFor retT meet
-  case v0 of
-    VTemp cond -> do
-      addConstraintsFor retT (PIfBoolEq cond True  <$> (ps1 \\ meet))
-      addConstraintsFor retT (PIfBoolEq cond False <$> (ps2 \\ meet))
-    VBool True ->
-      addConstraintsFor retT (ps1 \\ meet)
-    VBool False ->
-      addConstraintsFor retT (ps2 \\ meet)
-    VInt _ ->
-      error "unreachable!"
+  let
+    meet = ps1 `intersect` ps2
+    comb = meet ++
+      (case v0 of
+         VTemp cond  -> map (PIfBoolEq cond True)  (ps1 \\ meet) ++
+                        map (PIfBoolEq cond False) (ps2 \\ meet)
+         VBool True  -> ps1 \\ meet
+         VBool False -> ps2 \\ meet
+         VInt _      -> error "unreachable!")
 
+  retT <- newTemp
+  addConstraintsFor retT comb
   pure (VTemp retT)
 
 tc env (ECall fId args) = do
   fp <- predsOf =<< tc env (EVar fId)
   fSig <- case [s | PFun s <- fp] of
             [s] -> pure s
-            _ -> err $ printf "not a function: %s" (show fId)
+            _   -> err $ printf "not a function: %s" (show fId)
 
   unless (fnArity fSig == length args)
     (err "wrong number of arguments")
@@ -194,6 +214,8 @@ tc env (ECall fId args) = do
   mapM_ addCon post
   pure (VTemp retT)
 
+--------------------------------------------------------------------------------
+-- Utilities for actually running the typechecker
 
 op2 :: Pred Param -> Pred Param -> Pred Param -> FunSig
 op2 p q r = FunSig
@@ -201,6 +223,9 @@ op2 p q r = FunSig
   , fnPre   = Map.fromList [(Arg 0, [p]), (Arg 1, [q])]
   , fnPost  = Map.fromList [(RV, [r])] }
 
+pIf :: x -> Pred x -> Pred x -> [Pred x]
+pIf x pTrue pFalse = [PIfBoolEq x True pTrue, PIfBoolEq x False pFalse]
+
 prelude :: [(Id, FunSig)]
 prelude =
   [ (Id "+", op2 PInt PInt PInt)
@@ -208,57 +233,66 @@ prelude =
   , (Id "edgy", FunSig { fnArity = 2
                        , fnPre = Map.fromList
                          [ (Arg 0, [PBool])
-                         , (Arg 1, [ PIfBoolEq (Arg 0) True PInt
-                                   , PIfBoolEq (Arg 0) False PBool ]) ]
+                         , (Arg 1, pIf (Arg 0) PInt PBool) ]
                        , fnPost = Map.fromList
-                         [ (RV, [ PIfBoolEq (Arg 0) True  PBool
-                                , PIfBoolEq (Arg 0) False PInt ]) ] })
+                         [ (RV, pIf (Arg 0) PBool PInt) ] })
   ]
 
-initTC :: [(Id, FunSig)] -> (S, Env)
-initTC funs = (s, env)
+initS :: [(Id, FunSig)] -> (S, Env)
+initS funs = (s, env)
   where
-    env =
-      Map.fromList [ (funId, VTemp (Temp i))
-                   | ((funId, _), i) <- zip funs [0..] ]
+    env = Map.fromList
+          [ (funId, VTemp (Temp i))
+          | ((funId, _), i) <- zip funs [0..] ]
+
     s = S { counter = length funs
-          , constraints =
-            Map.fromList [ (Temp i, [PFun funSig])
-                         | ((_, funSig), i) <- zip funs [0..] ] }
+          , constraints = Map.fromList
+                          [ (Temp i, [PFun funSig])
+                          | ((_, funSig), i) <- zip funs [0..] ] }
 
 newtype TCResult = TCR (Either String [Pred Temp])
 
 instance Show TCResult where
   show (TCR (Left err)) = "ERROR: " ++ err
-  show (TCR (Right [])) = "T"
-  show (TCR (Right ps)) = intercalate " /\\ " (show <$> ps)
+  show (TCR (Right ps)) = showPreds ps
+
+runTC :: S -> TC Value -> TCResult
+runTC s0 t = TCR (fst <$> runExcept (runStateT t' s0))
+  where
+    t' = do
+      v <- t
+      predsOf v
+      --pure (v, ps)
 
 typecheck :: Expr -> TCResult
-typecheck e = TCR $ runExcept (fst <$> runStateT getPreds s0)
+typecheck e = runTC s0 (tc env e)
   where
-    (s0, env) = initTC prelude
-    getPreds  = predsOf =<< tc env e
+    (s0, env) = initS prelude
 
 
+--------------------------------------------------------------------------------
+-- Examples
+
 -- >>> typecheck $ EBool True
 -- bool
 -- >>> typecheck $ EInt 0
 -- int
 -- >>> typecheck $ ELet (Id "z") (EInt 3) (EVar (Id "z"))
 -- int
-
+-- >>> typecheck $ EVar (Id "<")
+-- fn(a0, a1 | a0: int, a1: int) -> rv | rv: bool
+-- >>> typecheck $ EVar (Id "+")
+-- fn(a0, a1 | a0: int, a1: int) -> rv | rv: int
 -- >>> typecheck $ ECall (Id "+") [EInt 3, EInt 4]
 -- int
 -- >>> typecheck $ ECall (Id "<") [EInt 3, EInt 5]
 -- bool
 -- >>> typecheck $ ECall (Id "+") [EInt 3, EBool True]
 -- ERROR: function preconditions not satisifed
-
 -- >>> typecheck $ ECall (Id "edgy") [EBool True, EInt 4]
 -- bool
 -- >>> typecheck $ ECall (Id "edgy") [EBool False, EBool True]
 -- int
-
 -- >>> typecheck $ EIf (EBool True) (EInt 2) (EInt 4)
 -- int
 -- >>> typecheck $ EIf (EBool True) (EInt 2) (EBool False)
@@ -266,9 +300,8 @@ typecheck e = TCR $ runExcept (fst <$> runStateT getPreds s0)
 -- >>> typecheck $ EIf (EBool False) (EInt 2) (EBool False)
 -- bool
 -- >>> typecheck $ EIf (ECall (Id "<") [EInt 3, EInt 0]) (EInt 2) (EBool False)
+-- (int | t3) /\ (bool | !t3)
 -- >>> typecheck $ EIf (ECall (Id "<") [EInt 3, EInt 0]) (EInt 2) (EInt 0)
 -- int
-
 -- >>> typecheck $ EIf (EInt 0) (EInt 2) (EBool False)
 -- ERROR: condition isn't a boolean