Agda-2.3.2.2: examples/outdated-and-incorrect/NBE.agda
-- NBE for Gödel System T
module NBE where
module Prelude where
-- Zero and One -----------------------------------------------------------
data Zero : Set where
data One : Set where
unit : One
-- Natural numbers --------------------------------------------------------
data Nat : Set where
zero : Nat
suc : Nat -> Nat
(+) : Nat -> Nat -> Nat
zero + m = m
suc n + m = suc (n + m)
-- Props ------------------------------------------------------------------
data True : Prop where
tt : True
data False : Prop where
postulate
falseE : (A:Set) -> False -> A
infix 3 /\
data (/\)(P Q:Prop) : Prop where
andI : P -> Q -> P /\ Q
module Fin where
open Prelude
-- Finite sets ------------------------------------------------------------
data Suc (A:Set) : Set where
fzero_ : Suc A
fsuc_ : A -> Suc A
mutual
data Fin (n:Nat) : Set where
finI : Fin_ n -> Fin n
Fin_ : Nat -> Set
Fin_ zero = Zero
Fin_ (suc n) = Suc (Fin n)
fzero : {n:Nat} -> Fin (suc n)
fzero = finI fzero_
fsuc : {n:Nat} -> Fin n -> Fin (suc n)
fsuc i = finI (fsuc_ i)
finE : {n:Nat} -> Fin n -> Fin_ n
finE (finI i) = i
module Vec where
open Prelude
open Fin
infixr 15 ::
-- Vectors ----------------------------------------------------------------
data Nil : Set where
nil_ : Nil
data Cons (A As:Set) : Set where
cons_ : A -> As -> Cons A As
mutual
data Vec (A:Set)(n:Nat) : Set where
vecI : Vec_ A n -> Vec A n
Vec_ : Set -> Nat -> Set
Vec_ A zero = Nil
Vec_ A (suc n) = Cons A (Vec A n)
nil : {A:Set} -> Vec A zero
nil = vecI nil_
(::) : {A:Set} -> {n:Nat} -> A -> Vec A n -> Vec A (suc n)
x :: xs = vecI (cons_ x xs)
vecE : {A:Set} -> {n:Nat} -> Vec A n -> Vec_ A n
vecE (vecI xs) = xs
vec : {A:Set} -> (n:Nat) -> A -> Vec A n
vec zero _ = nil
vec (suc n) x = x :: vec n x
map : {n:Nat} -> {A B:Set} -> (A -> B) -> Vec A n -> Vec B n
map {zero} f (vecI nil_) = nil
map {suc n} f (vecI (cons_ x xs)) = f x :: map f xs
(!) : {n:Nat} -> {A:Set} -> Vec A n -> Fin n -> A
(!) {suc n} (vecI (cons_ x _ )) (finI fzero_) = x
(!) {suc n} (vecI (cons_ _ xs)) (finI (fsuc_ i)) = xs ! i
tabulate : {n:Nat} -> {A:Set} -> (Fin n -> A) -> Vec A n
tabulate {zero} f = nil
tabulate {suc n} f = f fzero :: tabulate (\x -> f (fsuc x))
module Syntax where
open Prelude
open Fin
-- Types ------------------------------------------------------------------
infixr 8 =>
data Type : Set where
nat : Type
(=>) : Type -> Type -> Type
-- Terms ------------------------------------------------------------------
data Term (n:Nat) : Set where
eZero : Term n
eSuc : Term n
eApp : Term n -> Term n -> Term n
eLam : Term (suc n) -> Term n
eVar : Fin n -> Term n
module NormalForms where
open Prelude
open Syntax
open Fin
mutual
-- Normal terms -----------------------------------------------------------
data Normal (n:Nat) : Set where
nZero : Normal n
nSuc : Normal n -> Normal n
nLam : Normal (suc n) -> Normal n
nNeutral : Neutral n -> Normal n
nStuck : Normal n -- type error
-- Neutral terms ----------------------------------------------------------
data Neutral (n:Nat) : Set where
uVar : Fin n -> Neutral n
uApp : Neutral n -> Normal n -> Neutral n
nVar : {n:Nat} -> Fin n -> Normal n
nVar i = nNeutral (uVar i)
nApp : {n:Nat} -> Neutral n -> Normal n -> Normal n
nApp u n = nNeutral (uApp u n)
module Rename where
open Prelude
open Fin
open Vec
open NormalForms
-- Renamings --------------------------------------------------------------
Ren : Nat -> Nat -> Set
Ren m n = Vec (Fin n) m
id : {n:Nat} -> Ren n n
id = tabulate (\i -> i)
compose : {l m n:Nat} -> Ren m n -> Ren l m -> Ren l n
compose {l}{m}{n} ρ γ = map (\i -> ρ ! i) γ
lift : {m n:Nat} -> Ren m n -> Ren (suc m) (suc n)
lift ρ = fzero :: map fsuc ρ
mutual
rename : {m n:Nat} -> Ren m n -> Normal m -> Normal n
rename ρ nZero = nZero
rename ρ (nSuc n) = nSuc (rename ρ n)
rename ρ (nLam n) = nLam (rename (lift ρ) n)
rename ρ (nNeutral u) = nNeutral (renameNe ρ u)
rename ρ nStuck = nStuck
renameNe : {m n:Nat} -> Ren m n -> Neutral m -> Neutral n
renameNe ρ (uVar i) = uVar (ρ ! i)
renameNe ρ (uApp u n) = uApp (renameNe ρ u) (rename ρ n)
up : {n:Nat} -> Ren n (suc n)
up = map fsuc id
module Subst where
open Prelude
open Fin
open Vec
open NormalForms
open Rename using (Ren; rename; up)
-- Substitutions ----------------------------------------------------------
Sub : Nat -> Nat -> Set
Sub m n = Vec (Normal n) m
id : {n:Nat} -> Sub n n
id = tabulate nVar
ren2sub : {m n:Nat} -> Ren m n -> Sub m n
ren2sub ρ = map nVar ρ
lift : {m n:Nat} -> Sub m n -> Sub (suc m) (suc n)
lift σ = nVar fzero :: map (rename up) σ
mutual
app : {n:Nat} -> Normal n -> Normal n -> Normal n
app nZero _ = nStuck
app (nSuc _) _ = nStuck
app nStuck _ = nStuck
app (nLam u) v = subst (v :: id) u
app (nNeutral n) v = nApp n v
subst : {m n:Nat} -> Sub m n -> Normal m -> Normal n
subst σ nZero = nZero
subst σ (nSuc v) = nSuc (subst σ v)
subst σ (nLam v) = nLam (subst (lift σ) v)
subst σ (nNeutral n) = substNe σ n
subst σ nStuck = nStuck
substNe : {m n:Nat} -> Sub m n -> Neutral m -> Normal n
substNe σ (uVar i) = σ ! i
substNe σ (uApp n v) = substNe σ n `app` subst σ v
compose : {l m n:Nat} -> Sub m n -> Sub l m -> Sub l n
compose σ δ = map (subst σ) δ
module TypeSystem where
open Prelude
open Fin
open Vec
open Syntax
mutual
EqType : Type -> Type -> Prop
EqType nat nat = True
EqType (τ => τ') (σ => σ') = τ == σ /\ τ' == σ'
EqType _ _ = False
infix 5 ==
data (==) (τ0 τ1:Type) : Prop where
eqTypeI : EqType τ0 τ1 -> τ0 == τ1
eqSubst : {σ τ:Type} -> (C:Type -> Set) -> σ == τ -> C τ -> C σ
eqSubst {nat}{nat} C _ x = x
eqSubst {σ => τ}{σ' => τ'} C (eqTypeI (andI eqσ eqτ)) x =
eqSubst (\μ -> C (μ => τ)) eqσ (
eqSubst (\η -> C (σ' => η)) eqτ x
)
Context : Nat -> Set
Context n = Vec Type n
mutual
HasType : {n:Nat} -> Context n -> Term n -> Type -> Set
HasType Γ eZero τ = ZeroType Γ τ
HasType Γ eSuc τ = SucType Γ τ
HasType Γ (eVar i) τ = VarType Γ i τ
HasType Γ (eApp e1 e2) τ = AppType Γ e1 e2 τ
HasType Γ (eLam e) τ = LamType Γ e τ
data ZeroType {n:Nat}(Γ:Context n)(τ:Type) : Set where
zeroType : τ == nat -> HasType Γ eZero τ
data SucType {n:Nat}(Γ:Context n)(τ:Type) : Set where
sucType : τ == (nat => nat) -> HasType Γ eSuc τ
data VarType {n:Nat}(Γ:Context n)(i:Fin n)(τ:Type) : Set where
varType : τ == (Γ ! i) -> HasType Γ (eVar i) τ
data AppType {n:Nat}(Γ:Context n)(e1 e2:Term n)(τ:Type) : Set where
appType : (σ:Type) -> HasType Γ e1 (σ => τ) -> HasType Γ e2 σ -> HasType Γ (eApp e1 e2) τ
data LamType {n:Nat}(Γ:Context n)(e:Term (suc n))(τ:Type) : Set where
lamType : (τ0 τ1:Type) -> τ == (τ0 => τ1) -> HasType (τ0 :: Γ) e τ1 -> HasType Γ (eLam e) τ
module NBE where
open Prelude
open Syntax
open Fin
open Vec
open TypeSystem
mutual
D_ : Nat -> Type -> Set
D_ n nat = NatD n
D_ n (σ => τ) = FunD n σ τ
data D (n:Nat)(τ:Type) : Set where
dI : D_ n τ -> D n τ
data NatD (n:Nat) : Set where
zeroD_ : D_ n nat
sucD_ : D n nat -> D_ n nat
neD_ : Term n -> D_ n nat
-- Will this pass the positivity check?
data FunD (n:Nat)(σ τ:Type) : Set where
lamD_ : (D n σ -> D n τ) -> D_ n (σ => τ)
zeroD : {n:Nat} -> D n nat
zeroD = dI zeroD_
sucD : {n:Nat} -> D n nat -> D n nat
sucD d = dI (sucD_ d)
neD : {n:Nat} -> Term n -> D n nat
neD t = dI (neD_ t)
lamD : {n:Nat} -> {σ τ:Type} -> (D n σ -> D n τ) -> D n (σ => τ)
lamD f = dI (lamD_ f)
coerce : {n:Nat} -> {τ0 τ1:Type} -> τ0 == τ1 -> D n τ1 -> D n τ0
coerce {n} = eqSubst (D n)
mutual
down : {τ:Type} -> {n:Nat} -> D n τ -> Term n
down {σ => τ} (dI (lamD_ f)) = eLam (down {τ} ?) -- doesn't work!
down {nat} (dI zeroD_) = eZero
down {nat} (dI (sucD_ d)) = eSuc `eApp` down d
down {nat} (dI (neD_ t)) = t
up : {n:Nat} -> (τ:Type) -> Term n -> D n τ
up (σ => τ) t = lamD (\d -> up τ (t `eApp` down d))
up nat t = neD t
Valuation : {m:Nat} -> Nat -> Context m -> Set
Valuation {zero} n _ = Nil
Valuation {suc m} n (vecI (cons_ τ Γ)) = Cons (D n τ) (Valuation n Γ)
(!!) : {m n:Nat} -> {Γ:Context m} -> Valuation n Γ -> (i:Fin m) -> D n (Γ ! i)
(!!) {suc _} {_} {vecI (cons_ _ _)} (cons_ v ξ) (finI fzero_) = v
(!!) {suc _} {_} {vecI (cons_ _ _)} (cons_ v ξ) (finI (fsuc_ i)) = ξ !! i
ext : {m n:Nat} -> {τ:Type} -> {Γ:Context m} -> Valuation n Γ -> D n τ -> Valuation n (τ :: Γ)
ext ξ v = cons_ v ξ
app : {σ τ:Type} -> {n:Nat} -> D n (σ => τ) -> D n σ -> D n τ
--app (dI (lamD_ f)) d = f d
app (lamD f) d = f d
eval : {n:Nat} -> {Γ:Context n} -> (e:Term n) -> (τ:Type) -> HasType Γ e τ -> Valuation n Γ -> D n τ
eval (eVar i) τ (varType eq) ξ = coerce eq (ξ !! i)
eval (eApp r s) τ (appType σ dr ds) ξ = eval r (σ => τ) dr ξ `app` eval s σ ds ξ
eval (eLam r) τ (lamType τ0 τ1 eq dr) ξ = coerce eq (lamD (\d -> ?)) -- doesn't work either
eval eZero τ (zeroType eq) ξ = coerce eq zeroD
eval eSuc τ (sucType eq) ξ = coerce eq (lamD sucD)
module Eval where
open Prelude
open Fin
open Vec
open Syntax
open NormalForms
open Rename using (up; rename)
open Subst
open TypeSystem
eval : {n:Nat} -> (Γ:Context n) -> (e:Term n) -> (τ:Type) -> HasType Γ e τ -> Normal n
eval Γ eZero τ _ = nZero
eval Γ eSuc τ _ = nLam (nSuc (nVar fzero))
eval Γ (eVar i) τ _ = nVar i
eval Γ (eApp e1 e2) τ (appType σ d1 d2) = eval Γ e1 (σ => τ) d1 `app` eval Γ e2 σ d2
eval Γ (eLam e) τ (lamType τ0 τ1 _ d) = nLam (eval (τ0 :: Γ) e τ1 d)
open Prelude
open Fin
open Vec
open Syntax