Module Qcert.CAMP.Typing.TCAMPSugar

Require Import String.
Require Import List.
Require Import EquivDec.
Require Import Program.
Require Import Utils.
Require Import DataSystem.
Require Import CAMPSugar.
Require Export TCAMP.

Section TCAMPSugar.
  Local Open Scope camp_scope.

  Local Hint Constructors camp_type : qcert.

  Context {m:basic_model}.

  Lemma PTCast τc Γ br bs :
    [τc&Γ] |= pcast br ; (Brand bs) ~> (Brand br).

  Lemma PTSingleton τc Γ τ :
    [τc&Γ] |= psingleton ; (Coll τ) ~> τ.

  Lemma PTmapall τc {Γ : tbindings} {τ₁ τ₂ : rtype} {p : camp} :
    NoDup (domain Γ) ->
    ([τc&Γ] |= p; τ₁ ~> τ₂) -> [τc&Γ] |= mapall p; Coll τ₁ ~> Coll τ₂.

  Lemma PTmapall_inv τc {Γ : tbindings} {τ₁ τ₂ : rtype} {p : camp} :
    is_list_sorted ODT_lt_dec (domain Γ) = true ->
    [τc&Γ] |= mapall p; τ₁ ~> τ₂ ->
                       exists τ₁' τ₂',
                         τ₁ = Coll τ₁' /\
                         τ₂ = Coll τ₂' /\
                         ([τc&Γ] |= p; τ₁' ~> τ₂').

End TCAMPSugar.