Skip to content

Commit 6656cb6

Browse files
committed
Täienda fixpoint
1 parent b9a63b1 commit 6656cb6

2 files changed

Lines changed: 15 additions & 0 deletions

File tree

src/fixpoint/dune

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
(library
22
(name fixpoint)
3+
(libraries domain)
34
(preprocess (pps ppx_deriving.std)))

src/fixpoint/fixpoint.ml

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,3 +31,17 @@ struct
3131
let closure_strict_distr (f: D.t -> D.t) (initial: D.t): D.t =
3232
failwith "TODO"
3333
end
34+
35+
(** Püsipunktid üle domeenide. *)
36+
module MakeDomain (D: Domain.S) =
37+
struct
38+
include Make (D)
39+
40+
(** Leiab funktsiooni vähima püsipunkti. *)
41+
let lfp (f: D.t -> D.t): D.t =
42+
fp f D.bot
43+
44+
(** Leiab funktsiooni sulundi, mis sisaldab antud domeeni elementi. *)
45+
let closure (f: D.t -> D.t) (initial: D.t): D.t =
46+
lfp (fun x -> D.join initial (f x))
47+
end

0 commit comments

Comments
 (0)