fix contract with tuples starting at one

This commit is contained in:
Pierre-Emmanuel Wulfman 2020-02-19 16:15:43 +01:00
parent abfd561ffb
commit b8af9a56d9
15 changed files with 73 additions and 43 deletions

View File

@ -614,7 +614,7 @@ operation over maps is called `map_map` and is used as follows:
function map_op (const m : register) : register is function map_op (const m : register) : register is
block { block {
function increment (const i : address; const j : move) : move is function increment (const i : address; const j : move) : move is
(j.0, j.1 + 1); (j.1, j.2 + 1);
} with map_map (increment, m) } with map_map (increment, m)
``` ```
@ -664,7 +664,7 @@ follows:
```pascaligo group=f ```pascaligo group=f
function fold_op (const m : register) : int is block { function fold_op (const m : register) : int is block {
function folded (const j : int; const cur : address * move) : int is function folded (const j : int; const cur : address * move) : int is
j + cur.1.1 j + cur.2.2
} with map_fold (folded, m, 5) } with map_fold (folded, m, 5)
``` ```

View File

@ -84,10 +84,10 @@ let first_name : string = full_name.0
<!--ReasonLIGO--> <!--ReasonLIGO-->
Tuple components are one-indexed and accessed like so: Tuple components are zero-indexed and accessed like so:
```reasonligo group=tuple ```reasonligo group=tuple
let first_name : string = full_name[1]; let first_name : string = full_name[0];
``` ```
<!--END_DOCUSAURUS_CODE_TABS--> <!--END_DOCUSAURUS_CODE_TABS-->

View File

