tmp: some error

This commit is contained in:
Galfour 2019-04-17 15:41:20 +00:00
parent 5131ac0024
commit d97f546b45
10 changed files with 293 additions and 134 deletions

View File

@ -170,6 +170,12 @@ module PP = struct
| Some _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
| _ -> fprintf ppf "@[<v>%a@]" expression ae.expression
and lambda ppf l =
let {binder;input_type;output_type;result;body} = l in
fprintf ppf "lambda (%s:%a) : %a {@; @[<v>%a@]@;} return %a"
binder type_value input_type type_value output_type
block body annotated_expression result
and expression ppf (e:expression) : unit =
match e with
| E_literal l -> literal ppf l
@ -177,10 +183,7 @@ module PP = struct
| E_constructor (c, lst) -> fprintf ppf "%s(%a)" c annotated_expression lst
| E_variable a -> fprintf ppf "%s" a
| E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
| E_lambda {binder;input_type;output_type;result;body} ->
fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
binder type_value input_type type_value output_type
block body annotated_expression result
| E_lambda l -> fprintf ppf "%a" lambda l
| E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
| E_record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
| E_tuple lst -> fprintf ppf "tuple[@; @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) lst
@ -249,6 +252,68 @@ module PP = struct
end
module Free_variables = struct
type bindings = string list
let mem : string -> bindings -> bool = List.mem
let singleton : string -> bindings = fun s -> [ s ]
let union : bindings -> bindings -> bindings = (@)
let unions : bindings list -> bindings = List.concat
let empty : bindings = []
let of_list : string list -> bindings = fun x -> x
let rec expression : bindings -> expression -> bindings = fun b e ->
let self = annotated_expression b in
match e with
| E_lambda l ->
let b' = union (singleton l.binder) b in
union (annotated_expression b' l.result) (block b' l.body)
| E_literal _ -> empty
| E_constant (_ , lst) -> unions @@ List.map self lst
| E_variable name -> if mem name b then empty else singleton name
| E_application (a, b) -> unions @@ List.map self [ a ; b ]
| E_tuple lst -> unions @@ List.map self lst
| E_constructor (_ , a) -> self a
| E_record m -> unions @@ List.map self @@ Map.String.to_list m
| E_record_accessor (a, _) -> self a
| E_tuple_accessor (a, _) -> self a
| E_list lst -> unions @@ List.map self lst
| E_map m -> unions @@ List.map self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m
| E_look_up (a , b) -> unions @@ List.map self [ a ; b ]
| E_matching (a , cs) -> union (self a) (matching_expression b cs)
and annotated_expression : bindings -> annotated_expression -> bindings = fun b ae ->
expression b ae.expression
and instruction' : bindings -> instruction -> bindings * bindings = fun b i ->
match i with
| I_declaration n -> union (singleton n.name) b , (annotated_expression b n.annotated_expression)
| I_assignment n -> b , (annotated_expression b n.annotated_expression)
| I_skip -> b , empty
| I_fail e -> b , annotated_expression b e
| I_loop (a , bl) -> b , union (annotated_expression b a) (block b bl)
| I_patch (_ , _ , a) -> b , annotated_expression b a
| I_matching (a , cs) -> b , union (annotated_expression b a) (matching_block b cs)
and block : bindings -> block -> bindings = fun b bl ->
let aux = fun (binds, frees) cur ->
let (binds', frees') = instruction' binds cur in
(binds', union frees frees') in
let (_, frees) = List.fold_left aux (b , []) bl in
frees
and matching : type a . (bindings -> a -> bindings) -> bindings -> a matching -> bindings = fun f b m ->
match m with
| Match_bool { match_true = t ; match_false = fa } -> union (f b t) (f b fa)
| Match_list { match_nil = n ; match_cons = (hd, tl, c) } -> union (f b n) (f (union (of_list [hd ; tl]) b) c)
| Match_option { match_none = n ; match_some = ((opt, _), s) } -> union (f b n) (f (union (singleton opt) b) s)
| Match_tuple (lst, a) -> f (union (of_list lst) b) a
and matching_expression = fun x -> matching annotated_expression x
and matching_block = fun x -> matching block x
end
module Errors = struct
let different_kinds a b () =

