diff --git a/src/lib_utils/tezos_utils.ml b/src/lib_utils/tezos_utils.ml index 38bf94f97..3b7158df3 100644 --- a/src/lib_utils/tezos_utils.ml +++ b/src/lib_utils/tezos_utils.ml @@ -22,3 +22,4 @@ module Dictionary = Dictionary module Tree = Tree module Region = Region module Pos = Pos + diff --git a/src/lib_utils/x_list.ml b/src/lib_utils/x_list.ml index e0e1d4732..fd62b7088 100644 --- a/src/lib_utils/x_list.ml +++ b/src/lib_utils/x_list.ml @@ -97,9 +97,12 @@ module Ne = struct let of_list lst = List.(hd lst, tl lst) let to_list (hd, tl : _ t) = hd :: tl + let singleton hd : 'a t = hd , [] let hd : 'a t -> 'a = fst + let cons : 'a -> 'a t -> 'a t = fun hd' (hd , tl) -> hd' , hd :: tl let iter f (hd, tl : _ t) = f hd ; List.iter f tl let map f (hd, tl : _ t) = f hd, List.map f tl + let hd_map : _ -> 'a t -> 'a t = fun f (hd , tl) -> (f hd , tl) let mapi f (hd, tl : _ t) = let lst = List.mapi f (hd::tl) in of_list lst @@ -110,5 +113,9 @@ module Ne = struct | lst -> let r = List.rev lst in (List.hd r, List.tl r @ [hd]) + let find_map = fun f (hd , tl : _ t) -> + match f hd with + | Some x -> Some x + | None -> find_map f tl end diff --git a/src/ligo/ast_typed/combinators.ml b/src/ligo/ast_typed/combinators.ml index 4f6b8ab2f..6dc47492a 100644 --- a/src/ligo/ast_typed/combinators.ml +++ b/src/ligo/ast_typed/combinators.ml @@ -3,6 +3,7 @@ open Types let make_t type_value' simplified = { type_value' ; simplified } let make_a_e expression type_annotation environment = { expression ; type_annotation ; dummy_field = () ; environment } +let make_a_e_empty expression type_annotation = make_a_e expression type_annotation Environment.full_empty let make_n_e name a_e = { name ; annotated_expression = a_e } let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s @@ -116,19 +117,19 @@ let ez_e_a_record r = make_a_e (ez_e_record r) (ez_t_record (List.map (fun (x, y let e_a_map lst k v = make_a_e (e_map lst) (t_map k v ()) let e_a_list lst t = make_a_e (e_list lst) (t_list t ()) -let e_a_empty_unit = e_a_unit Environment.empty -let e_a_empty_int n = e_a_int n Environment.empty -let e_a_empty_nat n = e_a_nat n Environment.empty -let e_a_empty_bool b = e_a_bool b Environment.empty -let e_a_empty_string s = e_a_string s Environment.empty -let e_a_empty_pair a b = e_a_pair a b Environment.empty -let e_a_empty_some s = e_a_some s Environment.empty -let e_a_empty_none t = e_a_none t Environment.empty -let e_a_empty_tuple lst = e_a_tuple lst Environment.empty -let e_a_empty_record r = e_a_record r Environment.empty -let e_a_empty_map lst k v = e_a_map lst k v Environment.empty -let e_a_empty_list lst t = e_a_list lst t Environment.empty -let ez_e_a_empty_record r = ez_e_a_record r Environment.empty +let e_a_empty_unit = e_a_unit Environment.full_empty +let e_a_empty_int n = e_a_int n Environment.full_empty +let e_a_empty_nat n = e_a_nat n Environment.full_empty +let e_a_empty_bool b = e_a_bool b Environment.full_empty +let e_a_empty_string s = e_a_string s Environment.full_empty +let e_a_empty_pair a b = e_a_pair a b Environment.full_empty +let e_a_empty_some s = e_a_some s Environment.full_empty +let e_a_empty_none t = e_a_none t Environment.full_empty +let e_a_empty_tuple lst = e_a_tuple lst Environment.full_empty +let e_a_empty_record r = e_a_record r Environment.full_empty +let e_a_empty_map lst k v = e_a_map lst k v Environment.full_empty +let e_a_empty_list lst t = e_a_list lst t Environment.full_empty +let ez_e_a_empty_record r = ez_e_a_record r Environment.full_empty let get_a_int (t:annotated_expression) = match t.expression with @@ -148,6 +149,6 @@ let get_a_bool (t:annotated_expression) = open Environment let env_sum_type ?(env = full_empty) ?(name = "a_sum_type") - (lst : (string * ele) list) = - add env name (make_t_ez_sum lst) + (lst : (string * element) list) = + add_type name (make_t_ez_sum lst) env diff --git a/src/ligo/ast_typed/environment.ml b/src/ligo/ast_typed/environment.ml index d650f9269..c5a2251f5 100644 --- a/src/ligo/ast_typed/environment.ml +++ b/src/ligo/ast_typed/environment.ml @@ -1,49 +1,64 @@ open Types -type ele = type_value +type element = type_value + +module Small = struct + type t = small_environment + + let empty : t = ([] , []) + + let get_environment : t -> environment = fst + let get_type_environment : t -> type_environment = snd + let map_environment : _ -> t -> t = fun f (a , b) -> (f a , b) + let map_type_environment : _ -> t -> t = fun f (a , b) -> (a , f b) + + let add : string -> element -> t -> t = fun k v -> map_environment (fun x -> (k , v) :: x) + let add_type : string -> element -> t -> t = fun k v -> map_type_environment (fun x -> (k , v) :: x) + let get_opt : string -> t -> element option = fun k x -> List.assoc_opt k (get_environment x) + let get_type_opt : string -> t -> element option = fun k x -> List.assoc_opt k (get_type_environment x) +end + type t = full_environment +let empty : environment = Small.(get_environment empty) +let full_empty : t = List.Ne.singleton Small.empty +let add : string -> element -> t -> t = fun k v -> List.Ne.hd_map (Small.add k v) +let add_type : string -> element -> t -> t = fun k v -> List.Ne.hd_map (Small.add_type k v) +let get_opt : string -> t -> element option = fun k x -> List.Ne.find_map (Small.get_opt k) x +let get_type_opt : string -> t -> element option = fun k x -> List.Ne.find_map (Small.get_type_opt k) x -let empty = [] -let full_empty : t = { - (* TODO: use maps *) - environment = [] ; - type_environment = [] ; -} +let get_constructor : string -> t -> (element * element) option = fun k x -> (* Left is the constructor, right is the sum type *) + let aux = fun x -> + let aux = fun (_type_name , x) -> + match x.type_value' with + | T_sum m when Map.String.mem k m -> Some (Map.String.find k m , x) + | _ -> None + in + List.find_map aux (Small.get_type_environment x) in + List.Ne.find_map aux x -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 = - let rec aux = function - | [] -> None - | (_, ({type_value'=(T_sum m)} as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv) - | _ :: tl -> aux tl - in - aux e.environment - -let add (e:t) (s:string) (tv:ele) : t = - {e with environment = (s, tv) :: e.environment} -let get_type (e:t) (s:string) : ele option = - List.assoc_opt s e.type_environment -let add_type (e:t) (s:string) (tv:ele) : t = - {e with type_environment = (s, tv) :: e.type_environment} module PP = struct open Format open PP_helpers - let list_sep_d x = list_sep x (const " , ") + let list_sep_scope x = list_sep x (const " | ") - let value ppf (e:t) = - let pp ppf (s, e) = fprintf ppf "%s -> %a" s PP.type_value e in - fprintf ppf "ValueEnv[%a]" (list_sep_d pp) e.environment + let assoc = fun ppf (k , tv) -> + fprintf ppf "%s -> %a" k PP.type_value tv - let type_ ppf e = - let pp ppf (s, e) = fprintf ppf "%s -> %a" s PP.type_value e in - fprintf ppf "TypeEnv[%a]" (list_sep_d pp) e.type_environment + let environment : _ -> environment -> unit = fun ppf lst -> + fprintf ppf "E[%a]" (list_sep assoc (const " , ")) lst - let full ppf e = - fprintf ppf "%a\n%a" value e type_ e + let type_environment = fun ppf lst -> + fprintf ppf "T[%a]" (list_sep assoc (const " , ")) lst + + let small_environment : _ -> small_environment -> unit = fun ppf e -> + fprintf ppf "- %a\t%a" + environment (Small.get_environment e) + type_environment (Small.get_type_environment e) + + let full_environment : _ -> full_environment -> unit = fun ppf e -> + fprintf ppf "@[%a]" + (ne_list_sep small_environment (tag "@;")) e end diff --git a/src/ligo/ast_typed/types.ml b/src/ligo/ast_typed/types.ml index fcf31eadd..0a2bc4129 100644 --- a/src/ligo/ast_typed/types.ml +++ b/src/ligo/ast_typed/types.ml @@ -18,15 +18,13 @@ and declaration = and environment = (string * type_value) list and type_environment = (string * type_value) list -and full_environment = { - environment : environment ; - type_environment : type_environment ; -} +and small_environment = (environment * type_environment) +and full_environment = small_environment List.Ne.t and annotated_expression = { expression: expression ; type_annotation: tv ; - environment: environment ; + environment: full_environment ; dummy_field: unit ; } diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index 856057a1f..287c69f49 100644 --- a/src/ligo/transpiler.ml +++ b/src/ligo/transpiler.ml @@ -489,7 +489,7 @@ let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result = let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression result = let open! AST in - let return e = ok (make_a_e e t Environment.empty) in + let return e = ok (make_a_e_empty e t) in match t.type_value' with | T_constant ("unit", []) -> let%bind () = get_unit v in @@ -508,10 +508,10 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression return (E_literal (Literal_string n)) | T_constant ("option", [o]) -> ( match%bind get_option v with - | None -> ok (e_a_none o Environment.empty) + | None -> ok (e_a_empty_none o) | Some s -> let%bind s' = untranspile s o in - ok (e_a_some s' Environment.empty) + ok (e_a_empty_some s') ) | T_constant ("map", [k_ty;v_ty]) -> ( let%bind lst = get_map v in diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index 9261d515b..c3716b008 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -13,12 +13,12 @@ type environment = Environment.t module Errors = struct let unbound_type_variable (e:environment) (n:string) () = let title = (thunk "unbound type variable") in - let full () = Format.asprintf "%s in %a" n Environment.PP.type_ e in + let full () = Format.asprintf "%s in %a" n Environment.PP.full_environment e in error title full () let unbound_variable (e:environment) (n:string) () = let title = (thunk "unbound variable") in - let full () = Format.asprintf "%s in %a" n Environment.PP.value e in + let full () = Format.asprintf "%s in %a" n Environment.PP.full_environment e in error title full () let unrecognized_constant (n:string) () = @@ -67,13 +67,13 @@ let rec type_program (p:I.program) : O.program result = and type_declaration env : I.declaration -> (environment * 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 env type_name tv in + let env' = Environment.add_type type_name tv env in ok (env', None) | Declaration_constant {name;annotated_expression} -> let%bind ae' = trace (constant_declaration_error name annotated_expression) @@ type_annotated_expression env annotated_expression in - let env' = Environment.add env name ae'.type_annotation in + let env' = Environment.add name ae'.type_annotation env in ok (env', Some (O.Declaration_constant (make_n_e name ae'))) and type_block_full (e:environment) (b:I.block) : (O.block * environment) result = @@ -102,11 +102,11 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc let%bind body = type_block e body in return @@ O.I_loop (cond, body) | I_assignment {name;annotated_expression} -> ( - match annotated_expression.type_annotation, Environment.get e name with + match annotated_expression.type_annotation, Environment.get_opt name e with | None, None -> simple_fail "Initial assignments need type annotation" | Some _, None -> let%bind annotated_expression = type_annotated_expression e annotated_expression in - let e' = Environment.add e name annotated_expression.type_annotation in + let e' = Environment.add name annotated_expression.type_annotation e in 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 @@ -117,7 +117,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc 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 + let e' = Environment.add name annotated_expression.type_annotation e in ok (e', [O.I_assignment (make_n_e name annotated_expression)]) ) | I_matching (ex, m) -> @@ -129,7 +129,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc let%bind ae' = type_annotated_expression e ae in let%bind ty = trace_option (simple_error "unbound variable in record_patch") @@ - Environment.get e r in + Environment.get_opt r e in let tv = O.{type_name = r ; type_value = ty} in let aux ty access = match access with @@ -165,7 +165,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t let%bind match_none = f e match_none in let (n, b) = match_some in let n' = n, t_opt in - let e' = Environment.add e n t_opt in + let e' = Environment.add 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} -> @@ -174,8 +174,8 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t @@ get_t_list t in let%bind match_nil = f e match_nil in let (hd, tl, b) = match_cons in - let e' = Environment.add e hd t_list in - let e' = Environment.add e' tl t in + let e' = Environment.add hd t_list e in + let e' = Environment.add tl t e' in let%bind b' = f e' b in ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')}) | Match_tuple (lst, b) -> @@ -185,7 +185,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t let%bind lst' = generic_try (simple_error "Matching tuple of different size") @@ (fun () -> List.combine lst t_tuple) in - let aux prev (name, tv) = Environment.add prev name tv in + let aux prev (name, tv) = Environment.add 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')) @@ -219,7 +219,7 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = | T_variable name -> let%bind tv = trace_option (unbound_type_variable e name) - @@ Environment.get_type e name in + @@ 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 @@ -232,13 +232,13 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot let check tv = O.(merge_annotation tv_opt (Some tv)) in let return expr tv = let%bind type_annotation = check tv in - ok @@ make_a_e expr type_annotation e.environment in + ok @@ make_a_e expr type_annotation e in match ae.expression with (* Basic *) | E_variable name -> let%bind tv' = trace_option (unbound_variable e name) - @@ Environment.get e name in + @@ Environment.get_opt name e in return (E_variable name) tv' | E_literal (Literal_bool b) -> return (E_literal (Literal_bool b)) (t_bool ()) @@ -282,8 +282,15 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot (* Sum *) | E_constructor (c, expr) -> let%bind (c_tv, sum_tv) = - trace_option (simple_error "no such constructor") - @@ Environment.get_constructor e c in + 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_annotated_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 @@ -352,7 +359,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot } -> let%bind input_type = evaluate_type e input_type in let%bind output_type = evaluate_type e output_type in - let e' = Environment.add e binder input_type in + let e' = Environment.add binder input_type e in let%bind (body, e'') = type_block_full e' body in let%bind result = type_annotated_expression e'' result in return (E_lambda {binder;input_type;output_type;result;body}) (t_function input_type output_type ())