blob: ed7d891d61fb524f4d736dfe43f370863e5061a5 (
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
|
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
%hide Syntax.PreorderReasoning.prefix.(|~)
%hide Syntax.PreorderReasoning.Generic.prefix.(|~)
data TypeSTLC = B | (-:>) TypeSTLC TypeSTLC
data OpSTLC : TypeSTLC -> (TypeSTLC .Ctx, TypeSTLC).Ctx -> Type where
App : OpSTLC ty2 [<"f" :- ([<], ty1 -:> ty2), "x" :- ([<], ty1)]
Lam : OpSTLC (ty1 -:> ty2) [<"body" :- ([<"x" :- ty1], ty2)]
STLC : TypeSTLC .Signature
STLC = MkSig OpSTLC $ \case
App => [<Z, Z]
Lam => [<S Z]
Ex1 : STLC .Term Var (B -:> (B -:> B) -:> B) [<]
Ex1 =
Alg $ Op Lam [<Bind [<"x"] $
Alg $ Op Lam [<Bind [<"f"] $
Alg $ Op App [<[] (Var (%% "f")), [] (Var (%% "x"))]]]
beta :
{0 body : STLC .Term Var ty2 (ctx :< (x :- ty1))} ->
Singleton (Alg $ Op App [<[] (Alg $ Op Lam [<Bind [<x] body]), [] t]) ->
STLC .Term Var ty2 ctx
beta (Val $ Alg $ Op App [<Bind [<] $ Alg $ Op Lam [<Bind [<x] body], Bind [<] t]) =
(STLC .Term Var).sub body t
eta : STLC .Term Var (ty1 -:> ty2) ctx -> STLC .Term Var (ty1 -:> ty2) ctx
eta t =
Alg $ Op Lam [<Bind [<"x"] $
Alg $ Op App [<[] ((STLC .Term Var).wkn t), [] (Var $ %% "x")]]
Ex2 : STLC .Term Var (B -:> B) [<]
Ex2 =
Alg $ Op App
[<[] (Alg $ Op Lam [<Bind [<"f"] $
Alg $ Op Lam [<Bind [<"x"] $
Alg $ Op App [<[] (Var $ (%% "f") {pos = There Here}), [] (Var $ %% "x")]]])
, [] (Alg $ Op Lam [<Bind [<"x"] $ Var $ %% "x"])]
Ex3 : STLC .Term Var (B -:> B) [<]
Ex3 = eta $ beta $ Val Ex2
|
