From 93fa2d5d3440f2c44c1cc04e902d0ec9208e8f9d Mon Sep 17 00:00:00 2001
From: Valentin Blot <24938579+vblot@users.noreply.github.com>
Date: Thu, 7 Dec 2017 22:31:39 +0100
Subject: [PATCH] Optimized extraction

---
 Coq/f.v | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/Coq/f.v b/Coq/f.v
index 2d31325..536e4b8 100644
--- a/Coq/f.v
+++ b/Coq/f.v
@@ -965,9 +965,24 @@ rewrite form_to_type_substt.
 reflexivity.
 Qed.
 
-Extract Inductive unit => "unit" [ "()" ].
+Extraction Inline id.
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive list => "list" [ "[]" "(::)" ].
+Extract Inlined Constant List.map => "List.map".
+Extract Inlined Constant List.nth => "(fun n l d -> match List.nth_opt l n with Some a -> a | None -> d)".
+Extract Inlined Constant List.fold_right => "(fun f a l -> List.fold_right f l a)".
 Extract Inductive prod => "(*)"  [ "(,)" ].
+Extract Inlined Constant fst => "fst".
+Extract Inlined Constant snd => "snd".
+Extract Inductive sigT => "(*)" ["(,)"].
+Extract Inlined Constant projT1 => "fst".
+Extract Inlined Constant projT2 => "snd".
 Extract Inductive option => "option"  [ "Some" "None" ].
-Extraction "f.ml" term_equal bound term1 term2.
+Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
+Extract Inlined Constant pred => "pred".
+Extract Inlined Constant Init.Nat.sub => "(fun m n -> m - n)".
+Extract Inlined Constant Nat.eqb => "(fun m n -> m = n)".
+Extract Inlined Constant Nat.leb => "(fun m n -> m <= n)".
+Extract Inlined Constant Nat.ltb => "(fun m n -> m < n)".
+Extract Inlined Constant Nat.compare => "(fun m n -> if m < n then Lt else if m > n then Gt else Eq)".
+Extraction "f.ml" term_equal bound type1 term1 type2 term2.
-- 
GitLab