Module Monomorphization

module Monomorphization: sig .. end

Monomorphization

val name : string

exception InvalidProblem of string

type term = Nunchaku_core.TermInner.Default.t

type unmangle_state

State used to un-mangle specialized symbols

val monomorphize : ?depth_limit:int ->
       ?always_mangle:bool ->
       (term, term) Nunchaku_core.Problem.t ->
       (term, term) Nunchaku_core.Problem.t *
       unmangle_state

Filter and specialize definitions of the problem.

First it finds a set of instances for each symbol such that it is sufficient to instantiate the corresponding (partial) definitions of the symbol with those tuples.

Then it specializes relevant definitions with the set of tuples computed earlier.
Returns a new list of (monomorphized) statements, and the final state obtained after monomorphization

depth_limit : recursion limit for specialization of functions

always_mangle : if true, polymorphic types become new atomic types, e.g. list int becomes list_int (default: false)

val unmangle_term : state:unmangle_state ->
       term -> term

Unmangle a single term: replace mangled constants by their definition

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

Unmangles constants that have been collapsed with their type arguments

val pipe : always_mangle: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 : decode:(unmangle_state -> 'c -> 'd) ->
       always_mangle: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

always_mangle : see Monomorphization.monomorphize