From 4a9fee3f11158c68d918e801017f98bd581cda05 Mon Sep 17 00:00:00 2001 From: Benjamin Canou Date: Sat, 22 Jul 2017 22:56:00 +0200 Subject: [PATCH] Michelson: also display types inside lambdas. --- .../embedded/alpha/client_proto_programs.ml | 12 ++- .../embedded/alpha/script_located_ir.ml | 2 +- src/proto/alpha/script_ir_translator.ml | 101 +++++++++++++----- 3 files changed, 80 insertions(+), 35 deletions(-) diff --git a/src/client/embedded/alpha/client_proto_programs.ml b/src/client/embedded/alpha/client_proto_programs.ml index 75850f6c6..08a6621ce 100644 --- a/src/client/embedded/alpha/client_proto_programs.ml +++ b/src/client/embedded/alpha/client_proto_programs.ml @@ -533,7 +533,7 @@ let unexpand_macros type_map (program : Script.code) = List.filter (fun (loc, _) -> not (List.mem loc locs)) type_map in - let type_map = (loc, (before, after)):: type_map in + let type_map = (loc, (before, after)) :: type_map in type_map, Prim (loc, name, []) end | oth -> type_map, oth in @@ -678,7 +678,7 @@ let commands () = (Utils.filter_map (fun (n, loc) -> try - let bef, aft = List.assoc (n + 1) type_map in + let bef, aft = List.assoc n type_map in Some (loc, bef, aft) with Not_found -> None) @@ -700,7 +700,7 @@ let commands () = (report_typechecking_errors cctxt [ Ecoproto_error errs ] >>= fun () -> let (types, _) = emacs_type_map type_map in let loc = match collect_error_locations errs with - | hd :: _ -> hd - 1 + | hd :: _ -> hd | [] -> 0 in Lwt.return (types, [ List.assoc loc (List.assoc "code" program.loc_table), Buffer.contents msg ])) | _ -> Lwt.return ([], []) @@ -713,8 +713,10 @@ let commands () = { Script_located_ir.point = e }), bef, aft) -> Format.fprintf ppf "(%d %d \"%s\")" (s + 1) (e + 1) - (Format.asprintf "@[%a@, \\u2B87@,%a@]" - print_stack bef print_stack aft))) + (String.concat "\\n" + (String.split_on_char '\n' + (Format.asprintf "@[%a@, \\u2B87@,%a@]" + print_stack bef print_stack aft))))) types (Format.pp_print_list (fun ppf (({ Script_located_ir.point = s }, diff --git a/src/client/embedded/alpha/script_located_ir.ml b/src/client/embedded/alpha/script_located_ir.ml index 40e25f885..d465addcd 100644 --- a/src/client/embedded/alpha/script_located_ir.ml +++ b/src/client/embedded/alpha/script_located_ir.ml @@ -65,7 +65,7 @@ exception Missing_program_field of string (*-- Converters between IR and Located IR -----------------------------------*) let strip_locations root = - let id = let id = ref (-1) in fun () -> incr id ; !id in + let id = let id = ref 0 in fun () -> incr id ; !id in let loc_table = ref [] in let rec strip_locations l = let id = id () in diff --git a/src/proto/alpha/script_ir_translator.ml b/src/proto/alpha/script_ir_translator.ml index 36a884931..a3ac777fd 100644 --- a/src/proto/alpha/script_ir_translator.ml +++ b/src/proto/alpha/script_ir_translator.ml @@ -1455,41 +1455,82 @@ let type_map_enc = (list Script.expr_encoding))) let type_map descr = - let rec type_map + let rec instr_type_map : type bef aft. type_map -> (bef, aft) descr -> type_map = fun acc { loc ; instr ; bef ; aft } -> let self acc = (loc, (unparse_stack bef, unparse_stack aft)) :: acc in - match instr with - | If_none (dbt, dbf) -> - let acc = type_map acc dbt in - let acc = type_map acc dbf in + match instr, aft with + | If_none (dbt, dbf), _ -> + let acc = instr_type_map acc dbt in + let acc = instr_type_map acc dbf in self acc - | If_left (dbt, dbf) -> - let acc = type_map acc dbt in - let acc = type_map acc dbf in + | If_left (dbt, dbf), _ -> + let acc = instr_type_map acc dbt in + let acc = instr_type_map acc dbf in self acc - | If_cons (dbt, dbf) -> - let acc = type_map acc dbt in - let acc = type_map acc dbf in + | If_cons (dbt, dbf), _ -> + let acc = instr_type_map acc dbt in + let acc = instr_type_map acc dbf in self acc - | Seq (dl, dr) -> - let acc = type_map acc dl in - let acc = type_map acc dr in + | Seq (dl, dr), _ -> + let acc = instr_type_map acc dl in + let acc = instr_type_map acc dr in acc - | If (dbt, dbf) -> - let acc = type_map acc dbt in - let acc = type_map acc dbf in + | If (dbt, dbf), _ -> + let acc = instr_type_map acc dbt in + let acc = instr_type_map acc dbf in self acc - | Loop body -> - let acc = type_map acc body in + | Loop body, _ -> + let acc = instr_type_map acc body in self acc - | Dip body -> - let acc = type_map acc body in + | Dip body, _ -> + let acc = instr_type_map acc body in self acc - | _ -> - self acc in - type_map [] descr + | Lambda (Lam (body, _)), _ -> + let acc = instr_type_map acc body in + self acc + | Const v, Item_t (ty, _) -> + let acc = data_type_map acc ty v in + self acc + | _, _ -> + self acc + and data_type_map + : type a. type_map -> a ty -> a -> type_map + = fun acc ty v -> + match ty, v with + | Unit_t, _ -> acc + | Int_t _, _ -> acc + | Signature_t, _ -> acc + | String_t, _ -> acc + | Tez_t, _ -> acc + | Key_t, _ -> acc + | Timestamp_t, _ -> acc + | Bool_t, _ -> acc + | Contract_t _,_ -> acc + | Set_t _, _ -> acc + | Pair_t (lty, rty), (l, r) -> + let acc = data_type_map acc lty l in + let acc = data_type_map acc rty r in + acc + | Union_t (lty, _), L l -> + data_type_map acc lty l + | Union_t (_, rty), R r -> + data_type_map acc rty r + | Lambda_t _, Lam (body, _) -> + instr_type_map acc body + | Option_t _, None -> acc + | Option_t ty, Some v -> + data_type_map acc ty v + | List_t ty, l -> + List.fold_left + (fun acc v -> data_type_map acc ty v) + acc l + | Map_t (_, ty), m -> + map_fold + (fun _ v acc -> data_type_map acc ty v) + m acc in + instr_type_map [] descr let typecheck_code : context -> Script.code -> type_map tzresult Lwt.t @@ -1506,13 +1547,15 @@ let typecheck_code (Lwt.return (parse_ty storage_type)) >>=? fun (Ex_ty storage_type) -> let arg_type_full = Pair_t (Pair_t (Tez_t, arg_type), storage_type) in let ret_type_full = Pair_t (ret_type, storage_type) in + let result = + parse_lambda ctxt + ~storage_type + ~type_logger:(fun x -> failure_type_map := x :: !failure_type_map) + arg_type_full ret_type_full + code in trace (Ill_typed_contract (code, arg_type, ret_type, storage_type, !failure_type_map)) - (parse_lambda ctxt - ~storage_type - ~type_logger:(fun x -> failure_type_map := x :: !failure_type_map) - arg_type_full ret_type_full - code) >>=? fun (Lam (descr,_)) -> + result >>=? fun (Lam (descr,_)) -> return (type_map descr) let typecheck_data