stlc-model10.agda

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ; _+_; suc)
open import Data.Nat.Properties using (+-cancel-≡; +-comm; +-assoc; _<?_; +-suc)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product
open import Data.Fin hiding (suc; strengthen; _<?_) renaming (_+_ to _Fin+_)
open import Data.Vec
open import Relation.Binary.PropositionalEquality
open import Data.Bool using (true; false)

data `Type : Set where
  `False : `Type
  `Base : `Type
  `Fun : `Type -> `Type -> `Type

data Syn {Var : Set} : Set where
  `base : Syn
  `lam : (Var -> Syn {Var}) -> Syn {Var}
  `app : Syn {Var} -> Syn {Var} -> Syn
  `var : Var -> Syn

module Typing (Var : Set) (IsType : Var -> `Type -> Set) where
  data ⊢_∈_  : Syn {Var} -> `Type -> Set where

    IVar : ∀ {A} ->
      (m : Var) ->
      (D : (IsType m A)) ->
      -------------------------
      ⊢ `var m ∈ A

    IFun-I : ∀ {A B} ->
      {e : (Var -> Syn {Var})} ->
      ((v : Var) -> (D : (IsType v A)) ->
        ⊢ (e v) ∈ B) ->
      ----------------------
      ⊢ `lam e ∈ `Fun A B

    IFun-E : ∀ {A B e1 e2} ->
      ⊢ e1 ∈ `Fun A B ->
      ⊢ e2 ∈ A ->
      ------------------
      ⊢ `app e1 e2 ∈ B

    IBase-I :
      ----------------
      ⊢ `base ∈ `Base

module tests where
  Var : Set
  IsType : Var -> `Type -> Set
  open Typing(Var)(IsType)
  example1 : ⊢ (`lam `var) ∈ `Fun `Base `Base
  example1 = IFun-I IVar

  example2 : ⊢ (`app (`lam `var) `base) ∈ `Base
  example2 = IFun-E (IFun-I IVar) IBase-I

sub : ∀ {Var : Set} -> Syn {Syn {Var}} -> Syn {Var}
sub `base = `base
sub (`lam f) = `lam λ x → (sub (f (`var x)))
sub (`app e1 e2) = `app (sub e1) (sub e2)
sub (`var e) = e

Term1 = ∀ {Var : Set} -> Var -> Syn {Var}
Term = ∀ {Var : Set} -> Syn {Var}

Sub : Term1 -> Term -> Term
Sub e1 e2 {Var} = sub (e1 {Syn {Var}} (e2 {Var}))

data _⟶_ {Var : Set} : Syn {Syn {Var}} -> Syn {Var} -> Set where
  β : ∀ {f : (Syn {Var}) -> Syn {Syn {Var}}}
    {e2 : Syn {Syn {Var}}} ->
    ----------------------------------------
    (`app (`lam f) e2) ⟶ (sub (f (sub e2)))

  capp1 : ∀ {e1 e2 e1'} ->
    e1 ⟶ e1' ->
    ----------------------------
    (`app e1 e2) ⟶ (`app e1' (sub e2))

  capp2 : ∀ {e1 e2 e2'} ->
    e2 ⟶ e2' ->
    ----------------------------
    (`app e1 e2) ⟶ (`app (sub e1) e2')


module tests' where
  Var : Set
  _ : (`app (`lam `var) `base) ⟶ `base
  _ = β

module Foo where
  Var : Set
  IsType : Var -> `Type -> Set
  open Typing(Var)(IsType)

  IsType' : (Syn {Var}) -> `Type -> Set
  IsType' e A = ⊢ e ∈ A

  open Typing(Syn {Var})(IsType') renaming (⊢_∈_ to ⊢'_∈_)

  sub-lemma : ∀
    {e A} ->
    (⊢' e ∈ A) ->
    (⊢ (sub e) ∈ A)
  sub-lemma (Typing.IVar m D) = D
  sub-lemma (Typing.IFun-I Df) = Typing.IFun-I λ v D → (sub-lemma (Df (`var v) (IVar v D)))
  sub-lemma (Typing.IFun-E D D₁) = Typing.IFun-E (sub-lemma D) (sub-lemma D₁)
  sub-lemma Typing.IBase-I = Typing.IBase-I

  subject-reduction : ∀ {A} {e e'} ->
                      (⊢' e ∈ A) -> (e ⟶ e') ->
                      (⊢ e' ∈ A)
  subject-reduction {e = `app (`lam e1) e2} {e' = e'} (IFun-E (IFun-I D) Darg) β =
    (sub-lemma (D (sub e2) (sub-lemma Darg)))
  subject-reduction {e = `app e1 e2} (IFun-E D D₁) (capp1 step) =
    Typing.IFun-E (subject-reduction D step) (sub-lemma D₁)
  subject-reduction {e = `app e1 e2} (IFun-E D D₁) (capp2 step) =
    Typing.IFun-E (sub-lemma D) (subject-reduction D₁ step)