coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Wendlasida Ouedraogo <ouedraogo.tertius AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Extracting simplified Coq terms into OCaml code
Date: Mon, 9 Jan 2023 08:00:00 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ouedraogo.tertius AT gmail.com; spf=Pass smtp.mailfrom=ouedraogo.tertius AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f43.google.com
Ironport-data: A9a23:K3nA/aqSWMVv9g0oswC0V4cLejNeBmLEYRIvgKrLsJaIsI4StFCzt garIBmDP/yNMGv1ctF+PtnkoUgH65fUyNVkSAE4/H8zEilHoOPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKiefHkZqTZMEE8JkQhkl/MynrlmiN24BxLlk d7pqqUzAnf8s9JPGj9SuvzrRC9H5qyo42tB5gxmP5ingXeH/5UrJMJHTU2OByCgKmVkNrbSb /rOyri/4lTY838FYj9yuuuTnuUiG9Y+DCDW4pZkc/DKbitq+kTe5p0G2M80Mi+7vdkmc+dZk 72hvbToIesg0zaldO41C3G0GAkmVUFKFSOuzdFSfqV/wmWfG0YAzcmCA2kpFrEbwb4vAVh8+ OFCaxVSLU6Y2vmPlefTpulE3qzPLeHuNYIb/3Z8lHTXUa1gTpfETKHHo9Rf2V/chOgURaeYN 5dfM2M3KkibC/FMEg9/5JYWm/qlimP2dDJf7k6Yv7Y2/nP7wwl40byrO93QEjCPbZULwB3C+ TqZl4j/KjpKZceP0iK6y3CXtN+erCzeZ9MRJKLto5aGh3XKnjBJYPEMbnOwpuD8gUqjUfpEO kkM82wvq7Iz/QqlVLHAswaQpXeFulsbR4MVHbFhrg6KzaXQ7kCSAW1soiN9hMIOq+QKRgdyj l+wrd70X39K7/7LUi+Gz+LBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zT8ZZafWlSVnNL yC2QDsW3OpM0JZav0mv1RWW3GL2/8mhohsdv12PBgqYAhVFiJlJjrFEBHDe5PdEaYGFFxyP4 CNClM+Z4+QDS5qKkURhodnh/pn5up5p0xWG2TaD+qXNERzwpBZPmqgNsVlDyL9BaJpsRNMQS Ba7VfltzJFSJmC2SqR8fpi8Dc8npYC5S4u+DKiOMIAVPsQsHONiwM2ITR7Pt4wKuBh8+ZzTx b/GGSpRJSxLV/k4k2reqxk1ge96nEjSOl8/tbiil0j9uVZvTHGSTrgBPTOzghMRvcu5TPHu2 48HbaOikk0BOMWnO3W/2dNNcDgicCdjbbio8ZA/XrDYeWJORjpxY8I9NJt7JOSJaYwOxrmWl px8M2cEoGfCaYrveVrUMSw6Mu+yNXu9xFpiVRER0Z+T8yBLSe6SAG03LvPbpJF2r7Qx/u0+V PQfZcSLD9JGTzmNqXxXboDwoMYmPF6njB6HdXjtKjUuXY9SdyqQ8P/dfyzr6HYvCAizvpAAu LGO7F7QbqcCYAVAN/zoTsyT4Wm/hlUjvd5jflDpJ4BTcXr88YIxJC3WiOQ2Ev42Kh7C52W70 l+WCCgHueOWmp8Rz+iRoLHZqY3zQu10MXdHLjOK8Ze3Kijo0W6xyqBQUOuzXG78VUGl3I6Ad Olq3/XHH/lfp2lzsq14CKRO4ZMlwtnS+49h0QVvGUvUY2SRCr9PJmeM2e9NvPZvwoB1lBSXW EXV3PVnIpSMZd3YFWAOKDofbuis0e8enh/Q568XJGT4/CpGw6qVY35NPhWjiD1vE5UtCdkLm dwegc8x7xCzrjEIMdzc1yBdyDmqH0w6Cq4isskXPZ/vhg8V0Wp9WJ37CBGnxLGUat5JDFsmH S/MuorGmIZn5xTjd1gdKCHz+NRz1LU0ljJE9lsgH2iyu8Hkg6Y31SJB8D5sQQVyyA5G4t1JO WNqFhNUIKmSzghsn+xGeX6mICBaJRij4keq4UA4pG7YaEiJV2L2M2w2P9iWzn0Z625xejt6/ qmS7WTYDRLGWd7X5TRrf2JIsNnhQs5V2iyYvfu4DuKXG5UeShj0sJ+EPGYnhUPuPpIsuRfhu +JvwtdVVYT6Eiw1+IgQFIiQ0OUreiCufWBtb6low/IUIDv6Zjq35DmpLnKxcONrI9jh0xexK +5qF/J1eyWO7gS8hRFFOvdUOJ5xpuAj2/QacLCyJWImjaqWngA0jL3urBrBlE0ZaPQwt/ZlM Y7AVSOwIkrJj1tupmL9hs1lOG25XNo6WDPBzN2FqNsuKZZSn9xvIGcT06S1tUq7KAFI3QyZl yKdar70z95N85VNnYztIP8aBwyLNs7CDrWU0QGssuZhacHEHtfOujg09HjmHVVyFpkAV+tnk Y+itIbM43rEm7ItQkbllIKkBYAQwemPBM9sLdPQAFxBuCmzSOvAwkAkxTijCJprlNh92JGWd zGgYpHtSe9PCsZv+nJFTgN/TTMPALvTRYX9r3qfq/+sNEAs4TbfJon6yU6zPHBpTQ5WCZjQE QSuhu2P4Opfp4FyBBMpIfFqLpt7AV37U5sdaNzDmmiEP1asn2+9lOPupTg45RHPL0u0IsLwz JbGZxr5LRqM4fCCiJkTtoFppRQYAUpsmeR6LApX59dyjCv8F2Ica/gUNZIdEJxPjyjuz9fCa SrQaHc5QzDINdienc4QPPy4NuteOgAPBjs9Djkg/kfRbDvvQY3cW/1u8SBv53owcTzmpA1ix Rfy5VWoViVdALkwLQrQ2hB/qehiz/LegHkP/CgRVuTsVg0GD+xiOGNJRWJwuO+uLy0JvErOL GkxA2tDRSlXjKI3/dlIIxZoJf3SgN8jI/jEo8tCLBYzdrh3FNF99cA=
Ironport-hdrordr: A9a23:3eTh16NstgNG5sBcTsyjsMiBIKoaSvp037BL7TEXdfUxSKalfq +V7ZcmPHPP6Ar5O0tApTnjAtjjfZq0z/ccirX5Vo3SOTUO1lHYSL2KLrGP/9QjIUDDHyJmup uIupIRNOHN
Ironport-phdr: A9a23:gJQiQx168PBS6atmsmDOew4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaCo6UwxwaRBs3y0LFttan/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G 9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys+5DfeQZFiTqybb9vM Bm7oxjau9ULj4dlNqs+xRzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0Q rNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6 apgVRnlgzoFOTEk6mHaksN/gqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b 4wKD+cZPelXsY/9qEYKrRSkHgmsBf7gxSVVjXHvwK01zfkuERvc0wwnENIOt2nfodLyNKcPT ++60bPIwi/Eb/NZ3jfx8pTIfQ47ofGQXLJwbNHRxFIgFwPAlFqQqIjlMymJ2eQKtmiW9uxtX v+ghGA7sQ9+uCSvxtsyhYnTgIIY0k3J+CF5zos3JtC1SUp2bcOrHpZTuS+WKpd7T8IjTmxsp Cs3y6EKt5GlcSUE1pkqxRDSZv6bf4aH4R/uSvqdLzh+iXl4e7y/nw6//Va8xuD4TMW501ZHo jBbntXRqnwBzRPe58aBR/Bg5EmuwyyP2BrW6uxcIUA7i67bK5k5z741jJUTsEDDEjbxmEXqk aOab0sk9+em5uj9bbXmoZicN4Bwig7gKKghhsu/AeEgPggPWWiU5/i82aX98UHlRLhGlP47n 6nDvJzEOMgXurS1DgBb34o77hawFTam0NAWnXkdK1JFfQqKj4/0O17QPf/4F+2wg1OjkDds3 fzGIqPuAo/RLnjCjbfhZq1w60FZyAUpzNBf44hYBa0GIPL2QkPxssfXAQcjMwOo2+bnFMl91 oQGVG6SGqOZKr/dsUeU5uIzJOmBfJMauDHkK/Q8+/HuiWI5lkQGcKmy3ZoXbWi4Ee58L0WYZ 3rsmNYBHn0QsgowVuy5wGGFBDVUfjO5W782zjA9EoOvS4nZFa63h7nU4yq9EplffWFKAxirD HrkbYyDVPBEPCWPL8N7mzsLUv69RpU91Ay1nAD/wrtjaOHT/3tL5trYyNFp6riLxlkJ/jtuA pHFu4nsZ2R9n2dSAiQzwLg6u0t2jFGKzal/hfVcU91V/fJAFAkgZtbH1+IvLdf0V0rae8uRD k68S4ChHDw9VNs2zNhIf0tnB9S/lTjM2iOrB/kekLnYTIcs/Pfk1mPqb914126A0aAgi1c8R c4aMnCrirR28AfUQZLEiVmYir2CeqEV3SqL/2CGniKVpE8Ndgl2XO3eWGwHIEvbqdOs/kTZU 7qnEqgqKCNEwM+Gb6xWM5jn0Q4AS/DkN9DTJWm2ng9cHD6uwbWBJMrvcmQZhmDGDVQc1hoU9 jCAPBQ/ASGopyTfCiZvHBTheRGk9+42s369QkIuqmPCJ0R8y7q4/AIUjv2AWrsS2LwDoiIot zRzGh60wdvXD9OKowcpcr9bZJsx51JO1GSRsAIYXNToKL1vikQXdAtw+V/jzQl2F55ons0jr Xdsxw13aOqZ3F5HazKEzMXoILSETwu6tBuraqPQxhTfyIPMovZJuKl+8Qy7+l3yRS9Auz193 tJY0mWR/MDPBQsWC9fqV1ovsgJ9rPfcazU84IXd0TttN7O1u3nMwYFMZqNtxxC+ctNYKK7BG hX1FphQANWjJPYjnFeuKA4JJvxT6bUcMMavdv/A06mudrUF/nrunSFc7YZx31jZvS1hR+LS1 pEKxLeE0xGbVirnpFiku8Hz34tDYHtBewj3gTihD4lXaKpoeI8NAmr7OMy7yOJ1gJv1UmJZ/ lqub78f8PegYgHaL1n03AkKkF8SvWTigyyziTp9jzAuqKObmi3I2eXrMhQdaCZHQ2xrjFGkJ obR7ZhSW1WlYxIgkxSio1r33bRaub9XIGzaQEMOdC/zZ21vSaq/sLOebtUHsst593UKFr7lO RbGEfb0uH54m2v7EnFbxSwnej3ioZj/kxFgySqcIHt1sHvFaJR1zBbb6sbbQK0Z1T4HSS9kz DjPUwLkbp/5oJPOzs+F7rvtMgDpHodeeiTq046a4S6y5GkwRAa6g+j2gNrsVw4zzS780dBuE yTOthf1JIfxhMHYeapqeFdlAFjk5o90AIZ7x8E3mZwcw3EdiZLT4XcdjWbuKv1U3Kv/aDwGQ jtBkLu3qED1nVZuKH6E3dezUWiQztFoYNa9JH8bwD488ttiB6Kd7bgClixw6Andz0qZcb12m TETzuEr4XgRjrQSuQYj+S6aB6gbAUhSOSG/3wTN9d21q79bIXq+abXlnlQrhsivVfvRx2MUE Ga8YJopGjV8q9lyIE6ZmmOm8ZnqIZHRdY5B7UDSykaYybIJd9Rp0aBWzSt/ZTCj4Tt/kLV91 EI2m8n95dniSS0l/brlUEAGcGStPYVLvGmq1/4Wn97Kjd7xWM89S3NbBN2wCqjwWDMK6aa4b UDXTHtl+y3dQf2GTWr9oA9nty6dTMztbivKYiFflZI7GlGcPBAN2VhEGmxlwdhpUFjtnpWpc V8ltGlOvRih+0cKkqQwcEChNwWX7AawNmVuEMnZfEcQt1sSoR+SaJPW7/ovTXsBoNv8/ErUe zbdP0MRXCkIQhDWXQm9eOP1tJ+bqa7AQbPvSpmGKaOHregUPxuR7bSo1IYuvzOFN8HVe2JnE +V+wE1IG3ZwB8XenTwLDS0RjSPEKcCB9l+6/WVso8az/e6OOkqn7JaTC7ZULdRk+gynyaaFO emKgS9lKDFenpoSzH7MwbIb0RYckSZrPzWqFL0Bs2bKQsey0udPCAUHbipoKMZSx6c13w0IP tKCz92pjfh3ifk6D1oDXlvk24moacEMP2ChJQbHCUKMZ9HkbXXAx8D6Z7/5SKUF1r0F8U3t/ 2zCSwm/ZWfm9XGhTR2kPOBSgTvOORVfvNv4aRNxES35S9mgbBSnMdhxhDlwwLsuh3qMO3RPV Fo0O05LsLCU6jtVx/tlHGkUpH14IOWekiGW6K/EJ4wKsOZwKitxnuNepn89zvEGiUMMDOwwg ybUotN09hu+lfKTzzN8TBdUgjNChYbOulk7fKuFrd9PXnHL+B9L5mKVQUdvxZMtGpjkvKZez cLKnaT4JWJZ8t7aysAbAtDdNMONNHdJ2fXBFzvdDQ9DRjmuZzi3b6l1n/Sb93nTpZ8/+MCEc HsmT7ZaUBkyCqpfBBg+WtMFJ5hzU3UvlrvJ1KY1
Ironport-sdr: 63bbbb78_ymw4D8MhYBjO9KI9xhOFaNRMH7/UQz8dUJmhSV6MYHClKJe ffXMQrPaOtw5rw95NUWkcnsgrkQWMnYkB107WrA==

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