~plan/plunder

4e8879f33348c2c0b625cab2bc83666a78d0ca09 — Sol 4 months ago 02ee1bb
viceroy: letrec, recursive types, _-patterns
2 files changed, 203 insertions(+), 69 deletions(-)

M sire/pq.sire
M sire/viceroy.sire
M sire/pq.sire => sire/pq.sire +8 -12
@@ 35,14 35,6 @@
- LF
- BR a Pq Pq

= (pqCase t lf br)
# case t
- LF       | lf
- BR a l r | **br a l r

=?= 7 | pqCase (BR 7 LF LF) 3 (x l r & x)
=?= 3 | pqCase LF 3 (x l r & x)

= pqEmpty LF

= (pqNull t)


@@ 118,9 110,9 @@
= (heapify cmp ls)
^ _ (listLen ls) ls
? (go n vs)
| if (0 == n) [LF vs]
@ v (listUnsafeHead vs)
@ vs (listDrop 1 vs)
| ifz n    | [LF vs]
@ v        | listUnsafeHead vs
@ vs       | listDrop 1 vs
@ [t1 vs1] | go (div n 2) vs
@ [t2 vs2] | go (div (sub n 1) 2) vs1
| (siftDown cmp v t1 t2, vs2)


@@ 182,6 174,7 @@
            | add idx-0-p (listUnsafeHead idx-1-p)

; insert in descending order of key

=?= 110
  @ ls0 : x < listGen 11
        | (sub 10 x, repeat (sub 10 x))


@@ 190,7 183,10 @@
  | listSum : p < listForEach ls1
            | add idx-0-p (listUnsafeHead idx-1-p)


;;; Exports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

^-^
^-^ pqCase pqEmpty pqInsert pqDelMin pqMin pqNull
^-^ pqEmpty pqInsert pqDelMin pqMin pqNull
^-^ pqFromList pqToList pqSort
^-^

