if-let.isle

(spec (lower arg) (provide (= result arg)))
(decl lower (Inst) InstOutput)

;; Instruction formats.
(type MInst (enum))

;; Constructor to test whether two values are same.
(spec (same_value x y) (provide (= result x ) (= x y)))
(decl pure same_value (Value Value) Value)
(extern constructor same_value same_value)

(rule (lower (has_type (fits_in_64 ty) (iadd x y)))
      (if-let z (same_value x y))
      (add ty z z))

(spec (add ty a b)
  (provide 
    (= result 
       (if (<= ty 32) 
           (conv_to 64 (bvadd (extract 31 0 a) (extract 31 0 b)))
           (bvadd a b)))))
(decl add (Type Reg Reg) Reg)
(extern constructor add add)