---
tags: mp20-dabi
---
# Lista zagadnień nr 7 (na 21.04.2020)
### Metody programowania 2020, II UWr

Grupa ćwiczeniowa: dabi

---
### Ćwiczenie 1
::: info
Rozwiązuje: **Foxtrot**
:::

(struct pow(e1 e2) #:transparent)
(struct sum (e1 e2 i f) #:transparent)
(struct integral (e1 e2 x f) #:transparent)
(struct minimum (f i) #:transparent)
(struct infinity() #:transparent)

(define (expr? e)
  (match e
    [(const n) 
     (number? n)]
    [(binop op l r) 
     (and (symbol? op) (expr? l) (expr? r))]
    [(var-expr x) 
     (symbol? x)]
    [(let-expr x e1 e2) 
     (and (symbol? x) (expr? e1) (expr? e2))]
    [(pow e1 e2) 
     (and (expr? e1) (expr? e2))]
    [(sum e1 e2 i f) 
     (and (expr? e1) (expr? e2) (symbol? i) (expr? f))]
    [(integral e1 e2 x f) 
     (and (expr? e1) (expr e2) (symbol? x) (expr? f))]
    [(minimum f i) 
     (and (expr? f) (symbol? i)]
    [(infinity) true]
    [_ false]))
    
(define test-sum 
  (sum (const 1) 
       (const 5) 
       'i 
       '(binop '* 
               (const 2) 
               (var-expr 'i))))   

(define test-minimum 
  (minimum (binop '* 
                  (const 2) 
                  (var-expr 'i)) 
           'i))

(define test-integral 
  (integral (const 0) 
            (infinity) 
            'x 
            (binop '* 
                   (const 4) 
                   (var-expr 'x')))

(define (subst e1 x e2)        
  (match e2
    [(var-expr y) 
    (if (eq? x y) e1 (var-expr y))]
    [(const n) (const n)]
    [(binop op l r)
     (binop op (subst e1 x l) (subst e1 x r))]
    [(let-expr y e3 e4)
     (let-expr y (subst e1 x e3) 
                 (if (eq? x y) e4 (subst e1 x e4)))]
    [(minimum f i)
     (minimum (if (eq? x i) f (subst e1 x f)) i)]
    [(pow e3 e4)
     (pow (subst e1 x e3) (subst e1 x e4))]
    [(sum e3 e4 i f)
     (sum (subst e1 x e3)
          (subst e1 x e4)
          i
          (if (eq? x i)
              f
              (subst e1 x f)))]
    [(integral e3 e4 y f)
     (sum (subst e1 x e3)
          (subst e1 x e4)
          y
          (if (eq? x y)
              f
              (subst e1 x f)))]
    [(infinity) (infinity)]))

;; Bez ifa podstawienie w '(min i (+ i 1)) za 'i daje '(min i (+ 100 1)) (składnia konkretna)

;; Uwaga na przechwycenie zmiennej:

(define e1 'x)
(define e2 '(let (x 42) (+ y x)))
(define e3 '(let (z 42) (+ y z)))

> (subst (parse e1) 'y (parse e2))
(let-expr 'x (const 42) (binop '+ (var-expr 'x) (var-expr 'x)))

> (subst (parse e1) 'y (parse e3))
(let-expr 'z (const 42) (binop '+ (var-expr 'x) (var-expr 'z)))

;; Na szczęście my zawsze podstawiamy wyrażenia zamknięte (programy).

---
### Ćwiczenie 2
::: info
Rozwiązuje: **Alpha**
:::

;'(^ a b)
;'(sum begin end i f(i))
;'(integral begin end x f(x))
;'(min i f)
;'inf

(define (parse q)
  (cond [(number? q) 
         (const q)]
        [(symbol? q) 
         q]
        [(eq? 'inf q) 
         (infinity)]
        [(and (list? q) 
              (eq? (length q) 3) 
              (symbol? (second q))
              (eq? 'min (first q)))
         (minimum (parse (third q))
                  (second q))]
         [(and (list? q) 
               (eq? (length q) 3) 
               (eq? '^ (first q)))
         (pow (parse (second q)) 
              (parse (third q)))]
        [(and (list? q) 
              (eq? (length q) 3) 
              (symbol? (first q)))
         (binop (first q) 
                (parse (second q)) 
                (parse (third q)))]
        [(and (list? q) 
              (eq? (length q) 5) 
              (symbol? (fourth q)) 
              (eq? 'sum (first q)))
         (sum (parse (second q)) 
              (parse (third q)) 
              (fourth q)
              (parse (fifth q)))]
        [(and (list? q) 
              (eq? (length q) 5) 
              (symbol? (fourth q)) 
              (eq? 'integral (first q)))
         (integral (parse (second q)) 
                   (parse (third q)) 
                   (fourth q)
                   (parse (fifth q)))]))

(define test-parse 
  (parse '(^ (integral 1 5 x (^ x 2)) (sum 0 4 x x))))

---
### Ćwiczenie 3
::: info
Rozwiązuje: **Beta**
:::

(struct binsign (sign f1 f2)     #:transparent)
(struct monosign (sign f)        #:transparent)
(struct quantifier (q v formula) #:transparent)
(struct variable (v)             #:transparent)

(define (expr? e)
  (match e
    [(variable v)               (symbol? v)]
    [(binsign sign f1 f2)       (and (symbol? sign) (expr? f1) (expr? f2))]
    [(monosign sign f)          (and (symbol? sign) (expr? f))]
    [(quantifier q v formula)   (and (symbol? q) (symbol? v) (expr? formula))]
    [_              false]))

(define (good-binsign? sign)
  (member sign '(and or)))

(define (good-monosign? sign)
  (member sign '(neg)))

(define (good-quantifier? quantifier)
  (member quantifier '(forall exists)))

(define (parse e)
  (cond
    [(and (list? e)
          (= (length e) 3)
          (good-quantifier? (first e))
          (symbol? (second e)))
     (quantifier (first e) (second e) (parse (third e)))]
    [(and (list? e)
         (good-binsign? (second e))
         (= (length e) 3))
         (binsign (second e) (parse (first e)) (parse (third e)))]
    [(and (list? e)
         (good-monosign? (first e))
         (= (length e) 2))
         (monosign (first e) (parse (second e)))]
    [(symbol? e)
     (variable e)]
    [else false]))
    
;;Przykład działania parsera:
(parse (list 'forall 'x (list 'x 'and  (neg 'x))))
(quantifier 'forall (variable 'x) (binsign 'conj (variable 'x) (monosign 'neg (variable 'x))))   

---
### Ćwiczenie 4
::: info
Rozwiązuje: **Charlie**
:::

(define (eval x)
  (define (eval-formula f l)
    (define (eval-var v l)
      (if (null? l)
          #f
          (if (eq? (car (first l)) v)
              (cdr (first l))
              (eval-var v (cdr l)))))
    (match f
      [(binsign 'or f1 f2) (or (eval-formula f1 l)
                               (eval-formula f2 l))]
      [(binsign 'and f1 f2) (and (eval-formula f1 l)
                                 (eval-formula f2 l))]
      [(monosign 'neg f1) (not (eval-formula f1 l))]
      [(variable f1) (eval-var f1 l)]))
  (define (eval-aux ex lst)
    (match ex
      [(quantifier 'exists v f) (or (eval-aux f (append lst (list (cons v #t))))
                                    (eval-aux f (append lst (list (cons v #f)))))]
      [(quantifier 'forall v f) (and (eval-aux f (append lst (list (cons v #t))))
                                     (eval-aux f (append lst (list (cons v #f)))))]
      [_ (eval-formula ex lst)]))
  (match x
      [(quantifier 'exists v f) (or (eval-aux f (list (cons v #t)))
                                    (eval-aux f (list (cons v #f))))]
      [(quantifier 'forall v f) (and (eval-aux f (list (cons v #t)))
                                     (eval-aux f (list (cons v #f))))]))

Rozwiązanie z użyciem interfejsu środowiska (dabi):

;; formuły qbf

(struct conj (l r)    #:transparent)
(struct disj (l r)    #:transparent)
(struct pvar (id)     #:transparent)
(struct forall (id f) #:transparent)
(struct exists (id f) #:transparent)

;; ewaluator

(define (eval-env f env)
  (match f
    [(conj f1 f2)
     (and (eval-env f1 env)
          (eval-env f2 env))]
    [(disj f1 f2)
     (or (eval-env f1 env)
         (eval-env f2 env))]
    [(pvar x)
     (env-lookup x env)]
    [(forall x g)
     (and (eval-env g (env-add x true env))
          (eval-env g (env-add x false env)))]
    [(exists x g)
     (or (eval-env g (env-add x true env))
         (eval-env g (env-add x false env)))]))

(define (eval f)
  (eval-env f env-empty))

(define (test-eval-1)
  (eval (forall 'x (exists 'y (disj (pvar 'x) (pvar 'y))))))

---
### Ćwiczenie 5
::: info
Rozwiązuje: **Delta**
:::

:::warning
Czekamy na rozwiązanie.

**Uwaga:** w przypadku wykrycia przysłaniania, nie jest wymagane przemianowanie obu zmiennych - wystarczy zająć się wewnętrznym ```let```-em (mimo, że przykład w treści ćwiczenia może sugerować inaczej).
:::

;; środowisko (uwaga: env-lookup zwraca false w razie porażki)

(struct environ (xs))

(define env-empty (environ null))
(define (env-add x v env)
  (environ (cons (cons x v) (environ-xs env))))
(define (env-lookup x env)
  (define (assoc-lookup xs)
    (cond [(null? xs) #f]
          [(eq? x (car (car xs))) (cdr (car xs))]
          [else (assoc-lookup (cdr xs))]))
  (assoc-lookup (environ-xs env)))
  
(define (rename e)
  ...)

;; oczekiwane działanie:

> (rename (binop '+
                 (let-expr 'x (const 1) (var-expr 'x))
                 (let-expr 'x (const 1) (var-expr 'x))))
(binop '+ 
        (let-expr 'x31080 (const 1) 'x31080) 
        (let-expr 'x31081 (const 1) 'x31081))          


> (rename (let-expr 'x 
                    (const 3)
                    (binop '+
                           (var-expr 'x)
                           (let-expr 'x 
                                     (const 5)
                                     (var-expr 'x)))))
(let-expr 'x31664 
          (const 3) 
          (binop '+ 
                 'x31664 
                 (let-expr 'x31665 
                           (const 5) 
                           'x31665)))

---
### Ćwiczenie 6
::: info
Rozwiązuje: **Echo**
:::

(define (rename e)
  (define (walk e env)
    (match e
      [(const v) (const v)]
      [(binop op l r) (binop op 
                             (walk l env) 
                             (walk r env))]
      [(var-expr v) (var-expr (env-lookup v env))]
      [(let-expr x e1 e2) 
       (let ([z (gensym 'x)])
         (let-expr z 
                   (walk e1 env) 
                   (walk e2 (env-add x z env))))]))
  (walk e env-empty))

> (rename (binop '+
                 (let-expr 'x (const 1) (var-expr 'x))
                 (let-expr 'x (const 1) (var-expr 'x))))
(binop '+ 
        (let-expr 'x31080 (const 1) 'x31080) 
        (let-expr 'x31081 (const 1) 'x31081))          

> (rename (let-expr 'x 
                    (const 3)
                    (binop '+
                           (var-expr 'x)
                           (let-expr 'x 
                                     (const 5) 
                                     (var-expr 'x)))))
(let-expr 'x31664 
          (const 3) 
          (binop '+ 
                 'x31664 
                 (let-expr 'x31665 
                           (const 5) 
                           'x31665)))

:::danger
A jeszcze spróbujmy napisać wersję bez użycia procedury gensym.
:::

---
### Ćwiczenie 7
::: info
Rozwiązuje: **Wszyscy**
:::
:::warning
Czekamy na rozwiązanie.
:::