blob: 64b6a2730f6bf860970f96625ba5f3edb3866008 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
module NormalForm
import Data.SnocList.Elem
import Term
import Thinning
-- Neutrals and Normals --------------------------------------------------------
public export
data Neutral : SnocList Ty -> Ty -> Type
public export
data Normal : SnocList Ty -> Ty -> Type
data Neutral where
Var : (i : Elem ty ctx) -> Neutral ctx ty
App : Neutral ctx (ty ~> ty') -> Normal ctx ty -> Neutral ctx ty'
Rec : Neutral ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Neutral ctx ty
data Normal where
Ntrl : Neutral ctx ty -> Normal ctx ty
Abs : Normal (ctx :< ty) ty' -> Normal ctx (ty ~> ty')
Zero : Normal ctx N
Succ : Normal ctx N -> Normal ctx N
%name Neutral n, m, k
%name Normal n, m, k
-- Forgetting ------------------------------------------------------------------
export
forgetNtrl : Neutral ctx ty -> Term ctx ty
export
forgetNorm : Normal ctx ty -> Term ctx ty
forgetNtrl (Var i) = Var i
forgetNtrl (App n m) = App (forgetNtrl n) (forgetNorm m)
forgetNtrl (Rec n m k) = Rec (forgetNtrl n) (forgetNorm m) (forgetNorm k)
forgetNorm (Ntrl n) = forgetNtrl n
forgetNorm (Abs n) = Abs (forgetNorm n)
forgetNorm Zero = Zero
forgetNorm (Succ n) = Succ (forgetNorm n)
-- Weakening -------------------------------------------------------------------
export
wknNtrl : Neutral ctx ty -> ctx `Thins` ctx' -> Neutral ctx' ty
export
wknNorm : Normal ctx ty -> ctx `Thins` ctx' -> Normal ctx' ty
wknNtrl (Var i) thin = Var (index thin i)
wknNtrl (App n m) thin = App (wknNtrl n thin) (wknNorm m thin)
wknNtrl (Rec n m k) thin = Rec (wknNtrl n thin) (wknNorm m thin) (wknNorm k $ keep thin)
wknNorm (Ntrl n) thin = Ntrl (wknNtrl n thin)
wknNorm (Abs n) thin = Abs (wknNorm n $ keep thin)
wknNorm Zero thin = Zero
wknNorm (Succ n) thin = Succ (wknNorm n thin)
|
