Skip to content

✨ feat/collecting interp #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 4 commits into
base: main
Choose a base branch
from
Draft

✨ feat/collecting interp #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9d150a6
:sparkles: Rename View_spec -> View_specs
Zeta611 Sep 23, 2024
2f7dc0b
:recycle: Refactor eval
Zeta611 Sep 24, 2024
ec03cb5
:recycle: Make the value type abstract
Zeta611 Sep 26, 2024
a914d15
:fire: Remove the unused Value module
Zeta611 Sep 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
109 changes: 75 additions & 34 deletions lib/concrete_domains.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ module M : Domains.S = struct
| Int of int
| String of string
| Addr of addr
| View_spec of view_spec list
| View_specs of view_spec list
| Clos of clos
| Set_clos of set_clos
| Comp_clos of comp_clos
Expand Down Expand Up @@ -50,6 +50,76 @@ module M : Domains.S = struct

type entry = { part_view : part_view; children : tree Snoc_list.t }
[@@deriving sexp_of]

(* constructors *)
let unit () = Unit
let bool b = Bool b
let int i = Int i
let string s = String s
let addr a = Addr a
let view_specs vss = View_specs vss
let clos c = Clos c
let set_clos sc = Set_clos sc
let comp_clos cc = Comp_clos cc
let comp_spec cs = Comp_spec cs

(* coercions *)
let to_unit = function Unit -> Some () | _ -> None
let to_bool = function Bool b -> Some b | _ -> None
let to_int = function Int i -> Some i | _ -> None
let to_string = function String s -> Some s | _ -> None
let to_addr = function Addr l -> Some l | _ -> None

let to_view_spec = function
| Unit -> Some Vs_null
| Int i -> Some (Vs_int i)
| Comp_spec t -> Some (Vs_comp t)
| _ -> None

let to_view_specs = function View_specs vss -> Some vss | _ -> None
let to_clos = function Clos c -> Some c | _ -> None
let to_comp_clos = function Comp_clos c -> Some c | _ -> None
let to_set_clos = function Set_clos c -> Some c | _ -> None

(* comparison *)
(* TODO: may not be comparable, so should be bool option *)
let equal v1 v2 =
match (v1, v2) with
| Unit, Unit -> true
| Bool b1, Bool b2 -> Bool.(b1 = b2)
| Int i1, Int i2 -> i1 = i2
| Addr l1, Addr l2 -> Addr.(l1 = l2)
| _, _ -> false

let ( = ) = equal
let ( <> ) v1 v2 = not (v1 = v2)

(* primitive operations *)
let uop op v =
match (op, v) with
| Expr.Not, Bool b -> Some (Bool (not b))
| Uplus, Int i -> Some (Int i)
| Uminus, Int i -> Some (Int ~-i)
| _, _ -> None

let bop op v1 v2 =
match (op, v1, v2) with
| Expr.Eq, Unit, Unit -> Some (Bool true)
| Eq, Bool b1, Bool b2 -> Some (Bool Bool.(b1 = b2))
| Eq, Int i1, Int i2 -> Some (Bool Int.(i1 = i2))
| Lt, Int i1, Int i2 -> Some (Bool Int.(i1 < i2))
| Gt, Int i1, Int i2 -> Some (Bool Int.(i1 > i2))
| Le, Int i1, Int i2 -> Some (Bool Int.(i1 <= i2))
| Ge, Int i1, Int i2 -> Some (Bool Int.(i1 >= i2))
| Ne, Unit, Unit -> Some (Bool false)
| Ne, Bool b1, Bool b2 -> Some (Bool Bool.(b1 <> b2))
| Ne, Int i1, Int i2 -> Some (Bool Int.(i1 <> i2))
| And, Bool b1, Bool b2 -> Some (Bool (b1 && b2))
| Or, Bool b1, Bool b2 -> Some (Bool (b1 || b2))
| Plus, Int i1, Int i2 -> Some (Int (i1 + i2))
| Minus, Int i1, Int i2 -> Some (Int (i1 - i2))
| Times, Int i1, Int i2 -> Some (Int (i1 * i2))
| _, _, _ -> None
end

and Path : (Domains.Path with type t = T.path) = Int
Expand All @@ -70,7 +140,10 @@ module M : Domains.S = struct
type t = value Id.Map.t [@@deriving sexp_of]

let empty = Id.Map.empty
let lookup obj ~field = Map.find obj field |> Option.value ~default:T.Unit

let lookup obj ~field =
Map.find obj field |> Option.value ~default:(T.unit ())

