Mini_c: Inlining optimization

This commit is contained in:
Tom Jack 2019-11-25 17:15:25 -06:00
parent f7ef0472be
commit 66d2cda107
27 changed files with 1220 additions and 618 deletions

View File

@ -5,16 +5,16 @@ let contract basename =
let%expect_test _ =
run_ligo_good [ "measure-contract" ; contract "coase.ligo" ; "main" ] ;
[%expect {| 3098 bytes |}] ;
[%expect {| 2068 bytes |}] ;
run_ligo_good [ "measure-contract" ; contract "multisig.ligo" ; "main" ] ;
[%expect {| 1367 bytes |}] ;
[%expect {| 1093 bytes |}] ;
run_ligo_good [ "measure-contract" ; contract "multisig-v2.ligo" ; "main" ] ;
[%expect {| 861 bytes |}] ;
[%expect {| 627 bytes |}] ;
run_ligo_good [ "measure-contract" ; contract "vote.mligo" ; "main" ] ;
[%expect {| 1344 bytes |}] ;
[%expect {| 714 bytes |}] ;
()
@ -28,74 +28,100 @@ let%expect_test _ =
(pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
(map %cards nat (pair (address %card_owner) (nat %card_pattern))))
(nat %next_id)) ;
code { LAMBDA
(pair (pair (nat %card_to_transfer) (address %destination))
(pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
(map %cards nat (pair (address %card_owner) (nat %card_pattern))))
(nat %next_id)))
(pair (list operation)
(pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
(map %cards nat (pair (address %card_owner) (nat %card_pattern))))
(nat %next_id)))
code { DUP ;
CDR ;
DIP { DUP } ;
SWAP ;
CAR ;
IF_LEFT
{ DUP ;
IF_LEFT
{ DUP ;
DIP { DIP 2 { DUP } ; DIG 2 } ;
PAIR ;
DUP ;
CAR ;
DIP { DUP } ;
SWAP ;
CDR ;
DUP ;
CAR ;
CDR ;
DIP 2 { DUP } ;
DIG 2 ;
CAR ;
DIP { DUP } ;
SWAP ;
DIP { DUP ; CAR ; CAR } ;
GET ;
IF_NONE { PUSH string "GET_FORCE" ; FAILWITH } {} ;
DUP ;
CAR ;
SOURCE ;
DIP { DUP ; CDR ; PUSH nat 1 ; ADD } ;
MUL ;
DUP ;
AMOUNT ;
SWAP ;
COMPARE ;
NEQ ;
IF { PUSH string "This card doesn't belong to you" ; FAILWITH }
{ PUSH unit Unit } ;
GT ;
IF { PUSH string "Not enough money" ; FAILWITH } { PUSH unit Unit } ;
DROP ;
DIP 3 { DUP } ;
DIG 3 ;
NIL operation ;
DIP 2 { DUP } ;
DIG 2 ;
CDR ;
DIP { DUP ; CDR } ;
PAIR ;
DIP { DROP } ;
DIP 3 { DUP } ;
DIG 3 ;
CAR ;
DIP { DUP ; SOME ; DIP { DIP { DUP } ; SWAP } } ;
UPDATE ;
DIP { DIP { DUP } ; SWAP ; DROP } ;
PUSH nat 1 ;
ADD ;
DIP { DIP 2 { DUP } ; DIG 2 ; CAR } ;
SWAP ;
DIP { DIP { DROP } ; DUP } ;
SWAP ;
DIP { DIP 2 { DUP } ; DIG 2 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
SWAP ;
PAIR ;
PAIR ;
DIP 3 { DROP } ;
DUG 2 ;
NIL operation ;
DIP 3 { DUP } ;
DIG 3 ;
CAR ;
CAR ;
DIP 5 { DUP } ;
DIG 5 ;
DIP { DIP 3 { DUP } ; DIG 3 ; SOME ; DIP { DUP } } ;
UPDATE ;
DIP { DROP } ;
DUP ;
DIP { DIP 3 { DUP } ; DIG 3 } ;
DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CDR } ;
PAIR ;
DIP { DROP 6 } } ;
LAMBDA
(pair nat
(pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
(map %cards nat (pair (address %card_owner) (nat %card_pattern))))
(nat %next_id)))
(pair (list operation)
(pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
(map %cards nat (pair (address %card_owner) (nat %card_pattern))))
(nat %next_id)))
PAIR ;
DIP 5 { DROP } ;
DUG 4 ;
DIP 4 { DUP } ;
DIG 4 ;
CAR ;
CDR ;
DIP 5 { DUP } ;
DIG 5 ;
CDR ;
DIP { DIP 6 { DUP } ; DIG 6 ; SOURCE ; PAIR ; SOME ; DIP { DUP } } ;
UPDATE ;
DIP { DROP } ;
DUP ;
DIP { DIP 5 { DUP } ; DIG 5 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
SWAP ;
PAIR ;
PAIR ;
DIP 6 { DROP } ;
DUG 5 ;
DIP 5 { DUP } ;
DIG 5 ;
CDR ;
PUSH nat 1 ;
ADD ;
DIP { DIP 5 { DUP } ; DIG 5 ; CAR } ;
SWAP ;
PAIR ;
DIP 6 { DROP } ;
DUG 5 ;
DIP 2 { DUP } ;
DIG 2 ;
DIP { DIP 5 { DUP } ; DIG 5 } ;
PAIR ;
DIP { DROP 9 } }
{ DUP ;
DIP { DIP 2 { DUP } ; DIG 2 } ;
PAIR ;
DUP ;
CAR ;
DIP { DUP } ;
SWAP ;
@ -181,129 +207,61 @@ let%expect_test _ =
DUP ;
DIP { DIP 8 { DUP } ; DIG 8 } ;
PAIR ;
DIP { DROP 11 } } ;
LAMBDA
(pair nat
(pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
(map %cards nat (pair (address %card_owner) (nat %card_pattern))))
(nat %next_id)))
(pair (list operation)
(pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
(map %cards nat (pair (address %card_owner) (nat %card_pattern))))
(nat %next_id)))
DIP { DROP 12 } } ;
DIP { DROP } }
{ DUP ;
DIP { DIP { DUP } ; SWAP } ;
PAIR ;
DUP ;
CAR ;
DIP { DUP } ;
SWAP ;
CDR ;
DUP ;
CAR ;
CDR ;
DIP 2 { DUP } ;
DIG 2 ;
CAR ;
DIP { DUP } ;
SWAP ;
DIP { DUP ; CAR ; CAR } ;
GET ;
IF_NONE { PUSH string "GET_FORCE" ; FAILWITH } {} ;
DUP ;
CAR ;
DIP { DUP ; CDR ; PUSH nat 1 ; ADD } ;
MUL ;
DUP ;
AMOUNT ;
SOURCE ;
SWAP ;
COMPARE ;
GT ;
IF { PUSH string "Not enough money" ; FAILWITH } { PUSH unit Unit } ;
NEQ ;
IF { PUSH string "This card doesn't belong to you" ; FAILWITH }
{ PUSH unit Unit } ;
DROP ;
NIL operation ;
DIP 2 { DUP } ;
DIG 2 ;
DIP 3 { DUP } ;
DIG 3 ;
CDR ;
PUSH nat 1 ;
ADD ;
DIP { DIP 2 { DUP } ; DIG 2 ; CAR } ;
DIP { DUP ; CDR } ;
PAIR ;
DIP { DROP } ;
DIP 3 { DUP } ;
DIG 3 ;
CAR ;
DIP { DUP ; SOME ; DIP { DIP { DUP } ; SWAP } } ;
UPDATE ;
DIP { DIP { DUP } ; SWAP ; DROP } ;
SWAP ;
DIP { DIP { DROP } ; DUP } ;
SWAP ;
DIP { DIP 2 { DUP } ; DIG 2 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
SWAP ;
PAIR ;
PAIR ;
DIP 3 { DROP } ;
DUG 2 ;
DIP 3 { DUP } ;
DIG 3 ;
CAR ;
CAR ;
DIP 5 { DUP } ;
DIG 5 ;
DIP { DIP 3 { DUP } ; DIG 3 ; SOME ; DIP { DUP } } ;
UPDATE ;
DIP { DROP } ;
DUP ;
DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CDR } ;
PAIR ;
PAIR ;
DIP 5 { DROP } ;
DUG 4 ;
DIP 4 { DUP } ;
DIG 4 ;
CAR ;
CDR ;
DIP 5 { DUP } ;
DIG 5 ;
CDR ;
DIP { DIP 6 { DUP } ; DIG 6 ; SOURCE ; PAIR ; SOME ; DIP { DUP } } ;
UPDATE ;
DIP { DROP } ;
DUP ;
DIP { DIP 5 { DUP } ; DIG 5 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
SWAP ;
PAIR ;
PAIR ;
DIP 6 { DROP } ;
DUG 5 ;
DIP 5 { DUP } ;
DIG 5 ;
CDR ;
PUSH nat 1 ;
ADD ;
DIP { DIP 5 { DUP } ; DIG 5 ; CAR } ;
SWAP ;
PAIR ;
DIP 6 { DROP } ;
DUG 5 ;
DIP 2 { DUP } ;
DIG 2 ;
DIP { DIP 5 { DUP } ; DIG 5 } ;
NIL operation ;
PAIR ;
DIP { DROP 8 } } ;
DIP 3 { DUP } ;
DIG 3 ;
CAR ;
DIP 4 { DUP } ;
DIG 4 ;
CDR ;
DIP { DUP } ;
SWAP ;
IF_LEFT
{ DUP ;
IF_LEFT
{ DUP ;
DUP ;
DIP { DIP 3 { DUP } ; DIG 3 } ;
PAIR ;
DIP { DIP 5 { DUP } ; DIG 5 } ;
EXEC ;
DIP { DROP 2 } }
{ DUP ;
DUP ;
DIP { DIP 3 { DUP } ; DIG 3 } ;
PAIR ;
DIP { DIP 6 { DUP } ; DIG 6 } ;
EXEC ;
DIP { DROP 2 } } ;
DIP { DROP } }
{ DUP ;
DUP ;
DIP { DIP 2 { DUP } ; DIG 2 } ;
PAIR ;
DIP { DIP 6 { DUP } ; DIG 6 } ;
EXEC ;
DIP { DROP 2 } } ;
DIP { DROP 6 } } } |} ]
DIP { DROP 6 } } ;
DIP { DROP 2 } } } |} ]
let%expect_test _ =
run_ligo_good [ "compile-contract" ; contract "multisig.ligo" ; "main" ] ;
@ -314,13 +272,10 @@ let%expect_test _ =
storage
(pair (pair (list %auth key) (nat %counter)) (pair (string %id) (nat %threshold))) ;
code { DUP ;
LAMBDA
(pair (pair (pair (nat %counter) (lambda %message unit (list operation)))
(list %signatures (pair key_hash signature)))
(pair (pair (list %auth key) (nat %counter)) (pair (string %id) (nat %threshold))))
(pair (list operation)
(pair (pair (list %auth key) (nat %counter)) (pair (string %id) (nat %threshold))))
{ DUP ;
CAR ;
DIP { DUP ; CDR } ;
PAIR ;
DUP ;
CAR ;
DIP { DUP } ;
SWAP ;
@ -434,19 +389,6 @@ let%expect_test _ =
EXEC ;
DIP { DIP { DUP } ; SWAP } ;
PAIR ;
DIP { DROP 4 } } ;
SWAP ;
CAR ;
DIP 2 { DUP } ;
DIG 2 ;
CDR ;
DIP { DUP } ;
SWAP ;
DUP ;
DIP { DIP { DUP } ; SWAP } ;
PAIR ;
DIP { DIP 3 { DUP } ; DIG 3 } ;
EXEC ;
DIP { DROP 5 } } } |} ]
let%expect_test _ =
@ -457,17 +399,10 @@ let%expect_test _ =
(pair (pair (set %auth address) (big_map %message_store bytes (set address)))
(nat %threshold)) ;
code { DUP ;
LAMBDA
(pair (lambda unit (list operation))
(pair (pair (set %auth address) (big_map %message_store bytes (set address)))
(nat %threshold)))
(pair (list operation)
(pair (pair (set %auth address) (big_map %message_store bytes (set address)))
(nat %threshold)))
{ DUP ;
CAR ;
DIP { DUP } ;
SWAP ;
DIP { DUP ; CDR } ;
PAIR ;
DUP ;
CDR ;
DUP ;
CAR ;
@ -479,6 +414,7 @@ let%expect_test _ =
DROP ;
DIP { DUP } ;
SWAP ;
CAR ;
DUP ;
PACK ;
DUP ;
@ -528,20 +464,7 @@ let%expect_test _ =
SWAP ;
DIP { DIP 4 { DUP } ; DIG 4 } ;
PAIR ;
DIP { DROP 7 } } ;
SWAP ;
CAR ;
DIP 2 { DUP } ;
DIG 2 ;
CDR ;
DIP { DUP } ;
SWAP ;
DUP ;
DIP { DIP { DUP } ; SWAP } ;
PAIR ;
DIP { DIP 3 { DUP } ; DIG 3 } ;
EXEC ;
DIP { DROP 5 } } } |} ]
DIP { DROP 7 } } } |} ]
let%expect_test _ =
run_ligo_good [ "compile-contract" ; contract "vote.mligo" ; "main" ] ;
@ -555,17 +478,10 @@ let%expect_test _ =
(pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
(pair (timestamp %finish_time) (string %title)))
(set %voters address)) ;
code { LAMBDA
(pair (pair (pair (timestamp %beginning_time) (timestamp %finish_time)) (string %title))
(pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
(pair (timestamp %finish_time) (string %title)))
(set %voters address)))
(pair (list operation)
(pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
(pair (timestamp %finish_time) (string %title)))
(set %voters address)))
{ DUP ;
code { DUP ;
CAR ;
IF_LEFT
{ DUP ;
PUSH int 0 ;
SOME ;
DIP { PUSH int 0 ;
@ -594,17 +510,11 @@ let%expect_test _ =
PAIR ;
NIL operation ;
PAIR ;
DIP { DROP 3 } } ;
LAMBDA
(pair string
(pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
(pair (timestamp %finish_time) (string %title)))
(set %voters address)))
(pair (list operation)
(pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
(pair (timestamp %finish_time) (string %title)))
(set %voters address)))
DIP { DROP 3 } }
{ DUP ;
DIP { DIP { DUP } ; SWAP ; CDR } ;
PAIR ;
DUP ;
CAR ;
DIP { DUP } ;
SWAP ;
@ -645,28 +555,5 @@ let%expect_test _ =
PAIR ;
NIL operation ;
PAIR ;
DIP { DROP 6 } } ;
DIP 2 { DUP } ;
DIG 2 ;
CAR ;
DIP 3 { DUP } ;
DIG 3 ;
CDR ;
DIP { DUP } ;
SWAP ;
IF_LEFT
{ DUP ;
DUP ;
DIP { DIP 2 { DUP } ; DIG 2 } ;
PAIR ;
DIP { DIP 5 { DUP } ; DIG 5 } ;
EXEC ;
DIP { DROP 2 } }
{ DUP ;
DUP ;
DIP { DIP 2 { DUP } ; DIG 2 } ;
PAIR ;
DIP { DIP 4 { DUP } ; DIG 4 } ;
EXEC ;
DIP { DROP 2 } } ;
DIP { DROP 5 } } } |}]
DIP { DROP 7 } } ;
DIP { DROP } } } |}]

