aboutsummaryrefslogtreecommitdiff
path: root/semestr-2/racket/egzamin/zad2.bak
diff options
context:
space:
mode:
Diffstat (limited to 'semestr-2/racket/egzamin/zad2.bak')
-rw-r--r--semestr-2/racket/egzamin/zad2.bak119
1 files changed, 119 insertions, 0 deletions
diff --git a/semestr-2/racket/egzamin/zad2.bak b/semestr-2/racket/egzamin/zad2.bak
new file mode 100644
index 0000000..02e2ae0
--- /dev/null
+++ b/semestr-2/racket/egzamin/zad2.bak
@@ -0,0 +1,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)) \ No newline at end of file