M sire/viceroy.sire => sire/viceroy.sire +195 -57
@@ 7,8 7,20 @@
;;;; Viceroy will eventually replace Stew, but it is still in it's
;;;; infancy.
;;;;
;;;; TODO Implement the (^) rune.
;;;; TODO Implement the (:) rune.
;;;; TODO Implement the (::) rune.
;;;; TODO Implement the (~) rune (and #List literals).
;;;;
;;;; DONE Implement the (@@) rune (LETREC bindings).
;;;; DONE _-patterns in LET bindings (not included in namespace).
;;;; DONE && rune (EAND)
;;;;
;;;; TODO Errors show location in the context of the whole block.
;;;;
;;;; TODO Compiler and type-checking errors should use the input rex
;;;; for the error context, not the pretty-printed AST.
;;;;
;;;; DONE Support Function Application
;;;;
;;;; DONE Parser for sequence literals.


@@ 98,6 110,7 @@
;;;;     x/Nat y/(Row Nat) x/(Nat, Nat)
;;;;
;;;; TODO Arrays: Array(...), Array#(...), # Array ...
;;;; TODO Arrays: Array(...), Array#(...), # Array ...
;;;;
;;;; DONE Strict let bindings (@ !x/Nat (add 2 3) 4)
;;;;


@@ 131,6 144,7 @@
- TTYP
- TNAT
- TBIT
- TREF Str
- TFUN Typ Typ
- TTUP Row-Typ
- TDAT Type


@@ 138,6 152,7 @@
# typedef (CaseBranchE e) (Str, Row Maybe-Str, e)

# data Pat -legible
- PCAB
- PVAR Str Typ
- PSEQ Pat



@@ 146,11 161,13 @@
- EBIT Bit
- ENAT Nat
- EEQL Exp Exp
- EAND Exp Exp
- EREF Str
- EAPP Exp Exp
- ETUP Row-Exp
- ECAS Exp Row-(CaseBranchE Exp) (Maybe e)
- ELET p/Pat v/Exp b/Exp
- EREC n/Str t/Typ v/Exp b/Exp
- EFUN inline/Bit pin/Bit nm/Str Row-(Exp,Typ) rTy/Typ b/Exp

# typedef CaseBranch (CaseBranchE Exp)


@@ 208,6 225,11 @@ abstype#SireState
   + 123
   + 0xAF

= (tarSeqSimple rune rex)
| ifz rex NIL
| if (rexRune rex /= rune) ~[rex]
| (rexSetHeir 0 rex :: tarSeqSimple rune (rexHeir rex))

= (tarSeq rune rex)
| ifz rex NIL
| if (rexRune rex /= rune) ~[rex]


@@ 297,7 319,13 @@ abstype#SireState
| if (len kids /= 2) | failStr rex {nonsense (==) rune}
| EEQL (readExp a) (readExp b)

= (readType rex)
; TODO: Support more items.
= (readAnd readExp rex)
@ kids@[a b]         | rexKids rex
| if (len kids /= 2) | failStr rex {nonsense (&&) rune}
| EAND (readExp a) (readExp b)

= (readType self rex)
# switch (rexType rex)
* _
    | failStr rex {invalid type: what is this?}


@@ 307,10 335,11 @@ abstype#SireState
    @ txt               | rexText rex
    | if (txt == {Nat}) | TNAT
    | if (txt == {Bit}) | TBIT
    | failStr rex {todo: parse more types}
    | else              | TREF txt
* {NODE}
    # switch (rexRune rex)
    * _ | failStr rex {unknown rune in type expression}
    * {,} | TTUP (map readType-self rexKids-rex)
    * _   | failStr rex {unknown rune in type expression}

= (readApp readExp rex)
@ exps


@@ 340,7 369,7 @@ abstype#SireState
    | rexSons rex
| if (len sons /= 2)
    | failStr rex {this needs two have two parameters}
| (readSym name, readType type)
| (readSym name, readType-{} type)

= (readPat rex)
@ rune | rexRune rex


@@ 348,11 377,13 @@ abstype#SireState
@ nSon | len sons
| ifNonZero (rexHeir rex)
    | failStr rex {unexpected heir}
| if (rex == '_)
    | PCAB
| if (rune=={!} && nSon==1)
    | PSEQ (readPat | fst sons)
| if (rune=={/} && nSon==2)
    @ [name type] sons
    | PVAR (readSym name) (readType type)
    | PVAR (readSym name) (readType-{} type)
| else
    | failStr rex {invalid pattern}



@@ 364,7 395,7 @@ abstype#SireState
        && (rexHeir rex == 0)
        && (len sons == 1)
    | failStr rex {expected a return type annotation like: >Nat}
| readType tyRex
| readType-{} tyRex

= (readAnonSig rex params)
@ numArgs     | dec (len params)


@@ 401,11 432,21 @@ abstype#SireState
@ pat                    | readPat patRex
| ELET pat (readExp val) (readExp body)

= (readLetRec readExp rex)
@ kids@[patRex val body] | rexKids rex
| if (len kids /= 3)     | failStr rex {nonsense let binding}
# case (readPat patRex)
- PCAB     | failStr rex {recursive anon let binding?  Don't do that}
- PSEQ _   | failStr rex {strict letrec? I don't think that's such a good idea}
- PVAR n t | EREC n t (readExp val) (readExp body)

> _ > Rex > (Str, Row Maybe-Str, Exp)
= (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-{-} items
@ kids (rexKids rex)
@ nKid (len kids)
| if (rune /= "-")
    | failStr rex {expected an - item}
@ last dec-nKid
@ patSyms | map readSym (take last kids)
@ body    | readExp (idx last kids)


@@ 419,7 460,7 @@ abstype#SireState
> _ > Rex > (Row (Str, Row Maybe-Str, Exp), Maybe Exp)
= (readCaseBranches readExp rex)
@ branches
    | map (readCaseBranch readExp) | listToRow | tarSeq {-} rex
    | map (readCaseBranch readExp) | listToRow | tarSeqSimple {-} rex
@ fallbacks | filter (n,_,_)&(n == "_") branches
@ branches  | filter (n,_,_)&(n /= "_") branches
^ [branches _]


@@ 455,12 496,14 @@ abstype#SireState
* {LEAF} | readLeaf readExp rex
* {NODE} # switch (rexRune rex)
         * {==} | readEql readExp rex
         * {&&} | readAnd readExp rex
         * {|}  | readApp readExp rex
         * {.+} | readAdd readExp rex
         * {++} | ETUP (readSeq readExp rex)
         * {+}  | ETUP (readSeq readExp rex)
         * {,}  | ETUP (readSeq readExp rex)
         * {@}  | readLet readExp rex
         * {@@} | readLetRec readExp rex
         * {&}  | readAnonLambda readExp rex
         * {?}  | readNamedLambda FALSE readExp rex
         * {??} | readNamedLambda TRUE readExp rex


@@ 487,21 530,19 @@ abstype#SireState
^ ASSERT (readExp _)
| if (nKid == 1) (idx 0 kids) (rexSetRune {|} rex)

= (readConstructor rex)
= (readConstructors selfNm rex)
: rex  < foreach (listToRow | tarSeq {-} rex)
@ kids | rexKids rex
@ nKid | len kids
| if (rexRune rex == {|})
    | if (lth nKid 2)
        | failStr rex {bad constructor}
    @ cnstr  | readSym (fst kids)
    @ fields | map readType | drop 1 kids
    @ fields | map readType-selfNm (drop 1 kids)
    | (cnstr, fields)
| else
    (readSym rex, [])

= (readConstructors rex)
| map readConstructor | listToRow | tarSeq {-} rex

= (readCmdKeyword rex)
@ kids@[keywordRex] | rexKids rex
@ nKids             | len kids


@@ 516,14 557,14 @@ abstype#SireState
    | if (nKids == 4)
        @ [_ tyRex flagRex csRex] kids
        @ !typeName | readSym tyRex
        @ !cnstrs   | readConstructors csRex
        @ !cnstrs   | readConstructors typeName 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
        @ !cnstrs   | readConstructors typeName csRex
        | DATA FALSE typeName cnstrs
    | else
        | failStr rex {#data expects three params}


@@ 550,20 591,29 @@ abstype#SireState

;;; Converting Between Type Representations ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= (vty x)
= (lookupType ss nm)
@ rex (WORD nm 0)
@ bad (failStr rex {this is not a type!})
: _ _ bind@[_ plan _ _ _ props] < getBind nm ss rex failStr
| trk [=bind]
: yes < maybeCase (btSearch {isType} props) bad
| ifz yes bad
| plan

= (viceType ss x)
^ FORALL 0 (_ x)
? (vty x)
# case x
- TNAT        | natRoot
- TREF n      | snd (lookupType ss n) ;; HACK ATTACK TODO XXX
- TTYP        | typeRoot
- TBIT        | bitRoot
- TFUN a b    | funRoot (vty a) (vty b)
- TTUP ts     | rowApply (| head | snd | tupleType | len ts) (map vty ts)
- TDAT [a ty] | ifNonZero a
                  | die {viceType: TODO: support polymorphic datatypes}
              | ty
- TDAT [a ty] | ifz a ty
              | die {viceType: TODO: support polymorphic datatypes}
- _           | die [{viceType: malformed type} x]

(viceType x)=(FORALL 0 (vty x))

;; TODO {loadType} is an extremely gnarly hack.  That's fine, though,
;; because eventually we will get rid of the Typ and just work directly
;; with the real types.sire types.


@@ 586,8 636,18 @@ abstype#SireState

;;; Printing ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= (showViceType vty)
# case vty
- TTYP     | 'Type
- TNAT     | 'Nat
- TBIT     | 'Bit
- TREF-nm  | `[$(symToRex "nm")]
- TFUN a b | `($(showViceType a) -> $(showViceType b))
- TTUP xs  | NEST {,} (map showViceType xs) 0
- TDAT t   | ` #($(showType t))

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

= (showCase showExp x bs mFall)
| NEST "#" ('case, showExp x)


@@ 600,8 660,9 @@ abstype#SireState

= (showPat pat)
# case pat
- PCAB       | '_
- PSEQ p     | ` !($(showPat p))
- PVAR nm ty | ` ($(WORD nm 0) / $(showType | viceType ty))
- PVAR nm ty | ` ($(WORD nm 0) / $(showViceType ty))

= (showExp exp)
    # case exp


@@ 609,6 670,7 @@ abstype#SireState
    - EBIT b       | if b 'true 'false
    - ENAT n       | WORD (showNat n) 0
    - EEQL a b     | `($(showExp a) == $(showExp b))
    - EAND a b     | `($(showExp a) && $(showExp b))
    - EADD a b     | `($(showExp a) .+ $(showExp b))
    - EAPP a b     | `($(showExp a) $(showExp b))
    - ETUP xs      | NEST "," (map showExp xs) 0


@@ 619,12 681,16 @@ abstype#SireState
        ` @ $(showPat pat) $(showExp val)
          $(showExp body)

    - EREC n t v b
        ` @@ $(showPat (PVAR n t)) $(showExp v)
           $(showExp b)

    - EFUN inlined pinned name args resTy body
        | if (not inlined && not pinned && eqz name)
            @ argList
                ^ NEST {|} _ 0
                | rowSnoc (map showTypedSym args)
                ` >($(showType | viceType resTy))
                ` >($(showViceType resTy))
            ` & $argList
              $(showExp body)
        | die "umm",(inlined, pinned, name, args, resTy, body)


@@ 848,6 914,7 @@ abstype#SireState
;;; Misc Codegen ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= (addSire a b) | apple (G getBind#add) [a b]
= (andSire a b) | apple (G getBind#and) [a b]
= (eqlSire a b) | apple (G getBind#eql) [a b]




@@ 864,6 931,7 @@ abstype#SireState
    - 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)
    - EAND a b | andSire (go e a) (go e b)
    - ETUP xs  | rowSire (map go-e xs)

    - ECAS s bs f


@@ 879,15 947,23 @@ abstype#SireState
    - ELET pat var body
        @ rex (showExp exp)
        # case pat
        - PCAB        | go e body
        - PVAR nm _ty | L (go e var) (go (SOME nm)::e body)
        - PSEQ p
            # case p
            - PSEQ _      | failStr rex {double strict pattern}
            - PCAB        | apple K-seq (go e var, go e body)
            - PVAR nm _ty | L (go e var)
                          ^ apple K-seq [V-0 _]
                          | go (SOME nm :: e) body
        - PVAR nm _ty
            | L (go e var)
            | go (SOME nm :: e) body

    ;; TODO: Change the LETREC syntax to support multiple, simultaneous,
    ;; recursive binds.

    - EREC n t var body
        | R
        * [(go (SOME n :: e) var)]
        * go (SOME n :: e) body

    - EFUN inline pinned name args _rTy body
        @ tag     | name


@@ 926,13 1002,18 @@ abstype#SireState

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

= (unify rex mExpected ty)
: expected < maybeCase mExpected ty
| if (expected == ty) ty
| fail rex
` # type mismatch
  # expected=($(showType | viceType expected))
  # actual=($(showType | viceType ty))
= (unify ss rex mExpected ty)
# case mExpected
- NONE
    | ty
- SOME expected
    @ expectedTy | trk [viceType %ss expected] (viceType ss expected)
    @ actualTy   | trk [viceType %ss ty]       (viceType ss ty)
    | if (expectedTy == actualTy) ty
    | fail rex
    ` # type mismatch
      # expected=($$(expectedTy))
      # actual=($$(actualTy))

= (lookupBind ss nm)
: _ _ bind < getBind nm ss (WORD nm 0) failStr


@@ 942,7 1023,7 @@ abstype#SireState
^ _ #[] mExpect exp
? (go e mExpect exp)
@ rex (showExp exp)
| unify rex mExpect
| unify ss rex mExpect

    # case exp



@@ 962,6 1043,11 @@ abstype#SireState
        @ !bTy | go e SOME-aTy b
        | TBIT

    - EAND a b
        @ !aTy | go e SOME-TBIT a
        @ !bTy | go e SOME-TBIT b
        | TBIT

    - EADD a b
        @ !aTy | go e SOME-TNAT a
        @ !bTy | go e SOME-TNAT b


@@ 978,11 1064,15 @@ abstype#SireState

    - ELET pat val body
        # case pat
        - PSEQ p
            | go e mExpect (ELET p val body)
        - PVAR nm ty
            | seq (go e SOME-ty val)
            | go (tabPut e nm ty) mExpect body
        - PSEQ p     | go e mExpect (ELET p val body)
        - PCAB       | seq (go e NONE val) (go e mExpect body)
        - PVAR nm ty | seq (go e SOME-ty val)
                     | go (tabPut e nm ty) mExpect body

    - EREC nm ty val body
        @ e (tabPut e nm ty)
        | seq (go e SOME-ty val)
        | go e mExpect body

    - ECAS _ _ _
        | maybeCase mExpect TNAT id


@@ 1064,8 1154,8 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
    # expression y
    # reason
        # type mismatch
        # expected=Nat
        # actual=Bit
        # expected=($$Nat)
        # actual=($$Bit)

=?=  ++ ELET (PVAR {x} TNAT) ENAT-3 ETUP-(EREF {x}, EEQL EBIT-1 EBIT-1)
     ++ TTUP (TNAT, TBIT)


@@ 1122,13 1212,15 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))

= (doBind ss@(nex, ctx, binds, mods) bind@(name, sire, vty, props))

    @ type  | viceType vty
    @ type  | viceType ss 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 [=type]

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


@@ 1141,6 1233,17 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
: dup   < maybeCase (findDup names) 0
| fail rex `[{duplicate constructor name:} $(WORD dup 0)]

= (resolveType ss selfNm selfTy ty)
@ go (resolveType ss selfNm selfTy)
# case ty
- TFUN a b | TFUN (go a) (go b)
- TTUP xs  | TTUP (map go xs)
- TREF nm  | if nm==selfNm selfTy (lookupType ss nm)
- TTYP     | ty
- TNAT     | ty
- TBIT     | ty
- TDAT ty  | ty

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

    # case cmd


@@ 1173,8 1276,10 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))

        @ (newtype, ss) | mkNewType typeName 0 ss

        @ resolve (resolveType ss typeName (TDAT newtype))

        @ branches : (i, (nm, tys)) < foreach (rowIndexed cnstrs)
                   | (nm, if legible nm i, tys)
                   | (nm, if legible nm i, map resolve tys)

        | seq (checkForADTDups rex branches)



@@ 1185,12 1290,12 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
        @ ss | foldl doBind ss
             | constructorBinds adt (TDAT newtype) branches

        | doBind ss (typeName, K-newtype, TTYP, bstEmpty)
        | doBind ss (typeName, K-newtype, TTYP, bstSing {isType} 1)

    - EVAL x
        @ !typ (typecheck ss NONE x)
        @ plan (evaluate ss x)
        | trk ` > $(showType | viceType typ)
        | trk ` > $(showViceType typ)
                $$plan
        | ss



@@ 1214,10 1319,13 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
{!!}#=viceroy
{.+}#=viceroy
{==}#=viceroy
{&&}#=viceroy
{|}#=viceroy
{++}#=viceroy
{+}#=viceroy
{,}#=viceroy
{@}#=viceroy
{@@}#=viceroy
{&}#=viceroy
{?}#=viceroy
{??}#=viceroy


@@ 1263,22 1371,22 @@ t==true ; compare t to true, using the above information during

#=?= (#| tryVice '(1 =?= true))
   ^ LEFT (#| v2 {viceroy-error} _)
   ' # error during viceroy execution
   ` # error during viceroy execution
     # expression true
     # reason
         # type mismatch
         # expected=Nat
         # actual=Bit
         # expected=($$Nat)
         # actual=($$Bit)

#=?= (#| tryVice '(add 1 true))
   ^ LEFT (#| v2 {viceroy-error} _)
   ' # error during viceroy execution
   ` # error during viceroy execution
     # expression
         true
     # reason
         # type mismatch
         # expected=Nat
         # actual=Bit
         # expected=($$Nat)
         # actual=($$Bit)


;;; Record #data Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


@@ 1386,11 1494,41 @@ s3=(SOME 3)
;;; Strict Patterns ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= ex
& (x/Nat >(Nat, Nat))
@ !y/(Nat, Nat) [x x]
| y

#=?= ex
  #& x
  #@ y (#| v2 x x)
  #| seq y
  #| y

= ex
& (x/Nat >Nat)
@ !y/Nat x
| 3
@ !_ [x x]
| x

#=?= ex
  #& x
  #| seq x
  #| 3
  #| seq (#| v2 x x)
  #| x

(true && false)


;;; LETREC ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

# data ListNat
- LN_NIL
- LN_CONS Nat ListNat

= ex
 ? (repeat x/Nat >ListNat)
@@ ax/ListNat (LN_CONS x ax)
 | ax

#=?= ex
  #? (repeat x)
 #@@ ax=(#| LN_CONS x ax)
  #| ax