diff --git a/src/ligo/ast_typed/combinators.ml b/src/ligo/ast_typed/combinators.ml index 131609904..8d8a4f32c 100644 --- a/src/ligo/ast_typed/combinators.ml +++ b/src/ligo/ast_typed/combinators.ml @@ -2,7 +2,8 @@ open Trace open Types let make_t type_value' simplified = { type_value' ; simplified } -let make_a_e expression type_annotation = { expression ; type_annotation } +let make_a_e expression type_annotation = { expression ; type_annotation ; dummy_field = () ; environment = Environment.dummy } +let make_n_e name a_e = { name ; annotated_expression = a_e } let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s let t_string ?s () : type_value = make_t (T_constant ("string", [])) s @@ -129,3 +130,10 @@ let get_a_bool (t:annotated_expression) = match t.expression with | E_literal (Literal_bool b) -> ok b | _ -> simple_fail "not a bool" + +open Environment +let env_sum_type ?(env = empty) + ?(name = "a_sum_type") + (lst : (string * ele) list) = + add env name (make_t_ez_sum lst) + diff --git a/src/ligo/ast_typed/environment.ml b/src/ligo/ast_typed/environment.ml index af5a37bbc..2cb1ab3ce 100644 --- a/src/ligo/ast_typed/environment.ml +++ b/src/ligo/ast_typed/environment.ml @@ -1,17 +1,16 @@ open Types type ele = type_value +type t = full_environment -type t = { - environment: (string * ele) list ; - type_environment: (string * ele) list ; -} let empty : t = { (* TODO: use maps *) environment = [] ; type_environment = [] ; } +let dummy : environment = [] + let get (e:t) (s:string) : ele option = List.assoc_opt s e.environment let get_constructor (e:t) (s:string) : (ele * ele) option = @@ -47,10 +46,3 @@ module PP = struct fprintf ppf "%a\n%a" value e type_ e end -module Combinators = struct - let env_sum_type ?(env = empty) - ?(name = "a_sum_type") - (lst : (string * ele) list) = - add env name (Combinators.make_t_ez_sum lst) -end - diff --git a/src/ligo/ast_typed/types.ml b/src/ligo/ast_typed/types.ml index 6c8c2407e..fcf31eadd 100644 --- a/src/ligo/ast_typed/types.ml +++ b/src/ligo/ast_typed/types.ml @@ -1,3 +1,5 @@ +[@@@warning "-30"] + module S = Ast_simplified module SMap = Map.String @@ -14,9 +16,18 @@ and declaration = | Declaration_constant of named_expression (* | Macro_declaration of macro_declaration *) +and environment = (string * type_value) list +and type_environment = (string * type_value) list +and full_environment = { + environment : environment ; + type_environment : type_environment ; +} + and annotated_expression = { expression: expression ; type_annotation: tv ; + environment: environment ; + dummy_field: unit ; } and named_expression = { diff --git a/src/ligo/test/typer_tests.ml b/src/ligo/test/typer_tests.ml index 038adfd8a..3e056c551 100644 --- a/src/ligo/test/typer_tests.ml +++ b/src/ligo/test/typer_tests.ml @@ -30,7 +30,7 @@ module TestExpressions = struct module I = Simplified.Combinators module O = Typed.Combinators - module E = Typer.Environment.Combinators + module E = O let unit () : unit result = test_expression I.(e_unit ()) O.(t_unit ()) let int () : unit result = test_expression I.(e_int 32) O.(t_int ()) diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index 258712880..3c732d5d9 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -10,7 +10,6 @@ module Environment = O.Environment type environment = Environment.t - module Errors = struct let unbound_type_variable (e:environment) (n:string) () = let title = (thunk "unbound type variable") in @@ -75,7 +74,7 @@ and type_declaration env : I.declaration -> (environment * O.declaration option) 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.Declaration_constant {name;annotated_expression=ae'})) + ok (env', Some (O.Declaration_constant (make_n_e name ae'))) and type_block_full (e:environment) (b:I.block) : (O.block * environment) result = let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) = @@ -108,18 +107,18 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc | Some _, None -> let%bind annotated_expression = type_annotated_expression e annotated_expression in let e' = Environment.add e name annotated_expression.type_annotation in - ok (e', [O.I_declaration {name;annotated_expression}]) + ok (e', [O.I_declaration (make_n_e name annotated_expression)]) | None, Some prev -> let%bind annotated_expression = type_annotated_expression e annotated_expression in let%bind _ = O.assert_type_value_eq (annotated_expression.type_annotation, prev) in - ok (e, [O.I_assignment {name;annotated_expression}]) + ok (e, [O.I_assignment (make_n_e name annotated_expression)]) | Some _, Some prev -> let%bind annotated_expression = type_annotated_expression e annotated_expression in let%bind _assert = trace (simple_error "Annotation doesn't match environment") @@ O.assert_type_value_eq (annotated_expression.type_annotation, prev) in let e' = Environment.add e name annotated_expression.type_annotation in - ok (e', [O.I_assignment {name;annotated_expression}]) + ok (e', [O.I_assignment (make_n_e name annotated_expression)]) ) | I_matching (ex, m) -> let%bind ex' = type_annotated_expression e ex in @@ -231,38 +230,33 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an | None -> ok None | Some s -> let%bind r = evaluate_type e s in ok (Some r) in let check tv = O.(merge_annotation tv_opt (Some tv)) in + let return e tv = + let%bind type_annotation = check tv in + ok @@ make_a_e e type_annotation in match ae.expression with (* Basic *) | E_variable name -> let%bind tv' = trace_option (unbound_variable e name) @@ Environment.get e name in - let%bind type_annotation = check tv' in - ok O.{expression = E_variable name ; type_annotation} + return (E_variable name) tv' | E_literal (Literal_bool b) -> - let%bind type_annotation = check (t_bool ()) in - ok O.{expression = E_literal (Literal_bool b) ; type_annotation } + return (E_literal (Literal_bool b)) (t_bool ()) | E_literal Literal_unit -> - let%bind type_annotation = check (t_unit ()) in - ok O.{expression = E_literal (Literal_unit) ; type_annotation } + return (E_literal (Literal_unit)) (t_unit ()) | E_literal (Literal_string s) -> - let%bind type_annotation = check (t_string ()) in - ok O.{expression = E_literal (Literal_string s) ; type_annotation } + return (E_literal (Literal_string s)) (t_string ()) | E_literal (Literal_bytes s) -> - let%bind type_annotation = check (t_bytes ()) in - ok O.{expression = E_literal (Literal_bytes s) ; type_annotation } + return (E_literal (Literal_bytes s)) (t_bytes ()) | E_literal (Literal_int n) -> - let%bind type_annotation = check (t_int ()) in - ok O.{expression = E_literal (Literal_int n) ; type_annotation } + return (E_literal (Literal_int n)) (t_int ()) | E_literal (Literal_nat n) -> - let%bind type_annotation = check (t_nat ()) in - ok O.{expression = E_literal (Literal_nat n) ; type_annotation } + return (E_literal (Literal_nat n)) (t_nat ()) (* Tuple *) | E_tuple lst -> let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in let tv_lst = List.map get_type_annotation lst' in - let%bind type_annotation = check (t_tuple tv_lst ()) in - ok O.{expression = E_tuple lst' ; type_annotation } + return (E_tuple lst') (t_tuple tv_lst ()) | E_accessor (ae, path) -> let%bind e' = type_annotated_expression e ae in let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result = @@ -272,17 +266,14 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an let%bind tv = generic_try (simple_error "bad tuple index") @@ (fun () -> List.nth tpl_tv index) in - let%bind type_annotation = check tv in - let annotated_expression = O.{expression = E_tuple_accessor (prev, index) ; type_annotation} in - ok annotated_expression + 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 (simple_error "bad record index") @@ (fun () -> SMap.find property r_tv) in - let%bind type_annotation = check tv in - ok O.{expression = O.E_record_accessor (prev, property) ; type_annotation } + return (E_record_accessor (prev , property)) tv ) in trace (simple_error "accessing") @@ @@ -295,8 +286,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an @@ Environment.get_constructor e c in let%bind expr' = type_annotated_expression e expr in let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in - let%bind type_annotation = check sum_tv in - ok O.{expression = O.E_constructor(c, expr') ; type_annotation } + return (E_constructor (c , expr')) sum_tv (* Record *) | E_record m -> let aux prev k expr = @@ -304,12 +294,11 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an ok (SMap.add k expr' prev) in let%bind m' = bind_fold_smap aux (ok SMap.empty) m in - let%bind type_annotation = check @@ t_record (SMap.map get_type_annotation m') () in - ok O.{expression = O.E_record m' ; type_annotation } + return (E_record m') (t_record (SMap.map get_type_annotation m') ()) (* Data-structure *) | E_list lst -> let%bind lst' = bind_map_list (type_annotated_expression e) lst in - let%bind type_annotation = + let%bind tv = let aux opt c = match opt with | None -> ok (Some c) @@ -325,12 +314,12 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an let%bind opt = bind_fold_list aux init @@ List.map get_type_annotation lst' in trace_option (simple_error "empty list expression without annotation") opt in - check (t_list ty ()) + ok (t_list ty ()) in - ok O.{expression = O.E_list lst' ; type_annotation} + return (E_list lst') tv | E_map lst -> let%bind lst' = bind_map_list (bind_map_pair (type_annotated_expression e)) lst in - let%bind type_annotation = + let%bind tv = let aux opt c = match opt with | None -> ok (Some c) @@ -351,9 +340,9 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an @@ List.map snd lst' in trace_option (simple_error "empty map expression") opt in - check (t_map key_type value_type ()) + ok (t_map key_type value_type ()) in - ok O.{expression = O.E_map lst' ; type_annotation} + return (E_map lst') tv | E_lambda { binder ; input_type ; @@ -366,41 +355,37 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an let e' = Environment.add e binder input_type in let%bind (body, e'') = type_block_full e' body in let%bind result = type_annotated_expression e'' result in - let%bind type_annotation = check @@ (t_function input_type output_type ()) in - ok O.{expression = E_lambda {binder;input_type;output_type;result;body} ; type_annotation} + return (E_lambda {binder;input_type;output_type;result;body}) (t_function input_type output_type ()) | E_constant (name, lst) -> let%bind lst' = bind_list @@ List.map (type_annotated_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 in - let%bind type_annotation = check tv in - ok O.{expression = O.E_constant (name', lst') ; type_annotation} + return (E_constant (name' , lst')) tv | E_application (f, arg) -> let%bind f = type_annotated_expression e f in let%bind arg = type_annotated_expression e arg in - let%bind type_annotation = match f.type_annotation.type_value' with + 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 | _ -> simple_fail "applying to not-a-function" in - ok O.{expression = E_application (f, arg) ; type_annotation} + return (E_application (f , arg)) tv | E_look_up dsi -> let%bind (ds, ind) = bind_map_pair (type_annotated_expression e) dsi in let%bind (src, dst) = get_t_map ds.type_annotation in let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in - let dst_opt = (t_option dst ()) in - let%bind type_annotation = check dst_opt in - ok O.{expression = E_look_up (ds, ind) ; type_annotation} + return (E_look_up (ds , ind)) (t_option dst ()) (* Advanced *) | E_matching (ex, m) -> ( let%bind ex' = type_annotated_expression e ex in let%bind m' = type_match type_annotated_expression e ex'.type_annotation m in - let%bind type_annotation = match m' with + let%bind tv = match m' with | Match_bool {match_true ; match_false} -> let%bind _ = O.assert_type_value_eq (match_true.type_annotation, match_false.type_annotation) in ok match_true.type_annotation | _ -> simple_fail "can only type match_bool expressions yet" in - ok O.{expression = E_matching (ex', m') ; type_annotation} + return (E_matching (ex' , m')) tv ) and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result =