From 4a28b75fe834878b1c93d1fe6fe8a02576957f75 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 19 Nov 2021 18:26:00 +0100 Subject: Start working on pretty-printing --- .gitignore | 3 +- src/Interpreter.ml | 8 ++-- src/Print.ml | 133 +++++++++++++++++++++++++++++++++++++++++++++++++++++ src/Types.ml | 7 ++- src/main.ml | 2 + 5 files changed, 146 insertions(+), 7 deletions(-) create mode 100644 src/Print.ml diff --git a/.gitignore b/.gitignore index 4ad2b2b7..eb4a6bf9 100644 --- a/.gitignore +++ b/.gitignore @@ -30,4 +30,5 @@ _opam/ # Misc *~ -nohup.out \ No newline at end of file +nohup.out +.ocamlformat \ No newline at end of file diff --git a/src/Interpreter.ml b/src/Interpreter.ml index b8daf38d..ca821f5b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -91,13 +91,13 @@ and end_borrow_get_borrow_in_values config l outer_borrows vl0 : (res, v' :: vl') | _ -> (res, v' :: vl)) -(*let rec end_borrow_get_borrow_in_env config l env : borrow_lres * env = - match env with +(*let rec end_borrow_get_borrow_in_env config l env0 : borrow_lres * env = + match env0 with | [] -> NotFound - | Var (x, v) :: env' -> ( + | Var (x, v) :: env -> ( match end_borrow_get_borrow_in_value config None l v with | NotFound, v' -> - let res, env'' = end_borrow_get_borrow_in_env config l env' in + let res, env' = end_borrow_get_borrow_in_env config l env' in (res, Var (x, v') :: env'') | res, v' -> (res, Var (x, v') :: env')) | Abs _ :: _ -> unimplemented __LOC__*) diff --git a/src/Print.ml b/src/Print.ml new file mode 100644 index 00000000..adcce831 --- /dev/null +++ b/src/Print.ml @@ -0,0 +1,133 @@ +open Errors +open Identifiers +open Types + +let type_var_to_string (tv : type_var) : string = tv.tv_name + +let region_var_to_string (rv : region_var) : string = + match rv.rv_name with + | Some name -> name + | None -> RegionVarId.to_string rv.rv_index + +let region_to_string (rid_to_string : 'rid -> string) (r : 'rid region) : string + = + match r with Static -> "'static" | Var rid -> rid_to_string rid + +let erased_region_to_string (_ : erased_region) : string = "'_" + +let ref_kind_to_string (rk : ref_kind) : string = + match rk with Mut -> "Mut" | Shared -> "Shared" + +let assumed_ty_to_string (_ : assumed_ty) : string = "Box" + +(* TODO: This is probably not the most OCaml-like way of doing this *) +type 'r type_formatter = { + r_to_string : 'r -> string; + type_var_id_to_string : TypeVarId.id -> string; + type_def_id_to_string : TypeDefId.id -> string; +} + +let integer_type_to_string = function + | Isize -> "isize" + | I8 -> "i8" + | I16 -> "i16" + | I32 -> "i32" + | I64 -> "i64" + | I128 -> "i128" + | Usize -> "usize" + | U8 -> "u8" + | U16 -> "u16" + | U32 -> "u32" + | U64 -> "u64" + | U128 -> "u128" + +let rec ty_to_string (fmt : 'r type_formatter) (ty : 'r ty) : string = + match ty with + | Adt (id, regions, tys) -> + let params = params_to_string fmt regions tys in + fmt.type_def_id_to_string id ^ params + | TypeVar tv -> fmt.type_var_id_to_string tv + | Bool -> "bool" + | Char -> "char" + | Never -> "⊥" + | 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 ^ "]" + | Ref (r, rty, ref_kind) -> ( + match ref_kind with + | Mut -> "&" ^ fmt.r_to_string r ^ " mut (" ^ ty_to_string fmt rty ^ ")" + | Shared -> "&" ^ fmt.r_to_string r ^ " (" ^ ty_to_string fmt rty ^ ")") + | Tuple tys -> + "(" ^ String.concat ", " (List.map (ty_to_string fmt) tys) ^ ")" + | Assumed (aty, regions, tys) -> ( + let params = params_to_string fmt regions tys in + match aty with Box -> "std::boxed::Box" ^ params) + +and params_to_string fmt (regions : 'r list) (types : 'r ty list) : string = + if List.length regions + List.length types > 0 then + let regions = List.map fmt.r_to_string regions in + let types = List.map (ty_to_string fmt) types in + let params = String.concat ", " (List.append regions types) in + "<" ^ params ^ ">" + else "" + +let rty_to_string fmt (ty : rty) : string = ty_to_string fmt ty + +let ety_to_string fmt (ty : ety) : string = ty_to_string fmt ty + +let field_to_string fmt (f : field) : string = + f.field_name ^ " : " ^ ty_to_string fmt f.field_ty + +let variant_to_string fmt (v : variant) : string = + v.variant_name ^ "(" + ^ String.concat ", " + (List.map (field_to_string fmt) (FieldId.vector_to_list v.fields)) + ^ ")" + +let name_to_string (name : name) : string = String.concat "::" name + +let type_def_to_string (type_def_id_to_string : TypeDefId.id -> string) + (def : type_def) : string = + let regions : region_var list = + RegionVarId.vector_to_list def.region_params + in + let types : type_var list = TypeVarId.vector_to_list def.type_params in + let rid_to_string rid = + match List.find_opt (fun rv -> rv.rv_index = rid) regions with + | Some rv -> region_var_to_string rv + | None -> unreachable __LOC__ + in + let r_to_string = region_to_string rid_to_string in + let type_var_id_to_string id = + match List.find_opt (fun tv -> tv.tv_index = id) types with + | Some tv -> type_var_to_string tv + | None -> unreachable __LOC__ + in + let fmt = { r_to_string; type_var_id_to_string; type_def_id_to_string } in + let name = name_to_string def.name in + let params = + if List.length regions + List.length types > 0 then + let regions = List.map region_var_to_string regions in + let types = List.map type_var_to_string types in + let params = String.concat ", " (List.append regions types) in + "<" ^ params ^ ">" + else "" + in + match def.kind with + | Struct fields -> + let fields = FieldId.vector_to_list fields in + if List.length fields > 0 then + let fields = + String.concat "," + (List.map (fun f -> "\n " ^ field_to_string fmt f) fields) + in + "struct " ^ name ^ params ^ "{" ^ fields ^ "}" + else "struct" ^ name ^ params ^ "{}" + | Enum variants -> + let variants = VariantId.vector_to_list variants in + let variants = + List.map (fun v -> "| " ^ variant_to_string fmt v) variants + in + let variants = String.concat "\n" variants in + "enum " ^ name ^ params ^ " =\n" ^ variants diff --git a/src/Types.ml b/src/Types.ml index ef8eccf1..da01d73f 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -11,12 +11,15 @@ module FieldId = IdGen () module RegionVarId = IdGen () type type_var = { - tv_index : TypeVarId.id; (** Unique index identifying the variable *) + tv_index : TypeVarId.id; + (** Unique index identifying the variable - TODO: may be redundant with + using indexed vectors *) tv_name : string; (** Variable name *) } type region_var = { - rv_index : RegionVarId.id; (** Unique index identifying the region *) + rv_index : RegionVarId.id; + (** Unique index identifying the region - TODO: may be redundant *) rv_name : string option; (** Region name *) } diff --git a/src/main.ml b/src/main.ml index 9ba76a18..024209ff 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,5 +1,7 @@ open CfimOfJson + (*open Interpreter*) +open Print let () = let json = Yojson.Basic.from_file "../charon/charon/tests/test1.cfim" in -- cgit v1.2.3