Merge branch 'feature/more-operators' into 'dev'

Feature/more operators

See merge request ligolang/ligo!32
This commit is contained in:
Matej Šima 2019-06-12 20:34:16 +00:00
commit 072d753e91
31 changed files with 539 additions and 30 deletions

View File

@ -24,6 +24,7 @@ let literal ppf (l:literal) = match l with
| Literal_bool b -> fprintf ppf "%b" b
| Literal_int n -> fprintf ppf "%d" n
| Literal_nat n -> fprintf ppf "+%d" n
| Literal_timestamp n -> fprintf ppf "+%d" n
| Literal_tez n -> fprintf ppf "%dtz" n
| Literal_string s -> fprintf ppf "%S" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
@ -41,6 +42,7 @@ let rec expression ppf (e:expression) = match Location.unwrap e with
| E_record m -> fprintf ppf "record[%a]" (smap_sep_d expression) m
| E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_expression) m
| E_list lst -> fprintf ppf "list[%a]" (list_sep_d expression) lst
| E_set lst -> fprintf ppf "set[%a]" (list_sep_d expression) lst
| E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" expression ds expression ind
| E_lambda {binder;input_type;output_type;result} ->
fprintf ppf "lambda (%a:%a) : %a return %a"

View File

@ -1,5 +1,5 @@
include Types
include Misc
(* include Misc *)
include Combinators
module Types = Types

View File

@ -4,6 +4,17 @@ module Option = Simple_utils.Option
module SMap = Map.String
module Errors = struct
let bad_kind expected location =
let title () = Format.asprintf "a %s was expected" expected in
let message () = "" in
let data = [
("location" , fun () -> Format.asprintf "%a" Location.pp location) ;
] in
error ~data title message
end
open Errors
let t_bool : type_expression = T_constant ("bool", [])
let t_string : type_expression = T_constant ("string", [])
let t_bytes : type_expression = T_constant ("bytes", [])
@ -32,6 +43,7 @@ let ez_t_sum (lst:(string * type_expression) list) : type_expression =
let t_function param result : type_expression = T_function (param, result)
let t_map key value = (T_constant ("map", [key ; value]))
let t_set key = (T_constant ("set", [key]))
let make_name (s : string) : name = s
@ -40,6 +52,7 @@ let e_literal ?loc l : expression = Location.wrap ?loc @@ E_literal l
let e_unit ?loc () : expression = Location.wrap ?loc @@ E_literal (Literal_unit)
let e_int ?loc n : expression = Location.wrap ?loc @@ E_literal (Literal_int n)
let e_nat ?loc n : expression = Location.wrap ?loc @@ E_literal (Literal_nat n)
let e_timestamp ?loc n : expression = Location.wrap ?loc @@ E_literal (Literal_timestamp n)
let e_bool ?loc b : expression = Location.wrap ?loc @@ E_literal (Literal_bool b)
let e_string ?loc s : expression = Location.wrap ?loc @@ E_literal (Literal_string s)
let e_address ?loc s : expression = Location.wrap ?loc @@ E_literal (Literal_address s)
@ -51,6 +64,7 @@ let e_some ?loc s : expression = Location.wrap ?loc @@ E_constant ("SOME", [s])
let e_none ?loc () : expression = Location.wrap ?loc @@ E_constant ("NONE", [])
let e_map_add ?loc k v old : expression = Location.wrap ?loc @@ E_constant ("MAP_ADD" , [k ; v ; old])
let e_map ?loc lst : expression = Location.wrap ?loc @@ E_map lst
let e_set ?loc lst : expression = Location.wrap ?loc @@ E_set lst
let e_list ?loc lst : expression = Location.wrap ?loc @@ E_list lst
let e_pair ?loc a b : expression = Location.wrap ?loc @@ E_tuple [a; b]
let e_constructor ?loc s a : expression = Location.wrap ?loc @@ E_constructor (s , a)
@ -91,6 +105,8 @@ let e_typed_list ?loc lst t =
let e_typed_map ?loc lst k v = e_annotation ?loc (e_map lst) (t_map k v)
let e_typed_set ?loc lst k = e_annotation ?loc (e_set lst) (t_set k)
let e_lambda ?loc (binder : string)
(input_type : type_expression option)
(output_type : type_expression option)
@ -140,3 +156,23 @@ let get_e_failwith = fun e ->
| _ -> simple_fail "not a failwith"
let is_e_failwith e = to_bool @@ get_e_failwith e
let extract_pair : expression -> (expression * expression) result = fun e ->
match Location.unwrap e with
| E_tuple [ a ; b ] -> ok (a , b)
| _ -> fail @@ bad_kind "pair" e.location
let extract_list : expression -> (expression list) result = fun e ->
match Location.unwrap e with
| E_list lst -> ok lst
| _ -> fail @@ bad_kind "list" e.location
let extract_record : expression -> (string * expression) list result = fun e ->
match Location.unwrap e with
| E_record lst -> ok @@ SMap.to_kv_list lst
| _ -> fail @@ bad_kind "record" e.location
let extract_map : expression -> (expression * expression) list result = fun e ->
match Location.unwrap e with
| E_map lst -> ok lst
| _ -> fail @@ bad_kind "map" e.location

View File

