update: added legacy typechecker

FMCt.cabal

@@ -39,6 +39,7 @@ common library-specs
     FMCt.Syntax
     FMCt.TypeChecker
     FMCt.TypeChecker2
+    FMCt.TypeCheckerAlt
     FMCt.Aux.Pretty
     FMCt.Aux.ToTex
 

src/FMCt.hs

@@ -1,11 +1,13 @@
 -- | Module is made just for Re-Exporting basic functions.
-module FMCt (module X, module XX) where
+module FMCt (module X, module XX, module Y) where
 
-import FMCt.Aux.Pretty   as X
-import FMCt.Aux.ToTex    as X
-import FMCt.Evaluator    as X (eval, eval1, eval1', evalToString)
-import FMCt.Examples     as X (examplesList)
-import FMCt.Parsing      as X (parseFMC, parseFMCtoString, parseType)
-import FMCt.Pretty       as X (printOutput, printStack)
-import FMCt.TypeChecker  as X (derive, typeCheck, typeCheckP)
-import FMCt.TypeChecker2 as XX (derive2, getTermType, pShow')
+import FMCt.Aux.Pretty     as X
+import FMCt.Aux.ToTex      as X
+import FMCt.Evaluator      as X  (eval, eval1, eval1', evalToString)
+import FMCt.Examples       as X  (examplesList)
+import FMCt.Parsing        as X  (parseFMC, parseFMCtoString, parseType)
+import FMCt.Pretty         as X  (printOutput, printStack)
+import FMCt.TypeChecker    as X  (derive, typeCheck, typeCheckP)
+import FMCt.TypeChecker2   as XX (derive2, getTermType, pShow', normalForm, testD2)
+import FMCt.Syntax         as X  (T, Type(..),)
+import FMCt.TypeCheckerAlt as Y  (derive1, testD1)

src/FMCt/Aux/TC.hs

@@ -0,0 +1,112 @@
+module FMCt.Aux.TC where
+
+import FMCt.Syntax
+import Text.Read (readMaybe)
+
+-- | Merge contexts
+mergeCtx :: Context -> Context -> Either TError Context
+mergeCtx ox oy = makeSet ox oy
+  where
+    makeSet [] x = pure x
+    makeSet (t : xs) [] = (t :) <$> makeSet xs oy
+    makeSet t@((term, ty) : xs) ((term', ty') : ys) =
+        if term /= term'
+            then makeSet t ys
+            else
+                if ty == ty'
+                    then makeSet xs oy
+                    else
+                        Left . ErrOverride $
+                            "Type Conflict between: "
+                                ++ show term
+                                ++ ":"
+                                ++ show ty
+                                ++ " and "
+                                ++ show term'
+                                ++ ":"
+                                ++ show ty'
+
+
+
+flat :: Either a (Either a b) -> Either a b
+flat = either Left id
+
+
+-- | Pre parses the Term for primitives and adds their type to the context.
+buildContext :: Context -> Term -> Either TError Context
+buildContext eCtx =
+    let i = TCon "Int"
+        b = TCon "Bool"
+
+        to = (mempty :=>)
+
+        opType :: Operations -> T
+        opType = \case
+            Add -> TVec [i, i] :=> i
+            Subtract -> TVec [i, i] :=> i
+            If -> TVec[ b
+                      , TLoc (Lo "if") $ TVar "ifVar1"
+                      , TLoc (Lo "if") $ TVar "ifVar1"
+                      ] :=>
+                  TVec [ TLoc La $ TVar "ifVar1"]
+     in \case
+            V x St -> do
+                let rInt = (readMaybe x) :: Maybe Int
+                let rBool = (readMaybe x) :: Maybe Bool
+                let rOp = (readMaybe x) :: Maybe Operations
+                let nCtx = maybe [] (const [(x, to i)]) rInt
+                let nCtx' = maybe [] (const [(x, to b)]) rBool
+                let nCtx'' = maybe [] ((: []) . ((,) x) . opType) rOp
+                foldr (\m p -> flat $ mergeCtx <$> pure m <*> p) (pure []) $
+                    eCtx : nCtx : nCtx' : nCtx'' : []
+            V x t' -> do
+                let lCtx = buildContext eCtx (V x St)
+                let rCtx = buildContext eCtx t'
+                flat $ mergeCtx <$> lCtx <*> rCtx
+            P t _ t' -> do
+                let lCtx = buildContext eCtx t
+                let rCtx = buildContext eCtx t'
+                flat $ mergeCtx <$> lCtx <*> rCtx
+            B _ _ _ t -> buildContext eCtx t
+            St -> pure eCtx
+
+
+splitStream :: [a] -> ([a], [a])
+splitStream x = (,) l r
+  where
+    l = snd <$> (filter (odd . fst) $ zip ([1 ..] :: [Integer]) x)
+    r = snd <$> (filter (not . odd . fst) $ zip ([1 ..] :: [Integer]) x)
+
+
+freshTypeVar :: [T]
+freshTypeVar =
+    TVar
+        <$> [ mconcat $ [[x], show y]
+            | y <- [1 ..] :: [Integer]
+            , x <- ['a' .. 'z']
+            ]
+
+freshVarTypes :: [T]
+freshVarTypes = zipWith (:=>) ls rs
+  where
+    (ls,rs) = splitStream freshTypeVar
+
+
+-- | Normalise gets rid of empty Types at locations.
+normaliseT :: T -> T
+normaliseT t
+    | t == normalisedT = normalisedT
+    | otherwise = normaliseT normalisedT
+  where
+    normalisedT = normaliseT' t
+    normaliseT' = \case
+        TEmp -> mempty
+        TVec [] -> mempty
+        TLoc _ (TVec []) -> mempty
+        TLoc _ (TEmp) -> mempty
+        TLoc _ (TCon "") -> mempty
+        TLoc l (TVec (x : xs)) -> TLoc l x <> (TLoc l $ TVec xs)
+        TVec ([x]) -> normaliseT x
+        t1 :=> t2 -> normaliseT t1 :=> normaliseT t2
+        TVec (x : xs) -> normaliseT x <> (normaliseT $ TVec xs)
+        x -> x -- Just to be sure it gets through.

src/FMCt/Pretty.hs

@@ -1,11 +1,16 @@
 module FMCt.Pretty (
     printStack,
     printOutput,
+    printBindings2,
+    printBindingsA,
+    printSubs,
 ) where
 
 import Data.Map as M
 import FMCt.Evaluator
 import FMCt.Syntax
+import qualified FMCt.TypeChecker2 as T2
+import qualified FMCt.TypeCheckerAlt as TA
 
 printStack :: State -> String
 printStack (m, b) = "Memory: \n" ++ printer mem ++ "Bindings: \n" ++ printer bin
@@ -22,3 +27,19 @@ printOutput (m, _) = "Output: \n" ++ printer out
     printer = \case
         [] -> ""
         (x : xs) -> show x ++ "\n" ++ printer xs
+
+-- | Pretty Prints all the bindings in a context for derivation from TypeChecker 2.
+printBindings2 :: T2.Derivation -> String
+printBindings2 = auxCtxPP . T2.getContext
+
+-- | Pretty Prints all the bindings in a context for derivation from TypeChecker Alt.
+printBindingsA :: TA.Derivation -> String 
+printBindingsA = auxCtxPP . TA.getContext
+
+-- | Shared Pretty Printer.
+auxCtxPP :: [(String, T)] -> [Char]
+auxCtxPP = mconcat . fmap (\(b,t) -> mconcat [ " ", b, " : ", pShow t, "\n"])
+
+-- | Pretty Prints substitutions
+printSubs :: [T2.TSubs] -> String
+printSubs = mconcat . fmap (\(x,y) -> mconcat [" ", pShow x, " ~> ", pShow y, "\n"])

src/FMCt/TypeChecker.hs

@@ -20,7 +20,9 @@ module FMCt.TypeChecker (
     (<.>),
     getTermType,
     splitStream,
-    buildContext,    
+    buildContext,
+    pShow,
+    pShow',
 ) where
 
 --import Data.Set
@@ -565,3 +567,80 @@ instance Pretty Derivation where
                 (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ "  " ++ y | (x, y) <- zip d1 (extend (l2 + m2 + r2) d2)])
             | otherwise =
                 (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ " " ++ y | (x, y) <- zip (extend (l1 + m1 + r1) d1) d2])
+    pShow d = unlines (reverse strs)
+      where
+        (_, _, _, strs) = showD d
+        showT :: T -> String
+        showT = pShow
+        showC :: Context -> String
+        showC =
+            let sCtx (x, t) = show x ++ ":" ++ showT t ++ ", "
+             in \case
+                    [] -> []
+                    c -> (flip (++) " ") . mconcat $ sCtx <$> c
+        showJ :: Judgement -> String
+        showJ (cx, n, t) = mconcat $ showC cx{-"Γ "-} : "|- " : show n : " : " : showT t : []
+        showL :: Int -> Int -> Int -> String
+        showL l m r = mconcat $ replicate l ' ' : replicate m '-' : replicate r ' ' : []
+        showD :: Derivation -> (Int, Int, Int, [String])
+        showD (Star j) = (0, k, 0, [s, showL 0 k 0]) where s = showJ j; k = length s
+        showD (Variable j) = (0, k, 0, [s, showL 0 k 0]) where s = showJ j; k = length s
+        showD (Abstraction j d') = addrule (showJ j) (showD d')
+        showD (Application j d') = addrule (showJ j) (showD d')
+        showD (Fusion j d' e) = addrule (showJ j) (sidebyside (showD d') (showD e))
+        addrule :: String -> (Int, Int, Int, [String]) -> (Int, Int, Int, [String])
+        addrule x (l, m, r, xs)
+            | k <= m =
+                (ll, k, rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL l m r : xs)
+            | k <= l + m + r =
+                (ll, k, rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL ll k rr : xs)
+            | otherwise =
+                (0, k, 0, x : replicate k '-' : [replicate (- ll) ' ' ++ y ++ replicate (- rr) ' ' | y <- xs])
+          where
+            k = length x; i = div (m - k) 2; ll = l + i; rr = r + m - k - i
+        extend :: Int -> [String] -> [String]
+        extend i strs' = strs' ++ repeat (replicate i ' ')
+        sidebyside :: (Int, Int, Int, [String]) -> (Int, Int, Int, [String]) -> (Int, Int, Int, [String])
+        sidebyside (l1, m1, r1, d1) (l2, m2, r2, d2)
+            | length d1 > length d2 =
+                (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ "  " ++ y | (x, y) <- zip d1 (extend (l2 + m2 + r2) d2)])
+            | otherwise =
+                (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ " " ++ y | (x, y) <- zip (extend (l1 + m1 + r1) d1) d2])
+
+-- | Pretty Show of derivation hiding the context.
+pShow' :: Derivation -> String
+pShow' d = unlines (reverse strs)
+  where
+    (_, _, _, strs) = showD d
+    showT :: T -> String
+    showT = pShow
+    showC :: Context -> String
+    showC = const "Γ "
+    showJ :: Judgement -> String
+    showJ (cx, n, t) = mconcat $ showC cx : "|- " : pShow n : " : " : showT t : []
+    showL :: Int -> Int -> Int -> String
+    showL l m r = mconcat $ replicate l ' ' : replicate m '-' : replicate r ' ' : []
+    showD :: Derivation -> (Int, Int, Int, [String])
+    showD (Star j) = (0, k, 0, [s, showL 0 k 0]) where s = showJ j; k = length s
+    showD (Variable j) = (0, k, 0, [s, showL 0 k 0]) where s = showJ j; k = length s
+    showD (Abstraction j d') = addrule (showJ j) (showD d')
+    showD (Application j d') = addrule (showJ j) (showD d')
+    showD (Fusion j d' e) = addrule (showJ j) (sidebyside (showD d') (showD e))
+    addrule :: String -> (Int, Int, Int, [String]) -> (Int, Int, Int, [String])
+    addrule x (l, m, r, xs)
+        | k <= m =
+            (ll, k, rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL l m r : xs)
+        | k <= l + m + r =
+            (ll, k, rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL ll k rr : xs)
+        | otherwise =
+            (0, k, 0, x : replicate k '-' : [replicate (- ll) ' ' ++ y ++ replicate (- rr) ' ' | y <- xs])
+      where
+        k = length x; i = div (m - k) 2; ll = l + i; rr = r + m - k - i
+    extend :: Int -> [String] -> [String]
+    extend i strs' = strs' ++ repeat (replicate i ' ')
+    sidebyside :: (Int, Int, Int, [String]) -> (Int, Int, Int, [String]) -> (Int, Int, Int, [String])
+    sidebyside (l1, m1, r1, d1) (l2, m2, r2, d2)
+        | length d1 > length d2 =
+            (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ "  " ++ y | (x, y) <- zip d1 (extend (l2 + m2 + r2) d2)])
+        | otherwise =
+            (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ " " ++ y | (x, y) <- zip (extend (l1 + m1 + r1) d1) d2])

