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

add environment to typed expression

Browse Source
This commit is contained in:
Galfour 2019-04-20 21:35:18 +00:00
parent b61869cb16
commit af6da6bfa0
9 changed files with 87 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -2,7 +2,7 @@ open Trace
open Types
let make_t type_value' simplified = { type_value' ; simplified }
let make_a_e expression type_annotation = { expression ; type_annotation ; dummy_field = () ; environment = Environment.dummy }
let make_a_e expression type_annotation environment = { expression ; type_annotation ; dummy_field = () ; environment }
let make_n_e name a_e = { name ; annotated_expression = a_e }
let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
@ -116,6 +116,20 @@ let ez_e_a_record r = make_a_e (ez_e_record r) (ez_t_record (List.map (fun (x, y
let e_a_map lst k v = make_a_e (e_map lst) (t_map k v ())
let e_a_list lst t = make_a_e (e_list lst) (t_list t ())
let e_a_empty_unit = e_a_unit Environment.empty
let e_a_empty_int n = e_a_int n Environment.empty
let e_a_empty_nat n = e_a_nat n Environment.empty
let e_a_empty_bool b = e_a_bool b Environment.empty
let e_a_empty_string s = e_a_string s Environment.empty
let e_a_empty_pair a b = e_a_pair a b Environment.empty
let e_a_empty_some s = e_a_some s Environment.empty
let e_a_empty_none t = e_a_none t Environment.empty
let e_a_empty_tuple lst = e_a_tuple lst Environment.empty
let e_a_empty_record r = e_a_record r Environment.empty
let e_a_empty_map lst k v = e_a_map lst k v Environment.empty
let e_a_empty_list lst t = e_a_list lst t Environment.empty
let ez_e_a_empty_record r = ez_e_a_record r Environment.empty
let get_a_int (t:annotated_expression) =
match t.expression with
| E_literal (Literal_int n) -> ok n
@ -132,7 +146,7 @@ let get_a_bool (t:annotated_expression) =
| _ -> simple_fail "not a bool"
open Environment
let env_sum_type ?(env = empty)
let env_sum_type ?(env = full_empty)
?(name = "a_sum_type")
(lst : (string * ele) list) =
add env name (make_t_ez_sum lst)

3
src/ligo/ast_typed/environment.ml
View File

@ -3,7 +3,8 @@ open Types
type ele = type_value
type t = full_environment
let empty : t = {
let empty = []
let full_empty : t = {
(* TODO: use maps *)
environment = [] ;
type_environment = [] ;

2
src/ligo/ligo.ml
View File

@ -115,7 +115,7 @@ let unparse_simplified_expr (e:AST_Simplified.annotated_expression) : string res
ok @@ Format.asprintf "%a" AST_Simplified.PP.annotated_expression e
let type_ (p:AST_Simplified.program) : AST_Typed.program result = Typer.type_program p
let type_expression ?(env:Typer.Environment.t = Typer.Environment.empty)
let type_expression ?(env:Typer.Environment.t = Typer.Environment.full_empty)
(e:AST_Simplified.annotated_expression) : AST_Typed.annotated_expression result =
Typer.type_annotated_expression env e
let untype_expression (e:AST_Typed.annotated_expression) : AST_Simplified.annotated_expression result = Typer.untype_annotated_expression e

10
src/ligo/test/heap_tests.ml
View File

@ -15,13 +15,13 @@ let get_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_nat x, y in
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_map content (t_nat ()) value_type
e_a_empty_map content (t_nat ()) value_type
let ez lst =
let open AST_Typed.Combinators in
@ -32,7 +32,7 @@ let ez lst =
in
let lst' =
let aux (i, (j, s)) =
(i, e_a_pair (e_a_int j) (e_a_string s)) in
(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'
@ -49,7 +49,7 @@ let is_empty () : unit result =
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_bool (n = 0) in
let expected = e_a_empty_bool (n = 0) in
AST_Typed.assert_value_eq (expected, result)
in
let%bind _ = bind_list
@ -67,7 +67,7 @@ let get_top () : unit result =
| 0, _ -> ok ()
| _, result ->
let%bind result' = result in
let expected = e_a_pair (e_a_int 1) (e_a_string "1") in
let expected = e_a_empty_pair (e_a_empty_int 1) (e_a_empty_string "1") in
AST_Typed.assert_value_eq (expected, result')
in
let%bind _ = bind_list

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

@ -29,7 +29,7 @@ let complex_function () : unit result =
let%bind program = type_file "./contracts/function-complex.ligo" in
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
@ -46,9 +46,9 @@ let closure () : unit result =
let%bind _foo = trace (simple_error "test foo") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_typed "foo" program input in
let expected = e_a_int ( 2 * n ) in
let expected = e_a_empty_int ( 2 * n ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@ -57,9 +57,9 @@ let closure () : unit result =
let%bind _toto = trace (simple_error "toto") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_typed "toto" program input in
let expected = e_a_int ( 4 * n ) in
let expected = e_a_empty_int ( 4 * n ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@ -72,9 +72,9 @@ let shadow () : unit result =
let%bind _foo = trace (simple_error "test foo") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_typed "foo" program input in
let expected = e_a_int 0 in
let expected = e_a_empty_int 0 in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@ -87,9 +87,9 @@ let higher_order () : unit result =
let%bind _foo = trace (simple_error "test foo") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_typed "foobar" program input in
let expected = e_a_int ( n ) in
let expected = e_a_empty_int ( n ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@ -102,9 +102,9 @@ let shared_function () : unit result =
let%bind _inc = trace (simple_error "test inc") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_typed "inc" program input in
let expected = e_a_int ( n + 1 ) in
let expected = e_a_empty_int ( n + 1 ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@ -113,9 +113,9 @@ let shared_function () : unit result =
let%bind _double_inc = trace (simple_error "test double_inc") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_typed "double_inc" program input in
let expected = e_a_int ( n + 2 ) in
let expected = e_a_empty_int ( n + 2 ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@ -124,9 +124,9 @@ let shared_function () : unit result =
let%bind _foo = trace (simple_error "test foo") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_typed "foo" program input in
let expected = e_a_int ( 2 * n + 3 ) in
let expected = e_a_empty_int ( 2 * n + 3 ) in
AST_Typed.assert_value_eq (expected, result)
in
bind_list
@ -139,7 +139,7 @@ let bool_expression () : unit result =
let aux (name, f) =
let aux b =
let open AST_Typed.Combinators in
let input = e_a_bool b in
let input = e_a_empty_bool b in
let%bind result = easy_run_typed name program input in
let%bind result' =
trace (simple_error "bad result") @@
@ -165,7 +165,7 @@ let arithmetic () : unit result =
let aux (name, f) =
let aux n =
let open AST_Typed.Combinators in
let input = if name = "int_op" then e_a_nat n else e_a_int n in
let input = if name = "int_op" then e_a_empty_nat n else e_a_empty_int n in
let%bind result = easy_run_typed name program input in
AST_Typed.assert_value_eq (f n, result)
in
@ -178,10 +178,10 @@ let arithmetic () : unit result =
bind_list
@@ List.map aux
@@ [
("plus_op", fun n -> e_a_int (n + 42)) ;
("minus_op", fun n -> e_a_int (n - 42)) ;
("times_op", fun n -> e_a_int (n * 42)) ;
("int_op", fun n -> e_a_int n) ;
("plus_op", fun n -> e_a_empty_int (n + 42)) ;
("minus_op", fun n -> e_a_empty_int (n - 42)) ;
("times_op", fun n -> e_a_empty_int (n * 42)) ;
("int_op", fun n -> e_a_empty_int n) ;
] in
ok ()
@ -204,7 +204,7 @@ let include_ () : unit result =
let record_ez_int names n =
let open AST_Typed.Combinators in
ez_e_a_record @@ List.map (fun x -> x, e_a_int n) names
ez_e_a_empty_record @@ List.map (fun x -> x, e_a_empty_int n) names
let multiple_parameters () : unit result =
let%bind program = type_file "./contracts/multiple-parameters.ligo" in
@ -239,7 +239,7 @@ let record () : unit result =
let aux n =
let input = record_ez_int ["foo";"bar"] n in
let%bind result = easy_run_typed "projection" program input in
let expect = AST_Typed.Combinators.e_a_int (2 * n) in
let expect = AST_Typed.Combinators.e_a_empty_int (2 * n) in
AST_Typed.assert_value_eq (expect, result)
in
bind_list @@ List.map aux [0 ; -42 ; 144]
@ -255,7 +255,7 @@ let tuple () : unit result =
let%bind program = type_file "./contracts/tuple.ligo" in
let ez n =
let open AST_Typed.Combinators in
e_a_tuple (List.map e_a_int n) in
e_a_empty_tuple (List.map e_a_empty_int n) in
let%bind _foobar =
trace (simple_error "foobar") (
let%bind result = easy_evaluate_typed "fb" program in
@ -267,7 +267,7 @@ let tuple () : unit result =
let aux n =
let input = ez [n ; n] in
let%bind result = easy_run_typed "projection" program input in
let expect = AST_Typed.Combinators.e_a_int (2 * n) in
let expect = AST_Typed.Combinators.e_a_empty_int (2 * n) in
AST_Typed.assert_value_eq (expect, result)
in
bind_list @@ List.map aux [0 ; -42 ; 144]
@ -285,12 +285,12 @@ let option () : unit result =
let open AST_Typed.Combinators in
let%bind _some = trace (simple_error "some") @@
let%bind result = easy_evaluate_typed "s" program in
let expect = e_a_some (e_a_int 42) in
let expect = e_a_empty_some (e_a_empty_int 42) in
AST_Typed.assert_value_eq (expect, result)
in
let%bind _none = trace (simple_error "none") @@
let%bind result = easy_evaluate_typed "n" program in
let expect = e_a_none (t_int ()) in
let expect = e_a_empty_none (t_int ()) in
AST_Typed.assert_value_eq (expect, result)
in
ok ()
@ -299,14 +299,14 @@ let map () : unit result =
let%bind program = type_file "./contracts/map.ligo" in
let ez lst =
let open AST_Typed.Combinators in
let lst' = List.map (fun (x, y) -> e_a_int x, e_a_int y) lst in
e_a_map lst' (t_int ()) (t_int ())
let lst' = List.map (fun (x, y) -> e_a_empty_int x, e_a_empty_int y) lst in
e_a_empty_map lst' (t_int ()) (t_int ())
in
let%bind _get_force = trace (simple_error "get_force") @@
let aux n =
let input = ez [(23, n) ; (42, 4)] in
let%bind result = easy_run_typed "gf" program input in
let expect = AST_Typed.Combinators.(e_a_int n) in
let expect = AST_Typed.Combinators.(e_a_empty_int n) in
AST_Typed.assert_value_eq (expect, result)
in
bind_map_list aux [0 ; 42 ; 51 ; 421 ; -3]
@ -315,7 +315,7 @@ let map () : unit result =
let aux n =
let input = ez List.(map (fun x -> (x, x)) @@ range n) in
let%bind result = easy_run_typed "size_" program input in
let expect = AST_Typed.Combinators.(e_a_nat n) in
let expect = AST_Typed.Combinators.(e_a_empty_nat n) in
AST_Typed.assert_value_eq (expect, result)
in
bind_map_list aux [1 ; 10 ; 3]
@ -329,7 +329,7 @@ let map () : unit result =
let aux n =
let input =
let m = ez [(23, 0) ; (42, 0)] in
AST_Typed.Combinators.(e_a_tuple [ e_a_int n ; m ])
AST_Typed.Combinators.(e_a_empty_tuple [ e_a_empty_int n ; m ])
in
let%bind result = easy_run_typed "set_" program input in
let expect = ez [(23, n) ; (42, 0)] in
@ -341,7 +341,7 @@ let map () : unit result =
let aux n =
let input = ez [(23, n) ; (42, 4)] in
let%bind result = easy_run_typed "get" program input in
let expect = AST_Typed.Combinators.(e_a_some @@ e_a_int 4) in
let expect = AST_Typed.Combinators.(e_a_empty_some @@ e_a_empty_int 4) in
AST_Typed.assert_value_eq (expect, result)
in
bind_map_list aux [0 ; 42 ; 51 ; 421 ; -3]
@ -363,14 +363,14 @@ let list () : unit result =
let%bind program = type_file "./contracts/list.ligo" in
let ez lst =
let open AST_Typed.Combinators in
let lst' = List.map e_a_int lst in
e_a_list lst' (t_int ())
let lst' = List.map e_a_empty_int lst in
e_a_empty_list lst' (t_int ())
in
let%bind _size = trace (simple_error "size") @@
let aux n =
let input = ez (List.range n) in
let%bind result = easy_run_typed "size_" program input in
let expect = AST_Typed.Combinators.(e_a_nat n) in
let expect = AST_Typed.Combinators.(e_a_empty_nat n) in
AST_Typed.assert_value_eq (expect, result)
in
bind_map_list aux [1 ; 10 ; 3]
@ -391,7 +391,7 @@ let condition () : unit result =
let%bind program = type_file "./contracts/condition.ligo" in
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
@ -408,9 +408,9 @@ let loop () : unit result =
let%bind _dummy = trace (simple_error "dummy") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_nat n in
let input = e_a_empty_nat n in
let%bind result = easy_run_typed "dummy" program input in
let expected = e_a_nat n in
let expected = e_a_empty_nat n in
AST_Typed.assert_value_eq (expected, result)
in
let%bind _ = bind_list
@ -421,9 +421,9 @@ let loop () : unit result =
let%bind _counter = trace (simple_error "counter") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_nat n in
let input = e_a_empty_nat n in
let%bind result = easy_run_typed "counter" program input in
let expected = e_a_nat n in
let expected = e_a_empty_nat n in
AST_Typed.assert_value_eq (expected, result)
in
let%bind _ = bind_list
@ -434,9 +434,9 @@ let loop () : unit result =
let%bind _sum = trace (simple_error "sum") @@
let aux n =
let open AST_Typed.Combinators in
let input = e_a_nat n in
let input = e_a_empty_nat n in
let%bind result = easy_run_typed "sum" program input in
let expected = e_a_nat (n * (n + 1) / 2) in
let expected = e_a_empty_nat (n * (n + 1) / 2) in
AST_Typed.assert_value_eq (expected, result)
in
let%bind _ = bind_list
@ -452,7 +452,7 @@ let matching () : unit result =
let%bind _bool =
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_typed "match_bool" program input in
let%bind result' =
trace (simple_error "bad result") @@
@ -467,7 +467,7 @@ let matching () : unit result =
let%bind _expr_bool =
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_typed "match_expr_bool" program input in
let%bind result' =
trace (simple_error "bad result") @@
@ -483,8 +483,8 @@ let matching () : unit result =
let aux n =
let open AST_Typed.Combinators in
let input = match n with
| Some s -> e_a_some (e_a_int s)
| None -> e_a_none (t_int ()) in
| Some s -> e_a_empty_some (e_a_empty_int s)
| None -> e_a_empty_none (t_int ()) in
let%bind result = easy_run_typed "match_option" program input in
let%bind result' =
trace (simple_error "bad result") @@
@ -503,7 +503,7 @@ let declarations () : unit result =
let%bind program = type_file "./contracts/declarations.ligo" in
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
@ -519,7 +519,7 @@ let quote_declaration () : unit result =
let%bind program = type_file "./contracts/quote-declaration.ligo" in
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
@ -535,7 +535,7 @@ let quote_declarations () : unit result =
let%bind program = type_file "./contracts/quote-declarations.ligo" in
let aux n =
let open AST_Typed.Combinators in
let input = e_a_int n in
let input = e_a_empty_int n in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
@ -551,9 +551,9 @@ let counter_contract () : unit result =
let%bind program = type_file "./contracts/counter.ligo" in
let aux n =
let open AST_Typed.Combinators in
let input = e_a_pair (e_a_int n) (e_a_int 42) in
let input = e_a_empty_pair (e_a_empty_int n) (e_a_empty_int 42) in
let%bind result = easy_run_main_typed program input in
let expected = e_a_pair (e_a_list [] (t_int ())) (e_a_int (42 + n)) in
let expected = e_a_empty_pair (e_a_empty_list [] (t_int ())) (e_a_empty_int (42 + n)) in
AST_Typed.assert_value_eq (result, expected)
in
let%bind _ = bind_list

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

@ -16,7 +16,7 @@ let integration () : unit result =
let%bind simpl = Ligo.Simplify_multifix.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_int (42 + 127), result)
Ligo.AST_Typed.assert_value_eq (Ligo.AST_Typed.Combinators.e_a_empty_int (42 + 127), result)
let main = "Multifix", [
test "basic" basic ;

4
src/ligo/test/typer_tests.ml
View File

@ -10,7 +10,7 @@ let int () : unit result =
let open Combinators in
let pre = ae @@ e_int 32 in
let open Typer in
let e = Environment.empty in
let e = Environment.full_empty in
let%bind post = type_annotated_expression e pre in
let open! Typed in
let open Combinators in
@ -18,7 +18,7 @@ let int () : unit result =
ok ()
module TestExpressions = struct
let test_expression ?(env = Typer.Environment.empty)
let test_expression ?(env = Typer.Environment.full_empty)
(expr : expression)
(test_expected_ty : Typed.tv) =
let open Typer in

8
src/ligo/transpiler.ml
View File

@ -314,7 +314,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
let aux : expression result -> (AST.ae * AST.ae) -> expression result = fun prev (k, v) ->
let%bind prev' = prev in
let%bind (k', v') =
let v' = e_a_some v in
let v' = e_a_some v ae.environment in
bind_map_pair (translate_annotated_expression env) (k, v') in
return @@ E_constant ("UPDATE", [k' ; v' ; prev'])
in
@ -489,7 +489,7 @@ let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result =
let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression result =
let open! AST in
let return e = ok (make_a_e e t) in
let return e = ok (make_a_e e t Environment.empty) in
match t.type_value' with
| T_constant ("unit", []) ->
let%bind () = get_unit v in
@ -508,10 +508,10 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
return (E_literal (Literal_string n))
| T_constant ("option", [o]) -> (
match%bind get_option v with
| None -> ok (e_a_none o)
| None -> ok (e_a_none o Environment.empty)
| Some s ->
let%bind s' = untranspile s o in
ok (e_a_some s')
ok (e_a_some s' Environment.empty)
)
| T_constant ("map", [k_ty;v_ty]) -> (
let%bind lst = get_map v in

8
src/ligo/typer.ml
View File

@ -61,7 +61,7 @@ let rec type_program (p:I.program) : O.program result =
in
let%bind (_, lst) =
trace (fun () -> program_error p ()) @@
bind_fold_list aux (Environment.empty, []) p in
bind_fold_list aux (Environment.full_empty, []) p in
ok @@ List.rev lst
and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
@ -225,14 +225,14 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
return (T_constant(cst, lst'))
and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.annotated_expression result =
and type_annotated_expression : environment -> I.annotated_expression -> O.annotated_expression result = fun e ae ->
let%bind tv_opt = match ae.type_annotation with
| None -> ok None
| Some s -> let%bind r = evaluate_type e s in ok (Some r) in
let check tv = O.(merge_annotation tv_opt (Some tv)) in
let return e tv =
let return expr tv =
let%bind type_annotation = check tv in
ok @@ make_a_e e type_annotation in
ok @@ make_a_e expr type_annotation e.environment in
match ae.expression with
(* Basic *)
| E_variable name ->