~plan/plunder

11b8da7cb027afb4ac415e93e3e62f2ef5d937bf — Sol 4 months ago efb1079
viceroy: more sensible use of type-representations

Before this commit, there was a pretty significant overlap in the usage
between the `type-machinery.sire` representation and the `Typ` datatype
from Viceroy.

This commit clarify this usage, now Typ becomes `Txp`, which is just a
parse-tree for type expressions.  And the typing engine uses
`type-machinery.sire` types for everything.
2 files changed, 171 insertions(+), 147 deletions(-)

M sire/sire_07_dat.sire
M sire/viceroy.sire
M sire/sire_07_dat.sire => sire/sire_07_dat.sire +7 -1
@@ 61,6 61,12 @@
= (take n v)        | slice v 0 n
= (splitAt i r)     | v2 (take i r) (drop i r)

= (foldr1 f xs)
| if (null xs)
    | die {fold1: empty row}
@ las (dec len-xs)
| foldr f (idx las xs) (take las xs)

= (chunks sz row)
| gen | div (roundUp len-row sz) sz
& ix


@@ 950,7 956,7 @@ F=found
^-^ rowAnd rowOr sum sumOf all any zip zipWith
^-^ cat catMap
^-^ take drop rev
^-^ unfoldr span splitAt strictRow insert
^-^ unfoldr span splitAt foldr1 strictRow insert
^-^
^-^ bopE bapE bowE appE rowE
^-^ {,}

M sire/viceroy.sire => sire/viceroy.sire +164 -146
@@ 140,20 140,20 @@

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

# data Typ -legible
- TTYP
- TNAT
- TBIT
# data Txp -legible
- TREF Str
- TFUN Typ Typ
- TTUP Row-Typ
- TDAT Type
- TFUN Txp Txp
- TTUP Row-Txp

TTYP=(TREF "Type")
TBIT=(TREF "Bit")
TNAT=(TREF "Nat")

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

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

# data Exp -legible


@@ 167,18 167,18 @@
- 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
- EREC n/Str t/Txp v/Exp b/Exp
- EFUN inline/Bit pin/Bit nm/Str Row-(Exp,Txp) rTy/Txp b/Exp

# typedef CaseBranch (CaseBranchE Exp)

# typedef Constructor (Str, Row Typ)
# typedef (Constructor t) (Str, Row t)

# data Cmd -legible
- EVAL Exp
- BIND Str Exp
- ASSERT Exp
- DATA Bit Str (Row Constructor)
- DATA Bit Str (Row Constructor-Txp)
- CHK_EQ Exp Exp

; TODO: These belong elsewhere.


@@ 186,6 186,8 @@
abstype#Sire
abstype#(Bst k v)
abstype#SireState
abstype#DataType
abstype#TypeTree


;;; Misc Rex Rendering ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


@@ 332,10 334,7 @@ abstype#SireState
* {LEAF}
    | ifz ((rexHeir rex == 0) && (rexStyle rex == {WORD}))
        | failStr rex {invalid type name}
    @ txt               | rexText rex
    | if (txt == {Nat}) | TNAT
    | if (txt == {Bit}) | TBIT
    | else              | TREF txt
    | TREF (rexText rex)
* {NODE}
    # switch (rexRune rex)
    * {,} | TTUP (map readType-self rexKids-rex)


@@ 592,6 591,7 @@ abstype#SireState
;;; Converting Between Type Representations ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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


@@ 600,51 600,28 @@ abstype#SireState
| ifz yes bad
| plan

= (viceType ss x)
^ FORALL 0 (_ x)
? (vty x)
= (viceType ss locals x)
@ noPoly
    | die {viceType: TODO: support polymorphic datatypes}
@ go (viceType ss locals)
| if ((len x == 2) && (fst x == 0))
    | die "badType",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] | ifz a ty
              | die {viceType: TODO: support polymorphic datatypes}
- TREF nm     ^ maybeCase (tabLookup nm locals) _ id
              @ @(SCHEME arity tree) (lookupType ss nm)
              | ifz arity tree noPoly
- TFUN a b    | funRoot (go a) (go b)
- TTUP ts     | rowApply (| head | snd | tupleType | len ts) (map go ts)
- _           | die [{viceType: malformed type} 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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= (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))/($(showViceType vty))


@@ 960,10 937,9 @@ abstype#SireState
    ;; 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
    - EREC n _t var body
        @ e2 (SOME n :: e)
        | R [(go e2 var)] (go e2 body)

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


@@ 1002,86 978,120 @@ abstype#SireState

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

= (unify ss rex mExpected ty)
= (unify ss rex mExpected actualTy)
# 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
    | actualTy
