Coq to C Translation with Partial Evaluation
Akira Tanaka
National Institute of Advanced Industrial Science and Technology (AIST)

2021-01-18 PEPM 2021 (online)Purpose

I Practical C code generation from Coq
I Program verification in Coq and efficient execution in C

2 / 51

Coq Proof Assistant

I It provides the pure functional ML-like language, Gallina
I We can verify various properties of functions written in Gallina
I It has the extraction plugin to generate OCaml code from
Gallina

3 / 51

Codegen Plugin for Coq

I We are developing a Coq plugin to translate a Gallina subset
to C
I It intends to generate low-level code generation unlike theextraction plugin
I https://github.com/akr/codegen
I Two-phase translation:
I Gallina to Gallina Transformation
This includes partial evaluation
This transformation is easily verifiable
I Gallina to C Translation
C code generation for monomorphic Gallina function

4 / 51

Basic Idea

Gallina and C (and most imperative languages) shares basic
features:
I function definition
I function invocation
I conditional
I variable declaration and its initialization
I variable reference
I recursive function
We can translate a Gallina subset to C without an overhead

5 / 51

Mandatory Features for Low-level Programming
Our initial motivation is succinct data structures
It needs low-level features:
I various C types: 64 bit integer, SIMD register, etc.
→ Gallina inductive types are mapped to C types
I operators (+, -, *, etc.) andbuiltin functions (__builtin_popcount, etc.)→ Gallina applications are mapped to C function calls:
f x in Gallina is translated to f (x) in C
f can be implemented as a macro or builtin function
I loop without stack consumption (but Gallina has no loops)→ We guarantee tail recursion elimination
These features enable us to generate low-level C functions frommonomorphic Gallina functions

6 / 51

Good-to-Have Features

Although we can implement monomorphic functions in Gallina but
automatic transformations reduce the programmer’s effort
I Monomorphization for polymorphic functions
I Dependent type elimination for complex type computation
I Partial evaluation generalizes them
We implement a partial evaluation as Gallina to Gallina
transformations

7 / 51

Contents
Background
Monomorphic Translation Example
Partial Evaluation with Stock Coq?
Translation of Codegen
Codegen Reduction Rules
Summary

8 / 51Power Function: Gallina to Gallina

Fixpoint pow (a b : nat) : nat :=match b with
| O ⇒ 1| S b’ ⇒ a * pow a b’end.

↓ application arguments into variables to ease code generation
Fixpoint s_pow (v1_a v2_b : nat) : nat :=match v2_b with
| O ⇒ let v3_n := O in
S v3_n| S v4_b_ ⇒ let v5_n := s_pow v1_a v4_b_ in
Nat.mul v1_a v5_nend

9 / 51Power Function: Gallina to C
Fixpoint s_pow (v1_a v2_b : nat) : nat :=match v2_b with
| O ⇒ let v3_n := O in S v3_n
| S v4_b_ ⇒ let v5_n := s_pow v1_a v4_b_ in
Nat.mul v1_a v5_n
end↓
static nat pow(nat v1_a, nat v2_b) {nat v3_n, v4_b_, v5_n;switch (sw_nat(v2_b)) {default:v3_n = O(); return S(v3_n);case S_tag: v4_b_ = pred(v2_b);v5_n = pow(v1_a, v4_b_);
return mul(v1_a, v5_n);}}
10 / 51

User-Defined nat Implementation in C
I We can choose any implementation for nat in C
I nat implementation using uint64_t#include <stdint.h>
typedef uint64_t nat;#define O() 0#define S(n) ((n)+1)#define sw_nat(n) ((n) == 0)#define S_tag 0#define pred(n) ((n)-1)#define mul(x,y) ((x) * (y))
I uint64_t for nat works if overflow does not occur
We provide monadification plugin for Coq for verification
about overflow
https://github.com/akr/monadification
11 / 51

Translation of Tail Recursion(* a^b * c *)Fixpoint powmul a b c :=match b with
| O ⇒ c| S b’ ⇒powmul a b’ (a * c)end.

static nat powmul(nat v1_a,nat v2_b, nat v3_c) {nat v4_b_, v5_n;
entry_powmul:
switch (sw_nat(v2_b)) {default: return v3_c;case S_tag:
Tail recursion elimination for loop
v4_b_ = pred(v2_b);
without stack consumption
v5_n = mul(v1_a, v3_c);v2_b = v4_b_;v3_c = v5_n;
goto entry_powmul;}}
12 / 51

