~plan/plunder

5cddaf5ae05c1d57e39c06fd4d46fb3305e54fd6 — Sol 4 months ago 00f06ba
viceroy: #case looks up metadata, validates

{#case} now lookup up the ADT information about each constructor,
and validates the expression in several ways:

-   Each pattern corresponds to an actual #datatype constructor.

-   All of the patterns are from the same datatype.

-   No two patterns are for the same branch.

-   The number of fields bound on each branch matches the constructor.
1 files changed, 126 insertions(+), 65 deletions(-)

M sire/viceroy.sire
M sire/viceroy.sire => sire/viceroy.sire +126 -65
@@ 65,15 65,15 @@
;;;; DONE (DATA) command supports both legible and compact tags
;;;; DONE (#data) parser supports (-legible) config.
;;;;
;;;; TODO Write code to lookup information about constructors.
;;;; 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.
;;;;
;;;; TODO Validate that all branches of a #case are from the same ADT.
;;;; TODO Validate that the number of fields of each branch matches the ADT.
;;;; 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 no two branches of a #case are the same constructor.
;;;; TODO Validate that ADT-branch field names are not repeated (per branch).
;;;; TODO Validate that the scrutinee has the same type as the ADT.
;;;; TODO Collect the field-types associated with each field-binding.


@@ 107,7 107,7 @@
;;;; Each constructor has an {adt} property which is an array which is
;;;; packed into this layout:
;;;;
;;;;     [typeName constructorName tag fields constructorName tag fields ...]
;;;;     (ty:Type tab:(Tab Str (Tag, Fields)))


;;; Imports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


@@ 130,7 130,7 @@
- TTUP Row-Typ
- TDAT Type

# typedef (CaseBranchE e) (Str, Nat, Row Maybe-Str, e)
# typedef (CaseBranchE e) (Str, Row Maybe-Str, e)

# data Exp -legible
- EADD Exp Exp


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



@@ 155,10 155,18 @@
- DATA Bit Str (Row Constructor)
- CHK_EQ Exp Exp

; TODO: This belongs elsewhere.
; TODO: These belong elsewhere.

abstype#Sire
abstype#(Bst k v)
abstype#SireState


;;; Misc Rex Rendering ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(symToRex s)=(WORD s 0)

(natToRex n)=(WORD (showNat n) 0)


;;; Error Handling ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


@@ 385,12 393,10 @@ abstype#(Bst k v)
> Str > Nat
(lookupCnstrTag sym)=sym

> _ > Rex > (Str, Nat, Typ, Row Maybe-Str, Exp)
> _ > Rex > (Str, Row Maybe-Str, Exp)
= (readCaseBranches readExp rex)
: item      < foreach | listToRow | tarSeq {-} rex
@ [cn fs b] | readCaseBranch readExp item
@ tag       | lookupCnstrTag cn
| (cn, tag, fs, b)
: item < foreach | listToRow | tarSeq {-} rex
| readCaseBranch readExp item

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


@@ 601,7 607,7 @@ abstype#(Bst k v)
> Row CaseBranch > Set Nat
= (caseSlots branches)
^ foldl _ %[] branches
& (need branch@(_c, _t, fields, _))
& (need branch@(_c, fields, _))
^ setWeld need (setFromRow | catMaybes _)
: [i [mf _]] < foreach (rowIndexed fields)
| ifz mf NONE (SOME i)


@@ 618,15 624,15 @@ abstype#(Bst k v)
    | A K-(idx | inc fieldIx) V-(inc bindNum)
++
    ^ map _ branches
    & (_c, _t, fields, expr)
    & (_c, fields, expr)
    | sizedListToRow numBinds
    | (NONE :: listMap (get fields) (setToList slots))

; type CaseBranch (Str, Nat, Row Maybe-Str, Exp)

=?= %[1 2 4]
  | caseSlots ++ ("FOO", 3, [0 SOME-{x} SOME-{y}], EREF-{y})
              ++ ("BAR", 9, [0 0 0 0 SOME-{z}], EREF-{z})
  | caseSlots ++ ("FOO", [0 SOME-{x} SOME-{y}], EREF-{y})
              ++ ("BAR", [0 0 0 0 SOME-{z}], EREF-{z})

=?=  ++   ++ K {lol}
          ++ A K-(idx 2) V-1


@@ 635,17 641,65 @@ abstype#(Bst k v)
     ++   ++ [0 SOME-{x} SOME-{y} 0]
          ++ [0 0 0 SOME-{z}]
  | caseBinds K-{lol}
 ++ ("FOO", 3, [0 SOME-{x} SOME-{y}], EREF-{y})
 ++ ("FOO", 9, [0 0 0 0 SOME-{z}], EREF-{z})
 ++ ("FOO", [0 SOME-{x} SOME-{y}], EREF-{y})
 ++ ("FOO", [0 0 0 0 SOME-{z}], EREF-{z})

= (lookupAdt ss nm)
@ rex (WORD nm 0)
@ bad (failStr rex {this is not an ADT constructor})
: _ _ bind@[_ _ _ _ _ props] < getBind nm ss rex failStr
| maybeCase (btSearch {adt} props) bad id

= (findDup row)
@ res
    ^ foldr _ %[] row
    & (i seen)
    | if isNat-seen seen
    | if (setHas i seen) i (setIns i seen)
| if isNat-res (SOME res) NONE

> _ > _ > Exp > Tab Nat (Row (Maybe Str), Exp) > Sire
= (compileCase go e scrut branches)
=?= SOME-1 (findDup [2 1 1])
=?= NONE   (findDup [2 1 3])
=?= NONE   (findDup [])
=?= NONE   (findDup [1])
=?= SOME-1 (findDup [1 1])

;; TODO: ugly code, find some way to make this much more legible.

= (getBranchInfo ss branches)
@ rex            | '(#case)
@ cNames         | map fst branches
@ adt1           | lookupAdt ss (fst cNames)
@ (onDup dup)    | failStr rex {overlapping branch}
| if null-cNames | []
^ maybeCase (findDup cNames) _ onDup
: cNm < foreach cNames
@ adt@(PIN (ty, cnstrs)) (lookupAdt ss cNm)
| trk [=adt]
| if (adt /= adt1)
    | failStr rex {two branches from different ADTs}
@ c@[tag fieldTys] (tabGet cnstrs cNm)
| ifz c
    | 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)
@ (binds, envs) | caseBinds (go e scrut) branches
@ info          | getBranchInfo ss branches
^ foldr L _ binds
| switchSire (A K-dataTag V-(len binds)) K-{TODO: fallback}
| tabFromPairs
; trk [=branches =binds =envs]
: [[_ tag _ x] enu] < foreach (zip branches envs)
: [[[cNm binds x] enu] [tag fieldTys]]
    < foreach (zip (zip branches envs) info)
@ 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
| (tag, go (listWeld listFromRowRev-enu e) x)




@@ 669,7 723,7 @@ abstype#(Bst k v)
    - 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 go e s bs
    - ECAS s bs | traceShowIdWith "OUTPUT" | compileCase ss go e s (traceShowIdWith {BULLSHIT} bs)

    - EREF x
        @ rex (WORD x 0)


@@ 696,12 750,19 @@ abstype#(Bst k v)
      | 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 _)
     ## =3 | addSire V-2 V-1
     ## =9 | V-0
  ^ | compile (5, {REPL}, #[], #[])
     ## =FOO | addSire V-2 V-1
     ## =BAR | V-0
  @ adt
      ^ PIN [Nat _]
     ## =FOO ({FOO}, [TNAT TNAT TNAT])
     ## =BAR ({BAR}, [TNAT TNAT TNAT TNAT TNAT])
  @ 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} _
 ++ ("FOO", 3, [NONE SOME-{x} SOME-{y}], EADD EREF-{x} EREF-{y})
 ++ ("BAR", 9, [NONE NONE NONE NONE SOME-{z}], EREF-{z})
 ++ ("FOO", [NONE SOME-{x} SOME-{y}], EADD EREF-{x} EREF-{y})
 ++ ("BAR", [NONE NONE NONE NONE SOME-{z}], EREF-{z})


