tests

module TestPrograms where

  data Maybe (A : Set) : Set where
    just : A → Maybe A
    nothing : Maybe A

  isJust : {A : Set} → Maybe A → Set
  isJust (just _) = Truth
  isJust nothing = Falsehood

  extract : {A : Set} → (m : Maybe A) → (_ : isJust m) → A
  extract (just e) _ = e
  extract nothing ()


  -- The definition of ¬ given in the assignment is flawed;
  -- the tests use this instead.
  not : Set → Set
  not A = A → Falsehood

  module ScopeTesting where
    open WellTypedPrograms
    open WellScopedPrograms

    test₁ : let S = localInt x In
                      x ≔ᴵ (const (pos zero))
                    end
            in
              (extract (just S) witness) WellScoped
    test₁ = {!!}

    test₂ : let S = localInt x In
                    if varᴵ x < const (pos (suc (suc zero)))
                      then localInt y In skip end
                      else localInt z In skip end
                    end
                  end
         in
         (extract (just S) witness) WellScoped
    test₂ = {!!}

    test₃ : let S = x ≔ᴵ const (pos zero)
         in
         not ((extract (just S) witness) WellScoped)
    test₃ = {!!}


  module InitialisationTesting where
    open WellTypedPrograms
    open WellInitialised

    test₁ : (extract (just skip) witness) WellInitialised
    test₁ = {!!}

    test₂ : let S = localInt x In
                    x ≔ᴵ const (pos zero)
                  end
            in
            (extract (just S) witness)  WellInitialised
    test₂ = {!!}

    -- This is well-scoped, but not well-initialised, as we use x
    -- before assigning to it.
    -- Case split on bad here until you reach ().
    test₃ : let S = localInt x In
                    if varᴵ x < const (pos (suc (suc zero)))
                      then localInt y In skip end
                      else localInt z In skip end
                    end
                  end
          in
          not ((extract (just S) witness)  WellInitialised)
    test₃ = {!!}

    -- This is not well-scoped, but is well-initialised.
    test₄ : let S = x ≔ᴵ const (pos zero)
          in
          (extract (just S) witness)  WellInitialised
    test₄ = {!!}

    -- similar to test₄, this is well-initialised, though not well-scoped
    test₅ : let S = x ≔ᴵ (const (pos zero)) ⨾
                 x ≔ᴵ (varᴵ x + const (pos (suc zero)))
          in
          (extract (just S) witness)  WellInitialised
    test₅ = {!!}