balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Merge branch 'master' of gitlab.com:gabriel.alfour/tezos

Browse Source
This commit is contained in:
Christian Rinderknecht 2019-05-04 23:14:20 +02:00
commit bdec7d0add
No known key found for this signature in database
GPG Key ID: 9446816CFD267040
37 changed files with 739 additions and 287 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/lib_utils/PP.ml
View File

@ -1,6 +1,7 @@
open Format
let string : formatter -> string -> unit = fun ppf s -> fprintf ppf "%s" s
let tag tag : formatter -> unit -> unit = fun ppf () -> fprintf ppf tag
let bool ppf b = fprintf ppf "%b" b
let new_line : formatter -> unit -> unit = tag "@;"
let rec new_lines n ppf () =
match n with
@ -23,6 +24,11 @@ let option = fun f ppf opt ->
| Some x -> fprintf ppf "Some(%a)" f x
| None -> fprintf ppf "None"
let lr = fun ppf lr ->
match lr with
| `Left -> fprintf ppf "left"
| `Right -> fprintf ppf "right"
let int = fun ppf n -> fprintf ppf "%d" n
let map = fun f pp ppf x ->

2
src/lib_utils/function.ml
View File

@ -1,3 +1,5 @@
let constant x _ = x
let compose = fun f g x -> f (g x)
let (>|) = compose

11
src/lib_utils/logger.ml Normal file
View File

@ -0,0 +1,11 @@
module Stateful () : sig
val log : string -> unit
val get : unit -> string
end = struct
let logger = ref ""
let log : string -> unit =
fun s -> logger := !logger ^ s
let get () : string = !logger
end

1
src/lib_utils/tezos_utils.ml
View File

@ -10,6 +10,7 @@ module Micheline = X_tezos_micheline
module Function = Function
module Error_monad = X_error_monad
module Trace = Trace
module Logger = Logger
module PP_helpers = PP
module Location = Location

18
src/lib_utils/trace.ml
View File

@ -128,6 +128,10 @@ let trace_option error = function
| None -> fail error
| Some s -> ok s
let bind_map_option f = function
| None -> ok None
| Some s -> f s >>? fun x -> ok (Some x)
let rec bind_list = function
| [] -> ok []
| hd :: tl -> (
@ -175,6 +179,16 @@ let bind_fold_list f init lst =
in
List.fold_left aux (ok init) lst
let bind_fold_map_list = fun f acc lst ->
let rec aux (acc , prev) f = function
| [] -> ok (acc , prev)
| hd :: tl ->
f acc hd >>? fun (acc' , hd') ->
aux (acc' , hd' :: prev) f tl
in
aux (acc , []) f (List.rev lst) >>? fun (_acc' , lst') ->
ok lst'
let bind_fold_right_list f init lst =
let aux x y =
x >>? fun x ->
@ -342,6 +356,10 @@ let pp_to_string pp () x =
let errors_to_string = pp_to_string errors_pp
module Assert = struct
let assert_fail ?(msg="didn't fail") = function
| Ok _ -> simple_fail msg
| _ -> ok ()
let assert_true ?(msg="not true") = function
| true -> ok ()
| false -> simple_fail msg

10
src/lib_utils/x_list.ml
View File

@ -7,6 +7,16 @@ let map ?(acc = []) f lst =
in
aux acc f (List.rev lst)
let fold_map : type acc ele ret . (acc -> ele -> (acc * ret)) -> acc -> ele list -> ret list =
fun f acc lst ->
let rec aux (acc , prev) f = function
| [] -> (acc , prev)
| hd :: tl ->
let (acc' , hd') = f acc hd in
aux (acc' , hd' :: prev) f tl
in
snd @@ aux (acc , []) f (List.rev lst)
let fold_right' f init lst = List.fold_left f init (List.rev lst)
let filter_map f =

26
src/lib_utils/x_memory_proto_alpha.ml
View File

@ -44,6 +44,29 @@ let parse_michelson (type aft)
)
| _ -> Lwt.return @@ error_exn (Failure "Typing instr failed")
let parse_michelson_fail (type aft)
?(tezos_context = dummy_environment.tezos_context)
?(top_level = Lambda) (michelson:Michelson.t)
?type_logger
(bef:'a Script_typed_ir.stack_ty) (aft:aft Script_typed_ir.stack_ty)
=
let michelson = Michelson.strip_annots michelson in
let michelson = Michelson.strip_nops michelson in
parse_instr
?type_logger
top_level tezos_context
michelson bef >>=?? fun (j, _) ->
match j with
| Typed descr -> (
Lwt.return (
alpha_wrap (Script_ir_translator.stack_ty_eq tezos_context 0 descr.aft aft) >>? fun (Eq, _) ->
let descr : (_, aft) Script_typed_ir.descr = {descr with aft} in
Ok descr
)
)
| Failed { descr } ->
Lwt.return (Ok (descr aft))
let parse_michelson_data
?(tezos_context = dummy_environment.tezos_context)
michelson ty =
@ -79,7 +102,8 @@ let interpret
?(source = (List.nth dummy_environment.identities 0).implicit_contract)
?(self = (List.nth dummy_environment.identities 0).implicit_contract)
?(payer = (List.nth dummy_environment.identities 1).implicit_contract)
?(amount = Alpha_context.Tez.one)
?visitor
(instr:('a, 'b) descr) (bef:'a stack) : 'b stack tzresult Lwt.t =
Script_interpreter.step tezos_context ~source ~self ~payer ?visitor Alpha_context.Tez.one instr bef >>=??
Script_interpreter.step tezos_context ~source ~self ~payer ?visitor amount instr bef >>=??
fun (stack, _) -> return stack

21
src/ligo/TODO.txt
View File

@ -1,2 +1,19 @@
- Unify gets in Ast_simplified
- Unify assignments in Ast_simplified
# Main
## Back-end
- Replace Mini_c environments with stacks
- Think about Coq
## Amendments
- Bubble_n
- Partial application
- Type size limit (1.000 -> 10.000)
# PPX
## Deriving
- Generate ADT helpers (this removes 90% of Combinators and a lot of maintenance when modifying ASTs)
- Generate option helpers (this makes writing main much easier, much like one would in an untyped language)

6
src/ligo/ast_simplified/PP.ml
View File

@ -21,6 +21,7 @@ let literal ppf (l:literal) = match l with
| 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
| Literal_address s -> fprintf ppf "@%S" s
let rec expression ppf (e:expression) = match e with
| E_literal l -> literal ppf l
@ -50,6 +51,7 @@ and access ppf (a:access) =
match a with
| Access_tuple n -> fprintf ppf "%d" n
| Access_record s -> fprintf ppf "%s" s
| Access_map s -> fprintf ppf "(%a)" annotated_expression s
and access_path ppf (p:access_path) =
fprintf ppf "%a" (list_sep access (const ".")) p
@ -69,6 +71,9 @@ and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
and single_record_patch ppf ((p, ae) : string * ae) =
fprintf ppf "%s <- %a" p annotated_expression ae
and single_tuple_patch ppf ((p, ae) : int * ae) =
fprintf ppf "%d <- %a" p annotated_expression ae
and matching_variant_case : type a . (_ -> a -> unit) -> _ -> (constructor_name * name) * a -> unit =
fun f ppf ((c,n),a) ->
fprintf ppf "| %s %s -> %a" c n f a
@ -90,6 +95,7 @@ and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip"
| I_do ae -> fprintf ppf "do %a" annotated_expression ae
| I_record_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_record_patch) lst
| I_tuple_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_tuple_patch) lst
| I_loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
| I_assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae

16
src/ligo/ast_simplified/combinators.ml
View File

