Extract (imandra-base.Imandra_interactive.Extract)

Extraction

type model = Imandra_surface.Top_result.model

type expr = Imandra_surface.Term.t

val to_string : 
  ?scope:Opentelemetry.Trace.scope ->
  ?signature:Imandra_surface.Uid.t ->
  ?ext_sig:bool ->
  ?accessors:bool ->
  unit ->
  string

to_string () produces a code fragment that defines a module Mex which can be used to extract term models

parameter signature
if present, name of a function whose argument list will become a record type. This is typically a function we decompose using Modular_decomp.

parameter ext_sig
if true, the emitted module will include types for each argument of the signature function, named t_<name of argument>.

parameter accessors
if true, the emitted module will include accessors for the extract_type record, named ret_<name of argument>.

val eval : 
  ?scope:Opentelemetry.Trace.scope ->
  ?quiet:bool ->
  ?signature:Imandra_surface.Uid.t ->
  ?ext_sig:bool ->
  ?accessors:bool ->
  unit ->
  unit

Calls generate and then evaluates the code fragment

val to_file : 
  ?scope:Opentelemetry.Trace.scope ->
  ?signature:Imandra_surface.Uid.t ->
  ?ext_sig:bool ->
  ?accessors:bool ->
  string ->
  unit

to_file filename extracts code to the given file

Predefined Accessors

Accessors used by the generated code. Do not call directly.