Overview
| Comment: | TypeChecker now checks to see if a multiword handles every possible leading type. Fixes [56a0fe1350]. |
|---|---|
| Timelines: | family | ancestors | descendants | both | trunk |
| Files: | files | file ages | folders |
| SHA3-256: |
dbcb88d2fc2f2f1cfb95b2ba0900515a |
| User & Date: | robin.hansen on 2020-10-23 04:46:29 |
| Other Links: | manifest | tags |
Context
|
2020-11-19
| ||
| 05:57 | Fix 'Quotations' example in play ground. check-in: fc5483d159 user: robin.hansen tags: trunk, alpha-1, releases | |
|
2020-11-17
| ||
| 14:42 | Add test for compilation failure found in playground. check-in: d4ac6cbece user: robin.hansen tags: bugfix-generics-and-quotations | |
|
2020-10-23
| ||
| 04:46 | TypeChecker now checks to see if a multiword handles every possible leading type. Fixes [56a0fe1350]... check-in: dbcb88d2fc user: robin.hansen tags: trunk | |
| 04:44 | Add error message for inexhaustive multiwords. Closed-Leaf check-in: 30f96733db user: robin.hansen tags: exhaustiveness-checking | |
|
2020-10-13
| ||
| 05:00 | Unions with generic branches can now be used in multiwords. Fixing [0dd72ccbb4]. check-in: 1fd01c7a22 user: robin.hansen tags: trunk | |
Changes
Modified src/Play/TypeChecker.elm from [a76842cc9d] to [6269134213].
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
...
697
698
699
700
701
702
703
704
705
706
707
708
709
710
|
inferredType =
List.head inferredWhenTypes
|> Maybe.withDefault { input = [], output = [] }
|> replaceFirstType (unionOfTypeMatches whens)
|> joinOutputs (List.map .output inferredWhenTypes)
finalContext =
{ newContext
| typedWords =
Dict.insert untypedDef.name
{ name = untypedDef.name
, type_ =
TypeSignature.toMaybe untypedDef.metadata.type_
|> Maybe.withDefault inferredType
, metadata = untypedDef.metadata
, implementation =
MultiImpl
(List.map (Tuple.mapBoth mapTypeMatch (untypedToTypedImplementation newContext)) initialWhens)
(untypedToTypedImplementation newContext defaultImpl)
}
newContext.typedWords
, errors =
if whensAreConsistent && whensAreCompatible then
newContext.errors
else
let
error =
InconsistentWhens
(Maybe.withDefault SourceLocation.emptyRange untypedDef.metadata.sourceLocationRange)
untypedDef.name
in
error :: newContext.errors
}
in
verifyTypeSignature inferredType untypedDef finalContext
|> cleanContext
inferWhenTypes :
................................................................................
Qualifier.LiteralType val ->
( fieldName, LiteralType val )
Qualifier.RecursiveMatch val ->
( fieldName, RecursiveMatch (mapTypeMatch val) )
verifyTypeSignature : WordType -> Qualifier.WordDefinition -> Context -> Context
verifyTypeSignature inferredType untypedDef context =
case TypeSignature.toMaybe untypedDef.metadata.type_ of
Just annotatedType ->
let
( _, simplifiedAnnotatedType ) =
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|
<
<
|
<
<
<
<
<
<
<
<
<
<
<
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
...
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
|
inferredType =
List.head inferredWhenTypes
|> Maybe.withDefault { input = [], output = [] }
|> replaceFirstType (unionOfTypeMatches whens)
|> joinOutputs (List.map .output inferredWhenTypes)
exposedType =
TypeSignature.toMaybe untypedDef.metadata.type_
|> Maybe.withDefault inferredType
maybeConsistencyError =
if whensAreConsistent && whensAreCompatible then
Nothing
else
let
error =
InconsistentWhens
(Maybe.withDefault SourceLocation.emptyRange untypedDef.metadata.sourceLocationRange)
untypedDef.name
in
Just error
maybeInexhaustiveError =
inexhaustivenessCheck
(Maybe.withDefault SourceLocation.emptyRange untypedDef.metadata.sourceLocationRange)
whenPatterns
finalContext =
{ newContext
| typedWords =
Dict.insert untypedDef.name
{ name = untypedDef.name
, type_ = exposedType
, metadata = untypedDef.metadata
, implementation =
MultiImpl
(List.map (Tuple.mapBoth mapTypeMatch (untypedToTypedImplementation newContext)) initialWhens)
(untypedToTypedImplementation newContext defaultImpl)
}
newContext.typedWords
, errors = List.filterMap identity [ maybeConsistencyError, maybeInexhaustiveError ] ++ newContext.errors
}
in
verifyTypeSignature inferredType untypedDef finalContext
|> cleanContext
inferWhenTypes :
................................................................................
Qualifier.LiteralType val ->
( fieldName, LiteralType val )
Qualifier.RecursiveMatch val ->
( fieldName, RecursiveMatch (mapTypeMatch val) )
inexhaustivenessCheck : SourceLocationRange -> List Qualifier.TypeMatch -> Maybe Problem
inexhaustivenessCheck range patterns =
let
inexhaustiveStates =
List.foldl (inexhaustivenessCheckHelper []) [] patterns
|> List.filter (\( _, state ) -> state /= Total)
|> List.map Tuple.first
in
case inexhaustiveStates of
[] ->
Nothing
_ ->
Just (InexhaustiveMultiWord range inexhaustiveStates)
type InexhaustiveState
= Total
| SeenInt
| SeenType Type
inexhaustivenessCheckHelper : List Type -> Qualifier.TypeMatch -> List ( List Type, InexhaustiveState ) -> List ( List Type, InexhaustiveState )
inexhaustivenessCheckHelper typePrefix (Qualifier.TypeMatch _ t conds) acc =
let
typeList =
typePrefix ++ [ t ]
in
if List.any (\( toMatch, state ) -> typeList == toMatch && state == Total) acc then
acc
else
let
subcases =
conds
|> List.map Tuple.second
|> List.filterMap isRecursiveMatch
|> List.foldl (inexhaustivenessCheckHelper typeList) acc
isRecursiveMatch match =
case match of
Qualifier.RecursiveMatch cond ->
Just cond
_ ->
Nothing
toAdd =
case ( t, conds, subcases ) of
( _, [], _ ) ->
[ ( typeList, Total ) ]
( Type.Int, _, _ ) ->
[ ( typeList, SeenInt ) ]
_ ->
if List.all (Tuple.second >> (==) Total) subcases then
[ ( typeList, Total ) ]
else
subcases
modifiedAcc =
if toAdd /= [ ( typeList, Total ) ] then
acc
else
List.filter
(\( toMatch, _ ) ->
List.take (List.length typeList) toMatch /= typeList
)
acc
in
if List.find (\( toMatch, _ ) -> toMatch == typeList) modifiedAcc == Nothing then
toAdd ++ modifiedAcc
else
let
updatedStates =
List.filter (\( toMatch, _ ) -> toMatch /= typeList) modifiedAcc
in
toAdd ++ updatedStates
verifyTypeSignature : WordType -> Qualifier.WordDefinition -> Context -> Context
verifyTypeSignature inferredType untypedDef context =
case TypeSignature.toMaybe untypedDef.metadata.type_ of
Just annotatedType ->
let
( _, simplifiedAnnotatedType ) =
|
Modified src/Play/TypeChecker/Problem.elm from [6e4a47646f] to [b183d4af4c].
10
11
12
13
14
15
16
17
18
19
20
21
22
23
..
56
57
58
59
60
61
62
|
type Problem
= UndeclaredGeneric SourceLocationRange String (Set String)
| TypeError SourceLocationRange String WordType WordType
| UnexpectedType SourceLocationRange String Type Type
| InconsistentWhens SourceLocationRange String
| MissingTypeAnnotationInRecursiveCallStack SourceLocationRange String
toString : String -> Problem -> String
toString source problem =
case problem of
UndeclaredGeneric range generic _ ->
SourceLocation.extractFromString source range
................................................................................
MissingTypeAnnotationInRecursiveCallStack range name ->
SourceLocation.extractFromString source range
++ "\n\n"
++ "We require a type annotation for '"
++ name
++ "' as we're unable to infer the type of a recursive call."
|
>
>
>
>
>
>
>
>
>
>
>
|
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
..
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
type Problem
= UndeclaredGeneric SourceLocationRange String (Set String)
| TypeError SourceLocationRange String WordType WordType
| UnexpectedType SourceLocationRange String Type Type
| InconsistentWhens SourceLocationRange String
| MissingTypeAnnotationInRecursiveCallStack SourceLocationRange String
| InexhaustiveMultiWord SourceLocationRange (List (List Type))
toString : String -> Problem -> String
toString source problem =
case problem of
UndeclaredGeneric range generic _ ->
SourceLocation.extractFromString source range
................................................................................
MissingTypeAnnotationInRecursiveCallStack range name ->
SourceLocation.extractFromString source range
++ "\n\n"
++ "We require a type annotation for '"
++ name
++ "' as we're unable to infer the type of a recursive call."
InexhaustiveMultiWord range missingTypes ->
let
formatTypePattern tp =
String.join " -> " (List.map Type.toDisplayString tp)
in
SourceLocation.extractFromString source range
++ "\n\n"
++ "This multiword doesn't handle all potential patterns. Missing patterns for:\n\n"
++ String.join "\n" (List.map formatTypePattern missingTypes)
|
Modified tests/Test/TypeChecker/Error.elm from [2b38f63d66] to [6a887ebaba].
253 254 255 256 257 258 259 260 261 262 263 264 265 266 |
{ input = [ Type.Int ], output = [ Type.Union [ Type.Generic "b", Type.Generic "a" ] ] }
{ input = [ Type.Int ], output = [ Type.Union [ Type.Custom "False", Type.Custom "True" ] ] }
]
errors
Ok _ ->
Expect.fail "Did not expect type checking to succeed"
]
checkForError : (Problem.Problem -> Bool) -> AST -> Expectation
checkForError fn source =
case TypeChecker.run source of
Err errors ->
|
> > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > |
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 |
{ input = [ Type.Int ], output = [ Type.Union [ Type.Generic "b", Type.Generic "a" ] ] }
{ input = [ Type.Int ], output = [ Type.Union [ Type.Custom "False", Type.Custom "True" ] ] }
]
errors
Ok _ ->
Expect.fail "Did not expect type checking to succeed"
, describe "Inexhaustiveness checking"
[ test "Simple example" <|
\_ ->
let
ast =
{ types = Dict.empty
, words =
Dict.fromListBy .name
[ { name = "main"
, metadata =
Metadata.default
|> Metadata.asEntryPoint
, implementation =
SoloImpl
[ Integer emptyRange 2
, Word emptyRange "mword"
]
}
, { name = "mword"
, metadata = Metadata.default
, implementation =
MultiImpl
[ ( TypeMatch emptyRange Type.Int [ ( "value>", LiteralInt 1 ) ]
, [ Integer emptyRange 1
, Builtin emptyRange Builtin.Plus
]
)
]
[]
}
]
}
inexhaustiveError problem =
case problem of
Problem.InexhaustiveMultiWord _ [ [ Type.Int ] ] ->
True
_ ->
False
in
checkForError inexhaustiveError ast
, test "Default clause is exhaustive" <|
\_ ->
let
ast =
{ types = Dict.empty
, words =
Dict.fromListBy .name
[ { name = "main"
, metadata =
Metadata.default
|> Metadata.asEntryPoint
, implementation =
SoloImpl
[ Integer emptyRange 2
, Word emptyRange "mword"
]
}
, { name = "mword"
, metadata = Metadata.default
, implementation =
MultiImpl
[ ( TypeMatch emptyRange Type.Int [ ( "value>", LiteralInt 1 ) ]
, [ Integer emptyRange 1
, Builtin emptyRange Builtin.Plus
]
)
]
[ Integer emptyRange 0
, Builtin emptyRange Builtin.Plus
]
}
]
}
in
case TypeChecker.run ast of
Ok _ ->
Expect.pass
Err errs ->
Expect.fail <| "Failed for unexpected reason: " ++ Debug.toString errs
, test "Nested" <|
\_ ->
let
ast =
{ types =
Dict.fromListBy typeDefinitionName
[ CustomTypeDef "IntBox"
emptyRange
[]
[ ( "value", Type.Int ) ]
]
, words =
Dict.fromListBy .name
[ { name = "main"
, metadata =
Metadata.default
|> Metadata.asEntryPoint
|> Metadata.withType [] [ Type.Int ]
, implementation =
SoloImpl
[ Integer emptyRange 1
, Word emptyRange ">IntBox"
, Word emptyRange "mword"
, Word emptyRange "value>"
]
}
, { name = "mword"
, metadata = Metadata.default
, implementation =
MultiImpl
[ ( TypeMatch emptyRange
(Type.Custom "IntBox")
[ ( "value>"
, RecursiveMatch
(TypeMatch emptyRange Type.Int [ ( "value>", LiteralInt 1 ) ])
)
]
, [ Word emptyRange "value>"
, Integer emptyRange 1
, Builtin emptyRange Builtin.Plus
, Word emptyRange ">IntBox"
]
)
]
[]
}
, { name = ">IntBox"
, metadata =
Metadata.default
|> Metadata.withVerifiedType [ Type.Int ] [ Type.Custom "IntBox" ]
, implementation =
SoloImpl
[ ConstructType "IntBox" ]
}
, { name = ">value"
, metadata =
Metadata.default
|> Metadata.withVerifiedType [ Type.Custom "IntBox", Type.Int ] [ Type.Custom "IntBox" ]
, implementation =
SoloImpl
[ SetMember "IntBox" "value" ]
}
, { name = "value>"
, metadata =
Metadata.default
|> Metadata.withVerifiedType [ Type.Custom "IntBox" ] [ Type.Int ]
, implementation =
SoloImpl
[ GetMember "IntBox" "value" ]
}
]
}
inexhaustiveError problem =
case problem of
Problem.InexhaustiveMultiWord _ [ [ Type.Custom "IntBox", Type.Int ] ] ->
True
_ ->
False
in
checkForError inexhaustiveError ast
, test "A total branch should remove any earlier seen branch" <|
\_ ->
let
ast =
{ types = Dict.empty
, words =
Dict.fromListBy .name
[ { name = "main"
, metadata =
Metadata.default
|> Metadata.asEntryPoint
, implementation =
SoloImpl
[ Integer emptyRange 2
, Word emptyRange "mword"
]
}
, { name = "mword"
, metadata = Metadata.default
, implementation =
MultiImpl
[ ( TypeMatch emptyRange Type.Int [ ( "value>", LiteralInt 1 ) ]
, [ Integer emptyRange 1
, Builtin emptyRange Builtin.Plus
]
)
, ( TypeMatch emptyRange Type.Int []
, [ Builtin emptyRange Builtin.StackDuplicate
, Builtin emptyRange Builtin.Plus
]
)
]
[]
}
]
}
in
case TypeChecker.run ast of
Err errors ->
Expect.fail <| "Failed for unexpected reason: " ++ Debug.toString errors
Ok _ ->
Expect.pass
, test "A total branch should prevent addition of later partial branch" <|
\_ ->
let
ast =
{ types = Dict.empty
, words =
Dict.fromListBy .name
[ { name = "main"
, metadata =
Metadata.default
|> Metadata.asEntryPoint
, implementation =
SoloImpl
[ Integer emptyRange 2
, Word emptyRange "mword"
]
}
, { name = "mword"
, metadata = Metadata.default
, implementation =
MultiImpl
[ ( TypeMatch emptyRange Type.Int []
, [ Builtin emptyRange Builtin.StackDuplicate
, Builtin emptyRange Builtin.Plus
]
)
, ( TypeMatch emptyRange Type.Int [ ( "value>", LiteralInt 1 ) ]
, [ Integer emptyRange 1
, Builtin emptyRange Builtin.Plus
]
)
]
[]
}
]
}
in
case TypeChecker.run ast of
Err errors ->
Expect.fail <| "Failed for unexpected reason: " ++ Debug.toString errors
Ok _ ->
Expect.pass
, test "Test with non-int type as pattern" <|
\_ ->
let
maybeUnion =
Type.Union
[ Type.Custom "IntBox"
, Type.Custom "Nil"
]
input =
{ types =
Dict.fromListBy typeDefinitionName
[ UnionTypeDef "Maybe"
emptyRange
[ "a" ]
[ Type.Generic "a"
, Type.Custom "Nil"
]
, CustomTypeDef "IntBox"
emptyRange
[]
[ ( "value", Type.Int ) ]
, CustomTypeDef "Nil" emptyRange [] []
]
, words =
Dict.fromListBy .name
[ { name = ">Nil"
, metadata =
Metadata.default
|> Metadata.withType [] [ Type.Custom "Nil" ]
, implementation =
SoloImpl
[ ConstructType "Nil"
]
}
, { name = ">IntBox"
, metadata =
Metadata.default
|> Metadata.withVerifiedType [ Type.Int ] [ Type.Custom "IntBox" ]
, implementation =
SoloImpl
[ ConstructType "IntBox" ]
}
, { name = ">value"
, metadata =
Metadata.default
|> Metadata.withVerifiedType [ Type.Custom "IntBox", Type.Int ] [ Type.Custom "IntBox" ]
, implementation =
SoloImpl
[ SetMember "IntBox" "value" ]
}
, { name = "value>"
, metadata =
Metadata.default
|> Metadata.withVerifiedType [ Type.Custom "IntBox" ] [ Type.Int ]
, implementation =
SoloImpl
[ GetMember "IntBox" "value" ]
}
, { name = "with-default"
, metadata =
Metadata.default
|> Metadata.withType
[ maybeUnion, Type.Int ]
[ Type.Int ]
, implementation =
MultiImpl
[ ( TypeMatch emptyRange
(Type.Custom "IntBox")
[ ( "value>"
, RecursiveMatch <|
TypeMatch emptyRange Type.Int [ ( "value>", LiteralInt 0 ) ]
)
]
, [ Builtin emptyRange Builtin.StackDrop
, Word emptyRange "value>"
]
)
, ( TypeMatch emptyRange (Type.Custom "Nil") []
, [ Builtin emptyRange Builtin.StackSwap
, Builtin emptyRange Builtin.StackDrop
]
)
]
[]
}
, { name = "main"
, metadata =
Metadata.default
|> Metadata.asEntryPoint
, implementation =
SoloImpl
[ Word emptyRange ">Nil"
, Integer emptyRange 1
, Word emptyRange "with-default"
]
}
]
}
inexhaustiveError problem =
case problem of
Problem.InexhaustiveMultiWord _ [ [ Type.Custom "IntBox", Type.Int ] ] ->
True
_ ->
False
in
checkForError inexhaustiveError input
]
]
checkForError : (Problem.Problem -> Bool) -> AST -> Expectation
checkForError fn source =
case TypeChecker.run source of
Err errors ->
|