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 xs =
2004 DiagnosticRegion
2005 { drSourcePos = drSourcePos . fst $ head xs,
2006 drEndPos = drEndPos . fst $ last xs,
2007 drOffset = drOffset . fst $ head xs,
2008 drLength = sum $ map (drLength . fst) xs
2009 }
2010
2011 getMemberTypes :: Type -> ValidatorS [Type]
2012 getMemberTypes t = case t of
2013 TypeAny -> return $ repeat TypeAny
2014 -- TypeUnnamed na ->
2015 TypeTuple tys -> return tys
2016 _ -> return $ repeat TypeAny
2017
2018 -- unifyAbstractPatternOverExpression :: AbstractPatternNode -> Expression -> Validator (Name,Type)
2019 -- unifyAbstractPatternOverExpression pat exp = do
2020 -- t <- typeOf exp
2021
2022 -- empty
2023
2024 getDomainMembers :: Type -> Type
2025 getDomainMembers t = case t of
2026 TypeAny -> t
2027 TypeBool -> t
2028 TypeInt it -> case it of
2029 TagInt -> t
2030 TagEnum _ -> error "Domain should use typeEnum instead"
2031 TagUnnamed _ -> error "Domain should use typeUnamed instead"
2032 TypeEnum n -> TypeInt . TagEnum $ case n of
2033 Name txt -> txt
2034 MachineName {} -> error "This should never be user specified"
2035 NameMetaVar s -> pack s
2036 TypeUnnamed n -> TypeInt . TagUnnamed $ case n of
2037 Name txt -> txt
2038 MachineName {} -> error "This should never be user specified"
2039 NameMetaVar s -> pack s
2040 TypeTuple tys -> TypeTuple $ map getDomainMembers tys
2041 TypeRecord tys -> TypeRecord $ map (second getDomainMembers) tys
2042 TypeVariant tys -> TypeVariant $ map (second getDomainMembers) tys
2043 TypeList ty -> TypeList $ getDomainMembers ty
2044 TypeMatrix ty ty' -> TypeMatrix ty $ getDomainMembers ty'
2045 TypeSet ty -> TypeSet $ getDomainMembers ty
2046 TypeMSet ty -> TypeMSet $ getDomainMembers ty
2047 TypeFunction ty ty' -> TypeFunction (getDomainMembers ty) (getDomainMembers ty')
2048 TypeSequence ty -> TypeSequence $ getDomainMembers ty
2049 TypeRelation tys -> TypeRelation $ map getDomainMembers tys
2050 TypePartition ty -> TypePartition $ getDomainMembers ty
2051 _ -> bug $ "Unknown domain type" <+> pretty t
2052
2053 getDomainFromValue :: Type -> Type
2054 getDomainFromValue t = case t of
2055 TypeAny -> t
2056 TypeBool -> t
2057 TypeInt it -> case it of
2058 TagInt -> t
2059 TagEnum n -> TypeEnum (Name n)
2060 TagUnnamed n -> TypeUnnamed (Name n)
2061 TypeEnum _ -> t
2062 TypeUnnamed _ -> t
2063 TypeTuple tys -> TypeTuple $ map getDomainFromValue tys
2064 TypeRecord tys -> TypeRecord $ map (second getDomainFromValue) tys
2065 TypeVariant tys -> TypeVariant $ map (second getDomainFromValue) tys
2066 TypeList ty -> TypeList $ getDomainFromValue ty
2067 TypeMatrix ty ty' -> TypeMatrix ty $ getDomainFromValue ty'
2068 TypeSet ty -> TypeSet $ getDomainFromValue ty
2069 TypeMSet ty -> TypeMSet $ getDomainFromValue ty
2070 TypeFunction ty ty' -> TypeFunction (getDomainFromValue ty) (getDomainFromValue ty')
2071 TypeSequence ty -> TypeSequence $ getDomainFromValue ty
2072 TypeRelation tys -> TypeRelation $ map getDomainFromValue tys
2073 TypePartition ty -> TypePartition $ getDomainFromValue ty
2074 _ -> bug $ "Unknown member type" <+> pretty t
2075
2076 data DomainTyped a = DomainTyped DomainType a
2077
2078 data DomainSize = Unkown | Infinite | Sized Int
2079
2080 data DomainType
2081 = DomainTypeBool
2082 | DomainTypeInt DomainSize
2083 | DomainTypeTuple [DomainType]
2084
2085 f2n :: (a -> ValidatorS b) -> a -> Validator b
2086 f2n f a = do
2087 q <- f a
2088 return $ Just q
2089
2090 class Fallback a where
2091 fallback :: Text -> a
2092
2093 instance Fallback (Domain () Expression) where
2094 fallback reason = DomainAny reason TypeAny
2095
2096 instance Fallback Expression where
2097 fallback reason = Reference (Name reason) Nothing
2098
2099 instance (Fallback a) => Fallback (Typed a) where
2100 fallback = Typed TypeAny . fallback
2101
2102 instance (Fallback a) => Fallback (Kind, a) where
2103 fallback msg = (Kind (ValueType CatConstant) TypeAny, fallback msg)
2104
2105 instance Fallback (Maybe a) where
2106 fallback = const Nothing
2107
2108 instance Fallback Name where
2109 fallback = Name
2110
2111 instance Fallback [a] where
2112 fallback :: Text -> [a]
2113 fallback = const []
2114
2115 instance Fallback AbstractPattern where
2116 fallback = Single . fallback
2117
2118 type FuncOpDec = Int
2119
2120 funcOpBuilder :: Lexeme -> [Arg] -> ValidatorS (Typed Expression)
2121 funcOpBuilder l = functionOps l (mkOp $ FunctionOp l)
2122
2123 -- functionOps l@L_fAnd = (validateArgList [isLogicalContainer],const TypeBool)
2124 functionOps :: Lexeme -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2125 functionOps l = case l of
2126 L_fAnd -> unFuncV isLogicalContainer (pure . const TypeBool)
2127 L_fOr -> unFuncV isLogicalContainer (pure . const TypeBool)
2128 L_fXor -> unFuncV isLogicalContainer (pure . const TypeBool)
2129 L_Sum -> unFuncV sumArgs (pure . const tInt)
2130 L_Product -> unFunc (valueOnly sumArgs) (pure . const tInt)
2131 L_true -> unFuncV anyType (pure . const TypeBool)
2132 L_toInt -> unFuncV (only TypeBool) (pure . const tInt)
2133 L_makeTable -> unFuncV (only TypeBool) (pure . const TypeBool)
2134 L_table -> biFuncV tableArgs (const2 TypeBool)
2135 L_gcc -> triFunc (each3 $ valueOnly listInt) (const3 TypeBool)
2136 L_atleast -> triFunc (each3 $ valueOnly listInt) (const3 TypeBool)
2137 L_atmost -> triFunc (each3 $ valueOnly listInt) (const3 TypeBool)
2138 L_defined -> unFuncV funcSeq (fmap TypeSet . funcDomain)
2139 L_range -> unFuncV funcSeq (fmap TypeSet . funcRange)
2140 L_restrict -> biFunc restrictArgs restrictTypes
2141 L_allDiff -> unFuncV listOrMatrix (const $ pure TypeBool)
2142 L_alldifferent_except -> biFuncV (indep listOrMatrix enumerable) (const2 TypeBool)
2143 L_catchUndef -> biFuncV unifies (\a b -> pure $ mostDefinedS $ catMaybes [a, b])
2144 L_dontCare -> unFunc anyType (const $ pure TypeBool)
2145 L_toSet -> unFuncV toSetArgs typeToSet
2146 L_toMSet -> unFuncV toMSetArgs typeToMSet
2147 L_toRelation -> unFuncV func typeToRelation
2148 L_max -> unFunc minMaxArgs minMaxType
2149 L_min -> unFunc minMaxArgs minMaxType
2150 L_image -> biFuncV imageArgs (const . funcRange)
2151 L_transform -> biFuncV transformArgs (const id)
2152 L_imageSet -> biFuncV imSetArgs (\a -> const $ TypeSet <$> funcRange a)
2153 L_preImage -> biFuncV preImageArgs (\a -> const $ TypeSet <$> funcDomain a)
2154 L_inverse -> biFuncV inverseArgs (const2 TypeBool)
2155 L_freq -> biFuncV freqArgs (const2 tInt)
2156 L_hist -> unFuncV histArgs histType
2157 L_parts -> unFuncV part partsType
2158 L_together -> biFuncV setPartArgs (const2 TypeBool)
2159 L_apart -> biFuncV setPartArgs (const2 TypeBool)
2160 L_party -> biFuncV partyArgs partyType
2161 L_participants -> unFuncV part partInner
2162 L_active -> biFuncV activeArgs (const2 TypeBool)
2163 L_pred -> unFuncV enumerable enumerableType
2164 L_succ -> unFuncV enumerable enumerableType
2165 L_factorial -> unFuncV (only tInt) (const $ pure tInt)
2166 L_powerSet -> unFuncV set powerSetType
2167 L_concatenate -> unFuncV concatArgs concatType
2168 L_flatten -> \b a -> case a of
2169 [] -> unFuncV unaryFlattenArgs (flattenType Nothing) b a
2170 [_] -> unFuncV unaryFlattenArgs (flattenType Nothing) b a
2171 _ -> biFunc (valueOnly2 binaryFlattenArgs) (\v t -> flattenType (getNum v) (typeOnly t)) b a
2172 _ -> bug $ pretty $ "Unkown functional operator " ++ show l
2173 where
2174 valueOnly :: (SArg -> Validator a) -> Arg -> Validator a
2175 valueOnly f (r, (k, e)) = do
2176 t <- getValueType k
2177 f (r, Typed t e)
2178 valueOnly2 :: (SArg -> SArg -> Validator a) -> Arg -> Arg -> Validator a
2179 valueOnly2 f (r1, (k1, e1)) (r2, (k2, e2)) = do
2180 t1 <- getValueType k1
2181 t2 <- getValueType k2
2182 f (r1, Typed t1 e1) (r2, Typed t2 e2)
2183 typeOnly :: Maybe (Kind, Expression) -> Maybe Type
2184 typeOnly (Just (Kind ValueType {} t, _)) = Just t
2185 typeOnly _ = Nothing
2186 unFuncV a t = unFunc (valueOnly a) (t . typeOnly)
2187 biFuncV :: (SArg -> SArg -> Validator ()) -> (Maybe Type -> Maybe Type -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2188 biFuncV a t = biFunc (valueOnly2 a) (\t1 t2 -> t (typeOnly t1) (typeOnly t2))
2189 valid = return $ pure ()
2190 const2 = const . const . pure
2191 const3 = const . const . const . pure
2192 getNum :: Maybe (Kind, Expression) -> Maybe Int
2193 getNum (Just (_, x)) = case intOut "" x of
2194 Nothing -> Nothing
2195 Just n -> pure $ fromInteger n
2196 getNum _ = Nothing
2197 each3 f a b c = f a >> f b >> f c
2198 anyType = const . return $ Just ()
2199
2200 indep :: (SArg -> Validator ()) -> (SArg -> Validator ()) -> (SArg -> SArg -> Validator ())
2201 indep f1 f2 a b = do
2202 v1 <- f1 a
2203 v2 <- f2 b
2204 if not . null $ catMaybes [v1, v2] then return $ pure () else return Nothing
2205 binaryFlattenArgs :: SArg -> SArg -> Validator ()
2206 binaryFlattenArgs (r1, d) b = do
2207 off <- case intOut "" (untype d) of
2208 Just (fromInteger -> a :: Integer) | a > 0 -> return $ Just a
2209 _ -> invalid $ r1 <!> CustomError "1st arg must be a constant positive int"
2210 let ref = map (const TypeList) [0 .. fromMaybe 1 off]
2211 let ref' = foldr id TypeAny ref
2212 r <- unifyTypesFailing ref' b
2213 return $ if null off || null r then Nothing else Just ()
2214 unaryFlattenArgs :: SArg -> Validator ()
2215 unaryFlattenArgs (_, typeOf_ -> (TypeMatrix _ _)) = valid
2216 unaryFlattenArgs (_, typeOf_ -> (TypeList _)) = valid
2217 unaryFlattenArgs (_, typeOf_ -> TypeAny) = valid
2218 unaryFlattenArgs (r, typeOf_ -> t) = invalid $ r <!> ComplexTypeError "List or Matrix " t
2219
2220 concatType :: Maybe Type -> Maybe Type
2221 concatType (Just (TypeMatrix _ (TypeList t))) = Just $ TypeList t
2222 concatType (Just (TypeMatrix _ (TypeMatrix _ t))) = Just $ TypeList t
2223 concatType (Just (TypeList (TypeList t))) = Just $ TypeList t
2224 concatType (Just (TypeList (TypeMatrix _ t))) = Just $ TypeList t
2225 concatType _ = Just $ TypeList TypeAny
2226 concatArgs :: SArg -> Validator ()
2227 concatArgs s@(r, _) = binaryFlattenArgs (r, Typed tInt $ Constant $ ConstantInt TagInt 1) s
2228 tableArgs :: SArg -> SArg -> Validator ()
2229 tableArgs (r1, typeOf_ -> t1) (r2, typeOf_ -> t2) = do
2230 a <- case t1 of
2231 t | isValidInner t -> valid
2232 _ -> invalid $ r1 <!> ComplexTypeError "Matrix of Int/Enum" t1
2233 b <- case t2 of
2234 TypeAny -> valid
2235 TypeList t | isValidInner t -> valid
2236 TypeMatrix _ t | isValidInner t -> valid
2237 _ -> invalid $ r2 <!> ComplexTypeError "Matrix of Matrix of Int/Enum" t2
2238
2239 return $ if null a || null b then Nothing else Just ()
2240 where
2241 isValidInner t = case t of
2242 TypeAny -> True
2243 TypeList TypeInt {} -> True
2244 TypeList TypeAny -> True
2245 TypeMatrix _ TypeInt {} -> True
2246 TypeMatrix _ TypeAny -> True
2247 _ -> False
2248
2249 toMSetArgs :: SArg -> Validator ()
2250 toMSetArgs (r, typeOf_ -> a) = case a of
2251 TypeAny -> return $ pure ()
2252 TypeList _ -> return $ pure ()
2253 TypeMatrix {} -> return $ pure ()
2254 TypeMSet {} -> return $ pure ()
2255 TypeSet {} -> return $ pure ()
2256 TypeFunction {} -> return $ pure ()
2257 TypeRelation {} -> return $ pure ()
2258 _ -> invalid $ r <!> ComplexTypeError "Matrix ,list,function,relation,mset,set " a
2259 toSetArgs :: SArg -> Validator ()
2260 toSetArgs (r, typeOf_ -> a) = case a of
2261 TypeAny -> return $ pure ()
2262 TypeList _ -> return $ pure ()
2263 TypeMatrix {} -> return $ pure ()
2264 TypeMSet {} -> return $ pure ()
2265 TypeFunction {} -> return $ pure ()
2266 TypeRelation {} -> return $ pure ()
2267 _ -> invalid $ r <!> ComplexTypeError "Matrix ,list,function,relation,mset " a
2268 listOrMatrix :: SArg -> Validator ()
2269 listOrMatrix (r, typeOf_ -> a) = case a of
2270 TypeAny -> return $ pure ()
2271 TypeList _ -> return $ pure ()
2272 TypeMatrix {} -> return $ pure ()
2273 _ -> invalid $ r <!> ComplexTypeError "Matrix or list" a
2274 freqArgs :: SArg -> SArg -> Validator ()
2275 freqArgs (r1, a) (r2, b) = do
2276 let tb = typeOf_ b
2277 let (rt, ti) = case typeOf_ a of
2278 TypeMatrix idx ms -> (TypeMatrix idx md, md) where md = mostDefinedS [tb, ms]
2279 TypeMSet ms -> (TypeMSet md, md) where md = mostDefinedS [tb, ms]
2280 _ -> (TypeMatrix tInt tb, tb)
2281 a' <- unifyTypesFailing rt (r1, a)
2282 b' <- unifyTypesFailing ti (r2, b)
2283 return $ if null a' || null b' then Nothing else Just ()
2284
2285 unifies :: SArg -> SArg -> Validator ()
2286 unifies a b = do
2287 let md = mostDefinedS $ map (typeOf_ . unregion) [a, b]
2288 a' <- unifyTypesFailing md a
2289 b' <- unifyTypesFailing md b
2290 return $ if null a' || null b' then Nothing else Just ()
2291 func :: SArg -> Validator ()
2292 func (_, Typed (TypeFunction _ _) _) = valid
2293 func (_, Typed TypeAny _) = valid
2294 func (r, Typed t _) = invalid $ r <!> TypeError (TypeFunction TypeAny TypeAny) t
2295 set :: SArg -> Validator Type
2296 set (_, Typed (TypeSet t) _) = return $ pure t
2297 set (_, Typed TypeAny _) = return $ pure TypeAny
2298 set (r, Typed t _) = invalid $ r <!> TypeError (TypeSet TypeAny) t
2299
2300 powerSetType (Just ((TypeSet i))) = Just $ TypeSet (TypeSet i)
2301 powerSetType _ = Just $ TypeSet $ TypeSet TypeAny
2302
2303 only t (r, typeOf_ -> t') = do setContext r; if t' == TypeAny || t == t' then return $ Just t else invalid $ r <!> TypeError t t'
2304
2305 listInt (r, typeOf_ -> t') = case t' of
2306 TypeAny -> return $ Just t'
2307 TypeList TypeInt {} -> return $ Just t'
2308 TypeMatrix _ TypeInt {} -> return $ Just t'
2309 _ -> invalid $ r <!> ComplexTypeError "Matrix or list of int or enum" t'
2310 partInner :: Maybe Type -> Maybe Type
2311 partInner (Just (TypePartition a)) = Just $ TypeSet a
2312 partInner _ = Just $ TypeSet TypeAny
2313
2314 restrictArgs :: Arg -> Arg -> Validator ()
2315 restrictArgs (r1, (k, _)) (r2, (kd, _)) = do
2316 setContext r1
2317 funcType <- getValueType k
2318 setContext r2
2319 domType <- getDomainType kd
2320 unifyTypesFailing (TypeFunction domType TypeAny) (r1, Typed funcType ())
2321
2322 restrictTypes :: Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type
2323 restrictTypes (fmap fst -> kv) (fmap fst -> kd) = Just $ TypeFunction from to
2324 where
2325 dType = case kd of
2326 Just (Kind DomainType t) -> getDomainMembers t
2327 _ -> TypeAny
2328 from = case kv of
2329 Just (Kind ValueType {} (TypeFunction fr _)) | typesUnifyS [dType, fr] -> mostDefinedS [dType, fr]
2330 Just (Kind ValueType {} (TypeFunction fr _)) -> fr
2331 _ -> mostDefinedS [TypeAny, dType]
2332 to = case kv of
2333 Just (Kind ValueType {} (TypeFunction _ to')) -> to'
2334 _ -> TypeAny
2335
2336 imSetArgs :: SArg -> SArg -> Validator ()
2337 imSetArgs (r1, a) (r2, b) = do
2338 let t = case (typeOf_ a, typeOf_ b) of
2339 (TypeFunction i _, tb) -> mostDefinedS [i, tb]
2340 (TypeSequence _, _) -> tInt
2341 (_, tb) -> tb
2342 a' <- unifyTypesFailing (TypeFunction t TypeAny) (r1, a)
2343 b' <- unifyTypesFailing t (r2, b)
2344 return $ if null a' || null b' then Nothing else Just ()
2345 preImageArgs :: SArg -> SArg -> Validator ()
2346 preImageArgs _ _ = return $ Just ()
2347 -- preImageArgs (r1, a) (r2, b) = do
2348 -- let t = case (typeOf_ a, typeOf_ b) of
2349 -- (TypeFunction _ i, tb) -> mostDefinedS [i, tb]
2350 -- (TypeSequence i, _) -> i
2351 -- (_, tb) -> tb
2352 -- a' <- unifyTypesFailing (TypeFunction TypeAny t) (r1, a)
2353 -- b' <- unifyTypesFailing t (r2, b)
2354 -- return $ if null a' || null b' then Nothing else Just ()
2355
2356 partyArgs :: SArg -> SArg -> Validator ()
2357 partyArgs (r1, a) (r2, b) = do
2358 let t = case (typeOf_ a, typeOf_ b) of
2359 (ta, TypePartition tb) -> mostDefinedS [ta, tb]
2360 (ta, _) -> ta
2361 a' <- unifyTypesFailing t (r1, a)
2362 b' <- unifyTypesFailing (TypePartition t) (r2, b)
2363 return $ if null a' || null b' then Nothing else Just ()
2364
2365 inverseArgs :: SArg -> SArg -> Validator ()
2366 inverseArgs (r1, a) (r2, b) = do
2367 let (fIn, fOut) = case (typeOf_ a, typeOf_ b) of
2368 (TypeFunction fi fo, TypeFunction gi go) -> (mostDefinedS [fi, go], mostDefinedS [fo, gi])
2369 (TypeFunction fi fo, _) -> (fi, fo)
2370 (_, TypeFunction gi go) -> (gi, go)
2371 _ -> (TypeAny, TypeAny)
2372 a' <- unifyTypesFailing (TypeFunction fIn fOut) (r1, a)
2373 b' <- unifyTypesFailing (TypeFunction fOut fIn) (r2, b)
2374 return $ if null a' || null b' then Nothing else Just ()
2375 setPartArgs :: SArg -> SArg -> Validator ()
2376 setPartArgs (r1, a) (r2, b) = do
2377 let t = case (typeOf_ a, typeOf_ b) of
2378 (TypeSet st, TypePartition pt) -> mostDefinedS [st, pt]
2379 (TypeSet st, _) -> st
2380 (_, TypePartition ts) -> ts
2381 _ -> TypeAny
2382 a' <- unifyTypesFailing (TypeSet t) (r1, a)
2383 b' <- unifyTypesFailing (TypePartition t) (r2, b)
2384 return $ if null a' || null b' then Nothing else Just ()
2385
2386 partyType :: Maybe Type -> Maybe Type -> Maybe Type
2387 partyType a b = do
2388 let at' = fromMaybe TypeAny a
2389 let bt = case b of
2390 Just (TypePartition t) -> t
2391 _ -> TypeAny
2392 return $ TypeSet $ mostDefinedS [at', bt]
2393 partsType :: Maybe Type -> Maybe Type
2394 partsType (Just (TypePartition a)) = Just $ TypeSet $ TypeSet a
2395 partsType (Just TypeAny) = Just $ TypeSet $ TypeSet TypeAny
2396 partsType _ = Nothing
2397
2398 minMaxArgs :: Arg -> Validator ()
2399 minMaxArgs (r, (Kind DomainType t, _)) =
2400 case t of
2401 TypeInt TagInt -> valid
2402 TypeInt (TagEnum _) -> valid
2403 TypeEnum {} -> valid
2404 TypeAny -> valid
2405 _ -> invalid $ r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t
2406 minMaxArgs (r, (k, _)) = do
2407 t <- getValueType k
2408 inner <- case t of
2409 TypeList tyInner -> return tyInner
2410 TypeMatrix _ tyInner -> return tyInner
2411 TypeSet tyInner -> return tyInner
2412 TypeMSet tyInner -> return tyInner
2413 TypeAny -> return TypeAny
2414 _ -> TypeAny <$ invalid (r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t)
2415 case inner of
2416 TypeInt TagInt -> valid
2417 TypeInt (TagEnum _) -> valid
2418 TypeEnum {} -> valid
2419 TypeAny -> valid
2420 _ -> invalid $ r <!> ComplexTypeError "Domain of int-like or matrix of int-like" t
2421 minMaxType :: Maybe (Kind, a) -> Maybe Type
2422 minMaxType (Just (Kind DomainType t@(TypeInt {}), _)) = Just t
2423 minMaxType (Just (Kind DomainType (TypeEnum (Name nm)), _)) = Just . TypeInt $ TagEnum nm
2424 minMaxType (Just (Kind ValueType {} (TypeMatrix _ a), _)) = minMaxType (Just (Kind DomainType a, ()))
2425 minMaxType (Just (Kind ValueType {} (TypeList a), _)) = minMaxType (Just (Kind DomainType a, ()))
2426 minMaxType (Just (Kind ValueType {} (TypeSet a), _)) = minMaxType (Just (Kind DomainType a, ()))
2427 minMaxType (Just (Kind ValueType {} (TypeMSet a), _)) = minMaxType (Just (Kind DomainType a, ()))
2428 minMaxType _ = Just TypeAny
2429
2430 transformArgs :: SArg -> SArg -> Validator ()
2431 transformArgs _ _ = return $ pure ()
2432 activeArgs :: SArg -> SArg -> Validator ()
2433 activeArgs (_, typeOf_ -> TypeAny) _ = valid
2434 activeArgs (r, typeOf_ -> t@(TypeVariant _)) (r2, typeOf_ -> b) = checkRVMember (r, t) (r2, b)
2435 activeArgs (r, typeOf_ -> t) _ = invalid $ r <!> ComplexTypeError "Variant " t
2436
2437 typeToSet :: Maybe Type -> Maybe Type
2438 typeToSet (Just t) = Just . TypeSet $ fromMaybe TypeAny (tMembers t)
2439 typeToSet _ = Just $ TypeSet TypeAny
2440 typeToMSet :: Maybe Type -> Maybe Type
2441 typeToMSet (Just t) = Just . TypeMSet $ fromMaybe TypeAny (tMembers t)
2442 typeToMSet _ = Just $ TypeMSet TypeAny
2443 typeToRelation :: Maybe Type -> Maybe Type
2444 typeToRelation (Just (TypeFunction i j)) = Just $ TypeRelation [i, j]
2445 typeToRelation (Just TypeAny) = Just $ TypeRelation [TypeAny, TypeAny]
2446 typeToRelation _ = Nothing
2447 tMembers t = case t of
2448 TypeAny -> Just TypeAny
2449 TypeList ty -> Just ty
2450 TypeMatrix _ i -> Just i
2451 TypeSet ty -> Just ty
2452 TypeMSet ty -> Just ty
2453 TypeFunction i j -> Just $ TypeTuple [i, j]
2454 TypeRelation tys -> Just $ TypeTuple tys
2455 _ -> Nothing
2456
2457 imageArgs :: SArg -> SArg -> Validator ()
2458 imageArgs (r1, typeOf_ -> t1) r2 = do
2459 from <- case t1 of
2460 TypeAny -> return $ Just TypeAny
2461 TypeFunction a _ -> return $ Just a
2462 TypeSequence _ -> return $ Just tInt
2463 _ -> Nothing <$ raiseTypeError (r1 <!> ComplexTypeError "Function or Sequence" t1)
2464 case from of
2465 Just f -> unifyTypes f r2 >> return (pure ())
2466 Nothing -> return Nothing
2467
2468 sumArgs :: SArg -> Validator ()
2469 sumArgs (r, typeOf_ -> t') = do
2470 t <- case t' of
2471 TypeAny -> return TypeAny
2472 TypeList t -> return t
2473 TypeMatrix _ t -> return t
2474 TypeSet t -> return t
2475 TypeMSet t -> return t
2476 _ -> TypeAny <$ raiseTypeError (r <!> ComplexTypeError "Matrix or Set" t')
2477
2478 case t of
2479 TypeAny -> return $ pure ()
2480 TypeInt TagInt -> return $ pure ()
2481 _ -> Nothing <$ raiseTypeError (r <!> ComplexTypeError "Integer elements" t)
2482 funcSeq :: SArg -> Validator ()
2483 funcSeq (r, typeOf_ -> t') = case t' of
2484 TypeAny -> return $ pure ()
2485 TypeSequence _ -> return $ pure ()
2486 TypeFunction _ _ -> return $ pure ()
2487 _ -> invalid $ r <!> ComplexTypeError "Function or Sequence" t'
2488 funcDomain :: Maybe Type -> Maybe Type
2489 funcDomain (Just (TypeFunction a _)) = Just a
2490 funcDomain (Just (TypeSequence _)) = Just tInt
2491 funcDomain _ = Just TypeAny
2492 funcRange :: Maybe Type -> Maybe Type
2493 funcRange (Just (TypeFunction _ b)) = Just b
2494 funcRange (Just ((TypeSequence b))) = Just b
2495 funcRange _ = Just TypeAny
2496 part :: SArg -> Validator ()
2497 part (r, typeOf_ -> t) = case t of
2498 TypeAny -> valid
2499 TypePartition _ -> return $ pure ()
2500 _ -> invalid $ r <!> TypeError (TypePartition TypeAny) t
2501
2502 histArgs :: SArg -> Validator ()
2503 histArgs (r, typeOf_ -> a) = case a of
2504 TypeMSet _ -> return $ pure ()
2505 TypeList _ -> return $ pure ()
2506 TypeMatrix _ _ -> return $ pure ()
2507 TypeAny -> return $ pure ()
2508 _ -> invalid $ r <!> ComplexTypeError "Matrix, List or MSet" a
2509 histType :: Maybe Type -> Maybe Type
2510 histType (Just ((TypeMSet a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2511 histType (Just ((TypeMatrix _ a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2512 histType (Just ((TypeList a))) = Just $ TypeMatrix tInt $ TypeTuple [a, tInt]
2513 histType _ = Just $ TypeMatrix tInt $ TypeTuple [TypeAny, tInt]
2514 enumerable :: SArg -> Validator ()
2515 enumerable (r, typeOf_ -> t) = case t of
2516 TypeAny -> return $ pure ()
2517 TypeInt TagUnnamed {} -> invalid $ r <!> CustomError "Anonymous enums are not explictly enumerable"
2518 TypeInt _ -> return $ pure ()
2519 TypeEnum {} -> return $ pure ()
2520 TypeBool -> return $ pure ()
2521 _ -> invalid $ r <!> ComplexTypeError "int enum or bool" t
2522 enumerableType :: Maybe Type -> Maybe Type
2523 enumerableType (Just t@(TypeInt TagInt)) = Just t
2524 enumerableType (Just t@(TypeInt (TagEnum _))) = Just t
2525 enumerableType (Just t@(TypeEnum {})) = Just t
2526 enumerableType _ = Nothing
2527
2528 flattenType :: Maybe Int -> Maybe Type -> Maybe Type
2529 flattenType (Just n) (Just a) | n < 0 = Just $ TypeList a
2530 flattenType (Just n) (Just (TypeList m)) = flattenType (Just (n - 1)) (Just m)
2531 flattenType (Just n) (Just (TypeMatrix _ m)) = flattenType (Just (n - 1)) (Just m)
2532 flattenType Nothing (Just (TypeMatrix _ m)) = flattenType Nothing (Just m)
2533 flattenType Nothing (Just (TypeList m)) = flattenType Nothing (Just m)
2534 flattenType Nothing (Just t) = Just $ TypeList t
2535 flattenType _ _ = Just $ TypeList TypeAny
2536
2537 validateFuncOp :: Lexeme -> [RegionTagged (Kind, Expression)] -> ValidatorS (Typed Expression)
2538 validateFuncOp l args = do
2539 let b = funcOpBuilder l
2540 b args
2541
2542 -- case argCheck of
2543 -- Nothing -> return $ Typed (r []) $ fallback "arg fail"
2544 -- Just tys -> return $ Typed (r tys)(b $ map untype tys)
2545
2546 isOfType :: Type -> RegionTagged (Typed Expression) -> ValidatorS Bool
2547 isOfType t (r, v) = setContext r >> return v ?=> exactly t >> return (typesUnifyS [t, typeOf_ v])
2548
2549 isLogicalContainer :: RegionTagged (Typed Expression) -> Validator ()
2550 isLogicalContainer (r, Typed t _) = case t of
2551 TypeAny -> return $ pure ()
2552 TypeList TypeAny -> return $ pure ()
2553 TypeList TypeBool -> return $ pure ()
2554 TypeMatrix _ TypeAny -> return $ pure ()
2555 TypeMatrix _ TypeBool -> return $ pure ()
2556 TypeSet TypeAny -> return $ pure ()
2557 TypeMSet TypeBool -> return $ pure ()
2558 _ -> invalid $ r <!> ComplexTypeError "Collection of boolean" t
2559
2560 -- validateArgList :: [RegionTagged (Typed Expression) -> ValidatorS Bool] -> [RegionTagged (Typed Expression)] -> Validator [Typed Expression]
2561 -- validateArgList ps args | length args < length ps = do invalid $ args <!> MissingArgsError (length ps)
2562 -- validateArgList ps args = do
2563 -- let ps' = ps ++ repeat argOverflow
2564 -- xs <- zipWithM id ps' args
2565 -- return (if and xs then Just $ map unregion args else Nothing)
2566
2567 -- argOverflow :: RegionTagged a -> ValidatorS Bool
2568 -- argOverflow (region,_) = do
2569 -- setContext region
2570 -- void . contextError $ CustomError "Extra Args"
2571 -- return False
2572 type SArg = RegionTagged (Typed Expression)
2573
2574 type Arg = RegionTagged (Kind, Expression)
2575
2576 unFunc ::
2577 (Arg -> Validator a) -> -- Arg validator
2578 (Maybe (Kind, Expression) -> Maybe Type) -> -- typeEvaluator
2579 ([Expression] -> Expression) -> -- mkOp or similar
2580 [Arg] ->
2581 ValidatorS (Typed Expression)
2582 unFunc argVal t f args = do
2583 (v, ts) <- case args of
2584 [] -> tooFewArgs 1 0 >> return (Nothing, Nothing)
2585 [x] -> do
2586 r <- argVal x
2587 tc <- gets typeChecking
2588 let result = case r of
2589 Nothing | tc -> Nothing
2590 _ -> Just [(snd . unregion) x]
2591 return (result, Just $ unregion x)
2592 (x : rs) -> do
2593 tooManyArgs rs
2594 r <- argVal x
2595 let result = case r of
2596 Nothing -> Nothing
2597 Just _ -> Just [(snd . unregion) x]
2598 return (result, Just $ unregion x)
2599 let res = maybe (fallback "Arg Fail Unfunc") f v
2600 return $ Typed (fromMaybe TypeAny $ t ts) res
2601
2602 biFunc :: (Arg -> Arg -> Validator a) -> (Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2603 biFunc argVal t f args = do
2604 (v, ts) <- case args of
2605 [] -> tooFewArgs 2 0 >> return (Nothing, (Nothing, Nothing))
2606 [x] -> tooFewArgs 2 1 >> return (Nothing, (Just $ unregion x, Nothing))
2607 [x, y] -> do
2608 r <- argVal x y
2609 tc <- gets typeChecking
2610 let result = case r of
2611 Nothing | tc -> Nothing
2612 _ -> Just $ map (snd . unregion) [x, y]
2613 return (result, (Just (unregion x), Just (unregion y)))
2614 (x : y : rs) -> do
2615 tooManyArgs rs
2616 r <- argVal x y
2617 let result = case r of
2618 Nothing -> Nothing
2619 Just _ -> Just $ map (snd . unregion) [x, y]
2620 return (result, (Just (unregion x), Just (unregion y)))
2621 let res = maybe (fallback "Arg Fail BiFunct") f v
2622 return $ Typed (fromMaybe TypeAny $ uncurry t ts) res
2623
2624 triFunc :: (Arg -> Arg -> Arg -> Validator a) -> (Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe (Kind, Expression) -> Maybe Type) -> ([Expression] -> Expression) -> [Arg] -> ValidatorS (Typed Expression)
2625 triFunc argVal t f args = do
2626 (v, ts) <- case args of
2627 [] -> tooFewArgs 3 0 >> return (Nothing, (Nothing, Nothing, Nothing))
2628 [x] -> tooFewArgs 3 1 >> return (Nothing, (Just $ unregion x, Nothing, Nothing))
2629 [x, y] -> tooFewArgs 3 2 >> return (Nothing, (Just $ unregion x, Just $ unregion y, Nothing))
2630 [x, y, z] -> do
2631 r <- argVal x y z
2632 tc <- gets typeChecking
2633 let result = case r of
2634 Nothing | tc -> Nothing
2635 _ -> Just $ map (snd . unregion) [x, y, z]
2636 return (result, (Just (unregion x), Just (unregion y), Just (unregion z)))
2637 (x : y : z : rs) -> do
2638 tooManyArgs rs
2639 r <- argVal x y z
2640 let result = case r of
2641 Nothing -> Nothing
2642 Just _ -> Just $ map (snd . unregion) [x, y, z]
2643 return (result, (Just (unregion x), Just (unregion y), Just (unregion z)))
2644 let res = maybe (fallback "Arg Fail Tri") f v
2645 return $ Typed (fromMaybe TypeAny $ uncurry3 t ts) res
2646 where
2647 uncurry3 fn (a, b, c) = fn a b c -- todo export from prelude
2648
2649 tooFewArgs :: Int -> Int -> ValidatorS ()
2650 tooFewArgs n i = void . contextError $ MissingArgsError n i
2651
2652 tooManyArgs :: [RegionTagged a] -> ValidatorS ()
2653 tooManyArgs = mapM_ (\x -> raiseError $ x <!> UnexpectedArg)
2654
2655 checkRVMember :: RegionTagged Type -> RegionTagged Type -> Validator ()
2656 checkRVMember (_, TypeRecord ts) (_, TypeRecordMember nm _) | not . null $ lookup nm ts = return $ pure ()
2657 checkRVMember (_, TypeRecord ts) (r2, r) = do
2658 raiseTypeError $ r2 <!> TypeError (TypeRecordMember (Name "") ts) r
2659 return Nothing
2660 checkRVMember (_, TypeVariant ts) (_, TypeVariantMember nm _) | not . null $ lookup nm ts = return $ pure ()
2661 checkRVMember (_, TypeVariant ts) (r2, r) = do
2662 raiseTypeError $ r2 <!> TypeError (TypeVariantMember (Name "") ts) r
2663 return Nothing
2664 checkRVMember (r1, t) _ = do
2665 raiseTypeError $ r1 <!> TypeError (TypeVariant []) t
2666 return Nothing
2667
2668 type OpValidator = RegionTagged Kind -> RegionTagged Kind -> ValidatorS Type
2669
2670 type OpTyper = Kind -> Kind -> Type
2671
2672 sameToSameV :: (Type -> ValidatorS Type) -> (Type -> Type -> Type) -> OpValidator
2673 sameToSameV tc t (rl, kl) (rr, kr) = do
2674 setContext rl
2675 lt <- getValueType kl
2676 lt' <- tc lt
2677 setContext rr
2678 rt <- getValueType kr
2679 rt' <- tc rt
2680 let md = mostDefinedS [lt, rt]
2681 _ <- unifyTypesFailing md (rl, Typed lt' ())
2682 _ <- unifyTypesFailing md (rr, Typed rt' ())
2683 return $ t lt' rt'
2684
2685 binOpType :: Lexeme -> OpValidator
2686 binOpType l = case l of
2687 L_Plus -> sameToSameV number same
2688 L_Minus -> sameToSameV minusArgs same
2689 L_Times -> sameToSameV number same
2690 L_Div -> sameToSameV number same
2691 L_Mod -> sameToSameV number same
2692 L_Pow -> sameToSameV number same
2693 L_Eq -> sameToSameV pure cBool
2694 L_Neq -> sameToSameV pure cBool
2695 L_Lt -> sameToSameV orderable cBool
2696 L_Leq -> sameToSameV orderable cBool
2697 L_Gt -> sameToSameV orderable cBool
2698 L_Geq -> sameToSameV orderable cBool
2699 L_in -> checkIn
2700 L_And -> sameToSameV bools cBool
2701 L_Or -> sameToSameV bools cBool
2702 L_Imply -> sameToSameV bools cBool
2703 L_Iff -> sameToSameV bools cBool -- b b b
2704 L_subset -> sameToSameV setLike cBool -- set mset func rel
2705 L_subsetEq -> sameToSameV setLike cBool
2706 -- \^^^
2707 L_supset -> sameToSameV setLike cBool
2708 -- \^^^^
2709 L_supsetEq -> sameToSameV setLike cBool
2710 -- \^^
2711
2712 L_subsequence -> sameToSameV justSequence cBool -- seq - seq -bool
2713 L_substring -> sameToSameV justSequence cBool -- seq - seq -bool
2714 L_intersect -> sameToSameV setLike same
2715 L_union -> sameToSameV setLike same
2716 L_LexLt -> sameToSameV pure cBool
2717 L_LexLeq -> sameToSameV pure cBool
2718 L_LexGt -> sameToSameV pure cBool
2719 L_LexGeq -> sameToSameV pure cBool
2720 L_DotLt -> sameToSameV pure cBool
2721 L_DotLeq -> sameToSameV pure cBool
2722 L_DotGt -> sameToSameV pure cBool
2723 L_DotGeq -> sameToSameV pure cBool
2724 L_TildeLt -> sameToSameV pure cBool
2725 L_TildeLeq -> sameToSameV pure cBool
2726 L_TildeGt -> sameToSameV pure cBool
2727 L_TildeGeq -> sameToSameV pure cBool
2728 _ -> bug $ "Unkown operator" <+> pretty (show l)
2729 where
2730 cBool = const . const TypeBool
2731 same a b = mostDefinedS [a, b]
2732 checkIn :: OpValidator
2733 checkIn (r1, kl) (r2, kr) = do
2734 setContext r1
2735 lt <- getValueType kl
2736 setContext r2
2737 rt <- getValueType kr
2738 case innerTypeOf rt of
2739 Just t -> unifyTypes t (r1, Typed lt ())
2740 Nothing -> unless (rt == TypeAny) $ raiseTypeError (r2 <!> ComplexTypeError (T.pack . show $ "Container of " <+> pretty lt) rt)
2741 return TypeBool
2742
2743 number :: Type -> ValidatorS Type
2744 number t = case t of
2745 TypeInt TagInt -> return t
2746 TypeInt TagEnum {} -> return t
2747 TypeAny -> return t
2748 _ -> TypeAny <$ contextTypeError (ComplexTypeError "Number or Enum" t)
2749 minusArgs t = case t of
2750 TypeInt TagInt -> return t
2751 TypeSet _ -> return t
2752 TypeMSet _ -> return t
2753 TypeRelation _ -> return t
2754 TypeFunction _ _ -> return t
2755 _ -> TypeAny <$ contextTypeError (ComplexTypeError "Number / set/ mset / relation / function" t)
2756 orderable t = case t of
2757 TypeInt TagInt -> return t
2758 TypeInt TagEnum {} -> return t
2759 TypeBool -> return t
2760 TypeAny -> return t
2761 _ -> TypeAny <$ contextTypeError (ComplexTypeError "Number, Enum or Bool" t)
2762 justSequence t = case t of
2763 TypeAny -> return t
2764 TypeSequence _ -> return t
2765 _ -> TypeAny <$ contextTypeError (TypeError (TypeSequence TypeAny) t)
2766 bools t = case t of
2767 TypeAny -> return t
2768 TypeBool -> return t
2769 _ -> TypeAny <$ contextTypeError (TypeError TypeBool t)
2770 setLike t = case t of
2771 TypeAny -> return t
2772 TypeMSet _ -> return t
2773 TypeSet _ -> return t
2774 TypeFunction _ _ -> return t
2775 TypeRelation _ -> return t
2776 _ -> TypeAny <$ contextTypeError (ComplexTypeError "Set MSet funcition or relation" t)