### changeset 62:bfe7d83cf9ba

writeing Gears Semmantics of commands
author ryokka Sat, 21 Dec 2019 21:12:07 +0900 62dcb0ae2c94 222dd3869ab0 RelOp.agda whileTestGears.agda 2 files changed, 38 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
```--- a/RelOp.agda	Sat Dec 21 19:37:41 2019 +0900
+++ b/RelOp.agda	Sat Dec 21 21:12:07 2019 +0900
@@ -55,7 +55,6 @@
-- unionInf f = ⋃_{n ∈ ω} f(n)
unionInf : ∀ {l} -> (ℕ -> Rel S l) -> Rel S l
unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
-
-- restPre X R = { (s1,s2) ∈ R | s1 ∈ X }
restPre : ∀ {l} -> Pred S -> Rel S l -> Rel S l
restPre X R a b = X a × R a b```
```--- a/whileTestGears.agda	Sat Dec 21 19:37:41 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 21:12:07 2019 +0900
@@ -3,9 +3,11 @@
open import Function
open import Data.Nat
open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_)
+open import Data.Product
open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality
+open import Agda.Builtin.Unit

open import utilities
open  _/\_
@@ -174,11 +176,13 @@
c10 env
∎

+
+-- induction にする
{-# TERMINATING #-}
loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit

-
+--  wP を Env のRel にする  Env → Env → Set にしちゃう
whileTestPCallwP : (c :  ℕ ) → Set
whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c )  ) where
conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
@@ -191,10 +195,40 @@
-- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!}))

+data GComm : Set (succ Zero) where
+  Skip  : GComm
+  Abort : GComm
+  PComm : Set → GComm
+  -- Seq   : GComm → GComm → GComm
+  -- If   : whileTestState → GComm → GComm → GComm
+  while : whileTestState → GComm → GComm

-ProofConnect : {l : Level} {t : Set l} → (pr1 : Envc → Set → Set) → (Envc → Set → (Envc → Set → t)) → (pr2 : Envc → Set → Set)
-ProofConnect prev f env post with f env ({!!}) {!!}
-... | tt = {!!}
+gearsSem : {l : Level} {t : Set l} → {c10 : ℕ} → Envc → Envc → (Envc → (Envc → t) → t) → Set
+
+unionInf : ∀ {l} -> (ℕ -> Rel Set l) -> Rel Set l
+unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
+
+comp : ∀ {l} → Rel Set l → Rel Set l → Rel Set (succ Zero Level.⊔ l)
+comp r1 r2 a b = ∃ (λ (a' : Set) → r1 a a' × r2 a' b)
+
+-- repeat : ℕ -> rel set zero -> rel set zero
+-- repeat ℕ.zero r = λ x x₁ → ⊤
+-- repeat (ℕ.suc m) r = comp (repeat m r) r
+
+GSemComm : {l : Level} {t : Set l} → GComm → Rel whileTestState (Zero)
+GSemComm Skip = λ x x₁ → ⊤
+GSemComm Abort = λ x x₁ → ⊥
+GSemComm (PComm x) = λ x₁ x₂ → x
+-- GSemComm (Seq con con₁ con₃) = λ x₁ x₂ → {!!}
+-- GSemComm (If x con con₁) = {!!}
+GSemComm (while x con) = λ x₁ x₂ → unionInf {Zero} (λ (n : ℕ) →  {!!}) {!!} {!!}
+
+ProofConnect : {l : Level} {t : Set l}
+  → (pr1 : Envc → Set → Set)
+  → (Envc → Set → (Envc → Set → t))
+  → (Envc → Set → Set)
+ProofConnect prev f env post =  {!!} -- with f env ({!!}) {!!}

Proof2 : (env : Envc) → (vari env ≡ c10 env) → vari env ≡ c10 env
Proof2 _ refl = refl ```