From e4e77da97cf93e002b3af2445c70aeb0bb42f38e Mon Sep 17 00:00:00 2001 From: Pierre-Emmanuel Wulfman Date: Sat, 28 Sep 2019 01:56:09 +0200 Subject: [PATCH] add change for typer.ml --- src/passes/4-typer/typer.ml | 914 +++++++++++++++++++++--------------- 1 file changed, 526 insertions(+), 388 deletions(-) diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index efa65ae1b..080d3bacb 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -36,33 +36,33 @@ module Errors = struct let match_empty_variant : type a . a I.matching -> Location.t -> unit -> _ = fun matching loc () -> - let title = (thunk "match with no cases") in - let message () = "" in - let data = [ - ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ; - ("location" , fun () -> Format.asprintf "%a" Location.pp loc) - ] in - error ~data title message () + let title = (thunk "match with no cases") in + let message () = "" in + let data = [ + ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () let match_missing_case : type a . a I.matching -> Location.t -> unit -> _ = fun matching loc () -> - let title = (thunk "missing case in match") in - let message () = "" in - let data = [ - ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ; - ("location" , fun () -> Format.asprintf "%a" Location.pp loc) - ] in - error ~data title message () + let title = (thunk "missing case in match") in + let message () = "" in + let data = [ + ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () let match_redundant_case : type a . a I.matching -> Location.t -> unit -> _ = fun matching loc () -> - let title = (thunk "missing case in match") in - let message () = "" in - let data = [ - ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ; - ("location" , fun () -> Format.asprintf "%a" Location.pp loc) - ] in - error ~data title message () + let title = (thunk "missing case in match") in + let message () = "" in + let data = [ + ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () let unbound_constructor (e:environment) (n:string) (loc:Location.t) () = let title = (thunk "unbound constructor") in @@ -129,14 +129,14 @@ module Errors = struct let match_error : type a . ?msg:string -> expected: a I.matching -> actual: O.type_value -> Location.t -> unit -> _ = fun ?(msg = "") ~expected ~actual loc () -> - let title = (thunk "typing match") in - let message () = msg in - let data = [ - ("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected); - ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual) ; - ("location" , fun () -> Format.asprintf "%a" Location.pp loc) - ] in - error ~data title message () + let title = (thunk "typing match") in + let message () = msg in + let data = [ + ("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected); + ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] 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 @@ -192,7 +192,7 @@ module Errors = struct error ~data title message () let not_supported_yet (message : string) (ae : I.expression) () = - let title = (thunk "not suported yet") in + let title = (thunk "not supported yet") in let message () = message in let data = [ ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ; @@ -201,7 +201,7 @@ module Errors = struct error ~data title message () let not_supported_yet_untranspile (message : string) (ae : O.expression) () = - let title = (thunk "not suported yet") in + let title = (thunk "not supported yet") in let message () = message in let data = [ ("expression" , fun () -> Format.asprintf "%a" O.PP.expression ae) @@ -221,6 +221,7 @@ end open Errors +let swap (a,b) = ok (b,a) let rec type_program (p:I.program) : O.program result = let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = let%bind ed' = (bind_map_location (type_declaration e)) d in @@ -235,53 +236,56 @@ let rec type_program (p:I.program) : O.program result = bind_fold_list aux (Environment.full_empty, []) p in ok @@ List.rev lst -and type_declaration env : I.declaration -> (environment * O.declaration option) result = function +(* + Extract pairs of (name,type) in the declaration and add it to the environment +*) +let rec type_declaration env state : I.declaration -> (environment * Solver.state * O.declaration option) result = function | Declaration_type (type_name , type_expression) -> - let%bind tv = evaluate_type env type_expression in - let env' = Environment.add_type type_name tv env in - ok (env', None) + let%bind tv = evaluate_type env type_expression in + let env' = Environment.add_type type_name tv env in + ok (env', state , None) | Declaration_constant (name , tv_opt , expression) -> ( (* Determine the type of the expression and add it to the environment *) let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in - let%bind ae' = + let%bind (ae' , state') = trace (constant_declaration_error name expression tv'_opt) @@ - type_expression ?tv_opt:tv'_opt env expression in + type_expression env state expression in let env' = Environment.add_ez_ae name ae' env in - ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env')))) + ok (env', state' , Some (O.Declaration_constant ((make_n_e name ae') , (env , env')))) ) -and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> I.expression -> Location.t -> o O.matching result = - fun f e t i ae loc -> match i with +and type_match : environment -> Solver.state -> O.type_expression -> 'i I.matching -> I.expression -> Location.t -> (O.value O.matching * Solver.state) result = + fun e state t i ae loc -> match i with | Match_bool {match_true ; match_false} -> let%bind _ = trace_strong (match_error ~expected:i ~actual:t loc) @@ get_t_bool t in - let%bind match_true = f e match_true in - let%bind match_false = f e match_false in - ok (O.Match_bool {match_true ; match_false}) - | Match_option {match_none ; match_some} -> + let%bind (match_true , state') = type_expression e state match_true in + let%bind (match_false , state'') = type_expression e state' match_false in + ok (O.Match_bool {match_true ; match_false} , state'') + | Match_option {match_none ; match_some} -> let%bind t_opt = trace_strong (match_error ~expected:i ~actual:t loc) @@ get_t_option t in - let%bind match_none = f e match_none in + let%bind (match_none , state') = type_expression e state match_none in let (n, b) = match_some in let n' = n, t_opt in let e' = Environment.add_ez_binder n t_opt e in - let%bind b' = f e' b in - ok (O.Match_option {match_none ; match_some = (n', b')}) - | Match_list {match_nil ; match_cons} -> + let%bind (b' , state'') = type_expression e' state' b in + ok (O.Match_option {match_none ; match_some = (n', b')} , state'') + | Match_list {match_nil ; match_cons} -> let%bind t_list = trace_strong (match_error ~expected:i ~actual:t loc) @@ get_t_list t in - let%bind match_nil = f e match_nil in + let%bind (match_nil , state') = type_expression e state match_nil in let (hd, tl, b) = match_cons in let e' = Environment.add_ez_binder hd t_list e in let e' = Environment.add_ez_binder tl t e' in - let%bind b' = f e' b in - ok (O.Match_list {match_nil ; match_cons = (((hd , t_list), (tl , t)), b')}) - | Match_tuple (lst, b) -> + let%bind (b' , state'') = type_expression e' state' b in + ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')} , state'') + | Match_tuple (lst, b) -> let%bind t_tuple = trace_strong (match_error ~expected:i ~actual:t loc) @@ get_t_tuple t in @@ -290,9 +294,9 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t @@ (fun () -> List.combine lst t_tuple) in let aux prev (name, tv) = Environment.add_ez_binder name tv prev in let e' = List.fold_left aux e lst' in - let%bind b' = f e' b in - ok (O.Match_tuple (lst, b')) - | Match_variant lst -> + let%bind (b' , state') = type_expression e' state b in + ok (O.Match_tuple (lst, b') , state') + | Match_variant lst -> let%bind variant_opt = let aux acc ((constructor_name , _) , _) = let%bind (_ , variant) = @@ -334,17 +338,17 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t Assert.assert_true List.(length variant_cases = length match_cases) in ok () in - let%bind lst' = - let aux ((constructor_name , name) , b) = + let%bind (state'' , lst') = + let aux state ((constructor_name , name) , b) = let%bind (constructor , _) = trace_option (unbound_constructor e constructor_name loc) @@ Environment.get_constructor constructor_name e in let e' = Environment.add_ez_binder name constructor e in - let%bind b' = f e' b in - ok ((constructor_name , name) , b') + let%bind (b' , state') = type_expression e' state b in + ok (state' , ((constructor_name , name) , b')) in - bind_map_list aux lst in - ok (O.Match_variant (lst' , variant)) + bind_fold_map_list aux state lst in + ok (O.Match_variant (lst' , variant) , state'') (* Recursively search the type_expression and return a result containing the @@ -354,242 +358,261 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = let return tv' = ok (make_t tv' (Some t)) in match t with | T_function (a, b) -> - let%bind a' = evaluate_type e a in - let%bind b' = evaluate_type e b in - return (T_function (a', b')) + let%bind a' = evaluate_type e a in + let%bind b' = evaluate_type e b in + return (T_function (a', b')) | T_tuple lst -> - let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in - return (T_tuple lst') + let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in + return (T_tuple lst') | T_sum m -> - let aux k v prev = - let%bind prev' = prev in - let%bind v' = evaluate_type e v in - ok @@ SMap.add k v' prev' - in - let%bind m = SMap.fold aux m (ok SMap.empty) in - return (T_sum m) + let aux k v prev = + let%bind prev' = prev in + let%bind v' = evaluate_type e v in + ok @@ SMap.add k v' prev' + in + let%bind m = SMap.fold aux m (ok SMap.empty) in + return (T_sum m) | T_record m -> - let aux k v prev = - let%bind prev' = prev in - let%bind v' = evaluate_type e v in - ok @@ SMap.add k v' prev' - in - let%bind m = SMap.fold aux m (ok SMap.empty) in - return (T_record m) + let aux k v prev = + let%bind prev' = prev in + let%bind v' = evaluate_type e v in + ok @@ SMap.add k v' prev' + in + let%bind m = SMap.fold aux m (ok SMap.empty) in + return (T_record m) | T_variable name -> - let%bind tv = - trace_option (unbound_type_variable e name) - @@ Environment.get_type_opt name e in - ok tv + let%bind tv = + trace_option (unbound_type_variable e name) + @@ Environment.get_type_opt name e in + ok tv | T_constant (cst, lst) -> - let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in - return (T_constant(cst, lst')) + let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in + return (T_constant(cst, lst')) -and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.annotated_expression result = fun e ?tv_opt ae -> +and type_expression : environment -> Solver.state -> I.expression -> (O.annotated_expression * Solver.state) result = fun e state ae -> + let open Solver in let module L = Logger.Stateful() in - let return expr tv = - let%bind () = - match tv_opt with - | None -> ok () - | Some tv' -> O.assert_type_value_eq (tv' , tv) in + let return : _ -> Solver.state -> _ -> _ (* return of type_expression *) = fun expr state constraints type_name -> + let%bind new_state = aggregate_constraints state constraints in + let tv = t_variable type_name () in let location = ae.location in - ok @@ make_a_e ~location expr tv e in + let expr' = make_a_e ~location expr tv e in + ok @@ (expr' , new_state) in + let return_wrapped expr state (constraints , expr_type) = return expr state constraints expr_type in let main_error = let title () = "typing expression" in let content () = "" in let data = [ ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ; - ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp @@ ae.location) ; ("misc" , fun () -> L.get ()) ; ] in error ~data title content in trace main_error @@ - match ae.expression with + match ae.expression' with + + (* TODO: this file should take care only of the order in which program fragments + are translated by Wrap.xyz + + TODO: produce an ordered list of sub-fragments, and use a common piece of code + to actually perform the recursive calls *) + (* Basic *) + | E_failwith expr -> ( + let%bind (expr', state') = type_expression e state expr in + let (constraints , expr_type) = Wrap.failwith () in + let expr'' = e_failwith expr' in + return expr'' state' constraints expr_type + ) | E_variable name -> - let%bind tv' = - trace_option (unbound_variable e name ae.location) - @@ Environment.get_opt name e in - return (E_variable name) tv'.type_value + let%bind tv' = + trace_option (unbound_variable e name ae.location) + @@ Environment.get_opt name e in + let (constraints , expr_type) = Wrap.variable name tv'.type_expression in + let expr' = e_variable name in + return (E_variable name) tv'.type_value | E_literal (Literal_bool b) -> - return (E_literal (Literal_bool b)) (t_bool ()) + return (E_literal (Literal_bool b)) (t_bool ()) | E_literal Literal_unit | E_skip -> - return (E_literal (Literal_unit)) (t_unit ()) + return (E_literal (Literal_unit)) (t_unit ()) | E_literal (Literal_string s) -> - return (E_literal (Literal_string s)) (t_string ()) + return (E_literal (Literal_string s)) (t_string ()) | E_literal (Literal_bytes s) -> - return (E_literal (Literal_bytes s)) (t_bytes ()) + return (E_literal (Literal_bytes s)) (t_bytes ()) | E_literal (Literal_int n) -> - return (E_literal (Literal_int n)) (t_int ()) + return (E_literal (Literal_int n)) (t_int ()) | E_literal (Literal_nat n) -> - return (E_literal (Literal_nat n)) (t_nat ()) + return (E_literal (Literal_nat n)) (t_nat ()) | E_literal (Literal_timestamp n) -> - return (E_literal (Literal_timestamp n)) (t_timestamp ()) + return (E_literal (Literal_timestamp n)) (t_timestamp ()) | E_literal (Literal_mutez n) -> - return (E_literal (Literal_mutez n)) (t_tez ()) + return (E_literal (Literal_mutez n)) (t_tez ()) | E_literal (Literal_address s) -> - return (e_address s) (t_address ()) + return (e_address s) (t_address ()) | E_literal (Literal_operation op) -> - return (e_operation op) (t_operation ()) + return (e_operation op) (t_operation ()) (* Tuple *) | E_tuple lst -> - let%bind lst' = bind_list @@ List.map (type_expression e) lst in - let tv_lst = List.map get_type_annotation lst' in - return (E_tuple lst') (t_tuple tv_lst ()) + let aux state hd = type_expression e state hd >>? swap in + let%bind (state', lst') = bind_fold_map_list aux state lst in + let tv_lst = List.map get_type_annotation lst' in + return (E_tuple lst') (t_tuple tv_lst ()) | E_accessor (ae', path) -> - let%bind e' = type_expression e ae' in - let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result = - match a with - | Access_tuple index -> ( - let%bind tpl_tv = get_t_tuple prev.type_annotation in - let%bind tv = - generic_try (bad_tuple_index index ae' prev.type_annotation ae.location) - @@ (fun () -> List.nth tpl_tv index) in - return (E_tuple_accessor (prev , index)) tv - ) - | Access_record property -> ( - let%bind r_tv = get_t_record prev.type_annotation in - let%bind tv = - generic_try (bad_record_access property ae' prev.type_annotation ae.location) - @@ (fun () -> SMap.find property r_tv) in - return (E_record_accessor (prev , property)) tv - ) - | Access_map ae' -> ( - let%bind ae'' = type_expression e ae' in - let%bind (k , v) = bind_map_or (get_t_map , get_t_big_map) prev.type_annotation in - let%bind () = - Ast_typed.assert_type_value_eq (k , get_type_annotation ae'') in - return (E_look_up (prev , ae'')) v - ) - in - trace (simple_info "accessing") @@ - bind_fold_list aux e' path + let%bind e' = type_expression e ae' in + let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result = + match a with + | Access_tuple index -> ( + let%bind tpl_tv = get_t_tuple prev.type_annotation in + let%bind tv = + generic_try (bad_tuple_index index ae' prev.type_annotation ae.location) + @@ (fun () -> List.nth tpl_tv index) in + return (E_tuple_accessor (prev , index)) tv + ) + | Access_record property -> ( + let%bind r_tv = get_t_record prev.type_annotation in + let%bind tv = + generic_try (bad_record_access property ae' prev.type_annotation ae.location) + @@ (fun () -> SMap.find property r_tv) in + return (E_record_accessor (prev , property)) tv + ) + | Access_map ae' -> ( + let%bind ae'' = type_expression e ae' in + let%bind (k , v) = bind_map_or (get_t_map , get_t_big_map) prev.type_annotation in + let%bind () = + Ast_typed.assert_type_value_eq (k , get_type_annotation ae'') in + return (E_look_up (prev , ae'')) v + ) + in + trace (simple_info "accessing") @@ + bind_fold_list aux e' path (* Sum *) | E_constructor (c, expr) -> - let%bind (c_tv, sum_tv) = - let error = - let title () = "no such constructor" in - let content () = - Format.asprintf "%s in:\n%a\n" - c O.Environment.PP.full_environment e - in - error title content in - trace_option error @@ - Environment.get_constructor c e in - let%bind expr' = type_expression e expr in - let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in - return (E_constructor (c , expr')) sum_tv + let%bind (c_tv, sum_tv) = + let error = + let title () = "no such constructor" in + let content () = + Format.asprintf "%s in:\n%a\n" + c O.Environment.PP.full_environment e + in + error title content in + trace_option error @@ + Environment.get_constructor c e in + let%bind (expr' , state') = type_expression e state expr in + let%bind _assert = O.assert_type_expression_eq (expr'.type_annotation, c_tv) in + let wrapped = Wrap.constructor expr'.type_annotation c_tv sum_tv in + return_wrapped (E_constructor (c , expr')) state' wrapped (* Record *) | E_record m -> - let aux prev k expr = - let%bind expr' = type_expression e expr in - ok (SMap.add k expr' prev) - in - let%bind m' = bind_fold_smap aux (ok SMap.empty) m in - return (E_record m') (t_record (SMap.map get_type_annotation m') ()) + let aux (acc, state) k expr = + let%bind (expr' , state') = type_expression e state expr in + ok (SMap.add k expr' acc , state') + in + let%bind (m' , state') = bind_fold_smap aux (ok (SMap.empty , state)) m in + let wrapped = Wrap.record (SMap.map get_type_annotation m') in + return_wrapped (E_record m') state' wrapped (* Data-structure *) | E_list lst -> - let%bind lst' = bind_map_list (type_expression e) lst in - let%bind tv = - let aux opt c = - match opt with - | None -> ok (Some c) - | Some c' -> - let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in - ok (Some c') in - let%bind init = match tv_opt with - | None -> ok None - | Some ty -> - let%bind ty' = get_t_list ty in - ok (Some ty') in - let%bind ty = - let%bind opt = bind_fold_list aux init + let%bind lst' = bind_map_list (type_expression e) lst in + let%bind tv = + let aux opt c = + match opt with + | None -> ok (Some c) + | Some c' -> + let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in + ok (Some c') in + let%bind init = match tv_opt with + | None -> ok None + | Some ty -> + let%bind ty' = get_t_list ty in + ok (Some ty') in + let%bind ty = + let%bind opt = bind_fold_list aux init @@ List.map get_type_annotation lst' in - trace_option (needs_annotation ae "empty list") opt in - ok (t_list ty ()) - in - return (E_list lst') tv + trace_option (needs_annotation ae "empty list") opt in + ok (t_list ty ()) + in + return (E_list lst') tv | E_set lst -> - let%bind lst' = bind_map_list (type_expression e) lst in - let%bind tv = - let aux opt c = - match opt with - | None -> ok (Some c) - | Some c' -> - let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in - ok (Some c') in - let%bind init = match tv_opt with - | None -> ok None - | Some ty -> - let%bind ty' = get_t_set ty in - ok (Some ty') in - let%bind ty = - let%bind opt = bind_fold_list aux init + let%bind lst' = bind_map_list (type_expression e) lst in + let%bind tv = + let aux opt c = + match opt with + | None -> ok (Some c) + | Some c' -> + let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in + ok (Some c') in + let%bind init = match tv_opt with + | None -> ok None + | Some ty -> + let%bind ty' = get_t_set ty in + ok (Some ty') in + let%bind ty = + let%bind opt = bind_fold_list aux init @@ List.map get_type_annotation lst' in - trace_option (needs_annotation ae "empty set") opt in - ok (t_set ty ()) - in - return (E_set lst') tv + trace_option (needs_annotation ae "empty set") opt in + ok (t_set ty ()) + in + return (E_set lst') tv | E_map lst -> - let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in - let%bind tv = - let aux opt c = - match opt with - | None -> ok (Some c) - | Some c' -> - let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in - ok (Some c') in - let%bind key_type = - let%bind sub = - bind_fold_list aux None - @@ List.map get_type_annotation - @@ List.map fst lst' in - let%bind annot = bind_map_option get_t_map_key tv_opt in - trace (simple_info "empty map expression without a type annotation") @@ - O.merge_annotation annot sub (needs_annotation ae "this map literal") - in - let%bind value_type = - let%bind sub = - bind_fold_list aux None - @@ List.map get_type_annotation - @@ List.map snd lst' in - let%bind annot = bind_map_option get_t_map_value tv_opt in - trace (simple_info "empty map expression without a type annotation") @@ - O.merge_annotation annot sub (needs_annotation ae "this map literal") - in - ok (t_map key_type value_type ()) + let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in + let%bind tv = + let aux opt c = + match opt with + | None -> ok (Some c) + | Some c' -> + let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in + ok (Some c') in + let%bind key_type = + let%bind sub = + bind_fold_list aux None + @@ List.map get_type_annotation + @@ List.map fst lst' in + let%bind annot = bind_map_option get_t_map_key tv_opt in + trace (simple_info "empty map expression without a type annotation") @@ + O.merge_annotation annot sub (needs_annotation ae "this map literal") in - return (E_map lst') tv + let%bind value_type = + let%bind sub = + bind_fold_list aux None + @@ List.map get_type_annotation + @@ List.map snd lst' in + let%bind annot = bind_map_option get_t_map_value tv_opt in + trace (simple_info "empty map expression without a type annotation") @@ + O.merge_annotation annot sub (needs_annotation ae "this map literal") + in + ok (t_map key_type value_type ()) + in + return (E_map lst') tv | E_big_map lst -> - let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in - let%bind tv = - let aux opt c = - match opt with - | None -> ok (Some c) - | Some c' -> - let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in - ok (Some c') in - let%bind key_type = - let%bind sub = - bind_fold_list aux None - @@ List.map get_type_annotation - @@ List.map fst lst' in - let%bind annot = bind_map_option get_t_big_map_key tv_opt in - trace (simple_info "empty map expression without a type annotation") @@ - O.merge_annotation annot sub (needs_annotation ae "this map literal") - in - let%bind value_type = - let%bind sub = - bind_fold_list aux None - @@ List.map get_type_annotation - @@ List.map snd lst' in - let%bind annot = bind_map_option get_t_big_map_value tv_opt in - trace (simple_info "empty map expression without a type annotation") @@ - O.merge_annotation annot sub (needs_annotation ae "this map literal") - in - ok (t_big_map key_type value_type ()) + let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in + let%bind tv = + let aux opt c = + match opt with + | None -> ok (Some c) + | Some c' -> + let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in + ok (Some c') in + let%bind key_type = + let%bind sub = + bind_fold_list aux None + @@ List.map get_type_annotation + @@ List.map fst lst' in + let%bind annot = bind_map_option get_t_big_map_key tv_opt in + trace (simple_info "empty map expression without a type annotation") @@ + O.merge_annotation annot sub (needs_annotation ae "this map literal") in - return (E_big_map lst') tv + let%bind value_type = + let%bind sub = + bind_fold_list aux None + @@ List.map get_type_annotation + @@ List.map snd lst' in + let%bind annot = bind_map_option get_t_big_map_value tv_opt in + trace (simple_info "empty map expression without a type annotation") @@ + O.merge_annotation annot sub (needs_annotation ae "this map literal") + in + ok (t_big_map key_type value_type ()) + in + return (E_big_map lst') tv | E_lambda { binder ; input_type ; @@ -626,31 +649,21 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ()) ) | E_constant (name, lst) -> - let%bind lst' = bind_list @@ List.map (type_expression e) lst in - let tv_lst = List.map get_type_annotation lst' in - let%bind (name', tv) = - type_constant name tv_lst tv_opt ae.location in - return (E_constant (name' , lst')) tv + let%bind lst' = bind_list @@ List.map (type_expression e) lst in + let tv_lst = List.map get_type_annotation lst' in + let%bind (name', tv) = + type_constant name tv_lst tv_opt ae.location in + return (E_constant (name' , lst')) tv | E_application (f, arg) -> - let%bind f' = type_expression e f in - let%bind arg = type_expression e arg in - let%bind tv = match f'.type_annotation.type_value' with - | T_function (param, result) -> - let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in - ok result - | _ -> - fail @@ type_error_approximate - ~expected:"should be a function type" - ~expression:f - ~actual:f'.type_annotation - f'.location - in - return (E_application (f' , arg)) tv + let%bind (f' , state') = type_expression e state f in + let%bind (arg , state'') = type_expression e state' arg in + let wrapped = Wrap.application f'.type_annotation arg.type_annotation in + return_wrapped (E_application (f' , arg)) state'' wrapped | E_look_up dsi -> - let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in - let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in - let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in - return (E_look_up (ds , ind)) (t_option dst ()) + let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in + let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in + let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in + return (E_look_up (ds , ind)) (t_option dst ()) (* Advanced *) | E_matching (ex, m) -> ( let%bind ex' = type_expression e ex in @@ -677,40 +690,24 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a return (O.E_matching (ex', m')) tv ) | E_sequence (a , b) -> - let%bind a' = type_expression e a in - let%bind b' = type_expression e b in - let a'_type_annot = get_type_annotation a' in - let%bind () = - trace_strong (type_error - ~msg:"first part of the sequence should be of unit type" - ~expected:(O.t_unit ()) - ~actual:a'_type_annot - ~expression:a - a'.location) @@ - Ast_typed.assert_type_value_eq (t_unit () , a'_type_annot) in - return (O.E_sequence (a' , b')) (get_type_annotation b') + let%bind (a' , state') = type_expression e state a in + let%bind (b' , state'') = type_expression e state' b in + let wrapped = Wrap.sequence a'.type_annotation b'.type_annotation in + return_wrapped (O.E_sequence (a' , b')) state'' wrapped | E_loop (expr , body) -> - let%bind expr' = type_expression e expr in - let%bind body' = type_expression e body in - let t_expr' = get_type_annotation expr' in - let%bind () = - trace_strong (type_error - ~msg:"while condition isn't of type bool" - ~expected:(O.t_bool ()) - ~actual:t_expr' - ~expression:expr - expr'.location) @@ - Ast_typed.assert_type_value_eq (t_bool () , t_expr') in - let t_body' = get_type_annotation body' in - let%bind () = - trace_strong (type_error - ~msg:"while body isn't of unit type" - ~expected:(O.t_unit ()) - ~actual:t_body' - ~expression:body - body'.location) @@ - Ast_typed.assert_type_value_eq (t_unit () , t_body') in - return (O.E_loop (expr' , body')) (t_unit ()) + let%bind (expr' , state') = type_expression e state expr in + let%bind (body' , state'') = type_expression e state' body in + let wrapped = Wrap.loop expr'.type_annotation body'.type_annotation in + return_wrapped (O.E_loop (expr' , body')) state'' wrapped + | E_let_in {binder ; rhs ; result} -> + let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in + (* TODO: the binder annotation should just be an annotation node *) + let%bind (rhs , state') = type_expression e state rhs in + let e' = Environment.add_ez_declaration (fst binder) rhs e in + let%bind (result , state'') = type_expression e' state' result in + let wrapped = + Wrap.let_in rhs.type_annotation rhs_tv_opt result.type_annotation in + return_wrapped (E_let_in {binder = fst binder; rhs; result}) state'' wrapped | E_assign (name , path , expr) -> let%bind typed_name = let%bind ele = Environment.get_trace name e in @@ -735,34 +732,103 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a | Access_map _ -> fail @@ not_supported_yet "assign expressions with maps are not supported yet" ae in - bind_fold_list aux (typed_name.type_value , []) path in - let%bind expr' = type_expression e expr in - let t_expr' = get_type_annotation expr' in - let%bind () = - trace_strong (type_error - ~msg:"type of the expression to assign doesn't match left-hand-side" - ~expected:assign_tv - ~actual:t_expr' - ~expression:expr - expr'.location) @@ - Ast_typed.assert_type_value_eq (assign_tv , t_expr') in - return (O.E_assign (typed_name , path' , expr')) (t_unit ()) - | E_let_in {binder ; rhs ; result} -> - let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in - let%bind rhs = type_expression ?tv_opt:rhs_tv_opt e rhs in - let e' = Environment.add_ez_declaration (fst binder) rhs e in - let%bind result = type_expression e' result in - return (E_let_in {binder = fst binder; rhs; result}) result.type_annotation + bind_fold_list aux (typed_name.type_expression , []) path in + let%bind (expr' , state') = type_expression e state expr in + let wrapped = Wrap.assign assign_tv expr'.type_annotation in + return_wrapped (O.E_assign (typed_name , path' , expr')) state' wrapped | E_annotation (expr , te) -> let%bind tv = evaluate_type e te in - let%bind expr' = type_expression ~tv_opt:tv e expr in - let%bind type_annotation = - O.merge_annotation - (Some tv) - (Some expr'.type_annotation) - (internal_assertion_failure "merge_annotations (Some ...) (Some ...) failed") in - ok {expr' with type_annotation} + let%bind (expr' , state') = type_expression e state expr in + let wrapped = Wrap.annotation expr'.type_annotation tv + (* TODO: we're probably discarding too much by using expr'.expression. + Previously: {expr' with type_annotation = the_explicit_type_annotation} + but then this case is not like the others and doesn't call return_wrapped, + which might do some necessary work *) + in return_wrapped expr'.expression state' wrapped + | E_matching (ex, m) -> ( + let%bind (ex' , state') = type_expression e state ex in + let%bind (m' , state'') = type_match e state' ex'.type_annotation m ae ae.location in + let tvs = + let aux (cur:O.value O.matching) = + match cur with + | Match_bool { match_true ; match_false } -> [ match_true ; match_false ] + | Match_list { match_nil ; match_cons = (_ , _ , match_cons) } -> [ match_nil ; match_cons ] + | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ] + | Match_tuple (_ , match_tuple) -> [ match_tuple ] + | Match_variant (lst , _) -> List.map snd lst in + List.map get_type_annotation @@ aux m' in + let%bind () = match tvs with + [] -> fail @@ match_empty_variant m ae.location + | _ -> ok () in + (* constraints: + all the items of tvs should be equal to the first one + result = first item of tvs + *) + let wrapped = Wrap.matching tvs in + return_wrapped (O.E_matching (ex', m')) state'' wrapped + ) + + (* match m with *) + (* Special case for assert-like failwiths. TODO: CLEAN THIS. *) + (* | I.Match_bool { match_false ; match_true } when I.is_e_failwith match_true -> ( *) + (* let%bind fw = I.get_e_failwith match_true in *) + (* let%bind fw' = type_expression e fw in *) + (* let%bind mf' = type_expression e match_false in *) + (* let t = get_type_annotation ex' in *) + (* let%bind () = *) + (* trace_strong (match_error ~expected:m ~actual:t ae.location) *) + (* @@ assert_t_bool t in *) + (* let%bind () = *) + (* trace_strong (match_error *) + (* ~msg:"matching not-unit on an assert" *) + (* ~expected:m *) + (* ~actual:t *) + (* ae.location) *) + (* @@ assert_t_unit (get_type_annotation mf') in *) + (* let mt' = make_a_e *) + (* (E_constant ("ASSERT_INFERRED" , [ex' ; fw'])) *) + (* (t_unit ()) *) + (* e *) + (* in *) + (* let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in *) + (* return (O.E_matching (ex' , m')) (t_unit ()) *) + (* ) *) + (* | _ -> ( … ) *) + + + | E_lambda { + binder ; + input_type ; + output_type ; + result ; + } -> ( + let%bind input_type' = bind_map_option (evaluate_type e) input_type in + let%bind output_type' = bind_map_option (evaluate_type e) output_type in + + let fresh : O.type_expression = t_variable (Wrap.fresh_binder ()) () in + let e' = Environment.add_ez_binder (fst binder) fresh e in + + let%bind (result , state') = type_expression e' state result in + let output_type = result.type_annotation in + let wrapped = Wrap.lambda fresh input_type' output_type' in + return_wrapped + (E_lambda {binder = fst binder;input_type=fresh;output_type;result}) + state' wrapped + ) + + | E_constant (name, lst) -> + let () = ignore (name , lst) in + Pervasives.failwith "TODO: E_constant" + (* + let%bind lst' = bind_list @@ List.map (type_expression e) lst in + let tv_lst = List.map get_type_annotation lst' in + let%bind (name', tv) = + type_constant name tv_lst tv_opt ae.location in + return (E_constant (name' , lst')) tv + *) + +(* Advanced *) and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) (loc : Location.t) : (string * O.type_value) result = (* Constant poorman's polymorphism *) @@ -777,7 +843,76 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result = match t.simplified with | Some s -> ok s | _ -> fail @@ internal_assertion_failure "trying to untype generated type" +(* let type_statement : environment -> I.declaration -> Solver.state -> (environment * O.declaration * Solver.state) result = fun env declaration state -> *) +(* match declaration with *) +(* | I.Declaration_type td -> ( *) +(* let%bind (env', state', declaration') = type_declaration env state td in *) +(* let%bind toto = Solver.aggregate_constraints state' constraints in *) +(* let declaration' = match declaration' with None -> Pervasives.failwith "TODO" | Some x -> x in *) +(* ok (env' , declaration' , toto) *) +(* ) *) +(* | I.Declaration_constant ((_ , _ , expr) as cd) -> ( *) +(* let%bind state' = type_expression expr in *) +(* let constraints = constant_declaration cd in *) +(* Solver.aggregate_constraints state' constraints *) +(* ) *) +(* TODO: we ended up with two versions of type_program… ??? *) + +(* +Apply type_declaration on all the node of the AST_simplified from the root p +*) +let type_program (p:I.program) : (environment * Solver.state * O.program) result = + let env = Ast_typed.Environment.full_empty in + let state = Solver.initial_state in + let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = + let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in + let ds' = match d'_opt with + | None -> ds + | Some d' -> ds @ [Location.wrap ~loc:(Location.get_location d) d'] (* take O(n) insted of O(1) *) + in + ok (e' , s' , ds') + in + let%bind (env' , state' , declarations) = + trace (fun () -> program_error p ()) @@ + bind_fold_list aux (env , state , []) p in + let () = ignore (env' , state') in + ok (env', state', declarations) + + (* + 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 + let initial_env = Environment.full_empty in + let aux (env, state) (statement : I.declaration Location.wrap) = + let statement' = statement.wrap_content in (* TODO *) + let%bind (env' , state' , declaration') = type_declaration env state statement' in + let declaration'' = match declaration' with + None -> None + | Some x -> Some (Location.wrap ~loc:Location.(statement.location) x) in + ok ((env' , state') , declaration'') + in + let%bind ((env' , state') , p') = bind_fold_map_list aux (initial_env, initial_state) p in + let p' = List.fold_left (fun l e -> match e with None -> l | Some x -> x :: l) [] p' in + + (* here, maybe ensure that there are no invalid things in env' and state' ? *) + let () = ignore (env' , state') in + ok p' + +(* + Tranform a Ast_typed type_expression into an ast_simplified type_expression +*) +let untype_type_expression (t:O.type_expression) : (I.type_expression) result = + ok t +(* match t.simplified with *) +(* | Some s -> ok s *) +(* | _ -> fail @@ internal_assertion_failure "trying to untype generated type" *) + + +(* + Tranform a Ast_typed literal into an ast_simplified literal +*) let untype_literal (l:O.literal) : I.literal result = let open I in match l with @@ -800,17 +935,17 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result = let return e = ok e in match e.expression with | E_literal l -> - let%bind l = untype_literal l in - return (e_literal l) + let%bind l = untype_literal l in + return (e_literal l) | E_constant (n, lst) -> - let%bind lst' = bind_map_list untype_expression lst in - return (e_constant n lst') + let%bind lst' = bind_map_list untype_expression lst in + return (e_constant n lst') | E_variable n -> - return (e_variable n) + return (e_variable n) | E_application (f, arg) -> - let%bind f' = untype_expression f in - let%bind arg' = untype_expression arg in - return (e_application f' arg') + let%bind f' = untype_expression f in + let%bind arg' = untype_expression arg in + return (e_application f' arg') | E_lambda {binder ; body} -> ( let%bind io = get_t_function e.type_annotation in let%bind (input_type , output_type) = bind_map_pair untype_type_value io in @@ -818,49 +953,52 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result = return (e_lambda binder (Some input_type) (Some output_type) result) ) | E_tuple lst -> - let%bind lst' = bind_list - @@ List.map untype_expression lst in - return (e_tuple lst') + let%bind lst' = bind_list + @@ List.map untype_expression lst in + return (e_tuple lst') | E_tuple_accessor (tpl, ind) -> - let%bind tpl' = untype_expression tpl in - return (e_accessor tpl' [Access_tuple ind]) + let%bind tpl' = untype_expression tpl in + return (e_accessor tpl' [Access_tuple ind]) | E_constructor (n, p) -> - let%bind p' = untype_expression p in - return (e_constructor n p') + let%bind p' = untype_expression p in + return (e_constructor n p') | E_record r -> - let%bind r' = bind_smap - @@ SMap.map untype_expression r in - return (e_record r') + let%bind r' = bind_smap + @@ SMap.map untype_expression r in + return (e_record r') | E_record_accessor (r, s) -> - let%bind r' = untype_expression r in - return (e_accessor r' [Access_record s]) + let%bind r' = untype_expression r in + return (e_accessor r' [Access_record s]) | E_map m -> - let%bind m' = bind_map_list (bind_map_pair untype_expression) m in - return (e_map m') + let%bind m' = bind_map_list (bind_map_pair untype_expression) m in + return (e_map m') | E_big_map m -> - let%bind m' = bind_map_list (bind_map_pair untype_expression) m in - return (e_big_map m') + let%bind m' = bind_map_list (bind_map_pair untype_expression) m in + return (e_big_map m') | E_list lst -> - let%bind lst' = bind_map_list untype_expression lst in - return (e_list lst') + let%bind lst' = bind_map_list untype_expression lst in + return (e_list lst') | E_set lst -> - let%bind lst' = bind_map_list untype_expression lst in - return (e_set lst') + let%bind lst' = bind_map_list untype_expression lst in + return (e_set lst') | E_look_up dsi -> - let%bind (a , b) = bind_map_pair untype_expression dsi in - return (e_look_up a b) + let%bind (a , b) = bind_map_pair untype_expression dsi in + return (e_look_up a b) | E_matching (ae, m) -> - let%bind ae' = untype_expression ae in - let%bind m' = untype_matching untype_expression m in - return (e_matching ae' m') + let%bind ae' = untype_expression ae in + let%bind m' = untype_matching untype_expression m in + return (e_matching ae' m') + | E_failwith ae -> + let%bind ae' = untype_expression ae in + return (e_failwith ae') | E_sequence _ | E_loop _ | E_assign _ -> fail @@ not_supported_yet_untranspile "not possible to untranspile statements yet" e.expression | E_let_in {binder;rhs;result} -> - let%bind tv = untype_type_value rhs.type_annotation in - let%bind rhs = untype_expression rhs in - let%bind result = untype_expression result in - return (e_let_in (binder , (Some tv)) rhs result) + let%bind tv = untype_type_value rhs.type_annotation in + let%bind rhs = untype_expression rhs in + let%bind result = untype_expression result in + return (e_let_in (binder , (Some tv)) rhs result) (* Tranform a Ast_typed matching into an ast_simplified matching @@ -869,25 +1007,25 @@ and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matchin let open I in match m with | Match_bool {match_true ; match_false} -> - let%bind match_true = f match_true in - let%bind match_false = f match_false in - ok @@ Match_bool {match_true ; match_false} + let%bind match_true = f match_true in + let%bind match_false = f match_false in + ok @@ Match_bool {match_true ; match_false} | Match_tuple (lst, b) -> - let%bind b = f b in - ok @@ Match_tuple (lst, b) + let%bind b = f b in + ok @@ Match_tuple (lst, b) | Match_option {match_none ; match_some = (v, some)} -> - let%bind match_none = f match_none in - let%bind some = f some in - let match_some = fst v, some in - ok @@ Match_option {match_none ; match_some} + let%bind match_none = f match_none in + let%bind some = f some in + let match_some = fst v, some in + ok @@ Match_option {match_none ; match_some} | Match_list {match_nil ; match_cons = (((hd_name , _) , (tl_name , _)), cons)} -> - let%bind match_nil = f match_nil in - let%bind cons = f cons in - let match_cons = hd_name , tl_name , cons in - ok @@ Match_list {match_nil ; match_cons} + let%bind match_nil = f match_nil in + let%bind cons = f cons in + let match_cons = hd_name , tl_name , cons in + ok @@ Match_list {match_nil ; match_cons} | Match_variant (lst , _) -> - let aux ((a,b),c) = - let%bind c' = f c in - ok ((a,b),c') in - let%bind lst' = bind_map_list aux lst in - ok @@ Match_variant lst' + let aux ((a,b),c) = + let%bind c' = f c in + ok ((a,b),c') in + let%bind lst' = bind_map_list aux lst in + ok @@ Match_variant lst'