@ -238,7 +238,7 @@ rule `mapping_function`.
```pascaligo ```pascaligo
function map_op (const m : moveset) : moveset is function map_op (const m : moveset) : moveset is
block { block {
function increment (const i : address ; const j : move) : move is (j.0, j.1 + 1); function increment (const i : address ; const j : move) : move is (j.1, j.2 + 1);
} with map_map (increment, m); } with map_map (increment, m);
``` ```
@ -267,7 +267,7 @@ Combine every value in the map together according to a fold rule `folding_functi
```pascaligo ```pascaligo
function fold_op (const m : moveset) : int is function fold_op (const m : moveset) : int is
block { block {
function aggregate (const j : int; const cur : address * (int * int)) : int is j + cur.1.1 function aggregate (const j : int; const cur : address * (int * int)) : int is j + cur.2.2
} with map_fold(aggregate, m, 5) } with map_fold(aggregate, m, 5)
``` ```

View File

@ -591,6 +591,8 @@ let pattern_to_string ~offsets ~mode =
to_string ~offsets ~mode print_pattern to_string ~offsets ~mode print_pattern
let expr_to_string ~offsets ~mode = let expr_to_string ~offsets ~mode =
to_string ~offsets ~mode print_expr to_string ~offsets ~mode print_expr
let projection_to_string ~offsets ~mode =
to_string ~offsets ~mode print_projection
(** {1 Pretty-printing the AST} *) (** {1 Pretty-printing the AST} *)

View File

@ -17,6 +17,7 @@ val mk_state :
val print_tokens : state -> AST.t -> unit val print_tokens : state -> AST.t -> unit
val print_pattern : state -> AST.pattern -> unit val print_pattern : state -> AST.pattern -> unit
val print_expr : state -> AST.expr -> unit val print_expr : state -> AST.expr -> unit
val print_projection : state -> AST.projection Region.reg -> unit
val tokens_to_string : val tokens_to_string :
offsets:bool -> mode:[`Point|`Byte] -> AST.t -> string offsets:bool -> mode:[`Point|`Byte] -> AST.t -> string
@ -24,6 +25,8 @@ val pattern_to_string :
offsets:bool -> mode:[`Point|`Byte] -> AST.pattern -> string offsets:bool -> mode:[`Point|`Byte] -> AST.pattern -> string
val expr_to_string : val expr_to_string :
offsets:bool -> mode:[`Point|`Byte] -> AST.expr -> string offsets:bool -> mode:[`Point|`Byte] -> AST.expr -> string
val projection_to_string :
offsets:bool -> mode:[`Point|`Byte] -> AST.projection Region.reg -> string
(** {1 Pretty-printing of AST nodes} *) (** {1 Pretty-printing of AST nodes} *)

View File

@ -816,6 +816,8 @@ let pattern_to_string ~offsets ~mode =
to_string ~offsets ~mode print_pattern to_string ~offsets ~mode print_pattern
let instruction_to_string ~offsets ~mode = let instruction_to_string ~offsets ~mode =
to_string ~offsets ~mode print_instruction to_string ~offsets ~mode print_instruction
let projection_to_string ~offsets ~mode =
to_string ~offsets ~mode print_projection
(** {1 Pretty-printing the AST} *) (** {1 Pretty-printing the AST} *)

View File

@ -30,6 +30,8 @@ val pattern_to_string :
offsets:bool -> mode:[`Point|`Byte] -> AST.pattern -> string offsets:bool -> mode:[`Point|`Byte] -> AST.pattern -> string
val instruction_to_string : val instruction_to_string :
offsets:bool -> mode:[`Point|`Byte] -> AST.instruction -> string offsets:bool -> mode:[`Point|`Byte] -> AST.instruction -> string
val projection_to_string :
offsets:bool -> mode:[`Point|`Byte] -> AST.projection Region.reg -> string
(** {1 Pretty-printing of AST nodes} *) (** {1 Pretty-printing of AST nodes} *)

View File

@ -233,6 +233,20 @@ module Errors = struct
] in ] in
error ~data title message error ~data title message
let zero_index_access (p: _ Region.reg) =
let title () = "" in
let message () =
Format.asprintf "\n In PascaLigo, tuple indexes start at one \n" in
let pattern_loc = p.region in
let data = [
("location",
fun () -> Format.asprintf "%a" Location.pp_lift @@ pattern_loc);
("tuple",
fun () -> ParserLog.projection_to_string
~offsets:true ~mode:`Point p)
] in
error ~data title message
(* Logging *) (* Logging *)
let simplifying_instruction t = let simplifying_instruction t =
@ -348,13 +362,16 @@ let simpl_projection : Raw.projection Region.reg -> _ = fun p ->
let name = Var.of_name p'.struct_name.value in let name = Var.of_name p'.struct_name.value in
e_variable name in e_variable name in
let path = p'.field_path in let path = p'.field_path in
let path' = let%bind path' =
let aux (s:Raw.selection) = let aux (s:Raw.selection) =
match s with match s with
| FieldName property -> property.value | FieldName property -> ok property.value
| Component index -> (Z.to_string (snd index.value)) | Component index ->
let i:Z.t = Z.pred (snd index.value) in
if (Z.lt i Z.zero) then fail @@ zero_index_access p
else ok (Z.to_string i)
in in
List.map aux @@ npseq_to_list path in bind_map_list aux @@ npseq_to_list path in
ok @@ List.fold_left (e_accessor ~loc) var path' ok @@ List.fold_left (e_accessor ~loc) var path'
@ -547,7 +564,7 @@ let rec simpl_expression (t:Raw.expr) : expr result =
and simpl_update = fun (u:Raw.update Region.reg) -> and simpl_update = fun (u:Raw.update Region.reg) ->
let (u, loc) = r_split u in let (u, loc) = r_split u in
let (name, path) = simpl_path u.record in let%bind (name, path) = simpl_path u.record in
let record = match path with let record = match path with
| [] -> e_variable (Var.of_name name) | [] -> e_variable (Var.of_name name)
| _ -> e_accessor_list (e_variable (Var.of_name name)) path in | _ -> e_accessor_list (e_variable (Var.of_name name)) path in
@ -956,7 +973,7 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul
let%bind value_expr = simpl_expression a.rhs in let%bind value_expr = simpl_expression a.rhs in
match a.lhs with match a.lhs with
| Path path -> ( | Path path -> (
let (name , path') = simpl_path path in let%bind (name , path') = simpl_path path in
let (let_binder, mut, rhs, inline) = e_assign_with_let ~loc name path' value_expr in let (let_binder, mut, rhs, inline) = e_assign_with_let ~loc name path' value_expr in
return_let_in let_binder mut inline rhs return_let_in let_binder mut inline rhs
) )
@ -965,7 +982,7 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul
let%bind (varname,map,path) = match v'.path with let%bind (varname,map,path) = match v'.path with
| Name name -> ok (name.value , e_variable (Var.of_name name.value), []) | Name name -> ok (name.value , e_variable (Var.of_name name.value), [])
| Path p -> | Path p ->
let (name,p') = simpl_path v'.path in let%bind (name,p') = simpl_path v'.path in
let%bind accessor = simpl_projection p in let%bind accessor = simpl_projection p in
ok @@ (name , accessor , p') ok @@ (name , accessor , p')
in in
@ -1023,7 +1040,7 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul
} in } in
let u : Raw.update = {record=r.path;kwd_with=r.kwd_with; updates=update} in let u : Raw.update = {record=r.path;kwd_with=r.kwd_with; updates=update} in
let%bind expr = simpl_update {value=u;region=reg} in let%bind expr = simpl_update {value=u;region=reg} in
let (name , access_path) = simpl_path r.path in let%bind (name , access_path) = simpl_path r.path in
let loc = Some loc in let loc = Some loc in
let (binder, mut, rhs, inline) = e_assign_with_let ?loc name access_path expr in let (binder, mut, rhs, inline) = e_assign_with_let ?loc name access_path expr in
return_let_in binder mut inline rhs return_let_in binder mut inline rhs
@ -1031,7 +1048,7 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul
) )
| MapPatch patch -> ( | MapPatch patch -> (
let (map_p, loc) = r_split patch in let (map_p, loc) = r_split patch in
let (name, access_path) = simpl_path map_p.path in let%bind (name, access_path) = simpl_path map_p.path in
let%bind inj = bind_list let%bind inj = bind_list
@@ List.map (fun (x:Raw.binding Region.reg) -> @@ List.map (fun (x:Raw.binding Region.reg) ->
let x = x.value in let x = x.value in
@ -1054,7 +1071,7 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul
) )
| SetPatch patch -> ( | SetPatch patch -> (
let (setp, loc) = r_split patch in let (setp, loc) = r_split patch in
let (name , access_path) = simpl_path setp.path in let%bind (name , access_path) = simpl_path setp.path in
let%bind inj = let%bind inj =
bind_list @@ bind_list @@
List.map simpl_expression @@ List.map simpl_expression @@
@ -1074,7 +1091,7 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul
let%bind (varname,map,path) = match v.map with let%bind (varname,map,path) = match v.map with
| Name v -> ok (v.value , e_variable (Var.of_name v.value) , []) | Name v -> ok (v.value , e_variable (Var.of_name v.value) , [])
| Path p -> | Path p ->
let (name,p') = simpl_path v.map in let%bind (name,p') = simpl_path v.map in
let%bind accessor = simpl_projection p in let%bind accessor = simpl_projection p in
ok @@ (name , accessor , p') ok @@ (name , accessor , p')
in in
@ -1088,7 +1105,7 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul
let%bind (varname, set, path) = match set_rm.set with let%bind (varname, set, path) = match set_rm.set with
| Name v -> ok (v.value, e_variable (Var.of_name v.value), []) | Name v -> ok (v.value, e_variable (Var.of_name v.value), [])
| Path path -> | Path path ->
let(name, p') = simpl_path set_rm.set in let%bind (name, p') = simpl_path set_rm.set in
let%bind accessor = simpl_projection path in let%bind accessor = simpl_projection path in
ok @@ (name, accessor, p') ok @@ (name, accessor, p')
in in
@ -1098,21 +1115,25 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul
return_let_in binder mut inline rhs return_let_in binder mut inline rhs
) )
and simpl_path : Raw.path -> string * string list = fun p -> and simpl_path : Raw.path -> (string * string list) result = fun p ->
match p with match p with
| Raw.Name v -> (v.value , []) | Raw.Name v -> ok (v.value , [])
| Raw.Path p -> ( | Raw.Path p -> (
let p' = p.value in let p' = p.value in
let var = p'.struct_name.value in let var = p'.struct_name.value in
let path = p'.field_path in let path = p'.field_path in
let path' = let%bind path' =
let aux (s:Raw.selection) = let aux (s:Raw.selection) =
match s with match s with
| FieldName property -> property.value | FieldName property -> ok property.value
| Component index -> (Z.to_string (snd index.value)) | Component index ->
let i:Z.t = Z.pred (snd index.value) in
if (Z.lt i Z.zero) then fail @@ zero_index_access p
else ok (Z.to_string i)
in in
List.map aux @@ npseq_to_list path in bind_map_list aux @@ npseq_to_list path
(var , path') in
ok (var , path')
) )
and simpl_cases : (Raw.pattern * expression) list -> matching_expr result = fun t -> and simpl_cases : (Raw.pattern * expression) list -> matching_expr result = fun t ->

View File

@ -5,8 +5,8 @@ type return is list (operation) * storage
function main (const p : parameter; const s : storage) : return is function main (const p : parameter; const s : storage) : return is
block { block {
var toto : option (int) := Some (0); var toto : option (int) := Some (0);
toto := s.0[23]; toto := s.1[23];
s.0[2] := 444 s.1[2] := 444
} }
with ((nil: list(operation)), s) with ((nil: list(operation)), s)

View File

@ -11,14 +11,14 @@ function main (const toto : unit) : int is
var a : ppp := var a : ppp :=
(record [x = (0,1); y = (10,11)], (record [x = (0,1); y = (10,11)],
record [x = (100,101); y = (110,111)]); record [x = (100,101); y = (110,111)]);
a.0.x.0 := 2; a.1.x.1 := 2;
} with a.0.x.0 } with a.1.x.1
function asymetric_tuple_access (const foo : unit) : int is function asymetric_tuple_access (const foo : unit) : int is
block { block {
var tuple : int * (int * (int * int)) := (0,(1,(2,3))) var tuple : int * (int * (int * int)) := (0,(1,(2,3)))
} with tuple.0 + tuple.1.0 + tuple.1.1.0 + tuple.1.1.1 } with tuple.1 + tuple.2.1 + tuple.2.2.1 + tuple.2.2.2
type nested_record_t is type nested_record_t is
record [nesty : record [mymap : map (int,string)]] record [nesty : record [mymap : map (int,string)]]

View File

@ -8,4 +8,4 @@ function main(const p : parameter; const s : storage) : return is
function main (const p : parameter; const s : storage) : return is function main (const p : parameter; const s : storage) : return is
block { block {
const ret : return = main (p, s) const ret : return = main (p, s)
} with (ret.0, ret.1 + 1) } with (ret.1, ret.2 + 1)

View File

@ -28,7 +28,7 @@ function patch_ (var m : foobar) : foobar is block {
} with m } with m
function patch_deep (var m : foobar * nat) : foobar * nat is function patch_deep (var m : foobar * nat) : foobar * nat is
block { patch m.0 with map [1 -> 9] } with m block { patch m.1 with map [1 -> 9] } with m
function size_ (const m : foobar) : nat is size (m) function size_ (const m : foobar) : nat is size (m)
@ -54,12 +54,12 @@ function map_op (const m : foobar) : foobar is
function fold_op (const m : foobar) : int is function fold_op (const m : foobar) : int is
block { block {
function aggregate (const i : int; const j : int * int) : int is function aggregate (const i : int; const j : int * int) : int is
i + j.0 + j.1 i + j.1 + j.2
} with map_fold(aggregate, m, 10) } with map_fold(aggregate, m, 10)
function deep_op (var m : foobar) : foobar is function deep_op (var m : foobar) : foobar is
block { block {
var coco : int * foobar := (0, m); var coco : int * foobar := (0, m);
remove 42 from map coco.1; remove 42 from map coco.2;
coco.1[32] := 16 coco.2[32] := 16
} with coco.1 } with coco.2

View File

@ -47,8 +47,8 @@ function check_message (const param : check_message_pt;
nil -> skip nil -> skip
| key # tl -> block { | key # tl -> block {
keys := tl; keys := tl;
if pkh_sig.0 = crypto_hash_key (key) then if pkh_sig.1 = crypto_hash_key (key) then
if crypto_check (key, pkh_sig.1, packed_payload) if crypto_check (key, pkh_sig.2, packed_payload)
then valid := valid + 1n then valid := valid + 1n
else failwith ("Invalid signature") else failwith ("Invalid signature")
else skip else skip

View File

@ -11,8 +11,8 @@ function main (const toto : tpi) : int is
var a : tpi := toto; var a : tpi := toto;
var b : rpi := record x = 0; y=1 ; end; var b : rpi := record x = 0; y=1 ; end;
var m : mpi := map "y" -> 1; end; var m : mpi := map "y" -> 1; end;
a.0 := 2; a.1 := 2;
b.x := a.0; b.x := a.1;
m["x"] := b.x; m["x"] := b.x;
end with end with
case m["x"] of case m["x"] of

View File

@ -1,11 +1,11 @@
type abc is (int * int * int) type abc is (int * int * int)
function projection_abc (const tpl : abc) : int is function projection_abc (const tpl : abc) : int is
block { skip } with tpl.1 block { skip } with tpl.2
function modify_abc (const tpl : abc) : abc is function modify_abc (const tpl : abc) : abc is
block { block {
tpl.1 := 2048 ; tpl.2 := 2048 ;
} with tpl } with tpl
type foobar is (int * int) type foobar is (int * int)
@ -15,7 +15,7 @@ const fb : foobar = (0, 0)
function projection (const tpl : foobar) : int is function projection (const tpl : foobar) : int is
begin begin
skip skip
end with tpl.0 + tpl.1 end with tpl.1 + tpl.2
type big_tuple is (int * int * int * int * int) type big_tuple is (int * int * int * int * int)