(* Open Source License *)
(* Copyright (c) 2019 Nomadic Labs. <contact@nomadic-labs.com> *)

(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)

(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)

(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)

Require Import syntax.
Require Import comparable.

Module Macros(C:ContractContext) (S : SYNTAX C).

Export S.

Definition CMPEQ {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) (bool ::: S) := COMPARE ;; EQ.
Definition CMPNEQ {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) (bool ::: S) := COMPARE ;; NEQ.
Definition CMPLT {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) (bool ::: S) := COMPARE ;; LT.
Definition CMPGT {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) (bool ::: S) := COMPARE ;; GT.
Definition CMPLE {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) (bool ::: S) := COMPARE ;; LE.
Definition CMPGE {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) (bool ::: S) := COMPARE ;; GE.

Definition IFEQ {self_type SA SB} (bt bf : instruction self_type SA SB) := EQ ;; IF_ bt bf.
Definition IFNEQ {self_type SA SB} (bt bf : instruction self_type SA SB) := NEQ ;; IF_ bt bf.
Definition IFLT {self_type SA SB} (bt bf : instruction self_type SA SB) := LT ;; IF_ bt bf.
Definition IFGT {self_type SA SB} (bt bf : instruction self_type SA SB) := GT ;; IF_ bt bf.
Definition IFLE {self_type SA SB} (bt bf : instruction self_type SA SB) := LE ;; IF_ bt bf.
Definition IFGE {self_type SA SB} (bt bf : instruction self_type SA SB) := GE ;; IF_ bt bf.

Definition IFCMPEQ {a : comparable_type} {self_type SA SB} bt bf :
  instruction self_type (a ::: a ::: SA) SB := COMPARE ;; EQ ;; IF_ bt bf.
Definition IFCMPNEQ {a : comparable_type} {self_type SA SB} bt bf :
  instruction self_type (a ::: a ::: SA) SB := COMPARE ;; NEQ ;; IF_ bt bf.
Definition IFCMPLT {a : comparable_type} {self_type SA SB} bt bf :
  instruction self_type (a ::: a ::: SA) SB := COMPARE ;; LT ;; IF_ bt bf.
Definition IFCMPGT {a : comparable_type} {self_type SA SB} bt bf :
  instruction self_type (a ::: a ::: SA) SB := COMPARE ;; GT ;; IF_ bt bf.
Definition IFCMPLE {a : comparable_type} {self_type SA SB} bt bf :
  instruction self_type (a ::: a ::: SA) SB := COMPARE ;; LE ;; IF_ bt bf.
Definition IFCMPGE {a : comparable_type} {self_type SA SB} bt bf :
  instruction self_type (a ::: a ::: SA) SB := COMPARE ;; GE ;; IF_ bt bf.

Definition FAIL {self_type SA SB} : instruction self_type SA SB := UNIT ;; FAILWITH.

Definition ASSERT {self_type S} : instruction self_type (bool ::: S) S := IF_ NOOP FAIL.

Definition ASSERT_EQ {self_type S} : instruction self_type (int ::: S) S := IFEQ NOOP FAIL.
Definition ASSERT_NEQ {self_type S} : instruction self_type (int ::: S) S := IFNEQ NOOP FAIL.
Definition ASSERT_LT {self_type S} : instruction self_type (int ::: S) S := IFLT NOOP FAIL.
Definition ASSERT_GT {self_type S} : instruction self_type (int ::: S) S := IFGT NOOP FAIL.
Definition ASSERT_LE {self_type S} : instruction self_type (int ::: S) S := IFLE NOOP FAIL.
Definition ASSERT_GE {self_type S} : instruction self_type (int ::: S) S := IFGE NOOP FAIL.

Definition ASSERT_CMPEQ {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) S := IFCMPEQ NOOP FAIL.
Definition ASSERT_CMPNEQ {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) S := IFCMPNEQ NOOP FAIL.
Definition ASSERT_CMPLT {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) S := IFCMPLT NOOP FAIL.
Definition ASSERT_CMPGT {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) S := IFCMPGT NOOP FAIL.
Definition ASSERT_CMPLE {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) S := IFCMPLE NOOP FAIL.
Definition ASSERT_CMPGE {a : comparable_type} {self_type S} :
  instruction self_type (a ::: a ::: S) S := IFCMPGE NOOP FAIL.

