Skip to content

Commit c082bb2

Browse files
sim642sim642
committed
Lisa fixpoint
1 parent 8040654 commit c082bb2

8 files changed

Lines changed: 311 additions & 0 deletions

File tree

‎src/fixpoint/dune‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
(library
2+
(name fixpoint)
3+
(preprocess (pps ppx_deriving.std)))

‎src/fixpoint/fixpoint.ml‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
(** Püsipunktid.
2+
3+
Vt. "Introduction to Compiler Design" õpikust, peatükk 1.5.1.
4+
Vt. Vesali "The Sulund Design Pattern™" slaide. *)
5+
6+
(** Püsipunktid üle suvalise võrreldava tüübi. *)
7+
module Make (D: sig type t [@@deriving eq] end) =
8+
struct
9+
(** Leiab funktsiooni püsipunkti alustades iteratsiooni antud väärtusest. *)
10+
let rec fp (f: D.t -> D.t) (x: D.t): D.t =
11+
failwith "TODO"
12+
end
13+
14+
(** Püsipunktid üle hulkade. *)
15+
module MakeSet (D: Set.S) =
16+
struct
17+
include Make (D)
18+
19+
(** Leiab funktsiooni vähima püsipunkti.
20+
Kasutada fp funktsiooni. *)
21+
let lfp (f: D.t -> D.t): D.t =
22+
failwith "TODO"
23+
24+
(** Leiab funktsiooni sulundi, mis sisaldab antud väärtusi.
25+
Kasutada lfp funktsiooni. *)
26+
let closure (f: D.t -> D.t) (initial: D.t): D.t =
27+
failwith "TODO"
28+
29+
(** Leiab agara distributiivse funktsiooni sulundi, mis sisaldab antud väärtusi.
30+
Pole vaja kasutada fp/lfp funktsiooni. *)
31+
let closure_strict_distr (f: D.t -> D.t) (initial: D.t): D.t =
32+
failwith "TODO"
33+
end

‎test/fixpoint/dune‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
(test
2+
(name fixpoint_test)
3+
(libraries ounit2 ounittodo fixpoint)
4+
(preprocess (pps ppx_deriving.std)))

‎test/fixpoint/fixpoint_test.ml‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
open OUnit2
2+
3+
let tests =
4+
"fixpoint" >::: [
5+
Transition_test.tests;
6+
Nfa_eps_test.tests;
7+
]
8+
9+
let () = run_test_tt_main (OUnitTodo.wrap tests)

