Patmatch2 (imandra-base.Imandra_interactive.Patmatch2)

Compilation of Match

This goes from syntactic terms to internal Term.t, using case rather than partial operations or operations that do not have a strict OCaml equivalent. Terms obtained this way should be printable back into OCaml.

type term = Imandra_surface.Term.t

type syn_term = Imandra_surface.Term.Syn.t

type pattern = Imandra_surface.Term.Syn.pattern

val compile_top_let : 
  loc:Imandra_util.Iloc.t ->
  pattern ->
  term ->
  term Imandra_surface.Term.binding list

Compile a toplevel let pat = expr into a list of variable bindings

val compile : 
  loc:Imandra_util.Iloc.t ->
  syn_term ->
  term * (Imandra_surface.Term.t * Imandra_surface.As_trigger.t) list

Turn a syntactic term into a term, by compiling all pattern matching away