add more operators

This commit is contained in:
Galfour 2019-06-10 22:06:00 +00:00
parent 985eff44a9
commit b512bf31bb
11 changed files with 138 additions and 25 deletions

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", [])
@ -145,3 +156,13 @@ 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

View File

@ -6,14 +6,17 @@ type storage = {
finish_time : timestamp ;
}
type init_action = (string * timestamp * timestamp)
type init_action = {
title : string ;
beginning_time : timestamp ;
finish_time : timestamp ;
}
type action =
| Vote of string
| Init of (string * timestamp * timestamp)
| Init of init_action
let init (init_params : init_action) (_ : storage) =
let (title , s , t) = init_params in
let candidates = Map [
("Yes" , 0) ;
("No" , 0)
@ -21,21 +24,19 @@ let init (init_params : init_action) (_ : storage) =
(
([] : operation list),
{
title = title ;
title = init_params.title ;
candidates = candidates ;
voters = (Set [] : address set) ;
beginning_time = s ;
finish_time = t ;
beginning_time = init_params.beginning_time ;
finish_time = init_params.finish_time ;
}
)
let vote (parameter : string) (storage : storage) =
let now = Current.time () in
assert (now >= storage.beginning_time && storage.finish_time < now) ;
let addr = Current.source () in
assert (not Set.mem addr storage.voters) ;
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),
@ -47,7 +48,7 @@ let vote (parameter : string) (storage : storage) =
finish_time = storage.finish_time ;
}
)
)
let main (action : action) (storage : storage) =
match action with
| Vote p -> vote p storage

View File

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

View File

@ -90,6 +90,8 @@ module Simplify = struct
module Ligodity = struct
let constants = [
("assert" , "ASSERT") ;
("Current.balance", "BALANCE") ;
("balance", "BALANCE") ;
("Current.time", "NOW") ;
@ -100,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") ;
@ -209,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
@ -221,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 ()
@ -341,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
@ -375,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 ;
@ -391,6 +428,7 @@ module Typer = struct
comparator "GE" ;
boolean_operator_2 "OR" ;
boolean_operator_2 "AND" ;
not_ ;
map_remove ;
map_add ;
map_update ;
@ -400,6 +438,9 @@ module Typer = struct
map_map ;
map_fold ;
map_iter ;
set_mem ;
set_add ;
set_remove ;
(* map_size ; (* use size *) *)
int ;
size ;
@ -422,6 +463,7 @@ module Typer = struct
now ;
slice ;
address ;
assertion ;
]
end

View File

@ -104,7 +104,7 @@ let keywords = Token.[
"and", None;
"as", None;
"asr", None;
"assert", None;
(* "assert", None; *)
"class", None;
"constraint", None;
"do", None;

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

@ -71,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 =
@ -85,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 =

View File

@ -27,5 +27,5 @@ let init_vote () =
ok ()
let main = test_suite "Vote" [
(* test "type" init_vote ; *)
test "type" init_vote ;
]

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