Commit 7912ea6d authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Cleaned up Pirouette.v

parent ab81157d
This diff is collapsed.
This diff is collapsed.
Require Import Coq.Structures.Orders Coq.Structures.Equalities.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Lists.SetoidList.
Require Import Coq.FSets.FMapInterface.
Require Import Coq.Program.Wf.
Require Import Coq.Sorting.Permutation.
Require Import Coq.Sorting.Mergesort.
(*
A module describing the properties of locations in
Pirouette. Locations are simply any Set with a
......
This diff is collapsed.
This diff is collapsed.
......@@ -4,32 +4,34 @@ Require Export LocalLang.
Require Export TypedLocalLang.
Require Export SoundlyTypedLocalLang.
Module SoundlyTypedPirouette (Import LL : LocalLang) (Import TLL : TypedLocalLang LL) (Import STLL : SoundlyTypedLocalLang LL TLL) (L : Locations).
Include (TypedPirouette L LL TLL).
Module SoundlyTypedPirouette (Import LL : LocalLang) (Import TLL : TypedLocalLang LL)
(Import STLL : SoundlyTypedLocalLang LL TLL)
(L : Locations) (Import SL : SyncLabels).
Include (TypedPirouette L LL TLL SL).
Theorem Preservation:
forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (C : Chor) (τ : ChorTyp),
Γ;; Δ c C ::: τ -> forall (R : Redex) (B : list L.t) (C': Chor),
ChorStep R B C C' -> Γ;; Δ c C' ::: τ.
forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> PirTyp) (C : PirExpr) (τ : PirTyp),
Γ;; Δ c C ::: τ -> forall (R : Redex) (B : list L.t) (C': PirExpr),
PirStep R B C C' -> Γ;; Δ c C' ::: τ.
Proof.
apply RelativePreservation. intros Γ e τ H e' H0.
apply ExprPreservation with (e1 := e); auto.
Qed.
Theorem StepsPreservation :
forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (C : Chor) (τ : ChorTyp),
Γ;; Δ c C ::: τ -> forall (Rs : list Redex) (B : list L.t) (C': Chor),
ChorSteps Rs B C C' -> Γ;; Δ c C' ::: τ.
forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> PirTyp) (C : PirExpr) (τ : PirTyp),
Γ;; Δ c C ::: τ -> forall (Rs : list Redex) (B : list L.t) (C': PirExpr),
PirSteps Rs B C C' -> Γ;; Δ c C' ::: τ.
Proof.
apply RelativeStepsPreservation. intros Γ e τ H e' H0.
apply ExprPreservation with (e1 := e); auto.
Qed.
Theorem Progress :
forall (C : Chor) (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ : ChorTyp),
ChorClosed C -> Γ;; Δ c C ::: τ ->
ChorVal C \/ exists R C', ChorStep R nil C C'.
forall (C : PirExpr) (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> PirTyp) (τ : PirTyp),
PirExprClosed C -> Γ;; Δ c C ::: τ ->
PirExprVal C \/ exists R C', PirStep R nil C C'.
Proof.
apply RelativeProgress; auto.
intros e τ Γ H H0; eapply ExprProgress; eauto.
......
(*
A module defining synchronization labels. They are a choice of left or right. They have
decidable equality. By having them in their own module, we can share them between
Pirouette and the control language.
*)
Module Type SyncLabels.
Inductive SyncLabel := Left | Right.
Definition SyncLabelEqDec : forall d1 d2 : SyncLabel, {d1 = d2} + {d1 <> d2}.
decide equality.
Defined.
End SyncLabels.
This diff is collapsed.
......@@ -12,6 +12,7 @@ SoundlyTypedNatLang.v
Locations.v
LocationMap.v
FunLMap.v
SyncLabels.v
Pirouette.v
TypedPirouette.v
SoundlyTypedPirouette.v
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment