~plan/plunder

00f06bafd17ec53ddfa37469066072b39cc7ea84 — Sol 4 months ago 63ee536
viceroy: adt metadata in props, -legible #data

-   Metadata about the shape of each ADT is now stored in the props of
    each constructor.

-   #data now supports the -legible flag.

-   Empty #data declarations are allowed.

-   #data declarations are prevented from having multiple branches with
    the same constructor name.
1 files changed, 94 insertions(+), 39 deletions(-)

M sire/viceroy.sire
M sire/viceroy.sire => sire/viceroy.sire +94 -39
@@ 50,7 50,7 @@
;;;;     - BAR x y z | b1
;;;;     - ZAZ x y   | b2
;;;;
;;;; TODO Datatypes store metadata in props
;;;; DONE Datatypes store metadata in props
;;;;
;;;;     constructor=[%tag1 (PIN [(Type a) %tag1 FOO [Nat Nat] %tag2 BAR [a]])]
;;;;


@@ 60,10 60,16 @@
;;;;     + %tag1 FOO [Nat Nat]
;;;;     + %tag2 BAR [0]
;;;;
;;;; DONE Verify that #data commands don't contain duplicate constructors.
;;;; DONE Verify that empty (#data) commands work correctly (creates void type)
;;;; DONE (DATA) command supports both legible and compact tags
;;;; DONE (#data) parser supports (-legible) config.
;;;;
;;;; TODO Write code to lookup information about constructors.
;;;;
;;;; TODO Add support for a fallback case to the parser.
;;;; TODO Add support for a fallback case to the code generator.
;;;; 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.
;;;; TODO Validate that all branches of an ADT are handled.


@@ 79,14 85,10 @@
;;;; TODO Multi-Command Blocks
;;;; TODO Multi-Bind Commands
;;;;
;;;; TODO Type annotations
;;;; TODO Type annotations on Expressions
;;;;
;;;;     x/Nat y/(Row Nat) x/(Nat, Nat)
;;;;
;;;; TODO Record Syntax: [x=3 y=3 z=3]
;;;; TODO Record Compiler
;;;; TODO Record Type-Checking
;;;;
;;;; TODO Arrays: Array(...), Array#(...), # Array ...
;;;;
;;;; TODO Strict let bindings


@@ 99,11 101,13 @@
;;;;     @ [x/Nat y/Nat z/Nat] (3, 4, 5)
;;;;     x
;;;;
;;;; TODO Record destructuring:
;;;; Actual Docs
;;;; ===========
;;;;
;;;;     @ [x=(x/Nat) y=(y/Nat) z=(z/Nat)] point
;;;;     x
;;;; Each constructor has an {adt} property which is an array which is
;;;; packed into this layout:
;;;;
;;;;     [typeName constructorName tag fields constructorName tag fields ...]


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


@@ 148,7 152,7 @@
- EVAL Exp
- BIND Str Exp
- ASSERT Exp
- DATA Str (Row Constructor)
- DATA Bit Str (Row Constructor)
- CHK_EQ Exp Exp

; TODO: This belongs elsewhere.


@@ 370,7 374,7 @@ abstype#(Bst k v)
= (readCaseBranch readExp rex)
@ rune (rexRune rex)
@ kids (rexKids rex)    ;;  TODO: This needs to validate lengths
@ nKid (len kids)       ;;  TODO: Good err-msg in case of non-hep items
@ nKid (len kids)       ;;  TODO: Good err-msg in case of non-{-} items
@ last dec-nKid
@ patSyms | map readSym (take last kids)
@ body    | readExp (idx last kids)


@@ 469,12 473,23 @@ abstype#(Bst k v)
# switch keyword
* _ | failStr rex (strWeld {unknown keyword: } keyword)
* {data}
    @ [_ typeNameRex cnstrsRex] kids
    | if (nKids /= 3)
    | if (nKids == 2)
        @ [_ tyRex] kids
        | DATA FALSE (readSym tyRex) []
    | if (nKids == 4)
        @ [_ tyRex flagRex csRex] kids
        @ !typeName | readSym tyRex
        @ !cnstrs   | readConstructors csRex
        @ !legible  | if (flagRex == '(-legible)) TRUE
                    | failStr flagRex {expected -legible flag}
        | DATA legible typeName cnstrs
    | if (nKids == 3)
        @ [_ tyRex csRex] kids
        @ !typeName | readSym tyRex
        @ !cnstrs   | readConstructors csRex
        | DATA FALSE typeName cnstrs
    | else
        | failStr rex {#data expects three params}
    @ !typeName (readSym typeNameRex)
    @ !cnstrs   (readConstructors cnstrsRex)
    | DATA typeName cnstrs
* _
    | EVAL (readExp rex)



@@ 629,7 644,7 @@ abstype#(Bst k v)
^ foldr L _ binds
| switchSire (A K-dataTag V-(len binds)) K-{TODO: fallback}
| tabFromPairs
| trk [=branches =binds =envs]
; trk [=branches =binds =envs]
: [[_ tag _ x] enu] < foreach (zip branches envs)
| (tag, go (listWeld listFromRowRev-enu e) x)



@@ 917,40 932,41 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
;;; Creating ADT Constructors ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

> Typ > Row (Nat, Constructor) > Row (Str, Sire, Typ, Bst Str Any)
= (adtBinds newtype branches)
: (tag, cnstr@(name, fieldTypes)) < foreach branches
= (adtBinds adt newtype branches)
: (name, tag, fieldTypes) < foreach branches
@ arity | len fieldTypes
@ type  | foldr TFUN newtype fieldTypes
^ (name, _, type, bstEmpty)
^ (name, _, type, bstSing {adt} adt)
| ifz arity (K tag)
^ F (LAM 1 1 0 name arity _)
| rowSire | rowCons K-tag | gen arity i&(V (sub arity inc-i))

= (recordBind newtype (tag, cnstr@(name, fieldTypes)))
= (recordBind adt newtype cnstr@(name, tag, fieldTypes))
; trk [=cnstr]
@ arity     | len fieldTypes
@ type      | foldr TFUN newtype fieldTypes
| ifz arity | adtBinds [(tag, cnstr)]
^ (name, _, type, bstEmpty)
| ifz arity | adtBinds adt newtype [cnstr]
^ (name, _, type, bstSing {adt} adt)
^ F (LAM 1 1 0 name arity _)
| rowSire | gen arity i&(V (sub arity inc-i))

> Typ > Row (Nat, Constructor) > Row (Str, Sire, Typ, Bst Str Any)
= (constructorBinds newtype branches)
= (constructorBinds adt newtype branches)
| if (len branches == 1)
* [(recordBind newtype (idx 0 branches))]
* adtBinds newtype branches
* [(recordBind adt newtype (idx 0 branches))]
* adtBinds adt newtype branches

=?=  ++  ++ {FOO}
         ++ F-(LAM 1 1 0 {FOO} 2 (rowSire [K-{tag1} V-1 V-0]))
         ++ (TFUN TNAT (TFUN TNAT TNAT))
         ++ 0
         ++ (bstSing {adt} {ADT-HERE})
     ++  ++ {BAR}
         ++ K-{tag2}
         ++ TNAT
         ++ 0
  | constructorBinds TNAT
 ++ ({tag1}, ({FOO}, [TNAT TNAT]))
 ++ ({tag2}, ({BAR}, []))
         ++ (bstSing {adt} {ADT-HERE})
  | constructorBinds {ADT-HERE} TNAT
 ++ ({FOO}, {tag1}, [TNAT TNAT])
 ++ ({BAR}, {tag2}, [])


;;; Executing Commands ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


@@ 958,17 974,37 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
= (doBind ss@(nex, ctx, binds, mods) bind@(name, sire, vty, props))

    @ type  | viceType vty
    ; trk [=props]
    @ props | bstSave (bstPut props {type} type)
    @ plan  | evalSire sire
    @ bind  | PIN [nex plan sire ctx name props]
    @ ss    | (inc nex, ctx, tabPut binds name bind, mods)

    | trk ` > $(showType type)
            ; $$props
            = $(WORD name 0) $$plan
            \ $$props

    ; 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
| fail rex `[{duplicate constructor name:} $(WORD dup 0)]

= (execute rex ss@(nex, ctx, binds, mods) cmd)



@@ 998,13 1034,21 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
                     # expected $$1 but got
                     $$plan

    - DATA typeName cnstrs
    - DATA legible typeName cnstrs

        @ (newtype, ss) | mkNewType typeName 0 ss

        @ ss ^ foldl doBind ss (constructorBinds (TDAT newtype) _)
             : c@(nm,tys) < foreach cnstrs
             | (nm, (nm, tys))
        @ branches : (i, (nm, tys)) < foreach (rowIndexed cnstrs)
                   | (nm, if legible nm i, tys)

        | seq (checkForADTDups rex branches)

        ; TODO: Pin this (annoying for debugging but good for per)
        @ adt | rowCons newtype | cat | sortOn (idx 0) branches
        | trk [=adt]

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

        | doBind ss (typeName, K-newtype, TTYP, bstEmpty)



@@ 1021,7 1065,10 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
        | doBind ss (name, sire, type, bstEmpty)

| execute 'lol (3, {REPL}, #[] #[])
| DATA {MaybeNat} (({SOME}, [TNAT]), ({NONE}, []))
| DATA FALSE {MaybeNat}
++ ({SOME}, [TNAT])
++ ({NONE}, [])
++ ({x}, [])

(viceroy ss rex err ok)=(ok (execute rex ss (readCmd rex)) '(#*))



@@ 1131,3 1178,11 @@ s3=(SOME 3)
   #| tabSwitch (#| dataTag a) {TODO: fallback}
   #| %[SOME NONE]
   #| c2 1 (#| inc (#| idx 1 a))

# data MaybeNat -legible
- NONE
- SOME Nat

s3=(SOME 3)

data#Void