extend camligo and ligo
This commit is contained in:
parent
c5f6fe670a
commit
6cb341b162
@ -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
|
||||
|
||||
|
@ -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 ()
|
||||
|
@ -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"
|
||||
|
@ -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
|
||||
|
||||
|
@ -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
|
||||
|
||||
|
@ -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
|
||||
|
@ -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"
|
||||
|
@ -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
|
||||
|
||||
|
@ -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
|
||||
|
4
src/ligo/contracts/counter.mligo
Normal file
4
src/ligo/contracts/counter.mligo
Normal file
@ -0,0 +1,4 @@
|
||||
type storage = int
|
||||
|
||||
let%entry main (p:int) storage =
|
||||
(list [] : operation list , p + storage)
|
@ -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)
|
||||
|
@ -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]"
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -23,6 +23,7 @@ module Print_mly = struct
|
||||
let tokens = fun ppf tokens ->
|
||||
fprintf ppf "%%token EOF\n" ;
|
||||
fprintf ppf "%%token <int> INT\n" ;
|
||||
fprintf ppf "%%token <int> NAT\n" ;
|
||||
fprintf ppf "%%token <int> TZ\n" ;
|
||||
fprintf ppf "%%token <string> STRING\n" ;
|
||||
fprintf ppf "%%token <string> 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}
|
||||
|
@ -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 ->
|
||||
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
|
||||
|
@ -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 ;
|
||||
]
|
||||
|
@ -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 ;
|
||||
]
|
||||
|
@ -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
|
||||
|
@ -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,6 +441,26 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
|
||||
(* Advanced *)
|
||||
| E_matching (ex, m) -> (
|
||||
let%bind ex' = type_annotated_expression e ex in
|
||||
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) =
|
||||
@ -453,6 +483,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
|
||||
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 =
|
||||
(* Constant poorman's polymorphism *)
|
||||
@ -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)
|
||||
|
Loading…
Reference in New Issue
Block a user