blob: 7f0e3be408acebde6234e3dd7f40bb539dc626f9 (
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
|
module SOAS.Syntax
import SOAS.Algebra
import SOAS.Context
import SOAS.Family
import SOAS.Strength
import SOAS.Structure
import SOAS.Theory
import SOAS.Var
--------------------------------------------------------------------------------
-- Signatures
public export
(.ParamsErased) : (type.Ctx, type).Ctx -> Type
params.ParamsErased = params.All (\_, extty => (fst extty).Erased)
public export
record (.Signature) (type : Type) where
constructor MkSig
0 ops : (ty : type) -> (params : (type.Ctx, type).Ctx) -> Type
erased :
{0 ty : type} -> {0 params : (type.Ctx, type).Ctx} ->
(op : ops ty params) -> params.ParamsErased
--------------------------------------------------------------------------------
-- Functor
public export
data (.Args) : (type.Ctx, type).Ctx -> type.SortedFamily -> type.Family where
Lin : [<].Args a ctx
(:<) :
params.Args a ctx ->
BindRename ext a ty ctx ->
(params :< (n :- (ext, ty))).Args a ctx
public export
data (.functor) : type.Signature -> type.SortedFunctor where
Op : (op : sig.ops ty params) -> (args : params.Args a ctx) -> sig.functor a ty ctx
--------------------------------------------------------------------------------
-- Functoriality
argsMap : (a -|> b) -> params.Args a -||> params.Args b
argsMap f [<] = [<]
argsMap f (sx :< (Bind names x)) = argsMap f sx :< (Bind names $ f x)
export
%hint
(.functorMap) : (0 sig : type.Signature) -> sig.functor.Map
sig.functorMap = MkMap $ \f => \(Op op args) => Op op (argsMap f args)
--------------------------------------------------------------------------------
-- Strength
argsStr :
(erased : params.ParamsErased) -> (mon : type.PointedCoalgStruct p) =>
params.Args (x ^ p) -||> params.Args x ^^ p
argsStr [<] [<] {ctx} theta = [<]
argsStr (erased :< length) (sx :< (Bind names x)) {ctx} theta =
argsStr erased sx theta :< (Bind names $ x $ lift (erasedRename length) theta)
export
%hint
(.functorStrength) :
(sig : type.Signature) -> Strength sig.functor
sig.functorStrength = MkStrength $
\(Op op args), theta => Op op (argsStr (sig.erased op) args theta)
--------------------------------------------------------------------------------
-- Terms
public export
data (.Term) : (sig : type.Signature) -> type.SortedFunctor where
Var : Var -|> sig.Term a
Alg : sig.functor (sig.Term a) -|> sig.Term a
MVar : a -|> sig.Term a ^ sig.Term a
%hint
export
(.TermMetalg) : (sig : type.Signature) -> sig.functor.MetaAlg meta (sig.Term meta)
sig.TermMetalg = MkMetaAlg { alg = Alg, var = Var, mvar = MVar }
%hint
export
(.TermInitial) : (sig : type.Signature) -> sig.functor.Initial meta (sig.Term meta)
sig.TermInitial = MkInitial
{ metalg = sig.TermMetalg
, sem = sem
}
where
sem : (0 b : type.SortedFamily) -> (metalg : sig.functor.MetaAlg meta b) => sig.Term meta -|> b
semArgs :
(0 b : type.SortedFamily) -> (metalg : sig.functor.MetaAlg meta b) =>
{0 params : (type.Ctx, type).Ctx} ->
params.Args (sig.Term meta) -||> params.Args b
sem b (Var v) = metalg.var v
sem b (Alg (Op op args)) = metalg.alg $ Op op $ semArgs b args
sem b (MVar m f) = metalg.mvar m $ \v => sem b (f v)
semArgs b [<] = [<]
semArgs b (sx :< (Bind names x)) = semArgs b sx :< (Bind names $ sem b x)
|
