diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index a6622e944..906766540 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -138,25 +138,25 @@ module Errors = struct ] in error ~data title message () - let needs_annotation (e : I.expression) (case : string) () = - let title = (thunk "this expression must be annotated with its type") in - let message () = Format.asprintf "%s needs an annotation" case in - let data = [ - ("expression" , fun () -> Format.asprintf "%a" I.PP.expression e) ; - ("location" , fun () -> Format.asprintf "%a" Location.pp e.location) - ] in - error ~data title message () + (* let needs_annotation (e : I.expression) (case : string) () = + * let title = (thunk "this expression must be annotated with its type") in + * let message () = Format.asprintf "%s needs an annotation" case in + * let data = [ + * ("expression" , fun () -> Format.asprintf "%a" I.PP.expression e) ; + * ("location" , fun () -> Format.asprintf "%a" Location.pp e.location) + * ] in + * error ~data title message () *) - let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () = - let title = (thunk "type error") in - let message () = msg in - let data = [ - ("expected" , fun () -> Format.asprintf "%s" expected); - ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual); - ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ; - ("location" , fun () -> Format.asprintf "%a" Location.pp loc) - ] in - error ~data title message () + (* let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () = + * let title = (thunk "type error") in + * let message () = msg in + * let data = [ + * ("expected" , fun () -> Format.asprintf "%s" expected); + * ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual); + * ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ; + * ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + * ] in + * error ~data title message () *) let type_error ?(msg="") ~(expected: O.type_value) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () = let title = (thunk "type error") in @@ -945,7 +945,7 @@ let type_program (p : I.program) : (O.program * Solver.state) result = ok (program, state) (* - Similar to type_program but use a fold_map_list and List.fold_left and add element to the left or the list which gives a better complexity +TODO: Similar to type_program but use a fold_map_list and List.fold_left and add element to the left or the list which gives a better complexity *) let type_program' : I.program -> O.program result = fun p -> let initial_state = Solver.initial_state in diff --git a/src/passes/4-typer/typer.mli b/src/passes/4-typer/typer.mli index cd7c00012..e60ce51bb 100644 --- a/src/passes/4-typer/typer.mli +++ b/src/passes/4-typer/typer.mli @@ -6,6 +6,8 @@ module O = Ast_typed module SMap = O.SMap module Environment = O.Environment +module Solver = Solver + type environment = Environment.t module Errors : sig @@ -37,16 +39,18 @@ module Errors : sig *) end -val type_program : I.program -> O.program result -val type_declaration : environment -> I.declaration -> (environment * O.declaration option) result -val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result +val type_program : I.program -> (O.program * Solver.state) result +val type_program' : I.program -> (O.program) result (* TODO: merge with type_program *) +val type_declaration : environment -> Solver.state -> I.declaration -> (environment * Solver.state * O.declaration option) result +(* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *) val evaluate_type : environment -> I.type_expression -> O.type_value result -val type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.annotated_expression result +val type_expression : environment -> Solver.state -> I.expression -> (O.annotated_expression * Solver.state) result val type_constant : string -> O.type_value list -> O.type_value option -> Location.t -> (string * O.type_value) result (* val untype_type_value : O.type_value -> (I.type_expression) result val untype_literal : O.literal -> I.literal result *) +val untype_type_expression : O.type_value -> I.type_expression result val untype_expression : O.annotated_expression -> I.expression result (* val untype_matching : ('o -> 'i result) -> 'o O.matching -> ('i I.matching) result diff --git a/src/passes/operators/operators.mli b/src/passes/operators/operators.mli index 2224cc74e..10e61a48b 100644 --- a/src/passes/operators/operators.mli +++ b/src/passes/operators/operators.mli @@ -22,6 +22,79 @@ module Typer : sig open Helpers.Typer open Ast_typed + module Operators_types : sig + (* TODO: we need a map from type names to type values. Then, all + these bindings don't need to be exported anymore. *) + val tc_subarg : + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> Typesystem.Core.type_constraint + val tc_sizearg : + Typesystem.Core.type_value -> Typesystem.Core.type_constraint + val tc_packable : + Typesystem.Core.type_value -> Typesystem.Core.type_constraint + val tc_timargs : + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> Typesystem.Core.type_constraint + val tc_divargs : + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> Typesystem.Core.type_constraint + val tc_modargs : + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> Typesystem.Core.type_constraint + val tc_addargs : + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> + Typesystem.Core.type_value -> Typesystem.Core.type_constraint + val t_none : Typesystem.Core.type_value + val t_sub : Typesystem.Core.type_value + val t_some : Typesystem.Core.type_value + val t_map_remove : Typesystem.Core.type_value + val t_map_add : Typesystem.Core.type_value + val t_map_update : Typesystem.Core.type_value + val t_map_mem : Typesystem.Core.type_value + val t_map_find : Typesystem.Core.type_value + val t_map_find_opt : Typesystem.Core.type_value + val t_map_fold : Typesystem.Core.type_value + val t_map_map : Typesystem.Core.type_value + val t_map_map_fold : Typesystem.Core.type_value + val t_map_iter : Typesystem.Core.type_value + val t_size : Typesystem.Core.type_value + val t_slice : Typesystem.Core.type_value + val t_failwith : Typesystem.Core.type_value + val t_get_force : Typesystem.Core.type_value + val t_int : Typesystem.Core.type_value + val t_bytes_pack : Typesystem.Core.type_value + val t_bytes_unpack : Typesystem.Core.type_value + val t_hash256 : Typesystem.Core.type_value + val t_hash512 : Typesystem.Core.type_value + val t_blake2b : Typesystem.Core.type_value + val t_hash_key : Typesystem.Core.type_value + val t_check_signature : Typesystem.Core.type_value + val t_sender : Typesystem.Core.type_value + val t_source : Typesystem.Core.type_value + val t_unit : Typesystem.Core.type_value + val t_amount : Typesystem.Core.type_value + val t_address : Typesystem.Core.type_value + val t_now : Typesystem.Core.type_value + val t_transaction : Typesystem.Core.type_value + val t_get_contract : Typesystem.Core.type_value + val t_abs : Typesystem.Core.type_value + val t_cons : Typesystem.Core.type_value + val t_assertion : Typesystem.Core.type_value + val t_times : Typesystem.Core.type_value + val t_div : Typesystem.Core.type_value + val t_mod : Typesystem.Core.type_value + val t_add : Typesystem.Core.type_value + val t_set_mem : Typesystem.Core.type_value + val t_set_add : Typesystem.Core.type_value + val t_set_remove : Typesystem.Core.type_value + val t_not : Typesystem.Core.type_value + end + (* val none : typer val set_empty : typer diff --git a/src/stages/ast_typed/combinators.mli b/src/stages/ast_typed/combinators.mli index 082293b76..12b922013 100644 --- a/src/stages/ast_typed/combinators.mli +++ b/src/stages/ast_typed/combinators.mli @@ -17,13 +17,14 @@ val t_set : type_value -> ?s:S.type_expression -> unit -> type_value val t_contract : type_value -> ?s:S.type_expression -> unit -> type_value val t_int : ?s:S.type_expression -> unit -> type_value val t_nat : ?s:S.type_expression -> unit -> type_value -val t_tez : ?s:S.type_expression -> unit -> type_value +val t_mutez : ?s:S.type_expression -> unit -> type_value val t_address : ?s:S.type_expression -> unit -> type_value val t_unit : ?s:S.type_expression -> unit -> type_value val t_option : type_value -> ?s:S.type_expression -> unit -> type_value val t_pair : type_value -> type_value -> ?s:S.type_expression -> unit -> type_value val t_list : type_value -> ?s:S.type_expression -> unit -> type_value val t_tuple : type_value list -> ?s:S.type_expression -> unit -> type_value +val t_variable : name -> ?s:S.type_expression -> unit -> type_value val t_record : tv_map -> ?s:S.type_expression -> unit -> type_value val make_t_ez_record : (string * type_value) list -> type_value (* @@ -47,7 +48,7 @@ val get_t_bool : type_value -> unit result val get_t_int : type_value -> unit result val get_t_nat : type_value -> unit result val get_t_unit : type_value -> unit result -val get_t_tez : type_value -> unit result +val get_t_mutez : type_value -> unit result val get_t_bytes : type_value -> unit result val get_t_string : type_value -> unit result *) @@ -77,7 +78,7 @@ val assert_t_map : type_value -> unit result val is_t_map : type_value -> bool val is_t_big_map : type_value -> bool -val assert_t_tez : type_value -> unit result +val assert_t_mutez : type_value -> unit result val assert_t_key : type_value -> unit result val assert_t_signature : type_value -> unit result val assert_t_key_hash : type_value -> unit result @@ -104,26 +105,27 @@ val assert_t_unit : type_value -> unit result val e_record : ae_map -> expression val ez_e_record : ( string * annotated_expression ) list -> expression +*) val e_some : value -> expression val e_none : expression val e_map : ( value * value ) list -> expression val e_unit : expression val e_int : int -> expression val e_nat : int -> expression -val e_tez : int -> expression +val e_mutez : int -> expression val e_bool : bool -> expression val e_string : string -> expression -*) +val e_bytes : bytes -> expression +val e_timestamp : int -> expression val e_address : string -> expression val e_operation : Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation -> expression -(* val e_lambda : lambda -> expression val e_pair : value -> value -> expression val e_application : value -> value -> expression val e_variable : name -> expression val e_list : value list -> expression val e_let_in : string -> value -> value -> expression -*) +val e_tuple : value list -> expression val e_a_unit : full_environment -> annotated_expression val e_a_int : int -> full_environment -> annotated_expression