From 614970d2d759d763a492246e97ab455fd0b058ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Sat, 9 Nov 2019 02:45:43 +0100 Subject: [PATCH 1/4] Implemented some missing cases of the subst. First kinda actual typer test passes! --- src/passes/4-typer-new/solver.ml | 48 +++++++++--------- src/passes/4-typer-new/typer.ml | 29 +++++++++++ src/stages/ast_typed/misc.ml | 1 + src/stages/common/ast_common.ml | 1 + src/stages/common/misc.ml | 85 ++++++++++++++++++++++++++++++++ src/stages/typesystem/core.ml | 32 ++++++++++++ src/stages/typesystem/misc.ml | 38 +++++++++----- 7 files changed, 200 insertions(+), 34 deletions(-) create mode 100644 src/stages/common/misc.ml diff --git a/src/passes/4-typer-new/solver.ml b/src/passes/4-typer-new/solver.ml index e5f12b144..2adac9659 100644 --- a/src/passes/4-typer-new/solver.ml +++ b/src/passes/4-typer-new/solver.ml @@ -729,94 +729,98 @@ let compare_simple_c_constant = function | C_arrow -> (function (* N/A -> 1 *) | C_arrow -> 0 - | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_option -> (function | C_arrow -> 1 | C_option -> 0 - | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_tuple -> (function | C_arrow | C_option -> 1 | C_tuple -> 0 - | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_record -> (function | C_arrow | C_option | C_tuple -> 1 | C_record -> 0 - | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_variant -> (function | C_arrow | C_option | C_tuple | C_record -> 1 | C_variant -> 0 - | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_map -> (function | C_arrow | C_option | C_tuple | C_record | C_variant -> 1 | C_map -> 0 - | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_big_map -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map -> 1 | C_big_map -> 0 - | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_list -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map -> 1 | C_list -> 0 - | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_set -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list -> 1 | C_set -> 0 - | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_unit -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1 | C_unit -> 0 - | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_bool -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1 | C_bool -> 0 - | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_string -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool -> 1 | C_string -> 0 - | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_nat -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string -> 1 | C_nat -> 0 - | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_mutez -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat -> 1 | C_mutez -> 0 - | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_timestamp -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez -> 1 | C_timestamp -> 0 - | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_int -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp -> 1 | C_int -> 0 - | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_address -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1 | C_address -> 0 - | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_bytes -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1 | C_bytes -> 0 - | C_key_hash | C_key | C_signature | C_operation | C_contract -> -1) + | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_key_hash -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1 | C_key_hash -> 0 - | C_key | C_signature | C_operation | C_contract -> -1) + | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_key -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1 | C_key -> 0 - | C_signature | C_operation | C_contract -> -1) + | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_signature -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1 | C_signature -> 0 - | C_operation | C_contract -> -1) + | C_operation | C_contract | C_chain_id -> -1) | C_operation -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1 | C_operation -> 0 - | C_contract -> -1) + | C_contract | C_chain_id -> -1) | C_contract -> (function | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1 | C_contract -> 0 + | C_chain_id -> -1) + | C_chain_id -> (function + | C_arrow | C_option | C_tuple | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1 + | C_chain_id -> 0 (* N/A -> -1 *) ) let rec compare_typeclass a b = compare_list (compare_list compare_type_value) a b diff --git a/src/passes/4-typer-new/typer.ml b/src/passes/4-typer-new/typer.ml index 5d1d68465..537a4c485 100644 --- a/src/passes/4-typer-new/typer.ml +++ b/src/passes/4-typer-new/typer.ml @@ -956,12 +956,41 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p (* module TSMap = TMap(Solver.TypeVariable) *) +(* let c_tag_to_string : Solver.Core.constant_tag -> string = function + * | Solver.Core.C_arrow -> "arrow" + * | Solver.Core.C_option -> "option" + * | Solver.Core.C_tuple -> "tuple" + * | Solver.Core.C_record -> failwith "record" + * | Solver.Core.C_variant -> failwith "variant" + * | Solver.Core.C_map -> "map" + * | Solver.Core.C_big_map -> "big" + * | Solver.Core.C_list -> "list" + * | Solver.Core.C_set -> "set" + * | Solver.Core.C_unit -> "unit" + * | Solver.Core.C_bool -> "bool" + * | Solver.Core.C_string -> "string" + * | Solver.Core.C_nat -> "nat" + * | Solver.Core.C_mutez -> "mutez" + * | Solver.Core.C_timestamp -> "timestamp" + * | Solver.Core.C_int -> "int" + * | Solver.Core.C_address -> "address" + * | Solver.Core.C_bytes -> "bytes" + * | Solver.Core.C_key_hash -> "key_hash" + * | Solver.Core.C_key -> "key" + * | Solver.Core.C_signature -> "signature" + * | Solver.Core.C_operation -> "operation" + * | Solver.Core.C_contract -> "contract" + * | Solver.Core.C_chain_id -> "chain_id" *) + let type_program (p : I.program) : (O.program * Solver.state) result = let%bind (env, state, program) = type_program_returns_state p in let subst_all = let assignments = state.structured_dbs.assignments in let aux (v : I.type_variable) (expr : Solver.c_constructor_simpl) (p:O.program result) = let%bind p = p in + let Solver.{ tv ; c_tag ; tv_list } = expr in + let () = ignore tv (* I think there is an issue where the tv is stored twice (as a key and in the element itself) *) in + let%bind (expr : O.type_value') = Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.{ type_value' = T_variable s ; simplified = None }) tv_list)) in Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in (* let p = TSMap.bind_fold_Map aux program assignments in *) (* TODO: Module magic: this does not work *) let p = Solver.TypeVariableMap.fold aux assignments (ok program) in diff --git a/src/stages/ast_typed/misc.ml b/src/stages/ast_typed/misc.ml index 6ece0d8ab..43d0c8792 100644 --- a/src/stages/ast_typed/misc.ml +++ b/src/stages/ast_typed/misc.ml @@ -1,5 +1,6 @@ open Trace open Types +include Stage_common.Misc module Errors = struct let different_kinds a b () = diff --git a/src/stages/common/ast_common.ml b/src/stages/common/ast_common.ml index 302205f4b..b570d3941 100644 --- a/src/stages/common/ast_common.ml +++ b/src/stages/common/ast_common.ml @@ -1,2 +1,3 @@ module Types = Types module PP = PP +module Misc = Misc diff --git a/src/stages/common/misc.ml b/src/stages/common/misc.ml new file mode 100644 index 000000000..7f38acf62 --- /dev/null +++ b/src/stages/common/misc.ml @@ -0,0 +1,85 @@ +open Types +open Trace + +let map_type_operator f = function + TC_contract x -> TC_contract (f x) + | TC_option x -> TC_option (f x) + | TC_list x -> TC_list (f x) + | TC_set x -> TC_set (f x) + | TC_map (x , y) -> TC_map (f x , f y) + | TC_big_map (x , y)-> TC_big_map (f x , f y) + +let bind_map_type_operator f = function + TC_contract x -> let%bind x = f x in ok @@ TC_contract x + | TC_option x -> let%bind x = f x in ok @@ TC_option x + | TC_list x -> let%bind x = f x in ok @@ TC_list x + | TC_set x -> let%bind x = f x in ok @@ TC_set x + | TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y) + | TC_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y) + +let type_operator_name = function + TC_contract _ -> "TC_contract" + | TC_option _ -> "TC_option" + | TC_list _ -> "TC_list" + | TC_set _ -> "TC_set" + | TC_map _ -> "TC_map" + | TC_big_map _ -> "TC_big_map" + +let type_expression'_of_string = function + | "TC_contract" , [x] -> ok @@ T_operator(TC_contract x) + | "TC_option" , [x] -> ok @@ T_operator(TC_option x) + | "TC_list" , [x] -> ok @@ T_operator(TC_list x) + | "TC_set" , [x] -> ok @@ T_operator(TC_set x) + | "TC_map" , [x ; y] -> ok @@ T_operator(TC_map (x , y)) + | "TC_big_map" , [x ; y] -> ok @@ T_operator(TC_big_map (x, y)) + | ("TC_contract" | "TC_option" | "TC_list" | "TC_set" | "TC_map" | "TC_big_map"), _ -> + failwith "internal error: wrong number of arguments for type operator" + + | "TC_unit" , [] -> ok @@ T_constant(TC_unit) + | "TC_string" , [] -> ok @@ T_constant(TC_string) + | "TC_bytes" , [] -> ok @@ T_constant(TC_bytes) + | "TC_nat" , [] -> ok @@ T_constant(TC_nat) + | "TC_int" , [] -> ok @@ T_constant(TC_int) + | "TC_mutez" , [] -> ok @@ T_constant(TC_mutez) + | "TC_bool" , [] -> ok @@ T_constant(TC_bool) + | "TC_operation" , [] -> ok @@ T_constant(TC_operation) + | "TC_address" , [] -> ok @@ T_constant(TC_address) + | "TC_key" , [] -> ok @@ T_constant(TC_key) + | "TC_key_hash" , [] -> ok @@ T_constant(TC_key_hash) + | "TC_chain_id" , [] -> ok @@ T_constant(TC_chain_id) + | "TC_signature" , [] -> ok @@ T_constant(TC_signature) + | "TC_timestamp" , [] -> ok @@ T_constant(TC_timestamp) + | _, [] -> + failwith "internal error: wrong number of arguments for type constant" + | _ -> + failwith "internal error: unknown type operator" + +let string_of_type_operator = function + | TC_contract x -> "TC_contract" , [x] + | TC_option x -> "TC_option" , [x] + | TC_list x -> "TC_list" , [x] + | TC_set x -> "TC_set" , [x] + | TC_map (x , y) -> "TC_map" , [x ; y] + | TC_big_map (x , y) -> "TC_big_map" , [x ; y] + +let string_of_type_constant = function + | TC_unit -> "TC_unit", [] + | TC_string -> "TC_string", [] + | TC_bytes -> "TC_bytes", [] + | TC_nat -> "TC_nat", [] + | TC_int -> "TC_int", [] + | TC_mutez -> "TC_mutez", [] + | TC_bool -> "TC_bool", [] + | TC_operation -> "TC_operation", [] + | TC_address -> "TC_address", [] + | TC_key -> "TC_key", [] + | TC_key_hash -> "TC_key_hash", [] + | TC_chain_id -> "TC_chain_id", [] + | TC_signature -> "TC_signature", [] + | TC_timestamp -> "TC_timestamp", [] + +let string_of_type_expression' = function + | T_operator o -> string_of_type_operator o + | T_constant c -> string_of_type_constant c + | T_tuple _|T_sum _|T_record _|T_arrow (_, _)|T_variable _ -> + failwith "not a type operator or constant" diff --git a/src/stages/typesystem/core.ml b/src/stages/typesystem/core.ml index 30a3a5fa5..c21888908 100644 --- a/src/stages/typesystem/core.ml +++ b/src/stages/typesystem/core.ml @@ -31,6 +31,7 @@ type constant_tag = | C_signature (* * *) | C_operation (* * *) | C_contract (* * -> * *) + | C_chain_id (* * *) type accessor = | L_int of int @@ -67,3 +68,34 @@ and type_constraint = (* is the first list in case on of the type of the type class as a kind *->*->* ? *) and typeclass = type_value list list + +open Trace +let type_expression'_of_simple_c_constant = function + | C_contract , [x] -> ok @@ T_operator(TC_contract x) + | C_option , [x] -> ok @@ T_operator(TC_option x) + | C_list , [x] -> ok @@ T_operator(TC_list x) + | C_set , [x] -> ok @@ T_operator(TC_set x) + | C_map , [x ; y] -> ok @@ T_operator(TC_map (x , y)) + | C_big_map , [x ; y] -> ok @@ T_operator(TC_big_map (x, y)) + | (C_contract | C_option | C_list | C_set | C_map | C_big_map), _ -> + failwith "internal error: wrong number of arguments for type operator" + + | C_unit , [] -> ok @@ T_constant(TC_unit) + | C_string , [] -> ok @@ T_constant(TC_string) + | C_bytes , [] -> ok @@ T_constant(TC_bytes) + | C_nat , [] -> ok @@ T_constant(TC_nat) + | C_int , [] -> ok @@ T_constant(TC_int) + | C_mutez , [] -> ok @@ T_constant(TC_mutez) + | C_bool , [] -> ok @@ T_constant(TC_bool) + | C_operation , [] -> ok @@ T_constant(TC_operation) + | C_address , [] -> ok @@ T_constant(TC_address) + | C_key , [] -> ok @@ T_constant(TC_key) + | C_key_hash , [] -> ok @@ T_constant(TC_key_hash) + | C_chain_id , [] -> ok @@ T_constant(TC_chain_id) + | C_signature , [] -> ok @@ T_constant(TC_signature) + | C_timestamp , [] -> ok @@ T_constant(TC_timestamp) + | _ , [] -> + failwith "internal error: wrong number of arguments for type constant" + | _ , _ -> + failwith "internal error: unknown type operator" + diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index fdcaae910..b95c603fc 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -78,23 +78,37 @@ module Substitution = struct | T.T_constant (type_name) -> let%bind type_name = s_type_name_constant ~v ~expr type_name in ok @@ T.T_constant (type_name) - | T.T_variable _ -> failwith "TODO: T_variable" - | T.T_operator _ -> failwith "TODO: T_operator" + | T.T_variable variable -> + if Var.equal variable v + then ok @@ expr + else ok @@ T.T_variable variable + | T.T_operator (type_name_and_args) -> + let bind_map_type_operator = Stage_common.Misc.bind_map_type_operator in (* TODO: write T.Misc.bind_map_type_operator, but it doesn't work *) + let%bind type_name_and_args = bind_map_type_operator (s_type_value ~v ~expr) type_name_and_args in + ok @@ T.T_operator type_name_and_args | T.T_arrow _ -> let _TODO = (v, expr) in failwith "TODO: T_function" - and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun {type_expression'} -> + and s_type_expression' ~v ~expr : _ Ast_simplified.type_expression' w = fun type_expression' -> match type_expression' with - | Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_operator _ -> failwith "TODO: subst: unimplemented case s_type_expression" - | Ast_simplified.T_constant _ -> - let _TODO = (v, expr) in - failwith "TODO: subst: unimplemented case s_type_expression" + | Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression tuple" + | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum" + | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record" + | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow" + | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable" + | Ast_simplified.T_operator op -> + let%bind op = + Stage_common.Misc.bind_map_type_operator (* TODO: write Ast_simplified.Misc.type_operator_name *) + (s_type_expression ~v ~expr) + op in + ok @@ Ast_simplified.T_operator op + | Ast_simplified.T_constant constant -> + ok @@ Ast_simplified.T_constant constant + + and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun {type_expression'} -> + let%bind type_expression' = s_type_expression' ~v ~expr type_expression' in + ok @@ Ast_simplified.{type_expression'} and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } -> let%bind type_value' = s_type_value' ~v ~expr type_value' in From 57aeb4e9316ca0dcd9d1316a2db71d80dbf612db Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Mon, 20 Jan 2020 19:15:09 +0100 Subject: [PATCH 2/4] detect self_address when not at top level --- src/main/compile/of_mini_c.ml | 1 + .../self_ast_simplified.ml | 8 ------ src/passes/7-self_mini_c/helpers.ml | 8 ++++++ .../7-self_mini_c/michelson_restrictions.ml | 26 +++++++++++++++++++ src/passes/7-self_mini_c/self_mini_c.ml | 5 ++++ vendors/ligo-utils/simple-utils/trace.ml | 8 ++++++ 6 files changed, 48 insertions(+), 8 deletions(-) create mode 100644 src/passes/7-self_mini_c/michelson_restrictions.ml diff --git a/src/main/compile/of_mini_c.ml b/src/main/compile/of_mini_c.ml index 3b48d3921..4d99be97a 100644 --- a/src/main/compile/of_mini_c.ml +++ b/src/main/compile/of_mini_c.ml @@ -3,6 +3,7 @@ open Proto_alpha_utils open Trace let compile_contract : expression -> Compiler.compiled_expression result = fun e -> + let%bind e = Self_mini_c.contract_check e in let%bind (input_ty , _) = get_t_function e.type_value in let%bind body = get_function e in let%bind body = Compiler.Program.translate_function_body body [] input_ty in diff --git a/src/passes/3-self_ast_simplified/self_ast_simplified.ml b/src/passes/3-self_ast_simplified/self_ast_simplified.ml index a1ce4b580..f0ecd5183 100644 --- a/src/passes/3-self_ast_simplified/self_ast_simplified.ml +++ b/src/passes/3-self_ast_simplified/self_ast_simplified.ml @@ -6,14 +6,6 @@ let all = [ Literals.peephole_expression ; ] -let rec bind_chain : ('a -> 'a result) list -> 'a -> 'a result = fun fs x -> - match fs with - | [] -> ok x - | hd :: tl -> ( - let aux : 'a -> 'a result = fun x -> bind (bind_chain tl) (hd x) in - bind aux (ok x) - ) - let all_program = let all_p = List.map Helpers.map_program all in bind_chain all_p diff --git a/src/passes/7-self_mini_c/helpers.ml b/src/passes/7-self_mini_c/helpers.ml index ea7756a35..f5638cbe5 100644 --- a/src/passes/7-self_mini_c/helpers.ml +++ b/src/passes/7-self_mini_c/helpers.ml @@ -163,3 +163,11 @@ let rec map_expression : mapper -> expression -> expression result = fun f e -> let%bind updates = bind_map_list (fun (p,e) -> let%bind e = self e in ok(p,e)) updates in return @@ E_update(r,updates) ) + +let map_sub_level_expression : mapper -> expression -> expression result = fun f e -> + match e.content with + | E_closure {binder ; body} -> + let%bind body = map_expression f body in + let content = E_closure {binder; body} in + ok @@ { e with content } + | _ -> ok e \ No newline at end of file diff --git a/src/passes/7-self_mini_c/michelson_restrictions.ml b/src/passes/7-self_mini_c/michelson_restrictions.ml new file mode 100644 index 000000000..7f9e14169 --- /dev/null +++ b/src/passes/7-self_mini_c/michelson_restrictions.ml @@ -0,0 +1,26 @@ +open Mini_c +open Trace + +module Errors = struct + + let bad_self_address cst () = + let title = thunk @@ + Format.asprintf "Wrong %alocation" Mini_c.PP.expression' cst in + let message = thunk @@ + Format.asprintf "%ais only allowed at top-level" Mini_c.PP.expression' cst in + error title message () + +end +open Errors + +let self_in_lambdas : expression -> expression result = + fun e -> + match e.content with + | E_closure {binder=_ ; body} -> + let%bind _self_in_lambdas = Helpers.map_expression + (fun e -> match e.content with + | E_constant (C_SELF_ADDRESS, _) as c -> fail (bad_self_address c) + | _ -> ok e) + body in + ok e + | _ -> ok e diff --git a/src/passes/7-self_mini_c/self_mini_c.ml b/src/passes/7-self_mini_c/self_mini_c.ml index 329dad692..da2c66fa6 100644 --- a/src/passes/7-self_mini_c/self_mini_c.ml +++ b/src/passes/7-self_mini_c/self_mini_c.ml @@ -250,6 +250,11 @@ let betas : bool ref -> expression -> expression = fun changed -> map_expression (beta changed) +let contract_check = + let all = [Michelson_restrictions.self_in_lambdas] in + let all_e = List.map Helpers.map_sub_level_expression all in + bind_chain all_e + let rec all_expression : expression -> expression = fun e -> let changed = ref false in diff --git a/vendors/ligo-utils/simple-utils/trace.ml b/vendors/ligo-utils/simple-utils/trace.ml index dc80894d4..969de430d 100644 --- a/vendors/ligo-utils/simple-utils/trace.ml +++ b/vendors/ligo-utils/simple-utils/trace.ml @@ -718,6 +718,14 @@ let bind_fold_map_pair f acc (a, b) = let bind_map_triple f (a, b, c) = bind_and3 (f a, f b, f c) +let rec bind_chain : ('a -> 'a result) list -> 'a -> 'a result = fun fs x -> + match fs with + | [] -> ok x + | hd :: tl -> ( + let aux : 'a -> 'a result = fun x -> bind (bind_chain tl) (hd x) in + bind aux (ok x) + ) + (** Wraps a call that might trigger an exception in a result. From f1977b12aaa4ee50ce14e8cb8cb0eb3c9c1ba04e Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Mon, 20 Jan 2020 19:40:45 +0100 Subject: [PATCH 3/4] self in lambda negative test --- src/bin/expect_tests/contract_tests.ml | 14 ++++++++++++++ src/test/contracts/negative/self_in_lambda.mligo | 5 +++++ 2 files changed, 19 insertions(+) create mode 100644 src/test/contracts/negative/self_in_lambda.mligo diff --git a/src/bin/expect_tests/contract_tests.ml b/src/bin/expect_tests/contract_tests.ml index cc22a7410..443102d80 100644 --- a/src/bin/expect_tests/contract_tests.ml +++ b/src/bin/expect_tests/contract_tests.ml @@ -2,6 +2,8 @@ open Cli_expect let contract basename = "../../test/contracts/" ^ basename +let bad_contract basename = + "../../test/contracts/negative/" ^ basename let%expect_test _ = run_ligo_good [ "measure-contract" ; contract "coase.ligo" ; "main" ] ; @@ -1024,3 +1026,15 @@ let%expect_test _ = [%expect {| failwith("This contract always fails") |}] +let%expect_test _ = + run_ligo_bad [ "compile-contract" ; bad_contract "self_in_lambda.mligo" ; "main" ] ; + [%expect {| + ligo: Wrong SELF_ADDRESS location: SELF_ADDRESS is only allowed at top-level + + If you're not sure how to fix this error, you can + do one of the following: + + * Visit our documentation: https://ligolang.org/docs/intro/what-and-why/ + * Ask a question on our Discord: https://discord.gg/9rhYaEt + * Open a gitlab issue: https://gitlab.com/ligolang/ligo/issues/new + * Check the changelog by running 'ligo changelog' |}] \ No newline at end of file diff --git a/src/test/contracts/negative/self_in_lambda.mligo b/src/test/contracts/negative/self_in_lambda.mligo new file mode 100644 index 000000000..493047199 --- /dev/null +++ b/src/test/contracts/negative/self_in_lambda.mligo @@ -0,0 +1,5 @@ +let foo (u: unit) : address = + Current.self_address + +let main (ps: unit * address): (operation list * address) = + ( ([] : operation list) , foo) \ No newline at end of file From a2c51ddbcf8bb924a5aa4ac39e27ae8eb45bbc33 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 21 Jan 2020 10:44:32 +0100 Subject: [PATCH 4/4] better description for bad_contract error message --- src/main/compile/of_michelson.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/main/compile/of_michelson.ml b/src/main/compile/of_michelson.ml index 0b070fb79..87cfbb5a7 100644 --- a/src/main/compile/of_michelson.ml +++ b/src/main/compile/of_michelson.ml @@ -5,10 +5,9 @@ open Trace module Errors = struct (* TODO: those errors should have been caught in the earlier stages on the ligo pipeline - Here, in case of contract not typechecking, we should write a warning with a "please report" - on stderr and print the ill-typed michelson code; + build_contract is a kind of security net *) - let title_type_check_msg () = "Invalid contract (This might be a compiler bug, please report) " + let title_type_check_msg () = "generated Michelson contract failed to typecheck" let bad_parameter c () = let message () = let code = Format.asprintf "%a" Michelson.pp c in @@ -22,7 +21,7 @@ module Errors = struct let bad_contract c () = let message () = let code = Format.asprintf "%a" Michelson.pp c in - "bad contract type (contract entry point is expected to be of the form \"parameter * storage -> list(operation) * storage\"):\n"^code in + "bad contract type\n"^code in error title_type_check_msg message let unknown () = let message () =