Browse Source

started some work on totality checker (not going anywhere)

master
depsterr 6 months ago
parent
commit
c195c8a926
  1. 1
      app/Main.hs
  2. 3
      readme.simple.txt
  3. 1
      sexprml.cabal
  4. 4
      src/Misc.hs
  5. 52
      src/Simple/CC.hs
  6. 27
      src/Simple/TC.hs
  7. 15
      src/Simple/TC/TypeOps.hs
  8. 30
      src/Simple/TC/Types.hs

1
app/Main.hs

@ -7,6 +7,7 @@ import Parser.Parser (parse)
import Lexer.Lexer (runAlex')
import Simple.Convert
import Simple.TC
import Simple.TC.Types
import System.Environment
import System.Exit

3
readme.simple.txt

@ -2,6 +2,9 @@
(data 𝔹 ([𝔹] 𝕋)
([𝔹] 𝔽))
-- (data Fuck ([𝔹] T)
-- ([Integer -> Integer -> 𝔹] F))
[𝔹 → 𝔹]
(def (((not 𝕋) 𝔽)
((not 𝔽) 𝕋)))

1
sexprml.cabal

@ -32,6 +32,7 @@ library
, Simple.TC
, Simple.TC.Types
, Simple.TC.TypeOps
, Simple.CC
build-tool-depends: alex:alex >= 3.0, happy:happy >= 1.19.5
build-depends: base ^>=4.14.1.0
, array

4
src/Misc.hs

@ -13,3 +13,7 @@ infixl 6 <~>
-- | Swap the two elements of a pair
swap :: (a,b) -> (b,a)
swap (a,b) = (b,a)
-- | Two argument composition
(.:) :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
(.:) f g x y = f (g x y)

52
src/Simple/CC.hs

@ -0,0 +1,52 @@
{-|
Module: Simple.CC
Description: Case checker for the simple subset.
Checks pattern matching cases such that all cases are covered.
-}
{-# LANGUAGE LambdaCase #-}
module Simple.CC where
import Simple.TC.TypeOps
import Simple.TC.Types
import Simple.TC
import Simple.AST
import Types
import Error
import Control.Monad.State hiding (guard)
import Control.Monad.Except hiding (guard)
import Data.Map (Map)
import Data.Set (Set)
import qualified Data.Map as M
import qualified Data.Set as S
import Data.Foldable
toTree :: Type -> Pattern -> Check PatternTree
toTree t1 = \case
Wild _ -> pure PTW
PLit l -> inferLiteral l >>= \t2 -> guardt PTE (TypeMismatch (pos l) t1 t2) (t1 == t2)
PVar p i -> getCons >>= \cons -> case M.lookup i cons of
Just t2 -> guardt (PTC (M.fromList [(i, [])])) (TypeMismatch p t1 t2) (t1 == t2)
Nothing -> pure PTW -- pattern variable
PApp _ i [] -> throwError Urk -- should not happen (use nonempty lists)
PApp _ i ps -> getCons >>= \cons -> case M.lookup i cons of
Just t2 -> case typeList t2 of
[] -> throwError Urk -- should not happen (use nonempty lists)
_:[] -> throwError Urk -- TODO arity missmatch
xs@(_:_) -> (:[]) <$> sequenceA (zipWith toTree xs ps)
>>= \pts -> pure (PTC (M.fromList [(i, pts)]))
Nothing -> throwError Urk -- should not happen (use nonempty lists)
toTrees :: Type -> [Pattern] -> Check PatternTree
toTrees t ps = mapM (toTree t) ps >>= pure . fold
typeList :: Type -> [Type]
typeList (FuncType _ t1 t2) = t1 : typeList t2
typeList t = [t]
checkPatternTotal :: Type -> [Pattern] -> Check ()
checkPatternTotal t ps = toTrees t ps >>= \case
PTE -> throwError Urk -- TODO not total
PTW -> pure () -- all good!
PTC e -> undefined

27
src/Simple/TC.hs

@ -3,11 +3,9 @@ Module: Simple.TC
Description: Simple type checker.
A type checker for a simple subset of the language.
TODO: major refactor, split code accros modules
-}
{-# LANGUAGE LambdaCase, TupleSections #-}
module Simple.TC (runChecks, errorStr) where
module Simple.TC where
import Control.Monad.State hiding (guard)
import Control.Monad.Except hiding (guard)
@ -26,7 +24,7 @@ guard _ True = pure ()
guard e False = throwError e
-- | Error out on false and return given type on true.
guardt :: Type -> TypeError -> Bool -> Check Type
guardt :: a -> TypeError -> Bool -> Check a
guardt t _ True = pure t
guardt _ e False = throwError e
@ -44,12 +42,16 @@ tsToFunc p (t:ts) b = FuncType p t (tsToFunc p ts b)
-- totality checking of patterns in the future.
consOf :: Type -> Check [(Type, Identifier)]
consOf t = pure . filter (constructs t . fst) . map swap . M.toList =<< getEnv
where
-- | checks if second arg constructs first arg
constructs :: Type -> Type -> Bool
constructs t1 t2 | t1 == t2 = True
constructs t1 (FuncType _ _ t2) = constructs t1 t2
constructs _ _ = False
-- | checks if second arg constructs first arg
constructs :: Type -> Type -> Bool
constructs t1 t2 | t1 == t2 = True
constructs t1 (FuncType _ _ t2) = constructs t1 t2
constructs _ _ = False
-- | checks if second arg constructs first arg in the check monad
constructsM :: PN -> Type -> Type -> Check ()
constructsM p = guard (ConstructorMismatch p) .: constructs
-- | Check that expression has certain type. Error on fail, return type on success.
checkExpr :: Expr -> Type -> Check Type
@ -176,8 +178,11 @@ inferPattern target = \case
insertTLBinding :: TopLevel -> Check ()
insertTLBinding (Def p t i _ ) = insertUniqueBindings p [(t,i)]
insertTLBinding (Dat p i tis) = insertUniqueTypes p [i] >> insertUniqueBindings p tis
>> mapM_ (constructsM p (UsrType p i) . fst) tis
>> insertUniqueConstructors p tis
insertTLBinding (Rec p i tis) = insertUniqueTypes p [i] >> insertUniqueBindings p (constructor : deconstructors)
>> insertRecCons p i tis
>> insertRecCons p i tis
>> insertUniqueConstructors p [constructor]
where
constructor :: (Type, Identifier)
constructor = (tsToFunc p (fst <$> tis) curType, i)

15
src/Simple/TC/TypeOps.hs

@ -31,6 +31,10 @@ modState f = get >>= put . f
getEnv :: Check (Env Type)
getEnv = (^. defs) <$> get
-- | Get the value level enviornment
getCons :: Check (Env Type)
getCons = (^. constructors) <$> get
-- | Change value environment only for some computation.
localEnv :: (Env Type -> Env Type) -> Check a -> Check a
localEnv f = local (\env -> env & defs %~ f)
@ -39,6 +43,10 @@ localEnv f = local (\env -> env & defs %~ f)
modifyEnv :: (Env Type -> Env Type) -> Check ()
modifyEnv f = modState (\env -> env & defs %~ f)
-- | Modify the value environment
modifyCons :: (Env Type -> Env Type) -> Check ()
modifyCons f = modState (\env -> env & constructors %~ f)
-- | Modify the type environment
modifyTypeEnv :: (Set Identifier -> Set Identifier) -> Check ()
modifyTypeEnv f = modState (\env -> env & types %~ f)
@ -75,6 +83,13 @@ insertUniqueBindings p ais = getEnv >>= \env -> foldM go env ais >>= modifyEnv .
go e (a, i) | M.member i e = throwError (AlreadyBound p i)
| otherwise = pure (M.insert i a e)
insertUniqueConstructors :: PN -> [(Type, Identifier)] -> Check ()
insertUniqueConstructors p ais = getCons >>= \env -> foldM go env ais >>= modifyCons . const
where
go :: Env Type -> (Type, Identifier) -> Check (Env Type)
go e (a, i) | M.member i e = throwError (AlreadyBound p i)
| otherwise = pure (M.insert i a e)
-- | Bind some type names and make sure the names were not taken
insertUniqueTypes :: PN -> [Identifier] -> Check ()
insertUniqueTypes p is = getTypeEnv >>= \env -> foldM go env is >>= modifyTypeEnv . const

30
src/Simple/TC/Types.hs

@ -29,6 +29,7 @@ data TypeError
| UnboundVar PN Identifier
| AlreadyBound PN Identifier
| TypeAlreadyBound PN Identifier
| ConstructorMismatch PN
| NoCase PN
| UnknownPattern PN
| UndefinedType PN Identifier
@ -45,6 +46,7 @@ errorStr fp tx = \case
UnboundVar p i -> errorMessage p fp tx ("Unbound variable '" <> unId i <> "'")
AlreadyBound p i -> errorMessage p fp tx ("Identifier '" <> unId i <> "' already bound")
TypeAlreadyBound p i -> errorMessage p fp tx ("A type of name'" <> unId i <> "' already exists")
ConstructorMismatch p -> errorMessage p fp tx "Constructor does not construct correct type"
NoCase p -> errorMessage p fp tx "No case"
UnknownPattern p -> errorMessage p fp tx "Unknown pattern"
UndefinedType p i -> errorMessage p fp tx ("Undefined type '" <> unId i <> "'")
@ -55,17 +57,37 @@ errorStr fp tx = \case
type Env a = Map Identifier a
-- | The complete enviornment of the checker
data CheckEnv = CheckEnv { _defs :: Env Type
, _types :: Set Identifier
, _rec :: Env (Env Type)
data CheckEnv = CheckEnv { _defs :: Env Type
, _types :: Set Identifier
, _constructors :: Env Type
, _rec :: Env (Env Type)
} deriving Show
makeLenses ''CheckEnv
-- | The initial enviornment of the checker
initialState :: CheckEnv
initialState = CheckEnv M.empty S.empty M.empty
initialState = CheckEnv M.empty S.empty M.empty M.empty
-- | The monad which checking is performed in
newtype Check a = Check { runCheck :: StateT CheckEnv (ExceptT TypeError IO) a }
deriving (Functor, Applicative, Monad, MonadError TypeError, MonadState CheckEnv)
-- | Tree for analysing patterns. Maybe is for next arg
data PatternTree
= PTC (Env [[PatternTree]])
-- ^ Node with a constructor and patterns for each variable of the type
| PTW
-- ^ Wild match
| PTE
-- ^ Doesn't eliminate anything
instance Semigroup PatternTree where
x <> PTE = x
PTE <> x = x
_ <> PTW = PTW
PTW <> _ = PTW
PTC ipt1 <> PTC ipt2 = PTC (M.union ipt1 ipt2)
instance Monoid PatternTree where
mempty = PTE

Loading…
Cancel
Save