import-ir

Reference page for the import-ir.schema.json JSON schema.

Versions

Accepted format: arxo.import/0.1.

Top-level fields

name	type-or-$ref	required	description
format	"arxo.import/0.1"	yes	—
snapshot	#/$defs/Snapshot	yes	—
documents	object	yes	—
anchors	object	yes	—
modules	object	yes	—
symbols	object	yes	—
expressions	object	yes	—
declarations	object	yes	—
dependencies	array	yes	—
facts	object	no	—
dependency_completeness	enum (2)	no	—

Enumerations

location	values
properties/format	"arxo.import/0.1"
properties/dependencies/items/properties/kind	"type", "statement", "definition"
properties/facts/additionalProperties/properties/args/items/oneOf/0/properties/kind	"entity"
properties/facts/additionalProperties/properties/args/items/oneOf/1/properties/kind	"string"
properties/dependency_completeness	"module", "declaration"
$defs/Symbol/properties/kind	"type", "predicate"
$defs/Expression/oneOf/0/properties/kind	"var"
$defs/Expression/oneOf/1/properties/kind	"atom"
$defs/Expression/oneOf/2/properties/kind	"and"
$defs/Expression/oneOf/3/properties/kind	"or"
$defs/Expression/oneOf/4/properties/kind	"implies"
$defs/Expression/oneOf/5/properties/kind	"forall"
$defs/Expression/oneOf/6/properties/kind	"exists"
$defs/Expression/oneOf/7/properties/kind	"not"
$defs/Expression/oneOf/8/properties/kind	"equal"
$defs/Expression/oneOf/9/properties/kind	"opaque"
$defs/Declaration/properties/kind	"theorem", "definition", "axiom", "instance"

Raw schema

https://law.arxo.io/schema/import-ir.schema.json

Snapshot

Type: object. Required: project, revision, language, logic, adapter, context_complete, retrieved_at, requires.

name	type-or-$ref	description
project	string	—
revision	string	—
language	string	—
logic	string	—
adapter	string	—
context_complete	boolean	—
retrieved_at	string	—
requires	array	—

Document

Type: object. Required: uri, language, official, text, content_hash.

name	type-or-$ref	description
uri	string	—
language	string	—
official	boolean	—
text	string	—
content_hash	string	—

Anchor

Type: object. Required: document, start, end, locator.

name	type-or-$ref	description
document	string	—
start	integer	—
end	integer	—
locator	string	—

Symbol

Type: object. Required: kind, parameters, label.

name	type-or-$ref	description
kind	enum (2)	—
parameters	array	—
label	string	—

Expression

Definition Expression.

Declaration

Type: object. Required: module, kind, label, parameters, context, statement, anchor, requires.

name	type-or-$ref	description
module	string	—
kind	enum (4)	—
label	string	—
parameters	array	—
context	array	—
statement	string	—
anchor	string	—
requires	array	—