~plan/plunder

cfb72d70019b9628dd4ae919b50b0d3efd2c46b9 — Sol 4 months ago e575c0f
viceroy: cleanup
1 files changed, 110 insertions(+), 109 deletions(-)

M sire/viceroy.sire
M sire/viceroy.sire => sire/viceroy.sire +110 -109
@@ 1,3 1,9 @@
; Copyright 2023 The Plunder Authors
; Use of this source code is governed by a BSD-style license that can be
; found in the LICENSE file.

#### viceroy <- prelude

;;;; Viceroy will eventually replace Stew, but it is still in it's
;;;; infancy.
;;;;


@@ 28,28 34,24 @@
;;;;
;;;;     constructor=[%tag1 (PIN [(Type a) %tag1 FOO [Nat Nat] %tag2 BAR [a]])]
;;;;
;;;;     = constructor ^ [%tag1 (PIN _)]
;;;;                   + (0, (Type 0))
;;;;                   + %tag1 FOO [Nat Nat]
;;;;                   + %tag2 BAR [0]
;;;;     = constructor
;;;;     ^ [%tag1 (PIN _)]
;;;;     + (0, (Type 0))
;;;;     + %tag1 FOO [Nat Nat]
;;;;     + %tag2 BAR [0]
;;;;
;;;; TODO Codegen for case-on-ADT (simple ADT shapes only)
;;;;
;;;;     (Exp, Map Nat (Row Str, Exp))
;;;;
;;;;     @ val exp
;;;;     @ val | $valExp
;;;;     @ _1  | idx 1 val
;;;;     @ _2  | idx 2 val ; only binding fields that are used.
;;;;     @ _3  | idx 3 val
;;;;     # switch (_Head val)
;;;;     * k0
;;;;         | b0
;;;;     * k1
;;;;         @ f1 (idx 1 val)
;;;;         @ f2 (idx 2 val)
;;;;         @ f3 (idx 3 val)
;;;;         | b1
;;;;     * k2
;;;;         @ f1 (idx 1 val)
;;;;         @ f2 (idx 2 val)
;;;;         | b2
;;;;     * k0 b0
;;;;     * k1 b1 ; in appropriate namespace given field patterns.
;;;;     * k2 b2
;;;;
;;;; TODO Parsing for simple {#case} expressions
;;;;


@@ 88,8 90,6 @@
;;;;     x
;;;;

#### viceroy <- prelude


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



@@ 100,7 100,7 @@
:| plan [try]


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

# data Typ -legible
- TTYP


@@ 421,8 421,6 @@ abstype#(Bst k v)
* {#}   | readKeyword rex
* _     | EVAL (readExp rex)

(die2 x y)=(die [x y])


;;; Parsing Tests ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



@@ 448,11 446,41 @@ abstype#(Bst k v)
=?= [=1 =2 =3] | evalSire | tabSire [1=(K 1) 2=(K 2) 3=(K 3)]


;;; Evaluating Expressions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Switch Codegen ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= (getBindEx ss sym)
: _ pin _ < getBind sym ss (WORD sym 0) failStr
| pin
> Sire > Sire > Tab Nat Sire > Sire
= (switchSire tag fb tab)
@ keys     | tabKeysRow tab
@ nKey     | len keys
@ lastIdx  | dec nKey
| ifz nKey | fb
@ contig   | (lastIdx == idx lastIdx keys)  ; [0 1 2 3][3] == 3
| if contig
* apple K-switch    (tag, fb, rowSire (tabValsRow tab))
* apple K-tabSwitch (tag, fb, tabSire tab)

=?=   ^ (evalSire _, _)
      | switchSire K-3 K-777
      | [0=(K 0) 1=(K 1) 2=(K 2)]
  ^ [777 _]
  ^ apple K-switch (K 3, K 777, _)
  | rowSire (K 0, K 1, K 2)

=?=   ^ (evalSire _, _)
      | switchSire K-3 K-777
      | [1=(K 1) 2=(K 2) 3=(K 3)]
  ^ [3 _]
  ^ apple K-tabSwitch (K 3, K 777, tabSire _)
  | [1=(K 1) 2=(K 2) 3=(K 3)]


;;; Misc Codegen ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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


;;; Evaluating Expressions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= (compile ss exp)



@@ 460,20 488,19 @@ abstype#(Bst k v)
    ? (go e exp)
    # case exp

    - EADD a b
        | apple (G getBind#add) (go e a, go e b)

    - EREF x
        # case (listElemIndexOpt SOME-x e)
        - NONE   | G (getBindEx ss x)
        - SOME i | V i

    - EBIT n   | K n
    - ENAT n   | K n
    - EEQL a b | apple (G getBind#eql) (go e a, go e b)
    - 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)

    - EREF x
        @ rex (WORD x 0)
        # case (listElemIndexOpt SOME-x e)
        - NONE   | G (getBind x ss rex failStr (_ pin _ & pin))
        - SOME i | V i

    - ELET nm _ty var body
        | L (go e var)
        | go (SOME nm :: e) body


@@ 486,8 513,10 @@ abstype#(Bst k v)
        ^ listWeld (listRev _) e
        | listMap SOME (name :: listMap fst (listFromRow args))

    - _
        | die {malformed ast},exp
    - _ (die {malformed ast},exp)


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

= (vty x)
# case x


@@ 554,49 583,55 @@ abstype#(Bst k v)
| bind

= (typecheck ss mExpect exp)
| trk [typecheck exp]
^ _ #[] mExpect exp
? (go e mExpect exp)
| trk [{go} e mExpect exp]
^ trk [{go} e mExpect exp],{->},_ _
@ rex (showExp exp)
| unify rex mExpect
# case exp
- EREF nm
    # case (tabLookup nm e)
    - SOME x | x
    - NONE
        @ bind   | lookupBind ss nm
        @ ty     | getProp bind {type}
        | ifz ty | failStr rex {untyped global}
        | loadType ty
- EBIT _ | TBIT
- ENAT _ | TNAT
- EEQL a b
    @ !aTy | go e NONE a
    @ !bTy | go e SOME-aTy b
    | TBIT
- EADD a b
    @ !aTy | go e SOME-TNAT a
    @ !bTy | go e SOME-TNAT b
    | TNAT
- EAPP f x
    # case (go e NONE f)
    - _                   | failStr rex {head is not a function!}
    - TFUN inType outType | seq (go e SOME-inType x) outType
- ETUP xs
    @ elems (map (go e NONE) xs)
    | TTUP elems
- ELET nm ty val body
    | seq (go e SOME-ty val)
    | go (tabPut e nm ty) mExpect body
- EFUN inlined pinned name args resTy body
    @ funTy | foldr TFUN resTy (map snd args)
    ^ seq _ funTy
    ^ go (tabUnion _ e) SOME-resTy body
    | tabFromPairs (rowCons [name funTy] args)
- _
    | {showExp: malformed exp} exp

    # case exp

    - EBIT _ | TBIT
    - ENAT _ | TNAT

    - EREF nm
        # case (tabLookup nm e)
        - SOME x | x
        - NONE   @ bind   | lookupBind ss nm
                 @ ty     | getProp bind {type}
                 | ifz ty | failStr rex {untyped global}
                 | loadType ty

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

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

    - EAPP f x
        # case (go e NONE f)
        - _                   | failStr rex {head is not a function!}
        - TFUN inType outType | seq (go e SOME-inType x) outType

    - ETUP xs
        @ elems (map (go e NONE) xs)
        | TTUP elems

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

    - EFUN inlined pinned name args resTy body
        @ funTy | foldr TFUN resTy (map snd args)
        ^ seq _ funTy
        ^ go (tabUnion _ e) SOME-resTy body
        | tabFromPairs (rowCons [name funTy] args)

    - _
        | {showExp: malformed exp} exp

= (evaluate ss exp)
@ sire | compile ss exp


@@ 680,34 715,6 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
  | [x xTy xSr xVl]


;;; Switch Codegen ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

> Sire > Sire > Tab Nat Sire > Sire
= (switchSire tag fb tab)
@ keys     | tabKeysRow tab
@ nKey     | len keys
@ lastIdx  | dec nKey
| ifz nKey | fb
@ contig   | (lastIdx == idx lastIdx keys)  ; [0 1 2 3][3] == 3
| if contig
* apple K-switch    (tag, fb, rowSire (tabValsRow tab))
* apple K-tabSwitch (tag, fb, tabSire tab)

=?=   ^ (evalSire _, _)
      | switchSire K-3 K-777
      | [0=(K 0) 1=(K 1) 2=(K 2)]
  ^ [777 _]
  ^ apple K-switch (K 3, K 777, _)
  | rowSire (K 0, K 1, K 2)

=?=   ^ (evalSire _, _)
      | switchSire K-3 K-777
      | [1=(K 1) 2=(K 2) 3=(K 3)]
  ^ [3 _]
  ^ apple K-tabSwitch (K 3, K 777, tabSire _)
  | [1=(K 1) 2=(K 2) 3=(K 3)]


;;; Creating ADT Constructors ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

> Typ > Row (Nat, Constructor) > Row (Str, Sire, Typ, Bst Str Any)


@@ 755,7 762,6 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
    @ props | bstSave (bstPut props {type} type)
    @ plan  | evalSire sire
    @ bind  | PIN [nex plan sire ctx name props]
    | trk   | [newBind=[nex plan sire ctx name props]]
    @ ss    | (inc nex, ctx, tabPut binds name bind, mods)

    | trk ` > $(showType type)


@@ 805,11 811,6 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))

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