more tests

This commit is contained in:
Galfour 2019-03-26 08:36:22 +00:00
parent 043387ec14
commit 1fe74323be
8 changed files with 132 additions and 18 deletions

View File

@ -166,6 +166,15 @@ module PP = struct
fprintf ppf "%s := %a" name annotated_expression ae fprintf ppf "%s := %a" name annotated_expression ae
| Matching (ae, m) -> | Matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae matching m fprintf ppf "match %a with %a" annotated_expression ae matching m
let declaration ppf (d:declaration) = match d with
| Type_declaration {type_name ; type_expression = te} ->
fprintf ppf "type %s = %a" type_name type_expression te
| Constant_declaration {name ; annotated_expression = ae} ->
fprintf ppf "const %s = %a" name annotated_expression ae
let program ppf (p:program) =
fprintf ppf "%a" (list_sep declaration) p
end end
module Simplify = struct module Simplify = struct

View File

@ -0,0 +1,7 @@
function main (const i : int) : int is
var j : int := 0 ;
var k : int := 1 ;
begin
j := k + i ;
k := i + j ;
end with (k + j)

View File

@ -0,0 +1,8 @@
function foo (const input : int) : int is begin
skip
end with (input + 42)
function main (const i : int) : int is
begin
skip
end with i + foo (i)

View File

@ -0,0 +1,13 @@
function foo (const input : int) : int is begin
skip
end with (input + 23)
function bar (const input : int) : int is begin
skip
end with (input + 51)
function main (const i : int) : int is
begin
skip
end with foo (i) + bar (i)

View File

@ -167,8 +167,10 @@ module Assert = struct
| true -> ok () | true -> ok ()
| false -> simple_fail msg | false -> simple_fail msg
let assert_equal_int ?(msg="not equal int") a b = let assert_equal_int ?msg expected actual =
assert_true ~msg (a = b) let default = Format.asprintf "Not equal int : expected %d, got %d" expected actual in
let msg = Option.unopt ~default msg in
assert_true ~msg (expected = actual)
let assert_list_size ?(msg="lst doesn't have the right size") lst n = let assert_list_size ?(msg="lst doesn't have the right size") lst n =
assert_true ~msg List.(length lst = n) assert_true ~msg List.(length lst = n)

View File

@ -11,7 +11,9 @@ module Transpiler = Transpiler
open Ligo_helpers.Trace open Ligo_helpers.Trace
let parse_file (source:string) : AST_Raw.t result = let parse_file (source:string) : AST_Raw.t result =
let channel = open_in source in let%bind channel =
generic_try (simple_error "error opening file") @@
(fun () -> open_in source) in
let lexbuf = Lexing.from_channel channel in let lexbuf = Lexing.from_channel channel in
let Lexer.{read ; _} = let Lexer.{read ; _} =
Lexer.open_token_stream None in Lexer.open_token_stream None in
@ -91,9 +93,14 @@ let transpile_value ?(env:Mini_c.Environment.t = Mini_c.Environment.empty)
let untranspile_value (v : Mini_c.value) (e:AST_Typed.type_value) : AST_Typed.annotated_expression result = let untranspile_value (v : Mini_c.value) (e:AST_Typed.type_value) : AST_Typed.annotated_expression result =
Transpiler.untranspile v e Transpiler.untranspile v e
let type_file (path:string) : AST_Typed.program result = let type_file ?(debug_simplify = false) (path:string) : AST_Typed.program result =
let%bind raw = parse_file path in let%bind raw = parse_file path in
let%bind simpl = simplify raw in let%bind simpl =
trace (simple_error "simplifying") @@
simplify raw in
(if debug_simplify then
Format.printf "Simplified : %a\n%!" AST_Simplified.PP.program simpl
) ;
let%bind typed = let%bind typed =
trace (simple_error "typing") @@ trace (simple_error "typing") @@
type_ simpl in type_ simpl in

View File

@ -25,10 +25,8 @@ let function_ () : unit result =
let%bind _ = easy_run_main "./contracts/function.ligo" "2" in let%bind _ = easy_run_main "./contracts/function.ligo" "2" in
ok () ok ()
let declarations () : unit result = let complex_function () : unit result =
let%bind program = type_file "./contracts/declarations.ligo" in let%bind program = type_file ~debug_simplify:true "./contracts/function-complex.ligo" in
Format.printf "toto\n%!" ;
Printf.printf "toto\n%!" ;
let aux n = let aux n =
let open AST_Typed.Combinators in let open AST_Typed.Combinators in
let input = a_int n in let input = a_int n in
@ -36,15 +34,67 @@ let declarations () : unit result =
let%bind result' = let%bind result' =
trace (simple_error "bad result") @@ trace (simple_error "bad result") @@
get_a_int result in get_a_int result in
Assert.assert_equal_int result' (42 + n) Assert.assert_equal_int (3 * n + 2) result'
in in
let%bind _ = bind_list let%bind _ = bind_list
@@ List.map aux @@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in @@ [0 ; 2 ; 42 ; 163 ; -1] in
ok () ok ()
let declarations () : unit result =
let%bind program = type_file "./contracts/declarations.ligo" in
let aux n =
let open AST_Typed.Combinators in
let input = a_int n in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
get_a_int result in
Assert.assert_equal_int (42 + n) result'
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
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 = a_int n in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
get_a_int result in
Assert.assert_equal_int result' (42 + 2 * n)
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
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 = a_int n in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
get_a_int result in
Assert.assert_equal_int result' (74 + 2 * n)
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let main = "Integration (End to End)", [ let main = "Integration (End to End)", [
test "basic" basic ; test "basic" basic ;
test "function" function_ ; test "function" function_ ;
test "complex function" complex_function ;
test "declarations" declarations ; test "declarations" declarations ;
test "quote declaration" quote_declaration ;
test "quote declarations" quote_declarations ;
] ]

