From 1ff3eff78a6b9f2f5cb39d0cb0e4d56b772b3f59 Mon Sep 17 00:00:00 2001
From: Tilman Hinnerichs <tilman@hinnerichs.com>
Date: Mon, 22 Jan 2024 14:34:25 +0100
Subject: [PATCH] Update test, Readme and docs

---
 README.md                |  6 +++++-
 src/HerbSpecification.jl |  4 ++--
 src/problem.jl           | 18 +++++++++++++++---
 test/runtests.jl         |  2 +-
 4 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/README.md b/README.md
index 348d0d1..dd74fda 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,7 @@
 # HerbSpecification.jl
-Describes the types of specification to define program synthesis problems
+[![Build Status](https://github.com/Herb-AI/HerbSpecification.jl/actions/workflows/CI.yml/badge.svg?branch=master)](https://github.com/Herb-AI/HerbSpecification.jl/actions/workflows/CI.yml?query=branch%3Amaster)
+
+This package describes the types of specification to define program synthesis problems within the `Herb.jl` Program Synthesis framework. 
+
+For full documentation please see the `Herb.jl` documentation.
 
diff --git a/src/HerbSpecification.jl b/src/HerbSpecification.jl
index e359155..b44ea7b 100644
--- a/src/HerbSpecification.jl
+++ b/src/HerbSpecification.jl
@@ -11,11 +11,11 @@ export
 
     AbstractFormalSpecification,
     SMTSpecification,
-    AgdaSpecification,
 
     Trace,
 
     AbstractTypeSpecification,
-    DependentTypeSpecification
+    DependentTypeSpecification,
+    AgdaSpecification
 
 end # module HerbSpecification
diff --git a/src/problem.jl b/src/problem.jl
index 02369f3..f95f3f9 100644
--- a/src/problem.jl
+++ b/src/problem.jl
@@ -10,7 +10,12 @@ struct IOExample
     out::Any
 end
 
-# abstract type Trace end #@TODO combine with Gen.jl
+"""
+    struct Trace
+
+A trace defining a wanted program execution for program synthesis. 
+@TODO combine with Gen.jl
+"""
 struct Trace
     exec_path::Vector{Any}
 end
@@ -20,6 +25,7 @@ abstract type AbstractFormalSpecification end
 """
     struct SMTSpecification <: AbstractFormalSpecification
 
+A specification based on a logical formula defined by a SMT solver.
 """
 struct SMTSpecification <: AbstractFormalSpecification
     formula::Function
@@ -31,12 +37,14 @@ abstract type AbstractTypeSpecification end
 """
     struct AbstractDependentTypeSpecification <: AbstractTypeSpecification
 
+Defines a specification through dependent types. Needs a concrete type checker as oracle.
 """
 abstract type AbstractDependentTypeSpecification <: AbstractTypeSpecification end
 
 """
     struct AgdaSpecification <: AbstractDependentTypeSpecification
 
+Defines a specification 
 """
 struct AgdaSpecification <: AbstractDependentTypeSpecification
     formula::Function
@@ -47,7 +55,7 @@ const AbstractSpecification = Union{Vector{IOExample}, AbstractFormalSpecificati
 """
     struct Problem
 
-Program synthesis problem defined with a vector of [`AbstractSpecification`](@ref)s. 
+Program synthesis problem defined by an [`AbstractSpecification`](@ref)s. Has a name and a specification of type `T`.
 
 !!! warning
     Please care that concrete `Problem` types with different values of `T` are never subtypes of each other. 
@@ -64,7 +72,11 @@ struct Problem{T <: AbstractSpecification}
     end
 end
 
+"""
+    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 MetricProblem{T <: Vector{IOExample}}
     name::AbstractString
     cost_function::Function
@@ -84,7 +96,7 @@ end
 """
     Base.getindex(p::Problem{Vector{IOExample}}, indices)
 
-Overwrite `Base.getindex` to access allow for slicing of problems.
+Overwrite `Base.getindex` to allow for slicing of input/output-based problems.
 """
 Base.getindex(p::Problem{Vector{IOExample}}, indices) = Problem(p.spec[indices])
 Base.getindex(p::MetricProblem{Vector{IOExample}}, indices) = Problem(p.spec[indices])
diff --git a/test/runtests.jl b/test/runtests.jl
index 93bd827..45608d0 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -2,5 +2,5 @@ using HerbSpecification
 using Test
 
 @testset "HerbSpecification.jl" verbose=true begin
-    
+    include("test_ioproblem.jl") 
 end