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 ranges@(ListNode _ (Seq [SeqElem a _]) _)) = do
747 void $ listToSeq ranges
748 let maybe_tag = case maybe_tag' of Nothing -> Nothing ; Just (_, t) -> Just t
749 d <- case a of
750 SingleRangeNode en -> do
751 (t, e) <- typeSplit <$> validateExpression en
752 case t of
753 TypeInt _ -> return $ DomainInt (mkIntTag maybe_tag) [RangeSingle e]
754 TypeMatrix _ _ -> return $ DomainIntE (mkIntTag maybe_tag) e
755 TypeList _ -> return $ DomainIntE (mkIntTag maybe_tag) e
756 TypeSet _ -> return $ DomainIntE (mkIntTag maybe_tag) e
757 _ -> DomainIntE (mkIntTag maybe_tag) e <$ raiseTypeError (symbolRegion en <!> ComplexTypeError "Set/List of int or Int" t)
758 _ -> do
759 r <- validateRange tInt a
760 return $ DomainInt (mkIntTag maybe_tag) [r]
761 return $ Typed tInt d
762 validateRangedInt maybe_tag' (Just ranges) = do
763 let maybe_tag = case maybe_tag' of Nothing -> Nothing ; Just (_, t) -> Just t
764 ranges' <- catMaybes <$> validateList_ (f2n (validateRange tInt)) ranges
765 return . Typed tInt $ DomainInt (mkIntTag maybe_tag) ranges'
766 validateRangedInt maybe_tag' Nothing = do
767 let maybe_tag = case maybe_tag' of Nothing -> Nothing ; Just (_, t) -> Just t
768 return . Typed tInt $ DomainInt (mkIntTag maybe_tag) []
769
770 validateEnumRange :: NameNodeS -> Maybe (ListNode RangeNode) -> ValidatorS TypedDomain
771 validateEnumRange name@(NameNodeS n) ranges = do
772 flagSToken n TtEnum
773 setContextFrom name
774 name' <- validateIdentifierS name
775 _ <- resolveReference (symbolRegion name, Name name')
776 a <- getSymbol name'
777 case a of
778 Just (_, True, t) -> do
779 t' <- getDomainType t
780 rs <- case ranges of
781 Just rs -> pure . catMaybes <$> validateList_ (f2n $ validateRange (getDomainMembers t')) rs
782 Nothing -> return Nothing
783 return $ Typed t' $ DomainEnum (Name name') rs Nothing
784 Just (_, False, t) -> do
785 t' <- getDomainType t
786 case ranges of
787 Nothing -> return . Typed t' $ DomainReference (Name name') Nothing
788 Just rs -> do
789 void $ validateList_ (f2n (validateRange TypeAny)) rs
790 raiseError (symbolRegion name <!> SemanticError "range not supported on non enum ranges")
791 return . Typed t' $ DomainReference (Name name') Nothing
792 Nothing -> return $ fallback "unknown symbol"
793
794 validateTupleDomain :: ListNode DomainNode -> ValidatorS TypedDomain
795 validateTupleDomain doms = do
796 (ts, ds) <- unzip . map typeSplit <$> validateList_ validateDomain doms
797 return $ Typed (TypeTuple ts) (DomainTuple ds)
798
799 validateRecordDomain :: ListNode NamedDomainNode -> ValidatorS TypedDomain
800 validateRecordDomain namedDoms = do
801 lst <- validateList (f2n validateNamedDomainInVariant) namedDoms
802 let lst' = mapMaybe (\(r, m) -> (\x -> (r, x)) <$> m) lst
803 let (ts, ds) = unzip $ map (\(r, (x, typeSplit -> (t, d))) -> ((x, t), (r, (x, d)))) lst'
804 -- push members
805 let t n = Kind (ValueType CatConstant) $ TypeRecordMember n ts
806 mapM_ (\(r, (a, _)) -> putSymbol (a, (r, False, t a))) ds
807 return $ Typed (TypeRecord ts) (DomainRecord (unregion <$> ds))
808
809 validateVariantDomain :: ListNode NamedDomainNode -> ValidatorS TypedDomain
810 validateVariantDomain namedDoms = do
811 lst <- validateList (f2n validateNamedDomainInVariant) namedDoms
812 let lst' = mapMaybe (\(r, m) -> (\x -> (r, x)) <$> m) lst
813 let (ts, ds) = unzip $ map (\(r, (x, typeSplit -> (t, d))) -> ((x, t), (r, (x, d)))) lst'
814 -- push members
815 let t n = Kind (ValueType CatConstant) $ TypeVariantMember n ts
816 mapM_ (\(r, (a, _)) -> putSymbol (a, (r, False, t a))) ds
817 return $ Typed (TypeVariant ts) (DomainVariant (unregion <$> ds))
818
819 validateMatrixDomain :: ListNode DomainNode -> DomainNode -> ValidatorS TypedDomain
820 validateMatrixDomain indexes dom = do
821 idoms <- validateList_ validateDomain indexes
822 dom' <- validateDomain dom
823 return $ foldr acc dom' idoms
824 where
825 acc :: TypedDomain -> TypedDomain -> TypedDomain
826 acc (Typed t d) (Typed t' d') = Typed (TypeMatrix t t') (DomainMatrix d d')
827
828 validateSetDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
829 validateSetDomain attrs dom = do
830 let repr = ()
831 attrs' <- case attrs of
832 Just a -> validateSetAttributes a
833 Nothing -> return def
834 (t, dom') <- typeSplit <$> validateDomain dom
835 return . Typed (TypeSet t) $ DomainSet repr attrs' dom'
836
837 validateMSetDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
838 validateMSetDomain attrs dom = do
839 let repr = ()
840 attrs' <- case attrs of
841 Just a -> validateMSetAttributes a
842 Nothing -> return def
843 (t, dom') <- typeSplit <$> validateDomain dom
844 return . Typed (TypeMSet t) $ DomainMSet repr attrs' dom'
845
846 validateFunctionDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> DomainNode -> ValidatorS TypedDomain
847 validateFunctionDomain attrs dom1 dom2 = do
848 let _repr = Just () -- placeholder if this gets implemented in future
849 attrs' <- case attrs of
850 Just a -> validateFuncAttributes a
851 Nothing -> return def
852 (t1, d1) <- typeSplit <$> validateDomain dom1
853 (t2, d2) <- typeSplit <$> validateDomain dom2
854 let dType = Typed $ TypeFunction t1 t2
855 return . dType $ DomainFunction () attrs' d1 d2
856
857 validateSequenceDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
858 validateSequenceDomain attrs dom = do
859 let repr = ()
860 attrs' <- case attrs of
861 Just a -> validateSeqAttributes a
862 Nothing -> return def
863 (t, dom') <- typeSplit <$> validateDomain dom
864 return . Typed (TypeSequence t) $ DomainSequence repr attrs' dom'
865
866 validatePermutationDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
867 validatePermutationDomain attrs dom = do
868 let repr = ()
869 attrs' <- case attrs of
870 Just a -> validatePermutationAttributes a
871 Nothing -> return (PermutationAttr SizeAttr_None)
872 (t, dom') <- typeSplit <$> validateDomain dom
873 return . Typed (TypePermutation t) $ DomainPermutation repr attrs' dom'
874
875 validateRelationDomain :: Maybe (ListNode AttributeNode) -> ListNode DomainNode -> ValidatorS TypedDomain
876 validateRelationDomain attrs doms = do
877 let repr = ()
878 attrs' <- case attrs of
879 Just a -> validateRelationAttributes a
880 Nothing -> return def
881
882 (ts, doms') <- unzip . map typeSplit <$> validateList_ validateDomain doms
883 return . Typed (TypeRelation ts) $ DomainRelation repr attrs' doms'
884
885 validatePartitionDomain :: Maybe (ListNode AttributeNode) -> DomainNode -> ValidatorS TypedDomain
886 validatePartitionDomain attrs dom = do
887 let repr = ()
888 attrs' <- case attrs of
889 Just a -> validatePartitionAttributes a
890 Nothing -> return def
891 (t, dom') <- typeSplit <$> validateDomain dom
892 return . Typed (TypePartition t) $ DomainPartition repr attrs' dom'
893
894 mkIntTag :: Maybe ETok -> IntTag
895 mkIntTag Nothing = TagInt
896 mkIntTag (Just t) =
897 case lexeme t of
898 LIdentifier i -> TaggedInt i
899 _ -> bug $ "mkIntTag" <+> pretty (show t)
900
901 validateIndexedByNode :: Maybe IndexedByNode -> ValidatorS ()
902 validateIndexedByNode Nothing = return ()
903 validateIndexedByNode (Just (IndexedByNode a b)) = [a, b] `are` TtSubKeyword
904
905 todo :: Text -> Validator a
906 todo s = invalid $ ValidatorDiagnostic global $ Error $ InternalErrorS (append "Not Implemented: " s)
907
908 validateSizeAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS (SizeAttr Expression)
909 validateSizeAttributes attrs = do
910 let sizeAttrs = [L_size, L_minSize, L_maxSize]
911 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
912 case filtered of
913 [] -> return SizeAttr_None
914 [(L_size, Just a)] -> return $ SizeAttr_Size a
915 [(L_minSize, Just a)] -> return (SizeAttr_MinSize a)
916 [(L_maxSize, Just a)] -> return (SizeAttr_MaxSize a)
917 [(L_minSize, Just a), (L_maxSize, Just b)] -> return (SizeAttr_MinMaxSize a b)
918 as -> do
919 void $ contextError $ SemanticError $ pack $ "Incompatible attributes size:" ++ show as
920 return def
921
922 validatePermAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS (SizeAttr Expression)
923 validatePermAttributes attrs = do
924 let permAttrNames = [L_numMoved, L_minNumMoved, L_maxNumMoved]
925 let filtered = sort $ filter (\x -> fst x `elem` permAttrNames) attrs
926 case filtered of
927 [] -> return SizeAttr_None
928 [(L_numMoved, Just a)] -> return $ SizeAttr_Size a
929 [(L_minNumMoved, Just a)] -> return (SizeAttr_MinSize a)
930 [(L_maxNumMoved, Just a)] -> return (SizeAttr_MaxSize a)
931 [(L_minNumMoved, Just a), (L_maxNumMoved, Just b)] -> return (SizeAttr_MinMaxSize a b)
932 as -> do
933 void $ contextError $ SemanticError $ pack $ "Incompatible attributes numMoved:" ++ show as
934 return def
935
936 validatePartSizeAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS (SizeAttr Expression)
937 validatePartSizeAttributes attrs = do
938 let sizeAttrs = [L_partSize, L_minPartSize, L_maxPartSize]
939 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
940 case filtered of
941 [] -> return SizeAttr_None
942 [(L_partSize, Just a)] -> return (SizeAttr_Size a)
943 [(L_minPartSize, Just a)] -> return (SizeAttr_MinSize a)
944 [(L_maxPartSize, Just a)] -> return (SizeAttr_MaxSize a)
945 [(L_minPartSize, Just a), (L_maxPartSize, Just b)] -> return (SizeAttr_MinMaxSize a b)
946 as -> do
947 void $ contextError $ SemanticError $ pack $ "Incompatible attributes partitionSize :" ++ show as
948 return def
949
950 validateNumPartAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS (SizeAttr Expression)
951 validateNumPartAttributes attrs = do
952 let sizeAttrs = [L_numParts, L_maxNumParts, L_minNumParts]
953 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
954 case filtered of
955 [] -> return SizeAttr_None
956 [(L_numParts, Just a)] -> return (SizeAttr_Size a)
957 [(L_minNumParts, Just a)] -> return (SizeAttr_MinSize a)
958 [(L_maxNumParts, Just a)] -> return (SizeAttr_MaxSize a)
959 [(L_minNumParts, Just a), (L_maxNumParts, Just b)] -> return (SizeAttr_MinMaxSize a b)
960 as -> do
961 void $ contextError $ SemanticError $ pack $ "Incompatible attributes partitionSize :" ++ show as
962 return def
963
964 validateJectivityAttributes :: [(Lexeme, Maybe Expression)] -> ValidatorS JectivityAttr
965 validateJectivityAttributes attrs = do
966 let sizeAttrs = [L_injective, L_surjective, L_bijective]
967 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
968 case filtered of
969 [] -> return JectivityAttr_None
970 [(L_injective, _)] -> return JectivityAttr_Injective
971 [(L_surjective, _)] -> return JectivityAttr_Surjective
972 [(L_bijective, _)] -> return JectivityAttr_Bijective
973 [(L_injective, _), (L_surjective, _)] -> do
974 contextInfo $ UnclassifiedInfo "Inj and Sur can be combined to bijective"
975 return JectivityAttr_Bijective
976 as -> do
977 void $ contextError $ SemanticError $ pack $ "Incompatible attributes jectivity" ++ show as
978 return def
979
980 validateSetAttributes :: ListNode AttributeNode -> ValidatorS (SetAttr Expression)
981 validateSetAttributes atts = do
982 setContextFrom atts
983 attrs <- catMaybes <$> validateList_ (validateAttributeNode setValidAttrs) atts
984 size <- validateSizeAttributes attrs
985 return $ SetAttr size
986
987 validateMSetAttributes :: ListNode AttributeNode -> ValidatorS (MSetAttr Expression)
988 validateMSetAttributes atts = do
989 setContextFrom atts
990 attrs <- catMaybes <$> validateList_ (validateAttributeNode msetValidAttrs) atts
991 size <- validateSizeAttributes attrs
992 occurs <- validateOccursAttrs attrs
993 return $ MSetAttr size occurs
994 where
995 validateOccursAttrs attrs = do
996 let sizeAttrs = [L_minOccur, L_maxOccur]
997 let filtered = sort $ filter (\x -> fst x `elem` sizeAttrs) attrs
998 case filtered of
999 [] -> return OccurAttr_None
1000 [(L_minOccur, Just a)] -> return (OccurAttr_MinOccur a)
1001 [(L_maxOccur, Just a)] -> return (OccurAttr_MaxOccur a)
1002 [(L_minOccur, Just a), (L_maxOccur, Just b)] -> return (OccurAttr_MinMaxOccur a b)
1003 as -> do
1004 void $ contextError $ SemanticError $ pack $ "Bad args to occurs" ++ show as
1005 return def
1006
1007 validateFuncAttributes :: ListNode AttributeNode -> ValidatorS (FunctionAttr Expression)
1008 validateFuncAttributes atts = do
1009 attrs <- catMaybes <$> validateList_ (validateAttributeNode funAttrs) atts
1010 size <- validateSizeAttributes attrs
1011 let parts = if L_total `elem` map fst attrs then PartialityAttr_Total else PartialityAttr_Partial
1012 jectivity <- validateJectivityAttributes attrs
1013 return (FunctionAttr size parts jectivity)
1014
1015 validateSeqAttributes :: ListNode AttributeNode -> ValidatorS (SequenceAttr Expression)
1016 validateSeqAttributes atts = do
1017 attrs <- catMaybes <$> validateList_ (validateAttributeNode seqAttrs) atts
1018 size <- validateSizeAttributes attrs
1019 jectivity <- validateJectivityAttributes attrs
1020 return $ SequenceAttr size jectivity
1021
1022 validatePermutationAttributes :: ListNode AttributeNode -> ValidatorS (PermutationAttr Expression)
1023 validatePermutationAttributes atts = do
1024 attrs <- catMaybes <$> validateList_ (validateAttributeNode permValidAttrs) atts
1025 size <- validatePermAttributes attrs
1026 return $ PermutationAttr size
1027
1028 validateRelationAttributes :: ListNode AttributeNode -> ValidatorS (RelationAttr Expression)
1029 validateRelationAttributes atts = do
1030 setContextFrom atts
1031 attrs <- catMaybes <$> validateList_ (validateAttributeNode relAttrs) atts
1032 size <- validateSizeAttributes attrs
1033 others <- catMaybes <$> validateArray validateBinaryRel (filter (\x -> fst x `elem` map fst binRelAttrs) attrs)
1034 return $ RelationAttr size (BinaryRelationAttrs $ S.fromList others)
1035 where
1036 validateBinaryRel :: (Lexeme, Maybe Expression) -> Validator BinaryRelationAttr
1037 validateBinaryRel (l, _) = case lexemeToBinRel l of
1038 Just b -> return . pure $ b
1039 Nothing -> contextError $ InternalErrorS $ pack $ "Not found (bin rel) " ++ show l
1040
1041 validatePartitionAttributes :: ListNode AttributeNode -> ValidatorS (PartitionAttr Expression)
1042 validatePartitionAttributes atts = do
1043 attrs <- catMaybes <$> validateList_ (validateAttributeNode partitionAttrs) atts
1044 -- guard size attrs and complete as this is default
1045 size <- validateNumPartAttributes attrs
1046 partSize <- validatePartSizeAttributes attrs
1047 let regular = L_regular `elem` map fst attrs
1048 return $ PartitionAttr size partSize regular
1049
1050 validateAttributeNode :: Map Lexeme Bool -> AttributeNode -> Validator (Lexeme, Maybe Expression)
1051 validateAttributeNode vs (NamedAttributeNode t Nothing) = do
1052 flagSToken t TtAttribute
1053 name <- validateSToken t
1054 putDocs (T.pack $ show name) t
1055 case M.lookup name vs of
1056 Nothing -> invalid $ t <!> CustomError "Not a valid attribute in this context"
1057 Just True -> invalid $ t <!> CustomError "Argument required"
1058 Just False -> return . pure $ (name, Nothing)
1059 validateAttributeNode vs (NamedAttributeNode t (Just e)) = do
1060 flagSToken t TtAttribute
1061 setContextFrom e
1062 expr <- validateExpression e ?=> exactly tInt
1063 name <- validateSToken t
1064 putDocs (T.pack $ show name) t
1065 case M.lookup name vs of
1066 Nothing -> invalid $ t <!> CustomError "Not a valid attribute in this context"
1067 Just False -> invalid $ t <!> SemanticError "attribute %name% does not take an argument"
1068 Just True -> return . pure $ (\x -> (name, Just x)) expr
1069
1070 validateNamedDomainInVariant :: NamedDomainNode -> ValidatorS (Name, TypedDomain)
1071 validateNamedDomainInVariant (NameDomainNode name m_dom) = do
1072 name' <- validateNameAs TtRecordMember name
1073 domain' <- case m_dom of
1074 Nothing -> return . Typed tInt $ DomainInt TagInt [RangeSingle 0]
1075 Just (l, d) -> do l `isA'` TtOperator; validateDomain d
1076 return (name', domain')
1077
1078 validateNamedDomainInRecord :: NamedDomainNode -> ValidatorS (Name, TypedDomain)
1079 validateNamedDomainInRecord (NameDomainNode name m_dom) = do
1080 name' <- validateNameAs TtRecordMember name
1081 domain' <- case m_dom of
1082 Just (l, d) -> l `isA'` TtOperator >> validateDomain d
1083 Nothing -> do
1084 raiseError $ symbolRegion name <!> SemanticError "Dataless not allowed in record"
1085 return (fallback "Dataless RecordMemeber")
1086 return (name', domain')
1087
1088 validateRange :: Type -> RangeNode -> ValidatorS (Range Expression)
1089 validateRange t range = case range of
1090 SingleRangeNode en -> do ex <- validateExpression en ?=> exactly t; return $ RangeSingle ex
1091 OpenRangeNode dots -> do dots `isA` TtOther "Ellips"; return RangeOpen
1092 RightUnboundedRangeNode e1 dots -> do dots `isA` TtOther "Ellips"; ex <- validateExpression e1 ?=> exactly t; return $ RangeLowerBounded ex
1093 LeftUnboundedRangeNode dots e1 -> do dots `isA` TtOther "Ellips"; ex <- validateExpression e1 ?=> exactly t; return $ RangeUpperBounded ex
1094 BoundedRangeNode e1 dots e2 -> do
1095 dots `isA` TtOther "Ellips"
1096 e1' <- validateExpression e1 ?=> exactly t
1097 e2' <- validateExpression e2 ?=> exactly t
1098 return $ RangeBounded e1' e2'
1099
1100 validateArrowPair :: ArrowPairNode -> Validator (RegionTagged (Typed Expression), RegionTagged (Typed Expression))
1101 validateArrowPair (ArrowPairNode e1 s e2) = do
1102 s `isA'` TtOperator
1103 e1' <- validateExpression e1
1104 e2' <- validateExpression e2
1105 return . pure $ (\a b -> ((symbolRegion e1, a), (symbolRegion e2, b))) e1' e2'
1106
1107 validateExpression :: ExpressionNode -> ValidatorS (Typed Expression)
1108 validateExpression expr = do
1109 setContextFrom expr
1110 res <- case expr of
1111 Literal ln -> validateLiteral ln
1112 IdentifierNode nn -> validateIdentifierExpr nn
1113 MetaVarExpr tok -> do
1114 x <- validateMetaVar tok
1115 return $ Typed TypeAny $ ExpressionMetaVar x
1116 QuantificationExpr qen -> validateQuantificationExpression qen
1117 OperatorExpressionNode oen -> validateOperatorExpression oen
1118 DomainExpression dex -> validateDomainExpression dex
1119 ParenExpression (ParenExpressionNode l1 exp l2) -> checkSymbols [l1, l2] >> validateExpression exp
1120 AbsExpression (ParenExpressionNode l1 exp l2) -> do
1121 [l1, l2] `are` TtOperator
1122 (kExp, exp') <- validateFlexibleExpression exp
1123 typeCheckAbs kExp
1124 return . Typed tInt $ mkOp TwoBarOp [exp']
1125 FunctionalApplicationNode lt ln -> validateFunctionApplication lt ln
1126 AttributeAsConstriant lt exprs -> validateAttributeAsConstraint lt exprs
1127 SpecialCase scn -> validateSpecialCase scn
1128 MissingExpressionNode lt -> do raiseError (lt <!> TokenError lt); return (fallback "Missing expression")
1129 setContextFrom expr
1130 return res
1131 where
1132 typeCheckAbs :: Kind -> ValidatorS ()
1133 typeCheckAbs (Kind DomainType _) = pure ()
1134 typeCheckAbs (Kind ValueType {} t) = case t of
1135 TypeAny -> return ()
1136 TypeInt _ -> return ()
1137 TypeList {} -> return ()
1138 TypeSet {} -> return ()
1139 TypeMSet {} -> return ()
1140 TypeFunction {} -> return ()
1141 TypeSequence {} -> return ()
1142 TypePermutation {} -> return ()
1143 TypeRelation {} -> return ()
1144 TypePartition {} -> return ()
1145 _ -> contextTypeError $ ComplexTypeError "integer or collection" t
1146
1147 validateFlexibleExpression :: ExpressionNode -> ValidatorS (Kind, Expression)
1148 validateFlexibleExpression (IdentifierNode name) = do
1149 n <- validateIdentifierS name
1150 setContextFrom name
1151 t <- resolveReference (symbolRegion name, Name n)
1152 tagWithType (NameNode name) t
1153 return (t, Reference (Name n) Nothing)
1154 validateFlexibleExpression (DomainExpression den) = do
1155 (dType, d) <- typeSplit <$> validateDomainExpression den
1156 return (Kind DomainType dType, d)
1157 validateFlexibleExpression en = do
1158 (t, expr) <- typeSplit <$> validateExpression en
1159 return (simple t, expr)
1160
1161 validateAttributeAsConstraint :: SToken -> ListNode ExpressionNode -> ValidatorS (Typed Expression)
1162 validateAttributeAsConstraint l1 exprs = do
1163 es <- map untype <$> validateList_ validateExpression exprs
1164 do
1165 flagSToken l1 TtAAC
1166 lx <- validateSToken l1
1167 let n = lookup (Name (lexemeText lx)) allSupportedAttributes
1168 r <- case (n, es) of
1169 (Just 1, [e, v]) -> return . pure . Typed TypeBool $ aacBuilder e lx (Just v)
1170 (Just 1, _) -> invalid $ l1 <!> SemanticError (pack $ "Expected 2 args to " ++ show lx ++ "got" ++ show (length es))
1171 (Just 0, [e]) -> return . pure . Typed TypeBool $ aacBuilder e lx Nothing
1172 (Just 0, _) -> invalid $ l1 <!> SemanticError (pack $ "Expected 1 arg to " ++ show lx ++ "got" ++ show (length es))
1173 (_, _) -> invalid $ l1 <!> InternalErrorS "Bad AAC"
1174 return $ fromMaybe (fallback "bad AAC") r
1175 where
1176 aacBuilder e lx y = Op $ MkOpAttributeAsConstraint $ OpAttributeAsConstraint e (fromString (lexemeFace lx)) y
1177
1178 validateSpecialCase :: SpecialCaseNode -> ValidatorS (Typed Expression)
1179 validateSpecialCase (ExprWithDecls l1 ex l2 sts l3) = do
1180 mapM_ validateSToken [l1, l2, l3]
1181 scoped $ do
1182 conds <- validateProgramTree sts
1183 let decls =
1184 [ Declaration (FindOrGiven LocalFind nm dom)
1185 | Declaration (FindOrGiven Find nm dom) <- conds
1186 ]
1187 let cons =
1188 concat
1189 [ xs
1190 | SuchThat xs <- conds
1191 ]
1192 let locals =
1193 if null decls
1194 then DefinednessConstraints cons
1195 else AuxiliaryVars (decls ++ [SuchThat cons])
1196 (t, expr) <- typeSplit <$> validateExpression ex
1197 return . Typed t $ WithLocals expr locals
1198
1199 translateQnName :: Lexeme -> OpType
1200 translateQnName qnName = case qnName of
1201 L_ForAll -> FunctionOp L_fAnd
1202 L_Exists -> FunctionOp L_fOr
1203 L_Sum -> FunctionOp L_Sum
1204 L_Product -> FunctionOp L_Product
1205 _ -> FunctionOp qnName
1206
1207 validateQuantificationExpression :: QuantificationExpressionNode -> ValidatorS (Typed Expression)
1208 validateQuantificationExpression q@(QuantificationExpressionNode name pats over m_guard dot expr) =
1209 do
1210 setContextFrom q
1211 dot `isA'` TtKeyword
1212 scoped $ do
1213 flagSToken name TtQuantifier
1214 name' <- validateSToken name
1215 (over', genDec) <- holdDeclarations $ wrapRegion pats pats SGen $ validateQuantificationOver pats over
1216 (g', gDec) <- case m_guard of
1217 Nothing -> return ([], [])
1218 Just qg ->
1219 holdDeclarations
1220 $ wrapRegion qg qg SGuard
1221 $ validateQuantificationGuard m_guard
1222 setContextFrom expr
1223 let (iType, rType) = case name' of
1224 L_ForAll -> (tCondition, TypeBool)
1225 L_Exists -> (tCondition, TypeBool)
1226 L_Sum -> (exactly tInt, tInt)
1227 L_Product -> (exactly tInt, tInt)
1228 _ -> bug $ pretty ("Unkown quantifier " ++ show name')
1229 (body, bDecl) <-
1230 holdDeclarations
1231 $ wrapRegion expr expr SBody
1232 $ validateExpression expr
1233 ?=> iType
1234 let qBody = Comprehension body (over' ++ g')
1235 let result = Typed rType (mkOp (translateQnName name') [qBody])
1236 putDocs (T.pack $ show name') name
1237 wrapRegion q q (SQuantification (lexemeText name') (simple rType)) (mapM_ addRegion (gDec ++ genDec ++ bDecl))
1238 return result
1239 where
1240 validateQuantificationGuard :: Maybe QuanticationGuard -> ValidatorS [GeneratorOrCondition]
1241 validateQuantificationGuard Nothing = return []
1242 validateQuantificationGuard (Just (QuanticationGuard l1 exp)) = do
1243 l1 `isA` TtOther "Comma"
1244 expr' <- validateExpression exp ?=> exactly TypeBool
1245 return [Condition expr']
1246 validateQuantificationOver :: Sequence AbstractPatternNode -> QuantificationOverNode -> ValidatorS [GeneratorOrCondition]
1247 validateQuantificationOver lpats (QuantifiedSubsetOfNode lt en) = do
1248 lt `isA` TtKeyword
1249 putDocs "powerset_projection" lt
1250 ps <- sequenceElems lpats
1251 exp <- validateExpression en
1252 let (t, e) = typeSplit exp
1253 void $ unifyTypesFailing (TypeSet TypeAny) (symbolRegion en, exp)
1254 let pt = t
1255 apats <- unifyPatterns pt ps
1256 return [Generator $ GenInExpr pat (Op $ MkOpPowerSet $ OpPowerSet e) | pat <- apats]
1257 -- x in exp
1258 validateQuantificationOver lpats (QuantifiedMemberOfNode lt en) = do
1259 lt `isA` TtKeyword
1260 ps <- sequenceElems lpats
1261 exp <- validateExpression en
1262 let (t, e) = typeSplit exp
1263 pt <- projectionType (symbolRegion en) t
1264 apats <- unifyPatterns pt ps
1265 return [Generator $ GenInExpr pat e | pat <- apats]
1266 -- x : domain
1267 validateQuantificationOver lpats (QuantifiedDomainNode (OverDomainNode l1 dom)) = do
1268 l1 `isA'` TtOther "Colon in comprehension"
1269 ps <- sequenceElems lpats
1270 (dType, dom') <- typeSplit <$> validateDomain dom
1271 pt <- projectionTypeDomain (symbolRegion dom) dType
1272 apats <- unifyPatterns pt ps
1273 return [Generator $ GenDomainNoRepr pat dom' | pat <- apats]
1274
1275 validateMetaVar :: SToken -> ValidatorS String
1276 validateMetaVar tok = do
1277 lx <- validateSToken tok
1278 case lx of
1279 LMetaVar s -> return $ unpack s
1280 _ -> bug $ "Bad MetaVar" <+> pretty (show lx)
1281
1282 validateDomainExpression :: DomainExpressionNode -> ValidatorS (Typed Expression)
1283 validateDomainExpression (DomainExpressionNode l1 dom l2) = do
1284 [l1, l2] `are` TtOther "Backtick"
1285 (tdom, dom') <- typeSplit <$> validateDomain dom
1286 return . Typed tdom $ Domain dom'
1287
1288 validateFunctionApplication :: SToken -> ListNode ExpressionNode -> ValidatorS (Typed Expression)
1289 validateFunctionApplication name args = do
1290 args' <- validateList validateFlexibleExpression args
1291 flagSToken name TtFunction
1292 name' <- validateSToken name
1293 putDocs (lexemeText name') name
1294 setContextFrom args
1295 validateFuncOp name' args'
1296
1297 validateIdentifierExpr :: NameNodeS -> ValidatorS (Typed Expression)
1298 validateIdentifierExpr name = do
1299 n <- validateIdentifierS name
1300 setContextFrom name
1301 t <- resolveReference (symbolRegion name, Name n)
1302 checkCategory t
1303 tagWithType (NameNode name) t
1304 t' <- getValueType t
1305 return . Typed t' $ Reference (Name n) Nothing
1306
1307 validateOperatorExpression :: OperatorExpressionNode -> ValidatorS (Typed Expression)
1308 validateOperatorExpression (PrefixOpNode lt expr) = do
1309 flagSToken lt TtOperator
1310 op <- validateSToken lt
1311 setContextFrom expr
1312 let refT = case op of
1313 L_Minus -> tInt
1314 L_ExclamationMark -> TypeBool
1315 _ -> bug . pretty $ "Unknown prefix op " ++ show op
1316 putDocs (T.pack $ "pre_" ++ show op) lt
1317 expr' <- validateExpression expr ?=> exactly refT
1318 return . Typed refT $ mkOp (PrefixOp op) [expr']
1319 -- lookup symbol
1320 validateOperatorExpression (BinaryOpNode lexp op rexp) = do
1321 (lType, lExpr) <- validateFlexibleExpression lexp
1322 (rType, rExpr) <- validateFlexibleExpression rexp
1323 flagSToken op TtOperator
1324 op' <- validateSToken op
1325
1326 let resultValidator = binOpType op'
1327 resultType <- resultValidator (symbolRegion lexp, lType) (symbolRegion rexp, rType)
1328 addRegion
1329 ( RegionInfo
1330 { rRegion = symbolRegion op,
1331 rSubRegion = Nothing,
1332 rRegionType = Documentation (T.pack $ show op'),
1333 rChildren = [],
1334 rTable = M.empty
1335 }
1336 )
1337 return . Typed resultType $ mkBinOp (pack $ lexemeFace op') lExpr rExpr
1338 validateOperatorExpression (PostfixOpNode expr pon) = do
1339 postFixOp <- validatePostfixOp pon
1340 postFixOp expr
1341
1342 validatePostfixOp :: PostfixOpNode -> ValidatorS (ExpressionNode -> ValidatorS (Typed Expression))
1343 validatePostfixOp (OpFactorial lt) = do
1344 lt `isA` TtOperator
1345 putDocs "post_factorial" lt
1346 setContextFrom lt
1347 return $ \exp -> do
1348 v <- validateExpression exp ?=> exactly tInt
1349 return $ Typed tInt $ mkOp FactorialOp [v]
1350 validatePostfixOp (ApplicationNode args) = return $ \exp -> do
1351 let reg = symbolRegion exp
1352 (t, e) <- typeSplit <$> validateExpression exp
1353 case t of
1354 TypeFunction _ _ -> do
1355 args' <- validateList (validateExpression >=> \(Typed t' e') -> return (simple t', e')) args
1356 validateFuncOp L_image ((reg, (simple t, e)) : args')
1357 TypePermutation _ -> do
1358 args' <- validateList (validateExpression >=> \(Typed t' e') -> return (simple t', e')) args
1359 validateFuncOp L_image ((reg, (simple t, e)) : args')
1360 TypeSequence _ -> do
1361 args' <- validateList (validateExpression >=> \(Typed t' e') -> return (simple t', e')) args
1362 validateFuncOp L_image ((reg, (simple t, e)) : args')
1363 _ -> do
1364 as <- catMaybes <$> listElems args
1365 args' <- mapM validateProjectionArgs as
1366 let ys = args' -- [if underscore == v then Nothing else Just (r,Typed t v)| x@(r,(Kind ValueType t,v)) <- args']
1367 iType <- case t of
1368 TypeRelation ts -> checkProjectionArgs ts ys
1369 _ -> do
1370 raiseTypeError $ symbolRegion exp <!> ComplexTypeError "function, permutation or relation" t
1371 let ts = map (maybe TypeAny (typeOf_ . snd)) ys
1372 return $ TypeRelation ts
1373 let op = Op $ MkOpRelationProj $ OpRelationProj e (map (untype . snd <$>) ys)
1374 let resType = if any null ys then iType else TypeBool
1375 return . Typed resType $ op
1376 where
1377 validateProjectionArgs :: ExpressionNode -> ValidatorS (Maybe (RegionTagged (Typed Expression)))
1378 validateProjectionArgs (IdentifierNode (NameNodeS ((StrictToken _ (lexeme -> l))))) | l == LIdentifier "_" = return Nothing
1379 validateProjectionArgs e = validateExpression e >>= \x -> return . pure $ (symbolRegion e, x)
1380
1381 checkProjectionArgs :: [Type] -> [Maybe (RegionTagged (Typed Expression))] -> ValidatorS Type
1382 checkProjectionArgs ref bind = do
1383 unless (length ref == length bind)
1384 $ raiseError
1385 $ symbolRegion args
1386 <!> SemanticError "Member size mismatch for relation"
1387 let pairs = zip ref bind
1388 let (free, bound) = partition (null . snd) pairs
1389 mapM_
1390 ( \(t, x) -> case x of
1391 Nothing -> pure ()
1392 Just v -> void $ unifyTypes t v
1393 )
1394 bound
1395 let freeTypes = map fst free
1396 return $ if null freeTypes then TypeBool else TypeRelation freeTypes
1397 validatePostfixOp (IndexedNode ln) = do
1398 res <- catMaybes <$> listElems ln
1399 return $ \exp -> do
1400 e <- validateExpression exp
1401 foldM validateIndexingOrSlicing e res
1402 validatePostfixOp (ExplicitDomain l1 l2 dom l3) = do
1403 l1 `isA` TtOther "Colon in expr"
1404 l2 `isA` TtOther "BackTick"
1405 l3 `isA'` TtOther "BackTick"
1406 (getDomainMembers -> t, _) <- typeSplit <$> validateDomain dom
1407 return $ \exp -> do
1408 e <- validateExpression exp ?=> exactly t
1409 return . Typed t $ D.Typed e t
1410
1411 validateIndexingOrSlicing :: Typed Expression -> RangeNode -> ValidatorS (Typed Expression)
1412 validateIndexingOrSlicing (Typed t exp) (SingleRangeNode r) = do
1413 setContextFrom r
1414 (vType, e) <- case t of
1415 TypeRecord ts -> validateRecordMemberIndex ts r
1416 TypeVariant ts -> validateRecordMemberIndex ts r
1417 _ -> do
1418 t' <- getIndexingType t
1419 e <- validateExpression r ?=> exactly t'
1420 setContextFrom r
1421 vType <- getIndexedType t (Typed t' e)
1422 return (vType, e)
1423 return . Typed vType $ Op $ MkOpIndexing (OpIndexing exp e)
1424 validateIndexingOrSlicing exp range = do
1425 let (mType, m) = typeSplit exp
1426 setContextFrom range
1427 sType <- getSlicingType mType
1428 r' <- validateRange sType range
1429 let (i, j) = case r' of
1430 RangeOpen -> (Nothing, Nothing)
1431 RangeLowerBounded ex -> (Just ex, Nothing)
1432 RangeUpperBounded ex -> (Nothing, Just ex)
1433 RangeBounded exl exr -> (Just exl, Just exr)
1434 RangeSingle ex -> (Just ex, Just ex) -- This never gets hit in a well formed program
1435 return $ Typed mType $ Op $ MkOpSlicing (OpSlicing m i j)
1436
1437 validateRecordMemberIndex :: [(Name, Type)] -> ExpressionNode -> ValidatorS (Type, Expression)
1438 validateRecordMemberIndex ns (IdentifierNode nn) = do
1439 n <- tagNameAs TtRecordMember nn
1440 let t = lookup n ns
1441 ty <- case t of
1442 Just ty -> return ty
1443 Nothing -> do
1444 raiseError
1445 $ symbolRegion nn
1446 <!> WithReplacements
1447 (SemanticError "Expected member of record/variant ")
1448 [x | (Name x, _) <- ns]
1449 return TypeAny
1450 return (ty, Reference n Nothing)
1451 validateRecordMemberIndex ns (MissingExpressionNode nn) = do
1452 raiseError
1453 $ symbolRegion nn
1454 <!> WithReplacements
1455 (SemanticError "Expected member of record/variant ")
1456 [x | (Name x, _) <- ns]
1457 return (TypeAny, fallback "bad Index")
1458 validateRecordMemberIndex ns en = do
1459 g <- validateExpression en
1460 let msg =
1461 T.concat
1462 [ "Expected one of ",
1463 T.intercalate "," [x | (Name x, _) <- ns],
1464 " "
1465 ]
1466 raiseTypeError $ symbolRegion en <!> ComplexTypeError msg (typeOf_ g)
1467 return (TypeAny, untype g)
1468
1469 getSlicingType :: Type -> ValidatorS Type
1470 getSlicingType TypeAny = return TypeAny
1471 getSlicingType (TypeMatrix i _) = return i
1472 getSlicingType (TypeSequence _) = return tInt
1473 getSlicingType t = do
1474 contextTypeError (CustomError . pack $ "Type " ++ show (pretty t) ++ " does not support slicing")
1475 return TypeAny
1476
1477 getIndexingType :: Type -> ValidatorS Type
1478 getIndexingType TypeAny = return TypeAny
1479 getIndexingType (TypeMatrix i _) = return $ getDomainMembers i
1480 getIndexingType (TypeSequence _) = return tInt
1481 getIndexingType (TypeList _) = return tInt
1482 getIndexingType (TypeTuple _) = return tInt
1483 getIndexingType t = do
1484 contextTypeError (CustomError . pack $ "Type " ++ show (pretty t) ++ " does not support indexing")
1485 return TypeAny
1486
1487 getIndexedType :: Type -> Typed Expression -> ValidatorS Type
1488 getIndexedType (TypeMatrix _ ms) _ = return ms
1489 getIndexedType (TypeSequence t) _ = return t
1490 getIndexedType (TypeTuple ts) ex = case intOut "Index" (untype ex) of
1491 Left _ -> do
1492 contextTypeError (CustomError "Non constant value indexing tuple")
1493 return TypeAny
1494 Right v | v <= 0 || v > toInteger (length ts) -> do
1495 contextTypeError . CustomError . pack $ "Tuple index " ++ show v ++ " out of bounds"
1496 return TypeAny
1497 Right v -> return $ ts `at` (fromInteger v - 1)
1498 getIndexedType (TypeRecord _) (Typed _ _) = bug "Index type called on record, should be handled by special case"
1499 getIndexedType (TypeVariant _) _ = bug "Index type called on variant, should be handled by special case"
1500 getIndexedType _ _ = return TypeAny
1501
1502 validateLiteral :: LiteralNode -> ValidatorS (Typed Expression)
1503 validateLiteral litNode = case litNode of
1504 IntLiteral lt maybe_tag -> validateIntLiteral lt maybe_tag >>= \x -> return $ Typed tInt $ Constant x
1505 BoolLiteral lt -> validateBoolLiteral lt >>= \x -> return $ Typed TypeBool $ Constant x
1506 MatrixLiteral mln -> validateMatrixLiteral mln
1507 TupleLiteralNode (LongTuple lt xs) -> do
1508 lt `isA` TtType
1509 validateLiteral (TupleLiteralNodeShort (ShortTuple xs))
1510 TupleLiteralNodeShort (ShortTuple xs) -> do
1511 es <- validateExprList_ xs
1512 makeTupleLiteral es
1513 RecordLiteral lt ln -> lt `isA` TtType >> validateRecordLiteral ln
1514 VariantLiteral lt ln -> lt `isA` TtType >> validateVariantLiteral ln
1515 SetLiteral ls -> validateSetLiteral ls
1516 MSetLiteral lt ls -> lt `isA` TtType >> validateMSetLiteral ls
1517 FunctionLiteral lt ln -> lt `isA` TtType >> validateFunctionLiteral ln
1518 SequenceLiteral lt ln -> lt `isA` TtType >> validateSequenceLiteral ln
1519 PermutationLiteral lt ln -> lt `isA` TtType >> validatePermutationLiteral ln
1520 RelationLiteral lt ln -> lt `isA` TtType >> validateRelationLiteral ln
1521 PartitionLiteral lt ln -> lt `isA` TtType >> validatePartitionLiteral ln
1522
1523 validateSequenceLiteral :: ListNode ExpressionNode -> ValidatorS (Typed Expression)
1524 validateSequenceLiteral x = do
1525 (t, ss) <- typeSplit <$> (sameType =<< validateExprList x)
1526 let lType = TypeSequence t
1527 return . Typed lType $ mkAbstractLiteral $ AbsLitSequence ss
1528
1529 validatePermutationLiteral :: ListNode PermutationElemNode -> ValidatorS (Typed Expression)
1530 validatePermutationLiteral x = do
1531 members <- validateList validatePermutationElem x
1532 (t, xs) <- typeSplit <$> sameType members
1533 let eType = TypePermutation t
1534 return $ Typed eType (mkAbstractLiteral $ AbsLitPermutation xs)
1535 where
1536 validatePermutationElem :: PermutationElemNode -> ValidatorS (Typed [Expression])
1537 validatePermutationElem (PermutationElemNode exprs) = do
1538 xs <- validateExprList exprs
1539 sameType xs
1540
1541 validateRelationLiteral :: ListNode RelationElemNode -> ValidatorS (Typed Expression)
1542 validateRelationLiteral ln = do
1543 ms <- validateList validateRelationMember ln
1544 (t, xs) <- typeSplit <$> sameType ms
1545 setContextFrom ln
1546 return . Typed t $ mkAbstractLiteral $ AbsLitRelation xs
1547 where
1548 validateRelationMember :: RelationElemNode -> ValidatorS (Typed [Expression])
1549 validateRelationMember x = case x of
1550 RelationElemNodeLabeled (LongTuple lt xs) -> lt `isA` TtType >> validateRelationMember (RelationElemNodeShort $ ShortTuple xs)
1551 RelationElemNodeShort (ShortTuple xs) -> do
1552 es <- validateExprList_ xs
1553 let (ts, vs) = unzip $ typeSplit <$> es
1554 return $ Typed (TypeRelation ts) vs
1555
1556 validatePartitionLiteral :: ListNode PartitionElemNode -> ValidatorS (Typed Expression)
1557 validatePartitionLiteral ln = do
1558 members <- validateList validatePartitionElem ln
1559 (t, xs) <- typeSplit <$> sameType members
1560 let eType = TypePartition t
1561 return $ Typed eType (mkAbstractLiteral $ AbsLitPartition xs)
1562 where
1563 validatePartitionElem :: PartitionElemNode -> ValidatorS (Typed [Expression])
1564 validatePartitionElem (PartitionElemNode exprs) = do
1565 xs <- validateExprList exprs
1566 sameType xs
1567
1568 validateRecordLiteral :: ListNode RecordMemberNode -> ValidatorS (Typed Expression)
1569 validateRecordLiteral ln = do
1570 members <- catMaybes <$> listElems ln
1571 case members of
1572 [] -> return $ Typed (TypeRecord []) (mk []) -- REVIEW: should empty records be allowed?
1573 xs -> do
1574 (ns, unzip . map typeSplit -> (ts, es)) <- mapAndUnzipM validateRecordMember xs
1575 let t = TypeRecord $ zip ns ts
1576 return $ Typed t $ mk (zip ns es)
1577 where
1578 mk = mkAbstractLiteral . AbsLitRecord
1579
1580 validateVariantLiteral :: ListNode RecordMemberNode -> ValidatorS (Typed Expression)
1581 validateVariantLiteral ln = do
1582 members <- catMaybes <$> validateList_ (f2n validateRecordMember) ln
1583 res <- case members of
1584 [] -> invalid $ symbolRegion ln <!> SemanticError "Variants must contain exactly one member"
1585 [(n, Typed t v)] -> return . pure . Typed (TypeVariant [(n, t)]) $ AbstractLiteral $ AbsLitVariant Nothing n v
1586 _ : _ -> invalid $ symbolRegion ln <!> SyntaxError "Variants must contain exactly one member" -- tag subsequent members as unexpected
1587 return $ fromMaybe (fallback "bad variant") res
1588
1589 validateRecordMember :: RecordMemberNode -> ValidatorS (Name, Typed Expression)
1590 validateRecordMember (RecordMemberNode name lEq expr) = do
1591 lEq `isA'` TtKeyword
1592 name' <- validateName name
1593 expr' <- validateExpression expr
1594 return (name', expr')
1595
1596 validateFunctionLiteral :: ListNode ArrowPairNode -> ValidatorS (Typed Expression)
1597 validateFunctionLiteral ln = do
1598 pairs <- catMaybes <$> validateList_ validateArrowPair ln
1599 let (pl, pr) = unzip pairs
1600 (lhType, ls) <- typeSplit <$> sameType pl
1601 (rhType, rs) <- typeSplit <$> sameType pr
1602 let fType = TypeFunction lhType rhType
1603 return . Typed fType $ mkAbstractLiteral $ AbsLitFunction $ zip ls rs
1604
1605 validateSetLiteral :: ListNode ExpressionNode -> ValidatorS (Typed Expression)
1606 validateSetLiteral ls = do
1607 xs <- validateList validateExpression ls
1608 (t, es) <- typeSplit <$> sameType xs
1609 return . Typed (TypeSet t) $ mkAbstractLiteral $ AbsLitSet es
1610
1611 validateMSetLiteral :: ListNode ExpressionNode -> ValidatorS (Typed Expression)
1612 validateMSetLiteral ls = do
1613 xs <- validateList validateExpression ls
1614 (t, es) <- typeSplit <$> sameType xs
1615 let eType = TypeMSet t
1616 let result = mkAbstractLiteral $ AbsLitMSet es
1617 return $ Typed eType result
1618
1619 validateMatrixLiteral :: MatrixLiteralNode -> ValidatorS (Typed Expression)
1620 -- Matrix proper
1621 validateMatrixLiteral (MatrixLiteralNode l1 se m_dom Nothing l2) = do
1622 [l1, l2] `are` TtOther "SquareBrackets"
1623 matElems <- validateSequence validateExpression se
1624 (t, es) <- typeSplit <$> sameType matElems
1625 let defaultDomain :: TypedDomain = Typed tInt (mkDomainIntB 1 (fromInt $ genericLength matElems))
1626 dom <- fromMaybe defaultDomain <$> validateOverDomain m_dom
1627 let lit = AbsLitMatrix (untype dom) es
1628 return $ Typed (TypeMatrix tInt t) $ mkAbstractLiteral lit
1629 where
1630 validateOverDomain :: Maybe OverDomainNode -> Validator TypedDomain
1631 validateOverDomain Nothing = return Nothing
1632 validateOverDomain (Just (OverDomainNode l3 dom)) = do l3 `isA'` TtOther "Semicolon in matrix"; pure <$> validateDomain dom
1633
1634 -- Matrix as comprehension
1635 validateMatrixLiteral m@(MatrixLiteralNode l1 se m_dom (Just comp) l2) = do
1636 [l1, l2] `are` TtOther "SquareBrackets"
1637 case m_dom of
1638 Nothing -> return ()
1639 Just p@(OverDomainNode l3 dom) -> do
1640 l3 `isA'` TtOther "Semicolon in matrix"
1641 void $ validateDomain dom
1642 raiseError $ symbolRegion p <!> SemanticError "Index domains are not supported in comprehensions"
1643 scoped
1644 $ do
1645 -- check gens and put locals into scope
1646 (gens, dGens) <- holdDeclarations $ validateComprehension comp
1647 -- now validate expression(s)
1648 (es, dBody) <-
1649 holdDeclarations
1650 $ wrapRegion se se SBody
1651 $ validateSequence validateExpression se
1652 r <- case es of
1653 [] -> return $ fallback "missing" <$ raiseError $ symbolRegion se <!> SemanticError "MissingExpression"
1654 ((_, x) : xs) -> flagExtraExpressions xs >> return x
1655 let bodyType = typeOf_ r
1656 wrapRegion m se (SComprehension (simple $ TypeList bodyType)) (mapM_ addRegion (dGens ++ dBody))
1657 return . Typed (TypeList bodyType) $ Comprehension (untype r) gens
1658 where
1659 flagExtraExpressions :: [RegionTagged a] -> ValidatorS ()
1660 flagExtraExpressions [] = pure ()
1661 flagExtraExpressions xs = raiseError $ catRegions xs <!> SemanticError "Comprehensension may have only one expression before |"
1662
1663 validateComprehension :: ComprehensionNode -> ValidatorS [GeneratorOrCondition]
1664 validateComprehension (ComprehensionNode l1 body) = do
1665 l1 `isA` TtKeyword
1666 concat <$> validateSequence_ validateComprehensionBody body
1667
1668 validateComprehensionBody :: ComprehensionBodyNode -> ValidatorS [GeneratorOrCondition]
1669 -- guard
1670 validateComprehensionBody (CompBodyCondition en) = wrapRegion en en SGuard $ do
1671 e <- validateExpression en ?=> exactly TypeBool
1672 return [Condition e]
1673 -- x in dom
1674 validateComprehensionBody c@(CompBodyDomain apn l1 dom) = wrapRegion c apn SGen $ do
1675 l1 `isA` TtKeyword
1676 putDocs "expr_in_domain_projection" l1
1677 (td, domain) <- typeSplit <$> validateDomain dom
1678 td' <- projectionTypeDomain (symbolRegion dom) td
1679 pats <- validateSequence_ (flip unifyPattern td' . Just) apn
1680 return $ [Generator (GenDomainNoRepr pat domain) | pat <- pats]
1681
1682 -- x <- expr
1683 validateComprehensionBody c@(CompBodyGenExpr apn lt en) = wrapRegion c apn SGen $ do
1684 lt `isA` TtKeyword
1685 putDocs "expr_projection" lt
1686 e <- validateExpression en
1687 let (t, exp) = typeSplit e
1688 t' <- projectionType (symbolRegion en) t
1689 pats <- validateSequence_ (flip unifyPattern t' . Just) apn
1690 return $ [Generator (GenInExpr pat exp) | pat <- pats]
1691 -- letting x be
1692 validateComprehensionBody c@(CompBodyLettingNode l1 nn l2 en) = wrapRegion c nn SLetting $ do
1693 l1 `isA` TtKeyword
1694 l2 `isA'` TtKeyword
1695 (t, expr) <- typeSplit <$> validateExpression en
1696 pat <- unifyPattern (Just nn) t
1697 return [ComprehensionLetting pat expr]
1698
1699 projectionType :: DiagnosticRegion -> Type -> ValidatorS Type
1700 projectionType r t = case t of
1701 TypeAny -> return TypeAny
1702 TypeTuple _ -> return t
1703 TypeMatrix _ ty -> return ty
1704 TypeList ty -> return ty
1705 TypeSet ty -> return ty
1706 TypeMSet ty -> return ty
1707 TypeSequence ty -> return $ TypeTuple [tInt, ty]
1708 TypePermutation ty -> return $ TypeTuple [ty, ty]
1709 TypeRelation ts -> return $ TypeTuple ts
1710 TypePartition ty -> return $ TypeSet ty
1711 TypeFunction fr to -> return $ TypeTuple [fr, to]
1712 _ -> raiseTypeError (r <!> SemanticError (pack $ "Expression of type " ++ show (pretty t) ++ " cannot be projected in a comprehension")) >> return TypeAny
1713
1714 projectionTypeDomain :: DiagnosticRegion -> Type -> ValidatorS Type
1715 projectionTypeDomain _ t = case t of -- TODO check and do properly
1716 TypeAny -> return TypeAny
1717 TypeEnum (Name n) -> return $ TypeInt $ TagEnum n
1718 TypeUnnamed (Name n) -> return $ TypeInt $ TagUnnamed n
1719 _ -> return t
1720
1721 -- _ -> (raiseTypeError $ r <!> SemanticError (pack $ "Domain of type " ++ (show $pretty t) ++ " cannot be projected in a comprehension")) >> return TypeAny
1722
1723 mkAbstractLiteral :: AbstractLiteral Expression -> Expression
1724 mkAbstractLiteral x = case e2c (AbstractLiteral x) of
1725 Nothing -> AbstractLiteral x
1726 Just c -> Constant c
1727
1728 enforceConstraint :: Maybe Bool -> String -> ValidatorS ()
1729 enforceConstraint p msg = case p of
1730 Just True -> return ()
1731 _ -> void (contextError (CustomError $ pack msg))
1732
1733 checkSymbols :: [LToken] -> ValidatorS ()
1734 checkSymbols = mapM_ validateSymbol
1735
1736 -- Raise a non structural error (i.e type error)
1737 raiseError :: ValidatorDiagnostic -> ValidatorS ()
1738 raiseError e = tell [e]
1739
1740 raiseTypeError :: ValidatorDiagnostic -> ValidatorS ()
1741 raiseTypeError e = do
1742 tc <- gets typeChecking
1743 when tc $ raiseError e
1744
1745 makeTupleLiteral :: [Typed Expression] -> ValidatorS (Typed Expression)
1746 makeTupleLiteral members = do
1747 let memberTypes = unzip $ map typeSplit members
1748 let eType = TypeTuple (fst memberTypes)
1749 return . Typed eType . mkAbstractLiteral . AbsLitTuple $ snd memberTypes
1750
1751 validateIntLiteral :: SToken -> Maybe (LToken, ETok) -> ValidatorS Constant
1752 validateIntLiteral t maybe_tag' = do
1753 let maybe_tag = case maybe_tag' of Nothing -> Nothing ; Just (_, tag) -> Just tag
1754 flagSToken t TtNumber
1755 l <- validateSToken t
1756 let tag = case maybe_tag of
1757 Just ta -> case lexeme ta of
1758 LIdentifier ta_i -> TaggedInt ta_i
1759 _ -> TagInt
1760 Nothing -> TagInt
1761 case l of
1762 (LIntLiteral x) -> return $ ConstantInt tag x
1763 _ -> error "Bad int literal"
1764
1765 validateBoolLiteral :: SToken -> ValidatorS Constant
1766 validateBoolLiteral t = do
1767 flagSToken t TtBool
1768 l <- validateSToken t
1769 case l of
1770 L_true -> return $ ConstantBool True
1771 L_false -> return $ ConstantBool False
1772 _ -> error "Bad bool literal"
1773
1774 validateNameList :: Sequence NameNode -> ValidatorS [RegionTagged Name]
1775 validateNameList = validateSequence validateName
1776
1777 validateNameList_ :: Sequence NameNode -> ValidatorS [Name]
1778 validateNameList_ = validateSequence_ validateName
1779
1780 validateIdentifierS :: NameNodeS -> ValidatorS Text
1781 validateIdentifierS (NameNodeS iden) = do
1782 q <- validateSToken iden
1783 case q of
1784 (LIdentifier x) -> checkName x >> return x
1785 _ -> bug $ "Name wasn't a name:" <+> pretty (show q)
1786 where
1787 checkName :: Text -> Validator Text
1788 checkName "" = invalid $ iden <!> SemanticError "Empty names not allowed"
1789 checkName "\"\"" = invalid $ iden <!> SemanticError "Empty names not allowed"
1790 checkName x = return . pure $ x
1791
1792 validateIdentifier :: NameNode -> ValidatorS Text
1793 validateIdentifier (NameNode nns) = validateIdentifierS nns
1794 validateIdentifier (MissingNameNode iden) = do
1795 _ <- validateSymbol iden
1796 return " <Missing name>"
1797
1798 validateName :: NameNode -> ValidatorS Name
1799 validateName name = do
1800 n <- validateIdentifier name
1801 return (Name n)
1802
1803 validateNameAs :: TagType -> NameNode -> ValidatorS Name
1804 validateNameAs f (NameNode n) = tagNameAs f n
1805 validateNameAs _ name = validateName name
1806
1807 tagNameAs :: TagType -> NameNodeS -> ValidatorS Name
1808 tagNameAs f nn@(NameNodeS n) = flagSToken n f >> Name <$> validateIdentifier (NameNode nn)
1809
1810 listToSeq :: ListNode a -> ValidatorS (Sequence a)
1811 listToSeq (ListNode l1 s l2) = checkSymbols [l1, l2] >> return s
1812
1813 -- visit a sequence, return a list of elements, nothing if missing
1814 sequenceElems :: (HighLevelTree a) => Sequence a -> ValidatorS [Maybe a]
1815 sequenceElems (Seq els) = mapM (validateSequenceElem_ validateIdentity) els
1816
1817 listElems :: (HighLevelTree a) => ListNode a -> ValidatorS [Maybe a]
1818 listElems = sequenceElems <=< listToSeq
1819
1820 validateIdentity :: a -> Validator a
1821 validateIdentity = return . pure
1822
1823 validateArray :: (a -> ValidatorS b) -> [a] -> ValidatorS [b]
1824 validateArray = mapM
1825
1826 validateList :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> ListNode a -> ValidatorS [RegionTagged b]
1827 validateList validator (ListNode st seq end) = do
1828 _ <- validateSymbol st
1829 _ <- validateSymbol end
1830 validateSequence validator seq
1831
1832 validateList_ :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> ListNode a -> ValidatorS [b]
1833 validateList_ validator (ListNode st seq end) = do
1834 _ <- validateSymbol st
1835 _ <- validateSymbol end
1836 validateSequence_ validator seq
1837
1838 -- mapPrefixToOp :: Lexeme -> Text
1839 -- mapPrefixToOp x = case x of
1840 -- L_Minus -> "negate"
1841 -- L_ExclamationMark -> "not"
1842 -- _ -> pack $ lexemeFace x
1843
1844 validateSequence :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> Sequence a -> ValidatorS [RegionTagged b]
1845 validateSequence f (Seq vals) = validateArray (validateSequenceElem f) vals
1846
1847 validateSequence_ :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> Sequence a -> ValidatorS [b]
1848 validateSequence_ f s = do
1849 q <- validateSequence f s
1850 return . map snd $ q
1851
1852 validateSequenceElem :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> SeqElem a -> ValidatorS (RegionTagged b)
1853 validateSequenceElem f (SeqElem i s) = do
1854 case s of
1855 Nothing -> pure ()
1856 Just lt -> void $ validateSymbol lt
1857 v <- f i
1858 return (symbolRegion i, v)
1859 validateSequenceElem _ (MissingSeqElem plc sepr) = do
1860 checkSymbols [sepr]
1861 raiseError $ symbolRegion plc <!> TokenError plc
1862 return (symbolRegion plc, fallback "Missing elem")
1863
1864 validateSequenceElem_ :: (HighLevelTree a, Fallback b) => (a -> ValidatorS b) -> SeqElem a -> ValidatorS b
1865 validateSequenceElem_ f (SeqElem i s) = do
1866 case s of
1867 Nothing -> pure ()
1868 Just lt -> void $ validateSymbol lt
1869 f i
1870 validateSequenceElem_ _ (MissingSeqElem plc sepr) = do
1871 checkSymbols [sepr]
1872 raiseError $ symbolRegion plc <!> TokenError plc
1873 return $ fallback "Missing Elem"
1874
1875 validateExprList :: ListNode ExpressionNode -> ValidatorS [RegionTagged (Typed Expression)]
1876 validateExprList = validateList validateExpression
1877
1878 validateExprList_ :: ListNode ExpressionNode -> ValidatorS [Typed Expression]
1879 validateExprList_ = validateList_ validateExpression
1880
1881 offsetPositionBy :: Int -> SourcePos -> SourcePos
1882 offsetPositionBy amt sp@(SourcePos _ _ (unPos -> r)) = sp {sourceColumn = mkPos (amt + r)}
1883
1884 data DiagnosticRegion = DiagnosticRegion
1885 { drSourcePos :: SourcePos,
1886 drEndPos :: SourcePos,
1887 drOffset :: Int,
1888 drLength :: Int
1889 }
1890 deriving (Show, Eq, Ord)
1891
1892 global :: DiagnosticRegion
1893 global = DiagnosticRegion sourcePos0 sourcePos0 0 0
1894
1895 -- getTokenRegion :: LToken -> DiagnosticRegion
1896 -- getTokenRegion a = do
1897 -- let h =case a of
1898 -- RealToken et -> et
1899 -- MissingToken et -> et
1900 -- SkippedToken et -> et
1901 -- let start = tokenSourcePos h
1902 -- let offset = tokenStart h
1903 -- let tLength =case a of
1904 -- RealToken _ -> trueLength h
1905 -- MissingToken _ -> 1
1906 -- SkippedToken _ -> trueLength h
1907 -- DiagnosticRegion start (offsetPositionBy tLength start) offset tLength
1908
1909 symbolRegion :: (HighLevelTree a) => a -> DiagnosticRegion
1910 symbolRegion a = case range of
1911 (h :<| rst) -> do
1912 let end = case viewr rst of
1913 EmptyR -> h
1914 _ :> et -> et
1915 let start = tokenSourcePos h
1916 let offset = tokenStartOffset h
1917 let tLength = sum (totalLength <$> rst) + trueLength h
1918 let en = sourcePosAfter end
1919 DiagnosticRegion start en offset tLength
1920 _ -> global
1921 where
1922 range :: Seq ETok = flattenSeq a
1923
1924 (<!>) :: (WithRegion a) => a -> ErrorType -> ValidatorDiagnostic
1925 t <!> e = ValidatorDiagnostic (getRegion t) $ Error e
1926
1927 (/!\) :: (WithRegion a) => a -> WarningType -> ValidatorDiagnostic
1928 t /!\ e = ValidatorDiagnostic (getRegion t) $ Warning e
1929
1930 (<?>) :: (WithRegion a) => a -> InfoType -> ValidatorDiagnostic
1931 t <?> e = ValidatorDiagnostic (getRegion t) $ Info e
1932
1933 -- (<?!>) :: WithRegion a => Maybe a -> ErrorType -> ValidatorDiagnostic
1934 -- Nothing <?!> e = ValidatorDiagnostic global $ Error e
1935 -- Just t <?!> e = t <!> e
1936
1937 contextError :: ErrorType -> Validator a
1938 contextError e = do
1939 q <- getContext
1940 invalid $ ValidatorDiagnostic q $ Error e
1941
1942 contextTypeError :: ErrorType -> ValidatorS ()
1943 contextTypeError e = do
1944 q <- getContext
1945 tc <- gets typeChecking
1946 when tc $ raiseError $ ValidatorDiagnostic q $ Error e
1947
1948 contextInfo :: InfoType -> ValidatorS ()
1949 contextInfo e = do
1950 q <- getContext
1951 tell [ValidatorDiagnostic q $ Info e]
1952 return ()
1953
1954 -- getType :: (Pretty a ,TypeOf a) => a -> ValidatorS Type
1955 -- getType a = do
1956 -- tc <- gets typeChecking
1957 -- (if tc then (do
1958 -- let t = let ?typeCheckerMode = StronglyTyped in typeOf a
1959 -- case t of
1960 -- Left err -> do
1961 -- void $ contextError (CustomError . pack $ "type err in :" ++ show (pretty a) ++ "err:" ++ show err)
1962 -- return TypeAny
1963 -- Right ty -> return ty) else return TypeAny)
1964
1965 -- assertType :: (Pretty a,TypeOf a) => Typed a -> Type -> Text -> ValidatorS ()
1966 -- assertType v ref msg = do
1967 -- let Typed t _ = v
1968 -- tc <- gets typeChecking
1969 -- unless (not tc || t == ref) $ void . contextError $ CustomError msg
1970
1971 resolveReference :: RegionTagged Name -> ValidatorS Kind
1972 resolveReference (r, Name n) | n /= "" = do
1973 c <- getSymbol n
1974 case c of
1975 Nothing -> raiseTypeError (r <!> CustomError (T.concat ["Symbol not found \"", n, "\""])) >> return (simple TypeAny)
1976 Just (reg, _, t) -> do
1977 putReference r n t reg
1978 -- addRegion (RegionInfo {rRegion=r,rText=n, rType=Just t, rDeclaration=Ref reg})
1979 return t
1980 resolveReference _ = return $ simple TypeAny
1981
1982 sameType :: [RegionTagged (Typed a)] -> ValidatorS (Typed [a])
1983 sameType [] = return $ Typed TypeAny []
1984 sameType xs@(x : _) = do
1985 let ?typeCheckerMode = StronglyTyped
1986 let t = mostDefined $ map (typeOf_ . snd) xs
1987 let t' = mostDefined [t, typeOf_ $ snd x] -- Do this again to set type to first elem if possible
1988 xs' <- mapM (unifyTypes t') xs
1989 return $ Typed t' xs'
1990
1991 typesUnifyS :: [Type] -> Bool
1992 typesUnifyS = let ?typeCheckerMode = StronglyTyped in typesUnify
1993
1994 mostDefinedS :: [Type] -> Type
1995 mostDefinedS [] = TypeAny
1996 mostDefinedS [x] = x
1997 mostDefinedS (x : xs) =
1998 let ?typeCheckerMode = StronglyTyped
1999 in case mostDefined (xs ++ [x]) of
2000 TypeAny -> x
2001 t -> t
2002
2003 unifyTypes :: Type -> RegionTagged (Typed a) -> ValidatorS a
2004 unifyTypes _ (r, Typed TypeAny a) = raiseError (r /!\ AmbiguousTypeWarning) >> return a
2005 unifyTypes t (r, Typed t' a) = do
2006 let ?typeCheckerMode = StronglyTyped
2007 if typesUnify [t', t] then pure () else raiseTypeError $ r <!> TypeError t t'
2008 return a
2009
2010 unifyTypesFailing :: Type -> RegionTagged (Typed a) -> Validator a
2011 unifyTypesFailing _ (r, Typed TypeAny a) = raiseError (r /!\ AmbiguousTypeWarning) >> return (Just a)
2012 unifyTypesFailing t (r, Typed t' a) = do
2013 tc <- gets typeChecking
2014 let ?typeCheckerMode = StronglyTyped
2015 if not tc || typesUnify [t', t] then return $ Just a else invalid (r <!> TypeError t t')
2016
2017 scoped :: ValidatorS a -> ValidatorS a
2018 scoped m = do
2019 st <- gets symbolTable
2020 res <- m
2021 modifySymbolTable $ const st
2022 return res
2023
2024 unifyPatterns :: Type -> [Maybe AbstractPatternNode] -> ValidatorS [AbstractPattern]
2025 unifyPatterns t = mapM (`unifyPattern` t)
2026
2027 unifyPattern :: Maybe AbstractPatternNode -> Type -> ValidatorS AbstractPattern
2028 unifyPattern (Just (AbstractIdentifier nn)) t = do
2029 nm <- tagNameAs TtLocal nn
2030 let n = case nm of
2031 Name txt -> txt
2032 NameMetaVar s -> T.pack s
2033 _ -> bug "Bad name "
2034 void $ putSymbol (Name n, (symbolRegion nn, False, simple t))
2035 unless (n == "_") $ addRegion $ mkDeclaration (symbolRegion nn) n (simple t)
2036 -- addRegion (RegionInfo (symbolRegion nn) (Just $ simple t) n Definition)
2037 return $ Single $ Name n
2038 unifyPattern (Just (AbstractMetaVar lt)) _ = do
2039 s <- validateMetaVar lt
2040 return $ AbstractPatternMetaVar s
2041 unifyPattern (Just (AbstractPatternTuple m_lt ln)) t = do
2042 sps <- listToSeq ln
2043 ps <- sequenceElems sps
2044 case m_lt of
2045 Nothing -> void $ return ()
2046 Just lt -> lt `isA'` TtType
2047 memberTypes <- case t of
2048 TypeAny -> return $ replicate (length ps) TypeAny
2049 TypeTuple ts -> do
2050 let dif = length ts - length ps
2051 unless (dif <= 0) $ raiseError $ symbolRegion ln <!> (CustomError . T.pack $ "Missing " ++ show dif ++ " fields from projection tuple, if you dont want the value, use '_'")
2052 return ts
2053 _ -> replicate (length ps) TypeAny <$ raiseTypeError (symbolRegion ln <!> CustomError (T.concat ["Could not project ", prettyT t, " onto tuple pattern"]))
2054
2055 let (paired, unpaired) = splitAt (length memberTypes) ps
2056 let q = zip paired memberTypes
2057 aps <- mapM (uncurry unifyPattern) q
2058 mapM_ (\x -> raiseError $ symbolRegion x <!> CustomError "Extraneous tuple field from projection") (catMaybes unpaired)
2059 return $ AbsPatTuple aps
2060 unifyPattern (Just (AbstractPatternMatrix ln)) t = do
2061 sps <- listToSeq ln
2062 ps <- sequenceElems sps
2063 memberTypes <- case t of
2064 TypeAny -> return $ repeat TypeAny
2065 TypeList ty -> return $ repeat ty
2066 TypeMatrix _ ty -> return $ repeat ty
2067 _ -> repeat TypeAny <$ raiseTypeError (symbolRegion ln <!> CustomError (T.concat ["Could not project ", prettyT t, " onto list pattern"]))
2068
2069 let q = zip ps memberTypes
2070 aps <- mapM (uncurry unifyPattern) q
2071 return $ AbsPatMatrix aps
2072 unifyPattern (Just (AbstractPatternSet ln)) t = do
2073 sps <- listToSeq ln
2074 ps <- sequenceElems sps
2075 memberTypes <- case t of
2076 TypeAny -> return $ repeat TypeAny
2077 TypeSet ty -> return $ repeat ty
2078 TypeMSet ty -> return $ repeat ty
2079 _ -> repeat TypeAny <$ raiseTypeError (symbolRegion ln <!> CustomError (T.concat ["Could not project ", prettyT t, " onto set pattern"]))
2080 let q = zip ps memberTypes
2081 aps <- mapM (uncurry unifyPattern) q
2082 return $ AbsPatSet aps
2083 unifyPattern Nothing _ = return . Single $ fallback "No Pattern"
2084
2085 catRegions :: [RegionTagged a] -> DiagnosticRegion
2086 catRegions [] = global
2087 catRegions (x:xs) =
2088 DiagnosticRegion
2089 { drSourcePos = drSourcePos $ fst x,
2090 drEndPos = drEndPos $ fst $ last xs,
2091 drOffset = drOffset $ fst x,
2092 drLength = sum $ map (drLength . fst) (x:xs)
2093 }
2094
2095 getMemberTypes :: Type -> ValidatorS [Type]
2096 getMemberTypes t = case t of
2097 TypeAny -> return $ repeat TypeAny
2098 TypeTuple tys -> return tys
2099 _ -> return $ repeat TypeAny
2100
2101 getDomainMembers :: Type -> Type
2102 getDomainMembers t = case t of
2103 TypeAny -> t
2104 TypeBool -> t
2105 TypeInt it -> case it of
2106 TaggedInt {} -> t
2107 TagInt -> t
2108 TagEnum _ -> error "Domain should use typeEnum instead"
2109 TagUnnamed _ -> error "Domain should use typeUnamed instead"
2110 TypeEnum n -> TypeInt . TagEnum $ case n of
2111 Name txt -> txt
2112 MachineName {} -> error "This should never be user specified"
2113 NameMetaVar s -> pack s
2114 TypeUnnamed n -> TypeInt . TagUnnamed $ case n of
2115 Name txt -> txt
2116 MachineName {} -> error "This should never be user specified"
2117 NameMetaVar s -> pack s
2118 TypeTuple tys -> TypeTuple $ map getDomainMembers tys
2119 TypeRecord tys -> TypeRecord $ map (second getDomainMembers) tys
2120 TypeVariant tys -> TypeVariant $ map (second getDomainMembers) tys
2121 TypeList ty -> TypeList $ getDomainMembers ty
2122 TypeMatrix ty ty' -> TypeMatrix ty $ getDomainMembers ty'
2123 TypeSet ty -> TypeSet $ getDomainMembers ty
2124 TypeMSet ty -> TypeMSet $ getDomainMembers ty
2125 TypeFunction ty ty' -> TypeFunction (getDomainMembers ty) (getDomainMembers ty')
2126 TypeSequence ty -> TypeSequence $ getDomainMembers ty
2127 TypePermutation ty -> TypePermutation $ getDomainMembers ty
2128 TypeRelation tys -> TypeRelation $ map getDomainMembers tys
2129 TypePartition ty -> TypePartition $ getDomainMembers ty
2130 _ -> bug $ "Unknown domain type" <+> pretty t
2131
2132 getDomainFromValue :: Type -> Type
2133 getDomainFromValue t = case t of
2134 TypeAny -> t
2135 TypeBool -> t
2136 TypeInt it -> case it of
2137 TaggedInt {} -> t
2138 TagInt -> t
2139 TagEnum n -> TypeEnum (Name n)
2140 TagUnnamed n -> TypeUnnamed (Name n)
2141 TypeEnum _ -> t
2142 TypeUnnamed _ -> t
2143 TypeTuple tys -> TypeTuple $ map getDomainFromValue tys
2144 TypeRecord tys -> TypeRecord $ map (second getDomainFromValue) tys
2145 TypeVariant tys -> TypeVariant $ map (second getDomainFromValue) tys
2146 TypeList ty -> TypeList $ getDomainFromValue ty
2147 TypeMatrix ty ty' -> TypeMatrix ty $ getDomainFromValue ty'
2148 TypeSet ty -> TypeSet $ getDomainFromValue ty
2149 TypeMSet ty -> TypeMSet $ getDomainFromValue ty
2150 TypeFunction ty ty' -> TypeFunction (getDomainFromValue ty) (getDomainFromValue ty')
2151 TypeSequence ty -> TypeSequence $ getDomainFromValue ty
2152 TypePermutation ty -> TypePermutation $ getDomainFromValue ty
2153 TypeRelation tys -> TypeRelation $ map getDomainFromValue tys
2154 TypePartition ty -> TypePartition $ getDomainFromValue ty
2155 _ -> bug $ "Unknown member type" <+> pretty t
2156
2157 data DomainTyped a = DomainTyped DomainType a
2158
2159 data DomainSize = Unkown | Infinite | Sized Int
2160
2161 data DomainType
2162 = DomainTypeBool
2163 | DomainTypeInt DomainSize
2164 | DomainTypeTuple [DomainType]
2165
2166 f2n :: (a -> ValidatorS b) -> a -> Validator b
2167 f2n f a = do
2168 q <- f a
2169 return $ Just q
2170
2171 class Fallback a where
2172 fallback :: Text -> a
2173
2174 instance Fallback (Domain () Expression) where
2175 fallback reason = DomainAny reason TypeAny
2176
2177 instance Fallback Expression where
2178 fallback reason = Reference (Name reason) Nothing
2179
2180 instance (Fallback a) => Fallback (Typed a) where
2181 fallback = Typed TypeAny . fallback
2182
2183 instance (Fallback a) => Fallback (Kind, a) where
2184 fallback msg = (Kind (ValueType CatConstant) TypeAny, fallback msg)
2185
2186 instance Fallback (Maybe a) where
2187 fallback = const Nothing
2188
2189 instance Fallback Name where
2190 fallback = Name
2191
2192 instance Fallback [a] where
2193 fallback :: Text -> [a]
2194 fallback = const []
2195
2196 instance Fallback AbstractPattern where
2197 fallback = Single . fallback
2198
2199 type FuncOpDec = Int
2200
2201 funcOpBuilder :: Lexeme -> [Arg] -> ValidatorS (Typed Expression)
2202 funcOpBuilder l = functionOps l (mkOp $ FunctionOp l)
2203
2204
2205 functionOps :: Lexeme -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2206 functionOps l = case l of
2207 L_fAnd -> unFuncV isLogicalContainer (pure . const TypeBool)
2208 L_fOr -> unFuncV isLogicalContainer (pure . const TypeBool)
2209 L_fXor -> unFuncV isLogicalContainer (pure . const TypeBool)
2210 L_Sum -> unFuncV sumArgs (pure . const tInt)
2211 L_Product -> unFunc (valueOnly sumArgs) (pure . const tInt)
2212 L_true -> unFuncV anyType (pure . const TypeBool)
2213 L_toInt -> unFuncV (only TypeBool) (pure . const tInt)
2214 L_makeTable -> unFuncV (only TypeBool) (pure . const TypeBool)
2215 L_table -> biFuncV tableArgs (const2 TypeBool)
2216 L_gcc -> triFunc (each3 $ valueOnly listInt) (const3 TypeBool)
2217 L_elementId -> biFuncV elementIdArgs elementIdType
2218 L_atleast -> triFunc (each3 $ valueOnly listInt) (const3 TypeBool)
2219 L_atmost -> triFunc (each3 $ valueOnly listInt) (const3 TypeBool)
2220 L_defined -> unFuncV funcSeq (fmap TypeSet . funcDomain)
2221 L_range -> unFuncV funcSeq (fmap TypeSet . funcRange)
2222 L_restrict -> biFunc restrictArgs restrictTypes
2223 L_allDiff -> unFuncV listOrMatrix (const $ pure TypeBool)
2224 L_alldifferent_except -> biFuncV (indep listOrMatrix enumerable) (const2 TypeBool)
2225 L_catchUndef -> biFuncV unifies (\a b -> pure $ mostDefinedS $ catMaybes [a, b])
2226 L_quickPermutationOrder -> biFunc quickPermutationOrderArgs quickPermutationOrderTypes
2227 L_dontCare -> unFunc anyType (const $ pure TypeBool)
2228 L_toSet -> unFuncV toSetArgs typeToSet
2229 L_toMSet -> unFuncV toMSetArgs typeToMSet
2230 L_toRelation -> unFuncV func typeToRelation
2231 L_max -> unFunc minMaxArgs minMaxType
2232 L_min -> unFunc minMaxArgs minMaxType
2233 L_image -> biFuncV imageArgs (const . funcRange)
2234 L_transform -> biFuncV transformArgs (const id)
2235 L_imageSet -> biFuncV imSetArgs (\a -> const $ TypeSet <$> funcRange a)
2236 L_compose -> biFuncV composeArgs (const . funcRange)
2237 L_preImage -> biFuncV preImageArgs (\a -> const $ TypeSet <$> funcDomain a)
2238 L_inverse -> biFuncV inverseArgs (const2 TypeBool)
2239 L_freq -> biFuncV freqArgs (const2 tInt)
2240 L_hist -> unFuncV histArgs histType
2241 L_parts -> unFuncV part partsType
2242 L_together -> biFuncV setPartArgs (const2 TypeBool)
2243 L_apart -> biFuncV setPartArgs (const2 TypeBool)
2244 L_party -> biFuncV partyArgs partyType
2245 L_permInverse -> unFuncV permInverseArgs id
2246 L_participants -> unFuncV part partInner
2247 L_active -> biFuncV activeArgs (const2 TypeBool)
2248 L_pred -> unFuncV enumerable enumerableType
2249 L_succ -> unFuncV enumerable enumerableType
2250 L_factorial -> unFuncV (only tInt) (const $ pure tInt)
2251 L_powerSet -> unFuncV set powerSetType
2252 L_concatenate -> unFuncV concatArgs concatType
2253 L_flatten -> \b a -> case a of
2254 [] -> unFuncV unaryFlattenArgs (flattenType Nothing) b a
2255 [_] -> unFuncV unaryFlattenArgs (flattenType Nothing) b a
2256 _ -> biFunc (valueOnly2 binaryFlattenArgs) (\v t -> flattenType (getNum v) (typeOnly t)) b a
2257 _ -> bug $ pretty $ "Unkown functional operator " ++ show l
2258 where
2259 valueOnly :: (SArg -> Validator a) -> Arg -> Validator a
2260 valueOnly f (r, (k, e)) = do
2261 t <- getValueType k
2262 f (r, Typed t e)
2263
2264 valueOnly2 :: (SArg -> SArg -> Validator a) -> Arg -> Arg -> Validator a
2265 valueOnly2 f (r1, (k1, e1)) (r2, (k2, e2)) = do
2266 t1 <- getValueType k1
2267 t2 <- getValueType k2
2268 f (r1, Typed t1 e1) (r2, Typed t2 e2)
2269
2270 typeOnly :: Maybe (Kind, Expression) -> Maybe Type
2271 typeOnly (Just (Kind ValueType {} t, _)) = Just t
2272 typeOnly _ = Nothing
2273
2274 unFuncV ::
2275 (SArg -> Validator a0) ->
2276 (Maybe Type -> Maybe Type) ->
2277 ([Expression] -> Expression) ->
2278 [Arg] ->
2279 ValidatorS (Typed Expression)
2280 unFuncV a t = unFunc (valueOnly a) (t . typeOnly)
2281
2282 biFuncV :: (SArg -> SArg -> Validator ()) -> (Maybe Type -> Maybe Type -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2283 biFuncV a t = biFunc (valueOnly2 a) (\t1 t2 -> t (typeOnly t1) (typeOnly t2))
2284
2285 valid = return $ pure ()
2286
2287 const2 = const . const . pure
2288
2289 const3 = const . const . const . pure
2290
2291 getNum :: Maybe (Kind, Expression) -> Maybe Int
2292 getNum (Just (_, x)) = case intOut "" x of
2293 Nothing -> Nothing
2294 Just n -> pure $ fromInteger n
2295 getNum _ = Nothing
2296
2297 each3 f a b c = f a >> f b >> f c
2298
2299 anyType = const . return $ Just ()
2300
2301 indep :: (SArg -> Validator ()) -> (SArg -> Validator ()) -> (SArg -> SArg -> Validator ())
2302 indep f1 f2 a b = do
2303 v1 <- f1 a
2304 v2 <- f2 b
2305 if not . null $ catMaybes [v1, v2] then return $ pure () else return Nothing
2306
2307 binaryFlattenArgs :: SArg -> SArg -> Validator ()
2308 binaryFlattenArgs (r1, d) b = do
2309 off <- case intOut "" (untype d) of
2310 Just (fromInteger -> a :: Integer) | a > 0 -> return $ Just a
2311 _ -> invalid $ r1 <!> CustomError "1st arg must be a constant positive int"
2312 let ref = map (const TypeList) [0 .. fromMaybe 1 off]
2313 let ref' = foldr id TypeAny ref
2314 r <- unifyTypesFailing ref' b
2315 return $ if null off || null r then Nothing else Just ()
2316
2317 unaryFlattenArgs :: SArg -> Validator ()
2318 unaryFlattenArgs (_, typeOf_ -> (TypeMatrix _ _)) = valid
2319 unaryFlattenArgs (_, typeOf_ -> (TypeList _)) = valid
2320 unaryFlattenArgs (_, typeOf_ -> TypeAny) = valid
2321 unaryFlattenArgs (r, typeOf_ -> t) = invalid $ r <!> ComplexTypeError "List or Matrix " t
2322
2323 concatType :: Maybe Type -> Maybe Type
2324 concatType (Just (TypeMatrix _ (TypeList t))) = Just $ TypeList t
2325 concatType (Just (TypeMatrix _ (TypeMatrix _ t))) = Just $ TypeList t
2326 concatType (Just (TypeList (TypeList t))) = Just $ TypeList t
2327 concatType (Just (TypeList (TypeMatrix _ t))) = Just $ TypeList t
2328 concatType _ = Just $ TypeList TypeAny
2329 concatArgs :: SArg -> Validator ()
2330 concatArgs s@(r, _) = binaryFlattenArgs (r, Typed tInt $ Constant $ ConstantInt TagInt 1) s
2331
2332 tableArgs :: SArg -> SArg -> Validator ()
2333 tableArgs (r1, typeOf_ -> t1) (r2, typeOf_ -> t2) = do
2334 a <- case t1 of
2335 t | isValidInner t -> valid
2336 _ -> invalid $ r1 <!> ComplexTypeError "Matrix of Int/Enum" t1
2337 b <- case t2 of
2338 TypeAny -> valid
2339 TypeList t | isValidInner t -> valid
2340 TypeMatrix _ t | isValidInner t -> valid
2341 _ -> invalid $ r2 <!> ComplexTypeError "Matrix of Matrix of Int/Enum" t2
2342
2343 return $ if null a || null b then Nothing else Just ()
2344 where
2345 isValidInner t = case t of
2346 TypeAny -> True
2347 TypeList TypeInt {} -> True
2348 TypeList TypeAny -> True
2349 TypeMatrix _ TypeInt {} -> True
2350 TypeMatrix _ TypeAny -> True
2351 _ -> False
2352
2353 elementIdArgs :: SArg -> SArg -> Validator ()
2354 elementIdArgs (r1, typeOf_ -> t1) (r2, typeOf_ -> t2) = do
2355 let ?typeCheckerMode = RelaxedIntegerTags
2356 a <- case t1 of
2357 TypeAny -> valid
2358 TypeMatrix _ _ -> valid
2359 TypeList _ -> valid
2360 _ -> invalid $ r1 <!> ComplexTypeError "Matrix or List" t1
2361 b <- case (t1, t2) of
2362 (TypeMatrix _indexType _, TypeAny) -> valid
2363 (TypeMatrix indexType _, actualIndex) | typesUnify [indexType, actualIndex] -> valid
2364 (TypeList _, TypeAny) -> valid
2365 (TypeList _, TypeInt {}) -> valid
2366 (TypeAny, _) -> valid
2367 _ -> invalid $ r2 <!> ComplexTypeError "Appropriate index type" t2
2368
2369 return $ if null a || null b then Nothing else Just ()
2370
2371 toMSetArgs :: SArg -> Validator ()
2372 toMSetArgs (r, typeOf_ -> a) = case a of
2373 TypeAny -> return $ pure ()
2374 TypeList _ -> return $ pure ()
2375 TypeMatrix {} -> return $ pure ()
2376 TypeMSet {} -> return $ pure ()
2377 TypeSet {} -> return $ pure ()
2378 TypeFunction {} -> return $ pure ()
2379 TypeRelation {} -> return $ pure ()
2380 _ -> invalid $ r <!> ComplexTypeError "Matrix ,list,function,relation,mset,set " a
2381
2382 toSetArgs :: SArg -> Validator ()
2383 toSetArgs (r, typeOf_ -> a) = case a of
2384 TypeAny -> return $ pure ()
2385 TypeList _ -> return $ pure ()
2386 TypeMatrix {} -> return $ pure ()
2387 TypeMSet {} -> return $ pure ()
2388 TypeFunction {} -> return $ pure ()
2389 TypeRelation {} -> return $ pure ()
2390 _ -> invalid $ r <!> ComplexTypeError "Matrix ,list,function,relation,mset " a
2391
2392 listOrMatrix :: SArg -> Validator ()
2393 listOrMatrix (r, typeOf_ -> a) = case a of
2394 TypeAny -> return $ pure ()
2395 TypeList _ -> return $ pure ()
2396 TypeMatrix {} -> return $ pure ()
2397 _ -> invalid $ r <!> ComplexTypeError "Matrix or list" a
2398
2399 freqArgs :: SArg -> SArg -> Validator ()
2400 freqArgs (r1, a) (r2, b) = do
2401 let tb = typeOf_ b
2402 let (rt, ti) = case typeOf_ a of
2403 TypeMatrix idx ms -> (TypeMatrix idx md, md) where md = mostDefinedS [tb, ms]
2404 TypeMSet ms -> (TypeMSet md, md) where md = mostDefinedS [tb, ms]
2405 _ -> (TypeMatrix tInt tb, tb)
2406 a' <- unifyTypesFailing rt (r1, a)
2407 b' <- unifyTypesFailing ti (r2, b)
2408 return $ if null a' || null b' then Nothing else Just ()
2409
2410 unifies :: SArg -> SArg -> Validator ()
2411 unifies a b = do
2412 let md = mostDefinedS $ map (typeOf_ . unregion) [a, b]
2413 a' <- unifyTypesFailing md a
2414 b' <- unifyTypesFailing md b
2415 return $ if null a' || null b' then Nothing else Just ()
2416
2417 func :: SArg -> Validator ()
2418 func (_, Typed (TypeFunction _ _) _) = valid
2419 func (_, Typed TypeAny _) = valid
2420 func (r, Typed t _) = invalid $ r <!> TypeError (TypeFunction TypeAny TypeAny) t
2421
2422 set :: SArg -> Validator Type
2423 set (_, Typed (TypeSet t) _) = return $ pure t
2424 set (_, Typed TypeAny _) = return $ pure TypeAny
2425 set (r, Typed t _) = invalid $ r <!> TypeError (TypeSet TypeAny) t
2426
2427 powerSetType (Just ((TypeSet i))) = Just $ TypeSet (TypeSet i)
2428 powerSetType _ = Just $ TypeSet $ TypeSet TypeAny
2429
2430 only t (r, typeOf_ -> t') = do
2431 setContext r
2432 if t' == TypeAny || t == t'
2433 then return $ Just t
2434 else invalid $ r <!> TypeError t t'
2435
2436 listInt (r, typeOf_ -> t') = case t' of
2437 TypeAny -> return $ Just t'
2438 TypeList TypeInt {} -> return $ Just t'
2439 TypeMatrix _ TypeInt {} -> return $ Just t'
2440 _ -> invalid $ r <!> ComplexTypeError "Matrix or list of int or enum" t'
2441
2442 partInner :: Maybe Type -> Maybe Type
2443 partInner (Just (TypePartition a)) = Just $ TypeSet a
2444 partInner _ = Just $ TypeSet TypeAny
2445
2446 restrictArgs :: Arg -> Arg -> Validator ()
2447 restrictArgs (r1, (k, _)) (r2, (kd, _)) = do
2448 setContext r1
2449 funcType <- getValueType k
2450 setContext r2
2451 domType <- getDomainType kd
2452 unifyTypesFailing (TypeFunction domType TypeAny) (r1, Typed funcType ())
2453
2454 restrictTypes :: Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type
2455 restrictTypes (fmap fst -> kv) (fmap fst -> kd) = Just $ TypeFunction from to
2456 where
2457 dType = case kd of
2458 Just (Kind DomainType t) -> getDomainMembers t
2459 _ -> TypeAny
2460 from = case kv of
2461 Just (Kind ValueType {} (TypeFunction fr _)) | typesUnifyS [dType, fr] -> mostDefinedS [dType, fr]
2462 Just (Kind ValueType {} (TypeFunction fr _)) -> fr
2463 _ -> mostDefinedS [TypeAny, dType]
2464 to = case kv of
2465 Just (Kind ValueType {} (TypeFunction _ to')) -> to'
2466 _ -> TypeAny
2467
2468 -- TODO: validate
2469 quickPermutationOrderArgs :: Arg -> Arg -> Validator ()
2470 quickPermutationOrderArgs _ _ = return (pure ())
2471
2472 -- TODO
2473 permInverseArgs :: SArg -> Validator ()
2474 permInverseArgs _ = return (pure ())
2475
2476 -- TODO
2477 quickPermutationOrderTypes :: Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type
2478 quickPermutationOrderTypes _ _ = Just TypeBool
2479
2480 imSetArgs :: SArg -> SArg -> Validator ()
2481 imSetArgs (r1, a) (r2, b) = do
2482 let t = case (typeOf_ a, typeOf_ b) of
2483 (TypeFunction i _, tb) -> mostDefinedS [i, tb]
2484 (TypeSequence _, _) -> tInt
2485 (_, tb) -> tb
2486 a' <- unifyTypesFailing (TypeFunction t TypeAny) (r1, a)
2487 b' <- unifyTypesFailing t (r2, b)
2488 return $ if null a' || null b' then Nothing else Just ()
2489
2490 preImageArgs :: SArg -> SArg -> Validator ()
2491 preImageArgs _ _ = return $ Just ()
2492 -- preImageArgs (r1, a) (r2, b) = do
2493 -- let t = case (typeOf_ a, typeOf_ b) of
2494 -- (TypeFunction _ i, tb) -> mostDefinedS [i, tb]
2495 -- (TypeSequence i, _) -> i
2496 -- (_, tb) -> tb
2497 -- a' <- unifyTypesFailing (TypeFunction TypeAny t) (r1, a)
2498 -- b' <- unifyTypesFailing t (r2, b)
2499 -- return $ if null a' || null b' then Nothing else Just ()
2500
2501 partyArgs :: SArg -> SArg -> Validator ()
2502 partyArgs (r1, a) (r2, b) = do
2503 let t = case (typeOf_ a, typeOf_ b) of
2504 (ta, TypePartition tb) -> mostDefinedS [ta, tb]
2505 (ta, _) -> ta
2506 a' <- unifyTypesFailing t (r1, a)
2507 b' <- unifyTypesFailing (TypePartition t) (r2, b)
2508 return $ if null a' || null b' then Nothing else Just ()
2509
2510 inverseArgs :: SArg -> SArg -> Validator ()
2511 inverseArgs (_r1, a) (_r2, b) =
2512 case (typeOf_ a, typeOf_ b) of
2513 (TypeFunction {}, TypeFunction {}) -> return (Just ())
2514 (TypeFunction {}, _) -> return (Just ())
2515 (_, TypeFunction {}) -> return (Just ())
2516 (TypePermutation {}, TypePermutation {}) -> return (Just ())
2517 (TypePermutation {}, _) -> return (Just ())
2518 (_, TypePermutation {}) -> return (Just ())
2519 _ -> return Nothing
2520
2521 setPartArgs :: SArg -> SArg -> Validator ()
2522 setPartArgs (r1, a) (r2, b) = do
2523 let t = case (typeOf_ a, typeOf_ b) of
2524 (TypeSet st, TypePartition pt) -> mostDefinedS [st, pt]
2525 (TypeSet st, _) -> st
2526 (_, TypePartition ts) -> ts
2527 _ -> TypeAny
2528 a' <- unifyTypesFailing (TypeSet t) (r1, a)
2529 b' <- unifyTypesFailing (TypePartition t) (r2, b)
2530 return $ if null a' || null b' then Nothing else Just ()
2531
2532 partyType :: Maybe Type -> Maybe Type -> Maybe Type
2533 partyType a b = do
2534 let at' = fromMaybe TypeAny a
2535 let bt = case b of
2536 Just (TypePartition t) -> t
2537 _ -> TypeAny
2538 return $ TypeSet $ mostDefinedS [at', bt]
2539
2540 partsType :: Maybe Type -> Maybe Type
2541 partsType (Just (TypePartition a)) = Just $ TypeSet $ TypeSet a
2542 partsType (Just TypeAny) = Just $ TypeSet $ TypeSet TypeAny
2543 partsType _ = Nothing
2544
2545 minMaxArgs :: Arg -> Validator ()
2546 minMaxArgs (r, (Kind DomainType t, _)) =
2547 case t of
2548 TypeInt TagInt -> valid
2549 TypeInt (TagEnum _) -> valid
2550 TypeEnum {} -> valid
2551 TypeAny -> valid
2552 _ -> invalid $ r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t
2553 minMaxArgs (r, (k, _)) = do
2554 t <- getValueType k
2555 inner <- case t of
2556 TypeList tyInner -> return tyInner
2557 TypeMatrix _ tyInner -> return tyInner
2558 TypeSet tyInner -> return tyInner
2559 TypeMSet tyInner -> return tyInner
2560 TypeAny -> return TypeAny
2561 _ -> TypeAny <$ invalid (r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t)
2562 case inner of
2563 TypeInt TagInt -> valid
2564 TypeInt (TagEnum _) -> valid
2565 TypeEnum {} -> valid
2566 TypeAny -> valid
2567 _ -> invalid $ r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t
2568
2569 minMaxType :: Maybe (Kind, a) -> Maybe Type
2570 minMaxType (Just (Kind DomainType t@(TypeInt {}), _)) = Just t
2571 minMaxType (Just (Kind DomainType (TypeEnum (Name nm)), _)) = Just . TypeInt $ TagEnum nm
2572 minMaxType (Just (Kind ValueType {} (TypeMatrix _ a), _)) = minMaxType (Just (Kind DomainType a, ()))
2573 minMaxType (Just (Kind ValueType {} (TypeList a), _)) = minMaxType (Just (Kind DomainType a, ()))
2574 minMaxType (Just (Kind ValueType {} (TypeSet a), _)) = minMaxType (Just (Kind DomainType a, ()))
2575 minMaxType (Just (Kind ValueType {} (TypeMSet a), _)) = minMaxType (Just (Kind DomainType a, ()))
2576 minMaxType _ = Just TypeAny
2577
2578 transformArgs :: SArg -> SArg -> Validator ()
2579 transformArgs _ _ = return $ pure ()
2580 activeArgs :: SArg -> SArg -> Validator ()
2581 activeArgs (_, typeOf_ -> TypeAny) _ = valid
2582 activeArgs (r, typeOf_ -> t@(TypeVariant _)) (r2, typeOf_ -> b) = checkRVMember (r, t) (r2, b)
2583 activeArgs (r, typeOf_ -> t) _ = invalid $ r <!> ComplexTypeError "Variant " t
2584
2585 typeToSet :: Maybe Type -> Maybe Type
2586 typeToSet (Just t) = Just . TypeSet $ fromMaybe TypeAny (tMembers t)
2587 typeToSet _ = Just $ TypeSet TypeAny
2588
2589 typeToMSet :: Maybe Type -> Maybe Type
2590 typeToMSet (Just t) = Just . TypeMSet $ fromMaybe TypeAny (tMembers t)
2591 typeToMSet _ = Just $ TypeMSet TypeAny
2592
2593 typeToRelation :: Maybe Type -> Maybe Type
2594 typeToRelation (Just (TypeFunction i j)) = Just $ TypeRelation [i, j]
2595 typeToRelation (Just TypeAny) = Just $ TypeRelation [TypeAny, TypeAny]
2596 typeToRelation _ = Nothing
2597 tMembers t = case t of
2598 TypeAny -> Just TypeAny
2599 TypeList ty -> Just ty
2600 TypeMatrix _ i -> Just i
2601 TypeSet ty -> Just ty
2602 TypeMSet ty -> Just ty
2603 TypeFunction i j -> Just $ TypeTuple [i, j]
2604 TypeRelation tys -> Just $ TypeTuple tys
2605 _ -> Nothing
2606
2607 imageArgs :: SArg -> SArg -> Validator ()
2608 imageArgs (r1, typeOf_ -> t1) r2 = do
2609 from <- case t1 of
2610 TypeAny -> return $ Just TypeAny
2611 TypeFunction a _ -> return $ Just a
2612 TypeSequence _ -> return $ Just tInt
2613 TypePermutation a -> return $ Just a
2614 _ -> Nothing <$ raiseTypeError (r1 <!> ComplexTypeError "function, sequence or permutation" t1)
2615 case from of
2616 Just f -> unifyTypes f r2 >> return (pure ())
2617 Nothing -> return Nothing
2618
2619 -- TODO: validate
2620 composeArgs :: SArg -> SArg -> Validator ()
2621 composeArgs _ _ = return (pure ())
2622
2623 sumArgs :: SArg -> Validator ()
2624 sumArgs (r, typeOf_ -> t') = do
2625 t <- case t' of
2626 TypeAny -> return TypeAny
2627 TypeList t -> return t
2628 TypeMatrix _ t -> return t
2629 TypeSet t -> return t
2630 TypeMSet t -> return t
2631 _ -> TypeAny <$ raiseTypeError (r <!> ComplexTypeError "matrix or set" t')
2632 case t of
2633 TypeAny -> return $ pure ()
2634 TypeInt TagInt -> return $ pure ()
2635 _ -> Nothing <$ raiseTypeError (r <!> ComplexTypeError "integer elements" t)
2636
2637 funcSeq :: SArg -> Validator ()
2638 funcSeq (r, typeOf_ -> t') = case t' of
2639 TypeAny -> return $ pure ()
2640 TypeSequence _ -> return $ pure ()
2641 TypePermutation _ -> return $ pure ()
2642 TypeFunction _ _ -> return $ pure ()
2643 _ -> invalid $ r <!> ComplexTypeError "function, sequence or permutation" t'
2644
2645 funcDomain :: Maybe Type -> Maybe Type
2646 funcDomain (Just (TypeFunction a _)) = Just a
2647 funcDomain (Just (TypeSequence _)) = Just tInt
2648 funcDomain _ = Just TypeAny
2649
2650 funcRange :: Maybe Type -> Maybe Type
2651 funcRange (Just (TypeFunction _ b)) = Just b
2652 funcRange (Just ((TypeSequence b))) = Just b
2653 funcRange _ = Just TypeAny
2654
2655 elementIdType :: Maybe Type -> Maybe Type -> Maybe Type
2656 elementIdType (Just (TypeMatrix _ innerType)) _ = Just innerType
2657 elementIdType (Just (TypeList innerType)) _ = Just innerType
2658 elementIdType _ _ = Just TypeAny
2659
2660 part :: SArg -> Validator ()
2661 part (r, typeOf_ -> t) = case t of
2662 TypeAny -> valid
2663 TypePartition _ -> return $ pure ()
2664 _ -> invalid $ r <!> TypeError (TypePartition TypeAny) t
2665
2666 histArgs :: SArg -> Validator ()
2667 histArgs (r, typeOf_ -> a) = case a of
2668 TypeMSet _ -> return $ pure ()
2669 TypeList _ -> return $ pure ()
2670 TypeMatrix _ _ -> return $ pure ()
2671 TypeAny -> return $ pure ()
2672 _ -> invalid $ r <!> ComplexTypeError "matrix, list or mset" a
2673
2674 histType :: Maybe Type -> Maybe Type
2675 histType (Just ((TypeMSet a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2676 histType (Just ((TypeMatrix _ a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2677 histType (Just ((TypeList a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2678 histType _ = Just $ TypeMatrix tInt $ TypeTuple [TypeAny, tInt]
2679
2680 enumerable :: SArg -> Validator ()
2681 enumerable (r, typeOf_ -> t) = case t of
2682 TypeAny -> return $ pure ()
2683 TypeInt TagUnnamed {} -> invalid $ r <!> CustomError "Anonymous enums are not explictly enumerable"
2684 TypeInt _ -> return $ pure ()
2685 TypeEnum {} -> return $ pure ()
2686 TypeBool -> return $ pure ()
2687 _ -> invalid $ r <!> ComplexTypeError "int, enum or bool" t
2688
2689 enumerableType :: Maybe Type -> Maybe Type
2690 enumerableType (Just t@(TypeInt TagInt)) = Just t
2691 enumerableType (Just t@(TypeInt (TagEnum _))) = Just t
2692 enumerableType (Just t@(TypeEnum {})) = Just t
2693 enumerableType _ = Nothing
2694
2695 flattenType :: Maybe Int -> Maybe Type -> Maybe Type
2696 flattenType (Just n) (Just a) | n < 0 = Just $ TypeList a
2697 flattenType (Just n) (Just (TypeList m)) = flattenType (Just (n - 1)) (Just m)
2698 flattenType (Just n) (Just (TypeMatrix _ m)) = flattenType (Just (n - 1)) (Just m)
2699 flattenType Nothing (Just (TypeMatrix _ m)) = flattenType Nothing (Just m)
2700 flattenType Nothing (Just (TypeList m)) = flattenType Nothing (Just m)
2701 flattenType Nothing (Just t) = Just $ TypeList t
2702 flattenType _ _ = Just $ TypeList TypeAny
2703
2704 validateFuncOp :: Lexeme -> [RegionTagged (Kind, Expression)] -> ValidatorS (Typed Expression)
2705 validateFuncOp l args = do
2706 let b = funcOpBuilder l
2707 b args
2708
2709 -- case argCheck of
2710 -- Nothing -> return $ Typed (r []) $ fallback "arg fail"
2711 -- Just tys -> return $ Typed (r tys)(b $ map untype tys)
2712
2713 isOfType :: Type -> RegionTagged (Typed Expression) -> ValidatorS Bool
2714 isOfType t (r, v) = setContext r >> return v ?=> exactly t >> return (typesUnifyS [t, typeOf_ v])
2715
2716 isLogicalContainer :: RegionTagged (Typed Expression) -> Validator ()
2717 isLogicalContainer (r, Typed t _) = case t of
2718 TypeAny -> return $ pure ()
2719 TypeList TypeAny -> return $ pure ()
2720 TypeList TypeBool -> return $ pure ()
2721 TypeMatrix _ TypeAny -> return $ pure ()
2722 TypeMatrix _ TypeBool -> return $ pure ()
2723 TypeSet TypeAny -> return $ pure ()
2724 TypeMSet TypeBool -> return $ pure ()
2725 _ -> invalid $ r <!> ComplexTypeError "Collection of Booleans" t
2726
2727 -- validateArgList :: [RegionTagged (Typed Expression) -> ValidatorS Bool] -> [RegionTagged (Typed Expression)] -> Validator [Typed Expression]
2728 -- validateArgList ps args | length args < length ps = do invalid $ args <!> MissingArgsError (length ps)
2729 -- validateArgList ps args = do
2730 -- let ps' = ps ++ repeat argOverflow
2731 -- xs <- zipWithM id ps' args
2732 -- return (if and xs then Just $ map unregion args else Nothing)
2733
2734 -- argOverflow :: RegionTagged a -> ValidatorS Bool
2735 -- argOverflow (region,_) = do
2736 -- setContext region
2737 -- void . contextError $ CustomError "Extra Args"
2738 -- return False
2739 type SArg = RegionTagged (Typed Expression)
2740
2741 type Arg = RegionTagged (Kind, Expression)
2742
2743 unFunc ::
2744 (Arg -> Validator a) -> -- Arg validator
2745 (Maybe (Kind, Expression) -> Maybe Type) -> -- typeEvaluator
2746 ([Expression] -> Expression) -> -- mkOp or similar
2747 [Arg] ->
2748 ValidatorS (Typed Expression)
2749 unFunc argVal t f args = do
2750 (v, ts) <- case args of
2751 [] -> tooFewArgs 1 0 >> return (Nothing, Nothing)
2752 [x] -> do
2753 r <- argVal x
2754 tc <- gets typeChecking
2755 let result = case r of
2756 Nothing | tc -> Nothing
2757 _ -> Just [(snd . unregion) x]
2758 return (result, Just $ unregion x)
2759 (x : rs) -> do
2760 tooManyArgs rs
2761 r <- argVal x
2762 let result = case r of
2763 Nothing -> Nothing
2764 Just _ -> Just [(snd . unregion) x]
2765 return (result, Just $ unregion x)
2766 let res = maybe (fallback "Arg Fail Unfunc") f v
2767 return $ Typed (fromMaybe TypeAny $ t ts) res
2768
2769 biFunc :: (Arg -> Arg -> Validator a) -> (Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2770 biFunc argVal t f args = do
2771 (v, ts) <- case args of
2772 [] -> tooFewArgs 2 0 >> return (Nothing, (Nothing, Nothing))
2773 [x] -> tooFewArgs 2 1 >> return (Nothing, (Just $ unregion x, Nothing))
2774 [x, y] -> do
2775 r <- argVal x y
2776 tc <- gets typeChecking
2777 let result = case r of
2778 Nothing | tc -> Nothing
2779 _ -> Just $ map (snd . unregion) [x, y]
2780 return (result, (Just (unregion x), Just (unregion y)))
2781 (x : y : rs) -> do
2782 tooManyArgs rs
2783 r <- argVal x y
2784 let result = case r of
2785 Nothing -> Nothing
2786 Just _ -> Just $ map (snd . unregion) [x, y]
2787 return (result, (Just (unregion x), Just (unregion y)))
2788 let res = maybe (fallback "Arg Fail BiFunct") f v
2789 return $ Typed (fromMaybe TypeAny $ uncurry t ts) res
2790
2791 triFunc :: (Arg -> Arg -> Arg -> Validator a) -> (Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2792 triFunc argVal t f args = do
2793 (v, ts) <- case args of
2794 [] -> tooFewArgs 3 0 >> return (Nothing, (Nothing, Nothing, Nothing))
2795 [x] -> tooFewArgs 3 1 >> return (Nothing, (Just $ unregion x, Nothing, Nothing))
2796 [x, y] -> tooFewArgs 3 2 >> return (Nothing, (Just $ unregion x, Just $ unregion y, Nothing))
2797 [x, y, z] -> do
2798 r <- argVal x y z
2799 tc <- gets typeChecking
2800 let result = case r of
2801 Nothing | tc -> Nothing
2802 _ -> Just $ map (snd . unregion) [x, y, z]
2803 return (result, (Just (unregion x), Just (unregion y), Just (unregion z)))
2804 (x : y : z : rs) -> do
2805 tooManyArgs rs
2806 r <- argVal x y z
2807 let result = case r of
2808 Nothing -> Nothing
2809 Just _ -> Just $ map (snd . unregion) [x, y, z]
2810 return (result, (Just (unregion x), Just (unregion y), Just (unregion z)))
2811 let res = maybe (fallback "Arg Fail Tri") f v
2812 return $ Typed (fromMaybe TypeAny $ uncurry3 t ts) res
2813 where
2814 uncurry3 fn (a, b, c) = fn a b c -- todo export from prelude
2815
2816 tooFewArgs :: Int -> Int -> ValidatorS ()
2817 tooFewArgs n i = void . contextError $ MissingArgsError n i
2818
2819 tooManyArgs :: [RegionTagged a] -> ValidatorS ()
2820 tooManyArgs = mapM_ (\x -> raiseError $ x <!> UnexpectedArg)
2821
2822 checkRVMember :: RegionTagged Type -> RegionTagged Type -> Validator ()
2823 checkRVMember (_, TypeRecord ts) (_, TypeRecordMember nm _) | not . null $ lookup nm ts = return $ pure ()
2824 checkRVMember (_, TypeRecord ts) (r2, r) = do
2825 raiseTypeError $ r2 <!> TypeError (TypeRecordMember (Name "") ts) r
2826 return Nothing
2827 checkRVMember (_, TypeVariant ts) (_, TypeVariantMember nm _) | not . null $ lookup nm ts = return $ pure ()
2828 checkRVMember (_, TypeVariant ts) (r2, r) = do
2829 raiseTypeError $ r2 <!> TypeError (TypeVariantMember (Name "") ts) r
2830 return Nothing
2831 checkRVMember (r1, t) _ = do
2832 raiseTypeError $ r1 <!> TypeError (TypeVariant []) t
2833 return Nothing
2834
2835 type OpValidator = RegionTagged Kind -> RegionTagged Kind -> ValidatorS Type
2836
2837 type OpTyper = Kind -> Kind -> Type
2838
2839 sameToSameV :: (Type -> ValidatorS Type) -> (Type -> Type -> Type) -> OpValidator
2840 sameToSameV tc t (rl, kl) (rr, kr) = do
2841 setContext rl
2842 lt <- getValueType kl
2843 lt' <- tc lt
2844 setContext rr
2845 rt <- getValueType kr
2846 rt' <- tc rt
2847 let md = mostDefinedS [lt, rt]
2848 _ <- unifyTypesFailing md (rl, Typed lt' ())
2849 _ <- unifyTypesFailing md (rr, Typed rt' ())
2850 return $ t lt' rt'
2851
2852 binOpType :: Lexeme -> OpValidator
2853 binOpType l = case l of
2854 L_Plus -> sameToSameV number same
2855 L_Minus -> sameToSameV minusArgs same
2856 L_Times -> sameToSameV number same
2857 L_Div -> sameToSameV number same
2858 L_Mod -> sameToSameV number same
2859 L_Pow -> sameToSameV number same
2860 L_Eq -> sameToSameV pure cBool
2861 L_Neq -> sameToSameV pure cBool
2862 L_Lt -> sameToSameV orderable cBool
2863 L_Leq -> sameToSameV orderable cBool
2864 L_Gt -> sameToSameV orderable cBool
2865 L_Geq -> sameToSameV orderable cBool
2866 L_in -> checkIn
2867 L_And -> sameToSameV bools cBool
2868 L_Or -> sameToSameV bools cBool
2869 L_Imply -> sameToSameV bools cBool
2870 L_Iff -> sameToSameV bools cBool -- b b b
2871 L_subset -> sameToSameV setLike cBool -- set mset func rel
2872 L_subsetEq -> sameToSameV setLike cBool
2873 -- \^^^
2874 L_supset -> sameToSameV setLike cBool
2875 -- \^^^^
2876 L_supsetEq -> sameToSameV setLike cBool
2877 -- \^^
2878
2879 L_subsequence -> sameToSameV justSequence cBool -- seq - seq -bool
2880 L_substring -> sameToSameV justSequence cBool -- seq - seq -bool
2881 L_intersect -> sameToSameV setLike same
2882 L_union -> sameToSameV setLike same
2883 L_LexLt -> sameToSameV pure cBool
2884 L_LexLeq -> sameToSameV pure cBool
2885 L_LexGt -> sameToSameV pure cBool
2886 L_LexGeq -> sameToSameV pure cBool
2887 L_DotLt -> sameToSameV pure cBool
2888 L_DotLeq -> sameToSameV pure cBool
2889 L_DotGt -> sameToSameV pure cBool
2890 L_DotGeq -> sameToSameV pure cBool
2891 L_TildeLt -> sameToSameV pure cBool
2892 L_TildeLeq -> sameToSameV pure cBool
2893 L_TildeGt -> sameToSameV pure cBool
2894 L_TildeGeq -> sameToSameV pure cBool
2895 _ -> bug $ "Unkown operator" <+> pretty (show l)
2896 where
2897 cBool = const . const TypeBool
2898 same a b = mostDefinedS [a, b]
2899 checkIn :: OpValidator
2900 checkIn (r1, kl) (r2, kr) = do
2901 setContext r1
2902 lt <- getValueType kl
2903 setContext r2
2904 rt <- getValueType kr
2905 case innerTypeOf rt of
2906 Just t -> unifyTypes t (r1, Typed lt ())
2907 Nothing -> unless (rt == TypeAny) $ raiseTypeError (r2 <!> ComplexTypeError (T.pack . show $ "container of" <+> pretty lt) rt)
2908 return TypeBool
2909
2910 number :: Type -> ValidatorS Type
2911 number t = case t of
2912 TypeInt TagInt -> return t
2913 TypeInt TagEnum {} -> return t
2914 TypeAny -> return t
2915 _ -> TypeAny <$ contextTypeError (ComplexTypeError "number or enum" t)
2916 minusArgs t = case t of
2917 TypeInt TagInt -> return t
2918 TypeSet _ -> return t
2919 TypeMSet _ -> return t
2920 TypeRelation _ -> return t
2921 TypeFunction _ _ -> return t
2922 _ -> TypeAny <$ contextTypeError (ComplexTypeError "number, set, mset, relation or function" t)
2923 orderable t = case t of
2924 TypeInt TagInt -> return t
2925 TypeInt TagEnum {} -> return t
2926 TypeBool -> return t
2927 TypeAny -> return t
2928 _ -> TypeAny <$ contextTypeError (ComplexTypeError "number, enum or Boolean" t)
2929 justSequence t = case t of
2930 TypeAny -> return t
2931 TypeSequence _ -> return t
2932 _ -> TypeAny <$ contextTypeError (TypeError (TypeSequence TypeAny) t)
2933 bools t = case t of
2934 TypeAny -> return t
2935 TypeBool -> return t
2936 _ -> TypeAny <$ contextTypeError (TypeError TypeBool t)
2937 setLike t = case t of
2938 TypeAny -> return t
2939 TypeMSet _ -> return t
2940 TypeSet _ -> return t
2941 TypeFunction _ _ -> return t
2942 TypeRelation _ -> return t
2943 _ -> TypeAny <$ contextTypeError (ComplexTypeError "set, mset, function or relation" t)