Definition ASSERT_NONE {self_type a S} : instruction self_type (option a ::: S) S :=
  IF_NONE NOOP FAIL.

Definition ASSERT_SOME {self_type a S} : instruction self_type (option a ::: S) (a ::: S) :=
  IF_NONE FAIL NOOP.

Definition ASSERT_LEFT {self_type a b an bn S} : instruction self_type (or a an b bn ::: S) (a ::: S) :=
  IF_LEFT NOOP FAIL.
Definition ASSERT_RIGHT {self_type a b an bn S} : instruction self_type (or a an b bn ::: S) (b ::: S) :=
  IF_LEFT FAIL NOOP.


Definition DIIP {self_type a b SA SB} code : instruction self_type (a ::: b ::: SA) (a ::: b ::: SB) :=
  DIP (DIP code).
Definition DIIIP {self_type a b c SA SB} code :
  instruction self_type (a ::: b ::: c ::: SA) (a ::: b ::: c ::: SB) :=
  DIP (DIIP code).
Definition DIIIIP {self_type a b c d SA SB} code :
  instruction self_type (a ::: b ::: c ::: d ::: SA) (a ::: b ::: c ::: d ::: SB) :=
  DIP (DIIIP code).

Definition DUUP {self_type a b S} : instruction self_type (a ::: b ::: S) (b ::: a ::: b ::: S) :=
  DIP DUP ;; SWAP.
Definition DUUUP {self_type a b c S} : instruction self_type (a ::: b ::: c ::: S) (c ::: a ::: b ::: c ::: S) :=
  DIP DUUP ;; SWAP.
Definition DUUUUP {self_type a b c d S} : instruction self_type (a ::: b ::: c ::: d ::: S) (d ::: a ::: b ::: c ::: d ::: S) :=
  DIP DUUUP ;; SWAP.

(* Missing: PAPPAIIR and such *)

Definition UNPAIR {self_type a b S} : instruction self_type (pair a b ::: S) (a ::: b ::: S) :=
  DUP ;; CAR ;; DIP CDR.

Definition CAAR {self_type a b c S} : instruction self_type (pair (pair a b) c ::: S) (a ::: S) :=
  CAR ;; CAR.

Definition CADR {self_type a b c S} : instruction self_type (pair (pair a b) c ::: S) (b ::: S) :=
  CAR ;; CDR.

Definition CDAR {self_type a b c S} : instruction self_type (pair a (pair b c) ::: S) (b ::: S) :=
  CDR ;; CAR.

Definition CDDR {self_type a b c S} : instruction self_type (pair a (pair b c) ::: S) (c ::: S) :=
  CDR ;; CDR.

Definition IF_SOME {self_type a SA SB} bt bf : instruction self_type (option a ::: SA) SB :=
  IF_NONE bf bt.

Definition SET_CAR {self_type a b S} : instruction self_type (pair a b ::: a ::: S) (pair a b ::: S) :=
  CDR ;; SWAP ;; PAIR.

Definition SET_CDR {self_type a b S} : instruction self_type (pair a b ::: b ::: S) (pair a b ::: S) :=
  CAR ;; PAIR.

Definition MAP_CAR {self_type a1 a2 b S} (code : instruction self_type (a1 ::: S) (a2 ::: S)) :
  instruction self_type (pair a1 b ::: S) (pair a2 b ::: S) :=
  DUP ;; CDR ;; DIP (CAR ;; code) ;; SWAP ;; PAIR.

Definition MAP_CDR {self_type a b1 b2 S} (code : instruction self_type (b1 ::: pair a b1 ::: S) (b2 ::: pair a b1 ::: S)) :
  instruction self_type (pair a b1 ::: S) (pair a b2 ::: S) :=
  DUP ;; CDR ;; code ;; SWAP ;; CAR ;; PAIR.


Definition UNPAPAIR {self_type a b c S} : instruction self_type (pair a (pair b c) ::: S) (a ::: b ::: c ::: S) :=
  UNPAIR ;; DIP UNPAIR.
Definition PAPAIR {self_type a b c S} : instruction self_type (a ::: b ::: c ::: S) (pair a (pair b c) ::: S) :=
  DIP PAIR;; PAIR.

End Macros.