# Geolog DSL Structure

This directory contains example `.geolog` files that use a richer DSL than the
minimal `.chase` script language in `examples/scripts/`.

This README summarizes the Geolog DSL structure as it appears in the examples in
this directory. It should be read as a practical, example-driven reference, not
as a formal or complete language specification.

## At a Glance

- Top-level declarations are `theory` and `instance`.
- The main kind of type is `Sort`.
- Symbols can denote sorts, constants, functions, predicates, or nested
  instances.
- Axioms use sequent-style syntax: `premise |- conclusion`.
- Instance bodies can be plain literals (`= { ... }`) or chase blocks
  (`= chase { ... }`).
- Function application is postfix, and qualified names use `/`.

## Informal File Shape

```text
file := { comment | theory_decl | instance_decl }

comment := // ...

theory_decl :=
  theory theory_params? Name {
    theory_item*
  }

instance_decl :=
  instance Name : theory_app = {
    instance_item*
  }

  | instance Name : theory_app = chase {
      instance_item*
    }
```

In practice, a file is usually a sequence of theory declarations followed by one
or more example instances.

## Top-Level Declarations

### `theory`

A theory introduces sorts, symbols, and axioms.

```text
theory Graph {
  V : Sort;
  Edge : [src: V, tgt: V] -> Prop;
}
```

Theories may also be parameterized.

```text
theory (X : Sort) (Y : Sort) Iso {
  fwd : X -> Y;
  bwd : Y -> X;
}

theory (N : PetriNet instance) Marking {
  token : Sort;
  token/of : token -> N/P;
}
```

Observed parameter forms:

- sort parameters: `(X : Sort)`
- instance parameters: `(N : PetriNet instance)`
- dependent instance parameters: `(RP : N ReachabilityProblem instance)`

### `instance`

An instance provides concrete elements and assignments for a theory.

```text
instance Triangle : Graph = {
  A : V;
  B : V;
  C : V;
}
```

Instances may target parameterized theories by writing the arguments before the
theory name.

```text
instance MyMap : MyBase Map = { ... }
instance solution0 : ExampleNet problem0 Solution = { ... }
instance AB_Iso : As/a Bs/b Iso = { ... }
```

## Theory Body Items

The examples show the following declaration forms inside a theory body.

### Sort declarations

```text
V : Sort;
E : Sort;
```

This introduces carrier sorts.

### Constants or distinguished elements

```text
elem : X;
```

This introduces a named element of an existing sort.

### Functions

```text
src : E -> V;
fwd : X -> Y;
token/of : token -> N/P;
```

Names may contain `/`, which is used heavily for structured or qualified names.

### Predicates and relations

Unary predicates:

```text
completed : Item -> Prop;
```

Record-shaped predicates:

```text
Edge : [src: V, tgt: V] -> Prop;
depends : [item: Item, on: Item] -> Prop;
```

### Product-valued functions

Functions may return record-shaped values.

```text
pair_of : A -> [left: B, right: C];
W/src : W -> [firing: F, arc: N/out];
```

### Nested instance slots

Theories can contain fields whose values are themselves instances.

```text
initial_marking : N Marking instance;
trace : N Trace instance;
initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
```

### Axioms

Axioms use a sequent-like form.

```text
ax/trans : forall x, y, z : V.
  [src: x, tgt: y] Path, [src: y, tgt: z] Path |- [src: x, tgt: z] Path;
```

An axiom declaration has the observed structure:

```text
name : forall binders. premise |- conclusion;
```

## Formula and Term Syntax

The examples use the following building blocks inside axioms and assignments.

### Quantifiers

Universal binders appear after `forall`.

```text
forall x : X, y : Y.
```

Existentials appear directly inside conclusions or disjuncts.

```text
exists r : R. r R/data = [x: a, y: b]
exists w : W. w W/src_firing = f, w W/src_arc = arc
```

### Sequents

The central connective is `|-`, separating premise from conclusion.

```text
premise1, premise2 |- conclusion1, conclusion2;
```

In the examples:

- commas act as conjunctions
- the left side is the premise
- the right side is the conclusion

### Equality

Equality is used for ordinary values and compound values.

```text
ab src = A
r R/data = [x: a, y: b]
x fwd bwd = x
```

### Truth constants

```text
|- true;
|- false;
```

### Disjunction

Disjunction is written as `\/`.

```text
[item: x, on: y] depends |- x blocked \/ y completed;
```

### Predicate atoms

Unary predicate atoms:

```text
x blocked
y completed
```

Record-shaped predicate atoms:

```text
[src: x, tgt: y] Edge
[a: x, f: i] id
```

### Postfix application

Function application is postfix and can be chained.

```text
e src
x id
x fwd bwd
w W/src_arc N/out/tgt
```

This is one of the most distinctive traits of the DSL.

### Qualified paths

The slash `/` is used for qualification and nested access.

Observed examples include:

```text
R/data
N/P
N/out/src
trace/input_terminal
RP/initial_marking/token
ExampleNet/A
```

### Record literals

Records are written with brackets and named fields.