- SOME expectedTy
    | if (expectedTy == actualTy) actualTy
    | fail rex
    ` # type mismatch
      # expected=($$(expectedTy))
      # actual=($$(actualTy))
      # expected=($(showType (FORALL 0 expectedTy)))
      # actual=($(showType (FORALL 0 actualTy)))

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

> Type > Row TypeTree > Type
= (tyApp scheme params)

    @ @(FORALL arity tree) scheme

    | if (arity /= len params)
        | failStr (showType scheme) {Bad arity in type application}

    ^ _ tree
    ? (subst x)
    | if isNat-x (idx x params)
    | tnodeMapParams subst x

= (typecheck ss mExpect exp)
^ _ #[] mExpect exp
? (go e mExpect exp)
^ _ {typecheck} #[] mExpect exp
? (go from e mExpect exp)
| trk [%go [=from] [=e] [=mExpect] [=exp]]
@ rex (showExp exp)
| unify ss rex mExpect

    # case exp

    - EBIT _ | TBIT
    - ENAT _ | TNAT
    - EBIT _ | bitRoot
    - ENAT _ | natRoot

    - EREF nm
        # case (tabLookup nm e)
        - SOME x | x
        - SOME x | trk [=x] x
        - NONE   @ bind   | lookupBind ss nm
                 @ ty     | getProp bind {type}
                 | ifz ty | failStr rex {untyped global}
                 | loadType ty
                 @ @(SCHEME arity tree) ty
                 | ifz arity tree
                 | trk [=tree]
                 | failStr rex {polymorphic types are not yet supported}

    - EEQL a b
        @ !aTy | go e NONE a
        @ !bTy | go e SOME-aTy b
        | TBIT
        @ !aTy | go {eql} e NONE a
        @ !bTy | go {eql} e SOME-aTy b
        | bitRoot

    - EAND a b
        @ !aTy | go e SOME-TBIT a
        @ !bTy | go e SOME-TBIT b
        | TBIT
        @ !aTy | go {and} e SOME-bitRoot
        @ !bTy | go {and} e SOME-bitRoot
        | bitRoot

    - EADD a b
        @ !aTy | go e SOME-TNAT a
        @ !bTy | go e SOME-TNAT b
        | TNAT
        @ !aTy | go {add} e SOME-natRoot a
        @ !bTy | go {add} e SOME-natRoot b
        | natRoot

    - 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
        @ tree (go {app-fun} e NONE f)
        | trk {APP},[=tree]
        | if (head tree /= funRoot)
            | failStr rex {head is not a function!}
        @ [inType outType] (tnodeParams tree)
        | trk [=inType =outType =tree]
        | seq (go {app-arg} e SOME-inType x) outType

    - ETUP xs
        @ elems (map (go e NONE) xs)
        | TTUP elems
        | tyApp (tupleType | len xs)
        | map (go {tup} e NONE) xs

    - ELET pat val body
        # case pat
        - 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
        - PSEQ p      | go {let-seq} e mExpect (ELET p val body)
        - PCAB        | seq (go {let-cab} e NONE val) (go {let-cab-body} e mExpect body)
        - PVAR nm txp
            @ !ty | force (viceType ss #[] txp)
            | seq | force (go {let.val} e SOME-ty val)
            | go {let-body} (tabPut e nm ty) mExpect body

    - EREC nm txp val body
        @ !ty | force (viceType ss #[] txp)
        | trk [=ty]
        | trk [tabPut e nm ty]
        @ !e (tabPut e nm ty)
        | if (mExpect == SOME 0) die-[=mExpect]
        | trk [=e =mExpect]
        | seq | force (go {erec.head} e SOME-ty val)
        | go {erec.body} e mExpect body

    - ECAS _ _ _
        | maybeCase mExpect TNAT id

    - EFUN inlined pinned name args resTy body
        @ funTy | foldr TFUN resTy (map snd args)
        | maybeCase mExpect natRoot id
        ; TODO

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

    - _
        | {typecheck: malformed exp} exp


@@ 1135,16 1145,22 @@ ex=(ETUP ((EAPP (EAPP EREF-{add} ENAT-2) ENAT-3), ENAT-4, ENAT-5))

ex=(readExp '(const x/Nat y/Bit >Nat ? x))

=?= ex                  | EFUN 0 0 "const" ([%x TNAT], [%y TBIT]) TNAT EREF-{x}
=?= (compile ss ex)     | F (LAM 0 0 0 %const 2 V-1)
=?= (evaluate ss ex)    | (const x y ? x)
=?= (typecheck ss 0 ex) | TFUN TNAT (TFUN TBIT TNAT)
(funcType a b)=(tyApp Fun [a b])
(mkFun xs)=(foldr1 funcType xs)

=?= ex                     | EFUN 0 0 "const" ({x},TNAT, {y},TBIT) TNAT EREF-{x}

=?= (compile ss ex)        | F (LAM 0 0 0 %const 2 V-1)

=?= (TFUN TNAT (TFUN TBIT TNAT))
=?= (evaluate ss ex)       | (const x y ? x)

=?= (typecheck ss NONE ex) | mkFun [natRoot bitRoot natRoot]

=?= mkFun-[natRoot bitRoot natRoot]
  | typecheck ss NONE
  | readExp '(x/Nat y/Bit >Nat)&x

=?= TNAT
=?= natRoot
  | typecheck ss NONE
  | readExp '((x/Nat y/Bit >Nat & x) 3 true)



@@ 1154,11 1170,11 @@ 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)
     ++ tyApp Pair [natRoot bitRoot]
     ++ L K-3 | apple_ (K (cow 2), apple_ (eqlRef, K 1, K 1), V 0)
     ++ [3 TRUE]
  @ x   | readExp ' @ x/Nat 3 (x, true==true)


@@ 1170,12 1186,15 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))

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

> Typ > Row (Nat, Constructor) > Row (Str, Sire, Typ, Bst Str Any)
> DataType
> Type
> Row (Nat, Constructor Type)
> Row (Str, Sire, Type, Bst Str Any)
= (adtBinds adt newtype branches)
: (name, tag, fieldTypes) < foreach branches
@ arity | len fieldTypes
@ type  | foldr TFUN newtype fieldTypes
^ (name, _, type, bstSing {adt} adt)
@ type  | foldr funcType newtype fieldTypes
^ (name, _, [0 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))


@@ 1183,13 1202,13 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
= (recordBind adt newtype cnstr@(name, tag, fieldTypes))
; trk [=cnstr]
@ arity     | len fieldTypes
@ type      | foldr TFUN newtype fieldTypes
@ type      | foldr funcType newtype fieldTypes
| ifz arity | adtBinds adt newtype [cnstr]
^ (name, _, type, bstSing {adt} adt)
^ (name, _, [0 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)
> DataType > Type > Row (Nat, Constructor Type) > Row (Str, Sire, Type, Bst Str Any)
= (constructorBinds adt newtype branches)
| if (len branches == 1)
* [(recordBind adt newtype (idx 0 branches))]


@@ 1197,23 1216,21 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))

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


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

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

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


@@ 1233,19 1250,10 @@ 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)

    | trk "DERP",[=ss]

    # case cmd

    - _


@@ 1264,7 1272,7 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
          # right value was $$yVl

    - ASSERT x
        @ !typ | typecheck ss (SOME TBIT) x
        @ !_ty | typecheck ss (SOME bitRoot) x
        @ plan | evaluate ss x
        | trk ` !! $(showExp x)
        | if (plan == 1) ss


