Module LambdaLift

module LambdaLift: sig .. end

Lambda Lifting

Remaining λ expressions are extracted as toplevel named functions; equalities such as (fun x. t) = (fun y. u) are replaced by forall x. t = u[x/y].

type term = Nunchaku_core.TermInner.Default.t

val name : string

type state

val tr_problem : (term, term) Nunchaku_core.Problem.t ->
       (term, term) Nunchaku_core.Problem.t * state

val decode_model : state:state ->
       (term, term) Nunchaku_core.Model.t ->
       (term, term) Nunchaku_core.Model.t

val pipe : print:bool ->
       check:bool ->
       ((term, term) Nunchaku_core.Problem.t,
        (term, term) Nunchaku_core.Problem.t,
        (term, term) Nunchaku_core.Problem.Res.t,
        (term, term) Nunchaku_core.Problem.Res.t)
       Nunchaku_core.Transform.t

val pipe_with : decode:(state -> 'c -> 'd) ->
       print:bool ->
       check:bool ->
       ((term, term) Nunchaku_core.Problem.t,
        (term, term) Nunchaku_core.Problem.t, 'c, 'd)
       Nunchaku_core.Transform.t

Similar to LambdaLift.pipe but with a generic decode function.

print : if true, prints problem after lifting

check : if true, check the invariants on the result