blob: e86abdb3e9bf73f3f28f4bbf362b71fc133eff7f (
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
|
module Encoded.Vect
import Data.String
import Data.Vect
import Encoded.Bool
import Encoded.Pair
import Encoded.Fin
import Term.Syntax
export
Vect : Nat -> Ty -> Ty
Vect k ty = Fin k ~> ty
export
nil : {ty : Ty} -> Term (Vect 0 ty) ctx
nil = absurd
export
cons : {k : Nat} -> {ty : Ty} -> Term (ty ~> Vect k ty ~> Vect (S k) ty) ctx
cons = Abs $ Abs $ Abs $
let x = Var $ There $ There Here in
let xs = Var $ There Here in
let i = Var Here in
App induct [<i, x, App uncurry [<Abs $ Const $ App (shift xs) (Var Here)]]
export
tabulate : Term ((Fin k ~> ty) ~> Vect k ty) ctx
tabulate = Id
export
dmap :
{k : Nat} ->
{ty1, ty2 : Ty} ->
Term ((Fin k ~> ty1 ~> ty2) ~> Vect k ty1 ~> Vect k ty2) ctx
dmap =
Abs $ Abs $ Abs $
let f = Var (There $ There Here) in
let xs = Var (There Here) in
let i = Var Here in
App f [<i, App xs i]
export
map : {k : Nat} -> {ty1, ty2 : Ty} -> Term ((ty1 ~> ty2) ~> Vect k ty1 ~> Vect k ty2) ctx
map = Abs' (\f => App dmap (Const f))
export
index : {k : Nat} -> {ty : Ty} -> Term (Vect k ty ~> Fin k ~> ty) ctx
index = Id
export
foldr : {k : Nat} -> {ty, ty' : Ty} -> Term (ty' ~> (ty ~> ty' ~> ty') ~> Vect k ty ~> ty') ctx
foldr {k = 0} = Abs $ Const $ Const $ Var Here
foldr {k = S k} = Abs $ Abs $ Abs $
let z = Var (There $ There Here) in
let c = Var (There Here) in
let xs = Var Here in
App c [<App xs [<zero], App foldr [<z, c, xs . suc]]
export
fromVect : {k : Nat} -> {ty : Ty} -> Vect k (Term ty ctx) -> Term (Vect k ty) ctx
fromVect [] = nil
fromVect (t :: ts) = App cons [<t, fromVect ts]
export
toVect : {k : Nat} -> {ty : Ty} -> Term (Vect k ty) ctx -> Vect k (Term ty ctx)
toVect {k = 0} v = []
toVect {k = S k} v = App v [<zero] :: toVect (v . suc)
|
