'convert_from_left_comb' and 'convert_from_right_comb' for sum types

This commit is contained in:
Lesenechal Remi 2020-04-30 23:58:57 +02:00
parent 8fdf9a8b95
commit 5891a6f4cc
9 changed files with 239 additions and 90 deletions

View File

@ -36,13 +36,13 @@ let%expect_test _ =
( 2 , ( +3 , "q" ) ) |}] ;
run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_pair.mligo") ; "r4"] ;
[%expect {|
( 2 , ( +3 , ( "q" , true ) ) ) |}] ;
( 2 , ( +3 , ( "q" , true(unit) ) ) ) |}] ;
run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_pair.mligo") ; "l3"] ;
[%expect {|
( ( 2 , +3 ) , "q" ) |}] ;
run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_pair.mligo") ; "l4"] ;
[%expect {|
( ( ( 2 , +3 ) , "q" ) , true ) |}];
( ( ( 2 , +3 ) , "q" ) , true(unit) ) |}];
run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_or.mligo") ; "str3"] ;
[%expect {|
M_right(M_left(+3)) |}] ;
@ -100,7 +100,74 @@ let%expect_test _ =
CONCAT ;
NIL operation ;
PAIR ;
DIP { DROP 2 } } } |}]
DIP { DROP 2 } } } |}];
run_ligo_good [ "dry-run" ; contract "michelson_converter_or.mligo" ; "main_r" ; "vr" ; "Foo4 2"] ;
[%expect {|
( LIST_EMPTY() , Baz4("eq") ) |}] ;
run_ligo_good [ "compile-contract" ; contract "michelson_converter_or.mligo" ; "main_r" ] ;
[%expect {|
{ parameter (or (int %Foo4) (or (nat %Bar4) (or (string %Baz4) (bool %Boz4)))) ;
storage (or (or (nat %bar4) (string %baz4)) (or (bool %boz4) (int %foo4))) ;
code { PUSH string "eq" ;
LEFT bool ;
RIGHT nat ;
RIGHT int ;
PUSH string "eq" ;
RIGHT (or (int %foo4) (nat %bar4)) ;
LEFT bool ;
DIG 2 ;
DUP ;
DUG 3 ;
CAR ;
IF_LEFT
{ DUP ; RIGHT bool ; RIGHT (or nat string) ; DIP { DROP } }
{ DUP ;
IF_LEFT
{ DUP ; LEFT string ; LEFT (or bool int) ; DIP { DROP } }
{ DUP ;
IF_LEFT
{ DUP ; RIGHT nat ; LEFT (or bool int) ; DIP { DROP } }
{ DUP ; LEFT int ; RIGHT (or nat string) ; DIP { DROP } } ;
DIP { DROP } } ;
DIP { DROP } } ;
DUP ;
NIL operation ;
PAIR ;
DIP { DROP 4 } } } |}] ;
run_ligo_good [ "dry-run" ; contract "michelson_converter_or.mligo" ; "main_l" ; "vl" ; "Foo4 2"] ;
[%expect {|
( LIST_EMPTY() , Baz4("eq") ) |}] ;
run_ligo_good [ "compile-contract" ; contract "michelson_converter_or.mligo" ; "main_l" ] ;
[%expect {|
{ parameter (or (or (or (int %Foo4) (nat %Bar4)) (string %Baz4)) (bool %Boz4)) ;
storage (or (or (nat %bar4) (string %baz4)) (or (bool %boz4) (int %foo4))) ;
code { PUSH string "eq" ;
LEFT bool ;
RIGHT nat ;
RIGHT int ;
PUSH string "eq" ;
RIGHT (or (int %foo4) (nat %bar4)) ;
LEFT bool ;
DIG 2 ;
DUP ;
DUG 3 ;
CAR ;
IF_LEFT
{ DUP ;
IF_LEFT
{ DUP ;
IF_LEFT
{ DUP ; RIGHT bool ; RIGHT (or nat string) ; DIP { DROP } }
{ DUP ; LEFT string ; LEFT (or bool int) ; DIP { DROP } } ;
DIP { DROP } }
{ DUP ; RIGHT nat ; LEFT (or bool int) ; DIP { DROP } } ;
DIP { DROP } }
{ DUP ; LEFT int ; RIGHT (or nat string) ; DIP { DROP } } ;
DUP ;
NIL operation ;
PAIR ;
DIP { DROP 4 } } } |}]
let%expect_test _ =
run_ligo_good [ "compile-contract" ; contract "michelson_comb_type_operators.mligo" ; "main_r"] ;