@@ 1274,9 1282,17 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))

    - DATA legible typeName cnstrs

        @ (newtype, ss) | mkNewType typeName 0 ss
        | trk [=legible =typeName =cnstrs]

        @ (newtype@[_ ntt], ss) | mkNewType typeName 0 ss

        | trk [=newtype =ntt]

        @ resolve (resolveType ss typeName (TDAT newtype))
        @ resolve (viceType ss (tabSing typeName ntt))

        | trk [resolve=[viceType %ss (tabSing typeName ntt)]]

        | trk [=ss]

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


@@ 1285,30 1301,32 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))

        @ adt ^ PIN [newtype (tabFromPairs _)]
              : (n, t, fields) < foreach branches
              | (n, (t,fields))
              | (n, (t, fields))

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

        | trk [=branches adt=(pinItem adt)]

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

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

    - BIND name exp
        @ !type | typecheck ss NONE exp
        @ !sire | compile ss exp
        | doBind ss (name, sire, type, bstEmpty)
        | doBind ss (name, sire, [0 type], bstEmpty)

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

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



@@ 1375,8 1393,8 @@ t==true ; compare t to true, using the above information during
     # expression true
     # reason
         # type mismatch
         # expected=($$Nat)
         # actual=($$Bit)
         # expected=Nat
         # actual=Bit

#=?= (#| tryVice '(add 1 true))
   ^ LEFT (#| v2 {viceroy-error} _)


@@ 1385,8 1403,8 @@ t==true ; compare t to true, using the above information during
         true
     # reason
         # type mismatch
         # expected=($$Nat)
         # actual=($$Bit)
         # expected=Nat
         # actual=Bit


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


@@ 1425,7 1443,7 @@ s3=(SOME 3)
#| PIN
#| v2 MaybeNat
#| %[NONE SOME]
#| v2 (#| v2 %SOME (#| v1 TNAT))
#| v2 (#| v2 %SOME (#| v1 natRoot))
      (#| v2 %NONE v0)

= ex & (x/Nat >Nat)


@@ 1457,7 1475,7 @@ s3=(SOME 3)
#| PIN
#| v2 MaybeNat
#| %[NONE SOME]
#| v2 (#| v2 1 (#| v1 TNAT))
#| v2 (#| v2 1 (#| v1 natRoot))
      (#| v2 0 v0)