Initial structure for HerbSpecification

.github/workflows/CI.yml

@@ -0,0 +1,35 @@
+name: CI
+on:
+  push:
+    branches:
+      - master
+    tags: ['*']
+  pull_request:
+concurrency:
+  # Skip intermediate builds: always.
+  # Cancel intermediate builds: only if it is a pull request build.
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ startsWith(github.ref, 'refs/pull/') }}
+jobs:
+  test:
+    name: Julia ${{ matrix.version }} - ${{ matrix.os }} - ${{ matrix.arch }} - ${{ github.event_name }}
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        version:
+          - '1.8'
+          - 'nightly'
+        os:
+          - ubuntu-latest
+        arch:
+          - x64
+    steps:
+      - uses: actions/checkout@v3
+      - uses: julia-actions/setup-julia@v1
+        with:
+          version: ${{ matrix.version }}
+          arch: ${{ matrix.arch }}
+      - uses: julia-actions/cache@v1
+      - uses: julia-actions/julia-buildpkg@v1
+      - uses: julia-actions/julia-runtest@v1

.github/workflows/CompatHelper.yml

@@ -0,0 +1,16 @@
+name: CompatHelper
+on:
+  schedule:
+    - cron: 0 0 * * *
+  workflow_dispatch:
+jobs:
+  CompatHelper:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Pkg.add("CompatHelper")
+        run: julia -e 'using Pkg; Pkg.add("CompatHelper")'
+      - name: CompatHelper.main()
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          COMPATHELPER_PRIV: ${{ secrets.DOCUMENTER_KEY }}
+        run: julia -e 'using CompatHelper; CompatHelper.main()'

.github/workflows/TagBot.yml

@@ -0,0 +1,31 @@
+name: TagBot
+on:
+  issue_comment:
+    types:
+      - created
+  workflow_dispatch:
+    inputs:
+      lookback:
+        default: 3
+permissions:
+  actions: read
+  checks: read
+  contents: write
+  deployments: read
+  issues: read
+  discussions: read
+  packages: read
+  pages: read
+  pull-requests: read
+  repository-projects: read
+  security-events: read
+  statuses: read
+jobs:
+  TagBot:
+    if: github.event_name == 'workflow_dispatch' || github.actor == 'JuliaTagBot'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: JuliaRegistries/TagBot@v1
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          ssh: ${{ secrets.DOCUMENTER_KEY }}

LICENSE → LICENCE.md

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2024 Herb-AI
+Copyright (c) 2023 Herb-AI
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

Project.toml

@@ -0,0 +1,4 @@
+name = "HerbSpecification"
+uuid = "6d54aada-062f-46d8-85cf-a1ceaf058a06"
+authors = ["Tilman Hinnerichs <[email protected]>"]
+version = "0.1.0"

README.md

@@ -1,2 +1,3 @@
 # HerbSpecification.jl
 Describes the types of specification to define program synthesis problems
+

src/HerbSpecification.jl

@@ -0,0 +1,24 @@
+module HerbSpecification
+
+include("problem.jl")
+
+export 
+    Problem,
+    AbstractSpecification,
+
+    AbstractIOSpecification,
+    IOExample,
+    IOSpecification,
+    IOMetricSpecification,
+
+    AbstractFormalSpecification,
+    SMTSpecification,
+    AgdaSpecification,
+
+    Trace,
+    TraceSpecification,
+
+    TypeSpecification,
+    DependentTypeSpecification
+
+end # module HerbSpecification

src/problem.jl

@@ -0,0 +1,104 @@
+abstract type AbstractSpecification end
+
+"""
+    struct Problem
+
+Program synthesis problem defined with a vector of [`AbstractSpecification`](@ref)s. 
+
+!!! warning
+    Please care that concrete `Problem` types with different values of `T` are never subtypes of each other. 
+"""
+struct Problem{T <: AbstractSpecification}
+    name::AbstractString
+    spec::T
+
+    function Problem(spec::T) where T<:AbstractSpecification
+        new{T}("", spec)
+    end
+end
+
+
+abstract type AbstractIOSpecification <: AbstractSpecification end
+
+"""
+    struct IOExample
+
+An input-output example.
+`in` is a [`Dict`](@ref) of `{Symbol,Any}` where the symbol represents a variable in a program.
+`out` can be anything.
+"""
+
+struct IOExample
+    in::Dict{Symbol, Any}
+    out::Any
+end
+
+"""
+    struct IOSpecification <: AbstractIOSpecification
+
+"""
+struct IOSpecification <: AbstractIOSpecification
+    examples::Vector{IOExample}
+end
+
+"""
+    struct IOMetricSpecification <: AbstractIOSpecification
+
+"""
+struct IOMetricSpecification <: AbstractIOSpecification
+    examples::AbstractVector{IOExample}
+    cost_function::Function
+end
+
+"""
+    Base.getindex(p::Problem{AbstractIOSpecification}, indices)
+
+Overwrite `Base.getindex` to access allow for slicing of problems.
+"""
+Base.getindex(p::Problem{AbstractIOSpecification}, indices) = Problem(p.spec.examples[indices])
+
+
+abstract type AbstractFormalSpecification <: AbstractSpecification
+end
+
+"""
+    struct SMTSpecification <: AbstractFormalSpecification
+
+"""
+struct SMTSpecification <: AbstractFormalSpecification
+    formula::Function
+end
+
+"""
+    struct AgdaSpecification <: AbstractFormalSpecification
+
+"""
+struct AgdaSpecification <: AbstractFormalSpecification
+    formula::Function
+end
+
+# abstract type Trace end #@TODO combine with Gen.jl
+struct Trace
+    exec_path::Vector{Any}
+end
+
+
+"""
+    struct TraceSpecification
+
+"""
+struct TraceSpecification <: AbstractSpecification
+    traces::Vector{Trace}
+end
+
+
+
+abstract type AbstractTypeSpecification <: AbstractSpecification end
+
+"""
+    struct DependentTypeSpecification <: AbstractTypeSpecification
+
+"""
+struct DependentTypeSpecification <: AbstractTypeSpecification
+    formula::Function
+end

test/runtests.jl

@@ -0,0 +1,6 @@
+using HerbSpecification
+using Test
+
+@testset "HerbSpecification.jl" verbose=true begin
+
+end