A Tracing Meta-Interpreter for Thun

diff --git a/thun/metalogical.pl b/thun/metalogical.pl
new file mode 100644 (file)
index 0000000..440d13c
--- /dev/null
+++ b/thun/metalogical.pl
@@ -0,0 +1,55 @@
+% A Tracing Meta-Interpreter for Thun\r
+\r
+alpha(true).\r
+alpha((A, B)) :- alpha(A), alpha(B).\r
+alpha(number(A)) :- !, number(A).\r
+alpha(var(A)) :- !, var(A).\r
+alpha(!) :- !.\r
+\r
+% Meta-logical print trace.\r
+% (Could also be captured in a list or something instead.)\r
+alpha(thun(E, Si, _)) :- portray_clause(Si-E), fail.\r
+\r
+alpha(Goal) :-\r
+    checky(Goal),\r
+    clause(Goal, Body),  % doesn't work for e.g. +\r
+    alpha(Body).\r
+\r
+checky(Goal) :-\r
+    Goal \= true,\r
+    Goal \= (_,_),\r
+    Goal \= var(_),\r
+    Goal \= number(_),\r
+    Goal \= !.\r
+\r
+/*\r
+\r
+[debug]  ?- alpha(thun([1, 2, swap], Si, So)).\r
+_-[1, 2, swap].\r
+[1|_]-[2, swap].\r
+[2, 1|_]-[swap].\r
+[1, 2|_]-[].\r
+So = [1, 2|Si] ;\r
+false.\r
+\r
+[debug]  ?- alpha(thun([[1], 2, swons], Si, So)).\r
+_-[[1], 2, swons].\r
+[[1]|_]-[2, swons].\r
+[2, [1]|_]-[swons].\r
+[2, [1]|_]-[swap, cons].\r
+[[1], 2|_]-[cons].\r
+[[2, 1]|_]-[].\r
+So = [[2, 1]|Si] .\r
+\r
+[debug]  ?- alpha(thun([[1], 2, [swons], i], Si, So)).\r
+_-[[1], 2, [swons], i].\r
+[[1]|_]-[2, [swons], i].\r
+[2, [1]|_]-[[swons], i].\r
+[[swons], 2, [1]|_]-[i].\r
+[2, [1]|_]-[swons].\r
+[2, [1]|_]-[swap, cons].\r
+[[1], 2|_]-[cons].\r
+[[2, 1]|_]-[].\r
+So = [[2, 1]|Si] .\r
+\r
+*/
\ No newline at end of file