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_applySymmetriesEager -> biFunc permutationOrderDelayedArgs permutationOrderDelayedTypes
2227 L_applySymmetriesDelayed -> biFunc permutationOrderDelayedArgs permutationOrderDelayedTypes
2228 L_permutationOrderEager -> biFunc permutationOrderDelayedArgs permutationOrderDelayedTypes
2229 L_permutationOrderDelayed -> biFunc permutationOrderDelayedArgs permutationOrderDelayedTypes
2230 L_dontCare -> unFunc anyType (const $ pure TypeBool)
2231 L_toSet -> unFuncV toSetArgs typeToSet
2232 L_toMSet -> unFuncV toMSetArgs typeToMSet
2233 L_toRelation -> unFuncV func typeToRelation
2234 L_max -> unFunc minMaxArgs minMaxType
2235 L_min -> unFunc minMaxArgs minMaxType
2236 L_image -> biFuncV imageArgs (const . funcRange)
2237 L_transform -> biFuncV transformArgs (const id)
2238 L_imageSet -> biFuncV imSetArgs (\a -> const $ TypeSet <$> funcRange a)
2239 L_compose -> biFuncV composeArgs (const . funcRange)
2240 L_preImage -> biFuncV preImageArgs (\a -> const $ TypeSet <$> funcDomain a)
2241 L_inverse -> biFuncV inverseArgs (const2 TypeBool)
2242 L_freq -> biFuncV freqArgs (const2 tInt)
2243 L_hist -> unFuncV histArgs histType
2244 L_parts -> unFuncV part partsType
2245 L_together -> biFuncV setPartArgs (const2 TypeBool)
2246 L_apart -> biFuncV setPartArgs (const2 TypeBool)
2247 L_party -> biFuncV partyArgs partyType
2248 L_permInverse -> unFuncV permInverseArgs id
2249 L_participants -> unFuncV part partInner
2250 L_active -> biFuncV activeArgs (const2 TypeBool)
2251 L_pred -> unFuncV enumerable enumerableType
2252 L_succ -> unFuncV enumerable enumerableType
2253 L_factorial -> unFuncV (only tInt) (const $ pure tInt)
2254 L_powerSet -> unFuncV set powerSetType
2255 L_concatenate -> unFuncV concatArgs concatType
2256 L_flatten -> \b a -> case a of
2257 [] -> unFuncV unaryFlattenArgs (flattenType Nothing) b a
2258 [_] -> unFuncV unaryFlattenArgs (flattenType Nothing) b a
2259 _ -> biFunc (valueOnly2 binaryFlattenArgs) (\v t -> flattenType (getNum v) (typeOnly t)) b a
2260 _ -> bug $ pretty $ "Unkown functional operator " ++ show l
2261 where
2262 valueOnly :: (SArg -> Validator a) -> Arg -> Validator a
2263 valueOnly f (r, (k, e)) = do
2264 t <- getValueType k
2265 f (r, Typed t e)
2266
2267 valueOnly2 :: (SArg -> SArg -> Validator a) -> Arg -> Arg -> Validator a
2268 valueOnly2 f (r1, (k1, e1)) (r2, (k2, e2)) = do
2269 t1 <- getValueType k1
2270 t2 <- getValueType k2
2271 f (r1, Typed t1 e1) (r2, Typed t2 e2)
2272
2273 typeOnly :: Maybe (Kind, Expression) -> Maybe Type
2274 typeOnly (Just (Kind ValueType {} t, _)) = Just t
2275 typeOnly _ = Nothing
2276
2277 unFuncV ::
2278 (SArg -> Validator a0) ->
2279 (Maybe Type -> Maybe Type) ->
2280 ([Expression] -> Expression) ->
2281 [Arg] ->
2282 ValidatorS (Typed Expression)
2283 unFuncV a t = unFunc (valueOnly a) (t . typeOnly)
2284
2285 biFuncV :: (SArg -> SArg -> Validator ()) -> (Maybe Type -> Maybe Type -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2286 biFuncV a t = biFunc (valueOnly2 a) (\t1 t2 -> t (typeOnly t1) (typeOnly t2))
2287
2288 valid = return $ pure ()
2289
2290 const2 = const . const . pure
2291
2292 const3 = const . const . const . pure
2293
2294 getNum :: Maybe (Kind, Expression) -> Maybe Int
2295 getNum (Just (_, x)) = case intOut "" x of
2296 Nothing -> Nothing
2297 Just n -> pure $ fromInteger n
2298 getNum _ = Nothing
2299
2300 each3 f a b c = f a >> f b >> f c
2301
2302 anyType = const . return $ Just ()
2303
2304 indep :: (SArg -> Validator ()) -> (SArg -> Validator ()) -> (SArg -> SArg -> Validator ())
2305 indep f1 f2 a b = do
2306 v1 <- f1 a
2307 v2 <- f2 b
2308 if not . null $ catMaybes [v1, v2] then return $ pure () else return Nothing
2309
2310 binaryFlattenArgs :: SArg -> SArg -> Validator ()
2311 binaryFlattenArgs (r1, d) b = do
2312 off <- case intOut "" (untype d) of
2313 Just (fromInteger -> a :: Integer) | a > 0 -> return $ Just a
2314 _ -> invalid $ r1 <!> CustomError "1st arg must be a constant positive int"
2315 let ref = map (const TypeList) [0 .. fromMaybe 1 off]
2316 let ref' = foldr id TypeAny ref
2317 r <- unifyTypesFailing ref' b
2318 return $ if null off || null r then Nothing else Just ()
2319
2320 unaryFlattenArgs :: SArg -> Validator ()
2321 unaryFlattenArgs (_, typeOf_ -> (TypeMatrix _ _)) = valid
2322 unaryFlattenArgs (_, typeOf_ -> (TypeList _)) = valid
2323 unaryFlattenArgs (_, typeOf_ -> TypeAny) = valid
2324 unaryFlattenArgs (r, typeOf_ -> t) = invalid $ r <!> ComplexTypeError "List or Matrix " t
2325
2326 concatType :: Maybe Type -> Maybe Type
2327 concatType (Just (TypeMatrix _ (TypeList t))) = Just $ TypeList t
2328 concatType (Just (TypeMatrix _ (TypeMatrix _ t))) = Just $ TypeList t
2329 concatType (Just (TypeList (TypeList t))) = Just $ TypeList t
2330 concatType (Just (TypeList (TypeMatrix _ t))) = Just $ TypeList t
2331 concatType _ = Just $ TypeList TypeAny
2332 concatArgs :: SArg -> Validator ()
2333 concatArgs s@(r, _) = binaryFlattenArgs (r, Typed tInt $ Constant $ ConstantInt TagInt 1) s
2334
2335 tableArgs :: SArg -> SArg -> Validator ()
2336 tableArgs (r1, typeOf_ -> t1) (r2, typeOf_ -> t2) = do
2337 a <- case t1 of
2338 t | isValidInner t -> valid
2339 _ -> invalid $ r1 <!> ComplexTypeError "Matrix of Int/Enum" t1
2340 b <- case t2 of
2341 TypeAny -> valid
2342 TypeList t | isValidInner t -> valid
2343 TypeMatrix _ t | isValidInner t -> valid
2344 _ -> invalid $ r2 <!> ComplexTypeError "Matrix of Matrix of Int/Enum" t2
2345
2346 return $ if null a || null b then Nothing else Just ()
2347 where
2348 isValidInner t = case t of
2349 TypeAny -> True
2350 TypeList TypeInt {} -> True
2351 TypeList TypeAny -> True
2352 TypeMatrix _ TypeInt {} -> True
2353 TypeMatrix _ TypeAny -> True
2354 _ -> False
2355
2356 elementIdArgs :: SArg -> SArg -> Validator ()
2357 elementIdArgs (r1, typeOf_ -> t1) (r2, typeOf_ -> t2) = do
2358 let ?typeCheckerMode = RelaxedIntegerTags
2359 a <- case t1 of
2360 TypeAny -> valid
2361 TypeMatrix _ _ -> valid
2362 TypeList _ -> valid
2363 _ -> invalid $ r1 <!> ComplexTypeError "Matrix or List" t1
2364 b <- case (t1, t2) of
2365 (TypeMatrix _indexType _, TypeAny) -> valid
2366 (TypeMatrix indexType _, actualIndex) | typesUnify [indexType, actualIndex] -> valid
2367 (TypeList _, TypeAny) -> valid
2368 (TypeList _, TypeInt {}) -> valid
2369 (TypeAny, _) -> valid
2370 _ -> invalid $ r2 <!> ComplexTypeError "Appropriate index type" t2
2371
2372 return $ if null a || null b then Nothing else Just ()
2373
2374 toMSetArgs :: SArg -> Validator ()
2375 toMSetArgs (r, typeOf_ -> a) = case a of
2376 TypeAny -> return $ pure ()
2377 TypeList _ -> return $ pure ()
2378 TypeMatrix {} -> return $ pure ()
2379 TypeMSet {} -> return $ pure ()
2380 TypeSet {} -> return $ pure ()
2381 TypeFunction {} -> return $ pure ()
2382 TypeRelation {} -> return $ pure ()
2383 _ -> invalid $ r <!> ComplexTypeError "Matrix ,list,function,relation,mset,set " a
2384
2385 toSetArgs :: SArg -> Validator ()
2386 toSetArgs (r, typeOf_ -> a) = case a of
2387 TypeAny -> return $ pure ()
2388 TypeList _ -> return $ pure ()
2389 TypeMatrix {} -> return $ pure ()
2390 TypeMSet {} -> return $ pure ()
2391 TypeFunction {} -> return $ pure ()
2392 TypeRelation {} -> return $ pure ()
2393 _ -> invalid $ r <!> ComplexTypeError "Matrix ,list,function,relation,mset " a
2394
2395 listOrMatrix :: SArg -> Validator ()
2396 listOrMatrix (r, typeOf_ -> a) = case a of
2397 TypeAny -> return $ pure ()
2398 TypeList _ -> return $ pure ()
2399 TypeMatrix {} -> return $ pure ()
2400 _ -> invalid $ r <!> ComplexTypeError "Matrix or list" a
2401
2402 freqArgs :: SArg -> SArg -> Validator ()
2403 freqArgs (r1, a) (r2, b) = do
2404 let tb = typeOf_ b
2405 let (rt, ti) = case typeOf_ a of
2406 TypeMatrix idx ms -> (TypeMatrix idx md, md) where md = mostDefinedS [tb, ms]
2407 TypeMSet ms -> (TypeMSet md, md) where md = mostDefinedS [tb, ms]
2408 _ -> (TypeMatrix tInt tb, tb)
2409 a' <- unifyTypesFailing rt (r1, a)
2410 b' <- unifyTypesFailing ti (r2, b)
2411 return $ if null a' || null b' then Nothing else Just ()
2412
2413 unifies :: SArg -> SArg -> Validator ()
2414 unifies a b = do
2415 let md = mostDefinedS $ map (typeOf_ . unregion) [a, b]
2416 a' <- unifyTypesFailing md a
2417 b' <- unifyTypesFailing md b
2418 return $ if null a' || null b' then Nothing else Just ()
2419
2420 func :: SArg -> Validator ()
2421 func (_, Typed (TypeFunction _ _) _) = valid
2422 func (_, Typed TypeAny _) = valid
2423 func (r, Typed t _) = invalid $ r <!> TypeError (TypeFunction TypeAny TypeAny) t
2424
2425 set :: SArg -> Validator Type
2426 set (_, Typed (TypeSet t) _) = return $ pure t
2427 set (_, Typed TypeAny _) = return $ pure TypeAny
2428 set (r, Typed t _) = invalid $ r <!> TypeError (TypeSet TypeAny) t
2429
2430 powerSetType (Just ((TypeSet i))) = Just $ TypeSet (TypeSet i)
2431 powerSetType _ = Just $ TypeSet $ TypeSet TypeAny
2432
2433 only t (r, typeOf_ -> t') = do
2434 setContext r
2435 if t' == TypeAny || t == t'
2436 then return $ Just t
2437 else invalid $ r <!> TypeError t t'
2438
2439 listInt (r, typeOf_ -> t') = case t' of
2440 TypeAny -> return $ Just t'
2441 TypeList TypeInt {} -> return $ Just t'
2442 TypeMatrix _ TypeInt {} -> return $ Just t'
2443 _ -> invalid $ r <!> ComplexTypeError "Matrix or list of int or enum" t'
2444
2445 partInner :: Maybe Type -> Maybe Type
2446 partInner (Just (TypePartition a)) = Just $ TypeSet a
2447 partInner _ = Just $ TypeSet TypeAny
2448
2449 restrictArgs :: Arg -> Arg -> Validator ()
2450 restrictArgs (r1, (k, _)) (r2, (kd, _)) = do
2451 setContext r1
2452 funcType <- getValueType k
2453 setContext r2
2454 domType <- getDomainType kd
2455 unifyTypesFailing (TypeFunction domType TypeAny) (r1, Typed funcType ())
2456
2457 restrictTypes :: Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type
2458 restrictTypes (fmap fst -> kv) (fmap fst -> kd) = Just $ TypeFunction from to
2459 where
2460 dType = case kd of
2461 Just (Kind DomainType t) -> getDomainMembers t
2462 _ -> TypeAny
2463 from = case kv of
2464 Just (Kind ValueType {} (TypeFunction fr _)) | typesUnifyS [dType, fr] -> mostDefinedS [dType, fr]
2465 Just (Kind ValueType {} (TypeFunction fr _)) -> fr
2466 _ -> mostDefinedS [TypeAny, dType]
2467 to = case kv of
2468 Just (Kind ValueType {} (TypeFunction _ to')) -> to'
2469 _ -> TypeAny
2470
2471 -- TODO: validate
2472 permutationOrderDelayedArgs :: Arg -> Arg -> Validator ()
2473 permutationOrderDelayedArgs _ _ = return (pure ())
2474
2475 -- TODO
2476 permInverseArgs :: SArg -> Validator ()
2477 permInverseArgs _ = return (pure ())
2478
2479 -- TODO
2480 permutationOrderDelayedTypes :: Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type
2481 permutationOrderDelayedTypes _ _ = Just TypeBool
2482
2483 imSetArgs :: SArg -> SArg -> Validator ()
2484 imSetArgs (r1, a) (r2, b) = do
2485 let t = case (typeOf_ a, typeOf_ b) of
2486 (TypeFunction i _, tb) -> mostDefinedS [i, tb]
2487 (TypeSequence _, _) -> tInt
2488 (_, tb) -> tb
2489 a' <- unifyTypesFailing (TypeFunction t TypeAny) (r1, a)
2490 b' <- unifyTypesFailing t (r2, b)
2491 return $ if null a' || null b' then Nothing else Just ()
2492
2493 preImageArgs :: SArg -> SArg -> Validator ()
2494 preImageArgs _ _ = return $ Just ()
2495 -- preImageArgs (r1, a) (r2, b) = do
2496 -- let t = case (typeOf_ a, typeOf_ b) of
2497 -- (TypeFunction _ i, tb) -> mostDefinedS [i, tb]
2498 -- (TypeSequence i, _) -> i
2499 -- (_, tb) -> tb
2500 -- a' <- unifyTypesFailing (TypeFunction TypeAny t) (r1, a)
2501 -- b' <- unifyTypesFailing t (r2, b)
2502 -- return $ if null a' || null b' then Nothing else Just ()
2503
2504 partyArgs :: SArg -> SArg -> Validator ()
2505 partyArgs (r1, a) (r2, b) = do
2506 let t = case (typeOf_ a, typeOf_ b) of
2507 (ta, TypePartition tb) -> mostDefinedS [ta, tb]
2508 (ta, _) -> ta
2509 a' <- unifyTypesFailing t (r1, a)
2510 b' <- unifyTypesFailing (TypePartition t) (r2, b)
2511 return $ if null a' || null b' then Nothing else Just ()
2512
2513 inverseArgs :: SArg -> SArg -> Validator ()
2514 inverseArgs (_r1, a) (_r2, b) =
2515 case (typeOf_ a, typeOf_ b) of
2516 (TypeFunction {}, TypeFunction {}) -> return (Just ())
2517 (TypeFunction {}, _) -> return (Just ())
2518 (_, TypeFunction {}) -> return (Just ())
2519 (TypePermutation {}, TypePermutation {}) -> return (Just ())
2520 (TypePermutation {}, _) -> return (Just ())
2521 (_, TypePermutation {}) -> return (Just ())
2522 _ -> return Nothing
2523
2524 setPartArgs :: SArg -> SArg -> Validator ()
2525 setPartArgs (r1, a) (r2, b) = do
2526 let t = case (typeOf_ a, typeOf_ b) of
2527 (TypeSet st, TypePartition pt) -> mostDefinedS [st, pt]
2528 (TypeSet st, _) -> st
2529 (_, TypePartition ts) -> ts
2530 _ -> TypeAny
2531 a' <- unifyTypesFailing (TypeSet t) (r1, a)
2532 b' <- unifyTypesFailing (TypePartition t) (r2, b)
2533 return $ if null a' || null b' then Nothing else Just ()
2534
2535 partyType :: Maybe Type -> Maybe Type -> Maybe Type
2536 partyType a b = do
2537 let at' = fromMaybe TypeAny a
2538 let bt = case b of
2539 Just (TypePartition t) -> t
2540 _ -> TypeAny
2541 return $ TypeSet $ mostDefinedS [at', bt]
2542
2543 partsType :: Maybe Type -> Maybe Type
2544 partsType (Just (TypePartition a)) = Just $ TypeSet $ TypeSet a
2545 partsType (Just TypeAny) = Just $ TypeSet $ TypeSet TypeAny
2546 partsType _ = Nothing
2547
2548 minMaxArgs :: Arg -> Validator ()
2549 minMaxArgs (r, (Kind DomainType t, _)) =
2550 case t of
2551 TypeInt TagInt -> valid
2552 TypeInt (TagEnum _) -> valid
2553 TypeEnum {} -> valid
2554 TypeAny -> valid
2555 _ -> invalid $ r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t
2556 minMaxArgs (r, (k, _)) = do
2557 t <- getValueType k
2558 inner <- case t of
2559 TypeList tyInner -> return tyInner
2560 TypeMatrix _ tyInner -> return tyInner
2561 TypeSet tyInner -> return tyInner
2562 TypeMSet tyInner -> return tyInner
2563 TypeAny -> return TypeAny
2564 _ -> TypeAny <$ invalid (r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t)
2565 case inner of
2566 TypeInt TagInt -> valid
2567 TypeInt (TagEnum _) -> valid
2568 TypeEnum {} -> valid
2569 TypeAny -> valid
2570 _ -> invalid $ r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t
2571
2572 minMaxType :: Maybe (Kind, a) -> Maybe Type
2573 minMaxType (Just (Kind DomainType t@(TypeInt {}), _)) = Just t
2574 minMaxType (Just (Kind DomainType (TypeEnum (Name nm)), _)) = Just . TypeInt $ TagEnum nm
2575 minMaxType (Just (Kind ValueType {} (TypeMatrix _ a), _)) = minMaxType (Just (Kind DomainType a, ()))
2576 minMaxType (Just (Kind ValueType {} (TypeList a), _)) = minMaxType (Just (Kind DomainType a, ()))
2577 minMaxType (Just (Kind ValueType {} (TypeSet a), _)) = minMaxType (Just (Kind DomainType a, ()))
2578 minMaxType (Just (Kind ValueType {} (TypeMSet a), _)) = minMaxType (Just (Kind DomainType a, ()))
2579 minMaxType _ = Just TypeAny
2580
2581 transformArgs :: SArg -> SArg -> Validator ()
2582 transformArgs _ _ = return $ pure ()
2583 activeArgs :: SArg -> SArg -> Validator ()
2584 activeArgs (_, typeOf_ -> TypeAny) _ = valid
2585 activeArgs (r, typeOf_ -> t@(TypeVariant _)) (r2, typeOf_ -> b) = checkRVMember (r, t) (r2, b)
2586 activeArgs (r, typeOf_ -> t) _ = invalid $ r <!> ComplexTypeError "Variant " t
2587
2588 typeToSet :: Maybe Type -> Maybe Type
2589 typeToSet (Just t) = Just . TypeSet $ fromMaybe TypeAny (tMembers t)
2590 typeToSet _ = Just $ TypeSet TypeAny
2591
2592 typeToMSet :: Maybe Type -> Maybe Type
2593 typeToMSet (Just t) = Just . TypeMSet $ fromMaybe TypeAny (tMembers t)
2594 typeToMSet _ = Just $ TypeMSet TypeAny
2595
2596 typeToRelation :: Maybe Type -> Maybe Type
2597 typeToRelation (Just (TypeFunction i j)) = Just $ TypeRelation [i, j]
2598 typeToRelation (Just TypeAny) = Just $ TypeRelation [TypeAny, TypeAny]
2599 typeToRelation _ = Nothing
2600 tMembers t = case t of
2601 TypeAny -> Just TypeAny
2602 TypeList ty -> Just ty
2603 TypeMatrix _ i -> Just i
2604 TypeSet ty -> Just ty
2605 TypeMSet ty -> Just ty
2606 TypeFunction i j -> Just $ TypeTuple [i, j]
2607 TypeRelation tys -> Just $ TypeTuple tys
2608 _ -> Nothing
2609
2610 imageArgs :: SArg -> SArg -> Validator ()
2611 imageArgs (r1, typeOf_ -> t1) r2 = do
2612 from <- case t1 of
2613 TypeAny -> return $ Just TypeAny
2614 TypeFunction a _ -> return $ Just a
2615 TypeSequence _ -> return $ Just tInt
2616 TypePermutation a -> return $ Just a
2617 _ -> Nothing <$ raiseTypeError (r1 <!> ComplexTypeError "function, sequence or permutation" t1)
2618 case from of
2619 Just f -> unifyTypes f r2 >> return (pure ())
2620 Nothing -> return Nothing
2621
2622 -- TODO: validate
2623 composeArgs :: SArg -> SArg -> Validator ()
2624 composeArgs _ _ = return (pure ())
2625
2626 sumArgs :: SArg -> Validator ()
2627 sumArgs (r, typeOf_ -> t') = do
2628 t <- case t' of
2629 TypeAny -> return TypeAny
2630 TypeList t -> return t
2631 TypeMatrix _ t -> return t
2632 TypeSet t -> return t
2633 TypeMSet t -> return t
2634 _ -> TypeAny <$ raiseTypeError (r <!> ComplexTypeError "matrix or set" t')
2635 case t of
2636 TypeAny -> return $ pure ()
2637 TypeInt TagInt -> return $ pure ()
2638 _ -> Nothing <$ raiseTypeError (r <!> ComplexTypeError "integer elements" t)
2639
2640 funcSeq :: SArg -> Validator ()
2641 funcSeq (r, typeOf_ -> t') = case t' of
2642 TypeAny -> return $ pure ()
2643 TypeSequence _ -> return $ pure ()
2644 TypePermutation _ -> return $ pure ()
2645 TypeFunction _ _ -> return $ pure ()
2646 _ -> invalid $ r <!> ComplexTypeError "function, sequence or permutation" t'
2647
2648 funcDomain :: Maybe Type -> Maybe Type
2649 funcDomain (Just (TypeFunction a _)) = Just a
2650 funcDomain (Just (TypeSequence _)) = Just tInt
2651 funcDomain _ = Just TypeAny
2652
2653 funcRange :: Maybe Type -> Maybe Type
2654 funcRange (Just (TypeFunction _ b)) = Just b
2655 funcRange (Just ((TypeSequence b))) = Just b
2656 funcRange _ = Just TypeAny
2657
2658 elementIdType :: Maybe Type -> Maybe Type -> Maybe Type
2659 elementIdType (Just (TypeMatrix _ innerType)) _ = Just innerType
2660 elementIdType (Just (TypeList innerType)) _ = Just innerType
2661 elementIdType _ _ = Just TypeAny
2662
2663 part :: SArg -> Validator ()
2664 part (r, typeOf_ -> t) = case t of
2665 TypeAny -> valid
2666 TypePartition _ -> return $ pure ()
2667 _ -> invalid $ r <!> TypeError (TypePartition TypeAny) t
2668
2669 histArgs :: SArg -> Validator ()
2670 histArgs (r, typeOf_ -> a) = case a of
2671 TypeMSet _ -> return $ pure ()
2672 TypeList _ -> return $ pure ()
2673 TypeMatrix _ _ -> return $ pure ()
2674 TypeAny -> return $ pure ()
2675 _ -> invalid $ r <!> ComplexTypeError "matrix, list or mset" a
2676
2677 histType :: Maybe Type -> Maybe Type
2678 histType (Just ((TypeMSet a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2679 histType (Just ((TypeMatrix _ a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2680 histType (Just ((TypeList a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2681 histType _ = Just $ TypeMatrix tInt $ TypeTuple [TypeAny, tInt]
2682
2683 enumerable :: SArg -> Validator ()
2684 enumerable (r, typeOf_ -> t) = case t of
2685 TypeAny -> return $ pure ()
2686 TypeInt TagUnnamed {} -> invalid $ r <!> CustomError "Anonymous enums are not explictly enumerable"
2687 TypeInt _ -> return $ pure ()
2688 TypeEnum {} -> return $ pure ()
2689 TypeBool -> return $ pure ()
2690 _ -> invalid $ r <!> ComplexTypeError "int, enum or bool" t
2691
2692 enumerableType :: Maybe Type -> Maybe Type
2693 enumerableType (Just t@(TypeInt TagInt)) = Just t
2694 enumerableType (Just t@(TypeInt (TagEnum _))) = Just t
2695 enumerableType (Just t@(TypeEnum {})) = Just t
2696 enumerableType _ = Nothing
2697
2698 flattenType :: Maybe Int -> Maybe Type -> Maybe Type
2699 flattenType (Just n) (Just a) | n < 0 = Just $ TypeList a
2700 flattenType (Just n) (Just (TypeList m)) = flattenType (Just (n - 1)) (Just m)
2701 flattenType (Just n) (Just (TypeMatrix _ m)) = flattenType (Just (n - 1)) (Just m)
2702 flattenType Nothing (Just (TypeMatrix _ m)) = flattenType Nothing (Just m)
2703 flattenType Nothing (Just (TypeList m)) = flattenType Nothing (Just m)
2704 flattenType Nothing (Just t) = Just $ TypeList t
2705 flattenType _ _ = Just $ TypeList TypeAny
2706
2707 validateFuncOp :: Lexeme -> [RegionTagged (Kind, Expression)] -> ValidatorS (Typed Expression)
2708 validateFuncOp l args = do
2709 let b = funcOpBuilder l
2710 b args
2711
2712 -- case argCheck of
2713 -- Nothing -> return $ Typed (r []) $ fallback "arg fail"
2714 -- Just tys -> return $ Typed (r tys)(b $ map untype tys)
2715
2716 isOfType :: Type -> RegionTagged (Typed Expression) -> ValidatorS Bool
2717 isOfType t (r, v) = setContext r >> return v ?=> exactly t >> return (typesUnifyS [t, typeOf_ v])
2718
2719 isLogicalContainer :: RegionTagged (Typed Expression) -> Validator ()
2720 isLogicalContainer (r, Typed t _) = case t of
2721 TypeAny -> return $ pure ()
2722 TypeList TypeAny -> return $ pure ()
2723 TypeList TypeBool -> return $ pure ()
2724 TypeMatrix _ TypeAny -> return $ pure ()
2725 TypeMatrix _ TypeBool -> return $ pure ()
2726 TypeSet TypeAny -> return $ pure ()
2727 TypeMSet TypeBool -> return $ pure ()
2728 _ -> invalid $ r <!> ComplexTypeError "Collection of Booleans" t
2729
2730 -- validateArgList :: [RegionTagged (Typed Expression) -> ValidatorS Bool] -> [RegionTagged (Typed Expression)] -> Validator [Typed Expression]
2731 -- validateArgList ps args | length args < length ps = do invalid $ args <!> MissingArgsError (length ps)
2732 -- validateArgList ps args = do
2733 -- let ps' = ps ++ repeat argOverflow
2734 -- xs <- zipWithM id ps' args
2735 -- return (if and xs then Just $ map unregion args else Nothing)
2736
2737 -- argOverflow :: RegionTagged a -> ValidatorS Bool
2738 -- argOverflow (region,_) = do
2739 -- setContext region
2740 -- void . contextError $ CustomError "Extra Args"
2741 -- return False
2742 type SArg = RegionTagged (Typed Expression)
2743
2744 type Arg = RegionTagged (Kind, Expression)
2745
2746 unFunc ::
2747 (Arg -> Validator a) -> -- Arg validator
2748 (Maybe (Kind, Expression) -> Maybe Type) -> -- typeEvaluator
2749 ([Expression] -> Expression) -> -- mkOp or similar
2750 [Arg] ->
2751 ValidatorS (Typed Expression)
2752 unFunc argVal t f args = do
2753 (v, ts) <- case args of
2754 [] -> tooFewArgs 1 0 >> return (Nothing, Nothing)
2755 [x] -> do
2756 r <- argVal x
2757 tc <- gets typeChecking
2758 let result = case r of
2759 Nothing | tc -> Nothing
2760 _ -> Just [(snd . unregion) x]
2761 return (result, Just $ unregion x)
2762 (x : rs) -> do
2763 tooManyArgs rs
2764 r <- argVal x
2765 let result = case r of
2766 Nothing -> Nothing
2767 Just _ -> Just [(snd . unregion) x]
2768 return (result, Just $ unregion x)
2769 let res = maybe (fallback "Arg Fail Unfunc") f v
2770 return $ Typed (fromMaybe TypeAny $ t ts) res
2771
2772 biFunc :: (Arg -> Arg -> Validator a) -> (Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2773 biFunc argVal t f args = do
2774 (v, ts) <- case args of
2775 [] -> tooFewArgs 2 0 >> return (Nothing, (Nothing, Nothing))
2776 [x] -> tooFewArgs 2 1 >> return (Nothing, (Just $ unregion x, Nothing))
2777 [x, y] -> do
2778 r <- argVal x y
2779 tc <- gets typeChecking
2780 let result = case r of
2781 Nothing | tc -> Nothing
2782 _ -> Just $ map (snd . unregion) [x, y]
2783 return (result, (Just (unregion x), Just (unregion y)))
2784 (x : y : rs) -> do
2785 tooManyArgs rs
2786 r <- argVal x y
2787 let result = case r of
2788 Nothing -> Nothing
2789 Just _ -> Just $ map (snd . unregion) [x, y]
2790 return (result, (Just (unregion x), Just (unregion y)))
2791 let res = maybe (fallback "Arg Fail BiFunct") f v
2792 return $ Typed (fromMaybe TypeAny $ uncurry t ts) res
2793
2794 triFunc :: (Arg -> Arg -> Arg -> Validator a) -> (Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2795 triFunc argVal t f args = do
2796 (v, ts) <- case args of
2797 [] -> tooFewArgs 3 0 >> return (Nothing, (Nothing, Nothing, Nothing))
2798 [x] -> tooFewArgs 3 1 >> return (Nothing, (Just $ unregion x, Nothing, Nothing))
2799 [x, y] -> tooFewArgs 3 2 >> return (Nothing, (Just $ unregion x, Just $ unregion y, Nothing))
2800 [x, y, z] -> do
2801 r <- argVal x y z
2802 tc <- gets typeChecking
2803 let result = case r of
2804 Nothing | tc -> Nothing
2805 _ -> Just $ map (snd . unregion) [x, y, z]
2806 return (result, (Just (unregion x), Just (unregion y), Just (unregion z)))
2807 (x : y : z : rs) -> do
2808 tooManyArgs rs
2809 r <- argVal x y z
2810 let result = case r of
2811 Nothing -> Nothing
2812 Just _ -> Just $ map (snd . unregion) [x, y, z]
2813 return (result, (Just (unregion x), Just (unregion y), Just (unregion z)))
2814 let res = maybe (fallback "Arg Fail Tri") f v
2815 return $ Typed (fromMaybe TypeAny $ uncurry3 t ts) res
2816 where
2817 uncurry3 fn (a, b, c) = fn a b c -- todo export from prelude
2818
2819 tooFewArgs :: Int -> Int -> ValidatorS ()
2820 tooFewArgs n i = void . contextError $ MissingArgsError n i
2821
2822 tooManyArgs :: [RegionTagged a] -> ValidatorS ()
2823 tooManyArgs = mapM_ (\x -> raiseError $ x <!> UnexpectedArg)
2824
2825 checkRVMember :: RegionTagged Type -> RegionTagged Type -> Validator ()
2826 checkRVMember (_, TypeRecord ts) (_, TypeRecordMember nm _) | not . null $ lookup nm ts = return $ pure ()
2827 checkRVMember (_, TypeRecord ts) (r2, r) = do
2828 raiseTypeError $ r2 <!> TypeError (TypeRecordMember (Name "") ts) r
2829 return Nothing
2830 checkRVMember (_, TypeVariant ts) (_, TypeVariantMember nm _) | not . null $ lookup nm ts = return $ pure ()
2831 checkRVMember (_, TypeVariant ts) (r2, r) = do
2832 raiseTypeError $ r2 <!> TypeError (TypeVariantMember (Name "") ts) r
2833 return Nothing
2834 checkRVMember (r1, t) _ = do
2835 raiseTypeError $ r1 <!> TypeError (TypeVariant []) t
2836 return Nothing
2837
2838 type OpValidator = RegionTagged Kind -> RegionTagged Kind -> ValidatorS Type
2839
2840 type OpTyper = Kind -> Kind -> Type
2841
2842 sameToSameV :: (Type -> ValidatorS Type) -> (Type -> Type -> Type) -> OpValidator
2843 sameToSameV tc t (rl, kl) (rr, kr) = do
2844 setContext rl
2845 lt <- getValueType kl
2846 lt' <- tc lt
2847 setContext rr
2848 rt <- getValueType kr
2849 rt' <- tc rt
2850 let md = mostDefinedS [lt, rt]
2851 _ <- unifyTypesFailing md (rl, Typed lt' ())
2852 _ <- unifyTypesFailing md (rr, Typed rt' ())
2853 return $ t lt' rt'
2854
2855 binOpType :: Lexeme -> OpValidator
2856 binOpType l = case l of
2857 L_Plus -> sameToSameV number same
2858 L_Minus -> sameToSameV minusArgs same
2859 L_Times -> sameToSameV number same
2860 L_Div -> sameToSameV number same
2861 L_Mod -> sameToSameV number same
2862 L_Pow -> sameToSameV number same
2863 L_Eq -> sameToSameV pure cBool
2864 L_Neq -> sameToSameV pure cBool
2865 L_Lt -> sameToSameV orderable cBool
2866 L_Leq -> sameToSameV orderable cBool
2867 L_Gt -> sameToSameV orderable cBool
2868 L_Geq -> sameToSameV orderable cBool
2869 L_in -> checkIn
2870 L_And -> sameToSameV bools cBool
2871 L_Or -> sameToSameV bools cBool
2872 L_Imply -> sameToSameV bools cBool
2873 L_Iff -> sameToSameV bools cBool -- b b b
2874 L_subset -> sameToSameV setLike cBool -- set mset func rel
2875 L_subsetEq -> sameToSameV setLike cBool
2876 -- \^^^
2877 L_supset -> sameToSameV setLike cBool
2878 -- \^^^^
2879 L_supsetEq -> sameToSameV setLike cBool
2880 -- \^^
2881
2882 L_subsequence -> sameToSameV justSequence cBool -- seq - seq -bool
2883 L_substring -> sameToSameV justSequence cBool -- seq - seq -bool
2884 L_intersect -> sameToSameV setLike same
2885 L_union -> sameToSameV setLike same
2886 L_LexLt -> sameToSameV pure cBool
2887 L_LexLeq -> sameToSameV pure cBool
2888 L_LexGt -> sameToSameV pure cBool
2889 L_LexGeq -> sameToSameV pure cBool
2890 L_DotLt -> sameToSameV pure cBool
2891 L_DotLeq -> sameToSameV pure cBool
2892 L_DotGt -> sameToSameV pure cBool
2893 L_DotGeq -> sameToSameV pure cBool
2894 L_TildeLt -> sameToSameV pure cBool
2895 L_TildeLeq -> sameToSameV pure cBool
2896 L_TildeGt -> sameToSameV pure cBool
2897 L_TildeGeq -> sameToSameV pure cBool
2898 _ -> bug $ "Unkown operator" <+> pretty (show l)
2899 where
2900 cBool = const . const TypeBool
2901 same a b = mostDefinedS [a, b]
2902 checkIn :: OpValidator
2903 checkIn (r1, kl) (r2, kr) = do
2904 setContext r1
2905 lt <- getValueType kl
2906 setContext r2
2907 rt <- getValueType kr
2908 case innerTypeOf rt of
2909 Just t -> unifyTypes t (r1, Typed lt ())
2910 Nothing -> unless (rt == TypeAny) $ raiseTypeError (r2 <!> ComplexTypeError (T.pack . show $ "container of" <+> pretty lt) rt)
2911 return TypeBool
2912
2913 number :: Type -> ValidatorS Type
2914 number t = case t of
2915 TypeInt TagInt -> return t
2916 TypeInt TagEnum {} -> return t
2917 TypeAny -> return t
2918 _ -> TypeAny <$ contextTypeError (ComplexTypeError "number or enum" t)
2919 minusArgs t = case t of
2920 TypeInt TagInt -> return t
2921 TypeSet _ -> return t
2922 TypeMSet _ -> return t
2923 TypeRelation _ -> return t
2924 TypeFunction _ _ -> return t
2925 _ -> TypeAny <$ contextTypeError (ComplexTypeError "number, set, mset, relation or function" t)
2926 orderable t = case t of
2927 TypeInt TagInt -> return t
2928 TypeInt TagEnum {} -> return t
2929 TypeBool -> return t
2930 TypeAny -> return t
2931 _ -> TypeAny <$ contextTypeError (ComplexTypeError "number, enum or Boolean" t)
2932 justSequence t = case t of
2933 TypeAny -> return t
2934 TypeSequence _ -> return t
2935 _ -> TypeAny <$ contextTypeError (TypeError (TypeSequence TypeAny) t)
2936 bools t = case t of
2937 TypeAny -> return t
2938 TypeBool -> return t
2939 _ -> TypeAny <$ contextTypeError (TypeError TypeBool t)
2940 setLike t = case t of
2941 TypeAny -> return t
2942 TypeMSet _ -> return t
2943 TypeSet _ -> return t
2944 TypeFunction _ _ -> return t
2945 TypeRelation _ -> return t
2946 _ -> TypeAny <$ contextTypeError (ComplexTypeError "set, mset, function or relation" t)