module SystemFpred where

open import Data.Bool renaming (Bool to Boolean)
open import Relation.Binary.PropositionalEquality


record ↑ (a : Set) : Set1 where
  field
    value : a

up : ∀{a} -> a -> ↑ a
up a = record { value = a }

eqProp : ∀{p} -> (x y : T p) -> x ≡ y
eqProp {true} x y = refl
eqProp {false} () y


module Type (tvar : Set1) where
  mutual
    data type : Set1 where
      Bool : type
      _⇒_ : type → type → type
      Var : (x : tvar) → type
      Π : (tvar → type) → type
      inj : (t : type) -> {p : T (isMono t)} -> type

    isMono : type -> Boolean
    isMono Bool = true
    isMono (Var x) = true
    isMono (a ⇒ b) = isMono a ∧ isMono b
    isMono x = false 
  isPoly : type -> Boolean
  isPoly (Π _) = true
  isPoly (inj _) = true
  isPoly _ = false

open Type

π₁ : ∀ {a b} -> T (a ∧ b) -> T a
π₁ {true} p = (_) 
π₁ {false} ()
π₂ : ∀ {a b} -> T (a ∧ b) -> T b
π₂ {_} {true} p = (_)
π₂ {true} {false} ()
π₂ {false} {false} ()

⌊_,_⌋m : (t : type Set) -> T (isMono Set t) -> Set
⌊ Bool , p ⌋m = Boolean 
⌊ _⇒_ a b , p ⌋m = ⌊ a , π₁ p ⌋m → ⌊ b , π₂ {isMono Set a} p ⌋m
⌊ Var x , p ⌋m = x 
⌊_,_⌋m (Π _) ()
⌊_,_⌋m (inj _) ()


⌊_⌋p : type Set -> Set1
⌊ Π f ⌋p = (x : Set) → ⌊ f x ⌋p
⌊ inj m {p} ⌋p = ↑ ⌊ m , p ⌋m
⌊ _⇒_ a b ⌋p = ⌊ a ⌋p → ⌊ b ⌋p 
⌊_⌋p Bool = ↑ Boolean
⌊_⌋p (Var t) = ↑ t

module Subst {tvar : Set1} where
  data _$_≡_ : (tvar → type tvar) → type tvar → type tvar → Set1 where
    SBool : ∀ t → (λ _ → Bool) $ t ≡ Bool
    SVarEq : ∀ {t p} → (λ x -> inj (Var x)) $ t ≡ inj t {p}
    SVarNeq : ∀ {v t} → (λ _ → inj (Var v)) $ t ≡ inj (Var v)
    S⇒ : ∀ {t1 t2 t1' t2' t} →
      t1 $ t ≡ t1'
     → t2 $ t ≡ t2'
     → (λ v → (t1 v ⇒ t2 v)) $ t ≡ (t1' ⇒ t2')
    SΠ : ∀ {t1 : _ → _ } {t1' t} →
       (∀ v' → (λ v → t1 v v') $ t ≡ t1' v')
       → (λ v → Π (t1 v)) $ t ≡ Π t1'

open Subst


mutual 
  cast : {t1 : Set -> type Set} {t2 : type Set} {t1' : type Set} -> (p : T (isMono Set t2)) -> t1 $ t2 ≡ t1' -> ⌊ t1 ⌊ t2 , p ⌋m ⌋p -> ⌊ t1' ⌋p
  cast {._} {t2} p (SBool .t2) term = term 
  cast p (SVarEq {_} {p'}) term with p  | p' | eqProp p p' 
  ...                              | .x | x  | refl = term 
  cast p SVarNeq term = term 
  cast {._} {t2} p (S⇒ y y') term = λ t1'v -> cast p y' (term (cast' p y t1'v)) 
  cast p (SΠ y) term = λ x -> cast p (y x) (term x) 
  
  cast' : {t1 : Set -> type Set} {t2 : type Set} {t1' : type Set} -> (p : T (isMono Set t2)) -> t1 $ t2 ≡ t1' -> ⌊ t1' ⌋p -> ⌊ t1 ⌊ t2 , p ⌋m ⌋p
  cast' {.(λ _ → Bool)} {t2} p (SBool .t2) term = term 
  cast' p (SVarEq {_} {p'}) term with p  | p' | eqProp p p'
  ...                               | .x | x  | refl = term 
  cast' p SVarNeq term = term
  cast' {._} {t2} p (S⇒ y y') term = λ t1'v -> cast' p y' (term (cast p y t1'v))
  cast' p (SΠ y) term = λ x -> cast' p (y x) (term x) 


