never executed always true always false
1 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
2 {-# LANGUAGE InstanceSigs #-}
3 {-# LANGUAGE UndecidableInstances #-}
4
5 -- This module is where the syntax tree is mapped to the model. This is also the
6 -- stage at which all errrors are reported.
7 -- This has three main parts
8 -- Syntax checking:
9 -- When it comes to missing tokens these should usually be handled by the
10 -- low level token validation functions, however in some special cases
11 -- where the tokens are manipulated manually the checks need to be added
12 -- Type checking:
13 -- Type check operators and build up the symbol table.
14 -- Metadata additions:
15 -- this includeds things like marking tokens for documentation, as well as
16 -- setting up structural regions such as quantigied expressions
17
18 module Conjure.Language.Validator where
19
20 import Conjure.Bug (bug)
21 import Conjure.Language.AST.Reformer (HighLevelTree, flattenSeq, makeTree)
22 import Conjure.Language.AST.Syntax as S
23 import Conjure.Language.Attributes
24 import Conjure.Language.CategoryOf (Category (CatConstant, CatDecision, CatParameter))
25 import Conjure.Language.Definition hiding (Typed)
26 import Conjure.Language.Domain
27 import Conjure.Language.Domain.AddAttributes (allSupportedAttributes)
28 import Conjure.Language.Expression qualified as D
29 ( Expression (Typed),
30 )
31 import Conjure.Language.Expression.Op
32 ( Op (..),
33 OpAttributeAsConstraint (OpAttributeAsConstraint),
34 OpIndexing (..),
35 OpPowerSet (..),
36 OpRelationProj (..),
37 OpSlicing (..),
38 OpType (..),
39 mkBinOp,
40 mkOp
41 )
42 import Conjure.Language.Lexemes
43 import Conjure.Language.Lexer (ETok (ETok, lexeme), sourcePos0, sourcePosAfter, tokenSourcePos, tokenStartOffset, totalLength, trueLength)
44 import Conjure.Language.Pretty
45 import Conjure.Language.Type
46 import Conjure.Prelude
47 import Control.Monad (mapAndUnzipM)
48 import Control.Monad.Writer.Strict (Writer)
49 import Data.List (splitAt)
50 import Data.Map.Strict (Map)
51 import Data.Map.Strict qualified as M
52 import Data.Sequence (Seq (..), ViewR (..), viewr)
53 import Data.Set qualified as S
54 import Data.Text (append, pack, unpack)
55 import Data.Text qualified as T
56 import Text.Megaparsec (SourcePos, mkPos, unPos)
57 import Text.Megaparsec.Pos (SourcePos (..))
58
59 data TagType
60 = TtType
61 | TtNumber
62 | TtBool
63 | TtDomain
64 | TtEnum
65 | TtEnumMember
66 | TtRecord
67 | TtRecordMember
68 | TtUserFunction
69 | TtFunction
70 | TtAttribute
71 | TtAAC
72 | TtVariable
73 | TtKeyword
74 | TtQuantifier
75 | TtSubKeyword
76 | TtOperator
77 | TtLocal
78 | TtOther Text
79 deriving (Show)
80
81 data TaggedToken
82 = TaggedToken TagType ETok
83 deriving (Show)
84
85 class WithRegion a where
86 getRegion :: (WithRegion a) => a -> DiagnosticRegion
87
88 instance WithRegion (DiagnosticRegion, a) where
89 getRegion (r, _) = r
90
91 instance WithRegion DiagnosticRegion where
92 getRegion = id
93
94 instance WithRegion LToken where
95 getRegion = symbolRegion
96
97 instance WithRegion SToken where
98 getRegion = symbolRegion
99
100 type RegionTagged a = (DiagnosticRegion, a)
101
102 unregion :: RegionTagged a -> a
103 unregion (_, a) = a
104
105 data Typed a = Typed Type a
106 deriving (Show)
107
108 instance Functor Typed where
109 fmap f (Typed k a) = Typed k (f a)
110
111 simple :: Type -> Kind
112 simple = Kind $ ValueType CatConstant
113
114 withCat :: Category -> Type -> Kind
115 withCat = Kind . ValueType
116
117 data Kind = Kind Class Type
118 deriving (Show, Eq, Ord)
119
120 instance Pretty Kind where
121 -- pretty (Kind MemberType t) = "Member of " <> pretty t
122 pretty (Kind DomainType t) = "domain `" <> pretty t <> "`"
123 pretty (Kind (ValueType _) t) = pretty t
124
125 data Class = DomainType | ValueType Category
126 deriving (Show, Eq, Ord)
127
128 instance Pretty Class where
129 pretty c = case c of
130 DomainType -> "Domain"
131 ValueType _ -> "Value"
132
133 untype :: Typed a -> a
134 untype (Typed _ a) = a
135
136 typeOf_ :: Typed a -> Type
137 typeOf_ (Typed t _) = t
138
139 untypeAs :: Type -> Typed a -> ValidatorS a
140 untypeAs r ((Typed t a)) =
141 if let ?typeCheckerMode = StronglyTyped in typeUnify r t
142 then return a
143 else contextTypeError (TypeError r t) >> return a
144
145 type TypeCheck a = Typed a -> ValidatorS ()
146
147 exactly :: Type -> TypeCheck a
148 exactly t r = void $ untypeAs t r
149
150 typeAs :: Type -> Maybe a -> Maybe (Typed a)
151 typeAs t (Just a) = Just $ Typed t a
152 typeAs _ Nothing = Nothing
153
154 (?=>) :: ValidatorS (Typed a) -> TypeCheck a -> ValidatorS a
155 v ?=> t = v >>= (\a -> t a >> return (untype a))
156
157 castAny :: Validator a -> Validator (Typed a)
158 castAny a = typeAs TypeAny <$> a
159
160 tInt :: Type
161 tInt = TypeInt TagInt
162
163 typeSplit :: Typed a -> (Type, a)
164 typeSplit (Typed t v) = (t, v)
165
166 getTypeList :: [Typed a] -> [(Type, a)]
167 getTypeList = map typeSplit
168
169 data ErrorType
170 = TokenError LToken
171 | SyntaxError Text
172 | WithReplacements ErrorType [Text]
173 | SemanticError Text
174 | CustomError Text
175 | SkippedTokens
176 | MissingArgsError Int Int
177 | UnexpectedArg
178 | TypeError Type Type -- Expected, got
179 | ComplexTypeError Text Type -- Expected, got
180 | CategoryError Category Text
181 | KindError Class Class
182 | InternalError -- Used to explicitly tag invalid pattern matches
183 | InternalErrorS Text -- Used for giving detail to bug messages
184 deriving (Show, Eq, Ord)
185
186 data WarningType
187 = UnclassifiedWarning Text
188 | AmbiguousTypeWarning
189 deriving (Show, Eq, Ord)
190
191 data InfoType = UnclassifiedInfo Text deriving (Show, Eq, Ord)
192
193 data Diagnostic = Error ErrorType | Warning WarningType | Info InfoType
194 deriving (Show, Eq, Ord)
195
196 data ValidatorDiagnostic = ValidatorDiagnostic DiagnosticRegion Diagnostic
197 deriving (Show)
198
199 isError :: ValidatorDiagnostic -> Bool
200 isError (ValidatorDiagnostic _ (Error _)) = True
201 isError _ = False
202
203 data RegionType
204 = Definition Text Kind
205 | LiteralDecl Kind
206 | Ref Text Kind DiagnosticRegion
207 | Structural StructuralType
208 | Documentation Text
209 deriving (Show)
210
211 data StructuralType
212 = SSuchThat
213 | SGiven
214 | SFind
215 | SLetting
216 | SWhere
217 | SBranching
218 | SGoal Text
219 | SEnum Text
220 | SQuantification Text Kind
221 | SComprehension Kind
222 | SGuard
223 | SGen
224 | SBody
225 deriving (Show)
226
227 data RegionInfo = RegionInfo
228 { rRegion :: DiagnosticRegion,
229 rSubRegion :: Maybe DiagnosticRegion,
230 rRegionType :: RegionType,
231 rChildren :: [RegionInfo],
232 rTable :: SymbolTable
233 }
234 deriving (Show)
235
236 mkDeclaration :: DiagnosticRegion -> Text -> Kind -> RegionInfo
237 mkDeclaration r n t = RegionInfo r (Just r) (Definition n t) [] M.empty
238
239 mkLiteral :: DiagnosticRegion -> Text -> Typed a -> RegionInfo
240 mkLiteral r _ (Typed t _) = RegionInfo r (Just r) (LiteralDecl (simple t)) [] M.empty
241
242 putReference :: DiagnosticRegion -> Text -> Kind -> DiagnosticRegion -> ValidatorS ()
243 putReference r n t ref = addRegion (RegionInfo r Nothing (Ref n t ref) [] M.empty)
244
245 holdDeclarations :: ValidatorS a -> ValidatorS (a, [RegionInfo])
246 holdDeclarations f = do
247 prev <- gets regionInfo
248 modify (\s -> s {regionInfo = []})
249 res <- f
250 decls <- gets regionInfo
251 modify (\s -> s {regionInfo = prev})
252 return (res, decls)
253
254 wrapRegion :: (HighLevelTree a, HighLevelTree b) => a -> b -> StructuralType -> ValidatorS n -> ValidatorS n
255 wrapRegion regMain regSel = wrapRegion' (symbolRegion regMain) (symbolRegion regSel)
256
257 wrapRegion' :: DiagnosticRegion -> DiagnosticRegion -> StructuralType -> ValidatorS n -> ValidatorS n
258 wrapRegion' regMain regSel ty f = do
259 (res, ds) <- holdDeclarations f
260 let rMain = regMain
261 let rSel = Just regSel
262 st <- gets symbolTable
263 let new = RegionInfo rMain rSel (Structural ty) ds st
264 unless (null ds) $ addRegion new
265 return res
266
267 -- injectRegion :: DiagnosticRegion -> DiagnosticRegion -> ()
268
269 putDocs :: (HighLevelTree a) => Text -> a -> ValidatorS ()
270 putDocs nm r = addRegion $ RegionInfo {rRegion = symbolRegion r, rSubRegion = Nothing, rRegionType = Documentation nm, rChildren = [], rTable = M.empty}
271
272 -- Infix symbol validation and tagging
273 isA :: SToken -> TagType -> ValidatorS ()
274 isA = flagSToken
275
276 isA' :: LToken -> TagType -> ValidatorS ()
277 isA' a b = validateSymbol a >> flagToken a b
278
279 are :: [LToken] -> TagType -> ValidatorS ()
280 are a b = mapM_ (`isA'` b) a
281
282 flagToken :: LToken -> TagType -> ValidatorS ()
283 flagToken (RealToken s) c = flagSToken s c
284 flagToken _ _ = return ()
285
286 flagSToken :: SToken -> TagType -> ValidatorS ()
287 flagSToken (StrictToken _ t) c = modify (\x@ValidatorState {symbolCategories = sc} -> x {symbolCategories = M.insert t (TaggedToken c t) sc})
288
289 tagWithType :: NameNode -> Kind -> ValidatorS ()
290 tagWithType (NameNode (NameNodeS lt)) (Kind (ValueType _) ty) = flagSToken lt $ case ty of
291 TypeEnum _ -> TtEnum
292 TypeInt (TagEnum _) -> TtEnumMember
293 TypeInt (TagUnnamed _) -> TtEnumMember
294 TypeUnnamed _ -> TtEnum
295 TypeVariant _ -> TtRecord
296 TypeVariantMember {} -> TtRecordMember
297 TypeRecord _ -> TtRecord
298 TypeRecordMember {} -> TtRecordMember
299 TypeFunction _ _ -> TtFunction
300 TypeSequence _ -> TtFunction
301 TypeRelation _ -> TtFunction
302 _ -> TtVariable
303 tagWithType (NameNode (NameNodeS lt)) (Kind DomainType (TypeEnum {})) = flagSToken lt TtEnum
304 tagWithType (NameNode (NameNodeS lt)) (Kind DomainType (TypeRecord {})) = flagSToken lt TtRecord
305 tagWithType (NameNode (NameNodeS lt)) (Kind DomainType (TypeVariant {})) = flagSToken lt TtRecord
306 tagWithType (NameNode (NameNodeS lt)) (Kind DomainType _) = flagSToken lt TtDomain
307 tagWithType _ _ = pure ()
308
309 data ValidatorState = ValidatorState
310 { typeChecking :: Bool,
311 regionInfo :: [RegionInfo],
312 symbolTable :: SymbolTable,
313 symbolCategories :: Map ETok TaggedToken,
314 currentContext :: DiagnosticRegion,
315 filePath :: Maybe Text,
316 categoryLimit :: (Category, Text) -- Category,Context (e.g domain)
317 }
318 deriving (Show)
319
320 -- instance Default ValidatorState where
321 -- def = ValidatorState {
322 -- typeChecking = True,
323 -- regionInfo=[],
324 -- symbolCategories=M.empty,
325 -- symbolTable=M.empty
326 -- }
327
328 initialState :: (HighLevelTree a) => a -> Maybe Text -> ValidatorState
329 initialState r path =
330 ValidatorState
331 { typeChecking = True,
332 regionInfo = [],
333 symbolCategories = M.empty,
334 symbolTable = M.empty,
335 currentContext = symbolRegion r,
336 filePath = path,
337 categoryLimit = (CatDecision, "root")
338 }
339
340 type SymbolTable = (Map Text SymbolTableValue)
341
342 type SymbolTableValue = (DiagnosticRegion, Bool, Kind)
343
344 -- instance Show SymbolTableValue where
345 -- show (SType t) = show $ pretty t
346 -- show (SDomain d) = show $ pretty d
347 newtype ValidatorT r w a = ValidatorT (StateT r (Writer [w]) a)
348 deriving (Monad, Applicative, Functor, MonadState r, MonadWriter [w])
349
350 -- synonym wrapped in maybe to allow errors to propagate
351 type Validator a = ValidatorT ValidatorState ValidatorDiagnostic (Maybe a)
352
353 -- Non maybe version used in outward facing applications/ lists
354 type ValidatorS a = ValidatorT ValidatorState ValidatorDiagnostic a
355
356 -- addEnumDefns :: [Text] -> SymbolTable -> SymbolTable
357 -- addEnumDefns names (SymbolTable enums) = SymbolTable $ enums ++ map (\m -> (m,"Enum")) names
358 -- instance MonadFail (ValidatorT ValidatorState ValidatorDiagnostic a) where
359 -- fail = return . fallback . T.pack
360
361 modifySymbolTable :: (SymbolTable -> SymbolTable) -> ValidatorS ()
362 modifySymbolTable f = modify (\x -> x {symbolTable = f . symbolTable $ x})
363
364 getSymbol :: Text -> ValidatorS (Maybe SymbolTableValue)
365 getSymbol n = M.lookup n <$> getSymbolTable
366
367 putSymbol :: (Name, SymbolTableValue) -> ValidatorS Bool
368 putSymbol (Name name, t) = do
369 x <- getSymbol name
370 modifySymbolTable (M.insert name t)
371 case x of
372 Nothing -> return False
373 Just _ -> return True
374 putSymbol _ = return False -- skip types for meta and machine vars
375
376 addRegion :: RegionInfo -> ValidatorS ()
377 addRegion r = modify (\x -> x {regionInfo = r : regionInfo x})
378
379 makeEnumDomain :: Name -> Maybe [Range Expression] -> Domain () Expression
380 makeEnumDomain n es = DomainEnum n es Nothing
381
382 makeUnnamedDomain :: Name -> Domain () ()
383 makeUnnamedDomain n = DomainUnnamed n ()
384
385 getSymbolTable :: ValidatorS SymbolTable
386 getSymbolTable = symbolTable <$> get
387
388 getContext :: ValidatorS DiagnosticRegion
389 getContext = currentContext <$> get
390
391 setContext :: DiagnosticRegion -> ValidatorS ()
392 setContext r = modify (\p -> p {currentContext = r})
393
394 setContextFrom :: (HighLevelTree a) => a -> ValidatorS ()
395 setContextFrom a = setContext $ symbolRegion a
396
397 -- strict :: Validator a -> ValidatorS a
398 -- strict a = do res <- a; return res
399
400 deState :: ((a, r), n) -> (a, n, r)
401 deState ((a, r), n) = (a, n, r)
402
403 runValidator :: ValidatorT r w a -> r -> (a, [w], r)
404 runValidator (ValidatorT r) d = deState $ runWriter (runStateT r d)
405
406 isSyntacticallyValid :: (HighLevelTree a) => (a -> ValidatorS b) -> a -> Bool
407 isSyntacticallyValid v s = case runValidator (v s) (initialState s Nothing) {typeChecking = False} of
408 (_, vds, _) -> not $ any isError vds
409
410 todoTypeAny :: Maybe a -> Maybe (Typed a)
411 todoTypeAny = typeAs TypeAny
412
413 setCategoryLimit :: (Category, Text) -> ValidatorS a -> ValidatorS a
414 setCategoryLimit c f = do
415 tmp <- gets categoryLimit
416 modify (\s -> s {categoryLimit = c})
417 res <- f
418 modify (\s -> s {categoryLimit = tmp})
419 return res
420
421 checkCategory :: Kind -> ValidatorS ()
422 checkCategory (Kind (ValueType category) _) = do
423 (refCat, context) <- gets categoryLimit
424 unless (refCat >= category) $ contextTypeError $ CategoryError category context
425 checkCategory (Kind DomainType _) = return ()
426
427 validateModel :: ProgramTree -> ValidatorS Model
428 validateModel model = do
429 langVersion <- validateLanguageVersion $ langVersionInfo model
430 sts <- validateProgramTree (statements model)
431 return $ Model (fromMaybe def langVersion) sts def
432
433 validateProgramTree :: [StatementNode] -> ValidatorS [Statement]
434 validateProgramTree sts = do
435 q <- validateArray validateStatement sts
436 return $ concat q
437
438 validateLanguageVersion :: Maybe LangVersionNode -> Validator LanguageVersion
439 validateLanguageVersion Nothing = return $ pure $ LanguageVersion "Essence" [1, 3]
440 validateLanguageVersion (Just lv@(LangVersionNode l1 n v)) = do
441 setContextFrom lv
442 l1 `isA` TtKeyword
443 name <- validateIdentifier n
444 checkLanguageName name
445 nums <- catMaybes <$> validateSequence_ getNum v
446 return
447 . pure
448 $ LanguageVersion
449 (Name name)
450 (if null nums then [1, 3] else nums)
451 where
452 getNum :: SToken -> Validator Int
453 getNum c = do
454 c' <- validateSToken c
455 case c' of
456 (LIntLiteral x) -> return . pure $ fromInteger x
457 _ -> invalid $ c <!> InternalError
458 checkLanguageName nm
459 | T.toLower nm == "essence" = pure ()
460 | T.toLower nm == "essence'" = do
461 raiseError (symbolRegion lv /!\ UnclassifiedWarning "Essence prime file detected, type checking is off")
462 modify (\s -> s {typeChecking = False})
463 | otherwise = raiseError $ symbolRegion n <!> SyntaxError "Not a valid language name"
464
465 validateStatement :: StatementNode -> ValidatorS [Statement]
466 validateStatement (DeclarationStatement dsn) = validateDeclarationStatement dsn
467 validateStatement (BranchingStatement bsn) = validateBranchingStatement bsn
468 validateStatement (SuchThatStatement stsn) = validateSuchThatStatement stsn
469 validateStatement (WhereStatement wsn) = validateWhereStatement wsn
470 validateStatement (ObjectiveStatement osn) = validateObjectiveStatement osn
471 validateStatement (HeuristicStatement lt exp) = validateHeuristicStatement lt exp
472 validateStatement (UnexpectedToken lt) = [] <$ invalid (lt <!> TokenError lt) -- TODO address as part of skip token refactor
473
474 validateHeuristicStatement :: SToken -> ExpressionNode -> ValidatorS [Statement]
475 validateHeuristicStatement lt exp = do
476 let validHeuristics = ["static", "sdf", "conflict", "srf", "ldf", "wdeg", "domoverwdeg"]
477 lt `isA` TtKeyword
478 h <- case exp of
479 IdentifierNode nn@(NameNodeS (StrictToken _ (ETok {lexeme = (LIdentifier nm)}))) -> do
480 if nm `elem` validHeuristics
481 then return $ pure [SearchHeuristic (Name nm)]
482 else invalid $ symbolRegion nn <!> SemanticError (T.concat ["Invalid heuristic ", nm, " Expected one of: ", pack $ show validHeuristics])
483 _ -> invalid $ symbolRegion exp <!> SemanticError "Only identifiers are allowed as heuristics"
484 return $ fromMaybe [] h
485
486 tCondition :: TypeCheck a
487 tCondition (Typed TypeAny _) = pure ()
488 tCondition (Typed TypeBool _) = pure ()
489 tCondition (Typed (TypeMatrix _ TypeBool) _) = pure ()
490 tCondition (Typed (TypeList TypeBool) _) = pure ()
491 tCondition t = contextTypeError $ ComplexTypeError "Bool or [Bool]" $ typeOf_ t
492
493 validateWhereStatement :: WhereStatementNode -> ValidatorS [Statement]
494 validateWhereStatement w@(WhereStatementNode l1 exprs) = wrapRegion w w SWhere $ do
495 l1 `isA` TtKeyword
496 ws <- Where <$> validateSequence_ (\x -> do setContextFrom x; validateExpression x ?=> tCondition) exprs
497 return [ws]
498
499 validateObjectiveStatement :: ObjectiveStatementNode -> ValidatorS [Statement]
500 validateObjectiveStatement o@(ObjectiveMin lt en) = wrapRegion o o (SGoal "Minimising") $ do
501 lt `isA` TtKeyword
502 exp <- validateExpression en
503 return [Objective Minimising $ untype exp]
504 validateObjectiveStatement o@(ObjectiveMax lt en) = wrapRegion o o (SGoal "Maximising") $ do
505 lt `isA` TtKeyword
506 exp <- validateExpression en
507 return [Objective Maximising $ untype exp]
508
509 validateSuchThatStatement :: SuchThatStatementNode -> ValidatorS [Statement]
510 validateSuchThatStatement s@(SuchThatStatementNode l1 l2 exprs) = wrapRegion s s SSuchThat $ do
511 l1 `isA` TtKeyword
512 l2 `isA'` TtKeyword
513 putDocs "such_that" (makeTree l1 `mappend` makeTree l2)
514 exprs' <- validateSequence validateExpression exprs
515 bools <- mapM (\(a, b) -> do setContext a; return b ?=> tCondition) exprs'
516 let bool_exprs = bools
517 return [SuchThat bool_exprs]
518
519 validateBranchingStatement :: BranchingStatementNode -> ValidatorS [Statement]
520 validateBranchingStatement b@(BranchingStatementNode l1 l2 sts) = wrapRegion b b SBranching $ do
521 l1 `isA` TtKeyword
522 l2 `isA'` TtKeyword
523 putDocs "branching_on" (makeTree l1 `mappend` makeTree l2)
524 branchings <- catMaybes <$> validateList_ (f2n validateBranchingParts) sts
525 return [SearchOrder branchings]
526 where
527 validateBranchingParts :: ExpressionNode -> ValidatorS SearchOrder
528 validateBranchingParts (IdentifierNode nn) = do
529 n <- tagNameAs TtVariable nn
530 return $ BranchingOn n
531 validateBranchingParts exp = do
532 x <- validateExpression exp ?=> exactly TypeAny
533 return $ Cut x
534
535 validateDeclarationStatement :: DeclarationStatementNode -> ValidatorS [Statement]
536 validateDeclarationStatement stmt = do
537 stmt' <- case stmt of
538 FindStatement l1 fs -> l1 `isA` TtKeyword >> putDocs "find" l1 >> validateStatementSeq SFind validateFind fs
539 GivenStatement l1 gs -> l1 `isA` TtKeyword >> putDocs "given" l1 >> validateStatementSeq SGiven validateGiven gs
540 LettingStatement l1 ls -> l1 `isA` TtKeyword >> putDocs "letting" l1 >> validateStatementSeq SLetting validateLetting ls
541 return $ Declaration <$> stmt'
542 where
543 validateStatementSeq s v l = wrapRegion stmt stmt s $ do
544 decls <- validateSequence_ v l
545 when (null decls) $ raiseError (symbolRegion stmt <!> SemanticError "Declaration without any members")
546 return $ concat decls
547
548 validateGiven :: GivenStatementNode -> ValidatorS [Declaration]
549 validateGiven (GivenStatementNode idents l1 domain) =
550 do
551 checkSymbols [l1] -- Colon
552 names <- validateSequence (validateNameAs TtVariable) idents
553 (dType, dom) <- typeSplit <$> validateDomain domain
554 let memberType = getDomainMembers dType
555 let declarations = [mkDeclaration r n (withCat CatParameter memberType) | (r, Name n) <- names]
556 mapM_ addRegion declarations
557 mapM_ (\(r, x) -> putSymbol (x, (r, False, withCat CatParameter memberType))) names
558 return $ [FindOrGiven Given nm dom | (_, nm) <- names]
559 validateGiven (GivenEnumNode se l1 l2 l3) =
560 do
561 [l1, l2, l3] `are` TtKeyword -- new Type enum
562 putDocs "new_type_enum" [l1, l2, l3]
563 names <- validateSequence (validateNameAs TtEnum) se
564 let eType = Kind DomainType . TypeEnum
565 mapM_ (\(r, x) -> putSymbol (x, (r, True, eType x))) names
566 return $ [GivenDomainDefnEnum n | (_, n) <- names]
567
568 validateFind :: FindStatementNode -> ValidatorS [Declaration]
569 validateFind (FindStatementNode names colon domain) = do
570 checkSymbols [colon] -- colon
571 names' <- validateSequence (validateNameAs TtVariable) names
572 (dType, dom) <- typeSplit <$> validateDomain domain
573 let memberType = getDomainMembers dType
574 mapM_ (\(r, x) -> putSymbol (x, (r, False, withCat CatDecision memberType))) names'
575 mapM_ addRegion [mkDeclaration r n (withCat CatDecision memberType) | (r, Name n) <- names']
576 return $ [FindOrGiven Find nm dom | (_, nm) <- names']
577
578 validateLetting :: LettingStatementNode -> ValidatorS [Declaration]
579 -- Letting [names] be
580 validateLetting (LettingStatementNode names l1 assign) = do
581 l1 `isA'` TtKeyword -- be
582 validateLettingAssignment names assign
583
584 validateLettingAssignment :: Sequence NameNode -> LettingAssignmentNode -> ValidatorS [Declaration]
585 validateLettingAssignment names (LettingExpr en) = do
586 expr <- validateExpression en
587 setContextFrom en
588 names' <- validateSequence (validateNameAs TtVariable) names
589 let (t, e) = typeSplit expr
590 let declarations = [mkDeclaration r n (simple t) | (r, Name n) <- names']
591 mapM_ addRegion declarations
592 mapM_ (\(r, x) -> putSymbol (x, (r, False, simple t))) names'
593 return $ [Letting n e | (_, n) <- names']
594 validateLettingAssignment names (LettingDomain lt dn) = do
595 lt `isA` TtSubKeyword
596 putDocs "letting_domain" [lt]
597 (tDomain, domain) <- typeSplit <$> validateDomain dn
598 names' <- validateSequence (validateNameAs TtDomain) names
599 let declarations = [mkDeclaration r n (Kind DomainType tDomain) | (r, Name n) <- names']
600 mapM_ addRegion declarations
601 mapM_ (\(r, x) -> putSymbol (x, (r, False, Kind DomainType tDomain))) names'
602 return $ [Letting n (Domain domain) | (_, n) <- names']
603 validateLettingAssignment names (LettingEnum l1 l2 l3 enames) = do
604 [l1, l2, l3] `are` TtKeyword
605 putDocs "new_type_enum" [l1, l2, l3]
606 names' <- validateSequence (validateNameAs TtEnum) names
607 memberNames <- validateList (validateNameAs TtEnumMember) enames
608 let members = map snd memberNames
609 -- let (members,memberDecls) = unzip . map (\(r,n)->(n,\t->mkDeclaration r n (Kind ValueType (TypeEnum t)))) $ memberNames
610 sequence_
611 [ wrapRegion' (catRegions [(r, ()), (symbolRegion enames, ())]) r (SEnum n) $ do
612 let nameMap = zip memberNames ([1 ..] :: [Int])
613 let dType = Kind DomainType $ TypeEnum name
614 let tVal = TypeInt $ TagEnum n
615
616 putReference r n dType r
617 void $ putSymbol (Name n, (r, True, dType))
618 mapM_
619 ( \((r', x), _) -> do
620 let n' = case x of Name nm -> nm; _ -> ""
621 addRegion $ mkDeclaration r' n' (simple $ TypeInt (TagEnum n))
622 putSymbol (x, (r, False, simple tVal))
623 )
624 nameMap
625 | (r, name@(Name n)) <- names'
626 ]
627 return $ [LettingDomainDefnEnum n members | (_, n) <- names']
628 validateLettingAssignment names (LettingUnnamed l1 l2 l3 l4 szExp) = do
629 [l1, l2, l3, l4] `are` TtKeyword -- TODO keywords
630 putDocs "letting_unnamed" [l1, l2, l3, l4]
631 names' <- validateSequence (validateNameAs TtEnum) names
632 size <- do
633 setContextFrom szExp
634 validateExpression szExp ?=> exactly tInt
635 let d = Kind DomainType . TypeUnnamed
636 mapM_ addRegion [mkDeclaration r n (d $ Name n) | (r, Name n) <- names']
637 mapM_ (\(r, x) -> putSymbol (x, (r, False, d x))) names'
638 return $ [LettingDomainDefnUnnamed n size | (_, n) <- names']
639
640 invalid :: ValidatorDiagnostic -> Validator a
641 invalid err = do
642 raiseError err
643 return Nothing
644
645 validateSToken :: SToken -> ValidatorS Lexeme
646 validateSToken (StrictToken ss t) = do
647 checkSymbols (map SkippedToken ss)
648 return $ lexeme t
649
650 validateSymbol :: LToken -> Validator Lexeme
651 validateSymbol s =
652 case s of
653 RealToken st -> pure <$> validateSToken st
654 _ -> invalid $ ValidatorDiagnostic (getRegion s) $ Error $ TokenError s
655
656 -- [MissingTokenError ]
657 getValueType :: Kind -> ValidatorS Type
658 getValueType (Kind (ValueType _) t) = pure t
659 getValueType (Kind k _) = do
660 contextTypeError $ KindError (ValueType CatConstant) k
661 return TypeAny
662
663 getDomainType :: Kind -> ValidatorS Type
664 getDomainType (Kind DomainType t) = pure t
665 getDomainType (Kind k _) = do
666 contextTypeError $ KindError DomainType k
667 return TypeAny
668
669 type TypedDomain = Typed (Domain () Expression)
670
671 type DomainValidator = Validator TypedDomain
672
673 validateDomainWithRepr :: DomainNode -> ValidatorS (Typed (Domain HasRepresentation Expression))
674 validateDomainWithRepr dom = do
675 (t, dom') <- typeSplit <$> validateDomain dom
676 return . Typed t $ changeRepr NoRepresentation dom'
677
678 validateDomain :: DomainNode -> ValidatorS TypedDomain
679 validateDomain dm = setCategoryLimit (CatParameter, "Domain") $ case dm of
680 ParenDomainNode _ dom rt -> do checkSymbols [rt]; validateDomain dom
681 MetaVarDomain lt -> do mv <- validateMetaVar lt; return . Typed TypeAny $ DomainMetaVar mv
682 BoolDomainNode lt -> lt `isA` TtType >> (return . Typed TypeBool) DomainBool
683 RangedIntDomainNode l1 maybe_tag rs -> do
684 l1 `isA` TtType
685 validateRangedInt maybe_tag rs
686 RangedEnumNode nn ranges -> validateEnumRange nn ranges
687 ShortTupleDomainNode lst -> validateTupleDomain lst
688 TupleDomainNode l1 doms -> do
689 l1 `isA` TtType
690 putDocs "tuple" l1
691 validateTupleDomain doms
692 RecordDomainNode l1 ndom -> do
693 l1 `isA` TtType
694 putDocs "record" l1
695 validateRecordDomain ndom
696 VariantDomainNode l1 ndom -> do
697 l1 `isA` TtType
698 putDocs "variant" l1
699 validateVariantDomain ndom
700 MatrixDomainNode l1 m_ib idoms l2 dom -> do
701 l1 `isA` TtType
702 putDocs "matrix" l1
703 l2 `isA'` TtSubKeyword
704 validateIndexedByNode m_ib
705 validateMatrixDomain idoms dom
706 SetDomainNode l1 attrs l2 dom -> do
707 l1 `isA` TtType
708 putDocs "set" l1
709 l2 `isA'` TtSubKeyword
710 validateSetDomain attrs dom
711 MSetDomainNode l1 attrs l2 dom -> do
712 l1 `isA` TtType
713 putDocs "mset" l1
714 l2 `isA'` TtSubKeyword
715 validateMSetDomain attrs dom
716 FunctionDomainNode l1 attrs dom1 l2 dom2 -> do
717 l1 `isA` TtType
718 putDocs "function" l1
719 l2 `isA'` TtOperator
720 validateFunctionDomain attrs dom1 dom2
721 SequenceDomainNode l1 attrs l2 dom -> do
722 l1 `isA` TtType
723 putDocs "sequence" l1
724 l2 `isA'` TtSubKeyword
725 validateSequenceDomain attrs dom
726 PermutationDomainNode l1 attrs l2 dom -> do
727 l1 `isA` TtType
728 putDocs "permutation" l1
729 l2 `isA'` TtSubKeyword
730 validatePermutationDomain attrs dom
731 RelationDomainNode l1 attrs l2 doms -> do
732 l1 `isA` TtType
733 putDocs "relation" l1
734 l2 `isA'` TtSubKeyword
735 validateRelationDomain attrs doms
736 PartitionDomainNode l1 attrs l2 dom -> do
737 l1 `isA` TtType
738 putDocs "partition" l1
739 l2 `isA'` TtSubKeyword
740 validatePartitionDomain attrs dom
741 MissingDomainNode lt -> do raiseError $ lt <!> TokenError lt; return $ fallback "Missing Domain"
742
743 where
744
745 validateRangedInt :: Maybe (LToken, ETok) -> Maybe (ListNode RangeNode) -> ValidatorS TypedDomain
746 validateRangedInt maybe_tag' (Just (ListNode _ (Seq [SeqElem a _]) _)) = do
747 let maybe_tag = case maybe_tag' of Nothing -> Nothing ; Just (_, t) -> Just t
748 d <- case a of
749 SingleRangeNode en -> do
750 (t, e) <- typeSplit <$> validateExpression en
751 case t of
752 TypeInt _ -> return $ DomainInt (mkIntTag maybe_tag) [RangeSingle e]
753 TypeMatrix _ _ -> return $ DomainIntE (mkIntTag maybe_tag) e
754 TypeList _ -> return $ DomainIntE (mkIntTag maybe_tag) e
755 TypeSet _ -> return $ DomainIntE (mkIntTag maybe_tag) e
756 _ -> DomainIntE (mkIntTag maybe_tag) e <$ raiseTypeError (symbolRegion en <!> ComplexTypeError "Set/List of int or Int" t)
757 _ -> do
758 r <- validateRange tInt a
759 return $ DomainInt (mkIntTag maybe_tag) [r]
760 return $ Typed tInt d
761 validateRangedInt maybe_tag' (Just ranges) = do
762 let maybe_tag = case maybe_tag' of Nothing -> Nothing ; Just (_, t) -> Just t
763 ranges' <- catMaybes <$> validateList_ (f2n (validateRange tInt)) ranges
764 return . Typed tInt $ DomainInt (mkIntTag maybe_tag) ranges'
765 validateRangedInt maybe_tag' Nothing = do
766 let maybe_tag = case maybe_tag' of Nothing -> Nothing ; Just (_, t) -> Just t
767 return . Typed tInt $ DomainInt (mkIntTag maybe_tag) []
768
769 validateEnumRange :: NameNodeS -> Maybe (ListNode RangeNode) -> ValidatorS TypedDomain
770 validateEnumRange name@(NameNodeS n) ranges = do
771 flagSToken n TtEnum
772 setContextFrom name
773 name' <- validateIdentifierS name
774 _ <- resolveReference (symbolRegion name, Name name')
775 a <- getSymbol name'
776 case a of
777 Just (_, True, t) -> do
778 t' <- getDomainType t
779 rs <- case ranges of
780 Just rs -> pure . catMaybes <$> validateList_ (f2n $ validateRange (getDomainMembers t')) rs
781 Nothing -> return Nothing
782 return $ Typed t' $ DomainEnum (Name name') rs Nothing
783 Just (_, False, t) -> do
784 t' <- getDomainType t
785 case ranges of
786 Nothing -> return . Typed t' $ DomainReference (Name name') Nothing
787 Just rs -> do
788 void $ validateList_ (f2n (validateRange TypeAny)) rs
789 raiseError (symbolRegion name <!> SemanticError "range not supported on non enum ranges")
790 return . Typed t' $ DomainReference (Name name') Nothing
791 Nothing -> return $ fallback "unknown symbol"
792
793 validateTupleDomain :: ListNode DomainNode -> ValidatorS TypedDomain
794 validateTupleDomain doms = do
795 (ts, ds) <- unzip . map typeSplit <$> validateList_ validateDomain doms
796 return $ Typed (TypeTuple ts) (DomainTuple ds)
797
798 validateRecordDomain :: ListNode NamedDomainNode -> ValidatorS TypedDomain
799 validateRecordDomain namedDoms = do
800 lst <- validateList (f2n validateNamedDomainInVariant) namedDoms
801 let lst' = mapMaybe (\(r, m) -> (\x -> (r, x)) <$> m) lst
802 let (ts, ds) = unzip $ map (\(r, (x, typeSplit -> (t, d))) -> ((x, t), (r, (x, d)))) lst'
803 -- push members
804 let t n = Kind (ValueType CatConstant) $ TypeRecordMember n ts
805 mapM_ (\(r, (a, _)) -> putSymbol (a, (r, False, t a))) ds
806 return $ Typed (TypeRecord ts) (DomainRecord (unregion <$> ds))
807
808 validateVariantDomain :: ListNode NamedDomainNode -> ValidatorS TypedDomain
809 validateVariantDomain namedDoms = do
810 lst <- validateList (f2n validateNamedDomainInVariant) namedDoms
811 let lst' = mapMaybe (\(r, m) -> (\x -> (r, x)) <$> m) lst
812 let (ts, ds) = unzip $ map (\(r, (x, typeSplit -> (t, d))) -> ((x, t), (r, (x, d)))) lst'
813 -- push members
814 let t n = Kind (ValueType CatConstant) $ TypeVariantMember n ts
815 mapM_ (\(r, (a, _)) -> putSymbol (a, (r, False, t a))) ds
816 return $ Typed (TypeVariant ts) (DomainVariant (unregion <$> ds))
817
818 validateMatrixDomain :: ListNode DomainNode -> DomainNode -> ValidatorS TypedDomain
819 validateMatrixDomain indexes dom = do
820 idoms <- validateList_ validateDomain indexes
821 dom' <- validateDomain dom
822 return $ foldr acc dom' idoms
823 where
824 acc :: TypedDomain -> TypedDomain -> TypedDomain
825 acc (Typed t d) (Typed t' d') = Typed (TypeMatrix t t') (DomainMatrix d d')
826
827 validateSetDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
828 validateSetDomain attrs dom = do
829 let repr = ()
830 attrs' <- case attrs of
831 Just a -> validateSetAttributes a
832 Nothing -> return def
833 (t, dom') <- typeSplit <$> validateDomain dom
834 return . Typed (TypeSet t) $ DomainSet repr attrs' dom'
835
836 validateMSetDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
837 validateMSetDomain attrs dom = do
838 let repr = ()
839 attrs' <- case attrs of
840 Just a -> validateMSetAttributes a
841 Nothing -> return def
842 (t, dom') <- typeSplit <$> validateDomain dom
843 return . Typed (TypeMSet t) $ DomainMSet repr attrs' dom'
844
845 validateFunctionDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> DomainNode -> ValidatorS TypedDomain
846 validateFunctionDomain attrs dom1 dom2 = do
847 let _repr = Just () -- placeholder if this gets implemented in future
848 attrs' <- case attrs of
849 Just a -> validateFuncAttributes a
850 Nothing -> return def
851 (t1, d1) <- typeSplit <$> validateDomain dom1
852 (t2, d2) <- typeSplit <$> validateDomain dom2
853 let dType = Typed $ TypeFunction t1 t2
854 return . dType $ DomainFunction () attrs' d1 d2
855
856 validateSequenceDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
857 validateSequenceDomain attrs dom = do
858 let repr = ()
859 attrs' <- case attrs of
860 Just a -> validateSeqAttributes a
861 Nothing -> return def
862 (t, dom') <- typeSplit <$> validateDomain dom
863 return . Typed (TypeSequence t) $ DomainSequence repr attrs' dom'
864
865 validatePermutationDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
866 validatePermutationDomain attrs dom = do
867 let repr = ()
868 attrs' <- case attrs of
869 Just a -> validatePermutationAttributes a
870 Nothing -> return (PermutationAttr SizeAttr_None)
871 (t, dom') <- typeSplit <$> validateDomain dom
872 return . Typed (TypePermutation t) $ DomainPermutation repr attrs' dom'
873
874 validateRelationDomain :: Maybe (ListNode AttributeNode) -> ListNode DomainNode -> ValidatorS TypedDomain
875 validateRelationDomain attrs doms = do
876 let repr = ()
877 attrs' <- case attrs of
878 Just a -> validateRelationAttributes a
879 Nothing -> return def
880
881 (ts, doms') <- unzip . map typeSplit <$> validateList_ validateDomain doms
882 return . Typed (TypeRelation ts) $ DomainRelation repr attrs' doms'
883
884 validatePartitionDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
885 validatePartitionDomain attrs dom = do
886 let repr = ()
887 attrs' <- case attrs of
888 Just a -> validatePartitionAttributes a
889 Nothing -> return def
890 (t, dom') <- typeSplit <$> validateDomain dom
891 return . Typed (TypePartition t) $ DomainPartition repr attrs' dom'
892
893 mkIntTag :: Maybe ETok -> IntTag
894 mkIntTag Nothing = TagInt
895 mkIntTag (Just t) =
896 case lexeme t of
897 LIdentifier i -> TaggedInt i
898 _ -> bug $ "mkIntTag" <+> pretty (show t)
899
900 validateIndexedByNode :: Maybe IndexedByNode -> ValidatorS ()
901 validateIndexedByNode Nothing = return ()
902 validateIndexedByNode (Just (IndexedByNode a b)) = [a, b] `are` TtSubKeyword
903
904 todo :: Text -> Validator a
905 todo s = invalid $ ValidatorDiagnostic global $ Error $ InternalErrorS (append "Not Implemented: " s)
906
907 validateSizeAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS (SizeAttr Expression)
908 validateSizeAttributes attrs = do
909 let sizeAttrs = [L_size, L_minSize, L_maxSize]
910 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
911 case filtered of
912 [] -> return SizeAttr_None
913 [(L_size, Just a)] -> return $ SizeAttr_Size a
914 [(L_minSize, Just a)] -> return (SizeAttr_MinSize a)
915 [(L_maxSize, Just a)] -> return (SizeAttr_MaxSize a)
916 [(L_minSize, Just a), (L_maxSize, Just b)] -> return (SizeAttr_MinMaxSize a b)
917 as -> do
918 void $ contextError $ SemanticError $ pack $ "Incompatible attributes size:" ++ show as
919 return def
920
921 validatePermAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS (SizeAttr Expression)
922 validatePermAttributes attrs = do
923 let permAttrNames = [L_numMoved, L_minNumMoved, L_maxNumMoved]
924 let filtered = sort $ filter (\x -> fst x `elem` permAttrNames) attrs
925 case filtered of
926 [] -> return SizeAttr_None
927 [(L_numMoved, Just a)] -> return $ SizeAttr_Size a
928 [(L_minNumMoved, Just a)] -> return (SizeAttr_MinSize a)
929 [(L_maxNumMoved, Just a)] -> return (SizeAttr_MaxSize a)
930 [(L_minNumMoved, Just a), (L_maxNumMoved, Just b)] -> return (SizeAttr_MinMaxSize a b)
931 as -> do
932 void $ contextError $ SemanticError $ pack $ "Incompatible attributes numMoved:" ++ show as
933 return def
934
935 validatePartSizeAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS (SizeAttr Expression)
936 validatePartSizeAttributes attrs = do
937 let sizeAttrs = [L_partSize, L_minPartSize, L_maxPartSize]
938 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
939 case filtered of
940 [] -> return SizeAttr_None
941 [(L_partSize, Just a)] -> return (SizeAttr_Size a)
942 [(L_minPartSize, Just a)] -> return (SizeAttr_MinSize a)
943 [(L_maxPartSize, Just a)] -> return (SizeAttr_MaxSize a)
944 [(L_minPartSize, Just a), (L_maxPartSize, Just b)] -> return (SizeAttr_MinMaxSize a b)
945 as -> do
946 void $ contextError $ SemanticError $ pack $ "Incompatible attributes partitionSize :" ++ show as
947 return def
948
949 validateNumPartAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS (SizeAttr Expression)
950 validateNumPartAttributes attrs = do
951 let sizeAttrs = [L_numParts, L_maxNumParts, L_minNumParts]
952 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
953 case filtered of
954 [] -> return SizeAttr_None
955 [(L_numParts, Just a)] -> return (SizeAttr_Size a)
956 [(L_minNumParts, Just a)] -> return (SizeAttr_MinSize a)
957 [(L_maxNumParts, Just a)] -> return (SizeAttr_MaxSize a)
958 [(L_minNumParts, Just a), (L_maxNumParts, Just b)] -> return (SizeAttr_MinMaxSize a b)
959 as -> do
960 void $ contextError $ SemanticError $ pack $ "Incompatible attributes partitionSize :" ++ show as
961 return def
962
963 validateJectivityAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS JectivityAttr
964 validateJectivityAttributes attrs = do
965 let sizeAttrs = [L_injective, L_surjective, L_bijective]
966 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
967 case filtered of
968 [] -> return JectivityAttr_None
969 [(L_injective, _)] -> return JectivityAttr_Injective
970 [(L_surjective, _)] -> return JectivityAttr_Surjective
971 [(L_bijective, _)] -> return JectivityAttr_Bijective
972 [(L_injective, _), (L_surjective, _)] -> do
973 contextInfo $ UnclassifiedInfo "Inj and Sur can be combined to bijective"
974 return JectivityAttr_Bijective
975 as -> do
976 void $ contextError $ SemanticError $ pack $ "Incompatible attributes jectivity" ++ show as
977 return def
978
979 validateSetAttributes :: ListNode AttributeNode -> ValidatorS (SetAttr Expression)
980 validateSetAttributes atts = do
981 setContextFrom atts
982 attrs <- catMaybes <$> validateList_ (validateAttributeNode setValidAttrs) atts
983 size <- validateSizeAttributes attrs
984 return $ SetAttr size
985
986 validateMSetAttributes :: ListNode AttributeNode -> ValidatorS (MSetAttr Expression)
987 validateMSetAttributes atts = do
988 setContextFrom atts
989 attrs <- catMaybes <$> validateList_ (validateAttributeNode msetValidAttrs) atts
990 size <- validateSizeAttributes attrs
991 occurs <- validateOccursAttrs attrs
992 return $ MSetAttr size occurs
993 where
994 validateOccursAttrs attrs = do
995 let sizeAttrs = [L_minOccur, L_maxOccur]
996 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
997 case filtered of
998 [] -> return OccurAttr_None
999 [(L_minOccur, Just a)] -> return (OccurAttr_MinOccur a)
1000 [(L_maxOccur, Just a)] -> return (OccurAttr_MaxOccur a)
1001 [(L_minOccur, Just a), (L_maxOccur, Just b)] -> return (OccurAttr_MinMaxOccur a b)
1002 as -> do
1003 void $ contextError $ SemanticError $ pack $ "Bad args to occurs" ++ show as
1004 return def
1005
1006 validateFuncAttributes :: ListNode AttributeNode -> ValidatorS (FunctionAttr Expression)
1007 validateFuncAttributes atts = do
1008 attrs <- catMaybes <$> validateList_ (validateAttributeNode funAttrs) atts
1009 size <- validateSizeAttributes attrs
1010 let parts = if L_total `elem` map fst attrs then PartialityAttr_Total else PartialityAttr_Partial
1011 jectivity <- validateJectivityAttributes attrs
1012 return (FunctionAttr size parts jectivity)
1013
1014 validateSeqAttributes :: ListNode AttributeNode -> ValidatorS (SequenceAttr Expression)
1015 validateSeqAttributes atts = do
1016 attrs <- catMaybes <$> validateList_ (validateAttributeNode seqAttrs) atts
1017 size <- validateSizeAttributes attrs
1018 jectivity <- validateJectivityAttributes attrs
1019 return $ SequenceAttr size jectivity
1020
1021 validatePermutationAttributes :: ListNode AttributeNode -> ValidatorS (PermutationAttr Expression)
1022 validatePermutationAttributes atts = do
1023 attrs <- catMaybes <$> validateList_ (validateAttributeNode permValidAttrs) atts
1024 size <- validatePermAttributes attrs
1025 return $ PermutationAttr size
1026
1027 validateRelationAttributes :: ListNode AttributeNode -> ValidatorS (RelationAttr Expression)
1028 validateRelationAttributes atts = do
1029 setContextFrom atts
1030 attrs <- catMaybes <$> validateList_ (validateAttributeNode relAttrs) atts
1031 size <- validateSizeAttributes attrs
1032 others <- catMaybes <$> validateArray validateBinaryRel (filter (\x -> fst x `elem` map fst binRelAttrs) attrs)
1033 return $ RelationAttr size (BinaryRelationAttrs $ S.fromList others)
1034 where
1035 validateBinaryRel :: (Lexeme, Maybe Expression) -> Validator BinaryRelationAttr
1036 validateBinaryRel (l, _) = case lexemeToBinRel l of
1037 Just b -> return . pure $ b
1038 Nothing -> contextError $ InternalErrorS $ pack $ "Not found (bin rel) " ++ show l
1039
1040 validatePartitionAttributes :: ListNode AttributeNode -> ValidatorS (PartitionAttr Expression)
1041 validatePartitionAttributes atts = do
1042 attrs <- catMaybes <$> validateList_ (validateAttributeNode partitionAttrs) atts
1043 -- guard size attrs and complete as this is default
1044 size <- validateNumPartAttributes attrs
1045 partSize <- validatePartSizeAttributes attrs
1046 let regular = L_regular `elem` map fst attrs
1047 return $ PartitionAttr size partSize regular
1048
1049 validateAttributeNode :: Map Lexeme Bool -> AttributeNode -> Validator (Lexeme, Maybe Expression)
1050 validateAttributeNode vs (NamedAttributeNode t Nothing) = do
1051 flagSToken t TtAttribute
1052 name <- validateSToken t
1053 putDocs (T.pack $ show name) t
1054 case M.lookup name vs of
1055 Nothing -> invalid $ t <!> CustomError "Not a valid attribute in this context"
1056 Just True -> invalid $ t <!> CustomError "Argument required"
1057 Just False -> return . pure $ (name, Nothing)
1058 validateAttributeNode vs (NamedAttributeNode t (Just e)) = do
1059 flagSToken t TtAttribute
1060 setContextFrom e
1061 expr <- validateExpression e ?=> exactly tInt
1062 name <- validateSToken t
1063 putDocs (T.pack $ show name) t
1064 case M.lookup name vs of
1065 Nothing -> invalid $ t <!> CustomError "Not a valid attribute in this context"
1066 Just False -> invalid $ t <!> SemanticError "attribute %name% does not take an argument"
1067 Just True -> return . pure $ (\x -> (name, Just x)) expr
1068
1069 validateNamedDomainInVariant :: NamedDomainNode -> ValidatorS (Name, TypedDomain)
1070 validateNamedDomainInVariant (NameDomainNode name m_dom) = do
1071 name' <- validateNameAs TtRecordMember name
1072 domain' <- case m_dom of
1073 Nothing -> return . Typed tInt $ DomainInt TagInt [RangeSingle 0]
1074 Just (l, d) -> do l `isA'` TtOperator; validateDomain d
1075 return (name', domain')
1076
1077 validateNamedDomainInRecord :: NamedDomainNode -> ValidatorS (Name, TypedDomain)
1078 validateNamedDomainInRecord (NameDomainNode name m_dom) = do
1079 name' <- validateNameAs TtRecordMember name
1080 domain' <- case m_dom of
1081 Just (l, d) -> l `isA'` TtOperator >> validateDomain d
1082 Nothing -> do
1083 raiseError $ symbolRegion name <!> SemanticError "Dataless not allowed in record"
1084 return (fallback "Dataless RecordMemeber")
1085 return (name', domain')
1086
1087 validateRange :: Type -> RangeNode -> ValidatorS (Range Expression)
1088 validateRange t range = case range of
1089 SingleRangeNode en -> do ex <- validateExpression en ?=> exactly t; return $ RangeSingle ex
1090 OpenRangeNode dots -> do dots `isA` TtOther "Ellips"; return RangeOpen
1091 RightUnboundedRangeNode e1 dots -> do dots `isA` TtOther "Ellips"; ex <- validateExpression e1 ?=> exactly t; return $ RangeLowerBounded ex
1092 LeftUnboundedRangeNode dots e1 -> do dots `isA` TtOther "Ellips"; ex <- validateExpression e1 ?=> exactly t; return $ RangeUpperBounded ex
1093 BoundedRangeNode e1 dots e2 -> do
1094 dots `isA` TtOther "Ellips"
1095 e1' <- validateExpression e1 ?=> exactly t
1096 e2' <- validateExpression e2 ?=> exactly t
1097 return $ RangeBounded e1' e2'
1098
1099 validateArrowPair :: ArrowPairNode -> Validator (RegionTagged (Typed Expression), RegionTagged (Typed Expression))
1100 validateArrowPair (ArrowPairNode e1 s e2) = do
1101 s `isA'` TtOperator
1102 e1' <- validateExpression e1
1103 e2' <- validateExpression e2
1104 return . pure $ (\a b -> ((symbolRegion e1, a), (symbolRegion e2, b))) e1' e2'
1105
1106 validateExpression :: ExpressionNode -> ValidatorS (Typed Expression)
1107 validateExpression expr = do
1108 setContextFrom expr
1109 res <- case expr of
1110 Literal ln -> validateLiteral ln
1111 IdentifierNode nn -> validateIdentifierExpr nn
1112 MetaVarExpr tok -> do
1113 x <- validateMetaVar tok
1114 return $ Typed TypeAny $ ExpressionMetaVar x
1115 QuantificationExpr qen -> validateQuantificationExpression qen
1116 OperatorExpressionNode oen -> validateOperatorExpression oen
1117 DomainExpression dex -> validateDomainExpression dex
1118 ParenExpression (ParenExpressionNode l1 exp l2) -> checkSymbols [l1, l2] >> validateExpression exp
1119 AbsExpression (ParenExpressionNode l1 exp l2) -> do
1120 [l1, l2] `are` TtOperator
1121 (kExp, exp') <- validateFlexibleExpression exp
1122 typeCheckAbs kExp
1123 return . Typed tInt $ mkOp TwoBarOp [exp']
1124 FunctionalApplicationNode lt ln -> validateFunctionApplication lt ln
1125 AttributeAsConstriant lt exprs -> validateAttributeAsConstraint lt exprs
1126 SpecialCase scn -> validateSpecialCase scn
1127 MissingExpressionNode lt -> do raiseError (lt <!> TokenError lt); return (fallback "Missing expression")
1128 setContextFrom expr
1129 return res
1130 where
1131 typeCheckAbs :: Kind -> ValidatorS ()
1132 typeCheckAbs (Kind DomainType _) = pure ()
1133 typeCheckAbs (Kind ValueType {} t) = case t of
1134 TypeAny -> return ()
1135 TypeInt _ -> return ()
1136 TypeList {} -> return ()
1137 TypeSet {} -> return ()
1138 TypeMSet {} -> return ()
1139 TypeFunction {} -> return ()
1140 TypeSequence {} -> return ()
1141 TypePermutation {} -> return ()
1142 TypeRelation {} -> return ()
1143 TypePartition {} -> return ()
1144 _ -> contextTypeError $ ComplexTypeError "integer or collection" t
1145
1146 validateFlexibleExpression :: ExpressionNode -> ValidatorS (Kind, Expression)
1147 validateFlexibleExpression (IdentifierNode name) = do
1148 n <- validateIdentifierS name
1149 setContextFrom name
1150 t <- resolveReference (symbolRegion name, Name n)
1151 tagWithType (NameNode name) t
1152 return (t, Reference (Name n) Nothing)
1153 validateFlexibleExpression (DomainExpression den) = do
1154 (dType, d) <- typeSplit <$> validateDomainExpression den
1155 return (Kind DomainType dType, d)
1156 validateFlexibleExpression en = do
1157 (t, expr) <- typeSplit <$> validateExpression en
1158 return (simple t, expr)
1159
1160 validateAttributeAsConstraint :: SToken -> ListNode ExpressionNode -> ValidatorS (Typed Expression)
1161 validateAttributeAsConstraint l1 exprs = do
1162 es <- map untype <$> validateList_ validateExpression exprs
1163 do
1164 flagSToken l1 TtAAC
1165 lx <- validateSToken l1
1166 let n = lookup (Name (lexemeText lx)) allSupportedAttributes
1167 r <- case (n, es) of
1168 (Just 1, [e, v]) -> return . pure . Typed TypeBool $ aacBuilder e lx (Just v)
1169 (Just 1, _) -> invalid $ l1 <!> SemanticError (pack $ "Expected 2 args to " ++ show lx ++ "got" ++ show (length es))
1170 (Just 0, [e]) -> return . pure . Typed TypeBool $ aacBuilder e lx Nothing
1171 (Just 0, _) -> invalid $ l1 <!> SemanticError (pack $ "Expected 1 arg to " ++ show lx ++ "got" ++ show (length es))
1172 (_, _) -> invalid $ l1 <!> InternalErrorS "Bad AAC"
1173 return $ fromMaybe (fallback "bad AAC") r
1174 where
1175 aacBuilder e lx y = Op $ MkOpAttributeAsConstraint $ OpAttributeAsConstraint e (fromString (lexemeFace lx)) y
1176
1177 validateSpecialCase :: SpecialCaseNode -> ValidatorS (Typed Expression)
1178 validateSpecialCase (ExprWithDecls l1 ex l2 sts l3) = do
1179 mapM_ validateSToken [l1, l2, l3]
1180 scoped $ do
1181 conds <- validateProgramTree sts
1182 let decls =
1183 [ Declaration (FindOrGiven LocalFind nm dom)
1184 | Declaration (FindOrGiven Find nm dom) <- conds
1185 ]
1186 let cons =
1187 concat
1188 [ xs
1189 | SuchThat xs <- conds
1190 ]
1191 let locals =
1192 if null decls
1193 then DefinednessConstraints cons
1194 else AuxiliaryVars (decls ++ [SuchThat cons])
1195 (t, expr) <- typeSplit <$> validateExpression ex
1196 return . Typed t $ WithLocals expr locals
1197
1198 translateQnName :: Lexeme -> OpType
1199 translateQnName qnName = case qnName of
1200 L_ForAll -> FunctionOp L_fAnd
1201 L_Exists -> FunctionOp L_fOr
1202 L_Sum -> FunctionOp L_Sum
1203 L_Product -> FunctionOp L_Product
1204 _ -> FunctionOp qnName
1205
1206 validateQuantificationExpression :: QuantificationExpressionNode -> ValidatorS (Typed Expression)
1207 validateQuantificationExpression q@(QuantificationExpressionNode name pats over m_guard dot expr) =
1208 do
1209 setContextFrom q
1210 dot `isA'` TtKeyword
1211 scoped $ do
1212 flagSToken name TtQuantifier
1213 name' <- validateSToken name
1214 (over', genDec) <- holdDeclarations $ wrapRegion pats pats SGen $ validateQuantificationOver pats over
1215 (g', gDec) <- case m_guard of
1216 Nothing -> return ([], [])
1217 Just qg ->
1218 holdDeclarations
1219 $ wrapRegion qg qg SGuard
1220 $ validateQuantificationGuard m_guard
1221 setContextFrom expr
1222 let (iType, rType) = case name' of
1223 L_ForAll -> (tCondition, TypeBool)
1224 L_Exists -> (tCondition, TypeBool)
1225 L_Sum -> (exactly tInt, tInt)
1226 L_Product -> (exactly tInt, tInt)
1227 _ -> bug $ pretty ("Unkown quantifier " ++ show name')
1228 (body, bDecl) <-
1229 holdDeclarations
1230 $ wrapRegion expr expr SBody
1231 $ validateExpression expr
1232 ?=> iType
1233 let qBody = Comprehension body (over' ++ g')
1234 let result = Typed rType (mkOp (translateQnName name') [qBody])
1235 putDocs (T.pack $ show name') name
1236 wrapRegion q q (SQuantification (lexemeText name') (simple rType)) (mapM_ addRegion (gDec ++ genDec ++ bDecl))
1237 return result
1238 where
1239 validateQuantificationGuard :: Maybe QuanticationGuard -> ValidatorS [GeneratorOrCondition]
1240 validateQuantificationGuard Nothing = return []
1241 validateQuantificationGuard (Just (QuanticationGuard l1 exp)) = do
1242 l1 `isA` TtOther "Comma"
1243 expr' <- validateExpression exp ?=> exactly TypeBool
1244 return [Condition expr']
1245 validateQuantificationOver :: Sequence AbstractPatternNode -> QuantificationOverNode -> ValidatorS [GeneratorOrCondition]
1246 validateQuantificationOver lpats (QuantifiedSubsetOfNode lt en) = do
1247 lt `isA` TtKeyword
1248 putDocs "powerset_projection" lt
1249 ps <- sequenceElems lpats
1250 exp <- validateExpression en
1251 let (t, e) = typeSplit exp
1252 void $ unifyTypesFailing (TypeSet TypeAny) (symbolRegion en, exp)
1253 let pt = t
1254 apats <- unifyPatterns pt ps
1255 return [Generator $ GenInExpr pat (Op $ MkOpPowerSet $ OpPowerSet e) | pat <- apats]
1256 -- x in exp
1257 validateQuantificationOver lpats (QuantifiedMemberOfNode lt en) = do
1258 lt `isA` TtKeyword
1259 ps <- sequenceElems lpats
1260 exp <- validateExpression en
1261 let (t, e) = typeSplit exp
1262 pt <- projectionType (symbolRegion en) t
1263 apats <- unifyPatterns pt ps
1264 return [Generator $ GenInExpr pat e | pat <- apats]
1265 -- x : domain
1266 validateQuantificationOver lpats (QuantifiedDomainNode (OverDomainNode l1 dom)) = do
1267 l1 `isA'` TtOther "Colon in comprehension"
1268 ps <- sequenceElems lpats
1269 (dType, dom') <- typeSplit <$> validateDomain dom
1270 pt <- projectionTypeDomain (symbolRegion dom) dType
1271 apats <- unifyPatterns pt ps
1272 return [Generator $ GenDomainNoRepr pat dom' | pat <- apats]
1273
1274 validateMetaVar :: SToken -> ValidatorS String
1275 validateMetaVar tok = do
1276 lx <- validateSToken tok
1277 case lx of
1278 LMetaVar s -> return $ unpack s
1279 _ -> bug $ "Bad MetaVar" <+> pretty (show lx)
1280
1281 validateDomainExpression :: DomainExpressionNode -> ValidatorS (Typed Expression)
1282 validateDomainExpression (DomainExpressionNode l1 dom l2) = do
1283 [l1, l2] `are` TtOther "Backtick"
1284 (tdom, dom') <- typeSplit <$> validateDomain dom
1285 return . Typed tdom $ Domain dom'
1286
1287 validateFunctionApplication :: SToken -> ListNode ExpressionNode -> ValidatorS (Typed Expression)
1288 validateFunctionApplication name args = do
1289 args' <- validateList validateFlexibleExpression args
1290 flagSToken name TtFunction
1291 name' <- validateSToken name
1292 putDocs (lexemeText name') name
1293 setContextFrom args
1294 validateFuncOp name' args'
1295
1296 validateIdentifierExpr :: NameNodeS -> ValidatorS (Typed Expression)
1297 validateIdentifierExpr name = do
1298 n <- validateIdentifierS name
1299 setContextFrom name
1300 t <- resolveReference (symbolRegion name, Name n)
1301 checkCategory t
1302 tagWithType (NameNode name) t
1303 t' <- getValueType t
1304 return . Typed t' $ Reference (Name n) Nothing
1305
1306 validateOperatorExpression :: OperatorExpressionNode -> ValidatorS (Typed Expression)
1307 validateOperatorExpression (PrefixOpNode lt expr) = do
1308 flagSToken lt TtOperator
1309 op <- validateSToken lt
1310 setContextFrom expr
1311 let refT = case op of
1312 L_Minus -> tInt
1313 L_ExclamationMark -> TypeBool
1314 _ -> bug . pretty $ "Unknown prefix op " ++ show op
1315 putDocs (T.pack $ "pre_" ++ show op) lt
1316 expr' <- validateExpression expr ?=> exactly refT
1317 return . Typed refT $ mkOp (PrefixOp op) [expr']
1318 -- lookup symbol
1319 validateOperatorExpression (BinaryOpNode lexp op rexp) = do
1320 (lType, lExpr) <- validateFlexibleExpression lexp
1321 (rType, rExpr) <- validateFlexibleExpression rexp
1322 flagSToken op TtOperator
1323 op' <- validateSToken op
1324
1325 let resultValidator = binOpType op'
1326 resultType <- resultValidator (symbolRegion lexp, lType) (symbolRegion rexp, rType)
1327 addRegion
1328 ( RegionInfo
1329 { rRegion = symbolRegion op,
1330 rSubRegion = Nothing,
1331 rRegionType = Documentation (T.pack $ show op'),
1332 rChildren = [],
1333 rTable = M.empty
1334 }
1335 )
1336 return . Typed resultType $ mkBinOp (pack $ lexemeFace op') lExpr rExpr
1337 validateOperatorExpression (PostfixOpNode expr pon) = do
1338 postFixOp <- validatePostfixOp pon
1339 postFixOp expr
1340
1341 validatePostfixOp :: PostfixOpNode -> ValidatorS (ExpressionNode -> ValidatorS (Typed Expression))
1342 validatePostfixOp (OpFactorial lt) = do
1343 lt `isA` TtOperator
1344 putDocs "post_factorial" lt
1345 setContextFrom lt
1346 return $ \exp -> do
1347 v <- validateExpression exp ?=> exactly tInt
1348 return $ Typed tInt $ mkOp FactorialOp [v]
1349 validatePostfixOp (ApplicationNode args) = return $ \exp -> do
1350 let reg = symbolRegion exp
1351 (t, e) <- typeSplit <$> validateExpression exp
1352 case t of
1353 TypeFunction _ _ -> do
1354 args' <- validateList (validateExpression >=> \(Typed t' e') -> return (simple t', e')) args
1355 validateFuncOp L_image ((reg, (simple t, e)) : args')
1356 TypePermutation _ -> do
1357 args' <- validateList (validateExpression >=> \(Typed t' e') -> return (simple t', e')) args
1358 validateFuncOp L_image ((reg, (simple t, e)) : args')
1359 TypeSequence _ -> do
1360 args' <- validateList (validateExpression >=> \(Typed t' e') -> return (simple t', e')) args
1361 validateFuncOp L_image ((reg, (simple t, e)) : args')
1362 _ -> do
1363 as <- catMaybes <$> listElems args
1364 args' <- mapM validateProjectionArgs as
1365 let ys = args' -- [if underscore == v then Nothing else Just (r,Typed t v)| x@(r,(Kind ValueType t,v)) <- args']
1366 iType <- case t of
1367 TypeRelation ts -> checkProjectionArgs ts ys
1368 _ -> do
1369 raiseTypeError $ symbolRegion exp <!> ComplexTypeError "function, permutation or relation" t
1370 let ts = map (maybe TypeAny (typeOf_ . snd)) ys
1371 return $ TypeRelation ts
1372 let op = Op $ MkOpRelationProj $ OpRelationProj e (map (untype . snd <$>) ys)
1373 let resType = if any null ys then iType else TypeBool
1374 return . Typed resType $ op
1375 where
1376 validateProjectionArgs :: ExpressionNode -> ValidatorS (Maybe (RegionTagged (Typed Expression)))
1377 validateProjectionArgs (IdentifierNode (NameNodeS ((StrictToken _ (lexeme -> l))))) | l == LIdentifier "_" = return Nothing
1378 validateProjectionArgs e = validateExpression e >>= \x -> return . pure $ (symbolRegion e, x)
1379
1380 checkProjectionArgs :: [Type] -> [Maybe (RegionTagged (Typed Expression))] -> ValidatorS Type
1381 checkProjectionArgs ref bind = do
1382 unless (length ref == length bind)
1383 $ raiseError
1384 $ symbolRegion args
1385 <!> SemanticError "Member size mismatch for relation"
1386 let pairs = zip ref bind
1387 let (free, bound) = partition (null . snd) pairs
1388 mapM_
1389 ( \(t, x) -> case x of
1390 Nothing -> pure ()
1391 Just v -> void $ unifyTypes t v
1392 )
1393 bound
1394 let freeTypes = map fst free
1395 return $ if null freeTypes then TypeBool else TypeRelation freeTypes
1396 validatePostfixOp (IndexedNode ln) = do
1397 res <- catMaybes <$> listElems ln
1398 return $ \exp -> do
1399 e <- validateExpression exp
1400 foldM validateIndexingOrSlicing e res
1401 validatePostfixOp (ExplicitDomain l1 l2 dom l3) = do
1402 l1 `isA` TtOther "Colon in expr"
1403 l2 `isA` TtOther "BackTick"
1404 l3 `isA'` TtOther "BackTick"
1405 (getDomainMembers -> t, _) <- typeSplit <$> validateDomain dom
1406 return $ \exp -> do
1407 e <- validateExpression exp ?=> exactly t
1408 return . Typed t $ D.Typed e t
1409
1410 validateIndexingOrSlicing :: Typed Expression -> RangeNode -> ValidatorS (Typed Expression)
1411 validateIndexingOrSlicing (Typed t exp) (SingleRangeNode r) = do
1412 setContextFrom r
1413 (vType, e) <- case t of
1414 TypeRecord ts -> validateRecordMemberIndex ts r
1415 TypeVariant ts -> validateRecordMemberIndex ts r
1416 _ -> do
1417 t' <- getIndexingType t
1418 e <- validateExpression r ?=> exactly t'
1419 setContextFrom r
1420 vType <- getIndexedType t (Typed t' e)
1421 return (vType, e)
1422 return . Typed vType $ Op $ MkOpIndexing (OpIndexing exp e)
1423 validateIndexingOrSlicing exp range = do
1424 let (mType, m) = typeSplit exp
1425 setContextFrom range
1426 sType <- getSlicingType mType
1427 r' <- validateRange sType range
1428 let (i, j) = case r' of
1429 RangeOpen -> (Nothing, Nothing)
1430 RangeLowerBounded ex -> (Just ex, Nothing)
1431 RangeUpperBounded ex -> (Nothing, Just ex)
1432 RangeBounded exl exr -> (Just exl, Just exr)
1433 RangeSingle ex -> (Just ex, Just ex) -- This never gets hit in a well formed program
1434 return $ Typed mType $ Op $ MkOpSlicing (OpSlicing m i j)
1435
1436 validateRecordMemberIndex :: [(Name, Type)] -> ExpressionNode -> ValidatorS (Type, Expression)
1437 validateRecordMemberIndex ns (IdentifierNode nn) = do
1438 n <- tagNameAs TtRecordMember nn
1439 let t = lookup n ns
1440 ty <- case t of
1441 Just ty -> return ty
1442 Nothing -> do
1443 raiseError
1444 $ symbolRegion nn
1445 <!> WithReplacements
1446 (SemanticError "Expected member of record/variant ")
1447 [x | (Name x, _) <- ns]
1448 return TypeAny
1449 return (ty, Reference n Nothing)
1450 validateRecordMemberIndex ns (MissingExpressionNode nn) = do
1451 raiseError
1452 $ symbolRegion nn
1453 <!> WithReplacements
1454 (SemanticError "Expected member of record/variant ")
1455 [x | (Name x, _) <- ns]
1456 return (TypeAny, fallback "bad Index")
1457 validateRecordMemberIndex ns en = do
1458 g <- validateExpression en
1459 let msg =
1460 T.concat
1461 [ "Expected one of ",
1462 T.intercalate "," [x | (Name x, _) <- ns],
1463 " "
1464 ]
1465 raiseTypeError $ symbolRegion en <!> ComplexTypeError msg (typeOf_ g)
1466 return (TypeAny, untype g)
1467
1468 getSlicingType :: Type -> ValidatorS Type
1469 getSlicingType TypeAny = return TypeAny
1470 getSlicingType (TypeMatrix i _) = return i
1471 getSlicingType (TypeSequence _) = return tInt
1472 getSlicingType t = do
1473 contextTypeError (CustomError . pack $ "Type " ++ show (pretty t) ++ " does not support slicing")
1474 return TypeAny
1475
1476 getIndexingType :: Type -> ValidatorS Type
1477 getIndexingType TypeAny = return TypeAny
1478 getIndexingType (TypeMatrix i _) = return $ getDomainMembers i
1479 getIndexingType (TypeSequence _) = return tInt
1480 getIndexingType (TypeList _) = return tInt
1481 getIndexingType (TypeTuple _) = return tInt
1482 getIndexingType t = do
1483 contextTypeError (CustomError . pack $ "Type " ++ show (pretty t) ++ " does not support indexing")
1484 return TypeAny
1485
1486 getIndexedType :: Type -> Typed Expression -> ValidatorS Type
1487 getIndexedType (TypeMatrix _ ms) _ = return ms
1488 getIndexedType (TypeSequence t) _ = return t
1489 getIndexedType (TypeTuple ts) ex = case intOut "Index" (untype ex) of
1490 Left _ -> do
1491 contextTypeError (CustomError "Non constant value indexing tuple")
1492 return TypeAny
1493 Right v | v <= 0 || v > toInteger (length ts) -> do
1494 contextTypeError . CustomError . pack $ "Tuple index " ++ show v ++ " out of bounds"
1495 return TypeAny
1496 Right v -> return $ ts `at` (fromInteger v - 1)
1497 getIndexedType (TypeRecord _) (Typed _ _) = bug "Index type called on record, should be handled by special case"
1498 getIndexedType (TypeVariant _) _ = bug "Index type called on variant, should be handled by special case"
1499 getIndexedType _ _ = return TypeAny
1500
1501 validateLiteral :: LiteralNode -> ValidatorS (Typed Expression)
1502 validateLiteral litNode = case litNode of
1503 IntLiteral lt maybe_tag -> validateIntLiteral lt maybe_tag >>= \x -> return $ Typed tInt $ Constant x
1504 BoolLiteral lt -> validateBoolLiteral lt >>= \x -> return $ Typed TypeBool $ Constant x
1505 MatrixLiteral mln -> validateMatrixLiteral mln
1506 TupleLiteralNode (LongTuple lt xs) -> do
1507 lt `isA` TtType
1508 validateLiteral (TupleLiteralNodeShort (ShortTuple xs))
1509 TupleLiteralNodeShort (ShortTuple xs) -> do
1510 es <- validateExprList_ xs
1511 makeTupleLiteral es
1512 RecordLiteral lt ln -> lt `isA` TtType >> validateRecordLiteral ln
1513 VariantLiteral lt ln -> lt `isA` TtType >> validateVariantLiteral ln
1514 SetLiteral ls -> validateSetLiteral ls
1515 MSetLiteral lt ls -> lt `isA` TtType >> validateMSetLiteral ls
1516 FunctionLiteral lt ln -> lt `isA` TtType >> validateFunctionLiteral ln
1517 SequenceLiteral lt ln -> lt `isA` TtType >> validateSequenceLiteral ln
1518 PermutationLiteral lt ln -> lt `isA` TtType >> validatePermutationLiteral ln
1519 RelationLiteral lt ln -> lt `isA` TtType >> validateRelationLiteral ln
1520 PartitionLiteral lt ln -> lt `isA` TtType >> validatePartitionLiteral ln
1521
1522 validateSequenceLiteral :: ListNode ExpressionNode -> ValidatorS (Typed Expression)
1523 validateSequenceLiteral x = do
1524 (t, ss) <- typeSplit <$> (sameType =<< validateExprList x)
1525 let lType = TypeSequence t
1526 return . Typed lType $ mkAbstractLiteral $ AbsLitSequence ss
1527
1528 validatePermutationLiteral :: ListNode PermutationElemNode -> ValidatorS (Typed Expression)
1529 validatePermutationLiteral x = do
1530 members <- validateList validatePermutationElem x
1531 (t, xs) <- typeSplit <$> sameType members
1532 let eType = TypePermutation t
1533 return $ Typed eType (mkAbstractLiteral $ AbsLitPermutation xs)
1534 where
1535 validatePermutationElem :: PermutationElemNode -> ValidatorS (Typed [Expression])
1536 validatePermutationElem (PermutationElemNode exprs) = do
1537 xs <- validateExprList exprs
1538 sameType xs
1539
1540 validateRelationLiteral :: ListNode RelationElemNode -> ValidatorS (Typed Expression)
1541 validateRelationLiteral ln = do
1542 ms <- validateList validateRelationMember ln
1543 (t, xs) <- typeSplit <$> sameType ms
1544 setContextFrom ln
1545 return . Typed t $ mkAbstractLiteral $ AbsLitRelation xs
1546 where
1547 validateRelationMember :: RelationElemNode -> ValidatorS (Typed [Expression])
1548 validateRelationMember x = case x of
1549 RelationElemNodeLabeled (LongTuple lt xs) -> lt `isA` TtType >> validateRelationMember (RelationElemNodeShort $ ShortTuple xs)
1550 RelationElemNodeShort (ShortTuple xs) -> do
1551 es <- validateExprList_ xs
1552 let (ts, vs) = unzip $ typeSplit <$> es
1553 return $ Typed (TypeRelation ts) vs
1554
1555 validatePartitionLiteral :: ListNode PartitionElemNode -> ValidatorS (Typed Expression)
1556 validatePartitionLiteral ln = do
1557 members <- validateList validatePartitionElem ln
1558 (t, xs) <- typeSplit <$> sameType members
1559 let eType = TypePartition t
1560 return $ Typed eType (mkAbstractLiteral $ AbsLitPartition xs)
1561 where
1562 validatePartitionElem :: PartitionElemNode -> ValidatorS (Typed [Expression])
1563 validatePartitionElem (PartitionElemNode exprs) = do
1564 xs <- validateExprList exprs
1565 sameType xs
1566
1567 validateRecordLiteral :: ListNode RecordMemberNode -> ValidatorS (Typed Expression)
1568 validateRecordLiteral ln = do
1569 members <- catMaybes <$> listElems ln
1570 case members of
1571 [] -> return $ Typed (TypeRecord []) (mk []) -- REVIEW: should empty records be allowed?
1572 xs -> do
1573 (ns, unzip . map typeSplit -> (ts, es)) <- mapAndUnzipM validateRecordMember xs
1574 let t = TypeRecord $ zip ns ts
1575 return $ Typed t $ mk (zip ns es)
1576 where
1577 mk = mkAbstractLiteral . AbsLitRecord
1578
1579 validateVariantLiteral :: ListNode RecordMemberNode -> ValidatorS (Typed Expression)
1580 validateVariantLiteral ln = do
1581 members <- catMaybes <$> validateList_ (f2n validateRecordMember) ln
1582 res <- case members of
1583 [] -> invalid $ symbolRegion ln <!> SemanticError "Variants must contain exactly one member"
1584 [(n, Typed t v)] -> return . pure . Typed (TypeVariant [(n, t)]) $ AbstractLiteral $ AbsLitVariant Nothing n v
1585 _ : _ -> invalid $ symbolRegion ln <!> SyntaxError "Variants must contain exactly one member" -- tag subsequent members as unexpected
1586 return $ fromMaybe (fallback "bad variant") res
1587
1588 validateRecordMember :: RecordMemberNode -> ValidatorS (Name, Typed Expression)
1589 validateRecordMember (RecordMemberNode name lEq expr) = do
1590 lEq `isA'` TtKeyword
1591 name' <- validateName name
1592 expr' <- validateExpression expr
1593 return (name', expr')
1594
1595 validateFunctionLiteral :: ListNode ArrowPairNode -> ValidatorS (Typed Expression)
1596 validateFunctionLiteral ln = do
1597 pairs <- catMaybes <$> validateList_ validateArrowPair ln
1598 let (pl, pr) = unzip pairs
1599 (lhType, ls) <- typeSplit <$> sameType pl
1600 (rhType, rs) <- typeSplit <$> sameType pr
1601 let fType = TypeFunction lhType rhType
1602 return . Typed fType $ mkAbstractLiteral $ AbsLitFunction $ zip ls rs
1603
1604 validateSetLiteral :: ListNode ExpressionNode -> ValidatorS (Typed Expression)
1605 validateSetLiteral ls = do
1606 xs <- validateList validateExpression ls
1607 (t, es) <- typeSplit <$> sameType xs
1608 return . Typed (TypeSet t) $ mkAbstractLiteral $ AbsLitSet es
1609
1610 validateMSetLiteral :: ListNode ExpressionNode -> ValidatorS (Typed Expression)
1611 validateMSetLiteral ls = do
1612 xs <- validateList validateExpression ls
1613 (t, es) <- typeSplit <$> sameType xs
1614 let eType = TypeMSet t
1615 let result = mkAbstractLiteral $ AbsLitMSet es
1616 return $ Typed eType result
1617
1618 validateMatrixLiteral :: MatrixLiteralNode -> ValidatorS (Typed Expression)
1619 -- Matrix proper
1620 validateMatrixLiteral (MatrixLiteralNode l1 se m_dom Nothing l2) = do
1621 [l1, l2] `are` TtOther "SquareBrackets"
1622 matElems <- validateSequence validateExpression se
1623 (t, es) <- typeSplit <$> sameType matElems
1624 let defaultDomain :: TypedDomain = Typed tInt (mkDomainIntB 1 (fromInt $ genericLength matElems))
1625 dom <- fromMaybe defaultDomain <$> validateOverDomain m_dom
1626 let lit = AbsLitMatrix (untype dom) es
1627 return $ Typed (TypeMatrix tInt t) $ mkAbstractLiteral lit
1628 where
1629 validateOverDomain :: Maybe OverDomainNode -> Validator TypedDomain
1630 validateOverDomain Nothing = return Nothing
1631 validateOverDomain (Just (OverDomainNode l3 dom)) = do l3 `isA'` TtOther "Semicolon in matrix"; pure <$> validateDomain dom
1632
1633 -- Matrix as comprehension
1634 validateMatrixLiteral m@(MatrixLiteralNode l1 se m_dom (Just comp) l2) = do
1635 [l1, l2] `are` TtOther "SquareBrackets"
1636 case m_dom of
1637 Nothing -> return ()
1638 Just p@(OverDomainNode l3 dom) -> do
1639 l3 `isA'` TtOther "Semicolon in matrix"
1640 void $ validateDomain dom
1641 raiseError $ symbolRegion p <!> SemanticError "Index domains are not supported in comprehensions"
1642 scoped
1643 $ do
1644 -- check gens and put locals into scope
1645 (gens, dGens) <- holdDeclarations $ validateComprehension comp
1646 -- now validate expression(s)
1647 (es, dBody) <-
1648 holdDeclarations
1649 $ wrapRegion se se SBody
1650 $ validateSequence validateExpression se
1651 r <- case es of
1652 [] -> return $ fallback "missing" <$ raiseError $ symbolRegion se <!> SemanticError "MissingExpression"
1653 ((_, x) : xs) -> flagExtraExpressions xs >> return x
1654 let bodyType = typeOf_ r
1655 wrapRegion m se (SComprehension (simple $ TypeList bodyType)) (mapM_ addRegion (dGens ++ dBody))
1656 return . Typed (TypeList bodyType) $ Comprehension (untype r) gens
1657 where
1658 flagExtraExpressions :: [RegionTagged a] -> ValidatorS ()
1659 flagExtraExpressions [] = pure ()
1660 flagExtraExpressions xs = raiseError $ catRegions xs <!> SemanticError "Comprehensension may have only one expression before |"
1661
1662 validateComprehension :: ComprehensionNode -> ValidatorS [GeneratorOrCondition]
1663 validateComprehension (ComprehensionNode l1 body) = do
1664 l1 `isA` TtKeyword
1665 concat <$> validateSequence_ validateComprehensionBody body
1666
1667 validateComprehensionBody :: ComprehensionBodyNode -> ValidatorS [GeneratorOrCondition]
1668 -- guard
1669 validateComprehensionBody (CompBodyCondition en) = wrapRegion en en SGuard $ do
1670 e <- validateExpression en ?=> exactly TypeBool
1671 return [Condition e]
1672 -- x in dom
1673 validateComprehensionBody c@(CompBodyDomain apn l1 dom) = wrapRegion c apn SGen $ do
1674 l1 `isA` TtKeyword
1675 putDocs "expr_in_domain_projection" l1
1676 (td, domain) <- typeSplit <$> validateDomain dom
1677 td' <- projectionTypeDomain (symbolRegion dom) td
1678 pats <- validateSequence_ (flip unifyPattern td' . Just) apn
1679 return $ [Generator (GenDomainNoRepr pat domain) | pat <- pats]
1680
1681 -- x <- expr
1682 validateComprehensionBody c@(CompBodyGenExpr apn lt en) = wrapRegion c apn SGen $ do
1683 lt `isA` TtKeyword
1684 putDocs "expr_projection" lt
1685 e <- validateExpression en
1686 let (t, exp) = typeSplit e
1687 t' <- projectionType (symbolRegion en) t
1688 pats <- validateSequence_ (flip unifyPattern t' . Just) apn
1689 return $ [Generator (GenInExpr pat exp) | pat <- pats]
1690 -- letting x be
1691 validateComprehensionBody c@(CompBodyLettingNode l1 nn l2 en) = wrapRegion c nn SLetting $ do
1692 l1 `isA` TtKeyword
1693 l2 `isA'` TtKeyword
1694 (t, expr) <- typeSplit <$> validateExpression en
1695 pat <- unifyPattern (Just nn) t
1696 return [ComprehensionLetting pat expr]
1697
1698 projectionType :: DiagnosticRegion -> Type -> ValidatorS Type
1699 projectionType r t = case t of
1700 TypeAny -> return TypeAny
1701 TypeTuple _ -> return t
1702 TypeMatrix _ ty -> return ty
1703 TypeList ty -> return ty
1704 TypeSet ty -> return ty
1705 TypeMSet ty -> return ty
1706 TypeSequence ty -> return $ TypeTuple [tInt, ty]
1707 TypePermutation ty -> return $ TypeTuple [ty, ty]
1708 TypeRelation ts -> return $ TypeTuple ts
1709 TypePartition ty -> return $ TypeSet ty
1710 TypeFunction fr to -> return $ TypeTuple [fr, to]
1711 _ -> raiseTypeError (r <!> SemanticError (pack $ "Expression of type " ++ show (pretty t) ++ " cannot be projected in a comprehension")) >> return TypeAny
1712
1713 projectionTypeDomain :: DiagnosticRegion -> Type -> ValidatorS Type
1714 projectionTypeDomain _ t = case t of -- TODO check and do properly
1715 TypeAny -> return TypeAny
1716 TypeEnum (Name n) -> return $ TypeInt $ TagEnum n
1717 TypeUnnamed (Name n) -> return $ TypeInt $ TagUnnamed n
1718 _ -> return t
1719
1720 -- _ -> (raiseTypeError $ r <!> SemanticError (pack $ "Domain of type " ++ (show $pretty t) ++ " cannot be projected in a comprehension")) >> return TypeAny
1721
1722 mkAbstractLiteral :: AbstractLiteral Expression -> Expression
1723 mkAbstractLiteral x = case e2c (AbstractLiteral x) of
1724 Nothing -> AbstractLiteral x
1725 Just c -> Constant c
1726
1727 enforceConstraint :: Maybe Bool -> String -> ValidatorS ()
1728 enforceConstraint p msg = case p of
1729 Just True -> return ()
1730 _ -> void (contextError (CustomError $ pack msg))
1731
1732 checkSymbols :: [LToken] -> ValidatorS ()
1733 checkSymbols = mapM_ validateSymbol
1734
1735 -- Raise a non structural error (i.e type error)
1736 raiseError :: ValidatorDiagnostic -> ValidatorS ()
1737 raiseError e = tell [e]
1738
1739 raiseTypeError :: ValidatorDiagnostic -> ValidatorS ()
1740 raiseTypeError e = do
1741 tc <- gets typeChecking
1742 when tc $ raiseError e
1743
1744 makeTupleLiteral :: [Typed Expression] -> ValidatorS (Typed Expression)
1745 makeTupleLiteral members = do
1746 let memberTypes = unzip $ map typeSplit members
1747 let eType = TypeTuple (fst memberTypes)
1748 return . Typed eType . mkAbstractLiteral . AbsLitTuple $ snd memberTypes
1749
1750 validateIntLiteral :: SToken -> Maybe (LToken, ETok) -> ValidatorS Constant
1751 validateIntLiteral t maybe_tag' = do
1752 let maybe_tag = case maybe_tag' of Nothing -> Nothing ; Just (_, tag) -> Just tag
1753 flagSToken t TtNumber
1754 l <- validateSToken t
1755 let tag = case maybe_tag of
1756 Just ta -> case lexeme ta of
1757 LIdentifier ta_i -> TaggedInt ta_i
1758 _ -> TagInt
1759 Nothing -> TagInt
1760 case l of
1761 (LIntLiteral x) -> return $ ConstantInt tag x
1762 _ -> error "Bad int literal"
1763
1764 validateBoolLiteral :: SToken -> ValidatorS Constant
1765 validateBoolLiteral t = do
1766 flagSToken t TtBool
1767 l <- validateSToken t
1768 case l of
1769 L_true -> return $ ConstantBool True
1770 L_false -> return $ ConstantBool False
1771 _ -> error "Bad bool literal"
1772
1773 validateNameList :: Sequence NameNode -> ValidatorS [RegionTagged Name]
1774 validateNameList = validateSequence validateName
1775
1776 validateNameList_ :: Sequence NameNode -> ValidatorS [Name]
1777 validateNameList_ = validateSequence_ validateName
1778
1779 validateIdentifierS :: NameNodeS -> ValidatorS Text
1780 validateIdentifierS (NameNodeS iden) = do
1781 q <- validateSToken iden
1782 case q of
1783 (LIdentifier x) -> checkName x >> return x
1784 _ -> bug $ "Name wasn't a name:" <+> pretty (show q)
1785 where
1786 checkName :: Text -> Validator Text
1787 checkName "" = invalid $ iden <!> SemanticError "Empty names not allowed"
1788 checkName "\"\"" = invalid $ iden <!> SemanticError "Empty names not allowed"
1789 checkName x = return . pure $ x
1790
1791 validateIdentifier :: NameNode -> ValidatorS Text
1792 validateIdentifier (NameNode nns) = validateIdentifierS nns
1793 validateIdentifier (MissingNameNode iden) = do
1794 _ <- validateSymbol iden
1795 return " <Missing name>"
1796
1797 validateName :: NameNode -> ValidatorS Name
1798 validateName name = do
1799 n <- validateIdentifier name
1800 return (Name n)
1801
1802 validateNameAs :: TagType -> NameNode -> ValidatorS Name
1803 validateNameAs f (NameNode n) = tagNameAs f n
1804 validateNameAs _ name = validateName name
1805
1806 tagNameAs :: TagType -> NameNodeS -> ValidatorS Name
1807 tagNameAs f nn@(NameNodeS n) = flagSToken n f >> Name <$> validateIdentifier (NameNode nn)
1808
1809 listToSeq :: ListNode a -> ValidatorS (Sequence a)
1810 listToSeq (ListNode l1 s l2) = checkSymbols [l1, l2] >> return s
1811
1812 -- visit a sequence, return a list of elements, nothing if missing
1813 sequenceElems :: (HighLevelTree a) => Sequence a -> ValidatorS [Maybe a]
1814 sequenceElems (Seq els) = mapM (validateSequenceElem_ validateIdentity) els
1815
1816 listElems :: (HighLevelTree a) => ListNode a -> ValidatorS [Maybe a]
1817 listElems = sequenceElems <=< listToSeq
1818
1819 validateIdentity :: a -> Validator a
1820 validateIdentity = return . pure
1821
1822 validateArray :: (a -> ValidatorS b) -> [a] -> ValidatorS [b]
1823 validateArray = mapM
1824
1825 validateList :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> ListNode a -> ValidatorS [RegionTagged b]
1826 validateList validator (ListNode st seq end) = do
1827 _ <- validateSymbol st
1828 _ <- validateSymbol end
1829 validateSequence validator seq
1830
1831 validateList_ :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> ListNode a -> ValidatorS [b]
1832 validateList_ validator (ListNode st seq end) = do
1833 _ <- validateSymbol st
1834 _ <- validateSymbol end
1835 validateSequence_ validator seq
1836
1837 -- mapPrefixToOp :: Lexeme -> Text
1838 -- mapPrefixToOp x = case x of
1839 -- L_Minus -> "negate"
1840 -- L_ExclamationMark -> "not"
1841 -- _ -> pack $ lexemeFace x
1842
1843 validateSequence :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> Sequence a -> ValidatorS [RegionTagged b]
1844 validateSequence f (Seq vals) = validateArray (validateSequenceElem f) vals
1845
1846 validateSequence_ :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> Sequence a -> ValidatorS [b]
1847 validateSequence_ f s = do
1848 q <- validateSequence f s
1849 return . map snd $ q
1850
1851 validateSequenceElem :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> SeqElem a -> ValidatorS (RegionTagged b)
1852 validateSequenceElem f (SeqElem i s) = do
1853 case s of
1854 Nothing -> pure ()
1855 Just lt -> void $ validateSymbol lt
1856 v <- f i
1857 return (symbolRegion i, v)
1858 validateSequenceElem _ (MissingSeqElem plc sepr) = do
1859 checkSymbols [sepr]
1860 raiseError $ symbolRegion plc <!> TokenError plc
1861 return (symbolRegion plc, fallback "Missing elem")
1862
1863 validateSequenceElem_ :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> SeqElem a -> ValidatorS b
1864 validateSequenceElem_ f (SeqElem i s) = do
1865 case s of
1866 Nothing -> pure ()
1867 Just lt -> void $ validateSymbol lt
1868 f i
1869 validateSequenceElem_ _ (MissingSeqElem plc sepr) = do
1870 checkSymbols [sepr]
1871 raiseError $ symbolRegion plc <!> TokenError plc
1872 return $ fallback "Missing Elem"
1873
1874 validateExprList :: ListNode ExpressionNode -> ValidatorS [RegionTagged (Typed Expression)]
1875 validateExprList = validateList validateExpression
1876
1877 validateExprList_ :: ListNode ExpressionNode -> ValidatorS [Typed Expression]
1878 validateExprList_ = validateList_ validateExpression
1879
1880 offsetPositionBy :: Int -> SourcePos -> SourcePos
1881 offsetPositionBy amt sp@(SourcePos _ _ (unPos -> r)) = sp {sourceColumn = mkPos (amt + r)}
1882
1883 data DiagnosticRegion = DiagnosticRegion
1884 { drSourcePos :: SourcePos,
1885 drEndPos :: SourcePos,
1886 drOffset :: Int,
1887 drLength :: Int
1888 }
1889 deriving (Show, Eq, Ord)
1890
1891 global :: DiagnosticRegion
1892 global = DiagnosticRegion sourcePos0 sourcePos0 0 0
1893
1894 -- getTokenRegion :: LToken -> DiagnosticRegion
1895 -- getTokenRegion a = do
1896 -- let h =case a of
1897 -- RealToken et -> et
1898 -- MissingToken et -> et
1899 -- SkippedToken et -> et
1900 -- let start = tokenSourcePos h
1901 -- let offset = tokenStart h
1902 -- let tLength =case a of
1903 -- RealToken _ -> trueLength h
1904 -- MissingToken _ -> 1
1905 -- SkippedToken _ -> trueLength h
1906 -- DiagnosticRegion start (offsetPositionBy tLength start) offset tLength
1907
1908 symbolRegion :: (HighLevelTree a) => a -> DiagnosticRegion
1909 symbolRegion a = case range of
1910 (h :<| rst) -> do
1911 let end = case viewr rst of
1912 EmptyR -> h
1913 _ :> et -> et
1914 let start = tokenSourcePos h
1915 let offset = tokenStartOffset h
1916 let tLength = sum (totalLength <$> rst) + trueLength h
1917 let en = sourcePosAfter end
1918 DiagnosticRegion start en offset tLength
1919 _ -> global
1920 where
1921 range :: Seq ETok = flattenSeq a
1922
1923 (<!>) :: (WithRegion a) => a -> ErrorType -> ValidatorDiagnostic
1924 t <!> e = ValidatorDiagnostic (getRegion t) $ Error e
1925
1926 (/!\) :: (WithRegion a) => a -> WarningType -> ValidatorDiagnostic
1927 t /!\ e = ValidatorDiagnostic (getRegion t) $ Warning e
1928
1929 (<?>) :: (WithRegion a) => a -> InfoType -> ValidatorDiagnostic
1930 t <?> e = ValidatorDiagnostic (getRegion t) $ Info e
1931
1932 -- (<?!>) :: WithRegion a => Maybe a -> ErrorType -> ValidatorDiagnostic
1933 -- Nothing <?!> e = ValidatorDiagnostic global $ Error e
1934 -- Just t <?!> e = t <!> e
1935
1936 contextError :: ErrorType -> Validator a
1937 contextError e = do
1938 q <- getContext
1939 invalid $ ValidatorDiagnostic q $ Error e
1940
1941 contextTypeError :: ErrorType -> ValidatorS ()
1942 contextTypeError e = do
1943 q <- getContext
1944 tc <- gets typeChecking
1945 when tc $ raiseError $ ValidatorDiagnostic q $ Error e
1946
1947 contextInfo :: InfoType -> ValidatorS ()
1948 contextInfo e = do
1949 q <- getContext
1950 tell [ValidatorDiagnostic q $ Info e]
1951 return ()
1952
1953 -- getType :: (Pretty a ,TypeOf a) => a -> ValidatorS Type
1954 -- getType a = do
1955 -- tc <- gets typeChecking
1956 -- (if tc then (do
1957 -- let t = let ?typeCheckerMode = StronglyTyped in typeOf a
1958 -- case t of
1959 -- Left err -> do
1960 -- void $ contextError (CustomError . pack $ "type err in :" ++ show (pretty a) ++ "err:" ++ show err)
1961 -- return TypeAny
1962 -- Right ty -> return ty) else return TypeAny)
1963
1964 -- assertType :: (Pretty a,TypeOf a) => Typed a -> Type -> Text -> ValidatorS ()
1965 -- assertType v ref msg = do
1966 -- let Typed t _ = v
1967 -- tc <- gets typeChecking
1968 -- unless (not tc || t == ref) $ void . contextError $ CustomError msg
1969
1970 resolveReference :: RegionTagged Name -> ValidatorS Kind
1971 resolveReference (r, Name n) | n /= "" = do
1972 c <- getSymbol n
1973 case c of
1974 Nothing -> raiseTypeError (r <!> CustomError (T.concat ["Symbol not found \"", n, "\""])) >> return (simple TypeAny)
1975 Just (reg, _, t) -> do
1976 putReference r n t reg
1977 -- addRegion (RegionInfo {rRegion=r,rText=n, rType=Just t, rDeclaration=Ref reg})
1978 return t
1979 resolveReference _ = return $ simple TypeAny
1980
1981 sameType :: [RegionTagged (Typed a)] -> ValidatorS (Typed [a])
1982 sameType [] = return $ Typed TypeAny []
1983 sameType xs@(x : _) = do
1984 let ?typeCheckerMode = StronglyTyped
1985 let t = mostDefined $ map (typeOf_ . snd) xs
1986 let t' = mostDefined [t, typeOf_ $ snd x] -- Do this again to set type to first elem if possible
1987 xs' <- mapM (unifyTypes t') xs
1988 return $ Typed t' xs'
1989
1990 typesUnifyS :: [Type] -> Bool
1991 typesUnifyS = let ?typeCheckerMode = StronglyTyped in typesUnify
1992
1993 mostDefinedS :: [Type] -> Type
1994 mostDefinedS [] = TypeAny
1995 mostDefinedS [x] = x
1996 mostDefinedS (x : xs) =
1997 let ?typeCheckerMode = StronglyTyped
1998 in case mostDefined (xs ++ [x]) of
1999 TypeAny -> x
2000 t -> t
2001
2002 unifyTypes :: Type -> RegionTagged (Typed a) -> ValidatorS a
2003 unifyTypes _ (r, Typed TypeAny a) = raiseError (r /!\ AmbiguousTypeWarning) >> return a
2004 unifyTypes t (r, Typed t' a) = do
2005 let ?typeCheckerMode = StronglyTyped
2006 if typesUnify [t', t] then pure () else raiseTypeError $ r <!> TypeError t t'
2007 return a
2008
2009 unifyTypesFailing :: Type -> RegionTagged (Typed a) -> Validator a
2010 unifyTypesFailing _ (r, Typed TypeAny a) = raiseError (r /!\ AmbiguousTypeWarning) >> return (Just a)
2011 unifyTypesFailing t (r, Typed t' a) = do
2012 tc <- gets typeChecking
2013 let ?typeCheckerMode = StronglyTyped
2014 if not tc || typesUnify [t', t] then return $ Just a else invalid (r <!> TypeError t t')
2015
2016 scoped :: ValidatorS a -> ValidatorS a
2017 scoped m = do
2018 st <- gets symbolTable
2019 res <- m
2020 modifySymbolTable $ const st
2021 return res
2022
2023 unifyPatterns :: Type -> [Maybe AbstractPatternNode] -> ValidatorS [AbstractPattern]
2024 unifyPatterns t = mapM (`unifyPattern` t)
2025
2026 unifyPattern :: Maybe AbstractPatternNode -> Type -> ValidatorS AbstractPattern
2027 unifyPattern (Just (AbstractIdentifier nn)) t = do
2028 nm <- tagNameAs TtLocal nn
2029 let n = case nm of
2030 Name txt -> txt
2031 NameMetaVar s -> T.pack s
2032 _ -> bug "Bad name "
2033 void $ putSymbol (Name n, (symbolRegion nn, False, simple t))
2034 unless (n == "_") $ addRegion $ mkDeclaration (symbolRegion nn) n (simple t)
2035 -- addRegion (RegionInfo (symbolRegion nn) (Just $ simple t) n Definition)
2036 return $ Single $ Name n
2037 unifyPattern (Just (AbstractMetaVar lt)) _ = do
2038 s <- validateMetaVar lt
2039 return $ AbstractPatternMetaVar s
2040 unifyPattern (Just (AbstractPatternTuple m_lt ln)) t = do
2041 sps <- listToSeq ln
2042 ps <- sequenceElems sps
2043 case m_lt of
2044 Nothing -> void $ return ()
2045 Just lt -> lt `isA'` TtType
2046 memberTypes <- case t of
2047 TypeAny -> return $ replicate (length ps) TypeAny
2048 TypeTuple ts -> do
2049 let dif = length ts - length ps
2050 unless (dif <= 0) $ raiseError $ symbolRegion ln <!> (CustomError . T.pack $ "Missing " ++ show dif ++ " fields from projection tuple, if you dont want the value, use '_'")
2051 return ts
2052 _ -> replicate (length ps) TypeAny <$ raiseTypeError (symbolRegion ln <!> CustomError (T.concat ["Could not project ", prettyT t, " onto tuple pattern"]))
2053
2054 let (paired, unpaired) = splitAt (length memberTypes) ps
2055 let q = zip paired memberTypes
2056 aps <- mapM (uncurry unifyPattern) q
2057 mapM_ (\x -> raiseError $ symbolRegion x <!> CustomError "Extraneous tuple field from projection") (catMaybes unpaired)
2058 return $ AbsPatTuple aps
2059 unifyPattern (Just (AbstractPatternMatrix ln)) t = do
2060 sps <- listToSeq ln
2061 ps <- sequenceElems sps
2062 memberTypes <- case t of
2063 TypeAny -> return $ repeat TypeAny
2064 TypeList ty -> return $ repeat ty
2065 TypeMatrix _ ty -> return $ repeat ty
2066 _ -> repeat TypeAny <$ raiseTypeError (symbolRegion ln <!> CustomError (T.concat ["Could not project ", prettyT t, " onto list pattern"]))
2067
2068 let q = zip ps memberTypes
2069 aps <- mapM (uncurry unifyPattern) q
2070 return $ AbsPatMatrix aps
2071 unifyPattern (Just (AbstractPatternSet ln)) t = do
2072 sps <- listToSeq ln
2073 ps <- sequenceElems sps
2074 memberTypes <- case t of
2075 TypeAny -> return $ repeat TypeAny
2076 TypeSet ty -> return $ repeat ty
2077 TypeMSet ty -> return $ repeat ty
2078 _ -> repeat TypeAny <$ raiseTypeError (symbolRegion ln <!> CustomError (T.concat ["Could not project ", prettyT t, " onto set pattern"]))
2079 let q = zip ps memberTypes
2080 aps <- mapM (uncurry unifyPattern) q
2081 return $ AbsPatSet aps
2082 unifyPattern Nothing _ = return . Single $ fallback "No Pattern"
2083
2084 catRegions :: [RegionTagged a] -> DiagnosticRegion
2085 catRegions [] = global
2086 catRegions (x:xs) =
2087 DiagnosticRegion
2088 { drSourcePos = drSourcePos $ fst x,
2089 drEndPos = drEndPos $ fst $ last xs,
2090 drOffset = drOffset $ fst x,
2091 drLength = sum $ map (drLength . fst) (x:xs)
2092 }
2093
2094 getMemberTypes :: Type -> ValidatorS [Type]
2095 getMemberTypes t = case t of
2096 TypeAny -> return $ repeat TypeAny
2097 TypeTuple tys -> return tys
2098 _ -> return $ repeat TypeAny
2099
2100 getDomainMembers :: Type -> Type
2101 getDomainMembers t = case t of
2102 TypeAny -> t
2103 TypeBool -> t
2104 TypeInt it -> case it of
2105 TaggedInt {} -> t
2106 TagInt -> t
2107 TagEnum _ -> error "Domain should use typeEnum instead"
2108 TagUnnamed _ -> error "Domain should use typeUnamed instead"
2109 TypeEnum n -> TypeInt . TagEnum $ case n of
2110 Name txt -> txt
2111 MachineName {} -> error "This should never be user specified"
2112 NameMetaVar s -> pack s
2113 TypeUnnamed n -> TypeInt . TagUnnamed $ case n of
2114 Name txt -> txt
2115 MachineName {} -> error "This should never be user specified"
2116 NameMetaVar s -> pack s
2117 TypeTuple tys -> TypeTuple $ map getDomainMembers tys
2118 TypeRecord tys -> TypeRecord $ map (second getDomainMembers) tys
2119 TypeVariant tys -> TypeVariant $ map (second getDomainMembers) tys
2120 TypeList ty -> TypeList $ getDomainMembers ty
2121 TypeMatrix ty ty' -> TypeMatrix ty $ getDomainMembers ty'
2122 TypeSet ty -> TypeSet $ getDomainMembers ty
2123 TypeMSet ty -> TypeMSet $ getDomainMembers ty
2124 TypeFunction ty ty' -> TypeFunction (getDomainMembers ty) (getDomainMembers ty')
2125 TypeSequence ty -> TypeSequence $ getDomainMembers ty
2126 TypePermutation ty -> TypePermutation $ getDomainMembers ty
2127 TypeRelation tys -> TypeRelation $ map getDomainMembers tys
2128 TypePartition ty -> TypePartition $ getDomainMembers ty
2129 _ -> bug $ "Unknown domain type" <+> pretty t
2130
2131 getDomainFromValue :: Type -> Type
2132 getDomainFromValue t = case t of
2133 TypeAny -> t
2134 TypeBool -> t
2135 TypeInt it -> case it of
2136 TaggedInt {} -> t
2137 TagInt -> t
2138 TagEnum n -> TypeEnum (Name n)
2139 TagUnnamed n -> TypeUnnamed (Name n)
2140 TypeEnum _ -> t
2141 TypeUnnamed _ -> t
2142 TypeTuple tys -> TypeTuple $ map getDomainFromValue tys
2143 TypeRecord tys -> TypeRecord $ map (second getDomainFromValue) tys
2144 TypeVariant tys -> TypeVariant $ map (second getDomainFromValue) tys
2145 TypeList ty -> TypeList $ getDomainFromValue ty
2146 TypeMatrix ty ty' -> TypeMatrix ty $ getDomainFromValue ty'
2147 TypeSet ty -> TypeSet $ getDomainFromValue ty
2148 TypeMSet ty -> TypeMSet $ getDomainFromValue ty
2149 TypeFunction ty ty' -> TypeFunction (getDomainFromValue ty) (getDomainFromValue ty')
2150 TypeSequence ty -> TypeSequence $ getDomainFromValue ty
2151 TypePermutation ty -> TypePermutation $ getDomainFromValue ty
2152 TypeRelation tys -> TypeRelation $ map getDomainFromValue tys
2153 TypePartition ty -> TypePartition $ getDomainFromValue ty
2154 _ -> bug $ "Unknown member type" <+> pretty t
2155
2156 data DomainTyped a = DomainTyped DomainType a
2157
2158 data DomainSize = Unkown | Infinite | Sized Int
2159
2160 data DomainType
2161 = DomainTypeBool
2162 | DomainTypeInt DomainSize
2163 | DomainTypeTuple [DomainType]
2164
2165 f2n :: (a -> ValidatorS b) -> a -> Validator b
2166 f2n f a = do
2167 q <- f a
2168 return $ Just q
2169
2170 class Fallback a where
2171 fallback :: Text -> a
2172
2173 instance Fallback (Domain () Expression) where
2174 fallback reason = DomainAny reason TypeAny
2175
2176 instance Fallback Expression where
2177 fallback reason = Reference (Name reason) Nothing
2178
2179 instance (Fallback a) => Fallback (Typed a) where
2180 fallback = Typed TypeAny . fallback
2181
2182 instance (Fallback a) => Fallback (Kind, a) where
2183 fallback msg = (Kind (ValueType CatConstant) TypeAny, fallback msg)
2184
2185 instance Fallback (Maybe a) where
2186 fallback = const Nothing
2187
2188 instance Fallback Name where
2189 fallback = Name
2190
2191 instance Fallback [a] where
2192 fallback :: Text -> [a]
2193 fallback = const []
2194
2195 instance Fallback AbstractPattern where
2196 fallback = Single . fallback
2197
2198 type FuncOpDec = Int
2199
2200 funcOpBuilder :: Lexeme -> [Arg] -> ValidatorS (Typed Expression)
2201 funcOpBuilder l = functionOps l (mkOp $ FunctionOp l)
2202
2203
2204 functionOps :: Lexeme -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2205 functionOps l = case l of
2206 L_fAnd -> unFuncV isLogicalContainer (pure . const TypeBool)
2207 L_fOr -> unFuncV isLogicalContainer (pure . const TypeBool)
2208 L_fXor -> unFuncV isLogicalContainer (pure . const TypeBool)
2209 L_Sum -> unFuncV sumArgs (pure . const tInt)
2210 L_Product -> unFunc (valueOnly sumArgs) (pure . const tInt)
2211 L_true -> unFuncV anyType (pure . const TypeBool)
2212 L_toInt -> unFuncV (only TypeBool) (pure . const tInt)
2213 L_makeTable -> unFuncV (only TypeBool) (pure . const TypeBool)
2214 L_table -> biFuncV tableArgs (const2 TypeBool)
2215 L_gcc -> triFunc (each3 $ valueOnly listInt) (const3 TypeBool)
2216 L_elementId -> biFuncV elementIdArgs elementIdType
2217 L_atleast -> triFunc (each3 $ valueOnly listInt) (const3 TypeBool)
2218 L_atmost -> triFunc (each3 $ valueOnly listInt) (const3 TypeBool)
2219 L_defined -> unFuncV funcSeq (fmap TypeSet . funcDomain)
2220 L_range -> unFuncV funcSeq (fmap TypeSet . funcRange)
2221 L_restrict -> biFunc restrictArgs restrictTypes
2222 L_allDiff -> unFuncV listOrMatrix (const $ pure TypeBool)
2223 L_alldifferent_except -> biFuncV (indep listOrMatrix enumerable) (const2 TypeBool)
2224 L_catchUndef -> biFuncV unifies (\a b -> pure $ mostDefinedS $ catMaybes [a, b])
2225 L_quickPermutationOrder -> biFunc quickPermutationOrderArgs quickPermutationOrderTypes
2226 L_dontCare -> unFunc anyType (const $ pure TypeBool)
2227 L_toSet -> unFuncV toSetArgs typeToSet
2228 L_toMSet -> unFuncV toMSetArgs typeToMSet
2229 L_toRelation -> unFuncV func typeToRelation
2230 L_max -> unFunc minMaxArgs minMaxType
2231 L_min -> unFunc minMaxArgs minMaxType
2232 L_image -> biFuncV imageArgs (const . funcRange)
2233 L_transform -> biFuncV transformArgs (const id)
2234 L_imageSet -> biFuncV imSetArgs (\a -> const $ TypeSet <$> funcRange a)
2235 L_compose -> biFuncV composeArgs (const . funcRange)
2236 L_preImage -> biFuncV preImageArgs (\a -> const $ TypeSet <$> funcDomain a)
2237 L_inverse -> biFuncV inverseArgs (const2 TypeBool)
2238 L_freq -> biFuncV freqArgs (const2 tInt)
2239 L_hist -> unFuncV histArgs histType
2240 L_parts -> unFuncV part partsType
2241 L_together -> biFuncV setPartArgs (const2 TypeBool)
2242 L_apart -> biFuncV setPartArgs (const2 TypeBool)
2243 L_party -> biFuncV partyArgs partyType
2244 L_permInverse -> unFuncV permInverseArgs id
2245 L_participants -> unFuncV part partInner
2246 L_active -> biFuncV activeArgs (const2 TypeBool)
2247 L_pred -> unFuncV enumerable enumerableType
2248 L_succ -> unFuncV enumerable enumerableType
2249 L_factorial -> unFuncV (only tInt) (const $ pure tInt)
2250 L_powerSet -> unFuncV set powerSetType
2251 L_concatenate -> unFuncV concatArgs concatType
2252 L_flatten -> \b a -> case a of
2253 [] -> unFuncV unaryFlattenArgs (flattenType Nothing) b a
2254 [_] -> unFuncV unaryFlattenArgs (flattenType Nothing) b a
2255 _ -> biFunc (valueOnly2 binaryFlattenArgs) (\v t -> flattenType (getNum v) (typeOnly t)) b a
2256 _ -> bug $ pretty $ "Unkown functional operator " ++ show l
2257 where
2258 valueOnly :: (SArg -> Validator a) -> Arg -> Validator a
2259 valueOnly f (r, (k, e)) = do
2260 t <- getValueType k
2261 f (r, Typed t e)
2262
2263 valueOnly2 :: (SArg -> SArg -> Validator a) -> Arg -> Arg -> Validator a
2264 valueOnly2 f (r1, (k1, e1)) (r2, (k2, e2)) = do
2265 t1 <- getValueType k1
2266 t2 <- getValueType k2
2267 f (r1, Typed t1 e1) (r2, Typed t2 e2)
2268
2269 typeOnly :: Maybe (Kind, Expression) -> Maybe Type
2270 typeOnly (Just (Kind ValueType {} t, _)) = Just t
2271 typeOnly _ = Nothing
2272
2273 unFuncV ::
2274 (SArg -> Validator a0) ->
2275 (Maybe Type -> Maybe Type) ->
2276 ([Expression] -> Expression) ->
2277 [Arg] ->
2278 ValidatorS (Typed Expression)
2279 unFuncV a t = unFunc (valueOnly a) (t . typeOnly)
2280
2281 biFuncV :: (SArg -> SArg -> Validator ()) -> (Maybe Type -> Maybe Type -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2282 biFuncV a t = biFunc (valueOnly2 a) (\t1 t2 -> t (typeOnly t1) (typeOnly t2))
2283
2284 valid = return $ pure ()
2285
2286 const2 = const . const . pure
2287
2288 const3 = const . const . const . pure
2289
2290 getNum :: Maybe (Kind, Expression) -> Maybe Int
2291 getNum (Just (_, x)) = case intOut "" x of
2292 Nothing -> Nothing
2293 Just n -> pure $ fromInteger n
2294 getNum _ = Nothing
2295
2296 each3 f a b c = f a >> f b >> f c
2297
2298 anyType = const . return $ Just ()
2299
2300 indep :: (SArg -> Validator ()) -> (SArg -> Validator ()) -> (SArg -> SArg -> Validator ())
2301 indep f1 f2 a b = do
2302 v1 <- f1 a
2303 v2 <- f2 b
2304 if not . null $ catMaybes [v1, v2] then return $ pure () else return Nothing
2305
2306 binaryFlattenArgs :: SArg -> SArg -> Validator ()
2307 binaryFlattenArgs (r1, d) b = do
2308 off <- case intOut "" (untype d) of
2309 Just (fromInteger -> a :: Integer) | a > 0 -> return $ Just a
2310 _ -> invalid $ r1 <!> CustomError "1st arg must be a constant positive int"
2311 let ref = map (const TypeList) [0 .. fromMaybe 1 off]
2312 let ref' = foldr id TypeAny ref
2313 r <- unifyTypesFailing ref' b
2314 return $ if null off || null r then Nothing else Just ()
2315
2316 unaryFlattenArgs :: SArg -> Validator ()
2317 unaryFlattenArgs (_, typeOf_ -> (TypeMatrix _ _)) = valid
2318 unaryFlattenArgs (_, typeOf_ -> (TypeList _)) = valid
2319 unaryFlattenArgs (_, typeOf_ -> TypeAny) = valid
2320 unaryFlattenArgs (r, typeOf_ -> t) = invalid $ r <!> ComplexTypeError "List or Matrix " t
2321
2322 concatType :: Maybe Type -> Maybe Type
2323 concatType (Just (TypeMatrix _ (TypeList t))) = Just $ TypeList t
2324 concatType (Just (TypeMatrix _ (TypeMatrix _ t))) = Just $ TypeList t
2325 concatType (Just (TypeList (TypeList t))) = Just $ TypeList t
2326 concatType (Just (TypeList (TypeMatrix _ t))) = Just $ TypeList t
2327 concatType _ = Just $ TypeList TypeAny
2328 concatArgs :: SArg -> Validator ()
2329 concatArgs s@(r, _) = binaryFlattenArgs (r, Typed tInt $ Constant $ ConstantInt TagInt 1) s
2330
2331 tableArgs :: SArg -> SArg -> Validator ()
2332 tableArgs (r1, typeOf_ -> t1) (r2, typeOf_ -> t2) = do
2333 a <- case t1 of
2334 t | isValidInner t -> valid
2335 _ -> invalid $ r1 <!> ComplexTypeError "Matrix of Int/Enum" t1
2336 b <- case t2 of
2337 TypeAny -> valid
2338 TypeList t | isValidInner t -> valid
2339 TypeMatrix _ t | isValidInner t -> valid
2340 _ -> invalid $ r2 <!> ComplexTypeError "Matrix of Matrix of Int/Enum" t2
2341
2342 return $ if null a || null b then Nothing else Just ()
2343 where
2344 isValidInner t = case t of
2345 TypeAny -> True
2346 TypeList TypeInt {} -> True
2347 TypeList TypeAny -> True
2348 TypeMatrix _ TypeInt {} -> True
2349 TypeMatrix _ TypeAny -> True
2350 _ -> False
2351
2352 elementIdArgs :: SArg -> SArg -> Validator ()
2353 elementIdArgs (r1, typeOf_ -> t1) (r2, typeOf_ -> t2) = do
2354 let ?typeCheckerMode = RelaxedIntegerTags
2355 a <- case t1 of
2356 TypeAny -> valid
2357 TypeMatrix _ _ -> valid
2358 TypeList _ -> valid
2359 _ -> invalid $ r1 <!> ComplexTypeError "Matrix or List" t1
2360 b <- case (t1, t2) of
2361 (TypeMatrix _indexType _, TypeAny) -> valid
2362 (TypeMatrix indexType _, actualIndex) | typesUnify [indexType, actualIndex] -> valid
2363 (TypeList _, TypeAny) -> valid
2364 (TypeList _, TypeInt {}) -> valid
2365 (TypeAny, _) -> valid
2366 _ -> invalid $ r2 <!> ComplexTypeError "Appropriate index type" t2
2367
2368 return $ if null a || null b then Nothing else Just ()
2369
2370 toMSetArgs :: SArg -> Validator ()
2371 toMSetArgs (r, typeOf_ -> a) = case a of
2372 TypeAny -> return $ pure ()
2373 TypeList _ -> return $ pure ()
2374 TypeMatrix {} -> return $ pure ()
2375 TypeMSet {} -> return $ pure ()
2376 TypeSet {} -> return $ pure ()
2377 TypeFunction {} -> return $ pure ()
2378 TypeRelation {} -> return $ pure ()
2379 _ -> invalid $ r <!> ComplexTypeError "Matrix ,list,function,relation,mset,set " a
2380
2381 toSetArgs :: SArg -> Validator ()
2382 toSetArgs (r, typeOf_ -> a) = case a of
2383 TypeAny -> return $ pure ()
2384 TypeList _ -> return $ pure ()
2385 TypeMatrix {} -> return $ pure ()
2386 TypeMSet {} -> return $ pure ()
2387 TypeFunction {} -> return $ pure ()
2388 TypeRelation {} -> return $ pure ()
2389 _ -> invalid $ r <!> ComplexTypeError "Matrix ,list,function,relation,mset " a
2390
2391 listOrMatrix :: SArg -> Validator ()
2392 listOrMatrix (r, typeOf_ -> a) = case a of
2393 TypeAny -> return $ pure ()
2394 TypeList _ -> return $ pure ()
2395 TypeMatrix {} -> return $ pure ()
2396 _ -> invalid $ r <!> ComplexTypeError "Matrix or list" a
2397
2398 freqArgs :: SArg -> SArg -> Validator ()
2399 freqArgs (r1, a) (r2, b) = do
2400 let tb = typeOf_ b
2401 let (rt, ti) = case typeOf_ a of
2402 TypeMatrix idx ms -> (TypeMatrix idx md, md) where md = mostDefinedS [tb, ms]
2403 TypeMSet ms -> (TypeMSet md, md) where md = mostDefinedS [tb, ms]
2404 _ -> (TypeMatrix tInt tb, tb)
2405 a' <- unifyTypesFailing rt (r1, a)
2406 b' <- unifyTypesFailing ti (r2, b)
2407 return $ if null a' || null b' then Nothing else Just ()
2408
2409 unifies :: SArg -> SArg -> Validator ()
2410 unifies a b = do
2411 let md = mostDefinedS $ map (typeOf_ . unregion) [a, b]
2412 a' <- unifyTypesFailing md a
2413 b' <- unifyTypesFailing md b
2414 return $ if null a' || null b' then Nothing else Just ()
2415
2416 func :: SArg -> Validator ()
2417 func (_, Typed (TypeFunction _ _) _) = valid
2418 func (_, Typed TypeAny _) = valid
2419 func (r, Typed t _) = invalid $ r <!> TypeError (TypeFunction TypeAny TypeAny) t
2420
2421 set :: SArg -> Validator Type
2422 set (_, Typed (TypeSet t) _) = return $ pure t
2423 set (_, Typed TypeAny _) = return $ pure TypeAny
2424 set (r, Typed t _) = invalid $ r <!> TypeError (TypeSet TypeAny) t
2425
2426 powerSetType (Just ((TypeSet i))) = Just $ TypeSet (TypeSet i)
2427 powerSetType _ = Just $ TypeSet $ TypeSet TypeAny
2428
2429 only t (r, typeOf_ -> t') = do
2430 setContext r
2431 if t' == TypeAny || t == t'
2432 then return $ Just t
2433 else invalid $ r <!> TypeError t t'
2434
2435 listInt (r, typeOf_ -> t') = case t' of
2436 TypeAny -> return $ Just t'
2437 TypeList TypeInt {} -> return $ Just t'
2438 TypeMatrix _ TypeInt {} -> return $ Just t'
2439 _ -> invalid $ r <!> ComplexTypeError "Matrix or list of int or enum" t'
2440
2441 partInner :: Maybe Type -> Maybe Type
2442 partInner (Just (TypePartition a)) = Just $ TypeSet a
2443 partInner _ = Just $ TypeSet TypeAny
2444
2445 restrictArgs :: Arg -> Arg -> Validator ()
2446 restrictArgs (r1, (k, _)) (r2, (kd, _)) = do
2447 setContext r1
2448 funcType <- getValueType k
2449 setContext r2
2450 domType <- getDomainType kd
2451 unifyTypesFailing (TypeFunction domType TypeAny) (r1, Typed funcType ())
2452
2453 restrictTypes :: Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type
2454 restrictTypes (fmap fst -> kv) (fmap fst -> kd) = Just $ TypeFunction from to
2455 where
2456 dType = case kd of
2457 Just (Kind DomainType t) -> getDomainMembers t
2458 _ -> TypeAny
2459 from = case kv of
2460 Just (Kind ValueType {} (TypeFunction fr _)) | typesUnifyS [dType, fr] -> mostDefinedS [dType, fr]
2461 Just (Kind ValueType {} (TypeFunction fr _)) -> fr
2462 _ -> mostDefinedS [TypeAny, dType]
2463 to = case kv of
2464 Just (Kind ValueType {} (TypeFunction _ to')) -> to'
2465 _ -> TypeAny
2466
2467 -- TODO: validate
2468 quickPermutationOrderArgs :: Arg -> Arg -> Validator ()
2469 quickPermutationOrderArgs _ _ = return (pure ())
2470
2471 -- TODO
2472 permInverseArgs :: SArg -> Validator ()
2473 permInverseArgs _ = return (pure ())
2474
2475 -- TODO
2476 quickPermutationOrderTypes :: Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type
2477 quickPermutationOrderTypes _ _ = Just TypeBool
2478
2479 imSetArgs :: SArg -> SArg -> Validator ()
2480 imSetArgs (r1, a) (r2, b) = do
2481 let t = case (typeOf_ a, typeOf_ b) of
2482 (TypeFunction i _, tb) -> mostDefinedS [i, tb]
2483 (TypeSequence _, _) -> tInt
2484 (_, tb) -> tb
2485 a' <- unifyTypesFailing (TypeFunction t TypeAny) (r1, a)
2486 b' <- unifyTypesFailing t (r2, b)
2487 return $ if null a' || null b' then Nothing else Just ()
2488
2489 preImageArgs :: SArg -> SArg -> Validator ()
2490 preImageArgs _ _ = return $ Just ()
2491 -- preImageArgs (r1, a) (r2, b) = do
2492 -- let t = case (typeOf_ a, typeOf_ b) of
2493 -- (TypeFunction _ i, tb) -> mostDefinedS [i, tb]
2494 -- (TypeSequence i, _) -> i
2495 -- (_, tb) -> tb
2496 -- a' <- unifyTypesFailing (TypeFunction TypeAny t) (r1, a)
2497 -- b' <- unifyTypesFailing t (r2, b)
2498 -- return $ if null a' || null b' then Nothing else Just ()
2499
2500 partyArgs :: SArg -> SArg -> Validator ()
2501 partyArgs (r1, a) (r2, b) = do
2502 let t = case (typeOf_ a, typeOf_ b) of
2503 (ta, TypePartition tb) -> mostDefinedS [ta, tb]
2504 (ta, _) -> ta
2505 a' <- unifyTypesFailing t (r1, a)
2506 b' <- unifyTypesFailing (TypePartition t) (r2, b)
2507 return $ if null a' || null b' then Nothing else Just ()
2508
2509 inverseArgs :: SArg -> SArg -> Validator ()
2510 inverseArgs (_r1, a) (_r2, b) =
2511 case (typeOf_ a, typeOf_ b) of
2512 (TypeFunction {}, TypeFunction {}) -> return (Just ())
2513 (TypeFunction {}, _) -> return (Just ())
2514 (_, TypeFunction {}) -> return (Just ())
2515 (TypePermutation {}, TypePermutation {}) -> return (Just ())
2516 (TypePermutation {}, _) -> return (Just ())
2517 (_, TypePermutation {}) -> return (Just ())
2518 _ -> return Nothing
2519
2520 setPartArgs :: SArg -> SArg -> Validator ()
2521 setPartArgs (r1, a) (r2, b) = do
2522 let t = case (typeOf_ a, typeOf_ b) of
2523 (TypeSet st, TypePartition pt) -> mostDefinedS [st, pt]
2524 (TypeSet st, _) -> st
2525 (_, TypePartition ts) -> ts
2526 _ -> TypeAny
2527 a' <- unifyTypesFailing (TypeSet t) (r1, a)
2528 b' <- unifyTypesFailing (TypePartition t) (r2, b)
2529 return $ if null a' || null b' then Nothing else Just ()
2530
2531 partyType :: Maybe Type -> Maybe Type -> Maybe Type
2532 partyType a b = do
2533 let at' = fromMaybe TypeAny a
2534 let bt = case b of
2535 Just (TypePartition t) -> t
2536 _ -> TypeAny
2537 return $ TypeSet $ mostDefinedS [at', bt]
2538
2539 partsType :: Maybe Type -> Maybe Type
2540 partsType (Just (TypePartition a)) = Just $ TypeSet $ TypeSet a
2541 partsType (Just TypeAny) = Just $ TypeSet $ TypeSet TypeAny
2542 partsType _ = Nothing
2543
2544 minMaxArgs :: Arg -> Validator ()
2545 minMaxArgs (r, (Kind DomainType t, _)) =
2546 case t of
2547 TypeInt TagInt -> valid
2548 TypeInt (TagEnum _) -> valid
2549 TypeEnum {} -> valid
2550 TypeAny -> valid
2551 _ -> invalid $ r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t
2552 minMaxArgs (r, (k, _)) = do
2553 t <- getValueType k
2554 inner <- case t of
2555 TypeList tyInner -> return tyInner
2556 TypeMatrix _ tyInner -> return tyInner
2557 TypeSet tyInner -> return tyInner
2558 TypeMSet tyInner -> return tyInner
2559 TypeAny -> return TypeAny
2560 _ -> TypeAny <$ invalid (r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t)
2561 case inner of
2562 TypeInt TagInt -> valid
2563 TypeInt (TagEnum _) -> valid
2564 TypeEnum {} -> valid
2565 TypeAny -> valid
2566 _ -> invalid $ r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t
2567
2568 minMaxType :: Maybe (Kind, a) -> Maybe Type
2569 minMaxType (Just (Kind DomainType t@(TypeInt {}), _)) = Just t
2570 minMaxType (Just (Kind DomainType (TypeEnum (Name nm)), _)) = Just . TypeInt $ TagEnum nm
2571 minMaxType (Just (Kind ValueType {} (TypeMatrix _ a), _)) = minMaxType (Just (Kind DomainType a, ()))
2572 minMaxType (Just (Kind ValueType {} (TypeList a), _)) = minMaxType (Just (Kind DomainType a, ()))
2573 minMaxType (Just (Kind ValueType {} (TypeSet a), _)) = minMaxType (Just (Kind DomainType a, ()))
2574 minMaxType (Just (Kind ValueType {} (TypeMSet a), _)) = minMaxType (Just (Kind DomainType a, ()))
2575 minMaxType _ = Just TypeAny
2576
2577 transformArgs :: SArg -> SArg -> Validator ()
2578 transformArgs _ _ = return $ pure ()
2579 activeArgs :: SArg -> SArg -> Validator ()
2580 activeArgs (_, typeOf_ -> TypeAny) _ = valid
2581 activeArgs (r, typeOf_ -> t@(TypeVariant _)) (r2, typeOf_ -> b) = checkRVMember (r, t) (r2, b)
2582 activeArgs (r, typeOf_ -> t) _ = invalid $ r <!> ComplexTypeError "Variant " t
2583
2584 typeToSet :: Maybe Type -> Maybe Type
2585 typeToSet (Just t) = Just . TypeSet $ fromMaybe TypeAny (tMembers t)
2586 typeToSet _ = Just $ TypeSet TypeAny
2587
2588 typeToMSet :: Maybe Type -> Maybe Type
2589 typeToMSet (Just t) = Just . TypeMSet $ fromMaybe TypeAny (tMembers t)
2590 typeToMSet _ = Just $ TypeMSet TypeAny
2591
2592 typeToRelation :: Maybe Type -> Maybe Type
2593 typeToRelation (Just (TypeFunction i j)) = Just $ TypeRelation [i, j]
2594 typeToRelation (Just TypeAny) = Just $ TypeRelation [TypeAny, TypeAny]
2595 typeToRelation _ = Nothing
2596 tMembers t = case t of
2597 TypeAny -> Just TypeAny
2598 TypeList ty -> Just ty
2599 TypeMatrix _ i -> Just i
2600 TypeSet ty -> Just ty
2601 TypeMSet ty -> Just ty
2602 TypeFunction i j -> Just $ TypeTuple [i, j]
2603 TypeRelation tys -> Just $ TypeTuple tys
2604 _ -> Nothing
2605
2606 imageArgs :: SArg -> SArg -> Validator ()
2607 imageArgs (r1, typeOf_ -> t1) r2 = do
2608 from <- case t1 of
2609 TypeAny -> return $ Just TypeAny
2610 TypeFunction a _ -> return $ Just a
2611 TypeSequence _ -> return $ Just tInt
2612 TypePermutation a -> return $ Just a
2613 _ -> Nothing <$ raiseTypeError (r1 <!> ComplexTypeError "function, sequence or permutation" t1)
2614 case from of
2615 Just f -> unifyTypes f r2 >> return (pure ())
2616 Nothing -> return Nothing
2617
2618 -- TODO: validate
2619 composeArgs :: SArg -> SArg -> Validator ()
2620 composeArgs _ _ = return (pure ())
2621
2622 sumArgs :: SArg -> Validator ()
2623 sumArgs (r, typeOf_ -> t') = do
2624 t <- case t' of
2625 TypeAny -> return TypeAny
2626 TypeList t -> return t
2627 TypeMatrix _ t -> return t
2628 TypeSet t -> return t
2629 TypeMSet t -> return t
2630 _ -> TypeAny <$ raiseTypeError (r <!> ComplexTypeError "Matrix or Set" t')
2631 case t of
2632 TypeAny -> return $ pure ()
2633 TypeInt TagInt -> return $ pure ()
2634 _ -> Nothing <$ raiseTypeError (r <!> ComplexTypeError "Integer elements" t)
2635
2636 funcSeq :: SArg -> Validator ()
2637 funcSeq (r, typeOf_ -> t') = case t' of
2638 TypeAny -> return $ pure ()
2639 TypeSequence _ -> return $ pure ()
2640 TypePermutation _ -> return $ pure ()
2641 TypeFunction _ _ -> return $ pure ()
2642 _ -> invalid $ r <!> ComplexTypeError "function, sequence or permutation" t'
2643
2644 funcDomain :: Maybe Type -> Maybe Type
2645 funcDomain (Just (TypeFunction a _)) = Just a
2646 funcDomain (Just (TypeSequence _)) = Just tInt
2647 funcDomain _ = Just TypeAny
2648
2649 funcRange :: Maybe Type -> Maybe Type
2650 funcRange (Just (TypeFunction _ b)) = Just b
2651 funcRange (Just ((TypeSequence b))) = Just b
2652 funcRange _ = Just TypeAny
2653
2654 elementIdType :: Maybe Type -> Maybe Type -> Maybe Type
2655 elementIdType (Just (TypeMatrix _ innerType)) _ = Just innerType
2656 elementIdType (Just (TypeList innerType)) _ = Just innerType
2657 elementIdType _ _ = Just TypeAny
2658
2659 part :: SArg -> Validator ()
2660 part (r, typeOf_ -> t) = case t of
2661 TypeAny -> valid
2662 TypePartition _ -> return $ pure ()
2663 _ -> invalid $ r <!> TypeError (TypePartition TypeAny) t
2664
2665 histArgs :: SArg -> Validator ()
2666 histArgs (r, typeOf_ -> a) = case a of
2667 TypeMSet _ -> return $ pure ()
2668 TypeList _ -> return $ pure ()
2669 TypeMatrix _ _ -> return $ pure ()
2670 TypeAny -> return $ pure ()
2671 _ -> invalid $ r <!> ComplexTypeError "Matrix, List or MSet" a
2672
2673 histType :: Maybe Type -> Maybe Type
2674 histType (Just ((TypeMSet a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2675 histType (Just ((TypeMatrix _ a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2676 histType (Just ((TypeList a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2677 histType _ = Just $ TypeMatrix tInt $ TypeTuple [TypeAny, tInt]
2678
2679 enumerable :: SArg -> Validator ()
2680 enumerable (r, typeOf_ -> t) = case t of
2681 TypeAny -> return $ pure ()
2682 TypeInt TagUnnamed {} -> invalid $ r <!> CustomError "Anonymous enums are not explictly enumerable"
2683 TypeInt _ -> return $ pure ()
2684 TypeEnum {} -> return $ pure ()
2685 TypeBool -> return $ pure ()
2686 _ -> invalid $ r <!> ComplexTypeError "int enum or bool" t
2687
2688 enumerableType :: Maybe Type -> Maybe Type
2689 enumerableType (Just t@(TypeInt TagInt)) = Just t
2690 enumerableType (Just t@(TypeInt (TagEnum _))) = Just t
2691 enumerableType (Just t@(TypeEnum {})) = Just t
2692 enumerableType _ = Nothing
2693
2694 flattenType :: Maybe Int -> Maybe Type -> Maybe Type
2695 flattenType (Just n) (Just a) | n < 0 = Just $ TypeList a
2696 flattenType (Just n) (Just (TypeList m)) = flattenType (Just (n - 1)) (Just m)
2697 flattenType (Just n) (Just (TypeMatrix _ m)) = flattenType (Just (n - 1)) (Just m)
2698 flattenType Nothing (Just (TypeMatrix _ m)) = flattenType Nothing (Just m)
2699 flattenType Nothing (Just (TypeList m)) = flattenType Nothing (Just m)
2700 flattenType Nothing (Just t) = Just $ TypeList t
2701 flattenType _ _ = Just $ TypeList TypeAny
2702
2703 validateFuncOp :: Lexeme -> [RegionTagged (Kind, Expression)] -> ValidatorS (Typed Expression)
2704 validateFuncOp l args = do
2705 let b = funcOpBuilder l
2706 b args
2707
2708 -- case argCheck of
2709 -- Nothing -> return $ Typed (r []) $ fallback "arg fail"
2710 -- Just tys -> return $ Typed (r tys)(b $ map untype tys)
2711
2712 isOfType :: Type -> RegionTagged (Typed Expression) -> ValidatorS Bool
2713 isOfType t (r, v) = setContext r >> return v ?=> exactly t >> return (typesUnifyS [t, typeOf_ v])
2714
2715 isLogicalContainer :: RegionTagged (Typed Expression) -> Validator ()
2716 isLogicalContainer (r, Typed t _) = case t of
2717 TypeAny -> return $ pure ()
2718 TypeList TypeAny -> return $ pure ()
2719 TypeList TypeBool -> return $ pure ()
2720 TypeMatrix _ TypeAny -> return $ pure ()
2721 TypeMatrix _ TypeBool -> return $ pure ()
2722 TypeSet TypeAny -> return $ pure ()
2723 TypeMSet TypeBool -> return $ pure ()
2724 _ -> invalid $ r <!> ComplexTypeError "Collection of boolean" t
2725
2726 -- validateArgList :: [RegionTagged (Typed Expression) -> ValidatorS Bool] -> [RegionTagged (Typed Expression)] -> Validator [Typed Expression]
2727 -- validateArgList ps args | length args < length ps = do invalid $ args <!> MissingArgsError (length ps)
2728 -- validateArgList ps args = do
2729 -- let ps' = ps ++ repeat argOverflow
2730 -- xs <- zipWithM id ps' args
2731 -- return (if and xs then Just $ map unregion args else Nothing)
2732
2733 -- argOverflow :: RegionTagged a -> ValidatorS Bool
2734 -- argOverflow (region,_) = do
2735 -- setContext region
2736 -- void . contextError $ CustomError "Extra Args"
2737 -- return False
2738 type SArg = RegionTagged (Typed Expression)
2739
2740 type Arg = RegionTagged (Kind, Expression)
2741
2742 unFunc ::
2743 (Arg -> Validator a) -> -- Arg validator
2744 (Maybe (Kind, Expression) -> Maybe Type) -> -- typeEvaluator
2745 ([Expression] -> Expression) -> -- mkOp or similar
2746 [Arg] ->
2747 ValidatorS (Typed Expression)
2748 unFunc argVal t f args = do
2749 (v, ts) <- case args of
2750 [] -> tooFewArgs 1 0 >> return (Nothing, Nothing)
2751 [x] -> do
2752 r <- argVal x
2753 tc <- gets typeChecking
2754 let result = case r of
2755 Nothing | tc -> Nothing
2756 _ -> Just [(snd . unregion) x]
2757 return (result, Just $ unregion x)
2758 (x : rs) -> do
2759 tooManyArgs rs
2760 r <- argVal x
2761 let result = case r of
2762 Nothing -> Nothing
2763 Just _ -> Just [(snd . unregion) x]
2764 return (result, Just $ unregion x)
2765 let res = maybe (fallback "Arg Fail Unfunc") f v
2766 return $ Typed (fromMaybe TypeAny $ t ts) res
2767
2768 biFunc :: (Arg -> Arg -> Validator a) -> (Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2769 biFunc argVal t f args = do
2770 (v, ts) <- case args of
2771 [] -> tooFewArgs 2 0 >> return (Nothing, (Nothing, Nothing))
2772 [x] -> tooFewArgs 2 1 >> return (Nothing, (Just $ unregion x, Nothing))
2773 [x, y] -> do
2774 r <- argVal x y
2775 tc <- gets typeChecking
2776 let result = case r of
2777 Nothing | tc -> Nothing
2778 _ -> Just $ map (snd . unregion) [x, y]
2779 return (result, (Just (unregion x), Just (unregion y)))
2780 (x : y : rs) -> do
2781 tooManyArgs rs
2782 r <- argVal x y
2783 let result = case r of
2784 Nothing -> Nothing
2785 Just _ -> Just $ map (snd . unregion) [x, y]
2786 return (result, (Just (unregion x), Just (unregion y)))
2787 let res = maybe (fallback "Arg Fail BiFunct") f v
2788 return $ Typed (fromMaybe TypeAny $ uncurry t ts) res
2789
2790 triFunc :: (Arg -> Arg -> Arg -> Validator a) -> (Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2791 triFunc argVal t f args = do
2792 (v, ts) <- case args of
2793 [] -> tooFewArgs 3 0 >> return (Nothing, (Nothing, Nothing, Nothing))
2794 [x] -> tooFewArgs 3 1 >> return (Nothing, (Just $ unregion x, Nothing, Nothing))
2795 [x, y] -> tooFewArgs 3 2 >> return (Nothing, (Just $ unregion x, Just $ unregion y, Nothing))
2796 [x, y, z] -> do
2797 r <- argVal x y z
2798 tc <- gets typeChecking
2799 let result = case r of
2800 Nothing | tc -> Nothing
2801 _ -> Just $ map (snd . unregion) [x, y, z]
2802 return (result, (Just (unregion x), Just (unregion y), Just (unregion z)))
2803 (x : y : z : rs) -> do
2804 tooManyArgs rs
2805 r <- argVal x y z
2806 let result = case r of
2807 Nothing -> Nothing
2808 Just _ -> Just $ map (snd . unregion) [x, y, z]
2809 return (result, (Just (unregion x), Just (unregion y), Just (unregion z)))
2810 let res = maybe (fallback "Arg Fail Tri") f v
2811 return $ Typed (fromMaybe TypeAny $ uncurry3 t ts) res
2812 where
2813 uncurry3 fn (a, b, c) = fn a b c -- todo export from prelude
2814
2815 tooFewArgs :: Int -> Int -> ValidatorS ()
2816 tooFewArgs n i = void . contextError $ MissingArgsError n i
2817
2818 tooManyArgs :: [RegionTagged a] -> ValidatorS ()
2819 tooManyArgs = mapM_ (\x -> raiseError $ x <!> UnexpectedArg)
2820
2821 checkRVMember :: RegionTagged Type -> RegionTagged Type -> Validator ()
2822 checkRVMember (_, TypeRecord ts) (_, TypeRecordMember nm _) | not . null $ lookup nm ts = return $ pure ()
2823 checkRVMember (_, TypeRecord ts) (r2, r) = do
2824 raiseTypeError $ r2 <!> TypeError (TypeRecordMember (Name "") ts) r
2825 return Nothing
2826 checkRVMember (_, TypeVariant ts) (_, TypeVariantMember nm _) | not . null $ lookup nm ts = return $ pure ()
2827 checkRVMember (_, TypeVariant ts) (r2, r) = do
2828 raiseTypeError $ r2 <!> TypeError (TypeVariantMember (Name "") ts) r
2829 return Nothing
2830 checkRVMember (r1, t) _ = do
2831 raiseTypeError $ r1 <!> TypeError (TypeVariant []) t
2832 return Nothing
2833
2834 type OpValidator = RegionTagged Kind -> RegionTagged Kind -> ValidatorS Type
2835
2836 type OpTyper = Kind -> Kind -> Type
2837
2838 sameToSameV :: (Type -> ValidatorS Type) -> (Type -> Type -> Type) -> OpValidator
2839 sameToSameV tc t (rl, kl) (rr, kr) = do
2840 setContext rl
2841 lt <- getValueType kl
2842 lt' <- tc lt
2843 setContext rr
2844 rt <- getValueType kr
2845 rt' <- tc rt
2846 let md = mostDefinedS [lt, rt]
2847 _ <- unifyTypesFailing md (rl, Typed lt' ())
2848 _ <- unifyTypesFailing md (rr, Typed rt' ())
2849 return $ t lt' rt'
2850
2851 binOpType :: Lexeme -> OpValidator
2852 binOpType l = case l of
2853 L_Plus -> sameToSameV number same
2854 L_Minus -> sameToSameV minusArgs same
2855 L_Times -> sameToSameV number same
2856 L_Div -> sameToSameV number same
2857 L_Mod -> sameToSameV number same
2858 L_Pow -> sameToSameV number same
2859 L_Eq -> sameToSameV pure cBool
2860 L_Neq -> sameToSameV pure cBool
2861 L_Lt -> sameToSameV orderable cBool
2862 L_Leq -> sameToSameV orderable cBool
2863 L_Gt -> sameToSameV orderable cBool
2864 L_Geq -> sameToSameV orderable cBool
2865 L_in -> checkIn
2866 L_And -> sameToSameV bools cBool
2867 L_Or -> sameToSameV bools cBool
2868 L_Imply -> sameToSameV bools cBool
2869 L_Iff -> sameToSameV bools cBool -- b b b
2870 L_subset -> sameToSameV setLike cBool -- set mset func rel
2871 L_subsetEq -> sameToSameV setLike cBool
2872 -- \^^^
2873 L_supset -> sameToSameV setLike cBool
2874 -- \^^^^
2875 L_supsetEq -> sameToSameV setLike cBool
2876 -- \^^
2877
2878 L_subsequence -> sameToSameV justSequence cBool -- seq - seq -bool
2879 L_substring -> sameToSameV justSequence cBool -- seq - seq -bool
2880 L_intersect -> sameToSameV setLike same
2881 L_union -> sameToSameV setLike same
2882 L_LexLt -> sameToSameV pure cBool
2883 L_LexLeq -> sameToSameV pure cBool
2884 L_LexGt -> sameToSameV pure cBool
2885 L_LexGeq -> sameToSameV pure cBool
2886 L_DotLt -> sameToSameV pure cBool
2887 L_DotLeq -> sameToSameV pure cBool
2888 L_DotGt -> sameToSameV pure cBool
2889 L_DotGeq -> sameToSameV pure cBool
2890 L_TildeLt -> sameToSameV pure cBool
2891 L_TildeLeq -> sameToSameV pure cBool
2892 L_TildeGt -> sameToSameV pure cBool
2893 L_TildeGeq -> sameToSameV pure cBool
2894 _ -> bug $ "Unkown operator" <+> pretty (show l)
2895 where
2896 cBool = const . const TypeBool
2897 same a b = mostDefinedS [a, b]
2898 checkIn :: OpValidator
2899 checkIn (r1, kl) (r2, kr) = do
2900 setContext r1
2901 lt <- getValueType kl
2902 setContext r2
2903 rt <- getValueType kr
2904 case innerTypeOf rt of
2905 Just t -> unifyTypes t (r1, Typed lt ())
2906 Nothing -> unless (rt == TypeAny) $ raiseTypeError (r2 <!> ComplexTypeError (T.pack . show $ "Container of " <+> pretty lt) rt)
2907 return TypeBool
2908
2909 number :: Type -> ValidatorS Type
2910 number t = case t of
2911 TypeInt TagInt -> return t
2912 TypeInt TagEnum {} -> return t
2913 TypeAny -> return t
2914 _ -> TypeAny <$ contextTypeError (ComplexTypeError "Number or Enum" t)
2915 minusArgs t = case t of
2916 TypeInt TagInt -> return t
2917 TypeSet _ -> return t
2918 TypeMSet _ -> return t
2919 TypeRelation _ -> return t
2920 TypeFunction _ _ -> return t
2921 _ -> TypeAny <$ contextTypeError (ComplexTypeError "Number / set/ mset / relation / function" t)
2922 orderable t = case t of
2923 TypeInt TagInt -> return t
2924 TypeInt TagEnum {} -> return t
2925 TypeBool -> return t
2926 TypeAny -> return t
2927 _ -> TypeAny <$ contextTypeError (ComplexTypeError "Number, Enum or Bool" t)
2928 justSequence t = case t of
2929 TypeAny -> return t
2930 TypeSequence _ -> return t
2931 _ -> TypeAny <$ contextTypeError (TypeError (TypeSequence TypeAny) t)
2932 bools t = case t of
2933 TypeAny -> return t
2934 TypeBool -> return t
2935 _ -> TypeAny <$ contextTypeError (TypeError TypeBool t)
2936 setLike t = case t of
2937 TypeAny -> return t
2938 TypeMSet _ -> return t
2939 TypeSet _ -> return t
2940 TypeFunction _ _ -> return t
2941 TypeRelation _ -> return t
2942 _ -> TypeAny <$ contextTypeError (ComplexTypeError "Set MSet funcition or relation" t)