diff options
Diffstat (limited to 'compiler/PrintPure.ml')
| -rw-r--r-- | compiler/PrintPure.ml | 191 |
1 files changed, 117 insertions, 74 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 00a431a0..d0c243bb 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -2,6 +2,7 @@ open Pure open PureUtils +open Errors (** The formatting context for pure definitions uses non-pure definitions to lookup names. The main reason is that when building the pure definitions @@ -293,7 +294,7 @@ let mplace_to_string (env : fmt_env) (p : mplace) : string = let name = name ^ "^" ^ E.VarId.to_string p.var_id ^ "llbc" in mprojection_to_string env name p.projection -let adt_variant_to_string (env : fmt_env) (adt_id : type_id) +let adt_variant_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) (variant_id : VariantId.id option) : string = match adt_id with | TTuple -> "Tuple" @@ -307,29 +308,34 @@ let adt_variant_to_string (env : fmt_env) (adt_id : type_id) match aty with | TState | TArray | TSlice | TStr | TRawPtr _ -> (* Those types are opaque: we can't get there *) - raise (Failure "Unreachable") + craise_opt_meta __FILE__ __LINE__ meta "Unreachable" | 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") + craise_opt_meta __FILE__ __LINE__ meta + "Unreachable: improper variant id for result type" | 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") + else + craise_opt_meta __FILE__ __LINE__ meta + "Unreachable: improper variant id for error type" | 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")) + else + craise_opt_meta __FILE__ __LINE__ meta + "Unreachable: improper variant id for fuel type") -let adt_field_to_string (env : fmt_env) (adt_id : type_id) +let adt_field_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) (field_id : FieldId.id) : string = match adt_id with | TTuple -> - raise (Failure "Unreachable") + craise_opt_meta __FILE__ __LINE__ meta "Unreachable" (* Tuples don't use the opaque field id for the field indices, but [int] *) | TAdtId def_id -> ( (* "Regular" ADT *) @@ -342,17 +348,17 @@ let adt_field_to_string (env : fmt_env) (adt_id : type_id) match aty with | TState | TFuel | TArray | TSlice | TStr -> (* Opaque types: we can't get there *) - raise (Failure "Unreachable") + craise_opt_meta __FILE__ __LINE__ meta "Unreachable" | TResult | TError | TRawPtr _ -> (* Enumerations: we can't get there *) - raise (Failure "Unreachable")) + craise_opt_meta __FILE__ __LINE__ meta "Unreachable") (** TODO: we don't need a general function anymore (it is now only used for patterns) *) -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 adt_g_value_to_string ?(meta : Meta.meta option = None) (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 | TAdt (TTuple, _) -> @@ -385,50 +391,64 @@ let adt_g_value_to_string (env : fmt_env) (value_to_string : 'v -> string) match aty with | TState | TRawPtr _ -> (* This type is opaque: we can't get there *) - raise (Failure "Unreachable") + craise_opt_meta __FILE__ __LINE__ meta "Unreachable" | TResult -> let variant_id = Option.get variant_id in if variant_id = result_return_id then match field_values with | [ v ] -> "@Result::Return " ^ v - | _ -> raise (Failure "Result::Return takes exactly one value") + | _ -> + craise_opt_meta __FILE__ __LINE__ meta + "Result::Return takes exactly one value" else if variant_id = result_fail_id then match field_values with | [ v ] -> "@Result::Fail " ^ v - | _ -> raise (Failure "Result::Fail takes exactly one value") + | _ -> + craise_opt_meta __FILE__ __LINE__ meta + "Result::Fail takes exactly one value" else - raise (Failure "Unreachable: improper variant id for result type") + craise_opt_meta __FILE__ __LINE__ meta + "Unreachable: improper variant id for result type" | TError -> - assert (field_values = []); + cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta + "Ill-formed error value"; 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") + else + craise_opt_meta __FILE__ __LINE__ meta + "Unreachable: improper variant id for error type" | TFuel -> let variant_id = Option.get variant_id in if variant_id = fuel_zero_id then ( - assert (field_values = []); + cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta + "Ill-formed full value"; "@Fuel::Zero") else if variant_id = fuel_succ_id then match field_values with | [ v ] -> "@Fuel::Succ " ^ v - | _ -> raise (Failure "@Fuel::Succ takes exactly one value") - else raise (Failure "Unreachable: improper variant id for fuel type") + | _ -> + craise_opt_meta __FILE__ __LINE__ meta + "@Fuel::Succ takes exactly one value" + else + craise_opt_meta __FILE__ __LINE__ meta + "Unreachable: improper variant id for fuel type" | TArray | TSlice | TStr -> - assert (variant_id = None); + cassert_opt_meta __FILE__ __LINE__ (variant_id = None) meta + "Ill-formed value"; 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 ^ "]") | _ -> - raise - (Failure - ("Inconsistently typed value: expected ADT type but found:" - ^ "\n- ty: " ^ ty_to_string env false ty ^ "\n- variant_id: " - ^ Print.option_to_string VariantId.to_string variant_id)) + craise_opt_meta __FILE__ __LINE__ meta + ("Inconsistently typed value: expected ADT type but found:" ^ "\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 (env : fmt_env) (v : typed_pattern) : string = +let rec typed_pattern_to_string ?(meta : Meta.meta option = None) + (env : fmt_env) (v : typed_pattern) : string = match v.value with | PatConstant cv -> literal_to_string cv | PatVar (v, None) -> var_to_string env v @@ -439,8 +459,8 @@ let rec typed_pattern_to_string (env : fmt_env) (v : typed_pattern) : string = ^ ")" | PatDummy -> "_" | PatAdt av -> - adt_g_value_to_string env - (typed_pattern_to_string env) + adt_g_value_to_string ~meta env + (typed_pattern_to_string ~meta env) av.variant_id av.field_values v.ty let fun_sig_to_string (env : fmt_env) (sg : fun_sig) : string = @@ -521,8 +541,9 @@ let fun_or_op_id_to_string (env : fmt_env) (fun_id : fun_or_op_id) : string = binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">" (** [inside]: controls the introduction of parentheses *) -let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) - (indent_incr : string) (e : texpression) : string = +let rec texpression_to_string ?(metadata : Meta.meta option = None) + (env : fmt_env) (inside : bool) (indent : string) (indent_incr : string) + (e : texpression) : string = match e.e with | Var var_id -> var_id_to_string env var_id | CVar cg_id -> const_generic_var_id_to_string env cg_id @@ -531,22 +552,26 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) (* Recursively destruct the app, to have a pair (app, arguments list) *) let app, args = destruct_apps e in (* Convert to string *) - app_to_string env inside indent indent_incr app args + app_to_string ~meta:metadata env inside indent indent_incr app args | Lambda _ -> let xl, e = destruct_lambdas e in - let e = lambda_to_string env indent indent_incr xl e in + let e = lambda_to_string ~meta:metadata env indent indent_incr xl e in if inside then "(" ^ e ^ ")" else e | Qualif _ -> (* Qualifier without arguments *) - app_to_string env inside indent indent_incr e [] + app_to_string ~meta:metadata env inside indent indent_incr e [] | Let (monadic, lv, re, e) -> - let e = let_to_string env indent indent_incr monadic lv re e in + let e = + let_to_string ~meta:metadata env indent indent_incr monadic lv re e + in if inside then "(" ^ e ^ ")" else e | Switch (scrutinee, body) -> - let e = switch_to_string env indent indent_incr scrutinee body in + let e = + switch_to_string ~meta:metadata env indent indent_incr scrutinee body + in if inside then "(" ^ e ^ ")" else e | Loop loop -> - let e = loop_to_string env indent indent_incr loop in + let e = loop_to_string ~meta:metadata env indent indent_incr loop in if inside then "(" ^ e ^ ")" else e | StructUpdate supd -> ( let s = @@ -565,7 +590,8 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) (fun (fid, fe) -> let field = FieldId.nth field_names fid in let fe = - texpression_to_string env false indent2 indent_incr fe + texpression_to_string ~metadata env false indent2 indent_incr + fe in "\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";") supd.updates @@ -576,23 +602,23 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) let fields = List.map (fun (_, fe) -> - texpression_to_string env false indent2 indent_incr fe) + texpression_to_string ~metadata env false indent2 indent_incr fe) supd.updates in "[ " ^ String.concat ", " fields ^ " ]" - | _ -> raise (Failure "Unexpected")) + | _ -> craise_opt_meta __FILE__ __LINE__ metadata "Unexpected") | Meta (meta, e) -> ( - let meta_s = emeta_to_string env meta in - let e = texpression_to_string env inside indent indent_incr e in + let meta_s = emeta_to_string ~metadata env meta in + let e = texpression_to_string ~metadata env inside indent indent_incr e in match meta with | Assignment _ | SymbolicAssignments _ | SymbolicPlaces _ | Tag _ -> let e = meta_s ^ "\n" ^ indent ^ e in if inside then "(" ^ e ^ ")" else e | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")") -and app_to_string (env : fmt_env) (inside : bool) (indent : string) - (indent_incr : string) (app : texpression) (args : texpression list) : - string = +and app_to_string ?(meta : Meta.meta option = None) (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 *) @@ -610,13 +636,13 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string) (global_decl_id_to_string env global_id, generics) | AdtCons adt_cons_id -> let variant_s = - adt_variant_to_string env adt_cons_id.adt_id + adt_variant_to_string ~meta env adt_cons_id.adt_id adt_cons_id.variant_id in (ConstStrings.constructor_prefix ^ variant_s, []) | Proj { adt_id; field_id } -> - 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 + let adt_s = adt_variant_to_string ~meta env adt_id None in + let field_s = adt_field_to_string ~meta env adt_id field_id in (* Adopting an F*-like syntax *) (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, []) | TraitConst (trait_ref, const_name) -> @@ -626,7 +652,8 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string) | _ -> (* "Regular" expression case *) let inside = args <> [] || (args = [] && inside) in - (texpression_to_string env inside indent indent_incr app, []) + ( texpression_to_string ~metadata:meta env inside indent indent_incr app, + [] ) in (* Convert the arguments. * The arguments are expressions, so indentation might get weird... (though @@ -634,7 +661,7 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string) let arg_to_string = let inside = true in let indent1 = indent ^ indent_incr in - texpression_to_string env inside indent1 indent_incr + texpression_to_string ~metadata:meta env inside indent1 indent_incr in let args = List.map arg_to_string args in let all_args = List.append generics args in @@ -645,31 +672,41 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string) (* Add parentheses *) if all_args <> [] && inside then "(" ^ e ^ ")" else e -and lambda_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 env) xl in - let e = texpression_to_string env false indent indent_incr e in +and lambda_to_string ?(meta : Meta.meta option = None) (env : fmt_env) + (indent : string) (indent_incr : string) (xl : typed_pattern list) + (e : texpression) : string = + let xl = List.map (typed_pattern_to_string ~meta env) xl in + let e = texpression_to_string ~metadata:meta env false indent indent_incr e in "λ " ^ String.concat " " xl ^ ". " ^ e -and let_to_string (env : fmt_env) (indent : string) (indent_incr : string) - (monadic : bool) (lv : typed_pattern) (re : texpression) (e : texpression) : - string = +and let_to_string ?(meta : Meta.meta option = None) (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 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 + let re = + texpression_to_string ~metadata:meta env inside indent1 indent_incr re + in + let e = + texpression_to_string ~metadata:meta env inside indent indent_incr e + in + let lv = typed_pattern_to_string ~meta env lv in if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e -and switch_to_string (env : fmt_env) (indent : string) (indent_incr : string) - (scrutinee : texpression) (body : switch_body) : string = +and switch_to_string ?(meta : Meta.meta option = None) (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 env true indent1 indent_incr scrutinee in - let e_to_string = texpression_to_string env false indent1 indent_incr in + let scrut = + texpression_to_string ~metadata:meta env true indent1 indent_incr scrutinee + in + let e_to_string = + texpression_to_string ~metadata:meta env false indent1 indent_incr + in match body with | If (e_true, e_false) -> let e_true = e_to_string e_true in @@ -678,14 +715,14 @@ and switch_to_string (env : fmt_env) (indent : string) (indent_incr : string) ^ indent ^ "else\n" ^ indent1 ^ e_false | Match branches -> let branch_to_string (b : match_branch) : string = - let pat = typed_pattern_to_string env b.pat in + let pat = typed_pattern_to_string ~meta 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 (env : fmt_env) (indent : string) (indent_incr : string) - (loop : loop) : string = +and loop_to_string ?(meta : Meta.meta option = None) (env : fmt_env) + (indent : string) (indent_incr : string) (loop : loop) : string = let indent1 = indent ^ indent_incr in let indent2 = indent1 ^ indent_incr in let loop_inputs = @@ -695,17 +732,20 @@ and loop_to_string (env : fmt_env) (indent : string) (indent_incr : string) in let output_ty = "output_ty: " ^ ty_to_string env false loop.output_ty in let fun_end = - texpression_to_string env false indent2 indent_incr loop.fun_end + texpression_to_string ~metadata:meta env false indent2 indent_incr + loop.fun_end in let loop_body = - texpression_to_string env false indent2 indent_incr loop.loop_body + texpression_to_string ~metadata:meta env false indent2 indent_incr + loop.loop_body in "loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ output_ty ^ "\n" ^ indent1 ^ "fun_end: {\n" ^ indent2 ^ fun_end ^ "\n" ^ indent1 ^ "}\n" ^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n" ^ indent ^ "}" -and emeta_to_string (env : fmt_env) (meta : emeta) : string = +and emeta_to_string ?(metadata : Meta.meta option = None) (env : fmt_env) + (meta : emeta) : string = let meta = match meta with | Assignment (lp, rv, rp) -> @@ -715,14 +755,14 @@ and emeta_to_string (env : fmt_env) (meta : emeta) : string = | Some rp -> " [@src=" ^ mplace_to_string env rp ^ "]" in "@assign(" ^ mplace_to_string env lp ^ " := " - ^ texpression_to_string env false "" "" rv + ^ texpression_to_string ~metadata env false "" "" rv ^ rp ^ ")" | SymbolicAssignments info -> let infos = List.map (fun (var_id, rv) -> VarId.to_string var_id ^ " == " - ^ texpression_to_string env false "" "" rv) + ^ texpression_to_string ~metadata env false "" "" rv) info in let infos = String.concat ", " infos in @@ -755,5 +795,8 @@ let fun_decl_to_string (env : fmt_env) (def : fun_decl) : string = if inputs = [] then indent else " fun " ^ String.concat " " inputs ^ " ->\n" ^ indent in - let body = texpression_to_string env inside indent indent body.body in + let body = + texpression_to_string ~metadata:(Some def.meta) env inside indent indent + body.body + in "let " ^ name ^ " :\n " ^ signature ^ " =\n" ^ inputs ^ body |