src/FMCt/TypeChecker2.hs

@@ -8,14 +8,18 @@ module FMCt.TypeChecker2
     Derivation(..),
     Judgement,
     Context,
+    TSubs,
     derive0,
     derive1,
     testD0,    
     testD1,
     testD2,
     derive2,
+    derive2Subs,
     getTermType,
     pShow',
+    normalForm,
+    getContext,
   ) where
 import FMCt.Syntax
 import FMCt.Parsing
@@ -38,19 +42,25 @@ type Context = [(Vv, T)]
 type Judgement = (Context, Term, T)
 
 type Term = Tm
-
+
+-- | A type substitution is a pair of types             
 type TSubs = (T,T)
 
+-- | Standard Derivation type. Based on the FMC's BNF.
 data Derivation
     = Star        !Judgement
     | Variable    !Judgement !Derivation
     | Abstraction !Judgement !Derivation
     | Application !Judgement !Derivation !Derivation
     deriving (Show, Eq)
 
+-- | Default Empty Context
 emptyCx :: Context
 emptyCx = [("*",mempty :=> mempty)]
 
+-- | Converts a term into its normal form.
+-- Example:
+-- > a,l(al(b),a),c ~> a,c,l(a,al(b))
 normalForm :: T -> T
 normalForm = \x -> case x of 
   TEmp -> TEmp
