blob: 83d6acc2076560c0930192dac4ebcf0d320942a3 (
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
|
module Example
import Data.Singleton
import SOAS
infixr 3 -:>
-- Writing the descriptions directly is fine
-- but deriving their functoriality and strength is annoying
-- and not needed with enough metaprogramming
data TypeSTLC = B | (-:>) TypeSTLC TypeSTLC
data STLC : TypeSTLC .SortedFunctor where
App : (f : a (ty1 -:> ty2) ctx) ->
(x : a ty1 ctx) -> STLC a ty2 ctx
Lam : (x : String) ->
(body : a ty2 (ctx :< (x :- ty1))) ->
STLC a (ty1 -:> ty2) ctx
%hint
strSTLC : Strength STLC
strSTLC = MkStrength
{ strength = \p,x,mon => \case
(App f x) => \theta => App (f theta) (x theta)
(Lam str {ty1} body) => \theta =>
Lam str $ body $ extend p (mon.var (%% str))
$ \v => mon.ren (theta v)
(\u => ThereVar u) -- Bug: can't eta-reduce
}
%hint
functorialitySTLC : STLC .Map
functorialitySTLC = MkMap
{ map = \h => \case
(App f x) => App (h f) (h x)
(Lam str body) => Lam str (h body)
}
data Term : (meta : type.SortedFamily) -> type.SortedFamily where
Va : Var -|> Term meta
Me : meta -|> Term meta ^ Term meta
Op : STLC (Term meta) -|> Term meta
-- -- La : (x : String) -> bind [< x :- ty1 ] (Term meta) ty2 -||> Term meta (ty1 -:> ty2)
-- -- bug: unification error in Ex1
-- La : (x : String) -> Term meta ty2 (ctx :< (x :- ty1)) -> Term meta (ty1 -:> ty2) ctx
-- -- Ap : Term meta (ty1 -:> ty2) -||> Term meta ty1 =||> Term meta ty2
-- Ap : Term meta (ty1 -:> ty2) ctx -> Term meta ty1 ctx -> Term meta ty2 ctx
%hint
TermMetaAlg : STLC .MetaAlg meta (Term meta)
TermMetaAlg = MkMetaAlg
{ alg = Op
, var = Va
, mvar = Me
}
%hint
TermInitial : STLC .Initial meta (Term meta)
TermInitial = MkInitial
{ metalg = TermMetaAlg
, bang = bang
}
where
bang : (0 b : TypeSTLC .SortedFamily) -> (metalg : STLC .MetaAlg meta b) -> Term meta -|> b
bang b metalg (Va v) = metalg.var v
bang b metalg (Me m theta) = metalg.mvar m (\v => bang b metalg (theta v))
bang b metalg (Op (Lam str body)) = metalg.alg (Lam str (bang b metalg body))
bang b metalg (Op (App f x)) = metalg.alg (App (bang b metalg f) (bang b metalg x))
Ex1 : Term Var (B -:> (B -:> B) -:> B) [<]
Ex1 = Op $ Lam "x" $ Op $ Lam "f" $ Op $ App (Va $ %% "f") (Va $ %% "x")
beta :
{0 body : Term Var ty2 (ctx :< (x :- ty1))} ->
Singleton (Op $ App (Op $ Lam x body) t) -> Term Var ty2 ctx
beta (Val (Op $ App (Op $ Lam x body) t)) = TermInitial .monStruct.sub body t
Ex2 : Term Var (B -:> B) [<]
Ex2 = Op $ App
(Op $ Lam "f" $ Op $ Lam "x" $ Op $ App (Va $ %% "f") (Va $ (%% "x") {pos = Here}))
(Op $ Lam "x" $ Va $ %% "x")
Ex3 : Term Var (B -:> B) [<]
Ex3 = beta $ Val Ex2
|