View File

@ -0,0 +1,4 @@
function foo (const i : int) : int is
function bar (const j : int) : int is
block { skip } with i + j ;
block { skip } with bar (0)

View File

@ -0,0 +1,8 @@
function inc ( const i : int ) : int is
block { skip } with i + 1
function double_inc ( const i : int ) : int is
block { skip } with inc(inc(i))
function foo ( const i : int ) : int is
block { skip } with inc(i) + double_inc(i)

View File

@ -173,7 +173,13 @@ let easy_run_typed
let%bind mini_c_value = transpile_value input in
let%bind mini_c_result =
trace (simple_error "run mini_c") @@
let error =
let title () = "run Mini_c" in
let content () =
Format.asprintf "\n%a" Mini_c.PP.function_ mini_c_main.content
in
error title content in
trace error @@
Mini_c.Run.run_entry mini_c_main mini_c_value in
let%bind typed_result =
let%bind main_result_type =

View File

@ -105,7 +105,9 @@ and statement ppf ((s, _) : statement) = match s with
| S_while (e, b) -> fprintf ppf "while (%a) %a" expression e block b
and block ppf ((b, _):block) =
fprintf ppf "{ @;@[<v 2>%a@]@;}" (pp_print_list ~pp_sep:(tag "@;") statement) b
match b with
| [] -> fprintf ppf "{}"
| b -> fprintf ppf "{@; @[<v>%a@]@;}" (pp_print_list ~pp_sep:(tag "@;") statement) b
let tl_statement ppf (ass, _) = assignment ppf ass

View File

