► |  | Redex: Practical Semantics Engineering

1 | Amb: A Redex Tutorial
2 | Long Tutorial
3 | Extended Exercises
4 | The Redex Reference
5 | Automated Testing Benchmark
| Bibliography
| Index

▼ | 3 | Extended Exercises

3.1 | Problem: Objects
3.2 | Solution: Objects
3.3 | Problem: Types
3.4 | Solution: Types
3.5 | Problem: Missionaries and Cannibals
3.6 | Solution: Missionaries and Cannibals
3.7 | Problem: Towers of Hanoi
3.8 | Solution: Towers of Hanoi
3.9 | Problem: GC
3.10 | Solution: GC
3.11 | Problem: Finite State Machines
3.12 | Solution: Finite State Machines
3.13 | Problem: Threads
3.14 | Solution: Threads
3.15 | Problem: Contracts
3.16 | Solution: Contracts
3.17 | Problem: Binary Addition
3.18 | Solution: Binary Addition

top ← prev up next →

#### 3.8`` Solution: Towers of Hanoi

#lang racket
;; solving towers of Hanoi by searching the solution space
(require redex)
;; -----------------------------------------------------------------------------
;; the state space of configurations
(define-language L
[chunk *]
[tile (chunk ...)]
[stack (side-condition [tile_1 ...]
(term (stacked [tile_1 ...])))]
[state (stack ...)])
;; -----------------------------------------------------------------------------
;; checking the stacks
(define-metafunction L
stacked : [tile ...] -> any
[(stacked []) #t]
[(stacked [tile_0 tile_1 ...])
(stacked [tile_1 ...])
(judgment-holds (accepts [tile_1 ...] tile_0 ))])
(define-judgment-form L
#:mode (accepts I I)
#:contract (accepts stack tile)
[-----------------
(accepts [] tile)]
[-----------------
(accepts [(chunk_0 ... chunk_1 ..._1) tile ...]
(chunk_1 ..._1))])
;; -----------------------------------------------------------------------------
;; the redution system
(module+ test
(test-->>∃ -->hanoi
(term ([(*) (* *) (* * *)] [] []))
(term ([] [] [(*) (* *) (* * *)]))))
(define -->hanoi
(reduction-relation
L
[--> (stack_0 ... [tile_0 tile_1 ...]
stack_1 ... [tile_2 ...]
stack_3 ...)
(stack_0 ... [tile_1 ...]
stack_1 ... [tile_0 tile_2 ...]
stack_3 ...)
(judgment-holds (accepts [tile_2 ...] tile_0))]
[--> (stack_0 ... [tile_1 ...]
stack_1 ... [tile_0 tile_2 ...]
stack_3 ...)
(stack_0 ... [tile_0 tile_1 ...]
stack_1 ... [tile_2 ...]
stack_3 ...)
(judgment-holds (accepts [tile_1 ...] tile_0))]))
(module+ test
(test-results))
;; rendering the search
(module+ main
(traces -->hanoi (term ([(*) (* *) (* * *)] [] []))))

top ← prev up next →