---
jupytext:
  text_representation:
    extension: .md
    format_name: myst
    format_version: 0.12
    jupytext_version: 1.8.0
kernelspec:
  display_name: OCaml 4.11
  language: OCaml
  name: ocaml-jupyter
---

# Vaje

```{code-cell}
:tags: [remove-cell, remove-stdout]

(* Ko se v Jupytru prvič požene OCaml, program Findlib izpiše neko sporočilo.
   Da se to sporočilo ne bi videlo v zapiskih, je tu ta celica, ki sproži izpis,
   vendar ima nastavljeno, da je v zapiskih v celoti skrita. *)
```

## Naloga 1

Zapišite evaluacijsko drevo za naslednja ukaza v jeziku IMP:

  1. `#a := 1; if #a < 2 then #b := 2 * #a else #b := 0`
  
  2. `#a := 0; while #a < 2 do #a := #a + 1`

## Naloga 2

Dopolnite operacijsko semantiko jezika IMP z:

  1. Logičnima operacijama `&&` in `||`. Primerjajte pravila, kjer izračunamo vrednosti obeh argumentov in t.i. 'short-circuit evaluation', ki vrednost drugega argumenta izračuna zgolj, če je to potrebno.

  2. Operacijo CAS (compare and swap), kjer `cas loc n m` preveri, ali ima lokacija `loc` vrednost `n`. V primeru ujemanja vrednost lokacije posodobi na `m`, sicer ne spremeni ničesar.

## Naloga 3

Zapišite induktivno definicijo seznamov z elementi iz množice A in nato izpeljite pravila za dokaz z indukcijo.

V nadaljevanju bomo uporabljali OCaml notacijo za sezname, torej `[]` in `x :: xs` za konstruktorja in `l1 @ l2` za lepljenje seznamov.

Definirajte manjkajoče funkcije in z indukcijo pokažite enakosti:

  1. `xs @ [] = xs`

  2. `reverse (xs @ ys) = reverse ys @ reverse xs`

  3. `reverse (reverse xs) = xs`

  4. `map f (map g xs) = map (fun x -> f (g x)) xs`

  5. `map f (reverse xs) = reverse (map f xs)`

## Naloga 4

Pokažite, da lahko podmnožico naraščajočih seznamov podamo z induktivno relacijo.

## Naloga 5

Zapišite induktivno definicijo dvojiških dreves z vrednostmi iz množice A in nato izpeljite pravila za dokaz z indukcijo.

Za funkciji

```ocaml
let rec mirror = function
  | Empty -> Empty
  | Node (lt, x, rt) -> Node (mirror rt, x, mirror lt)

let rec depth = function
  | Empty -> 0
  | Node (lt, x, rt) -> 1 + (max (depth lt) (depth rt))
```

pokažite `depth tree = depth (mirror tree)`. Katero lastnost funkcije `max` je  potrebno privzeti?

Nato napišite funkciji `tree_map` in `tree_to_list` in dokažite enakost

``` tree_to_list (tree_map f tree) = list_map f (tree_to_list tree) ```

## Naloga 6

Razširite izrek o varnosti za jezik IMP za konstrukciji iz Naloge 1.