oeiuwq.com
A Golang runtime and compilation backend for Delta Interaction Nets.
1package main
2
3import (
4 "fmt"
5 "os"
6 "path/filepath"
7
8 "github.com/vic/godnet/pkg/lambda"
9)
10
11type TestCase struct {
12 Name string
13 Input string
14 Output string
15}
16
17const testTemplate = `
18package gentests
19import _ "embed"
20import "testing"
21import "github.com/vic/godnet/cmd/gentests/helper"
22//go:embed input.nix
23var input string
24//go:embed output.nix
25var output string
26func Test_%s_Reduction(t *testing.T) {
27 gentests.CheckLambdaReduction(t, "%s", input, output)
28}
29`
30
31func main() {
32 tests := []TestCase{
33 // Identity
34 {"001_id", "x: x", "y: y"},
35 {"002_id_id", "(x: x) (y: y)", "z: z"},
36
37 // K Combinator (Erasure)
38 {"003_k_1", "(x: y: x) a b", "a"},
39 {"004_k_2", "(x: y: y) a b", "b"},
40 {"005_erase_complex", "(x: y: x) a ((z: z) b)", "a"},
41
42 // S Combinator (Sharing)
43 {"006_s_1", "(x: y: z: x z (y z)) (a: b: a) (c: d: c) e", "e"},
44 {"007_s_2", "(x: y: z: x z (y z)) (a: b: b) (c: d: c) e", "e"},
45
46 // Church Numerals
47 {"010_zero", "(f: x: x) f x", "x"},
48 {"011_one", "(f: x: f x) f x", "f x"},
49 {"012_two", "(f: x: f (f x)) f x", "f (f x)"},
50 {"013_succ_0", "(n: f: x: f (n f x)) (f: x: x) f x", "f x"},
51 //{"014_succ_1", "(n: f: x: f (n f x)) (f: x: f x) f x", "f (f x)"},
52 //{"015_add_1_1", "(m: n: f: x: m f (n f x)) (f: x: f x) (f: x: f x) f x", "f (f x)"},
53 //{"016_mul_2_2", "(m: n: f: m (n f)) (f: x: f (f x)) (f: x: f (f x)) f x", "f (f (f (f x)))"},
54
55 // Logic
56 {"020_true", "(x: y: x) a b", "a"},
57 {"021_false", "(x: y: y) a b", "b"},
58 {"022_not_true", "(b: b (x: y: y) (x: y: x)) (x: y: x) a b", "b"},
59 {"023_not_false", "(b: b (x: y: y) (x: y: x)) (x: y: y) a b", "a"},
60 {"024_and_true_true", "(p: q: p q p) (x: y: x) (x: y: x) a b", "a"},
61 {"025_and_true_false", "(p: q: p q p) (x: y: x) (x: y: y) a b", "b"},
62
63 // Pairs
64 {"030_pair_fst", "(p: p (x: y: x)) ((x: y: f: f x y) a b)", "a"},
65 {"031_pair_snd", "(p: p (x: y: y)) ((x: y: f: f x y) a b)", "b"},
66
67 // Let bindings
68 {"040_let_simple", "let x = a; in x", "a"},
69 {"041_let_id", "let i = x: x; in i a", "a"},
70 //{"042_let_nested", "let x = a; in let y = b; in x", "a"},
71 //{"043_let_shadow", "let x = a; in let x = b; in x", "b"},
72
73 // Complex / Stress
74 //{"050_deep_app", "(x: x x x) (y: y)", "y: y"},
75 {"051_share_app", "(f: f (f x)) (y: y)", "x"},
76
77 //{"060_pow_2_3", "(b: e: e b) (f: x: f (f x)) (f: x: f (f (f x))) f x", "f (f (f (f (f (f (f (f x)))))))"},
78
79 // Replicator tests
80 {"070_share_complex", "(x: x (x a)) (y: y)", "a"},
81
82 // Erasure of shared term
83 {"071_erase_shared", "(x: y: y) ((z: z) a) b", "b"},
84
85 // Commutation
86 //{"072_self_app", "(x: x x) (y: y)", "y: y"},
87
88 // Nested Lambdas
89 //{"080_nested_1", "x: y: z: x y z", "x: y: z: x y z"},
90 {"081_nested_app", "(x: y: x y) a b", "a b"},
91
92 // Free variables
93 {"090_free_1", "x", "x"},
94 {"091_free_app", "x y", "x y"},
95 //{"092_free_abs", "y: x y", "y: x y"},
96
97 // Mixed
98 {"100_mixed_1", "(x: x) ((y: y) a)", "a"},
99 }
100
101 baseDir := "cmd/gentests/generated"
102 os.MkdirAll(baseDir, 0755)
103
104 for _, tc := range tests {
105 dir := filepath.Join(baseDir, tc.Name)
106 os.MkdirAll(dir, 0755)
107
108 // Normalize Input
109 inTerm, err := lambda.Parse(tc.Input)
110 if err != nil {
111 fmt.Printf("Error parsing input for %s: %v\n", tc.Name, err)
112 continue
113 }
114
115 // Normalize Output
116 outTerm, err := lambda.Parse(tc.Output)
117 if err != nil {
118 fmt.Printf("Error parsing output for %s: %v\n", tc.Name, err)
119 continue
120 }
121
122 testGo := fmt.Sprintf(testTemplate, tc.Name, tc.Name)
123
124 os.WriteFile(filepath.Join(dir, "input.nix"), []byte(inTerm.String()), 0644)
125 os.WriteFile(filepath.Join(dir, "output.nix"), []byte(outTerm.String()), 0644)
126 os.WriteFile(filepath.Join(dir, "reduction_test.go"), []byte(testGo), 0644)
127 }
128
129 fmt.Printf("Generated %d tests\n", len(tests))
130}
131
132/*
133func church(n int) string {
134 body := "x"
135 for i := 0; i < n; i++ {
136 body = fmt.Sprintf("f (%s)", body)
137 }
138 return fmt.Sprintf("(f: x: %s)", body)
139}
140
141func churchBody(n int) string {
142 body := "x"
143 for i := 0; i < n; i++ {
144 body = fmt.Sprintf("f (%s)", body)
145 }
146 return body
147}
148*/