From 704c744acea7a3f85d930b3af52f16742b12628d Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Fri, 18 Oct 2019 13:41:02 +0200 Subject: [PATCH 1/5] 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 b721a19b00f13b2c7827bb81a793afa526e995e0 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Fri, 18 Oct 2019 14:32:58 +0200 Subject: [PATCH 2/5] 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 71548f8c7c3b83eeb03672cf7fd15e2a046f5345 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Fri, 18 Oct 2019 14:42:36 +0200 Subject: [PATCH 3/5] 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 bec34199361f1dfb8dc2b4b4753c796f945dced9 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Fri, 18 Oct 2019 14:47:04 +0200 Subject: [PATCH 4/5] 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 From eae3348d5104b4f08cf90ec43d7a0cf7b0204398 Mon Sep 17 00:00:00 2001 From: Christian Rinderknecht Date: Wed, 23 Oct 2019 00:35:29 +0200 Subject: [PATCH 5/5] I forbade empty patches (parser). Fixed AST pretty-printer (PascaLIGO). Changed accordingly the simplifier: the dead code for the error about empty record patches is no long. --- src/passes/1-parser/pascaligo/AST.ml | 17 +++- src/passes/1-parser/pascaligo/AST.mli | 17 +++- src/passes/1-parser/pascaligo/Parser.mly | 50 +++++++--- src/passes/1-parser/pascaligo/ParserLog.ml | 101 ++++++++++++--------- src/passes/2-simplify/pascaligo.ml | 51 +++++------ src/test/contracts/map.ligo | 4 - src/test/contracts/set_arithmetic.ligo | 6 -- src/test/integration_tests.ml | 25 ++--- 8 files changed, 147 insertions(+), 124 deletions(-) diff --git a/src/passes/1-parser/pascaligo/AST.ml b/src/passes/1-parser/pascaligo/AST.ml index 97eab1c20..35726f15b 100644 --- a/src/passes/1-parser/pascaligo/AST.ml +++ b/src/passes/1-parser/pascaligo/AST.ml @@ -187,7 +187,7 @@ and type_decl = { and type_expr = TProd of cartesian | TSum of (variant reg, vbar) nsepseq reg -| TRecord of field_decl reg injection reg +| TRecord of field_decl reg ne_injection reg | TApp of (type_name * type_tuple) reg | TFun of (type_expr * arrow * type_expr) reg | TPar of type_expr par reg @@ -217,7 +217,7 @@ and fun_decl = { colon : colon; ret_type : type_expr; kwd_is : kwd_is; - local_decls : local_decl list option; + local_decls : local_decl list; block : block reg option; kwd_with : kwd_with option; return : expr; @@ -315,14 +315,14 @@ and set_patch = { kwd_patch : kwd_patch; path : path; kwd_with : kwd_with; - set_inj : expr injection reg + set_inj : expr ne_injection reg } and map_patch = { kwd_patch : kwd_patch; path : path; kwd_with : kwd_with; - map_inj : binding reg injection reg + map_inj : binding reg ne_injection reg } and binding = { @@ -335,7 +335,7 @@ and record_patch = { kwd_patch : kwd_patch; path : path; kwd_with : kwd_with; - record_inj : record_expr + record_inj : field_assign reg ne_injection reg } and cond_expr = { @@ -479,6 +479,13 @@ and 'a injection = { closing : closing } +and 'a ne_injection = { + opening : opening; + ne_elements : ('a, semi) nsepseq; + terminator : semi option; + closing : closing +} + and opening = Kwd of keyword | KwdBracket of keyword * lbracket diff --git a/src/passes/1-parser/pascaligo/AST.mli b/src/passes/1-parser/pascaligo/AST.mli index a41fb005f..a682a9cd1 100644 --- a/src/passes/1-parser/pascaligo/AST.mli +++ b/src/passes/1-parser/pascaligo/AST.mli @@ -178,7 +178,7 @@ and type_decl = { and type_expr = TProd of cartesian | TSum of (variant reg, vbar) nsepseq reg -| TRecord of field_decl reg injection reg +| TRecord of field_decl reg ne_injection reg | TApp of (type_name * type_tuple) reg | TFun of (type_expr * arrow * type_expr) reg | TPar of type_expr par reg @@ -208,7 +208,7 @@ and fun_decl ={ colon : colon; ret_type : type_expr; kwd_is : kwd_is; - local_decls : local_decl list option; + local_decls : local_decl list; block : block reg option; kwd_with : kwd_with option; return : expr; @@ -306,14 +306,14 @@ and set_patch = { kwd_patch : kwd_patch; path : path; kwd_with : kwd_with; - set_inj : expr injection reg + set_inj : expr ne_injection reg } and map_patch = { kwd_patch : kwd_patch; path : path; kwd_with : kwd_with; - map_inj : binding reg injection reg + map_inj : binding reg ne_injection reg } and binding = { @@ -326,7 +326,7 @@ and record_patch = { kwd_patch : kwd_patch; path : path; kwd_with : kwd_with; - record_inj : field_assign reg injection reg + record_inj : field_assign reg ne_injection reg } and cond_expr = { @@ -470,6 +470,13 @@ and 'a injection = { closing : closing } +and 'a ne_injection = { + opening : opening; + ne_elements : ('a, semi) nsepseq; + terminator : semi option; + closing : closing +} + and opening = Kwd of keyword | KwdBracket of keyword * lbracket diff --git a/src/passes/1-parser/pascaligo/Parser.mly b/src/passes/1-parser/pascaligo/Parser.mly index 38b86357b..77abea723 100644 --- a/src/passes/1-parser/pascaligo/Parser.mly +++ b/src/passes/1-parser/pascaligo/Parser.mly @@ -213,21 +213,21 @@ variant: record_type: Record sep_or_term_list(field_decl,SEMI) End { - let elements, terminator = $2 in + let ne_elements, terminator = $2 in let region = cover $1 $3 - and value = { + and value = { opening = Kwd $1; - elements = Some elements; + ne_elements; terminator; closing = End $3} in {region; value} } | Record LBRACKET sep_or_term_list(field_decl,SEMI) RBRACKET { - let elements, terminator = $3 in + let ne_elements, terminator = $3 in let region = cover $1 $4 - and value = { + and value = { opening = KwdBracket ($1,$2); - elements = Some elements; + ne_elements; terminator; closing = RBracket $4} in {region; value} } @@ -258,7 +258,7 @@ fun_decl: colon = $4; ret_type = $5; kwd_is = $6; - local_decls = Some $7; + local_decls = $7; block = Some $8; kwd_with = Some $9; return = $10; @@ -266,7 +266,7 @@ fun_decl: in {region;value}} | Function fun_name parameters COLON type_expr Is expr option(SEMI) { - let stop = + let stop = match $8 with Some region -> region | None -> expr_to_region $7 in @@ -278,7 +278,7 @@ fun_decl: colon = $4; ret_type = $5; kwd_is = $6; - local_decls = None; + local_decls = []; block = None; kwd_with = None; return = $7; @@ -433,7 +433,7 @@ map_remove: in {region; value}} set_patch: - Patch path With injection(Set,expr) { + Patch path With ne_injection(Set,expr) { let region = cover $1 $4.region in let value = { kwd_patch = $1; @@ -443,7 +443,7 @@ set_patch: in {region; value}} map_patch: - Patch path With injection(Map,binding) { + Patch path With ne_injection(Map,binding) { let region = cover $1 $4.region in let value = { kwd_patch = $1; @@ -491,6 +491,28 @@ injection(Kind,element): closing = RBracket $3} in {region; value}} +ne_injection(Kind,element): + Kind sep_or_term_list(element,SEMI) End { + let ne_elements, terminator = $2 in + let region = cover $1 $3 + and value = { + opening = Kwd $1; + ne_elements; + terminator; + closing = End $3} + in {region; value} + } +| Kind LBRACKET sep_or_term_list(element,SEMI) RBRACKET { + let ne_elements, terminator = $3 in + let region = cover $1 $4 + and value = { + opening = KwdBracket ($1,$2); + ne_elements; + terminator; + closing = RBracket $4} + in {region; value} + } + binding: expr ARROW expr { let start = expr_to_region $1 @@ -503,7 +525,7 @@ binding: in {region; value}} record_patch: - Patch path With record_expr { + Patch path With ne_injection(Record,field_assignment) { let region = cover $1 $4.region in let value = { kwd_patch = $1; @@ -906,7 +928,7 @@ record_expr: Record sep_or_term_list(field_assignment,SEMI) End { let elements, terminator = $2 in let region = cover $1 $3 - and value = { + and value : field_assign AST.reg injection = { opening = Kwd $1; elements = Some elements; terminator; @@ -916,7 +938,7 @@ record_expr: | Record LBRACKET sep_or_term_list(field_assignment,SEMI) RBRACKET { let elements, terminator = $3 in let region = cover $1 $4 - and value = { + and value : field_assign AST.reg injection = { opening = KwdBracket ($1,$2); elements = Some elements; terminator; diff --git a/src/passes/1-parser/pascaligo/ParserLog.ml b/src/passes/1-parser/pascaligo/ParserLog.ml index e09149bce..3941cbb79 100644 --- a/src/passes/1-parser/pascaligo/ParserLog.ml +++ b/src/passes/1-parser/pascaligo/ParserLog.ml @@ -125,7 +125,7 @@ and print_sum_type buffer {value; _} = print_nsepseq buffer "|" print_variant value and print_record_type buffer record_type = - print_injection buffer "record" print_field_decl record_type + print_ne_injection buffer "record" print_field_decl record_type and print_type_app buffer {value; _} = let type_name, type_tuple = value in @@ -222,10 +222,7 @@ and print_block_closing buffer = function | End kwd_end -> print_token buffer kwd_end "end" and print_local_decls buffer sequence = - match sequence with - | Some sequence -> - List.iter (print_local_decl buffer) sequence - | None -> () + List.iter (print_local_decl buffer) sequence and print_local_decl buffer = function LocalFun decl -> print_fun_decl buffer decl @@ -576,24 +573,24 @@ and print_selection buffer = function and print_record_patch buffer node = let {kwd_patch; path; kwd_with; record_inj} = node in - print_token buffer kwd_patch "patch"; - print_path buffer path; - print_token buffer kwd_with "with"; - print_record_expr buffer record_inj + print_token buffer kwd_patch "patch"; + print_path buffer path; + print_token buffer kwd_with "with"; + print_ne_injection buffer "record" print_field_assign record_inj and print_set_patch buffer node = let {kwd_patch; path; kwd_with; set_inj} = node in - print_token buffer kwd_patch "patch"; - print_path buffer path; - print_token buffer kwd_with "with"; - print_injection buffer "set" print_expr set_inj + print_token buffer kwd_patch "patch"; + print_path buffer path; + print_token buffer kwd_with "with"; + print_ne_injection buffer "set" print_expr set_inj and print_map_patch buffer node = let {kwd_patch; path; kwd_with; map_inj} = node in - print_token buffer kwd_patch "patch"; - print_path buffer path; - print_token buffer kwd_with "with"; - print_injection buffer "map" print_binding map_inj + print_token buffer kwd_patch "patch"; + print_path buffer path; + print_token buffer kwd_with "with"; + print_ne_injection buffer "map" print_binding map_inj and print_map_remove buffer node = let {kwd_remove; key; kwd_from; kwd_map; map} = node in @@ -621,6 +618,16 @@ and print_injection : print_terminator buffer terminator; print_closing buffer closing +and print_ne_injection : + 'a.Buffer.t -> string -> (Buffer.t -> 'a -> unit) -> + 'a ne_injection reg -> unit = + fun buffer kwd print {value; _} -> + let {opening; ne_elements; terminator; closing} = value in + print_opening buffer kwd opening; + print_nsepseq buffer ";" print ne_elements; + print_terminator buffer terminator; + print_closing buffer closing + and print_opening buffer lexeme = function Kwd kwd -> print_token buffer kwd lexeme @@ -774,10 +781,10 @@ and pp_declaration buffer ~pad:(_,pc as pad) = function pp_type_expr buffer ~pad:(mk_pad 2 1 pc) value.type_expr | ConstDecl {value; _} -> pp_node buffer ~pad "ConstDecl"; - pp_const_decl buffer ~pad:(mk_pad 1 0 pc) value + pp_const_decl buffer ~pad value | FunDecl {value; _} -> pp_node buffer ~pad "FunDecl"; - pp_fun_decl buffer ~pad:(mk_pad 1 0 pc) value + pp_fun_decl buffer ~pad value and pp_const_decl buffer ~pad:(_,pc) decl = pp_ident buffer ~pad:(mk_pad 3 0 pc) decl.name.value; @@ -817,7 +824,7 @@ and pp_type_expr buffer ~pad:(_,pc as pad) = function let apply len rank field_decl = pp_field_decl buffer ~pad:(mk_pad len rank pc) field_decl.value in - let fields = Utils.sepseq_to_list value.elements in + let fields = Utils.nsepseq_to_list value.ne_elements in List.iteri (List.length fields |> apply) fields and pp_cartesian buffer ~pad:(_,pc) {value; _} = @@ -844,23 +851,26 @@ and pp_type_tuple buffer ~pad:(_,pc) {value; _} = in List.iteri (List.length components |> apply) components and pp_fun_decl buffer ~pad:(_,pc) decl = + let fields = + if decl.local_decls = [] then 5 else 6 in let () = - let pad = mk_pad 6 0 pc in + let pad = mk_pad fields 0 pc in pp_ident buffer ~pad decl.name.value in let () = - let pad = mk_pad 6 1 pc in + let pad = mk_pad fields 1 pc in pp_node buffer ~pad ""; pp_parameters buffer ~pad decl.param in let () = - let _, pc as pad = mk_pad 6 2 pc in + let _, pc as pad = mk_pad fields 2 pc in pp_node buffer ~pad ""; pp_type_expr buffer ~pad:(mk_pad 1 0 pc) decl.ret_type in let () = - let pad = mk_pad 6 3 pc in - pp_node buffer ~pad ""; - pp_local_decls buffer ~pad decl.local_decls in + if fields = 6 then + let pad = mk_pad fields 3 pc in + pp_node buffer ~pad ""; + pp_local_decls buffer ~pad decl.local_decls in let () = - let pad = mk_pad 6 4 pc in + let pad = mk_pad fields (fields - 2) pc in pp_node buffer ~pad ""; let statements = match decl.block with @@ -868,7 +878,7 @@ and pp_fun_decl buffer ~pad:(_,pc) decl = | None -> Instr (Skip Region.ghost), [] in pp_statements buffer ~pad statements in let () = - let _, pc as pad = mk_pad 6 5 pc in + let _, pc as pad = mk_pad fields (fields - 1) pc in pp_node buffer ~pad ""; pp_expr buffer ~pad:(mk_pad 1 0 pc) decl.return in () @@ -1090,6 +1100,15 @@ and pp_injection : let apply len rank = printer buffer ~pad:(mk_pad len rank pc) in List.iteri (apply length) elements +and pp_ne_injection : + 'a.(Buffer.t -> pad:(string*string) -> 'a -> unit) + -> Buffer.t -> pad:(string*string) -> 'a ne_injection -> unit = + fun printer buffer ~pad:(_,pc) inj -> + let ne_elements = Utils.nsepseq_to_list inj.ne_elements in + let length = List.length ne_elements in + let apply len rank = printer buffer ~pad:(mk_pad len rank pc) + in List.iteri (apply length) ne_elements + and pp_tuple_pattern buffer ~pad:(_,pc) tuple = let patterns = Utils.nsepseq_to_list tuple.inside in let length = List.length patterns in @@ -1228,7 +1247,7 @@ and pp_fun_call buffer ~pad:(_,pc) (name, args) = and pp_record_patch buffer ~pad:(_,pc as pad) patch = pp_path buffer ~pad:(mk_pad 2 0 pc) patch.path; - pp_injection pp_field_assign buffer + pp_ne_injection pp_field_assign buffer ~pad patch.record_inj.value and pp_field_assign buffer ~pad:(_,pc as pad) {value; _} = @@ -1238,7 +1257,7 @@ and pp_field_assign buffer ~pad:(_,pc as pad) {value; _} = and pp_map_patch buffer ~pad:(_,pc as pad) patch = pp_path buffer ~pad:(mk_pad 2 0 pc) patch.path; - pp_injection pp_binding buffer + pp_ne_injection pp_binding buffer ~pad patch.map_inj.value and pp_binding buffer ~pad:(_,pc as pad) {value; _} = @@ -1249,7 +1268,7 @@ and pp_binding buffer ~pad:(_,pc as pad) {value; _} = and pp_set_patch buffer ~pad:(_,pc as pad) patch = pp_path buffer ~pad:(mk_pad 2 0 pc) patch.path; - pp_injection pp_expr buffer ~pad patch.set_inj.value + pp_ne_injection pp_expr buffer ~pad patch.set_inj.value and pp_map_remove buffer ~pad:(_,pc) rem = pp_expr buffer ~pad:(mk_pad 2 0 pc) rem.key; @@ -1260,17 +1279,14 @@ and pp_set_remove buffer ~pad:(_,pc) rem = pp_path buffer ~pad:(mk_pad 2 1 pc) rem.set and pp_local_decls buffer ~pad:(_,pc) decls = - match decls with - | Some decls -> - let apply len rank = - pp_local_decl buffer ~pad:(mk_pad len rank pc) - in List.iteri (List.length decls |> apply) decls - | None -> () + let apply len rank = + pp_local_decl buffer ~pad:(mk_pad len rank pc) + in List.iteri (List.length decls |> apply) decls and pp_local_decl buffer ~pad:(_,pc as pad) = function LocalFun {value; _} -> pp_node buffer ~pad "LocalFun"; - pp_fun_decl buffer ~pad:(mk_pad 1 0 pc) value + pp_fun_decl buffer ~pad value | LocalData data -> pp_node buffer ~pad "LocalData"; pp_data_decl buffer ~pad:(mk_pad 1 0 pc) data @@ -1469,10 +1485,9 @@ and pp_annotated buffer ~pad:(_,pc) (expr, t_expr) = pp_expr buffer ~pad:(mk_pad 2 0 pc) expr; pp_type_expr buffer ~pad:(mk_pad 2 1 pc) t_expr -and pp_bin_op node buffer ~pad:(_,pc) op = - pp_node buffer ~pad:(mk_pad 1 0 pc) node; - let _, pc = mk_pad 1 0 pc in - (pp_expr buffer ~pad:(mk_pad 2 0 pc) op.arg1; - pp_expr buffer ~pad:(mk_pad 2 1 pc) op.arg2) +and pp_bin_op node buffer ~pad:(_,pc as pad) op = + pp_node buffer ~pad node; + pp_expr buffer ~pad:(mk_pad 2 0 pc) op.arg1; + pp_expr buffer ~pad:(mk_pad 2 1 pc) op.arg2 let pp_ast buffer = pp_ast buffer ~pad:("","") diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index d094f3819..742c22eb7 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -78,16 +78,6 @@ module Errors = struct ] in error ~data title message - let unsupported_empty_record_patch record_expr = - let title () = "empty record patch" in - let message () = - Format.asprintf "empty record patches are not supported yet" in - let data = [ - ("record_loc", - fun () -> Format.asprintf "%a" Location.pp_lift @@ record_expr.Region.region) - ] in - error ~data title message - let unsupported_non_var_pattern p = let title () = "pattern is not a variable" in let message () = @@ -225,7 +215,7 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result = let%bind lst = bind_list @@ List.map aux @@ List.map apply - @@ pseq_to_list r.value.elements in + @@ npseq_to_list r.value.ne_elements in let m = List.fold_left (fun m (x, y) -> SMap.add x y m) SMap.empty lst in ok @@ T_record m | TSum s -> @@ -551,11 +541,6 @@ and simpl_fun_declaration : fun ~loc x -> let open! Raw in let {name;param;ret_type;local_decls;block;return} : fun_decl = x in - let local_decls = - match local_decls with - | Some local_decls -> local_decls - | None -> [] - in let statements = match block with | Some block -> npseq_to_list block.value.statements @@ -736,26 +721,32 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul | RecordPatch r -> ( let r = r.value in let (name , access_path) = simpl_path r.path in - let%bind inj = bind_list - @@ List.map (fun (x:Raw.field_assign Region.reg) -> + + let head, tail = r.record_inj.value.ne_elements in + + let%bind tail' = bind_list + @@ List.map (fun (x: Raw.field_assign Region.reg) -> let (x , loc) = r_split x in let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e , loc) ) - @@ pseq_to_list r.record_inj.value.elements in + @@ List.map snd tail in + + let%bind head' = + let (x , loc) = r_split head in + let%bind e = simpl_expression x.field_expr + in ok (x.field_name.value, e , loc) in + let%bind expr = let aux = fun (access , v , loc) -> - e_assign ~loc name (access_path @ [ Access_record access ]) v in - let assigns = List.map aux inj in - match assigns with - | [] -> fail @@ unsupported_empty_record_patch r.record_inj - | hd :: tl -> ( - let aux acc cur = e_sequence acc cur in - ok @@ List.fold_left aux hd tl - ) + e_assign ~loc name (access_path @ [Access_record access]) v in + + let hd, tl = aux head', List.map aux tail' in + let aux acc cur = e_sequence acc cur in + ok @@ List.fold_left aux hd tl in return_statement @@ expr - ) + ) | MapPatch patch -> ( let (map_p, loc) = r_split patch in let (name, access_path) = simpl_path map_p.path in @@ -767,7 +758,7 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul let%bind value' = simpl_expression value in ok @@ (key', value') ) - @@ pseq_to_list map_p.map_inj.value.elements in + @@ npseq_to_list map_p.map_inj.value.ne_elements in let expr = match inj with | [] -> e_skip ~loc () @@ -785,7 +776,7 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul let%bind inj = bind_list @@ List.map simpl_expression @@ - pseq_to_list setp.set_inj.value.elements in + npseq_to_list setp.set_inj.value.ne_elements in let expr = match inj with | [] -> e_skip ~loc () diff --git a/src/test/contracts/map.ligo b/src/test/contracts/map.ligo index a022379cd..5c169fe25 100644 --- a/src/test/contracts/map.ligo +++ b/src/test/contracts/map.ligo @@ -29,10 +29,6 @@ function patch_ (var m: foobar) : foobar is block { patch m with map [0 -> 5; 1 -> 6; 2 -> 7] } with m -function patch_empty (var m : foobar) : foobar is block { - patch m with map [] -} with m - function patch_deep (var m: foobar * nat) : foobar * nat is begin patch m.0 with map [1 -> 9]; end with m diff --git a/src/test/contracts/set_arithmetic.ligo b/src/test/contracts/set_arithmetic.ligo index 879d13940..eb0f8cf9e 100644 --- a/src/test/contracts/set_arithmetic.ligo +++ b/src/test/contracts/set_arithmetic.ligo @@ -26,11 +26,5 @@ function patch_op (var s: set(string)) : set(string) is function patch_op_deep (var s: set(string)*nat) : set(string)*nat is begin patch s.0 with set ["foobar"]; end with s -function patch_op_empty (var s: set(string)) : set(string) is - begin patch s with set []; end with s - function mem_op (const s : set(string)) : bool is begin skip end with set_mem("foobar" , s) - - - diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 401f446ce..cdc4f2196 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -20,7 +20,7 @@ let blockless () : unit result = let make_expect = fun n-> n + 10 in expect_eq_n_int program "blockless" make_expect -(* Procedures are not supported yet +(* Procedures are not supported yet let procedure () : unit result = let%bind program = type_file "./contracts/procedure.ligo" in let make_expect = fun n -> n + 1 in @@ -121,7 +121,7 @@ let higher_order () : unit result = let%bind _ = expect_eq_n_int program "foobar3" make_expect in let%bind _ = expect_eq_n_int program "foobar4" make_expect in let%bind _ = expect_eq_n_int program "foobar5" make_expect in - ok () + ok () let shared_function () : unit result = let%bind program = type_file "./contracts/function-shared.ligo" in @@ -256,11 +256,11 @@ let set_arithmetic () : unit result = (e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) (e_set [e_string "foo" ; e_string "bar"]) in let%bind () = - expect_eq program "remove_deep" - (e_pair + expect_eq program "remove_deep" + (e_pair (e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) (e_nat 42)) - (e_pair + (e_pair (e_set [e_string "foo" ; e_string "bar"]) (e_nat 42)) in @@ -276,10 +276,6 @@ let set_arithmetic () : unit result = (e_pair (e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) (e_nat 42)) in - let%bind () = - expect_eq program "patch_op_empty" - (e_set [e_string "foo" ; e_string "bar"]) - (e_set [e_string "foo" ; e_string "bar"]) in let%bind () = expect_eq program "mem_op" (e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) @@ -451,11 +447,6 @@ let map_ type_f path : unit result = let expected = ez [(0, 5) ; (1, 6) ; (2, 7)] in expect_eq program "patch_" input expected in - let%bind () = - let input = ez [(0,0) ; (1,1) ; (2,2)] in - let expected = ez [(0,0) ; (1,1) ; (2,2)] in - expect_eq program "patch_empty" input expected - in let%bind () = let input = (e_pair (ez [(0,0) ; (1,1) ; (2,2)]) @@ -630,9 +621,9 @@ let loop () : unit result = let make_input = e_nat in let make_expected = fun n -> e_nat (n * (n + 1) / 2) in expect_eq_n_pos_mid program "while_sum" make_input make_expected - in(* For loop is currently unsupported - - let%bind () = + in(* For loop is currently unsupported + + let%bind () = let make_input = e_nat in let make_expected = fun n -> e_nat (n * (n + 1) / 2) in expect_eq_n_pos_mid program "for_sum" make_input make_expected