From d95f345dbf3dd2cb85daf49e5e9f13e76b794120 Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Fri, 18 Oct 2019 13:41:02 +0200 Subject: [PATCH 1/4] First attempt at adding conditionals as expressions. Warning: The simplifier is not done yet. --- src/passes/1-parser/pascaligo/AST.ml | 14 ++++++- src/passes/1-parser/pascaligo/AST.mli | 11 +++++ src/passes/1-parser/pascaligo/Parser.mly | 20 +++++++-- src/passes/1-parser/pascaligo/ParserLog.ml | 48 +++++++++++++++++----- src/passes/2-simplify/pascaligo.ml | 22 ++++++++++ 5 files changed, 100 insertions(+), 15 deletions(-) diff --git a/src/passes/1-parser/pascaligo/AST.ml b/src/passes/1-parser/pascaligo/AST.ml index 36cbdf637..c572160ac 100644 --- a/src/passes/1-parser/pascaligo/AST.ml +++ b/src/passes/1-parser/pascaligo/AST.ml @@ -339,6 +339,16 @@ and record_patch = { record_inj : record_expr } +and cond_expr = { + kwd_if : kwd_if; + test : expr; + kwd_then : kwd_then; + ifso : expr; + terminator : semi option; + kwd_else : kwd_else; + ifnot : expr +} + and conditional = { kwd_if : kwd_if; test : expr; @@ -438,7 +448,8 @@ and collection = (* Expressions *) and expr = -| ECase of expr case reg + ECase of expr case reg +| ECond of cond_expr reg | EAnnot of annot_expr reg | ELogic of logic_expr | EArith of arith_expr @@ -629,6 +640,7 @@ let rec expr_to_region = function | EBytes {region; _} | EUnit region | ECase {region;_} +| ECond {region; _} | EPar {region; _} -> region and tuple_expr_to_region {region; _} = region diff --git a/src/passes/1-parser/pascaligo/AST.mli b/src/passes/1-parser/pascaligo/AST.mli index e18903f55..cbb5ffd36 100644 --- a/src/passes/1-parser/pascaligo/AST.mli +++ b/src/passes/1-parser/pascaligo/AST.mli @@ -330,6 +330,16 @@ and record_patch = { record_inj : field_assign reg injection reg } +and cond_expr = { + kwd_if : kwd_if; + test : expr; + kwd_then : kwd_then; + ifso : expr; + terminator : semi option; + kwd_else : kwd_else; + ifnot : expr +} + and conditional = { kwd_if : kwd_if; test : expr; @@ -430,6 +440,7 @@ and collection = and expr = ECase of expr case reg +| ECond of cond_expr reg | EAnnot of annot_expr reg | ELogic of logic_expr | EArith of arith_expr diff --git a/src/passes/1-parser/pascaligo/Parser.mly b/src/passes/1-parser/pascaligo/Parser.mly index bd9f63174..a22c005e7 100644 --- a/src/passes/1-parser/pascaligo/Parser.mly +++ b/src/passes/1-parser/pascaligo/Parser.mly @@ -497,7 +497,7 @@ proc_call: conditional: If expr Then if_clause option(SEMI) Else if_clause { let region = cover $1 (if_clause_to_region $7) in - let value = { + let value : conditional = { kwd_if = $1; test = $2; kwd_then = $3; @@ -640,14 +640,28 @@ interactive_expr: expr: case(expr) { ECase ($1 expr_to_region) } +| cond_expr { $1 } | disj_expr { $1 } +cond_expr: + If expr Then expr option(SEMI) Else expr { + let region = cover $1 (expr_to_region $7) in + let value : cond_expr = { + kwd_if = $1; + test = $2; + kwd_then = $3; + ifso = $4; + terminator = $5; + kwd_else = $6; + ifnot = $7} + in ECond {region; value} } + disj_expr: disj_expr Or conj_expr { let start = expr_to_region $1 and stop = expr_to_region $3 in let region = cover start stop - and value = {arg1 = $1; op = $2; arg2 = $3} in + and value = {arg1=$1; op=$2; arg2=$3} in ELogic (BoolExpr (Or {region; value})) } | conj_expr { $1 } @@ -657,7 +671,7 @@ conj_expr: let start = expr_to_region $1 and stop = expr_to_region $3 in let region = cover start stop - and value = {arg1 = $1; op = $2; arg2 = $3} + and value = {arg1=$1; op=$2; arg2=$3} in ELogic (BoolExpr (And {region; value})) } | set_membership { $1 } diff --git a/src/passes/1-parser/pascaligo/ParserLog.ml b/src/passes/1-parser/pascaligo/ParserLog.ml index de4b683c2..aed9454da 100644 --- a/src/passes/1-parser/pascaligo/ParserLog.ml +++ b/src/passes/1-parser/pascaligo/ParserLog.ml @@ -256,16 +256,23 @@ and print_instruction buffer = function | MapRemove {value; _} -> print_map_remove buffer value | SetRemove {value; _} -> print_set_remove buffer value -and print_conditional buffer node = - let {kwd_if; test; kwd_then; ifso; terminator; - kwd_else; ifnot} = node in - print_token buffer kwd_if "if"; - print_expr buffer test; - print_token buffer kwd_then "then"; - print_if_clause buffer ifso; - print_terminator buffer terminator; - print_token buffer kwd_else "else"; - print_if_clause buffer ifnot +and print_cond_expr buffer (node: cond_expr) = + print_token buffer node.kwd_if "if"; + print_expr buffer node.test; + print_token buffer node.kwd_then "then"; + print_expr buffer node.ifso; + print_terminator buffer node.terminator; + print_token buffer node.kwd_else "else"; + print_expr buffer node.ifnot + +and print_conditional buffer (node: conditional) = + print_token buffer node.kwd_if "if"; + print_expr buffer node.test; + print_token buffer node.kwd_then "then"; + print_if_clause buffer node.ifso; + print_terminator buffer node.terminator; + print_token buffer node.kwd_else "else"; + print_if_clause buffer node.ifnot and print_if_clause buffer = function ClauseInstr instr -> print_instruction buffer instr @@ -374,6 +381,7 @@ and print_bind_to buffer = function and print_expr buffer = function ECase {value;_} -> print_case_expr buffer value +| ECond {value;_} -> print_cond_expr buffer value | EAnnot {value;_} -> print_annot_expr buffer value | ELogic e -> print_logic_expr buffer e | EArith e -> print_arith_expr buffer e @@ -919,7 +927,22 @@ and pp_instruction buffer ~pad:(_,pc as pad) = function pp_node buffer ~pad "SetRemove"; pp_set_remove buffer ~pad value -and pp_conditional buffer ~pad:(_,pc) cond = +and pp_cond_expr buffer ~pad:(_,pc) (cond: cond_expr) = + let () = + let _, pc as pad = mk_pad 3 0 pc in + pp_node buffer ~pad ""; + pp_expr buffer ~pad:(mk_pad 1 0 pc) cond.test in + let () = + let _, pc as pad = mk_pad 3 1 pc in + pp_node buffer ~pad ""; + pp_expr buffer ~pad:(mk_pad 1 0 pc) cond.ifso in + let () = + let _, pc as pad = mk_pad 3 2 pc in + pp_node buffer ~pad ""; + pp_expr buffer ~pad:(mk_pad 1 0 pc) cond.ifnot + in () + +and pp_conditional buffer ~pad:(_,pc) (cond: conditional) = let () = let _, pc as pad = mk_pad 3 0 pc in pp_node buffer ~pad ""; @@ -1254,6 +1277,9 @@ and pp_expr buffer ~pad:(_,pc as pad) = function ECase {value; _} -> pp_node buffer ~pad "ECase"; pp_case pp_expr buffer ~pad value +| ECond {value; _} -> + pp_node buffer ~pad "ECond"; + pp_cond_expr buffer ~pad value | EAnnot {value; _} -> pp_node buffer ~pad "EAnnot"; pp_annotated buffer ~pad value diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index e9195e8a5..42a33d930 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -379,6 +379,28 @@ let rec simpl_expression (t:Raw.expr) : expr result = | ELogic l -> simpl_logic_expression l | EList l -> simpl_list_expression l | ESet s -> simpl_set_expression s + | ECond _ -> ( failwith "TODO" +(* + let (c , loc) = r_split c in + let%bind expr = simpl_expression c.test in + + let%bind match_true = simpl_expression c.ifso in + let%bind match_false = simpl_expression c.ifnot in + + let%bind match_true = match_true None in + let%bind match_false = match_false None in + return @@ e_matching expr ~loc (Match_bool {match_true; match_false}) +*) + +(* + let%bind lst = + bind_list @@ + [ok (Raw.PTrue Region.ghost, simpl_expression c.ifso); + ok (Raw.PFalse Region.ghost, simpl_expression c.ifnot)] in + let%bind cases = simpl_cases lst in + return @@ e_matching ~loc e cases +*) + ) | ECase c -> ( let (c , loc) = r_split c in let%bind e = simpl_expression c.expr in From 080b25a3bd817269cf09af4ac55cfcfd60e5289e Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Fri, 18 Oct 2019 14:32:58 +0200 Subject: [PATCH 2/4] WIP: add test. still have two ECond implementation, none of them pass the test --- src/passes/2-simplify/pascaligo.ml | 28 +++++++++++----------------- src/test/contracts/condition.ligo | 6 ++++++ src/test/integration_tests.ml | 13 ++++++++++--- 3 files changed, 27 insertions(+), 20 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 42a33d930..591e61180 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -379,28 +379,22 @@ let rec simpl_expression (t:Raw.expr) : expr result = | ELogic l -> simpl_logic_expression l | EList l -> simpl_list_expression l | ESet s -> simpl_set_expression s - | ECond _ -> ( failwith "TODO" -(* - let (c , loc) = r_split c in + | ECond c -> (*fail @@ simple_error "TODO"*) + (* let (c , loc) = r_split c in let%bind expr = simpl_expression c.test in - let%bind match_true = simpl_expression c.ifso in let%bind match_false = simpl_expression c.ifnot in + return @@ e_matching expr ~loc (Match_bool {match_true; match_false}) *) - let%bind match_true = match_true None in - let%bind match_false = match_false None in - return @@ e_matching expr ~loc (Match_bool {match_true; match_false}) -*) - -(* - let%bind lst = - bind_list @@ - [ok (Raw.PTrue Region.ghost, simpl_expression c.ifso); - ok (Raw.PFalse Region.ghost, simpl_expression c.ifnot)] in + let (c , loc) = r_split c in + let%bind expr = simpl_expression c.test in + let%bind match_true = simpl_expression c.ifso in + let%bind match_false = simpl_expression c.ifnot in + let%bind lst = ok @@ + [(Raw.PTrue Region.ghost, match_true); + (Raw.PFalse Region.ghost, match_false)] in let%bind cases = simpl_cases lst in - return @@ e_matching ~loc e cases -*) - ) + return @@ e_matching ~loc expr cases | ECase c -> ( let (c , loc) = r_split c in let%bind e = simpl_expression c.expr in diff --git a/src/test/contracts/condition.ligo b/src/test/contracts/condition.ligo index 98672b1c9..53a75ed07 100644 --- a/src/test/contracts/condition.ligo +++ b/src/test/contracts/condition.ligo @@ -8,3 +8,9 @@ function main (const i : int) : int is else result := 0 end with result + +function foo (const b : bool) : int is + var x : int := 41 ; + begin + x := 1 + (if b then x else main(x)) ; + end with x \ No newline at end of file diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 6726d66b5..8f7cd5415 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -587,9 +587,16 @@ let list () : unit result = let condition () : unit result = let%bind program = type_file "./contracts/condition.ligo" in - let make_input = e_int in - let make_expected = fun n -> e_int (if n = 2 then 42 else 0) in - expect_eq_n program "main" make_input make_expected + let%bind _ = + let make_input = e_int in + let make_expected = fun n -> e_int (if n = 2 then 42 else 0) in + expect_eq_n program "main" make_input make_expected + in + let%bind _ = + let make_expected = fun b -> e_int (if b then 42 else 1) in + expect_eq_b program "main" make_expected + in + ok () let condition_simple () : unit result = let%bind program = type_file "./contracts/condition-simple.ligo" in From 85fe8d2018e7cf0e60f0a5a419348d7635616c3f Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Fri, 18 Oct 2019 14:42:36 +0200 Subject: [PATCH 3/4] using the proper entry point in the test.. --- src/test/integration_tests.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 8f7cd5415..ba4fc9520 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -594,7 +594,7 @@ let condition () : unit result = in let%bind _ = let make_expected = fun b -> e_int (if b then 42 else 1) in - expect_eq_b program "main" make_expected + expect_eq_b program "foo" make_expected in ok () From 6b55bf3630aa92e8fa4630b5fa582171e4631337 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Fri, 18 Oct 2019 14:47:04 +0200 Subject: [PATCH 4/4] cleaning --- src/passes/2-simplify/pascaligo.ml | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 591e61180..0e9ddaf7e 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -379,22 +379,12 @@ let rec simpl_expression (t:Raw.expr) : expr result = | ELogic l -> simpl_logic_expression l | EList l -> simpl_list_expression l | ESet s -> simpl_set_expression s - | ECond c -> (*fail @@ simple_error "TODO"*) - (* let (c , loc) = r_split c in - let%bind expr = simpl_expression c.test in - let%bind match_true = simpl_expression c.ifso in - let%bind match_false = simpl_expression c.ifnot in - return @@ e_matching expr ~loc (Match_bool {match_true; match_false}) *) - + | ECond c -> let (c , loc) = r_split c in let%bind expr = simpl_expression c.test in let%bind match_true = simpl_expression c.ifso in let%bind match_false = simpl_expression c.ifnot in - let%bind lst = ok @@ - [(Raw.PTrue Region.ghost, match_true); - (Raw.PFalse Region.ghost, match_false)] in - let%bind cases = simpl_cases lst in - return @@ e_matching ~loc expr cases + return @@ e_matching expr ~loc (Match_bool {match_true; match_false}) | ECase c -> ( let (c , loc) = r_split c in let%bind e = simpl_expression c.expr in