Stabel

Check-in [abd5404398]
Login
Overview
Comment:Consider all multifunctions with a default branch to be exhaustive.
Timelines: family | ancestors | descendants | both | int-literals-in-pattern-match
Files: files | file ages | folders
SHA3-256: abd5404398ea05eca952340103d4be70a52190021b22ded658615ffc36bace02
User & Date: robin.hansen on 2021-09-24 09:33:44
Other Links: branch diff | manifest | tags
Context
2021-09-24
09:35
Integers can now be represented directly in multifunction pattern matching. [c2996a5e70] check-in: 71f2929943 user: robin.hansen tags: trunk
09:33
Consider all multifunctions with a default branch to be exhaustive. Closed-Leaf check-in: abd5404398 user: robin.hansen tags: int-literals-in-pattern-match
2021-09-23
16:51
Codegen should be fixed. But the exhaustiveness checker still has bugs. check-in: cc2965ccda user: robin.hansen tags: int-literals-in-pattern-match
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Modified src/Stabel/Parser.elm from [bbf63e8a58] to [0ae4b446a0].

63
64
65
66
67
68
69

70
71
72
73
74
75
76
    , imports : Dict String (List String)
    , implementation : FunctionImplementation
    }


type FunctionImplementation
    = SoloImpl (List AstNode)

    | MultiImpl (List ( TypeMatch, List AstNode )) (List AstNode)


type TypeMatch
    = TypeMatchInt SourceLocationRange Int
    | TypeMatchType SourceLocationRange PossiblyQualifiedType (List ( String, TypeMatch ))








>







63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
    , imports : Dict String (List String)
    , implementation : FunctionImplementation
    }


type FunctionImplementation
    = SoloImpl (List AstNode)
      -- TODO: Default branch should be a (Maybe (List AstNode))
    | MultiImpl (List ( TypeMatch, List AstNode )) (List AstNode)


type TypeMatch
    = TypeMatchInt SourceLocationRange Int
    | TypeMatchType SourceLocationRange PossiblyQualifiedType (List ( String, TypeMatch ))

Modified src/Stabel/TypeChecker.elm from [e970f167c0] to [8902188c94].

413
414
415
416
417
418
419



420
421
422
423
424
425
426
...
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
....
1107
1108
1109
1110
1111
1112
1113
1114
1115




1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
                    case inferredDefaultType.input of
                        [] ->
                            ( Qualifier.TypeMatchType SourceLocation.emptyRange (Type.Generic "*") [], defaultImpl ) :: initialWhens

                        firstType :: _ ->
                            ( Qualifier.TypeMatchType SourceLocation.emptyRange firstType [], defaultImpl ) :: initialWhens




        whens =
            List.map (Tuple.mapFirst (resolveWhenConditions untypedDef)) allBranches

        ( inferredWhenTypes, newContext ) =
            whens
                |> List.foldr (inferWhenTypes untypedDef) ( [], context )
                |> Tuple.mapFirst normalizeWhenTypes
................................................................................
            if whensAreConsistent && whensAreCompatible then
                Nothing

            else
                Just <| InconsistentWhens sourceLocation untypedDef.name

        maybeInexhaustiveError =
            inexhaustivenessCheck sourceLocation whenPatterns

        sourceLocation =
            Maybe.withDefault SourceLocation.emptyRange untypedDef.sourceLocation

        typedDef =
            { name = untypedDef.name
            , sourceLocation = untypedDef.sourceLocation
................................................................................


type InexhaustiveState
    = Total
    | SeenInt


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 (InexhaustiveMultiFunction range inexhaustiveStates)


inexhaustivenessCheckHelper : List Type -> Qualifier.TypeMatch -> List ( List Type, InexhaustiveState ) -> List ( List Type, InexhaustiveState )
inexhaustivenessCheckHelper typePrefix typeMatch acc =
    let
        ( t, intLiteral, conds ) =
            case typeMatch of







>
>
>







 







|







 







|
|
>
>
>
>
|
|
|
|
|
|
|
|
|

|
|







413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
...
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
....
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
                    case inferredDefaultType.input of
                        [] ->
                            ( Qualifier.TypeMatchType SourceLocation.emptyRange (Type.Generic "*") [], defaultImpl ) :: initialWhens

                        firstType :: _ ->
                            ( Qualifier.TypeMatchType SourceLocation.emptyRange firstType [], defaultImpl ) :: initialWhens

        hasDefaultBranch =
            not <| List.isEmpty defaultImpl

        whens =
            List.map (Tuple.mapFirst (resolveWhenConditions untypedDef)) allBranches

        ( inferredWhenTypes, newContext ) =
            whens
                |> List.foldr (inferWhenTypes untypedDef) ( [], context )
                |> Tuple.mapFirst normalizeWhenTypes
................................................................................
            if whensAreConsistent && whensAreCompatible then
                Nothing

            else
                Just <| InconsistentWhens sourceLocation untypedDef.name

        maybeInexhaustiveError =
            inexhaustivenessCheck sourceLocation hasDefaultBranch whenPatterns

        sourceLocation =
            Maybe.withDefault SourceLocation.emptyRange untypedDef.sourceLocation

        typedDef =
            { name = untypedDef.name
            , sourceLocation = untypedDef.sourceLocation
................................................................................


type InexhaustiveState
    = Total
    | SeenInt


inexhaustivenessCheck : SourceLocationRange -> Bool -> List Qualifier.TypeMatch -> Maybe Problem
inexhaustivenessCheck range hasDefaultBranch patterns =
    if hasDefaultBranch then
        Nothing

    else
        let
            inexhaustiveStates =
                List.foldl (inexhaustivenessCheckHelper []) [] patterns
                    |> List.filter (\( _, state ) -> state /= Total)
                    |> List.map Tuple.first
        in
        case inexhaustiveStates of
            [] ->
                Nothing

            _ ->
                Just (InexhaustiveMultiFunction range inexhaustiveStates)


inexhaustivenessCheckHelper : List Type -> Qualifier.TypeMatch -> List ( List Type, InexhaustiveState ) -> List ( List Type, InexhaustiveState )
inexhaustivenessCheckHelper typePrefix typeMatch acc =
    let
        ( t, intLiteral, conds ) =
            case typeMatch of

Modified tests/Test/TypeChecker/Errors.elm from [9bf4cbb6a5] to [92b4c5c362].

344
345
346
347
348
349
350



















351
352
353
354
355
356
357
                                Problem.InexhaustiveMultiFunction _ [ [ Type.Custom "IntBox", Type.Int ] ] ->
                                    True

                                _ ->
                                    False
                    in
                    checkForError inexhaustiveError input



















            , test "A total branch should remove any earlier seen branch" <|
                \_ ->
                    let
                        input =
                            """
                            def: main
                            : 2 mword







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







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
                                Problem.InexhaustiveMultiFunction _ [ [ Type.Custom "IntBox", Type.Int ] ] ->
                                    True

                                _ ->
                                    False
                    in
                    checkForError inexhaustiveError input
            , test "Default clause is exhaustive in case of nested match" <|
                \_ ->
                    let
                        input =
                            """
                            defstruct: Box
                            : value Int

                            def: main
                            : 2 >Box mword

                            defmulti: mword
                            : Box( value 1 )
                              drop 1
                            else: 
                              drop 0
                            """
                    in
                    Util.expectTypeCheck input
            , test "A total branch should remove any earlier seen branch" <|
                \_ ->
                    let
                        input =
                            """
                            def: main
                            : 2 mword