{-# OPTIONS --safe --without-K #-}
module IS4.Applications.IS4Plus where

open import Relation.Nullary using (_because_; yes; no)

open import Relation.Binary.Definitions           using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≑_ ; refl ; cong ; congβ‚‚)

-- IS4 with extensions

data Ty : Set where
  Unit : Ty
  𝕔    : Ty
  _β‡’_  : Ty β†’ Ty β†’ Ty
  β—»_   : Ty β†’ Ty
  Bool : Ty

variable
    a b c d : Ty

Ty-Decidable : Decidable (_≑_ {A = Ty})
Ty-Decidable Unit    Unit    = yes refl
Ty-Decidable Unit    Bool    = no  Ξ» ()
Ty-Decidable Unit    𝕔       = no  Ξ» ()
Ty-Decidable Unit    (a β‡’ b) = no  Ξ» ()
Ty-Decidable Unit    (β—» a)   = no  Ξ» ()
Ty-Decidable Bool    Unit    = no  Ξ» ()
Ty-Decidable Bool    Bool    = yes refl
Ty-Decidable Bool    𝕔       = no  Ξ» ()
Ty-Decidable Bool    (a β‡’ b) = no  Ξ» ()
Ty-Decidable Bool    (β—» a)   = no  Ξ» ()
Ty-Decidable 𝕔       Unit    = no  Ξ» ()
Ty-Decidable 𝕔       Bool    = no  Ξ» ()
Ty-Decidable 𝕔       𝕔       = yes refl
Ty-Decidable 𝕔       (a β‡’ b) = no  Ξ» ()
Ty-Decidable 𝕔       (β—» a)   = no  Ξ» ()
Ty-Decidable (a β‡’ b) Unit    = no  Ξ» ()
Ty-Decidable (a β‡’ b) Bool    = no  Ξ» ()
Ty-Decidable (a β‡’ b) 𝕔       = no  Ξ» ()
Ty-Decidable (a β‡’ b) (c β‡’ d) with Ty-Decidable a c | Ty-Decidable b d
... | yes a≑c  | yes b≑d     = yes (congβ‚‚ _β‡’_ a≑c b≑d)
... | yes a≑c  | no  Β¬b≑d    = no  Ξ» { refl β†’ Β¬b≑d refl }
... | no  Β¬a≑c | yes b≑d     = no  Ξ» { refl β†’ Β¬a≑c refl }
... | no  Β¬a≑c | no  Β¬b≑d    = no  Ξ» { refl β†’ Β¬a≑c refl }
Ty-Decidable (a β‡’ b) (β—» c)   = no  Ξ» ()
Ty-Decidable (β—» a)   Unit    = no  Ξ» ()
Ty-Decidable (β—» a)   Bool    = no  Ξ» ()
Ty-Decidable (β—» a)   𝕔       = no  Ξ» ()
Ty-Decidable (β—» a)   (b β‡’ c) = no  Ξ» ()
Ty-Decidable (β—» a)   (β—» b)   with Ty-Decidable a b
... | yes a≑b                = yes (cong β—»_ a≑b)
... | no  Β¬a≑b               = no  Ξ» { refl β†’ Β¬a≑b refl }

