Remove (unused) assignment from mini_c

This commit is contained in:
Tom Jack 2020-02-25 12:25:15 -06:00
parent b969672596
commit 8229d6a6af
9 changed files with 5 additions and 176 deletions

View File

@ -80,10 +80,6 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
let%bind res = bind_fold_pair self init' ab in let%bind res = bind_fold_pair self init' ab in
ok res ok res
) )
| E_assignment (_, _, exp) -> (
let%bind res = self init' exp in
ok res
)
| E_record_update (r, _, e) -> ( | E_record_update (r, _, e) -> (
let%bind res = self init' r in let%bind res = self init' r in
let%bind res = self res e in let%bind res = self res e in
@ -150,10 +146,6 @@ let rec map_expression : mapper -> expression -> expression result = fun f e ->
let%bind ab' = bind_map_pair self ab in let%bind ab' = bind_map_pair self ab in
return @@ E_sequence ab' return @@ E_sequence ab'
) )
| E_assignment (s, lrl, exp) -> (
let%bind exp' = self exp in
return @@ E_assignment (s, lrl, exp')
)
| E_record_update (r, l, e) -> ( | E_record_update (r, l, e) -> (
let%bind r = self r in let%bind r = self r in
let%bind e = self e in let%bind e = self e in
@ -166,4 +158,4 @@ let map_sub_level_expression : mapper -> expression -> expression result = fun f
let%bind body = map_expression f body in let%bind body = map_expression f body in
let content = E_closure {binder; body} in let content = E_closure {binder; body} in
ok @@ { e with content } ok @@ { e with content }
| _ -> ok e | _ -> ok e

View File

@ -79,10 +79,6 @@ let rec is_pure : expression -> bool = fun e ->
is near... *) is near... *)
| E_while _ -> false | E_while _ -> false
(* definitely not pure *)
| E_assignment _ -> false
let occurs_in : expression_variable -> expression -> bool = let occurs_in : expression_variable -> expression -> bool =
fun x e -> fun x e ->
let fvs = Free_variables.expression [] e in let fvs = Free_variables.expression [] e in
@ -93,63 +89,6 @@ let occurs_count : expression_variable -> expression -> int =
let fvs = Free_variables.expression [] e in let fvs = Free_variables.expression [] e in
Free_variables.mem_count x fvs Free_variables.mem_count x fvs
(* 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 -> expression_variable -> 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_assignment (x, _, e) ->
it x || self e
| E_record_update (r, _, e) ->
self r || self e
| E_closure { binder; body } ->
if ignore_lambdas
then false
else self_binder binder body
| E_constant (c) ->
selfs c.arguments
| 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 "inlining" mean transforming the code: (* Let "inlining" mean transforming the code:
let x = e1 in e2 let x = e1 in e2
@ -163,25 +102,11 @@ let rec is_assigned : ignore_lambdas:bool -> expression_variable -> expression -
Things which can go wrong for inlining: Things which can go wrong for inlining:
- If `e1` is not pure, inlining may fail to preserve semantics. - 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 - Free variables of `e1` may be shadowed in e2, at usages of `x`. This
is not a problem if the substitution is capture-avoiding. is not a problem if the substitution is capture-avoiding.
- ? - ?
*) *)
let can_inline : expression_variable -> 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 : expression_variable -> expression -> bool = let should_inline : expression_variable -> expression -> bool =
fun x e -> fun x e ->
occurs_count x e <= 1 occurs_count x e <= 1
@ -190,10 +115,8 @@ let inline_let : bool ref -> expression -> expression =
fun changed e -> fun changed e ->
match e.content with match e.content with
| E_let_in ((x, _a), should_inline_here, e1, e2) -> | E_let_in ((x, _a), should_inline_here, e1, e2) ->
if can_inline x e1 e2 && (should_inline_here || should_inline x e2) if is_pure e1 && (should_inline_here || should_inline x e2)
then 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 let e2' = Subst.subst_expression ~body:e2 ~x:x ~expr:e1 in
(changed := true ; e2') (changed := true ; e2')
else else
@ -215,26 +138,15 @@ let inline_lets : bool ref -> expression -> expression =
Things which can go wrong for beta reduction: Things which can go wrong for beta reduction:
- If e1 contains (meaningful) assignments to free variables, semantics - Nothing?
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 = let beta : bool ref -> expression -> expression =
fun changed e -> fun changed e ->
match e.content with match e.content with
| E_application ({ content = E_closure { binder = x ; body = e1 } ; type_value = T_function (xtv, tv) }, e2) -> | E_application ({ content = E_closure { binder = x ; body = e1 } ; type_value = T_function (xtv, tv) }, e2) ->
if can_beta { binder = x ; body = e1 } (changed := true ;
then Expression.make (E_let_in ((x, xtv), false, e2, e1)) tv)
(changed := true ;
Expression.make (E_let_in ((x, xtv), false, 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 *) (* also do CAR (PAIR x y) ↦ x, or CDR (PAIR x y) ↦ y, only if x and y are pure *)
| E_constant {cons_name = C_CAR| C_CDR as const; arguments = [ { content = E_constant {cons_name = C_PAIR; arguments = [ e1 ; e2 ]} ; type_value = _ } ]} -> | E_constant {cons_name = C_CAR| C_CDR as const; arguments = [ { content = E_constant {cons_name = C_PAIR; arguments = [ e1 ; e2 ]} ; type_value = _ } ]} ->

View File

@ -90,10 +90,6 @@ let rec replace : expression -> var_name -> var_name -> expression =
let e1 = replace e1 in let e1 = replace e1 in
let e2 = replace e2 in let e2 = replace e2 in
return @@ E_sequence (e1, e2) 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_record_update (r, p, e) -> | E_record_update (r, p, e) ->
let r = replace r in let r = replace r in
let e = replace e in let e = replace e in
@ -107,7 +103,6 @@ let rec replace : expression -> var_name -> var_name -> expression =
Computes `body[x := expr]`. Computes `body[x := expr]`.
This raises Bad_argument in the case of assignments with a name clash. (`x <- 42[x := 23]` makes no sense.) 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 = let rec subst_expression : body:expression -> x:var_name -> expr:expression -> expression =
fun ~body ~x ~expr -> fun ~body ~x ~expr ->
let self body = subst_expression ~body ~x ~expr in let self body = subst_expression ~body ~x ~expr in
@ -204,11 +199,6 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e
let ab' = Tuple.map2 self ab in let ab' = Tuple.map2 self ab in
return @@ E_sequence ab' 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')
)
| E_record_update (r, p, e) -> ( | E_record_update (r, p, e) -> (
let r' = self r in let r' = self r in
let e' = self e in let e' = self e in

View File

@ -35,29 +35,6 @@ let get : environment -> expression_variable -> michelson result = fun e s ->
ok code ok code
let set : environment -> expression_variable -> michelson result = fun e n ->
let%bind (_ , position) =
generic_try (simple_error "Environment.set") @@
(fun () -> Environment.get_i n e) in
let rec aux_bubble = fun n ->
match n with
| 0 -> dip i_drop
| n -> seq [
i_swap ;
dip (aux_bubble (n - 1)) ;
]
in
let aux_dug = fun n -> seq [
dipn (n + 1) i_drop ;
i_dug n ;
] in
let code =
if position < 2
then aux_bubble position
else aux_dug position in
ok code
let pack_closure : environment -> selector -> michelson result = fun e lst -> let pack_closure : environment -> selector -> michelson result = fun e lst ->
let%bind () = Assert.assert_true (e <> []) in let%bind () = Assert.assert_true (e <> []) in

View File

@ -8,7 +8,6 @@ module Stack = Meta_michelson.Stack
*) *)
val empty: environment val empty: environment
val get : environment -> expression_variable -> michelson result val get : environment -> expression_variable -> michelson result
val set : environment -> expression_variable -> michelson result
val pack_closure : environment -> selector -> michelson result val pack_closure : environment -> selector -> michelson result
val unpack_closure : environment -> michelson result val unpack_closure : environment -> michelson result

View File

@ -386,42 +386,6 @@ and translate_expression (expr:expression) (env:environment) : michelson result
] in ] in
ok code ok code
) )
| E_assignment (name , lrs , expr) -> (
let%bind expr' = translate_expression expr env in
let%bind get_code = Compiler_environment.get env name in
let modify_code =
let aux acc step = match step with
| `Left -> seq [dip i_unpair ; acc ; i_pair]
| `Right -> seq [dip i_unpiar ; acc ; i_piar]
in
let init = dip i_drop in
List.fold_right' aux init lrs
in
let%bind set_code = Compiler_environment.set env name in
let error =
let title () = "michelson type-checking patch" in
let content () =
let aux ppf = function
| `Left -> Format.fprintf ppf "left"
| `Right -> Format.fprintf ppf "right" in
Format.asprintf "Sub path: %a\n"
PP_helpers.(list_sep aux (const " , ")) lrs
in
error title content in
trace error @@
return @@ seq [
i_comment "assign: start # env" ;
expr' ;
i_comment "assign: compute rhs # rhs : env" ;
dip get_code ;
i_comment "assign: get name # rhs : name : env" ;
modify_code ;
i_comment "assign: modify code # name+rhs : env" ;
set_code ;
i_comment "assign: set new # new_env" ;
i_push_unit ;
]
)
| E_record_update (record, path, expr) -> ( | E_record_update (record, path, expr) -> (
let%bind record' = translate_expression record env in let%bind record' = translate_expression record env in

View File

@ -104,8 +104,6 @@ and expression' ppf (e:expression') = match e with
| E_fold (((name , _) , body) , collection , initial) -> | E_fold (((name , _) , body) , collection , initial) ->
fprintf ppf "fold %a on %a with %a do ( %a )" expression collection expression initial Var.pp 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 "%a.%a := %a" Var.pp r (list_sep lr (const ".")) path expression e
| E_record_update (r, path,update) -> | E_record_update (r, path,update) ->
fprintf ppf "%a with { %a = %a }" expression r (list_sep lr (const ".")) path expression update fprintf ppf "%a with { %a = %a }" expression r (list_sep lr (const ".")) path expression update
| E_while (e , b) -> | E_while (e , b) ->

View File

@ -79,8 +79,6 @@ module Free_variables = struct
expression (union (singleton v) b) body ; expression (union (singleton v) b) body ;
] ]
| E_sequence (x, y) -> union (self x) (self y) | E_sequence (x, y) -> union (self x) (self y)
(* NB different from ast_typed... *)
| E_assignment (v, _, e) -> unions [ var_name b v ; self e ]
| E_record_update (r, _,e) -> union (self r) (self e) | E_record_update (r, _,e) -> union (self r) (self e)
| E_while (cond , body) -> union (self cond) (self body) | E_while (cond , body) -> union (self cond) (self body)

View File

@ -72,7 +72,6 @@ and expression' =
| E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression) | E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression)
| E_let_in of ((var_name * type_value) * inline * expression * expression) | E_let_in of ((var_name * type_value) * inline * expression * expression)
| E_sequence of (expression * expression) | E_sequence of (expression * expression)
| E_assignment of (expression_variable * [`Left | `Right] list * expression)
| E_record_update of (expression * [`Left | `Right] list * expression) | E_record_update of (expression * [`Left | `Right] list * expression)
| E_while of (expression * expression) | E_while of (expression * expression)