|
1 | 1 | module TermReducer where |
2 | 2 |
|
3 | | -import Data.Generics.Uniplate.Data |
| 3 | +import Data.Generics.Uniplate.Data |
4 | 4 | import CLTerm |
5 | | -import Debug.Trace |
6 | 5 |
|
7 | | --- reduce :: Exp -> Exp |
8 | | --- reduce (((S :@ x) :@ y) :@ z) = (x :@ z) :@ (y :@ z) |
9 | | --- reduce ((((S' :@ x) :@ y) :@ z) :@ w) = (x :@ (y :@ w)) :@ (z :@ w) |
10 | | --- reduce ((K :@ x) :@ _y) = x |
11 | | --- reduce ((A :@ _x) :@ y) = y |
12 | | --- reduce ((U :@ x) :@ y) = y :@ x |
13 | | --- reduce (I :@ x) = x |
14 | | --- reduce (((B :@ x) :@ y) :@ z) = x :@ (y :@ z) |
15 | | --- reduce ((((B' :@ x) :@ y) :@ z) :@ w) = (x :@ y) :@ (z :@ w) |
16 | | --- reduce (((Z :@ x) :@ y) :@ _z) = x :@ y |
17 | | --- reduce (((C :@ x) :@ y) :@ z) = (x :@ z) :@ y |
18 | | --- reduce ((((C' :@ x) :@ y) :@ z) :@ w) = (x :@ (y :@ w)) :@ z |
19 | | --- reduce (((P :@ x) :@ y) :@ z) = (z :@ x) :@ y |
20 | | --- reduce (((R :@ x) :@ y) :@ z) = (y :@ z) :@ x |
21 | | --- reduce ((((O :@ x) :@ y) :@ z) :@ w) = (w :@ x) :@ y |
22 | | --- reduce (((K2 :@ x) :@ _y) :@ _z) = x |
23 | | --- reduce ((((K3 :@ x) :@ _y) :@ _z) :@ _w) = x |
24 | | --- reduce (((((K4 :@ x) :@ _y) :@ _z) :@ _w) :@ _v) = x |
25 | | --- reduce ((((C'B :@ x) :@ y) :@ z) :@ w) = (x :@ z) :@ (y :@ w) |
26 | | --- reduce (Label _ e) = e |
27 | | --- reduce (Tick _ :@ e) = e |
28 | | --- reduce e = e |
29 | 6 |
|
30 | 7 | -- | Single step reduction - reduces only the outermost redex |
31 | 8 | reduceStep :: CL -> CL |
32 | 9 | reduceStep (Com c) = Com c |
33 | 10 | reduceStep (INT i) = INT i |
34 | 11 | reduceStep (Com I :@ t) = t |
35 | | -reduceStep (Com K :@ t :@ u) = t |
36 | | -reduceStep (Com S :@ x :@ y :@ z) = (x :@ z) :@ (y :@ z) |
37 | | -reduceStep (Com B :@ f :@ g :@ x) = f :@ (g :@ x) -- B F G X = F (G X) |
38 | | -reduceStep (Com C :@ x :@ y :@ z) = x :@ z :@ y |
39 | | -reduceStep yt@(Com Y :@ t) = t :@ yt |
40 | | -reduceStep (Com P :@ t :@ u) = Com P :@ t :@ u |
41 | | -reduceStep (Com R :@ t :@ u) = Com R :@ t :@ u |
42 | | -reduceStep (Com ADD :@ INT i :@ INT j) = INT (i + j) |
43 | | -reduceStep (Com SUB :@ INT i :@ INT j) = INT (i - j) |
44 | | -reduceStep (Com MUL :@ INT i :@ INT j) = INT (i * j) |
45 | | -reduceStep (Com DIV :@ INT i :@ INT j) = INT (i `div` j) |
46 | | -reduceStep (Com REM :@ INT i :@ INT j) = INT (i `rem` j) |
| 12 | +reduceStep ((Com K :@ t) :@ u) = t |
| 13 | +reduceStep (((Com S :@ x) :@ y) :@ z) = (x :@ z) :@ (y :@ z) |
| 14 | +reduceStep (((Com B :@ f) :@ g) :@ x) = f :@ (g :@ x) -- B F G X = F (G X) |
| 15 | +reduceStep (((Com C :@ x) :@ y) :@ z) = x :@ z :@ y |
| 16 | +-- Y combinator: expand only when it's applied to something |
| 17 | +-- Y f x should reduce to f (Y f) x, not Y f should reduce to f (Y f) |
| 18 | +reduceStep ((Com Y :@ f) :@ x) = (f :@ (Com Y :@ f)) :@ x |
| 19 | +--reduceStep (Com Y :@ t) = Com Y :@ t -- Don't expand Y on its own |
| 20 | +reduceStep ((Com P :@ t) :@ u) = (Com P :@ t) :@ u -- P doesn't reduce |
| 21 | +-- R takes 3 arguments: R F G X = G X F |
| 22 | +reduceStep (((Com R :@ f) :@ g) :@ x) = (g :@ x) :@ f |
| 23 | +reduceStep ((Com ADD :@ INT i) :@ INT j) = INT (i + j) |
| 24 | +reduceStep ((Com SUB :@ INT i) :@ INT j) = INT (i - j) |
| 25 | +reduceStep ((Com MUL :@ INT i) :@ INT j) = INT (i * j) |
| 26 | +reduceStep ((Com DIV :@ INT i) :@ INT j) = INT (i `div` j) |
| 27 | +reduceStep ((Com REM :@ INT i) :@ INT j) = INT (i `rem` j) |
47 | 28 | reduceStep (Com SUB1 :@ INT i) = INT (i - 1) |
48 | | -reduceStep (Com EQL :@ INT i :@ INT j) = if i == j then trueCL else falseCL |
49 | | -reduceStep (Com GEQ :@ INT i :@ INT j) = if i >= j then trueCL else falseCL |
| 29 | +reduceStep ((Com EQL :@ INT i) :@ INT j) = if i == j then trueCL else falseCL |
| 30 | +reduceStep ((Com GEQ :@ INT i) :@ INT j) = if i >= j then trueCL else falseCL |
50 | 31 | reduceStep (Com ZEROP :@ INT i) = if i == 0 then trueCL else falseCL |
51 | | -reduceStep (Com ZEROP :@ i) = Com ZEROP :@ (reduce i) -- Keep ZEROP combinator for non-integer terms |
52 | | -reduceStep (Com B' :@ t :@ u :@ v) = t :@ (u :@ v) |
53 | | -reduceStep (Com C' :@ t :@ u :@ v) = t :@ v :@ u |
54 | | -reduceStep (Com S' :@ t :@ u :@ v) = (t :@ v) :@ (u :@ v) |
| 32 | +reduceStep (Com ZEROP :@ i) = Com ZEROP :@ reduceStep i -- Reduce argument without calling full reduce |
| 33 | +-- B' takes 4 arguments: B' P Q R S = P Q (R S) |
| 34 | +reduceStep ((((Com B' :@ p) :@ q) :@ r) :@ s) = (p :@ q) :@ (r :@ s) |
| 35 | +-- C' takes 4 arguments: C' P Q R S = P (Q S) R |
| 36 | +reduceStep ((((Com C' :@ p) :@ q) :@ r) :@ s) = (p :@ (q :@ s)) :@ r |
| 37 | +-- S' takes 4 arguments: S' P Q R S = P (Q S) (R S) |
| 38 | +reduceStep ((((Com S' :@ p) :@ q) :@ r) :@ s) = (p :@ (q :@ s)) :@ (r :@ s) |
55 | 39 | reduceStep (Com T :@ t) = t |
56 | | -reduceStep (Com A :@ x :@ y) = y -- A combinator: λx y. y (like FALSE) |
57 | | --- For partial applications, try to reduce arguments |
58 | | -reduceStep (f :@ x) = |
59 | | - let f' = reduce f |
60 | | - in if f' == f |
61 | | - then f :@ reduceStep x -- Only reduce argument if function can't be reduced |
62 | | - else f' :@ x -- Apply reduction to function first |
| 40 | +reduceStep ((Com A :@ x) :@ y) = y -- A combinator: λx y. y (like TRUE, selects second) |
| 41 | +-- For partial applications, don't reduce recursively in reduceStep |
| 42 | +reduceStep (f :@ x) = f :@ x -- No reduction for general applications |
63 | 43 | reduceStep x = x |
64 | 44 |
|
65 | | --- | Reduce with step limit to avoid infinite loops |
| 45 | +-- | Reduce with step limit using leftmost-outermost strategy |
66 | 46 | reduceWithLimit :: Int -> CL -> CL |
67 | 47 | reduceWithLimit 0 x = x |
68 | 48 | reduceWithLimit n x = |
69 | | - let x' = reduceStep (trace (show x) x) |
| 49 | + let x' = reduceOnce x |
70 | 50 | in if x' == x |
71 | 51 | then x -- Normal form reached |
72 | 52 | else reduceWithLimit (n-1) x' |
73 | 53 |
|
| 54 | +-- | Perform one reduction step using leftmost-outermost strategy |
| 55 | +reduceOnce :: CL -> CL |
| 56 | +reduceOnce term = |
| 57 | + -- First try direct reduction at the top level |
| 58 | + let stepped = reduceStep term |
| 59 | + in if stepped /= term |
| 60 | + then stepped -- A reduction happened at the top level |
| 61 | + else case term of |
| 62 | + -- For applications, use leftmost-outermost strategy |
| 63 | + f :@ x -> |
| 64 | + -- Try to reduce f first (leftmost) |
| 65 | + let f' = reduceOnce f |
| 66 | + in if f' /= f |
| 67 | + then f' :@ x -- If f reduced, keep x unchanged |
| 68 | + else |
| 69 | + -- If f didn't reduce, try to reduce x |
| 70 | + let x' = reduceOnce x |
| 71 | + in if x' /= x |
| 72 | + then f :@ x' |
| 73 | + else term -- Nothing can be reduced |
| 74 | + _ -> term -- No reduction possible |
| 75 | + |
74 | 76 | -- | Original reduce function - now with step limit |
75 | 77 | reduce :: CL -> CL |
76 | | -reduce = reduceWithLimit 50 -- Allow up to 50 reduction steps |
| 78 | +reduce = reduceWithLimit 1000 -- Increased limit for recursive functions |
77 | 79 |
|
78 | 80 | -- | Deep reduction using transform (original approach) |
79 | 81 | redDeep :: CL -> CL |
|
0 commit comments