Module Smyth.Term_gen

val fresh_ident : Lang.type_ctx -> char -> string

fresh_ident gamma c returns an identifier starting with the character c that does not appear in the type context gamma

val function_char : char

The canonical first character for function names.

val variable_char : char

The canonical first character for variable names.

val match_char : char

The canonical first character for variable names used in pattern matching in a case expression.

val clear_cache : unit -> unit

Clears the memoization cache. Important note: make sure to call clear_cache once synthesis is fully complete for a problem, and not any sooner or later!

val up_to_e : Lang.datatype_ctx -> int -> Lang.gen_goal -> Lang.exp Nondet.t

up_to_e sigma n goal nondeterministically generates elimination forms at a goal goal up to (and including) AST size n.