From 6cb341b1624d0fc32ddaafa0283944e870136420 Mon Sep 17 00:00:00 2001 From: Galfour Date: Mon, 29 Apr 2019 13:30:28 +0000 Subject: [PATCH] extend camligo and ligo --- src/ligo/ast_simplified/PP.ml | 3 +- src/ligo/ast_simplified/combinators.ml | 11 +++ src/ligo/ast_simplified/misc.ml | 3 + src/ligo/ast_simplified/types.ml | 1 + src/ligo/ast_typed/PP.ml | 3 +- src/ligo/ast_typed/combinators.ml | 28 ++++++++ src/ligo/ast_typed/misc.ml | 3 + src/ligo/ast_typed/types.ml | 1 + src/ligo/compiler/compiler_program.ml | 1 + src/ligo/contracts/counter.mligo | 4 ++ src/ligo/contracts/new-syntax.mligo | 3 +- src/ligo/mini_c/PP.ml | 3 +- src/ligo/mini_c/types.ml | 1 + src/ligo/operators/operators.ml | 92 ++++++++++++++++++++++-- src/ligo/parser/camligo/lex/generator.ml | 6 +- src/ligo/simplify/camligo.ml | 60 +++++++++------- src/ligo/test/integration_tests.ml | 26 +++++++ src/ligo/test/multifix_tests.ml | 8 --- src/ligo/transpiler/transpiler.ml | 1 + src/ligo/typer/typer.ml | 74 +++++++++++++------ 20 files changed, 269 insertions(+), 63 deletions(-) create mode 100644 src/ligo/contracts/counter.mligo diff --git a/src/ligo/ast_simplified/PP.ml b/src/ligo/ast_simplified/PP.ml index 7cf55c5fc..36e339209 100644 --- a/src/ligo/ast_simplified/PP.ml +++ b/src/ligo/ast_simplified/PP.ml @@ -17,7 +17,8 @@ let literal ppf (l:literal) = match l with | Literal_unit -> fprintf ppf "Unit" | Literal_bool b -> fprintf ppf "%b" b | Literal_int n -> fprintf ppf "%d" n - | Literal_nat n -> fprintf ppf "%d" n + | Literal_nat 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 diff --git a/src/ligo/ast_simplified/combinators.ml b/src/ligo/ast_simplified/combinators.ml index cea1d6905..c8a1257b3 100644 --- a/src/ligo/ast_simplified/combinators.ml +++ b/src/ligo/ast_simplified/combinators.ml @@ -77,6 +77,7 @@ let e_match_bool a b c : expression = e_match a (Match_bool {match_true = b ; ma let e_accessor a b = E_accessor (a , b) let e_accessor_props a b = e_accessor a (List.map (fun x -> Access_record x) b) let e_variable v = E_variable v +let e_failwith v = E_failwith v let e_a_unit : annotated_expression = make_e_a_full (e_unit ()) t_unit let e_a_int n : annotated_expression = make_e_a_full (e_int n) t_int @@ -152,3 +153,13 @@ let ez_e_record (lst : (string * expression) list) : expression = (* TODO: define a correct implementation of List.map * (an implementation that does not fail with stack overflow) *) e_record (List.map (fun (s,e) -> (s, make_e_a e)) lst) + + +let get_a_accessor = fun t -> + match t.expression with + | E_accessor (a , b) -> ok (a , b) + | _ -> simple_fail "not an accessor" + +let assert_a_accessor = fun t -> + let%bind _ = get_a_accessor t in + ok () diff --git a/src/ligo/ast_simplified/misc.ml b/src/ligo/ast_simplified/misc.ml index 02788c082..49baa1820 100644 --- a/src/ligo/ast_simplified/misc.ml +++ b/src/ligo/ast_simplified/misc.ml @@ -12,6 +12,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 _ -> simple_fail "different nats" | Literal_nat _, _ -> simple_fail "nat vs non-nat" + | Literal_tez a, Literal_tez b when a = b -> ok () + | Literal_tez _, Literal_tez _ -> simple_fail "different tezs" + | Literal_tez _, _ -> simple_fail "tez vs non-tez" | Literal_string a, Literal_string b when a = b -> ok () | Literal_string _, Literal_string _ -> simple_fail "different strings" | Literal_string _, _ -> simple_fail "string vs non-string" diff --git a/src/ligo/ast_simplified/types.ml b/src/ligo/ast_simplified/types.ml index 73308daf6..4df0d9fda 100644 --- a/src/ligo/ast_simplified/types.ml +++ b/src/ligo/ast_simplified/types.ml @@ -83,6 +83,7 @@ and literal = | Literal_bool of bool | Literal_int of int | Literal_nat of int + | Literal_tez of int | Literal_string of string | Literal_bytes of bytes diff --git a/src/ligo/ast_typed/PP.ml b/src/ligo/ast_typed/PP.ml index 98ef3d7fe..4363c3490 100644 --- a/src/ligo/ast_typed/PP.ml +++ b/src/ligo/ast_typed/PP.ml @@ -58,7 +58,8 @@ and literal ppf (l:literal) : unit = | Literal_unit -> fprintf ppf "unit" | Literal_bool b -> fprintf ppf "%b" b | Literal_int n -> fprintf ppf "%d" n - | Literal_nat n -> fprintf ppf "%d" n + | Literal_nat 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 diff --git a/src/ligo/ast_typed/combinators.ml b/src/ligo/ast_typed/combinators.ml index 1391fa29b..c0670fb20 100644 --- a/src/ligo/ast_typed/combinators.ml +++ b/src/ligo/ast_typed/combinators.ml @@ -10,13 +10,18 @@ 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_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 let t_nat ?s () : type_value = make_t (T_constant ("nat", [])) s +let t_tez ?s () : type_value = make_t (T_constant ("tez", [])) s 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_contract t ?s () : type_value = make_t (T_constant ("contract", [t])) s let t_pair a b ?s () = t_tuple [a ; b] ?s () + let t_record m ?s () : type_value = make_t (T_record m) s let make_t_ez_record (lst:(string * type_value) list) : type_value = let aux prev (k, v) = SMap.add k v prev in @@ -43,6 +48,18 @@ let get_t_bool (t:type_value) : unit result = match t.type_value' with | T_constant ("bool", []) -> ok () | _ -> simple_fail "not a bool" +let get_t_unit (t:type_value) : unit result = match t.type_value' with + | T_constant ("unit", []) -> ok () + | _ -> simple_fail "not a unit" + +let get_t_tez (t:type_value) : unit result = match t.type_value' with + | T_constant ("tez", []) -> ok () + | _ -> simple_fail "not a tez" + +let get_t_contract (t:type_value) : type_value result = match t.type_value' with + | T_constant ("contract", [x]) -> ok x + | _ -> simple_fail "not a contract" + let get_t_option (t:type_value) : type_value result = match t.type_value' with | T_constant ("option", [o]) -> ok o | _ -> simple_fail "not a option" @@ -80,6 +97,8 @@ let get_t_map (t:type_value) : (type_value * type_value) result = | T_constant ("map", [k;v]) -> ok (k, v) | _ -> simple_fail "get: not a map" +let assert_t_tez :type_value -> unit result = get_t_tez + let assert_t_map (t:type_value) : unit result = match t.type_value' with | T_constant ("map", [_ ; _]) -> ok () @@ -107,6 +126,9 @@ let assert_t_nat : type_value -> unit result = fun t -> match t.type_value' with | T_constant ("nat", []) -> ok () | _ -> simple_fail "not an nat" +let assert_t_bool : type_value -> unit result = fun v -> get_t_bool v +let assert_t_unit : type_value -> unit result = fun v -> get_t_unit v + let e_record map : expression = E_record map let ez_e_record (lst : (string * ae) list) : expression = let aux prev (k, v) = SMap.add k v prev in @@ -168,6 +190,12 @@ let get_a_bool (t:annotated_expression) = | E_literal (Literal_bool b) -> ok b | _ -> simple_fail "not a bool" + +let get_a_record_accessor = fun t -> + match t.expression with + | E_record_accessor (a , b) -> ok (a , b) + | _ -> simple_fail "not an accessor" + let get_declaration_by_name : program -> string -> declaration result = fun p name -> let aux : declaration -> bool = fun declaration -> match declaration with diff --git a/src/ligo/ast_typed/misc.ml b/src/ligo/ast_typed/misc.ml index 4093b5482..063bacb1a 100644 --- a/src/ligo/ast_typed/misc.ml +++ b/src/ligo/ast_typed/misc.ml @@ -178,6 +178,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 _ -> simple_fail "different nats" | Literal_nat _, _ -> simple_fail "nat vs non-nat" + | Literal_tez a, Literal_tez b when a = b -> ok () + | Literal_tez _, Literal_tez _ -> simple_fail "different tezs" + | Literal_tez _, _ -> simple_fail "tez vs non-tez" | Literal_string a, Literal_string b when a = b -> ok () | Literal_string _, Literal_string _ -> simple_fail "different strings" | Literal_string _, _ -> simple_fail "string vs non-string" diff --git a/src/ligo/ast_typed/types.ml b/src/ligo/ast_typed/types.ml index 06fd54aab..96a8bf9e7 100644 --- a/src/ligo/ast_typed/types.ml +++ b/src/ligo/ast_typed/types.ml @@ -98,6 +98,7 @@ and literal = | Literal_bool of bool | Literal_int of int | Literal_nat of int + | Literal_tez of int | Literal_string of string | Literal_bytes of bytes diff --git a/src/ligo/compiler/compiler_program.ml b/src/ligo/compiler/compiler_program.ml index 3e77c6f95..35fd8e7cf 100644 --- a/src/ligo/compiler/compiler_program.ml +++ b/src/ligo/compiler/compiler_program.ml @@ -47,6 +47,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_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) | D_unit -> ok @@ prim D_Unit diff --git a/src/ligo/contracts/counter.mligo b/src/ligo/contracts/counter.mligo new file mode 100644 index 000000000..0cfa95bdf --- /dev/null +++ b/src/ligo/contracts/counter.mligo @@ -0,0 +1,4 @@ +type storage = int + +let%entry main (p:int) storage = + (list [] : operation list , p + storage) diff --git a/src/ligo/contracts/new-syntax.mligo b/src/ligo/contracts/new-syntax.mligo index dfd965c11..f2fed5396 100644 --- a/src/ligo/contracts/new-syntax.mligo +++ b/src/ligo/contracts/new-syntax.mligo @@ -15,6 +15,7 @@ type param = { let%entry attempt (p:param) storage = if Crypto.hash (Bytes.pack p.attempt) <> Bytes.pack storage.challenge then failwith "Failed challenge" ; - let transfer : operation = Operation.transfer (sender , 10tz) in + let contract : unit contract = Operation.get_contract sender in + let transfer : operation = Operation.transaction (unit , contract , 10.00tz) in let storage : storage = storage.challenge <- p.new_challenge in ((list [] : operation list), storage) diff --git a/src/ligo/mini_c/PP.ml b/src/ligo/mini_c/PP.ml index df09d281e..410a228e4 100644 --- a/src/ligo/mini_c/PP.ml +++ b/src/ligo/mini_c/PP.ml @@ -46,7 +46,8 @@ let environment ppf (x:environment) = let rec value ppf : value -> unit = function | D_bool b -> fprintf ppf "%b" b | D_int n -> fprintf ppf "%d" n - | D_nat n -> fprintf ppf "%d" n + | D_nat n -> fprintf ppf "+%d" n + | D_tez n -> fprintf ppf "%dtz" n | D_unit -> fprintf ppf " " | D_string s -> fprintf ppf "\"%s\"" s | D_bytes _ -> fprintf ppf "[bytes]" diff --git a/src/ligo/mini_c/types.ml b/src/ligo/mini_c/types.ml index 3ba6a7571..7a443742e 100644 --- a/src/ligo/mini_c/types.ml +++ b/src/ligo/mini_c/types.ml @@ -41,6 +41,7 @@ type value = | D_unit | D_bool of bool | D_nat of int + | D_tez of int | D_int of int | D_string of string | D_bytes of bytes diff --git a/src/ligo/operators/operators.ml b/src/ligo/operators/operators.ml index 98523c75c..57ca170f6 100644 --- a/src/ligo/operators/operators.ml +++ b/src/ligo/operators/operators.ml @@ -5,10 +5,14 @@ module Simplify = struct let type_constants = [ ("unit" , 0) ; ("string" , 0) ; + ("bytes" , 0) ; ("nat" , 0) ; ("int" , 0) ; + ("tez" , 0) ; ("bool" , 0) ; ("operation" , 0) ; + ("address" , 0) ; + ("contract" , 1) ; ("list" , 1) ; ("option" , 1) ; ("set" , 1) ; @@ -26,7 +30,11 @@ module Simplify = struct let constants = [ ("Bytes.pack" , 1) ; ("Crypto.hash" , 1) ; - ("Operation.transfer" , 2) ; + ("Operation.transaction" , 3) ; + ("Operation.get_contract" , 1) ; + ("sender" , 0) ; + ("unit" , 0) ; + ("source" , 0) ; ] end @@ -71,6 +79,10 @@ module Typer = struct let true_2 = predicate_2 (fun _ _ -> true) let true_3 = predicate_3 (fun _ _ _ -> true) + let eq_1 : type_value -> typer_predicate = fun v -> + let aux = fun a -> type_value_eq (a, v) in + predicate_1 aux + let eq_2 : type_value -> typer_predicate = fun v -> let aux = fun a b -> type_value_eq (a, v) && type_value_eq (b, v) in predicate_2 aux @@ -85,6 +97,11 @@ module Typer = struct | [ a ] -> f a | _ -> simple_fail "!!!" + let typer'_1_opt : (type_value -> type_value option -> type_result result) -> typer' = fun f lst tv_opt -> + match lst with + | [ a ] -> f a tv_opt + | _ -> simple_fail "!!!" + let typer'_2 : (type_value -> type_value -> type_result result) -> typer' = fun f lst _ -> match lst with | [ a ; b ] -> f a b @@ -95,6 +112,8 @@ module Typer = struct | [ a ; b ; c ] -> f a b c | _ -> simple_fail "!!!" + let typer_constant cst : typer' = fun _ _ -> ok cst + let constant_2 : string -> type_value -> typer' = fun s tv -> let aux = fun _ _ -> ok (s, tv) in typer'_2 aux @@ -113,6 +132,7 @@ module Typer = struct let comparator : string -> typer = fun s -> s , 2 , [ (eq_2 (t_int ()), constant_2 s (t_bool ())) ; (eq_2 (t_nat ()), constant_2 s (t_bool ())) ; + (eq_2 (t_bytes ()), constant_2 s (t_bool ())) ; ] let boolean_operator_2 : string -> typer = fun s -> very_same_2 s (t_bool ()) @@ -162,11 +182,66 @@ module Typer = struct ] let int : typer = "int" , 1 , [ - (true_1, typer'_1 (fun t -> - let%bind () = assert_t_nat t in - ok ("INT", t_int ()))) + (eq_1 (t_nat ()), typer_constant ("INT" , t_int ())) ] + let bytes_pack : typer = "Bytes.pack" , 1 , [ + (true_1 , typer'_1 (fun _ -> ok ("PACK" , t_bytes ()))) + ] + + let bytes_unpack = "Bytes.unpack" , 1 , [ + eq_1 (t_bytes ()) , typer'_1_opt (fun _ tv_opt -> match tv_opt with + | None -> simple_fail "untyped UNPACK" + | Some t -> ok ("UNPACK", t)) + ] + + let crypto_hash = "Crypto.hash" , 1 , [ + eq_1 (t_bytes ()) , typer_constant ("HASH" , t_bytes ()) ; + ] + + let sender = "sender" , 0 , [ + predicate_0 , typer_constant ("SENDER", t_address ()) + ] + + let source = "source" , 0 , [ + predicate_0 , typer_constant ("SOURCE", t_address ()) + ] + + let unit = "unit" , 0 , [ + predicate_0 , typer_constant ("UNIT", t_unit ()) + ] + + let transaction = "Operation.transaction" , 3 , [ + true_3 , typer'_3 ( + fun param contract amount -> + let%bind () = + assert_t_tez amount in + let%bind contract_param = + get_t_contract contract in + let%bind () = + assert_type_value_eq (param , contract_param) in + ok ("TRANSFER_TOKENS" , t_operation ()) + ) + ] + + let get_contract = "Operation.get_contract" , 1 , [ + eq_1 (t_address ()) , typer'_1_opt ( + fun _ tv_opt -> + let%bind tv = + trace_option (simple_error "get_contract needs a type annotation") tv_opt in + let%bind tv' = + trace_strong (simple_error "get_contract has a not-contract annotation") @@ + get_t_contract tv in + ok ("CONTRACT" , t_contract tv' ()) + ) + ] + + (* let record_assign = "RECORD_ASSIGN" , 2 , [ + * true_2 , typer'_2 (fun path new_value -> + * let%bind (a , b) = get_a_record_accessor path in + * ) + * ] *) + let constant_typers = let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in Map.String.of_list @@ -184,6 +259,7 @@ module Typer = struct none ; some ; comparator "EQ" ; + comparator "NEQ" ; comparator "LT" ; comparator "GT" ; comparator "LE" ; @@ -195,6 +271,14 @@ module Typer = struct int ; size ; get_force ; + bytes_pack ; + bytes_unpack ; + crypto_hash ; + sender ; + source ; + unit ; + transaction ; + get_contract ; ] end diff --git a/src/ligo/parser/camligo/lex/generator.ml b/src/ligo/parser/camligo/lex/generator.ml index acd64732a..0bc669729 100644 --- a/src/ligo/parser/camligo/lex/generator.ml +++ b/src/ligo/parser/camligo/lex/generator.ml @@ -23,6 +23,7 @@ module Print_mly = struct let tokens = fun ppf tokens -> fprintf ppf "%%token EOF\n" ; fprintf ppf "%%token INT\n" ; + fprintf ppf "%%token NAT\n" ; fprintf ppf "%%token TZ\n" ; fprintf ppf "%%token STRING\n" ; fprintf ppf "%%token NAME\n" ; @@ -58,8 +59,10 @@ rule token = parse | '"' { string "" lexbuf } | [' ' '\t'] { token lexbuf } +| (['0'-'9']+ as i) 'p' + { NAT (int_of_string i) } | (['0'-'9']+ as n) '.' (['0'-'9']['0'-'9'] as d) "tz" { TZ ((int_of_string n) * 100 + (int_of_string d)) } -| (['0'-'9']+ as i) 'p'? +| (['0'-'9']+ as i) { INT (int_of_string i) } |pre} let post = @@ -108,6 +111,7 @@ let to_string : token -> string = function | NAME _ -> "NAME s" | CONSTRUCTOR_NAME _ -> "CONSTRUCTOR_NAME s" | INT _ -> "INT n" + | NAT _ -> "NAT n" | TZ _ -> "TZ n" | EOF -> "EOF" |pre} diff --git a/src/ligo/simplify/camligo.ml b/src/ligo/simplify/camligo.ml index 32b7f49b8..2b15bfe89 100644 --- a/src/ligo/simplify/camligo.ml +++ b/src/ligo/simplify/camligo.ml @@ -35,7 +35,6 @@ let get_unrestricted_pattern : I.restricted_pattern -> I.pattern Location.wrap r error title content in fail error - let get_p_type_annotation : I.pattern -> (I.pattern Location.wrap * I.restricted_type_expression Location.wrap) result = fun p -> match p with | I.P_type_annotation pta -> ok pta @@ -195,14 +194,17 @@ and expression_last_instruction : I.expression -> lir result = fun e -> | I.E_let_in l -> let_in_last_instruction l | I.E_sequence s -> sequence_last_instruction s | I.E_fun _|I.E_record _|I.E_ifthenelse _ - |I.E_ifthen _|I.E_match _|I.E_main _ -> ( + | I.E_ifthen _|I.E_match _|I.E_main _ -> ( let%bind result' = expression e in ok ([] , result') ) and expression_sequence : I.expression -> O.instruction result = fun e -> - let%bind e' = expression e in - ok @@ O.I_do e' + match e with + | _ -> ( + let%bind e' = expression e in + ok @@ O.I_do e' + ) and let_in_last_instruction : I.pattern Location.wrap * I.expression Location.wrap * I.expression Location.wrap -> lir result @@ -211,7 +213,9 @@ and let_in_last_instruction : let%bind (var , ty) = get_p_typed_variable (unwrap pat) in let%bind ty' = type_expression @@ of_restricted_type_expression (unwrap ty) in let%bind expr' = expression (unwrap expr) in - let%bind uexpr' = get_untyped_expression expr' in + let%bind uexpr' = + trace_strong (simple_error "no annotation on let bodies") @@ + get_untyped_expression expr' in let%bind (body' , last') = expression_last_instruction (unwrap body) in let assignment = O.(i_assignment @@ named_typed_expression (unwrap var) uexpr' ty') in ok (assignment :: body' , last') @@ -277,20 +281,23 @@ and expression_main : I.expression_main Location.wrap -> O.annotated_expression let simple_binop name ab = let%bind (a' , b') = bind_map_pair expression_main ab in return @@ E_constant (name, [a' ; b']) in - trace ( + let error_main = let title () = "simplifying main_expression" in let content () = Format.asprintf "%a" I.pp_expression_main (unwrap em) in error title content - ) @@ + in + trace error_main @@ match (unwrap em) with | Eh_tuple lst -> let%bind lst' = bind_map_list expression_main lst in return @@ E_tuple lst' + | Eh_module_ident (lst , v) -> identifier_application (lst , v) None + | Eh_variable v -> identifier_application ([] , v) None | Eh_application (f , arg) -> ( let%bind arg' = expression_main arg in match unwrap f with - | Eh_variable v -> identifier ([] , v) arg' - | Eh_module_ident (lst , v) -> identifier (lst , v) arg' + | Eh_variable v -> identifier_application ([] , v) (Some arg') + | Eh_module_ident (lst , v) -> identifier_application (lst , v) (Some arg') | _ -> ( let%bind f' = expression_main f in return @@ E_application (f' , arg') @@ -328,16 +335,8 @@ and expression_main : I.expression_main Location.wrap -> O.annotated_expression return @@ E_literal (Literal_string (unwrap s)) | Eh_unit _ -> return @@ E_literal Literal_unit - | Eh_tz _ -> - simple_fail "tz literals not supported yet" - | Eh_module_ident _ -> - let error = - let title () = "modules not supported yet" in - let content () = Format.asprintf "%a" I.pp_expression_main (unwrap em) in - error title content in - fail error - | Eh_variable v -> - return @@ E_variable (unwrap v) + | Eh_tz n -> + return @@ E_literal (Literal_tez (unwrap n)) | Eh_constructor _ -> simple_fail "constructor without parameter" | Eh_data_structure (kind , content) -> ( @@ -363,10 +362,18 @@ and expression_main : I.expression_main Location.wrap -> O.annotated_expression | Eh_bottom e -> expression (unwrap e) -and identifier : (string Location.wrap) list * string Location.wrap -> _ -> _ result = fun (lst , v) param -> +and identifier_application : (string Location.wrap) list * string Location.wrap -> O.value option -> _ result = fun (lst , v) param_opt -> let constant_name = String.concat "." ((List.map unwrap lst) @ [unwrap v]) in - match List.assoc_opt constant_name constants with - | Some n -> ( + match List.assoc_opt constant_name constants , param_opt with + | Some 0 , None -> + ok O.(untyped_expression @@ E_constant (constant_name , [])) + | Some _ , None -> + simple_fail "n-ary constant without parameter" + | Some 0 , Some _ -> simple_fail "applying to nullary constant" + | Some 1 , Some param -> ( + ok O.(untyped_expression @@ E_constant (constant_name , [param])) + ) + | Some n , Some param -> ( let params = match get_expression param with | E_tuple lst -> lst @@ -376,7 +383,7 @@ and identifier : (string Location.wrap) list * string Location.wrap -> _ -> _ re Assert.assert_list_size params n in ok O.(untyped_expression @@ E_constant (constant_name , params)) ) - | None -> + | None , param_opt -> ( let%bind () = let error = let title () = "no module identifiers yet" in @@ -384,8 +391,11 @@ and identifier : (string Location.wrap) list * string Location.wrap -> _ -> _ re error title content in trace_strong error @@ Assert.assert_list_empty lst in - ok O.(untyped_expression @@ E_application (untyped_expression @@ E_variable (unwrap v) , param)) - + match constant_name , param_opt with + | "failwith" , Some param -> ok O.(untyped_expression @@ e_failwith param) + | _ , Some param -> ok O.(untyped_expression @@ E_application (untyped_expression @@ E_variable (unwrap v) , param)) + | _ , None -> ok O.(untyped_expression @@ e_variable (unwrap v)) + ) let let_content : I.let_content -> _ result = fun l -> match l with diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml index 9d622b825..32dcf41aa 100644 --- a/src/ligo/test/integration_tests.ml +++ b/src/ligo/test/integration_tests.ml @@ -4,6 +4,12 @@ open Test_helpers open Ast_simplified.Combinators +let mtype_file path : Ast_typed.program result = + let%bind raw = Parser.Camligo.User.parse_file path in + let%bind simpl = Simplify.Camligo.main raw in + let%bind typed = Ligo.Typer.type_program (Location.unwrap simpl) in + ok typed + let function_ () : unit result = let%bind program = type_file "./contracts/function.ligo" in let make_expect = fun n -> n in @@ -341,6 +347,23 @@ let super_counter_contract () : unit result = e_a_pair (e_a_list [] t_operation) (e_a_int (op 42 n)) in expect_n program "main" make_input make_expected +let basic_mligo () : unit result = + let%bind typed = mtype_file "./contracts/basic.mligo" in + let%bind result = Ligo.easy_evaluate_typed "foo" typed in + Ligo.AST_Typed.assert_value_eq (Ligo.AST_Typed.Combinators.e_a_empty_int (42 + 127), result) + +let counter_mligo () : unit result = + let%bind program = mtype_file "./contracts/counter.mligo" in + let make_input = fun n-> e_a_pair (e_a_int n) (e_a_int 42) in + let make_expected = fun n -> e_a_pair (e_a_list [] t_operation) (e_a_int (42 + n)) in + expect_n program "main" make_input make_expected + +let guess_the_hash_mligo () : unit result = + let%bind program = mtype_file "./contracts/new-syntax.mligo" in + let make_input = fun n-> e_a_pair (e_a_int n) (e_a_int 42) in + let make_expected = fun n -> e_a_pair (e_a_list [] t_operation) (e_a_int (42 + n)) in + expect_n program "main" make_input make_expected + let main = "Integration (End to End)", [ test "function" function_ ; test "complex function" complex_function ; @@ -368,4 +391,7 @@ let main = "Integration (End to End)", [ test "counter contract" counter_contract ; test "super counter contract" super_counter_contract ; test "higher order" higher_order ; + test "basic mligo" basic_mligo ; + test "counter contract mligo" counter_mligo ; + test "guess the hash mligo" guess_the_hash_mligo ; ] diff --git a/src/ligo/test/multifix_tests.ml b/src/ligo/test/multifix_tests.ml index 134ddf253..48b21e478 100644 --- a/src/ligo/test/multifix_tests.ml +++ b/src/ligo/test/multifix_tests.ml @@ -11,15 +11,7 @@ let simplify () : unit result = let%bind _simpl = Simplify.Camligo.main raw in ok () -let integration () : unit result = - let%bind raw = User.parse_file "./contracts/basic.mligo" in - let%bind simpl = Simplify.Camligo.main raw in - let%bind typed = Ligo.Typer.type_program (Location.unwrap simpl) in - let%bind result = Ligo.easy_evaluate_typed "foo" typed in - Ligo.AST_Typed.assert_value_eq (Ligo.AST_Typed.Combinators.e_a_empty_int (42 + 127), result) - let main = "Multifix", [ test "basic" basic ; test "simplify" simplify ; - test "integration" integration ; ] diff --git a/src/ligo/transpiler/transpiler.ml b/src/ligo/transpiler/transpiler.ml index 2a884ed37..607b04778 100644 --- a/src/ligo/transpiler/transpiler.ml +++ b/src/ligo/transpiler/transpiler.ml @@ -178,6 +178,7 @@ and 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_tez n -> D_tez n | Literal_bytes s -> D_bytes s | Literal_string s -> D_string s | Literal_unit -> D_unit diff --git a/src/ligo/typer/typer.ml b/src/ligo/typer/typer.ml index 11b857f87..e71cf024d 100644 --- a/src/ligo/typer/typer.ml +++ b/src/ligo/typer/typer.ml @@ -94,6 +94,9 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc | I_skip -> return O.I_skip | I_do x -> let%bind expression = type_annotated_expression e x in + let%bind () = + trace_strong (simple_error "do without unit") @@ + Ast_typed.assert_type_value_eq (get_type_annotation expression , t_unit ()) in return @@ O.I_do expression | I_loop (cond, body) -> let%bind cond = type_annotated_expression e cond in @@ -277,6 +280,11 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot let return expr tv = let%bind type_annotation = check tv in ok @@ make_a_e expr type_annotation e in + let main_error = + let title () = "typing annotated_expression" in + let content () = Format.asprintf "%a" I.PP.annotated_expression ae in + error title content in + trace main_error @@ match ae.expression with (* Basic *) | E_failwith _ -> simple_fail "can't type failwith in isolation" @@ -297,6 +305,8 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot return (E_literal (Literal_int n)) (t_int ()) | E_literal (Literal_nat n) -> return (E_literal (Literal_nat n)) (t_nat ()) + | E_literal (Literal_tez n) -> + return (E_literal (Literal_tez n)) (t_tez ()) (* Tuple *) | E_tuple lst -> let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in @@ -431,27 +441,48 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot (* Advanced *) | E_matching (ex, m) -> ( let%bind ex' = type_annotated_expression e ex in - let%bind m' = type_match type_annotated_expression e ex'.type_annotation m in - let tvs = - let aux (cur:O.value O.matching) = - match cur with - | Match_bool { match_true ; match_false } -> [ match_true ; match_false ] - | Match_list { match_nil ; match_cons = (_ , _ , match_cons) } -> [ match_nil ; match_cons ] - | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ] - | Match_tuple (_ , match_tuple) -> [ match_tuple ] - | Match_variant (lst , _) -> List.map snd lst in - List.map get_type_annotation @@ aux m' in - let aux prec cur = - let%bind () = - match prec with - | None -> ok () - | Some cur' -> Ast_typed.assert_type_value_eq (cur , cur') in - ok (Some cur) in - let%bind tv_opt = bind_fold_list aux None tvs in - let%bind tv = - trace_option (simple_error "empty matching") @@ - tv_opt in - return (O.E_matching (ex', m')) tv + match m with + (* Special case for assert-like failwiths. TODO: CLEAN THIS. *) + | I.Match_bool { match_false ; match_true = { expression = E_failwith fw } } -> ( + let%bind fw' = type_annotated_expression e fw in + let%bind mf' = type_annotated_expression e match_false in + let%bind () = + trace_strong (simple_error "Matching bool on not-a-bool") + @@ assert_t_bool (get_type_annotation ex') in + let%bind () = + trace_strong (simple_error "Matching not-unit on an assert") + @@ assert_t_unit (get_type_annotation mf') in + let mt' = make_a_e + (E_failwith fw') + (t_unit ()) + e + in + let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in + return (O.E_matching (ex' , m')) (t_unit ()) + ) + | _ -> ( + let%bind m' = type_match type_annotated_expression e ex'.type_annotation m in + let tvs = + let aux (cur:O.value O.matching) = + match cur with + | Match_bool { match_true ; match_false } -> [ match_true ; match_false ] + | Match_list { match_nil ; match_cons = (_ , _ , match_cons) } -> [ match_nil ; match_cons ] + | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ] + | Match_tuple (_ , match_tuple) -> [ match_tuple ] + | Match_variant (lst , _) -> List.map snd lst in + List.map get_type_annotation @@ aux m' in + let aux prec cur = + let%bind () = + match prec with + | None -> ok () + | Some cur' -> Ast_typed.assert_type_value_eq (cur , cur') in + ok (Some cur) in + let%bind tv_opt = bind_fold_list aux None tvs in + let%bind tv = + trace_option (simple_error "empty matching") @@ + tv_opt in + return (O.E_matching (ex', m')) tv + ) ) and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result = @@ -497,6 +528,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_tez n -> ok (Literal_tez n) | Literal_int n -> ok (Literal_int n) | Literal_string s -> ok (Literal_string s) | Literal_bytes b -> ok (Literal_bytes b)