module Term {tvar : Set1} {v : type tvar → Set1} where
  private ty = type tvar 
  data term : ty → Set1 where
    Var : ∀{t} → v t → term t
    True : term (inj Bool)
    False : term (inj Bool)
    Λ : ∀ {t1 : tvar -> ty} → (∀ v → term (t1 v)) → term (Π t1)
    _[_]_ : ∀ {t1 : tvar -> ty} → term (Π t1) → (t2 : type tvar ) {m : T (isMono tvar t2)} → {t1' : ty} → t1 $ t2 ≡ t1' → term t1'
    _$_ : ∀{a b} -> (f : term (a ⇒ b)) (x : term a) -> term b
    Lam : ∀{a b} -> (f : v a -> term b) -> term (a ⇒ b)
  
  var : tvar -> ty 
  var = λ a -> inj (Var a)
 -- inferred, id : term (Π (λ x → inj (Var x) ⇒ inj (Var x)))
  id = Λ λ a -> Lam {var a} λ x -> Var x
  flip = Λ λ a → Λ λ b → Λ λ c → Lam {var a ⇒ (var b ⇒ var c)} λ f → Lam λ x → Lam  λ y → (Var f $ Var y) $ Var x
--  idBool : (inj Bool ⇒ inj Bool)
  idBool = id [ Bool ] (S⇒ SVarEq SVarEq)
  idBoolBool = id [ Bool ⇒ Bool ] (S⇒ SVarEq SVarEq) 
  appid : {t : type tvar} -> {p : T (isMono tvar t)} -> term (inj t {p} ⇒ inj t {p})
  appid {t} {p} = _[_]_ id t {p} (S⇒ SVarEq SVarEq)
  idBoolBool' = appid {Bool ⇒ Bool}
  true' : term (inj Bool)
  true' = appid $ True
{-  appflip : ∀ (t : ty)  p -> term (Π
    (λ b →
       Π
       (λ c →
          (inj t {p} ⇒ (inj (Var b) ⇒ inj (Var c))) ⇒
          (inj (Var b) ⇒ (inj t {p} ⇒ inj (Var c))))))-}
  appflip : ∀ _ _  -> _
  appflip = λ a p → _[_]_ flip a {p} 
    (SΠ (λ v -> SΠ (λ v' -> (S⇒ (S⇒ (SVarEq {_} {_} {p}) (S⇒ SVarNeq SVarNeq)) (S⇒ SVarNeq (S⇒ (SVarEq {_} {_} {p}) SVarNeq))))))
open Term

⟦_⟧ : ∀ {t} -> term {Set} {⌊_⌋p} t -> ⌊ t ⌋p
⟦ Var x ⟧ = x 
⟦ True ⟧ = up true 
⟦ False ⟧ = up false
⟦ Λ y ⟧ = λ x → ⟦ y x ⟧
⟦ _[_]_ pi t2 {p} sub ⟧ = cast p sub (⟦ pi ⟧ ⌊ t2 , p ⌋m)
⟦ f $ x ⟧ = ⟦ f ⟧ ⟦ x ⟧
⟦ Lam f ⟧ = λ x → ⟦ f x ⟧


-- inferred, (x : Set) → ↑ x → ↑ x
id' = ⟦ id ⟧