;;; Type-Checking ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


@@ 751,16 812,14 @@ abstype#(Bst k v)

= (showCaseBranches showExp bs)
^ bloodline | listFromRow | map _ bs
& (cnstr, tag, fields, body)
& (cnstr, fields, body)
^ NEST {-} (cat _) 0
++ [(WORD 0 cnstr)]
++ map x&(maybeCase x "_" n&n) fields
++ showExp body

(showSym s)=(WORD s 0)

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

= (showExp exp)
    # case exp


@@ 987,20 1046,6 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
    ; trk [bind=(pinItem bind) =props]
    ss

= (findDup row)
@ res
    ^ foldr _ %[] row
    & (i seen)
    | if isNat-seen seen
    | if (setHas i seen) i (setIns i seen)
| if isNat-res (SOME res) NONE

=?= SOME-1 (findDup [2 1 1])
=?= NONE   (findDup [2 1 3])
=?= NONE   (findDup [])
=?= NONE   (findDup [1])
=?= SOME-1 (findDup [1 1])

= (checkForADTDups rex branches)
@ names | map idx-0 branches
: dup   < maybeCase (findDup names) 0


@@ 1043,9 1088,9 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))

        | seq (checkForADTDups rex branches)

        ; TODO: Pin this (annoying for debugging but good for per)
        @ adt | rowCons newtype | cat | sortOn (idx 0) branches
        | trk [=adt]
        @ adt ^ PIN [newtype (tabFromPairs _)]
              : (n, t, fields) < foreach branches
              | (n, (t,fields))

        @ ss | foldl doBind ss
             | constructorBinds adt (TDAT newtype) branches


@@ 1145,15 1190,8 @@ t==true ; compare t to true, using the above information during
         # expected=Nat
         # actual=Bit

# data MaybeNat
- NONE
- SOME Nat

(NONE == SOME 3)
(NONE == NONE)
(SOME 1 == SOME 2)
(SOME 2 == SOME 2)
(SOME 2 == NONE)
;;; Record #data Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

# data Pair
- PAIR Nat Nat


@@ 1163,15 1201,27 @@ t==true ; compare t to true, using the above information during
(PAIR 3 4 == PAIR 3 4)
(PAIR 3 4 == PAIR 3 4)


;;; Examples ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

# data MaybeNat -legible
- NONE
- SOME Nat

(NONE == SOME 3)
(NONE == NONE)
(SOME 1 == SOME 2)
(SOME 2 == SOME 2)
(SOME 2 == NONE)

s3=(SOME 3)

(#| dataTag s3)

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

#=?= ex
   #& a


@@ 1179,10 1229,21 @@ s3=(SOME 3)
   #| %[SOME NONE]
   #| c2 1 (#| inc (#| idx 1 a))

# data MaybeNat -legible

;;; Same thing, but without -legible ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

# data MaybeNat
- NONE
- SOME Nat

s3=(SOME 3)

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

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