https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 1af9370326ed6cc6dadf367f09efab5d3fb98322 authored by Guillaume Claret on 09 March 2020, 17:47:59 UTC
Merge branch 'guillaume-claret-add-entrypoint-to-self' into 'dev'
Merge branch 'guillaume-claret-add-entrypoint-to-self' into 'dev'
Tip revision: 1af9370
macros.v
(* 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 syntax_type.
Require Import comparable.
Section macros.
Context {self_type : Datatypes.option type}.
Definition CMPop (a : comparable_type) S (op : instruction self_type Datatypes.false (int ::: S) (bool ::: S))
: instruction self_type Datatypes.false (a ::: a ::: S) (bool ::: S) := COMPARE ;; op.
Definition CMPEQ {a S} := CMPop a S EQ.
Definition CMPNEQ {a S} := CMPop a S NEQ.
Definition CMPLT {a S} := CMPop a S LT.
Definition CMPGT {a S} := CMPop a S GT.
Definition CMPLE {a S} := CMPop a S LE.
Definition CMPGE {a S} := CMPop a S GE.
Definition IFop SA SB tffa tffb
(bt : instruction self_type tffa SA SB) (bf : instruction self_type tffb SA SB)
(op : instruction self_type Datatypes.false (int ::: SA) (bool ::: SA)) :=
op ;; IF_ bt bf.
Definition IFEQ {SA SB tffa tffb} bt bf := IFop SA SB tffa tffb bt bf EQ.
Definition IFNEQ {SA SB tffa tffb} bt bf := IFop SA SB tffa tffb bt bf NEQ.
Definition IFLT {SA SB tffa tffb} bt bf := IFop SA SB tffa tffb bt bf LT.
Definition IFGT {SA SB tffa tffb} bt bf := IFop SA SB tffa tffb bt bf GT.
Definition IFLE {SA SB tffa tffb} bt bf := IFop SA SB tffa tffb bt bf LE.
Definition IFGE {SA SB tffa tffb} bt bf := IFop SA SB tffa tffb bt bf GE.
Definition IFCMPop (a : comparable_type) SA SB tffa tffb
(bt : instruction self_type tffa SA SB) (bf : instruction self_type tffb SA SB)
(op : instruction self_type Datatypes.false (int ::: SA) (bool ::: SA)) :
instruction self_type (tffa && tffb) (a ::: a ::: SA) SB :=
COMPARE ;; op ;; IF_ bt bf.
Definition IFCMPEQ {a SA SB tffa tffb} bt bf := IFCMPop a SA SB tffa tffb bt bf EQ.
Definition IFCMPNEQ {a SA SB tffa tffb} bt bf := IFCMPop a SA SB tffa tffb bt bf NEQ.
Definition IFCMPLT {a SA SB tffa tffb} bt bf := IFCMPop a SA SB tffa tffb bt bf LT.
Definition IFCMPGT {a SA SB tffa tffb} bt bf := IFCMPop a SA SB tffa tffb bt bf GT.
Definition IFCMPLE {a SA SB tffa tffb} bt bf := IFCMPop a SA SB tffa tffb bt bf LE.
Definition IFCMPGE {a SA SB tffa tffb} bt bf := IFCMPop a SA SB tffa tffb bt bf GE.
Definition FAIL {SA SB} : instruction self_type Datatypes.true SA SB := UNIT ;; FAILWITH.
Definition ASSERT {S} : instruction self_type Datatypes.false (bool ::: S) S := IF_ NOOP FAIL.
Definition ASSERT_op S (op : instruction self_type Datatypes.false (int ::: S) (bool ::: S)) : instruction self_type Datatypes.false (int ::: S) S :=
IFop _ _ _ _ NOOP FAIL op.
Definition ASSERT_EQ {S} := ASSERT_op S EQ.
Definition ASSERT_NEQ {S} := ASSERT_op S NEQ.
Definition ASSERT_LT {S} := ASSERT_op S LT.
Definition ASSERT_GT {S} := ASSERT_op S GT.
Definition ASSERT_LE {S} := ASSERT_op S LE.
Definition ASSERT_GE {S} := ASSERT_op S GE.
Definition ASSERT_CMPop (a : comparable_type) S (op : instruction self_type Datatypes.false (int ::: S) (bool ::: S))
: instruction self_type Datatypes.false (a ::: a ::: S) S := IFCMPop _ _ _ _ _ NOOP FAIL op.
Definition ASSERT_CMPEQ {a S} := ASSERT_CMPop a S EQ.
Definition ASSERT_CMPNEQ {a S} := ASSERT_CMPop a S NEQ.
Definition ASSERT_CMPLT {a S} := ASSERT_CMPop a S LT.
Definition ASSERT_CMPGT {a S} := ASSERT_CMPop a S GT.
Definition ASSERT_CMPLE {a S} := ASSERT_CMPop a S LE.
Definition ASSERT_CMPGE {a S} := ASSERT_CMPop a S GE.
Definition ASSERT_NONE {a S} : instruction self_type Datatypes.false (option a ::: S) S :=
IF_NONE NOOP FAIL.
Definition ASSERT_SOME {a S} : instruction self_type Datatypes.false (option a ::: S) (a ::: S) :=
IF_NONE FAIL NOOP.
Definition ASSERT_LEFT {a b S} : instruction self_type Datatypes.false (or a b ::: S) (a ::: S) :=
IF_LEFT NOOP FAIL.
Definition ASSERT_RIGHT {a b S} : instruction self_type Datatypes.false (or a b ::: S) (b ::: S) :=
IF_LEFT FAIL NOOP.
Definition DROP1 {a SA} : instruction self_type Datatypes.false (a ::: SA) SA :=
DROP (A := a ::: nil) 1 eq_refl.
Definition DIP1 {a SA SB} code : instruction self_type _ (a ::: SA) (a ::: SB) :=
DIP (A := (a ::: nil)) 1 eq_refl code.
Definition DIIP {a b SA SB} code : instruction self_type _ (a ::: b ::: SA) (a ::: b ::: SB) :=
DIP (A := (a ::: b ::: nil)) 2 eq_refl code.
Definition DIIIP {a b c SA SB} code :
instruction self_type _ (a ::: b ::: c ::: SA) (a ::: b ::: c ::: SB) :=
DIP (A := (a ::: b ::: c ::: nil)) 3 eq_refl code.
Definition DIIIIP {a b c d SA SB} code :
instruction self_type _ (a ::: b ::: c ::: d ::: SA) (a ::: b ::: c ::: d ::: SB) :=
DIP (A := (a ::: b ::: c ::: d ::: nil)) 4 eq_refl code.
Definition DUUP {a b S} : instruction self_type Datatypes.false (a ::: b ::: S) (b ::: a ::: b ::: S) :=
DIP1 DUP ;; SWAP.
Definition DUPn {A b C} n (H : length A = n) : instruction self_type Datatypes.false (A +++ b ::: C) (b ::: A +++ b ::: C) :=
DIG n H ;; DUP ;; DIP1 (DUG n H).
Definition DUUUP {a b c S} : instruction self_type Datatypes.false (a ::: b ::: c ::: S) (c ::: a ::: b ::: c ::: S) :=
DUPn (A := a ::: b ::: nil) 2 eq_refl.
Definition DUUUUP {a b c d S} : instruction self_type Datatypes.false (a ::: b ::: c ::: d ::: S) (d ::: a ::: b ::: c ::: d ::: S) :=
DUPn (A := a ::: b ::: c ::: nil) 3 eq_refl.
(* Missing: PAPPAIIR and such *)
Definition UNPAIR {a b S} : instruction self_type Datatypes.false (pair a b ::: S) (a ::: b ::: S) :=
DUP ;; CAR ;; DIP1 CDR.
Definition CAAR {a b c S} : instruction self_type Datatypes.false (pair (pair a b) c ::: S) (a ::: S) :=
CAR ;; CAR.
Definition CADR {a b c S} : instruction self_type Datatypes.false (pair (pair a b) c ::: S) (b ::: S) :=
CAR ;; CDR.
Definition CDAR {a b c S} : instruction self_type Datatypes.false (pair a (pair b c) ::: S) (b ::: S) :=
CDR ;; CAR.
Definition CDDR {a b c S} : instruction self_type Datatypes.false (pair a (pair b c) ::: S) (c ::: S) :=
CDR ;; CDR.
Definition IF_SOME {a SA SB tffa tffb} (bt : instruction self_type tffa _ _) (bf : instruction self_type tffb _ _) : instruction self_type _ (option a ::: SA) SB :=
IF_NONE bf bt.
Definition IF_RIGHT {a b SA SB tffa tffb} (bt : instruction self_type tffa _ _) (bf : instruction self_type tffb _ _) : instruction self_type _ (or a b ::: SA) SB :=
IF_LEFT bf bt.
Definition SET_CAR {a b S} : instruction self_type Datatypes.false (pair a b ::: a ::: S) (pair a b ::: S) :=
CDR ;; SWAP ;; PAIR.
Definition SET_CDR {a b S} : instruction self_type Datatypes.false (pair a b ::: b ::: S) (pair a b ::: S) :=
CAR ;; PAIR.
Definition MAP_CAR {a1 a2 b S} (code : instruction self_type Datatypes.false (a1 ::: S) (a2 ::: S)) :
instruction self_type Datatypes.false (pair a1 b ::: S) (pair a2 b ::: S) :=
DUP ;; CDR ;; DIP1 (CAR ;; code) ;; SWAP ;; PAIR.
Definition MAP_CDR {a b1 b2 S} (code : instruction self_type Datatypes.false (b1 ::: pair a b1 ::: S) (b2 ::: pair a b1 ::: S)) :
instruction self_type Datatypes.false (pair a b1 ::: S) (pair a b2 ::: S) :=
DUP ;; CDR ;; code ;; SWAP ;; CAR ;; PAIR.
Definition UNPAPAIR {a b c S} : instruction self_type Datatypes.false (pair a (pair b c) :: S) (a ::: b ::: c ::: S) := UNPAIR ;; DIP1 UNPAIR.
Definition PAPAIR {a b c S} : instruction self_type Datatypes.false (a ::: b ::: c ::: S) (pair a (pair b c) :: S) := DIP1 PAIR;; PAIR.
End macros.