multiple parameters

This commit is contained in:
Galfour 2019-03-28 10:26:25 +00:00
parent 4025e9e169
commit 2ae73f80a9
9 changed files with 137 additions and 80 deletions

View File

@ -150,6 +150,10 @@ module PP = struct
and access_path ppf (p:access_path) =
fprintf ppf "%a" (list_sep ~pp_sep:(const ".") access) p
and type_annotation ppf (ta:type_expression option) = match ta with
| None -> fprintf ppf ""
| Some t -> type_expression ppf t
and annotated_expression ppf (ae:annotated_expression) = match ae.type_annotation with
| None -> fprintf ppf "%a" expression ae.expression
| Some t -> fprintf ppf "(%a) : %a" expression ae.expression type_expression t
@ -461,7 +465,8 @@ module Simplify = struct
let%bind lst = bind_list @@ List.map simpl_expression lst in
ok @@ ae @@ Tuple lst
and simpl_local_declaration (t:Raw.local_decl) : instruction result =
and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result =
let return x = ok (Assignment x, x) in
match t with
| LocalVar x ->
let x = x.value in
@ -469,14 +474,14 @@ module Simplify = struct
let%bind t = simpl_type_expression x.var_type in
let type_annotation = Some t in
let%bind expression = simpl_expression x.init in
ok @@ Assignment {name;annotated_expression={expression with type_annotation}}
return {name;annotated_expression={expression with type_annotation}}
| LocalConst x ->
let x = x.value in
let name = x.name.value in
let%bind t = simpl_type_expression x.const_type in
let type_annotation = Some t in
let%bind expression = simpl_expression x.init in
ok @@ Assignment {name;annotated_expression={expression with type_annotation}}
return {name;annotated_expression={expression with type_annotation}}
| _ -> simple_fail "todo"
and simpl_param (t:Raw.param_decl) : named_type_expression result =
@ -514,7 +519,10 @@ module Simplify = struct
let name = name.value in
let binder = input.type_name in
let input_type = input.type_expression in
let%bind local_declarations = bind_list @@ List.map simpl_local_declaration local_decls 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_instruction
@@ npseq_to_list block.value.instr in
@ -536,11 +544,13 @@ module Simplify = struct
@@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression)
params
) in
{ type_name = "arguments" ; type_expression } in
{ type_name = "arguments" ; type_expression } in
let binder = input.type_name in
let input_type = input.type_expression in
let%bind local_declarations =
bind_list @@ List.map simpl_local_declaration local_decls in
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_instruction
@ -552,7 +562,10 @@ module Simplify = struct
in
List.map aux params
in
let%bind r = simpl_expression return 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
@ -561,7 +574,7 @@ module Simplify = struct
let decl =
let expression = Lambda {binder ; input_type ; output_type ; result ; body } in
let type_annotation = Some (Type_function (input_type, output_type)) in
Constant_declaration {name="arguments";annotated_expression = {expression;type_annotation}}
Constant_declaration {name = name.value;annotated_expression = {expression;type_annotation}}
in
ok decl
)

View File

