and opt1_lambda g es c name w t =
let name = H.mk_fresh_name c name in
let entry = Some (name, C.Decl w) in
and opt1_lambda g es c name w t =
let name = H.mk_fresh_name c name in
let entry = Some (name, C.Decl w) in
- let g t =
- let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
- g (C.Lambda (name, w, t))
- in
+ let g t = g (C.Lambda (name, w, t)) in
| Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv ->
let x = C.Appl (t :: List.rev rvs @ [define rv]) in
HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x
| Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv ->
let x = C.Appl (t :: List.rev rvs @ [define rv]) in
HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x
let rec aux h prev = function
| C.LetIn (name, vv, tt) :: vs ->
let t = S.lift 1 t in
let rec aux h prev = function
| C.LetIn (name, vv, tt) :: vs ->
let t = S.lift 1 t in
let optimize_obj = function
| C.Constant (name, Some bo, ty, pars, attrs) ->
let g bo =
let optimize_obj = function
| C.Constant (name, Some bo, ty, pars, attrs) ->
let g bo =
let _ = H.get_type [] (C.Cast (bo, ty)) in
C.Constant (name, Some bo, ty, pars, attrs)
in
let _ = H.get_type [] (C.Cast (bo, ty)) in
C.Constant (name, Some bo, ty, pars, attrs)
in
- Printf.eprintf "BEGIN: %s\n" name;
- begin try opt1_term (opt2_term g []) true [] bo
+ Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n"
+ name (I.count_nodes 0 bo);
+ begin try opt1_term g (* (opt2_term g []) *) true [] bo