module hoare-test where

open import Data.Nat hiding (_⊔_)
open import Level renaming ( suc to succ ; zero to Zero )

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Relation.Nullary hiding (proof)

open import Data.Nat.Properties as NatProp -- <-cmp

record Env : Set where
  field
    var-init-x : ℕ
    var-init-y : ℕ
    var-x : ℕ
    var-y : ℕ
open Env

plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
plus-com env next exit with var-y env
... | zero  = exit record env{var-x = var-x env ; var-y = zero}
... | suc y = next record env{var-x = suc (var-x env) ; var-y = y}

plus-init : {l : Level} {t : Set l} → ( x y : ℕ ) → (next : Env → t) → t
plus-init x y next = next (record { var-init-x = x ; var-init-y = y ; var-x = x ; var-y = y })

{-# TERMINATING #-}
plus-p : {l : Level} {t : Set l} → (env : Env) → (exit : Env → t) → t
plus-p env exit = plus-com env ( λ env → plus-p env exit ) exit

plus : ℕ → ℕ → Env
plus x y = plus-init x y (λ env →  plus-p env (λ env → env))
--(record { varx = x ; vary = y }) (λ env → env)

-- ここまでplusの定義

-- mdg (meta code gear)
data mdg-state : Set where
  s-init  : mdg-state
  s-doing : mdg-state
  s-fin   : mdg-state

record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   field
      proj1 : A
      proj2 : B

-- mcg (meta code gear)
plus-mdg : mdg-state → Env → Set
plus-mdg s-init  env = (var-x env ≡ var-init-x env) ∧ (var-y env ≡ var-init-y env)
plus-mdg s-doing env = (var-init-x env ≡ var-init-x env) ∧ (var-init-y env ≡ var-init-y env) -- よくないmdg
plus-mdg s-fin   env = (var-init-x env ≡ var-init-x env) ∧ (var-init-y env ≡ var-init-y env) -- よくないmdg

-- 実行のwrapperを作って，そこでmcgが適切に選ばれて接続をしたい．多分できる気がする．
plus-init-mcg : {l : Level} {t : Set l} → (x y : ℕ) →  ((env : Env ) → plus-mdg s-init env → t) → t
plus-init-mcg x y next = next ( plus-init x y ( λ env → env ) ) record { proj1 = refl ; proj2 = refl } where

plus-com-mcg : {l : Level} {t : Set l} → (env : Env ) → (next : (env : Env ) → plus-mdg s-doing env  → t) → (exit : (env : Env ) → plus-mdg s-fin env → t) → t
plus-com-mcg env-in next exit with (var-y env-in)
... | suc y = next ( plus-com env-in ( λ env → env ) ( λ env → env ) ) (record { proj1 = refl ; proj2 = refl }) where
... | zero = exit env-in (record { proj1 = refl ; proj2 = refl })

--plus-com-mcg
{-# TERMINATING #-}
plus-p-mcg : {l : Level} {t : Set l} → (env : Env) → (exit : (env : Env ) → plus-mdg s-fin env → t) → t
plus-p-mcg env exit = plus-com-mcg env (λ env s → plus-p-mcg env exit ) exit

plus-mcg : (x y : ℕ) → Env
plus-mcg x y = plus-init-mcg x y (λ env s → plus-p-mcg env (λ env s → env))

test1 = plus-mcg 3 4

{-
next env ? where
   env : Env
   env = plus-com env-in {!!} {!!}
-}
--plus-mdg s-init (plus-p record env{var-x = var-init-x env ; var-y = var-init-y env} (λ env → env))



{-
whileTestPwP  : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
   env : Envc
   env = whileTestP c10 ( λ env → env )
-}

data hoare-cond : Set where
  p : hoare-cond
  q : hoare-cond


{-
continuation-hoare-triple : {l : Level} {t : Set l} → hoare-cond → (next : Env → t) Set
continuation-hoare-triple p next = continuation-hoare-triple q
continuation-hoare-triple q next = continuation-hoare-triple p
-}