open import Context Ty Ty-Decidable hiding (ext#) public

------------------------------------
-- Variables, terms and substituions
------------------------------------

data Tm : Ctx β†’ Ty β†’ Set where

  var  : Var Ξ“ a
       ---------
       β†’ Tm Ξ“ a

  lam  : Tm (Ξ“ `, a) b
         -------------
       β†’ Tm Ξ“ (a β‡’ b)

  app  : Tm Ξ“ (a β‡’ b) β†’ Tm Ξ“ a
         ---------------------
       β†’ Tm Ξ“ b

  box   : Tm (Ξ“ #) a
        ------------
        β†’ Tm Ξ“ (β—» a)

  unbox : Tm Ξ“L (β—» a) β†’ CExt Ξ“ Ξ“L Ξ“R
        ----------------------------
        β†’ Tm Ξ“ a

  unit : Tm Ξ“ Unit

  true  : Tm Ξ“ Bool

  false : Tm Ξ“ Bool

  ifte  : CExt Ξ“ Ξ“L Ξ“R β†’ Tm Ξ“L Bool β†’ Tm Ξ“ a β†’ Tm Ξ“ a β†’ Tm Ξ“ a

TM : Ty β†’ Ctx β†’ Set
TM a Ξ“ = Tm Ξ“ a

wkTm : Ξ“ βŠ† Ξ“' β†’ Tm Ξ“ a β†’ Tm Ξ“' a
wkTm w (var x)     = var (wkVar w x)
wkTm w (lam t)     = lam (wkTm (keep w) t)
wkTm w (app t u)   = app (wkTm w t) (wkTm w u)
wkTm w (box t)     = box (wkTm (keep# w) t)
wkTm w (unbox t e) = unbox (wkTm (factorWk e w) t) (factorExt e w)
wkTm w unit = unit
wkTm w true = true
wkTm w false = false
wkTm w (ifte e t t₁ tβ‚‚) = ifte (factorExt e w) (wkTm (factorWk e w) t) (wkTm w t₁) (wkTm w tβ‚‚)

open import Data.Unit  using (⊀ ; tt)
open import Data.Product  using (Ξ£ ; _Γ—_ ; _,_ ) renaming (projβ‚‚ to snd)

---------------
-- Normal forms
---------------
data Ne : Ctx β†’ Ty β†’ Set
data Nf : Ctx β†’ Ty β†’ Set

data Ne where
  var   : Var Ξ“ a β†’ Ne Ξ“ a
  app   : Ne Ξ“ (a β‡’ b) β†’ Nf Ξ“ a β†’ Ne Ξ“ b
  unbox : Ne Ξ“L (β—» a) β†’ CExt Ξ“ Ξ“L Ξ“R β†’ Ne Ξ“ a

data Nf where
  up    : Ne Ξ“ 𝕔 β†’ Nf Ξ“ 𝕔
  lam   : Nf (Ξ“ `, a) b β†’ Nf Ξ“ (a β‡’ b)
  box   : Nf (Ξ“ #) a β†’ Nf Ξ“ (β—» a)
  true  : Nf Ξ“ Bool
  false : Nf Ξ“ Bool
  ifte  : CExt Ξ“ Ξ“L Ξ“R β†’ Ne Ξ“L Bool β†’ Nf Ξ“ a β†’ Nf Ξ“ a β†’ Nf Ξ“ a
  unit  : Nf Ξ“ Unit

-- embedding into terms

embNe : Ne Ξ“ a β†’ Tm Ξ“ a
embNf : Nf Ξ“ a β†’ Tm Ξ“ a

embNe (var x)     = var x
embNe (app m n)   = app (embNe m) (embNf n)
embNe (unbox n x) = unbox (embNe n) x

embNf (up  x)          = embNe x
embNf (lam n)          = lam (embNf n)
embNf (box n)          = box (embNf n)
embNf true             = true
embNf false            = false
embNf (ifte x x₁ n n₁) = ifte x true (embNf n) (embNf n₁)
embNf unit             = unit

-- weakening lemmas

wkNe : Ξ“ βŠ† Ξ“' β†’ Ne Ξ“ a β†’ Ne Ξ“' a
wkNf : Ξ“ βŠ† Ξ“' β†’ Nf Ξ“ a β†’ Nf Ξ“' a

wkNe w (var   x)   = var (wkVar w x)
wkNe w (app   m n) = app (wkNe w m) (wkNf w n)
wkNe w (unbox n e) = unbox (wkNe (factorWk e w) n) (factorExt e w)

wkNf w (up  x)         = up  (wkNe w x)
wkNf w (lam n)         = lam (wkNf (keep w) n)
wkNf w (box n)         = box (wkNf (keep# w) n)
wkNf w true            = true
wkNf w false           = false
wkNf w (ifte e m n n₁) = ifte (factorExt e w) (wkNe (factorWk e w) m) (wkNf w n) (wkNf w n₁)
wkNf w unit            = unit

NF NE : Ty β†’ Ctx β†’ Set
NF a Ξ“ = Nf Ξ“ a
NE a Ξ“ = Ne Ξ“ a

------------
-- NbE Model
------------

variable
  A B C : Ctx β†’ Set

-- family of maps between interpretations
_β†’Μ‡_ : (Ctx β†’ Set) β†’ (Ctx β†’ Set) β†’ Set
_β†’Μ‡_ A B = {Ξ” : Ctx} β†’ A Ξ” β†’ B Ξ”

infixr 10 _β†’Μ‡_

-- constructions on context-indexed families of sets
_β‡’'_ : (Ctx β†’ Set) β†’ (Ctx β†’ Set) β†’ (Ctx β†’ Set)
_β‡’'_ A B Ξ“ = {Ξ“' : Ctx} β†’ Ξ“ βŠ† Ξ“' β†’ A Ξ“' β†’ B Ξ“'

_Γ—'_ : (Ctx β†’ Set) β†’ (Ctx β†’ Set) β†’ (Ctx β†’ Set)
_Γ—'_ A B Ξ“ = A Ξ“ Γ— B Ξ“

Box : (Ctx β†’ Set) β†’ (Ctx β†’ Set)
Box A Ξ“L = {Ξ“L' Ξ“ Ξ“R : Ctx} β†’ Ξ“L βŠ† Ξ“L' β†’ CExt Ξ“ Ξ“L' Ξ“R β†’ A Ξ“

-- semantic counterpart of `lock` from `Sub`
data Lock (A : Ctx β†’ Set) : Ctx β†’ Set where
  lock : A Ξ“L β†’ CExt Ξ“ Ξ“L Ξ“R  β†’ Lock A Ξ“

⊀' : (Ctx β†’ Set)
⊀' = Ξ» Ξ“ β†’ ⊀

data Cov (A : Ctx β†’ Set) : Ctx β†’ Set where
  ret    : A Ξ“ β†’ Cov A Ξ“
  ifte'  : CExt Ξ“ Ξ“L Ξ“R β†’ NE Bool Ξ“L β†’ Cov A Ξ“ β†’ Cov A Ξ“ β†’ Cov A Ξ“

wkCov : (Ξ“ βŠ† Ξ“' β†’ A Ξ“ β†’ A Ξ“') β†’ Ξ“ βŠ† Ξ“' β†’ Cov A Ξ“ β†’ Cov A Ξ“'
wkCov wk w (ret x)
  = ret (wk w x)
wkCov wk w (ifte' e n m m₁)
  = ifte' (factorExt e w) (wkNe (factorWk e w) n) (wkCov wk w m) (wkCov wk w m₁)

fmapCov : (A β†’Μ‡ B) β†’ (Cov A β†’Μ‡ Cov B)
fmapCov f (ret x) = ret (f x)
fmapCov f (ifte' e x m m₁) = ifte' e x (fmapCov f m) (fmapCov f m₁)

mapCov : (A β‡’' B) β†’Μ‡ (Cov A β‡’' Cov B)
mapCov f w (ret x) = ret (f w x)
mapCov f w (ifte' e x m m₁) = ifte' e x (mapCov f w m) (mapCov f w m₁)

joinCov : Cov (Cov A) β†’Μ‡ Cov A
joinCov (ret m) = m
joinCov (ifte' e x m m₁) = ifte' e x (joinCov m₁) (joinCov m₁)

bindCov : (A β‡’' Cov B) β†’Μ‡ (Cov A β‡’' Cov B)
bindCov f e m = joinCov (mapCov f e m)

collect : Cov (NF a) β†’Μ‡ NF a
collect (ret x) = x
collect (ifte' e x m m₁) = ifte e x (collect m) (collect m₁)

open import Data.Bool renaming (Bool to Bool')

Tm'- : Ty β†’ (Ctx β†’ Set)
Tm'- Unit    = ⊀'
Tm'- 𝕔       = Cov (NE 𝕔)
Tm'- (a β‡’ b) = (Tm'- a) β‡’' (Tm'- b)
Tm'- (β—» a)  = Box (Tm'- a)
Tm'- Bool    = Cov (Ξ» _ β†’ Bool')

Sub'- : Ctx β†’ (Ctx β†’ Set)
Sub'- []       = ⊀'
Sub'- (Ξ“ `, a) = Sub'- Ξ“ Γ—' Tm'- a
Sub'- (Ξ“ #)    = Lock (Sub'- Ξ“)

-- values in the model can be weakened
wkTm'- : Ξ“ βŠ† Ξ“' β†’ Tm'- a Ξ“ β†’ Tm'- a Ξ“'
wkTm'- {a = 𝕔}     w m  = wkCov wkNe w m
wkTm'- {a = a β‡’ b} w f  = Ξ» w' y β†’ f (w βˆ™ w') y
wkTm'- {a = β—» a}  w bx = Ξ» w' e β†’ bx (w βˆ™ w') e
wkTm'- {a = Unit}  w n  = tt
wkTm'- {a = Bool}  w m  = wkCov (Ξ» _ z β†’ z) w m

-- substitutions in the model can be weakened
wkSub'- : Ξ“ βŠ† Ξ“' β†’ Sub'- Ξ” Ξ“ β†’ Sub'- Ξ” Ξ“'
wkSub'- {Ξ” = []}     w tt          = tt
wkSub'- {Ξ” = Ξ” `, a} w (s , x)     = wkSub'- {Ξ” = Ξ”} w s , wkTm'- {a = a} w x
wkSub'- {Ξ” = Ξ” #}    w (lock s e)  = lock (wkSub'- {Ξ” = Ξ”} (factorWk e w) s) (factorExt e w)

-- semantic counterpart of `unbox` from `Tm`
unbox' : Box (Tm'- a) Ξ“L β†’ CExt Ξ“ Ξ“L Ξ“R β†’ Tm'- a Ξ“
unbox' bx e = bx idWk e

unboxCov : Cov (Box (Tm'- a)) Ξ” β†’ CExt Ξ“ Ξ” Ξ“R β†’ Cov (Tm'- a) Ξ“
unboxCov (ret x) e
  = ret (x idWk e)
unboxCov {a = a} (ifte' e' x m1 m2) e
  = ifte' (extRAssoc e' e) x (unboxCov {a = a} m1 e) (unboxCov {a = a} m2 e)

appCov : Cov (Tm'- (a β‡’ b)) Ξ“ β†’ Cov (Tm'- a) Ξ“ β†’ Cov (Tm'- b) Ξ“
runCov : Cov (Tm'- a) β†’Μ‡ Tm'- a

appCov {a = a} (ret f) m
  = ret (f idWk (runCov {a = a} m))
appCov {a = a} {b = b} (ifte' e n m1 m2) m
  = ifte' e n (appCov {a = a} {b = b} m1 m) (appCov {a = a} {b = b} m2 m)

runCov {Unit}   m
  = tt
runCov {𝕔}      m
  = joinCov m
runCov {a β‡’ b}  m
  = Ξ» w x β†’ runCov {b} (appCov {a = a} {b = b} (wkCov (wkTm'- {a = a β‡’ b}) w m) (ret x))
runCov {β—» a}   m
  = Ξ» w e β†’ runCov {a} (unboxCov {a = a} (wkCov (wkTm'- {a = β—» a}) w m) e)
runCov {Bool}   m
  = joinCov m

-------------------------
-- Normalization function
-------------------------

VAR : Ty β†’ Ctx β†’ Set
VAR a Ξ“ = Var Ξ“ a

reify   : Tm'- a β†’Μ‡ NF a
reflect : NE a  β†’Μ‡ Tm'- a

reify {Unit}  x = unit
reify {𝕔}     x = collect (mapCov (Ξ» _ n β†’ up n) idWk x)
reify {a β‡’ b} x = lam (reify {b} (x (drop idWk) (reflect {a} (var zero))))
reify {β—» a}   x = box (reify (x idWk (ext#- nil)))
reify {Bool}  x = true

reflect {Unit}  n = tt
reflect {𝕔}     n = ret n
reflect {a β‡’ b} n = Ξ» e t β†’ reflect {b} (app (wkNe e n) (reify t))
reflect {β—» a}   n = Ξ» w e β†’ reflect (unbox (wkNe w n) e)
reflect {Bool}  n = ifte' nil n (ret true) (ret false)

-- identity substitution
idβ‚›' : Sub'- Ξ“ Ξ“
idβ‚›' {[]}     = tt
idβ‚›' {Ξ“ `, a} = wkSub'- {Ξ” = Ξ“} (drop idWk) (idβ‚›' {Ξ“ = Ξ“}) , reflect {a} (var zero)
idβ‚›' {Ξ“ #}    = lock (idβ‚›' {Ξ“}) (ext#- nil)

-- interpretation of variables
substVar' : Var Ξ“ a β†’ (Sub'- Ξ“ β†’Μ‡ Tm'- a)
substVar' zero     (_ , x) = x
substVar' (succ x) (Ξ³ , _) = substVar' x Ξ³

unlock' : Sub'- (Ξ“ #) Ξ” β†’ Ξ£ (Ctx Γ— Ctx) Ξ» { (Ξ”L , Ξ”R) β†’ Sub'- Ξ“ Ξ”L Γ— CExt Ξ” Ξ”L Ξ”R }
unlock' (lock Ξ³ e) = _ , Ξ³ , e

CExt' : CExt Ξ“ Ξ“L Ξ“R β†’ Sub'- Ξ“ β†’Μ‡ Sub'- (Ξ“L #)
CExt' nil       Ξ³                         = lock Ξ³ nil
CExt' (ext e)   (Ξ³ , _)                   = CExt' e Ξ³
CExt' {Ξ“ = Ξ“} {Ξ“L} {Ξ“R} (ext#- e) (lock Ξ³ e') with unlock' {Ξ“ = Ξ“L} (CExt' e Ξ³) .snd
... | (Ξ³' , e'') = lock Ξ³' (extRAssoc e'' e')

eval-ifte : CExt Ξ“ Ξ“L Ξ“R β†’ Cov (Ξ» _ β†’ Bool') Ξ“L β†’ Cov A Ξ“ β†’ Cov A Ξ“ β†’ Cov A Ξ“
eval-ifte e (ret false)        m1 m2 = m2
eval-ifte e (ret true)         m1 m2 = m2
eval-ifte e (ifte' e' n c1 c2) m1 m2  = ifte' (extRAssoc e' e) n (eval-ifte e c1 m1 m2) (eval-ifte e c2 m1 m2)

-- interpretation of terms
eval : Tm Ξ“ a β†’ (Sub'- Ξ“ β†’Μ‡ Tm'- a)
eval (var x)                       s
  = substVar' x s
eval {Ξ“ = Ξ“} (lam t)               s
  = Ξ» e x β†’ eval t (wkSub'- {Ξ” = Ξ“} e s , x)
eval (app t u)                     s
  = (eval t s) idWk (eval u s)
eval {Ξ“ = Ξ“} (box t)               s
  = Ξ» w e β†’ eval t (lock (wkSub'- {Ξ” = Ξ“} w s) e)
eval {a = a} (unbox t nil)         s
  = unbox' {a = a} (eval t s) nil
eval (unbox t (ext e))             (s , _)
  = eval (unbox t e) s
eval (unbox t (ext#- e))           (lock s nil)
  = eval (unbox t e) s
eval {a = a} (unbox t (ext#- e))   (lock s (ext {a = b} e'))
  = wkTm'- {_} {_} {a} fresh[ b ] (eval (unbox t (ext#- e)) (lock s e'))
eval {a = a} (unbox t (ext#- nil)) (lock s (ext#- e'))
  = unbox' {a} (eval t s) (ext#- e')
eval (unbox t (ext#- (ext e)))     (lock (s , _) (ext#- e'))
  = eval (unbox t (ext#- e)) (lock s (ext#- e'))
eval (unbox t (ext#- (ext#- e)))   (lock (lock s e'') (ext#- e'))
  = eval (unbox t (ext#- e)) (lock s (ext#- (extRAssoc e'' e')))
eval unit                          s
  = tt
eval true                          s
  = ret true
eval false                         s
  = ret false
eval {Ξ“ = Ξ“} {a = a} (ifte {Ξ“L = Ξ“L} e t t₁ tβ‚‚) {Ξ” = Ξ”} s with unlock' {Ξ“ = Ξ“L} (CExt' e s)
... | ((Ξ“L' , Ξ“R') , s' , e')
  = runCov {a = a} (eval-ifte e' (eval t s') (ret (eval t₁ s)) (ret (eval t₁ s)))

-- retraction of interpretation
quot : (Sub'- Ξ“ β†’Μ‡ Tm'- a) β†’ Nf Ξ“ a
quot {Ξ“} f = reify (f (idβ‚›' {Ξ“}))

-- normalization function
norm : Tm Ξ“ a β†’ Nf Ξ“ a
norm t = quot (eval t)

Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.