coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Extracting simplified Coq terms into OCaml code

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Extracting simplified Coq terms into OCaml code
Date: Mon, 9 Jan 2023 09:20:49 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT mslow1.mail.gandi.net
Ironport-data: A9a23:56BvLqiNqYE7tylyn7FpMAp9X161pBQKZh0ujC45NGQN5FlHY01je htvXjyCaKzbMWvzL41/Ptm3px8H7MfdndFrT1BrpX83Fn9jpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqidUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYpdDNKg06/gEk35q+q4WtI5gZWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGJkcbM5QxvdhOLWRC9 fEjcmtcdgG+mLfjqF67YrEEasULKdLvO5xG/HRpzDWfAv8gTZGFRajWjTNa9G1p2YYRRbCHO JpfM2Y3BPjDS0Un1lM/B5szgO6uwHb+dzdVsk69vqkm+GvSyQl8yv7rPca9ltmiFZsLwx/H/ zquE2LRMysDJsKTxxe+8X+nh7HkxhHxZJ4OLejtnhJtqAfCnjNPVUV+uUGAifK+kwu1X89VA 1cF/zIn66k07k2iCNfnNyBUu1aBpRobRIMWFuQ77EeCw6zY4kCfC3RsoiN9hMIOnskbSyUDk WGws9blBTFU6ubEUWOg6eLBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4+QcZZafWoSFnNL yC2QDsW2+VD0J5Rv0mv1Qqc2GLzznTcZldtvl2/Y46z0u9uTKCfD7FEBHDe9vJHM9/fS1CAu D4Lks6S7aYIAI3leM2xrAclTOnBCxWtamG0bbtT838Jq2rFF5mLId843d2GDB01WvvogBewC KMphStf5YVIIFyhZrJtboS6BqwClPa/To69DK6OMIAUMvCdkTNrGgkwPSZ8OEizyCARfV0XY /93jO7wVCdKVcyLMhLoGLp1PUAXKtAWnzKLGsyml3xLIJKRbXiZSP8eOUDmUwzKxP3snekhy P4Gb5Hi40wHDoXWO3CHmaZOcwxiBSVlVPje9ZYLHsbdeVAOMD96VJfsLUYJINENc1J9zbuTo RlQmyZwlDLCuJEwAV7XMi8zNe2wDcYXQLBSFXVEAGtEEkMLOe6HhJrzvbNtFVX+3LwykaxHX LMedt+eA/9CbD3C9n5PJdP+tYFuPlDjzw6HIyPvMnB1co9CVj753IbuXjLu0y0SUQuxl881+ IO72i3hHJEsegVFDeTtUsyJ8W+fh3YmtdxXY1rpOfhWIUXlz5hrIXf+j9gxOMA9Fi/AzTq7i SeTWAUSiriWhrRo7Oj2gbugqoupGe5EBm5fQm3XxpetFCzg5mH465RxYOWJWjH8VW3P56SpY 9tO/cz8KPEqmFVrsZJ2NqRCl4YSwsTJnKBL6DhkEFHgTUWZOpk5LlaohcBw57BwnJlHsg6Ia 2ez09h9O4TRHvj6EVQUdTEXXs7a2d46wjDtvOkIemPk7ypK/Z2CY0VYHz+IrAd/dLJVEocU8 d0Nif4syT6Uq0QVa46dryVu6W6zAGQKUPwnurEkEYbbsFcX5W8YU6PMKB3dwc+pW41XP1gIM w2kovPIp45hy3rod1sxEnnw3tRhu6kehSASzHI/IwWmp9mUoN42wxxbzhovRCt30Bhs8rx+K 0prBWJPNISM+DZj3tQeVDqwAwt+XRmS+xHs+WswlUnybUqhZkrSJkITZMeP+0E49TpHXz55p bu39kfsYQzITurQgBQgeBdChaT4bNpT8gbippiWL/6dFcNnXQu/076cW2UYjjDGX+UzvRTjj st39r9SbabbC3Yhk5cjAdPH6YVKGQG2H00cc/RP56hTIHr9fgu10j2wK0ycXMNBCvjJ0E2gA fxVOcN9eEWi5RmKswwkK/YAE51skN4twegySLfhCGoFkrmY9zRSoM3x8Ar6jzQVWNlAq5s2B b7QUDOgKVauo0VotVXDlvQZBVrgU+I4PFX9+MuX7NQ2E4kytbAwUEMqjZqxkXanECpm2BO2r gqYY73fleh+w7tSjq/pT6FPLCSvCNbJTO/T2huCg9dPStLuMMn1qAIerGf8DTlWJbc8X9dWl 6yHldzKgHP+o7c9Vl7Gl6m7F6Vm4du4WMxVOJnVKEZ2sDSjWsi2xTc+4EG9dIJ0le1C6vmdR weXbNW6cfgXUYx/wFxXcy1vLAYPOZ/ob6vPpTKPkNrUM0IziTf4FdKA8WPlSUp5dSVSYp33N VLSisaUv9tdqNxBOQ8AC/RYGKRHGV7EW5V3R+2p4HPcRiOtj0iZs7TvqQs45HuZQjOYGcL9+ tTeSgK4aB22v7rSwcpEt5Bp+CcaF2t5nfJ6a3d1FwSaUNxmJDVuwSUh3ZQ65lV8lzf2046hI jTEbW9kBiz7UTUCdxjgiDgmssFzGcRWUuoV5BRwl69XV8tyLJiDEaBi9yJl7m0wfDb/pA1iA c9L4WX+Z3Bd3bkwLdv+JZWHbSNP3fDL3XEJ/EXwiYr0Dgp27XDmEpB+NFIlaBEr2P0hWKkGy abZiIyErIyGpZbNLPtd
Ironport-hdrordr: A9a23:CT0uUqN64Z7qmsBcTs6jsMiBIKoaSvp037BZ7SBMoHtuA6qlfq GV7ZMmPHDP5Ar5NEtQ/OxofZPwJU80lqQb3WByB9qftWDd0QPCRr2Kr7GSoQEIcBeeygcy79 YCT0EzMrPNMWQ=
Ironport-phdr: A9a23:grixwxZcCIRWWBVmRj0H3IT/LTHP2oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gKPDdiQsqgew8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtIiTanYr5/L Bq6oRjPusUInIBvNrs/xhzVr3RHfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQ LJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4 btnRAPuhSwaMTMy7WPZhdFqjK9DoxyvqRNwzIDJbo+LOvpwfqHScs8VS2daQsZcVDZMDp+gY 4YBDecMO/tToYnnp1sJqBuzHQiiC/nzzT9UnHD227Ax3eUgEQHCxwMvAcgOsGjJp9jyO6cdS /66zLXSwjXFdf9W1jb96IzTfR8/u/GMQal9cdHSyUgvDAPFjVSQqYngPzyLzOQBqW6b4PR8V e+2jWMstg5+rCS1yMg2lonJmpwaykrC9Shh3Yo7Kt22RVJ7bNK5E5ZdtyCXOpd3T80tXW1kp jg2x78JtJOneCUG1JspyhHQZfGbcoWF/hLuWeiNLTtmmH9oeLSyjAux/0i40uDwSNS43VRQo idHjtXArG0B2h7Q58SdVPdw8Vut1S6R2wzO6OxIO0I5mbbBJ5I8wbM9mIAfvVrfEiPqnkj9k bWYeV8++uey7uTqerXmqYGYN49zkgz+N78umsi4AeU2LwQCRW2b9v691L3n50H5T69Fjvsrn anYqpzaI9oUprKhDw9U1IYs9Qq/Ai+43NgFn3QLNlBIdA6dg4T0OVzDI+r0AemwjliwiDtrw urJPrzlApXDNHjDl7LhcK5y60FG1gUz0cpQ55ROBrEOIfLzXlT+u8LCDh8lKAG02OXnCdVm1 oMdWGKPB6qZP73IsVOS4OIgPfWMaJcTuDnmM/cl/eLhjWclmV8BeqmkxYYbZGiiHvt6O0WZf WbsgtAZHGgWuQo+VfXmh0GGUT5OfHm/RLk85zE+CIK+F4jPXIGtgLqb3Ce6BJJafG5GCkrfW UvvIo6DQrIHbD+YCs5niD0NE7a7GKE70hT7mwZ517NhZsXV/icVr46rgNd86vHak1c99Dh+A t6B+3qOXnp3n2YNSiVw2q1j9x8ugmyf2LR11qQLXedY4OlEB19S3f/0yuV7D4q3QQfdZpKTT 13gRNy6ADY3R9Z3wtkUYk87Fc/xxgvb0X+MBLkY36eOGIRy6rjVinf4Ktp0zTDJ1a0rgkM6a tBMJHalh6t6+hKVAYPVwA2Cj6j/Ta0Hx2bW8Xubi2+HvUVWSgl1BKrMUGwWYA3ZrNDz61neZ 6StGK8kMw5ExNTELKZWOZXylVsTYvDlNZzFZn6p3We9ARHd3rSXcI/jYHkQxg3YE0wDjFlV+ H+HMU4xDyGtoiTYASAG+UvHRUTq/KE+rXq6ShVx1ASWdwh70LHz/BcJhPuaQvdV37QeuS5np S8mVFC6l8nbDdaNvW8DNO1VfM897VFb1GnYqx01P5quKLpnj0IfdAI/tl3n1hF+AIFN2cYwq 3ZiwA13IKOemFRPElHQlZ/5N6HeLC/9/RSlZrTK8krdwc2V+6IK5e5+rVj//UmoGkck73R7w oxNyXLPg/eCRAEWUJ/3TgM2700g/u6cPXF7vtyEkycwafrR0HeKwd8iCeo7xwz1et5eNPnBD wruC4gAAMPoLuU2ml+vZxZCPeZI9adyMdn1EpnOkKOtIutkmyqryGpd54UomE2F+jZ1TKjH3 pIPzuuE9hCERiz/jVKkv9qxn41YL2J3fCL32W3/CYhda7cnN4kCBHunJYu4x9F0ioTxc2Vb5 UWgBlYD1dXvfxeOJQ+Yv0UYxQEcpnqpnjG9xjp/nmQyr6aR6yfJxvzraBsNPmMjqHBKtV73O sD0itkbWBLtdA01jF6/4k28waFHpaN5Jm2VQEFSfiGwIXswGqe3s7ODZYZI5vZK+W1YWemga FbcRb/5qRYAzwv4HHpFxzE+cjyw/JP0g1R2hXmcI3B6sHfCMZspmlGAvJqFGq4XhGZeDCBj7 FufTkCxJdyo4cmZm9/Yv+ayWnjgHpxffC/3zJ+R4S6y5GlkGxq6zJXR0pXsFQk31zO+1sE/D 3yX6kmkJNC0h+Lgbbo0GysgTEXx4Md7BIxkx445hZVKnGMfmo3Q530M12H6LdRc36v6KnsLX z8ChdDPs22HkAVuKGyEw4XhWzCT2MxkMpO1a24K0yR74MFOAqqO8JRfnjpuoVu9qA/LJ/5wg n1OrJlmoG5fmOwPtAc3m2+SC70OFE8eMi3onRmS8/ilr7RMZ2eqdLWqkkxzgZryadPK6hEZU 3H/dJA4GCZ25cgqK1PA3kr47YT8ccXRZ9Ye5VWE1g3NhO9PJNcth+IH0GB5bHnlsyRvmItZx VR+mIu3t4+dJyBx8bKlV1RGYybtaZpb+ymx3/wHwYDJh8b2QcUnQ2RRG8G2KJDgWDMK66a9b 17XQmE2+yfJFbGDT1/NugA48zrOC8z5bSjIYiZBi4wyH1/EdRYY2lBxPn1yn4ZlRFrzm4q+K AEgtmpXuQS/8UEEy/o0ZUOmDSGA/EHxOm1yF8TYd0AeuQhG4w293dW2yOV1EmkY+5SgqFbIM WmHf0FSCmpPXEWYBlflN73o5N/a8uHeCPDsZ/3JKa6Dr+BTTZLqjdqmz5dm8jCQN86OImgqD vs13VBGVGx4HMKRkisGSigenSbAJ8CBoxL09ipyp8G5uPPlPWCnrZOIEKdXOM5z9gqehLyHM PHJwiNwKDIe2ZoKyX6OzrUDnRYThyxoazixAOEAuCrKH8ey0udcCx8WbT82NdMdtftjmFYVf 5eE2pWviuYr65x9Q01IXlHghMyzMMkDImXncUjCGF7OLrONYzvC38DwZ6q4D7xWluRd8ROq6 lP5WwfuOCqOkz7xWlWhK+ZJ2WuUNRFCsYf7fRdpA2X5UPr9aQygM95yiDAsh7s5mjmZUAxUe Sg5aE5LorCKuGlAhe5jHmVa8nd/BeyfnyGGtq/dI5cS9/RiBCh10eRX/D5prtkdpDEBT/tzl izIq9doqFzzieiDxA1sVx9WoypKjoaG1a2NEb7a54JDWHPB8QhL62iMWU1iTzpND8brvL8Jj N3Glaa1Jz5E/9OS+8YAVZC8wCevK3kwKhnoHTvZFk0DQCL5bQni
Ironport-sdr: 63bbd0cf_q/WIkOwNeiXFb3Ueera16CMB5ctxg4xglXJi8w0I+ioFJ3w hmeOVK+XfGtKXIQWJWaFF+XeUd1fK66xlXhhsSg==