@ -209,15 +209,19 @@ module Errors = struct
let full = Format.asprintf "%s VS %s" a b in
error title full
let different_size_constants a b =
let title = "constants have different sizes" in
let different_size_type name a b =
let title = name ^ " have different sizes" in
let full = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in
error title full
let different_size_tuples a b =
let title = "tuple have different sizes" in
let full = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in
error title full
let different_size_constants = different_size_type "constants"
let different_size_tuples = different_size_type "tuples"
let different_size_sums = different_size_type "sums"
let different_size_records = different_size_type "records"
end
open Errors
@ -240,31 +244,37 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
@@ bind_list_iter assert_type_value_eq (List.combine lsta lstb)
)
| Type_constant _, _ -> fail @@ different_kinds a b
| Type_sum a, Type_sum b -> (
let a' = list_of_smap a in
let b' = list_of_smap b in
| Type_sum sa, Type_sum sb -> (
let sa' = list_of_smap sa in
let sb' = list_of_smap sb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in sum types"
@@ (ka = kb) in
assert_type_value_eq (va, vb)
in
trace (simple_error "sum type")
@@ bind_list_iter aux (List.combine a' b')
let%bind _ =
trace_strong (different_size_sums a b)
@@ Assert.assert_list_same_size sa' sb' in
trace (simple_error "sum type") @@
bind_list_iter aux (List.combine sa' sb')
)
| Type_sum _, _ -> fail @@ different_kinds a b
| Type_record a, Type_record b -> (
let a' = list_of_smap a in
let b' = list_of_smap b in
| Type_record ra, Type_record rb -> (
let ra' = list_of_smap ra in
let rb' = list_of_smap rb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in record types"
@@ (ka = kb) in
assert_type_value_eq (va, vb)
in
let%bind _ =
trace_strong (different_size_records a b)
@@ Assert.assert_list_same_size ra' rb' in
trace (simple_error "record type")
@@ bind_list_iter aux (List.combine a' b')
@@ bind_list_iter aux (List.combine ra' rb')
)
| Type_record _, _ -> fail @@ different_kinds a b
@ -325,6 +335,9 @@ module Combinators = struct
type_value (Type_record map) None
let make_t_record m = t_record m None
let make_t_record_ez lst =
let m = SMap.of_list lst in
make_t_record m
let t_sum m s : type_value = type_value (Type_sum m) s
let make_t_sum m = t_sum m None
@ -358,10 +371,12 @@ module Combinators = struct
| Type_record m -> ok m
| _ -> simple_fail "not a record"
let record (lst : (string * ae) list) : expression =
let record map : expression = Record map
let record_ez (lst : (string * ae) list) : expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
Record map
record map
let int n : expression = Literal (Int n)
let bool b : expression = Literal (Bool b)
@ -370,6 +385,8 @@ module Combinators = struct
let a_int n = annotated_expression (int n) make_t_int
let a_bool b = annotated_expression (bool b) make_t_bool
let a_pair a b = annotated_expression (pair a b) (make_t_pair a.type_annotation b.type_annotation)
let a_record r = annotated_expression (record r) (make_t_record (SMap.map (fun x -> x.type_annotation) r))
let a_record_ez r = annotated_expression (record_ez r) (make_t_record_ez (List.map (fun (x, y) -> x, y.type_annotation) r))
let get_a_int (t:annotated_expression) =
match t.expression with

View File

@ -1,2 +1,2 @@
function bi(const a : int; const b : int) : int is
function main(const a : int; const b : int) : int is
begin skip end with (a + b)

View File

@ -66,6 +66,13 @@ let bind_smap (s:_ X_map.String.t) =
ok @@ add k v' prev' in
fold aux s (ok empty)
let bind_fold_smap f init (smap : _ X_map.String.t) =
let aux k v prev =
prev >>? fun prev' ->
f prev' k v
in
X_map.String.fold aux smap init
let bind_map_list f lst = bind_list (List.map f lst)
let bind_fold_list f init lst =

View File

@ -105,9 +105,9 @@ let type_file ?(debug_simplify = false) ?(debug_typed = false)
let%bind typed =
trace (simple_error "typing") @@
type_ simpl in
(if debug_typed then
Format.(printf "Typed : %a\n%!" AST_Typed.PP.program typed)
) ;
(if debug_typed then (
Format.(printf "Typed : %a\n%!" AST_Typed.PP.program typed)
)) ;
ok typed
let easy_run_typed

View File

@ -104,11 +104,6 @@ and block = block' * environment_wrap
and program = toplevel_statement list
let expression_to_value ((e, _, _):expression) : value result =
match e with
| Literal v -> ok v
| _ -> simple_fail "not a value"
module PP = struct
open Format
open Ligo_helpers.PP
@ -192,6 +187,13 @@ module PP = struct
fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p
end
let expression_to_value ((e', _, _) as e:expression) : value result =
match e' with
| Literal v -> ok v
| _ -> fail
@@ error "not a value"
@@ Format.asprintf "%a" PP.expression e
module Free_variables = struct
type free_variable = string
type free_variables = free_variable list
@ -627,6 +629,8 @@ module Translate_program = struct
| "OR" -> ok @@ simple_binary @@ prim I_OR
| "AND" -> ok @@ simple_binary @@ prim I_AND
| "PAIR" -> ok @@ simple_binary @@ prim I_PAIR
| "CAR" -> ok @@ simple_unary @@ prim I_CAR
| "CDR" -> ok @@ simple_unary @@ prim I_CDR
| "EQ" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_EQ]
| x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist"
@ -774,20 +778,21 @@ module Translate_program = struct
let%bind () =
let%bind (Ex_ty schema_ty) = Environment.to_ty env in
let%bind output_ty = Translate_type.type_ ty in
let%bind output_type = Translate_type.type_ ty in
let%bind (Ex_ty output_ty) =
let error_message = Format.asprintf "%a" Michelson.pp output_ty in
let error_message = Format.asprintf "%a" Michelson.pp output_type in
Trace.trace_tzresult_lwt (error "error parsing output ty" error_message) @@
Tezos_utils.Memory_proto_alpha.parse_michelson_ty output_ty in
Tezos_utils.Memory_proto_alpha.parse_michelson_ty output_type in
let input_stack_ty = Stack.(Types.unit @: schema_ty @: nil) in
let output_stack_ty = Stack.(Types.(pair output_ty unit) @: schema_ty @: nil) in
let%bind error_message =
let%bind schema_michelson = Environment.to_michelson_type env in
ok @@ Format.asprintf
"expression : %a\ncode : %a\nschema type : %a"
"expression : %a\ncode : %a\nschema type : %a\noutput type : %a"
PP.expression (expr', ty, env)
Tezos_utils.Micheline.Michelson.pp code
Tezos_utils.Micheline.Michelson.pp schema_michelson
Michelson.pp code
Michelson.pp schema_michelson
Michelson.pp output_type
in
let%bind _ =
Trace.trace_tzresult_lwt (error "error parsing expression code" error_message) @@
@ -1025,6 +1030,10 @@ module Combinators = struct
| `Pair (a, b) -> ok (a, b)
| _ -> simple_fail "not a pair"
let get_t_pair (t:type_value) = match t with
| `Pair (a, b) -> ok (a, b)
| _ -> simple_fail "not a type pair"
let get_left (v:value) = match v with
| `Left b -> ok b
| _ -> simple_fail "not a left"

View File

@ -42,15 +42,18 @@ let complex_function () : unit result =
ok ()
let multiple_parameters () : unit result =
let%bind program = type_file "./contracts/multiple-parameters.ligo" in
let%bind program = type_file ~debug_typed:true "./contracts/multiple-parameters.ligo" in
let aux n =
let open AST_Typed.Combinators in
let input = a_int n in
let input = a_record_ez [
("a", a_int n) ;
("b", a_int n) ;
] in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
get_a_int result in
Assert.assert_equal_int (3 * n + 2) result'
Assert.assert_equal_int (2 * n) result'
in
let%bind _ = bind_list
@@ List.map aux

View File

@ -167,32 +167,32 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
ok (Predicate ("PAIR", [a; b]), `Pair(a_ty, b_ty), env)
in
Append_tree.fold_ne (translate_annotated_expression env) aux node
| Record_accessor (r, key) ->
let%bind (r'_expr, _, _) = translate_annotated_expression env r in
let%bind r_tv = get_t_record ae.type_annotation in
let node_tv = Append_tree.of_list @@ kv_list_of_map r_tv in
let%bind ae' =
let leaf (key', tv) : (expression' option * type_value) result =
let%bind tv = translate_type tv in
if key = key' then (
ok (Some (r'_expr), tv)
) else (
ok (None, tv)
| Record_accessor (record, property) ->
let%bind translation = translate_annotated_expression env record in
let%bind record_type_map =
trace (simple_error (Format.asprintf "Accessing field of %a, that has type %a, which isn't a record" AST.PP.annotated_expression record AST.PP.type_value record.type_annotation)) @@
get_t_record record.type_annotation in
let node_tv = Append_tree.of_list @@ kv_list_of_map record_type_map in
let leaf (key, _) : expression result =
if property = key then (
ok translation
) else (
simple_fail "bad leaf"
) in
let node (a:expression result) b : expression result =
match%bind bind_lr (a, b) with
| `Left ((_, t, env) as ex) -> (
let%bind (a, _) = get_t_pair t in
ok (Predicate ("CAR", [ex]), a, env)
)
| `Right ((_, t, env) as ex) -> (
let%bind (_, b) = get_t_pair t in
ok (Predicate ("CDR", [ex]), b, env)
) in
let node a b : (expression' option * type_value) result =
let%bind a = a in
let%bind b = b in
match (a, b) with
| (None, a), (None, b) -> ok (None, `Pair (a, b))
| (Some _, _), (Some _, _) -> simple_fail "several identical keys in the same record (shouldn't happen here)"
| (Some v, a), (None, b) -> ok (Some (Predicate ("CAR", [v, a, env])), `Pair (a, b))
| (None, a), (Some v, b) -> ok (Some (Predicate ("CDR", [v, b, env])), `Pair (a, b))
in
let%bind (ae_opt, tv) = Append_tree.fold_ne leaf node node_tv in
let%bind ae = trace_option (simple_error "bad key in record (shouldn't happen here)")
ae_opt in
ok (ae, tv, env) in
ok ae'
let%bind expr =
trace_strong (simple_error "bad key in record (shouldn't happen here)") @@
Append_tree.fold_ne leaf node node_tv in
ok expr
| Constant (name, lst) ->
let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in
ok (Predicate (name, lst'), tv, env)

View File

@ -70,8 +70,18 @@ module Errors = struct
let full = n in
error title full
let constant_declaration_error (name:string) =
error "typing constant declaration" name
let program_error (p:I.program) =
let title = "typing program" in
let full = Format.asprintf "%a" I.PP.program p in
error title full
let constant_declaration_error (name:string) (ae:I.ae) =
let title = "typing constant declaration" in
let full =
Format.asprintf "%s = %a" name
I.PP.annotated_expression ae
in
error title full
end
open Errors
@ -85,7 +95,7 @@ let rec type_program (p:I.program) : O.program result =
| Some d' -> ok (e', d' :: acc)
in
let%bind (_, lst) =
trace (simple_error "typing program") @@
trace (program_error p) @@
bind_fold_list aux (Environment.empty, []) p in
ok @@ List.rev lst
@ -96,7 +106,7 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
ok (env', None)
| Constant_declaration {name;annotated_expression} ->
let%bind ae' =
trace (constant_declaration_error name) @@
trace (constant_declaration_error name annotated_expression) @@
type_annotated_expression env annotated_expression in
let env' = Environment.add env name ae'.type_annotation in
ok (env', Some (O.Constant_declaration {name;annotated_expression=ae'}))
@ -181,10 +191,9 @@ and type_match (e:environment) (t:O.type_value) : I.matching -> O.matching resul
let%bind t_tuple =
trace_strong (simple_error "Matching tuple on not-a-tuple")
@@ get_t_tuple t in
let%bind _ =
trace_strong (simple_error "Matching tuple of different size")
@@ Assert.assert_list_same_size t_tuple lst in
let lst' = List.combine lst t_tuple in
let%bind lst' =
generic_try (simple_error "Matching tuple of different size")
@@ (fun () -> List.combine lst t_tuple) in
let aux prev (name, tv) = Environment.add prev name tv in
let e' = List.fold_left aux e lst' in
let%bind b' = type_block e' b in
@ -293,12 +302,11 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
ok O.{expression = O.Constructor(c, expr') ; type_annotation }
(* Record *)
| Record m ->
let aux k expr prev =
let%bind prev' = prev in
let aux prev k expr =
let%bind expr' = type_annotated_expression e expr in
ok (SMap.add k expr' prev')
ok (SMap.add k expr' prev)
in
let%bind m' = SMap.fold aux m (ok SMap.empty) in
let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
let%bind type_annotation = check @@ make_t_record (SMap.map get_annotation m') in
ok O.{expression = O.Record m' ; type_annotation }
| Lambda {