From 50af296306bfee9f0b127dde8abe5fb0ec1b0acb Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 1 Aug 2023 11:16:06 +0200 Subject: Start adding support for const generics --- compiler/PrintPure.ml | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 3f35a023..03252200 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -55,8 +55,10 @@ 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 integer_type_to_string = Print.Types.integer_type_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 = @@ -392,7 +394,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.PrimitiveValues.primitive_value_to_string cv + | PatConstant cv -> literal_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 @@ -450,6 +452,16 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = | A.VecLen -> "alloc::vec::Vec::len" | A.VecIndex -> "core::ops::index::Index::index" | A.VecIndexMut -> "core::ops::index::IndexMut::index_mut" + | ArraySharedIndex -> "@ArraySharedIndex" + | ArrayMutIndex -> "@ArrayMutIndex" + | ArrayToSharedSlice -> "@ArrayToSharedSlice" + | ArrayToMutSlice -> "@ArrayToMutSlice" + | ArraySharedSubslice -> "@ArraySharedSubslice" + | ArrayMutSubslice -> "@ArrayMutSubslice" + | SliceSharedIndex -> "@SliceSharedIndex" + | SliceMutIndex -> "@SliceMutIndex" + | SliceSharedSubslice -> "@SliceSharedSubslice" + | SliceMutSubslice -> "@SliceMutSubslice" let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string = match fid with @@ -495,7 +507,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.PrimitiveValues.primitive_value_to_string cv + | 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 -- cgit v1.2.3 From 9d27e2e27db06eaad7565b55366ca8734b364fca Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 2 Aug 2023 11:03:59 +0200 Subject: Make progress proapagating the changes --- compiler/PrintPure.ml | 113 ++++++++++++++++++++++++++++++++++---------------- 1 file changed, 78 insertions(+), 35 deletions(-) (limited to 'compiler/PrintPure.ml') 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 -- cgit v1.2.3 From 59ec03d37d2ad51cf77e456622703c4c84780f48 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 2 Aug 2023 11:46:09 +0200 Subject: Make progress --- compiler/PrintPure.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 6f857b4f..33a86df5 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -532,6 +532,7 @@ let unop_to_string (unop : unop) : string = | Cast (src, tgt) -> "cast<" ^ integer_type_to_string src ^ "," ^ integer_type_to_string tgt ^ ">" + | SliceNew tgt_len -> "array_to_slice<" ^ scalar_value_to_string tgt_len ^ ">" let binop_to_string = Print.Expressions.binop_to_string -- cgit v1.2.3 From a1e24c2a13713b015abc9a93e6915b6d4a6f22fe Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 2 Aug 2023 14:10:15 +0200 Subject: Make progress --- compiler/PrintPure.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 33a86df5..8fb6d644 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -164,6 +164,7 @@ let assumed_ty_to_string (aty : assumed_ty) : string = | Array -> "Array" | Slice -> "Slice" | Str -> "Str" + | Range -> "Range" let type_id_to_string (fmt : type_formatter) (id : type_id) : string = match id with @@ -293,9 +294,11 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id) | Assumed aty -> ( (* Assumed type *) match aty with - | State | Vec | Array | Slice | Str -> + | State | Array | Slice | Str -> (* Those types are opaque: we can't get there *) raise (Failure "Unreachable") + | Vec -> "@Vec" + | Range -> "@Range" | Result -> let variant_id = Option.get variant_id in if variant_id = result_return_id then "@Result::Return" @@ -334,6 +337,7 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id) | Assumed aty -> ( (* Assumed type *) match aty with + | Range -> FieldId.to_string field_id | State | Fuel | Vec | Array | Slice | Str -> (* Opaque types: we can't get there *) raise (Failure "Unreachable") @@ -425,7 +429,14 @@ let adt_g_value_to_string (fmt : value_formatter) 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 ^ "]" + | Range -> + 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 ^ "}") | _ -> let fmt = value_to_type_formatter fmt in raise -- cgit v1.2.3 From 56aa15e45e8cbc32eec6ec07221d93cbe56fad59 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 2 Aug 2023 14:57:55 +0200 Subject: Make progress --- compiler/PrintPure.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 8fb6d644..211fb2c2 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -543,7 +543,6 @@ let unop_to_string (unop : unop) : string = | Cast (src, tgt) -> "cast<" ^ integer_type_to_string src ^ "," ^ integer_type_to_string tgt ^ ">" - | SliceNew tgt_len -> "array_to_slice<" ^ scalar_value_to_string tgt_len ^ ">" let binop_to_string = Print.Expressions.binop_to_string -- cgit v1.2.3 From 931fabe3e8590815548d606b33fc8db31e9f6010 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 3 Aug 2023 16:21:43 +0200 Subject: Fix an issue with the extraction of aggregated arrays --- compiler/PrintPure.ml | 38 ++++++++++++++++++++++++++------------ 1 file changed, 26 insertions(+), 12 deletions(-) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 211fb2c2..43b11aa5 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -583,25 +583,39 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool) | Loop loop -> let e = loop_to_string fmt indent indent_incr loop in if inside then "(" ^ e ^ ")" else e - | StructUpdate supd -> + | StructUpdate supd -> ( let s = match supd.init with | None -> "" | Some vid -> " " ^ fmt.var_id_to_string vid ^ " with" in - let field_names = Option.get (fmt.adt_field_names supd.struct_id None) in let indent1 = indent ^ indent_incr in let indent2 = indent1 ^ indent_incr 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 in - "\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";") - supd.updates - in - let bl = if fields = [] then "" else "\n" ^ indent in - "{" ^ s ^ String.concat "" fields ^ bl ^ "}" + (* 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 + 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 + in + "\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";") + supd.updates + in + let bl = if fields = [] then "" else "\n" ^ indent in + "{" ^ s ^ String.concat "" fields ^ bl ^ "}" + | Assumed Array -> + let fields = + List.map + (fun (_, fe) -> + texpression_to_string fmt 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 -- cgit v1.2.3 From 79225e6ca645ca3902b3b761966dc869306cedbd Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 4 Aug 2023 19:57:48 +0200 Subject: Add SliceLen as a primitive function and make minor adjustments --- compiler/PrintPure.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 43b11aa5..ad7ab05f 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -512,6 +512,7 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = | ArrayToMutSlice -> "@ArrayToMutSlice" | ArraySharedSubslice -> "@ArraySharedSubslice" | ArrayMutSubslice -> "@ArrayMutSubslice" + | SliceLen -> "@SliceLen" | SliceSharedIndex -> "@SliceSharedIndex" | SliceMutIndex -> "@SliceMutIndex" | SliceSharedSubslice -> "@SliceSharedSubslice" -- cgit v1.2.3 From 987dc5c25a1d5cee19f4bba2416cbfa83e6ab6de Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 7 Aug 2023 08:59:27 +0200 Subject: Change some fun id names to use "Mut"/"Shared" as a suffix --- compiler/PrintPure.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index ad7ab05f..cfb63ec2 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -506,17 +506,17 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string = | A.VecLen -> "alloc::vec::Vec::len" | A.VecIndex -> "core::ops::index::Index::index" | A.VecIndexMut -> "core::ops::index::IndexMut::index_mut" - | ArraySharedIndex -> "@ArraySharedIndex" - | ArrayMutIndex -> "@ArrayMutIndex" - | ArrayToSharedSlice -> "@ArrayToSharedSlice" - | ArrayToMutSlice -> "@ArrayToMutSlice" - | ArraySharedSubslice -> "@ArraySharedSubslice" - | ArrayMutSubslice -> "@ArrayMutSubslice" + | ArrayIndexShared -> "@ArrayIndexShared" + | ArrayIndexMut -> "@ArrayIndexMut" + | ArrayToSliceShared -> "@ArrayToSliceShared" + | ArrayToSliceMut -> "@ArrayToSliceMut" + | ArraySubsliceShared -> "@ArraySubsliceShared" + | ArraySubsliceMut -> "@ArraySubsliceMut" | SliceLen -> "@SliceLen" - | SliceSharedIndex -> "@SliceSharedIndex" - | SliceMutIndex -> "@SliceMutIndex" - | SliceSharedSubslice -> "@SliceSharedSubslice" - | SliceMutSubslice -> "@SliceMutSubslice" + | SliceIndexShared -> "@SliceIndexShared" + | SliceIndexMut -> "@SliceIndexMut" + | SliceSubsliceShared -> "@SliceSubsliceShared" + | SliceSubsliceMut -> "@SliceSubsliceMut" let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string = match fid with -- cgit v1.2.3