Definition b_red := Eval cbv in b.
Recursive Extraction b_red.

Gaëtan Gilbert

On 09/01/2023 08:00, Wendlasida Ouedraogo wrote:

Dear List,

I wish you a successful and happy new year 2023.

I am trying to extract the computed version of some Coq terms into OCaml
code. My minimized problem is:

Considering the following Coq code:
===================================================
From Coq Require Import List String Extraction ExtrOcamlNatInt.
Import ListNotations.

Definition a := [1; 2; 3].
Definition b := List.map S a.

Extraction Language OCaml.

Recursive Extraction b.
==================================================

I obtain the following OCaml code:

==================================================
(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
let rec map f = function | [] -> [] | a0 :: t -> (f a0) :: (map f t)
(** val a : int list **)
let a = (Pervasives.succ 0) :: ((Pervasives.succ (Pervasives.succ 0)) ::
((Pervasives.succ (Pervasives.succ (Pervasives.succ 0))) :: []))
(** val b : int list **)
let b = map (fun x -> Pervasives.succ x) a
==================================================

What I would like is to obtain:

let b = (Pervasives.succ (Pervasives.succ 0)) :: ((Pervasives.succ
(Pervasives.succ (Pervasives.succ 0))) :: ((Pervasives.succ (Pervasives.succ
(Pervasives.succ (Pervasives.succ 0)))) :: []))

instead of

let b = map (fun x -> Pervasives.succ x) a

This implies some simplifications before the code extraction.

Any ideas?

--
Regards,
M. Wendlasida Tertius OUEDRAOGO

[Coq-Club] Extracting simplified Coq terms into OCaml code, Wendlasida Ouedraogo, 01/09/2023
- Re: [Coq-Club] Extracting simplified Coq terms into OCaml code, Gaëtan Gilbert, 01/09/2023