~plan/plunder

291a06c8146f058bb8f3ef3e8829905cd85de903 — Sol 4 months ago 5cddaf5
viceroy: more #case validation

- Check exaustivity
- Disallow fallback patterns in exaustive matches.
- Disallow binding multiple fields with the same name.
1 files changed, 129 insertions(+), 38 deletions(-)

M sire/viceroy.sire
M sire/viceroy.sire => sire/viceroy.sire +129 -38
@@ 67,14 67,18 @@
;;;;
;;;; DONE Write code to lookup information about constructors.
;;;;
;;;; TODO Add support for a fallback case to the #case parser.
;;;; TODO Add support for a fallback case to the #case code generator.
;;;; DONE Add support for a fallback case to the #case parser.
;;;; DONE Add support for a fallback case to the #case code generator.
;;;; DONE Generate a default fallback-case if none is specified.
;;;;
;;;; DONE Validate that all branches of a #case are from the same ADT.
;;;; DONE Validate that the number of fields of each branch matches the ADT.
;;;; DONE Validate that no two branches of a #case are the same constructor.
;;;; TODO Validate that all branches of an ADT are handled.
;;;; TODO Validate that ADT-branch field names are not repeated (per branch).
;;;;
;;;; DONE Validate that all branches of an ADT are handled.
;;;; DONE Validate that ADT-branch field names are not repeated (per branch).
;;;; DONE If all cases are handled, do not accept a fallback case.
;;;;
;;;; TODO Validate that the scrutinee has the same type as the ADT.
;;;; TODO Collect the field-types associated with each field-binding.
;;;; TODO Construct the type-environment for the body of each branch.


@@ 140,7 144,7 @@
- EREF Str
- EAPP Exp Exp
- ETUP Row-Exp
- ECAS Exp Row-(CaseBranchE Exp)
- ECAS Exp Row-(CaseBranchE Exp) (Maybe e)
- ELET nm/Str vTy/Typ v/Exp b/Exp
- EFUN inline/Bit pin/Bit nm/Str Row-(Exp,Typ) rTy/Typ b/Exp



@@ 393,10 397,19 @@ abstype#SireState
> Str > Nat
(lookupCnstrTag sym)=sym

> _ > Rex > (Str, Row Maybe-Str, Exp)
> _ > Rex > (Row (Str, Row Maybe-Str, Exp), Maybe Exp)
= (readCaseBranches readExp rex)
: item < foreach | listToRow | tarSeq {-} rex
| readCaseBranch readExp item
@ branches
    | map (readCaseBranch readExp) | listToRow | tarSeq {-} rex
@ fallbacks | filter (n,_,_)&(n == "_") branches
@ branches  | filter (n,_,_)&(n /= "_") branches
^ [branches _]
# switch (len fallbacks)
* _ | failStr rex {multiple fallback cases}
* 0 | NONE
* 1 @ [[_ fields expr]] fallbacks
    | if (null fields) (SOME expr)
    | failStr rex {fallback case cannot have fields!}

(traceShowIdWith tag x)=(trk [tag x] x)
(traceShowId x)=(trk x x)