View File

@ -22,17 +22,17 @@ let compile_function = fun e ->
let compile_expression_as_function_entry = fun program name ->
let%bind aggregated = aggregate_entry program name true in
let%bind aggregated = Self_mini_c.all_expression aggregated in
let aggregated = Self_mini_c.all_expression aggregated in
compile_function aggregated
let compile_function_entry = fun program name ->
let%bind aggregated = aggregate_entry program name false in
let%bind aggregated = Self_mini_c.all_expression aggregated in
let aggregated = Self_mini_c.all_expression aggregated in
compile_function aggregated
let compile_contract_entry = fun program name ->
let%bind aggregated = aggregate_entry program name false in
let%bind aggregated = Self_mini_c.all_expression aggregated in
let aggregated = Self_mini_c.all_expression aggregated in
let%bind compiled = compile_function aggregated in
let%bind (param_ty , storage_ty) =
let%bind fun_ty = get_t_function aggregated.type_value in

View File

@ -706,13 +706,6 @@ let propagator_break_ctor : output_break_ctor propagator =
type output_specialize1 = { poly : c_poly_simpl ; a_k_var : c_constructor_simpl }
module Int = struct
(* Restrict use of Pervasives.compare to just `int`, because we
don't want to risk the type of a field changing from int to
something not compatible with Pervasives.compare, and not
noticing that the comparator needs to be updated. *)
let compare (a : int) (b : int) = Pervasives.compare a b
end
let (<?) ca cb =
if ca = 0 then cb () else ca
let rec compare_list f = function

