add refine iota transformation in lcalc

This commit is contained in:
Alain 2021-12-01 15:42:01 +01:00
parent 5f86837428
commit 3f8bc482f3

View File

@ -18,7 +18,9 @@ let ( let+ ) x f = Bindlib.box_apply f x
let ( and+ ) x y = Bindlib.box_pair x y
let visitor_map (t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box) (ctx : 'a)
let visitor_map
(t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
(ctx : 'a)
(e : expr Pos.marked) : expr Pos.marked Bindlib.box =
(* calls [t ctx] on every direct childs of [e], then rebuild an abstract syntax tree modified.
Used in other transformations. *)
@ -67,6 +69,19 @@ let rec iota_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box
| EMatch ((EInj (e1, i, n', _ts), _), cases, n) when Dcalc.Ast.EnumName.compare n n' = 0 ->
let+ e1 = visitor_map iota_expr () e1 and+ case = visitor_map iota_expr () (List.nth cases i) in
default_mark @@ EApp (case, [ e1 ])
| EMatch (e', cases, n) when begin
cases
|> List.mapi (fun i (case, _pos) ->
match case with
| EInj (_ei, i', n', _ts') ->
i = i' && (* n = n' *) (Dcalc.Ast.EnumName.compare n n' = 0)
| _ -> false
)
|> List.for_all Fun.id
end ->
visitor_map iota_expr () e'
| _ -> visitor_map iota_expr () e
let iota_optimizations (p : program) : program =