diff options
| -rw-r--r-- | src/PrintPure.ml | 77 |
1 files changed, 74 insertions, 3 deletions
diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 499c16cb..54c2bedf 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -64,6 +64,8 @@ let option_to_string = Print.option_to_string let type_var_to_string = Print.Types.type_var_to_string +let integer_type_to_string = Print.Types.integer_type_to_string + let scalar_value_to_string = Print.Values.scalar_value_to_string (* TODO: there is a bit of duplication with Print.fun_def_to_ast_formatter. @@ -129,7 +131,7 @@ let rec ty_to_string (fmt : type_formatter) (ty : ty) : string = | TypeVar tv -> fmt.type_var_id_to_string tv | Bool -> "bool" | Char -> "char" - | Integer int_ty -> Print.Types.integer_type_to_string int_ty + | Integer int_ty -> integer_type_to_string int_ty | Str -> "str" | Array aty -> "[" ^ ty_to_string fmt aty ^ "; ?]" | Slice sty -> "[" ^ ty_to_string fmt sty ^ "]" @@ -261,7 +263,10 @@ let fun_sig_to_string (fmt : ast_formatter) (sg : fun_sig) : string = let outputs = List.map (ty_to_string ty_fmt) sg.outputs in let outputs = match outputs with - | [] -> "()" + | [] -> + (* Can happen with backward functions which don't give back + * anything (shared borrows only) *) + "()" | [ out ] -> out | outputs -> "(" ^ String.concat " * " outputs ^ ")" in @@ -281,6 +286,33 @@ let inst_fun_sig_to_string (fmt : ast_formatter) (sg : inst_fun_sig) : string = let all_types = List.append inputs [ outputs ] in String.concat " -> " all_types +let regular_fun_id_to_string (fmt : ast_formatter) (fun_id : A.fun_id) : string + = + match fun_id with + | A.Local fid -> fmt.fun_def_id_to_string fid + | A.Assumed fid -> ( + match fid with + | A.BoxNew -> "alloc::boxed::Box::new" + | A.BoxDeref -> "core::ops::deref::Deref::deref" + | A.BoxDerefMut -> "core::ops::deref::DerefMut::deref_mut" + | A.BoxFree -> "alloc::alloc::box_free") + +let unop_to_string (unop : unop) : string = + match unop with Not -> "¬" | Neg _ -> "-" + +let binop_to_string = Print.CfimAst.binop_to_string + +let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string = + match fun_id with + | Regular (fun_id, rg_id) -> ( + let f = regular_fun_id_to_string fmt fun_id in + match rg_id with + | None -> f + | Some rg_id -> f ^ "@" ^ T.RegionGroupId.to_string rg_id) + | Unop unop -> unop_to_string unop + | Binop (binop, int_ty) -> + binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">" + let rec expression_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) (e : expression) : string = match e with @@ -292,7 +324,46 @@ let rec expression_to_string (fmt : ast_formatter) (indent : string) and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) (lb : let_bindings) (e : expression) : string = - raise Unimplemented + let e = expression_to_string fmt indent indent_incr e in + let val_fmt = ast_to_value_formatter fmt in + match lb with + | Call (lvs, call) -> + let lvs = List.map (typed_lvalue_to_string val_fmt) lvs in + let lvs = + match lvs with + | [] -> + (* Can happen with backward functions which don't give back + * anything (shared borrows only) *) + "()" + | [ lv ] -> lv + | lvs -> "(" ^ String.concat " " lvs ^ ")" + in + let ty_fmt = ast_to_type_formatter fmt in + let tys = List.map (ty_to_string ty_fmt) call.type_params in + let args = List.map (typed_rvalue_to_string fmt) call.args in + let all_args = List.append tys args in + let fun_id = fun_id_to_string fmt call.func in + let call = + if all_args = [] then fun_id + else fun_id ^ " " ^ String.concat " " all_args + in + indent ^ "let " ^ lvs ^ " = " ^ call ^ " in\n" ^ e + | Assign (lv, rv) -> + let lv = typed_lvalue_to_string val_fmt lv in + let rv = typed_rvalue_to_string fmt rv in + indent ^ "let " ^ lv ^ " = " ^ rv ^ " in\n" ^ e + | Deconstruct (lvs, opt_adt_id, rv) -> + let rv = typed_rvalue_to_string fmt rv in + let lvs = List.map (var_or_dummy_to_string val_fmt) lvs in + let lvs = + match opt_adt_id with + | None -> "(" ^ String.concat ", " lvs ^ ")" + | Some (adt_id, variant_id) -> + let cons = fmt.adt_variant_to_string adt_id variant_id in + let lvs = if lvs = [] then "" else " " ^ String.concat " " lvs in + cons ^ lvs + in + indent ^ "let " ^ lvs ^ " = " ^ rv ^ " in\n" ^ e and switch_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) (scrutinee : typed_rvalue) (body : switch_body) : |