「SF-LC」15 Extraction

Logical Foundations - Extracting ML From Coq

Posted by Hux on January 15, 2019

Basic Extraction

• OCaml (most mature)
• 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.


Controlling Extraction of Specific Types

We can tell Coq how to extract certain Inductive definitions to specific OCaml types. we must say:

1. how the Coq type itself should be represented in OCaml
2. 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 ⇒ "( - )".


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


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]


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


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 *)