blob: 2710ad3aafcff0ed19724e42f4f23d2c8639f5bf (
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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
module Total.Syntax
import public Data.List
import public Data.List.Quantifiers
import public Data.SnocList
import public Data.SnocList.Quantifiers
import public Total.Term
import public Total.Term.CoDebruijn
infixr 20 ~>*
infixl 9 .~, .*
public export
data Len : SnocList a -> Type where
Z : Len [<]
S : Len sx -> Len (sx :< x)
%name Len k
export
lenToNat : Len sx -> Nat
lenToNat Z = 0
lenToNat (S k) = S (lenToNat k)
public export
(~>*) : SnocList Ty -> Ty -> Ty
tys ~>* ty = foldr (~>) ty tys
public export
0 Fun : (sx : SnocList a) -> (a -> Type) -> Type -> Type
Fun [<] p ret = ret
Fun (sx :< x) p ret = Fun sx p (p x -> ret)
after : Len sx -> (r -> s) -> Fun sx p r -> Fun sx p s
after Z f = f
after (S k) f = after k (f .)
before : Len sx -> (forall x. p x -> q x) -> Fun sx q ret -> Fun sx p ret
before Z f = id
before (S k) f = before k f . after k (. f)
export
lit : Nat -> FullTerm N ctx
lit 0 = Zero `Over` Empty
lit (S n) = suc (lit n)
absHelper :
Len tys ->
Fun tys (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
FullTerm (tys ~>* ty) ctx
absHelper Z x = x
absHelper (S k) x =
absHelper k $
after k (\f => CoDebruijn.abs (f SnocList.Elem.Here)) $
before k SnocList.Elem.There x
export
abs' :
Len tys ->
Fun tys (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
FullTerm (tys ~>* ty) ctx
abs' k = absHelper k . before k var
export
app' :
{tys : SnocList Ty} ->
FullTerm (tys ~>* ty) ctx ->
All (flip FullTerm ctx) tys ->
FullTerm ty ctx
app' t [<] = t
app' t (us :< u) = app (app' t us) u
-- export
-- compose :
-- {ty, ty' : Ty} ->
-- (t : FullTerm (ty' ~> ty'') ctx) ->
-- (u : FullTerm (ty ~> ty') ctx) ->
-- Len u.support =>
-- Covering Covers t.thin u.thin ->
-- CoTerm (ty ~> ty'') ctx
-- compose (t `Over` thin1) (u `Over` thin2) cover =
-- Abs
-- (MakeBound
-- (App
-- (MakePair
-- (t `Over` Drop thin1)
-- (App
-- (MakePair
-- (u `Over` Drop id)
-- (Var `Over` Keep empty)
-- (DropKeep (coverIdLeft empty)))
-- `Over` Keep thin2)
-- (DropKeep cover)))
-- (Keep Empty))
-- export
-- (.~) :
-- Len ctx =>
-- {ty, ty' : Ty} ->
-- CoTerm (ty' ~> ty'') ctx ->
-- CoTerm (ty ~> ty') ctx ->
-- CoTerm (ty ~> ty'') ctx
-- t .~ u = compose (t `Over` id) (u `Over` id) (coverIdLeft id)
export
(.) :
{ty, ty' : Ty} ->
FullTerm (ty' ~> ty'') ctx ->
FullTerm (ty ~> ty') ctx ->
FullTerm (ty ~> ty'') ctx
t . u = abs' (S Z) (\x => app (drop t) (app (drop u) x))
export
(.*) :
{ty : Ty} ->
{tys : SnocList Ty} ->
FullTerm (ty ~> ty') ctx ->
FullTerm (tys ~>* ty) ctx ->
FullTerm (tys ~>* ty') ctx
(.*) {tys = [<]} t u = app t u
(.*) {tys = tys :< ty''} t u = abs' (S Z) (\f => drop t . f) .* u
export
lift : FullTerm ty [<] -> FullTerm ty ctx
lift t = wkn t Empty
export
id : FullTerm (ty ~> ty) [<]
id = Abs Var `Over` Empty
|
