From 2c3a69fa299fd2040a9a7c8c1263634f56c2ccdf Mon Sep 17 00:00:00 2001 From: cstml Date: Thu, 2 Sep 2021 15:06:30 +0100 Subject: [PATCH] update: added legacy typechecker --- FMCt.cabal | 1 + src/FMCt.hs | 20 +- src/FMCt/Aux/TC.hs | 112 ++++++++ src/FMCt/Pretty.hs | 21 ++ src/FMCt/TypeChecker.hs | 81 +++++- src/FMCt/TypeChecker2.hs | 27 +- src/FMCt/TypeCheckerAlt.hs | 382 ++++++++++++++++++++++++++++ src/FMCt/Web/Components/MainPage.hs | 4 +- src/FMCt/Web/MainWebsite.hs | 7 + src/FMCt/Web/Pages/Derive.hs | 33 ++- src/FMCt/Web/Pages/DeriveAlt.hs | 92 +++++++ src/FMCt/Web/Pages/Root.hs | 9 +- 12 files changed, 768 insertions(+), 21 deletions(-) create mode 100644 src/FMCt/Aux/TC.hs create mode 100644 src/FMCt/TypeCheckerAlt.hs create mode 100644 src/FMCt/Web/Pages/DeriveAlt.hs diff --git a/FMCt.cabal b/FMCt.cabal index 6e165de..0462787 100644 --- a/FMCt.cabal +++ b/FMCt.cabal @@ -39,6 +39,7 @@ common library-specs FMCt.Syntax FMCt.TypeChecker FMCt.TypeChecker2 + FMCt.TypeCheckerAlt FMCt.Aux.Pretty FMCt.Aux.ToTex diff --git a/src/FMCt.hs b/src/FMCt.hs index e20aca6..d04278a 100644 --- a/src/FMCt.hs +++ b/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) diff --git a/src/FMCt/Aux/TC.hs b/src/FMCt/Aux/TC.hs new file mode 100644 index 0000000..7887c56 --- /dev/null +++ b/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. diff --git a/src/FMCt/Pretty.hs b/src/FMCt/Pretty.hs index 5f0806e..dff90f2 100644 --- a/src/FMCt/Pretty.hs +++ b/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"]) diff --git a/src/FMCt/TypeChecker.hs b/src/FMCt/TypeChecker.hs index 6a92bad..598c150 100644 --- a/src/FMCt/TypeChecker.hs +++ b/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]) diff --git a/src/FMCt/TypeChecker2.hs b/src/FMCt/TypeChecker2.hs index 174bed9..1be40a9 100644 --- a/src/FMCt/TypeChecker2.hs +++ b/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,9 +42,11 @@ 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 @@ -48,9 +54,13 @@ data 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 = [] diff --git a/src/FMCt/TypeCheckerAlt.hs b/src/FMCt/TypeCheckerAlt.hs new file mode 100644 index 0000000..ff4cecb --- /dev/null +++ b/src/FMCt/TypeCheckerAlt.hs @@ -0,0 +1,382 @@ +{-# OPTIONS_GHC -Wno-unused-imports #-} +{-# OPTIONS_GHC -Wno-unused-matches #-} +{-# OPTIONS_GHC -Wno-unused-top-binds#-} + +-- | +--Module : Alternative Type Checker (Legacy} +-- +--Description : Alternative Type Checker that uses a different set of derivation rules. +-- +--Alternative type-checker (legacy). + +module FMCt.TypeCheckerAlt ( derive1, testD1, getContext, Derivation(..), pShow') +where + +import FMCt.Syntax +import FMCt.Parsing +import FMCt.TypeChecker ( + Derivation(..), + freshVarTypes, + splitStream, + TError(..), + normaliseT, + pShow', + buildContext, + Operations(..)) +import Control.Monad +import FMCt.Aux.Pretty (pShow,Pretty) + +type Context = [(Vv, T)] + +type Term = Tm + +emptyCx :: Context +emptyCx = [("*",mempty :=> mempty)] + +derive1 :: Term -> Either TError Derivation +derive1 term = do + preBuildCtx <- buildContext emptyCx term + derive1' freshVarTypes preBuildCtx term + + where + + derive1' :: [T] -> Context -> Term -> Either TError Derivation + derive1' stream exCx = \case + + St -> do + ty <- getType St exCx + return $ Star (exCx, St, ty) + + xx@(V x St) -> do + ty <- getType xx exCx + return $ Variable (exCx, xx, ty) + + xx@(V bi tm) -> do + + let (lStr,rStr) = splitStream $ tail stream + derivL <- (derive1' lStr exCx (V bi St)) + let lCx = getContext derivL + derivR <- (derive1' rStr lCx tm) + let rCx = getContext derivR + let mCx = makeSet $ lCx ++ rCx + let tL = getDerivationT derivL + let tR = getDerivationT derivR + let (tCasts,ty) = fuse tL tR + return $ applyTSubsD tCasts $ Fusion (mCx, xx, ty) derivL derivR + + xx@(B bi bTy lo St) -> do + let ty = TLoc lo bTy :=> mempty + let nCx = (bi,bTy) : exCx + deriv <- derive1' (tail stream) nCx (V bi St) + let aboveCx = getContext deriv + return $ Abstraction (aboveCx, xx, ty) deriv + + xx@(B bi bTy lo tm) -> do + let (lStr,rStr) = splitStream $ tail stream + derivL <- (derive1' lStr exCx (B bi bTy lo St)) + let lCx = getContext derivL + derivR <- derive1' rStr lCx tm + let rCx = getContext derivR + let mCx = makeSet $ lCx ++ rCx + + let tL = getDerivationT derivL + let tR = getDerivationT derivR + + let (tCasts,ty) = fuse tL tR + + return . applyTSubsD tCasts $ Fusion (mCx, xx, ty) derivL derivR + + xx@(P ptm lo St) -> do + deriv <- derive1' (tail stream) exCx ptm + let abvT = getDerivationT deriv + let ty = mempty :=> TLoc lo abvT + let aboveCx = getContext deriv + return $ Application (aboveCx, xx, ty) deriv + + xx@(P ptm lo tm) -> do + let (lStr,rStr) = splitStream $ tail stream + derivL <- derive1' lStr exCx (P ptm lo St) + let lCx = getContext derivL + derivR <- derive1' rStr lCx tm + let rCx = getContext derivR + let mCx = makeSet $ lCx ++ rCx + + let tL = getDerivationT derivL + let tR = getDerivationT derivR + + let (tCasts,ty) = fuse tL tR + return . applyTSubsD tCasts $ Fusion (mCx, xx, ty) derivL derivR + +testD1 :: String -> IO () +testD1 = either (putStrLn.show) putStrLn . fmap pShow . derive1 . parseFMC + +type TSubs = (T,T) + +consume :: [TSubs] -- ^ Substitutions to be made in both types. + -> T -- ^ The consuming Type. + -> T -- ^ The consumed Type. + -> ([TSubs],T,T) -- ^ The new list of substitutions, remaining from the consuming, remaining from the consumed. +consume exSubs x y = + let + x' = normaliseT $ applyTSub exSubs x -- we use the already subtituted form when consuming + y' = normaliseT $ applyTSub exSubs y -- for both terms + in + case x' of + TEmp -> case y' of +-- TVar _ -> ((y',x'):exSubs,mempty,mempty) + _ -> (exSubs,mempty,y') -- mempty doesn't change anything else + + TVec [] -> (exSubs,mempty,y') -- synonym for mempty + + TCon _ -> case y' of + TEmp -> (exSubs,x',mempty) + TVec [] -> (exSubs,x',mempty) + TCon _ -> if x' == y' + then (exSubs, mempty, mempty) + else error $ "cannot consume! - type " ++ show y' ++ " should be " ++ show x' + TVec (yy': yys') -> + let + (interSubs,interX,remainY) = consume exSubs x' yy' + (finalSubs,finalX,finalY) = consume interSubs interX (TVec yys') + in + (finalSubs,finalX,remainY <> finalY) + t1 :=> t2 -> error $ show x' ++ " cannot consume higher type " ++ show y' + -- if a constant tries to consume a variable, it creates a substitution and gets fully consumed + TVar _ -> ((y',x') : exSubs, mempty, mempty) + TLoc _ _ -> (exSubs,x',y') + + TVar _ -> case y' of + TEmp -> ((x',y'):exSubs,mempty,mempty) + TVec [] -> (exSubs,x',mempty) + -- if consumed by anything, the Variable gets cast and changes all the + -- other appearances of itself. + _ -> (((x',y'):exSubs),mempty,mempty) + + TLoc xl' xt' -> case y' of + TEmp -> (exSubs,x',mempty) + TVec [] -> (exSubs,x',mempty) + TCon _ -> (exSubs,x',y) -- home row and locations don't interact + TVar _ -> (exSubs,x',y) -- home row variable and locations don't interact + TVec (yy': yys') -> + let + (interSubs,interX,remainY) = consume exSubs x' yy' + (finalSubs,finalX,finalY) = consume interSubs interX (TVec yys') + in + (finalSubs,finalX,remainY <> finalY) + TLoc yl' yt' -> if yl' == xl' + then + let + (finalSubs, finalX', finalY') = consume exSubs xt' yt' + in + (finalSubs, TLoc xl' finalX', TLoc yl' finalY') + else + (exSubs,x',y) + _ :=> _ -> (exSubs,x',y) + + ix' :=> ox' -> case y' of + TEmp -> (exSubs,x',mempty) + TVec [] -> (exSubs,x',mempty) + TCon _ -> error $ "cannot fuse higer type " ++ show x' ++ " with " ++ show y' + TVar _ -> (((y',x'):exSubs),mempty,mempty) + TLoc _ _ -> (exSubs,x',y') + TVec (yy' : yys') -> + let + (interSubs, interX', interYY') = consume exSubs x' yy' + (finalSubs, finalX', finalYY') = consume interSubs interX' (TVec yys') + in + (finalSubs, finalX', interYY' <> finalYY') + iy' :=> oy' -> + if normaliseT x' == normaliseT y' + then (exSubs, mempty, mempty) + else let + (intSubs, leftIX', leftIY') = consume exSubs ix' iy' + (finalSubs, rightIX', rightIY') = consume intSubs ox' oy' + (finalL,finalR) = (normaliseT $ leftIX' <> leftIY', normaliseT $ rightIX' <> rightIY') + res = (finalSubs, finalL, finalR) +-- res = (finalSubs,mempty,mempty) + in case res of + (_,TEmp,TEmp) -> res + + _ -> error $ show x' ++ " cannot consume " ++ show y' ++ " fusion result: " ++ show res + + TVec (xx':xxs') -> case y' of + TEmp -> (exSubs,x',mempty) + TVec [] -> (exSubs,x',mempty) + TVec (_:_) -> + let + (interSubs, interXX', interY') = consume exSubs xx' y' + (finalSubs, finalXXs', finalY') = consume interSubs (TVec xxs') interY' + in + (finalSubs, interXX' <> finalXXs', finalY') + + -- The same way for all the other types. We recursively try the first of + -- the first vector with all of the second. + _ -> + let + (interSubs, interXX', interY') = consume exSubs xx' y' + (finalSubs, finalXXs', finalY') = consume interSubs (TVec xxs') interY' + in + (finalSubs, interXX' <> finalXXs', finalY') + +diffLoc :: T -> T -> Bool +diffLoc = \case + x@(TCon _) -> \case + TCon _ -> False + TVar _ -> False -- Unsure about this + TEmp -> True + TVec [] -> True + TVec y -> diffLoc x `all` y + TLoc _ _ -> True + _ -> False + x@(TVar _) -> \case + TLoc _ _ -> True + TEmp -> True + TVec [] -> True + TVec y -> diffLoc x `all` y + _ -> False + TVec [] -> const True + TEmp -> const True + xx@(TVec (x:xs)) -> \case + y@(TVec yy) -> diffLoc x `all` yy && (diffLoc (TVec xs) y) + y -> diffLoc y xx -- flip it + TLoc l _ -> \case + TLoc k _ -> if l == k then False else True + _ -> True + x@(_ :=> _) -> \y -> diffLoc y x + +fuse :: T -> T -> ([TSubs],T) +fuse = \case + x@(xi :=> xo) -> \case + y@(yi :=> yo) -> + let + (subs, remainY, remainX) = consume [] yi xo + res = (subs, normaliseT remainX, normaliseT remainY) + in + case res of +-- _ -> error $ show res + (_,TEmp,_) -> (,) subs ((xi <> remainY) :=> yo) + (_,_,TEmp) -> (,) subs (xi :=> (yo <> remainX)) + _ -> if snd $ aux diffLoc [remainX, remainY, xi, yi] + then (,) subs ((xi <> remainY) :=> (yo <> remainX)) + else error $ "cannot fuse " ++ show x ++ " " ++ show y ++ " result: " ++ show res + where + aux :: Monoid a => (a -> a -> Bool) -> [a] -> (a,Bool) + aux f [] = (mempty,True) + aux f (z:zs) = (z, (f z (fst $ aux f zs)) && (snd $ aux f zs)) + y@(TVar _) -> + ([(y,x)],mempty) + y -> error $ "cannot fuse " ++ show x ++ " and " ++ show y ++ ". Wrong type Types - Use Function Types" + x -> \y -> error $ "cannot fuse " ++ show x ++ " and " ++ show y + +applyTSub :: [TSubs] -> T -> T +applyTSub = \case + [] -> id + xx@((xi,xo):xs) -> \case + TEmp -> TEmp + y@(TCon _ ) -> y + TLoc l t -> TLoc l (applyTSub xx t) + TVec y -> TVec $ applyTSub xx <$> y + yi :=> yo -> applyTSub xx yi :=> applyTSub xx yo + y@(TVar _) -> if y == xi then xo else applyTSub xs y + +{- +The first derivation always can find a way to derive the term. Now we need a way + to specialise it. Given that we are not allowing for types to be re-cast we can + merge the context by creating our first round of substitutions. +-} + + +type Subs = [(T,T)] + +getType :: Term -> Context -> Either TError T +getType = \case + t@(V b St) -> \case + [] -> + Left $ + ErrUndefT $ + mconcat + [ "Cannot Find type for binder: " + , show b + , " in context. Have you defined it prior to calling it ?" + ] + ((b', ty) : xs) -> if b == b' then pure ty else getType t xs + St -> \_ -> pure $ mempty :=> mempty + t -> \_ -> + Left . ErrNotBinder $ + mconcat ["Attempting to get type of:", show t] + +getContext :: Derivation -> Context +getContext = \case + Star (c,_,_) -> c + Variable (c,_,_) -> c + Abstraction (c,_,_) _ -> c + Fusion (c,_,_) _ _ -> c + Application (c,_,_) _ -> c + + +applySubsT :: Subs -> T -> T +applySubsT [] x = x +applySubsT ((ti,to):xs) x = if ti == x then applySubsT xs to else applySubsT xs x + +applySubsCx :: Subs -> Context -> Context +applySubsCx x y = applySubsVvT x <$> y + +applySubsVvT :: Subs -> (Vv,T) -> (Vv,T) +applySubsVvT [] y = y +applySubsVvT ((ti,to):xs) y@(yv,yt) + | yt == ti = applySubsVvT xs (yv,to) + | otherwise = applySubsVvT xs y + +applySubsD :: Subs -> Derivation -> Derivation +applySubsD subs = \case + Star (cx,tm,ty) -> Star (applySubsCx subs cx, tm ,applySubsT subs ty) + Variable (cx,tm,ty) -> Variable (applySubsCx subs cx, tm ,applySubsT subs ty) + Abstraction (cx,tm,ty) de -> + Abstraction + (makeSet $ applySubsCx subs cx, tm ,applySubsT subs ty) + (applySubsD subs de) + Application (cx,tm,ty) de -> + Application + (makeSet $ applySubsCx subs cx, tm ,applySubsT subs ty) + (applySubsD subs de) + Fusion (cx,tm,ty) dL dR -> + Fusion + (makeSet $ applySubsCx subs cx, tm ,applySubsT subs ty) + (applySubsD subs dL) + (applySubsD subs dR) + +applyTSubsD :: [TSubs] -> Derivation -> Derivation +applyTSubsD subs = \case + Fusion (cx,tm,ty) dL dR -> Fusion ( (\(x,y)-> (x,applyTSub subs y)) <$> cx, nTm , applyTSub subs ty) dL dR + where + nTm = case tm of + B v ty' l t' -> B v (applyTSub subs ty') l t' + x -> x + + _ -> error "You are not allowed to cast here! - this should never happen" + +allCtx :: Derivation -> Context +allCtx = \case + x@(Star _) -> getContext x + x@(Variable _) -> getContext x + x@(Application _ d) -> getContext x ++ allCtx d + x@(Abstraction _ d) -> getContext x ++ allCtx d + x@(Fusion _ dL dR) -> getContext x ++ allCtx dR ++ allCtx dL + +makeSet :: Eq a => [a] -> [a] +makeSet [] = [] +makeSet (x:xs) = if elem x xs then makeSet xs else x : makeSet xs + +getDerivationT :: Derivation -> T +getDerivationT = \case + Star (_,_,t) -> t + Variable (_,_,t) -> t + Application (_,_,t) _ -> t + Abstraction (_,_,t) _ -> t + Fusion (_,_,t) _ _ -> t + +getLocation :: Term -> Lo +getLocation = \case + P _ l _ -> l + B _ _ l _ -> l + x -> error $ "should't be reaching for location in term: " ++ show x diff --git a/src/FMCt/Web/Components/MainPage.hs b/src/FMCt/Web/Components/MainPage.hs index 03c74d3..e653465 100644 --- a/src/FMCt/Web/Components/MainPage.hs +++ b/src/FMCt/Web/Components/MainPage.hs @@ -18,7 +18,7 @@ mainPage = LU.renderText sMainPage LB.container_ $ do LB.row_ $ do LB.span2_ $ LU.div_ [LU.name_ "Title"] $ LU.h1_ "FMCt-Web" - LB.span2_ $ LU.div_ [LU.name_ "SubTitle"] $ LU.h2_ "V.0.4.1.beta" + LB.span2_ $ LU.div_ [LU.name_ "SubTitle"] $ LU.h2_ "V.2.0.2.beta" LU.hr_ [] LB.span2_ $ LU.h3_ "Welcome to the FMCt Web Interpreter." @@ -27,5 +27,5 @@ mainPage = LU.renderText sMainPage LB.span2_ $ LU.div_ [LU.name_ "Links"] $ do LU.h3_ "Links" - LU.ul_ $ LU.a_ [LU.href_ "parse?term=*"] "Parser" +-- LU.ul_ $ LU.a_ [LU.href_ "parse?term=*"] "Parser" -- Broken this is LU.ul_ $ LU.a_ [LU.href_ "derive?term=*"] "Derivation Tester" diff --git a/src/FMCt/Web/MainWebsite.hs b/src/FMCt/Web/MainWebsite.hs index d771a0c..a9f8fea 100644 --- a/src/FMCt/Web/MainWebsite.hs +++ b/src/FMCt/Web/MainWebsite.hs @@ -4,6 +4,7 @@ module FMCt.Web.MainWebsite (mainWebsite, mainWebsitePort) where import FMCt.Web.Helpers.Heroku (herokuGetPort) import FMCt.Web.Pages.Derive (pDerive) +import qualified FMCt.Web.Pages.DeriveAlt as Da (pDerive) import FMCt.Web.Pages.Evaluator (pEvaluator) import FMCt.Web.Pages.Root (pRoot) import FMCt.Web.Style.MainStyle (mainStylePage) @@ -25,6 +26,11 @@ mainWebsitePort port = do term' <- param "term" (html . LU.renderText . pDerive) term' + -- Alt Derivation Page. + let rDerivationPageAlt = get "/deriveAlt" $ do + term' <- param "term" + (html . LU.renderText . Da.pDerive) term' + -- Styling. let css = S.get "/style.css" $ html mainStylePage @@ -34,6 +40,7 @@ mainWebsitePort port = do rParse css rDerivationPage + rDerivationPageAlt -- | Start serving the website. diff --git a/src/FMCt/Web/Pages/Derive.hs b/src/FMCt/Web/Pages/Derive.hs index 574937d..1207547 100644 --- a/src/FMCt/Web/Pages/Derive.hs +++ b/src/FMCt/Web/Pages/Derive.hs @@ -3,7 +3,9 @@ module FMCt.Web.Pages.Derive (pDerive) where import Data.List (unfoldr) import qualified Data.Text.Lazy as LA import FMCt (derive2, pShow, getTermType, pShow') +import FMCt.TypeChecker2 (derive2Subs) import FMCt.Parsing (parseFMC') +import FMCt.Pretty (printBindings2, printSubs) import FMCt.Web.Components.Brick (brick) import FMCt.Web.Components.RegularPage (regularPage) import qualified Lucid as LU @@ -23,6 +25,8 @@ pDerive term = sDerivePage parsedBox termTypeBox derivationBox + bindgingTypeBox + subsTypeBox termForm :: LU.Html () termForm = do @@ -52,8 +56,35 @@ pDerive term = sDerivePage deriv = case getTermType pTerm of Left e -> show e Right ty -> pShow pTerm ++ " : "++ pShow ty - + bindgingTypeBox :: LU.Html () + bindgingTypeBox = + case (parseFMC' . LA.unpack) term of + Left _ -> pure () + Right pTerm -> + brick + ("types-div" :: String) + ("Variables & Types" :: LA.Text) + ("Each variable has the following (inferred) type in the context" :: LA.Text) + types + where + types = either mempty (rBr . printBindings2) $ derive2 pTerm + + subsTypeBox :: LU.Html () + subsTypeBox = + case (parseFMC' . LA.unpack) term of + Left _ -> pure () + Right pTerm -> + brick + ("subs-div" :: String) + ("Substitutions" :: LA.Text) + ("Substitutions needed to derive the term:" :: LA.Text) + subs + where + subs = either mempty (rBr . printSubs) $ derive2Subs pTerm + + -- | Utility function that re-writes whitespaces and newlines so that they + -- display correctly in HTML. rBr :: String -> LU.Html () rBr str = aux spStr where diff --git a/src/FMCt/Web/Pages/DeriveAlt.hs b/src/FMCt/Web/Pages/DeriveAlt.hs new file mode 100644 index 0000000..f06b9ef --- /dev/null +++ b/src/FMCt/Web/Pages/DeriveAlt.hs @@ -0,0 +1,92 @@ +module FMCt.Web.Pages.DeriveAlt (pDerive) where + +import Data.List (unfoldr) +import qualified Data.Text.Lazy as LA +import FMCt (pShow, getTermType) +import FMCt.TypeCheckerAlt (pShow', derive1) +import FMCt.Parsing (parseFMC') +import FMCt.Pretty (printBindingsA, printSubs) +import FMCt.Web.Components.Brick (brick) +import FMCt.Web.Components.RegularPage (regularPage) +import qualified Lucid as LU +import qualified Lucid.Bootstrap as LB + +pDerive :: LA.Text -> LU.Html () +pDerive term = sDerivePage + where + sDerivePage :: LU.Html () + sDerivePage = do + regularPage ("Derivator (Legacy)" :: LA.Text) $ LB.span1_ page + + page :: LU.Html () + page = do + LU.body_ $ do + termForm + parsedBox + termTypeBox + derivationBox + bindgingTypeBox + + termForm :: LU.Html () + termForm = do + LU.hr_ [] + LU.div_ [LU.name_ "term-div"] $ LU.form_ [LU.action_ "deriveAlt"] $ LU.input_ [LU.type_ "text", LU.name_ "term"] + + parsedBox :: LU.Html () + parsedBox = + brick ("parsed-div" :: LA.Text) ("Parsed Term" :: LA.Text) ("" :: LA.Text) pTerm + where + pTerm = either (LU.toHtml . show) (LU.toHtml . pShow) $ (parseFMC' . LA.unpack) term + + derivationBox :: LU.Html () + derivationBox = + case (parseFMC' . LA.unpack) term of + Left e -> LU.toHtml . show $ e + Right pTerm -> brick ("parsed-div" :: String) ("Term Derivation (Legacy)" :: LA.Text) ("" :: LA.Text) deriv + where + deriv = either (rBr . show) (rBr . pShow') $ derive1 pTerm + + termTypeBox :: LU.Html () + termTypeBox = + case (parseFMC' . LA.unpack) term of + Left e -> LU.toHtml . show $ e + Right pTerm -> brick ("parsed-div" :: String) ("Term-Type (Legacy)" :: LA.Text) ("" :: LA.Text) deriv + where + deriv = case getTermType pTerm of + Left e -> show e + Right ty -> pShow pTerm ++ " : "++ pShow ty + + bindgingTypeBox :: LU.Html () + bindgingTypeBox = + case (parseFMC' . LA.unpack) term of + Left _ -> pure () + Right pTerm -> + brick + ("types-div" :: String) + ("Variables & Types (Legacy)" :: LA.Text) + ("Each variable has the following (inferred) type in the context" :: LA.Text) + types + where + types = either mempty (rBr . printBindingsA) $ derive1 pTerm + + -- | Utility function that re-writes whitespaces and newlines so that they + -- display correctly in HTML. + rBr :: String -> LU.Html () + rBr str = aux spStr + where + aux = \case + [] -> LU.hr_ [] + (x : xs) -> LU.p_ [] (LU.toHtml x) >> aux xs + + separateBy :: Eq a => a -> [a] -> [[a]] + separateBy chr = unfoldr sep + where + sep [] = Nothing + sep l = Just . fmap (drop 1) . break (== chr) $ l + + spStr = separateBy '\n' $ replaceSp str + + replaceSp [] = [] + replaceSp (' ' : xs) = ' ' : replaceSp xs + -- space taken from https://qwerty.dev/whitespace/ + replaceSp (x : xs) = x : replaceSp xs diff --git a/src/FMCt/Web/Pages/Root.hs b/src/FMCt/Web/Pages/Root.hs index 37c308a..18b6803 100644 --- a/src/FMCt/Web/Pages/Root.hs +++ b/src/FMCt/Web/Pages/Root.hs @@ -12,12 +12,13 @@ pRoot = sMainPage where sMainPage :: LU.Html () sMainPage = do - regularPage "FMCt Homepage" $ do - brick "version" "V.0.0.1" "" "Welcome to the FMCt Web Interpreter." - brick "version" "V.0.0.1" "" "Links" + regularPage ("FMCt Homepage"::String) $ do + brick ("version"::String) ("V.2.0.1"::String) (""::String) ("Welcome to the FMCt Web Interpreter." :: String) LB.row_ $ do LB.span2_ $ LU.div_ [LU.name_ "Links"] $ do LU.h3_ "Links" - LU.ul_ $ LU.a_ [LU.href_ "parse?term=*"] "Parser" +-- LU.ul_ $ LU.a_ [LU.href_ "parse?term=*"] "Parser" +-- Evaluator has fallen a bit behind. TODO fix LU.ul_ $ LU.a_ [LU.href_ "derive?term=*"] "Derivation Tester" + LU.ul_ $ LU.a_ [LU.href_ "deriveAlt?term=*"] "Derivation Tester (Legacy)"