~plan/plunder

00e114980e3025561791804cffcf8e5db78455ca — Sol 4 months ago 9b7d850
viceroy: typecheck #case patterns
1 files changed, 40 insertions(+), 14 deletions(-)

M sire/viceroy.sire
M sire/viceroy.sire => sire/viceroy.sire +40 -14
@@ 94,11 94,11 @@
;;;;
;;;; Typecheck Case Expressions:
;;;;
;;;; - 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)
;;;; - DONE Validate that the scrutinee has the same type as the ADT.
;;;; - DONE Collect the field-types associated with each field-binding.
;;;; - DONE Construct the type-environment for the body of each branch.
;;;; - DONE Typecheck the body of each branch.
;;;; - DONE Unify the types of all of the branches (and the fallback)
;;;;
;;;; Multi-Command Sugar:
;;;;


@@ 119,6 119,10 @@
;;;;     @ [x/Nat y/Nat z/Nat] (3, 4, 5)
;;;;     x
;;;;
;;;; TODO Strictness Patterns on Arguments.
;;;; TODO Cab-Patterns on Arguments.
;;;; TODO Tuple-Patterns on Arguments.
;;;;
;;;; Actual Docs
;;;; ===========
;;;;


@@ 931,8 935,7 @@ abstype#TypeTree

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

= (getBranchInfo ss branches)
@ rex            | '(#case)
= (getBranchInfo rex ss branches)
@ cNames         | map fst branches
@ adt1           | lookupAdt ss (fst cNames)
@ (onDup dup)    | failStr rex {overlapping branch}


@@ 972,7 975,7 @@ abstype#TypeTree
> SireState > _ > _ > Exp > Tab Nat (Row (Maybe Str), Exp) > Maybe Exp > Sire
= (compileCase ss go e scrut branches mFall)
@ (binds, envs) | caseBinds (go e scrut) branches
@ (adt, info)   | getBranchInfo ss branches
@ (adt, info)   | getBranchInfo '(#case) ss branches
| seq           | checkExaustivity adt info branches mFall
@ scrutVar      | V dec-(len binds)
@ fall          | maybeCase mFall (defaultFallback adt scrutVar) f&(go e f)


@@ 1129,6 1132,7 @@ abstype#TypeTree
= (typecheck ss mExpect exp)
^ _ {typecheck} #[] mExpect exp
? (go from e mExpect exp)
| trk [%go [=from] [=e] [=mExpect] [=exp]]
@ rex (showExp exp)
| unify ss rex mExpect



@@ 1211,21 1215,43 @@ abstype#TypeTree
        | seq | force (go {erec.head} e SOME-ty val)
        | go {erec.body} e mExpect body

    - ECAS _ _ _
        | maybeCase mExpect natRoot id
        ; TODO
    ; TODO
    ; # typedef (CaseBranchE Exp) (Str, Row Maybe-Str, Expr)
    ; ECAS Exp Row-(CaseBranchE Exp) (Maybe e)
    - ECAS scrut cases mFall

        ; The value that we scrutinize is the same as the type of the
        ; ADT that we are branching on.
        @ (adt, infos) | getBranchInfo rex ss cases
        @ adtType      | snd (fst (pinItem adt))
        | trk [=adtType =scrut =e]
        @ !scrutTy     | go {case.scrut} e SOME-adtType scrut

        ; The fallback matches the type that's expected of this
        ; expression.
        @ !mResTy : fall < maybeCase mFall mExpect
                  | SOME (go {case.fall} e mExpect fall)

        ; The return type of each branch does too.
        ^ foldr _ mResTy (zip cases infos)
        & ([[cnstr binds body] [tag types]] mExpect)
        ^ go {case.branch} _ mExpect body
        ^ tabUnion (tabFromPairs | catMaybes _) e
        : [mBind ty] < foreach (zip binds types)
        : bind       < maybeCase mBind NONE
        | SOME (bind, ty)

    - ECOL (rTy, args) expr body
        | go {ecol} e mExpect (EAPP expr (ELAM FALSE FALSE 0 args rTy body))

    - ELAM inlined pinned name args resTxp body
    - ELAM inlined pinned selfNm args resTxp body
        @ argTxps  | map snd args
        @ !argTys  | force | map (viceType ss #[]) argTxps
        @ !resTy   | force | viceType ss #[] resTxp
        @ funTy    | foldr (a b & tyApp Fun [a b]) resTy argTys
        ^ seq _ funTy
        ^ go {fun} (tabUnion _ e) SOME-resTy body
        | tabFromPairs | rowCons [name funTy]
        | tabFromPairs | weld (ifz selfNm [] [[selfNm funTy]])
                       : [[argName _] ty] < foreach (zip args argTys)
                       | (argName, ty)



@@ 1568,7 1594,7 @@ s3=(SOME 3)

(#| dataTag s3)

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