@@ 414,9 427,8 @@ abstype#SireState
    | if (nKids /= 3)
        | failStr rex {#case expects three params}
    | traceShowIdWith "HERE"
    | ECAS
    * readExp scrutRex
    * readCaseBranches readExp branchesRex
    @ (branches, fallback) | readCaseBranches readExp branchesRex
    | ECAS (readExp scrutRex) branches fallback

= (readExp rex)
# switch (rexType rex)


@@ 673,6 685,7 @@ abstype#SireState
@ (onDup dup)    | failStr rex {overlapping branch}
| if null-cNames | []
^ maybeCase (findDup cNames) _ onDup
^ [adt1 _]
: cNm < foreach cNames
@ adt@(PIN (ty, cnstrs)) (lookupAdt ss cNm)
| trk [=adt]


@@ 680,26 693,53 @@ abstype#SireState
    | failStr rex {two branches from different ADTs}
@ c@[tag fieldTys] (tabGet cnstrs cNm)
| ifz c
    | failStr rex {internal error: failed to lookup constructor information}
    | failStr rex
    | {internal error: failed to lookup constructor information}
| trk [=tag =fieldTys]
| [tag fieldTys]

> SireState > _ > _ > Exp > Tab Nat (Row (Maybe Str), Exp) > Sire
= (compileCase ss go e scrut branches)
= (badCase adt)
| trk [adt=(pinItem adt)]
^ die (strCat _)
++ {unhandled case when pattern-matching on }
++ lawName (pinItem (snd (fst (pinItem adt))))

(defaultFallback adt)=(A K-badCase K-adt)

= (checkExaustivity (PIN [ty cnstrs]) info branches mFall)
@ rex       | `(#case)
@ cnstrSet  | tabKeysSet cnstrs
@ branchSet | setFromRow (map fst branches)
| if (cnstrSet == branchSet)
    | if (mFall == NONE) TRUE
    | failStr rex {Fallback case is redundate because all cases are handled}
| else
    | if (mFall /= NONE) TRUE
    | fail rex
    ` # Non-Exaustive #case
      - {Missing constructors:} $$(setToRow | setSub cnstrSet branchSet)

> SireState > _ > _ > Exp > Tab Nat (Row (Maybe Str), Exp) > Maybe Exp > Sire
= (compileCase ss go e scrut branches mFall)
@ (binds, envs) | caseBinds (go e scrut) branches
@ info          | getBranchInfo ss branches
@ (adt, info)   | getBranchInfo ss branches
| seq           | checkExaustivity adt info branches mFall
@ fall          | maybeCase mFall (defaultFallback adt) f&(go e f)
^ foldr L _ binds
| switchSire (A K-dataTag V-(len binds)) K-{TODO: fallback}
| switchSire (A K-dataTag V-(len binds)) fall
| tabFromPairs
: [[[cNm binds x] enu] [tag fieldTys]]
    < foreach (zip (zip branches envs) info)
^ : dup < maybeCase (findDup | catMaybes binds) _
  | failStr (symToRex dup) {duplicate field name in #case}
@ cnstrArity | len fieldTys
@ boundArity | len binds
| if (cnstrArity /= boundArity)
    | fail (symToRex cNm)
    ` # Arity mismatch in pattern-match
      - The constructor has $(natToRex cnstrArity) fields
      - The pattern-match binds $(natToRex boundArity) fields
    `
        # Arity mismatch in pattern-match
        - The constructor has $(natToRex cnstrArity) fields
        - The pattern-match binds $(natToRex boundArity) fields
| (tag, go (listWeld listFromRowRev-enu e) x)




@@ 717,13 757,16 @@ abstype#SireState
    ? (go e exp)
    # case exp

    - EBIT n    | K n
    - ENAT n    | K n
    - EAPP a b  | A (go e a) (go e b)
    - EADD a b  | addSire (go e a) (go e b)
    - EEQL a b  | eqlSire (go e a) (go e b)
    - ETUP xs   | rowSire (map go-e xs)
    - ECAS s bs | traceShowIdWith "OUTPUT" | compileCase ss go e s (traceShowIdWith {BULLSHIT} bs)
    - EBIT n   | K n
    - ENAT n   | K n
    - EAPP a b | A (go e a) (go e b)
    - EADD a b | addSire (go e a) (go e b)
    - EEQL a b | eqlSire (go e a) (go e b)
    - ETUP xs  | rowSire (map go-e xs)

    - ECAS s bs f
        | traceShowIdWith "OUTPUT"
        | compileCase ss go e s (traceShowIdWith {BULLSHIT} bs) f

    - EREF x
        @ rex (WORD x 0)


@@ 749,18 792,23 @@ abstype#SireState
      | L (A K-(idx 2) V-1)
      | L (A K-(idx 3) V-2)
      | L (A K-(idx 5) V-3)
      ^ apple K-tabSwitch (A K-dataTag V-4, K-{TODO: fallback}, tabSire _)
      ^ apple K-tabSwitch (A K-dataTag V-4, K-{fallback}, tabSire _)
     ## =FOO | addSire V-2 V-1
     ## =BAR | V-0

  @ adt
      ^ PIN [Nat _]
     ## =FOO ({FOO}, [TNAT TNAT TNAT])
     ## =BAR ({BAR}, [TNAT TNAT TNAT TNAT TNAT])
     ## =ZAZ ({ZAZ}, [])

  @ scope
      ## =FOO | PIN [3 %plan %sire %ctx {FOO} [{adt} adt]]
      ## =BAR | PIN [4 %plan %sire %ctx {BAR} [{adt} adt]]
  ^ | compile (5, {REPL}, scope, #[])
    | ECAS ENAT-{ADT} _

  | compile (5, {REPL}, scope, #[])

  ^ ECAS ENAT-{ADT} _ (SOME ENAT-{fallback})
 ++ ("FOO", [NONE SOME-{x} SOME-{y}], EADD EREF-{x} EREF-{y})
 ++ ("BAR", [NONE NONE NONE NONE SOME-{z}], EREF-{z})



@@ 808,9 856,11 @@ abstype#SireState
  # expected=($(showType | viceType expected))
  # actual=($(showType | viceType ty))

= (showTypedSym [sym vty])
` ($(symToRex sym))/($(showType | viceType vty))


= (showCaseBranches showExp bs)
= (showCase showExp x bs mFall)
| NEST "#" ('case, showExp x)
^ bloodline | listFromRow | map _ bs
& (cnstr, fields, body)
^ NEST {-} (cat _) 0


@@ 818,9 868,6 @@ abstype#SireState
++ map x&(maybeCase x "_" n&n) fields
++ showExp body

= (showTypedSym [sym vty])
` ($(symToRex sym))/($(showType | viceType vty))

= (showExp exp)
    # case exp
    - EREF n       | WORD n 0


@@ 830,7 877,7 @@ abstype#SireState
    - EADD a b     | `($(showExp a) .+ $(showExp b))
    - EAPP a b     | `($(showExp a) $(showExp b))
    - ETUP xs      | NEST "," (map showExp xs) 0
    - ECAS x bs    | NEST "#" ('case, showExp x) (showCaseBranches showExp bs)
    - ECAS x bs f  | showCase showExp x bs f
    - _            | {showExp: malformed exp} exp

    - ELET name ty val body


@@ 894,7 941,7 @@ abstype#SireState
        | seq (go e SOME-ty val)
        | go (tabPut e nm ty) mExpect body

    - ECAS _ _
    - ECAS _ _ _
        | maybeCase mExpect TNAT id

    - EFUN inlined pinned name args resTy body


@@ 1219,13 1266,25 @@ s3=(SOME 3)
(#| dataTag s3)

= ex & (x/Nat >Nat)
     # case x
     - NONE   | 1
     - SOME x | inc x

#= maybeNatAdt
#| PIN
#| v2 MaybeNat
#| %[NONE SOME]
#| v2 (#| v2 %SOME (#| v1 TNAT))
      (#| v2 %NONE v0)

= ex & (x/Nat >Nat)
     # case (SOME x)
     - NONE   | 1
     - SOME x | inc x

#=?= ex
   #& a
   #| tabSwitch (#| dataTag a) {TODO: fallback}
   #| tabSwitch (#| dataTag a) (#| badCase maybeNatAdt)
   #| %[SOME NONE]
   #| c2 1 (#| inc (#| idx 1 a))



@@ 1243,7 1302,39 @@ s3=(SOME 3)
     - NONE   | 1
     - SOME x | inc x

#= maybeNatAdt
#| PIN
#| v2 MaybeNat
#| %[NONE SOME]
#| v2 (#| v2 1 (#| v1 TNAT))
      (#| v2 0 v0)


#=?= ex
   #& a
   #| switch (#| dataTag a) {TODO: fallback}
   #| switch (#| dataTag a) (#| badCase maybeNatAdt)
   #| c2 (#| inc (#| idx 1 a)) 1


;;; Testing Fallback Handlers ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= ex & (x/Nat >Nat)
     # case (SOME x)
     - NONE   | 1
     - _      | 2

#=?= ex
   #& a
   #| switch (#| dataTag a) 2
   #| c1 1


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

# data FooBar
- FOO Nat Nat
- BAR Nat Nat Nat

# case (FOO 3 4)
- FOO x y | x
- _       | 3