replace tuples by records
This commit is contained in:
parent
d29502c926
commit
d7426504d0
@ -166,20 +166,6 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
|
||||
i_pair ;
|
||||
i_exec ; (* output :: stack :: env *)
|
||||
]
|
||||
(* return @@ virtual_push @@ seq [
|
||||
* i_comment "(\* unit :: env *\)" ;
|
||||
* i_comment "compute closure" ;
|
||||
* f' ;
|
||||
* i_comment "(\* (closure * unit) :: env *\)" ;
|
||||
* i_comment "compute arg" ;
|
||||
* arg' ;
|
||||
* i_comment "(\* (arg * closure * unit) :: env *\)" ;
|
||||
* i_comment "separate stuff" ;
|
||||
* i_unpair ; dip i_unpair ; dip i_unpair ;
|
||||
* i_comment "(\* arg :: capture :: f :: unit :: env *\)" ;
|
||||
* i_pair ;
|
||||
* i_exec ; (\* output :: stack :: env *\)
|
||||
* ] *)
|
||||
)
|
||||
| _ -> simple_fail "E_applicationing something not appliable"
|
||||
)
|
||||
|
@ -1,3 +1,6 @@
|
||||
type heap_element is int * string
|
||||
|
||||
function heap_element_lt(const x : heap_element ; const y : heap_element) : bool is
|
||||
block { skip } with x.0 < y.0
|
||||
|
||||
#include "heap.ligo"
|
||||
|
@ -13,14 +13,22 @@ function pop_switch (const h : heap) : heap is
|
||||
const last : heap_element = get_force(s, h) ;
|
||||
remove 1n from map h ;
|
||||
h[1n] := last ;
|
||||
} with h ;
|
||||
} with h
|
||||
|
||||
|
||||
// function pop (const h : heap) : heap is
|
||||
// function largest_child (const h : heap) : nat is
|
||||
// block {
|
||||
// const result : heap_element = get_top (h) ;
|
||||
// const s : nat = size(h) ;
|
||||
// const last : heap_element = get_force(int(s), h) ;
|
||||
// remove 1 from map h ;
|
||||
// h[1] := last ;
|
||||
// } with h ;
|
||||
// var current : heap_element := get_force(s, h) ;
|
||||
// const i : nat = 1n ;
|
||||
// const left : nat = 2n * i ;
|
||||
// const right : nat = left + 1n ;
|
||||
// remove 1n from map h ;
|
||||
// h[1n] := current ;
|
||||
// var largest : nat := i ;
|
||||
// if (left <= s and heap_element_lt(get_force(s , h) , get_force(left , h))) then
|
||||
// largest := left
|
||||
// else if (right <= s and heap_element_lt(get_force(s , h) , get_force(right , h))) then
|
||||
// largest := right
|
||||
// else skip
|
||||
// } with largest
|
||||
|
4
src/ligo/contracts/shadow.ligo
Normal file
4
src/ligo/contracts/shadow.ligo
Normal file
@ -0,0 +1,4 @@
|
||||
function foo (const i : int) : int is
|
||||
function bar (const i : int) : int is
|
||||
block { skip } with i ;
|
||||
block { skip } with bar (0)
|
@ -35,13 +35,25 @@ let parse_file (source: string) : AST_Raw.t result =
|
||||
let start = Lexing.lexeme_start_p lexbuf in
|
||||
let end_ = Lexing.lexeme_end_p lexbuf in
|
||||
let str = Format.sprintf
|
||||
"Parse error at \"%s\" from (%d, %d) to (%d, %d)\n"
|
||||
"Parse error at \"%s\" from (%d, %d) to (%d, %d). In file \"%s|%s\"\n"
|
||||
(Lexing.lexeme lexbuf)
|
||||
start.pos_lnum (start.pos_cnum - start.pos_bol)
|
||||
end_.pos_lnum (end_.pos_cnum - end_.pos_bol) in
|
||||
end_.pos_lnum (end_.pos_cnum - end_.pos_bol)
|
||||
start.pos_fname source
|
||||
in
|
||||
simple_error str
|
||||
)
|
||||
| _ -> simple_error "unrecognized parse_ error"
|
||||
| _ ->
|
||||
let start = Lexing.lexeme_start_p lexbuf in
|
||||
let end_ = Lexing.lexeme_end_p lexbuf in
|
||||
let str = Format.sprintf
|
||||
"Unrecognized error at \"%s\" from (%d, %d) to (%d, %d). In file \"%s|%s\"\n"
|
||||
(Lexing.lexeme lexbuf)
|
||||
start.pos_lnum (start.pos_cnum - start.pos_bol)
|
||||
end_.pos_lnum (end_.pos_cnum - end_.pos_bol)
|
||||
start.pos_fname source
|
||||
in
|
||||
simple_error str
|
||||
) @@ (fun () ->
|
||||
let raw = Parser.contract read lexbuf in
|
||||
close () ;
|
||||
|
@ -162,31 +162,31 @@ module Typer = struct
|
||||
let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in
|
||||
Map.String.of_list
|
||||
@@ List.map typer_to_kv [
|
||||
same_2 "ADD" [
|
||||
("ADD_INT" , t_int ()) ;
|
||||
("ADD_NAT" , t_nat ()) ;
|
||||
("CONCAT" , t_string ()) ;
|
||||
] ;
|
||||
same_2 "TIMES" [
|
||||
("TIMES_INT" , t_int ()) ;
|
||||
("TIMES_NAT" , t_nat ()) ;
|
||||
] ;
|
||||
sub ;
|
||||
none ;
|
||||
some ;
|
||||
comparator "EQ" ;
|
||||
comparator "LT" ;
|
||||
comparator "GT" ;
|
||||
comparator "LE" ;
|
||||
comparator "GE" ;
|
||||
boolean_operator_2 "OR" ;
|
||||
boolean_operator_2 "AND" ;
|
||||
map_remove ;
|
||||
map_update ;
|
||||
int ;
|
||||
size ;
|
||||
get_force ;
|
||||
]
|
||||
same_2 "ADD" [
|
||||
("ADD_INT" , t_int ()) ;
|
||||
("ADD_NAT" , t_nat ()) ;
|
||||
("CONCAT" , t_string ()) ;
|
||||
] ;
|
||||
same_2 "TIMES" [
|
||||
("TIMES_INT" , t_int ()) ;
|
||||
("TIMES_NAT" , t_nat ()) ;
|
||||
] ;
|
||||
sub ;
|
||||
none ;
|
||||
some ;
|
||||
comparator "EQ" ;
|
||||
comparator "LT" ;
|
||||
comparator "GT" ;
|
||||
comparator "LE" ;
|
||||
comparator "GE" ;
|
||||
boolean_operator_2 "OR" ;
|
||||
boolean_operator_2 "AND" ;
|
||||
map_remove ;
|
||||
map_update ;
|
||||
int ;
|
||||
size ;
|
||||
get_force ;
|
||||
]
|
||||
|
||||
end
|
||||
|
||||
|
@ -318,16 +318,29 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
|
||||
ok {name;annotated_expression = {expression;type_annotation}}
|
||||
)
|
||||
| lst -> (
|
||||
let arguments_name = "arguments" in
|
||||
let%bind params = bind_map_list simpl_param lst in
|
||||
let input =
|
||||
let type_expression = T_record (
|
||||
SMap.of_list
|
||||
@@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression)
|
||||
params
|
||||
) in
|
||||
{ type_name = "arguments" ; type_expression } in
|
||||
let aux = fun x -> x.type_expression in
|
||||
let type_expression = T_tuple (List.map aux params) in
|
||||
{ type_name = arguments_name ; type_expression } in
|
||||
let binder = input.type_name in
|
||||
let input_type = input.type_expression in
|
||||
let tpl_declarations =
|
||||
let aux = fun i (x:named_type_expression) ->
|
||||
let ass = I_assignment {
|
||||
name = x.type_name ;
|
||||
annotated_expression = {
|
||||
expression = E_accessor ({
|
||||
expression = E_variable arguments_name ;
|
||||
type_annotation = Some input.type_expression ;
|
||||
} , [ Access_tuple i ] ) ;
|
||||
type_annotation = Some (x.type_expression) ;
|
||||
}
|
||||
} in
|
||||
ass
|
||||
in
|
||||
List.mapi aux params in
|
||||
let%bind local_declarations =
|
||||
let%bind typed = bind_map_list simpl_local_declaration local_decls in
|
||||
ok (List.map fst typed)
|
||||
@ -336,22 +349,9 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
|
||||
let%bind instructions = bind_list
|
||||
@@ List.map simpl_statement
|
||||
@@ npseq_to_list block.value.statements in
|
||||
let%bind (body, result) =
|
||||
let renamings =
|
||||
let aux ({type_name}:named_type_expression) : Rename.Value.renaming =
|
||||
type_name, ("arguments", [Access_record type_name])
|
||||
in
|
||||
List.map aux params
|
||||
in
|
||||
let%bind r =
|
||||
let%bind tmp = simpl_expression return in
|
||||
Rename.Value.rename_annotated_expression renamings tmp
|
||||
in
|
||||
let%bind b =
|
||||
let tmp = local_declarations @ instructions in
|
||||
Rename.Value.rename_block renamings tmp
|
||||
in
|
||||
ok (b, r) in
|
||||
|
||||
let body = tpl_declarations @ local_declarations @ instructions in
|
||||
let%bind result = simpl_expression return in
|
||||
let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
|
||||
let type_annotation = Some (T_function (input_type, output_type)) in
|
||||
ok {name = name.value;annotated_expression = {expression;type_annotation}}
|
||||
|
@ -67,6 +67,21 @@ let closure () : unit result =
|
||||
@@ [0 ; 2 ; 42 ; 163 ; -1] in
|
||||
ok ()
|
||||
|
||||
let shadow () : unit result =
|
||||
let%bind program = type_file "./contracts/shadow.ligo" in
|
||||
let%bind _foo = trace (simple_error "test foo") @@
|
||||
let aux n =
|
||||
let open AST_Typed.Combinators in
|
||||
let input = e_a_int n in
|
||||
let%bind result = easy_run_typed "foo" program input in
|
||||
let expected = e_a_int 0 in
|
||||
AST_Typed.assert_value_eq (expected, result)
|
||||
in
|
||||
bind_list
|
||||
@@ List.map aux
|
||||
@@ [3 ; 2 ; 0 ; 42 ; 163 ; -1] in
|
||||
ok ()
|
||||
|
||||
let higher_order () : unit result =
|
||||
let%bind program = type_file "./contracts/high-order.ligo" in
|
||||
let%bind _foo = trace (simple_error "test foo") @@
|
||||
@ -314,7 +329,7 @@ let map () : unit result =
|
||||
let aux n =
|
||||
let input =
|
||||
let m = ez [(23, 0) ; (42, 0)] in
|
||||
AST_Typed.Combinators.(ez_e_a_record [("n", e_a_int n) ; ("m", m)])
|
||||
AST_Typed.Combinators.(e_a_tuple [ e_a_int n ; m ])
|
||||
in
|
||||
let%bind result = easy_run_typed "set_" program input in
|
||||
let expect = ez [(23, n) ; (42, 0)] in
|
||||
@ -552,6 +567,8 @@ let main = "Integration (End to End)", [
|
||||
test "complex function" complex_function ;
|
||||
test "closure" closure ;
|
||||
test "shared function" shared_function ;
|
||||
test "shadow" shadow ;
|
||||
test "multiple parameters" multiple_parameters ;
|
||||
test "bool" bool_expression ;
|
||||
test "arithmetic" arithmetic ;
|
||||
test "unit" unit_expression ;
|
||||
@ -560,7 +577,6 @@ let main = "Integration (End to End)", [
|
||||
test "option" option ;
|
||||
test "map" map ;
|
||||
test "list" list ;
|
||||
test "multiple parameters" multiple_parameters ;
|
||||
test "condition" condition ;
|
||||
test "loop" loop ;
|
||||
test "matching" matching ;
|
||||
|
@ -61,26 +61,21 @@ let rec translate_type (t:AST.type_value) : type_value result =
|
||||
let%bind result' = translate_type result in
|
||||
ok (T_function (param', result'))
|
||||
|
||||
let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * (type_value * [`Left | `Right]) list) result = fun ty tys ind ->
|
||||
let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * [`Left | `Right]) list result = fun ty tys ind ->
|
||||
let node_tv = Append_tree.of_list @@ List.mapi (fun i a -> (i, a)) tys in
|
||||
let leaf (i, _) : (type_value * (type_value * [`Left | `Right]) list) result =
|
||||
if i = ind then (
|
||||
ok (ty, [])
|
||||
) else (
|
||||
simple_fail "bad leaf"
|
||||
) in
|
||||
let node a b : (type_value * (type_value * [`Left | `Right]) list) result =
|
||||
match%bind bind_lr (a, b) with
|
||||
| `Left (t, acc) ->
|
||||
let%bind (a, _) = get_t_pair t in
|
||||
ok @@ (t, (a, `Left) :: acc)
|
||||
| `Right (t, acc) -> (
|
||||
let%bind (_, b) = get_t_pair t in
|
||||
ok @@ (t, (b, `Right) :: acc)
|
||||
) in
|
||||
let error_content () = Format.asprintf "(%a).%d" (PP.list_sep_d PP.type_) tys ind in
|
||||
trace_strong (fun () -> error (thunk "bad index in tuple (shouldn't happen here)") error_content ()) @@
|
||||
Append_tree.fold_ne leaf node node_tv
|
||||
let%bind path =
|
||||
let aux (i , _) = i = ind in
|
||||
trace_option (simple_error "no leaf with given index") @@
|
||||
Append_tree.exists_path aux node_tv in
|
||||
let lr_path = List.map (fun b -> if b then `Right else `Left) path in
|
||||
let%bind (_ , lst) =
|
||||
let aux = fun (ty , acc) cur ->
|
||||
let%bind (a , b) = get_t_pair ty in
|
||||
match cur with
|
||||
| `Left -> ok (a , (a , `Left) :: acc)
|
||||
| `Right -> ok (b , (b , `Right) :: acc) in
|
||||
bind_fold_list aux (ty , []) lr_path in
|
||||
ok lst
|
||||
|
||||
let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -> (type_value * (type_value * [`Left | `Right]) list) result = fun ty tym ind ->
|
||||
let tys = kv_list_of_map tym in
|
||||
@ -133,7 +128,7 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
|
||||
| Access_tuple ind ->
|
||||
let%bind ty_lst = AST.Combinators.get_t_tuple prev in
|
||||
let%bind ty'_lst = bind_map_list translate_type ty_lst in
|
||||
let%bind (_, path) = tuple_access_to_lr ty' ty'_lst ind in
|
||||
let%bind path = tuple_access_to_lr ty' ty'_lst ind in
|
||||
let path' = List.map snd path in
|
||||
ok (List.nth ty_lst ind, path' @ acc)
|
||||
| Access_record prop ->
|
||||
@ -243,17 +238,17 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
||||
in
|
||||
Append_tree.fold_ne (translate_annotated_expression env) aux node
|
||||
| E_tuple_accessor (tpl, ind) ->
|
||||
let%bind ty' = translate_type tpl.type_annotation in
|
||||
let%bind ty_lst = get_t_tuple tpl.type_annotation in
|
||||
let%bind ty'_lst = bind_map_list translate_type ty_lst in
|
||||
let%bind ty' = translate_type tpl.type_annotation in
|
||||
let%bind (_, path) = tuple_access_to_lr ty' ty'_lst ind in
|
||||
let%bind path = tuple_access_to_lr ty' ty'_lst ind in
|
||||
let aux = fun pred (ty, lr) ->
|
||||
let c = match lr with
|
||||
| `Left -> "CAR"
|
||||
| `Right -> "CDR" in
|
||||
Combinators.Expression.make_tpl (E_constant (c, [pred]) , ty , env) in
|
||||
let%bind tpl' = translate_annotated_expression env tpl in
|
||||
let expr = List.fold_left aux tpl' path in
|
||||
let expr = List.fold_right' aux tpl' path in
|
||||
ok expr
|
||||
| E_record m ->
|
||||
let node = Append_tree.of_list @@ list_of_map m in
|
||||
|
@ -326,7 +326,8 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
|
||||
generic_try (simple_error "bad tuple index")
|
||||
@@ (fun () -> List.nth tpl_tv index) in
|
||||
let%bind type_annotation = check tv in
|
||||
ok O.{expression = O.E_tuple_accessor (prev, index) ; type_annotation}
|
||||
let annotated_expression = O.{expression = E_tuple_accessor (prev, index) ; type_annotation} in
|
||||
ok annotated_expression
|
||||
)
|
||||
| Access_record property -> (
|
||||
let%bind r_tv = get_t_record prev.type_annotation in
|
||||
@ -468,8 +469,13 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
|
||||
Assert.assert_true (arity = l) in
|
||||
|
||||
let error =
|
||||
let title () = "typing: unrecognized constant" in
|
||||
let content () = name in
|
||||
let title () = "typing: constant predicates all failed" in
|
||||
let content () =
|
||||
Format.asprintf "%s in %a"
|
||||
name
|
||||
PP_helpers.(list_sep Ast_typed.PP.type_value (const " , "))
|
||||
lst
|
||||
in
|
||||
error title content in
|
||||
let rec aux = fun ts ->
|
||||
match ts with
|
||||
|
Loading…
Reference in New Issue
Block a user