module hoare-test where

open import Data.Nat hiding (_!$\sqcup$!_)
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 : !$\mathbb{N}$!
    var-init-y : !$\mathbb{N}$!
    var-x : !$\mathbb{N}$!
    var-y : !$\mathbb{N}$!
open Env

plus-com : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! 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} !$\rightarrow$! ( x y : !$\mathbb{N}$! ) !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! 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} !$\rightarrow$! (env : Env) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
plus-p env exit = plus-com env ( !$\lambda$! env !$\rightarrow$! plus-p env exit ) exit

plus : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Env
plus x y = plus-init x y (!$\lambda$! env !$\rightarrow$!  plus-p env (!$\lambda$! env !$\rightarrow$! env))
--(record { varx = x ; vary = y }) (!$\lambda$! env !$\rightarrow$! env)

-- ここまでplusの定義

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

record  _!$\wedge$!_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n !$\sqcup$! m) where
   field
      proj1 : A
      proj2 : B

-- mcg (meta code gear)
plus-mdg : mdg-state !$\rightarrow$! Env !$\rightarrow$! Set
plus-mdg s-init  env = (var-x env !$\equiv$! var-init-x env) !$\wedge$! (var-y env !$\equiv$! var-init-y env)
plus-mdg s-doing env = (var-init-x env !$\equiv$! var-init-x env) !$\wedge$! (var-init-y env !$\equiv$! var-init-y env) -- よくないmdg
plus-mdg s-fin   env = (var-init-x env !$\equiv$! var-init-x env) !$\wedge$! (var-init-y env !$\equiv$! var-init-y env) -- よくないmdg

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

plus-com-mcg : {l : Level} {t : Set l} !$\rightarrow$! (env : Env ) !$\rightarrow$! (next : (env : Env ) !$\rightarrow$! plus-mdg s-doing env  !$\rightarrow$! t) !$\rightarrow$! (exit : (env : Env ) !$\rightarrow$! plus-mdg s-fin env !$\rightarrow$! t) !$\rightarrow$! t
plus-com-mcg env-in next exit with (var-y env-in)
... | suc y = next ( plus-com env-in ( !$\lambda$! env !$\rightarrow$! env ) ( !$\lambda$! env !$\rightarrow$! 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} !$\rightarrow$! (env : Env) !$\rightarrow$! (exit : (env : Env ) !$\rightarrow$! plus-mdg s-fin env !$\rightarrow$! t) !$\rightarrow$! t
plus-p-mcg env exit = plus-com-mcg env (!$\lambda$! env s !$\rightarrow$! plus-p-mcg env exit ) exit

plus-mcg : (x y : !$\mathbb{N}$!) !$\rightarrow$! Env
plus-mcg x y = plus-init-mcg x y (!$\lambda$! env s !$\rightarrow$! plus-p-mcg env (!$\lambda$! env s !$\rightarrow$! 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} (!$\lambda$! env !$\rightarrow$! env))



{-
whileTestPwP  : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$! ((env : Envc ) !$\rightarrow$! whileTestStateP s1 env !$\rightarrow$! t) !$\rightarrow$! t
whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
   env : Envc
   env = whileTestP c10 ( !$\lambda$! env !$\rightarrow$! env )
-}

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


{-
continuation-hoare-triple : {l : Level} {t : Set l} !$\rightarrow$! hoare-cond !$\rightarrow$! (next : Env !$\rightarrow$! t) Set
continuation-hoare-triple p next = continuation-hoare-triple q
continuation-hoare-triple q next = continuation-hoare-triple p
-}