Skip to content

Commit bc2091c

Browse files
awalterschulzeawalterschulze
committed
comment out noisy IO tests
1 parent fbc51c3 commit bc2091c

File tree

1 file changed

+108
-108
lines changed

1 file changed

+108
-108
lines changed

‎Validator/Validator/TestIO.lean‎

Lines changed: 108 additions & 108 deletions
Original file line numberDiff line numberDiff line change
@@ -29,111 +29,111 @@ unsafe def runTwice' (x: Expr) (t: ParseTree): Except String Bool :=
2929

3030
open ParseTree (node)
3131

32-
#eval runTwice'
33-
Expr.emptyset
34-
(node "a" [node "b" [], node "c" [node "d" []]])
35-
36-
#eval runTwice'
37-
(Expr.tree (Pred.eq (Token.string "a")) Expr.epsilon)
38-
(node "a" [])
39-
40-
#eval runTwice'
41-
(Expr.tree (Pred.eq (Token.string "a")) Expr.epsilon)
42-
(node "a" [node "b" []])
43-
44-
#eval runTwice'
45-
(Expr.tree (Pred.eq (Token.string "a"))
46-
(Expr.tree (Pred.eq (Token.string "b"))
47-
Expr.epsilon
48-
)
49-
)
50-
(node "a" [node "b" []])
51-
52-
#eval runTwice'
53-
(Expr.tree (Pred.eq (Token.string "a"))
54-
(Expr.concat
55-
(Expr.tree (Pred.eq (Token.string "b"))
56-
Expr.epsilon
57-
)
58-
(Expr.tree (Pred.eq (Token.string "c"))
59-
Expr.epsilon
60-
)
61-
)
62-
)
63-
(node "a" [node "b" [], node "c" []])
64-
65-
#eval runTwice'
66-
(Expr.tree (Pred.eq (Token.string "a"))
67-
(Expr.concat
68-
(Expr.tree (Pred.eq (Token.string "b"))
69-
Expr.epsilon
70-
)
71-
(Expr.tree (Pred.eq (Token.string "c"))
72-
(Expr.tree (Pred.eq (Token.string "d"))
73-
Expr.epsilon
74-
)
75-
)
76-
)
77-
)
78-
(node "a" [node "b" [], node "c" [node "d" []]])
79-
80-
-- try to engage skip using emptyset, since it is unescapable
81-
#eval runTwice'
82-
(Expr.tree (Pred.eq (Token.string "a"))
83-
Expr.emptyset
84-
)
85-
(node "a" [node "b" []])
86-
87-
#eval runTwice'
88-
(Expr.tree (Pred.eq (Token.string "a"))
89-
(Expr.concat
90-
(Expr.tree (Pred.eq (Token.string "b"))
91-
Expr.emptyset
92-
)
93-
(Expr.tree (Pred.eq (Token.string "c"))
94-
(Expr.tree (Pred.eq (Token.string "d"))
95-
Expr.epsilon
96-
)
97-
)
98-
)
99-
)
100-
(node "a" [node "b" [], node "c" [node "d" []]])
101-
102-
#eval runTwice'
103-
(Expr.tree (Pred.eq (Token.string "a"))
104-
(Expr.concat
105-
(Expr.tree (Pred.eq (Token.string "b"))
106-
Expr.epsilon
107-
)
108-
Expr.emptyset
109-
)
110-
)
111-
(node "a" [node "b" [], node "c" [node "d" []]])
112-
113-
#eval runTwice'
114-
(Expr.tree (Pred.eq (Token.string "a"))
115-
(Expr.concat
116-
(Expr.tree (Pred.eq (Token.string "b"))
117-
Expr.epsilon
118-
)
119-
(Expr.tree (Pred.eq (Token.string "c"))
120-
Expr.emptyset
121-
)
122-
)
123-
)
124-
(node "a" [node "b" [], node "c" [node "d" []]])
125-
126-
#eval runTwice'
127-
(Expr.tree (Pred.eq (Token.string "a"))
128-
(Expr.concat
129-
(Expr.tree (Pred.eq (Token.string "b"))
130-
Expr.epsilon
131-
)
132-
(Expr.tree (Pred.eq (Token.string "c"))
133-
(Expr.tree (Pred.eq (Token.string "d"))
134-
Expr.emptyset
135-
)
136-
)
137-
)
138-
)
139-
(node "a" [node "b" [], node "c" [node "d" []]])
32+
-- #eval runTwice'
33+
-- Expr.emptyset
34+
-- (node "a" [node "b" [], node "c" [node "d" []]])
35+
36+
-- #eval runTwice'
37+
-- (Expr.tree (Pred.eq (Token.string "a")) Expr.epsilon)
38+
-- (node "a" [])
39+
40+
-- #eval runTwice'
41+
-- (Expr.tree (Pred.eq (Token.string "a")) Expr.epsilon)
42+
-- (node "a" [node "b" []])
43+
44+
-- #eval runTwice'
45+
-- (Expr.tree (Pred.eq (Token.string "a"))
46+
-- (Expr.tree (Pred.eq (Token.string "b"))
47+
-- Expr.epsilon
48+
-- )
49+
-- )
50+
-- (node "a" [node "b" []])
51+
52+
-- #eval runTwice'
53+
-- (Expr.tree (Pred.eq (Token.string "a"))
54+
-- (Expr.concat
55+
-- (Expr.tree (Pred.eq (Token.string "b"))
56+
-- Expr.epsilon
57+
-- )
58+
-- (Expr.tree (Pred.eq (Token.string "c"))
59+
-- Expr.epsilon
60+
-- )
61+
-- )
62+
-- )
63+
-- (node "a" [node "b" [], node "c" []])
64+
65+
-- #eval runTwice'
66+
-- (Expr.tree (Pred.eq (Token.string "a"))
67+
-- (Expr.concat
68+
-- (Expr.tree (Pred.eq (Token.string "b"))
69+
-- Expr.epsilon
70+
-- )
71+
-- (Expr.tree (Pred.eq (Token.string "c"))
72+
-- (Expr.tree (Pred.eq (Token.string "d"))
73+
-- Expr.epsilon
74+
-- )
75+
-- )
76+
-- )
77+
-- )
78+
-- (node "a" [node "b" [], node "c" [node "d" []]])
79+
80+
-- -- try to engage skip using emptyset, since it is unescapable
81+
-- #eval runTwice'
82+
-- (Expr.tree (Pred.eq (Token.string "a"))
83+
-- Expr.emptyset
84+
-- )
85+
-- (node "a" [node "b" []])
86+
87+
-- #eval runTwice'
88+
-- (Expr.tree (Pred.eq (Token.string "a"))
89+
-- (Expr.concat
90+
-- (Expr.tree (Pred.eq (Token.string "b"))
91+
-- Expr.emptyset
92+
-- )
93+
-- (Expr.tree (Pred.eq (Token.string "c"))
94+
-- (Expr.tree (Pred.eq (Token.string "d"))
95+
-- Expr.epsilon
96+
-- )
97+
-- )
98+
-- )
99+
-- )
100+
-- (node "a" [node "b" [], node "c" [node "d" []]])
101+
102+
-- #eval runTwice'
103+
-- (Expr.tree (Pred.eq (Token.string "a"))
104+
-- (Expr.concat
105+
-- (Expr.tree (Pred.eq (Token.string "b"))
106+
-- Expr.epsilon
107+
-- )
108+
-- Expr.emptyset
109+
-- )
110+
-- )
111+
-- (node "a" [node "b" [], node "c" [node "d" []]])
112+
113+
-- #eval runTwice'
114+
-- (Expr.tree (Pred.eq (Token.string "a"))
115+
-- (Expr.concat
116+
-- (Expr.tree (Pred.eq (Token.string "b"))
117+
-- Expr.epsilon
118+
-- )
119+
-- (Expr.tree (Pred.eq (Token.string "c"))
120+
-- Expr.emptyset
121+
-- )
122+
-- )
123+
-- )
124+
-- (node "a" [node "b" [], node "c" [node "d" []]])
125+
126+
-- #eval runTwice'
127+
-- (Expr.tree (Pred.eq (Token.string "a"))
128+
-- (Expr.concat
129+
-- (Expr.tree (Pred.eq (Token.string "b"))
130+
-- Expr.epsilon
131+
-- )
132+
-- (Expr.tree (Pred.eq (Token.string "c"))
133+
-- (Expr.tree (Pred.eq (Token.string "d"))
134+
-- Expr.emptyset
135+
-- )
136+
-- )
137+
-- )
138+
-- )
139+
-- (node "a" [node "b" [], node "c" [node "d" []]])

0 commit comments

Comments
 (0)