View File

@ -1,4 +1,4 @@
open Ast_typed
open Stage_common.Constant
let environment = env_sum_type ~type_name:t_bool @@ [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None})]
let environment = env_sum_type ~type_name:t_bool @@ [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=0});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=1})]

View File

@ -236,8 +236,6 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
| Empty -> fail @@ corner_case ~loc:__LOC__ "empty record"
| Full t -> ok t in
let%bind lst =
(* let () = Format.printf "\n%a\n" Ast_typed.PP.type_expression t in
let () = Format.printf "\n%a\n" Mini_c.PP.value v in *)
trace_strong (corner_case ~loc:__LOC__ "record extract") @@
extract_record v node in
let%bind lst = bind_list

View File

@ -519,7 +519,7 @@ and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) :
)
and type_match : (environment -> I.expression -> O.expression result) -> environment -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> O.matching_expr result =
fun f e t i ae loc -> match i with
fun f e t i _ae loc -> match i with
| Match_option {match_none ; match_some} ->
let%bind tv =
trace_strong (match_error ~expected:i ~actual:t loc)

View File

@ -21,11 +21,25 @@ let constructor (constructor:constructor') (element:expression) (t:type_expressi
type_expression = t ;
environment = element.environment }
let match_var env (t:type_expression) =
let match_var (t:type_expression) =
{ expression_content = E_variable (Var.of_name "x") ;
location = Location.generated ;
type_expression = t ;
environment = env }
environment = Environment.add_ez_binder (Var.of_name "x") t Environment.full_empty}
let matching (e:expression) matchee cases =
{ expression_content = E_matching {matchee ; cases};
location = Location.generated ;
type_expression = e.type_expression ;
environment = e.environment }
let rec descend_types s lmap i =
if i > 0 then
let {ctor_type;_} = CMap.find (Constructor s) lmap in
match ctor_type.type_content with
| T_sum a -> ctor_type::(descend_types s a (i-1))
| _ -> []
else []
let rec to_left_comb_record' first prev l conv_map =
match l with
@ -43,20 +57,12 @@ let rec to_left_comb_record' first prev l conv_map =
to_left_comb_record' first prev tl conv_map'
let to_left_comb_record = to_left_comb_record' true
let rec to_right_comb_variant' (i:int) (e:expression) (dst_lmap:ctor_content constructor_map) (src_kvl:(constructor' * ctor_content) list) : expression list =
let rec descend_types lmap i =
if i > 0 then
let {ctor_type;_} = CMap.find (Constructor "M_right") lmap in
match ctor_type.type_content with
| T_sum a -> ctor_type::(descend_types a (i-1))
| _ -> []
else [] in
let intermediary_types i = if i = 0 then [] else e.type_expression::(descend_types dst_lmap i) in
let rec right_comb_variant_combination' (i:int) (e:expression) (dst_lmap:ctor_content constructor_map) (src_kvl:(constructor' * ctor_content) list) : expression list =
let intermediary_types i = if i = 0 then [] else e.type_expression::(descend_types "M_right" dst_lmap i) in
let rec comb (ctor_type,outer) l =
let env' = Environment.add_ez_binder (Var.of_name "x") ctor_type e.environment in
match l with
| [] -> constructor outer (match_var env' ctor_type) e.type_expression
| [t] -> constructor outer (match_var env' ctor_type) t
| [] -> constructor outer (match_var ctor_type) e.type_expression
| [t] -> constructor outer (match_var ctor_type) t
| t::tl -> constructor (Constructor "M_right") (comb (ctor_type,outer) tl) t in
( match src_kvl with
| [] -> []
@ -65,23 +71,15 @@ let rec to_right_comb_variant' (i:int) (e:expression) (dst_lmap:ctor_content con
[comb (ctor_type,Constructor "M_right") combs_t]
| (_,{ctor_type;_})::tl ->
let combs_t = intermediary_types i in
(comb (ctor_type,Constructor "M_left") combs_t) :: to_right_comb_variant' (i+1) e dst_lmap tl )
let to_right_comb_variant = to_right_comb_variant' 0
(comb (ctor_type,Constructor "M_left") combs_t) :: right_comb_variant_combination' (i+1) e dst_lmap tl )
let right_comb_variant_combination = right_comb_variant_combination' 0
let rec to_left_comb_variant' (i:int) (e:expression) (dst_lmap:ctor_content constructor_map) (src_kvl:(constructor' * ctor_content) list) : expression list =
let rec descend_types lmap i =
if i > 0 then
let {ctor_type;_} = CMap.find (Constructor "M_left") lmap in
match ctor_type.type_content with
| T_sum a -> ctor_type::(descend_types a (i-1))
| _ -> []
else [] in
let intermediary_types i = if i = 0 then [] else e.type_expression::(descend_types dst_lmap i) in
let rec left_comb_variant_combination' (i:int) (e:expression) (dst_lmap:ctor_content constructor_map) (src_kvl:(constructor' * ctor_content) list) : expression list =
let intermediary_types i = if i = 0 then [] else e.type_expression::(descend_types "M_left" dst_lmap i) in
let rec comb (ctor_type,outer) l =
let env' = Environment.add_ez_binder (Var.of_name "x") ctor_type e.environment in
match l with
| [] -> constructor outer (match_var env' ctor_type) e.type_expression
| [t] -> constructor outer (match_var env' ctor_type) t
| [] -> constructor outer (match_var ctor_type) e.type_expression
| [t] -> constructor outer (match_var ctor_type) t
| t::tl -> constructor (Constructor "M_left") (comb (ctor_type,outer) tl) t in
( match src_kvl with
| [] -> []
@ -90,8 +88,8 @@ let rec to_left_comb_variant' (i:int) (e:expression) (dst_lmap:ctor_content cons
[comb (ctor_type,Constructor "M_left") combs_t]
| (_,{ctor_type;_})::tl ->
let combs_t = intermediary_types i in
(comb (ctor_type,Constructor "M_right") combs_t) :: to_left_comb_variant' (i+1) e dst_lmap tl )
let to_left_comb_variant a b c = List.rev @@ to_left_comb_variant' 0 a b (List.rev c)
(comb (ctor_type,Constructor "M_right") combs_t) :: left_comb_variant_combination' (i+1) e dst_lmap tl )
let left_comb_variant_combination a b c = List.rev @@ left_comb_variant_combination' 0 a b (List.rev c)
let rec to_right_comb_record
(prev:expression)
@ -111,7 +109,7 @@ let rec to_right_comb_record
let conv_map' = LMap.add (Label "0") exp conv_map in
LMap.add (Label "1") ({exp with expression_content = E_record (to_right_comb_record prev tl conv_map')}) conv_map'
let rec from_right_comb
let rec from_right_comb_record
(prev:expression)
(src_lmap: field_content label_map)
(dst_kvl:(label * field_content) list)
@ -124,11 +122,11 @@ let rec from_right_comb
| _ -> src_lmap in
let conv_map' = LMap.add label (accessor prev (Label "0") field_type) conv_map in
let next = accessor prev (Label "1") intermediary_type.field_type in
from_right_comb next src_lmap' tl conv_map'
from_right_comb_record next src_lmap' tl conv_map'
| [(label,_)] -> LMap.add label prev conv_map
| [] -> conv_map
let rec from_left_comb'
let rec from_left_comb_record
(prev:expression)
(src_lmap: field_content label_map)
(dst_kvl:(label * field_content) list)
@ -141,15 +139,62 @@ let rec from_left_comb'
| _ -> src_lmap in
let conv_map' = LMap.add label (accessor prev (Label "1") field_type) conv_map in
let next = accessor prev (Label "0") intermediary_type.field_type in
from_left_comb' next src_lmap' tl conv_map'
from_left_comb_record next src_lmap' tl conv_map'
| [(label,_)] -> LMap.add label prev conv_map
| [] -> conv_map
let from_left_comb prev src_lmap dst_kvl conv_map =
from_left_comb' prev src_lmap (List.rev dst_kvl) conv_map
from_left_comb_record prev src_lmap (List.rev dst_kvl) conv_map
let rec from_right_comb_or (to_convert:expression) (e:expression) (matchee_t,bodies) : expression result =
match matchee_t , bodies with
| [m] , bl::br::[] ->
let cases = [
{ constructor = Constructor "M_left" ;
pattern = Var.of_name "x";
body = bl } ;
{ constructor = Constructor "M_right" ;
pattern = Var.of_name "x";
body = br } ] in
ok @@ matching e m (Match_variant { cases ; tv = to_convert.type_expression })
| m::mtl , b::btl ->
let%bind body = from_right_comb_or to_convert e (mtl,btl) in
let cases = [
{ constructor = Constructor "M_left" ;
pattern = Var.of_name "x";
body = b } ;
{ constructor = Constructor "M_right" ;
pattern = Var.of_name "x";
body } ] in
ok @@ matching e m (Match_variant { cases ; tv = to_convert.type_expression })
| _ -> simple_fail "corner case"
let rec from_left_comb_or (to_convert:expression) (e:expression) (matchee_t,bodies) : expression result =
match matchee_t , bodies with
| [m] , bl::br::[] ->
let cases = [
{ constructor = Constructor "M_right" ;
pattern = Var.of_name "x";
body = bl } ;
{ constructor = Constructor "M_left" ;
pattern = Var.of_name "x";
body = br } ] in
ok @@ matching e m (Match_variant { cases ; tv = to_convert.type_expression })
| m::mtl , b::btl ->
let%bind body = from_left_comb_or to_convert e (mtl,btl) in
let cases = [
{ constructor = Constructor "M_right" ;
pattern = Var.of_name "x";
body = b } ;
{ constructor = Constructor "M_left" ;
pattern = Var.of_name "x";
body } ] in
ok @@ matching e m (Match_variant { cases ; tv = to_convert.type_expression })
| _ -> simple_fail "corner case"
(**
converts pair/record of a given layout to record/pair to another
- foo = (a,(b,(c,d))) -> foo_converted = { a=foo.0 ; b=foo.1.0 ; c=foo.1.1.0 ; d=foo.1.1.1 }
- foo = M_left(a) -> foo_converted = match foo with M_left x -> Foo x | M_right x -> Bar x
**)
let peephole_expression : expression -> expression result = fun e ->
let return expression_content = ok { e with expression_content } in
@ -162,7 +207,7 @@ let peephole_expression : expression -> expression result = fun e ->
| T_sum src_cmap ->
let%bind dst_cmap = get_t_sum e.type_expression in
let src_kvl = to_sorted_kv_list_c src_cmap in
let bodies = to_left_comb_variant e dst_cmap src_kvl in
let bodies = left_comb_variant_combination e dst_cmap src_kvl in
let to_cases ((constructor,{ctor_type=_;_}),body) =
let pattern = (Var.of_name "x") in
{constructor ; pattern ; body }
@ -182,7 +227,7 @@ let peephole_expression : expression -> expression result = fun e ->
| T_sum src_cmap ->
let%bind dst_cmap = get_t_sum e.type_expression in
let src_kvl = to_sorted_kv_list_c src_cmap in
let bodies = to_right_comb_variant e dst_cmap src_kvl in
let bodies = right_comb_variant_combination e dst_cmap src_kvl in
let to_cases ((constructor,{ctor_type=_;_}),body) =
let pattern = (Var.of_name "x") in
{constructor ; pattern ; body }
@ -194,16 +239,40 @@ let peephole_expression : expression -> expression result = fun e ->
return @@ E_matching {matchee = to_convert ; cases}
| _ -> return e.expression_content
)
| E_constant {cons_name= (C_CONVERT_FROM_RIGHT_COMB);
arguments= [ to_convert ] } ->
| E_constant {cons_name= (C_CONVERT_FROM_RIGHT_COMB); arguments= [ to_convert ] } -> (
match to_convert.type_expression.type_content with
| T_record src_lmap ->
let%bind dst_lmap = get_t_record e.type_expression in
let%bind src_lmap = get_t_record to_convert.type_expression in
let dst_kvl = to_sorted_kv_list_l dst_lmap in
return @@ E_record (from_right_comb to_convert src_lmap dst_kvl LMap.empty)
| E_constant {cons_name= (C_CONVERT_FROM_LEFT_COMB);
arguments= [ to_convert ] } ->
return @@ E_record (from_right_comb_record to_convert src_lmap dst_kvl LMap.empty)
| T_sum src_cmap ->
let%bind dst_lmap = get_t_sum e.type_expression in
let dst_kvl = to_sorted_kv_list_c dst_lmap in
let intermediary_types i = descend_types "M_right" src_cmap i in
let matchee = to_convert :: (List.map (fun t -> match_var t) @@ intermediary_types ((List.length dst_kvl)-2)) in
let bodies = List.map
(fun (ctor , {ctor_type;_}) -> constructor ctor (match_var ctor_type) e.type_expression)
dst_kvl in
let%bind match_expr = from_right_comb_or to_convert e (matchee,bodies) in
return match_expr.expression_content
| _ -> return e.expression_content
)
| E_constant {cons_name= (C_CONVERT_FROM_LEFT_COMB); arguments= [ to_convert ] } -> (
match to_convert.type_expression.type_content with
| T_record src_lmap ->
let%bind dst_lmap = get_t_record e.type_expression in
let%bind src_lmap = get_t_record to_convert.type_expression in
let dst_kvl = to_sorted_kv_list_l dst_lmap in
return @@ E_record (from_left_comb to_convert src_lmap dst_kvl LMap.empty)
| T_sum src_cmap ->
let%bind dst_lmap = get_t_sum e.type_expression in
let dst_kvl = to_sorted_kv_list_c dst_lmap in
let intermediary_types i = descend_types "M_left" src_cmap i in
let matchee = to_convert :: (List.map (fun t -> match_var t) @@ intermediary_types ((List.length dst_kvl)-2)) in
let bodies = List.map
(fun (ctor , {ctor_type;_}) -> constructor ctor (match_var ctor_type) e.type_expression)
(List.rev dst_kvl) in
let%bind match_expr = from_left_comb_or to_convert e (matchee,bodies) in
return match_expr.expression_content
| _ -> return e.expression_content
)
| _ as e -> return e

View File

@ -1212,12 +1212,19 @@ module Typer = struct
ok {t with type_content = variant}
| _ -> simple_fail "converter can only be used on record or variants"
let convert_from_left_comb = typer_1_opt "CONVERT_FROM_LEFT_COMB" @@ fun pair opt ->
let convert_from_left_comb = typer_1_opt "CONVERT_FROM_LEFT_COMB" @@ fun t opt ->
match t.type_content with
| T_record src_lmap ->
let%bind dst_t = trace_option (simple_error "convert_from_left_comb must be annotated") opt in
let%bind dst_lmap = get_t_record dst_t in
let%bind src_lmap = get_t_record pair in
let%bind record = Converter.convert_pair_from_left_comb src_lmap dst_lmap in
ok {pair with type_content = record}
ok {t with type_content = record}
| T_sum src_cmap ->
let%bind dst_t = trace_option (simple_error "convert_from_left_comb must be annotated") opt in
let%bind dst_cmap = get_t_sum dst_t in
let%bind variant = Converter.convert_variant_from_left_comb src_cmap dst_cmap in
ok {t with type_content = variant}
| _ -> simple_fail "converter can only be used on record or variants"
let constant_typers c : typer result = match c with
| C_INT -> ok @@ int ;

View File

@ -12,6 +12,7 @@ let needs_parens = {
);
type_variable = (fun _ _ _ -> true) ;
bool = (fun _ _ _ -> false) ;
int = (fun _ _ _ -> false) ;
z = (fun _ _ _ -> false) ;
string = (fun _ _ _ -> false) ;
bytes = (fun _ _ _ -> false) ;
@ -49,6 +50,7 @@ let op ppf = {
| PolyInstance { poly=_; arguments=_; poly_continue } ->
(poly_continue ())
);
int = (fun _visitor () i -> fprintf ppf "%i" i );
type_variable = (fun _visitor () type_variable -> fprintf ppf "Var %a" Var.pp type_variable) ;
bool = (fun _visitor () b -> fprintf ppf "%s" (if b then "true" else "false")) ;
z = (fun _visitor () i -> fprintf ppf "%a" Z.pp_print i) ;

View File

@ -9,6 +9,28 @@ type st3 =
| Bar3 of nat
| Baz3 of string
(*convert from*)
type tr3 = (string,"baz4",bool,"boz4")michelson_or
type tr2 = (nat,"bar4",tr3,"") michelson_or
type tr1 = (int,"foo4",tr2,"")michelson_or
let vr : tr1 = M_right (M_right (M_left "eq":tr3):tr2)
type tl3 = (int,"foo4",nat,"bar4")michelson_or
type tl2 = (tl3,"",string,"baz4") michelson_or
type tl1 = (tl2,"",bool,"boz4")michelson_or
let vl : tl1 = M_left (M_right "eq":tl2)
type param_r = st4 michelson_or_right_comb
let main_r (p, s : param_r * st4) : (operation list * st4) =
let r4 : st4 = Layout.convert_from_right_comb p in
([] : operation list), r4
type param_l = st4 michelson_or_left_comb
let main_l (p, s : param_l * st4) : (operation list * st4) =
let r4 : st4 = Layout.convert_from_left_comb p in
([] : operation list), r4
(** convert_to **)
let vst3 = Bar3 3n
@ -19,19 +41,3 @@ let str4 = Layout.convert_to_right_comb (vst4:st4)
let stl3 = Layout.convert_to_left_comb (vst3:st3)
let stl4 = Layout.convert_to_left_comb (vst4:st4)
(*convert from*)
// let s = "eq"
// let test_input_pair_r = (1,(2n,(s,true)))
// let test_input_pair_l = (((1,2n), s), true)
type param_r = st4 michelson_or_right_comb
let main_r (p, s : param_r * string) : (operation list * string) =
// let r4 : t4 = Layout.convert_from_right_comb p in
([] : operation list), "hey"
type param_l = st4 michelson_or_left_comb
let main_l (p, s : param_l * string) : (operation list * string) =
// let r4 : t4 = Layout.convert_from_left_comb p in
([] : operation list), "hey"

View File

@ -1,17 +1,6 @@
type t3 = { foo : int ; bar : nat ; baz : string}
type t4 = { one: int ; two : nat ; three : string ; four : bool}
(*convert to*)
let v3 = { foo = 2 ; bar = 3n ; baz = "q" }
let v4 = { one = 2 ; two = 3n ; three = "q" ; four = true }
let r3 = Layout.convert_to_right_comb (v3:t3)
let r4 = Layout.convert_to_right_comb (v4:t4)
let l3 = Layout.convert_to_left_comb (v3:t3)
let l4 = Layout.convert_to_left_comb (v4:t4)
(*convert from*)
let s = "eq"
@ -27,3 +16,14 @@ type param_l = t4 michelson_pair_left_comb
let main_l (p, s : param_l * string) : (operation list * string) =
let r4 : t4 = Layout.convert_from_left_comb p in
([] : operation list), r4.three ^ p.0.1
(*convert to*)
let v3 = { foo = 2 ; bar = 3n ; baz = "q" }
let v4 = { one = 2 ; two = 3n ; three = "q" ; four = true }
let r3 = Layout.convert_to_right_comb (v3:t3)
let r4 = Layout.convert_to_right_comb (v4:t4)
let l3 = Layout.convert_to_left_comb (v3:t3)
let l4 = Layout.convert_to_left_comb (v4:t4)