diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 2 | ||||
| -rw-r--r-- | compiler/Print.ml | 533 | ||||
| -rw-r--r-- | compiler/PrintPure.ml | 12 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 2 |
4 files changed, 279 insertions, 270 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 0f6ed530..83cdfc9b 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -117,7 +117,7 @@ let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) : log#ldebug (lazy ("primitive_to_typed_value:" ^ "\n- cv: " - ^ Print.Values.primitive_value_to_string cv)); + ^ Print.PrimitiveValues.primitive_value_to_string cv)); match (ty, cv) with (* Scalar, boolean... *) | T.Bool, Bool v -> { V.value = V.Primitive (Bool v); ty } diff --git a/compiler/Print.ml b/compiler/Print.ml index 52a93a4d..cc25c780 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -164,10 +164,63 @@ module Types = struct let variants = String.concat "\n" variants in "enum " ^ name ^ params ^ " =\n" ^ variants | T.Opaque -> "opaque type " ^ name ^ params + + let type_ctx_to_adt_variant_to_string_fun + (ctx : T.type_decl T.TypeDeclId.Map.t) : + T.TypeDeclId.id -> T.VariantId.id -> string = + fun def_id variant_id -> + let def = T.TypeDeclId.Map.find def_id ctx in + match def.kind with + | Struct _ | Opaque -> failwith "Unreachable" + | Enum variants -> + let variant = T.VariantId.nth variants variant_id in + name_to_string def.name ^ "::" ^ variant.variant_name + + let type_ctx_to_adt_field_names_fun (ctx : T.type_decl T.TypeDeclId.Map.t) : + T.TypeDeclId.id -> T.VariantId.id option -> string list option = + fun def_id opt_variant_id -> + let def = T.TypeDeclId.Map.find def_id ctx in + let fields = TU.type_decl_get_fields def opt_variant_id in + (* There are two cases: either all the fields have names, or none of them + * has names *) + let has_names = + List.exists (fun f -> Option.is_some f.T.field_name) fields + in + if has_names then + let fields = List.map (fun f -> Option.get f.T.field_name) fields in + Some fields + else None + + let type_ctx_to_adt_field_to_string_fun (ctx : T.type_decl T.TypeDeclId.Map.t) + : + T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option + = + fun def_id opt_variant_id field_id -> + let def = T.TypeDeclId.Map.find def_id ctx in + let fields = TU.type_decl_get_fields def opt_variant_id in + let field = T.FieldId.nth fields field_id in + field.T.field_name end module PT = Types (* local module *) +(** Pretty-printing for primitive values *) +module PrimitiveValues = struct + let big_int_to_string (bi : V.big_int) : string = Z.to_string bi + + let scalar_value_to_string (sv : V.scalar_value) : string = + big_int_to_string sv.value ^ ": " ^ PT.integer_type_to_string sv.int_ty + + let primitive_value_to_string (cv : V.primitive_value) : string = + match cv with + | Scalar sv -> scalar_value_to_string sv + | Bool b -> Bool.to_string b + | Char c -> String.make 1 c + | String s -> s +end + +module PPV = PrimitiveValues (* local module *) + (** Pretty-printing for values *) module Values = struct type value_formatter = { @@ -205,18 +258,6 @@ module Values = struct let var_id_to_string (id : V.VarId.id) : string = "var@" ^ V.VarId.to_string id - let big_int_to_string (bi : V.big_int) : string = Z.to_string bi - - let scalar_value_to_string (sv : V.scalar_value) : string = - big_int_to_string sv.value ^ ": " ^ PT.integer_type_to_string sv.int_ty - - let primitive_value_to_string (cv : V.primitive_value) : string = - match cv with - | Scalar sv -> scalar_value_to_string sv - | Bool b -> Bool.to_string b - | Char c -> String.make 1 c - | String s -> s - let symbolic_value_id_to_string (id : V.SymbolicValueId.id) : string = "s@" ^ V.SymbolicValueId.to_string id @@ -240,7 +281,7 @@ module Values = struct string = let ty_fmt : PT.etype_formatter = value_to_etype_formatter fmt in match v.value with - | Primitive cv -> primitive_value_to_string cv + | Primitive cv -> PPV.primitive_value_to_string cv | Adt av -> ( let field_values = List.map (typed_value_to_string fmt) av.field_values @@ -352,7 +393,7 @@ module Values = struct string = let ty_fmt : PT.rtype_formatter = value_to_rtype_formatter fmt in match v.value with - | APrimitive cv -> primitive_value_to_string cv + | APrimitive cv -> PPV.primitive_value_to_string cv | AAdt av -> ( let field_values = List.map (typed_avalue_to_string fmt) av.field_values @@ -481,193 +522,7 @@ end module PV = Values (* local module *) -(** Pretty-printing for contexts *) -module Contexts = struct - let binder_to_string (bv : C.binder) : string = - match bv.name with - | None -> PV.var_id_to_string bv.index - | Some name -> name - - let env_elem_to_string (fmt : PV.value_formatter) (indent : string) - (indent_incr : string) (ev : C.env_elem) : string = - match ev with - | Var (var, tv) -> - let bv = - match var with Some var -> binder_to_string var | None -> "_" - in - indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;" - | Abs abs -> PV.abs_to_string fmt indent indent_incr abs - | Frame -> failwith "Can't print a Frame element" - - let opt_env_elem_to_string (fmt : PV.value_formatter) (indent : string) - (indent_incr : string) (ev : C.env_elem option) : string = - match ev with - | None -> indent ^ "..." - | Some ev -> env_elem_to_string fmt indent indent_incr ev - - (** Filters "dummy" bindings from an environment, to gain space and clarity/ - See [env_to_string]. *) - let filter_env (env : C.env) : C.env_elem option list = - (* We filter: - * - non-dummy bindings which point to ⊥ - * - dummy bindings which don't contain loans nor borrows - * Note that the first case can sometimes be confusing: we may try to improve - * it... - *) - let filter_elem (ev : C.env_elem) : C.env_elem option = - match ev with - | Var (Some _, tv) -> - (* Not a dummy binding: check if the value is ⊥ *) - if VU.is_bottom tv.value then None else Some ev - | Var (None, tv) -> - (* Dummy binding: check if the value contains borrows or loans *) - if VU.borrows_in_value tv || VU.loans_in_value tv then Some ev - else None - | _ -> Some ev - in - let env = List.map filter_elem env in - (* We collapse groups of filtered values - so that we can print one - * single "..." for a whole group of filtered values *) - let rec group_filtered (env : C.env_elem option list) : - C.env_elem option list = - match env with - | [] -> [] - | None :: None :: env -> group_filtered (None :: env) - | x :: env -> x :: group_filtered env - in - group_filtered env - - (** Environments can have a lot of dummy or uninitialized values: [filter] - allows to filter them when printing, replacing groups of such bindings with - "..." to gain space and clarity. - *) - let env_to_string (filter : bool) (fmt : PV.value_formatter) (env : C.env) : - string = - let env = - if filter then filter_env env else List.map (fun ev -> Some ev) env - in - "{\n" - ^ String.concat "\n" - (List.map (fun ev -> opt_env_elem_to_string fmt " " " " ev) env) - ^ "\n}" - - type ctx_formatter = PV.value_formatter - - let ctx_to_etype_formatter (fmt : ctx_formatter) : PT.etype_formatter = - PV.value_to_etype_formatter fmt - - let ctx_to_rtype_formatter (fmt : ctx_formatter) : PT.rtype_formatter = - PV.value_to_rtype_formatter fmt - - let type_ctx_to_adt_variant_to_string_fun - (ctx : T.type_decl T.TypeDeclId.Map.t) : - T.TypeDeclId.id -> T.VariantId.id -> string = - fun def_id variant_id -> - let def = T.TypeDeclId.Map.find def_id ctx in - match def.kind with - | Struct _ | Opaque -> failwith "Unreachable" - | Enum variants -> - let variant = T.VariantId.nth variants variant_id in - name_to_string def.name ^ "::" ^ variant.variant_name - - let type_ctx_to_adt_field_names_fun (ctx : T.type_decl T.TypeDeclId.Map.t) : - T.TypeDeclId.id -> T.VariantId.id option -> string list option = - fun def_id opt_variant_id -> - let def = T.TypeDeclId.Map.find def_id ctx in - let fields = TU.type_decl_get_fields def opt_variant_id in - (* There are two cases: either all the fields have names, or none of them - * has names *) - let has_names = - List.exists (fun f -> Option.is_some f.T.field_name) fields - in - if has_names then - let fields = List.map (fun f -> Option.get f.T.field_name) fields in - Some fields - else None - - let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter = - (* We shouldn't use rvar_to_string *) - let rvar_to_string _r = failwith "Unexpected use of rvar_to_string" in - let r_to_string r = PT.region_id_to_string r in - - let type_var_id_to_string vid = - let v = C.lookup_type_var ctx vid in - v.name - in - let type_decl_id_to_string def_id = - let def = C.ctx_lookup_type_decl ctx def_id in - name_to_string def.name - in - let adt_variant_to_string = - type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls - in - let var_id_to_string vid = - let bv = C.ctx_lookup_binder ctx vid in - binder_to_string bv - in - let adt_field_names = - type_ctx_to_adt_field_names_fun ctx.type_context.type_decls - in - { - rvar_to_string; - r_to_string; - type_var_id_to_string; - type_decl_id_to_string; - adt_variant_to_string; - var_id_to_string; - adt_field_names; - } - - (** Split an [env] at every occurrence of [Frame], eliminating those elements. - Also reorders the frames and the values in the frames according to the - following order: - * frames: from the current frame to the first pushed (oldest frame) - * values: from the first pushed (oldest) to the last pushed - *) - let split_env_according_to_frames (env : C.env) : C.env list = - let rec split_aux (frames : C.env list) (curr_frame : C.env) (env : C.env) = - match env with - | [] -> - if List.length curr_frame > 0 then curr_frame :: frames else frames - | Frame :: env' -> split_aux (curr_frame :: frames) [] env' - | ev :: env' -> split_aux frames (ev :: curr_frame) env' - in - let frames = split_aux [] [] env in - frames - - let eval_ctx_to_string (ctx : C.eval_ctx) : string = - let fmt = eval_ctx_to_ctx_formatter ctx in - let ended_regions = T.RegionId.Set.to_string None ctx.ended_regions in - let frames = split_env_according_to_frames ctx.env in - let num_frames = List.length frames in - let frames = - List.mapi - (fun i f -> - let num_bindings = ref 0 in - let num_dummies = ref 0 in - let num_abs = ref 0 in - List.iter - (fun ev -> - match ev with - | C.Var (None, _) -> num_dummies := !num_abs + 1 - | C.Var (Some _, _) -> num_bindings := !num_bindings + 1 - | C.Abs _ -> num_abs := !num_abs + 1 - | _ -> raise (Failure "Unreachable")) - f; - "\n# Frame " ^ string_of_int i ^ ":" ^ "\n- locals: " - ^ string_of_int !num_bindings - ^ "\n- dummy bindings: " ^ string_of_int !num_dummies - ^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n" - ^ env_to_string true fmt f ^ "\n") - frames - in - "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames - ^ " frame(s)\n" ^ String.concat "" frames -end - -module PC = Contexts (* local module *) - -(** Pretty-printing for contexts (generic functions) *) +(** Pretty-printing for LLBC AST (generic functions) *) module LlbcAst = struct let var_to_string (var : A.var) : string = match var.name with @@ -689,20 +544,6 @@ module LlbcAst = struct global_decl_id_to_string : A.GlobalDeclId.id -> string; } - let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter = - { - PV.rvar_to_string = fmt.rvar_to_string; - PV.r_to_string = fmt.r_to_string; - PV.type_var_id_to_string = fmt.type_var_id_to_string; - PV.type_decl_id_to_string = fmt.type_decl_id_to_string; - PV.adt_variant_to_string = fmt.adt_variant_to_string; - PV.var_id_to_string = fmt.var_id_to_string; - PV.adt_field_names = fmt.adt_field_names; - } - - let ast_to_value_formatter (fmt : ast_formatter) : PV.value_formatter = - ast_to_ctx_formatter fmt - let ast_to_etype_formatter (fmt : ast_formatter) : PT.etype_formatter = { PT.r_to_string = PT.erased_region_to_string; @@ -724,42 +565,6 @@ module LlbcAst = struct PT.type_decl_id_to_string = fmt.type_decl_id_to_string; } - let type_ctx_to_adt_field_to_string_fun (ctx : T.type_decl T.TypeDeclId.Map.t) - : - T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option - = - fun def_id opt_variant_id field_id -> - let def = T.TypeDeclId.Map.find def_id ctx in - let fields = TU.type_decl_get_fields def opt_variant_id in - let field = T.FieldId.nth fields field_id in - field.T.field_name - - let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : ast_formatter = - let ctx_fmt = PC.eval_ctx_to_ctx_formatter ctx in - let adt_field_to_string = - type_ctx_to_adt_field_to_string_fun ctx.type_context.type_decls - in - let fun_decl_id_to_string def_id = - let def = C.ctx_lookup_fun_decl ctx def_id in - fun_name_to_string def.name - in - let global_decl_id_to_string def_id = - let def = C.ctx_lookup_global_decl ctx def_id in - global_name_to_string def.name - in - { - rvar_to_string = ctx_fmt.PV.rvar_to_string; - r_to_string = ctx_fmt.PV.r_to_string; - type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string; - type_decl_id_to_string = ctx_fmt.PV.type_decl_id_to_string; - adt_variant_to_string = ctx_fmt.PV.adt_variant_to_string; - var_id_to_string = ctx_fmt.PV.var_id_to_string; - adt_field_names = ctx_fmt.PV.adt_field_names; - adt_field_to_string; - fun_decl_id_to_string; - global_decl_id_to_string; - } - let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t) (fun_decls : A.fun_decl A.FunDeclId.Map.t) (global_decls : A.global_decl A.GlobalDeclId.Map.t) (fdef : A.fun_decl) : @@ -779,14 +584,16 @@ module LlbcAst = struct name_to_string def.name in let adt_variant_to_string = - PC.type_ctx_to_adt_variant_to_string_fun type_decls + PT.type_ctx_to_adt_variant_to_string_fun type_decls in let var_id_to_string vid = let var = V.VarId.nth (Option.get fdef.body).locals vid in var_to_string var in - let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in - let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_decls in + let adt_field_names = PT.type_ctx_to_adt_field_names_fun type_decls in + let adt_field_to_string = + PT.type_ctx_to_adt_field_to_string_fun type_decls + in let fun_decl_id_to_string def_id = let def = A.FunDeclId.Map.find def_id fun_decls in fun_name_to_string def.name @@ -877,7 +684,7 @@ module LlbcAst = struct | E.Move p -> "move " ^ place_to_string fmt p | E.Constant (ty, cv) -> "(" - ^ PV.primitive_value_to_string cv + ^ PPV.primitive_value_to_string cv ^ " : " ^ PT.ety_to_string (ast_to_etype_formatter fmt) ty ^ ")" @@ -1024,7 +831,9 @@ module LlbcAst = struct List.map (fun (svl, be) -> let svl = - List.map (fun sv -> "| " ^ PV.scalar_value_to_string sv) svl + List.map + (fun sv -> "| " ^ PPV.scalar_value_to_string sv) + svl in let svl = String.concat " " svl in indent1 ^ svl ^ " => {\n" ^ inner_to_string2 be ^ "\n" @@ -1120,6 +929,206 @@ end module PA = LlbcAst (* local module *) +(** Pretty-printing for contexts *) +module Contexts = struct + let binder_to_string (bv : C.binder) : string = + match bv.name with + | None -> PV.var_id_to_string bv.index + | Some name -> name + + let env_elem_to_string (fmt : PV.value_formatter) (indent : string) + (indent_incr : string) (ev : C.env_elem) : string = + match ev with + | Var (var, tv) -> + let bv = + match var with Some var -> binder_to_string var | None -> "_" + in + indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;" + | Abs abs -> PV.abs_to_string fmt indent indent_incr abs + | Frame -> failwith "Can't print a Frame element" + + let opt_env_elem_to_string (fmt : PV.value_formatter) (indent : string) + (indent_incr : string) (ev : C.env_elem option) : string = + match ev with + | None -> indent ^ "..." + | Some ev -> env_elem_to_string fmt indent indent_incr ev + + (** Filters "dummy" bindings from an environment, to gain space and clarity/ + See [env_to_string]. *) + let filter_env (env : C.env) : C.env_elem option list = + (* We filter: + * - non-dummy bindings which point to ⊥ + * - dummy bindings which don't contain loans nor borrows + * Note that the first case can sometimes be confusing: we may try to improve + * it... + *) + let filter_elem (ev : C.env_elem) : C.env_elem option = + match ev with + | Var (Some _, tv) -> + (* Not a dummy binding: check if the value is ⊥ *) + if VU.is_bottom tv.value then None else Some ev + | Var (None, tv) -> + (* Dummy binding: check if the value contains borrows or loans *) + if VU.borrows_in_value tv || VU.loans_in_value tv then Some ev + else None + | _ -> Some ev + in + let env = List.map filter_elem env in + (* We collapse groups of filtered values - so that we can print one + * single "..." for a whole group of filtered values *) + let rec group_filtered (env : C.env_elem option list) : + C.env_elem option list = + match env with + | [] -> [] + | None :: None :: env -> group_filtered (None :: env) + | x :: env -> x :: group_filtered env + in + group_filtered env + + (** Environments can have a lot of dummy or uninitialized values: [filter] + allows to filter them when printing, replacing groups of such bindings with + "..." to gain space and clarity. + *) + let env_to_string (filter : bool) (fmt : PV.value_formatter) (env : C.env) : + string = + let env = + if filter then filter_env env else List.map (fun ev -> Some ev) env + in + "{\n" + ^ String.concat "\n" + (List.map (fun ev -> opt_env_elem_to_string fmt " " " " ev) env) + ^ "\n}" + + type ctx_formatter = PV.value_formatter + + let ast_to_ctx_formatter (fmt : PA.ast_formatter) : ctx_formatter = + { + PV.rvar_to_string = fmt.rvar_to_string; + PV.r_to_string = fmt.r_to_string; + PV.type_var_id_to_string = fmt.type_var_id_to_string; + PV.type_decl_id_to_string = fmt.type_decl_id_to_string; + PV.adt_variant_to_string = fmt.adt_variant_to_string; + PV.var_id_to_string = fmt.var_id_to_string; + PV.adt_field_names = fmt.adt_field_names; + } + + let ast_to_value_formatter (fmt : PA.ast_formatter) : PV.value_formatter = + ast_to_ctx_formatter fmt + + let ctx_to_etype_formatter (fmt : ctx_formatter) : PT.etype_formatter = + PV.value_to_etype_formatter fmt + + let ctx_to_rtype_formatter (fmt : ctx_formatter) : PT.rtype_formatter = + PV.value_to_rtype_formatter fmt + + let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter = + (* We shouldn't use rvar_to_string *) + let rvar_to_string _r = failwith "Unexpected use of rvar_to_string" in + let r_to_string r = PT.region_id_to_string r in + + let type_var_id_to_string vid = + let v = C.lookup_type_var ctx vid in + v.name + in + let type_decl_id_to_string def_id = + let def = C.ctx_lookup_type_decl ctx def_id in + name_to_string def.name + in + let adt_variant_to_string = + PT.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls + in + let var_id_to_string vid = + let bv = C.ctx_lookup_binder ctx vid in + binder_to_string bv + in + let adt_field_names = + PT.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls + in + { + rvar_to_string; + r_to_string; + type_var_id_to_string; + type_decl_id_to_string; + adt_variant_to_string; + var_id_to_string; + adt_field_names; + } + + let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : PA.ast_formatter = + let ctx_fmt = eval_ctx_to_ctx_formatter ctx in + let adt_field_to_string = + PT.type_ctx_to_adt_field_to_string_fun ctx.type_context.type_decls + in + let fun_decl_id_to_string def_id = + let def = C.ctx_lookup_fun_decl ctx def_id in + fun_name_to_string def.name + in + let global_decl_id_to_string def_id = + let def = C.ctx_lookup_global_decl ctx def_id in + global_name_to_string def.name + in + { + rvar_to_string = ctx_fmt.PV.rvar_to_string; + r_to_string = ctx_fmt.PV.r_to_string; + type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string; + type_decl_id_to_string = ctx_fmt.PV.type_decl_id_to_string; + adt_variant_to_string = ctx_fmt.PV.adt_variant_to_string; + var_id_to_string = ctx_fmt.PV.var_id_to_string; + adt_field_names = ctx_fmt.PV.adt_field_names; + adt_field_to_string; + fun_decl_id_to_string; + global_decl_id_to_string; + } + + (** Split an [env] at every occurrence of [Frame], eliminating those elements. + Also reorders the frames and the values in the frames according to the + following order: + * frames: from the current frame to the first pushed (oldest frame) + * values: from the first pushed (oldest) to the last pushed + *) + let split_env_according_to_frames (env : C.env) : C.env list = + let rec split_aux (frames : C.env list) (curr_frame : C.env) (env : C.env) = + match env with + | [] -> + if List.length curr_frame > 0 then curr_frame :: frames else frames + | Frame :: env' -> split_aux (curr_frame :: frames) [] env' + | ev :: env' -> split_aux frames (ev :: curr_frame) env' + in + let frames = split_aux [] [] env in + frames + + let eval_ctx_to_string (ctx : C.eval_ctx) : string = + let fmt = eval_ctx_to_ctx_formatter ctx in + let ended_regions = T.RegionId.Set.to_string None ctx.ended_regions in + let frames = split_env_according_to_frames ctx.env in + let num_frames = List.length frames in + let frames = + List.mapi + (fun i f -> + let num_bindings = ref 0 in + let num_dummies = ref 0 in + let num_abs = ref 0 in + List.iter + (fun ev -> + match ev with + | C.Var (None, _) -> num_dummies := !num_abs + 1 + | C.Var (Some _, _) -> num_bindings := !num_bindings + 1 + | C.Abs _ -> num_abs := !num_abs + 1 + | _ -> raise (Failure "Unreachable")) + f; + "\n# Frame " ^ string_of_int i ^ ":" ^ "\n- locals: " + ^ string_of_int !num_bindings + ^ "\n- dummy bindings: " ^ string_of_int !num_dummies + ^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n" + ^ env_to_string true fmt f ^ "\n") + frames + in + "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames + ^ " frame(s)\n" ^ String.concat "" frames +end + +module PC = Contexts (* local module *) + (** Pretty-printing for ASTs (functions based on a definition context) *) module Module = struct (** This function pretty-prints a type definition by using a definition @@ -1167,12 +1176,12 @@ module Module = struct PA.var_to_string var in let adt_variant_to_string = - PC.type_ctx_to_adt_variant_to_string_fun type_context + PT.type_ctx_to_adt_variant_to_string_fun type_context in let adt_field_to_string = - PA.type_ctx_to_adt_field_to_string_fun type_context + PT.type_ctx_to_adt_field_to_string_fun type_context in - let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_context in + let adt_field_names = PT.type_ctx_to_adt_field_names_fun type_context in { rvar_to_string; r_to_string; @@ -1269,15 +1278,15 @@ module EvalCtxLlbcAst = struct PV.typed_avalue_to_string fmt v let place_to_string (ctx : C.eval_ctx) (op : E.place) : string = - let fmt = PA.eval_ctx_to_ast_formatter ctx in + let fmt = PC.eval_ctx_to_ast_formatter ctx in PA.place_to_string fmt op let operand_to_string (ctx : C.eval_ctx) (op : E.operand) : string = - let fmt = PA.eval_ctx_to_ast_formatter ctx in + let fmt = PC.eval_ctx_to_ast_formatter ctx in PA.operand_to_string fmt op let statement_to_string (ctx : C.eval_ctx) (indent : string) (indent_incr : string) (e : A.statement) : string = - let fmt = PA.eval_ctx_to_ast_formatter ctx in + let fmt = PC.eval_ctx_to_ast_formatter ctx in PA.statement_to_string fmt indent indent_incr e end diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 6fafa0a3..67353547 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -56,7 +56,7 @@ let global_name_to_string = Print.global_name_to_string 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 +let scalar_value_to_string = Print.PrimitiveValues.scalar_value_to_string let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t) (type_params : type_var list) : type_formatter = @@ -89,17 +89,17 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) name_to_string def.name in let adt_variant_to_string = - Print.Contexts.type_ctx_to_adt_variant_to_string_fun type_decls + Print.Types.type_ctx_to_adt_variant_to_string_fun type_decls in let var_id_to_string vid = (* TODO: somehow lookup in the context *) "^" ^ VarId.to_string vid in let adt_field_names = - Print.Contexts.type_ctx_to_adt_field_names_fun type_decls + Print.Types.type_ctx_to_adt_field_names_fun type_decls in let adt_field_to_string = - Print.LlbcAst.type_ctx_to_adt_field_to_string_fun type_decls + Print.Types.type_ctx_to_adt_field_to_string_fun type_decls in let fun_decl_id_to_string def_id = let def = FunDeclId.Map.find def_id fun_decls in @@ -357,7 +357,7 @@ let adt_g_value_to_string (fmt : value_formatter) let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) : string = match v.value with - | PatConstant cv -> Print.Values.primitive_value_to_string cv + | PatConstant cv -> Print.PrimitiveValues.primitive_value_to_string cv | PatVar (v, None) -> var_to_string (ast_to_type_formatter fmt) v | PatVar (v, Some mp) -> let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in @@ -436,7 +436,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool) | Var var_id -> let s = fmt.var_id_to_string var_id in if inside then "(" ^ s ^ ")" else s - | Const cv -> Print.Values.primitive_value_to_string cv + | Const cv -> Print.PrimitiveValues.primitive_value_to_string cv | App _ -> (* Recursively destruct the app, to have a pair (app, arguments list) *) let app, args = destruct_apps e in diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 749eae1d..f393b059 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -197,7 +197,7 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string = (* TODO: move *) let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = let fmt = bs_ctx_to_ast_formatter ctx in - let fmt = Print.LlbcAst.ast_to_value_formatter fmt in + let fmt = Print.Contexts.ast_to_value_formatter fmt in let indent = "" in let indent_incr = " " in Print.Values.abs_to_string fmt indent indent_incr abs |