Skip to content

Commit

Permalink
Update example of how data constructors are translated
Browse files Browse the repository at this point in the history
  • Loading branch information
krame505 authored and quark17 committed Feb 16, 2024
1 parent 62ea8c3 commit e1aa0fd
Showing 1 changed file with 10 additions and 13 deletions.
23 changes: 10 additions & 13 deletions doc/BH_ref_guide/BH_lang.tex
Original file line number Diff line number Diff line change
Expand Up @@ -1017,25 +1017,22 @@ \subsection{\te{data}}
Error messages involving data type definitions sometimes show traces
of how they are handled internally. Data type definitions are
translated into a data type where each constructor has exactly one
argument. Each argument is a struct type. The types above translate
argument. The types above translate
to:
\begin{verbatim}
data Bool = False PrimUnit | True PrimUnit
data Operand = Register Operand.Register
| Operand.Literal
| Operand.Indexed
struct Operand°Register = { _1 :: Bit 5 }
struct Operand°Literal = { _1 :: Bit 22 }
struct Operand°Indexed = { _1 :: Reg 5; _2 :: Reg 5 }
data Operand = Register (Bit 5)
| Literal (Bit 22)
| Indexed Operand_$Indexed
struct Operand_$Indexed = { _1 :: Reg 5; _2 :: Reg 5 }
data Maybe a = Nothing PrimUnit | Maybe.Just a
struct Maybe.Just a = { _1 :: a }
data Maybe a = Nothing PrimUnit | Just a
data Instruction = Immediate Instruction°Immediate |
Register Instruction°Register
struct Instruction°Immediate = { op::Op; rs::Reg; rt::CPUReg; imm::UInt16; }
struct Instruction°Register = { op::Op; target::UInt26; }
data Instruction = Immediate Instruction_$Immediate
| Register Instruction_$Register
struct Instruction_$Immediate = { op::Op; rs::Reg; rt::CPUReg; imm::UInt16; }
struct Instruction_$Register = { op::Op; target::UInt26; }
\end{verbatim}
\end{NOTE}

Expand Down

0 comments on commit e1aa0fd

Please sign in to comment.