From 3e6e96644cf0ba25b84aac3745a9514883220cdf Mon Sep 17 00:00:00 2001 From: Galfour Date: Sun, 14 Apr 2019 12:02:45 +0000 Subject: [PATCH] add list (partial) --- src/ligo/ast_simplified.ml | 5 +++ src/ligo/ast_typed.ml | 12 ++++++- src/ligo/contracts/list.ligo | 19 +++++++++++ src/ligo/mini_c/PP.ml | 3 ++ src/ligo/mini_c/combinators.ml | 8 +++++ src/ligo/mini_c/compiler.ml | 12 +++++++ src/ligo/mini_c/compiler_type.ml | 7 ++++ src/ligo/mini_c/types.ml | 3 ++ src/ligo/mini_c/uncompiler.ml | 10 ++++++ src/ligo/simplify.ml | 28 ++++++++++++---- src/ligo/test/integration_tests.ml | 53 ++++++++++++++++++++++++++++++ src/ligo/transpiler.ml | 17 ++++++++++ src/ligo/typer.ml | 21 +++++++++++- 13 files changed, 190 insertions(+), 8 deletions(-) create mode 100644 src/ligo/contracts/list.ligo diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml index 7873ab08a..19c85fe29 100644 --- a/src/ligo/ast_simplified.ml +++ b/src/ligo/ast_simplified.ml @@ -65,6 +65,7 @@ and expression = | E_accessor of (ae * access_path) (* Data Structures *) | E_map of (ae * ae) list + | E_list of ae list | E_look_up of (ae * ae) (* Matching *) | E_matching of (ae * matching_expr) @@ -152,6 +153,7 @@ module PP = struct | E_accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p | E_record m -> fprintf ppf "record[%a]" (smap_sep_d annotated_expression) m | E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_annotated_expression) m + | E_list lst -> fprintf ppf "list[%a]" (list_sep_d annotated_expression) lst | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind | E_lambda {binder;input_type;output_type;result;body} -> fprintf ppf "lambda (%s:%a) : %a {@; @[%a@]@;} return %a" @@ -342,6 +344,9 @@ module Rename = struct let%bind m' = bind_map_list (fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in ok (E_map m') + | E_list lst -> + let%bind lst' = bind_map_list (rename_annotated_expression r) lst in + ok (E_list lst') | E_look_up m -> let%bind m' = bind_map_pair (rename_annotated_expression r) m in ok (E_look_up m') diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index 9493f9392..f34781fd5 100644 --- a/src/ligo/ast_typed.ml +++ b/src/ligo/ast_typed.ml @@ -71,6 +71,7 @@ and expression = | E_record_accessor of (ae * string) (* Data Structures *) | E_map of (ae * ae) list + | E_list of ae list | E_look_up of (ae * ae) (* Advanced *) | E_matching of (ae * matching_expr) @@ -184,6 +185,7 @@ module PP = struct | E_tuple lst -> fprintf ppf "tuple[@; @[%a@]@;]" (list_sep annotated_expression (tag ",@;")) lst | E_record m -> fprintf ppf "record[%a]" (smap_sep_d annotated_expression) m | E_map m -> fprintf ppf "map[@; @[%a@]@;]" (list_sep assoc_annotated_expression (tag ",@;")) m + | E_list m -> fprintf ppf "list[@; @[%a@]@;]" (list_sep annotated_expression (tag ",@;")) m | E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i | E_matching (ae, m) -> fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m @@ -451,6 +453,7 @@ module Combinators = struct let t_unit ?s () : type_value = type_value (T_constant ("unit", [])) s let t_option o ?s () : type_value = type_value (T_constant ("option", [o])) s let t_tuple lst ?s () : type_value = type_value (T_tuple lst) s + let t_list t ?s () : type_value = type_value (T_constant ("list", [t])) s let t_pair a b ?s () = t_tuple [a ; b] ?s () let t_record m ?s () : type_value = type_value (T_record m) s @@ -501,12 +504,17 @@ module Combinators = struct let get_t_map (t:type_value) : (type_value * type_value) result = match t.type_value' with | T_constant ("map", [k;v]) -> ok (k, v) - | _ -> simple_fail "not a map" + | _ -> simple_fail "get: not a map" let assert_t_map (t:type_value) : unit result = match t.type_value' with | T_constant ("map", [_ ; _]) -> ok () | _ -> simple_fail "not a map" + let assert_t_list (t:type_value) : unit result = + match t.type_value' with + | T_constant ("list", [_]) -> ok () + | _ -> simple_fail "assert: not a list" + let assert_t_int : type_value -> unit result = fun t -> match t.type_value' with | T_constant ("int", []) -> ok () | _ -> simple_fail "not an int" @@ -531,6 +539,7 @@ module Combinators = struct let e_bool b : expression = E_literal (Literal_bool b) let e_string s : expression = E_literal (Literal_string s) let e_pair a b : expression = E_tuple [a; b] + let e_list lst : expression = E_list lst let e_a_unit = annotated_expression e_unit (t_unit ()) let e_a_int n = annotated_expression (e_int n) (t_int ()) @@ -544,6 +553,7 @@ module Combinators = struct let e_a_record r = annotated_expression (e_record r) (t_record (SMap.map get_type_annotation r) ()) let ez_e_a_record r = annotated_expression (ez_e_record r) (ez_t_record (List.map (fun (x, y) -> x, y.type_annotation) r) ()) let e_a_map lst k v = annotated_expression (e_map lst) (t_map k v ()) + let e_a_list lst t = annotated_expression (e_list lst) (t_list t ()) let get_a_int (t:annotated_expression) = match t.expression with diff --git a/src/ligo/contracts/list.ligo b/src/ligo/contracts/list.ligo new file mode 100644 index 000000000..60af05003 --- /dev/null +++ b/src/ligo/contracts/list.ligo @@ -0,0 +1,19 @@ +type foobar is list(int) + +const fb : foobar = list + 23 ; + 42 ; +end + +function size_ (const m : foobar) : nat is + block {skip} with (size(m)) + +// function hdf (const m : foobar) : int is begin skip end with hd(m) + +const bl : foobar = list + 144 ; + 51 ; + 42 ; + 120 ; + 421 ; +end diff --git a/src/ligo/mini_c/PP.ml b/src/ligo/mini_c/PP.ml index 450f901db..3b0cef09c 100644 --- a/src/ligo/mini_c/PP.ml +++ b/src/ligo/mini_c/PP.ml @@ -20,6 +20,7 @@ let rec type_ ppf : type_value -> _ = function | T_base b -> type_base ppf b | T_function(a, b) -> fprintf ppf "(%a) -> (%a)" type_ a type_ b | T_map(k, v) -> fprintf ppf "map(%a -> %a)" type_ k type_ v + | T_list(t) -> fprintf ppf "list(%a)" type_ t | T_option(o) -> fprintf ppf "option(%a)" type_ o | T_shallow_closure(_, a, b) -> fprintf ppf "[big_closure](%a) -> (%a)" type_ a type_ b | T_deep_closure(c, arg, ret) -> @@ -55,6 +56,7 @@ let rec value ppf : value -> unit = function | D_none -> fprintf ppf "None" | D_some s -> fprintf ppf "Some (%a)" value s | D_map m -> fprintf ppf "Map[%a]" (list_sep_d value_assoc) m + | D_list lst -> fprintf ppf "List[%a]" (list_sep_d value) lst and value_assoc ppf : (value * value) -> unit = fun (a, b) -> fprintf ppf "%a -> %a" value a value b @@ -66,6 +68,7 @@ and expression' ppf (e:expression') = match e with | E_literal v -> fprintf ppf "%a" value v | E_function c -> function_ ppf c | E_empty_map _ -> fprintf ppf "map[]" + | E_empty_list _ -> fprintf ppf "list[]" | E_make_none _ -> fprintf ppf "none" | E_Cond (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b diff --git a/src/ligo/mini_c/combinators.ml b/src/ligo/mini_c/combinators.ml index cb7b33bf0..d6f328ba3 100644 --- a/src/ligo/mini_c/combinators.ml +++ b/src/ligo/mini_c/combinators.ml @@ -34,6 +34,10 @@ let get_map (v:value) = match v with | D_map lst -> ok lst | _ -> simple_fail "not a map" +let get_list (v:value) = match v with + | D_list lst -> ok lst + | _ -> simple_fail "not a list" + let get_t_option (v:type_value) = match v with | T_option t -> ok t | _ -> simple_fail "not an option" @@ -50,6 +54,10 @@ let get_t_map (t:type_value) = match t with | T_map kv -> ok kv | _ -> simple_fail "not a type map" +let get_t_list (t:type_value) = match t with + | T_list t -> ok t + | _ -> simple_fail "not a type list" + let get_left (v:value) = match v with | D_left b -> ok b | _ -> simple_fail "not a left" diff --git a/src/ligo/mini_c/compiler.ml b/src/ligo/mini_c/compiler.ml index 348d50c36..b9ab70f76 100644 --- a/src/ligo/mini_c/compiler.ml +++ b/src/ligo/mini_c/compiler.ml @@ -51,6 +51,7 @@ let rec get_predicate : string -> expression list -> predicate result = fun s ls | "GET" -> ok @@ simple_binary @@ prim I_GET | "SIZE" -> ok @@ simple_unary @@ prim I_SIZE | "INT" -> ok @@ simple_unary @@ prim I_INT + | "CONS" -> ok @@ simple_binary @@ seq [prim I_SWAP ; prim I_CONS] | "MAP_REMOVE" -> let%bind v = match lst with | [ _ ; (_, m, _) ] -> @@ -86,6 +87,10 @@ and translate_value (v:value) : michelson result = match v with let%bind lst' = bind_map_list (bind_map_pair translate_value) lst in let aux (a, b) = prim ~children:[a;b] D_Elt in ok @@ seq @@ List.map aux lst' + | D_list lst -> + let%bind lst' = bind_map_list translate_value lst in + let aux = fun a -> prim ~children:[a] D_Elt in + ok @@ seq @@ List.map aux lst' and translate_function ({capture;content}:anon_function) : michelson result = let {capture_type } = content in @@ -181,6 +186,13 @@ and translate_expression ((expr', ty, env) as expr:expression) : michelson resul i_pair ; ] in ok code + | E_empty_list t -> + let%bind t' = Compiler_type.type_ t in + let code = seq [ + prim ~children:[t'] I_NIL ; + i_pair ; + ] in + ok code | E_make_none o -> let%bind o' = Compiler_type.type_ o in let code = seq [ diff --git a/src/ligo/mini_c/compiler_type.ml b/src/ligo/mini_c/compiler_type.ml index f9d245fc0..c8bc5597e 100644 --- a/src/ligo/mini_c/compiler_type.ml +++ b/src/ligo/mini_c/compiler_type.ml @@ -31,6 +31,7 @@ module Ty = struct | T_or _ -> fail (not_comparable "or") | T_pair _ -> fail (not_comparable "pair") | T_map _ -> fail (not_comparable "map") + | T_list _ -> fail (not_comparable "list") | T_option _ -> fail (not_comparable "option") let base_type : type_base -> ex_ty result = fun b -> @@ -76,6 +77,9 @@ module Ty = struct let%bind (Ex_comparable_ty k') = comparable_type k in let%bind (Ex_ty v') = type_ v in ok @@ Ex_ty Contract_types.(map k' v') + | T_list t -> + let%bind (Ex_ty t') = type_ t in + ok @@ Ex_ty Contract_types.(list t') | T_option t -> let%bind (Ex_ty t') = type_ t in ok @@ Ex_ty Contract_types.(option t') @@ -127,6 +131,9 @@ let rec type_ : type_value -> O.michelson result = | T_map kv -> let%bind (k', v') = bind_map_pair type_ kv in ok @@ O.prim ~children:[k';v'] O.T_map + | T_list t -> + let%bind t' = type_ t in + ok @@ O.prim ~children:[t'] O.T_list | T_option o -> let%bind o' = type_ o in ok @@ O.prim ~children:[o'] O.T_option diff --git a/src/ligo/mini_c/types.ml b/src/ligo/mini_c/types.ml index 1f8c2c9e9..6e71a2ffa 100644 --- a/src/ligo/mini_c/types.ml +++ b/src/ligo/mini_c/types.ml @@ -16,6 +16,7 @@ type type_value = | T_shallow_closure of environment * type_value * type_value | T_base of type_base | T_map of (type_value * type_value) + | T_list of type_value | T_option of type_value @@ -48,6 +49,7 @@ type value = | D_some of value | D_none | D_map of (value * value) list + | D_list of value list (* | `Macro of anon_macro ... The future. *) | D_function of anon_function @@ -58,6 +60,7 @@ and expression' = | E_application of expression * expression | E_variable of var_name | E_empty_map of (type_value * type_value) + | E_empty_list of type_value | E_make_none of type_value | E_Cond of expression * expression * expression diff --git a/src/ligo/mini_c/uncompiler.ml b/src/ligo/mini_c/uncompiler.ml index 07dd41986..9cfb7199b 100644 --- a/src/ligo/mini_c/uncompiler.ml +++ b/src/ligo/mini_c/uncompiler.ml @@ -55,6 +55,16 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result = bind_map_list aux lst in ok @@ D_map lst' + | (List_t (ty, _)), lst -> + let lst' = + let aux acc cur = cur :: acc in + let lst = List.fold_left aux lst [] in + List.rev lst in + let%bind lst'' = + let aux = fun t -> translate_value (Ex_typed_value (ty, t)) in + bind_map_list aux lst' + in + ok @@ D_list lst'' | ty, v -> let%bind error = let%bind m_data = diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml index 637cccacf..ae6ad0b04 100644 --- a/src/ligo/simplify.ml +++ b/src/ligo/simplify.ml @@ -16,6 +16,7 @@ let type_constants = [ ("nat", 0) ; ("int", 0) ; ("bool", 0) ; + ("operation", 0) ; ("list", 1) ; ("option", 1) ; ("set", 1) ; @@ -108,7 +109,7 @@ let rec simpl_expression (t:Raw.expr) : ae result = let args' = npseq_to_list args.value.inside in match List.assoc_opt f constants with | None -> - let%bind arg = simpl_list_expression args' in + let%bind arg = simpl_tuple_expression args' in ok @@ ae @@ E_application (ae @@ E_variable f, arg) | Some arity -> let%bind _arity = @@ -122,7 +123,7 @@ let rec simpl_expression (t:Raw.expr) : ae result = | EBytes x -> ok @@ ae @@ E_literal (Literal_bytes (Bytes.of_string @@ fst x.value)) | ETuple tpl -> let (Raw.TupleInj tpl') = tpl in - simpl_list_expression + simpl_tuple_expression @@ npseq_to_list tpl'.value.inside | ERecord (RecordInj r) -> let%bind fields = bind_list @@ -138,13 +139,13 @@ let rec simpl_expression (t:Raw.expr) : ae result = | EConstr (ConstrApp c) -> let (c, args) = c.value in let%bind arg = - simpl_list_expression + simpl_tuple_expression @@ npseq_to_list args.value.inside in ok @@ ae @@ E_constructor (c.value, arg) | EConstr (SomeApp a) -> let (_, args) = a.value in let%bind arg = - simpl_list_expression + simpl_tuple_expression @@ npseq_to_list args.value.inside in ok @@ ae @@ E_constant ("SOME", [arg]) | EConstr (NoneExpr n) -> @@ -166,7 +167,7 @@ let rec simpl_expression (t:Raw.expr) : ae result = ok @@ ae @@ E_literal (Literal_string s.value) | EString _ -> simple_fail "string: not supported yet" | ELogic l -> simpl_logic_expression l - | EList _ -> simple_fail "list: not supported yet" + | EList l -> simpl_list_expression l | ESet _ -> simple_fail "set: not supported yet" | ECase c -> let%bind e = simpl_expression c.value.expr in @@ -222,6 +223,21 @@ and simpl_logic_expression (t:Raw.logic_expr) : ae result = | CompExpr (Neq c) -> simpl_binop "NEQ" c.value +and simpl_list_expression (t:Raw.list_expr) : ae result = + match t with + | Cons c -> + simpl_binop "CONS" c.value + | List lst -> + let%bind lst' = + bind_map_list simpl_expression @@ + pseq_to_list lst.value.elements in + ok (ae (E_list lst')) + | Nil n -> + let n' = n.value.inside in + let%bind t' = simpl_type_expression n'.list_type in + let e' = E_list [] in + ok (annotated_expression e' (Some t')) + and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result = let%bind a = simpl_expression t.arg1 in let%bind b = simpl_expression t.arg2 in @@ -231,7 +247,7 @@ and simpl_unop (name:string) (t:_ Raw.un_op) : ae result = let%bind a = simpl_expression t.arg in ok @@ ae @@ E_constant (name, [a]) -and simpl_list_expression (lst:Raw.expr list) : ae result = +and simpl_tuple_expression (lst:Raw.expr list) : ae result = match lst with | [] -> ok @@ ae @@ E_literal Literal_unit | [hd] -> simpl_expression hd diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml index dd84c32d7..af4dfa3e5 100644 --- a/src/ligo/test/integration_tests.ml +++ b/src/ligo/test/integration_tests.ml @@ -265,6 +265,43 @@ let map () : unit result = in ok () +let list () : unit result = + let%bind program = type_file "./contracts/list.ligo" in + let ez lst = + let open AST_Typed.Combinators in + let lst' = List.map e_a_int lst in + e_a_list lst' (t_int ()) + in + (* let%bind _get_force = trace (simple_error "hd_force") @@ + * let aux n = + * let input = ez [n ; 12] in + * let%bind result = easy_run_typed "hdf" program input in + * let expect = AST_Typed.Combinators.(e_a_int n) in + * AST_Typed.assert_value_eq (expect, result) + * in + * bind_map_list aux [0 ; 42 ; 51 ; 421 ; -3] + * in *) + let%bind _size = trace (simple_error "size") @@ + let aux n = + let input = ez (List.range n) in + let%bind result = easy_run_typed "size_" program input in + let expect = AST_Typed.Combinators.(e_a_nat n) in + AST_Typed.assert_value_eq (expect, result) + in + bind_map_list aux [1 ; 10 ; 3] + in + let%bind _foobar = trace (simple_error "foobar") @@ + let%bind result = easy_evaluate_typed "fb" program in + let expect = ez [23 ; 42] in + AST_Typed.assert_value_eq (expect, result) + in + let%bind _biglist = trace (simple_error "biglist") @@ + let%bind result = easy_evaluate_typed "bl" program in + let expect = ez [144 ; 51 ; 42 ; 120 ; 421] in + AST_Typed.assert_value_eq (expect, result) + in + ok () + let condition () : unit result = let%bind program = type_file "./contracts/condition.ligo" in let aux n = @@ -424,6 +461,20 @@ let quote_declarations () : unit result = @@ [0 ; 2 ; 42 ; 163 ; -1] in ok () +(* let counter_contract () : unit result = + * let%bind program = type_file "./contracts/counter.ligo" in + * let aux n = + * let open AST_Typed.Combinators in + * let input = e_a_pair (e_a_int n) (e_a_int 42) in + * let%bind result = easy_run_main_typed program input in + * let expected = e_a_pair (e_a_list []) (e_a_int (42 + n)) in + * AST_Typed.assert_value_eq (result, expected) + * in + * let%bind _ = bind_list + * @@ List.map aux + * @@ [0 ; 2 ; 42 ; 163 ; -1] in + * ok () *) + let main = "Integration (End to End)", [ test "basic" basic ; test "function" function_ ; @@ -435,6 +486,7 @@ let main = "Integration (End to End)", [ test "tuple" tuple ; test "option" option ; test "map" map ; + test "list" list ; test "multiple parameters" multiple_parameters ; test "condition" condition ; test "loop" loop ; @@ -443,4 +495,5 @@ let main = "Integration (End to End)", [ test "quote declaration" quote_declaration ; test "quote declarations" quote_declarations ; test "#include directives" include_ ; + (* test "counter contract" counter_contract ; *) ] diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index f1ad1332c..16a6df154 100644 --- a/src/ligo/transpiler.ml +++ b/src/ligo/transpiler.ml @@ -21,6 +21,9 @@ let rec translate_type (t:AST.type_value) : type_value result = | T_constant ("map", [key;value]) -> let%bind kv' = bind_map_pair translate_type (key, value) in ok (T_map kv') + | T_constant ("list", [t]) -> + let%bind t' = translate_type t in + ok (T_list t') | T_constant ("option", [o]) -> let%bind o' = translate_type o in ok (T_option o') @@ -306,6 +309,13 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express | _ -> ok (E_constant (name, lst'), tv, env) ) | E_lambda l -> translate_lambda env l tv + | E_list lst -> + let%bind t = Mini_c.Combinators.get_t_list tv in + let%bind lst' = bind_map_list (translate_annotated_expression env) lst in + let aux : expression -> expression -> expression result = fun prev cur -> + return (E_constant ("CONS", [cur ; prev]), tv) in + let%bind (init : expression) = return (E_empty_list t, tv) in + bind_fold_list aux init lst' | E_map m -> let%bind (src, dst) = Mini_c.Combinators.get_t_map tv in let aux : expression result -> (AST.ae * AST.ae) -> expression result = fun prev (k, v) -> @@ -513,6 +523,13 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression bind_map_list aux lst in return (E_map lst') ) + | T_constant ("list", [ty]) -> ( + let%bind lst = get_list v in + let%bind lst' = + let aux = fun e -> untranspile e ty in + bind_map_list aux lst in + return (E_list lst') + ) | T_constant _ -> simple_fail "unknown type_constant" | T_sum m -> diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index 2beeaada6..46306876b 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -351,6 +351,22 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an let%bind type_annotation = check @@ t_record (SMap.map get_annotation m') () in ok O.{expression = O.E_record m' ; type_annotation } (* Data-structure *) + | E_list lst -> + let%bind lst' = bind_map_list (type_annotated_expression e) lst in + let%bind type_annotation = + 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 ty = + let%bind opt = bind_fold_list aux None + @@ List.map Ast_typed.get_type_annotation lst' in + trace_option (simple_error "empty list expression") opt in + check (t_list ty ()) + in + ok O.{expression = O.E_list lst' ; type_annotation} | E_map lst -> let%bind lst' = bind_map_list (bind_map_pair (type_annotated_expression e)) lst in let%bind type_annotation = @@ -474,7 +490,7 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt ok ("GET_FORCE", dst) | "get_force", _ -> simple_fail "bad number of params to get_force" | "size", [t] -> - let%bind () = assert_t_map t in + let%bind () = bind_or (assert_t_map t, assert_t_list t) in ok ("SIZE", t_nat ()) | "size", _ -> simple_fail "bad number of params to size" | "int", [t] -> @@ -542,6 +558,9 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex | E_map m -> let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in return (E_map m') + | E_list lst -> + let%bind lst' = bind_map_list untype_annotated_expression lst in + return (E_list lst') | E_look_up dsi -> let%bind dsi' = bind_map_pair untype_annotated_expression dsi in return (E_look_up dsi')