FormCore.js 移植到 Dart。

到目前为止，只有解析器和类型检查器被
移植，即原始存储库中的 FormCore.js 文件。
存储库。

(来自 https://github.com/moonad/FormCoreJS 的原始自述文件)

FormCoreJS

一个纯 JavaScript、无依赖、700 行代码实现的 FormCore，这是一个最小化的证明语言，具有归纳推理功能。它是 Kind 的核心。它可以编译为超快的 JavaScript 和 Haskell。其他后端即将推出。

用法

使用 npm i -g formcore-js 进行安装。输入 fmc -h 查看可用命令。

• fmc file.fmc：检查 file.fmc 中的所有类型

• fmc file.fmc --js main：将 file.fmc 中的 main 编译为 JavaScript

作为库

var {fmc} = require("formcore-js");
fmc.report(`
  id : @(A: *) @(x: A) A = #A #x x;
`);

什么是 FormCore？

FormCore 是一种基于自依赖类型的最小化的纯函数式语言。
本质上，它是能够通过
归纳推理进行定理证明的最简单的语言。它的语法很简单

它主要有两个用途：

一个最小化的、可审计的证明内核

证明助手用于验证软件的正确性，但谁来验证
验证器呢？使用 FormCore，像 Kind 这样的复杂语言中的证明
可以编译为最小化的核心并再次检查，以防止证明语言本身中的错误。
至于 FormCore 本身，由于它非常小，
可以由人工手动审计，从而结束这个循环。

函数式编译的中间格式

FormCore 可以用作一个通用的中间格式，其他函数式
语言可以将其作为目标，以便转译为其他语言。FormCore 的
纯洁性和丰富的类型信息允许从中恢复高效的程序。
目前，我们使用 FormCore 将 Kind
编译为 JavaScript，但也可以涉及其他源语言和目标语言。

JavaScript 编译器

此实现包含一个高质量的从 FormCore 到
JavaScript 的编译器。该编译器利用类型信息将高度函数式的
代码转换为高效的 JavaScript。例如，编译器将这些
λ 编码转换为原生表示：

此外，它还将任何合适的自定义的自编码数据类型
转换为原生对象树，使用 switch 进行模式匹配。它还将
已知函数如 Nat.mul 替换为原生 *，String.concat 替换为原生 + 等。
它还执行尾调用优化并内联某些函数，
例如将 List.for 转换为内联循环。生成的 JS
在大多数情况下应与手写代码一样快。

示例

该程序使用自依赖数据类型来实现布尔值、命题
等价性、布尔否定函数，并证明双重否定是
恒等式（∀ (b: Bool) -> not(not(b)) == b）

Bool : * =
  %self(P: @(self: Bool) *)
  @(true: (P true))
  @(false: (P false))
  (P self);

true : Bool =
  #P #t #f t;

false : Bool =
  #P #t #f f;

not : @(x: Bool) Bool =
  #x (((x #self Bool) false) true);

Equal : @(A: *) @(a: A) @(b: A) * =
  #A #a #b
  %self(P: @(b: A) @(self: (((Equal A) a) b)) *)
  @(refl: ((P a) ((refl A) a)))
  ((P b) self);

refl : %(A: *) %(a: A) (((Equal A) a) a) =
  #A #x #P #refl refl;

double_negation_theorem : @(b: Bool) (((Equal Bool) (not (not b))) b) =
  #b (((b #self (((Equal Bool) (not (not self))) self))
    ((refl Bool) true))
    ((refl Bool) false));

main : Bool =
  (not false);

它等同于这个 Kind
代码片段

// The boolean type
type Bool {
  true,
  false,
}

// Propositional equality
type Equal <A: Type> (a: A) ~ (b: A) {
  refl ~ (b: a)
}

// Boolean negation
not(b: Bool): Bool
  case b {
    true: false,
    false: true,
  }

// Proof that double negation is identity
theorem(b: Bool): Equal(Bool, not(not(b)), b)
  case b {
    true: refl
    false: refl
  }!

GitHub 链接

https://github.com/modulovalue/FormCore.dart