‎test/fixpoint/nfa_eps_test.ml‎

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
(** Epsilonsulundi näide "Introduction to Compiler Design" õpikust, peatükk 1.5.1. *)
2+
open OUnit2
3+
open Fixpoint
4+
5+
module IntSet =
6+
struct
7+
include Set.Make (Int) (* Taaskasutame standardset hulga moodulit. *)
8+
(* Aga lisame mõne funktsiooni juurde. *)
9+
10+
let show is = [%show: int list] (elements is)
11+
end
12+
13+
(** Epsilonsammude funktsioon, joonis 1.5. *)
14+
let nfa_eps = function
15+
| 1 -> [2; 5]
16+
| 5 -> [6; 7]
17+
| 8 -> [1]
18+
| _ -> []
19+
20+
(** Epsilonsammude funktsioon hulgal. *)
21+
let nfa_eps_set states =
22+
IntSet.elements states
23+
|> List.concat_map nfa_eps
24+
|> IntSet.of_list
25+
26+
module IntSetFP = MakeSet (IntSet)
27+
28+
let assert_equal = assert_equal ~cmp:IntSet.equal ~printer:IntSet.show
29+
30+
(** Generaatorid omaduspõhiseks testimiseks. *)
31+
let arbitrary_state = QCheck.int_range 1 10
32+
let arbitrary_states = QCheck.(map ~rev:IntSet.elements IntSet.of_list (list_small arbitrary_state))
33+
34+
35+
(** Omaduspõhine test, mis kontrollib püsipunkti funktsiooni monotoonsust. *)
36+
let test_fp_f_mono =
37+
QCheck.Test.make ~name:"f_mono"
38+
(QCheck.triple arbitrary_states arbitrary_states arbitrary_states)
39+
(fun (initial, states1, states2) ->
40+
QCheck.assume (IntSet.subset states1 states2);
41+
let f x = IntSet.union initial (nfa_eps_set x) in
42+
IntSet.subset (f states1) (f states2)
43+
)
44+
|> QCheck_ounit.to_ounit2_test
45+
46+
let test_fp _ =
47+
(* Olekust 1. *)
48+
let f1 x = IntSet.union (IntSet.singleton 1) (nfa_eps_set x) in
49+
assert_equal (IntSet.of_list [1; 2; 5; 6; 7]) (IntSetFP.fp f1 IntSet.empty);
50+
(* Olekust 2. *)
51+
let f2 x = IntSet.union (IntSet.singleton 2) (nfa_eps_set x) in
52+
assert_equal (IntSet.of_list [2]) (IntSetFP.fp f2 IntSet.empty);
53+
(* Olekust 8. *)
54+
let f8 x = IntSet.union (IntSet.singleton 8) (nfa_eps_set x) in
55+
assert_equal (IntSet.of_list [1; 2; 5; 6; 7; 8]) (IntSetFP.fp f8 IntSet.empty)
56+
57+
let test_lfp _ =
58+
(* Olekust 1. *)
59+
let f1 x = IntSet.union (IntSet.singleton 1) (nfa_eps_set x) in
60+
assert_equal (IntSet.of_list [1; 2; 5; 6; 7]) (IntSetFP.lfp f1);
61+
(* Olekust 2. *)
62+
let f2 x = IntSet.union (IntSet.singleton 2) (nfa_eps_set x) in
63+
assert_equal (IntSet.of_list [2]) (IntSetFP.lfp f2);
64+
(* Olekust 8. *)
65+
let f8 x = IntSet.union (IntSet.singleton 8) (nfa_eps_set x) in
66+
assert_equal (IntSet.of_list [1; 2; 5; 6; 7; 8]) (IntSetFP.lfp f8)
67+
68+
69+
(** Omaduspõhine test, mis kontrollib sulundi funktsiooni monotoonsust. *)
70+
let test_closure_f_mono =
71+
QCheck.Test.make ~name:"f_mono"
72+
(QCheck.pair arbitrary_states arbitrary_states)
73+
(fun (states1, states2) ->
74+
QCheck.assume (IntSet.subset states1 states2);
75+
IntSet.subset (nfa_eps_set states1) (nfa_eps_set states2)
76+
)
77+
|> QCheck_ounit.to_ounit2_test
78+
79+
let test_closure _ =
80+
(* Olekust 1. *)
81+
assert_equal (IntSet.of_list [1; 2; 5; 6; 7]) (IntSetFP.closure nfa_eps_set (IntSet.singleton 1));
82+
(* Olekust 2. *)
83+
assert_equal (IntSet.of_list [2]) (IntSetFP.closure nfa_eps_set (IntSet.singleton 2));
84+
(* Olekust 8. *)
85+
assert_equal (IntSet.of_list [1; 2; 5; 6; 7; 8]) (IntSetFP.closure nfa_eps_set (IntSet.singleton 8))
86+
87+
(** Test, mis kontrollib sulundi funktsiooni agarust. *)
88+
let test_closure_f_strict _ =
89+
assert_equal IntSet.empty (nfa_eps_set IntSet.empty)
90+
91+
(** Omaduspõhine test, mis kontrollib sulundi funktsiooni distributiivsust. *)
92+
let test_closure_f_distr =
93+
QCheck.Test.make ~name:"f_distr"
94+
(QCheck.pair arbitrary_states arbitrary_states)
95+
(fun (states1, states2) ->
96+
IntSet.equal (nfa_eps_set (IntSet.union states1 states2)) (IntSet.union (nfa_eps_set states1) (nfa_eps_set states2))
97+
)
98+
|> QCheck_ounit.to_ounit2_test
99+
100+
let test_closure_strict_distr _ =
101+
(* Olekust 1. *)
102+
assert_equal (IntSet.of_list [1; 2; 5; 6; 7]) (IntSetFP.closure_strict_distr nfa_eps_set (IntSet.singleton 1));
103+
(* Olekust 2. *)
104+
assert_equal (IntSet.of_list [2]) (IntSetFP.closure_strict_distr nfa_eps_set (IntSet.singleton 2));
105+
(* Olekust 8. *)
106+
assert_equal (IntSet.of_list [1; 2; 5; 6; 7; 8]) (IntSetFP.closure_strict_distr nfa_eps_set (IntSet.singleton 8))
107+
108+
(** Omaduspõhine test, mis kontrollib kahe sulundi samaväärsust. *)
109+
let test_closure_equivalent =
110+
QCheck.Test.make ~name:"equivalent"
111+
arbitrary_states
112+
(fun initial ->
113+
IntSet.equal (IntSetFP.closure nfa_eps_set initial) (IntSetFP.closure_strict_distr nfa_eps_set initial)
114+
)
115+
|> QCheck_ounit.to_ounit2_test
116+
117+
118+
let tests =
119+
"nfa_eps" >::: [
120+
"fp" >::: [
121+
test_fp_f_mono;
122+
"fp" >:: test_fp;
123+
"lfp" >:: test_lfp;
124+
];
125+
"closure" >::: [
126+
test_closure_f_mono;
127+
"closure" >:: test_closure;
128+
"f_strict" >:: test_closure_f_strict;
129+
test_closure_f_distr;
130+
"closure_strict_distr" >:: test_closure_strict_distr;
131+
test_closure_equivalent;
132+
];
133+
]