@ -42,6 +42,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_nat a, Literal_nat b when a = b -> ok ()
| Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
| Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
| Literal_timestamp a, Literal_timestamp b when a = b -> ok ()
| Literal_timestamp _, Literal_timestamp _ -> fail @@ different_literals "different timestamps" a b
| Literal_timestamp _, _ -> fail @@ different_literals_because_different_types "timestamp vs non-timestamp" a b
| Literal_tez a, Literal_tez b when a = b -> ok ()
| Literal_tez _, Literal_tez _ -> fail @@ different_literals "different tezs" a b
| Literal_tez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
@ -59,7 +62,6 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
| Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b
let rec assert_value_eq (a, b: (expression * expression )) : unit result =
let error_content () =
Format.asprintf "\n@[<v>- %a@;- %a]" PP.expression a PP.expression b
@ -143,6 +145,19 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
)
| E_list _, _ ->
simple_fail "comparing list with other stuff"
| E_set lsta, E_set lstb -> (
let lsta' = List.sort (compare) lsta in
let lstb' = List.sort (compare) lstb in
let%bind lst =
generic_try (simple_error "set of different lengths")
(fun () -> List.combine lsta' lstb') in
let%bind _all = bind_map_list assert_value_eq lst in
ok ()
)
| E_set _, _ ->
simple_fail "comparing set with other stuff"
| (E_annotation (a , _) , _b') -> assert_value_eq (a , b)
| (_a' , E_annotation (b , _)) -> assert_value_eq (a , b)
| (E_variable _, _) | (E_lambda _, _)
@ -151,6 +166,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
| (E_look_up _, _) | (E_matching _, _) | (E_failwith _, _) | (E_sequence _, _)
| (E_loop _, _) | (E_assign _, _) | (E_skip, _) -> simple_fail "comparing not a value"
let is_value_eq (a , b) = to_bool @@ assert_value_eq (a , b)
(* module Rename = struct
* open Trace

View File

@ -60,6 +60,7 @@ and expression' =
(* Data Structures *)
| E_map of (expr * expr) list
| E_list of expr list
| E_set of expr list
| E_look_up of (expr * expr)
(* Matching *)
| E_matching of (expr * matching_expr)
@ -90,6 +91,7 @@ and literal =
| Literal_string of string
| Literal_bytes of bytes
| Literal_address of string
| Literal_timestamp of int
| Literal_operation of Memory_proto_alpha.Alpha_context.packed_internal_operation
and 'a matching =

View File

@ -43,6 +43,7 @@ and expression ppf (e:expression) : unit =
| 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_set m -> fprintf ppf "set[@; @[<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
@ -68,6 +69,7 @@ and literal ppf (l:literal) : unit =
| Literal_bool b -> fprintf ppf "%b" b
| Literal_int n -> fprintf ppf "%d" n
| Literal_nat n -> fprintf ppf "+%d" n
| Literal_timestamp n -> fprintf ppf "+%d" n
| Literal_tez n -> fprintf ppf "%dtz" n
| Literal_string s -> fprintf ppf "%s" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b

View File

@ -15,6 +15,8 @@ let make_n_t type_name type_value = { type_name ; type_value }
let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
let t_string ?s () : type_value = make_t (T_constant ("string", [])) s
let t_bytes ?s () : type_value = make_t (T_constant ("bytes", [])) s
let t_key ?s () : type_value = make_t (T_constant ("key", [])) s
let t_key_hash ?s () : type_value = make_t (T_constant ("key_hash", [])) s
let t_int ?s () : type_value = make_t (T_constant ("int", [])) s
let t_address ?s () : type_value = make_t (T_constant ("address", [])) s
let t_operation ?s () : type_value = make_t (T_constant ("operation", [])) s
@ -25,6 +27,7 @@ let t_unit ?s () : type_value = make_t (T_constant ("unit", [])) s
let t_option o ?s () : type_value = make_t (T_constant ("option", [o])) s
let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s
let t_list t ?s () : type_value = make_t (T_constant ("list", [t])) s
let t_set t ?s () : type_value = make_t (T_constant ("set", [t])) s
let t_contract t ?s () : type_value = make_t (T_constant ("contract", [t])) s
let t_pair a b ?s () = t_tuple [a ; b] ?s ()
@ -93,6 +96,22 @@ let get_t_list (t:type_value) : type_value result = match t.type_value' with
| T_constant ("list", [o]) -> ok o
| _ -> simple_fail "not a list"
let get_t_set (t:type_value) : type_value result = match t.type_value' with
| T_constant ("set", [o]) -> ok o
| _ -> simple_fail "not a set"
let get_t_key (t:type_value) : unit result = match t.type_value' with
| T_constant ("key", []) -> ok ()
| _ -> simple_fail "not a key"
let get_t_signature (t:type_value) : unit result = match t.type_value' with
| T_constant ("signature", []) -> ok ()
| _ -> simple_fail "not a signature"
let get_t_key_hash (t:type_value) : unit result = match t.type_value' with
| T_constant ("key_hash", []) -> ok ()
| _ -> simple_fail "not a key_hash"
let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
| T_tuple lst -> ok lst
| _ -> simple_fail "not a tuple"
@ -137,6 +156,9 @@ let assert_t_map = fun t ->
let is_t_map = Function.compose to_bool get_t_map
let assert_t_tez : type_value -> unit result = get_t_tez
let assert_t_key = get_t_key
let assert_t_signature = get_t_signature
let assert_t_key_hash = get_t_key_hash
let assert_t_list t =
let%bind _ = get_t_list t in

View File

@ -155,6 +155,7 @@ module Free_variables = struct
| E_record_accessor (a, _) -> self a
| E_tuple_accessor (a, _) -> self a
| E_list lst -> unions @@ List.map self lst
| E_set lst -> unions @@ List.map self lst
| E_map m -> unions @@ List.map self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m
| E_look_up (a , b) -> unions @@ List.map self [ a ; b ]
| E_matching (a , cs) -> union (self a) (matching_expression b cs)
@ -344,6 +345,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_nat a, Literal_nat b when a = b -> ok ()
| Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
| Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
| Literal_timestamp a, Literal_timestamp b when a = b -> ok ()
| Literal_timestamp _, Literal_timestamp _ -> fail @@ different_literals "different timestamps" a b
| Literal_timestamp _, _ -> fail @@ different_literals_because_different_types "timestamp vs non-timestamp" a b
| Literal_tez a, Literal_tez b when a = b -> ok ()
| Literal_tez _, Literal_tez _ -> fail @@ different_literals "different tezs" a b
| Literal_tez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
@ -443,6 +447,15 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
)
| E_list _, _ ->
fail @@ different_values_because_different_types "list vs. non-list" a b
| E_set lsta, E_set lstb -> (
let%bind lst =
generic_try (different_size_values "sets of different lengths" a b)
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_map_list assert_value_eq lst in
ok ()
)
| E_set _, _ ->
fail @@ different_values_because_different_types "set vs. non-set" a b
| (E_literal _, _) | (E_variable _, _) | (E_application _, _)
| (E_lambda _, _) | (E_let_in _, _) | (E_tuple_accessor _, _)
| (E_record_accessor _, _)

View File

@ -77,6 +77,9 @@ module Captured_variables = struct
| E_list lst ->
let%bind lst' = bind_map_list self lst in
ok @@ unions lst'
| E_set lst ->
let%bind lst' = bind_map_list self lst in
ok @@ unions lst'
| E_map m ->
let%bind lst' = bind_map_list self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m in
ok @@ unions lst'

View File

@ -100,6 +100,7 @@ and expression =
(* Data Structures *)
| E_map of (ae * ae) list
| E_list of ae list
| E_set of ae list
| E_look_up of (ae * ae)
(* Advanced *)
| E_matching of (ae * matching_expr)
@ -116,6 +117,7 @@ and literal =
| Literal_bool of bool
| Literal_int of int
| Literal_nat of int
| Literal_timestamp of int
| Literal_tez of int
| Literal_string of string
| Literal_bytes of bytes

View File

@ -16,6 +16,16 @@ let get_predicate : string -> type_value -> expression list -> predicate result
| Some x -> ok x
| None -> (
match s with
| "NONE" -> (
let%bind ty' = Mini_c.get_t_option ty in
let%bind m_ty = Compiler_type.type_ ty' in
ok @@ simple_unary @@ prim ~children:[m_ty] I_NONE
)
| "UNPACK" -> (
let%bind ty' = Mini_c.get_t_option ty in
let%bind m_ty = Compiler_type.type_ ty' in
ok @@ simple_unary @@ prim ~children:[m_ty] I_UNPACK
)
| "MAP_REMOVE" ->
let%bind v = match lst with
| [ _ ; expr ] ->
@ -52,6 +62,7 @@ let rec translate_value (v:value) : michelson result = match v with
| D_bool b -> ok @@ prim (if b then D_True else D_False)
| D_int n -> ok @@ int (Z.of_int n)
| D_nat n -> ok @@ int (Z.of_int n)
| D_timestamp n -> ok @@ int (Z.of_int n)
| D_tez n -> ok @@ int (Z.of_int n)
| D_string s -> ok @@ string s
| D_bytes s -> ok @@ bytes (Tezos_stdlib.MBytes.of_bytes s)
@ -75,6 +86,9 @@ let rec translate_value (v:value) : michelson result = match v with
| D_list lst ->
let%bind lst' = bind_map_list translate_value lst in
ok @@ seq lst'
| D_set lst ->
let%bind lst' = bind_map_list translate_value lst in
ok @@ seq lst'
| D_operation _ ->
simple_fail "can't compile an operation"
@ -216,14 +230,6 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
i_drop ;
b' ;
]
(* | E_sequence_drop (a , b) ->
* let%bind (a' , env_a) = translate_expression a env in
* let%bind (b' , env_b) = translate_expression b env_a in
* return ~end_env:env_b @@ seq [
* a' ;
* i_drop ;
* b' ;
* ] *)
| E_constant(str, lst) ->
let module L = Logger.Stateful() in
let%bind lst' =
@ -269,6 +275,9 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
| E_make_empty_list t ->
let%bind t' = Compiler_type.type_ t in
return @@ i_nil t'
| E_make_empty_set t ->
let%bind t' = Compiler_type.type_ t in
return @@ i_empty_set t'
| E_make_none o ->
let%bind o' = Compiler_type.type_ o in
return @@ i_none o'

View File

@ -35,6 +35,7 @@ module Ty = struct
| T_pair _ -> fail (not_comparable "pair")
| T_map _ -> fail (not_comparable "map")
| T_list _ -> fail (not_comparable "list")
| T_set _ -> fail (not_comparable "set")
| T_option _ -> fail (not_comparable "option")
| T_contract _ -> fail (not_comparable "contract")
@ -82,6 +83,10 @@ module Ty = struct
| T_list t ->
let%bind (Ex_ty t') = type_ t in
ok @@ Ex_ty Contract_types.(list t')
| T_set t -> (
let%bind (Ex_comparable_ty t') = comparable_type t in
ok @@ Ex_ty Contract_types.(set t')
)
| T_option t ->
let%bind (Ex_ty t') = type_ t in
ok @@ Ex_ty Contract_types.(option t')
@ -142,6 +147,9 @@ let rec type_ : type_value -> O.michelson result =
| T_list t ->
let%bind t' = type_ t in
ok @@ O.prim ~children:[t'] O.T_list
| T_set t ->
let%bind t' = type_ t in
ok @@ O.prim ~children:[t'] O.T_set
| T_option o ->
let%bind o' = type_ o in
ok @@ O.prim ~children:[o'] O.T_option

View File

@ -29,6 +29,11 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
trace_option (simple_error "too big to fit an int") @@
Alpha_context.Script_int.to_int n in
ok @@ D_nat n
| (Timestamp_t _), n ->
let n =
Z.to_int @@
Alpha_context.Script_timestamp.to_zint n in
ok @@ D_timestamp n
| (Mutez_t _), n ->
let%bind n =
generic_try (simple_error "too big to fit an int") @@
@ -72,6 +77,18 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
bind_map_list aux lst'
in
ok @@ D_list lst''
| (Set_t (ty, _)), (module S) -> (
let lst = S.OPS.elements S.boxed in
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_of_comparable_ty ty, t)) in
bind_map_list aux lst'
in
ok @@ D_set lst''
)
| (Operation_t _) , op ->
ok @@ D_operation op
| ty, v ->

View File

@ -0,0 +1,10 @@
type action =
| Increment of int
| Decrement of int
let main (p : action) (s : int) : (operation list * int) =
let storage =
match p with
| Increment n -> s + n
| Decrement n -> s - n in
(([] : operation list) , storage)

55
src/contracts/vote.mligo Normal file
View File

@ -0,0 +1,55 @@
type storage = {
title : string ;
candidates : (string , int) map ;
voters : address set ;
beginning_time : timestamp ;
finish_time : timestamp ;
}
type init_action = {
title : string ;
beginning_time : timestamp ;
finish_time : timestamp ;
}
type action =
| Vote of string
| Init of init_action
let init (init_params : init_action) (_ : storage) =
let candidates = Map [
("Yes" , 0) ;
("No" , 0)
] in
(
([] : operation list),
{
title = init_params.title ;
candidates = candidates ;
voters = (Set [] : address set) ;
beginning_time = init_params.beginning_time ;
finish_time = init_params.finish_time ;
}
)
let vote (parameter : string) (storage : storage) =
let now = Current.time in
(* let _ = assert (now >= storage.beginning_time && storage.finish_time > now) in *)
let addr = Current.source in
(* let _ = assert (not Set.mem addr storage.voters) in *)
let x = Map.find parameter storage.candidates in
(
([] : operation list),
{
title = storage.title ;
candidates = Map.update parameter (Some (x + 1)) storage.candidates ;
voters = Set.add addr storage.voters ;
beginning_time = storage.beginning_time ;
finish_time = storage.finish_time ;
}
)
let main (action : action) (storage : storage) =
match action with
| Vote p -> vote p storage
| Init ps -> init ps storage

View File

@ -267,6 +267,7 @@ module Types = struct
let key = Key_t None
let list a = List_t (a, None)
let set a = Set_t (a, None)
let assert_list = function
| List_t (a, _) -> a
| _ -> assert false

View File

@ -27,6 +27,7 @@ let rec type_ ppf : type_value -> _ = function
| 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_set(t) -> fprintf ppf "set(%a)" type_ t
| T_option(o) -> fprintf ppf "option(%a)" type_ o
| T_contract(t) -> fprintf ppf "contract(%a)" type_ t
| T_deep_closure(c, arg, ret) ->
@ -45,6 +46,7 @@ let rec value ppf : value -> unit = function
| D_operation _ -> fprintf ppf "operation[...bytes]"
| D_int n -> fprintf ppf "%d" n
| D_nat n -> fprintf ppf "+%d" n
| D_timestamp n -> fprintf ppf "+%d" n
| D_tez n -> fprintf ppf "%dtz" n
| D_unit -> fprintf ppf " "
| D_string s -> fprintf ppf "\"%s\"" s
@ -57,6 +59,7 @@ let rec value ppf : value -> unit = function
| 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
| D_set lst -> fprintf ppf "Set[%a]" (list_sep_d value) lst
and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" value a value b
@ -73,6 +76,7 @@ and expression' ppf (e:expression') = match e with
| E_literal v -> fprintf ppf "%a" value v
| E_make_empty_map _ -> fprintf ppf "map[]"
| E_make_empty_list _ -> fprintf ppf "list[]"
| E_make_empty_set _ -> fprintf ppf "set[]"
| E_make_none _ -> fprintf ppf "none"
| E_if_bool (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b
| E_if_none (c, n, ((name, _) , s)) -> fprintf ppf "%a ?? %a : %s -> %a" expression c expression n name expression s

View File

@ -37,6 +37,10 @@ let get_nat (v:value) = match v with
| D_nat n -> ok n
| _ -> simple_fail "not a nat"
let get_timestamp (v:value) = match v with
| D_timestamp n -> ok n
| _ -> simple_fail "not a timestamp"
let get_string (v:value) = match v with
| D_string s -> ok s
| _ -> simple_fail "not a string"
@ -62,6 +66,10 @@ let get_list (v:value) = match v with
| D_list lst -> ok lst
| _ -> simple_fail "not a list"
let get_set (v:value) = match v with
| D_set lst -> ok lst
| _ -> simple_fail "not a set"
let get_t_option (v:type_value) = match v with
| T_option t -> ok t
| _ -> simple_fail "not an option"
@ -82,6 +90,10 @@ let get_t_list (t:type_value) = match t with
| T_list t -> ok t
| _ -> simple_fail "not a type list"
let get_t_set (t:type_value) = match t with
| T_set t -> ok t
| _ -> simple_fail "not a type set"
let get_left (v:value) = match v with
| D_left b -> ok b
| _ -> simple_fail "not a left"

View File

@ -16,6 +16,7 @@ type type_value =
| T_base of type_base
| T_map of (type_value * type_value)
| T_list of type_value
| T_set of type_value
| T_contract of type_value
| T_option of type_value
@ -35,6 +36,7 @@ type value =
| D_unit
| D_bool of bool
| D_nat of int
| D_timestamp of int
| D_tez of int
| D_int of int
| D_string of string
@ -46,6 +48,7 @@ type value =
| D_none
| D_map of (value * value) list
| D_list of value list
| D_set of value list
(* | `Macro of anon_macro ... The future. *)
| D_function of anon_function
| D_operation of Memory_proto_alpha.Alpha_context.packed_internal_operation
@ -64,6 +67,7 @@ and expression' =
| E_variable of var_name
| E_make_empty_map of (type_value * type_value)
| E_make_empty_list of type_value
| E_make_empty_set of type_value
| E_make_none of type_value
| E_if_bool of expression * expression * expression
| E_if_none of expression * expression * ((var_name * type_value) * expression)

View File

@ -88,6 +88,7 @@ module Typer = struct
t_string () ;
t_bytes () ;
t_address () ;
t_timestamp () ;
] in
ok @@ t_bool ()

View File

@ -42,6 +42,9 @@ module Simplify = struct
("bool" , "bool") ;
("operation" , "operation") ;
("address" , "address") ;
("key" , "key") ;
("key_hash" , "key_hash") ;
("signature" , "signature") ;
("timestamp" , "timestamp") ;
("contract" , "contract") ;
("list" , "list") ;
@ -76,7 +79,7 @@ module Simplify = struct
("Bytes.pack" , "PACK") ;
("Crypto.hash" , "HASH") ;
("Operation.transaction" , "CALL") ;
("Operation.get_contract" , "GET_CONTRACT") ;
("Operation.get_contract" , "CONTRACT") ;
("sender" , "SENDER") ;
("unit" , "UNIT") ;
("source" , "SOURCE") ;
@ -87,6 +90,8 @@ module Simplify = struct
module Ligodity = struct
let constants = [
("assert" , "ASSERT") ;
("Current.balance", "BALANCE") ;
("balance", "BALANCE") ;
("Current.time", "NOW") ;
@ -97,6 +102,8 @@ module Simplify = struct
("gas", "STEPS_TO_QUOTA") ;
("Current.sender" , "SENDER") ;
("sender", "SENDER") ;
("Current.source" , "SOURCE") ;
("source", "SOURCE") ;
("Current.failwith", "FAILWITH") ;
("failwith" , "FAILWITH") ;
@ -115,6 +122,17 @@ module Simplify = struct
("Bytes.slice", "SLICE") ;
("Bytes.sub", "SLICE") ;
("Set.mem" , "SET_MEM") ;
("Set.empty" , "SET_EMPTY") ;
("Set.add" , "SET_ADD") ;
("Set.remove" , "SET_REMOVE") ;
("Map.find_opt" , "MAP_FIND_OPT") ;
("Map.find" , "MAP_FIND") ;
("Map.update" , "MAP_UPDATE") ;
("Map.add" , "MAP_ADD") ;
("Map.remove" , "MAP_REMOVE") ;
("String.length", "SIZE") ;
("String.size", "SIZE") ;
("String.slice", "SLICE") ;
@ -126,7 +144,7 @@ module Simplify = struct
("List.iter", "ITER") ;
("Operation.transaction" , "CALL") ;
("Operation.get_contract" , "GET_CONTRACT") ;
("Operation.get_contract" , "CONTRACT") ;
("int" , "INT") ;
("abs" , "ABS") ;
("unit" , "UNIT") ;
@ -195,7 +213,7 @@ module Typer = struct
let%bind () = assert_type_value_eq (dst, v) in
ok m
let map_update : typer = typer_3 "MAP_UPDATE_TODO" @@ fun k v m ->
let map_update : typer = typer_3 "MAP_UPDATE" @@ fun k v m ->
let%bind (src, dst) = get_t_map m in
let%bind () = assert_type_value_eq (src, k) in
let%bind v' = get_t_option v in
@ -207,7 +225,12 @@ module Typer = struct
let%bind () = assert_type_value_eq (src, k) in
ok @@ t_bool ()
let map_find : typer = typer_2 "MAP_FIND_TODO" @@ fun k m ->
let map_find : typer = typer_2 "MAP_FIND" @@ fun k m ->
let%bind (src, dst) = get_t_map m in
let%bind () = assert_type_value_eq (src, k) in
ok @@ dst
let map_find_opt : typer = typer_2 "MAP_FIND_OPT" @@ fun k m ->
let%bind (src, dst) = get_t_map m in
let%bind () = assert_type_value_eq (src, k) in
ok @@ t_option dst ()
@ -243,9 +266,15 @@ module Typer = struct
let size = typer_1 "SIZE" @@ fun t ->
let%bind () =
Assert.assert_true @@
(is_t_map t || is_t_list t) in
(is_t_map t || is_t_list t || is_t_string t) in
ok @@ t_nat ()
let slice = typer_3 "SLICE" @@ fun i j s ->
let%bind () =
Assert.assert_true @@
(is_t_nat i && is_t_nat j && is_t_string s) in
ok @@ t_string ()
let failwith_ = typer_1 "FAILWITH" @@ fun t ->
let%bind () =
Assert.assert_true @@
@ -269,10 +298,28 @@ module Typer = struct
trace_option (simple_error "untyped UNPACK") @@
output_opt
let crypto_hash = typer_1 "HASH" @@ fun t ->
let hash256 = typer_1 "SHA256" @@ fun t ->
let%bind () = assert_t_bytes t in
ok @@ t_bytes ()
let hash512 = typer_1 "SHA512" @@ fun t ->
let%bind () = assert_t_bytes t in
ok @@ t_bytes ()
let blake2b = typer_1 "BLAKE2b" @@ fun t ->
let%bind () = assert_t_bytes t in
ok @@ t_bytes ()
let hash_key = typer_1 "HASH_KEY" @@ fun t ->
let%bind () = assert_t_key t in
ok @@ t_key_hash ()
let check_signature = typer_3 "CHECK_SIGNATURE" @@ fun k s b ->
let%bind () = assert_t_key k in
let%bind () = assert_t_signature s in
let%bind () = assert_t_bytes b in
ok @@ t_bool ()
let sender = constant "SENDER" @@ t_address ()
let source = constant "SOURCE" @@ t_address ()
@ -281,6 +328,8 @@ module Typer = struct
let amount = constant "AMOUNT" @@ t_tez ()
let address = constant "ADDRESS" @@ t_address ()
let now = constant "NOW" @@ t_timestamp ()
let transaction = typer_3 "CALL" @@ fun param amount contract ->
@ -301,6 +350,11 @@ module Typer = struct
let%bind () = assert_t_int t in
ok @@ t_nat ()
let assertion = typer_1 "ASSERT" @@ fun a ->
if eq_1 a (t_bool ())
then ok @@ t_unit ()
else simple_fail "Asserting a non-bool"
let times = typer_2 "TIMES" @@ fun a b ->
if eq_2 (a , b) (t_nat ())
then ok @@ t_nat () else
@ -335,6 +389,29 @@ module Typer = struct
then ok @@ t_int () else
simple_fail "Adding with wrong types. Expected nat, int or tez."
let set_mem = typer_2 "SET_MEM" @@ fun elt set ->
let%bind key = get_t_set set in
if eq_1 elt key
then ok @@ t_bool ()
else simple_fail "Set_mem: elt and set don't match"
let set_add = typer_2 "SET_ADD" @@ fun elt set ->
let%bind key = get_t_set set in
if eq_1 elt key
then ok set
else simple_fail "Set_add: elt and set don't match"
let set_remove = typer_2 "SET_REMOVE" @@ fun elt set ->
let%bind key = get_t_set set in
if eq_1 elt key
then ok set
else simple_fail "Set_remove: elt and set don't match"
let not_ = typer_1 "NOT" @@ fun elt ->
if eq_1 elt (t_bool ())
then ok @@ t_bool ()
else simple_fail "bad parameter to not"
let constant_typers = Map.String.of_list [
add ;
times ;
@ -351,6 +428,7 @@ module Typer = struct
comparator "GE" ;
boolean_operator_2 "OR" ;
boolean_operator_2 "AND" ;
not_ ;
map_remove ;
map_add ;
map_update ;
@ -360,6 +438,9 @@ module Typer = struct
map_map ;
map_fold ;
map_iter ;
set_mem ;
set_add ;
set_remove ;
(* map_size ; (* use size *) *)
int ;
size ;
@ -367,7 +448,11 @@ module Typer = struct
get_force ;
bytes_pack ;
bytes_unpack ;
crypto_hash ;
hash256 ;
hash512 ;
blake2b ;
hash_key ;
check_signature ;
sender ;
source ;
unit ;
@ -376,6 +461,9 @@ module Typer = struct
get_contract ;
abs ;
now ;
slice ;
address ;
assertion ;
]
end
@ -407,6 +495,8 @@ module Compiler = struct
("NEG" , simple_unary @@ prim I_NEG) ;
("OR" , simple_binary @@ prim I_OR) ;
("AND" , simple_binary @@ prim I_AND) ;
("XOR" , simple_binary @@ prim I_XOR) ;
("NOT" , simple_unary @@ prim I_NOT) ;
("PAIR" , simple_binary @@ prim I_PAIR) ;
("CAR" , simple_unary @@ prim I_CAR) ;
("CDR" , simple_unary @@ prim I_CDR) ;
@ -419,21 +509,35 @@ module Compiler = struct
("UPDATE" , simple_ternary @@ prim I_UPDATE) ;
("SOME" , simple_unary @@ prim I_SOME) ;
("MAP_GET_FORCE" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "GET_FORCE")]) ;
("MAP_FIND" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "MAP FIND")]) ;
("MAP_GET" , simple_binary @@ prim I_GET) ;
("SIZE" , simple_unary @@ prim I_SIZE) ;
("FAILWITH" , simple_unary @@ prim I_FAILWITH) ;
("ASSERT" , simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit])) ;
("ASSERT_INFERRED" , simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit])) ;
("ASSERT" , simple_unary @@ i_if (seq [i_push_unit ; i_failwith]) (seq [i_push_unit])) ;
("INT" , simple_unary @@ prim I_INT) ;
("ABS" , simple_unary @@ prim I_ABS) ;
("CONS" , simple_binary @@ prim I_CONS) ;
("UNIT" , simple_constant @@ prim I_UNIT) ;
("AMOUNT" , simple_constant @@ prim I_AMOUNT) ;
("ADDRESS" , simple_constant @@ prim I_ADDRESS) ;
("NOW" , simple_constant @@ prim I_NOW) ;
("CALL" , simple_ternary @@ prim I_TRANSFER_TOKENS) ;
("SOURCE" , simple_constant @@ prim I_SOURCE) ;
("SENDER" , simple_constant @@ prim I_SENDER) ;
("MAP_ADD" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]) ;
("MAP_UPDATE" , simple_ternary @@ prim I_UPDATE) ;
("SET_MEM" , simple_binary @@ prim I_MEM) ;
("SET_ADD" , simple_binary @@ seq [dip (i_push (prim T_bool) (prim D_True)) ; prim I_UPDATE]) ;
("SLICE" , simple_ternary @@ prim I_SLICE) ;
("SHA256" , simple_unary @@ prim I_SHA256) ;
("SHA512" , simple_unary @@ prim I_SHA512) ;
("BLAKE2B" , simple_unary @@ prim I_BLAKE2B) ;
("CHECK_SIGNATURE" , simple_ternary @@ prim I_CHECK_SIGNATURE) ;
("HASH_KEY" , simple_unary @@ prim I_HASH_KEY) ;
("PACK" , simple_unary @@ prim I_PACK) ;
]
(* Some complex predicates will need to be added in compiler/compiler_program *)
end

View File

@ -34,6 +34,19 @@ let parse_file (source: string) : AST.t result =
in
simple_error str
)
| Lexer.Error err -> (
let start = Lexing.lexeme_start_p lexbuf in
let end_ = Lexing.lexeme_end_p lexbuf in
let str = Format.sprintf
"Lexer error (%s) at \"%s\" from (%d, %d) to (%d, %d). In file \"%s|%s\"\n"
(err.value)
(Lexing.lexeme lexbuf)
start.pos_lnum (start.pos_cnum - start.pos_bol)
end_.pos_lnum (end_.pos_cnum - end_.pos_bol)
start.pos_fname source
in
simple_error str
)
| exn ->
let start = Lexing.lexeme_start_p lexbuf in
let end_ = Lexing.lexeme_end_p lexbuf in

View File

@ -147,6 +147,22 @@ module Errors = struct
] in
error ~data title message
let bad_set_definition =
let title () = "bad set definition" in
let message () = "a set definition is a list" in
info title message
let bad_list_definition =
let title () = "bad list definition" in
let message () = "a list definition is a list" in
info title message
let bad_map_definition =
let title () = "bad map definition" in
let message () = "a map definition is a list of pairs" in
info title message
let corner_case ~loc message =
let title () = "corner case" in
let content () = "We don't have a good error message for this case. \
@ -158,6 +174,7 @@ module Errors = struct
("message" , fun () -> message) ;
] in
error ~data title content
end
open Errors
@ -170,6 +187,7 @@ let rec pattern_to_var : Raw.pattern -> _ = fun p ->
match p with
| Raw.PPar p -> pattern_to_var p.value.inside
| Raw.PVar v -> ok v
| Raw.PWild r -> ok @@ ({ region = r ; value = "_" } : Raw.variable)
| _ -> fail @@ wrong_pattern "var" p
let rec pattern_to_typed_var : Raw.pattern -> _ = fun p ->
@ -181,6 +199,7 @@ let rec pattern_to_typed_var : Raw.pattern -> _ = fun p ->
ok (v , Some tp.type_expr)
)
| Raw.PVar v -> ok (v , None)
| Raw.PWild r -> ok (({ region = r ; value = "_" } : Raw.variable) , None)
| _ -> fail @@ wrong_pattern "typed variable" p
let rec expr_to_typed_expr : Raw.expr -> _ = fun e ->
@ -358,11 +377,38 @@ let rec simpl_expression :
let (c_name , _c_loc) = r_split c_name in
let args =
match args with
None -> []
| None -> []
| Some arg -> [arg] in
let%bind arg = simpl_tuple_expression @@ args in
match c_name with
| "Set" -> (
let%bind args' =
trace bad_set_definition @@
extract_list arg in
return @@ e_set ~loc args'
)
| "List" -> (
let%bind args' =
trace bad_list_definition @@
extract_list arg in
return @@ e_list ~loc args'
)
| "Map" -> (
let%bind args' =
trace bad_map_definition @@
extract_list arg in
let%bind pairs =
trace bad_map_definition @@
bind_map_list extract_pair args' in
return @@ e_map ~loc pairs
)
| "Some" -> (
return @@ e_some ~loc arg
)
| _ -> (
return @@ e_constructor ~loc c_name arg
)
)
| EArith (Add c) ->
simpl_binop "ADD" c
| EArith (Sub c) ->

View File

@ -217,7 +217,7 @@ let sell () =
let expected_storage =
let cards = List.hds @@ cards_ez first_owner n in
basic 99 1000 cards (2 * n) in
Ast_simplified.assert_value_eq (expected_storage , storage)
Ast_simplified.Misc.assert_value_eq (expected_storage , storage)
in
let%bind () =
let amount = Memory_proto_alpha.Alpha_context.Tez.zero in

View File

@ -429,6 +429,16 @@ let super_counter_contract () : unit result =
e_pair (e_typed_list [] t_operation) (e_int (op 42 n)) in
expect_eq_n program "main" make_input make_expected
let super_counter_contract_mligo () : unit result =
let%bind program = mtype_file "./contracts/super-counter.mligo" in
let make_input = fun n ->
let action = if n mod 2 = 0 then "Increment" else "Decrement" in
e_pair (e_constructor action (e_int n)) (e_int 42) in
let make_expected = fun n ->
let op = if n mod 2 = 0 then (+) else (-) in
e_pair (e_typed_list [] t_operation) (e_int (op 42 n)) in
expect_eq_n program "main" make_input make_expected
let dispatch_counter_contract () : unit result =
let%bind program = type_file "./contracts/dispatch-counter.ligo" in
let make_input = fun n ->
@ -566,6 +576,7 @@ let main = test_suite "Integration (End to End)" [
test "#include directives" include_ ;
test "counter contract" counter_contract ;
test "super counter contract" super_counter_contract ;
test "super counter contract" super_counter_contract_mligo ;
test "dispatch counter contract" dispatch_counter_contract ;
test "closure" closure ;
test "shared function" shared_function ;

View File

@ -51,6 +51,7 @@ let () =
Typer_tests.main ;
Heap_tests.main ;
Coase_tests.main ;
Vote_tests.main ;
Bin_tests.main ;
] ;
()

View File

@ -5,7 +5,7 @@ type test =
| Test_suite of (string * test list)
| Test of test_case
let error_pp out (e : error) =
let rec error_pp out (e : error) =
let open JSON_string_utils in
let message =
let opt = e |> member "message" |> string in
@ -30,6 +30,7 @@ let error_pp out (e : error) =
let infos = e |> member "infos" in
match infos with
| `Null -> ""
| `List lst -> Format.asprintf "@[<v2>%a@]" PP_helpers.(list_sep error_pp (tag "@,")) lst
| _ -> " " ^ (J.to_string infos) ^ "\n" in
Format.fprintf out "%s%s%s.\n%s%s" title error_code message data infos
@ -70,7 +71,7 @@ let expect_eq ?options program entry_point input expected =
Ast_simplified.PP.expression result in
error title content in
trace expect_error @@
Ast_simplified.assert_value_eq (expected , result) in
Ast_simplified.Misc.assert_value_eq (expected , result) in
expect ?options program entry_point input expecter
let expect_evaluate program entry_point expecter =
@ -84,7 +85,7 @@ let expect_evaluate program entry_point expecter =
let expect_eq_evaluate program entry_point expected =
let expecter = fun result ->
Ast_simplified.assert_value_eq (expected , result) in
Ast_simplified.Misc.assert_value_eq (expected , result) in
expect_evaluate program entry_point expecter
let expect_n_aux ?options lst program entry_point make_input make_expecter =

55
src/test/vote_tests.ml Normal file
View File

@ -0,0 +1,55 @@
open Trace
open Ligo.Run
open Test_helpers
let get_program =
let s = ref None in
fun () -> match !s with
| Some s -> ok s
| None -> (
let%bind program = type_file "cameligo" "./contracts/vote.mligo" in
s := Some program ;
ok program
)
open Ast_simplified
let init_storage name = ez_e_record [
("title" , e_string name) ;
("candidates" , e_map [
(e_string "Yes" , e_int 0) ;
(e_string "No" , e_int 0) ;
]) ;
("voters" , e_typed_set [] t_address) ;
("beginning_time" , e_timestamp 0) ;
("finish_time" , e_timestamp 1000000000) ;
]
let init title beginning_time finish_time =
let init_action = ez_e_record [
("title" , e_string title) ;
("beginning_time" , e_timestamp beginning_time) ;
("finish_time" , e_timestamp finish_time) ;
] in
e_constructor "Init" init_action
let vote str =
let vote = e_string str in
e_constructor "Vote" vote
let init_vote () =
let%bind program = get_program () in
let%bind result = Ligo.Run.run_simplityped program "main" (e_pair (vote "Yes") (init_storage "basic")) in
let%bind (_ , storage) = extract_pair result in
let%bind storage' = extract_record storage in
let votes = List.assoc "candidates" storage' in
let%bind votes' = extract_map votes in
let%bind (_ , yess) =
trace_option (simple_error "") @@
List.find_opt (fun (k , _) -> Ast_simplified.Misc.is_value_eq (k , e_string "Yes")) votes' in
let%bind () = Ast_simplified.Misc.assert_value_eq (yess , e_int 1) in
ok ()
let main = test_suite "Vote" [
test "type" init_vote ;
]

View File

@ -105,6 +105,9 @@ let rec translate_type (t:AST.type_value) : type_value result =
| T_constant ("list", [t]) ->
let%bind t' = translate_type t in
ok (T_list t')
| T_constant ("set", [t]) ->
let%bind t' = translate_type t in
ok (T_set t')
| T_constant ("option", [o]) ->
let%bind o' = translate_type o in
ok (T_option o')
@ -181,6 +184,7 @@ let rec translate_literal : AST.literal -> value = fun l -> match l with
| Literal_bool b -> D_bool b
| Literal_int n -> D_int n
| Literal_nat n -> D_nat n
| Literal_timestamp n -> D_timestamp n
| Literal_tez n -> D_tez n
| Literal_bytes s -> D_bytes s
| Literal_string s -> D_string s
@ -362,6 +366,16 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
let%bind (init : expression) = return @@ E_make_empty_list t in
bind_fold_list aux init lst'
)
| E_set lst -> (
let%bind t =
trace_strong (corner_case ~loc:__LOC__ "not a set") @@
Mini_c.Combinators.get_t_set tv in
let%bind lst' = bind_map_list (translate_annotated_expression) lst in
let aux : expression -> expression -> expression result = fun prev cur ->
return @@ E_constant ("CONS", [cur ; prev]) in
let%bind (init : expression) = return @@ E_make_empty_set t in
bind_fold_list aux init lst'
)
| E_map m -> (
let%bind (src, dst) =
trace_strong (corner_case ~loc:__LOC__ "not a map") @@
@ -663,6 +677,12 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
get_nat v in
return (E_literal (Literal_nat n))
)
| T_constant ("timestamp", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "timestamp" v) @@
get_timestamp v in
return (E_literal (Literal_timestamp n))
)
| T_constant ("tez", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "tez" v) @@
@ -712,6 +732,15 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
bind_map_list aux lst in
return (E_list lst')
)
| T_constant ("set", [ty]) -> (
let%bind lst =
trace_strong (wrong_mini_c_value "set" v) @@
get_set v in
let%bind lst' =
let aux = fun e -> untranspile e ty in
bind_map_list aux lst in
return (E_set lst')
)
| T_constant ("contract" , [_ty]) ->
fail @@ bad_untranspile "contract" v
| T_constant ("operation" , []) -> (

View File

@ -206,11 +206,13 @@ module Errors = struct
] in
error ~data title message ()
let constant_error loc =
let constant_error loc lst tv_opt =
let title () = "typing constant" in
let message () = "" in
let data = [
("location" , fun () -> Format.asprintf "%a" Location.pp loc ) ;
("argument_types" , fun () -> Format.asprintf "%a" PP_helpers.(list_sep Ast_typed.PP.type_value (const " , ")) lst) ;
("type_opt" , fun () -> Format.asprintf "%a" PP_helpers.(option Ast_typed.PP.type_value) tv_opt) ;
] in
error ~data title message
end
@ -416,6 +418,8 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
return (E_literal (Literal_int n)) (t_int ())
| E_literal (Literal_nat n) ->
return (E_literal (Literal_nat n)) (t_nat ())
| E_literal (Literal_timestamp n) ->
return (E_literal (Literal_timestamp n)) (t_timestamp ())
| E_literal (Literal_tez n) ->
return (E_literal (Literal_tez n)) (t_tez ())
| E_literal (Literal_address s) ->
@ -501,6 +505,27 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
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
@@ 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
| E_map lst ->
let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
let%bind tv =
@ -613,7 +638,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
ae.location)
@@ assert_t_unit (get_type_annotation mf') in
let mt' = make_a_e
(E_constant ("ASSERT" , [ex' ; fw']))
(E_constant ("ASSERT_INFERRED" , [ex' ; fw']))
(t_unit ())
e
in
@ -738,7 +763,7 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
let%bind typer =
trace_option (unrecognized_constant name loc) @@
Map.String.find_opt name ct in
trace (constant_error loc) @@
trace (constant_error loc lst tv_opt) @@
typer lst tv_opt
let untype_type_value (t:O.type_value) : (I.type_expression) result =
@ -752,6 +777,7 @@ let untype_literal (l:O.literal) : I.literal result =
| Literal_unit -> ok Literal_unit
| Literal_bool b -> ok (Literal_bool b)
| Literal_nat n -> ok (Literal_nat n)
| Literal_timestamp n -> ok (Literal_timestamp n)
| Literal_tez n -> ok (Literal_tez n)
| Literal_int n -> ok (Literal_int n)
| Literal_string s -> ok (Literal_string s)
@ -803,6 +829,9 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
| 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')
| E_look_up dsi ->
let%bind (a , b) = bind_map_pair untype_expression dsi in
return (e_look_up a b)

View File

@ -47,6 +47,7 @@ let i_push_unit = i_push t_unit d_unit
let i_push_string str = i_push t_string (string str)
let i_none ty = prim ~children:[ty] I_NONE
let i_nil ty = prim ~children:[ty] I_NIL
let i_empty_set ty = prim ~children:[ty] I_EMPTY_SET
let i_some = prim I_SOME
let i_lambda arg ret body = prim ~children:[arg;ret;body] I_LAMBDA
let i_empty_map src dst = prim ~children:[src;dst] I_EMPTY_MAP