Skip to content

Commit

Permalink
Basic JS Conversion (#3)
Browse files Browse the repository at this point in the history
* ✨ Basic features of convert function

* ✨ Add export statements, remove unnecessary names for binding

* Add js mem

* Add update without set test

* Add js array expression conversion

* Add js syntax conversion tests

* Add more js conversion tests

* Add more conversion

* Add string

* Update &&, ||, ?? conversion

* Add alpha conversion in test

* - Remove T.memory
- Rename Loc to Addr
- Add exceptions
  • Loading branch information
joongwon authored Sep 23, 2024
1 parent ffb6300 commit 920f097
Show file tree
Hide file tree
Showing 12 changed files with 1,176 additions and 61 deletions.
6 changes: 4 additions & 2 deletions bin/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -58,9 +58,11 @@ let () =
in
Arg.parse speclist (fun x -> filename := x) usage_msg;
if String.is_empty !filename then Arg.usage speclist usage_msg
else if !opt_parse_js then
else if !opt_parse_js then (
let js_syntax, _ = Js_syntax.parse !filename in
print_endline (Js_syntax.show js_syntax)
print_endline (Js_syntax.show js_syntax);
let prog = Js_syntax.convert js_syntax in
Sexp.pp_hum Stdlib.Format.std_formatter (Syntax.Prog.sexp_of_t prog))
else (
Fmt_tty.setup_std_outputs ();
Logs.set_reporter (Logs_fmt.reporter ());
Expand Down
31 changes: 31 additions & 0 deletions lib/concrete_domains.ml
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ module M : Domains.S = struct
module rec T : (Domains.T with type path = int) = struct
type path = Path.t [@@deriving sexp_of]
type env = Env.t [@@deriving sexp_of]
type addr = Addr.t [@@deriving sexp_of]
type obj = Obj.t [@@deriving sexp_of]
type st_store = St_store.t [@@deriving sexp_of]
type job_q = Job_q.t [@@deriving sexp_of]

Expand All @@ -15,6 +17,8 @@ module M : Domains.S = struct
| 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
Expand Down Expand Up @@ -59,6 +63,29 @@ module M : Domains.S = struct
let extend env ~id ~value = Map.set env ~key:id ~data:value
end

and Addr : (Domains.Addr with type t = T.addr) = Int

and Obj : (Domains.Obj with type value = T.value and type t = T.obj) = struct
type value = T.value [@@deriving sexp_of]
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 update obj ~field ~value = Map.set obj ~key:field ~data:value
end

and Memory : (Domains.Memory with type obj = T.obj and type addr = T.addr) =
struct
type obj = T.obj [@@deriving sexp_of]
type addr = T.addr [@@deriving sexp_of]
type t = obj Map.M(Addr).t [@@deriving sexp_of]

let empty = Map.empty (module Addr)
let alloc = Map.length
let lookup memory ~addr = Map.find_exn memory addr
let update memory ~addr ~obj = Map.set memory ~key:addr ~data:obj
end

and St_store :
(Domains.St_store
with type value = T.value
Expand Down Expand Up @@ -149,10 +176,13 @@ module M : Domains.S = struct
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
Expand All @@ -168,6 +198,7 @@ module M : Domains.S = struct
| 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
Expand Down
46 changes: 46 additions & 0 deletions lib/domains.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ open Syntax
module type T = sig
type path
type env
type addr
type obj
type st_store
type job_q
type clos = { param : Id.t; body : Expr.hook_free_t; env : env }
Expand All @@ -14,6 +16,8 @@ module type T = sig
| 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
Expand Down Expand Up @@ -49,6 +53,8 @@ module type T = sig
val sexp_of_part_view : part_view -> Sexp.t
val sexp_of_tree : tree -> Sexp.t
val sexp_of_entry : entry -> Sexp.t
val sexp_of_addr : addr -> Sexp.t
val sexp_of_obj : obj -> Sexp.t
end

module type Path = sig
Expand All @@ -72,6 +78,39 @@ module type Env = sig
val sexp_of_t : t -> Sexp.t
end

module type Addr = sig
type t
type comparator_witness

val comparator : (t, comparator_witness) Comparator.t
val sexp_of_t : t -> Sexp.t
val equal : t -> t -> bool
val ( = ) : t -> t -> bool
val ( <> ) : t -> t -> bool
end

module type Obj = sig
type value
type t

val empty : t
val lookup : t -> field:Id.t -> value
val update : t -> field:Id.t -> value:value -> t
val sexp_of_t : t -> Sexp.t
end

module type Memory = sig
type obj
type addr
type t

val empty : t
val alloc : t -> addr
val lookup : t -> addr:addr -> obj
val update : t -> addr:addr -> obj:obj -> t
val sexp_of_t : t -> Sexp.t
end

module type St_store = sig
type value
type job_q
Expand Down Expand Up @@ -110,10 +149,13 @@ 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
Expand Down Expand Up @@ -143,6 +185,9 @@ module type S = sig
include T
module Path : Path with type t = path
module Env : Env with type value = value and type t = env
module Addr : Addr with type t = addr
module Obj : Obj with type value = value and type t = obj
module Memory : Memory with type obj = obj and type addr = addr

module St_store :
St_store
Expand All @@ -166,6 +211,7 @@ module type S = sig
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
Expand Down
122 changes: 88 additions & 34 deletions lib/interp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -16,15 +16,21 @@ type _ Stdlib.Effect.t +=
| Rd_env : Env.t t
| In_env : Env.t -> (('b -> 'a) -> 'b -> 'a) t

(* memory effects in eval/eval_mult *)
(* memory effects *)
type _ Stdlib.Effect.t +=
| Alloc_addr : obj -> Addr.t t
| Lookup_addr : Addr.t -> obj t
| Update_addr : Addr.t * obj -> unit t

(* tree memory effects in eval/eval_mult *)
type _ Stdlib.Effect.t +=
| Lookup_st : Path.t * Label.t -> (value * Job_q.t) t
| Update_st : (Path.t * Label.t * (value * Job_q.t)) -> unit t
| Get_dec : Path.t -> decision t
| Set_dec : Path.t * decision -> unit t
| Enq_eff : Path.t * clos -> unit t

(* memory effects in render *)
(* tree memory effects in render *)
type _ Stdlib.Effect.t +=
| Alloc_pt : Path.t t
| Lookup_ent : Path.t -> entry t
Expand Down Expand Up @@ -102,51 +108,82 @@ let mem_h =
Logger.mem mem `Ret;
(v, mem));
exnc = raise;
effc =
(fun (type a) (eff : a t) ->
match eff with
| Alloc_addr obj ->
Some
(fun (k : (a, _) continuation) ~(mem : Memory.t) ->
Logger.mem mem `Alloc_addr;
let addr = Memory.alloc mem in
let mem = Memory.update mem ~addr ~obj in
continue k addr ~mem)
| Lookup_addr addr ->
Some
(fun (k : (a, _) continuation) ~(mem : Memory.t) ->
Logger.mem mem (`Lookup_addr addr);
continue k (Memory.lookup mem ~addr) ~mem)
| Update_addr (addr, v) ->
Some
(fun (k : (a, _) continuation) ~(mem : Memory.t) ->
Logger.mem mem (`Update_addr (addr, v));
continue k () ~mem:(Memory.update mem ~addr ~obj:v))
| _ -> None);
}