View File

@ -2,6 +2,8 @@
For more info, see back-end.md: https://gitlab.com/ligolang/ligo/blob/dev/gitlab-pages/docs/contributors/big-picture/back-end.md *)
(* TODO(tomjack) all Var.of_name are suspicious, continue war against string? *)
open! Trace
open Helpers
@ -267,14 +269,14 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
| E_let_in {binder; rhs; result} ->
let%bind rhs' = transpile_annotated_expression rhs in
let%bind result' = transpile_annotated_expression result in
return (E_let_in ((binder, rhs'.type_value), rhs', result'))
return (E_let_in ((Var.of_name binder, rhs'.type_value), rhs', result'))
| E_literal l -> return @@ E_literal (transpile_literal l)
| E_variable name -> (
let%bind ele =
trace_option (corner_case ~loc:__LOC__ "name not in environment") @@
AST.Environment.get_opt name ae.environment in
let%bind tv = transpile_environment_element_type ele in
return ~tv @@ E_variable name
return ~tv @@ E_variable (Var.of_name name)
)
| E_application (a, b) ->
let%bind a = transpile_annotated_expression a in
@ -377,7 +379,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
let%bind body' = transpile_annotated_expression l.body in
let%bind (input , _) = AST.get_t_function f.type_annotation in
let%bind input' = transpile_type input in
ok ((l.binder , input') , body')
ok ((Var.of_name l.binder , input') , body')
in
let expression_to_iterator_body (f : AST.annotated_expression) =
match f.expression with
@ -520,7 +522,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
in
let%bind (_, path) = bind_fold_right_list aux (ty, []) path in
let%bind expr' = transpile_annotated_expression expr in
return (E_assignment (typed_name.type_name, path, expr'))
return (E_assignment (Var.of_name typed_name.type_name, path, expr'))
)
| E_matching (expr, m) -> (
let%bind expr' = transpile_annotated_expression expr in
@ -535,7 +537,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
let%bind s' = transpile_annotated_expression s in
ok (tv' , s')
in
return @@ E_if_none (expr' , n , ((name , tv') , s'))
return @@ E_if_none (expr' , n , ((Var.of_name name , tv') , s'))
| Match_list {
match_nil ;
match_cons = (((hd_name , hd_ty) , (tl_name , tl_ty)) , match_cons) ;
@ -545,7 +547,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
let%bind hd_ty' = transpile_type hd_ty in
let%bind tl_ty' = transpile_type tl_ty in
let%bind match_cons' = transpile_annotated_expression match_cons in
ok (((hd_name , hd_ty') , (tl_name , tl_ty')) , match_cons')
ok (((Var.of_name hd_name , hd_ty') , (Var.of_name tl_name , tl_ty')) , match_cons')
in
return @@ E_if_cons (expr' , nil , cons)
)
@ -577,19 +579,19 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
trace_option (corner_case ~loc:__LOC__ "missing match clause") @@
List.find_opt (fun ((constructor_name' , _) , _) -> constructor_name' = constructor_name) lst in
let%bind body' = transpile_annotated_expression body in
return @@ E_let_in ((name , tv) , top , body')
return @@ E_let_in ((Var.of_name name , tv) , top , body')
)
| ((`Node (a , b)) , tv) ->
let%bind a' =
let%bind a_ty = get_t_left tv in
let a_var = "left" , a_ty in
let%bind e = aux (((Expression.make (E_variable "left") a_ty))) a in
let a_var = Var.of_name "left" , a_ty in
let%bind e = aux (((Expression.make (E_variable (Var.of_name "left")) a_ty))) a in
ok (a_var , e)
in
let%bind b' =
let%bind b_ty = get_t_right tv in
let b_var = "right" , b_ty in
let%bind e = aux (((Expression.make (E_variable "right") b_ty))) b in
let b_var = Var.of_name "right" , b_ty in
let%bind e = aux (((Expression.make (E_variable (Var.of_name "right")) b_ty))) b in
ok (b_var , e)
in
return @@ E_if_left (top , a' , b')
@ -606,7 +608,7 @@ and transpile_lambda l (input_type , output_type) =
let%bind input = transpile_type input_type in
let%bind output = transpile_type output_type in
let tv = Combinators.t_function input output in
let closure = E_closure { binder ; body = result'} in
let closure = E_closure { binder = Var.of_name binder ; body = result'} in
ok @@ Combinators.Expression.make_tpl (closure , tv)
let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
@ -614,8 +616,8 @@ let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
| Declaration_constant ({name;annotated_expression} , _) ->
let%bind expression = transpile_annotated_expression annotated_expression in
let tv = Combinators.Expression.get_type expression in
let env' = Environment.add (name, tv) env in
ok @@ ((name, expression), environment_wrap env env')
let env' = Environment.add (Var.of_name name, tv) env in
ok @@ ((Var.of_name name, expression), environment_wrap env env')
let transpile_program (lst : AST.program) : program result =
let aux (prev:(toplevel_statement list * Environment.t) result) cur =

View File

@ -4,8 +4,9 @@
(libraries
mini_c
)
(inline_tests)
(preprocess
(pps ppx_let)
(pps ppx_let ppx_expect)
)
(flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
)

View File

@ -1,8 +1,17 @@
open Mini_c
open Trace
open! Trace
(* Overly conservative purity test: ok to treat pure things as impure,
must not treat impure things as pure. *)
(* TODO hack to specialize map_expression to identity monad *)
let map_expression :
(expression -> expression) -> (expression -> expression) =
fun f e ->
match Helpers.map_expression (fun e -> ok (f e)) e with
| Ok (e, _) -> e
| Error _ -> assert false (* impossible *)
(* Conservative purity test: ok to treat pure things as impure, must
not treat impure things as pure. *)
(* true if the name names a pure constant -- i.e. if uses will be pure
assuming arguments are pure *)
@ -54,25 +63,177 @@ let rec is_pure : expression -> bool = fun e ->
(* definitely not pure *)
| E_assignment _ -> false
let occurs_in : Var.t -> expression -> bool =
fun x e ->
let fvs = Free_variables.expression [] e in
Free_variables.mem x fvs
(* Eliminate dead `let` with pure rhs *)
let occurs_count : Var.t -> expression -> int =
fun x e ->
let fvs = Free_variables.expression [] e in
Free_variables.mem_count x fvs
let rec elim_dead_code : expression -> expression result = fun e ->
let changed = ref false in (* ugh *)
let mapper : Helpers.mapper = fun e ->
(* If `ignore_lambdas` is true, ignore assignments which occur inside
lambdas, which have no effect on the value of the variable outside
of the lambda. *)
let rec is_assigned : ignore_lambdas:bool -> Var.t -> expression -> bool =
fun ~ignore_lambdas x e ->
let self = is_assigned ~ignore_lambdas x in
let selfs = List.exists self in
let it = Var.equal x in
let self_binder binder body =
if it binder
then false
else self body in
let self_binder2 binder1 binder2 body =
if it binder1 || it binder2
then false
else self body in
match e.content with
| E_let_in ((x, _), e1, e2) when is_pure e1 ->
let fvs = Free_variables.expression [] e2 in
if Free_variables.mem x fvs
then ok e
else
(* pure e1 is not used, eliminate! *)
(changed := true ; ok e2)
| _ -> ok e in
let%bind e = Helpers.map_expression mapper e in
if !changed
then elim_dead_code e
else ok e
| E_assignment (x, _, e) ->
it x || self e
| E_closure { binder; body } ->
if ignore_lambdas
then false
else self_binder binder body
| E_constant (_, args) ->
selfs args
| E_application (f, arg) ->
selfs [ f ; arg ]
| E_iterator (_, ((x, _), e1), e2) ->
self_binder x e1 || self e2
| E_fold (((x, _), e1), e2, e3) ->
self_binder x e1 || selfs [ e2 ; e3 ]
| E_if_bool (e1, e2, e3) ->
selfs [ e1 ; e2 ; e3 ]
| E_if_none (e1, e2, ((x, _), e3)) ->
selfs [ e1 ; e2 ] || self_binder x e3
| E_if_cons (e1, e2, (((hd, _), (tl, _)), e3)) ->
selfs [ e1 ; e2 ] || self_binder2 hd tl e3
| E_if_left (e1, ((l, _), e2), ((r, _), e3)) ->
self e1 || self_binder l e2 || self_binder r e3
| E_let_in ((x, _), e1, e2) ->
self e1 || self_binder x e2
| E_sequence (e1, e2) ->
selfs [ e1 ; e2 ]
| E_while (e1, e2) ->
selfs [ e1 ; e2 ]
| E_literal _
| E_skip
| E_variable _
| E_make_empty_map _
| E_make_empty_big_map _
| E_make_empty_list _
| E_make_empty_set _
| E_make_none _ ->
false
let all_expression : expression -> expression result =
elim_dead_code
(* Let "inlining" mean transforming the code:
let x = e1 in e2
to:
e2[e1/x]
(where the latter signifies substituting e1 for x in e2.)
Things which can go wrong for inlining:
- If `e1` is not pure, inlining may fail to preserve semantics.
- If assignments to `x` occur in e2, inlining does not make sense.
- Free variables of `e1` may be assigned in e2, before usages of `x`.
- Free variables of `e1` may be shadowed in e2, at usages of `x`. This
is not a problem if the substitution is capture-avoiding.
- ?
*)
let can_inline : Var.t -> expression -> expression -> bool =
fun x e1 e2 ->
is_pure e1 &&
(* if x does not occur in e2, there can be no other problems:
substitution will be a noop up to alpha-equivalence *)
(not (occurs_in x e2) ||
(* else, must worry about assignment *)
(not (is_assigned ~ignore_lambdas:false x e2) &&
List.for_all
(fun y -> not (is_assigned ~ignore_lambdas:true y e2))
(Free_variables.expression [] e2)))
let should_inline : Var.t -> expression -> bool =
fun x e ->
occurs_count x e <= 1
let inline_let : bool ref -> expression -> expression =
fun changed e ->
match e.content with
| E_let_in ((x, _a), e1, e2) ->
if can_inline x e1 e2 && should_inline x e2
then
(* can raise Subst.Bad_argument, but should not happen, due to
can_inline *)
let e2' = Subst.subst_expression ~body:e2 ~x:x ~expr:e1 in
(changed := true ; e2')
else
e
| _ -> e
let inline_lets : bool ref -> expression -> expression =
fun changed ->
map_expression (inline_let changed)
(* Let "beta" mean transforming the code:
(\x. e1) e2
to:
let x = e2 in e1
Things which can go wrong for beta reduction:
- If e1 contains (meaningful) assignments to free variables, semantics
will not be preserved.
- ?
*)
let can_beta : anon_function -> bool =
fun lam ->
List.for_all
(fun x -> not (is_assigned ~ignore_lambdas:true x lam.body))
(Free_variables.lambda [] lam)
let beta : bool ref -> expression -> expression =
fun changed e ->
match e.content with
| E_application ({ content = E_closure { binder = x ; body = e1 } ; type_value = T_function (xtv, tv) }, e2) ->
if can_beta { binder = x ; body = e1 }
then
(changed := true ;
Expression.make (E_let_in ((x, xtv), e2, e1)) tv)
else e
(* also do CAR (PAIR x y) ↦ x, or CDR (PAIR x y) ↦ y, only if x and y are pure *)
| E_constant ("CAR"|"CDR" as const, [ { content = E_constant ("PAIR", [ e1 ; e2 ]) ; type_value = _ } ]) ->
if is_pure e1 && is_pure e2
then (changed := true ;
match const with
| "CAR" -> e1
| "CDR" -> e2
| _ -> assert false)
else e
| _ -> e
let betas : bool ref -> expression -> expression =
fun changed ->
map_expression (beta changed)
let rec all_expression : expression -> expression =
fun e ->
let changed = ref false in
let e = inline_lets changed e in
let e = betas changed e in
if !changed
then all_expression e
else e

View File

@ -0,0 +1,430 @@
open Mini_c
(* Reference implementation:
https://www.cs.cornell.edu/courses/cs3110/2019sp/textbook/interp/lambda-subst/main.ml
...but, it has at least one bug: in subst,
`let new_body = replace e' y fresh in ...` should be:
`let new_body = replace e' fresh y in ...`,
due to the arg order choice for replace.
Below, this bug is fixed by adopting the other order choice for
replace (as well as subst). *)
(* replace in `e` the variable `x` with `y`.
It would be fine -- better? -- to only replace the _free_ x.
*)
let rec replace : expression -> var_name -> var_name -> expression =
fun e x y ->
let replace e = replace e x y in
let return content = { e with content } in
let replace_var v =
if Var.equal v x
then y
else v in
match e.content with
| E_literal _ -> e
| E_closure { binder ; body } ->
let body = replace body in
let binder = replace_var binder in
return @@ E_closure { binder ; body }
| E_skip -> e
| E_constant (c, args) ->
let args = List.map replace args in
return @@ E_constant (c, args)
| E_application (f, x) ->
let (f, x) = Tuple.map2 replace (f, x) in
return @@ E_application (f, x)
| E_variable z ->
let z = replace_var z in
return @@ E_variable z
| E_make_empty_map _ -> e
| E_make_empty_big_map _ -> e
| E_make_empty_list _ -> e
| E_make_empty_set _ -> e
| E_make_none _ -> e
| E_iterator (name, ((v, tv), body), expr) ->
let body = replace body in
let expr = replace expr in
let v = replace_var v in
return @@ E_iterator (name, ((v, tv), body), expr)
| E_fold (((v, tv), body), collection, initial) ->
let body = replace body in
let collection = replace collection in
let initial = replace initial in
let v = replace_var v in
return @@ E_fold (((v, tv), body), collection, initial)
| E_if_bool (c, bt, bf) ->
let c = replace c in
let bt = replace bt in
let bf = replace bf in
return @@ E_if_bool (c, bt, bf)
| E_if_none (c, bt, ((v, tv), bf)) ->
let c = replace c in
let bt = replace bt in
let bf = replace bf in
let v = replace_var v in
return @@ E_if_none (c, bt, ((v, tv), bf))
| E_if_cons (c, bf, (((v1, tv1), (v2, tv2)), bt)) ->
let c = replace c in
let bf = replace bf in
let v1 = replace_var v1 in
let v2 = replace_var v2 in
let bt = replace bt in
return @@ E_if_cons (c, bf, (((v1, tv1), (v2, tv2)), bt))
| E_if_left (c, ((v1, tv1), bt), ((v2, tv2), bf)) ->
let c = replace c in
let bf = replace bf in
let v1 = replace_var v1 in
let v2 = replace_var v2 in
let bt = replace bt in
return @@ E_if_left (c, ((v1, tv1), bt), ((v2, tv2), bf))
| E_let_in ((v, tv), e1, e2) ->
let v = replace_var v in
let e1 = replace e1 in
let e2 = replace e2 in
return @@ E_let_in ((v, tv), e1, e2)
| E_sequence (e1, e2) ->
let e1 = replace e1 in
let e2 = replace e2 in
return @@ E_sequence (e1, e2)
| E_assignment (v, path, e) ->
let v = replace_var v in
let e = replace e in
return @@ E_assignment (v, path, e)
| E_while (cond, body) ->
let cond = replace cond in
let body = replace body in
return @@ E_while (cond, body)
(**
Computes `body[x := expr]`.
This raises Bad_argument in the case of assignments with a name clash. (`x <- 42[x := 23]` makes no sense.)
**)
exception Bad_argument
let rec subst_expression : body:expression -> x:var_name -> expr:expression -> expression =
fun ~body ~x ~expr ->
let self body = subst_expression ~body ~x ~expr in
let subst_binder y expr' =
(* if x is shadowed, binder doesn't change *)
if Var.equal x y
then (y, expr')
(* else, if no capture, subst in binder *)
else if not (Free_variables.mem y (Free_variables.expression [] expr))
then (y, self expr')
(* else, avoid capture and subst in binder *)
else
let fresh = Var.fresh_like y in
let new_body = replace expr' y fresh in
(fresh, self new_body) in
(* hack to avoid reimplementing subst_binder for 2-ary binder in E_if_cons:
intuitively, we substitute in \hd tl. expr' as if it were \hd. \tl. expr *)
let subst_binder2 y z expr' =
let dummy = T_base Base_unit in
let hack = { content = E_closure { binder = z ; body = expr' } ;
type_value = dummy } in
match subst_binder y hack with
| (y', { content = E_closure { binder = z' ; body = body } ; type_value = _dummy }) ->
(y', z', { body with type_value = expr'.type_value })
| _ -> assert false in
let return content = {body with content} in
let return_id = body in
match body.content with
| E_variable x' ->
if x' = x
then expr
else return_id
| E_closure { binder; body } -> (
let (binder, body) = subst_binder binder body in
return @@ E_closure { binder ; body }
)
| E_let_in ((v , tv) , expr , body) -> (
let expr = self expr in
let (v, body) = subst_binder v body in
return @@ E_let_in ((v , tv) , expr , body)
)
| E_iterator (s, ((name , tv) , body) , collection) -> (
let (name, body) = subst_binder name body in
let collection = self collection in
return @@ E_iterator (s, ((name , tv) , body) , collection)
)
| E_fold (((name , tv) , body) , collection , init) -> (
let (name, body) = subst_binder name body in
let collection = self collection in
let init = self init in
return @@ E_fold (((name , tv) , body) , collection , init)
)
| E_if_none (c, n, ((name, tv) , s)) -> (
let c = self c in
let n = self n in
let (name, s) = subst_binder name s in
return @@ E_if_none (c, n, ((name, tv) , s))
)
| E_if_cons (c, n, (((hd, hdtv) , (tl, tltv)) , cons)) -> (
let c = self c in
let n = self n in
let (hd, tl, cons) = subst_binder2 hd tl cons in
return @@ E_if_cons (c, n, (((hd, hdtv) , (tl, tltv)) , cons))
)
| E_if_left (c, ((name_l, tvl) , l), ((name_r, tvr) , r)) -> (
let c = self c in
let (name_l, l) = subst_binder name_l l in
let (name_r, r) = subst_binder name_r r in
return @@ E_if_left (c, ((name_l, tvl) , l), ((name_r, tvr) , r))
)
(* All that follows is boilerplate *)
| E_literal _ | E_skip | E_make_none _
| E_make_empty_map (_,_)
| E_make_empty_big_map _
| E_make_empty_list _
| E_make_empty_set _ as em -> return em
| E_constant (name, lst) -> (
let lst' = List.map self lst in
return @@ E_constant (name,lst')
)
| E_application farg -> (
let farg' = Tuple.map2 self farg in
return @@ E_application farg'
)
| E_while eb -> (
let eb' = Tuple.map2 self eb in
return @@ E_while eb'
)
| E_if_bool cab -> (
let cab' = Tuple.map3 self cab in
return @@ E_if_bool cab'
)
| E_sequence ab -> (
let ab' = Tuple.map2 self ab in
return @@ E_sequence ab'
)
| E_assignment (s, lrl, exp) -> (
let exp' = self exp in
if Var.equal s x then raise Bad_argument ;
return @@ E_assignment (s, lrl, exp')
)
let%expect_test _ =
let dummy_type = T_base Base_unit in
let wrap e = { content = e ; type_value = dummy_type } in
let show_subst ~body ~x ~expr =
Format.printf "(%a)[%a := %a] =@ %a"
PP.expression body
Var.pp x
PP.expression expr
PP.expression (subst_expression ~body ~x ~expr) in
let x = Var.of_name "x" in
let y = Var.of_name "y" in
let z = Var.of_name "z" in
let var x = wrap (E_variable x) in
let app f x = wrap (E_application (f, x)) in
let lam x u = wrap (E_closure { binder = x ; body = u }) in
let unit = wrap (E_literal D_unit) in
(* substituted var *)
Var.reset_counter () ;
show_subst
~body:(var x)
~x:x
~expr:unit ;
[%expect{|
(V(x))[x := L(unit)] =
L(unit) |}] ;
(* other var *)
Var.reset_counter () ;
show_subst
~body:(var y)
~x:x
~expr:unit ;
[%expect{|
(V(y))[x := L(unit)] =
V(y)
|}] ;
(* closure shadowed *)
Var.reset_counter () ;
show_subst
~body:(lam x (var x))
~x:x
~expr:unit ;
[%expect{|
(C(fun x -> (V(x))))[x := L(unit)] =
C(fun x -> (V(x)))
|}] ;
(* closure not shadowed *)
Var.reset_counter () ;
show_subst
~body:(lam y (var x))
~x:x
~expr:unit ;
[%expect{|
(C(fun y -> (V(x))))[x := L(unit)] =
C(fun y -> (L(unit)))
|}] ;
(* closure capture-avoidance *)
Var.reset_counter () ;
show_subst
~body:(lam y (app (var x) (var y)))
~x:x
~expr:(wrap (E_variable y)) ;
[%expect{|
(C(fun y -> ((V(x))@(V(y)))))[x := V(y)] =
C(fun y#1 -> ((V(y))@(V(y#1))))
|}] ;
(* let-in shadowed (not in rhs) *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_let_in ((x, dummy_type), var x, var x)))
~x:x
~expr:unit ;
[%expect{|
(let x = V(x) in ( V(x) ))[x := L(unit)] =
let x = L(unit) in ( V(x) )
|}] ;
(* let-in not shadowed *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_let_in ((y, dummy_type), var x, var x)))
~x:x
~expr:unit ;
[%expect{|
(let y = V(x) in ( V(x) ))[x := L(unit)] =
let y = L(unit) in ( L(unit) )
|}] ;
(* let-in capture avoidance *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_let_in ((y, dummy_type), var x,
app (var x) (var y))))
~x:x
~expr:(var y) ;
[%expect{|
(let y = V(x) in ( (V(x))@(V(y)) ))[x := V(y)] =
let y#1 = V(y) in ( (V(y))@(V(y#1)) )
|}] ;
(* iter shadowed *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_iterator ("ITER", ((x , dummy_type) , var x) , var x)))
~x:x
~expr:unit ;
[%expect{|
(for_ITER x of V(x) do ( V(x) ))[x := L(unit)] =
for_ITER x of L(unit) do ( V(x) )
|}] ;
(* iter not shadowed *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_iterator ("ITER", ((y , dummy_type) , var x) , var x)))
~x:x
~expr:unit ;
[%expect{|
(for_ITER y of V(x) do ( V(x) ))[x := L(unit)] =
for_ITER y of L(unit) do ( L(unit) )
|}] ;
(* iter capture-avoiding *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_iterator ("ITER", ((y , dummy_type) , app (var x) (var y)), app (var x) (var y))))
~x:x
~expr:(var y) ;
[%expect{|
(for_ITER y of (V(x))@(V(y)) do ( (V(x))@(V(y)) ))[x := V(y)] =
for_ITER y#1 of (V(y))@(V(y)) do ( (V(y))@(V(y#1)) )
|}] ;
(* if_cons shadowed 1 *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_if_cons (var x,
var x,
(((x, dummy_type), (y, dummy_type)),
var x))))
~x:x
~expr:unit ;
[%expect{|
(V(x) ?? V(x) : (x :: y) -> V(x))[x := L(unit)] =
L(unit) ?? L(unit) : (x :: y) -> V(x)
|}] ;
(* if_cons shadowed 2 *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_if_cons (var x,
var x,
(((y, dummy_type), (x, dummy_type)),
var x))))
~x:x
~expr:unit ;
[%expect{|
(V(x) ?? V(x) : (y :: x) -> V(x))[x := L(unit)] =
L(unit) ?? L(unit) : (y :: x) -> V(x)
|}] ;
(* if_cons not shadowed *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_if_cons (var x,
var x,
(((y, dummy_type), (z, dummy_type)),
var x))))
~x:x
~expr:unit ;
[%expect{|
(V(x) ?? V(x) : (y :: z) -> V(x))[x := L(unit)] =
L(unit) ?? L(unit) : (y :: z) -> L(unit)
|}] ;
(* if_cons capture avoidance 1 *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_if_cons (var x,
var x,
(((y, dummy_type), (z, dummy_type)),
app (var x) (app (var y) (var z))))))
~x:x
~expr:(var y) ;
[%expect{|
(V(x) ?? V(x) : (y :: z) -> (V(x))@((V(y))@(V(z))))[x := V(y)] =
V(y) ?? V(y) : (y#1 :: z) -> (V(y))@((V(y#1))@(V(z)))
|}] ;
(* if_cons capture avoidance 2 *)
Var.reset_counter () ;
show_subst
~body:(wrap (E_if_cons (var x,
var x,
(((y, dummy_type), (z, dummy_type)),
app (var x) (app (var y) (var z))))))
~x:x
~expr:(var z) ;
[%expect{|
(V(x) ?? V(x) : (y :: z) -> (V(x))@((V(y))@(V(z))))[x := V(z)] =
V(z) ?? V(z) : (y :: z#1) -> (V(z))@((V(y))@(V(z#1)))
|}] ;
(* old bug *)
Var.reset_counter () ;
let y0 = Var.fresh ~name:"y" () in
show_subst
~body:(lam y (lam y0 (app (var x) (app (var y) (var y0)))))
~x:x
~expr:(var y) ;
[%expect{|
(C(fun y -> (C(fun y#1 -> ((V(x))@((V(y))@(V(y#1))))))))[x := V(y)] =
C(fun y#2 -> (C(fun y#1 -> ((V(y))@((V(y#2))@(V(y#1)))))))
|}] ;

View File

@ -5,12 +5,12 @@ open Michelson
let empty : environment = []
let get : environment -> string -> michelson result = fun e s ->
let get : environment -> Var.t -> michelson result = fun e s ->
let%bind (_ , position) =
let error =
let title () = "Environment.get" in
let content () = Format.asprintf "%s in %a"
s PP.environment e in
let content () = Format.asprintf "%a in %a"
Var.pp s PP.environment e in
error title content in
generic_try error @@
(fun () -> Environment.get_i s e) in
@ -34,7 +34,7 @@ let get : environment -> string -> michelson result = fun e s ->
ok code
let set : environment -> string -> michelson result = fun e s ->
let set : environment -> Var.t -> michelson result = fun e s ->
let%bind (_ , position) =
generic_try (simple_error "Environment.set") @@
(fun () -> Environment.get_i s e) in
@ -65,8 +65,8 @@ let pack_closure : environment -> selector -> michelson result = fun e lst ->
let e_lst =
let e_lst = Environment.to_list e in
let aux selector (s , _) =
match List.mem s selector with
| true -> List.remove_element s selector , true
match List.mem ~compare:Var.compare s selector with
| true -> List.remove_element ~compare:Var.compare s selector , true
| false -> selector , false in
let e_lst' = List.fold_map_right aux lst e_lst in
let e_lst'' = List.combine e_lst e_lst' in

View File

@ -7,8 +7,8 @@ open Michelson
module Stack = Meta_michelson.Stack
*)
val empty: environment
val get : environment -> string -> michelson result
val set : environment -> string -> michelson result
val get : environment -> Var.t -> michelson result
val set : environment -> Var.t -> michelson result
val pack_closure : environment -> selector -> michelson result
val unpack_closure : environment -> michelson result

View File

@ -457,7 +457,7 @@ let get_main : program -> string -> (anon_function * _) result = fun p entry ->
let is_main (((name , expr), _):toplevel_statement) =
match Combinators.Expression.(get_content expr , get_type expr)with
| (E_closure content , T_function ty)
when name = entry ->
when Var.equal name (Var.of_name entry) ->
Some (content , ty)
| _ -> None
in

View File

@ -42,7 +42,7 @@ and annotated ppf : type_value annotated -> _ = function
| (None, a) -> type_ ppf a
and environment_element ppf ((s, tv) : environment_element) =
Format.fprintf ppf "%s : %a" s type_ tv
Format.fprintf ppf "%a : %a" Var.pp s type_ tv
and environment ppf (x:environment) =
fprintf ppf "Env[%a]" (list_sep_d environment_element) x
@ -75,7 +75,7 @@ and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
and expression' ppf (e:expression') = match e with
| E_skip -> fprintf ppf "skip"
| E_closure x -> fprintf ppf "C(%a)" function_ x
| E_variable v -> fprintf ppf "V(%s)" v
| E_variable v -> fprintf ppf "V(%a)" Var.pp v
| E_application(a, b) -> fprintf ppf "(%a)@(%a)" expression a expression b
| E_constant(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst
| E_literal v -> fprintf ppf "L(%a)" value v
@ -85,19 +85,25 @@ and expression' ppf (e:expression') = match e with
| E_make_empty_set _ -> fprintf ppf "set[]"
| E_make_none _ -> fprintf ppf "none"
| E_if_bool (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b
| E_if_none (c, n, ((name, _) , s)) -> fprintf ppf "%a ?? %a : %s -> %a" expression c expression n name expression s
| E_if_cons (c, n, (((hd_name, _) , (tl_name, _)) , cons)) -> fprintf ppf "%a ?? %a : (%s :: %s) -> %a" expression c expression n hd_name tl_name expression cons
| E_if_none (c, n, ((name, _) , s)) ->
fprintf ppf "%a ?? %a : %a -> %a"
expression c expression n Var.pp name expression s
| E_if_cons (c, n, (((hd_name, _) , (tl_name, _)) , cons)) ->
fprintf ppf "%a ?? %a : (%a :: %a) -> %a"
expression c expression n Var.pp hd_name Var.pp tl_name expression cons
| E_if_left (c, ((name_l, _) , l), ((name_r, _) , r)) ->
fprintf ppf "%a ?? %s -> %a : %s -> %a" expression c name_l expression l name_r expression r
fprintf ppf "%a ?? %a -> %a : %a -> %a"
expression c Var.pp name_l expression l Var.pp name_r expression r
| E_sequence (a , b) -> fprintf ppf "%a ;; %a" expression a expression b
| E_let_in ((name , _) , expr , body) ->
fprintf ppf "let %s = %a in ( %a )" name expression expr expression body
fprintf ppf "let %a = %a in ( %a )" Var.pp name expression expr expression body
| E_iterator (s , ((name , _) , body) , expr) ->
fprintf ppf "for_%s %s of %a do ( %a )" s name expression expr expression body
fprintf ppf "for_%s %a of %a do ( %a )" s Var.pp name expression expr expression body
| E_fold (((name , _) , body) , collection , initial) ->
fprintf ppf "fold %a on %a with %s do ( %a )" expression collection expression initial name expression body
fprintf ppf "fold %a on %a with %a do ( %a )"
expression collection expression initial Var.pp name expression body
| E_assignment (r , path , e) ->
fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e
fprintf ppf "%a.%a := %a" Var.pp r (list_sep lr (const ".")) path expression e
| E_while (e , b) ->
fprintf ppf "while (%a) %a" expression e expression b
@ -110,15 +116,28 @@ and expression_with_type : _ -> expression -> _ = fun ppf e ->
type_ e.type_value
and function_ ppf ({binder ; body}:anon_function) =
fprintf ppf "fun %s -> (%a)"
binder
fprintf ppf "fun %a -> (%a)"
Var.pp binder
expression body
and assignment ppf ((n, e):assignment) = fprintf ppf "%s = %a;" n expression e
and assignment ppf ((n, e):assignment) = fprintf ppf "%a = %a;" Var.pp n expression e
and declaration ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e
and declaration ppf ((n, e):assignment) = fprintf ppf "let %a = %a;" Var.pp n expression e
let tl_statement ppf (ass, _) = assignment ppf ass
let program ppf (p:program) =
fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p
let%expect_test _ =
let pp = expression' Format.std_formatter in
let dummy_type = T_base Base_unit in
let wrap e = { content = e ; type_value = dummy_type } in
pp @@ E_closure { binder = Var.of_name "y" ; body = wrap (E_variable (Var.of_name "y")) } ;
[%expect{|
C(fun y -> (V(y)))
|}] ;
pp @@ E_closure { binder = Var.of_name "z" ; body = wrap (E_variable (Var.of_name "z")) } ;
[%expect{|
C(fun z -> (V(z)))
|}]

View File

@ -168,13 +168,6 @@ let t_function x y : type_value = T_function ( x , y )
let t_pair x y : type_value = T_pair ( x , y )
let t_union x y : type_value = T_or ( x , y )
let quote binder body : anon_function =
{
binder ;
body ;
}
let e_int expr : expression = Expression.make_tpl (expr, t_int)
let e_unit : expression = Expression.make_tpl (E_literal D_unit, t_unit)
let e_skip : expression = Expression.make_tpl (E_skip, t_unit)
@ -188,13 +181,6 @@ let ez_e_sequence a b : expression = Expression.(make_tpl (E_sequence (make_tpl
let d_unit : value = D_unit
let basic_quote expr in_ty out_ty : expression result =
let expr' = E_closure (quote "input" expr) in
ok @@ Expression.make_tpl (expr' , t_function in_ty out_ty)
let basic_int_quote expr : expression result =
basic_quote expr t_int t_int
let environment_wrap pre_environment post_environment = { pre_environment ; post_environment }
let id_environment_wrap e = environment_wrap e e

View File

@ -66,18 +66,14 @@ val e_int : Expression.t' -> Expression.t
*)
val e_unit : Expression.t
val e_skip : Expression.t
val e_var_int : string -> Expression.t
val e_let_in : string -> type_value -> Expression.t -> Expression.t -> Expression.t
val e_var_int : Var.t -> Expression.t
val e_let_in : Var.t -> type_value -> Expression.t -> Expression.t -> Expression.t
val ez_e_sequence : Expression.t' -> Expression.t -> expression
(*
val ez_e_return : Expression.t -> Expression.t
*)
val d_unit : value
(*
val basic_quote : type_value -> type_value -> Expression.t -> anon_function result
*)
val basic_int_quote : expression -> expression result
val environment_wrap : environment -> environment -> environment_wrap
val id_environment_wrap : environment -> environment_wrap

View File

@ -1,6 +0,0 @@
open Types
open Combinators
let basic_int_quote_env : environment =
let e = Environment.empty in
Environment.add ("input", t_int) e

View File

@ -1,3 +0,0 @@
open Types
val basic_int_quote_env : environment

View File

@ -5,8 +5,7 @@
simple-utils
tezos-utils
)
(preprocess
(pps ppx_let)
)
(inline_tests)
(preprocess (pps ppx_expect ppx_let))
(flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
)

View File

@ -21,23 +21,23 @@ module Environment (* : ENVIRONMENT *) = struct
let empty : t = []
let add : element -> t -> t = List.cons
let concat : t list -> t = List.concat
let get_opt : string -> t -> type_value option = List.assoc_opt
let has : string -> t -> bool = fun s t ->
let get_opt : Var.t -> t -> type_value option = List.assoc_opt ~compare:Var.compare
let has : Var.t -> t -> bool = fun s t ->
match get_opt s t with
| None -> false
| Some _ -> true
let get_i : string -> t -> (type_value * int) = List.assoc_i
let get_i : Var.t -> t -> (type_value * int) = List.assoc_i ~compare:Var.compare
let of_list : element list -> t = fun x -> x
let to_list : t -> element list = fun x -> x
let get_names : t -> string list = List.map fst
let get_names : t -> Var.t list = List.map fst
let remove : int -> t -> t = List.remove
let select ?(rev = false) ?(keep = true) : string list -> t -> t = fun lst env ->
let select ?(rev = false) ?(keep = true) : Var.t list -> t -> t = fun lst env ->
let e_lst =
let e_lst = to_list env in
let aux selector (s , _) =
match List.mem s selector with
| true -> List.remove_element s selector , keep
match List.mem ~compare:Var.compare s selector with
| true -> List.remove_element ~compare:Var.compare s selector , keep
| false -> selector , not keep in
let e_lst' =
if rev = keep

View File

@ -11,15 +11,15 @@ module Environment : sig
val add : element -> t -> t
val concat : t list -> t
(*
val get_opt : string -> t -> type_value option
val has : string -> t -> bool
val get_opt : Var.t -> t -> type_value option
val has : Var.t -> t -> bool
*)
val get_i : string -> t -> (type_value * int)
val get_i : Var.t -> t -> (type_value * int)
val of_list : element list -> t
val to_list : t -> element list
val get_names : t -> string list
val get_names : t -> Var.t list
val remove : int -> t -> t
val select : ?rev:bool -> ?keep:bool -> string list -> t -> t
val select : ?rev:bool -> ?keep:bool -> Var.t list -> t -> t
(*
val fold : ('a -> element -> 'a ) -> 'a -> t -> 'a
val filter : ( element -> bool ) -> t -> t
@ -36,20 +36,20 @@ val empty : t
val add : element -> t -> t
val concat : t list -> t
(*
val get_opt : string -> t -> type_value option
val get_opt : Var.t -> t -> type_value option
*)
val has : string -> t -> bool
val has : Var.t -> t -> bool
(*
val get_i : string -> t -> (type_value * int)
val get_i : Var.t -> t -> (type_value * int)
*)
val of_list : element list -> t
(*
val to_list : t -> element list
val get_names : t -> string list
val get_names : t -> Var.t list
val remove : int -> t -> t
*)
val select : ?rev:bool -> ?keep:bool -> string list -> t -> t
val select : ?rev:bool -> ?keep:bool -> Var.t list -> t -> t
val fold : ('a -> element -> 'a ) -> 'a -> t -> 'a
val filter : ( element -> bool ) -> t -> t

View File

@ -24,13 +24,16 @@ end
module Free_variables = struct
type bindings = string list
let mem : string -> bindings -> bool = List.mem
let singleton : string -> bindings = fun s -> [ s ]
type bindings = Var.t list
let mem : Var.t -> bindings -> bool = List.memq ~eq:Var.equal
let mem_count : Var.t -> bindings -> int =
fun x fvs ->
List.length (List.filter (Var.equal x) fvs)
let singleton : Var.t -> bindings = fun s -> [ s ]
let union : bindings -> bindings -> bindings = (@)
let unions : bindings list -> bindings = List.concat
let empty : bindings = []
let of_list : string list -> bindings = fun x -> x
let of_list : Var.t list -> bindings = fun x -> x
let rec expression : bindings -> expression -> bindings = fun b e ->
let self = expression b in
@ -121,7 +124,7 @@ end
Converts `expr` in `fun () -> expr`.
*)
let functionalize (body : expression) : expression =
let content = E_closure { binder = "_" ; body } in
let content = E_closure { binder = Var.fresh () ; body } in
let type_value = t_function t_unit body.type_value in
{ content ; type_value }
@ -130,7 +133,7 @@ let get_entry (lst : program) (name : string) : (expression * int) result =
trace_option (Errors.missing_entry_point name) @@
let aux x =
let (((decl_name , decl_expr) , _)) = x in
if (decl_name = name)
if (Var.equal decl_name (Var.of_name name))
then Some decl_expr
else None
in
@ -139,7 +142,7 @@ let get_entry (lst : program) (name : string) : (expression * int) result =
let entry_index =
let aux x =
let (((decl_name , _) , _)) = x in
decl_name = name
Var.equal decl_name (Var.of_name name)
in
List.find_index aux lst
in

View File

@ -23,7 +23,7 @@ type type_value =
| T_contract of type_value
| T_option of type_value
and environment_element = string * type_value
and environment_element = Var.t * type_value
and environment = environment_element list
@ -32,8 +32,8 @@ type environment_wrap = {
post_environment : environment ;
}
type var_name = string
type fun_name = string
type var_name = Var.t
type fun_name = Var.t
type value =
| D_unit
@ -78,7 +78,7 @@ and expression' =
| E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression)
| E_let_in of ((var_name * type_value) * expression * expression)
| E_sequence of (expression * expression)
| E_assignment of (string * [`Left | `Right] list * expression)
| E_assignment of (var_name * [`Left | `Right] list * expression)
| E_while of (expression * expression)
and expression = {
@ -91,7 +91,7 @@ and assignment = var_name * expression
and toplevel_statement = assignment * environment_wrap
and anon_function = {
binder : string ;
binder : var_name ;
body : expression ;
}

View File

@ -6,10 +6,12 @@ module Location = Location
module List = X_list
module Option = X_option
module Int = X_int
module Tuple = Tuple
module Map = X_map
module Dictionary = Dictionary
module Tree = Tree
module Region = Region
module Pos = Pos
module Var = Var

View File

@ -1,5 +1,6 @@
let map_h_2 f g (a , b) = (f a , g b)
let map2 f (a, b) = (f a, f b)
let map3 f (a , b , c) = (f a , f b , f c)
let apply2 f (a, b) = f a b
let list2 (a, b) = [a;b]

39
vendors/ligo-utils/simple-utils/var.ml vendored Normal file
View File

@ -0,0 +1,39 @@
type t = {
name : string ;
counter : int option ;
}
let pp ppf v =
match v.counter with
| None -> Format.fprintf ppf "%s" v.name
| Some i -> Format.fprintf ppf "%s#%d" v.name i
module Int = X_int
module Option = X_option
let equal v1 v2 =
String.equal v1.name v2.name
&& Option.equal Int.equal v1.counter v2.counter
let compare v1 v2 =
let cname = String.compare v1.name v2.name in
if Int.equal cname 0
then Option.compare Int.compare v1.counter v2.counter
else cname
let global_counter = ref 0
let reset_counter () = global_counter := 0
let of_name name =
{ name = name ;
counter = None
}
let fresh ?name () =
let name = Option.unopt ~default:"" name in
let counter = incr global_counter ; Some !global_counter in
{ name ; counter }
let fresh_like v =
fresh ~name:v.name ()

42
vendors/ligo-utils/simple-utils/var.mli vendored Normal file
View File

@ -0,0 +1,42 @@
(* Currently, Var.t is equivalent to (string * int option). The
optional counter value is present on variables generated with
`fresh`.
The intent is that there are two disjoint classes of variables:
'user variables' (embedded with `of_name`) and 'generated
variables' (generated with `fresh`.)
Vars with indices are printed as %s#%d. This could be confusing if
vars like `name_of "foo#121"` are allowed -- `name_of "foo#121"`
will be _not equal_ to a generated var `fresh ~name:"foo"` with
counter 121, despite being printed the same way.
This module does not prevent that confusion. But, the LIGO lexer
does not accept names like "foo#121" as possible variable names, so
this confusion should not arise for us. *)
type t
val equal : t -> t -> bool
val compare : t -> t -> int
(* Prints vars as %s or %s#%d *)
val pp : Format.formatter -> t -> unit
(* Construct a user variable directly from a string. This should only
be used for embedding user variable names. For programmatically
generated variables, use `fresh`. Take care not to cause
shadowing/capture except as the user intended. *)
val of_name : string -> t
(* Generate a variable, using a counter value from a _global_
counter. If the name is not provided, it will be empty. *)
val fresh : ?name:string -> unit -> t
(* Generate a variable as with `fresh`, reusing the name part of the
given variable. *)
val fresh_like : t -> t
(* Reset the global counter. Danger, do not use... Provided for tests
only. *)
val reset_counter : unit -> unit

View File

@ -0,0 +1,2 @@
let equal : int -> int -> bool = (=)
let compare : int -> int -> int = compare

View File

@ -39,11 +39,17 @@ let fold_map : type acc ele ret . (acc -> ele -> (acc * ret)) -> acc -> ele list
let fold_right' f init lst = List.fold_left f init (List.rev lst)
let rec remove_element x lst =
(* breaking a dependency cycle with X_option *)
let unopt ~default x = match x with
| None -> default
| Some x -> x
let rec remove_element ?compare:cmp x lst =
let compare = unopt ~default:compare cmp in
match lst with
| [] -> raise (Failure "X_list.remove_element")
| hd :: tl when x = hd -> tl
| hd :: tl -> hd :: remove_element x tl
| hd :: tl when compare x hd = 0 -> tl
| hd :: tl -> hd :: remove_element ~compare x tl
let filter_map f =
let rec aux acc lst = match lst with
@ -94,10 +100,10 @@ let find_full f lst =
| _ :: tl -> aux (n + 1) tl in
aux 0 lst
let assoc_i x lst =
let assoc_i ~compare x lst =
let rec aux n = function
| [] -> raise (Failure "List:assoc_i")
| (x', y) :: _ when x = x' -> (y, n)
| (x', y) :: _ when compare x x' = 0 -> (y, n)
| _ :: tl -> aux (n + 1) tl
in
aux 0 lst
@ -139,6 +145,35 @@ let to_singleton = function
| [a] -> Some a
| _ -> None
(** overriding stdlib List functions with optional compare/eq
arguments *)
let rec mem ?compare:cmp x =
let compare = unopt ~default:compare cmp in
function
| [] -> false
| a::l -> compare a x = 0 || mem ~compare x l
let rec memq ?eq:eq x =
let eq = unopt ~default:(=) eq in
function
| [] -> false
| a::l -> eq a x || memq ~eq x l
let rec assoc ?compare:cmp x =
let compare = unopt ~default:compare cmp in
function
[] -> raise Not_found
| (a,b)::l -> if compare a x = 0 then b else assoc ~compare x l
let rec assoc_opt ?compare:cmp x =
let compare = unopt ~default:compare cmp in
function
[] -> None
| (a,b)::l -> if compare a x = 0 then Some b else assoc_opt ~compare x l
module Ne = struct
type 'a t = 'a * 'a list

View File

@ -72,3 +72,16 @@ let bind_smap (s:_ X_map.String.t) =
fold aux s (Some empty)
let bind_map_smap f smap = bind_smap (X_map.String.map f smap)
let equal eq x y =
match (x, y) with
| (None, None) -> true
| (Some x, Some y) -> eq x y
| _ -> false
let compare compare x y =
match (x, y) with
| (None, None) -> 0
| (None, Some _) -> -1
| (Some _, None) -> 1
| (Some x, Some y) -> compare x y