let update obj ~field ~value = Map.set obj ~key:field ~data:value
end

Expand Down Expand Up @@ -173,38 +246,6 @@ module M : Domains.S = struct

include T

module Value = struct
type nonrec view_spec = view_spec
type nonrec clos = clos
type nonrec addr = addr
type t = value

let to_bool = function Bool b -> Some b | _ -> None
let to_int = function Int i -> Some i | _ -> None
let to_string = function String s -> Some s | _ -> None
let to_addr = function Addr l -> Some l | _ -> None

let to_vs = function
| Unit -> Some Vs_null
| Int i -> Some (Vs_int i)
| Comp_spec t -> Some (Vs_comp t)
| _ -> None

let to_vss = function View_spec vss -> Some vss | _ -> None
let to_clos = function Clos c -> Some c | _ -> None

let equal v1 v2 =
match (v1, v2) with
| Unit, Unit -> true
| Bool b1, Bool b2 -> Bool.(b1 = b2)
| Int i1, Int i2 -> i1 = i2
| Addr l1, Addr l2 -> Addr.(l1 = l2)
| _, _ -> false

let ( = ) = equal
let ( <> ) v1 v2 = not (v1 = v2)
end

module Phase = struct
type t = phase = P_init | P_update | P_retry | P_effect [@@deriving equal]

Expand Down
79 changes: 38 additions & 41 deletions lib/domains.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,22 +11,9 @@ module type T = sig
type clos = { param : Id.t; body : Expr.hook_free_t; env : env }
type set_clos = { label : Label.t; path : path }
type comp_clos = { comp : Prog.comp; env : env }

type value =
| Unit
| Bool of bool
| Int of int
| String of string
| Addr of addr
| View_spec of view_spec list
| Clos of clos
| Set_clos of set_clos
| Comp_clos of comp_clos
| Comp_spec of comp_spec

and comp_spec = { comp : Prog.comp; env : env; arg : value }
and view_spec = Vs_null | Vs_int of int | Vs_comp of comp_spec

type value
type comp_spec = { comp : Prog.comp; env : env; arg : value }
type view_spec = Vs_null | Vs_int of int | Vs_comp of comp_spec
type phase = P_init | P_update | P_retry | P_effect
type decision = Idle | Retry | Update

Expand All @@ -42,6 +29,41 @@ module type T = sig
type tree = Leaf_null | Leaf_int of int | Path of path
type entry = { part_view : part_view; children : tree Snoc_list.t }

(* constructors *)
val unit : unit -> value
val bool : bool -> value
val int : int -> value
val string : string -> value
val addr : addr -> value
val view_specs : view_spec list -> value
val clos : clos -> value
val set_clos : set_clos -> value
val comp_clos : comp_clos -> value
val comp_spec : comp_spec -> value

(* coercions *)
val to_unit : value -> unit option
val to_bool : value -> bool option
val to_int : value -> int option
val to_string : value -> string option
val to_addr : value -> addr option
val to_view_spec : value -> view_spec option
val to_view_specs : value -> view_spec list option
val to_clos : value -> clos option
val to_comp_clos : value -> comp_clos option
val to_set_clos : value -> set_clos option

(* comparison *)
(* TODO: may not be comparable, so should be bool option *)
val equal : value -> value -> bool
val ( = ) : value -> value -> bool
val ( <> ) : value -> value -> bool

(* primitive operations *)
val uop : Expr.uop -> value -> value option
val bop : Expr.bop -> value -> value -> value option

(* sexp_of *)
val sexp_of_clos : clos -> Sexp.t
val sexp_of_set_clos : set_clos -> Sexp.t
val sexp_of_comp_clos : comp_clos -> Sexp.t
Expand Down Expand Up @@ -146,24 +168,6 @@ module type Tree_mem = sig
val sexp_of_t : t -> Sexp.t
end

module type Value = sig
type view_spec
type clos
type addr
type t

val to_bool : t -> bool option
val to_int : t -> int option
val to_string : t -> string option
val to_addr : t -> addr option
val to_vs : t -> view_spec option
val to_vss : t -> view_spec list option
val to_clos : t -> clos option
val equal : t -> t -> bool
val ( = ) : t -> t -> bool
val ( <> ) : t -> t -> bool
end

module type Phase = sig
type t

Expand Down Expand Up @@ -206,13 +210,6 @@ module type S = sig
and type clos = clos
and type entry = entry

module Value :
Value
with type view_spec = view_spec
and type clos = clos
and type t = value
and type addr = addr

module Phase : Phase with type t = phase
module Decision : Decision with type t = decision
end
Loading