6daa55af82
This latest refactor adds "extractor macros" in place of the very-confusing-even-to-the-DSL-author reverse-rules-as-extractors concept. It was beautifully symmetric but also just too mind-bending to be practical. It also adds argument polarity to external extractors. This is inspired by Prolog's similar notion (see e.g. the "+x" vs. "-x" argument notation in library documentation) where the unification-based semantics allow for bidirectional flow through arguments. We don't want polymorphism or dynamism w.r.t. directions/polarities here; the polarities are static; but it is useful to be able to feed values *into* an extractor (aside from the one value being extracted). Semantically this still correlates to a term-rewriting/value-equivalence world since we can still translate all of this to a list of equality constraints. To make that work, this change also adds expressions into patterns, specifically only for extractor "input" args. This required quite a bit of internal refactoring but is only a small addition to the language semantics. I plan to build out the little instruction-selector sketch further but the one that is here (in `test3.isle`) is starting to get interesting already with the current DSL semantics.
66 lines
1.8 KiB
Plaintext
66 lines
1.8 KiB
Plaintext
(type Opcode extern (enum
|
|
Iadd
|
|
Isub
|
|
Load
|
|
Store))
|
|
|
|
(type Inst (primitive Inst))
|
|
(type InstInput (primitive InstInput))
|
|
(type Reg (primitive Reg))
|
|
(type u32 (primitive u32))
|
|
|
|
(decl Op (Opcode) Inst)
|
|
(extern extractor Op get_opcode)
|
|
|
|
(decl InstInput (InstInput u32) Inst)
|
|
(extern extractor InstInput get_inst_input (out in))
|
|
|
|
(decl Producer (Inst) InstInput)
|
|
(extern extractor Producer get_input_producer)
|
|
|
|
(decl UseInput (InstInput) Reg)
|
|
(extern constructor UseInput put_input_in_reg)
|
|
|
|
(type MachInst (enum
|
|
(Add (a Reg) (b Reg))
|
|
(Add3 (a Reg) (b Reg) (c Reg))
|
|
(Sub (a Reg) (b Reg))))
|
|
|
|
(decl Lower (Inst) MachInst)
|
|
|
|
;; Extractors that give syntax sugar for (Iadd ra rb), etc.
|
|
;;
|
|
;; Note that this is somewhat simplistic: it directly connects inputs to
|
|
;; MachInst regs; really we'd want to return a VReg or InstInput that we can use
|
|
;; another extractor to connect to another (producer) inst.
|
|
;;
|
|
;; Also, note that while it looks a little indirect, a verification effort could
|
|
;; define equivalences across the `rule` LHS/RHS pairs, and the types ensure that
|
|
;; we are dealing (at the semantic level) with pure value equivalences of
|
|
;; "terms", not arbitrary side-effecting calls.
|
|
|
|
(decl Iadd (InstInput InstInput) Inst)
|
|
(decl Isub (InstInput InstInput) Inst)
|
|
(extractor
|
|
(Iadd a b)
|
|
(and
|
|
(Op (Opcode.Iadd))
|
|
(InstInput a <0)
|
|
(InstInput b <1)))
|
|
(extractor
|
|
(Isub a b)
|
|
(and
|
|
(Op (Opcode.Isub))
|
|
(InstInput a <0)
|
|
(InstInput b <1)))
|
|
|
|
;; Now the nice syntax-sugar that "end-user" backend authors can write:
|
|
(rule
|
|
(Lower (Iadd ra rb))
|
|
(MachInst.Add (UseInput ra) (UseInput rb)))
|
|
(rule
|
|
(Lower (Iadd (Producer (Iadd ra rb)) rc))
|
|
(MachInst.Add3 (UseInput ra) (UseInput rb) (UseInput rc)))
|
|
(rule
|
|
(Lower (Isub ra rb))
|
|
(MachInst.Sub (UseInput ra) (UseInput rb))) |