coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Can I apply "Extraction Inline" and "Extraction Constant" for definitions hidden by a module?

From: Kazuhiko Sakaguchi <pi8027 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Can I apply "Extraction Inline" and "Extraction Constant" for definitions hidden by a module?
Date: Tue, 10 Apr 2018 12:27:35 +0900
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pi8027 AT gmail.com; spf=Pass smtp.mailfrom=pi8027 AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb0-f180.google.com
Ironport-phdr: 9a23:tXRKIhafencMXZbuKE7MUTH/LSx+4OfEezUN459isYplN5qZocW7bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA5/m/ZidF+grxHrx+6ohxz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGoayYJEODuocPeZYror9p1wTphWjHwasB/ngyjBVhnDq3a060vkqHAbe3AwhHN8CrGrYodfuOacdVOC61qjIzTHZY/xK3jf97ZHFfxY8qv+PRbJ9adTdxVUrGg/fjVidqZbpMy2I2ukDqWSX8ultWf6phmU6sQ9+uCKvyd0pioTRhoIa1FTE9SJhzYYwP9K4SUp7bcekEZRLqy2WLoV2Tt4hTm10oio6xboGuZm0fCgO1psr3QLQa/uCc4SQ4xLjUvieIStgiX57ZL6ygwy+/Eugx+HmSMW4zVhHojBYntTPqnwBzxnT5dKGSvt58EehwzGP1wXL5+FcIEA5lrbXJ4Ajz7MrmZoTtF7MHi7ymEnskKCWcUAk9vCy6+v7erXmuoOcN4hshw7iNaQug9WzDvg8MggTRGeW4v+81b3m/U3hWrpGlPw2kq/DsJDbP8sXvKC5AxUGmrokvh24FnKt1MkStXgBNlNMPhyd3KbzPFSbA/nqEPe+gFPkqz5ozv/bNb3gSsHVLyibyujJcrN06koaww02m4MMr6lIA60MdaqgEnT6s8bVW0dgYl6Eht3/AdA47bswHGeGA6uXKqTX6Aba6ecmIu3Kb4gQ6m+kd6oVosX2hHp8omczOLGz1MJOOn+9F/ViZU6eZCi024pTISIxpgM7CdfSphiCXDpUPSjgWqs94nQqAtrjA96THsaih7uO2Cr9FZpTNDhL

Hello,

I tried to apply "Extraction Inline" and "Extraction Constant" for
definitions hidden by using "Module Type" and "Module" in two ways,
but both of them are failed. Do you have any idea for solving this?

Best Regards,
Kazuhiko

Require Extraction.

Extraction Language Ocaml.
Extract Inductive
  nat => "int"
           ["0" "succ"]
           "(fun zero succ n -> if n = 0 then zero () else succ (n - 1))".

Module Type ASig.

Parameter x : nat.

End ASig.

Module A : ASig.

Definition hidden := 10.
Definition x := hidden * hidden.

Extract Inlined Constant x => "10".

End A.

Fail Print A.hidden. (* A.hidden is not accessible from outside of A. *)

Extraction A.
(*
A.hidden is not replaced by the constant and not inlined:

module A =
 struct
  (** val hidden : int **)

  let hidden =
    succ (succ (succ (succ (succ (succ (succ (succ (succ (succ 0)))))))))

  (** val x : int **)

  let x =
    mul hidden hidden
 end
*)

Fail Extraction Inline hidden.
Fail Extract Constant x => "10".

[Coq-Club] Can I apply "Extraction Inline" and "Extraction Constant" for definitions hidden by a module?, Kazuhiko Sakaguchi, 04/10/2018
- Re: [Coq-Club] Can I apply "Extraction Inline" and "Extraction Constant" for definitions hidden by a module?, Kazuhiko Sakaguchi, 04/10/2018