@ -26,17 +26,15 @@ let t_bytes : type_expression = T_constant ("bytes", [])
let t_int : type_expression = T_constant ("int", [])
let t_operation : type_expression = T_constant ("operation", [])
let t_nat : type_expression = T_constant ("nat", [])
let t_tez : type_expression = T_constant ("tez", [])
let t_unit : type_expression = T_constant ("unit", [])
let t_address : type_expression = T_constant ("address", [])
let t_option o : type_expression = T_constant ("option", [o])
let t_list t : type_expression = T_constant ("list", [t])
let t_variable n : type_expression = T_variable n
let t_tuple lst : type_expression = T_tuple lst
let t_pair (a , b) = t_tuple [a ; b]
let t_record m : type_expression = (T_record m)
let t_ez_record (lst:(string * type_expression) list) : type_expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
T_record map
let t_record_ez lst =
let m = SMap.of_list lst in
@ -63,6 +61,8 @@ let e_int n : expression = E_literal (Literal_int n)
let e_nat n : expression = E_literal (Literal_nat n)
let e_bool b : expression = E_literal (Literal_bool b)
let e_string s : expression = E_literal (Literal_string s)
let e_address s : expression = E_literal (Literal_address s)
let e_tez s : expression = E_literal (Literal_tez s)
let e_bytes b : expression = E_literal (Literal_bytes (Bytes.of_string b))
let e_record map : expression = E_record map
let e_tuple lst : expression = E_tuple lst
@ -84,6 +84,8 @@ let e_a_int n : annotated_expression = make_e_a_full (e_int n) t_int
let e_a_nat n : annotated_expression = make_e_a_full (e_nat n) t_nat
let e_a_bool b : annotated_expression = make_e_a_full (e_bool b) t_bool
let e_a_constructor s a : annotated_expression = make_e_a (e_constructor s a)
let e_a_address x = make_e_a_full (e_address x) t_address
let e_a_tez x = make_e_a_full (e_tez x) t_tez
let e_a_record r =
let type_annotation = Option.(
@ -163,3 +165,9 @@ let get_a_accessor = fun t ->
let assert_a_accessor = fun t ->
let%bind _ = get_a_accessor t in
ok ()
let get_access_record : access -> string result = fun a ->
match a with
| Access_tuple _
| Access_map _ -> simple_fail "not an access record"
| Access_record s -> ok s

3
src/ligo/ast_simplified/misc.ml
View File

@ -23,6 +23,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
| Literal_unit, Literal_unit -> ok ()
| Literal_unit, _ -> simple_fail "unit vs non-unit"
| Literal_address a, Literal_address b when a = b -> ok ()
| Literal_address _, Literal_address _ -> simple_fail "different addresss"
| Literal_address _, _ -> simple_fail "address vs non-address"
let rec assert_value_eq (a, b: (value*value)) : unit result =
let error_content () =

5
src/ligo/ast_simplified/types.ml
View File

@ -75,6 +75,7 @@ and expression =
and access =
| Access_tuple of int
| Access_record of string
| Access_map of ae
and access_path = access list
@ -86,6 +87,7 @@ and literal =
| Literal_tez of int
| Literal_string of string
| Literal_bytes of bytes
| Literal_address of string
and block = instruction list
and b = block
@ -96,7 +98,8 @@ and instruction =
| I_loop of ae * b
| I_skip
| I_do of ae
| I_record_patch of name * access_path * (string * ae) list
| I_record_patch of (name * access_path * (string * ae) list)
| I_tuple_patch of (name * access_path * (int * ae) list)
and 'a matching =
| Match_bool of {

2
src/ligo/ast_typed/PP.ml
View File

@ -62,6 +62,7 @@ and literal ppf (l:literal) : unit =
| 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
| Literal_address s -> fprintf ppf "@%s" s
and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
@ -87,6 +88,7 @@ and matching : type a . (formatter -> a -> unit) -> _ -> a matching -> unit = fu
and pre_access ppf (a:access) = match a with
| Access_record n -> fprintf ppf ".%s" n
| Access_tuple i -> fprintf ppf ".%d" i
| Access_map n -> fprintf ppf ".%a" annotated_expression n
and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip"

14
src/ligo/ast_typed/combinators.ml
View File

@ -91,13 +91,21 @@ let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value' wi
let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value' with
| T_record m -> ok m
| _ -> simple_fail "not a record"
| _ -> simple_fail "not a record type"
let get_t_map (t:type_value) : (type_value * type_value) result =
match t.type_value' with
| T_constant ("map", [k;v]) -> ok (k, v)
| _ -> simple_fail "get: not a map"
let get_t_map_key : type_value -> type_value result = fun t ->
let%bind (key , _) = get_t_map t in
ok key
let get_t_map_value : type_value -> type_value result = fun t ->
let%bind (_ , value) = get_t_map t in
ok value
let assert_t_tez :type_value -> unit result = get_t_tez
let assert_t_map (t:type_value) : unit result =
@ -143,16 +151,20 @@ let e_map lst : expression = E_map lst
let e_unit : expression = E_literal (Literal_unit)
let e_int n : expression = E_literal (Literal_int n)
let e_nat n : expression = E_literal (Literal_nat n)
let e_tez n : expression = E_literal (Literal_tez n)
let e_bool b : expression = E_literal (Literal_bool b)
let e_string s : expression = E_literal (Literal_string s)
let e_address s : expression = E_literal (Literal_address s)
let e_pair a b : expression = E_tuple [a; b]
let e_list lst : expression = E_list lst
let e_a_unit = make_a_e e_unit (t_unit ())
let e_a_int n = make_a_e (e_int n) (t_int ())
let e_a_nat n = make_a_e (e_nat n) (t_nat ())
let e_a_tez n = make_a_e (e_tez n) (t_tez ())
let e_a_bool b = make_a_e (e_bool b) (t_bool ())
let e_a_string s = make_a_e (e_string s) (t_string ())
let e_a_address s = make_a_e (e_address s) (t_address ())
let e_a_pair a b = make_a_e (e_pair a b) (t_pair a.type_annotation b.type_annotation ())
let e_a_some s = make_a_e (e_some s) (t_option s.type_annotation ())
let e_a_none t = make_a_e e_none (t_option t ())

2
src/ligo/ast_typed/combinators_environment.ml
View File

@ -6,8 +6,10 @@ let make_a_e_empty expression type_annotation = make_a_e expression type_annotat
let e_a_empty_unit = e_a_unit Environment.full_empty
let e_a_empty_int n = e_a_int n Environment.full_empty
let e_a_empty_nat n = e_a_nat n Environment.full_empty
let e_a_empty_tez n = e_a_tez n Environment.full_empty
let e_a_empty_bool b = e_a_bool b Environment.full_empty
let e_a_empty_string s = e_a_string s Environment.full_empty
let e_a_empty_address s = e_a_address s Environment.full_empty
let e_a_empty_pair a b = e_a_pair a b Environment.full_empty
let e_a_empty_some s = e_a_some s Environment.full_empty
let e_a_empty_none t = e_a_none t Environment.full_empty

11
src/ligo/ast_typed/misc.ml
View File

@ -226,8 +226,12 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
let rb' = SMap.to_kv_list rb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in record types"
@@ (ka = kb) in
let error =
let title () = "different props in record" in
let content () = Format.asprintf "%s vs %s" ka kb in
error title content in
trace_strong error @@
Assert.assert_true (ka = kb) in
assert_type_value_eq (va, vb)
in
let%bind _ =
@ -269,6 +273,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
| Literal_unit, Literal_unit -> ok ()
| Literal_unit, _ -> simple_fail "unit vs non-unit"
| Literal_address a, Literal_address b when a = b -> ok ()
| Literal_address _, Literal_address _ -> simple_fail "different addresss"
| Literal_address _, _ -> simple_fail "address vs non-address"
let rec assert_value_eq (a, b: (value*value)) : unit result =

8
src/ligo/ast_typed/types.ml
View File

@ -106,6 +106,7 @@ and literal =
| Literal_tez of int
| Literal_string of string
| Literal_bytes of bytes
| Literal_address of string
and block = instruction list
and b = block
@ -119,9 +120,12 @@ and instruction =
| I_skip
| I_patch of named_type_value * access_path * ae
and access = Ast_simplified.access
and access =
| Access_tuple of int
| Access_record of string
| Access_map of ae
and access_path = Ast_simplified.access_path
and access_path = access list
and 'a matching =
| Match_bool of {

214
src/ligo/compiler/compiler_program.ml
View File

@ -402,95 +402,7 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
and translate_statement ((s', w_env) as s:statement) : michelson result =
let error_message () = Format.asprintf "%a" PP.statement s in
let%bind (code : michelson) =
trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with
| S_environment_extend ->
ok @@ Compiler_environment.to_michelson_extend w_env.pre_environment
| S_environment_restrict ->
Compiler_environment.to_michelson_restrict w_env.pre_environment
| S_environment_add _ ->
simple_fail "add not ready yet"
(* | S_environment_add (name, tv) ->
* Environment.to_michelson_add (name, tv) w_env.pre_environment *)
| S_declaration (s, expr) ->
let tv = Combinators.Expression.get_type expr in
let%bind expr = translate_expression expr in
let%bind add = Compiler_environment.to_michelson_add (s, tv) w_env.pre_environment in
ok (seq [
i_comment "declaration" ;
seq [
i_comment "expr" ;
i_push_unit ; expr ; i_car ;
] ;
seq [
i_comment "env <- env . expr" ;
add ;
];
])
| S_assignment (s, expr) ->
let%bind expr = translate_expression expr in
let%bind set = Compiler_environment.to_michelson_set s w_env.pre_environment in
ok (seq [
i_comment "assignment" ;
seq [
i_comment "expr" ;
i_push_unit ; expr ; i_car ;
] ;
seq [
i_comment "env <- env . expr" ;
set ;
];
])
| S_cond (expr, a, b) ->
let%bind expr = translate_expression expr in
let%bind a' = translate_regular_block a in
let%bind b' = translate_regular_block b in
ok @@ (seq [
i_push_unit ;
expr ;
prim I_CAR ;
prim ~children:[seq [a'];seq [b']] I_IF ;
])
| S_if_none (expr, none, ((name, tv), some)) ->
let%bind expr = translate_expression expr in
let%bind none' = translate_regular_block none in
let%bind some' = translate_regular_block some in
let%bind add =
let env' = Environment.extend w_env.pre_environment in
Compiler_environment.to_michelson_add (name, tv) env' in
ok @@ (seq [
i_push_unit ; expr ; i_car ;
prim ~children:[
seq [none'] ;
seq [add ; some'] ;
] I_IF_NONE
])
| S_while (expr, block) ->
let%bind expr = translate_expression expr in
let%bind block' = translate_regular_block block in
let%bind restrict_block =
let env_while = (snd block).pre_environment in
Compiler_environment.to_michelson_restrict env_while in
ok @@ (seq [
i_push_unit ; expr ; i_car ;
prim ~children:[seq [
Compiler_environment.to_michelson_extend w_env.pre_environment;
block' ;
restrict_block ;
i_push_unit ; expr ; i_car]] I_LOOP ;
])
| S_patch (name, lrs, expr) ->
let%bind expr' = translate_expression expr in
let%bind (name_path, _) = Environment.get_path name w_env.pre_environment in
let path = name_path @ lrs in
let set_code = Compiler_environment.path_to_michelson_set path in
ok @@ seq [
i_push_unit ; expr' ; i_car ;
set_code ;
]
in
let%bind () =
let return code =
let%bind (Ex_ty pre_ty) = Compiler_environment.to_ty w_env.pre_environment in
let input_stack_ty = Stack.(pre_ty @: nil) in
let%bind (Ex_ty post_ty) = Compiler_environment.to_ty w_env.post_environment in
@ -510,14 +422,130 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
ok (fun () -> error (thunk "error parsing statement code")
(fun () -> error_message)
())) @@
Tezos_utils.Memory_proto_alpha.parse_michelson code
Tezos_utils.Memory_proto_alpha.parse_michelson_fail code
input_stack_ty output_stack_ty
in
ok ()
ok code
in
ok code
trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with
| S_environment_extend ->
return @@ Compiler_environment.to_michelson_extend w_env.pre_environment
| S_environment_restrict ->
let%bind code = Compiler_environment.to_michelson_restrict w_env.pre_environment in
return code
| S_environment_add _ ->
simple_fail "add not ready yet"
(* | S_environment_add (name, tv) ->
* Environment.to_michelson_add (name, tv) w_env.pre_environment *)
| S_declaration (s, expr) ->
let tv = Combinators.Expression.get_type expr in
let%bind expr = translate_expression expr in
let%bind add = Compiler_environment.to_michelson_add (s, tv) w_env.pre_environment in
return @@ seq [
i_comment "declaration" ;
seq [
i_comment "expr" ;
i_push_unit ; expr ; i_car ;
] ;
seq [
i_comment "env <- env . expr" ;
add ;
];
]
| S_assignment (s, expr) ->
let%bind expr = translate_expression expr in
let%bind set = Compiler_environment.to_michelson_set s w_env.pre_environment in
return @@ seq [
i_comment "assignment" ;
seq [
i_comment "expr" ;
i_push_unit ; expr ; i_car ;
] ;
seq [
i_comment "env <- env . expr" ;
set ;
];
]
| S_cond (expr, a, b) ->
let%bind expr = translate_expression expr in
let%bind a' = translate_regular_block a in
let%bind b' = translate_regular_block b in
return @@ seq [
i_push_unit ;
expr ;
prim I_CAR ;
prim ~children:[seq [a'];seq [b']] I_IF ;
]
| S_do expr -> (
match Combinators.Expression.get_content expr with
| E_constant ("FAILWITH" , [ fw ] ) -> (
let%bind fw' = translate_expression fw in
return @@ seq [
i_push_unit ;
fw' ;
i_car ;
i_failwith ;
]
)
| _ -> (
let%bind expr' = translate_expression expr in
return @@ seq [
i_push_unit ;
expr' ;
i_drop ;
]
)
)
| S_if_none (expr, none, ((name, tv), some)) ->
let%bind expr = translate_expression expr in
let%bind none' = translate_regular_block none in
let%bind some' = translate_regular_block some in
let%bind add =
let env' = Environment.extend w_env.pre_environment in
Compiler_environment.to_michelson_add (name, tv) env' in
return @@ seq [
i_push_unit ; expr ; i_car ;
prim ~children:[
seq [none'] ;
seq [add ; some'] ;
] I_IF_NONE
]
| S_while (expr, block) ->
let%bind expr = translate_expression expr in
let%bind block' = translate_regular_block block in
let%bind restrict_block =
let env_while = (snd block).pre_environment in
Compiler_environment.to_michelson_restrict env_while in
return @@ seq [
i_push_unit ; expr ; i_car ;
prim ~children:[seq [
Compiler_environment.to_michelson_extend w_env.pre_environment;
block' ;
restrict_block ;
i_push_unit ; expr ; i_car]] I_LOOP ;
]
| S_patch (name, lrs, expr) ->
let%bind expr' = translate_expression expr in
let%bind (name_path, _) = Environment.get_path name w_env.pre_environment in
let path = name_path @ lrs in
let set_code = Compiler_environment.path_to_michelson_set path in
let error =
let title () = "michelson type-checking patch" in
let content () =
let aux ppf = function
| `Left -> Format.fprintf ppf "left"
| `Right -> Format.fprintf ppf "right" in
Format.asprintf "Name path: %a\nSub path: %a\n"
PP_helpers.(list_sep aux (const " , ")) name_path
PP_helpers.(list_sep aux (const " , ")) lrs
in
error title content in
trace error @@
return @@ seq [
i_push_unit ; expr' ; i_car ;
set_code ;
]
and translate_regular_block ((b, env):block) : michelson result =
let aux prev statement =

6
src/ligo/compiler/compiler_type.ml
View File

@ -18,8 +18,10 @@ module Ty = struct
| Base_unit -> fail (not_comparable "unit")
| Base_bool -> fail (not_comparable "bool")
| Base_nat -> return nat_k
| Base_tez -> return tez_k
| Base_int -> return int_k
| Base_string -> return string_k
| Base_address -> return address_k
| Base_bytes -> return bytes_k
| Base_operation -> fail (not_comparable "operation")
@ -43,7 +45,9 @@ module Ty = struct
| Base_bool -> return bool
| Base_int -> return int
| Base_nat -> return nat
| Base_tez -> return tez
| Base_string -> return string
| Base_address -> return address
| Base_bytes -> return bytes
| Base_operation -> return operation
@ -113,7 +117,9 @@ let base_type : type_base -> O.michelson result =
| Base_bool -> ok @@ O.prim T_bool
| Base_int -> ok @@ O.prim T_int
| Base_nat -> ok @@ O.prim T_nat
| Base_tez -> ok @@ O.prim T_mutez
| Base_string -> ok @@ O.prim T_string
| Base_address -> ok @@ O.prim T_address
| Base_bytes -> ok @@ O.prim T_bytes
| Base_operation -> ok @@ O.prim T_operation

7
src/ligo/compiler/uncompiler.ml
View File

@ -29,10 +29,17 @@ 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
| (Mutez_t _), n ->
let%bind n =
generic_try (simple_error "too big to fit an int") @@
(fun () -> Int64.to_int @@ Alpha_context.Tez.to_mutez n) in
ok @@ D_nat n
| (Bool_t _), b ->
ok @@ D_bool b
| (String_t _), s ->
ok @@ D_string s
| (Address_t _), s ->
ok @@ D_string (Alpha_context.Contract.to_b58check s)
| (Unit_t _), () ->
ok @@ D_unit
| (Option_t _), None ->

18
src/ligo/contracts/coase.ligo
View File

@ -4,7 +4,6 @@ type card_pattern_id is nat
type card_pattern is record [
coefficient : tez ;
quantity : nat ;
last_id : nat ;
]
type card_patterns is map(card_pattern_id , card_pattern)
@ -18,6 +17,7 @@ type cards is map(card_id , card)
type storage_type is record [
cards : cards ;
card_patterns : card_patterns ;
next_id : nat ;
]
type action_buy_single is record [
@ -38,14 +38,24 @@ type action is
function buy_single(const action : action_buy_single ; const s : storage_type) : (list(operation) * storage_type) is
begin
const pattern : card_pattern = get_force(action.card_to_buy , s.card_patterns) ;
// Check funds
const card_pattern : card_pattern = get_force(action.card_to_buy , s.card_patterns) ;
const price : tez = card_pattern.coefficient * (card_pattern.quantity + 1n) ;
if (price > amount) then fail "Not enough money" else skip ;
// Administrative procedure
const operations : list(operation) = nil ;
pattern.quantity := pattern.quantity + 1n ;
// Increase quantity
card_pattern.quantity := card_pattern.quantity + 1n ;
const card_patterns : card_patterns = s.card_patterns ;
card_patterns[action.card_to_buy] := pattern ;
card_patterns[action.card_to_buy] := card_pattern ;
s.card_patterns := card_patterns ;
// Add card
const cards : cards = s.cards ;
cards[s.next_id] := record
card_owner = source ;
end ;
s.cards := cards ;
s.next_id := s.next_id + 1n ;
end with (operations , s)
function main(const action : action ; const s : storage_type) : (list(operation) * storage_type) is

26
src/ligo/contracts/record.ligo
View File

@ -8,11 +8,37 @@ const fb : foobar = record
bar = 0 ;
end
type abc is record
a : int ;
b : int ;
c : int ;
end
const abc : abc = record
a = 42 ;
b = 142 ;
c = 242 ;
end
const a : int = abc.a ;
const b : int = abc.b ;
const c : int = abc.c ;
function projection (const r : foobar) : int is
begin
skip
end with r.foo + r.bar
function modify (const r : foobar) : foobar is
block {
r.foo := 256 ;
} with r
function modify_abc (const r : abc) : abc is
block {
r.b := 2048 ;
} with r
type big_record is record
a : int ;
b : int ;

10
src/ligo/contracts/tuple.ligo
View File

@ -10,3 +10,13 @@ function projection (const tpl : foobar) : int is
type big_tuple is (int * int * int * int * int)
const br : big_tuple = (23, 23, 23, 23, 23)
type abc is (int * int * int)
function projection_abc (const tpl : abc) : int is
block { skip } with tpl.1
function modify_abc (const tpl : abc) : abc is
block {
tpl.1 := 2048 ;
} with tpl

17
src/ligo/main/main.ml
View File

@ -87,8 +87,17 @@ let easy_evaluate_typed_simplified (entry:string) (program:AST_Typed.program) :
let easy_evaluate_typed = trace_f_2_ez easy_evaluate_typed (thunk "easy evaluate typed")
let easy_run_typed
?(debug_mini_c = false) (entry:string)
?(debug_mini_c = false) ?amount (entry:string)
(program:AST_Typed.program) (input:AST_Typed.annotated_expression) : AST_Typed.annotated_expression result =
let%bind () =
let open Ast_typed in
let%bind (Declaration_constant (d , _)) = get_declaration_by_name program entry in
let%bind (arg_ty , _) =
trace_strong (simple_error "entry-point doesn't have a function type") @@
get_t_function @@ get_type_annotation d.annotated_expression in
Ast_typed.assert_type_value_eq (arg_ty , (Ast_typed.get_type_annotation input))
in
let%bind mini_c_main =
trace (simple_error "transpile mini_c entry") @@
transpile_entry program entry in
@ -106,7 +115,7 @@ let easy_run_typed
in
error title content in
trace error @@
Run_mini_c.run_entry mini_c_main mini_c_value in
Run_mini_c.run_entry ?amount mini_c_main mini_c_value in
let%bind typed_result =
let%bind main_result_type =
let%bind typed_main = Ast_typed.get_functional_entry program entry in
@ -117,7 +126,7 @@ let easy_run_typed
ok typed_result
let easy_run_typed_simplified
?(debug_mini_c = false) (entry:string)
?(debug_mini_c = false) ?amount (entry:string)
(program:AST_Typed.program) (input:Ast_simplified.annotated_expression) : Ast_simplified.annotated_expression result =
let%bind mini_c_main =
trace (simple_error "transpile mini_c entry") @@
@ -143,7 +152,7 @@ let easy_run_typed_simplified
in
error title content in
trace error @@
Run_mini_c.run_entry mini_c_main mini_c_value in
Run_mini_c.run_entry ?amount mini_c_main mini_c_value in
let%bind typed_result =
let%bind main_result_type =
let%bind typed_main = Ast_typed.get_functional_entry program entry in

8
src/ligo/main/run_mini_c.ml
View File

@ -3,7 +3,7 @@ open Mini_c
open Compiler.Program
open Memory_proto_alpha.Script_ir_translator
let run_aux (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_value result =
let run_aux ?amount (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_value result =
let Compiler.Program.{input;output;body} : compiled_program = program in
let (Ex_ty input_ty) = input in
let (Ex_ty output_ty) = output in
@ -18,7 +18,7 @@ let run_aux (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_
let open! Memory_proto_alpha.Script_interpreter in
let%bind (Item(output, Empty)) =
Trace.trace_tzresult_lwt (simple_error "error of execution") @@
Tezos_utils.Memory_proto_alpha.interpret descr (Item(input, Empty)) in
Tezos_utils.Memory_proto_alpha.interpret ?amount descr (Item(input, Empty)) in
ok (Ex_typed_value (output_ty, output))
let run_node (program:program) (input:Michelson.t) : Michelson.t result =
@ -29,7 +29,7 @@ let run_node (program:program) (input:Michelson.t) : Michelson.t result =
Tezos_utils.Memory_proto_alpha.unparse_michelson_data output_ty output in
ok output
let run_entry (entry:anon_function) (input:value) : value result =
let run_entry ?amount (entry:anon_function) (input:value) : value result =
let%bind compiled =
let error =
let title () = "compile entry" in
@ -40,7 +40,7 @@ let run_entry (entry:anon_function) (input:value) : value result =
trace error @@
translate_entry entry in
let%bind input_michelson = translate_value input in
let%bind ex_ty_value = run_aux compiled input_michelson in
let%bind ex_ty_value = run_aux ?amount compiled input_michelson in
let%bind (result : value) = Compiler.Uncompiler.translate_value ex_ty_value in
ok result

3
src/ligo/meta_michelson/contract.ml
View File

@ -245,8 +245,10 @@ module Types = struct
let bytes_k = Bytes_key None
let nat = Nat_t None
let tez = Mutez_t None
let int = Int_t None
let nat_k = Nat_key None
let tez_k = Mutez_key None
let int_k = Int_key None
let big_map k v = Big_map_t (k, v, None)
@ -260,6 +262,7 @@ module Types = struct
let string = String_t None
let string_k = String_key None
let address_k = Address_key None
let key = Key_t None

9
src/ligo/mini_c/PP.ml
View File

@ -6,12 +6,17 @@ let list_sep_d x = list_sep x (const " , ")
let space_sep ppf () = fprintf ppf " "
let lr = fun ppf -> function `Left -> fprintf ppf "L" | `Right -> fprintf ppf "R"
let type_base ppf : type_base -> _ = function
| Base_unit -> fprintf ppf "unit"
| Base_bool -> fprintf ppf "bool"
| Base_int -> fprintf ppf "int"
| Base_nat -> fprintf ppf "nat"
| Base_tez -> fprintf ppf "tez"
| Base_string -> fprintf ppf "string"
| Base_address -> fprintf ppf "address"
| Base_bytes -> fprintf ppf "bytes"
| Base_operation -> fprintf ppf "operation"
@ -109,10 +114,10 @@ and statement ppf ((s, _) : statement) = match s with
| S_environment_add (name, tv) -> fprintf ppf "add %s %a" name type_ tv
| S_declaration ass -> declaration ppf ass
| S_assignment ass -> assignment ppf ass
| S_do e -> fprintf ppf "do %a" expression e
| S_cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
| S_patch (r, path, e) ->
let aux = fun ppf -> function `Left -> fprintf ppf ".L" | `Right -> fprintf ppf ".R" in
fprintf ppf "%s%a := %a" r (list aux) path expression e
fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e
| S_if_none (expr, none, ((name, _), some)) -> fprintf ppf "if_none (%a) %a %s->%a" expression expr block none name block some
| S_while (e, b) -> fprintf ppf "while (%a) %a" expression e block b

1
src/ligo/mini_c/combinators_smart.ml
View File

@ -12,6 +12,7 @@ let statement s' env : statement =
| S_environment_restrict -> s', environment_wrap env (Environment.restrict env)
| S_environment_add (name, tv) -> s' , environment_wrap env (Environment.add (name , tv) env)
| S_cond _ -> s' , id_environment_wrap env
| S_do _ -> s' , id_environment_wrap env
| S_if_none _ -> s' , id_environment_wrap env
| S_while _ -> s' , id_environment_wrap env
| S_patch _ -> s' , id_environment_wrap env

5
src/ligo/mini_c/types.ml
View File

@ -5,8 +5,8 @@ type type_name = string
type type_base =
| Base_unit
| Base_bool
| Base_int | Base_nat
| Base_string | Base_bytes
| Base_int | Base_nat | Base_tez
| Base_string | Base_bytes | Base_address
| Base_operation
type type_value =
@ -84,6 +84,7 @@ and statement' =
| S_environment_add of (var_name * type_value)
| S_declaration of assignment (* First assignment *)
| S_assignment of assignment
| S_do of expression
| S_cond of expression * block * block
| S_patch of string * [`Left | `Right] list * expression
| S_if_none of expression * block * ((var_name * type_value) * block)

40
src/ligo/operators/operators.ml
View File

@ -24,6 +24,9 @@ module Simplify = struct
("get_force" , 2) ;
("size" , 1) ;
("int" , 1) ;
("amount" , 0) ;
("unit" , 0) ;
("source" , 0) ;
]
module Camligo = struct
@ -132,7 +135,10 @@ 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_tez ()), constant_2 s (t_bool ())) ;
(eq_2 (t_bytes ()), constant_2 s (t_bool ())) ;
(eq_2 (t_string ()), constant_2 s (t_bool ())) ;
(eq_2 (t_address ()), constant_2 s (t_bool ())) ;
]
let boolean_operator_2 : string -> typer = fun s -> very_same_2 s (t_bool ())
@ -211,6 +217,10 @@ module Typer = struct
predicate_0 , typer_constant ("UNIT", t_unit ())
]
let amount = "amount" , 0 , [
predicate_0 , typer_constant ("AMOUNT", t_tez ())
]
let transaction = "Operation.transaction" , 3 , [
true_3 , typer'_3 (
fun param contract amount ->
@ -236,12 +246,6 @@ module Typer = struct
)
]
(* 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 num_2 : typer_predicate =
let aux = fun a b ->
(type_value_eq (a , t_int ()) || type_value_eq (a , t_nat ())) &&
@ -252,6 +256,17 @@ module Typer = struct
num_2 , constant_2 "MOD" (t_nat ()) ;
]
let times = "TIMES" , 2 , [
(eq_2 (t_nat ()) , constant_2 "TIMES_NAT" (t_nat ())) ;
(num_2 , constant_2 "TIMES_INT" (t_int ())) ;
(
let aux a b =
(type_value_eq (a , t_nat ()) && type_value_eq (b , t_tez ())) ||
(type_value_eq (b , t_nat ()) && type_value_eq (a , t_tez ())) in
predicate_2 aux , constant_2 "TIMES_TEZ" (t_tez ())
) ;
]
let constant_typers =
let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in
Map.String.of_list
@ -261,10 +276,7 @@ module Typer = struct
("ADD_NAT" , t_nat ()) ;
("CONCAT" , t_string ()) ;
] ;
same_2 "TIMES" [
("TIMES_INT" , t_int ()) ;
("TIMES_NAT" , t_nat ()) ;
] ;
times ;
same_2 "DIV" [
("DIV_INT" , t_int ()) ;
("DIV_NAT" , t_nat ()) ;
@ -292,6 +304,7 @@ module Typer = struct
sender ;
source ;
unit ;
amount ;
transaction ;
get_contract ;
]
@ -324,6 +337,7 @@ module Compiler = struct
("SUB_NAT" , simple_binary @@ prim I_SUB) ;
("TIMES_INT" , simple_binary @@ prim I_MUL) ;
("TIMES_NAT" , simple_binary @@ prim I_MUL) ;
("TIMES_TEZ" , simple_binary @@ prim I_MUL) ;
("DIV_INT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
("DIV_NAT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
("MOD" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "MOD by 0") ; i_cdr]) ;
@ -344,8 +358,14 @@ module Compiler = struct
("GET_FORCE" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "GET_FORCE")]) ;
("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])) ;
("INT" , simple_unary @@ prim I_INT) ;
("CONS" , simple_binary @@ prim I_CONS) ;
("UNIT" , simple_constant @@ prim I_UNIT) ;
("AMOUNT" , simple_constant @@ prim I_AMOUNT) ;
("SOURCE" , simple_constant @@ prim I_SOURCE) ;
("SENDER" , simple_constant @@ prim I_SENDER) ;
( "MAP_UPDATE" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]) ;
]

28
src/ligo/simplify/pascaligo.ml
View File

@ -90,14 +90,16 @@ let rec simpl_expression (t:Raw.expr) : ae result =
| Component index -> Access_tuple (Z.to_int (snd index.value))
in
List.map aux @@ npseq_to_list path in
ok @@ make_e_a @@ E_accessor (var, path')
in
match t with
| EVar c ->
if c.value = "unit"
then ok @@ make_e_a @@ E_literal Literal_unit
else ok @@ make_e_a @@ E_variable c.value
| EVar c -> (
let c' = c.value in
match List.assoc_opt c' constants with
| None -> return @@ E_variable c.value
| Some 0 -> return @@ E_constant (c' , [])
| Some _ -> simple_fail "non nullary constant without parameters"
)
| ECall x -> (
let (name, args) = x.value in
let f = name.value in
@ -426,12 +428,18 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| NoneExpr _ -> simple_fail "no none assignments yet"
in
match a.lhs with
| Path (Name name) -> (
ok @@ I_assignment {name = name.value ; annotated_expression = value_expr}
)
| Path path -> (
let err_content () = Format.asprintf "%a" (PP_helpers.printer Parser.Pascaligo.ParserLog.print_path) path in
fail @@ (fun () -> error (thunk "no path assignments") err_content ())
let (name , path') = simpl_path path in
match List.rev_uncons_opt path' with
| None -> (
ok @@ I_assignment {name ; annotated_expression = value_expr}
)
| Some (hds , last) -> (
match last with
| Access_record property -> ok @@ I_record_patch (name , hds , [(property , value_expr)])
| Access_tuple index -> ok @@ I_tuple_patch (name , hds , [(index , value_expr)])
| _ -> simple_fail "no map assignment in this weird case yet"
)
)
| MapPath v -> (
let v' = v.value in

139
src/ligo/test/coase_tests.ml
View File

@ -14,49 +14,114 @@ let get_program =
ok program
)
let a_heap_ez ?value_type (content:(int * AST_Typed.ae) list) =
let open AST_Typed.Combinators in
let content =
let aux = fun (x, y) -> e_a_empty_nat x, y in
List.map aux content in
let value_type = match value_type, content with
| None, hd :: _ -> (snd hd).type_annotation
| Some s, _ -> s
| _ -> raise (Failure "no value type and heap empty when building heap") in
e_a_empty_map content (t_nat ()) value_type
open Ast_simplified
let ez lst =
let open AST_Typed.Combinators in
let value_type = t_pair
(t_int ())
(t_string ())
()
in
let lst' =
let aux (i, (j, s)) =
(i, e_a_empty_pair (e_a_empty_int j) (e_a_empty_string s)) in
List.map aux lst in
a_heap_ez ~value_type lst'
let card owner =
ez_e_a_record [
("card_owner" , owner) ;
]
let dummy n =
ez List.(
map (fun n -> (n, (n, string_of_int n)))
@@ tl
@@ range (n + 1)
)
let card_ty = t_record_ez [
("card_owner" , t_address) ;
]
let card_ez owner = card (e_a_address owner)
let make_cards assoc_lst =
let card_id_ty = t_nat in
e_a_map assoc_lst card_id_ty card_ty
let card_pattern (coeff , qtt) =
ez_e_a_record [
("coefficient" , coeff) ;
("quantity" , qtt) ;
]
let card_pattern_ty =
t_record_ez [
("coefficient" , t_tez) ;
("quantity" , t_nat) ;
]
let card_pattern_ez (coeff , qtt) =
card_pattern (e_a_tez coeff , e_a_nat qtt)
let make_card_patterns lst =
let card_pattern_id_ty = t_nat in
let assoc_lst = List.mapi (fun i x -> (e_a_nat i , x)) lst in
e_a_map assoc_lst card_pattern_id_ty card_pattern_ty
let storage cards_patterns cards next_id =
ez_e_a_record [
("cards" , cards) ;
("card_patterns" , cards_patterns) ;
("next_id" , next_id) ;
]
let storage_ez cps cs next_id =
storage (make_card_patterns cps) (make_cards cs) (e_a_nat next_id)
let cards_ez owner n =
List.mapi (fun i x -> (e_a_nat i , x))
@@ List.map card_ez
@@ List.map (Function.constant owner)
@@ List.range n
let first_owner =
let open Tezos_utils.Memory_proto_alpha in
let id = List.nth dummy_environment.identities 0 in
let kt = id.implicit_contract in
Alpha_context.Contract.to_b58check kt
let second_owner =
let open Tezos_utils.Memory_proto_alpha in
let id = List.nth dummy_environment.identities 1 in
let kt = id.implicit_contract in
Alpha_context.Contract.to_b58check kt
let basic a b cards next_id =
let card_patterns = List.map card_pattern_ez [
(100 , a) ;
(20 , b) ;
] in
storage_ez card_patterns cards next_id
let buy () =
let%bind program = get_program () in
let aux n =
let open AST_Typed.Combinators in
let input = dummy n in
let%bind result = easy_run_typed "is_empty" program input in
let expected = e_a_empty_bool (n = 0) in
AST_Typed.assert_value_eq (expected, result)
let%bind () =
let make_input = fun n ->
let buy_action = ez_e_a_record [
("card_to_buy" , e_a_nat 0) ;
] in
let storage = basic 100 1000 (cards_ez first_owner n) (2 * n) in
e_a_pair buy_action storage
in
let make_expected = fun n ->
let ops = e_a_list [] t_operation in
let storage =
let cards =
cards_ez first_owner n @
[(e_a_nat (2 * n) , card (e_a_address second_owner))]
in
basic 101 1000 cards ((2 * n) + 1) in
e_a_pair ops storage
in
let%bind () =
let%bind amount =
trace_option (simple_error "getting amount for run") @@
Tezos_utils.Memory_proto_alpha.Alpha_context.Tez.of_mutez @@ Int64.of_int 10000000000 in
let options = make_options ~amount () in
expect_n_pos_small ~options program "buy_single" make_input make_expected in
let%bind () =
let%bind amount =
trace_option (simple_error "getting amount for run") @@
Tezos_utils.Memory_proto_alpha.Alpha_context.Tez.of_mutez @@ Int64.of_int 0 in
let options = make_options ~amount () in
trace_strong (simple_error "could buy without money") @@
Assert.assert_fail
@@ expect_n_pos_small ~options program "buy_single" make_input make_expected in
ok ()
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 7 ; 12] in
ok ()
let main = "Coase (End to End)", [

39
src/ligo/test/integration_tests.ml
View File

@ -140,11 +140,31 @@ let record () : unit result =
let expected = record_ez_int ["foo" ; "bar"] 0 in
expect_evaluate program "fb" expected
in
let%bind () =
let%bind () = expect_evaluate program "a" (e_a_int 42) in
let%bind () = expect_evaluate program "b" (e_a_int 142) in
let%bind () = expect_evaluate program "c" (e_a_int 242) in
ok ()
in
let%bind () =
let make_input = record_ez_int ["foo" ; "bar"] in
let make_expected = fun n -> e_a_int (2 * n) in
expect_n program "projection" make_input make_expected
in
let%bind () =
let make_input = record_ez_int ["foo" ; "bar"] in
let make_expected = fun n -> ez_e_a_record [("foo" , e_a_int 256) ; ("bar" , e_a_int n) ] in
expect_n program "modify" make_input make_expected
in
let%bind () =
let make_input = record_ez_int ["a" ; "b" ; "c"] in
let make_expected = fun n -> ez_e_a_record [
("a" , e_a_int n) ;
("b" , e_a_int 2048) ;
("c" , e_a_int n)
] in
expect_n program "modify_abc" make_input make_expected
in
let%bind () =
let expected = record_ez_int ["a";"b";"c";"d";"e"] 23 in
expect_evaluate program "br" expected
@ -164,6 +184,21 @@ let tuple () : unit result =
let make_expected = fun n -> e_a_int (2 * n) in
expect_n program "projection" make_input make_expected
in
let%bind () =
let make_input = fun n -> ez [n ; 2 * n ; n] in
let make_expected = fun n -> e_a_int (2 * n) in
expect_n program "projection_abc" make_input make_expected
in
let%bind () =
let make_input = fun n -> ez [n ; n ; n] in
let make_expected = fun n -> ez [n ; 2048 ; n] in
expect program "modify_abc" (make_input 12) (make_expected 12)
in
let%bind () =
let make_input = fun n -> ez [n ; n ; n] in
let make_expected = fun n -> ez [n ; 2048 ; n] in
expect_n program "modify_abc" make_input make_expected
in
let%bind () =
let expected = ez [23 ; 23 ; 23 ; 23 ; 23] in
expect_evaluate program "br" expected
@ -372,6 +407,8 @@ let main = "Integration (End to End)", [
test "complex function" complex_function ;
test "variant" variant ;
test "variant matching" variant_matching ;
test "tuple" tuple ;
test "record" record ;
test "closure" closure ;
test "shared function" shared_function ;
test "shadow" shadow ;
@ -379,8 +416,6 @@ let main = "Integration (End to End)", [
test "bool" bool_expression ;
test "arithmetic" arithmetic ;
test "unit" unit_expression ;
test "record" record ;
test "tuple" tuple ;
test "option" option ;
test "map" map ;
test "list" list ;

2
src/ligo/test/test.ml
View File

@ -9,6 +9,6 @@ let () =
Transpiler_tests.main ;
Typer_tests.main ;
Heap_tests.main ;
(* Coase_tests.main ; *)
Coase_tests.main ;
] ;
()

26
src/ligo/test/test_helpers.ml
View File

@ -13,14 +13,22 @@ let test name f =
open Ast_simplified.Combinators
let expect program entry_point input expected =
type options = {
amount : Memory_proto_alpha.Alpha_context.Tez.t option ;
}
let make_options ?amount () = {
amount ;
}
let expect ?(options = make_options ()) program entry_point input expected =
let%bind result =
let run_error =
let title () = "expect run" in
let content () = Format.asprintf "Entry_point: %s" entry_point in
error title content in
trace run_error @@
Ligo.easy_run_typed_simplified entry_point program input in
Ligo.easy_run_typed_simplified ?amount:options.amount entry_point program input in
let expect_error =
let title () = "expect result" in
let content () = Format.asprintf "Expected %a, got %a"
@ -39,22 +47,22 @@ let expect_evaluate program entry_point expected =
let%bind result = Ligo.easy_evaluate_typed_simplified entry_point program in
Ast_simplified.assert_value_eq (expected , result)
let expect_n_aux lst program entry_point make_input make_expected =
let expect_n_aux ?options lst program entry_point make_input make_expected =
let aux n =
let input = make_input n in
let expected = make_expected n in
trace (simple_error ("expect_n " ^ (string_of_int n))) @@
let result = expect program entry_point input expected in
let result = expect ?options program entry_point input expected in
result
in
let%bind _ = bind_map_list aux lst in
ok ()
let expect_n = expect_n_aux [0 ; 2 ; 42 ; 163 ; -1]
let expect_n_pos = expect_n_aux [0 ; 2 ; 42 ; 163]
let expect_n_strict_pos = expect_n_aux [2 ; 42 ; 163]
let expect_n_pos_small = expect_n_aux [0 ; 2 ; 10]
let expect_n_strict_pos_small = expect_n_aux [2 ; 10]
let expect_n ?options = expect_n_aux ?options [0 ; 2 ; 42 ; 163 ; -1]
let expect_n_pos ?options = expect_n_aux ?options [0 ; 2 ; 42 ; 163]
let expect_n_strict_pos ?options = expect_n_aux ?options [2 ; 42 ; 163]
let expect_n_pos_small ?options = expect_n_aux ?options [0 ; 2 ; 10]
let expect_n_strict_pos_small ?options = expect_n_aux ?options [2 ; 10]
let expect_n_pos_mid = expect_n_aux [0 ; 2 ; 10 ; 33]
let expect_b program entry_point make_expected =

157
src/ligo/transpiler/transpiler.ml
View File

@ -19,7 +19,9 @@ let rec translate_type (t:AST.type_value) : type_value result =
| T_constant ("bool", []) -> ok (T_base Base_bool)
| T_constant ("int", []) -> ok (T_base Base_int)
| T_constant ("nat", []) -> ok (T_base Base_nat)
| T_constant ("tez", []) -> ok (T_base Base_tez)
| T_constant ("string", []) -> ok (T_base Base_string)
| T_constant ("address", []) -> ok (T_base Base_address)
| T_constant ("unit", []) -> ok (T_base Base_unit)
| T_constant ("operation", []) -> ok (T_base Base_operation)
| T_constant ("map", [key;value]) ->
@ -31,7 +33,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
| T_constant ("option", [o]) ->
let%bind o' = translate_type o in
ok (T_option o')
| T_constant (name, _) -> fail (fun () -> error (thunk "unrecognized constant") (fun () -> name) ())
| T_constant (name, _) -> fail (fun () -> error (thunk "unrecognized type constant") (fun () -> name) ())
| T_sum m ->
let node = Append_tree.of_list @@ list_of_map m in
let aux a b : type_value result =
@ -69,37 +71,43 @@ let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * [
Append_tree.exists_path aux node_tv in
let lr_path = List.map (fun b -> if b then `Right else `Left) path in
let%bind (_ , lst) =
let aux = fun (ty , acc) cur ->
let%bind (a , b) = Mini_c.get_t_pair ty in
let aux = fun (ty' , acc) cur ->
let%bind (a , b) =
let error =
let title () = "expected a pair" in
let content () = Format.asprintf "Big: %a.\tGot: %a\tFull path: %a\tSmall path: %a"
Mini_c.PP.type_ ty
Mini_c.PP.type_ ty'
PP_helpers.(list_sep bool (const ".")) path
PP_helpers.(list_sep lr (const ".")) (List.map snd acc)
in
error title content
in
trace_strong error @@
Mini_c.get_t_pair ty' in
match cur with
| `Left -> ok (a , (a , `Left) :: acc)
| `Right -> ok (b , (b , `Right) :: acc) in
| `Left -> ok (a , acc @ [(a , `Left)])
| `Right -> ok (b , acc @ [(b , `Right)])
in
bind_fold_list aux (ty , []) lr_path in
ok lst
let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -> (type_value * (type_value * [`Left | `Right]) list) result = fun ty tym ind ->
let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -> (type_value * [`Left | `Right]) list result = fun ty tym ind ->
let tys = kv_list_of_map tym in
let node_tv = Append_tree.of_list tys in
let leaf (i, _) : (type_value * (type_value * [`Left | `Right]) list) result =
if i = ind then (
ok (ty, [])
) else (
simple_fail "bad leaf"
) in
let node a b : (type_value * (type_value * [`Left | `Right]) list) result =
match%bind bind_lr (a, b) with
| `Left (t, acc) ->
let%bind (a, _) = Mini_c.get_t_pair t in
ok @@ (t, (a, `Left) :: acc)
| `Right (t, acc) -> (
let%bind (_, b) = Mini_c.get_t_pair t in
ok @@ (t, (b, `Right) :: acc)
) in
let error_content () =
let aux ppf (name, ty) = Format.fprintf ppf "%s -> %a" name PP.type_ ty in
Format.asprintf "(%a).%s" (PP.list_sep_d aux) tys ind in
trace_strong (fun () -> error (thunk "bad index in record (shouldn't happen here)") error_content ()) @@
Append_tree.fold_ne leaf node node_tv
let%bind path =
let aux (i , _) = i = ind in
trace_option (simple_error "no leaf with given index") @@
Append_tree.exists_path aux node_tv in
let lr_path = List.map (fun b -> if b then `Right else `Left) path in
let%bind (_ , lst) =
let aux = fun (ty , acc) cur ->
let%bind (a , b) = Mini_c.get_t_pair ty in
match cur with
| `Left -> ok (a , acc @ [(a , `Left)])
| `Right -> ok (b , acc @ [(b , `Right)] ) in
bind_fold_list aux (ty , []) lr_path in
ok lst
let rec translate_block env (b:AST.block) : block result =
let aux = fun (precs, env) instruction ->
@ -124,21 +132,30 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
let aux : ((AST.type_value * [`Left | `Right] list) as 'a) -> AST.access -> 'a result =
fun (prev, acc) cur ->
let%bind ty' = translate_type prev in
match cur with
| Access_tuple ind ->
let%bind ty_lst = AST.Combinators.get_t_tuple prev in
let%bind ty'_lst = bind_map_list translate_type ty_lst in
let%bind path = tuple_access_to_lr ty' ty'_lst ind in
let path' = List.map snd path in
ok (List.nth ty_lst ind, path' @ acc)
| Access_record prop ->
let%bind ty_map = AST.Combinators.get_t_record prev in
let%bind ty'_map = bind_map_smap translate_type ty_map in
let%bind (_, path) = record_access_to_lr ty' ty'_map prop in
let path' = List.map snd path in
ok (Map.String.find prop ty_map, path' @ acc)
match cur with
| Access_tuple ind ->
let%bind ty_lst = AST.Combinators.get_t_tuple prev in
let%bind ty'_lst = bind_map_list translate_type ty_lst in
let%bind path = tuple_access_to_lr ty' ty'_lst ind in
let path' = List.map snd path in
ok (List.nth ty_lst ind, acc @ path')
| Access_record prop ->
let%bind ty_map =
let error =
let title () = "accessing property on not a record" in
let content () = Format.asprintf "%s on %a in %a"
prop Ast_typed.PP.type_value prev Ast_typed.PP.instruction i in
error title content
in
trace error @@
AST.Combinators.get_t_record prev in
let%bind ty'_map = bind_map_smap translate_type ty_map in
let%bind path = record_access_to_lr ty' ty'_map prop in
let path' = List.map snd path in
ok (Map.String.find prop ty_map, acc @ path')
| Access_map _k -> simple_fail "no patch for map yet"
in
let%bind (_, path) = bind_fold_list aux (ty, []) s in
let%bind (_, path) = bind_fold_right_list aux (ty, []) s in
let%bind v' = translate_annotated_expression env v in
return (S_patch (r.type_name, path, v'))
)
@ -172,7 +189,10 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
let%bind body' = translate_block env' body in
return (S_while (expr', body'))
| I_skip -> ok []
| I_do _ae -> simple_fail "todo : do"
| I_do ae -> (
let%bind ae' = translate_annotated_expression env ae in
return @@ S_do ae'
)
and translate_literal : AST.literal -> value = fun l -> match l with
| Literal_bool b -> D_bool b
@ -181,6 +201,7 @@ and translate_literal : AST.literal -> value = fun l -> match l with
| Literal_tez n -> D_tez n
| Literal_bytes s -> D_bytes s
| Literal_string s -> D_string s
| Literal_address s -> D_string s
| Literal_unit -> D_unit
and transpile_small_environment : AST.small_environment -> Environment.Small.t result = fun x ->
@ -207,7 +228,10 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
ok @@ Combinators.Expression.make_tpl (expr, tv, env) in
let f = translate_annotated_expression env in
match ae.expression with
| E_failwith _ae -> simple_fail "todo : failwith"
| E_failwith ae -> (
let%bind ae' = translate_annotated_expression env ae in
return @@ E_constant ("FAILWITH" , [ae'])
)
| E_literal l -> return @@ E_literal (translate_literal l)
| E_variable name ->
let%bind tv =
@ -268,7 +292,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
| `Right -> "CDR" in
Combinators.Expression.make_tpl (E_constant (c, [pred]) , ty , env) in
let%bind tpl' = translate_annotated_expression env tpl in
let expr = List.fold_right' aux tpl' path in
let expr = List.fold_left aux tpl' path in
ok expr
| E_record m ->
let node = Append_tree.of_list @@ list_of_map m in
@ -282,36 +306,17 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
in
Append_tree.fold_ne (translate_annotated_expression env) aux node
| E_record_accessor (record, property) ->
let%bind translation = translate_annotated_expression env record in
let%bind record_type_map =
let error =
let title () =
Format.asprintf "Accessing field of %a, that has type %a, which isn't a record"
AST.PP.annotated_expression record AST.PP.type_value record.type_annotation in
let content () = "" in
error title content in
trace error @@
get_t_record record.type_annotation in
let node_tv = Append_tree.of_list @@ kv_list_of_map record_type_map in
let leaf (key, _) : expression result =
if property = key then (
ok translation
) else (
simple_fail "bad leaf"
) in
let node (a:expression result) b : expression result =
match%bind bind_lr (a, b) with
| `Left expr -> (
let%bind (tv, _) = Mini_c.get_t_pair @@ Expression.get_type expr in
return ~tv @@ E_constant ("CAR", [expr])
)
| `Right expr -> (
let%bind (_, tv) = Mini_c.get_t_pair @@ Expression.get_type expr in
return ~tv @@ E_constant ("CDR", [expr])
) in
let%bind expr =
trace_strong (simple_error "bad key in record (shouldn't happen here)") @@
Append_tree.fold_ne leaf node node_tv in
let%bind ty' = translate_type (get_type_annotation record) in
let%bind ty_smap = get_t_record (get_type_annotation record) in
let%bind ty'_smap = bind_map_smap translate_type ty_smap in
let%bind path = record_access_to_lr ty' ty'_smap property in
let aux = fun pred (ty, lr) ->
let c = match lr with
| `Left -> "CAR"
| `Right -> "CDR" in
Combinators.Expression.make_tpl (E_constant (c, [pred]) , ty , env) in
let%bind record' = translate_annotated_expression env record in
let expr = List.fold_left aux record' path in
ok expr
| E_constant (name, lst) ->
let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in (
@ -615,9 +620,15 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
| T_constant ("nat", []) ->
let%bind n = get_nat v in
return (E_literal (Literal_nat n))
| T_constant ("tez", []) ->
let%bind n = get_nat v in
return (E_literal (Literal_tez n))
| T_constant ("string", []) ->
let%bind n = get_string v in
return (E_literal (Literal_string n))
| T_constant ("address", []) ->
let%bind n = get_string v in
return (E_literal (Literal_address n))
| T_constant ("option", [o]) -> (
match%bind get_option v with
| None -> ok (e_a_empty_none o)

109
src/ligo/typer/typer.ml
View File

@ -127,21 +127,18 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
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 = [ I_do { expression = E_failwith fw } ] } -> (
| I.Match_bool { match_false = [] ; match_true = [ I_do { expression = E_failwith fw } ] }
| I.Match_bool { match_false = [ I_skip ] ; match_true = [ I_do { expression = E_failwith fw } ] } -> (
let%bind fw' = type_annotated_expression e fw in
let%bind mf' = type_block 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 mt' = [ O.I_do (
make_a_e
(E_failwith fw')
(t_unit ())
e
) ]
let assert_ = make_a_e
(E_constant ("ASSERT" , [ex' ; fw']))
(t_unit ())
e
in
let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in
return (O.I_matching (ex' , m'))
return (O.I_do assert_)
)
| _ -> (
let%bind m' = type_match type_block e ex'.type_annotation m in
@ -159,15 +156,56 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
match access with
| I.Access_record s ->
let%bind m = O.Combinators.get_t_record ty in
trace_option (simple_error "unbound record access in record_patch") @@
Map.String.find_opt s m
| Access_tuple i ->
let%bind ty =
trace_option (simple_error "unbound record access in record_patch") @@
Map.String.find_opt s m in
ok (ty , O.Access_record s)
| I.Access_tuple i ->
let%bind t = O.Combinators.get_t_tuple ty in
generic_try (simple_error "unbound tuple access in record_patch") @@
(fun () -> List.nth t i)
let%bind ty =
generic_try (simple_error "unbound tuple access in record_patch") @@
(fun () -> List.nth t i) in
ok (ty , O.Access_tuple i)
| I.Access_map ind ->
let%bind (k , v) = O.Combinators.get_t_map ty in
let%bind ind' = type_annotated_expression e ind in
let%bind () = Ast_typed.assert_type_value_eq (get_type_annotation ind' , k) in
ok (v , O.Access_map ind')
in
let%bind _assert = bind_fold_list aux ty.type_value (path @ [Access_record s]) in
ok @@ O.I_patch (tv, path @ [Access_record s], ae')
let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_record s]) in
ok @@ O.I_patch (tv, path', ae')
in
let%bind lst' = bind_map_list aux lst in
ok (e, lst')
| I_tuple_patch (r, path, lst) ->
let aux (s, ae) =
let%bind ae' = type_annotated_expression e ae in
let%bind ty =
trace_option (simple_error "unbound variable in tuple_patch") @@
Environment.get_opt r e in
let tv = O.{type_name = r ; type_value = ty.type_value} in
let aux ty access =
match access with
| I.Access_record s ->
let%bind m = O.Combinators.get_t_record ty in
let%bind ty =
trace_option (simple_error "unbound record access in tuple_patch") @@
Map.String.find_opt s m in
ok (ty , O.Access_record s)
| I.Access_tuple i ->
let%bind t = O.Combinators.get_t_tuple ty in
let%bind ty =
generic_try (simple_error "unbound tuple access in tuple_patch") @@
(fun () -> List.nth t i) in
ok (ty , O.Access_tuple i)
| I.Access_map ind ->
let%bind (k , v) = O.Combinators.get_t_map ty in
let%bind ind' = type_annotated_expression e ind in
let%bind () = Ast_typed.assert_type_value_eq (get_type_annotation ind' , k) in
ok (v , O.Access_map ind')
in
let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_tuple s]) in
ok @@ O.I_patch (tv, path', ae')
in
let%bind lst' = bind_map_list aux lst in
ok (e, lst')
@ -328,6 +366,8 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
return (E_literal (Literal_nat n)) (t_nat ())
| E_literal (Literal_tez n) ->
return (E_literal (Literal_tez n)) (t_tez ())
| E_literal (Literal_address s) ->
return (e_address s) (t_address ())
(* Tuple *)
| E_tuple lst ->
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
@ -351,6 +391,13 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
@@ (fun () -> SMap.find property r_tv) in
return (E_record_accessor (prev , property)) tv
)
| Access_map ae -> (
let%bind ae' = type_annotated_expression e ae in
let%bind (k , v) = get_t_map prev.type_annotation in
let%bind () =
Ast_typed.assert_type_value_eq (k , get_type_annotation ae') in
return (E_look_up (prev , ae')) v
)
in
trace (simple_error "accessing") @@
bind_fold_list aux e' path
@ -410,18 +457,22 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
ok (Some c') in
let%bind key_type =
let%bind opt =
let%bind sub =
bind_fold_list aux None
@@ List.map get_type_annotation
@@ List.map fst lst' in
trace_option (simple_error "empty map expression") opt
let%bind annot = bind_map_option get_t_map_key tv_opt in
trace (simple_error "untyped empty map expression") @@
O.merge_annotation annot sub
in
let%bind value_type =
let%bind opt =
let%bind sub =
bind_fold_list aux None
@@ List.map get_type_annotation
@@ List.map snd lst' in
trace_option (simple_error "empty map expression") opt
let%bind annot = bind_map_option get_t_map_value tv_opt in
trace (simple_error "untyped empty map expression") @@
O.merge_annotation annot sub
in
ok (t_map key_type value_type ())
in
@ -553,6 +604,7 @@ let untype_literal (l:O.literal) : I.literal result =
| Literal_int n -> ok (Literal_int n)
| Literal_string s -> ok (Literal_string s)
| Literal_bytes b -> ok (Literal_bytes b)
| Literal_address s -> ok (Literal_address s)
let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_expression) result =
let open I in
@ -643,8 +695,19 @@ and untype_instruction (i:O.instruction) : (I.instruction) result =
List.rev_uncons_opt p in
let%bind tl_name = match tl with
| Access_record n -> ok n
| Access_tuple _ -> simple_fail "last element of patch is tuple" in
ok @@ I_record_patch (s.type_name, hds, [tl_name, e'])
| Access_tuple _ -> simple_fail "last element of patch is tuple"
| Access_map _ -> simple_fail "last element of patch is map"
in
let%bind hds' = bind_map_list untype_access hds in
ok @@ I_record_patch (s.type_name, hds', [tl_name, e'])
and untype_access (a:O.access) : I.access result =
match a with
| Access_record n -> ok @@ I.Access_record n
| Access_tuple n -> ok @@ I.Access_tuple n
| Access_map n ->
let%bind n' = untype_annotated_expression n in
ok @@ I.Access_map n'
and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
let open I in