@@ -67,7 +77,8 @@ normalForm = \x -> case x of
   TLoc l t -> TLoc l (normalForm t)
   m :=> n -> normalForm m :=> normalForm n
 
-
+-- | Derive0 provides the structure of the derivation, without unifing the
+-- types. Useful for testing the AST of a type derivation.
 derive0 :: Term -> Derivation
 derive0 term = derive0' freshVarTypes term
   where
@@ -192,13 +203,21 @@ type Result a = Either TError a
 
 -- | Same as "derive1" but safe, and applies all substitutions at the end.
 derive2 :: Term -> Result Derivation
-derive2 term = do
+derive2 = (fmap snd) . derive2Aux
+
+-- | Get the substitutions that were needed for the unification.
+derive2Subs :: Term -> Result [TSubs]
+derive2Subs = (fmap fst) . derive2Aux
+
+-- | Same as "derive1" but safe, and applies all substitutions at the end.
+derive2Aux :: Term -> Result ([TSubs],Derivation)
+derive2Aux term = do
   let (ppTerm,lTStream) = replaceInfer freshVarTypes term
   bCx           <- pBCx ppTerm                             -- pre build context
   result        <- derive2' lTStream bCx emptySb ppTerm    -- derive
   let derivation = snd result                              -- take final derivation
   let casts      = fst result                              -- take the final casts 
-  return $ applyTSubsD casts derivation                    -- apply them to the derivation and return it 
+  return $ (casts,applyTSubsD casts derivation)            -- apply them to the derivation and return it 
 
   where
     emptySb = []