HerbSpecification.jl Documentation

struct AbstractDependentTypeSpecification <: AbstractTypeSpecification

Defines a specification through dependent types. Needs a concrete type checker as oracle.

struct AgdaSpecification <: AbstractDependentTypeSpecification

Defines a specification

struct IOExample

An input-output example. in is a Dict of {Symbol,Any} where the symbol represents a variable in a program. out can be anything.

struct MetricProblem{T <: Vector{IOExample}}

Program synthesis problem defined by an specification and a metric. The specification has to be based on input/output examples, while the function needs to return a numerical value.

struct Problem

Program synthesis problem defined by an AbstractSpecifications. Has a name and a specification of type T.

struct SMTSpecification <: AbstractFormalSpecification

A specification based on a logical formula defined by a SMT solver.

struct Trace

A trace defining a wanted program execution for program synthesis. @TODO combine with Gen.jl

Base.getindex(p::Problem{Vector{IOExample}}, indices)

Overwrite Base.getindex to allow for slicing of input/output-based problems.