add list (partial)

This commit is contained in:
Galfour 2019-04-14 12:02:45 +00:00
parent 7ca28cb34a
commit 3e6e96644c
13 changed files with 190 additions and 8 deletions

View File

@ -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 {@; @[<v>%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')

View File

@ -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[@; @[<v>%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[@; @[<v>%a@]@;]" (list_sep assoc_annotated_expression (tag ",@;")) m
| E_list m -> fprintf ppf "list[@; @[<v>%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

View File

@ -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

View File

@ -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

View File

@ -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"

View File

@ -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 [

View File

@ -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

View File

@ -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

View File

@ -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 =

View File

@ -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

View File

@ -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 ; *)
]

View File

@ -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 ->

View File

@ -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')