Skip to content

Commit 7d9e65e

Browse files
committed
Lisa abseval
1 parent 20e320e commit 7d9e65e

File tree

4 files changed

+504
-0
lines changed

4 files changed

+504
-0
lines changed

src/abseval/abseval.ml

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
(** Abstraktne väärtustaja ehk abstraktne interpretaator. *)
2+
open Ast
3+
4+
(** Abstraktseid väärtustajaid saab luua kasutades erinevaid täisarve abstraheerivaid domeene.
5+
Vt. IntDomain. *)
6+
module Make (ID: IntDomain.S) =
7+
struct
8+
(** Väärtuskeskkonna domeen kasutades antud täisarvude domeeni. *)
9+
module ED = EnvDomain.Make (ID)
10+
11+
(** Väärtustab avaldise keskkonnas.
12+
Vihje: ID.of_int.
13+
Vihje: ID.of_interval.
14+
Vihje: ID.eval_binary. *)
15+
let rec eval_expr (env: ED.t) (expr: expr): ID.t =
16+
failwith "TODO"
17+
18+
(** Väärtustab valvuri (avaldis ja selle oodatav tõeväärtus) keskkonnas.
19+
Kui valvur on keskkonnaga vastuolus, siis tagastab saavutamatu programmi oleku ED.bot.
20+
Kui valvuriga saab keskkonna muutujate väärtusi täpsemaks kitsendada, siis võib keskkonda muuta.
21+
Võib jätta keskkonna muutmata, kuid siis ei kasutata valvurist saadavat lisainfot. *)
22+
let eval_guard (env: ED.t) (expr: expr) (branch: bool): ED.t =
23+
failwith "TODO"
24+
25+
module EDFP = Fixpoint.MakeDomain (ED)
26+
27+
(** Väärtustab lause keskkonnas.
28+
Vihje: Vea jaoks kasuta failwith funktsiooni.
29+
Vihje: eval_guard.
30+
Vihje: While jaoks kasuta püsipunkti moodulit EDFP. *)
31+
let rec eval_stmt (env: ED.t) (stmt: stmt): ED.t =
32+
failwith "TODO"
33+
end

src/abseval/dune

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
(library
2+
(name abseval)
3+
(libraries ast domain fixpoint))

0 commit comments

Comments
 (0)