From f4c08beedf54f57ba9b930e2d8952a90646b33e6 Mon Sep 17 00:00:00 2001 From: y-tak6 Date: Sun, 12 May 2024 20:48:07 +0900 Subject: [PATCH] a-normalize(anormal_ir.ml) of ifthenelse with adding some comments --- src/anormal.ml | 7 +++++-- src/anormal_ir.ml | 18 +++++++++++++++++- src/normalized_ir_ast.ml | 8 +++++--- src/normalized_ir_ast.mli | 3 ++- 4 files changed, 29 insertions(+), 7 deletions(-) diff --git a/src/anormal.ml b/src/anormal.ml index dd1ebdc..f4635b2 100644 --- a/src/anormal.ml +++ b/src/anormal.ml @@ -35,6 +35,7 @@ let rename_cexp rename e mut = let mut = application_mut mut f in (AApp (f, rename_avals rename args, t), mut) | ATuple el -> (ATuple (rename_avals rename el), mut) + | AIf _ -> assert false | _ -> (e, mut) let cexp_to_exp e = @@ -51,6 +52,7 @@ let cexp_to_exp e = let res_var = Utils.fresh_var () in Letin ([ res_var ], LApp (f, args), Rexp (RVal (Var res_var)))) | ATuple el -> Rexp (RTuple el) + | AIf _ -> assert false let rec remove_tuple rename e mut = match e with @@ -77,8 +79,9 @@ let rec remove_tuple rename e mut = in (gen_tuple_let (vars, el), mut) | AVal arg -> (Letin (vars, LVal arg, e2'), mut) - | AApp (f, args, _) -> (Letin (vars, LApp (f, args), e2'), mut)) - + | AApp (f, args, _) -> (Letin (vars, LApp (f, args), e2'), mut) + | AIf _ -> assert false) + let normalize { name = func_name; arg_pats = args; body; mutability = mut } = let renames, args = List.fold_left diff --git a/src/anormal_ir.ml b/src/anormal_ir.ml index 387775a..84e11ed 100644 --- a/src/anormal_ir.ml +++ b/src/anormal_ir.ml @@ -19,6 +19,7 @@ let get_bop s = else if s = "/" then SDiv else assert false +(* operation functions made usable especially, such as replace caller*) let pdot_to_aval p s = match p with | Path.Pdot (Path.Pident id, "Hashtbl") -> @@ -33,7 +34,9 @@ let pdot_to_aval p s = else assert false | _ -> assert false -let rec normalize_aux p { exp_desc = e; exp_type = t; _ } k = + (* The first argument p is a storage. To check whether the storage changes, it is needed. + The last argument k is a continue. A first argument of k is hole, and a first element of a return value is AST with the hole.*) +let rec normalize_aux p { exp_desc = e; exp_type = t; _ } k :aexp * bool= match e with | Texp_ident (Pident s, _, _) -> (AVal (Var (Ident.unique_name s)), t, false) |> k @@ -98,8 +101,18 @@ let rec normalize_aux p { exp_desc = e; exp_type = t; _ } k = normalize_aux None e1 (fun (e1', _, _) -> let e, non_update_stor = normalize_aux p e2 k in (ALetin ((vars, rename), e1', e), non_update_stor)) + | Texp_ifthenelse (e1, e2, e3) -> + let a, b = normalize_aux p e2 (fun (x, _, b) -> (ACexp x, b)) in + let e3' = match e3 with Some e -> e | _ -> assert false in + let a2, b2 = normalize_aux p e3' (fun (x, _, b) -> (ACexp x, b)) in + normalize_name e1 (fun x -> k (AIf(x, a, a2), t, b && b2 )) | _ -> assert false + (* | A.If(e1,e2,e3) -> + normalize_name e1 (fun x -> + k (A.If(x, normalize e2 id, normalize e3 id))) *) + +(* when a new variable is needed *) and normalize_name e k = normalize_aux None e (fun (e', t, _) -> match e' with @@ -112,6 +125,9 @@ and normalize_name e k = (ALetin (([ var ], [ (var, xs) ]), e', e), non_update_stor) | None -> (ALetin (([ var ], []), e', e), non_update_stor))) + +(* because a second argument is a storage and we have to check whether it is possible to change (for nonpayable/view), + the storage argument is distinct as stor_pat*) let rec expand_function_decl n stor_pat e = match e with | { diff --git a/src/normalized_ir_ast.ml b/src/normalized_ir_ast.ml index 4efe269..fbd61dc 100644 --- a/src/normalized_ir_ast.ml +++ b/src/normalized_ir_ast.ml @@ -4,8 +4,9 @@ type acexp = | AVal of value | AApp of (value * value list * Types.type_expr) | ATuple of value list + | AIf of value * aexp * aexp -type aexp = +and aexp = | ACexp of acexp | ASeq of acexp * aexp | ALetin of (string list * (string * string list) list) * acexp * aexp @@ -17,7 +18,7 @@ type adecl = { mutability : Abi.state_mutability; } -let string_of_acexp = function +let rec string_of_acexp = function | AVal v -> string_of_value v | AApp (f, args, _) -> string_of_value f @@ -26,8 +27,9 @@ let string_of_acexp = function "(" ^ List.fold_left (fun acc x -> acc ^ ", " ^ string_of_value x) "" vs ^ ")" + | AIf (e1, e2, e3) -> "if " ^ string_of_value e1 ^ " then " ^ string_of_aexp e2 ^ " else " ^ string_of_aexp e3 -let rec string_of_aexp = function +and string_of_aexp = function | ACexp e -> string_of_acexp e | ASeq (e1, e2) -> string_of_acexp e1 ^ "; " ^ string_of_aexp e2 | ALetin ((xs, _), e1, e2) -> diff --git a/src/normalized_ir_ast.mli b/src/normalized_ir_ast.mli index 5c6d657..c1a8e91 100644 --- a/src/normalized_ir_ast.mli +++ b/src/normalized_ir_ast.mli @@ -5,9 +5,10 @@ type acexp = | AVal of value | AApp of (value * value list * Types.type_expr) | ATuple of value list + | AIf of value * aexp * aexp (** computation expressions *) -type aexp = +and aexp = | ACexp of acexp | ASeq of acexp * aexp | ALetin of (string list * (string * string list) list) * acexp * aexp