1;; Instruction formats.
2(type MInst (enum))
3
4(form
5  lhs_form
6  ((args Bool (bv 8) (bv 8)) (ret (bv 8)) (canon (bv 8)))
7  ((args Bool (bv 16) (bv 16)) (ret (bv 16)) (canon (bv 16)))
8  ((args Bool (bv 32) (bv 32)) (ret (bv 32)) (canon (bv 32)))
9  ((args Bool (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64)))
10)
11
12(spec (lhs cond x y)
13  (provide (= result (load_effect #x0000 (widthof (if cond x y)) (if cond x y)))))
14(decl lhs (bool Value Value) Inst)
15(extern extractor lhs lhs)
16(instantiate lhs lhs_form)
17
18(spec (rhs x y)
19  (provide (= result (load_effect #x0000 (widthof x) x))))
20(decl rhs (Value Value) Inst)
21(extern constructor rhs rhs)
22
23(rule (lhs true x y)
24  (rhs x y))
25