module-lib
模块分析:lib
1. 角色定位
lib/ 提供通用数据结构、Coq/OCaml
互操作辅助与解析工具,是全仓库的基础依赖。
2. 关键组件
- 数学与整数:
Integers.v,Zbits.v,IEEE754_extra.v - 集合/映射:
Maps.v,FSetAVLplus.v,Ordered.v,UnionFind.v - 图与遍历:
Postorder.v,Iteration.v,Wfsimpl.v - 区间/格:
Intv.v,IntvSets.v,Lattice.v - Coq 兼容与抽取:
Coqlib.v,Camlcoq.ml
3. OCaml 侧工具
Commandline.ml: 命令行解析与选项定义(driver 等使用)Printlines.ml: 行号与输出格式Readconfig.mll,Tokenize.mll,Responsefile.mll: 基础解析/配置读取工具
4. 特点
- 多数为纯函数式结构,作为证明与抽取的基础
- OCaml 文件用于运行时解析、命令行和配置读取,不参与核心证明