summaryrefslogtreecommitdiff
path: root/compiler/PrintPure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/PrintPure.ml')
-rw-r--r--compiler/PrintPure.ml113
1 files changed, 78 insertions, 35 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 03252200..6f857b4f 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -6,11 +6,15 @@ open PureUtils
type type_formatter = {
type_var_id_to_string : TypeVarId.id -> string;
type_decl_id_to_string : TypeDeclId.id -> string;
+ const_generic_var_id_to_string : ConstGenericVarId.id -> string;
+ global_decl_id_to_string : GlobalDeclId.id -> string;
}
type value_formatter = {
type_var_id_to_string : TypeVarId.id -> string;
type_decl_id_to_string : TypeDeclId.id -> string;
+ const_generic_var_id_to_string : ConstGenericVarId.id -> string;
+ global_decl_id_to_string : GlobalDeclId.id -> string;
adt_variant_to_string : TypeDeclId.id -> VariantId.id -> string;
var_id_to_string : VarId.id -> string;
adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
@@ -20,6 +24,8 @@ let value_to_type_formatter (fmt : value_formatter) : type_formatter =
{
type_var_id_to_string = fmt.type_var_id_to_string;
type_decl_id_to_string = fmt.type_decl_id_to_string;
+ const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
+ global_decl_id_to_string = fmt.global_decl_id_to_string;
}
(* TODO: we need to store which variables we have encountered so far, and
@@ -28,6 +34,7 @@ let value_to_type_formatter (fmt : value_formatter) : type_formatter =
type ast_formatter = {
type_var_id_to_string : TypeVarId.id -> string;
type_decl_id_to_string : TypeDeclId.id -> string;
+ const_generic_var_id_to_string : ConstGenericVarId.id -> string;
adt_variant_to_string : TypeDeclId.id -> VariantId.id -> string;
var_id_to_string : VarId.id -> string;
adt_field_to_string :
@@ -41,6 +48,8 @@ let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
{
type_var_id_to_string = fmt.type_var_id_to_string;
type_decl_id_to_string = fmt.type_decl_id_to_string;
+ const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
+ global_decl_id_to_string = fmt.global_decl_id_to_string;
adt_variant_to_string = fmt.adt_variant_to_string;
var_id_to_string = fmt.var_id_to_string;
adt_field_names = fmt.adt_field_names;
@@ -55,22 +64,38 @@ let fun_name_to_string = Print.fun_name_to_string
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 const_generic_var_to_string = Print.Types.const_generic_var_to_string
let integer_type_to_string = Print.PrimitiveValues.integer_type_to_string
let literal_type_to_string = Print.PrimitiveValues.literal_type_to_string
let scalar_value_to_string = Print.PrimitiveValues.scalar_value_to_string
let literal_to_string = Print.PrimitiveValues.literal_to_string
let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
- (type_params : type_var list) : type_formatter =
+ (global_decls : A.global_decl GlobalDeclId.Map.t)
+ (type_params : type_var list)
+ (const_generic_params : const_generic_var list) : type_formatter =
let type_var_id_to_string vid =
let var = T.TypeVarId.nth type_params vid in
type_var_to_string var
in
+ let const_generic_var_id_to_string vid =
+ let var = T.ConstGenericVarId.nth const_generic_params vid in
+ const_generic_var_to_string var
+ in
let type_decl_id_to_string def_id =
let def = T.TypeDeclId.Map.find def_id type_decls in
name_to_string def.name
in
- { type_var_id_to_string; type_decl_id_to_string }
+ let global_decl_id_to_string def_id =
+ let def = T.GlobalDeclId.Map.find def_id global_decls in
+ name_to_string def.name
+ in
+ {
+ type_var_id_to_string;
+ type_decl_id_to_string;
+ const_generic_var_id_to_string;
+ global_decl_id_to_string;
+ }
(* TODO: there is a bit of duplication with Print.fun_decl_to_ast_formatter.
@@ -81,11 +106,16 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
(fun_decls : A.fun_decl FunDeclId.Map.t)
(global_decls : A.global_decl GlobalDeclId.Map.t)
- (type_params : type_var list) : ast_formatter =
+ (type_params : type_var list)
+ (const_generic_params : const_generic_var list) : ast_formatter =
let type_var_id_to_string vid =
let var = T.TypeVarId.nth type_params vid in
type_var_to_string var
in
+ let const_generic_var_id_to_string vid =
+ let var = T.ConstGenericVarId.nth const_generic_params vid in
+ const_generic_var_to_string var
+ in
let type_decl_id_to_string def_id =
let def = T.TypeDeclId.Map.find def_id type_decls in
name_to_string def.name
@@ -113,6 +143,7 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
in
{
type_var_id_to_string;
+ const_generic_var_id_to_string;
type_decl_id_to_string;
adt_variant_to_string;
var_id_to_string;
@@ -122,36 +153,50 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
global_decl_id_to_string;
}
+let assumed_ty_to_string (aty : assumed_ty) : string =
+ match aty with
+ | State -> "State"
+ | Result -> "Result"
+ | Error -> "Error"
+ | Fuel -> "Fuel"
+ | Option -> "Option"
+ | Vec -> "Vec"
+ | Array -> "Array"
+ | Slice -> "Slice"
+ | Str -> "Str"
+
let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
match id with
| AdtId id -> fmt.type_decl_id_to_string id
| Tuple -> ""
- | Assumed aty -> (
- match aty with
- | State -> "State"
- | Result -> "Result"
- | Error -> "Error"
- | Fuel -> "Fuel"
- | Option -> "Option"
- | Vec -> "Vec")
+ | Assumed aty -> assumed_ty_to_string aty
+
+(* TODO: duplicates Charon.PrintTypes.const_generic_to_string *)
+let const_generic_to_string (fmt : type_formatter) (cg : T.const_generic) :
+ string =
+ match cg with
+ | ConstGenericGlobal id -> fmt.global_decl_id_to_string id
+ | ConstGenericVar id -> fmt.const_generic_var_id_to_string id
+ | ConstGenericValue lit -> literal_to_string lit
let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string =
match ty with
- | Adt (id, tys) -> (
+ | Adt (id, tys, cgs) -> (
let tys = List.map (ty_to_string fmt false) tys in
+ let cgs = List.map (const_generic_to_string fmt) cgs in
+ let params = List.append tys cgs in
match id with
- | Tuple -> "(" ^ String.concat " * " tys ^ ")"
+ | Tuple ->
+ assert (cgs = []);
+ "(" ^ String.concat " * " tys ^ ")"
| AdtId _ | Assumed _ ->
- let tys_s = if tys = [] then "" else " " ^ String.concat " " tys in
- let ty_s = type_id_to_string fmt id ^ tys_s in
- if tys <> [] && inside then "(" ^ ty_s ^ ")" else ty_s)
+ let params_s =
+ if params = [] then "" else " " ^ String.concat " " params
+ in
+ let ty_s = type_id_to_string fmt id ^ params_s in
+ if params <> [] && inside then "(" ^ ty_s ^ ")" else ty_s)
| TypeVar tv -> fmt.type_var_id_to_string tv
- | Bool -> "bool"
- | Char -> "char"
- | Integer int_ty -> integer_type_to_string int_ty
- | Str -> "str"
- | Array aty -> "[" ^ ty_to_string fmt false aty ^ "; ?]"
- | Slice sty -> "[" ^ ty_to_string fmt false sty ^ "]"
+ | Literal lty -> literal_type_to_string lty
| Arrow (arg_ty, ret_ty) ->
let ty =
ty_to_string fmt true arg_ty ^ " -> " ^ ty_to_string fmt false ret_ty
@@ -248,8 +293,8 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
| Assumed aty -> (
(* Assumed type *)
match aty with
- | State ->
- (* This type is opaque: we can't get there *)
+ | State | Vec | Array | Slice | Str ->
+ (* Those types are opaque: we can't get there *)
raise (Failure "Unreachable")
| Result ->
let variant_id = Option.get variant_id in
@@ -272,10 +317,7 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
if variant_id = option_some_id then "@Option::Some "
else if variant_id = option_none_id then "@Option::None"
else
- raise (Failure "Unreachable: improper variant id for result type")
- | Vec ->
- assert (variant_id = None);
- "Vec")
+ raise (Failure "Unreachable: improper variant id for result type"))
let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
(field_id : FieldId.id) : string =
@@ -292,7 +334,7 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
| Assumed aty -> (
(* Assumed type *)
match aty with
- | State | Fuel | Vec ->
+ | State | Fuel | Vec | Array | Slice | Str ->
(* Opaque types: we can't get there *)
raise (Failure "Unreachable")
| Result | Error | Option ->
@@ -300,17 +342,17 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
raise (Failure "Unreachable"))
(** TODO: we don't need a general function anymore (it is now only used for
- patterns (i.e., patterns)
+ patterns)
*)
let adt_g_value_to_string (fmt : value_formatter)
(value_to_string : 'v -> string) (variant_id : VariantId.id option)
(field_values : 'v list) (ty : ty) : string =
let field_values = List.map value_to_string field_values in
match ty with
- | Adt (Tuple, _) ->
+ | Adt (Tuple, _, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | Adt (AdtId def_id, _) ->
+ | Adt (AdtId def_id, _, _) ->
(* "Regular" ADT *)
let adt_ident =
match variant_id with
@@ -332,7 +374,7 @@ let adt_g_value_to_string (fmt : value_formatter)
let field_values = String.concat " " field_values in
adt_ident ^ " { " ^ field_values ^ " }"
else adt_ident
- | Adt (Assumed aty, _) -> (
+ | Adt (Assumed aty, _, _) -> (
(* Assumed type *)
match aty with
| State ->
@@ -377,12 +419,13 @@ let adt_g_value_to_string (fmt : value_formatter)
"@Option::None")
else
raise (Failure "Unreachable: improper variant id for result type")
- | Vec ->
+ | Vec | Array | Slice | Str ->
assert (variant_id = None);
let field_values =
List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
in
- "Vec [" ^ String.concat "; " field_values ^ "]")
+ let id = assumed_ty_to_string aty in
+ id ^ " [" ^ String.concat "; " field_values ^ "]")
| _ ->
let fmt = value_to_type_formatter fmt in
raise
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 20:20:55 +0000