diff options
Diffstat (limited to 'compiler/PrintPure.ml')
-rw-r--r-- | compiler/PrintPure.ml | 57 |
1 files changed, 5 insertions, 52 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index be7b3cb4..6396fe96 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -195,12 +195,9 @@ let assumed_ty_to_string (aty : assumed_ty) : string = | 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 = match id with @@ -354,10 +351,6 @@ let rec mprojection_to_string (fmt : ast_formatter) (inside : string) | pe :: p' -> ( let s = mprojection_to_string fmt 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 = @@ -395,8 +388,6 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id) | 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" @@ -412,13 +403,7 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id) 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) (field_id : FieldId.id) : string = @@ -435,11 +420,10 @@ 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 -> + | State | Fuel | Array | Slice | Str -> (* Opaque types: we can't get there *) raise (Failure "Unreachable") - | Result | Error | Option -> + | Result | Error -> (* Enumerations: we can't get there *) raise (Failure "Unreachable")) @@ -510,31 +494,13 @@ 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 -> + | 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 ^ "}") + id ^ " [" ^ String.concat "; " field_values ^ "]") | _ -> let fmt = value_to_type_formatter fmt in raise @@ -593,29 +559,16 @@ 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 - | Replace -> "core::mem::replace" | BoxNew -> "alloc::boxed::Box::new" - | BoxDeref -> "core::ops::deref::Deref::deref" - | BoxDerefMut -> "core::ops::deref::DerefMut::deref_mut" | BoxFree -> "alloc::alloc::box_free" - | VecNew -> "alloc::vec::Vec::new" - | VecPush -> "alloc::vec::Vec::push" - | VecInsert -> "alloc::vec::Vec::insert" - | VecLen -> "alloc::vec::Vec::len" - | VecIndex -> "core::ops::index::Index<alloc::vec::Vec>::index" - | VecIndexMut -> "core::ops::index::IndexMut<alloc::vec::Vec>::index_mut" | ArrayIndexShared -> "@ArrayIndexShared" | ArrayIndexMut -> "@ArrayIndexMut" | ArrayToSliceShared -> "@ArrayToSliceShared" | ArrayToSliceMut -> "@ArrayToSliceMut" - | ArraySubsliceShared -> "@ArraySubsliceShared" - | ArraySubsliceMut -> "@ArraySubsliceMut" | ArrayRepeat -> "@ArrayRepeat" | SliceLen -> "@SliceLen" | SliceIndexShared -> "@SliceIndexShared" | SliceIndexMut -> "@SliceIndexMut" - | SliceSubsliceShared -> "@SliceSubsliceShared" - | SliceSubsliceMut -> "@SliceSubsliceMut" let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string = match fid with |