Verification of Gallina to Gallina Transformation

We can verify s_pow easily in Coq:
Goal pow = s_pow.
Proof. reflexivity. Qed.

This guarantees pow and s_pow returns the same value for allarguments

13 / 51

Contents
Background
Monomorphic Translation Example
Partial Evaluation with Stock Coq?
Translation of Codegen
Codegen Reduction Rules
Summary

14 / 51

We Want Partial Evaluation

I Implementing monomorphic functions is a tiring task
I We want monomorphization for polymorphic functions
I Monomorphization can be considered as specialization withrespect to type arguments in Gallina(Type arguments are usual arguments since Gallina is adependently typed language)I Partial evaluation solves it (and more)

15 / 51

Partial Evaluation Example

pow(a, b) =

(
1

b=0

a ∗ pow(a, b − 1) b > 0

f(x) = . . . pow(x, 3) . . .
Specialization of pow with respect to b = 3
pow3(a) = pow(a, 3) = a ∗ a ∗ a ∗ 1
f(x) = . . . pow3(x) . . .
f(x) would run faster16 / 51

Coq has Partial Evaluation?
Fixpoint pow a b :=match b with
| O ⇒ 1| S b’ ⇒ a * pow a b’end.
Definition pow3 a :=Eval cbv beta iota delta [pow] in pow a 3.
(* Same as Definition pow3 a := a * (a * (a * 1)). *)I Definition c := Eval cbv beta iota delta [pow] in t.
defines c with t reduced with beta and iota reductions, anddelta (unfolding) pow using call-by-value (cbv) strategy.
I The reductions eliminate static computation (recursion andmatch-expression) well
I Problem 1: The reductions can duplicate computation
I Problem 2: No automatic mechanism to replace call sites
17 / 51

Problem 1: Computation Duplication
I The reductions may duplicate computation:
Definition pow_2x_3 x :=Eval cbv beta iota delta [pow] in pow (x + x) 3.
(* Same as Definition pow_2x_3 x :=(x + x) * ((x + x) * ((x + x) * 1)). *)The adding function is invoked only once in pow (x + x) 3
but 3 times in pow_2x_3 in the strict evaluation
I It’s because beta reduction ((λx : T . t) u . t{x/u}) can copy
the argument u of the application
I We don’t want to duplicate computation since it can makeprogram much slower(t{x/u} means a term in which x in term t is replaced by u. [Coq reference manual])

18 / 51

Problem 2: Call Site Replacement
I Coq has no feature to replace functions already definedFixpoint pow a b :=match b with
| O ⇒ 1| S b’ ⇒ a * pow a b’end.
Definition f x := ... pow x 3 ...
Definition pow3 a :=Eval cbv beta iota delta [pow] in pow a 3.

I We cannot redefine f in Coq
I The extraction plugin cannot generate the code of f to use
pow3

19 / 51

Contents
Background
Monomorphic Translation Example
Partial Evaluation with Stock Coq?
Translation of Codegen
Codegen Reduction Rules
Summary

20 / 51

Codegen Translation Flow
1. A user defines a function pow and f
2. A user specifies the second argument of pow is static
3. Codegen transforms f
I Codegen finds that pow is called with the second argument of 3
I Codegen defines p_pow3
Definition p_pow3 a := pow a 3.
I Codegen defines s_f using p_pow3

4. Codegen transforms p_pow3
I Codegen defines s_pow3
Definition s_pow3 a := ...
I Codegen verifies p_pow3 = s_pow3

5. Codegen generates C function pow3 from s_pow3
6. Codegen generates C function f from s_f
The invocation of p_pow3 is translated to the invocation of
pow3(Problem 2, call site replacement, is solved)
21 / 51

Specialization of pow
Fixpoint pow (a b : nat) : nat :=match b with
| O ⇒ 1| S b’ ⇒ a * pow a b’end.

↓ specialize with respect to b = 3
Definition p_pow3 (a : nat) : nat := pow a 3.
Definition s_pow3 (v1_a : nat) : nat :=let v2_n := O in
let v3_n := S v2_n in
let v4_n := Nat.mul v1_a v3_n in
let v5_n := Nat.mul v1_a v4_n in
Nat.mul v1_a v5_n.
Goal s_pow3 = p_pow3. Proof. reflexivity. Qed.

22 / 51

Convertible Transformations
We define Gallina to Gallina transformation as several steps
1. Inlining
2. V-normalization: Make application arguments and match item
variables
3. S-normalization: Simplification
4. Replace call sites with specialized functions
5. Unused let-in Deletion
6. Argument completion to avoid partial application
7. C Variable Allocation
These steps transform a term convertibly for verification withreflexivity

We explain V-normalization and S-normalization

23 / 51

Contents
Background
Monomorphic Translation Example
Partial Evaluation with Stock Coq?
Translation of Codegen
Codegen Reduction Rules
Summary

24 / 51

Gallina Termt, u = xvariable|cconstant|C

constructor

|T

type

| λx : T . t

abstraction|t u

application| let x := t : T in u

let-in| match t0 with (Ci ⇒ ti )i=1...h end

conditional| fix (fi /ki : Ti := ti )i=1...h for fj

fixpoint

Note: We omit details of types.
Actual Gallina syntax permits any term as a type because it isdependently typed
We ignore Var, Meta, Evar because they are not used in complete program. Int and Float are considered as
constants. Prod, Ind and Sort are considered as types. Cast is ignored because it can be eliminated immediately.
CoFix is ignored because lazy-evaluation is not suitable to C. Proj is ignored because it is similar to match.
25 / 51

Difference with Actual Gallina Term
Our Gallina syntax is more concise than actual Gallina:
I λx : T . t means fun (x : T ) ⇒ t
I let x := t : T in u

means

let x : T := t in u

I fix (fi /ki : Ti := λxi1 : Ti1 · · · . ti )i=1...h for fj means
fix f1 (x11 : T11 ) . . . {struct x1k1 } := t1
with . . .
with fh (xh1 : Th1 ) . . . {struct xhkh } := th for fj
I match t0 with (Ci ⇒ λxi1 · · · . ti )i=1...h end means
match t0 with
| C1 x11 . . . ⇒ t1
| ...
| Ch xh1 . . . ⇒ thend
We ignore as-in-return clauses because they are not used in
reductions
26 / 51

Convertion Rules
reflexivity tactic checks two terms are confluent by these rules

beta: E [Γ] ` ((λx. t) u) . t{x/u}(x := t) ∈ Γ(c := t) ∈ E
delta-local:delta-global:
E [Γ] ` x . t
E [Γ] ` c . t
zeta: E [Γ] ` let x := t in u . u{x/t}E [Γ] ` Cj u1 . . . up+m : T
iota-match:p is the number of parameters of the inductive type T
E [Γ] ` match (Cj u1 . . . up+m ) with (Ci ⇒ ti )i=1...h end. tj up+1 . . . up+m

iota-fix:0
ukj = C u10 . . . um

E [Γ] ` (fix (fi /ki := ti )i=1...h for fj ) u1 . . . ukj. tj {fk /fix (fi /ki := ti )i=1...h for fk }k=1...h u1 . . . ukj

eta expansion:

E [Γ] ` t : ∀x : T . U
E [Γ] ` t . λx : T . (t x)(t{x/u} means a term in which x in term t is replaced by u. [Coq reference manual])

27 / 51

Evaluation Strategy for Codegen

I The six reduction rules of the conversion rules (beta,delta-local, delta-global, zeta, iota-match, and iota-fix) defines
the execution of Gallina
I Gallina itself can use any evaluation strategy
I We use strict evaluation strategy as C:
Application arguments are evaluated before the function call
I A partial application does not call the function because there
is no partial application in C
(Partial application will generate a closure when we support
closures in future)

28 / 51

Computation SizeI We do not want to transform functions slower
I We define “computation size” as the number ofmatch-expression evaluated in run time
I computation size is a rough approximation of running time
I it includes loop count because Gallina recursion needs
match-expression to obtain a subterm of a decreasingargument

I Our transformations does not increase computation size
Note: Computation size does not mean code size

29 / 51

V-Normal Form
We use V-normal form for our transformations
V-normal form restricts Gallina terms that
(1) application arguments and (2) match items to variablest = x | c | C | T | λx : T . t | let x := t : T in u
| fix (fi /ki : Ti := ti )i=1...h for fj
|t x

← (1)

| match x with (Ci ⇒ ti )i=1...h end← (2)V-normalization transforms Gallina to V-normal form:
I t0 x1 . . . xi−1 ti ti+1 . . . tn
. let xi := ti in t0 x1 . . . xi−1 xi ti+1 . . . tn
I match t0 with (Ci ⇒ ti )i=1...h end. let x0 := t0 in match x0 with (Ci ⇒ ti )i=1...h end
Note: V-normal form is similar to A-normal form [Flanagan1993]
but let-binding (t of let x:=t:T in u) and function position of
application (t of t x) can be any V-normal term
30 / 51

S-Reductions: Reduction Rules without Computation
Duplication
We define reduction rules similar to the conversion rules but
without computation duplication
I beta-var
I delta-var
I delta-fun
I zeta-flat
I zeta-app
I zeta-del
I iota-match-var
I iota-fix-var

31 / 51

Beta May Duplicate Computation

beta: E [Γ] ` ((λx. t) u) . t{x/u}Problem: (λx. x + x) (x ∗ x) . (x ∗ x) + (x ∗ x)
Solution: V-normal form restrict arguments as variables
Copying variables does not cause computation duplication because
evaluation of a variable does not contain evaluation of match

32 / 51

Beta May Expose Computation in Partial Application
Problem: (λx. match x with tt ⇒ λy . t end) z .
match z with tt ⇒ λy . t end
I The evaluation of the former has no evaluation of match(It generates a closure because it is a partial application)
I The evaluation of the latter does cause an evaluation of match
I So computation size increases
Solution: We apply beta reduction if one of the following issatisfied
I it is not a partial application i.e. the result is an inductive type(full application evaluates function body anyway)
I the abstraction body is an abstraction or fixpoint(evaluation of abstraction and fixpoint is closure generation
thus it has no evaluation of match)
Note: the second condition is added after the camera-ready33 / 51

Beta-Var Reduction

0<nbeta-var:E [Γ] ` (λx. t) y1 . . . yn : T(T is an inductive type) or (t is an abstraction or fixpoint)
E [Γ] ` (λx. t) y1 . . . yn . t{x/y1 } y2 . . . yn

I Since this rule is a restricted beta reduction, convertibility ispreserved

34 / 51

Zeta May Duplicate Computation
zeta: E [Γ] ` let x := t in u . u{x/t}

Example: let x := y ∗ y in x + x . (y ∗ y ) + (y ∗ y )Solution: We apply zeta only for moving or removing an expression(“moving” is combination of zeta reduction and zeta expansion)
zeta-flat: E [Γ] ` let y := (let x := t1 in t2 ) in t0. let x := t1 in (let y := t2 in t0 )zeta-app: E [Γ] ` (let x0 := t in u) x1 . . . xn
. let x0 := t in (u x1 . . . xn )x does not occur in u
zeta-del:E [Γ] ` let x := t in u . u
35 / 51

Delta-Local May Duplicate Computationand May Break V-Normal Formdelta-local:(x := t) ∈ Γ
E [Γ] ` x . t

Γ is a local context
It contains (x := t) if x is occurs in u of let x := t in u

Example: let x := y ∗ y in x + x. let x := y ∗ y in (y ∗ y ) + x. let x := y ∗ y in (y ∗ y ) + (y ∗ y )Solution: We apply delta-local reduction if one of the following issatisfiedI t is a variable
I Evaluation of t has no computation and x occur in a function
position of application
36 / 51

Delta-Var and Delta-Fun Reduction
I t is a variable:
I Since an evaluation of a variable has no computation, copying
it does not increase computation size
I Replacing a variable with a variable does not break V-normal
form

delta-var:(x := y ) ∈ Γ
E [Γ] ` x . y

I Evaluation of t has no computation and x occur in a function
position of application:
I Since an evaluation of t has no computation, copying it does
not increase computation size
I Function position is not restricted by V-normal form

0≤pdelta-fun:0<q(f := t x1 . . . xp ) ∈ Γt is one of x, c, C , λx. u, fix (fi /ki := ti )i=1...h for fj
E [Γ] ` f y1 . . . yq . t x1 . . . xp y1 . . . yq

37 / 51

Iota-Match Conflicts with V-Normal Form
E [Γ] ` Cj u1 . . . up+m : T
iota-match:p is the number of parameters of the inductive type T
E [Γ] ` match (Cj u1 . . . up+m ) with (Ci ⇒ ti )i=1...h end. tj up+1 . . . up+m

Problems:
I match item must be a variable in V-normal form
I up+1 . . . up+m may have computation
Solutions:
I We examine the local context for the match item
I The constructor application arguments must be variables(x := Cj y1 . . . yp+m : T ) ∈ Γ
iota-match-var:

p is the number of parameters of the inductive type T
E [Γ] ` match x with (Ci ⇒ ti )i=1...h end. tj yp+1 . . . yp+m
38 / 51

Iota-Fix Conflicts with V-Normal Formand May Break V-Normal Form
iota-fix:0
ukj = C u10 . . . um

E [Γ] ` (fix (fi /ki := ti )i=1...h for fj ) u1 . . . ukj. tj {fk /fix (fi /ki := ti )i=1...h for fk }k=1...h u1 . . . ukj

Problems:
I iota-fix needs the decreasing argument constructor form but it
is not possible in V-normal form
I iota-fix replaces fk with fixpoints which may break V-normal
form
Solutions:
I We examine the local context for the decreasing argument
I We introduce let-in expressions for the fixpoints
I Also, we prohibit partial application (same as beta-var)
39 / 51

Iota-Fix-Var Reduction(xkj := C y1 . . . ym ) ∈ Γ f10 . . . fh0 are fresh variables
E [Γ] ` (fix (fi /ki := ti )i=1...h for fj ) x1 . . . xn : T
iota-fix-var:

T is an inductive type
E [Γ] ` (fix (fi /ki := ti )i=1...h for fj ) x1 . . . xn .
let f10 := fix (fi /ki := ti )i=1...h for f1 in . . .
let fh0 := fix (fi /ki := ti )i=1...h for fh in
tj {fk /fk0 }k=1...h x1 . . . xn

40 / 51

Summary

I Codegen implements partial evaluation using Gallina to
Gallina transformation
I The partial evaluation does not duplicate computation
I This transformation can be verified easily
I The partial evaluation also be used for monomorphization anddependent type elimination
Future work:
I Support downward funarg (restricted closure)
I Support proof elimination

41 / 51

Extra Slides

42 / 51

Code Size

I The partial evaluation can cause exponential code bloat
Static computation of pow 2 b causes exponential code bloat
because nat is Peano’s naturals
This is unavoidable as far as we provide general partial
evaluation
I We can avoid exponential code bloat by sacrificing generalpartial evaluation: disabling delta-fun and iota-fix-var
In this case, monomorphization is still possible (because it
does not need them)

43 / 51

Monomorphization of List.rev
List.rev is defined as follows:(The type parameter A is a usual argument because Gallina is adependently-typed language)
Definition rev := fun (A : Type) ⇒fix rev (l : list A) : list A :=match l with| nil ⇒ nil| x :: l’ ⇒ rev l’ ++ x :: nilend.

We want a monomorphic version of List.rev for nat:
Definition rev_nat :=fix rev (l : list nat) : list nat :=match l with| nil ⇒ nil| x :: l’ ⇒ rev l’ ++ x :: nil
end.
44 / 51

Monomorphization is Beta-Reduction

Monomorphization can be considered as beta reduction:
rev nat= (fun (A : Type) ⇒ fix rev ...) nat= (fix rev (l : list A) : list A := ...){A/nat}= fix rev (l : list nat) : list nat := ...
= rev_nat(delta-global)(beta)(substitution)

45 / 51

Dependent Type
When the partial evaluation compute types statically, we caneliminate dependent types
Fixpoint sprintf_type (fmt : string) : Type := match fmt with
| EmptyString ⇒ buffer| String "%"%char (String "d"%char rest) ⇒ nat → sprintf_type rest
| String "%"%char (String "b"%char rest) ⇒ bool → sprintf_type rest
| String "%"%char (String "s"%char rest) ⇒ string → sprintf_type rest
| String "%"%char (String _ rest) ⇒ sprintf_type rest
| String "%"%char EmptyString ⇒ buffer| String _ rest ⇒ sprintf_type rest end.
Fixpoint sprintf (buf : buffer) (fmt : string) : sprintf_type fmt :=match fmt return sprintf_type fmt with
| EmptyString ⇒ buf| String "%"%char (String "d"%char rest) ⇒ fun (n : nat) ⇒ sprintf (buf_addnat buf n) rest
| String "%"%char (String "b"%char rest) ⇒ fun (b : bool) ⇒ sprintf (buf_addbool buf b) rest
| String "%"%char (String "s"%char rest) ⇒ fun (s : string) ⇒ sprintf (buf_addstr buf s) rest
| String "%"%char (String ch rest) ⇒ sprintf (buf_addch (buf_addch buf "%") ch) rest
| String "%"%char EmptyString ⇒ buf_addch buf "%"%char| String ch rest ⇒ sprintf (buf_addch buf ch) rest end.

Compute sprintf (Buf "") "%d + %d = %d" 3 4 7.
(* = Buf "3 + 4 = 7" *)46 / 51

Dependent Type Elimination
sprintf specialized with respect to the format string "x=%d".
Definition s_sprintf_x_eq_nat v1_buf v2_n :=let v3_b := false in let v4_b := false in let v5_b := false in let v6_b := true inlet v7_b := true in let v8_b := true in let v9_b := true in let v10_b := false in
let v11_a := Ascii v3_b v4_b v5_b v6_b v7_b v8_b v9_b v10_b in
let v12_b := true in let v13_b := false in let v14_b := true in let v15_b := true inlet v16_b := true in let v17_b := true in let v18_b := false in let v19_b := false in
let v20_a := Ascii v12_b v13_b v14_b v15_b v16_b v17_b v18_b v19_b in
let v21_b := buf_addch v1_buf v11_a in let v22_b := buf_addch v21_b v20_a in
let v23_b := buf_addnat v22_b v2_n in v23_b
typedef unsigned char ascii;#define Ascii(b0,b1,b2,b3,b4,b5,b6,b7) \((b0) | (b1) << 1 | (b2) << 2 | (b3) << 3 | (b4) << 4 | (b5) << 5 | (b6) << 6 | (b7) << 7)static buffer sprintf_x_eq_nat(buffer v1_buf, nat v2_n) {bool v3_b, v4_b, v5_b, v6_b, v7_b, v8_b, v9_b, v10_b; ascii v11_a;bool v12_b, v13_b, v14_b, v15_b, v16_b, v17_b, v18_b, v19_b; ascii v20_a;buffer v21_b, v22_b, v23_b;/* v11_a = ’x’; */v3_b = false; v4_b = false; v5_b = false; v6_b = true;
v7_b = true; v8_b = true; v9_b = true; v10_b = false;
v11_a = Ascii(v3_b, v4_b, v5_b, v6_b, v7_b, v8_b, v9_b, v10_b);/* v20_a = ’=’; */v12_b = true; v13_b = false; v14_b = true; v15_b = true;
v16_b = true; v17_b = true; v18_b = false; v19_b = false;
v20_a = Ascii(v12_b, v13_b, v14_b, v15_b, v16_b, v17_b, v18_b, v19_b);v21_b = buf_addch(v1_buf, v11_a); v22_b = buf_addch(v21_b, v20_a); v23_b = buf_addnat(v22_b, v2_n);return v23_b;}

47 / 51

Cleaner Code Generation for match
CodeGen Inductive Match nat ⇒ "" | O ⇒ "case 0"| S ⇒ "default" "pred".
CodeGen Constant O ⇒ "0".
CodeGen Primitive S ⇒ "succ".

static nat pow(nat v1_x, nat v2_y) {nat v3_n, v4_z, v5_n;switch (v2_y) {case 0:v3_n = 0;
return succ(v3_n);default:
v4_z = pred(v2_y);v5_n = pow(v1_x, v4_z);
return mul(v1_x, v5_n);}
48 / 51

A-Normal Form, K-Normal Form, and V-Normal FormI A-normal form [Flanagan1993] restricts let-binding bindneither let nor match:
let v := (let . . . ) in t and let v := match . . . end in t
Arguments of application and match item must be variables.
A-normal form also restricts a function position (f off x1 . . . xn ) as a variable or primitive function.
I K-normal form [Birkedal1996] relax the let-binding but still
restricts function position, arguments, and match item
I V-normal form allows any V-normal term at a function
position
I V-normal form is useful to represent an equivalent of a loop in
C as (fix . . .) x1 . . . xn

49 / 51

Limitation of Codegen

It is possible the convertible transformation retains a Gallina termthat Codegen cannot generate C functions
I Type computation
I Closure generation
We have a plan to implement restricted closures (downward
funarg), though

50 / 51

Iota-Match Example
E [Γ] ` Cj u1 . . . up+m : T
iota-match:p is the number of parameters of the inductive type T
E [Γ] ` match (Cj u1 . . . up+m ) with (Ci ⇒ ti )i=1...h end. tj up+1 . . . up+m

I The definition of list
Inductive list (A : Type) : Type :=| nil : list A| cons : A → list A → list A

I list : Type → Typelist has one parameter, A (p = 1)
I cons : ∀ (A : Type), A → list A → list A
cons has two members (m = 2)
cons has three arguments (p + m = 3)
match @cons nat 1 nil with (nil ⇒ t1 ) (cons ⇒ t2 ) end. t2 1 nil

51 / 51