Skip to content

Commit

Permalink
implement alias_to_mochi
Browse files Browse the repository at this point in the history
  • Loading branch information
@artoy
artoy committed Aug 3, 2023
1 parent 681da2e commit 06eb5da
Showing 1 changed file with 94 additions and 107 deletions.
201 changes: 94 additions & 107 deletions src/convMoCHi.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,22 @@ let is_builtin_fn = function
else false

module Mochi = struct
type adist = Left | Right | Niladist [@@deriving sexp]
type atype = ABase of adist | ATuple of atype list [@@deriving sexp]
(** Direction of assignment generated by alias statements *)
type adist = Left | Right | None [@@deriving sexp]

(** The value actually assigned by alias statements *)
type arhs =
| AVar of string
| AList of string list
[@@deriving sexp]

(** The expression to assign value by alias statements *)
type aexp =
| AVarExp of string list
| ATupleLhsExp of string list * string * string * aexp * string list
| ATupleRhsExp of string list * string * aexp
| AListExp of string * string * string * aexp
[@@deriving sexp]

type exp =
| Unit
Expand All @@ -47,14 +61,7 @@ module Mochi = struct
| Read of string * string
| Assert of relation * exp
| Update of string * string * string * exp
| Alias of
(* Paths.steps list は Paths と逆順 *)
string
* string
* patt
* patt
* patt
* exp
| Alias of string * aexp
| Nil
| Cons of exp * exp
| Match of string * exp * string * string * exp
Expand Down Expand Up @@ -187,6 +194,7 @@ module Mochi = struct
pf " :: ";
pp_exp t;
]
(* It is not right. We have to use monad to use variables that is defined or updated in branch *)
| Match (x, e1, h, r, e2) ->
pl [
pf "match %s with " x;
Expand Down Expand Up @@ -224,6 +232,17 @@ module Mochi = struct
pp_prog prog std_formatter
end

let pull_type ty con i =
let open OwnershipInference in
match ty with
| Ref (t, _) -> t
| Tuple ts -> List.nth ts i
| IntList ol ->
if con = "Cons" && i = 2
then Ref (IntList (List.tl ol @ [(List.hd @@ List.rev ol)]), List.hd ol)
else failwith "Only .Cons.2 is supported in paths related to recursive types in alias statement"
| _ -> assert false

let rec lhs_to_mochi (ri : OwnershipInference.Result.t) (ro : (int * float) list) i
=
let open OwnershipInference in
Expand Down Expand Up @@ -284,13 +303,11 @@ let alias_to_adist (ro : (int * float) list)
| Tuple tys -> walk (List.nth tys i) ss
| _ -> assert false)
| `Cons (s, i) :: ss ->
if s = "Cons" && i = 2 then (
match ty with
| IntList ol ->
let ty' = Ref (IntList (List.tl ol @ [(List.hd @@ List.rev ol)]), List.hd ol) in
walk ty' ss
| _ -> assert false)
else failwith "Only .Cons.2 is supported in paths related to recursive types in alias statement"
match ty with
| IntList _ ->
let ty' = pull_type ty s i in
walk ty' ss
| _ -> assert false
in
let tl = walk tl rsl in
let tr = walk tr rsr in
Expand All @@ -299,7 +316,7 @@ let alias_to_adist (ro : (int * float) list)
match (tl, tr) with
| Array (tl', o1), Array (tr', o2) | Ref (tl', o1), Ref (tr', o2) ->
let zl, zr = (map_o ro o1 = 0., map_o ro o2 = 0.) in
if zl then if zr then Niladist else Left
if zl then if zr then None else Left
else if zr then Right
else loop tl' tr'
| Tuple tsl, Tuple tsr ->
Expand All @@ -309,112 +326,85 @@ let alias_to_adist (ro : (int * float) list)
(fun (nl, nr, nn) -> function
| Left -> (nl + 1, nr, nn)
| Right -> (nl, nr + 1, nn)
| Niladist -> (nl, nr, nn + 1))
| None -> (nl, nr, nn + 1))
(0, 0, 0) adists
in
let n = List.length adists in
if nn = n then Niladist
if nn = n then None
else if nl + nn = n then Left
else if nr + nn = n then Right
else assert false
| Int, Int -> Niladist
| Int, Int -> None
| t1, _ ->
failwith
(Printf.sprintf "ill type: %s" (sexp_of_otype t1 |> string_of_sexp))
in
(rsl, rsr, loop tl tr)

let alias_to_patt (ro : (int * float) list)
let alias_to_mochi (ro : (int * float) list)
((xl, tl, sl) : string * OwnershipInference.otype * Paths.steps list)
((xr, tr, sr) : string * OwnershipInference.otype * Paths.steps list) =
((xr, tr, sr) : string * OwnershipInference.otype * Paths.steps list)
(e : Mochi.exp) : Mochi.exp =
let open OwnershipInference in
let rsl, rsr, adist = alias_to_adist ro (tl, sl) (tr, sr) in
let xd, td, sd, xs, ts, ss =
match adist with
| Left -> (xl, tl, rsl, xr, tr, rsr)
| _ -> (xr, tr, rsr, xl, tl, rsl)
in
let rec xname x = function
| [] -> x
| `Deref :: s -> xname x s
| `Proj i :: s -> xname (Printf.sprintf "%s'%i" x i) s
| `Cons _ :: _ -> assert false
let rec conv_alias_rhs xs ts rss e acc =
match rss with
| [] -> Mochi.AVarExp (List.rev (xs :: acc))
| `Deref :: ss -> (
match ts with
| Ref (_, o) ->
assert (map_o ro o > 0.);
let ty' = pull_type ts "" 0 in
conv_alias_rhs xs ty' ss e acc
| _ -> assert false)
| `Proj i :: ss -> (
match ts with
| Tuple tys ->
let xspats = List.mapi (fun j _ -> if i = j then Printf.sprintf "%s'%i" xs j else "_") tys in
let xsi = Printf.sprintf "%s'%i" xs i in
let ty' = pull_type ts "" i in
Mochi.ATupleRhsExp (xspats, xs, conv_alias_rhs xsi ty' ss e acc)
| _ -> assert false)
| `Cons (s, i) :: ss -> (
match ts with
| IntList _ ->
let ty' = pull_type ts s i in
let h = Printf.sprintf "%s'1" xs in
let t = Printf.sprintf "%s'2" xs in
Mochi.AListExp (xs, h, t, conv_alias_rhs t ty' ss e acc)
| _ -> assert false)
in
let xxd = xname xd sd in
let xxs = xname xs ss in
let rec e_patt rx x t = function
| [] -> PVar rx
| `Deref :: s -> (
match t with
let rec conv_alias xd td rsd xs ts rss e acc =
match rsd with
| [] -> conv_alias_rhs xs ts rss e acc
| `Deref :: ss -> (
match td with
| Ref (t', o) ->
assert (map_o ro o > 0.);
e_patt rx x t' s
assert (map_o ro o > 0.);
conv_alias xd t' ss xs ts rss e acc
| _ -> assert false)
| `Proj i :: s -> (
match t with
| `Proj i :: ss -> (
match td with
| Tuple tys ->
let x' = Printf.sprintf "%s'%i" x i in
PTuple
(List.mapi
(fun j ty -> if i = j then e_patt rx x' ty s else PVar x')
tys)
| _ -> assert false)
| `Cons _ :: _ -> assert false
in
let ptd = e_patt xxd xd td sd in
let pts = e_patt xxs xs ts ss in
let pt_ = e_patt xxs xd td sd in
(xd, xs, ptd, pts, pt_)
(*
let alias_to_aty (ro : (int * float) list)
((tl, sl) : OwnershipInference.otype * Paths.steps list)
((tr, sr) : OwnershipInference.otype * Paths.steps list) =
let open OwnershipInference in
let rsl = List.rev sl in
let rsr = List.rev sr in
let rec walk ty = function
| [] -> ty
| `Deref :: ss -> (
match ty with
| Ref (ty', o) ->
assert (map_o ro o > 0.);
walk ty' ss
let xdpats = List.mapi (fun j _ -> Printf.sprintf "%s'%i" xd j) tys in
let xdpats' = List.mapi (fun j _ -> Printf.sprintf (if i = j then "%s''%i" else "%s'%i") xd j) tys in
let xdi' = Printf.sprintf "%s''%i" xd i in
let ty' = pull_type td "" i in
Mochi.ATupleLhsExp (xdpats, xd, xdi', conv_alias xdi' ty' ss xs ts rss e acc, xdpats')
| _ -> assert false)
| `Proj i :: ss -> (
match ty with
| Tuple tys -> walk (List.nth tys i) ss
| `Cons (s, i) :: ss -> (
match td with
| IntList _ ->
let ty' = pull_type td s i in
let h = Printf.sprintf "%s'1" xd in
let t = Printf.sprintf "%s'2" xd in
Mochi.AListExp(xd, h, t, conv_alias t ty' ss xs ts rss e (h :: acc))
| _ -> assert false)
in
let tl = walk tl rsl in
let tr = walk tr rsr in
let open Mochi in
let rec loop tl tr =
match (tl, tr) with
| Array (tl', o1), Array (tr', o2) | Ref (tl', o1), Ref (tr', o2) ->
let zl, zr = (map_o ro o1 = 0., map_o ro o2 = 0.) in
if zl then if zr then ABase Nil else ABase Left
else if zr then ABase Right
else loop tl' tr'
| Tuple tsl, Tuple tsr ->
let atys = List.map2 loop tsl tsr in
let nl, nr, nn =
List.fold_left
(fun ((nl, nr, nn) as acc) -> function
| ABase Left -> (nl + 1, nr, nn)
| ABase Right -> (nl, nr + 1, nn)
| ABase Nil -> (nl, nr, nn + 1)
| _ -> acc)
(0, 0, 0) atys
in
let n = List.length atys in
if nl = n then ABase Left
else if nr = n then ABase Right
else if nn = n then ABase Nil
else ATuple atys
| Int, Int -> ABase Nil
| _ -> assert false
in
loop tl tr *)
let rsl, rsr, adist = alias_to_adist ro (tl, sl) (tr, sr) in
match adist with
| Left -> Mochi.Alias(xl, conv_alias xl tl rsl xr tr rsr e [])
| Right -> Mochi.Alias(xr, conv_alias xr tr rsr xl tl rsl e [])
| None -> e

let rec exp_to_mochi (ri : OwnershipInference.Result.t)
(ro : (int * float) list) (vs : string list) (((i, _), e) : exp) =
Expand Down Expand Up @@ -462,10 +452,7 @@ let rec exp_to_mochi (ri : OwnershipInference.Result.t)
let r2, st2, _ = (p2 :> root * steps list * suff) in
match (r1, r2) with
| Var x1, Var x2 ->
let xd, xs, p1, p2, p3 =
alias_to_patt ro (x1, map_ty x1, st1) (x2, map_ty x2, st2)
in
Mochi.Alias (xd, xs, p1, p2, p3, exp_to_mochi ri ro vs e)
alias_to_mochi ro (x1, map_ty x1, st1) (x2, map_ty x2, st2) (exp_to_mochi ri ro vs e)
| _ -> assert false)
| Match (e1, e2, h, t, e3) ->
match e1 with
Expand Down

0 comments on commit 06eb5da

Please sign in to comment.