Struct TypeDirectedSynth 

pub struct TypeDirectedSynth {
    pub depth_limit: usize,
    pub attempts: usize,
}

Type-directed synthesiser: Djinn/Agsy-style proof search.

Fields

depth_limit: usize

Depth limit for proof search.

attempts: usize

Number of synthesis attempts made.

Implementations

impl TypeDirectedSynth

pub fn new(depth_limit: usize) -> Self

Create a new synthesiser with a depth limit.

pub fn synthesise( &mut self, ctx: &SynthContext, goal_type: &SynthType, depth: usize, ) -> Option<String>

Attempt to synthesise a term of goal_type from ctx.

Returns a program string on success.

Trait Implementations

impl Clone for TypeDirectedSynth

fn clone(&self) -> TypeDirectedSynth

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TypeDirectedSynth

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.