```text
[x: a, y: b]
[firing: f, arc: arc]
```

The examples also show positional shorthand for record arguments when the field
order is known:

```text
[e, e] mul = e;
[cook_dinner, on: buy_groceries] depends;
```

### Field projection

Record-valued terms support field projection.

```text
r R/data .x = a
```

## Instance Body Items

The examples show the following forms inside instance bodies.

### Element declarations

```text
a : V;
tok : token;
ab : T;
```

### Function assignments

```text
ab src = A;
tok token/of = ExampleNet/A;
a1 map = MyBase/b1;
```

### Predicate facts

Unary facts:

```text
buy_groceries completed;
```

Record-shaped facts:

```text
[src: a, tgt: b] Edge;
[item: x, on: y] depends;
```

### Product-valued assignments

```text
a1 pair_of = [left: b1, right: c1];
ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out];
```

### Nested instance literals

Instance-valued fields can be assigned inline blocks.

```text
initial_marking = {
  tok : token;
  tok token/of = ExampleNet/A;
};
```

## `= { ... }` vs `= chase { ... }`

The examples consistently use two instance forms.

### Plain instance

```text
instance Triangle : Graph = {
  ...
}
```

This gives a direct structure with only the explicitly listed elements and
assignments.

### Chase instance

```text
instance Chain : Graph = chase {
  ...
}
```

This marks an instance whose contents should be extended by the theory axioms.
Examples use this for transitive closure, existential witness generation, and
trace/reachability constructions.

## Observed Design Patterns

### Parameterized theories

Theories can be abstract over:

- a sort, such as `theory (X : Sort) Container`
- an instance, such as `theory (N : PetriNet instance) Marking`
- multiple arguments, such as `theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution`

### Theory application by adjacency

Theory arguments are written before the theory name.

```text
N Marking instance
MyBase Map
ExampleNet problem0 Solution
```

### Nested structure via qualified names

Many examples model dependent structure by naming into earlier declarations.

```text
token/of : token -> N/P;
initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
```

## What Seems Outside the File DSL

Some example comments refer to interactive commands such as:

```text
:source
:load
:inspect
:chase
:solve
```

Those commands appear to belong to an external REPL or tool environment rather
than to the `.geolog` file grammar itself.

## Querying

The examples do **not** show a stable, implemented query form inside `.geolog`
files in the same way they show `theory` and `instance` declarations.

What they do show is:

### 1. External interactive commands

Some files suggest that querying or inspection happens through an external tool
or REPL:

```text
:source examples/geolog/transitive_closure.geolog
:inspect Chain
:chase Chain
:solve EmptyModel
```

Based on the example comments, these commands appear to mean roughly:

- `:source` or `:load`: load Geolog definitions from files
- `:inspect`: inspect a declared instance
- `:chase`: materialize or display the closure of a `= chase` instance
- `:solve`: ask a solver to construct a satisfying instance for a theory

These are tool commands, not part of the confirmed `.geolog` declaration syntax.

### 2. A sketched future query form

One file contains a commented-out example of a possible query block:

```text
query can_reach_B_from_A {
  ? : ExampleNet problem0 Solution instance;
}
```

This suggests an aspirational style where querying is expressed as asking for a
witness inhabiting some instance type. However, in the current examples this is
only a comment, not an observed live construct.

### 3. Current implemented querying elsewhere in the repo

The currently implemented query syntax in this repository belongs to the minimal
frontend language, not to Geolog. That language supports forms such as:

```text
query Ancestor(?X, ?Y)?
explain Ancestor(alice, carol)?
```

So the safest summary is:

- Geolog examples define theories, instances, and chase-oriented structure.
- Querying appears to be external, REPL-driven, or still in design.
- The only clearly implemented query syntax in this repo today is the minimal
  `.chase` frontend query language.

## Best Example Files by Feature

- `transitive_closure.geolog`: basic theory, axiom, and `= chase` usage
- `graph.geolog`: plain structural instances
- `monoid.geolog`: postfix application and positional record syntax
- `todo_list.geolog`: unary predicates and disjunction
- `sort_param_simple.geolog`: sort and instance parameters
- `nested_instance_test.geolog`: nested instance-valued fields
- `product_codomain_test.geolog`: record-valued function codomains
- `field_projection_test.geolog`: field projection syntax
- `record_existential_test.geolog`: existential witness creation with records
- `petri_net_showcase.geolog`: large multi-theory composition
- `solver_demo.geolog`: satisfiability-oriented axiom patterns

## Minimal Example

```text
theory Graph {
  V : Sort;
  Edge : [src: V, tgt: V] -> Prop;
  Path : [src: V, tgt: V] -> Prop;

  ax/base : forall x, y : V.
    [src: x, tgt: y] Edge |- [src: x, tgt: y] Path;
}

instance Chain : Graph = chase {
  a : V;
  b : V;
  [src: a, tgt: b] Edge;
}
```

That small example already shows the core structure of the DSL:

- a `theory`
- sort and predicate declarations
- an axiom written as a sequent
- an `instance`
- a `chase` block that asks for closure under the theory axioms