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
|
module Encoded.Sum
import public Data.SnocList.Operations
import Encoded.Bool
import Encoded.Pair
import Term.Syntax
-- Binary Sums -----------------------------------------------------------------
export
(+) : Ty -> Ty -> Ty
ty1 + ty2 = B * (ty1 <+> ty2)
export
left : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 + ty2)) ctx
left = Abs' (\t => App pair [<True, App inL [<t]])
export
right : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 + ty2)) ctx
right = Abs' (\t => App pair [<False, App inR [<t]])
export
case' : {ty1, ty2, ty : Ty} -> Term ((ty1 + ty2) ~> (ty1 ~> ty) ~> (ty2 ~> ty) ~> ty) ctx
case' = Abs' (\t =>
App if'
[<App fst [<t]
, Abs $ Const $ App (Var Here . prL . snd) [<shift t]
, Const $ Abs $ App (Var Here . prR . snd) [<shift t]
])
export
either : {ty1, ty2, ty : Ty} -> Term ((ty1 ~> ty) ~> (ty2 ~> ty) ~> (ty1 + ty2) ~> ty) ctx
either = Abs $ Abs $ Abs $
let f = Var $ There $ There Here in
let g = Var $ There Here in
let x = Var Here in
App case' [<x, f, g]
-- N-ary Sums ------------------------------------------------------------------
public export
mapNonEmpty : NonEmpty sx -> NonEmpty (map f sx)
mapNonEmpty IsSnoc = IsSnoc
export
Sum : (sty : SnocList Ty) -> {auto 0 ok : NonEmpty sty} -> Ty
Sum [<ty] = ty
Sum (sty@(_ :< _) :< ty) = Sum sty + ty
export
any :
{sty : SnocList Ty} ->
{ty : Ty} ->
{auto 0 ok : NonEmpty sty} ->
Term (map (~> ty) sty ~>* Sum sty ~> ty) ctx
any {sty = [<ty']} = Id
any {sty = sty :< ty'' :< ty'} =
Abs (Abs $ Abs $
let rec = Var (There $ There Here) in
let f = Var (There Here) in
let g = Var Here in
App either [<App rec [<f], g]) .:
any {sty = sty :< ty''}
export
tag :
{sty : SnocList Ty} ->
{ty : Ty} ->
{auto 0 ok : NonEmpty sty} ->
Elem ty sty ->
Term (ty ~> Sum sty) ctx
tag {sty = [<ty]} Here = Id
tag {sty = sty :< ty' :< ty} Here = right
tag {sty = sty :< ty'' :< ty'} (There i) = left . tag i
|
