blob: fead58617edad5a06ef17b17a15b1267055c6345 (
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
|
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
(~>*) : SnocList Ty -> Ty -> Ty
tys ~>* ty = foldr (~>) ty tys
public export
0 Fun : {sx : SnocList a} -> Len sx -> (a -> Type) -> Type -> Type
Fun Z arg ret = ret
Fun (S {x = ty} k) arg ret = Fun k arg (arg ty -> ret)
after : (k : Len sx) -> (a -> b) -> Fun k p a -> Fun k p b
after Z f x = f x
after (S k) f x = after k (f .) x
before :
(k : Len sx) ->
(forall x. p x -> q x) ->
Fun k q ret ->
Fun k p ret
before Z f x = x
before (S k) f x = before k f (after k (. f) x)
export
lit : Len ctx => Nat -> FullTerm N ctx
lit 0 = Zero `Over` empty
lit (S n) = suc (lit n)
absHelper :
(k : Len tys) ->
Fun k (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 : Len ctx) =>
(k : Len tys) ->
Fun k (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
FullTerm (tys ~>* ty) ctx
abs' k = absHelper k . before k (var @{lenAppend len k})
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
(.) :
Len ctx =>
{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
(.*) :
Len ctx =>
{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 : Len ctx => FullTerm ty [<] -> FullTerm ty ctx
lift t = wkn t empty
export
id' : CoTerm (ty ~> ty) [<]
id' = Abs (MakeBound Var (Keep Empty))
export
id : FullTerm (ty ~> ty) [<]
id = id' `Over` empty
|
