Module Imandra_tools.Region_term_synth

exception Unsupported

Raised for unsupported Term.t expressions

val decompile : ?compound:bool -> ?default:Imandra_surface.Term.Syn.t -> ?xf:( Imandra_surface.Term.Syn.t -> Imandra_surface.Term.Syn.t ) -> Imandra_surface.Term.t -> Imandra_surface.Term.Syn.t

Decompiles a Term.t value as a Term.Syn.t. Raises Unsupported if the Term.t is not compatible with the fragment returned by Decompose.

  • parameter compound

    if true, don't expand connectives into if-then-else

  • parameter default

    default value when needing to close a non-present branch

  • parameter xf

    apply a transformation to a (non default) leaf of a branch

val synthesize : ?compound:bool -> ?default:Imandra_surface.Term.Syn.t -> ?xf:( Imandra_surface.Term.Syn.t -> Imandra_surface.Term.Syn.t ) -> Imandra_surface.Term.t -> string

Synthesize a Term.t value as ocaml code. Raises Unsupported if the Term.t is not compatible with the fragment returned by Decompose.

  • parameter compound

    if true, don't expand connectives into if-then-else

  • parameter default

    default value when needing to close a non-present branch

  • parameter xf

    apply a transformation to a (non default) leaf of a branch