blob: 02e2ae01a02998129fb5be9652e0a0747bd17b11 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
#lang racket
;; ZADANIE 2
;; =========
;; W tym zadaniu przyjrzymy się pierwszemu "językowi programowania"
;; który widzieliśmy na zajęciach: wyrażeniom arytmetycznym. Ich
;; prostota przejawia się przede wszystkim tym że nie występują w nich
;; zmienne (a w szczególności ich wiązanie) — dlatego możemy o nich
;; wnioskować nie używając narzędzi cięższych niż te poznane na
;; wykładzie.
;; W tym zadaniu będziemy chcieli udowodnić że nasza prosta kompilacja
;; do odwrotnej notacji polskiej jest poprawna. Konkretniej, należy
;; · sformułować zasady indukcji dla obydwu typów danych
;; reprezentujących wyrażenia (expr? i rpn-expr?)
;; · sformułować i udowodnić twierdzenie mówiące że kompilacja
;; zachowuje wartość programu, tj. że obliczenie wartości programu
;; jest równoważne skompilowaniu go do RPN i obliczeniu.
;; · sformułować i udowodnić twierdzenie mówiące że translacja z RPN
;; do wyrażeń arytmetycznych (ta która była zadaniem domowym;
;; implementacja jest poniżej) jest (prawą) odwrotnością translacji
;; do RPN (czyli że jak zaczniemy od wyrażenia i przetłumaczymy do
;; RPN i z powrotem, to dostaniemy to samo wyrażenie).
;; Swoje rozwiązanie należy wpisać na końcu tego szablonu w
;; komentarzu, podobnie do niniejszej treści zadania; proszę zadbać o
;; czytelność dowodów!
(struct const (val) #:transparent)
(struct binop (op l r) #:transparent)
(define (operator? x)
(member x '(+ * - /)))
(define (expr? e)
(match e
[(const v)
(integer? v)]
[(binop op l r)
(and (operator? op)
(expr? l)
(expr? r))]
[_ false]))
(define (value? v)
(number? v))
(define (op->proc op)
(match op
['+ +]
['- -]
['* *]
['/ /]))
;; zał: (expr? e) jest prawdą
;; (value? (eval e)) jest prawdą
(define (eval e)
(match e
[(const v) v]
[(binop op l r)
(let ((vl (eval l))
(vr (eval r))
(p (op->proc op)))
(p vl vr))]))
(define (rpn-expr? e)
(and (list? e)
(pair? e)
(andmap (lambda (x) (or (number? x) (operator? x))) e)))
(struct stack (xs))
(define empty-stack (stack null))
(define (empty-stack? s) (null? (stack-xs s)))
(define (top s) (car (stack-xs s)))
(define (push a s) (stack (cons a (stack-xs s))))
(define (pop s) (stack (cdr (stack-xs s))))
(define (eval-am e s)
(cond
[(null? e) (top s)]
[(number? (car e)) (eval-am (cdr e) (push (car e) s))]
[(operator? (car e))
(let* ((vr (top s))
(s (pop s))
(vl (top s))
(s (pop s))
(v ((op->proc (car e)) vl vr)))
(eval-am (cdr e) (push v s)))]))
(define (rpn-eval e)
(eval-am e empty-stack))
(define (arith->rpn e)
(match e
[(const v) (list v)]
[(binop op l r) (append (arith->rpn l) (arith->rpn r) (list op))]))
(define (rpn-translate e s)
(cond
[(null? e)
(top s)]
[(number? (car e))
(rpn-translate (cdr e) (push (const (car e)) s))]
[(operator? (car e))
(let* ((er (top s))
(s (pop s))
(el (top s))
(s (pop s))
(en (binop (car e) el er)))
(rpn-translate (cdr e) (push en s)))]))
(define (rpn->arith e)
(rpn-translate e empty-stack))
|