View File

@ -60,13 +60,23 @@ module Errors = struct
let full = Format.asprintf "%s in %a" n Environment.PP.type_ e in let full = Format.asprintf "%s in %a" n Environment.PP.type_ e in
error title full error title full
let unbound_variable (e:environment) (n:string) =
let title = "unbound variable" in
let full = Format.asprintf "%s in %a" n Environment.PP.value e in
error title full
let unrecognized_constant (n:string) = let unrecognized_constant (n:string) =
let title = "unrecognized constant" in let title = "unrecognized constant" in
let full = n in let full = n in
error title full error title full
let constant_declaration_error (name:string) =
error "typing constant declaration" name
end end
open Errors open Errors
let rec type_program (p:I.program) : O.program result = let rec type_program (p:I.program) : O.program result =
let aux (e, acc:(environment * O.declaration list)) (d:I.declaration) = let aux (e, acc:(environment * O.declaration list)) (d:I.declaration) =
let%bind (e', d') = type_declaration e d in let%bind (e', d') = type_declaration e d in
@ -74,7 +84,9 @@ let rec type_program (p:I.program) : O.program result =
| None -> ok (e', acc) | None -> ok (e', acc)
| Some d' -> ok (e', d' :: acc) | Some d' -> ok (e', d' :: acc)
in in
let%bind (_, lst) = bind_fold_list aux (Environment.empty, []) p in let%bind (_, lst) =
trace (simple_error "typing program") @@
bind_fold_list aux (Environment.empty, []) p in
ok @@ List.rev lst ok @@ List.rev lst
and type_declaration env : I.declaration -> (environment * O.declaration option) result = function and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
@ -83,17 +95,23 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
let env' = Environment.add_type env type_name tv in let env' = Environment.add_type env type_name tv in
ok (env', None) ok (env', None)
| Constant_declaration {name;annotated_expression} -> | Constant_declaration {name;annotated_expression} ->
let%bind ae' = type_annotated_expression env annotated_expression in let%bind ae' =
trace (constant_declaration_error name) @@
type_annotated_expression env annotated_expression in
let env' = Environment.add env name ae'.type_annotation in let env' = Environment.add env name ae'.type_annotation in
ok (env', Some (O.Constant_declaration {name;annotated_expression=ae'})) ok (env', Some (O.Constant_declaration {name;annotated_expression=ae'}))
and type_block (e:environment) (b:I.block) : O.block result = and type_block_full (e:environment) (b:I.block) : (O.block * environment) result =
let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) = let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) =
let%bind (e', i') = type_instruction e i in let%bind (e', i') = type_instruction e i in
ok (e', i' :: acc) ok (e', i' :: acc)
in in
let%bind (_, lst) = bind_fold_list aux (e, []) b in let%bind (e', lst) = bind_fold_list aux (e, []) b in
ok @@ List.rev lst ok @@ (List.rev lst, e')
and type_block (e:environment) (b:I.block) : O.block result =
let%bind (block, _) = type_block_full e b in
ok block
and type_instruction (e:environment) : I.instruction -> (environment * O.instruction) result = function and type_instruction (e:environment) : I.instruction -> (environment * O.instruction) result = function
| Skip -> ok (e, O.Skip) | Skip -> ok (e, O.Skip)
@ -216,7 +234,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
(* Basic *) (* Basic *)
| Variable name -> | Variable name ->
let%bind tv' = let%bind tv' =
trace_option (simple_error "var not in env") trace_option (unbound_variable e name)
@@ Environment.get e name in @@ Environment.get e name in
let%bind type_annotation = check tv' in let%bind type_annotation = check tv' in
ok O.{expression = Variable name ; type_annotation} ok O.{expression = Variable name ; type_annotation}
@ -286,8 +304,8 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind input_type = evaluate_type e input_type in let%bind input_type = evaluate_type e input_type in
let%bind output_type = evaluate_type e output_type in let%bind output_type = evaluate_type e output_type in
let e' = Environment.add e binder input_type in let e' = Environment.add e binder input_type in
let%bind result = type_annotated_expression e' result in let%bind (body, e'') = type_block_full e' body in
let%bind body = type_block e' body in let%bind result = type_annotated_expression e'' result in
let%bind type_annotation = check @@ make_t_function (input_type, output_type) in let%bind type_annotation = check @@ make_t_function (input_type, output_type) in
ok O.{expression = Lambda {binder;input_type;output_type;result;body} ; type_annotation} ok O.{expression = Lambda {binder;input_type;output_type;result;body} ; type_annotation}
| Constant (name, lst) -> | Constant (name, lst) ->