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