module STLC where
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_)
open import Data.Nat.Properties using (m≤m+n)
open import Data.List using (List; []; _∷_; length)
open import Data.Product using (_×_; uncurry; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Nullary.Decidable using (map′)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong; cong₂)
infix  4 _⊢_
infix  4 _∋_
infixl 5 _,_
infixl 5 `λ_
infixr 7 _`⇒_
infixl 7 _`$_
infix  8 `S_
infix  9 `_
Id : Set
Id = ℕ
data Ty : Set where
 `ℕ   : Ty
 _`⇒_ : Ty → Ty → Ty
module _ where
  -- without map′, cong₂ and `⇒-dec
  `⇒-inj₁ : ∀ {τ τ' σ σ'} → τ `⇒ σ ≡ τ' `⇒ σ' → τ ≡ τ'
  `⇒-inj₁ refl = refl
  
  `⇒-inj₂ : ∀ {τ τ' σ σ'} → τ `⇒ σ ≡ τ' `⇒ σ' → σ ≡ σ'
  `⇒-inj₂ refl = refl
  
  _≡?_ :  (τ : Ty) → (σ : Ty) → Dec (τ ≡ σ)
  `ℕ ≡? `ℕ = yes refl
  `ℕ ≡? (_ `⇒ _) = no (λ ())
  (_ `⇒ _) ≡? `ℕ = no (λ ())
  (τ `⇒ σ) ≡? (τ' `⇒ σ') with τ ≡? τ'
  ((τ `⇒ σ) ≡? (τ' `⇒ σ')) | yes τ≡τ' with σ ≡? σ'  
  ((τ `⇒ σ) ≡? (τ' `⇒ σ')) | yes τ≡τ'  | yes σ≡σ' rewrite τ≡τ' rewrite σ≡σ' = yes refl
  ((τ `⇒ σ) ≡? (τ' `⇒ σ')) | yes τ≡τ'  | no ¬σ≡σ' = no (λ p → ¬σ≡σ' (`⇒-inj₂ p))
  ((τ `⇒ σ) ≡? (τ' `⇒ σ')) | no ¬τ≡τ'  = no (λ p → ¬τ≡τ' (`⇒-inj₁ p))
`⇒-inj : ∀ {τ τ' σ σ'} → τ `⇒ σ ≡ τ' `⇒ σ' → τ ≡ τ' × σ ≡ σ'
`⇒-inj refl = ⟨ refl , refl ⟩
{--
map′ : (P → Q) → (Q → P) → Dec P → Dec Q
cong₂ : x ≡ y → u ≡ v → f x u ≡ f y v
--}
`⇒-dec :  ∀ {τ τ' σ σ'} → Dec (τ ≡ τ' × σ ≡ σ') → Dec (τ `⇒ σ ≡ τ' `⇒ σ')
`⇒-dec prf = map′ (uncurry (cong₂ _`⇒_)) `⇒-inj prf
_≟_ :  (τ : Ty) → (σ : Ty) → Dec (τ ≡ σ)
`ℕ ≟ `ℕ                 = yes refl
`ℕ ≟ (_ `⇒ _)           = no (λ ())
(_ `⇒ _) ≟ `ℕ           = no (λ ())
(t `⇒ t₁) ≟ (t' `⇒ t'') = `⇒-dec (t ≟ t' ×-dec t₁ ≟ t'')
Ctx : Set
Ctx = List Ty
_,_ : ∀ {A : Set} → List A → A → List A
Γ , τ = τ ∷ Γ
_∋_ : ∀ {A} → List A → A -> Set
Γ ∋ τ = Any (λ σ -> σ ≡ τ) Γ
private
  variable
    Γ Δ : Ctx
    τ τ' σ σ' : Ty
    n m : ℕ
data Arrow : Ty → Set where
  arrow : Arrow (τ `⇒ σ)
  
arrow? : (τ : Ty) → Dec (Arrow τ)
arrow? `ℕ       = no (λ ())
arrow? (τ `⇒ σ) = yes arrow
index : Γ ∋ τ → ℕ
index (here px) = zero
index (there p) = suc (index p)
data Lookup (Γ : Ctx) : ℕ → Set where
  inside : (τ : Ty) → (p : Γ ∋ τ) → Lookup Γ (index p)
  outside : (m : ℕ) → Lookup Γ (length Γ + m)
_!_ : (Γ : Ctx) → (m : ℕ) → Lookup Γ m
[] ! m         = outside m
(x ∷ Γ) ! zero = inside x (here refl)
(x ∷ Γ) ! suc m with Γ ! m
... | inside τ p = inside τ (there p)
... | outside m  = outside m
data UTerm : Set where
  `_     : Id → UTerm
  `λ_∙_  : Ty → UTerm → UTerm
  `let_`in_ : UTerm → UTerm → UTerm
  `Z     : UTerm
  `S_    : UTerm → UTerm
  `ucase : UTerm → UTerm → UTerm → UTerm
  _`$_   : UTerm → UTerm → UTerm
data _⊢_ : Ctx → Ty → Set where
  `_   : Γ ∋ τ
         --------
         → Γ ⊢ τ
  `λ_  : Γ , τ ⊢ σ
         --------------
         → Γ ⊢ τ `⇒ σ  
  `let_`in_ : Γ ⊢ τ
              → Γ , τ ⊢ σ
              ------------
              → Γ ⊢ σ
              
  `Z   : Γ ⊢ `ℕ
  `S_  : Γ ⊢ `ℕ
         ----------
         →  Γ ⊢ `ℕ
         
  `case_[Z⇒_|S⇒_] :
          Γ ⊢ `ℕ
          → Γ ⊢ τ
          → Γ , `ℕ ⊢ τ
          --------------
          → Γ ⊢ τ
         
  _`$_ : Γ ⊢ τ `⇒ σ
         → Γ ⊢ τ
         ---------
         → Γ ⊢ σ
erase : Γ ⊢ τ → UTerm
erase (` x)             = ` index x
erase {Γ}{τ `⇒ σ}(`λ t) = `λ τ ∙ erase t
erase (`let t `in t₁) = `let erase t `in erase t₁
erase `Z                = `Z
erase (`S t)            = `S erase t
erase (`case n [Z⇒ t₁ |S⇒ t₂ ]) = `ucase (erase n) (erase t₁) (erase t₂)
erase (t `$ t₁)         = erase t `$ erase t₁
data _⊬_ : Ctx → UTerm → Set where
  ill-scoped       : length Γ ≤ n →  Γ ⊬ (` n)
  not-a-nat-S      : (t : Γ ⊢ τ) → τ ≢ `ℕ → Γ ⊬ (`S erase t)
  not-a-nat-case   : ∀ {a b} → (n : Γ ⊢ τ) → τ ≢ `ℕ → Γ ⊬ (`ucase (erase n) a b)
  not-a-function   : ∀ {a} → (f : Γ ⊢ τ) → ¬ Arrow τ → Γ ⊬ (erase f `$ a)
  ty-mismatch-app  : (f : Γ ⊢ τ `⇒ σ) → (a : Γ ⊢ τ') → τ ≢ τ' → Γ ⊬ ((erase f) `$ (erase a))
  ty-mismatch-case : ∀ {n} → (a :  Γ ⊢ τ) → (b : Γ , `ℕ ⊢ σ) → τ ≢ σ → Γ ⊬ (`ucase n (erase a) (erase b))
  propagate-λ      : ∀ {t} → (Γ , τ) ⊬ t → Γ ⊬ (`λ τ ∙ t) 
  propagate-let₀   : ∀ {t t₁} → Γ ⊬ t → Γ ⊬ (`let t `in t₁)
  propagate-let₁   : ∀ {t t₁}{τ} → (Γ , τ) ⊬ t₁ → Γ ⊬ (`let t `in t₁)
  propagate-S      : ∀ {t} → Γ ⊬ t → Γ ⊬ (`S t)
  propagate-left   : ∀ {f a} → Γ ⊬ f → Γ ⊬ (f `$ a) 
  propagate-right  : ∀ {f a} → Γ ⊬ a → Γ ⊬ (f `$ a) 
  propagate-case-n : ∀ {n a b} → Γ ⊬ n → Γ ⊬ (`ucase n a b)
  propagate-case-Z : ∀ {n a b} → Γ ⊬ a → Γ ⊬ (`ucase n a b)
  propagate-case-S : ∀ {n a b} → (Γ , `ℕ) ⊬ b → Γ ⊬ (`ucase n a b)
  
data Infer (Γ : Ctx) : UTerm → Set where
  inf : (τ : Ty) → (t : Γ ⊢ τ) → Infer Γ (erase t)
  bad : {t : UTerm} → Γ ⊬ t → Infer Γ t
infer : (Γ : Ctx) → (t : UTerm) → Infer Γ t
infer Γ (` x)              with Γ ! x
infer Γ (` .(index p))      | inside τ p = inf τ (` p)
infer Γ (` .(length Γ + m)) | outside m  = bad (ill-scoped (m≤m+n (length Γ) m))
infer Γ (`λ τ ∙ t)         with infer (Γ , τ) t
infer Γ (`λ τ ∙ .(erase t)) | inf σ t = inf (τ `⇒ σ) (`λ t)
infer Γ (`λ τ ∙ t)          | bad e   = bad (propagate-λ e)
infer Γ (`let t `in t₁)                  with infer Γ t
infer Γ (`let .(erase t) `in t₁)          | inf τ t with infer (Γ , τ) t₁
infer Γ (`let .(erase t) `in .(erase t₁)) | inf τ t  | inf σ t₁ = inf σ (`let t `in t₁)
infer Γ (`let .(erase t) `in t₁)          | inf τ t  | bad x = bad (propagate-let₁ x)
infer Γ (`let t `in t₁)                   | bad x = bad (propagate-let₀ x)
infer Γ `Z = inf `ℕ `Z
infer Γ (`S t)         with infer Γ t
infer Γ (`S .(erase t)) | inf `ℕ t       = inf `ℕ (`S t)
infer Γ (`S .(erase t)) | inf (τ `⇒ τ₁) t = bad (not-a-nat-S t (λ ()))
infer Γ (`S t)          | bad e           = bad (propagate-S e)
infer Γ (`ucase n t₁ t₂)                             with infer Γ n
infer Γ (`ucase .(erase n) t₁ t₂)                     | inf `ℕ n with infer Γ t₁
infer Γ (`ucase .(erase n) .(erase t₁) t₂)            | inf `ℕ n  | inf τ t₁ with infer (Γ , `ℕ) t₂
infer Γ (`ucase .(erase n) .(erase t₁) .(erase t₂))   | inf `ℕ n  | inf τ t₁  | inf σ t₂ with τ ≟ σ
infer Γ (`ucase .(erase n) _ .(erase t₂))             | inf `ℕ n  | inf τ t₁  | inf σ t₂  | yes τ≡σ rewrite τ≡σ = inf σ `case n [Z⇒ t₁ |S⇒ t₂ ]
infer Γ (`ucase .(erase n) .(erase t₁) .(erase t₂))   | inf `ℕ n  | inf τ t₁  | inf σ t₂  | no ¬τ≡σ = bad (ty-mismatch-case t₁ t₂ ¬τ≡σ)
infer Γ (`ucase .(erase n) .(erase t₁) t₂)            | inf `ℕ n | inf τ t₁ | bad e = bad (propagate-case-S e)
infer Γ (`ucase .(erase n) t₁ t₂)                     | inf `ℕ n | bad e = bad (propagate-case-Z e)
infer Γ (`ucase .(erase n) t₁ t₂)                     | inf (τ `⇒ τ₁) n = bad (not-a-nat-case n (λ ()))
infer Γ (`ucase n t₁ t₂)                              | bad x = bad (propagate-case-n x)
infer Γ (f `$ a)                   with infer Γ f
infer Γ (.(erase t) `$ a)           | inf `ℕ t = bad (not-a-function t (λ ()))
infer Γ (.(erase t) `$ a)           | inf (τ `⇒ σ) t with infer Γ a
infer Γ (.(erase t) `$ .(erase t₁)) | inf (τ `⇒ σ) t  | inf τ₁ t₁ with τ ≟ τ₁
infer Γ (_ `$ .(erase t₁))          | inf (τ `⇒ σ) t  | inf τ₁ t₁  | yes τ≡τ₁ rewrite τ≡τ₁ = inf σ (t `$ t₁)
infer Γ (.(erase t) `$ .(erase t₁)) | inf (τ `⇒ σ) t  | inf τ₁ t₁  | no ¬τ≡τ₁ = bad (ty-mismatch-app t t₁ ¬τ≡τ₁)
infer Γ (.(erase t) `$ a)           | inf (τ `⇒ σ) t  | bad e = bad (propagate-right e)
infer Γ (f `$ a)                    | bad e = bad (propagate-left e)

{ pkgs ? import <nixpkgs> { } }:
with pkgs;
mkShell {
  buildInputs = [
    (agda.withPackages (ps: [
      ps.standard-library
    ]))
];
}
    

{ nixpkgs ? <nixpkgs> }:
with (import nixpkgs {});
agdaPackages.mkDerivation {
  version = "1.0";
  pname = "code-transformation";
  src = ./.;
  buildInputs = [
    agdaPackages.standard-library
  ];
}

name: code-transformation
include: src
depend: standard-library