summaryrefslogtreecommitdiff
path: root/compiler/Print.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Print.ml')
-rw-r--r--compiler/Print.ml202
1 files changed, 59 insertions, 143 deletions
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 7f0d95ff..dd24767e 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -15,8 +15,7 @@ let bool_to_string (b : bool) : string = if b then "true" else "false"
(** Pretty-printing for values *)
module Values = struct
type value_formatter = {
- rvar_to_string : T.RegionVarId.id -> string;
- r_to_string : T.RegionId.id -> string;
+ region_id_to_string : T.RegionId.id -> string;
type_var_id_to_string : T.TypeVarId.id -> string;
type_decl_id_to_string : T.TypeDeclId.id -> string;
const_generic_var_id_to_string : T.ConstGenericVarId.id -> string;
@@ -30,33 +29,9 @@ module Values = struct
T.TypeDeclId.id -> T.VariantId.id option -> string list option;
}
- let value_to_etype_formatter (fmt : value_formatter) : PT.etype_formatter =
+ let value_to_type_formatter (fmt : value_formatter) : PT.type_formatter =
{
- PT.r_to_string = PT.erased_region_to_string;
- PT.type_var_id_to_string = fmt.type_var_id_to_string;
- PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
- PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
- PT.global_decl_id_to_string = fmt.global_decl_id_to_string;
- PT.trait_decl_id_to_string = fmt.trait_decl_id_to_string;
- PT.trait_impl_id_to_string = fmt.trait_impl_id_to_string;
- PT.trait_clause_id_to_string = fmt.trait_clause_id_to_string;
- }
-
- let value_to_rtype_formatter (fmt : value_formatter) : PT.rtype_formatter =
- {
- PT.r_to_string = PT.region_to_string fmt.r_to_string;
- PT.type_var_id_to_string = fmt.type_var_id_to_string;
- PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
- PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
- PT.global_decl_id_to_string = fmt.global_decl_id_to_string;
- PT.trait_decl_id_to_string = fmt.trait_decl_id_to_string;
- PT.trait_impl_id_to_string = fmt.trait_impl_id_to_string;
- PT.trait_clause_id_to_string = fmt.trait_clause_id_to_string;
- }
-
- let value_to_stype_formatter (fmt : value_formatter) : PT.stype_formatter =
- {
- PT.r_to_string = PT.region_to_string fmt.rvar_to_string;
+ PT.region_id_to_string = fmt.region_id_to_string;
PT.type_var_id_to_string = fmt.type_var_id_to_string;
PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
@@ -72,17 +47,17 @@ module Values = struct
let symbolic_value_id_to_string (id : V.SymbolicValueId.id) : string =
"s@" ^ V.SymbolicValueId.to_string id
- let symbolic_value_to_string (fmt : PT.rtype_formatter)
- (sv : V.symbolic_value) : string =
- symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.rty_to_string fmt sv.sv_ty
+ let symbolic_value_to_string (fmt : PT.type_formatter) (sv : V.symbolic_value)
+ : string =
+ symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.ty_to_string fmt sv.sv_ty
let symbolic_value_proj_to_string (fmt : value_formatter)
- (sv : V.symbolic_value) (rty : T.rty) : string =
+ (sv : V.symbolic_value) (rty : T.ty) : string =
+ let ty_fmt = value_to_type_formatter fmt in
symbolic_value_id_to_string sv.sv_id
^ " : "
- ^ PT.ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty
- ^ " <: "
- ^ PT.ty_to_string (value_to_rtype_formatter fmt) rty
+ ^ PT.ty_to_string ty_fmt sv.sv_ty
+ ^ " <: " ^ PT.ty_to_string ty_fmt rty
(* TODO: it may be a good idea to try to factorize this function with
* typed_avalue_to_string. At some point we had done it, because [typed_value]
@@ -90,18 +65,18 @@ module Values = struct
* but then we removed this general type because it proved to be a bad idea. *)
let rec typed_value_to_string (fmt : value_formatter) (v : V.typed_value) :
string =
- let ty_fmt : PT.etype_formatter = value_to_etype_formatter fmt in
+ let ty_fmt : PT.type_formatter = value_to_type_formatter fmt in
match v.value with
- | Literal cv -> PPV.literal_to_string cv
- | Adt av -> (
+ | VLiteral cv -> PPV.literal_to_string cv
+ | VAdt av -> (
let field_values =
List.map (typed_value_to_string fmt) av.field_values
in
match v.ty with
- | T.Adt (T.Tuple, _) ->
+ | T.TAdt (T.Tuple, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | T.Adt (T.AdtId def_id, _) ->
+ | T.TAdt (T.AdtId def_id, _) ->
(* "Regular" ADT *)
let adt_ident =
match av.variant_id with
@@ -123,11 +98,11 @@ module Values = struct
let field_values = String.concat " " field_values in
adt_ident ^ " { " ^ field_values ^ " }"
else adt_ident
- | T.Adt (T.Assumed aty, _) -> (
+ | T.TAdt (T.TAssumed aty, _) -> (
(* Assumed type *)
match (aty, field_values) with
- | Box, [ bv ] -> "@Box(" ^ bv ^ ")"
- | Array, _ ->
+ | TBox, [ bv ] -> "@Box(" ^ bv ^ ")"
+ | TArray, _ ->
(* Happens when we aggregate values *)
"@Array[" ^ String.concat ", " field_values ^ "]"
| _ ->
@@ -136,7 +111,7 @@ module Values = struct
| Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
| Borrow bc -> borrow_content_to_string fmt bc
| Loan lc -> loan_content_to_string fmt lc
- | Symbolic s -> symbolic_value_to_string (value_to_rtype_formatter fmt) s
+ | Symbolic s -> symbolic_value_to_string ty_fmt s
and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) :
string =
@@ -180,7 +155,7 @@ module Values = struct
" (" ^ String.concat "," given_back ^ ") "
in
"⌊"
- ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv
+ ^ symbolic_value_to_string (value_to_type_formatter fmt) sv
^ given_back ^ "⌋"
| AProjBorrows (sv, rty) ->
"(" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
@@ -195,17 +170,17 @@ module Values = struct
let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) :
string =
- let ty_fmt : PT.rtype_formatter = value_to_rtype_formatter fmt in
+ let ty_fmt : PT.type_formatter = value_to_type_formatter fmt in
match v.value with
| AAdt av -> (
let field_values =
List.map (typed_avalue_to_string fmt) av.field_values
in
match v.ty with
- | T.Adt (T.Tuple, _) ->
+ | T.TAdt (T.Tuple, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | T.Adt (T.AdtId def_id, _) ->
+ | T.TAdt (T.AdtId def_id, _) ->
(* "Regular" ADT *)
let adt_ident =
match av.variant_id with
@@ -227,10 +202,10 @@ module Values = struct
let field_values = String.concat " " field_values in
adt_ident ^ " { " ^ field_values ^ " }"
else adt_ident
- | T.Adt (T.Assumed aty, _) -> (
+ | T.TAdt (T.TAssumed aty, _) -> (
(* Assumed type *)
match (aty, field_values) with
- | Box, [ bv ] -> "@Box(" ^ bv ^ ")"
+ | TBox, [ bv ] -> "@Box(" ^ bv ^ ")"
| _ -> raise (Failure "Inconsistent value"))
| _ -> raise (Failure "Inconsistent typed value"))
| ABottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
@@ -352,7 +327,7 @@ module Values = struct
let inst_fun_sig_to_string (fmt : value_formatter) (sg : LlbcAst.inst_fun_sig)
: string =
(* TODO: print the trait type constraints? *)
- let ty_fmt = value_to_rtype_formatter fmt in
+ let ty_fmt = value_to_type_formatter fmt in
let ty_to_string = PT.ty_to_string ty_fmt in
let inputs =
@@ -376,23 +351,23 @@ module Contexts = struct
let binder_to_string (bv : C.binder) : string =
match bv with
- | VarBinder b -> var_binder_to_string b
- | DummyBinder bid -> dummy_var_id_to_string bid
+ | BVar b -> var_binder_to_string b
+ | BDummy bid -> dummy_var_id_to_string bid
let env_elem_to_string (fmt : PV.value_formatter) (verbose : bool)
(with_var_types : bool) (indent : string) (indent_incr : string)
(ev : C.env_elem) : string =
match ev with
- | Var (var, tv) ->
+ | EBinding (var, tv) ->
let bv = binder_to_string var in
let ty =
if with_var_types then
- " : " ^ PT.ty_to_string (PV.value_to_etype_formatter fmt) tv.V.ty
+ " : " ^ PT.ty_to_string (PV.value_to_type_formatter fmt) tv.V.ty
else ""
in
indent ^ bv ^ ty ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
- | Abs abs -> PV.abs_to_string fmt verbose indent indent_incr abs
- | Frame -> raise (Failure "Can't print a Frame element")
+ | EAbs abs -> PV.abs_to_string fmt verbose indent indent_incr abs
+ | EFrame -> raise (Failure "Can't print a Frame element")
let opt_env_elem_to_string (fmt : PV.value_formatter) (verbose : bool)
(with_var_types : bool) (indent : string) (indent_incr : string)
@@ -413,10 +388,10 @@ module Contexts = struct
*)
let filter_elem (ev : C.env_elem) : C.env_elem option =
match ev with
- | Var (VarBinder _, tv) ->
+ | EBinding (BVar _, tv) ->
(* Not a dummy binding: check if the value is ⊥ *)
if VU.is_bottom tv.value then None else Some ev
- | Var (DummyBinder _, tv) ->
+ | EBinding (BDummy _, 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
@@ -456,8 +431,7 @@ module Contexts = struct
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.region_id_to_string = fmt.region_id_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.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
@@ -473,22 +447,11 @@ module Contexts = struct
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 ctx_to_stype_formatter (fmt : ctx_formatter) : PT.stype_formatter =
- PV.value_to_stype_formatter fmt
+ let ctx_to_type_formatter (fmt : ctx_formatter) : PT.type_formatter =
+ PV.value_to_type_formatter fmt
let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
- let rvar_to_string r =
- (* In theory we shouldn't use rvar_to_string, but it can happen
- when printing definitions for instance... *)
- T.RegionVarId.to_string r
- in
- let r_to_string r = PT.region_id_to_string r in
+ let region_id_to_string r = PT.region_id_to_string r in
let type_var_id_to_string vid =
(* The context may be invalid *)
@@ -529,8 +492,7 @@ module Contexts = struct
PT.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls
in
{
- rvar_to_string;
- r_to_string;
+ region_id_to_string;
type_var_id_to_string;
type_decl_id_to_string;
const_generic_var_id_to_string;
@@ -566,8 +528,7 @@ module Contexts = struct
in
let trait_clause_id_to_string id = PT.trait_clause_id_to_pretty_string id in
{
- rvar_to_string = ctx_fmt.PV.rvar_to_string;
- r_to_string = ctx_fmt.PV.r_to_string;
+ region_id_to_string = ctx_fmt.PV.region_id_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;
const_generic_var_id_to_string = ctx_fmt.PV.const_generic_var_id_to_string;
@@ -593,7 +554,7 @@ module Contexts = struct
match env with
| [] ->
if List.length curr_frame > 0 then curr_frame :: frames else frames
- | Frame :: env' -> split_aux (curr_frame :: frames) [] env'
+ | EFrame :: env' -> split_aux (curr_frame :: frames) [] env'
| ev :: env' -> split_aux frames (ev :: curr_frame) env'
in
let frames = split_aux [] [] env in
@@ -613,9 +574,9 @@ module Contexts = struct
List.iter
(fun ev ->
match ev with
- | C.Var (DummyBinder _, _) -> num_dummies := !num_abs + 1
- | C.Var (VarBinder _, _) -> num_bindings := !num_bindings + 1
- | C.Abs _ -> num_abs := !num_abs + 1
+ | C.EBinding (BDummy _, _) -> num_dummies := !num_abs + 1
+ | C.EBinding (BVar _, _) -> num_bindings := !num_bindings + 1
+ | C.EAbs _ -> num_abs := !num_abs + 1
| _ -> raise (Failure "Unreachable"))
f;
"\n# Frame " ^ string_of_int i ^ ":" ^ "\n- locals: "
@@ -645,77 +606,32 @@ module PC = Contexts (* local module *)
(** Pretty-printing for LLBC ASTs (functions based on an evaluation context) *)
module EvalCtxLlbcAst = struct
- let ety_to_string (ctx : C.eval_ctx) (t : T.ety) : string =
+ let ty_to_string (ctx : C.eval_ctx) (t : T.ty) : string =
let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_etype_formatter fmt in
- PT.ety_to_string fmt t
-
- let rty_to_string (ctx : C.eval_ctx) (t : T.rty) : string =
- let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_rtype_formatter fmt in
- PT.rty_to_string fmt t
-
- let sty_to_string (ctx : C.eval_ctx) (t : T.sty) : string =
- let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_stype_formatter fmt in
- PT.sty_to_string fmt t
+ let fmt = PC.ctx_to_type_formatter fmt in
+ PT.ty_to_string fmt t
let generic_params_to_strings (ctx : C.eval_ctx) (x : T.generic_params) :
string list * string list =
let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_stype_formatter fmt in
+ let fmt = PC.ctx_to_type_formatter fmt in
PT.generic_params_to_strings fmt x
- let egeneric_args_to_string (ctx : C.eval_ctx) (x : T.egeneric_args) : string
- =
- let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_etype_formatter fmt in
- PT.egeneric_args_to_string fmt x
-
- let rgeneric_args_to_string (ctx : C.eval_ctx) (x : T.rgeneric_args) : string
- =
- let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_rtype_formatter fmt in
- PT.rgeneric_args_to_string fmt x
-
- let sgeneric_args_to_string (ctx : C.eval_ctx) (x : T.sgeneric_args) : string
- =
+ let generic_args_to_string (ctx : C.eval_ctx) (x : T.generic_args) : string =
let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_stype_formatter fmt in
- PT.sgeneric_args_to_string fmt x
+ let fmt = PC.ctx_to_type_formatter fmt in
+ PT.generic_args_to_string fmt x
- let etrait_ref_to_string (ctx : C.eval_ctx) (x : T.etrait_ref) : string =
+ let trait_ref_to_string (ctx : C.eval_ctx) (x : T.trait_ref) : string =
let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_etype_formatter fmt in
- PT.etrait_ref_to_string fmt x
+ let fmt = PC.ctx_to_type_formatter fmt in
+ PT.trait_ref_to_string fmt x
- let rtrait_ref_to_string (ctx : C.eval_ctx) (x : T.rtrait_ref) : string =
- let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_rtype_formatter fmt in
- PT.rtrait_ref_to_string fmt x
-
- let strait_ref_to_string (ctx : C.eval_ctx) (x : T.strait_ref) : string =
- let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_stype_formatter fmt in
- PT.strait_ref_to_string fmt x
-
- let etrait_instance_id_to_string (ctx : C.eval_ctx) (x : T.etrait_instance_id)
- : string =
- let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_etype_formatter fmt in
- PT.etrait_instance_id_to_string fmt x
-
- let rtrait_instance_id_to_string (ctx : C.eval_ctx) (x : T.rtrait_instance_id)
- : string =
- let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_rtype_formatter fmt in
- PT.rtrait_instance_id_to_string fmt x
-
- let strait_instance_id_to_string (ctx : C.eval_ctx) (x : T.strait_instance_id)
- : string =
+ let trait_instance_id_to_string (ctx : C.eval_ctx) (x : T.trait_instance_id) :
+ string =
let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_stype_formatter fmt in
- PT.strait_instance_id_to_string fmt x
+ let fmt = PC.ctx_to_type_formatter fmt in
+ PT.trait_instance_id_to_string fmt x
let borrow_content_to_string (ctx : C.eval_ctx) (bc : V.borrow_content) :
string =
@@ -743,7 +659,7 @@ module EvalCtxLlbcAst = struct
let symbolic_value_to_string (ctx : C.eval_ctx) (sv : V.symbolic_value) :
string =
let fmt = PC.eval_ctx_to_ctx_formatter ctx in
- let fmt = PC.ctx_to_rtype_formatter fmt in
+ let fmt = PC.ctx_to_type_formatter fmt in
PV.symbolic_value_to_string fmt sv
let typed_value_to_string (ctx : C.eval_ctx) (v : V.typed_value) : string =
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-10 23:17:50 +0000