-
Notifications
You must be signed in to change notification settings - Fork 0
/
loader_sim.py
115 lines (93 loc) · 3.23 KB
/
loader_sim.py
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
#from recordclass import recordclass
from coc import *
class judgement:
__slots__ = ['ctx', 'typ', 'term']
def __init__(self, ctx=0, typ=0, term=0):
self.ctx = ctx; self.typ = typ; self.term = term
def copy(self):
return judgement(ctx=self.ctx, typ=self.typ, term=self.term)
t = judgement(ctx=[], typ=Sort(1), term=Sort(0))
states = ['warmup', 'loop', 'apply', 'new-var', 'abstract', 'make-lambda',
'scope']
class Stack:
def __init__(self):
self.list = []
def __iter__(self):
return iter(self.list)
def push(self, x):
self.list.append(x)
def index(self, i):
return self.list[-1-i]
def top(self):
return self.index(0)
def pop(self):
return self.list.pop()
def copy(self):
return [j.copy() for j in self.list]
def interactive_parse(stack, log=print):
t = judgement(ctx=[], typ=Sort(1), term=Sort(0))
stack.push(t)
yield 'warmup'
#while (yield 'loop'):
while True:
#if (yield 'test'):
# t.term = Sort(1)
while (yield 'loop'):
t = judgement(ctx=[], typ=Sort(1), term=Sort(0))
stack.push(t)
t = stack.index(1)
a = stack.top()
alt_ctx = a.ctx
alt_typ = a.typ
alt_term = a.term
if alt_ctx == t.ctx:
if isinstance(t.typ, ProdType) and t.typ.args[0] == alt_typ and \
(yield 'apply'):
t.typ = t.typ.type_with_arg(alt_term)
#ap = app
ap = Apply
t.term = ap(t.term, alt_term)
if (yield 'new-var') and isinstance(alt_typ, Sort):
t.ctx = [alt_term.eval()] + t.ctx
t.typ = t.typ.mkfree_var(0)
t.term = t.term.mkfree_var(0)
stack.pop()
if len(t.ctx) > 0 and (yield 'abstract'):
domain = t.ctx[0]
if (yield 'make-lambda') or not isinstance(t.typ, Sort):
t.typ = ProdType(domain, t.typ)
t.term = Lambda(domain, t.term)
else:
t.term = ProdType(domain, t.term)
t.ctx = t.ctx[1:]
if (yield 'scope') and isinstance(t.typ, Sort):
t.ctx = [t.term.eval()] + t.ctx
t.typ = t.term.eval().mkfree_var(0)
t.term = Var(0)
def test_show(ctx, typ, term):
"""
vargen = std_vargen()
ctx_var = []
ctx_str = []
for typ in reversed(ctx):
typ_str = typ.show(ctx_var, vargen)
var = next(vargen)
ctx_var.append(var)
ctx_str.append('{:s}: {:s}'.format(var, ctx_str))
term_str = term.show(ctx_var, vargen)
typ_str = typ.show(ctx_var, vargen)
return '{:s} |- {:s} : {:s}'.format(', '.join(ctx_str), term_str, typ_str)
"""
return show_judgement(judgement(ctx, typ, term))
def show_judgement(t):
vargen = std_vargen()
ctx_var = []
ctx_str = []
for typ in reversed(t.ctx):
typ_str = typ.show(ctx_var, vargen)
var = next(vargen)
ctx_var = [var] + ctx_var
ctx_str.append('{:s}: {:s}'.format(var, typ_str))
term_str = t.term.show(ctx_var, vargen)
typ_str = t.typ.show(ctx_var, vargen)
return '{:s} |- {:s} : {:s}'.format(', '.join(ctx_str), term_str, typ_str)