language-oberon-0.3.3: src/Language/Oberon/TypeChecker.hs
{-# LANGUAGE DataKinds, DeriveGeneric, DuplicateRecordFields, FlexibleContexts, FlexibleInstances,
MultiParamTypeClasses, NamedFieldPuns, OverloadedRecordDot, OverloadedStrings,
ScopedTypeVariables, StandaloneDeriving,
TypeFamilies, TypeOperators, UndecidableInstances, ViewPatterns #-}
-- | Type checker for Oberon AST. The AST must have its ambiguities previously resolved by "Language.Oberon.Resolver".
module Language.Oberon.TypeChecker (checkModules, errorMessage, Error(..), ErrorType(..), predefined, predefined2) where
import Control.Applicative (liftA2, (<|>), ZipList(ZipList, getZipList))
import Control.Arrow (first)
import Data.Coerce (coerce)
import Data.Proxy (Proxy(..))
import qualified Data.List as List
import Data.Functor.Const (Const(..))
import Data.Maybe (fromMaybe)
import Data.Map.Lazy (Map)
import qualified Data.Map.Lazy as Map
import Data.Semigroup (Semigroup(..))
import qualified Data.Text as Text
import GHC.Generics (Generic)
import qualified Rank2
import qualified Transformation
import qualified Transformation.Shallow as Shallow
import qualified Transformation.Deep as Deep
import qualified Transformation.Full as Full
import qualified Transformation.Full.TH
import qualified Transformation.AG as AG
import qualified Transformation.AG.Generics as AG
import Transformation.AG (Attribution(..), Atts, Inherited(..), Synthesized(..), Semantics)
import Transformation.AG.Generics (Auto(Auto), Folded(..), Bequether(..), Synthesizer(..), SynthesizedField)
import qualified Language.Oberon.Abstract as Abstract
import qualified Language.Oberon.AST as AST
import Language.Oberon.Grammar (ParsedLexemes(Trailing))
import Language.Oberon.Resolver (Placed)
data Type l = NominalType (Abstract.QualIdent l) (Maybe (Type l))
| RecordType{ancestry :: [Abstract.QualIdent l],
recordFields :: Map AST.Ident (Type l)}
| NilType
| IntegerType Int
| StringType Int
| ArrayType [Int] (Type l)
| PointerType (Type l)
| ReceiverType (Type l)
| ProcedureType Bool [(Bool, Type l)] (Maybe (Type l))
| BuiltinType Text.Text
| UnknownType
data ErrorType l = ArgumentCountMismatch Int Int
| ExtraDimensionalIndex Int Int
| IncomparableTypes (Type l) (Type l)
| IncompatibleTypes (Type l) (Type l)
| TooSmallArrayType Int Int
| OpenArrayVariable
| NonArrayType (Type l)
| NonBooleanType (Type l)
| NonFunctionType (Type l)
| NonIntegerType (Type l)
| NonNumericType (Type l)
| NonPointerType (Type l)
| NonProcedureType (Type l)
| NonRecordType (Type l)
| TypeMismatch (Type l) (Type l)
| UnequalTypes (Type l) (Type l)
| UnrealType (Type l)
| UnknownName (Abstract.QualIdent l)
| UnknownField AST.Ident (Type l)
data Error m l = Error{errorModule :: m,
errorPosition :: LexicalPosition,
errorType :: ErrorType l}
type LexicalPosition = (Int, ParsedLexemes, Int)
instance Eq (Abstract.QualIdent l) => Eq (Type l) where
NominalType q1 (Just t1) == t2@(NominalType q2 _) = q1 == q2 || t1 == t2
t1@(NominalType q1 _) == NominalType q2 (Just t2) = q1 == q2 || t1 == t2
NominalType q1 Nothing == NominalType q2 Nothing = q1 == q2
ArrayType [] t1 == ArrayType [] t2 = t1 == t2
ProcedureType _ p1 r1 == ProcedureType _ p2 r2 = r1 == r2 && p1 == p2
StringType len1 == StringType len2 = len1 == len2
NilType == NilType = True
BuiltinType name1 == BuiltinType name2 = name1 == name2
ReceiverType t1 == t2 = t1 == t2
t1 == ReceiverType t2 = t1 == t2
_ == _ = False
deriving instance Show (Abstract.QualIdent l) => Show (Type l)
deriving instance Eq (Abstract.QualIdent l) => Eq (ErrorType l)
deriving instance Show (Abstract.QualIdent l) => Show (ErrorType l)
deriving instance (Eq m, Eq (Abstract.QualIdent l)) => Eq (Error m l)
deriving instance (Show m, Show (Abstract.QualIdent l)) => Show (Error m l)
errorMessage :: (Abstract.Nameable l, Abstract.Oberon l, Show (Abstract.QualIdent l)) => ErrorType l -> String
errorMessage (ArgumentCountMismatch expected actual) =
"Expected " <> show expected <> ", received " <> show actual <> " arguments"
errorMessage (ExtraDimensionalIndex expected actual) =
"Expected " <> show expected <> ", received " <> show actual <> " indexes"
errorMessage (IncomparableTypes left right) =
"Values of types " <> typeMessage left <> " and " <> typeMessage right <> " cannot be compared"
errorMessage (IncompatibleTypes left right) =
"Incompatible types " <> typeMessage left <> " and " <> typeMessage right
errorMessage (TooSmallArrayType expected actual) =
"The array of length " <> show expected <> " cannot contain " <> show actual <> " items"
errorMessage OpenArrayVariable = "A variable cannot be declared an open array"
errorMessage (NonArrayType t) = "Trying to index a non-array type " <> typeMessage t
errorMessage (NonBooleanType t) = "Type " <> typeMessage t <> " is not Boolean"
errorMessage (NonFunctionType t) = "Trying to invoke a " <> typeMessage t <> " as a function"
errorMessage (NonIntegerType t) = "Type " <> typeMessage t <> " is not an integer type"
errorMessage (NonNumericType t) = "Type " <> typeMessage t <> " is not a numeric type"
errorMessage (NonPointerType t) = "Trying to dereference a non-pointer type " <> typeMessage t
errorMessage (NonProcedureType t) = "Trying to invoke a " <> typeMessage t <> " as a procedure"
errorMessage (NonRecordType t) = "Non-record type " <> typeMessage t
errorMessage (TypeMismatch t1 t2) = "Type mismatch between " <> typeMessage t1 <> " and " <> typeMessage t2
errorMessage (UnequalTypes t1 t2) = "Unequal types " <> typeMessage t1 <> " and " <> typeMessage t2
errorMessage (UnrealType t) = "Type " <> typeMessage t <> " is not a numeric real type"
errorMessage (UnknownName q) = "Unknown name " <> show q
errorMessage (UnknownField name t) = "Record type " <> typeMessage t <> " has no field " <> show name
typeMessage :: (Abstract.Nameable l, Abstract.Oberon l) => Type l -> String
typeMessage (BuiltinType name) = Text.unpack name
typeMessage (NominalType name _) = nameMessage name
typeMessage (RecordType ancestry fields) =
"RECORD " ++ foldMap (("(" ++) . (++ ") ") . nameMessage) ancestry
++ List.intercalate ";\n" (fieldMessage <$> Map.toList fields) ++ "END"
where fieldMessage (name, t) = "\n " <> Text.unpack name <> ": " <> typeMessage t
typeMessage (ArrayType dimensions itemType) =
"ARRAY " ++ List.intercalate ", " (show <$> dimensions) ++ " OF " ++ typeMessage itemType
typeMessage (PointerType targetType) = "POINTER TO " ++ typeMessage targetType
typeMessage (ProcedureType _ parameters result) =
"PROCEDURE (" ++ List.intercalate ", " (argMessage <$> parameters) ++ "): " ++ foldMap typeMessage result
where argMessage (True, t) = "VAR " <> typeMessage t
argMessage (False, t) = typeMessage t
typeMessage (ReceiverType t) = typeMessage t
typeMessage (IntegerType n) = "INTEGER"
typeMessage (StringType len) = "STRING [" ++ shows len "]"
typeMessage NilType = "NIL"
typeMessage UnknownType = "[Unknown]"
nameMessage :: (Abstract.Nameable l, Abstract.Oberon l) => Abstract.QualIdent l -> String
nameMessage q
| Just (mod, name) <- Abstract.getQualIdentNames q = Text.unpack mod <> "." <> Text.unpack name
| Just name <- Abstract.getNonQualIdentName q = Text.unpack name
type Environment l = Map (Abstract.QualIdent l) (Type l)
newtype Modules l f' f = Modules (Map AST.Ident (f (AST.Module l l f' f')))
data TypeCheck = TypeCheck
type Sem = Semantics (Auto TypeCheck)
data InhTCRoot l = InhTCRoot{rootEnv :: Environment l}
data InhTC l = InhTC{env :: Environment l}
deriving Generic
data InhTCExp l = InhTCExp{env :: Environment l,
expectedType :: Type l}
deriving Generic
data InhTCDecl l = InhTCDecl{env :: Environment l,
pointerTargets :: Map AST.Ident AST.Ident}
deriving Generic
data SynTC l = SynTC{errors :: Folded [Error () l]}
deriving Generic
data SynTCMods l = SynTCMods{errors :: Folded [Error AST.Ident l]}
deriving Generic
data SynTCMod l = SynTCMod{errors :: Folded [Error () l],
moduleEnv :: Environment l,
pointerTargets :: Folded (Map AST.Ident AST.Ident)}
deriving Generic
data SynTCType l = SynTCType{errors :: Folded [Error () l],
typeName :: Maybe AST.Ident,
definedType :: Type l,
pointerTarget :: Maybe AST.Ident}
deriving Generic
data SynTCFields l = SynTCFields{errors :: Folded [Error () l],
fieldEnv :: Map AST.Ident (Type l)}
deriving Generic
data SynTCHead l = SynTCHead{errors :: Folded [Error () l],
insideEnv :: Environment l,
outsideEnv :: Environment l}
deriving Generic
data SynTCSig l = SynTCSig{errors :: Folded [Error () l],
signatureEnv :: Environment l,
signatureType :: Type l}
deriving Generic
data SynTCSec l = SynTCSec{errors :: Folded [Error () l],
sectionEnv :: Environment l,
sectionParameters :: [(Bool, Type l)]}
deriving Generic
data SynTCDes l = SynTCDes{errors :: Folded [Error () l],
designatorName :: Maybe (Maybe Abstract.Ident, Abstract.Ident),
designatorType :: Type l}
deriving Generic
data SynTCExp l = SynTCExp{errors :: Folded [Error () l],
inferredType :: Type l}
deriving Generic
-- * Modules instances, TH candidates
instance (Transformation.Transformation t, Functor (Transformation.Domain t), Deep.Functor t (AST.Module l l),
Transformation.At t (AST.Module l l (Transformation.Codomain t) (Transformation.Codomain t))) =>
Deep.Functor t (Modules l) where
t <$> ~(Modules ms) = Modules (mapModule <$> ms)
where mapModule m = t Transformation.$ ((t Deep.<$>) <$> m)
instance (Transformation.Transformation t, Functor (Transformation.Domain t),
Transformation.At t (AST.Module l l f f)) =>
Shallow.Functor t (Modules l f) where
t <$> ~(Modules ms) = Modules ((t Transformation.$) <$> ms)
instance (Transformation.Transformation t, Functor (Transformation.Domain t), Shallow.Foldable t (AST.Module l l f),
Transformation.At t (AST.Module l l f f)) =>
Shallow.Foldable t (Modules l f) where
foldMap t ~(Modules ms) = getConst (foldMap (t Transformation.$) ms)
instance Rank2.Functor (Modules l f') where
f <$> ~(Modules ms) = Modules (f <$> ms)
instance Rank2.Foldable (Modules l f) where
foldMap f ~(Modules ms) = foldMap f ms
instance Rank2.Apply (Modules l f') where
~(Modules fs) <*> ~(Modules ms) = Modules (Map.intersectionWith Rank2.apply fs ms)
-- * Boring attribute types
type instance Atts (Inherited TypeCheck) (Modules l _ _) = InhTCRoot l
type instance Atts (Synthesized TypeCheck) (Modules l _ _) = SynTCMods l
type instance Atts (Inherited TypeCheck) (AST.Module l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.Module l l _ _) = SynTCMod l
type instance Atts (Inherited TypeCheck) (AST.Declaration l l _ _) = InhTCDecl l
type instance Atts (Synthesized TypeCheck) (AST.Declaration l l _ _) = SynTCMod l
type instance Atts (Inherited TypeCheck) (AST.ProcedureHeading l l _ _) = InhTCDecl l
type instance Atts (Synthesized TypeCheck) (AST.ProcedureHeading l l _ _) = SynTCHead l
type instance Atts (Inherited TypeCheck) (AST.Block l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.Block l l _ _) = SynTCMod l
type instance Atts (Inherited TypeCheck) (AST.FormalParameters l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.FormalParameters l l _ _) = SynTCSig l
type instance Atts (Inherited TypeCheck) (AST.FPSection l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.FPSection l l _ _) = SynTCSec l
type instance Atts (Inherited TypeCheck) (AST.Type l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.Type l l _ _) = SynTCType l
type instance Atts (Inherited TypeCheck) (AST.FieldList l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.FieldList l l _ _) = SynTCFields l
type instance Atts (Inherited TypeCheck) (AST.StatementSequence l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.StatementSequence l l _ _) = SynTC l
type instance Atts (Inherited TypeCheck) (AST.Expression l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.Expression l l _ _) = SynTCExp l
type instance Atts (Inherited TypeCheck) (AST.Element l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.Element l l _ _) = SynTCExp l
type instance Atts (Inherited TypeCheck) (AST.Value l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.Value l l _ _) = SynTCExp l
type instance Atts (Inherited TypeCheck) (AST.Designator l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.Designator l l _ _) = SynTCDes l
type instance Atts (Inherited TypeCheck) (AST.Statement l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.Statement l l _ _) = SynTC l
type instance Atts (Inherited TypeCheck) (AST.ConditionalBranch l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.ConditionalBranch l l _ _) = SynTC l
type instance Atts (Inherited TypeCheck) (AST.Case l l _ _) = InhTCExp l
type instance Atts (Synthesized TypeCheck) (AST.Case l l _ _) = SynTC l
type instance Atts (Inherited TypeCheck) (AST.CaseLabels l l _ _) = InhTCExp l
type instance Atts (Synthesized TypeCheck) (AST.CaseLabels l l _ _) = SynTC l
type instance Atts (Inherited TypeCheck) (AST.WithAlternative l l _ _) = InhTC l
type instance Atts (Synthesized TypeCheck) (AST.WithAlternative l l _ _) = SynTC l
-- * Rules
instance Ord (Abstract.QualIdent l) => Bequether (Auto TypeCheck) (Modules l) Sem Placed where
bequest _ (_, Modules self) inheritance (Modules ms) =
Modules (Map.mapWithKey moduleInheritance self)
where moduleInheritance name mod = Inherited InhTC{env= rootEnv inheritance <> foldMap (moduleEnv . syn) ms}
instance Ord (Abstract.QualIdent l) => Synthesizer (Auto TypeCheck) (Modules l) Sem Placed where
synthesis _ _ _ (Modules ms) = SynTCMods{errors= Map.foldMapWithKey moduleErrors ms}
where moduleErrors name (Synthesized SynTCMod{errors= Folded errs}) =
Folded [Error name pos t | Error () pos t <- errs]
instance (Abstract.Oberon l, Abstract.Nameable l, k ~ Abstract.QualIdent l, Ord k,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Block l l Sem Sem) ~ SynTCMod l) =>
SynthesizedField "moduleEnv" (Map k (Type l)) (Auto TypeCheck) (AST.Module l l) Sem Placed where
synthesizedField _ _ (pos, AST.Module moduleName imports body) _inheritance (AST.Module _ _ body') = exportedEnv
where exportedEnv = exportNominal <$> Map.mapKeysMonotonic export (moduleEnv $ syn body')
export q
| Just name <- Abstract.getNonQualIdentName q = Abstract.qualIdent moduleName name
| otherwise = q
exportNominal (NominalType q (Just t))
| Just name <- Abstract.getNonQualIdentName q =
NominalType (Abstract.qualIdent moduleName name) (Just $ exportNominal' t)
exportNominal t = exportNominal' t
exportNominal' (RecordType ancestry fields) = RecordType (export <$> ancestry) (exportNominal' <$> fields)
exportNominal' (ProcedureType False parameters result) =
ProcedureType False ((exportNominal' <$>) <$> parameters) (exportNominal' <$> result)
exportNominal' (PointerType target) = PointerType (exportNominal' target)
exportNominal' (ArrayType dimensions itemType) = ArrayType dimensions (exportNominal' itemType)
exportNominal' (NominalType q (Just t))
| Just name <- Abstract.getNonQualIdentName q =
fromMaybe (NominalType (Abstract.qualIdent moduleName name) $ Just $ exportNominal' t)
(Map.lookup q exportedEnv)
exportNominal' t = t
instance (Abstract.Nameable l, Ord (Abstract.QualIdent l),
Atts (Inherited (Auto TypeCheck)) (Abstract.Type l l Sem Sem) ~ InhTC l,
Atts (Inherited (Auto TypeCheck)) (Abstract.ProcedureHeading l l Sem Sem) ~ InhTCDecl l,
Atts (Inherited (Auto TypeCheck)) (Abstract.Block l l Sem Sem) ~ InhTC l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.ProcedureHeading l l Sem Sem) ~ SynTCHead l,
Atts (Inherited (Auto TypeCheck)) (Abstract.FormalParameters l l Sem Sem) ~ InhTC l,
Atts (Inherited (Auto TypeCheck)) (Abstract.ConstExpression l l Sem Sem) ~ InhTC l) =>
Bequether (Auto TypeCheck) (AST.Declaration l l) Sem Placed where
bequest _ (pos, AST.ProcedureDeclaration{})
inheritance@InhTCDecl{env= declEnv} (AST.ProcedureDeclaration heading _body) =
AST.ProcedureDeclaration (Inherited inheritance) (Inherited bodyInherited)
where bodyInherited = InhTC{env= insideEnv (syn heading) `Map.union` declEnv}
bequest t local inheritance synthesized = AG.bequestDefault t local inheritance synthesized
instance (Abstract.Nameable l, k ~ Abstract.QualIdent l, Ord k,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Declaration l l Sem Sem) ~ SynTCMod l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Type l l Sem Sem) ~ SynTCType l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.FormalParameters l l Sem Sem) ~ SynTCSig l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.ProcedureHeading l l Sem Sem) ~ SynTCHead l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.ConstExpression l l Sem Sem) ~ SynTCExp l) =>
SynthesizedField "moduleEnv" (Map k (Type l)) (Auto TypeCheck) (AST.Declaration l l) Sem Placed where
synthesizedField _ _ (pos, AST.ConstantDeclaration namedef _) _ (AST.ConstantDeclaration _ expression) =
Map.singleton (Abstract.nonQualIdent $ Abstract.getIdentDefName namedef) (inferredType $ syn expression)
synthesizedField _ _ (pos, AST.TypeDeclaration namedef _) _ (AST.TypeDeclaration _ definition) =
Map.singleton qname (nominal $ definedType $ syn definition)
where nominal t@BuiltinType{} = t
nominal t@NominalType{} = t
nominal (PointerType t@RecordType{}) =
NominalType qname (Just $ PointerType $ NominalType (Abstract.nonQualIdent $ name<>"^") (Just t))
nominal t = NominalType qname (Just t)
qname = Abstract.nonQualIdent name
name = Abstract.getIdentDefName namedef
synthesizedField _ _ (pos, AST.VariableDeclaration names _) _ (AST.VariableDeclaration _names declaredType) =
foldMap binding names
where binding name = Map.singleton (Abstract.nonQualIdent $ Abstract.getIdentDefName name)
(definedType $ syn declaredType)
synthesizedField _ _ (pos, AST.ProcedureDeclaration{}) _ (AST.ProcedureDeclaration heading body) =
outsideEnv (syn heading)
synthesizedField _ _ (pos, AST.ForwardDeclaration namedef _sig) _ (AST.ForwardDeclaration _namedef sig) =
foldMap (Map.singleton (Abstract.nonQualIdent $ Abstract.getIdentDefName namedef) . signatureType . syn) sig
instance (Abstract.Nameable l, k ~ Abstract.QualIdent l, Ord k,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Type l l Sem Sem) ~ SynTCType l) =>
SynthesizedField "pointerTargets" (Folded (Map AST.Ident AST.Ident)) (Auto TypeCheck)
(AST.Declaration l l) Sem Placed where
synthesizedField _ _ (pos, AST.TypeDeclaration namedef _) _ (AST.TypeDeclaration _ definition) =
foldMap (Folded . Map.singleton name) (pointerTarget $ syn definition)
where name = Abstract.getIdentDefName namedef
synthesizedField _ _ _ _ _ = mempty
instance (Abstract.Nameable l, Ord (Abstract.QualIdent l),
Atts (Synthesized (Auto TypeCheck)) (Abstract.FormalParameters l l Sem Sem) ~ SynTCSig l) =>
Synthesizer (Auto TypeCheck) (AST.ProcedureHeading l l) Sem Placed where
synthesis _ (pos, AST.ProcedureHeading indirect namedef _sig) _inheritance (AST.ProcedureHeading _indirect _ sig) =
SynTCHead{errors= foldMap ((.errors) . syn) sig,
outsideEnv= Map.singleton (Abstract.nonQualIdent name) $
maybe (ProcedureType False [] Nothing) (signatureType . syn) sig,
insideEnv= foldMap (signatureEnv . syn) sig}
where name = Abstract.getIdentDefName namedef
synthesis _ (pos, AST.TypeBoundHeading var receiverName receiverType indirect namedef _sig)
InhTCDecl{env, pointerTargets} (AST.TypeBoundHeading _var _name _type _indirect _ sig) =
SynTCHead{errors= receiverError <> foldMap ((.errors) . syn) sig,
outsideEnv= case Map.lookup receiverType pointerTargets
of Just targetName -> Map.singleton (Abstract.nonQualIdent targetName) methodType
Nothing -> Map.singleton (Abstract.nonQualIdent receiverType) methodType,
insideEnv= receiverEnv `Map.union` foldMap (signatureEnv . syn) sig}
where receiverEnv =
foldMap (Map.singleton (Abstract.nonQualIdent receiverName) . ReceiverType)
(Map.lookup (Abstract.nonQualIdent receiverType) env)
methodType = NominalType (Abstract.nonQualIdent "")
(Just $ RecordType [] $ Map.singleton name procedureType)
name = Abstract.getIdentDefName namedef
procedureType = maybe (ProcedureType False [] Nothing) (signatureType . syn) sig
receiverError =
case Map.lookup (Abstract.nonQualIdent receiverType) env
of Nothing -> Folded [Error () pos (UnknownName $ Abstract.nonQualIdent receiverType)]
Just t
| RecordType{} <- ultimate t -> mempty
| PointerType t' <- ultimate t, RecordType{} <- ultimate t' -> mempty
| otherwise -> Folded [Error () pos (NonRecordType t)]
instance (Abstract.Nameable l, Ord (Abstract.QualIdent l), Show (Abstract.QualIdent l),
Atts (Synthesized (Auto TypeCheck)) (Abstract.Declaration l l Sem Sem) ~ SynTCMod l,
Atts (Inherited (Auto TypeCheck)) (Abstract.Declaration l l Sem Sem) ~ InhTCDecl l,
Atts (Inherited (Auto TypeCheck)) (Abstract.StatementSequence l l Sem Sem) ~ InhTC l) =>
Bequether (Auto TypeCheck) (AST.Block l l) Sem Placed where
bequest _ (pos, AST.Block{}) inheritance@InhTC{env} (AST.Block declarations _statements) =
AST.Block (pure $ Inherited InhTCDecl{env= localEnv,
pointerTargets= getFolded pointers})
(pure $ Inherited localInheritance)
where localInheritance :: InhTC l
localInheritance = inheritance{env= localEnv}
localEnv = newEnv declarations <> env
pointers= foldMap (\Synthesized{syn= SynTCMod{pointerTargets= ptrs}}-> ptrs) declarations
instance (Abstract.Nameable l, k ~ Abstract.QualIdent l, Ord k, Show k,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Declaration l l Sem Sem) ~ SynTCMod l) =>
SynthesizedField "moduleEnv" (Map k (Type l)) (Auto TypeCheck) (AST.Block l l) Sem Placed where
synthesizedField _ _ (pos, AST.Block{}) _inheritance (AST.Block declarations _statements) = newEnv declarations
newEnv :: (Abstract.Nameable l, Ord (Abstract.QualIdent l), Show (Abstract.QualIdent l),
Atts (Synthesized (Auto TypeCheck)) (Abstract.Declaration l l Sem Sem) ~ SynTCMod l) =>
ZipList (Synthesized (Auto TypeCheck) (Abstract.Declaration l l Sem Sem)) -> Environment l
newEnv declarations = Map.unionsWith mergeTypeBoundProcedures (moduleEnv . syn <$> declarations)
where mergeTypeBoundProcedures (NominalType q (Just t1)) t2
| Abstract.getNonQualIdentName q == Just "" = mergeTypeBoundProcedures t1 t2
| otherwise = NominalType q (Just $ mergeTypeBoundProcedures t1 t2)
mergeTypeBoundProcedures t1 (NominalType q (Just t2))
| Abstract.getNonQualIdentName q == Just "" = mergeTypeBoundProcedures t1 t2
| otherwise = NominalType q (Just $ mergeTypeBoundProcedures t1 t2)
mergeTypeBoundProcedures (RecordType ancestry1 fields1) (RecordType ancestry2 fields2) =
RecordType (ancestry1 <> ancestry2) (fields1 <> fields2)
mergeTypeBoundProcedures (PointerType (RecordType ancestry1 fields1)) (RecordType ancestry2 fields2) =
PointerType (RecordType (ancestry1 <> ancestry2) (fields1 <> fields2))
mergeTypeBoundProcedures (RecordType ancestry1 fields1) (PointerType (RecordType ancestry2 fields2)) =
PointerType (RecordType (ancestry1 <> ancestry2) (fields1 <> fields2))
mergeTypeBoundProcedures (PointerType (NominalType q (Just (RecordType ancestry1 fields1))))
(RecordType ancestry2 fields2) =
PointerType (NominalType q $ Just $ RecordType (ancestry1 <> ancestry2) (fields1 <> fields2))
mergeTypeBoundProcedures (RecordType ancestry1 fields1)
(PointerType (NominalType q (Just (RecordType ancestry2 fields2)))) =
PointerType (NominalType q $ Just $ RecordType (ancestry1 <> ancestry2) (fields1 <> fields2))
mergeTypeBoundProcedures t1 t2 = error (take 90 $ show t1)
instance (Ord (Abstract.QualIdent l),
Atts (Synthesized (Auto TypeCheck)) (Abstract.FPSection l l Sem Sem) ~ SynTCSec l) =>
Synthesizer (Auto TypeCheck) (AST.FormalParameters l l) Sem Placed where
synthesis _ (pos, AST.FormalParameters sections returnType) InhTC{env}
(AST.FormalParameters sections' _) =
SynTCSig{errors= foldMap ((.errors) . syn) sections' <> foldMap typeRefErrors returnType,
signatureType= ProcedureType False (foldMap (sectionParameters . syn) sections')
$ returnType >>= (`Map.lookup` env),
signatureEnv= foldMap (sectionEnv . syn) sections'}
where typeRefErrors q
| Map.member q env = mempty
| otherwise = Folded [Error () pos (UnknownName q)]
instance (Abstract.Wirthy l, Ord (Abstract.QualIdent l),
Atts (Synthesized (Auto TypeCheck)) (Abstract.Type l l Sem Sem) ~ SynTCType l) =>
Synthesizer (Auto TypeCheck) (AST.FPSection l l) Sem Placed where
synthesis _ (pos, AST.FPSection var names _typeDef) _inheritance (AST.FPSection _var _names typeDef) =
SynTCSec{errors= (syn typeDef).errors,
sectionParameters= (var, definedType (syn typeDef)) <$ names,
sectionEnv= Map.fromList (flip (,) (definedType $ syn typeDef) . Abstract.nonQualIdent <$> names)}
instance (Abstract.Nameable l, Ord (Abstract.QualIdent l),
Atts (Synthesized (Auto TypeCheck)) (Abstract.FormalParameters l l Sem Sem) ~ SynTCSig l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.FieldList l l Sem Sem) ~ SynTCFields l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Type l l Sem Sem) ~ SynTCType l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.ConstExpression l l Sem Sem) ~ SynTCExp l) =>
Synthesizer (Auto TypeCheck) (AST.Type l l) Sem Placed where
synthesis _ (pos, AST.TypeReference q) InhTC{env} _ =
SynTCType{errors= if Map.member q env then mempty else Folded [Error () pos (UnknownName q)],
typeName= Abstract.getNonQualIdentName q,
pointerTarget= Nothing,
definedType= fromMaybe UnknownType (Map.lookup q env)}
synthesis _ (pos, AST.ArrayType _dims _itemType) InhTC{} (AST.ArrayType dimensions itemType) =
SynTCType{errors= foldMap ((.errors) . syn) dimensions
<> (syn itemType).errors
<> foldMap (expectInteger . syn) dimensions,
typeName= Nothing,
pointerTarget= Nothing,
definedType= ArrayType (integerValue . syn <$> getZipList dimensions) (definedType $ syn itemType)}
where expectInteger SynTCExp{inferredType= IntegerType{}} = mempty
expectInteger SynTCExp{inferredType= t} = Folded [Error () pos (NonIntegerType t)]
integerValue SynTCExp{inferredType= IntegerType n} = n
integerValue _ = 0
synthesis _ (pos, AST.RecordType base fields) InhTC{env} (AST.RecordType _base fields') =
SynTCType{errors= fst baseRecord <> foldMap ((.errors) . syn) fields',
typeName= Nothing,
pointerTarget= Nothing,
definedType= RecordType (maybe [] (maybe id (:) base . ancestry) $ snd baseRecord)
(maybe Map.empty recordFields (snd baseRecord)
<> foldMap (fieldEnv . syn) fields')}
where baseRecord = case flip Map.lookup env <$> base
of Just (Just t@RecordType{}) -> (mempty, Just t)
Just (Just (NominalType _ (Just t@RecordType{}))) -> (mempty, Just t)
Just (Just t) -> (Folded [Error () pos (NonRecordType t)], Nothing)
Just Nothing ->
(foldMap (Folded . (:[]) . Error () pos . UnknownName) base, Nothing)
Nothing -> (mempty, Nothing)
synthesis (Auto TypeCheck) _self _inheritance (AST.PointerType targetType') =
SynTCType{errors= (syn targetType').errors,
typeName= Nothing,
pointerTarget= typeName (syn targetType'),
definedType= PointerType (definedType $ syn targetType')}
synthesis _ (pos, AST.ProcedureType signature) _inheritance (AST.ProcedureType signature') =
SynTCType{errors= foldMap ((.errors) . syn) signature',
typeName= Nothing,
pointerTarget= Nothing,
definedType= maybe (ProcedureType False [] Nothing) (signatureType . syn) signature'}
instance (Abstract.Nameable l, Atts (Synthesized (Auto TypeCheck)) (Abstract.Type l l Sem Sem) ~ SynTCType l) =>
SynthesizedField "fieldEnv" (Map AST.Ident (Type l)) (Auto TypeCheck) (AST.FieldList l l) Sem Placed where
synthesizedField _ _ (_, AST.FieldList names _declaredType) _inheritance (AST.FieldList _names declaredType) =
foldMap (\name-> Map.singleton (Abstract.getIdentDefName name) (definedType $ syn declaredType)) names
instance (Abstract.Wirthy l, Abstract.Nameable l, Ord (Abstract.QualIdent l),
Atts (Inherited (Auto TypeCheck)) (Abstract.StatementSequence l l Sem Sem) ~ InhTC l,
Atts (Inherited (Auto TypeCheck)) (Abstract.ConditionalBranch l l Sem Sem) ~ InhTC l,
Atts (Inherited (Auto TypeCheck)) (Abstract.Case l l Sem Sem) ~ InhTCExp l,
Atts (Inherited (Auto TypeCheck)) (Abstract.WithAlternative l l Sem Sem) ~ InhTC l,
Atts (Inherited (Auto TypeCheck)) (Abstract.Expression l l Sem Sem) ~ InhTC l,
Atts (Inherited (Auto TypeCheck)) (Abstract.Designator l l Sem Sem) ~ InhTC l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Expression l l Sem Sem) ~ SynTCExp l) =>
Bequether (Auto TypeCheck) (AST.Statement l l) Sem Placed where
bequest _ (_pos, AST.CaseStatement{}) i@InhTC{env} (AST.CaseStatement value _branches _fallback) =
AST.CaseStatement (Inherited i) (pure $ Inherited InhTCExp{env= env,
expectedType= inferredType $ syn value})
(Just $ Inherited i)
bequest _ (_pos, statement) InhTC{env} _ =
AG.passDown InhTCExp{env= env,
expectedType= error "No statement except CASE needs expectedType"} statement
instance {-# overlaps #-} (Abstract.Wirthy l, Abstract.Nameable l, Ord (Abstract.QualIdent l),
Atts (Synthesized (Auto TypeCheck)) (Abstract.StatementSequence l l Sem Sem) ~ SynTC l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Expression l l Sem Sem) ~ SynTCExp l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Designator l l Sem Sem) ~ SynTCDes l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Case l l Sem Sem) ~ SynTC l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.ConditionalBranch l l Sem Sem) ~ SynTC l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.WithAlternative l l Sem Sem) ~ SynTC l) =>
Synthesizer (Auto TypeCheck) (AST.Statement l l) Sem Placed where
synthesis t (pos, _) InhTC{} statement@(AST.Assignment var value) =
{-# SCC "Assignment" #-}
SynTC{errors= assignmentCompatible pos (designatorType $ syn var) (inferredType $ syn value)
<> AG.foldedField (Proxy :: Proxy "errors") t statement}
synthesis _ (pos, AST.ProcedureCall _proc parameters) _inheritance (AST.ProcedureCall procedure' parameters') =
SynTC{errors= (case syn procedure'
of SynTCDes{errors= Folded [],
designatorType= t} -> procedureErrors t
SynTCDes{errors= errs} -> errs)
<> foldMap (foldMap ((.errors) . syn)) parameters'}
where procedureErrors (ProcedureType _ formalTypes Nothing)
| length formalTypes /= maybe 0 (length . getZipList) parameters,
not (length formalTypes == 2 && (length . getZipList <$> parameters) == Just 1
&& designatorName (syn procedure') == Just (Nothing, "ASSERT")
|| length formalTypes == 1 && (length . getZipList <$> parameters) == Just 2
&& designatorName (syn procedure') == Just (Nothing, "NEW")
&& all (all (isIntegerType . inferredType . syn) . tail . getZipList) parameters') =
Folded [Error () pos
$ ArgumentCountMismatch (length formalTypes) $ maybe 0 (length . getZipList) parameters]
| otherwise = mconcat (zipWith (parameterCompatible pos) formalTypes
$ maybe [] ((inferredType . syn <$>) . getZipList) parameters')
procedureErrors (NominalType _ (Just t)) = procedureErrors t
procedureErrors t = Folded [Error () pos (NonProcedureType t)]
synthesis _ (pos, _) _inheritance (AST.While condition body) =
SynTC{errors= booleanExpressionErrors pos (syn condition) <> (syn body).errors}
synthesis _ (pos, _) _inheritance (AST.Repeat body condition) =
SynTC{errors= booleanExpressionErrors pos (syn condition) <> (syn body).errors}
synthesis _ (pos, _) _inheritance (AST.For _counter start end step body) =
SynTC{errors= integerExpressionErrors pos (syn start)
<> integerExpressionErrors pos (syn end)
<> foldMap (integerExpressionErrors pos . syn) step <> (syn body).errors}
synthesis t self _ statement = SynTC{errors= AG.foldedField (Proxy :: Proxy "errors") t statement}
instance (Abstract.Nameable l, Ord (Abstract.QualIdent l),
Atts (Inherited (Auto TypeCheck)) (Abstract.StatementSequence l l Sem Sem) ~ InhTC l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.StatementSequence l l Sem Sem) ~ SynTC l) =>
Attribution (Auto TypeCheck) (AST.WithAlternative l l) Sem Placed where
attribution _ (pos, AST.WithAlternative var subtype _body)
(Inherited InhTC{env},
AST.WithAlternative _var _subtype body) =
(Synthesized SynTC{errors= case (Map.lookup var env, Map.lookup subtype env)
of (Just supertype, Just subtypeDef) ->
assignmentCompatible pos supertype subtypeDef
(Nothing, _) -> Folded [Error () pos (UnknownName var)]
(_, Nothing) -> Folded [Error () pos (UnknownName subtype)]
<> (syn body).errors},
AST.WithAlternative var subtype (Inherited $ InhTC $ maybe id (Map.insert var) (Map.lookup subtype env) env))
instance (Abstract.Nameable l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Expression l l Sem Sem) ~ SynTCExp l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.StatementSequence l l Sem Sem) ~ SynTC l) =>
Synthesizer (Auto TypeCheck) (AST.ConditionalBranch l l) Sem Placed where
synthesis _ (pos, _) _inheritance (AST.ConditionalBranch condition body) =
SynTC{errors= booleanExpressionErrors pos (syn condition) <> (syn body).errors}
instance {-# overlaps #-} (Abstract.Nameable l, Eq (Abstract.QualIdent l),
Atts (Synthesized (Auto TypeCheck)) (Abstract.ConstExpression l l Sem Sem) ~ SynTCExp l) =>
Synthesizer (Auto TypeCheck) (AST.CaseLabels l l) Sem Placed where
synthesis _ (pos, _) inheritance (AST.SingleLabel value) =
SynTC{errors= assignmentCompatibleIn inheritance pos (inferredType $ syn value)}
synthesis _ (pos, _) inheritance (AST.LabelRange start end) =
SynTC{errors= assignmentCompatibleIn inheritance pos (inferredType $ syn start)
<> assignmentCompatibleIn inheritance pos (inferredType $ syn end)}
instance {-# overlaps #-} (Abstract.Nameable l, Ord (Abstract.QualIdent l),
Atts (Inherited (Auto TypeCheck)) (Abstract.Expression l l Sem Sem) ~ InhTC l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Expression l l Sem Sem) ~ SynTCExp l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Element l l Sem Sem) ~ SynTCExp l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Value l l Sem Sem) ~ SynTCExp l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Designator l l Sem Sem) ~ SynTCDes l) =>
Synthesizer (Auto TypeCheck) (AST.Expression l l) Sem Placed where
synthesis _ (pos, AST.Relation op _ _) InhTC{} (AST.Relation _op left right) =
SynTCExp{errors= case (syn left).errors <> (syn right).errors
of Folded []
| t1 == t2 -> mempty
| AST.In <- op -> membershipCompatible (ultimate t1) (ultimate t2)
| equality op,
Folded [] <- assignmentCompatible pos t1 t2
-> mempty
| equality op,
Folded [] <- assignmentCompatible pos t2 t1
-> mempty
| otherwise -> comparable (ultimate t1) (ultimate t2)
errs -> errs,
inferredType= BuiltinType "BOOLEAN"}
where t1 = inferredType (syn left)
t2 = inferredType (syn right)
equality AST.Equal = True
equality AST.Unequal = True
equality _ = False
comparable (BuiltinType "BOOLEAN") (BuiltinType "BOOLEAN") = mempty
comparable (BuiltinType "CHAR") (BuiltinType "CHAR") = mempty
comparable StringType{} StringType{} = mempty
comparable (StringType 1) (BuiltinType "CHAR") = mempty
comparable (BuiltinType "CHAR") (StringType 1) = mempty
comparable StringType{} (ArrayType _ (BuiltinType "CHAR")) = mempty
comparable (ArrayType _ (BuiltinType "CHAR")) StringType{} = mempty
comparable (ArrayType _ (BuiltinType "CHAR")) (ArrayType _ (BuiltinType "CHAR")) = mempty
comparable (BuiltinType t1) (BuiltinType t2)
| isNumerical t1 && isNumerical t2 = mempty
comparable (BuiltinType t1) IntegerType{}
| isNumerical t1 = mempty
comparable IntegerType{} (BuiltinType t2)
| isNumerical t2 = mempty
comparable t1 t2 = Folded [Error () pos (IncomparableTypes t1 t2)]
membershipCompatible IntegerType{} (BuiltinType "SET") = mempty
membershipCompatible (BuiltinType t1) (BuiltinType "SET")
| isNumerical t1 = mempty
synthesis _ (pos, AST.IsA _ q) InhTC{env} (AST.IsA left _) =
SynTCExp{errors= case Map.lookup q env
of Nothing -> Folded [Error () pos (UnknownName q)]
Just t -> assignmentCompatible pos (inferredType $ syn left) t,
inferredType= BuiltinType "BOOLEAN"}
synthesis _ (pos, _) _inheritance (AST.Positive expr) =
SynTCExp{errors= unaryNumericOrSetOperatorErrors pos (syn expr),
inferredType= inferredType (syn expr)}
synthesis _ (pos, _) _inheritance (AST.Negative expr) =
SynTCExp{errors= unaryNumericOrSetOperatorErrors pos (syn expr),
inferredType= unaryNumericOrSetOperatorType negate (syn expr)}
synthesis _ (pos, _) _inheritance (AST.Add left right) = binaryNumericOrSetSynthesis pos left right
synthesis _ (pos, _) _inheritance (AST.Subtract left right) = binaryNumericOrSetSynthesis pos left right
synthesis _ (pos, _) _inheritance (AST.Or left right) = binaryBooleanSynthesis pos left right
synthesis _ (pos, _) _inheritance (AST.Multiply left right) = binaryNumericOrSetSynthesis pos left right
synthesis _ (pos, _) InhTC{} (AST.Divide left right) =
SynTCExp{errors=
case (syn left, syn right)
of (SynTCExp{errors= Folded [], inferredType= BuiltinType t1},
SynTCExp{errors= Folded [], inferredType= BuiltinType t2})
| t1 == "REAL", t2 == "REAL" -> mempty
| t1 == "SET", t2 == "SET" -> mempty
(SynTCExp{errors= Folded [], inferredType= t1},
SynTCExp{errors= Folded [], inferredType= t2})
| t1 == t2 -> Folded [Error () pos (UnrealType t1)]
| otherwise -> Folded [Error () pos (TypeMismatch t1 t2)],
inferredType= BuiltinType "REAL"}
synthesis _ (pos, _) _inheritance (AST.IntegerDivide left right) = binaryIntegerSynthesis pos left right
synthesis _ (pos, _) _inheritance (AST.Modulo left right) = binaryIntegerSynthesis pos left right
synthesis _ (pos, _) _inheritance (AST.And left right) = binaryBooleanSynthesis pos left right
synthesis (Auto TypeCheck) _self _ (AST.Set elements) =
SynTCExp{errors= mempty,
inferredType= BuiltinType "SET"}
synthesis (Auto TypeCheck) _self _ (AST.Read designator) =
SynTCExp{errors= (syn designator).errors,
inferredType= designatorType (syn designator)}
synthesis (Auto TypeCheck) _self _ (AST.Literal value) =
SynTCExp{errors= (syn value).errors,
inferredType= inferredType (syn value)}
synthesis _ (pos, AST.FunctionCall _designator (ZipList parameters)) _inheritance
(AST.FunctionCall designator (ZipList parameters')) =
SynTCExp{errors=
case {-# SCC "FunctionCall" #-} syn designator
of SynTCDes{errors= Folded [],
designatorName= name,
designatorType= ultimate -> ProcedureType _ formalTypes Just{}}
| length formalTypes /= length parameters ->
Folded [Error () pos
$ ArgumentCountMismatch (length formalTypes) (length parameters)]
| name == Just (Just "SYSTEM", "VAL") -> mempty
| otherwise -> mconcat (zipWith (parameterCompatible pos) formalTypes
$ inferredType . syn <$> parameters')
SynTCDes{errors= Folded [],
designatorType= t} -> Folded [Error () pos (NonFunctionType t)]
SynTCDes{errors= errs} -> errs
<> foldMap ((.errors) . syn) parameters',
inferredType=
case syn designator
of SynTCDes{designatorName= Just (Just "SYSTEM", name)}
| Just t <- systemCallType name (inferredType . syn <$> parameters') -> t
SynTCDes{designatorName= d, designatorType= t}
| ProcedureType _ _ (Just returnType) <- ultimate t -> returnType
_ -> UnknownType}
where systemCallType "VAL" [t1, t2] = Just t1
systemCallType _ _ = Nothing
synthesis _ (pos, _) _inheritance (AST.Not expr) =
SynTCExp{errors= booleanExpressionErrors pos (syn expr),
inferredType= BuiltinType "BOOLEAN"}
instance Abstract.Wirthy l => SynthesizedField "inferredType" (Type l) (Auto TypeCheck) (AST.Value l l) Sem Placed where
synthesizedField _ _ (_, AST.Integer x) _ _ = IntegerType (fromIntegral x)
synthesizedField _ _ (_, AST.Real x) _ _ = BuiltinType "REAL"
synthesizedField _ _ (_, AST.Boolean x) _ _ = BuiltinType "BOOLEAN"
synthesizedField _ _ (_, AST.CharCode x) _ _ = BuiltinType "CHAR"
synthesizedField _ _ (_, AST.String x) _ _ = StringType (Text.length x)
synthesizedField _ _ (_, AST.Nil) _ _ = NilType
synthesizedField _ _ (_, AST.Builtin x) _ _ = BuiltinType x
instance (Atts (Synthesized (Auto TypeCheck)) (Abstract.Expression l l Sem Sem) ~ SynTCExp l) =>
SynthesizedField "errors" (Folded [Error () l]) (Auto TypeCheck) (AST.Element l l) Sem Placed where
synthesizedField _ _ (pos, _) _inheritance (AST.Element expr) = integerExpressionErrors pos (syn expr)
synthesizedField _ _ (pos, _) _inheritance (AST.Range low high) = integerExpressionErrors pos (syn high)
<> integerExpressionErrors pos (syn low)
instance SynthesizedField "inferredType" (Type l) (Auto TypeCheck) (AST.Element l l) Sem Placed where
synthesizedField _ _ _ _ _ = BuiltinType "SET"
instance {-# overlaps #-} (Abstract.Nameable l, Abstract.Oberon l, Ord (Abstract.QualIdent l),
Show (Abstract.QualIdent l),
Atts (Inherited (Auto TypeCheck)) (Abstract.Designator l l Sem Sem) ~ InhTC l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Expression l l Sem Sem) ~ SynTCExp l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Designator l l Sem Sem) ~ SynTCDes l) =>
Synthesizer (Auto TypeCheck) (AST.Designator l l) Sem Placed where
synthesis _ (pos, AST.Variable q) InhTC{env} _ =
SynTCDes{errors= case designatorType
of Nothing -> Folded [Error () pos (UnknownName q)]
Just{} -> mempty,
designatorName= (,) Nothing <$> Abstract.getNonQualIdentName q
<|> first Just <$> Abstract.getQualIdentNames q,
designatorType= fromMaybe UnknownType designatorType}
where designatorType = Map.lookup q env
synthesis _ (pos, AST.Field _record fieldName) InhTC{} (AST.Field record _fieldName) =
SynTCDes{errors= case syn record
of SynTCDes{errors= Folded [],
designatorType= t} ->
maybe (Folded [Error () pos (NonRecordType t)])
(maybe (Folded [Error () pos (UnknownField fieldName t)]) $ const mempty)
(access True t)
SynTCDes{errors= errors} -> errors,
designatorName= Nothing,
designatorType= fromMaybe UnknownType (fromMaybe Nothing $ access True
$ designatorType $ syn record)}
where access _ (RecordType _ fields) = Just (Map.lookup fieldName fields)
access True (PointerType t) = access False t
access allowPtr (NominalType _ (Just t)) = access allowPtr t
access allowPtr (ReceiverType t) = (receive <$>) <$> access allowPtr t
access _ _ = Nothing
receive (ProcedureType _ params result) = ProcedureType True params result
receive t = t
synthesis _ (pos, AST.Index _array index indexes) InhTC{} (AST.Index array _index _indexes) =
SynTCDes{errors= case syn array
of SynTCDes{errors= Folded [],
designatorType= t} -> either id (const mempty) (access True t)
SynTCDes{errors= errors} -> errors,
designatorName= Nothing,
designatorType= either (const UnknownType) id (access True $ designatorType $ syn array)}
where access _ (ArrayType dimensions t)
| length dimensions == length indexes + 1 = Right t
| length dimensions == 0 && length indexes == 0 = Right t
| otherwise = Left (Folded [Error () pos
$ ExtraDimensionalIndex (length dimensions) (1 + length indexes)])
access allowPtr (NominalType _ (Just t)) = access allowPtr t
access allowPtr (ReceiverType t) = access allowPtr t
access True (PointerType t) = access False t
access _ t = Left (Folded [Error () pos (NonArrayType t)])
synthesis _ (pos, AST.TypeGuard _designator q) InhTC{env} (AST.TypeGuard designator _q) =
SynTCDes{errors= case (syn designator, targetType)
of (SynTCDes{errors= Folded [],
designatorType= t},
Just t') -> assignmentCompatible pos t t'
(SynTCDes{errors= errors},
Nothing) -> Folded (Error () pos (UnknownName q) : getFolded errors)
(SynTCDes{errors= errors}, _) -> errors,
designatorName= Nothing,
designatorType= fromMaybe UnknownType targetType}
where targetType = Map.lookup q env
synthesis _ (pos, _) InhTC{} (AST.Dereference pointer) =
SynTCDes{errors= case syn pointer
of SynTCDes{errors= Folded [],
designatorType= t}
| PointerType{} <- t -> mempty
| NominalType _ (Just PointerType{}) <- t -> mempty
| ProcedureType True _ _ <- t -> mempty
| otherwise -> Folded [Error () pos (NonPointerType t)]
SynTCDes{errors= es} -> es,
designatorName= Nothing,
designatorType= case designatorType (syn pointer)
of NominalType _ (Just (PointerType t)) -> t
ProcedureType True params result -> ProcedureType False params result
PointerType t -> t
_ -> UnknownType}
binaryNumericOrSetSynthesis pos left right =
SynTCExp{errors= binarySetOrNumericOperatorErrors pos (syn left) (syn right),
inferredType= binaryNumericOperatorType (syn left) (syn right)}
binaryIntegerSynthesis pos left right =
SynTCExp{errors= binaryIntegerOperatorErrors pos (syn left) (syn right),
inferredType= binaryNumericOperatorType (syn left) (syn right)}
binaryBooleanSynthesis pos left right =
SynTCExp{errors= binaryBooleanOperatorErrors pos (syn left) (syn right),
inferredType= BuiltinType "BOOLEAN"}
unaryNumericOrSetOperatorErrors :: forall l. Abstract.Nameable l => LexicalPosition -> SynTCExp l -> Folded [Error () l]
unaryNumericOrSetOperatorErrors pos SynTCExp{errors= Folded [], inferredType= t}
| IntegerType{} <- t = mempty
| BuiltinType name <- t, isNumerical name || name == "SET" = mempty
| otherwise = Folded [Error () pos (NonNumericType t)]
unaryNumericOrSetOperatorErrors _ SynTCExp{errors= errs} = errs
unaryNumericOrSetOperatorType :: (Int -> Int) -> SynTCExp l -> Type l
unaryNumericOrSetOperatorType f SynTCExp{inferredType= IntegerType x} = IntegerType (f x)
unaryNumericOrSetOperatorType _ SynTCExp{inferredType= t} = t
binarySetOrNumericOperatorErrors :: forall l. (Abstract.Nameable l, Eq (Abstract.QualIdent l))
=> LexicalPosition -> SynTCExp l -> SynTCExp l -> Folded [Error () l]
binarySetOrNumericOperatorErrors _
SynTCExp{errors= Folded [], inferredType= BuiltinType name1}
SynTCExp{errors= Folded [], inferredType= BuiltinType name2}
| isNumerical name1 && isNumerical name2 || name1 == "SET" && name2 == "SET" = mempty
binarySetOrNumericOperatorErrors _
SynTCExp{errors= Folded [], inferredType= IntegerType{}}
SynTCExp{errors= Folded [], inferredType= BuiltinType name}
| isNumerical name = mempty
binarySetOrNumericOperatorErrors _
SynTCExp{errors= Folded [], inferredType= BuiltinType name}
SynTCExp{errors= Folded [], inferredType= IntegerType{}}
| isNumerical name = mempty
binarySetOrNumericOperatorErrors _
SynTCExp{errors= Folded [], inferredType= IntegerType{}}
SynTCExp{errors= Folded [], inferredType= IntegerType{}} = mempty
binarySetOrNumericOperatorErrors pos SynTCExp{errors= Folded [], inferredType= t1}
SynTCExp{errors= Folded [], inferredType= t2}
| t1 == t2 = Folded [Error () pos (NonNumericType t1)]
| otherwise = Folded [Error () pos (TypeMismatch t1 t2)]
binarySetOrNumericOperatorErrors _ SynTCExp{errors= errs1} SynTCExp{errors= errs2} = errs1 <> errs2
binaryNumericOperatorType :: (Abstract.Nameable l, Eq (Abstract.QualIdent l)) => SynTCExp l -> SynTCExp l -> Type l
binaryNumericOperatorType SynTCExp{inferredType= t1} SynTCExp{inferredType= t2}
| t1 == t2 = t1
| IntegerType{} <- t1 = t2
| IntegerType{} <- t2 = t1
| BuiltinType name1 <- t1, BuiltinType name2 <- t2,
Just index1 <- List.elemIndex name1 numericTypeNames,
Just index2 <- List.elemIndex name2 numericTypeNames = BuiltinType (numericTypeNames !! max index1 index2)
| otherwise = t1
binaryIntegerOperatorErrors :: Abstract.Nameable l =>
LexicalPosition -> SynTCExp l -> SynTCExp l -> Folded [Error () l]
binaryIntegerOperatorErrors pos syn1 syn2 = integerExpressionErrors pos syn1 <> integerExpressionErrors pos syn2
integerExpressionErrors :: forall l. LexicalPosition -> SynTCExp l -> Folded [Error () l]
integerExpressionErrors pos SynTCExp{errors= Folded [], inferredType= t}
| isIntegerType t = mempty
| otherwise = Folded [Error () pos (NonIntegerType t)]
integerExpressionErrors _ SynTCExp{errors= errs} = errs
isIntegerType IntegerType{} = True
isIntegerType (BuiltinType "SHORTINT") = True
isIntegerType (BuiltinType "INTEGER") = True
isIntegerType (BuiltinType "LONGINT") = True
isIntegerType t = False
booleanExpressionErrors :: forall l. LexicalPosition -> SynTCExp l -> Folded [Error () l]
booleanExpressionErrors _ SynTCExp{errors= Folded [],
inferredType= BuiltinType "BOOLEAN"} = mempty
booleanExpressionErrors pos SynTCExp{errors= Folded [], inferredType= t} =
Folded [Error () pos (NonBooleanType t)]
booleanExpressionErrors _ SynTCExp{errors= errs} = errs
binaryBooleanOperatorErrors :: forall l. (Abstract.Nameable l, Eq (Abstract.QualIdent l))
=> LexicalPosition -> SynTCExp l -> SynTCExp l -> Folded [Error () l]
binaryBooleanOperatorErrors _pos
SynTCExp{errors= Folded [], inferredType= BuiltinType "BOOLEAN"}
SynTCExp{errors= Folded [], inferredType= BuiltinType "BOOLEAN"} = mempty
binaryBooleanOperatorErrors pos
SynTCExp{errors= Folded [], inferredType= t1}
SynTCExp{errors= Folded [], inferredType= t2}
| t1 == t2 = Folded [Error () pos (NonBooleanType t1)]
| otherwise = Folded [Error () pos (TypeMismatch t1 t2)]
binaryBooleanOperatorErrors _ SynTCExp{errors= errs1} SynTCExp{errors= errs2} = errs1 <> errs2
parameterCompatible :: forall l. (Abstract.Nameable l, Eq (Abstract.QualIdent l))
=> LexicalPosition -> (Bool, Type l) -> Type l -> Folded [Error () l]
parameterCompatible _ (_, expected@(ArrayType [] _)) actual
| arrayCompatible expected actual = mempty
parameterCompatible pos (True, expected) actual
| expected == actual = mempty
| otherwise = Folded [Error () pos (UnequalTypes expected actual)]
parameterCompatible pos (False, expected) actual
| BuiltinType "ARRAY" <- expected, ArrayType{} <- actual = mempty
| otherwise = assignmentCompatible pos expected actual
assignmentCompatibleIn :: forall l. (Abstract.Nameable l, Eq (Abstract.QualIdent l))
=> InhTCExp l -> LexicalPosition -> Type l -> Folded [Error () l]
assignmentCompatibleIn InhTCExp{expectedType} pos = assignmentCompatible pos expectedType
assignmentCompatible :: forall l. (Abstract.Nameable l, Eq (Abstract.QualIdent l))
=> LexicalPosition -> Type l -> Type l -> Folded [Error () l]
assignmentCompatible pos expected actual
| expected == actual = mempty
| BuiltinType name1 <- expected, BuiltinType name2 <- actual,
Just index1 <- List.elemIndex name1 numericTypeNames,
Just index2 <- List.elemIndex name2 numericTypeNames,
index1 >= index2 = mempty
| BuiltinType name <- expected, IntegerType{} <- actual, isNumerical name = mempty
| BuiltinType "BASIC TYPE" <- expected, BuiltinType name <- actual,
name `elem` ["BOOLEAN", "CHAR", "SHORTINT", "INTEGER", "LONGINT", "REAL", "LONGREAL", "SET"] = mempty
| BuiltinType "POINTER" <- expected, PointerType{} <- actual = mempty
| BuiltinType "POINTER" <- expected, NominalType _ (Just t) <- actual =
assignmentCompatible pos expected t
| BuiltinType "CHAR" <- expected, actual == StringType 1 = mempty
| ReceiverType t <- actual = assignmentCompatible pos expected t
| ReceiverType t <- expected = assignmentCompatible pos t actual
| NilType <- actual, PointerType{} <- expected = mempty
| NilType <- actual, ProcedureType{} <- expected = mempty
| NilType <- actual, NominalType _ (Just t) <- expected = assignmentCompatible pos t actual
-- | ArrayType [] (BuiltinType "CHAR") <- expected, StringType{} <- actual = mempty
| ArrayType [m] (BuiltinType "CHAR") <- expected, StringType n <- actual =
Folded (if m < n then [Error () pos (TooSmallArrayType m n)] else [])
| targetExtends actual expected = mempty
| NominalType _ (Just t) <- expected, ProcedureType{} <- actual = assignmentCompatible pos t actual
| otherwise = Folded [Error () pos (IncompatibleTypes expected actual)]
arrayCompatible (ArrayType [] t1) (ArrayType _ t2) = t1 == t2 || arrayCompatible t1 t2
arrayCompatible (ArrayType [] (BuiltinType "CHAR")) StringType{} = True
arrayCompatible (NominalType _ (Just t1)) t2 = arrayCompatible t1 t2
arrayCompatible t1 (NominalType _ (Just t2)) = arrayCompatible t1 t2
arrayCompatible _ _ = False
extends, targetExtends :: Eq (Abstract.QualIdent l) => Type l -> Type l -> Bool
t1 `extends` t2 | t1 == t2 = True
RecordType ancestry _ `extends` NominalType q _ = q `elem` ancestry
NominalType _ (Just t1) `extends` t2 = t1 `extends` t2
t1 `extends` t2 = False -- error (show (t1, t2))
ultimate :: Type l -> Type l
ultimate (NominalType _ (Just t)) = ultimate t
ultimate t = t
isNumerical t = t `elem` numericTypeNames
numericTypeNames = ["SHORTINT", "INTEGER", "LONGINT", "REAL", "LONGREAL"]
PointerType t1 `targetExtends` PointerType t2 = t1 `extends` t2
NominalType _ (Just t1) `targetExtends` t2 = t1 `targetExtends` t2
t1 `targetExtends` NominalType _ (Just t2) = t1 `targetExtends` t2
t1 `targetExtends` t2 | t1 == t2 = True
t1 `targetExtends` t2 = False
instance Transformation.Transformation (Auto TypeCheck) where
type Domain (Auto TypeCheck) = Placed
type Codomain (Auto TypeCheck) = Semantics (Auto TypeCheck)
instance AG.Revelation (Auto TypeCheck) where
reveal (Auto TypeCheck) = snd
instance Ord (Abstract.QualIdent l) => Transformation.At (Auto TypeCheck) (Modules l Sem Sem) where
($) = AG.applyDefault snd
-- * Unsafe Rank2 AST instances
instance Rank2.Apply (AST.Module l l f') where
AST.Module name1 imports1 body1 <*> ~(AST.Module name2 imports2 body2) =
AST.Module name1 imports1 (Rank2.apply body1 body2)
-- | Check if the given collection of modules is well typed and return all type errors found. The collection is a
-- 'Map' keyed by module name. The first argument's value is typically 'predefined' or 'predefined2'.
checkModules :: forall l. (Abstract.Oberon l, Abstract.Nameable l,
Ord (Abstract.QualIdent l), Show (Abstract.QualIdent l),
Atts (Inherited (Auto TypeCheck)) (Abstract.Block l l Sem Sem) ~ InhTC l,
Atts (Synthesized (Auto TypeCheck)) (Abstract.Block l l Sem Sem) ~ SynTCMod l,
Full.Functor (Auto TypeCheck) (Abstract.Block l l))
=> Environment l -> Map AST.Ident (Placed (AST.Module l l Placed Placed)) -> [Error AST.Ident l]
checkModules predef modules =
getFolded ((syn (Transformation.apply (Auto TypeCheck) (wrap $ Auto TypeCheck Deep.<$> Modules modules)
`Rank2.apply`
Inherited (InhTCRoot predef))).errors)
where wrap = (,) (0, Trailing [], 0)
predefined, predefined2 :: (Abstract.Wirthy l, Ord (Abstract.QualIdent l)) => Environment l
-- | The set of 'Predefined' types and procedures defined in the Oberon Language Report.
predefined = Map.fromList $ map (first Abstract.nonQualIdent) $
[("BOOLEAN", BuiltinType "BOOLEAN"),
("CHAR", BuiltinType "CHAR"),
("SHORTINT", BuiltinType "SHORTINT"),
("INTEGER", BuiltinType "INTEGER"),
("LONGINT", BuiltinType "LONGINT"),
("REAL", BuiltinType "REAL"),
("LONGREAL", BuiltinType "LONGREAL"),
("SET", BuiltinType "SET"),
("TRUE", BuiltinType "BOOLEAN"),
("FALSE", BuiltinType "BOOLEAN"),
("ABS", ProcedureType False [(False, BuiltinType "INTEGER")] $ Just $ BuiltinType "INTEGER"),
("ASH", ProcedureType False [(False, BuiltinType "INTEGER")] $ Just $ BuiltinType "INTEGER"),
("CAP", ProcedureType False [(False, BuiltinType "CHAR")] $ Just $ BuiltinType "CHAR"),
("LEN", ProcedureType False [(False, BuiltinType "ARRAY")] $ Just $ BuiltinType "LONGINT"),
("MAX", ProcedureType False [(False, BuiltinType "BASIC TYPE")] $ Just UnknownType),
("MIN", ProcedureType False [(False, BuiltinType "BASIC TYPE")] $ Just UnknownType),
("ODD", ProcedureType False [(False, BuiltinType "CHAR")] $ Just $ BuiltinType "BOOLEAN"),
("SIZE", ProcedureType False [(False, BuiltinType "CHAR")] $ Just $ BuiltinType "INTEGER"),
("ORD", ProcedureType False [(False, BuiltinType "CHAR")] $ Just $ BuiltinType "INTEGER"),
("CHR", ProcedureType False [(False, BuiltinType "LONGINT")] $ Just $ BuiltinType "CHAR"),
("SHORT", ProcedureType False [(False, BuiltinType "LONGINT")] $ Just $ BuiltinType "SHORTINT"),
("LONG", ProcedureType False [(False, BuiltinType "INTEGER")] $ Just $ BuiltinType "INTEGER"),
("ENTIER", ProcedureType False [(False, BuiltinType "REAL")] $ Just $ BuiltinType "INTEGER"),
("INC", ProcedureType False [(False, BuiltinType "LONGINT")] Nothing),
("DEC", ProcedureType False [(False, BuiltinType "LONGINT")] Nothing),
("INCL", ProcedureType False [(False, BuiltinType "SET"), (False, BuiltinType "INTEGER")] Nothing),
("EXCL", ProcedureType False [(False, BuiltinType "SET"), (False, BuiltinType "INTEGER")] Nothing),
("COPY", ProcedureType False [(False, BuiltinType "ARRAY"), (False, BuiltinType "ARRAY")] Nothing),
("NEW", ProcedureType False [(False, BuiltinType "POINTER")] Nothing),
("HALT", ProcedureType False [(False, BuiltinType "INTEGER")] Nothing)]
-- | The set of 'Predefined' types and procedures defined in the Oberon-2 Language Report.
predefined2 = predefined <>
Map.fromList (first Abstract.nonQualIdent <$>
[("ASSERT", ProcedureType False [(False, BuiltinType "BOOLEAN"),
(False, BuiltinType "INTEGER")] Nothing)])