diff options
Diffstat (limited to 'compiler/PrintPure.ml')
| -rw-r--r-- | compiler/PrintPure.ml | 141 |
1 files changed, 87 insertions, 54 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 6ef87194..1162251a 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -314,17 +314,22 @@ let adt_variant_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) if variant_id = result_return_id then "@Result::Return" else if variant_id = result_fail_id then "@Result::Fail" else - craise_opt_meta meta "Unreachable: improper variant id for result type" + craise_opt_meta 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 craise_opt_meta meta "Unreachable: improper variant id for error type" + else + craise_opt_meta 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 craise_opt_meta meta "Unreachable: improper variant id for fuel type") + else + craise_opt_meta meta + "Unreachable: improper variant id for fuel type") let adt_field_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) (field_id : FieldId.id) : string = @@ -351,9 +356,9 @@ let adt_field_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) (** 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) (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, _) -> @@ -398,13 +403,16 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (val | [ v ] -> "@Result::Fail " ^ v | _ -> craise_opt_meta meta "Result::Fail takes exactly one value" else - craise_opt_meta meta "Unreachable: improper variant id for result type" + craise_opt_meta meta + "Unreachable: improper variant id for result type" | TError -> cassert_opt_meta (field_values = []) meta "TODO: error message"; 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 meta "Unreachable: improper variant id for error type" + else + craise_opt_meta meta + "Unreachable: improper variant id for error type" | TFuel -> let variant_id = Option.get variant_id in if variant_id = fuel_zero_id then ( @@ -414,7 +422,9 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (val match field_values with | [ v ] -> "@Fuel::Succ " ^ v | _ -> craise_opt_meta meta "@Fuel::Succ takes exactly one value" - else craise_opt_meta meta "Unreachable: improper variant id for fuel type" + else + craise_opt_meta meta + "Unreachable: improper variant id for fuel type" | TArray | TSlice | TStr -> cassert_opt_meta (variant_id = None) meta "TODO: error message"; let field_values = @@ -423,13 +433,13 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (val let id = assumed_ty_to_string aty in id ^ " [" ^ String.concat "; " field_values ^ "]") | _ -> - craise_opt_meta - 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) + craise_opt_meta 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 ?(meta : Meta.meta option = None) (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 @@ -440,8 +450,8 @@ let rec typed_pattern_to_string ?(meta : Meta.meta option = None) (env : fmt_env ^ ")" | PatDummy -> "_" | PatAdt av -> - adt_g_value_to_string ~meta:meta env - (typed_pattern_to_string ~meta:meta 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 = @@ -522,8 +532,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 ?(metadata : Meta.meta option = None) (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 @@ -541,10 +552,14 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None) (env : fmt_e (* Qualifier without arguments *) app_to_string ~meta:metadata 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 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 ~meta:metadata 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 ~meta:metadata env indent indent_incr loop in @@ -566,7 +581,8 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None) (env : fmt_e (fun (fid, fe) -> let field = FieldId.nth field_names fid in let fe = - texpression_to_string ~metadata:metadata env false indent2 indent_incr fe + texpression_to_string ~metadata env false indent2 indent_incr + fe in "\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";") supd.updates @@ -577,23 +593,23 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None) (env : fmt_e let fields = List.map (fun (_, fe) -> - texpression_to_string ~metadata:metadata env false indent2 indent_incr fe) + texpression_to_string ~metadata env false indent2 indent_incr fe) supd.updates in "[ " ^ String.concat ", " fields ^ " ]" | _ -> craise_opt_meta metadata "Unexpected") | Meta (meta, e) -> ( - let meta_s = emeta_to_string ~metadata:metadata env meta in - let e = texpression_to_string ~metadata:metadata 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 ?(meta : Meta.meta option = None) (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 *) @@ -611,13 +627,13 @@ and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (inside : bo (global_decl_id_to_string env global_id, generics) | AdtCons adt_cons_id -> let variant_s = - adt_variant_to_string ~meta:meta 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 ~meta:meta env adt_id None in - let field_s = adt_field_to_string ~meta:meta 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) -> @@ -627,7 +643,8 @@ and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (inside : bo | _ -> (* "Regular" expression case *) let inside = args <> [] || (args = [] && inside) in - (texpression_to_string ~metadata:meta 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 @@ -646,31 +663,41 @@ and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (inside : bo (* Add parentheses *) if all_args <> [] && inside then "(" ^ e ^ ")" else e -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:meta env) xl 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 ?(meta : Meta.meta option = None) (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 ~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:meta 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 ?(meta : Meta.meta option = None) (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 ~metadata:meta env true indent1 indent_incr scrutinee in - let e_to_string = texpression_to_string ~metadata:meta 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 @@ -679,14 +706,14 @@ and switch_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : ^ indent ^ "else\n" ^ indent1 ^ e_false | Match branches -> let branch_to_string (b : match_branch) : string = - let pat = typed_pattern_to_string ~meta:meta 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 ?(meta : Meta.meta option = None) (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 = @@ -696,17 +723,20 @@ and loop_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : s 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 loop.fun_end + texpression_to_string ~metadata:meta env false indent2 indent_incr + loop.fun_end in let loop_body = - texpression_to_string ~metadata:meta 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 ?(metadata : Meta.meta option = None) (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) -> @@ -716,14 +746,14 @@ and emeta_to_string ?(metadata : Meta.meta option = None) (env : fmt_env) (meta | Some rp -> " [@src=" ^ mplace_to_string env rp ^ "]" in "@assign(" ^ mplace_to_string env lp ^ " := " - ^ texpression_to_string ~metadata:metadata 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 ~metadata:metadata env false "" "" rv) + ^ texpression_to_string ~metadata env false "" "" rv) info in let infos = String.concat ", " infos in @@ -756,5 +786,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 ~metadata:(Some def.meta) 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 |