Module Specialize

module Specialize: sig .. end

Specialization

Specialization replaces some function, argument to another (higher-order) function, by its definition. It only works when the argument is known.

Example:

 let rec map f l = match l with

     | [] -> []

     | x::l2 -> f x :: map f l2



    map (fun x -> x+ g(x)) l

is converted into

  let rec map_357 l = match l with

    | [] -> []

    | x::l2 -> (x + g(x)) :: map_357 l2



    map_357 l

val name : string

exception Error of string

type term = Nunchaku_core.TermInner.Default.t

type ty = term

type decode_state

Used to decode

val specialize_problem : (term, term) Nunchaku_core.Problem.t ->
       (term, term) Nunchaku_core.Problem.t *
       decode_state

val decode_term : decode_state -> term -> term

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

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