Last active
November 13, 2025 00:26
-
-
Save saulshanabrook/fe7cd1ff78329a38616f43212f322076 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "$schema": "https://json-schema.org/draft/2020-12/schema", | |
| "title": "Array_of_GenericCommand", | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericCommand" | |
| }, | |
| "$defs": { | |
| "GenericCommand": { | |
| "description": "A [`Command`] is the top-level construct in egglog.\nIt includes defining rules, declaring functions,\nadding to tables, and running rules (via a [`Schedule`]).", | |
| "oneOf": [ | |
| { | |
| "$ref": "#/$defs/Sort" | |
| }, | |
| { | |
| "$ref": "#/$defs/Datatype" | |
| }, | |
| { | |
| "$ref": "#/$defs/Datatypes" | |
| }, | |
| { | |
| "$ref": "#/$defs/Constructor" | |
| }, | |
| { | |
| "$ref": "#/$defs/Relation" | |
| }, | |
| { | |
| "$ref": "#/$defs/Function" | |
| }, | |
| { | |
| "$ref": "#/$defs/AddRuleset" | |
| }, | |
| { | |
| "$ref": "#/$defs/UnstableCombinedRuleset" | |
| }, | |
| { | |
| "$ref": "#/$defs/Rule" | |
| }, | |
| { | |
| "$ref": "#/$defs/Rewrite" | |
| }, | |
| { | |
| "$ref": "#/$defs/BiRewrite" | |
| }, | |
| { | |
| "$ref": "#/$defs/Action" | |
| }, | |
| { | |
| "$ref": "#/$defs/Extract" | |
| }, | |
| { | |
| "$ref": "#/$defs/RunSchedule" | |
| }, | |
| { | |
| "$ref": "#/$defs/PrintOverallStatistics" | |
| }, | |
| { | |
| "$ref": "#/$defs/Check" | |
| }, | |
| { | |
| "$ref": "#/$defs/PrintFunction" | |
| }, | |
| { | |
| "$ref": "#/$defs/PrintSize" | |
| }, | |
| { | |
| "$ref": "#/$defs/Input" | |
| }, | |
| { | |
| "$ref": "#/$defs/Output" | |
| }, | |
| { | |
| "$ref": "#/$defs/Push" | |
| }, | |
| { | |
| "$ref": "#/$defs/Pop" | |
| }, | |
| { | |
| "$ref": "#/$defs/Fail" | |
| }, | |
| { | |
| "$ref": "#/$defs/Include" | |
| }, | |
| { | |
| "$ref": "#/$defs/UserDefined" | |
| } | |
| ] | |
| }, | |
| "Sort": { | |
| "description": "Create a new user-defined sort, which can then\nbe used in new [`Command::Function`] declarations.\nThe [`Command::Datatype`] command desugars directly to this command, with one [`Command::Function`]\nper constructor.\nThe main use of this command (as opposed to using [`Command::Datatype`]) is for forward-declaring a sort for mutually-recursive datatypes.\n\nIt can also be used to create\na container sort.\nFor example, here's how to make a sort for vectors\nof some user-defined sort `Math`:\n```text\n(sort MathVec (Vec Math))\n```\n\nNow `MathVec` can be used as an input or output sort.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "field3": { | |
| "type": [ | |
| "array", | |
| "null" | |
| ], | |
| "prefixItems": [ | |
| { | |
| "type": "string" | |
| }, | |
| { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericExpr" | |
| } | |
| } | |
| ], | |
| "minItems": 2, | |
| "maxItems": 2 | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Sort" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "Span": { | |
| "oneOf": [ | |
| { | |
| "$ref": "#/$defs/Panic" | |
| }, | |
| { | |
| "$ref": "#/$defs/Egglog" | |
| }, | |
| { | |
| "$ref": "#/$defs/Rust" | |
| } | |
| ] | |
| }, | |
| "Panic": { | |
| "type": "object", | |
| "properties": { | |
| "type": { | |
| "type": "string", | |
| "const": "Panic" | |
| } | |
| }, | |
| "required": [ | |
| "type" | |
| ] | |
| }, | |
| "Egglog": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/EgglogSpan" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Egglog" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1" | |
| ] | |
| }, | |
| "EgglogSpan": { | |
| "type": "object", | |
| "properties": { | |
| "file": { | |
| "$ref": "#/$defs/SrcFile" | |
| }, | |
| "i": { | |
| "type": "integer", | |
| "format": "uint", | |
| "minimum": 0 | |
| }, | |
| "j": { | |
| "type": "integer", | |
| "format": "uint", | |
| "minimum": 0 | |
| } | |
| }, | |
| "required": [ | |
| "file", | |
| "i", | |
| "j" | |
| ] | |
| }, | |
| "SrcFile": { | |
| "type": "object", | |
| "properties": { | |
| "name": { | |
| "type": [ | |
| "string", | |
| "null" | |
| ] | |
| }, | |
| "contents": { | |
| "type": "string" | |
| } | |
| }, | |
| "required": [ | |
| "contents" | |
| ] | |
| }, | |
| "Rust": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/RustSpan" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Rust" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1" | |
| ] | |
| }, | |
| "RustSpan": { | |
| "type": "object", | |
| "properties": { | |
| "file": { | |
| "type": "string" | |
| }, | |
| "line": { | |
| "type": "integer", | |
| "format": "uint32", | |
| "minimum": 0 | |
| }, | |
| "column": { | |
| "type": "integer", | |
| "format": "uint32", | |
| "minimum": 0 | |
| } | |
| }, | |
| "required": [ | |
| "file", | |
| "line", | |
| "column" | |
| ] | |
| }, | |
| "GenericExpr": { | |
| "oneOf": [ | |
| { | |
| "$ref": "#/$defs/Var" | |
| }, | |
| { | |
| "$ref": "#/$defs/Call" | |
| }, | |
| { | |
| "$ref": "#/$defs/Lit" | |
| } | |
| ] | |
| }, | |
| "Var": { | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "name": { | |
| "type": "string" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Var" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "span", | |
| "name" | |
| ] | |
| }, | |
| "Call": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "field3": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericExpr" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Call" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3" | |
| ] | |
| }, | |
| "Lit": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/Literal" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Lit" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "Literal": { | |
| "anyOf": [ | |
| { | |
| "type": "integer", | |
| "format": "int64" | |
| }, | |
| { | |
| "type": "number", | |
| "format": "double" | |
| }, | |
| { | |
| "type": "string" | |
| }, | |
| { | |
| "type": "boolean" | |
| }, | |
| { | |
| "type": "null" | |
| } | |
| ] | |
| }, | |
| "Datatype": { | |
| "description": "Egglog supports three types of functions\n\nA constructor models an egg-style user-defined datatype\nIt can only be defined through the `datatype`/`datatype*` command\nor the `constructor` command\n\nA relation models a datalog-style mathematical relation\nIt can only be defined through the `relation` command\n\nA custom function is a dictionary\nIt can only be defined through the `function` command\n\nThe `datatype` command declares a user-defined datatype.\nDatatypes can be unioned with [`Action::Union`] either\nat the top level or in the actions of a rule.\nThis makes them equal in the implicit, global equality relation.\n\nExample:\n```text\n(datatype Math\n (Num i64)\n (Var String)\n (Add Math Math)\n (Mul Math Math))\n```\n\ndefines a simple `Math` datatype with variants for numbers, named variables, addition and multiplication.\n\nDatatypes desugar directly to a [`Command::Sort`] and a [`Command::Constructor`] for each constructor.\nThe code above becomes:\n```text\n(sort Math)\n(constructor Num (i64) Math)\n(constructor Var (String) Math)\n(constructor Add (Math Math) Math)\n(constructor Mul (Math Math) Math)\n\nDatatypes are also known as algebraic data types, tagged unions and sum types.", | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "name": { | |
| "type": "string" | |
| }, | |
| "variants": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/Variant" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Datatype" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "span", | |
| "name", | |
| "variants" | |
| ] | |
| }, | |
| "Variant": { | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "name": { | |
| "type": "string" | |
| }, | |
| "types": { | |
| "type": "array", | |
| "items": { | |
| "type": "string" | |
| } | |
| }, | |
| "cost": { | |
| "type": [ | |
| "integer", | |
| "null" | |
| ], | |
| "format": "uint64", | |
| "minimum": 0 | |
| }, | |
| "unextractable": { | |
| "type": "boolean" | |
| } | |
| }, | |
| "required": [ | |
| "span", | |
| "name", | |
| "types", | |
| "unextractable" | |
| ] | |
| }, | |
| "Datatypes": { | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "datatypes": { | |
| "type": "array", | |
| "items": { | |
| "type": "array", | |
| "prefixItems": [ | |
| { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| { | |
| "type": "string" | |
| }, | |
| { | |
| "$ref": "#/$defs/Subdatatypes" | |
| } | |
| ], | |
| "minItems": 3, | |
| "maxItems": 3 | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Datatypes" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "span", | |
| "datatypes" | |
| ] | |
| }, | |
| "Subdatatypes": { | |
| "oneOf": [ | |
| { | |
| "$ref": "#/$defs/Variants" | |
| }, | |
| { | |
| "$ref": "#/$defs/NewSort" | |
| } | |
| ] | |
| }, | |
| "Variants": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/Variant" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Variants" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1" | |
| ] | |
| }, | |
| "NewSort": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "type": "string" | |
| }, | |
| "field2": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericExpr" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "NewSort" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "Constructor": { | |
| "description": "The `constructor` command defines a new constructor for a user-defined datatype\nExample:\n```text\n(constructor Add (i64 i64) Math)\n```", | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "name": { | |
| "type": "string" | |
| }, | |
| "schema": { | |
| "$ref": "#/$defs/Schema" | |
| }, | |
| "cost": { | |
| "type": [ | |
| "integer", | |
| "null" | |
| ], | |
| "format": "uint64", | |
| "minimum": 0 | |
| }, | |
| "unextractable": { | |
| "type": "boolean" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Constructor" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "span", | |
| "name", | |
| "schema", | |
| "unextractable" | |
| ] | |
| }, | |
| "Schema": { | |
| "type": "object", | |
| "properties": { | |
| "input": { | |
| "type": "array", | |
| "items": { | |
| "type": "string" | |
| } | |
| }, | |
| "output": { | |
| "type": "string" | |
| } | |
| }, | |
| "required": [ | |
| "input", | |
| "output" | |
| ] | |
| }, | |
| "Relation": { | |
| "description": "The `relation` command declares a named relation\nExample:\n```text\n(relation path (i64 i64))\n(relation edge (i64 i64))\n```", | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "name": { | |
| "type": "string" | |
| }, | |
| "inputs": { | |
| "type": "array", | |
| "items": { | |
| "type": "string" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Relation" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "span", | |
| "name", | |
| "inputs" | |
| ] | |
| }, | |
| "Function": { | |
| "description": "The `function` command declare an egglog custom function, which is a database table with a\na functional dependency (also called a primary key) on its inputs to one output.\n\n```text\n(function <name:Ident> <schema:Schema> <cost:Cost>\n (:on_merge <List<Action>>)?\n (:merge <Expr>)?)\n```\nA function can have a `cost` for extraction.\n\nFinally, it can have a `merge` and `on_merge`, which are triggered when\nthe function dependency is violated.\nIn this case, the merge expression determines which of the two outputs\nfor the same input is used.\nThe `on_merge` actions are run after the merge expression is evaluated.\n\nNote that the `:merge` expression must be monotonic\nfor the behavior of the egglog program to be consistent and defined.\nIn other words, the merge function must define a lattice on the output of the function.\nIf values are merged in different orders, they should still result in the same output.\nIf the merge expression is not monotonic, the behavior can vary as\nactions may be applied more than once with different results.\n\n```text\n(function LowerBound (Math) i64 :merge (max old new))\n```\n\nSpecifically, a custom function can also have an EqSort output type:\n\n```text\n(function Add (i64 i64) Math)\n```\n\nAll functions can be `set`\nwith [`Action::Set`].\n\nOutput of a function, if being the EqSort type, can be unioned with [`Action::Union`]\nwith another datatype of the same `sort`.", | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "name": { | |
| "type": "string" | |
| }, | |
| "schema": { | |
| "$ref": "#/$defs/Schema" | |
| }, | |
| "merge": { | |
| "anyOf": [ | |
| { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| { | |
| "type": "null" | |
| } | |
| ] | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Function" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "span", | |
| "name", | |
| "schema" | |
| ] | |
| }, | |
| "AddRuleset": { | |
| "description": "Using the `ruleset` command, defines a new\nruleset that can be added to in [`Command::Rule`]s.\nRulesets are used to group rules together\nso that they can be run together in a [`Schedule`].\n\nExample:\nRuleset allows users to define a ruleset- a set of rules\n\n```text\n(ruleset myrules)\n(rule ((edge x y))\n ((path x y))\n :ruleset myrules)\n(run myrules 2)\n```", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "AddRuleset" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "UnstableCombinedRuleset": { | |
| "description": "Using the `combined-ruleset` command, construct another ruleset\nwhich runs all the rules in the given rulesets.\nThis is useful for running multiple rulesets together.\nThe combined ruleset also inherits any rules added to the individual rulesets\nafter the combined ruleset is declared.\n\nExample:\n```text\n(ruleset myrules1)\n(rule ((edge x y))\n ((path x y))\n :ruleset myrules1)\n(ruleset myrules2)\n(rule ((path x y) (edge y z))\n ((path x z))\n :ruleset myrules2)\n(combined-ruleset myrules-combined myrules1 myrules2)\n```", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "field3": { | |
| "type": "array", | |
| "items": { | |
| "type": "string" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "UnstableCombinedRuleset" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3" | |
| ] | |
| }, | |
| "Rule": { | |
| "description": "```text\n(rule <body:List<Fact>> <head:List<Action>>)\n```\n\ndefines an egglog rule.\nThe rule matches a list of facts with respect to\nthe global database, and runs the list of actions\nfor each match.\nThe matches are done *modulo equality*, meaning\nequal datatypes in the database are considered\nequal.\n\nExample:\n```text\n(rule ((edge x y))\n ((path x y)))\n\n(rule ((path x y) (edge y z))\n ((path x z)))\n```", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/GenericRule" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Rule" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1" | |
| ] | |
| }, | |
| "GenericRule": { | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "head": { | |
| "$ref": "#/$defs/GenericActions" | |
| }, | |
| "body": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericFact" | |
| } | |
| }, | |
| "name": { | |
| "description": "A globally unique name for this rule in the EGraph.", | |
| "type": "string" | |
| }, | |
| "ruleset": { | |
| "description": "The ruleset this rule belongs to. Defaults to `\"\"`.", | |
| "type": "string" | |
| } | |
| }, | |
| "required": [ | |
| "span", | |
| "head", | |
| "body", | |
| "name", | |
| "ruleset" | |
| ] | |
| }, | |
| "GenericActions": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericAction" | |
| } | |
| }, | |
| "GenericAction": { | |
| "oneOf": [ | |
| { | |
| "$ref": "#/$defs/Let" | |
| }, | |
| { | |
| "$ref": "#/$defs/Set" | |
| }, | |
| { | |
| "$ref": "#/$defs/Change" | |
| }, | |
| { | |
| "$ref": "#/$defs/Union" | |
| }, | |
| { | |
| "$ref": "#/$defs/Panic2" | |
| }, | |
| { | |
| "$ref": "#/$defs/Expr" | |
| } | |
| ] | |
| }, | |
| "Let": { | |
| "description": "Bind a variable to a particular datatype or primitive.\nAt the top level (in a [`Command::Action`]), this defines a global variable.\nIn a [`Command::Rule`], this defines a local variable in the actions.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "field3": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Let" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3" | |
| ] | |
| }, | |
| "Set": { | |
| "description": "`set` a function to a particular result.\n`set` should not be used on datatypes-\ninstead, use `union`.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "field3": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericExpr" | |
| } | |
| }, | |
| "field4": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Set" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3", | |
| "field4" | |
| ] | |
| }, | |
| "Change": { | |
| "description": "Delete or subsume (mark as hidden from future rewrites and unextractable) an entry from a function.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/Change2" | |
| }, | |
| "field3": { | |
| "type": "string" | |
| }, | |
| "field4": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericExpr" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Change" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3", | |
| "field4" | |
| ] | |
| }, | |
| "Change2": { | |
| "description": "Change a function entry.", | |
| "anyOf": [ | |
| { | |
| "description": "`delete` this entry from a function.\nBe wary! Only delete entries that are guaranteed to be not useful.", | |
| "type": "null" | |
| }, | |
| { | |
| "description": "`subsume` this entry so that it cannot be queried or extracted, but still can be checked.\nNote that this is currently forbidden for functions with custom merges.", | |
| "type": "null" | |
| } | |
| ] | |
| }, | |
| "Union": { | |
| "description": "`union` two datatypes, making them equal\nin the implicit, global equality relation\nof egglog.\nAll rules match modulo this equality relation.\n\nExample:\n```text\n(datatype Math (Num i64))\n(union (Num 1) (Num 2)); Define that Num 1 and Num 2 are equivalent\n(extract (Num 1)); Extracts Num 1\n(extract (Num 2)); Extracts Num 1\n```", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "field3": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Union" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3" | |
| ] | |
| }, | |
| "Panic2": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Panic" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "Expr": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Expr" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "GenericFact": { | |
| "description": "Facts are the left-hand side of a [`Command::Rule`].\nThey represent a part of a database query.\nFacts can be expressions or equality constraints between expressions.\n\nNote that primitives such as `!=` are partial.\nWhen two things are equal, it returns nothing and the query does not match.\nFor example, the following egglog code runs:\n```text\n(fail (check (!= 1 1)))\n```", | |
| "oneOf": [ | |
| { | |
| "$ref": "#/$defs/Eq" | |
| }, | |
| { | |
| "$ref": "#/$defs/Fact" | |
| } | |
| ] | |
| }, | |
| "Eq": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "field3": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Eq" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3" | |
| ] | |
| }, | |
| "Fact": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Fact" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1" | |
| ] | |
| }, | |
| "Rewrite": { | |
| "description": "`rewrite` is syntactic sugar for a specific form of `rule`\nwhich simply unions the left and right hand sides.\n\nExample:\n```text\n(rewrite (Add a b)\n (Add b a))\n```\n\nDesugars to:\n```text\n(rule ((= lhs (Add a b)))\n ((union lhs (Add b a))))\n```\n\nAdditionally, additional facts can be specified\nusing a `:when` clause.\nFor example, the same rule can be run only\nwhen `a` is zero:\n\n```text\n(rewrite (Add a b)\n (Add b a)\n :when ((= a (Num 0)))\n```\n\nAdd the `:subsume` flag to cause the left hand side to be subsumed after matching, which means it can\nno longer be matched in a rule, but can still be checked against (See [`Change`] for more details.)\n\n```text\n(rewrite (Mul a 2) (bitshift-left a 1) :subsume)\n```\n\nDesugars to:\n```text\n(rule ((= lhs (Mul a 2)))\n ((union lhs (bitshift-left a 1))\n (subsume (Mul a 2))))\n```", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "type": "string" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/GenericRewrite" | |
| }, | |
| "field3": { | |
| "type": "boolean" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Rewrite" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3" | |
| ] | |
| }, | |
| "GenericRewrite": { | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "lhs": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "rhs": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "conditions": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericFact" | |
| } | |
| } | |
| }, | |
| "required": [ | |
| "span", | |
| "lhs", | |
| "rhs", | |
| "conditions" | |
| ] | |
| }, | |
| "BiRewrite": { | |
| "description": "Similar to [`Command::Rewrite`], but\ngenerates two rules, one for each direction.\n\nExample:\n```text\n(bi-rewrite (Mul (Var x) (Num 0))\n (Var x))\n```\n\nBecomes:\n```text\n(rule ((= lhs (Mul (Var x) (Num 0))))\n ((union lhs (Var x))))\n(rule ((= lhs (Var x)))\n ((union lhs (Mul (Var x) (Num 0)))))\n```", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "type": "string" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/GenericRewrite" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "BiRewrite" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "Action": { | |
| "description": "Perform an [`Action`] on the global database\n(see documentation for [`Action`] for more details).\nExample:\n```text\n(let xplusone (Add (Var \"x\") (Num 1)))\n```", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/GenericAction" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Action" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1" | |
| ] | |
| }, | |
| "Extract": { | |
| "description": "`extract` a datatype from the egraph, choosing\nthe smallest representative.\nBy default, each constructor costs 1 to extract\n(common subexpressions are not shared in the cost\nmodel).", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "field3": { | |
| "$ref": "#/$defs/GenericExpr" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Extract" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3" | |
| ] | |
| }, | |
| "RunSchedule": { | |
| "description": "Runs a [`Schedule`], which specifies\nrulesets and the number of times to run them.\n\nExample:\n```text\n(run-schedule\n (saturate my-ruleset-1)\n (run my-ruleset-2 4))\n```\n\nRuns `my-ruleset-1` until saturation,\nthen runs `my-ruleset-2` four times.\n\nSee [`Schedule`] for more details.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/GenericSchedule" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "RunSchedule" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1" | |
| ] | |
| }, | |
| "GenericSchedule": { | |
| "oneOf": [ | |
| { | |
| "$ref": "#/$defs/Saturate" | |
| }, | |
| { | |
| "$ref": "#/$defs/Repeat" | |
| }, | |
| { | |
| "$ref": "#/$defs/Run" | |
| }, | |
| { | |
| "$ref": "#/$defs/Sequence" | |
| } | |
| ] | |
| }, | |
| "Saturate": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/GenericSchedule" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Saturate" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "Repeat": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "integer", | |
| "format": "uint", | |
| "minimum": 0 | |
| }, | |
| "field3": { | |
| "$ref": "#/$defs/GenericSchedule" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Repeat" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3" | |
| ] | |
| }, | |
| "Run": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/GenericRunConfig" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Run" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "GenericRunConfig": { | |
| "type": "object", | |
| "properties": { | |
| "ruleset": { | |
| "type": "string" | |
| }, | |
| "until": { | |
| "type": [ | |
| "array", | |
| "null" | |
| ], | |
| "items": { | |
| "$ref": "#/$defs/GenericFact" | |
| } | |
| } | |
| }, | |
| "required": [ | |
| "ruleset" | |
| ] | |
| }, | |
| "Sequence": { | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericSchedule" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Sequence" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "PrintOverallStatistics": { | |
| "description": "Print runtime statistics about rules\nand rulesets so far.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": [ | |
| "string", | |
| "null" | |
| ] | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "PrintOverallStatistics" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1" | |
| ] | |
| }, | |
| "Check": { | |
| "description": "The `check` command checks that the given facts\nmatch at least once in the current database.\nThe list of facts is matched in the same way a [`Command::Rule`] is matched.\n\nExample:\n\n```text\n(check (= (+ 1 2) 3))\n(check (<= 0 3) (>= 3 0))\n(fail (check (= 1 2)))\n```\n\nprints\n\n```text\n[INFO ] Checked.\n[INFO ] Checked.\n[ERROR] Check failed\n[INFO ] Command failed as expected.\n```", | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "facts": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericFact" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Check" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "span", | |
| "facts" | |
| ] | |
| }, | |
| "PrintFunction": { | |
| "description": "Print out rows of a given function, extracting each of the elements of the function.\nExample:\n\n```text\n(print-function Add 20)\n```\nprints the first 20 rows of the `Add` function.\n\n```text\n(print-function Add)\n```\nprints all rows of the `Add` function.\n\n```text\n(print-function Add :file \"add.csv\")\n```\nprints all rows of the `Add` function to a CSV file.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "field3": { | |
| "type": [ | |
| "integer", | |
| "null" | |
| ], | |
| "format": "uint", | |
| "minimum": 0 | |
| }, | |
| "field4": { | |
| "type": [ | |
| "string", | |
| "null" | |
| ] | |
| }, | |
| "field5": { | |
| "$ref": "#/$defs/PrintFunctionMode" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "PrintFunction" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field5" | |
| ] | |
| }, | |
| "PrintFunctionMode": { | |
| "description": "The mode of printing a function. The default mode prints the function in a user-friendly way and\nhas an unreliable interface.\nThe CSV mode prints the function in the CSV format.", | |
| "type": "string", | |
| "enum": [ | |
| "Default", | |
| "CSV" | |
| ] | |
| }, | |
| "PrintSize": { | |
| "description": "Print out the number of rows in a function or all functions.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": [ | |
| "string", | |
| "null" | |
| ] | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "PrintSize" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1" | |
| ] | |
| }, | |
| "Input": { | |
| "description": "Input a CSV file directly into a function.", | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "name": { | |
| "type": "string" | |
| }, | |
| "file": { | |
| "type": "string" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Input" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "span", | |
| "name", | |
| "file" | |
| ] | |
| }, | |
| "Output": { | |
| "description": "Extract and output a set of expressions to a file.", | |
| "type": "object", | |
| "properties": { | |
| "span": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "file": { | |
| "type": "string" | |
| }, | |
| "exprs": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericExpr" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Output" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "span", | |
| "file", | |
| "exprs" | |
| ] | |
| }, | |
| "Push": { | |
| "description": "`push` the current egraph `n` times so that it is saved.\nLater, the current database and rules can be restored using `pop`.", | |
| "type": "object", | |
| "properties": { | |
| "n": { | |
| "type": "integer", | |
| "format": "uint", | |
| "minimum": 0 | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Push" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "n" | |
| ] | |
| }, | |
| "Pop": { | |
| "description": "`pop` the current egraph, restoring the previous one.\nThe argument specifies how many egraphs to pop.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "integer", | |
| "format": "uint", | |
| "minimum": 0 | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Pop" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "Fail": { | |
| "description": "Assert that a command fails with an error.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "$ref": "#/$defs/GenericCommand" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Fail" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "Include": { | |
| "description": "Include another egglog file directly as text and run it.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "Include" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2" | |
| ] | |
| }, | |
| "UserDefined": { | |
| "description": "User-defined command.", | |
| "type": "object", | |
| "properties": { | |
| "field1": { | |
| "$ref": "#/$defs/Span" | |
| }, | |
| "field2": { | |
| "type": "string" | |
| }, | |
| "field3": { | |
| "type": "array", | |
| "items": { | |
| "$ref": "#/$defs/GenericExpr" | |
| } | |
| }, | |
| "type": { | |
| "type": "string", | |
| "const": "UserDefined" | |
| } | |
| }, | |
| "required": [ | |
| "type", | |
| "field1", | |
| "field2", | |
| "field3" | |
| ] | |
| } | |
| } | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment