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