diff options
Diffstat (limited to 'compiler/PrintPure.ml')
| -rw-r--r-- | compiler/PrintPure.ml | 138 |
1 files changed, 69 insertions, 69 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index db9c583d..b1b42207 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -288,14 +288,14 @@ let rec mprojection_to_string (env : fmt_env) (inside : 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 + (* We add the "llbc" suffix to the variable index, because span-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 env name p.projection -let adt_variant_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) +let adt_variant_to_string ?(span = None) (env : fmt_env) (adt_id : type_id) (variant_id : VariantId.id option) : string = match adt_id with | TTuple -> "Tuple" @@ -309,34 +309,34 @@ let adt_variant_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) match aty with | TState | TArray | TSlice | TStr | TRawPtr _ -> (* Those types are opaque: we can't get there *) - craise_opt_meta __FILE__ __LINE__ meta "Unreachable" + craise_opt_span __FILE__ __LINE__ span "Unreachable" | TResult -> let variant_id = Option.get variant_id in if variant_id = result_ok_id then "@Result::Return" else if variant_id = result_fail_id then "@Result::Fail" else - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span "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 - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span "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 - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span "Unreachable: improper variant id for fuel type") -let adt_field_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) +let adt_field_to_string ?(span = None) (env : fmt_env) (adt_id : type_id) (field_id : FieldId.id) : string = match adt_id with | TTuple -> - craise_opt_meta __FILE__ __LINE__ meta "Unreachable" + craise_opt_span __FILE__ __LINE__ span "Unreachable" (* Tuples don't use the opaque field id for the field indices, but [int] *) | TAdtId def_id -> ( (* "Regular" ADT *) @@ -349,15 +349,15 @@ let adt_field_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) match aty with | TState | TFuel | TArray | TSlice | TStr -> (* Opaque types: we can't get there *) - craise_opt_meta __FILE__ __LINE__ meta "Unreachable" + craise_opt_span __FILE__ __LINE__ span "Unreachable" | TResult | TError | TRawPtr _ -> (* Enumerations: we can't get there *) - craise_opt_meta __FILE__ __LINE__ meta "Unreachable") + craise_opt_span __FILE__ __LINE__ span "Unreachable") (** TODO: we don't need a general function anymore (it is now only used for patterns) *) -let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) +let adt_g_value_to_string ?(span : Meta.span 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 @@ -392,50 +392,50 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) match aty with | TState | TRawPtr _ -> (* This type is opaque: we can't get there *) - craise_opt_meta __FILE__ __LINE__ meta "Unreachable" + craise_opt_span __FILE__ __LINE__ span "Unreachable" | TResult -> let variant_id = Option.get variant_id in if variant_id = result_ok_id then match field_values with | [ v ] -> "@Result::Return " ^ v | _ -> - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span "Result::Return takes exactly one value" else if variant_id = result_fail_id then match field_values with | [ v ] -> "@Result::Fail " ^ v | _ -> - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span "Result::Fail takes exactly one value" else - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span "Unreachable: improper variant id for result type" | TError -> - cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta + cassert_opt_span __FILE__ __LINE__ (field_values = []) span "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 - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span "Unreachable: improper variant id for error type" | TFuel -> let variant_id = Option.get variant_id in if variant_id = fuel_zero_id then ( - cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta + cassert_opt_span __FILE__ __LINE__ (field_values = []) span "Ill-formed full value"; "@Fuel::Zero") else if variant_id = fuel_succ_id then match field_values with | [ v ] -> "@Fuel::Succ " ^ v | _ -> - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span "@Fuel::Succ takes exactly one value" else - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span "Unreachable: improper variant id for fuel type" | TArray | TSlice | TStr -> - cassert_opt_meta __FILE__ __LINE__ (variant_id = None) meta + cassert_opt_span __FILE__ __LINE__ (variant_id = None) span "Ill-formed value"; let field_values = List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values @@ -443,12 +443,12 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) let id = assumed_ty_to_string aty in id ^ " [" ^ String.concat "; " field_values ^ "]") | _ -> - craise_opt_meta __FILE__ __LINE__ meta + craise_opt_span __FILE__ __LINE__ span ("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 ?(meta : Meta.meta option = None) +let rec typed_pattern_to_string ?(span : Meta.span option = None) (env : fmt_env) (v : typed_pattern) : string = match v.value with | PatConstant cv -> literal_to_string cv @@ -460,8 +460,8 @@ let rec typed_pattern_to_string ?(meta : Meta.meta option = None) ^ ")" | PatDummy -> "_" | PatAdt av -> - adt_g_value_to_string ~meta env - (typed_pattern_to_string ~meta env) + adt_g_value_to_string ~span env + (typed_pattern_to_string ~span env) av.variant_id av.field_values v.ty let fun_sig_to_string (env : fmt_env) (sg : fun_sig) : string = @@ -542,7 +542,7 @@ 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 ?(metadata : Meta.meta option = None) +let rec texpression_to_string ?(spandata : Meta.span option = None) (env : fmt_env) (inside : bool) (indent : string) (indent_incr : string) (e : texpression) : string = match e.e with @@ -553,26 +553,26 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None) (* Recursively destruct the app, to have a pair (app, arguments list) *) let app, args = destruct_apps e in (* Convert to string *) - app_to_string ~meta:metadata env inside indent indent_incr app args + app_to_string ~span:spandata env inside indent indent_incr app args | Lambda _ -> let xl, e = destruct_lambdas e in - let e = lambda_to_string ~meta:metadata env indent indent_incr xl e in + let e = lambda_to_string ~span:spandata env indent indent_incr xl e in if inside then "(" ^ e ^ ")" else e | Qualif _ -> (* Qualifier without arguments *) - app_to_string ~meta:metadata env inside indent indent_incr e [] + app_to_string ~span:spandata env inside indent indent_incr e [] | Let (monadic, lv, re, e) -> let e = - let_to_string ~meta:metadata env indent indent_incr monadic lv re e + let_to_string ~span:spandata env indent indent_incr monadic lv re e in if inside then "(" ^ e ^ ")" else e | Switch (scrutinee, body) -> let e = - switch_to_string ~meta:metadata env indent indent_incr scrutinee body + switch_to_string ~span:spandata env indent indent_incr scrutinee body in if inside then "(" ^ e ^ ")" else e | Loop loop -> - let e = loop_to_string ~meta:metadata env indent indent_incr loop in + let e = loop_to_string ~span:spandata env indent indent_incr loop in if inside then "(" ^ e ^ ")" else e | StructUpdate supd -> ( let s = @@ -591,7 +591,7 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None) (fun (fid, fe) -> let field = FieldId.nth field_names fid in let fe = - texpression_to_string ~metadata env false indent2 indent_incr + texpression_to_string ~spandata env false indent2 indent_incr fe in "\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";") @@ -603,22 +603,22 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None) let fields = List.map (fun (_, fe) -> - texpression_to_string ~metadata env false indent2 indent_incr fe) + texpression_to_string ~spandata env false indent2 indent_incr fe) supd.updates in "[ " ^ String.concat ", " fields ^ " ]" - | _ -> craise_opt_meta __FILE__ __LINE__ metadata "Unexpected") - | Meta (meta, e) -> ( - 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 + | _ -> craise_opt_span __FILE__ __LINE__ spandata "Unexpected") + | Meta (span, e) -> ( + let span_s = espan_to_string ~spandata env span in + let e = texpression_to_string ~spandata env inside indent indent_incr e in + match span with | Assignment _ | SymbolicAssignments _ | SymbolicPlaces _ | Tag _ -> - let e = meta_s ^ "\n" ^ indent ^ e in + let e = span_s ^ "\n" ^ indent ^ e in if inside then "(" ^ e ^ ")" else e - | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")") + | MPlace _ -> "(" ^ span_s ^ " " ^ e ^ ")") | EError (_, _) -> "@Error" -and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) +and app_to_string ?(span : Meta.span 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, @@ -638,13 +638,13 @@ and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (global_decl_id_to_string env global_id, generics) | AdtCons adt_cons_id -> let variant_s = - adt_variant_to_string ~meta env adt_cons_id.adt_id + adt_variant_to_string ~span 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 ~meta env adt_id None in - let field_s = adt_field_to_string ~meta env adt_id field_id in + let adt_s = adt_variant_to_string ~span env adt_id None in + let field_s = adt_field_to_string ~span env adt_id field_id in (* Adopting an F*-like syntax *) (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, []) | TraitConst (trait_ref, const_name) -> @@ -654,7 +654,7 @@ and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) | _ -> (* "Regular" expression case *) let inside = args <> [] || (args = [] && inside) in - ( texpression_to_string ~metadata:meta env inside indent indent_incr app, + ( texpression_to_string ~spandata:span env inside indent indent_incr app, [] ) in (* Convert the arguments. @@ -663,7 +663,7 @@ and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) let arg_to_string = let inside = true in let indent1 = indent ^ indent_incr in - texpression_to_string ~metadata:meta env inside indent1 indent_incr + texpression_to_string ~spandata:span env inside indent1 indent_incr in let args = List.map arg_to_string args in let all_args = List.append generics args in @@ -674,29 +674,29 @@ and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (* Add parentheses *) if all_args <> [] && inside then "(" ^ e ^ ")" else e -and lambda_to_string ?(meta : Meta.meta option = None) (env : fmt_env) +and lambda_to_string ?(span : Meta.span 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 + let xl = List.map (typed_pattern_to_string ~span env) xl in + let e = texpression_to_string ~spandata:span env false indent indent_incr e in "λ " ^ String.concat " " xl ^ ". " ^ e -and let_to_string ?(meta : Meta.meta option = None) (env : fmt_env) +and let_to_string ?(span : Meta.span 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 ~metadata:meta env inside indent1 indent_incr re + texpression_to_string ~spandata:span env inside indent1 indent_incr re in let e = - texpression_to_string ~metadata:meta env inside indent indent_incr e + texpression_to_string ~spandata:span env inside indent indent_incr e in - let lv = typed_pattern_to_string ~meta env lv in + let lv = typed_pattern_to_string ~span env lv in if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e -and switch_to_string ?(meta : Meta.meta option = None) (env : fmt_env) +and switch_to_string ?(span : Meta.span option = None) (env : fmt_env) (indent : string) (indent_incr : string) (scrutinee : texpression) (body : switch_body) : string = let indent1 = indent ^ indent_incr in @@ -704,10 +704,10 @@ and switch_to_string ?(meta : Meta.meta option = None) (env : fmt_env) * in most situations it will be a value or a function call, so it should be * ok*) let scrut = - texpression_to_string ~metadata:meta env true indent1 indent_incr scrutinee + texpression_to_string ~spandata:span env true indent1 indent_incr scrutinee in let e_to_string = - texpression_to_string ~metadata:meta env false indent1 indent_incr + texpression_to_string ~spandata:span env false indent1 indent_incr in match body with | If (e_true, e_false) -> @@ -717,13 +717,13 @@ and switch_to_string ?(meta : Meta.meta option = None) (env : fmt_env) ^ indent ^ "else\n" ^ indent1 ^ e_false | Match branches -> let branch_to_string (b : match_branch) : string = - let pat = typed_pattern_to_string ~meta env b.pat in + let pat = typed_pattern_to_string ~span 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 ?(meta : Meta.meta option = None) (env : fmt_env) +and loop_to_string ?(span : Meta.span 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 @@ -734,11 +734,11 @@ and loop_to_string ?(meta : Meta.meta option = None) (env : fmt_env) in let output_ty = "output_ty: " ^ ty_to_string env false loop.output_ty in let fun_end = - texpression_to_string ~metadata:meta env false indent2 indent_incr + texpression_to_string ~spandata:span env false indent2 indent_incr loop.fun_end in let loop_body = - texpression_to_string ~metadata:meta env false indent2 indent_incr + texpression_to_string ~spandata:span env false indent2 indent_incr loop.loop_body in "loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ output_ty ^ "\n" @@ -746,10 +746,10 @@ and loop_to_string ?(meta : Meta.meta option = None) (env : fmt_env) ^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n" ^ indent ^ "}" -and emeta_to_string ?(metadata : Meta.meta option = None) (env : fmt_env) - (meta : emeta) : string = - let meta = - match meta with +and espan_to_string ?(spandata : Meta.span option = None) (env : fmt_env) + (span : espan) : string = + let span = + match span with | Assignment (lp, rv, rp) -> let rp = match rp with @@ -757,14 +757,14 @@ and emeta_to_string ?(metadata : Meta.meta option = None) (env : fmt_env) | Some rp -> " [@src=" ^ mplace_to_string env rp ^ "]" in "@assign(" ^ mplace_to_string env lp ^ " := " - ^ texpression_to_string ~metadata env false "" "" rv + ^ texpression_to_string ~spandata env false "" "" rv ^ rp ^ ")" | SymbolicAssignments info -> let infos = List.map (fun (var_id, rv) -> VarId.to_string var_id ^ " == " - ^ texpression_to_string ~metadata env false "" "" rv) + ^ texpression_to_string ~spandata env false "" "" rv) info in let infos = String.concat ", " infos in @@ -781,7 +781,7 @@ and emeta_to_string ?(metadata : Meta.meta option = None) (env : fmt_env) | MPlace mp -> "@mplace=" ^ mplace_to_string env mp | Tag msg -> "@tag \"" ^ msg ^ "\"" in - "@meta[" ^ meta ^ "]" + "@span[" ^ span ^ "]" let fun_decl_to_string (env : fmt_env) (def : fun_decl) : string = let env = { env with generics = def.signature.generics } in @@ -798,7 +798,7 @@ let fun_decl_to_string (env : fmt_env) (def : fun_decl) : string = else " fun " ^ String.concat " " inputs ^ " ->\n" ^ indent in let body = - texpression_to_string ~metadata:(Some def.meta) env inside indent indent + texpression_to_string ~spandata:(Some def.span) env inside indent indent body.body in "let " ^ name ^ " :\n " ^ signature ^ " =\n" ^ inputs ^ body |