reduce.zig (5188B)
1 const std = @import("std"); 2 const tree = @import("tree.zig"); 3 const Arena = @import("arena.zig").Arena; 4 5 pub const ReduceError = error{ 6 FuelExhausted, 7 InvalidApply, 8 OutOfMemory, 9 }; 10 11 /// Reduce a term to weak head normal form. 12 pub fn reduce(root: u32, arena: *Arena, fuel: u64) ReduceError!u32 { 13 var remaining = fuel; 14 return try whnf(root, arena, &remaining); 15 } 16 17 fn whnf(term: u32, arena: *Arena, fuel: *u64) ReduceError!u32 { 18 var current = term; 19 20 while (true) { 21 switch (arena.get(current).*) { 22 .leaf, .stem, .fork => return current, 23 .app => |app| { 24 if (fuel.* == 0) return error.FuelExhausted; 25 fuel.* -= 1; 26 27 const orig = current; 28 const func_idx = app.func; 29 const arg_idx = app.arg; 30 31 // Reduce function to WHNF 32 const f = try whnf(func_idx, arena, fuel); 33 34 switch (arena.get(f).*) { 35 // apply Leaf b = Stem b 36 .leaf => { 37 arena.get(orig).* = .{ .stem = .{ .child = arg_idx } }; 38 return orig; 39 }, 40 // apply (Stem a) b = Fork a b 41 .stem => |s| { 42 const a = s.child; 43 arena.get(orig).* = .{ .fork = .{ .left = a, .right = arg_idx } }; 44 return orig; 45 }, 46 .fork => |fork_f| { 47 const left_idx = fork_f.left; 48 const right_idx = fork_f.right; 49 50 // Reduce left child of Fork 51 const left = try whnf(left_idx, arena, fuel); 52 53 switch (arena.get(left).*) { 54 // apply (Fork Leaf a) _ = a 55 .leaf => { 56 const result = try whnf(right_idx, arena, fuel); 57 if (orig != result) { 58 arena.get(orig).* = arena.get(result).*; 59 } 60 return orig; 61 }, 62 // apply (Fork (Stem a) b) c = (a c) (b c) 63 .stem => |s| { 64 const a = s.child; 65 const inner1 = try arena.alloc(.{ .app = .{ .func = a, .arg = arg_idx } }); 66 const inner2 = try arena.alloc(.{ .app = .{ .func = right_idx, .arg = arg_idx } }); 67 arena.get(orig).* = .{ .app = .{ .func = inner1, .arg = inner2 } }; 68 current = orig; 69 continue; 70 }, 71 .fork => { 72 // Reduce argument 73 const arg = try whnf(arg_idx, arena, fuel); 74 75 switch (arena.get(arg).*) { 76 // apply (Fork (Fork a b) c) Leaf = a 77 .leaf => { 78 const a_idx = arena.get(left).fork.left; 79 const result = try whnf(a_idx, arena, fuel); 80 if (orig != result) { 81 arena.get(orig).* = arena.get(result).*; 82 } 83 return orig; 84 }, 85 // apply (Fork (Fork a b) c) (Stem u) = b u 86 .stem => |s| { 87 const b_idx = arena.get(left).fork.right; 88 const u = s.child; 89 arena.get(orig).* = .{ .app = .{ .func = b_idx, .arg = u } }; 90 current = orig; 91 continue; 92 }, 93 // apply (Fork (Fork a b) c) (Fork u v) = (c u) v 94 .fork => |arg_fork| { 95 const c_idx = right_idx; 96 const u = arg_fork.left; 97 const v = arg_fork.right; 98 const inner = try arena.alloc(.{ .app = .{ .func = c_idx, .arg = u } }); 99 arena.get(orig).* = .{ .app = .{ .func = inner, .arg = v } }; 100 current = orig; 101 continue; 102 }, 103 .app => return error.InvalidApply, 104 } 105 }, 106 .app => return error.InvalidApply, 107 } 108 }, 109 .app => return error.InvalidApply, 110 } 111 }, 112 } 113 } 114 }