Theory Shallow_Micro_Rust.Tuple

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Tuple
  imports
    Core_Expression
begin
(*>*)

datatype tnil = TNil

abbreviation(input) tuple_base_pair :: ‹('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
                                        ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
                                        ('s, 'arg0 × 'arg1 × tnil, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_base_pair ≡ bindlift2 (λx y. (x, y, TNil))›

abbreviation(input) tuple_cons :: ‹('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
                                   ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
                                   ('s, 'arg0 × 'arg1, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_cons ≡ bindlift2 (λx y. (x, y))›

abbreviation(input) tuple_index_0 :: ‹('s, 'arg0 × 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_0 ≡ bindlift1 fst›

abbreviation(input) tuple_index_1 :: ‹('s, 'arg0 × 'arg1 × 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_1 ≡ bindlift1 (fst ∘ snd)›

abbreviation(input) tuple_index_2 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_2 ≡ bindlift1 (fst ∘ snd ∘ snd)›

abbreviation(input) tuple_index_3 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_3 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_4 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_4 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd)›

abbreviation(input) tuple_index_5 :: ‹('s, 'arg0 × 'arg1 × 'arg2 × 'arg3 × 'arg4 × 'arg5 × 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
                                      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression› where
  ‹tuple_index_5 ≡ bindlift1 (fst ∘ snd ∘ snd ∘ snd ∘ snd ∘ snd)›

(*<*)
end
(*>*)