- OCaml (most mature)
- Haskell (mostly works)
- Scheme (a bit out of date)
1
| Extraction "imp1.ml" ceval_step.
|
When Coq processes this command:
1
2
| The file imp1.ml has been created by extraction.
The file imp1.mli has been created by extraction.
|
如果不做任何处理的话…生成的 ml 里的 nat 则都会是 Church Numeral…
We can tell Coq how to extract certain Inductive definitions to specific OCaml types.
we must say:
- how the Coq type itself should be represented in OCaml
- how each constructor should be translated
1
| Extract Inductive bool ⇒ "bool" [ "true" "false" ].
|
also, for non-enumeration types (where the constructors take arguments),
we give an OCaml expression that can be used as a “recursor” over elements of the type. (Think Church numerals.)
1
2
3
4
| Extract Inductive nat ⇒ "int"
[ "0" "(fun x → x + 1)" ]
"(fun zero succ n →
if n=0 then zero () else succ (n-1))".
|
1
2
3
| Extract Constant plus ⇒ "( + )".
Extract Constant mult ⇒ "( * )".
Extract Constant eqb ⇒ "( = )".
|
注意：保证提取结果的合理性是你的责任。
1
| Extract Constant minus ⇒ "( - )".
|
比如这么做很诱人……但是我们 Coq 的定义里 0 - 1 = 0, OCaml 的 int 则会有负数…
Recursor 的理论与实现 - a “encoding” of case expression and sum type
1
2
3
4
5
6
| Fixpoint ceval_step (st : state) (c : com) (i : nat)
: option state :=
match i with
| O => None
| S i' =>
match c with
|
1
2
3
4
| let rec ceval_step st c = function
| O -> None
| S i' ->
(match c with
|
1
2
3
4
5
| let rec ceval_step st c i =
(fun zero succ n -> if n=0 then zero () else succ (n-1))
(fun _ -> None) (* zero *)
(fun i' -> (* succ *)
match c with
|
注意我们是如何使用 “recursor” 来替代 case, match, pattern matching 得。
recall sum type 在 PLT 中的语法与语义：
1
2
3
4
5
6
7
8
| T ::=
T + T
e ::=
case e of
| L(e) => e
| R(e) => e
|
1
2
3
4
5
6
7
8
9
10
11
12
13
| e → e'
------------- (work inside constructor)
C(e) -> C(e')
e → e'
------------------------------- (work on the expr match against)
case e of ... → case e' of ...
----------------------------------------------- (match Left constructor, substitute)
case L(v) of L(x) => e1 | R(y) => e2 → e1 [v/x]
----------------------------------------------- (match Right constructor, substitute)
case R(v) of L(x) => e1 | R(y) => e2 → e1 [v/x]
|
可以发现 case 表达式可以理解为一种特殊的 application，会将其 argument 根据某种 tag （这里为构造函数） apply 到对应的 case body 上，
每个 case body 都是和 lambda abstraction 同构的一种 binder：
1
2
3
4
| L(x) => e1 === λx.e1
R(x) => e2 === λx.e2
case v e1|e2 === (λx.e1|e2) v -- `e1` or `e2` depends on the _tag_ wrapped on `v`
|
这个角度也解释了 Haskell/SML 在申明函数时直接对参数写 pattern match 的理论合理性.
根据经验几乎所有的 binding 都可以被 desugar 成函数（即 lambda expression).
难点在于我们如何 re-implement 这个 tag 的 switch 机制?
对于 Inductive nat 翻译到 OCaml int 时，这个机制可以用 v =? 0 来判断，因此我们的 recursor 实现为
1
2
3
4
| fun zero succ (* partial application *)
n -> if n=0 (* 判断 tag ... *)
then zero () (* 0 case => (λx.e1) v *)
else succ (n-1) (* S n case => (λx.e2) v *)
|
