#category-theory #encoding #语法树 #gadt #ast #strict-encoding #内存布局

bin+lib strict_types

严格类型:受限制的泛化代数数据类型(GADT)

25 个版本 (13 个稳定版)

2.7.0-rc.12024 年 8 月 14 日
2.7.0-beta.42024 年 5 月 24 日
2.7.0-beta.32024 年 4 月 18 日
2.7.0-beta.22024 年 3 月 12 日
1.0.0-rc.12023 年 3 月 28 日

#105 in 解析器实现

Download history 422/week @ 2024-05-01 112/week @ 2024-05-08 138/week @ 2024-05-15 752/week @ 2024-05-22 308/week @ 2024-05-29 831/week @ 2024-06-05 734/week @ 2024-06-12 592/week @ 2024-06-19 1016/week @ 2024-06-26 709/week @ 2024-07-03 1406/week @ 2024-07-10 680/week @ 2024-07-17 1310/week @ 2024-07-24 1028/week @ 2024-07-31 879/week @ 2024-08-07 2085/week @ 2024-08-14

每月下载量 5,386
用于 25 个crate(14 个直接使用)

Apache-2.0

270KB
6K SLoC

严格类型 AST 和 typelib 实现

Build Tests Lints codecov

crates.io Docs unsafe forbidden Apache-2 licensed

功能编程的 Protobufs

这是一套用于处理抽象语法树和严格类型库(type system made with category theory which ensures provable properties and bounds for the in-memory and serialized type representation)的库。

严格类型是一种用于以确定性和受限制的方式定义和序列化广义代数数据类型(GADT)的正式符号。它是在类型理论的基础上开发的。

严格类型是

  • 基于模式的(模式是严格编码表示),
  • 语义的,即定义类型不仅基于其在内存中的布局,而且基于其含义,
  • 确定的,即对于给定的类型产生相同的结果,
  • 可移植的,即可以在任何硬件架构和操作系统上运行,包括低性能的嵌入式系统,
  • 受限制的,即提供有关类型数据最大大小的保证和静态分析,
  • 形式可验证的.

要了解更多关于严格编码的信息,请阅读规范

严格类型与类型定义一起工作。它允许

  • 对数据类型进行静态分析,例如
    • 定义语义类型 ID;
    • 指定精确的内存布局;
    • 基于语义和内存布局的类型等价;
    • 序列化数据的尺寸
  • 将类型组合到类型库中;
  • 基于语义类型对类型库进行版本控制;

该库允许从实现 StrictEncoding 特性的 Rust 类型生成和编译严格类型库(STL),并确保使用 StrictDecode 进行反序列化时遵循相同的内存和语义布局。

严格类型库

该库能够自我反射,在严格类型系统中生成其锈数据类型的副本。

严格类型库ID:stl:9KALDYR8Nyjq4FdMW6kYoL7vdkWnqPqNuFnmE9qHpNjZ#lagoon-rodent-option

通过在文件头部添加以下代码导入此库:import lagoon_rodent_option_9KALDYR8Nyjq4FdMW6kYoL7vdkWnqPqNuFnmE9qHpNjZ as StrictTypes

源代码可以在[stl/StrictTypes.sty]文件中找到。

贡献

CONTRIBUTING.md

许可证

该库在Apache 2.0许可证的条款下分发。

依赖项

~4–5MB
~107K SLoC