🥮 mooncakes.io

moondatalog

A pure MoonBit Datalog query engine with stratified negation, aggregation, static checks and moon prove formal verification.

datalog
query-engine
logic-programming
database
graph
formal-verification
moon add haol-05/moondatalog@0.1.1
Download zip
Author
Version
0.1.1
License
Apache-2.0
Repository
Last updated
20 hours ago
Downloads
4

Dependencies

README

#MoonDatalog

一个用纯 MoonBit 实现的 Datalog 查询引擎，带 形式化验证 与完整工程化交付。

Datalog 是一种声明式逻辑查询语言，广泛应用于图分析、静态分析、数据血缘追踪与配置校验等场景。本项目实现了一个边界清晰、可嵌入、经过机器校验 的 Datalog 引擎，包含：

  • 事实 / 规则 / 查询：p(...).、h(...) :- b1, b2.、?- ...
  • 递归：bottom-up 半朴素（semi-naive） 求值
  • 算术与比较：+ - * / %、= != < <= > >=（整数与浮点）
  • 分层否定：not p(...)，Tarjan SCC 自动分层
  • 聚合：Soufflé 风格 count / sum / min / max / avg
  • 静态检查：未定义谓词、元数不一致、不安全规则等在求值前报错
  • 形式化验证：核心纯函数经 moon prove 机器校验
  • 工程化交付：发布到 mooncakes.io，含 CI、50+ 测试、CLI 与示例

#快速开始

moon test           # 运行 50 个测试
moon prove verified # 形式化验证（需 Z3 等 SMT 求解器）

运行示例：

moon run cmd/main -- examples/ancestor.dl
moon run cmd/main -- examples/graph_reachability.dl
moon run cmd/main -- examples/aggregation.dl

Windows 提示：moon prove 前请将 TMP/TEMP 指向不含非 ASCII 字符的目录（如 C:\Temp）。

#作为库使用

import {
  "haol-05/moondatalog",
}

let src = "edge(a, b). edge(b, c).\npath(X, Y) :- edge(X, Y).\npath(X, Z) :- path(X, Y), edge(Y, Z).\n?- path(a, X).\n"

match @moondatalog.parse(src) {
  Err(e) => println(e.to_string())
  Ok(program) => match @moondatalog.evaluate(program) {
    Err(e) => println(e.to_string())
    Ok(result) => {
      for t in result.answers[0] {
        println(t.to_string()) // (b)\n(c)
      }
    }
  }
}

#语言语法

parent(alice, bob).
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Z) :- ancestor(X, Y), parent(Y, Z).
safe(X) :- node(X), not danger(X), X != secret.
dept_size(D, N) :- employee(X, D), N = count : { X }.
?- ancestor(X, carol).

变量以大写字母开头，_ 为匿名变量；小写标识符为符号常量；字符串用双引号；匿名变量不作为聚合分组键。

#形式化验证

verified/ 子包通过 moon prove 对核心纯函数机器校验：

函数契约
clamp(x, lo, hi)返回值在 [lo, hi] 内
bounded_sum(xs, lo, hi)总和在 [lo*len, hi*len] 内
index_of_max(xs)返回全局最大值的下标

#许可证

Apache-2.0

#
AggFunc

source
pub enum AggFunc {
  Count
  Sum
  Min
  Max
  Avg
} derive(Eq, 
Debug)

聚合函数。

#
Aggregate

source
pub struct Aggregate {
  agg_var : String
  func : AggFunc
  agg_vars : Array[String]
  pos : Pos
} derive(Eq, 
Debug)

聚合项：agg_var = func : { agg_vars... }。

语义与 Soufflé 一致：以规则体中其余变量为分组键， 组内对 agg_vars 对应的取值集合计算聚合函数，结果绑定到 agg_var。

#
Atom

source
pub struct Atom {
  pred : String
  args : Array[Term]
  pos : Pos
} derive(Eq, 
Debug)

谓词原子 pred(t1, ..., tn)。

#
BinOp

source
pub enum BinOp {
  Add
  Sub
  Mul
  Div
  Mod
} derive(Eq, 
Debug)

算术二元运算符。

#
BodyItem