‎test/fixpoint/nfa_eps_test.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
val tests: OUnit2.test

‎test/fixpoint/transition_test.ml‎

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
(** Transitiivse sulundi näide Vesali "The Sulund Design Pattern™" slaididelt. *)
2+
open OUnit2
3+
open Fixpoint
4+
5+
module Transition =
6+
struct
7+
type t = int * string * int [@@deriving ord, show]
8+
end
9+
10+
module TransitionSet =
11+
struct
12+
include Set.Make (Transition) (* Taaskasutame standardset hulga moodulit. *)
13+
(* Aga lisame mõne funktsiooni juurde. *)
14+
15+
(** Relatsioonide kompositsioon. *)
16+
let compose rel1 rel2 =
17+
fold (fun (s1, l1, t1) acc ->
18+
fold (fun (s2, l2, t2) acc ->
19+
if t1 = s2 then
20+
add (s1, l1 ^ l2, t2) acc
21+
else
22+
acc
23+
) rel2 acc
24+
) rel1 empty
25+
26+
let show ts = [%show: Transition.t list] (elements ts)
27+
end
28+
29+
(** Algne relatsioon. *)
30+
let initial = TransitionSet.of_list [
31+
(0, "a", 1);
32+
(1, "b", 2);
33+
(1, "c", 3);
34+
(3, "d", 4);
35+
]
36+
37+
(** Oodatav transitiivne sulund. *)
38+
let expected = TransitionSet.of_list [
39+
(0, "a", 1);
40+
(1, "b", 2);
41+
(1, "c", 3);
42+
(3, "d", 4);
43+
(0, "ab", 2);
44+
(0, "ac", 3);
45+
(1, "cd", 4);
46+
(0, "acd", 4);
47+
]
48+
49+
module TransitionSetFP = MakeSet (TransitionSet)
50+
51+
let assert_equal = assert_equal ~cmp:TransitionSet.equal ~printer:TransitionSet.show
52+
53+
(** Generaatorid omaduspõhiseks testimiseks. *)
54+
let arbitrary_state = QCheck.int_range 0 6
55+
let arbitrary_label = QCheck.(string_small_of (Gen.oneof_list ['a'; 'b'; 'c'; 'd'; 'e'; 'f']))
56+
let arbitrary_transition = QCheck.triple arbitrary_state arbitrary_label arbitrary_state
57+
let arbitrary_ts = QCheck.(map ~rev:TransitionSet.elements TransitionSet.of_list (list_small arbitrary_transition))
58+
59+
60+
(** Püsipunkti funktsioon. *)
61+
let f ts = TransitionSet.union initial (TransitionSet.compose ts initial)
62+
63+
(** Omaduspõhine test, mis kontrollib püsipunkti funktsiooni monotoonsust. *)
64+
let test_fp_f_mono =
65+
QCheck.Test.make ~name:"f_mono"
66+
(QCheck.pair arbitrary_ts arbitrary_ts)
67+
(fun (ts1, ts2) ->
68+
QCheck.assume (TransitionSet.subset ts1 ts2);
69+
TransitionSet.subset (f ts1) (f ts2)
70+
)
71+
|> QCheck_ounit.to_ounit2_test
72+
73+
let test_fp _ =
74+
assert_equal expected (TransitionSetFP.fp f TransitionSet.empty)
75+
76+
let test_lfp _ =
77+
assert_equal expected (TransitionSetFP.lfp f)
78+
79+
80+
(** Sulundi funktsioon. *)
81+
let f ts = TransitionSet.compose ts initial
82+
83+
(** Omaduspõhine test, mis kontrollib sulundi funktsiooni monotoonsust. *)
84+
let test_closure_f_mono =
85+
QCheck.Test.make ~name:"f_mono"
86+
(QCheck.pair arbitrary_ts arbitrary_ts)
87+
(fun (ts1, ts2) ->
88+
QCheck.assume (TransitionSet.subset ts1 ts2);
89+
TransitionSet.subset (f ts1) (f ts2)
90+
)
91+
|> QCheck_ounit.to_ounit2_test
92+
93+
let test_closure _ =
94+
assert_equal expected (TransitionSetFP.closure f initial)
95+
96+
(** Test, mis kontrollib sulundi funktsiooni agarust. *)
97+
let test_closure_f_strict _ =
98+
assert_equal TransitionSet.empty (f TransitionSet.empty)
99+
100+
(** Omaduspõhine test, mis kontrollib sulundi funktsiooni distributiivsust. *)
101+
let test_closure_f_distr =
102+
QCheck.Test.make ~name:"f_distr"
103+
(QCheck.pair arbitrary_ts arbitrary_ts)
104+
(fun (ts1, ts2) ->
105+
TransitionSet.equal (f (TransitionSet.union ts1 ts2)) (TransitionSet.union (f ts1) (f ts2))
106+
)
107+
|> QCheck_ounit.to_ounit2_test
108+
109+
let test_closure_strict_distr _ =
110+
assert_equal expected (TransitionSetFP.closure_strict_distr f initial)
111+
112+
113+
let tests =
114+
"transition" >::: [
115+
"fp" >::: [
116+
test_fp_f_mono;
117+
"fp" >:: test_fp;
118+
"lfp" >:: test_lfp;
119+
];
120+
"closure" >::: [
121+
test_closure_f_mono;
122+
"closure" >:: test_closure;
123+
"f_strict" >:: test_closure_f_strict;
124+
test_closure_f_distr;
125+
"closure_strict_distr" >:: test_closure_strict_distr;
126+
];
127+
]

‎test/fixpoint/transition_test.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
val tests: OUnit2.test

0 commit comments

Comments
 (0)