「SF-LC」15 Extraction

Basic Extraction

OCaml (most mature)
Haskell (mostly works)
Scheme (a bit out of date)

代码语言：javascript复制

Extraction "imp1.ml" ceval_step.

When Coq processes this command:

代码语言：javascript复制

The file imp1.ml has been created by extraction.
The file imp1.mli has been created by extraction.

Controlling Extraction of Specific Types

如果不做任何处理的话…生成的 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

代码语言：javascript复制

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

代码语言：javascript复制

Extract Inductive nat ⇒ "int"
  [ "0" "(fun x → x   1)" ]
  "(fun zero succ n →
      if n=0 then zero () else succ (n-1))".

代码语言：javascript复制

Extract Constant plus ⇒ "(   )".
Extract Constant mult ⇒ "( * )".
Extract Constant eqb ⇒ "( = )".

注意：保证提取结果的合理性是你的责任。

代码语言：javascript复制

Extract Constant minus ⇒ "( - )".

比如这么做很诱人……但是我们 Coq 的定义里 0 - 1 = 0, OCaml 的 int 则会有负数…

Recursor 的理论与实现 - a “encoding” of case expression and sum type

代码语言：javascript复制

Fixpoint ceval_step (st : state) (c : com) (i : nat)
                    : option state :=
  match i with
  | O => None
  | S i' =>
    match c with

代码语言：javascript复制

let rec ceval_step st c = function
  | O -> None
  | S i' ->
    (match c with

代码语言：javascript复制

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 中的语法与语义：

代码语言：javascript复制

T ::= 
  T   T

e ::=
  case e of
    | L(e) => e
    | R(e) => e

代码语言：javascript复制

                 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：

代码语言：javascript复制

 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 实现为

代码语言：javascript复制

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

express css nat haskell NAT网关

0 人点赞