test for condition

This commit is contained in:
Galfour 2019-03-26 09:59:20 +00:00
parent 1fe74323be
commit 5507482b2d
9 changed files with 125 additions and 40 deletions

View File

@ -280,8 +280,7 @@ module Simplify = struct
ok @@ ae @@ Constructor (c.value, arg)
| EConstr _ -> simple_fail "econstr: not supported yet"
| EArith (Add c) ->
let%bind (a, b) = simpl_binop c.value in
ok @@ ae @@ Constant ("ADD", [a;b])
simpl_binop "ADD" c.value
| EArith (Int n) ->
let n = Z.to_int @@ snd @@ n.value in
ok @@ ae @@ Literal (Number n)
@ -289,20 +288,44 @@ module Simplify = struct
| EString (String s) ->
ok @@ ae @@ Literal (String s.value)
| EString _ -> simple_fail "string: not supported yet"
| ELogic (BoolExpr (False _)) ->
ok @@ ae @@ Literal (Bool false)
| ELogic (BoolExpr (True _)) ->
ok @@ ae @@ Literal (Bool true)
| ELogic _ -> simple_fail "logic: not supported yet"
| ELogic l -> simpl_logic_expression l
| EList _ -> simple_fail "list: not supported yet"
| ESet _ -> simple_fail "set: not supported yet"
| EMap _ -> simple_fail "map: not supported yet"
and simpl_logic_expression (t:Raw.logic_expr) : ae result =
match t with
| BoolExpr (False _) ->
ok @@ ae @@ Literal (Bool false)
| BoolExpr (True _) ->
ok @@ ae @@ Literal (Bool true)
| BoolExpr (Or b) ->
simpl_binop "OR" b.value
| BoolExpr (And b) ->
simpl_binop "AND" b.value
| BoolExpr (Not b) ->
simpl_unop "NOT" b.value
| CompExpr (Lt c) ->
simpl_binop "LT" c.value
| CompExpr (Gt c) ->
simpl_binop "GT" c.value
| CompExpr (Leq c) ->
simpl_binop "LE" c.value
| CompExpr (Geq c) ->
simpl_binop "GE" c.value
| CompExpr (Equal c) ->
simpl_binop "EQ" c.value
| CompExpr (Neq c) ->
simpl_binop "NEQ" c.value
and simpl_binop (t:_ Raw.bin_op) : (ae * ae) result =
and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result =
let%bind a = simpl_expression t.arg1 in
let%bind b = simpl_expression t.arg2 in
ok (a, b)
ok @@ ae @@ Constant (name, [a;b])
and simpl_unop (name:string) (t:_ Raw.un_op) : ae result =
let%bind a = simpl_expression t.arg in
ok @@ ae @@ Constant (name, [a])
and simpl_list_expression (lst:Raw.expr list) : ae result =
match lst with

View File

@ -187,6 +187,14 @@ module PP = struct
| Matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae matching m
let declaration ppf (d:declaration) =
match d with
| 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

View File

@ -0,0 +1,8 @@
function main (const i : int) : int is
var result : int := 23 ;
begin
if i = 2 then
result := 42
else
result := 0
end with result

View File

@ -72,6 +72,16 @@ module Append = struct
in
aux @@ List.rev lst
let rec to_list' t' =
match t' with
| Leaf x -> [x]
| Node {a;b} -> (to_list' a) @ (to_list' b)
let to_list t =
match t with
| Empty -> []
| Full x -> to_list' x
let rec fold' leaf node = function
| Leaf x -> leaf x
| Node {a;b} -> node (fold' leaf node a) (fold' leaf node b)

View File

@ -93,25 +93,36 @@ 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 =
Transpiler.untranspile v e
let type_file ?(debug_simplify = false) (path:string) : AST_Typed.program result =
let type_file ?(debug_simplify = false) ?(debug_typed = false)
(path:string) : AST_Typed.program result =
let%bind raw = parse_file path 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
Format.(printf "Simplified : %a\n%!" AST_Simplified.PP.program simpl)
) ;
let%bind typed =
trace (simple_error "typing") @@
type_ simpl in
(if debug_typed then
Format.(printf "Typed : %a\n%!" AST_Typed.PP.program typed)
) ;
ok typed
let easy_run_main_typed (program:AST_Typed.program) (input:AST_Typed.annotated_expression) : AST_Typed.annotated_expression result =
let easy_run_main_typed
?(debug_mini_c = false)
(program:AST_Typed.program) (input:AST_Typed.annotated_expression) : AST_Typed.annotated_expression result =
let%bind mini_c_main =
trace (simple_error "transpile mini_c main") @@
transpile_entry program "main" in
(if debug_mini_c then
Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main.content)
) ;
let%bind mini_c_value = transpile_value input in
let%bind mini_c_result =
trace (simple_error "run mini_c") @@
Mini_c.Run.run_entry mini_c_main mini_c_value in

View File