let treemem_h =
{
retc =
(fun v ~treemem ->
Logger.treemem treemem `Ret;
(v, treemem));
exnc = raise;
effc =
(fun (type a) (eff : a t) ->
match eff with
(* in eval *)
| Lookup_st (path, label) ->
Some
(fun (k : (a, _) continuation) ~(mem : Tree_mem.t) ->
Logger.mem mem (`Lookup_st (path, label));
continue k (Tree_mem.lookup_st mem ~path ~label) ~mem)
(fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) ->
Logger.treemem treemem (`Lookup_st (path, label));
continue k (Tree_mem.lookup_st treemem ~path ~label) ~treemem)
| Update_st (path, label, (v, q)) ->
Some
(fun (k : (a, _) continuation) ~(mem : Tree_mem.t) ->
Logger.mem mem (`Update_st (path, label, (v, q)));
continue k () ~mem:(Tree_mem.update_st mem ~path ~label (v, q)))
(fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) ->
Logger.treemem treemem (`Update_st (path, label, (v, q)));
continue k ()
~treemem:(Tree_mem.update_st treemem ~path ~label (v, q)))
| Get_dec path ->
Some
(fun (k : (a, _) continuation) ~(mem : Tree_mem.t) ->
Logger.mem mem (`Get_dec path);
continue k (Tree_mem.get_dec mem ~path) ~mem)
(fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) ->
Logger.treemem treemem (`Get_dec path);
continue k (Tree_mem.get_dec treemem ~path) ~treemem)
| Set_dec (path, dec) ->
Some
(fun (k : (a, _) continuation) ~(mem : Tree_mem.t) ->
Logger.mem mem (`Set_dec (path, dec));
continue k () ~mem:(Tree_mem.set_dec mem ~path dec))
(fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) ->
Logger.treemem treemem (`Set_dec (path, dec));
continue k () ~treemem:(Tree_mem.set_dec treemem ~path dec))
| Enq_eff (path, clos) ->
Some
(fun (k : (a, _) continuation) ~(mem : Tree_mem.t) ->
Logger.mem mem (`Enq_eff (path, clos));
continue k () ~mem:(Tree_mem.enq_eff mem ~path clos))
(fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) ->
Logger.treemem treemem (`Enq_eff (path, clos));
continue k () ~treemem:(Tree_mem.enq_eff treemem ~path clos))
(* in render *)
| Alloc_pt ->
Some
(fun (k : (a, _) continuation) ~(mem : Tree_mem.t) ->
Logger.mem mem `Alloc_pt;
continue k (Tree_mem.alloc_pt mem) ~mem)
(fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) ->
Logger.treemem treemem `Alloc_pt;
continue k (Tree_mem.alloc_pt treemem) ~treemem)
| Lookup_ent path ->
Some
(fun (k : (a, _) continuation) ~(mem : Tree_mem.t) ->
Logger.mem mem (`Lookup_ent path);
continue k (Tree_mem.lookup_ent mem ~path) ~mem)
(fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) ->
Logger.treemem treemem (`Lookup_ent path);
continue k (Tree_mem.lookup_ent treemem ~path) ~treemem)
| Update_ent (path, ent) ->
Some
(fun (k : (a, _) continuation) ~(mem : Tree_mem.t) ->
Logger.mem mem (`Update_ent (path, ent));
continue k () ~mem:(Tree_mem.update_ent mem ~path ent))
(fun (k : (a, _) continuation) ~(treemem : Tree_mem.t) ->
Logger.treemem treemem (`Update_ent (path, ent));
continue k () ~treemem:(Tree_mem.update_ent treemem ~path ent))
| _ -> None);
}

Expand All @@ -155,6 +192,8 @@ let value_exn exn v =

let int_of_value_exn v = v |> Value.to_int |> value_exn Type_error
let bool_of_value_exn v = v |> Value.to_bool |> value_exn Type_error
let string_of_value_exn v = v |> Value.to_string |> value_exn Type_error
let addr_of_value_exn v = v |> Value.to_addr |> value_exn Type_error
let vs_of_value_exn v = v |> Value.to_vs |> value_exn Type_error
let vss_of_value_exn v = v |> Value.to_vss |> value_exn Type_error
let clos_of_value_exn v = v |> Value.to_clos |> value_exn Type_error
Expand Down Expand Up @@ -256,6 +295,7 @@ let rec eval : type a. a Expr.t -> value =
| Const Unit -> Unit
| Const (Bool b) -> Bool b
| Const (Int i) -> Int i
| Const (String s) -> String s
| Var id ->
let env = perform Rd_env in
Env.lookup_exn env ~id
Expand Down Expand Up @@ -361,6 +401,22 @@ let rec eval : type a. a Expr.t -> value =
| Minus, Int i1, Int i2 -> Int (i1 - i2)
| Times, Int i1, Int i2 -> Int (i1 * i2)
| _, _, _ -> raise Type_error)
| Alloc ->
let addr = perform (Alloc_addr Obj.empty) in
Addr addr
| Get { obj; idx } ->
let addr = eval obj |> addr_of_value_exn in
let i = eval idx |> string_of_value_exn in
let obj = perform (Lookup_addr addr) in
Obj.lookup obj ~field:i
| Set { obj; idx; value } ->
let addr = eval obj |> addr_of_value_exn in
let i = eval idx |> string_of_value_exn in
let old_obj = perform (Lookup_addr addr) in
let value = eval value in
let new_obj = Obj.update old_obj ~field:i ~value in
perform (Update_addr (addr, new_obj));
Unit

let rec eval_mult : type a. ?re_render:int -> a Expr.t -> value =
fun ?(re_render = 1) expr ->
Expand Down Expand Up @@ -548,7 +604,7 @@ let step_path (path : Path.t) : bool =

has_updates

type run_info = { steps : int; mem : Tree_mem.t }
type run_info = { steps : int; mem : Memory.t; treemem : Tree_mem.t }

let run ?(fuel : int option) ?(report : bool = false) (prog : Prog.t) : run_info
=
Expand All @@ -568,10 +624,8 @@ let run ?(fuel : int option) ?(report : bool = false) (prog : Prog.t) : run_info
loop ();
!cnt
in

let steps, mem =
match_with
(fun () -> try_with driver () (Report_box.log_h report))
() mem_h ~mem:Tree_mem.empty
in
{ steps; mem }
let driver () = match_with driver () mem_h ~mem:Memory.empty in
let driver () = match_with driver () treemem_h ~treemem:Tree_mem.empty in
let driver () = try_with driver () (Report_box.log_h report) in
let (steps, mem), treemem = driver () in
{ steps; mem; treemem }
Loading

0 comments on commit 920f097

Please sign in to comment.