blob: 723d5dc1be2e2ffa6b04adf06e4712e1075dfacc (
plain) (
blame)
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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
# MIT License, Copyright (c) 2023 Marvin Borner
# utilities for meta programming with quoted terms
:import std/Logic .
:import std/Combinator .
:import std/Number/Unary .
:import std/List .
# constructor of meta abstraction
abs [[[[0 3]]]] ⧗ Meta → Meta
:test (abs '0) ('[0])
# true if abstraction
abs? [0 [false] [[false]] [true]] ⧗ Meta → Bool
:test (abs? '[0]) (true)
:test (abs? '([0] [0])) (false)
:test (abs? '0) (false)
# extracts meta term from meta abstraction
abs! [0 0 0 [0]] ⧗ Meta → Meta
:test (abs! '[[0]]) ('[0])
# constructor of meta application
app [[[[[1 4 3]]]]] ⧗ Meta → Meta → Meta
# TODO: parser bug without lhs application
:test ((app '[[1]]) '[0]) ('([[1]] [0]))
# true if application
app? [0 [false] [[true]] [false]] ⧗ Meta → Bool
:test (app? '[0]) (false)
:test (app? '([0] [0])) (true)
:test (app? '0) (false)
# extracts both meta terms from meta application
app! [0 0 [[1 : 0]] 0] ⧗ Meta → (Pair Meta Meta)
# TODO: parser bug with mixfix application
:test (app! '([[1]] [[0]])) ((cons '[[1]]) '[[0]])
# extracts lhs meta term from meta application
app-lhs! ^‣ ∘ app! ⧗ Meta → Meta
:test (app-lhs! '([[1]] [[0]])) ('[[1]])
# extracts rhs meta term from meta application
app-rhs! ~‣ ∘ app! ⧗ Meta → Meta
:test (app-rhs! '([[1]] [[0]])) ('[[0]])
# constructor of meta variable/index
idx [[[[2 3]]]] ⧗ Unary → Meta
:test (idx (+0u)) ('0)
# true if variable/index
idx? [0 [true] [[false]] [false]] ⧗ Meta → Bool
:test (idx? '[0]) (false)
:test (idx? '([0] [0])) (false)
:test (idx? '0) (true)
# extracts index from meta index
idx! [0 [0] 0 0] ⧗ Meta → Unary
:test (idx! '0) ((+0u))
:test (idx! '3) ((+3u))
# traverses meta term
fold y [[[[[rec]]]]] ⧗ (Unary → a) → (a → a → a) → (a → a) → Meta → a
rec 0 case-idx case-app case-abs
case-idx 3
case-app ψ 2 (4 3 2 1)
case-abs 1 ∘ (4 3 2 1)
# calculates blc length of meta term
length fold idx-cb app-cb abs-cb ⧗ Meta → Unary
idx-cb add (+2u)
app-cb (add (+2u)) ∘∘ add
abs-cb add (+2u)
:test (length '[0]) ((+4u))
:test (length '[[1 1]]) ((+12u))
# true bit
blc1 [[0]] ⧗ LcBit
# false bit
blc0 [[1]] ⧗ LcBit
# converts meta term to blc list
blc fold idx-cb app-cb abs-cb ⧗ Meta → (List LcBit)
idx-cb [++0 (cons blc1) {}blc0]
app-cb (cons blc0) ∘ (cons blc1) ∘∘ append
abs-cb (cons blc0) ∘ (cons blc0)
:test (blc '[0]) (blc0 : (blc0 : (blc1 : {}blc0)))
:test (blc '[[1 1]]) (blc0 : (blc0 : (blc0 : (blc0 : (blc0 : (blc1 : (blc1 : (blc1 : (blc0 : (blc1 : (blc1 : {}blc0)))))))))))
α-eq? y [[[rec]]] ⧗ Meta → Meta → Bool
rec 1 case-idx case-app case-abs
case-idx [(idx? 1) ⋀? (0 =? (idx! 1))]
case-app [[(app? 2) ⋀? (4 1 (app-lhs! 2)) ⋀? (4 0 (app-rhs! 2))]]
case-abs [(abs? 1) ⋀? (3 (abs! 1) 0)]
# TODO: parser bug
:test ((α-eq? '0) '1) ([[0]])
:test ((α-eq? '1) '1) ([[1]])
:test ((α-eq? '(0 0)) '1) ([[0]])
:test ((α-eq? '(0 0)) '(1 0)) ([[0]])
:test ((α-eq? '(0 0)) '(0 0)) ([[1]])
:test ((α-eq? '(0 1)) '(0 1)) ([[1]])
:test ((α-eq? '[0]) '[1]) ([[0]])
:test ((α-eq? '[0]) '[0]) ([[1]])
|