source
pub enum BodyItem {
  Pos(Atom)
  Neg(Atom)
  Cmp(Cmp)
  Agg(Aggregate)
} derive(Eq, 
Debug)

规则体中的一项。

#
Cmp

source
pub struct Cmp {
  op : CmpOp
  lhs : Term
  rhs : Term
  pos : Pos
} derive(Eq, 
Debug)

比较 / 赋值约束。

#
CmpOp

source
pub enum CmpOp {
  Eq
  Ne
  Lt
  Le
  Gt
  Ge
} derive(Eq, 
Debug)

比较 / 赋值运算符。

#
DlError

source
pub enum DlError {
  LexError(Pos, String)
  ParseError(Pos, String)
  SemanticError(String)
  EvalError(String)
} derive(Eq, 
Debug)

引擎错误。

#
DlError::to_string

source
fn DlError::to_string(self : DlError) -> String

#
EvalResult

source
pub struct EvalResult {
  relations : 
HashMap[String, Relation]
  answers : Array[Array[Tuple]]
}

求值结果：最终关系集合与各查询答案。

#
Pos

source
pub struct Pos {
  line : Int
  col : Int
} derive(Eq, 
Debug)

源码位置（行 / 列，均从 1 起）。
impl Show for Pos

#
Program

source
pub struct Program {
  rules : Array[Rule]
  queries : Array[Query]
} derive(Eq, 
Debug)

完整程序：规则（含事实）与查询。

#
Query

source
pub struct Query {
  body : Array[BodyItem]
  pos : Pos
} derive(Eq, 
Debug)

一个查询：?- body.

#
Relation

source

一个关系（谓词实例）：同元数元组的集合，并维护按首参数的值索引。

#
Relation::arity

source
fn Relation::arity(self : Relation) -> Int

#
Relation::clear

source
fn Relation::clear(self : Relation) -> Unit

移除全部元组（用于分层求值前的重置）。

#
Relation::contains

source
fn Relation::contains(self : Relation, t : Tuple) -> Bool

元组是否已存在。

#
Relation::insert

source
fn Relation::insert(self : Relation, t : Tuple) -> Bool

插入一个元组；若已存在返回 false。

#
Relation::insert_all

source
fn Relation::insert_all(self : Relation, ts : Iter[Tuple]) -> Int

批量插入并返回新增数量。

#
Relation::iter

source
fn Relation::iter(self : Relation) -> Iter[Tuple]

遍历全部元组。

#
Relation::length

source
fn Relation::length(self : Relation) -> Int

#
Relation::lookup0

source
fn Relation::lookup0(self : Relation, v : Value) -> Iter[Tuple]

按首参数精确查找（利用首参数索引）。

#
Relation::to_string

source
fn Relation::to_string(self : Relation) -> String

以确定顺序输出所有元组（字典序）。

#
Rule

source
pub struct Rule {
  head : Atom
  body : Array[BodyItem]
  pos : Pos
} derive(Eq, 
Debug)

一条规则：head :- body.（事实为 body 为空）。

#
Term

source
pub enum Term {
  Const(Value)
  Var(String)
  Neg(Term)
  Arith(BinOp, Term, Term)
} derive(Eq, 
Debug)

项（原子参数）：常量、变量、一元负号或算术表达式。

#
TokKind

source
pub enum TokKind {
  Ident(String)
  IntLit(String)
  FloatLit(String)
  StrLit(String)
  LParen
  RParen
  Comma
  Dot
  Colon
  LBrace
  RBrace
  ColonDash
  QuestionDash
  Not
  Eq
  Ne
  Lt
  Le
  Gt
  Ge
  Plus
  Minus
  Star
  Slash
  Percent
  Eof
} derive(Eq, 
Debug)

记号类别。

#
TokKind::describe

source
fn TokKind::describe(self : TokKind) -> String

记号类别的简短描述（用于错误信息）。

#
Token

source
pub struct Token {
  kind : TokKind
  pos : Pos
} derive(Eq, 
Debug)

一个带位置的记号。

#
Tokens

source
pub struct Tokens {
  items : Array[Token]
}

记号流。

#
Tokens::get

source
fn Tokens::get(self : Tokens, i : Int) -> Token

#
Tokens::length

