WIP
This commit is contained in:
parent
e9e0a462ac
commit
9946c4206f
@ -428,6 +428,65 @@ Some example comments refer to interactive commands such as:
|
|||||||
Those commands appear to belong to an external REPL or tool environment rather
|
Those commands appear to belong to an external REPL or tool environment rather
|
||||||
than to the `.geolog` file grammar itself.
|
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
|
## Best Example Files by Feature
|
||||||
|
|
||||||
- `transitive_closure.geolog`: basic theory, axiom, and `= chase` usage
|
- `transitive_closure.geolog`: basic theory, axiom, and `= chase` usage
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user