@ -111,6 +111,7 @@ let expression_to_value ((e, _, _):expression) : value result =
module PP = struct
open Format
open Ligo_helpers.PP
let space_sep ppf () = fprintf ppf " "
@ -137,29 +138,16 @@ module PP = struct
and environment_element ppf ((s, tv) : environment_element) =
Format.fprintf ppf "%s : %a" s type_ tv
and environment_small' ppf = let open Append_tree in function
| Leaf x -> environment_element ppf x
| Node {a; b ; full ; size} ->
fprintf ppf "@[<v 2>N(f:%b,s:%d)[@;%a,@;%a@]@;]"
full size
environment_small' a environment_small' b
and environment_small' ppf e' = let open Append_tree in
let lst = to_list' e' in
fprintf ppf "S[%a]" (list_sep environment_element) lst
and environment_small ppf = function
| Empty -> fprintf ppf "[]"
| Full x -> environment_small' ppf x
and environment_small ppf e = let open Append_tree in
let lst = to_list e in
fprintf ppf "S[%a]" (list_sep environment_element) lst
and environment_small_hlist' ppf = let open Append_tree in function
| Leaf x -> environment_element ppf x
| Node {a;b} ->
fprintf ppf "%a, %a"
environment_small_hlist' a
environment_small_hlist' b
and environment_small_hlist ppf = let open Append_tree in function
| Empty -> fprintf ppf ""
| Full x -> environment_small_hlist' ppf x
let environment ppf (x:environment) = Format.pp_print_list environment_small ppf x
let environment ppf (x:environment) =
fprintf ppf "Env[%a]" (list_sep environment_small) x
let rec value ppf : value -> _ = function
| `Bool b -> fprintf ppf "%b" b
@ -394,6 +382,17 @@ module Environment = struct
in
aux @@ List.rev lst
let rec to_list' (e:t') =
match e with
| Leaf x -> [x]
| Node {a;b} -> (to_list' a) @ (to_list' b)
let to_list (e:t) =
match e with
| Empty -> []
| Full x -> to_list' x
type bound = string list
open Michelson
@ -461,9 +460,10 @@ module Environment = struct
let restrict t : t = List.tl t
let of_small small : t = [small]
let has x : t -> bool = function
let rec has x : t -> bool = function
| [] -> raise (Failure "Schema.Big.has")
| hd :: _ -> Small.has x hd
| [hd] -> Small.has x hd
| hd :: tl -> Small.has x hd || has x tl
let add x : t -> t = function
| [] -> raise (Failure "Schema.Big.add")
| hd :: tl -> Small.append x hd :: tl
@ -573,7 +573,9 @@ module Environment = struct
| a :: b -> (
match Small.to_michelson_set str a with
| Ok (code, tv) -> ok (seq [dip i_unpair ; code ; i_pair], tv)
| Errors _ -> aux b str
| Errors _ ->
let%bind (tmp, tv) = aux b str in
ok (seq [dip i_unpiar ; tmp ; i_piar], tv)
)
in
let%bind (code, tv) = aux s str in
@ -586,12 +588,13 @@ module Environment = struct
let output_stack_ty = Stack.(schema_ty @: nil) in
let%bind error_message =
ok @@ Format.asprintf
"\ncode : %a\nschema type : %a"
"\ncode : %a\nschema : %a\nschema type : %a"
Tezos_utils.Micheline.Michelson.pp code
PP.environment s
Tezos_utils.Micheline.Michelson.pp schema_michelson
in
let%bind _ =
Trace.trace_tzresult_lwt (error "error parsing big.get code" error_message) @@
Trace.trace_tzresult_lwt (error "error parsing big.set code" error_message) @@
Tezos_utils.Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty
in
@ -622,6 +625,7 @@ module Translate_program = struct
| "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD
| "NEG" -> ok @@ simple_unary @@ prim I_NEG
| "PAIR" -> ok @@ simple_binary @@ prim I_PAIR
| "EQ" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_EQ]
| x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist"
and translate_value (v:value) : michelson result = match v with

View File

@ -41,6 +41,23 @@ let complex_function () : unit result =
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let condition () : unit result =
let%bind program = type_file "./contracts/condition.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 (if n = 2 then 42 else 0) result'
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let declarations () : unit result =
let%bind program = type_file "./contracts/declarations.ligo" in
let aux n =
@ -94,6 +111,7 @@ let main = "Integration (End to End)", [
test "basic" basic ;
test "function" function_ ;
test "complex function" complex_function ;
test "condition" condition ;
test "declarations" declarations ;
test "quote declaration" quote_declaration ;
test "quote declarations" quote_declarations ;

View File

@ -69,8 +69,9 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
return ~env' (Assignment (name, expression))
| Matching (expr, Match_bool {match_true ; match_false}) ->
let%bind expr' = translate_annotated_expression env expr in
let%bind true_branch = translate_block env match_true in
let%bind false_branch = translate_block env match_false in
let env' = Environment.extend env in
let%bind true_branch = translate_block env' match_true in
let%bind false_branch = translate_block env' match_false in
return (Cond (expr', true_branch, false_branch))
| Matching _ -> simple_fail "todo : match"
| Loop (expr, body) ->

View File

@ -333,6 +333,8 @@ and type_constant (name:string) (lst:O.type_value list) : (string * O.type_value
| "ADD", [a ; b] when type_value_eq (a, make_t_string) && type_value_eq (b, make_t_string) -> ok ("CONCAT", make_t_string)
| "ADD", [_ ; _] -> simple_fail "bad types to add"
| "ADD", _ -> simple_fail "bad number of params to add"
| "EQ", [a ; b] when type_value_eq (a, make_t_int) && type_value_eq (b, make_t_int) -> ok ("EQ", make_t_bool)
| "EQ", _ -> simple_fail "EQ only defined over int"
| name, _ -> fail @@ unrecognized_constant name
let untype_type_value (t:O.type_value) : (I.type_expression) result =