~plan/plunder

02ee1bbdeeae599139785da1111b296305e0467d — Sol 4 months ago 291a06c
viceroy: strict let-bindings

This add supports for bang-patterns in let bindings:

    @ !x/Nat 3
    4
1 files changed, 152 insertions(+), 96 deletions(-)

M sire/viceroy.sire
M sire/viceroy.sire => sire/viceroy.sire +152 -96
@@ 79,15 79,19 @@
;;;; 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.
;;;; TODO Typecheck the body of each branch.
;;;; TODO Unify the types of all of the branches (and the fallback)
;;;; Typecheck Case Expressions:
;;;;
;;;; TODO Multi-Assertion Blocks
;;;; TODO Multi-Command Blocks
;;;; TODO Multi-Bind Commands
;;;; - 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.
;;;; - TODO Typecheck the body of each branch.
;;;; - TODO Unify the types of all of the branches (and the fallback)
;;;;
;;;; Multi-Command Sugar:
;;;;
;;;; - TODO Multi-Assertion Blocks
;;;; - TODO Multi-Command Blocks
;;;; - TODO Multi-Bind Commands
;;;;
;;;; TODO Type annotations on Expressions
;;;;


@@ 95,10 99,7 @@
;;;;
;;;; TODO Arrays: Array(...), Array#(...), # Array ...
;;;;
;;;; TODO Strict let bindings
;;;;
;;;;     @ !x/Nat (add 2 3)
;;;;     | a
;;;; DONE Strict let bindings (@ !x/Nat (add 2 3) 4)
;;;;
;;;; TODO Tuple destructuring:
;;;;


@@ 136,6 137,10 @@

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

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

# data Exp -legible
- EADD Exp Exp
- EBIT Bit


@@ 145,7 150,7 @@
- EAPP Exp Exp
- ETUP Row-Exp
- ECAS Exp Row-(CaseBranchE Exp) (Maybe e)
- ELET nm/Str vTy/Typ v/Exp b/Exp
- ELET p/Pat v/Exp b/Exp
- EFUN inline/Bit pin/Bit nm/Str Row-(Exp,Typ) rTy/Typ b/Exp

# typedef CaseBranch (CaseBranchE Exp)


@@ 337,6 342,20 @@ abstype#SireState
    | failStr rex {this needs two have two parameters}
| (readSym name, readType type)

= (readPat rex)
@ rune | rexRune rex
@ sons | rexSons rex
@ nSon | len sons
| ifNonZero (rexHeir rex)
    | failStr rex {unexpected heir}
| if (rune=={!} && nSon==1)
    | PSEQ (readPat | fst sons)
| if (rune=={/} && nSon==2)
    @ [name type] sons
    | PVAR (readSym name) (readType type)
| else
    | failStr rex {invalid pattern}

(readArgList rex)=(readSeq readTypedSym rex)

= (readRetTy rex)


@@ 377,10 396,10 @@ abstype#SireState
| EFUN FALSE FALSE 0 args retTy (readExp body)

= (readLet readExp rex)
@ kids@[name val body] | rexKids rex
| if (len kids /= 3)   | failStr rex {nonsense let binding}
@ (!nm, !ty)           | readTypedSym name
| ELET nm ty (readExp val) (readExp body)
@ kids@[patRex val body] | rexKids rex
| if (len kids /= 3)     | failStr rex {nonsense let binding}
@ pat                    | readPat patRex
| ELET pat (readExp val) (readExp body)

> _ > Rex > (Str, Row Maybe-Str, Exp)
= (readCaseBranch readExp rex)


@@ 529,6 548,89 @@ abstype#SireState
  | readCmd '(x = (3.+y))


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

= (vty x)
# case x
- TNAT        | natRoot
- 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
- _           | 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.

= (loadTypeTree ty tree)
    | if (tree == natRoot) | TNAT
    | if (tree == bitRoot) | TBIT

    | if (head tree == funRoot)
        @ [a b] (tnodeParams tree)
        | TFUN (loadTypeTree ty a) (loadTypeTree ty b)

    | TDAT [0 tree]
    ; die [{unknown type} [=ty subtree=tree]]

= (loadType ty@[arity tree])
| if arity | die {no polymorphism support yet}
| loadTypeTree ty tree


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

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

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

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

= (showExp exp)
    # case exp
    - EREF n       | WORD n 0
    - EBIT b       | if b 'true 'false
    - ENAT n       | WORD (showNat n) 0
    - EEQL 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
    - ECAS x bs f  | showCase showExp x bs f
    - _            | {showExp: malformed exp} exp

    - ELET pat val body
        ` @ $(showPat pat) $(showExp val)
          $(showExp body)

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



;;; Codegen for Rows and Tabs ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= (rowSire items)


@@ 774,9 876,18 @@ abstype#SireState
        - 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
    - ELET pat var body
        @ rex (showExp exp)
        # case pat
        - PSEQ p
            # case p
            - PSEQ _      | failStr rex {double strict pattern}
            - 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

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


@@ 815,39 926,6 @@ abstype#SireState

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

= (vty x)
# case x
- TNAT        | natRoot
- 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
- _           | 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.

= (loadTypeTree ty tree)
    | if (tree == natRoot) | TNAT
    | if (tree == bitRoot) | TBIT

    | if (head tree == funRoot)
        @ [a b] (tnodeParams tree)
        | TFUN (loadTypeTree ty a) (loadTypeTree ty b)

    | TDAT [0 tree]
    ; die [{unknown type} [=ty subtree=tree]]

= (loadType ty@[arity tree])
| if arity | die {no polymorphism support yet}
| loadTypeTree ty tree

= (unify rex mExpected ty)
: expected < maybeCase mExpected ty
| if (expected == ty) ty


@@ 856,45 934,6 @@ abstype#SireState
  # expected=($(showType | viceType expected))
  # actual=($(showType | viceType ty))

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

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

= (showExp exp)
    # case exp
    - EREF n       | WORD n 0
    - EBIT b       | if b 'true 'false
    - ENAT n       | WORD (showNat n) 0
    - EEQL 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
    - ECAS x bs f  | showCase showExp x bs f
    - _            | {showExp: malformed exp} exp

    - ELET name ty val body
        ` @ ($(WORD name 0) / $(showType | viceType ty))
             $val
          $body

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

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


@@ 937,9 976,13 @@ abstype#SireState
        @ 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
    - 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

    - ECAS _ _ _
        | maybeCase mExpect TNAT id


@@ 1024,7 1067,7 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
        # expected=Nat
        # actual=Bit

=?=  ++ ELET {x} TNAT ENAT-3 ETUP-(EREF {x}, EEQL EBIT-1 EBIT-1)
=?=  ++ ELET (PVAR {x} TNAT) ENAT-3 ETUP-(EREF {x}, EEQL EBIT-1 EBIT-1)
     ++ TTUP (TNAT, TBIT)
     ++ L K-3 | apple_ (K (cow 2), apple_ (eqlRef, K 1, K 1), V 0)
     ++ [3 TRUE]


@@ 1338,3 1381,16 @@ s3=(SOME 3)
# case (FOO 3 4)
- FOO x y | x
- _       | 3


;;; Strict Patterns ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

#=?= ex
  #& x
  #| seq x
  #| 3