Module Polarize

module Polarize: sig .. end

Polarize

This duplicates some predicate definitions (either recursive equations, or (co)inductive specifications) depending on the call-site polarity.

type term = Nunchaku_core.TermInner.Default.t

type decode_state

val name : string

val polarize : polarize_rec:bool ->
       (term, term) Nunchaku_core.Problem.t ->
       (term, term) Nunchaku_core.Problem.t *
       decode_state

Polarize inductive predicates and possibly some other predicates in the problem.

polarize_rec : if true, some propositions defined with `rec` might be polarized

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

val pipe : polarize_rec:bool ->
       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

Pipeline component

val pipe_with : ?on_decoded:('d -> unit) list ->
       decode:(decode_state -> 'c -> 'd) ->
       polarize_rec:bool ->
       print:bool ->
       check:bool ->
       ((term, term) Nunchaku_core.Problem.t,
        (term, term) Nunchaku_core.Problem.t, 'c, 'd)
       Nunchaku_core.Transform.t

Generic Pipe Component

decode : the decode function that takes an applied (module S) in addition to the state