source
fn Tokens::length(self : Tokens) -> Int

#
Tuple

source
pub struct Tuple {
  elems : Array[Value]
}

一个关系元组：有序的值数组。

自定义 Eq / Hash / Compare，使元组可作为哈希集合的元素， 并按字典序可比，从而支持去重与排序输出。
impl Compare for Tuple
impl Eq for Tuple
impl Hash for Tuple

#
Tuple::get

source
fn Tuple::get(self : Tuple, i : Int) -> Value

#
Tuple::length

source
fn Tuple::length(self : Tuple) -> Int

#
Tuple::to_string

source
fn Tuple::to_string(self : Tuple) -> String

以 (a, b, c) 形式输出。

#
Value

source
pub enum Value {
  Sym(String)
  Str(String)
  Int(Int64)
  Float(Double)
} derive(Compare, Eq, Hash, 
Debug)

一个 Datalog 数据值。

四种构造子按全序排列：符号常量 < 字符串 < 整数 < 浮点数。 该顺序保证元组与关系具备确定的字典序，便于排序与去重。
impl Show for Value

#
compare_values

source
fn compare_values(a : Value, b : Value) -> Int

值的确定化全序比较：
  • 同类数值按数值比较（Int/Float 混合按浮点）；
  • 符号 / 字符串按字典序（lexical_compare，注意非 String::compare）；
  • 跨类别按 符号 < 字符串 < 整数 < 浮点 的固定序。

#
evaluate

source
fn evaluate(program : Program) -> Result[EvalResult, DlError]

运行完整求值：语义检查 -> 初始化 -> 分层求值 -> 回答查询。

#
float_const

source
fn float_const(f : Double) -> Value

构造浮点常量。

#
from_literal

source
fn from_literal(s : String) -> Value

将任意字面量文本（数字或标识符）规约为 Value： 可解析为整数则取整数，否则可解析为浮点则取浮点，否则视为符号常量。

#
int_const

source
fn int_const(i : Int64) -> Value

构造整数常量。

#
is_variable_name

source
fn is_variable_name(s : String) -> Bool

是否为变量名：_ 或大写字母开头的标识符。

#
lex

source
fn lex(src : String) -> Result[Tokens, DlError]

词法分析：将源码切分为记号。失败时返回带位置的词法错误。

#
make_tuple

source
fn make_tuple(values : Array[Value]) -> Tuple

#
new_relation

source
fn new_relation(arity : Int) -> Relation

#
parse

source
fn parse(src : String) -> Result[Program, DlError]

解析完整程序。

#
parse_float

source
fn parse_float(s : String) -> Value?

解析一个十进制浮点字面量（可为负、可含指数）。失败返回 None。

#
parse_int

source
fn parse_int(s : String) -> Value?

解析一个十进制整数字面量（可为负）。失败返回 None。

#
relation_names

source
fn relation_names(result : EvalResult) -> Array[String]

获取所有关系的谓词名（排序后，便于 CLI 展示）。

#
render_agg

source
fn render_agg(agg : Aggregate) -> String

渲染一个聚合项。

#
render_atom

source
fn render_atom(a : Atom) -> String

渲染一个原子。

#
render_body_item

source
fn render_body_item(item : BodyItem) -> String

渲染一个规则体项。

#
render_cmp

source
fn render_cmp(c : Cmp) -> String

渲染一个比较约束。

#
render_query

source
fn render_query(q : Query) -> String

渲染一条查询为可读文本。

#
render_rule

source
fn render_rule(r : Rule) -> String

渲染一条规则（含事实）为可读文本。

#
render_term

source
fn render_term(t : Term) -> String

渲染一个项。

#
str_const

source
fn str_const(s : String) -> Value

构造字符串常量。

#
stratify

source
fn stratify(rules : Array[Rule]) -> Result[Array[Array[Rule]], DlError]

对规则集做分层。

返回按求值顺序排列的分层（每层为一组规则）；若程序不可分层 （否定依赖存在递归环），返回语义错误。

#
sym

source
fn sym(s : String) -> Value

构造符号常量（供外部使用，等价于公开枚举构造子）。

Source Files

Powered by MoonBit

Site sourceReport issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io