|
1 | 1 | module TermReducer where |
2 | 2 |
|
3 | | -import Data.Generics.Uniplate.Data |
| 3 | +import Data.Generics.Uniplate.Data (descend) |
4 | 4 | import CLTerm |
5 | 5 |
|
6 | 6 |
|
@@ -42,37 +42,27 @@ reduceStep ((Com A :@ x) :@ y) = y -- A combinator: λx y. y (like TRUE, select |
42 | 42 | reduceStep (f :@ x) = f :@ x -- No reduction for general applications |
43 | 43 | --reduceStep x = x |
44 | 44 |
|
45 | | --- | Reduce with step limit using leftmost-outermost strategy |
46 | | -reduce :: CL -> CL |
47 | | -reduce x = |
48 | | - let x' = reduceOnce x |
49 | | - in if x' == x |
50 | | - then x -- Normal form reached |
51 | | - else reduce x' |
52 | 45 |
|
53 | | --- | Perform one reduction step using leftmost-outermost strategy |
54 | | -reduceOnce :: CL -> CL |
55 | | -reduceOnce term = |
56 | | - -- First try direct reduction at the top level |
57 | | - let stepped = reduceStep term |
58 | | - in if stepped /= term |
59 | | - then stepped -- A reduction happened at the top level |
60 | | - else case term of |
61 | | - -- For applications, use leftmost-outermost strategy |
62 | | - f :@ x -> |
63 | | - -- Try to reduce f first (leftmost) |
64 | | - let f' = reduceOnce f |
65 | | - in if f' /= f |
66 | | - then f' :@ x -- If f reduced, keep x unchanged |
67 | | - else |
68 | | - -- If f didn't reduce, try to reduce x |
69 | | - let x' = reduceOnce x |
70 | | - in if x' /= x |
71 | | - then f :@ x' |
72 | | - else term -- Nothing can be reduced |
73 | | - _ -> term -- No reduction possible |
74 | 46 |
|
| 47 | +-- | reduction using uniplate with custom traversal |
| 48 | +-- The key insight: we need to control the order of reduction |
| 49 | +reduce :: CL -> CL |
| 50 | +reduce = fixpoint reduceOnce |
| 51 | + where |
| 52 | + fixpoint f x = let x' = f x in if x' == x then x else fixpoint f x' |
75 | 53 |
|
76 | | --- | reduction using transform |
77 | | -reduce' :: CL -> CL |
78 | | -reduce' = transform reduceStep |
| 54 | +-- | One-step reduction with leftmost-outermost strategy |
| 55 | +-- Uses descend to try reduction at each level |
| 56 | +reduceOnce :: CL -> CL |
| 57 | +reduceOnce term = |
| 58 | + -- First try to reduce at the root |
| 59 | + let rootReduced = reduceStep term |
| 60 | + in if rootReduced /= term |
| 61 | + then rootReduced |
| 62 | + else |
| 63 | + -- If root doesn't reduce, use descend to try one level down |
| 64 | + -- descend applies function to immediate children |
| 65 | + let descended = descend reduceOnce' term |
| 66 | + in if descended /= term |
| 67 | + then descended |
| 68 | + else term |
0 commit comments