@ -114,7 +114,7 @@ and translate_function ({capture;content}:anon_function) : michelson result =
and translate_expression ((expr', ty, env) as expr:expression) : michelson result =
let error_message () = Format.asprintf "%a" PP.expression expr in
let%bind (code : michelson) =
trace (fun () -> error (thunk "translating expression") error_message ()) @@
trace (error (thunk "translating expression") error_message) @@
match expr' with
| E_literal v ->
let%bind v = translate_value v in
@ -411,16 +411,16 @@ and translate_regular_block ((b, env):block) : michelson result =
let%bind instruction = translate_statement statement in
ok (instruction :: lst)
in
let error_message () =
let%bind schema_michelson = Environment.to_michelson_type env.pre_environment in
ok @@ Format.asprintf "\nblock : %a\nschema : %a\n"
PP.block (b, env)
Tezos_utils.Micheline.Michelson.pp schema_michelson
in
let%bind codes =
let error_message () =
let%bind schema_michelson = Environment.to_michelson_type env.pre_environment in
ok @@ Format.asprintf "\nblock : %a\nschema : %a\n"
PP.block (b, env)
Tezos_utils.Micheline.Michelson.pp schema_michelson
in
trace_r (fun () ->
let%bind error_message = error_message () in
ok (fun () -> error (thunk "error translating block")
ok (fun () -> error (thunk "translating regular block")
(fun () -> error_message)
())) @@
List.fold_left aux (ok []) b in
@ -447,9 +447,9 @@ and translate_function_body ({body;result} as f:anon_function_content) : michels
Tezos_utils.Micheline.Michelson.pp code
in
let%bind _ =
Trace.trace_tzresult_lwt (fun () -> error (thunk "error parsing function code")
error_message
()) @@
Trace.trace_tzresult_lwt (
error (thunk "error parsing function code") error_message
) @@
Tezos_utils.Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty
in
@ -487,7 +487,9 @@ let translate_program (p:program) (entry:string) : compiled_program result =
let translate_entry (p:anon_function) : compiled_program result =
let {input;output} : anon_function_content = p.content in
let%bind body = translate_function_body p.content in
let%bind body =
trace (simple_error "compile entry body") @@
translate_function_body p.content in
let%bind input = Compiler_type.Ty.type_ input in
let%bind output = Compiler_type.Ty.type_ output in
ok ({input;output;body}:compiled_program)

View File

@ -30,7 +30,15 @@ let run_node (program:program) (input:Michelson.t) : Michelson.t result =
ok output
let run_entry (entry:anon_function) (input:value) : value result =
let%bind compiled = translate_entry entry in
let%bind compiled =
let error =
let title () = "compile entry" in
let content () =
Format.asprintf "%a" PP.function_ entry.content
in
error title content in
trace error @@
translate_entry entry in
let%bind input_michelson = translate_value input in
let%bind ex_ty_value = run_aux compiled input_michelson in
let%bind (result : value) = Uncompiler.translate_value ex_ty_value in

View File

@ -242,7 +242,16 @@ and simpl_tuple_expression (lst:Raw.expr list) : ae result =
and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result =
match t with
| LocalData d -> simpl_data_declaration d
| LocalLam _ -> simple_fail "no local lambdas yet"
| LocalLam l -> simpl_lambda_declaration l
and simpl_lambda_declaration : Raw.lambda_decl -> (instruction * named_expression) result =
fun l ->
match l with
| FunDecl f ->
let%bind e = simpl_fun_declaration (f.value) in
ok (I_assignment e, e)
| ProcDecl _ -> simple_fail "no local procedure yet"
| EntryDecl _ -> simple_fail "no local entry-point yet"
and simpl_data_declaration (t:Raw.data_decl) : (instruction * named_expression) result =
let return x = ok (I_assignment x, x) in
@ -276,6 +285,70 @@ and simpl_param : Raw.param_decl -> named_type_expression result = fun t ->
let%bind type_expression = simpl_type_expression c.param_type in
ok { type_name ; type_expression }
and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
let open! Raw in
let {name;param;ret_type;local_decls;block;return} : fun_decl = x in
(match npseq_to_list param.value.inside with
| [] -> simple_fail "function without parameters are not allowed"
| [a] -> (
let%bind input = simpl_param a in
let name = name.value in
let binder = input.type_name in
let input_type = input.type_expression in
let%bind local_declarations =
let%bind tmp = bind_list
@@ List.map simpl_local_declaration local_decls in
ok (List.map fst tmp) in
let%bind instructions = bind_list
@@ List.map simpl_statement
@@ npseq_to_list block.value.statements in
let%bind result = simpl_expression return in
let%bind output_type = simpl_type_expression ret_type in
let body = local_declarations @ instructions in
let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (T_function (input_type, output_type)) in
ok {name;annotated_expression = {expression;type_annotation}}
)
| lst -> (
let%bind params = bind_map_list simpl_param lst in
let input =
let type_expression = T_record (
SMap.of_list
@@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression)
params
) in
{ type_name = "arguments" ; type_expression } in
let binder = input.type_name in
let input_type = input.type_expression in
let%bind local_declarations =
let%bind typed = bind_map_list simpl_local_declaration local_decls in
ok (List.map fst typed)
in
let%bind output_type = simpl_type_expression ret_type in
let%bind instructions = bind_list
@@ List.map simpl_statement
@@ npseq_to_list block.value.statements in
let%bind (body, result) =
let renamings =
let aux ({type_name}:named_type_expression) : Rename.Value.renaming =
type_name, ("arguments", [Access_record type_name])
in
List.map aux params
in
let%bind r =
let%bind tmp = simpl_expression return in
Rename.Value.rename_annotated_expression renamings tmp
in
let%bind b =
let tmp = local_declarations @ instructions in
Rename.Value.rename_block renamings tmp
in
ok (b, r) in
let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (T_function (input_type, output_type)) in
ok {name = name.value;annotated_expression = {expression;type_annotation}}
)
)
and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fun t ->
let open! Raw in
let loc : 'a . 'a Raw.reg -> _ -> _ = fun x v -> Location.wrap ~loc:(File x.region) v in
@ -285,80 +358,18 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu
let%bind type_expression = simpl_type_expression type_expr in
ok @@ loc x @@ Declaration_type {type_name=name.value;type_expression}
| ConstDecl x ->
let {name;const_type;init} = x.value in
let%bind expression = simpl_expression init in
let%bind t = simpl_type_expression const_type in
let type_annotation = Some t in
ok @@ loc x @@ Declaration_constant {name=name.value;annotated_expression={expression with type_annotation}}
let simpl_const_decl = fun {name;const_type;init} ->
let%bind expression = simpl_expression init in
let%bind t = simpl_type_expression const_type in
let type_annotation = Some t in
ok @@ Declaration_constant {name=name.value;annotated_expression={expression with type_annotation}}
in
bind_map_location simpl_const_decl (Location.lift_region x)
| LambdaDecl (FunDecl x) ->
let {name;param;ret_type;local_decls;block;return} : fun_decl = x.value in
(match npseq_to_list param.value.inside with
| [] -> simple_fail "function without parameters are not allowed"
| [a] -> (
let%bind input = simpl_param a in
let name = name.value in
let binder = input.type_name in
let input_type = input.type_expression in
let%bind local_declarations =
let%bind tmp = bind_list
@@ List.map simpl_local_declaration local_decls in
ok (List.map fst tmp) in
let%bind instructions = bind_list
@@ List.map simpl_statement
@@ npseq_to_list block.value.statements in
let%bind result = simpl_expression return in
let%bind output_type = simpl_type_expression ret_type in
let body = local_declarations @ instructions in
let decl =
let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (T_function (input_type, output_type)) in
Declaration_constant {name;annotated_expression = {expression;type_annotation}}
in
ok @@ loc x @@ decl
)
| lst -> (
let%bind params = bind_map_list simpl_param lst in
let input =
let type_expression = T_record (
SMap.of_list
@@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression)
params
) in
{ type_name = "arguments" ; type_expression } in
let binder = input.type_name in
let input_type = input.type_expression in
let%bind local_declarations =
let%bind typed = bind_map_list simpl_local_declaration local_decls in
ok (List.map fst typed)
in
let%bind output_type = simpl_type_expression ret_type in
let%bind instructions = bind_list
@@ List.map simpl_statement
@@ npseq_to_list block.value.statements in
let%bind (body, result) =
let renamings =
let aux ({type_name}:named_type_expression) : Rename.Value.renaming =
type_name, ("arguments", [Access_record type_name])
in
List.map aux params
in
let%bind r =
let%bind tmp = simpl_expression return in
Rename.Value.rename_annotated_expression renamings tmp
in
let%bind b =
let tmp = local_declarations @ instructions in
Rename.Value.rename_block renamings tmp
in
ok (b, r) in
let decl =
let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (T_function (input_type, output_type)) in
Declaration_constant {name = name.value;annotated_expression = {expression;type_annotation}}
in
ok @@ loc x @@ decl
)
)
let aux f x =
let%bind x' = f x in
ok @@ Declaration_constant x' in
bind_map_location (aux simpl_fun_declaration) (Location.lift_region x)
| LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet"
| LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet"

View File

@ -41,6 +41,58 @@ let complex_function () : unit result =
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let closure () : unit result =
let%bind program = type_file "./contracts/closure.ligo" in
let%bind _foo = trace (simple_error "test foo") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let%bind result = easy_run_typed "foo" program input in
let expected = e_a_int ( n + 1 ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let shared_function () : unit result =
let%bind program = type_file "./contracts/function-shared.ligo" in
let%bind _inc = trace (simple_error "test inc") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let%bind result = easy_run_typed "inc" program input in
let expected = e_a_int ( n + 1 ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
let%bind _double_inc = trace (simple_error "test double_inc") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let%bind result = easy_run_typed "double_inc" program input in
let expected = e_a_int ( n + 2 ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
let%bind _foo = trace (simple_error "test foo") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let%bind result = easy_run_typed "foo" program input in
let expected = e_a_int ( 2 * n + 3 ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let bool_expression () : unit result =
let%bind program = type_file "./contracts/boolean_operators.ligo" in
let aux (name, f) =
@ -272,15 +324,6 @@ let list () : unit result =
let lst' = List.map e_a_int lst in
e_a_list lst' (t_int ())
in
(* let%bind _get_force = trace (simple_error "hd_force") @@
* let aux n =
* let input = ez [n ; 12] in
* let%bind result = easy_run_typed "hdf" program input in
* let expect = AST_Typed.Combinators.(e_a_int n) in
* AST_Typed.assert_value_eq (expect, result)
* in
* bind_map_list aux [0 ; 42 ; 51 ; 421 ; -3]
* in *)
let%bind _size = trace (simple_error "size") @@
let aux n =
let input = ez (List.range n) in
@ -480,6 +523,8 @@ let main = "Integration (End to End)", [
test "basic" basic ;
test "function" function_ ;
test "complex function" complex_function ;
test "closure" closure ;
test "shared function" shared_function ;
test "bool" bool_expression ;
test "arithmetic" arithmetic ;
test "unit" unit_expression ;

View File

@ -336,23 +336,32 @@ and translate_lambda_shallow env l tv =
and translate_lambda env l tv =
let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in
(* Try to type it in an empty env, if it succeeds, transpiles it as a quote value, else, as a closure expression. *)
(* Try to translate it in an empty env, if it succeeds, transpiles it as a quote value, else, as a closure expression. *)
let%bind init_env =
let%bind input = translate_type input_type in
ok Environment.(add (binder, input) env) in
let%bind empty_env =
let%bind input = translate_type input_type in
ok Environment.(add (binder, input) empty) in
match to_option (translate_block init_env body) with
| Some ((_, e) as body) -> (
match to_option (translate_annotated_expression e.post_environment result) with
| Some result -> (
let capture_type = No_capture in
let%bind input = translate_type input_type in
let%bind output = translate_type output_type in
let content = {binder;input;output;body;result;capture_type} in
ok (E_literal (D_function {capture=None;content}), tv, env)
)
| _ -> translate_lambda_shallow init_env l tv
let (body_fvs, result_fvs) = AST.Free_variables.(
let bindings = singleton binder in
block bindings body , annotated_expression bindings result
) in
match (body_fvs, result_fvs) with
| [] , [] -> (
let%bind ((_, e) as body') = translate_block empty_env body in
let%bind result' = translate_annotated_expression e.post_environment result in
trace (simple_error "translate quote") @@
let capture_type = No_capture in
let%bind input = translate_type input_type in
let%bind output = translate_type output_type in
let content = {binder;input;output;body=body';result=result';capture_type} in
ok (E_literal (D_function {capture=None;content}), tv, env)
)
| _ -> (
trace (simple_error "translate lambda shallow") @@
translate_lambda_shallow init_env l tv
)
| _ -> translate_lambda_shallow init_env l tv
let translate_declaration env (d:AST.declaration) : toplevel_statement result =
match d with
@ -390,30 +399,29 @@ let functionalize (e:AST.annotated_expression) : AST.lambda * AST.type_value =
}, Combinators.(t_function (t_unit ()) t ())
let translate_entry (lst:AST.program) (name:string) : anon_function result =
let rec aux acc (lst:AST.program) =
match lst with
| [] -> None
| hd :: tl -> (
let AST.Declaration_constant an = temp_unwrap_loc hd in
if an.name = name
then (
match an.annotated_expression.expression with
| E_lambda l -> Some (acc, l, an.annotated_expression.type_annotation)
| _ ->
let (a, b) = functionalize an.annotated_expression in
Some (acc, a, b)
) else (
aux ((AST.I_declaration an) :: acc) tl
)
)
in
let%bind (lst', l, tv) =
let rec aux acc (lst:AST.program) =
match lst with
| [] -> None
| hd :: tl -> (
let (AST.Declaration_constant an) = temp_unwrap_loc hd in
match an.name = name with
| true -> (
match an.annotated_expression.expression with
| E_lambda l -> Some (acc, l, an.annotated_expression.type_annotation)
| _ ->
let (a, b) = functionalize an.annotated_expression in
Some (acc, a, b)
)
| false -> aux (acc @ [AST.I_declaration an]) tl
)
in
let%bind (lst', l, tv) =
trace_option (simple_error "no entry-point with given name")
@@ aux [] lst in
ok (List.rev lst', l, tv) in
ok (lst', l, tv) in
let l' = {l with body = lst' @ l.body} in
trace (simple_error "translate entry")
trace (simple_error "translating entry")
@@ translate_main l' tv
open Combinators