llee454
commented
4 years ago - [x] Create the Tagged Union data type
- [x] Tagged Union is an approximation of the "Abstract Data Types" of Haskell. It consists of a list of (String * Kind) pairs (just like Kami Struct), where the String represents the "name" of the constructor, and Kind represents the type of the info this constructor holds. Eg: "Either Value Error = Left Value | Right Error" in haskell can be written as [ ("left", Data), ("right", Error) ]
- [x] getTaggedUnionRaw: forall (ls: list (String * Kind)), (TaggedUnion ls) @# ty -> (Pair (Tag ls) (Data ls)) @# ty
- [x] Data: list (String * Kind) -> Kind (Raw bit vector containing the maximum data that this tagged union holds)
- [x] Tag: list (String * Kind) -> Kind (= Bit (log2_up (length list))
- [x] getTaggedUnionKind: forall (ls: (String * Kind)) (s: String), Kind
- [x] getTaggedUnionDataTypecast: forall (ls: (String * Kind)) (e: Data ls @# ty) (s: String), Maybe (getTaggedUnionKind ls s) @# ty -- the Maybe represents whether "e" contained the data corresponding to the string "s"
- [x] createTaggedUnion: forall (ls: (String * Kind)) s (e: getTaggedUnionKind ls s @# ty), Pair (Tag ls) (Data ls) @# ty
vmurali