Skip to content

Commit 7007826

Browse files
committed
Lahenda abseval praktikumis
1 parent b048da5 commit 7007826

1 file changed

Lines changed: 42 additions & 3 deletions

File tree

src/abseval/abseval.ml

Lines changed: 42 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,14 +13,40 @@ struct
1313
Vihje: ID.of_interval.
1414
Vihje: ID.eval_binary. *)
1515
let rec eval_expr (env: ED.t) (expr: expr): ID.t =
16-
failwith "TODO"
16+
match expr with
17+
| Num i -> ID.of_int i
18+
| Var x -> ED.find x env
19+
| Rand (l, r) -> ID.of_interval (l, r)
20+
| Binary (l, b, r) ->
21+
ID.eval_binary (eval_expr env l) b (eval_expr env r)
1722

1823
(** Väärtustab valvuri (avaldis ja selle oodatav tõeväärtus) keskkonnas.
1924
Kui valvur on keskkonnaga vastuolus, siis tagastab saavutamatu programmi oleku ED.bot.
2025
Kui valvuriga saab keskkonna muutujate väärtusi täpsemaks kitsendada, siis võib keskkonda muuta.
2126
Võib jätta keskkonna muutmata, kuid siis ei kasutata valvurist saadavat lisainfot. *)
2227
let eval_guard (env: ED.t) (expr: expr) (branch: bool): ED.t =
23-
failwith "TODO"
28+
let id = eval_expr env expr in
29+
if not branch && not (ID.leq (ID.of_int 0) id) then
30+
ED.bot
31+
(* else if branch && ID.equal (ID.of_int 0) id then *)
32+
else if branch && ID.leq id (ID.of_int 0) then
33+
ED.bot
34+
else
35+
match expr, branch with
36+
| Var x, false -> ED.add x (ID.of_int 0) env
37+
| Var x, true ->
38+
let prev = ED.find x env in
39+
let excl = ID.exclude 0 prev in
40+
ED.add x excl env
41+
| Binary (Var x, Eq, Num i), false
42+
| Binary (Var x, Ne, Num i), true ->
43+
let prev = ED.find x env in
44+
let excl = ID.exclude i prev in
45+
ED.add x excl env
46+
| Binary (Var x, Eq, Num i), true
47+
| Binary (Var x, Ne, Num i), false ->
48+
ED.add x (ID.of_int i) env
49+
| _ -> env
2450

2551
module EDFP = Fixpoint.MakeDomain (ED)
2652

@@ -29,5 +55,18 @@ struct
2955
Vihje: eval_guard.
3056
Vihje: While jaoks kasuta püsipunkti moodulit EDFP. *)
3157
let rec eval_stmt (env: ED.t) (stmt: stmt): ED.t =
32-
failwith "TODO"
58+
match stmt with
59+
| Nop -> env
60+
| Assign (x, e) -> ED.add x (eval_expr env e) env
61+
| Seq (a, b) -> eval_stmt (eval_stmt env a) b
62+
| If (c, t, f) ->
63+
let env_t = eval_stmt (eval_guard env c true) t in
64+
let env_f = eval_stmt (eval_guard env c false) f in
65+
ED.join env_t env_f
66+
| Error ->
67+
if ED.equal env ED.bot then
68+
ED.bot
69+
else
70+
failwith "eval_stmt: Error"
71+
| _ -> failwith "TODO"
3372
end

0 commit comments

Comments
 (0)