summaryrefslogtreecommitdiff
path: root/compiler/PrintPure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/PrintPure.ml')
-rw-r--r--compiler/PrintPure.ml709
1 files changed, 339 insertions, 370 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index cfb63ec2..5d8297d3 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -3,238 +3,251 @@
open Pure
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;
+(** The formatting context for pure definitions uses non-pure definitions
+ to lookup names. The main reason is that when building the pure definitions
+ like in [SymbolicToPure] we don't have a pure context available, while
+ at every stage we have the original LLBC definitions at hand.
+ *)
+type fmt_env = {
+ type_decls : Types.type_decl TypeDeclId.Map.t;
+ fun_decls : LlbcAst.fun_decl FunDeclId.Map.t;
+ global_decls : LlbcAst.global_decl GlobalDeclId.Map.t;
+ trait_decls : LlbcAst.trait_decl TraitDeclId.Map.t;
+ trait_impls : LlbcAst.trait_impl TraitImplId.Map.t;
+ generics : generic_params;
+ locals : (VarId.id * string option) list;
}
-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;
-}
+let var_id_to_pretty_string (id : var_id) : string = "v@" ^ VarId.to_string id
+
+let type_var_id_to_string (env : fmt_env) (id : type_var_id) : string =
+ (* Note that the types are not necessarily ordered following their indices *)
+ match
+ List.find_opt (fun (x : type_var) -> x.index = id) env.generics.types
+ with
+ | None -> Print.Types.type_var_id_to_pretty_string id
+ | Some x -> Print.Types.type_var_to_string x
-let value_to_type_formatter (fmt : value_formatter) : type_formatter =
+let const_generic_var_id_to_string (env : fmt_env) (id : const_generic_var_id) :
+ string =
+ (* Note that the regions are not necessarily ordered following their indices *)
+ match
+ List.find_opt
+ (fun (x : const_generic_var) -> x.index = id)
+ env.generics.const_generics
+ with
+ | None -> Print.Types.const_generic_var_id_to_pretty_string id
+ | Some x -> Print.Types.const_generic_var_to_string x
+
+let var_id_to_string (env : fmt_env) (id : VarId.id) : string =
+ match List.find_opt (fun (i, _) -> i = id) env.locals with
+ | None -> var_id_to_pretty_string id
+ | Some (_, name) -> (
+ match name with
+ | None -> var_id_to_pretty_string id
+ | Some name -> name ^ "^" ^ VarId.to_string id)
+
+let trait_clause_id_to_string = Print.Types.trait_clause_id_to_string
+
+let fmt_env_to_llbc_fmt_env (env : fmt_env) : Print.fmt_env =
{
- 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;
+ type_decls = env.type_decls;
+ fun_decls = env.fun_decls;
+ global_decls = env.global_decls;
+ trait_decls = env.trait_decls;
+ trait_impls = env.trait_impls;
+ generics = TypesUtils.empty_generic_params;
+ preds = TypesUtils.empty_predicates;
+ locals = [];
}
-(* TODO: we need to store which variables we have encountered so far, and
- remove [var_id_to_string].
-*)
-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 :
- TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option;
- adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
- fun_decl_id_to_string : FunDeclId.id -> string;
- global_decl_id_to_string : GlobalDeclId.id -> string;
-}
-
-let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
+let decls_ctx_to_fmt_env (ctx : Contexts.decls_ctx) : fmt_env =
{
- 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;
+ type_decls = ctx.type_ctx.type_decls;
+ fun_decls = ctx.fun_ctx.fun_decls;
+ global_decls = ctx.global_ctx.global_decls;
+ trait_decls = ctx.trait_decls_ctx.trait_decls;
+ trait_impls = ctx.trait_impls_ctx.trait_impls;
+ generics = empty_generic_params;
+ locals = [];
}
-let ast_to_type_formatter (fmt : ast_formatter) : type_formatter =
- let fmt = ast_to_value_formatter fmt in
- value_to_type_formatter fmt
+let name_to_string (env : fmt_env) =
+ Print.Types.name_to_string (fmt_env_to_llbc_fmt_env env)
+
+let type_decl_id_to_string (env : fmt_env) =
+ Print.Types.type_decl_id_to_string (fmt_env_to_llbc_fmt_env env)
+
+let global_decl_id_to_string (env : fmt_env) =
+ Print.Types.global_decl_id_to_string (fmt_env_to_llbc_fmt_env env)
+
+let fun_decl_id_to_string (env : fmt_env) =
+ Print.Expressions.fun_decl_id_to_string (fmt_env_to_llbc_fmt_env env)
+
+let trait_decl_id_to_string (env : fmt_env) =
+ Print.Types.trait_decl_id_to_string (fmt_env_to_llbc_fmt_env env)
+
+let trait_impl_id_to_string (env : fmt_env) =
+ Print.Types.trait_impl_id_to_string (fmt_env_to_llbc_fmt_env env)
+
+let adt_field_to_string (env : fmt_env) =
+ Print.Types.adt_field_to_string (fmt_env_to_llbc_fmt_env env)
+
+let adt_variant_from_type_decl_id_to_string (env : fmt_env) =
+ Print.Types.adt_variant_to_string (fmt_env_to_llbc_fmt_env env)
+
+let adt_field_names (env : fmt_env) =
+ Print.Types.adt_field_names (fmt_env_to_llbc_fmt_env env)
-let name_to_string = Print.name_to_string
-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)
- (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
- 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.
-
- TODO: use the pure defs as inputs? Note that it is a bit annoying for the
- functions (there is a difference between the forward/backward functions...)
- while we only need those definitions to lookup proper names for the def ids.
-*)
-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)
- (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
- in
- let adt_variant_to_string =
- 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.Types.type_ctx_to_adt_field_names_fun type_decls
- in
- let adt_field_to_string =
- 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
- fun_name_to_string def.name
- in
- let global_decl_id_to_string def_id =
- let def = GlobalDeclId.Map.find def_id global_decls in
- global_name_to_string def.name
- 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;
- adt_field_names;
- adt_field_to_string;
- fun_decl_id_to_string;
- global_decl_id_to_string;
- }
+let integer_type_to_string = Print.Values.integer_type_to_string
+let literal_type_to_string = Print.Values.literal_type_to_string
+let scalar_value_to_string = Print.Values.scalar_value_to_string
+let literal_to_string = Print.Values.literal_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"
- | Range -> "Range"
-
-let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
+ | TState -> "State"
+ | TResult -> "Result"
+ | TError -> "Error"
+ | TFuel -> "Fuel"
+ | TArray -> "Array"
+ | TSlice -> "Slice"
+ | TStr -> "Str"
+ | TRawPtr Mut -> "MutRawPtr"
+ | TRawPtr Const -> "ConstRawPtr"
+
+let type_id_to_string (env : fmt_env) (id : type_id) : string =
match id with
- | AdtId id -> fmt.type_decl_id_to_string id
- | Tuple -> ""
- | Assumed aty -> assumed_ty_to_string aty
+ | TAdtId id -> type_decl_id_to_string env id
+ | TTuple -> ""
+ | TAssumed 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 =
+let const_generic_to_string (env : fmt_env) (cg : 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
+ | CgGlobal id -> global_decl_id_to_string env id
+ | CgVar id -> const_generic_var_id_to_string env id
+ | CgValue lit -> literal_to_string lit
-let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string =
+let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
match ty with
- | 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
+ | TAdt (id, generics) -> (
match id with
- | Tuple ->
- assert (cgs = []);
- "(" ^ String.concat " * " tys ^ ")"
- | AdtId _ | Assumed _ ->
- let params_s =
- if params = [] then "" else " " ^ String.concat " " params
+ | TTuple ->
+ let generics = generic_args_to_strings env false generics in
+ "(" ^ String.concat " * " generics ^ ")"
+ | TAdtId _ | TAssumed _ ->
+ let generics = generic_args_to_strings env true generics in
+ let generics_s =
+ if generics = [] then "" else " " ^ String.concat " " generics
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
- | Literal lty -> literal_type_to_string lty
- | Arrow (arg_ty, ret_ty) ->
+ let ty_s = type_id_to_string env id ^ generics_s in
+ if generics <> [] && inside then "(" ^ ty_s ^ ")" else ty_s)
+ | TVar tv -> type_var_id_to_string env tv
+ | TLiteral lty -> literal_type_to_string lty
+ | TArrow (arg_ty, ret_ty) ->
let ty =
- ty_to_string fmt true arg_ty ^ " -> " ^ ty_to_string fmt false ret_ty
+ ty_to_string env true arg_ty ^ " -> " ^ ty_to_string env false ret_ty
in
if inside then "(" ^ ty ^ ")" else ty
+ | TTraitType (trait_ref, generics, type_name) ->
+ let trait_ref = trait_ref_to_string env false trait_ref in
+ let s =
+ if generics = empty_generic_args then trait_ref ^ "::" ^ type_name
+ else
+ let generics = generic_args_to_string env generics in
+ "(" ^ trait_ref ^ " " ^ generics ^ ")::" ^ type_name
+ in
+ if inside then "(" ^ s ^ ")" else s
+
+and generic_args_to_strings (env : fmt_env) (inside : bool)
+ (generics : generic_args) : string list =
+ let tys = List.map (ty_to_string env inside) generics.types in
+ let cgs = List.map (const_generic_to_string env) generics.const_generics in
+ let trait_refs =
+ List.map (trait_ref_to_string env inside) generics.trait_refs
+ in
+ List.concat [ tys; cgs; trait_refs ]
+
+and generic_args_to_string (env : fmt_env) (generics : generic_args) : string =
+ String.concat " " (generic_args_to_strings env true generics)
-let field_to_string fmt inside (f : field) : string =
+and trait_ref_to_string (env : fmt_env) (inside : bool) (tr : trait_ref) :
+ string =
+ let trait_id = trait_instance_id_to_string env false tr.trait_id in
+ let generics = generic_args_to_string env tr.generics in
+ let s = trait_id ^ generics in
+ if tr.generics = empty_generic_args || not inside then s else "(" ^ s ^ ")"
+
+and trait_instance_id_to_string (env : fmt_env) (inside : bool)
+ (id : trait_instance_id) : string =
+ match id with
+ | Self -> "Self"
+ | TraitImpl id -> trait_impl_id_to_string env id
+ | Clause id -> trait_clause_id_to_string env id
+ | ParentClause (inst_id, _decl_id, clause_id) ->
+ let inst_id = trait_instance_id_to_string env false inst_id in
+ let clause_id = trait_clause_id_to_string env clause_id in
+ "parent(" ^ inst_id ^ ")::" ^ clause_id
+ | ItemClause (inst_id, _decl_id, item_name, clause_id) ->
+ let inst_id = trait_instance_id_to_string env false inst_id in
+ let clause_id = trait_clause_id_to_string env clause_id in
+ "(" ^ inst_id ^ ")::" ^ item_name ^ "::[" ^ clause_id ^ "]"
+ | TraitRef tr -> trait_ref_to_string env inside tr
+ | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")"
+
+let trait_clause_to_string (env : fmt_env) (clause : trait_clause) : string =
+ let clause_id = trait_clause_id_to_string env clause.clause_id in
+ let trait_id = trait_decl_id_to_string env clause.trait_id in
+ let generics = generic_args_to_strings env true clause.generics in
+ let generics =
+ if generics = [] then "" else " " ^ String.concat " " generics
+ in
+ "[" ^ clause_id ^ "]: " ^ trait_id ^ generics
+
+let generic_params_to_strings (env : fmt_env) (generics : generic_params) :
+ string list =
+ let tys = List.map type_var_to_string generics.types in
+ let cgs = List.map const_generic_var_to_string generics.const_generics in
+ let trait_clauses =
+ List.map (trait_clause_to_string env) generics.trait_clauses
+ in
+ List.concat [ tys; cgs; trait_clauses ]
+
+let field_to_string env inside (f : field) : string =
match f.field_name with
- | None -> ty_to_string fmt inside f.field_ty
+ | None -> ty_to_string env inside f.field_ty
| Some field_name ->
- let s = field_name ^ " : " ^ ty_to_string fmt false f.field_ty in
+ let s = field_name ^ " : " ^ ty_to_string env false f.field_ty in
if inside then "(" ^ s ^ ")" else s
-let variant_to_string fmt (v : variant) : string =
+let variant_to_string env (v : variant) : string =
v.variant_name ^ "("
- ^ String.concat ", " (List.map (field_to_string fmt false) v.fields)
+ ^ String.concat ", " (List.map (field_to_string env false) v.fields)
^ ")"
-let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string =
- let types = def.type_params in
- let name = name_to_string def.name in
+let type_decl_to_string (env : fmt_env) (def : type_decl) : string =
+ let env = { env with generics = def.generics } in
+ let name = def.name in
let params =
- if types = [] then ""
- else " " ^ String.concat " " (List.map type_var_to_string types)
+ if def.generics = empty_generic_params then ""
+ else " " ^ String.concat " " (generic_params_to_strings env def.generics)
in
match def.kind with
| Struct fields ->
if List.length fields > 0 then
let fields =
String.concat ","
- (List.map (fun f -> "\n " ^ field_to_string fmt false f) fields)
+ (List.map (fun f -> "\n " ^ field_to_string env false f) fields)
in
"struct " ^ name ^ params ^ "{" ^ fields ^ "}"
else "struct " ^ name ^ params ^ "{}"
| Enum variants ->
let variants =
- List.map (fun v -> "| " ^ variant_to_string fmt v) variants
+ List.map (fun v -> "| " ^ variant_to_string env v) variants
in
let variants = String.concat "\n" variants in
"enum " ^ name ^ params ^ " =\n" ^ variants
@@ -245,126 +258,115 @@ let var_to_varname (v : var) : string =
| Some name -> name ^ "^" ^ VarId.to_string v.id
| None -> "^" ^ VarId.to_string v.id
-let var_to_string (fmt : type_formatter) (v : var) : string =
+let var_to_string (env : fmt_env) (v : var) : string =
let varname = var_to_varname v in
- "(" ^ varname ^ " : " ^ ty_to_string fmt false v.ty ^ ")"
+ "(" ^ varname ^ " : " ^ ty_to_string env false v.ty ^ ")"
-let rec mprojection_to_string (fmt : ast_formatter) (inside : string)
+let rec mprojection_to_string (env : fmt_env) (inside : string)
(p : mprojection) : string =
match p with
| [] -> inside
| pe :: p' -> (
- let s = mprojection_to_string fmt inside p' in
+ let s = mprojection_to_string env inside p' in
match pe.pkind with
- | E.ProjOption variant_id ->
- assert (variant_id = T.option_some_id);
- assert (pe.field_id = T.FieldId.zero);
- "(" ^ s ^ "as Option::Some)." ^ T.FieldId.to_string pe.field_id
| E.ProjTuple _ -> "(" ^ s ^ ")." ^ T.FieldId.to_string pe.field_id
| E.ProjAdt (adt_id, opt_variant_id) -> (
let field_name =
- match fmt.adt_field_to_string adt_id opt_variant_id pe.field_id with
+ match adt_field_to_string env adt_id opt_variant_id pe.field_id with
| Some field_name -> field_name
| None -> T.FieldId.to_string pe.field_id
in
match opt_variant_id with
| None -> "(" ^ s ^ ")." ^ field_name
| Some variant_id ->
- let variant_name = fmt.adt_variant_to_string adt_id variant_id in
+ let variant_name =
+ adt_variant_from_type_decl_id_to_string env adt_id variant_id
+ in
"(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
-let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
+let mplace_to_string (env : fmt_env) (p : mplace) : string =
let name = match p.name with None -> "" | Some name -> name in
(* We add the "llbc" suffix to the variable index, because meta-places
* use indices of the variables in the original LLBC program, while
* regular places use indices for the pure variables: we want to make
* this explicit, otherwise it is confusing. *)
let name = name ^ "^" ^ E.VarId.to_string p.var_id ^ "llbc" in
- mprojection_to_string fmt name p.projection
+ mprojection_to_string env name p.projection
-let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
+let adt_variant_to_string (env : fmt_env) (adt_id : type_id)
(variant_id : VariantId.id option) : string =
match adt_id with
- | Tuple -> "Tuple"
- | AdtId def_id -> (
+ | TTuple -> "Tuple"
+ | TAdtId def_id -> (
(* "Regular" ADT *)
match variant_id with
- | Some vid -> fmt.adt_variant_to_string def_id vid
- | None -> fmt.type_decl_id_to_string def_id)
- | Assumed aty -> (
+ | Some vid -> adt_variant_from_type_decl_id_to_string env def_id vid
+ | None -> type_decl_id_to_string env def_id)
+ | TAssumed aty -> (
(* Assumed type *)
match aty with
- | State | Array | Slice | Str ->
+ | TState | TArray | TSlice | TStr | TRawPtr _ ->
(* Those types are opaque: we can't get there *)
raise (Failure "Unreachable")
- | Vec -> "@Vec"
- | Range -> "@Range"
- | Result ->
+ | TResult ->
let variant_id = Option.get variant_id in
if variant_id = result_return_id then "@Result::Return"
else if variant_id = result_fail_id then "@Result::Fail"
else
raise (Failure "Unreachable: improper variant id for result type")
- | Error ->
+ | TError ->
let variant_id = Option.get variant_id in
if variant_id = error_failure_id then "@Error::Failure"
else if variant_id = error_out_of_fuel_id then "@Error::OutOfFuel"
else raise (Failure "Unreachable: improper variant id for error type")
- | Fuel ->
+ | TFuel ->
let variant_id = Option.get variant_id in
if variant_id = fuel_zero_id then "@Fuel::Zero"
else if variant_id = fuel_succ_id then "@Fuel::Succ"
- else raise (Failure "Unreachable: improper variant id for fuel type")
- | Option ->
- let variant_id = Option.get variant_id in
- 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"))
+ else raise (Failure "Unreachable: improper variant id for fuel type"))
-let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
+let adt_field_to_string (env : fmt_env) (adt_id : type_id)
(field_id : FieldId.id) : string =
match adt_id with
- | Tuple ->
+ | TTuple ->
raise (Failure "Unreachable")
(* Tuples don't use the opaque field id for the field indices, but [int] *)
- | AdtId def_id -> (
+ | TAdtId def_id -> (
(* "Regular" ADT *)
- let fields = fmt.adt_field_names def_id None in
+ let fields = adt_field_names env def_id None in
match fields with
| None -> FieldId.to_string field_id
| Some fields -> FieldId.nth fields field_id)
- | Assumed aty -> (
+ | TAssumed aty -> (
(* Assumed type *)
match aty with
- | Range -> FieldId.to_string field_id
- | State | Fuel | Vec | Array | Slice | Str ->
+ | TState | TFuel | TArray | TSlice | TStr ->
(* Opaque types: we can't get there *)
raise (Failure "Unreachable")
- | Result | Error | Option ->
+ | TResult | TError | TRawPtr _ ->
(* Enumerations: we can't get there *)
raise (Failure "Unreachable"))
(** TODO: we don't need a general function anymore (it is now only used for
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 adt_g_value_to_string (env : fmt_env) (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, _, _) ->
+ | TAdt (TTuple, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | Adt (AdtId def_id, _, _) ->
+ | TAdt (TAdtId def_id, _) ->
(* "Regular" ADT *)
let adt_ident =
match variant_id with
- | Some vid -> fmt.adt_variant_to_string def_id vid
- | None -> fmt.type_decl_id_to_string def_id
+ | Some vid -> adt_variant_from_type_decl_id_to_string env def_id vid
+ | None -> type_decl_id_to_string env def_id
in
if field_values <> [] then
- match fmt.adt_field_names def_id variant_id with
+ match adt_field_names env def_id variant_id with
| None ->
let field_values = String.concat ", " field_values in
adt_ident ^ " (" ^ field_values ^ ")"
@@ -378,13 +380,13 @@ 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, _, _) -> (
+ | TAdt (TAssumed aty, _) -> (
(* Assumed type *)
match aty with
- | State ->
+ | TState | TRawPtr _ ->
(* This type is opaque: we can't get there *)
raise (Failure "Unreachable")
- | Result ->
+ | TResult ->
let variant_id = Option.get variant_id in
if variant_id = result_return_id then
match field_values with
@@ -396,13 +398,13 @@ let adt_g_value_to_string (fmt : value_formatter)
| _ -> raise (Failure "Result::Fail takes exactly one value")
else
raise (Failure "Unreachable: improper variant id for result type")
- | Error ->
+ | TError ->
assert (field_values = []);
let variant_id = Option.get variant_id in
if variant_id = error_failure_id then "@Error::Failure"
else if variant_id = error_out_of_fuel_id then "@Error::OutOfFuel"
else raise (Failure "Unreachable: improper variant id for error type")
- | Fuel ->
+ | TFuel ->
let variant_id = Option.get variant_id in
if variant_id = fuel_zero_id then (
assert (field_values = []);
@@ -412,68 +414,46 @@ let adt_g_value_to_string (fmt : value_formatter)
| [ v ] -> "@Fuel::Succ " ^ v
| _ -> raise (Failure "@Fuel::Succ takes exactly one value")
else raise (Failure "Unreachable: improper variant id for fuel type")
- | Option ->
- let variant_id = Option.get variant_id in
- if variant_id = option_some_id then
- match field_values with
- | [ v ] -> "@Option::Some " ^ v
- | _ -> raise (Failure "Option::Some takes exactly one value")
- else if variant_id = option_none_id then (
- assert (field_values = []);
- "@Option::None")
- else
- raise (Failure "Unreachable: improper variant id for result type")
- | Vec | Array | Slice | Str ->
- assert (variant_id = None);
- let field_values =
- List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
- in
- let id = assumed_ty_to_string aty in
- id ^ " [" ^ String.concat "; " field_values ^ "]"
- | Range ->
+ | TArray | TSlice | TStr ->
assert (variant_id = None);
let field_values =
List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
in
let id = assumed_ty_to_string aty in
- id ^ " {" ^ String.concat "; " field_values ^ "}")
+ id ^ " [" ^ String.concat "; " field_values ^ "]")
| _ ->
- let fmt = value_to_type_formatter fmt in
raise
(Failure
("Inconsistently typed value: expected ADT type but found:"
- ^ "\n- ty: " ^ ty_to_string fmt false ty ^ "\n- variant_id: "
+ ^ "\n- ty: " ^ ty_to_string env false ty ^ "\n- variant_id: "
^ Print.option_to_string VariantId.to_string variant_id))
-let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
- string =
+let rec typed_pattern_to_string (env : fmt_env) (v : typed_pattern) : string =
match v.value with
| PatConstant cv -> literal_to_string cv
- | PatVar (v, None) -> var_to_string (ast_to_type_formatter fmt) v
+ | PatVar (v, None) -> var_to_string env v
| PatVar (v, Some mp) ->
- let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in
+ let mp = "[@mplace=" ^ mplace_to_string env mp ^ "]" in
"(" ^ var_to_varname v ^ " " ^ mp ^ " : "
- ^ ty_to_string (ast_to_type_formatter fmt) false v.ty
+ ^ ty_to_string env false v.ty
^ ")"
| PatDummy -> "_"
| PatAdt av ->
- adt_g_value_to_string
- (ast_to_value_formatter fmt)
- (typed_pattern_to_string fmt)
+ adt_g_value_to_string env
+ (typed_pattern_to_string env)
av.variant_id av.field_values v.ty
-let fun_sig_to_string (fmt : ast_formatter) (sg : fun_sig) : string =
- let ty_fmt = ast_to_type_formatter fmt in
- let type_params = List.map type_var_to_string sg.type_params in
- let inputs = List.map (ty_to_string ty_fmt false) sg.inputs in
- let output = ty_to_string ty_fmt false sg.output in
- let all_types = List.concat [ type_params; inputs; [ output ] ] in
+let fun_sig_to_string (env : fmt_env) (sg : fun_sig) : string =
+ let env = { env with generics = sg.generics } in
+ let generics = generic_params_to_strings env sg.generics in
+ let inputs = List.map (ty_to_string env false) sg.inputs in
+ let output = ty_to_string env false sg.output in
+ let all_types = List.concat [ generics; inputs; [ output ] ] in
String.concat " -> " all_types
-let inst_fun_sig_to_string (fmt : ast_formatter) (sg : inst_fun_sig) : string =
- let ty_fmt = ast_to_type_formatter fmt in
- let inputs = List.map (ty_to_string ty_fmt false) sg.inputs in
- let output = ty_to_string ty_fmt false sg.output in
+let inst_fun_sig_to_string (env : fmt_env) (sg : inst_fun_sig) : string =
+ let inputs = List.map (ty_to_string env false) sg.inputs in
+ let output = ty_to_string env false sg.output in
let all_types = List.append inputs [ output ] in
String.concat " -> " all_types
@@ -495,28 +475,20 @@ let fun_suffix (lp_id : LoopId.id option) (rg_id : T.RegionGroupId.id option) :
let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
match fid with
- | A.Replace -> "core::mem::replace"
- | 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"
- | A.VecNew -> "alloc::vec::Vec::new"
- | A.VecPush -> "alloc::vec::Vec::push"
- | A.VecInsert -> "alloc::vec::Vec::insert"
- | A.VecLen -> "alloc::vec::Vec::len"
- | A.VecIndex -> "core::ops::index::Index<alloc::vec::Vec>::index"
- | A.VecIndexMut -> "core::ops::index::IndexMut<alloc::vec::Vec>::index_mut"
+ | BoxNew -> "alloc::boxed::Box::new"
+ | BoxFree -> "alloc::alloc::box_free"
| ArrayIndexShared -> "@ArrayIndexShared"
| ArrayIndexMut -> "@ArrayIndexMut"
| ArrayToSliceShared -> "@ArrayToSliceShared"
| ArrayToSliceMut -> "@ArrayToSliceMut"
- | ArraySubsliceShared -> "@ArraySubsliceShared"
- | ArraySubsliceMut -> "@ArraySubsliceMut"
- | SliceLen -> "@SliceLen"
+ | ArrayRepeat -> "@ArrayRepeat"
| SliceIndexShared -> "@SliceIndexShared"
| SliceIndexMut -> "@SliceIndexMut"
- | SliceSubsliceShared -> "@SliceSubsliceShared"
- | SliceSubsliceMut -> "@SliceSubsliceMut"
+
+let llbc_fun_id_to_string (env : fmt_env) (fid : A.fun_id) : string =
+ match fid with
+ | FRegular fid -> fun_decl_id_to_string env fid
+ | FAssumed fid -> llbc_assumed_fun_id_to_string fid
let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string =
match fid with
@@ -526,13 +498,15 @@ let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string =
| FuelDecrease -> "fuel_decrease"
| FuelEqZero -> "fuel_eq_zero"
-let regular_fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string =
+let regular_fun_id_to_string (env : fmt_env) (fun_id : fun_id) : string =
match fun_id with
| FromLlbc (fid, lp_id, rg_id) ->
let f =
match fid with
- | Regular fid -> fmt.fun_decl_id_to_string fid
- | Assumed fid -> llbc_assumed_fun_id_to_string fid
+ | FunId (FRegular fid) -> fun_decl_id_to_string env fid
+ | FunId (FAssumed fid) -> llbc_assumed_fun_id_to_string fid
+ | TraitMethod (trait_ref, method_name, _) ->
+ trait_ref_to_string env true trait_ref ^ "." ^ method_name
in
f ^ fun_suffix lp_id rg_id
| Pure fid -> pure_assumed_fun_id_to_string fid
@@ -547,123 +521,124 @@ let unop_to_string (unop : unop) : string =
let binop_to_string = Print.Expressions.binop_to_string
-let fun_or_op_id_to_string (fmt : ast_formatter) (fun_id : fun_or_op_id) :
- string =
+let fun_or_op_id_to_string (env : fmt_env) (fun_id : fun_or_op_id) : string =
match fun_id with
- | Fun fun_id -> regular_fun_id_to_string fmt fun_id
+ | Fun fun_id -> regular_fun_id_to_string env fun_id
| Unop unop -> unop_to_string unop
| Binop (binop, int_ty) ->
binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">"
(** [inside]: controls the introduction of parentheses *)
-let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
- (indent : string) (indent_incr : string) (e : texpression) : string =
+let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string)
+ (indent_incr : string) (e : texpression) : string =
match e.e with
- | Var var_id ->
- let s = fmt.var_id_to_string var_id in
- if inside then "(" ^ s ^ ")" else s
+ | Var var_id -> var_id_to_string env var_id
+ | CVar cg_id -> const_generic_var_id_to_string env cg_id
| Const cv -> literal_to_string cv
| App _ ->
(* Recursively destruct the app, to have a pair (app, arguments list) *)
let app, args = destruct_apps e in
(* Convert to string *)
- app_to_string fmt inside indent indent_incr app args
+ app_to_string env inside indent indent_incr app args
| Abs _ ->
let xl, e = destruct_abs_list e in
- let e = abs_to_string fmt indent indent_incr xl e in
+ let e = abs_to_string env indent indent_incr xl e in
if inside then "(" ^ e ^ ")" else e
| Qualif _ ->
(* Qualifier without arguments *)
- app_to_string fmt inside indent indent_incr e []
+ app_to_string env inside indent indent_incr e []
| Let (monadic, lv, re, e) ->
- let e = let_to_string fmt indent indent_incr monadic lv re e in
+ let e = let_to_string env indent indent_incr monadic lv re e in
if inside then "(" ^ e ^ ")" else e
| Switch (scrutinee, body) ->
- let e = switch_to_string fmt indent indent_incr scrutinee body in
+ let e = switch_to_string env indent indent_incr scrutinee body in
if inside then "(" ^ e ^ ")" else e
| Loop loop ->
- let e = loop_to_string fmt indent indent_incr loop in
+ let e = loop_to_string env indent indent_incr loop in
if inside then "(" ^ e ^ ")" else e
| StructUpdate supd -> (
let s =
match supd.init with
| None -> ""
- | Some vid -> " " ^ fmt.var_id_to_string vid ^ " with"
+ | Some vid -> " " ^ var_id_to_string env vid ^ " with"
in
let indent1 = indent ^ indent_incr in
let indent2 = indent1 ^ indent_incr in
(* The id should be a custom type decl id or an array *)
match supd.struct_id with
- | AdtId aid ->
- let field_names = Option.get (fmt.adt_field_names aid None) in
+ | TAdtId aid ->
+ let field_names = Option.get (adt_field_names env aid None) in
let fields =
List.map
(fun (fid, fe) ->
let field = FieldId.nth field_names fid in
let fe =
- texpression_to_string fmt false indent2 indent_incr fe
+ texpression_to_string env false indent2 indent_incr fe
in
"\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";")
supd.updates
in
let bl = if fields = [] then "" else "\n" ^ indent in
"{" ^ s ^ String.concat "" fields ^ bl ^ "}"
- | Assumed Array ->
+ | TAssumed TArray ->
let fields =
List.map
(fun (_, fe) ->
- texpression_to_string fmt false indent2 indent_incr fe)
+ texpression_to_string env false indent2 indent_incr fe)
supd.updates
in
"[ " ^ String.concat ", " fields ^ " ]"
| _ -> raise (Failure "Unexpected"))
| Meta (meta, e) -> (
- let meta_s = meta_to_string fmt meta in
- let e = texpression_to_string fmt inside indent indent_incr e in
+ let meta_s = emeta_to_string env meta in
+ let e = texpression_to_string env inside indent indent_incr e in
match meta with
| Assignment _ | SymbolicAssignment _ | Tag _ ->
let e = meta_s ^ "\n" ^ indent ^ e in
if inside then "(" ^ e ^ ")" else e
| MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
-and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
+and app_to_string (env : fmt_env) (inside : bool) (indent : string)
(indent_incr : string) (app : texpression) (args : texpression list) :
string =
(* There are two possibilities: either the [app] is an instantiated,
* top-level qualifier (function, ADT constructore...), or it is a "regular"
* expression *)
- let app, tys =
+ let app, generics =
match app.e with
| Qualif qualif ->
(* Qualifier case *)
(* Convert the qualifier identifier *)
let qualif_s =
match qualif.id with
- | FunOrOp fun_id -> fun_or_op_id_to_string fmt fun_id
- | Global global_id -> fmt.global_decl_id_to_string global_id
+ | FunOrOp fun_id -> fun_or_op_id_to_string env fun_id
+ | Global global_id -> global_decl_id_to_string env global_id
| AdtCons adt_cons_id ->
let variant_s =
- adt_variant_to_string
- (ast_to_value_formatter fmt)
- adt_cons_id.adt_id adt_cons_id.variant_id
+ adt_variant_to_string env adt_cons_id.adt_id
+ adt_cons_id.variant_id
in
ConstStrings.constructor_prefix ^ variant_s
| Proj { adt_id; field_id } ->
- let value_fmt = ast_to_value_formatter fmt in
- let adt_s = adt_variant_to_string value_fmt adt_id None in
- let field_s = adt_field_to_string value_fmt adt_id field_id in
+ let adt_s = adt_variant_to_string env adt_id None in
+ let field_s = adt_field_to_string env adt_id field_id in
(* Adopting an F*-like syntax *)
ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s
+ | TraitConst (trait_ref, generics, const_name) ->
+ let trait_ref = trait_ref_to_string env true trait_ref in
+ let generics_s = generic_args_to_string env generics in
+ if generics <> empty_generic_args then
+ "(" ^ trait_ref ^ generics_s ^ ")." ^ const_name
+ else trait_ref ^ "." ^ const_name
in
(* Convert the type instantiation *)
- let ty_fmt = ast_to_type_formatter fmt in
- let tys = List.map (ty_to_string ty_fmt true) qualif.type_args in
+ let generics = generic_args_to_strings env true qualif.generics in
(* *)
- (qualif_s, tys)
+ (qualif_s, generics)
| _ ->
(* "Regular" expression case *)
let inside = args <> [] || (args = [] && inside) in
- (texpression_to_string fmt inside indent indent_incr app, [])
+ (texpression_to_string env inside indent indent_incr app, [])
in
(* Convert the arguments.
* The arguments are expressions, so indentation might get weird... (though
@@ -671,10 +646,10 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
let arg_to_string =
let inside = true in
let indent1 = indent ^ indent_incr in
- texpression_to_string fmt inside indent1 indent_incr
+ texpression_to_string env inside indent1 indent_incr
in
let args = List.map arg_to_string args in
- let all_args = List.append tys args in
+ let all_args = List.append generics args in
(* Put together *)
let e =
if all_args = [] then app else app ^ " " ^ String.concat " " all_args
@@ -682,32 +657,31 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
(* Add parentheses *)
if all_args <> [] && inside then "(" ^ e ^ ")" else e
-and abs_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
+and abs_to_string (env : fmt_env) (indent : string) (indent_incr : string)
(xl : typed_pattern list) (e : texpression) : string =
- let xl = List.map (typed_pattern_to_string fmt) xl in
- let e = texpression_to_string fmt false indent indent_incr e in
+ let xl = List.map (typed_pattern_to_string env) xl in
+ let e = texpression_to_string env false indent indent_incr e in
"λ " ^ String.concat " " xl ^ ". " ^ e
-and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
+and let_to_string (env : fmt_env) (indent : string) (indent_incr : string)
(monadic : bool) (lv : typed_pattern) (re : texpression) (e : texpression) :
string =
let indent1 = indent ^ indent_incr in
let inside = false in
- let re = texpression_to_string fmt inside indent1 indent_incr re in
- let e = texpression_to_string fmt inside indent indent_incr e in
- let lv = typed_pattern_to_string fmt lv in
+ let re = texpression_to_string env inside indent1 indent_incr re in
+ let e = texpression_to_string env inside indent indent_incr e in
+ let lv = typed_pattern_to_string env lv in
if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e
else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e
-and switch_to_string (fmt : ast_formatter) (indent : string)
- (indent_incr : string) (scrutinee : texpression) (body : switch_body) :
- string =
+and switch_to_string (env : fmt_env) (indent : string) (indent_incr : string)
+ (scrutinee : texpression) (body : switch_body) : string =
let indent1 = indent ^ indent_incr in
(* Printing can mess up on the scrutinee, because it is an expression - but
* in most situations it will be a value or a function call, so it should be
* ok*)
- let scrut = texpression_to_string fmt true indent1 indent_incr scrutinee in
- let e_to_string = texpression_to_string fmt false indent1 indent_incr in
+ let scrut = texpression_to_string env true indent1 indent_incr scrutinee in
+ let e_to_string = texpression_to_string env false indent1 indent_incr in
match body with
| If (e_true, e_false) ->
let e_true = e_to_string e_true in
@@ -716,79 +690,74 @@ and switch_to_string (fmt : ast_formatter) (indent : string)
^ indent ^ "else\n" ^ indent1 ^ e_false
| Match branches ->
let branch_to_string (b : match_branch) : string =
- let pat = typed_pattern_to_string fmt b.pat in
+ let pat = typed_pattern_to_string env b.pat in
indent ^ "| " ^ pat ^ " ->\n" ^ indent1 ^ e_to_string b.branch
in
let branches = List.map branch_to_string branches in
"match " ^ scrut ^ " with\n" ^ String.concat "\n" branches
-and loop_to_string (fmt : ast_formatter) (indent : string)
- (indent_incr : string) (loop : loop) : string =
+and loop_to_string (env : fmt_env) (indent : string) (indent_incr : string)
+ (loop : loop) : string =
let indent1 = indent ^ indent_incr in
let indent2 = indent1 ^ indent_incr in
- let type_fmt = ast_to_type_formatter fmt in
let loop_inputs =
"fresh_vars: ["
- ^ String.concat "; " (List.map (var_to_string type_fmt) loop.inputs)
+ ^ String.concat "; " (List.map (var_to_string env) loop.inputs)
^ "]"
in
let back_output_tys =
let tys =
match loop.back_output_tys with
| None -> ""
- | Some tys ->
- String.concat "; "
- (List.map (ty_to_string (ast_to_type_formatter fmt) false) tys)
+ | Some tys -> String.concat "; " (List.map (ty_to_string env false) tys)
in
"back_output_tys: [" ^ tys ^ "]"
in
let fun_end =
- texpression_to_string fmt false indent2 indent_incr loop.fun_end
+ texpression_to_string env false indent2 indent_incr loop.fun_end
in
let loop_body =
- texpression_to_string fmt false indent2 indent_incr loop.loop_body
+ texpression_to_string env false indent2 indent_incr loop.loop_body
in
"loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ back_output_tys ^ "\n"
^ indent1 ^ "fun_end: {\n" ^ indent2 ^ fun_end ^ "\n" ^ indent1 ^ "}\n"
^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n"
^ indent ^ "}"
-and meta_to_string (fmt : ast_formatter) (meta : meta) : string =
+and emeta_to_string (env : fmt_env) (meta : emeta) : string =
let meta =
match meta with
| Assignment (lp, rv, rp) ->
let rp =
match rp with
| None -> ""
- | Some rp -> " [@src=" ^ mplace_to_string fmt rp ^ "]"
+ | Some rp -> " [@src=" ^ mplace_to_string env rp ^ "]"
in
- "@assign(" ^ mplace_to_string fmt lp ^ " := "
- ^ texpression_to_string fmt false "" "" rv
+ "@assign(" ^ mplace_to_string env lp ^ " := "
+ ^ texpression_to_string env false "" "" rv
^ rp ^ ")"
| SymbolicAssignment (var_id, rv) ->
"@symb_assign(" ^ VarId.to_string var_id ^ " := "
- ^ texpression_to_string fmt false "" "" rv
+ ^ texpression_to_string env false "" "" rv
^ ")"
- | MPlace mp -> "@mplace=" ^ mplace_to_string fmt mp
+ | MPlace mp -> "@mplace=" ^ mplace_to_string env mp
| Tag msg -> "@tag \"" ^ msg ^ "\""
in
"@meta[" ^ meta ^ "]"
-let fun_decl_to_string (fmt : ast_formatter) (def : fun_decl) : string =
- let type_fmt = ast_to_type_formatter fmt in
- let name =
- fun_name_to_string def.basename ^ fun_suffix def.loop_id def.back_id
- in
- let signature = fun_sig_to_string fmt def.signature in
+let fun_decl_to_string (env : fmt_env) (def : fun_decl) : string =
+ let env = { env with generics = def.signature.generics } in
+ let name = def.name ^ fun_suffix def.loop_id def.back_id in
+ let signature = fun_sig_to_string env def.signature in
match def.body with
| None -> "val " ^ name ^ " :\n " ^ signature
| Some body ->
let inside = false in
let indent = " " in
- let inputs = List.map (var_to_string type_fmt) body.inputs in
+ let inputs = List.map (var_to_string env) body.inputs in
let inputs =
if inputs = [] then indent
else " fun " ^ String.concat " " inputs ^ " ->\n" ^ indent
in
- let body = texpression_to_string fmt inside indent indent body.body in
+ let body = texpression_to_string env inside indent indent body.body in
"let " ^ name ^ " :\n " ^ signature ^ " =\n" ^ inputs ^ body
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 01:49:44 +0000