coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Opaque module typing with exposing function defs

From: Julia Belyakova <julbinb AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Opaque module typing with exposing function defs
Date: Wed, 26 Apr 2017 20:57:29 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=julbinb AT gmail.com; spf=Pass smtp.mailfrom=julbinb AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f173.google.com
Ironport-phdr: 9a23:Gyjirx8jpxYW6v9uRHKM819IXTAuvvDOBiVQ1KB52+McTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDohikJNDA37X/ZhdBrga1BvB6svQZyz5LIbIyXMvd1Y6PTfckdRWpERstfUzFBAoe9b4QVEuEMIPhXr439plQUrhu+AhesC/nywTJPhH/2wKk63P8gEQHAxwMtBN0OsHHOo9X0MKceS/y6zK7NzTjaaf5dxDTz6JDQfxw/vf2BWah8fMnRxEU1CQ/Jk1edpZb4Mz6X2OkAtXWQ4fB6WuK1kWEnrhl8ojixyccojYnEnocVxUrF9SV92Yo1OMe3RFJibd6qDZddtS+XO5F5QsMlRGFotyI6xaMctZGneygKzYwrxx/Za/OZb4iF+gzvWPqVLDtih39oeKiziwiv/UWi0OHwS8u53VhSoipAiNbMt3QN1xLJ6siAT/tw5kWh2SuL1w/I6+FEJ1s7mLHUK54k2LEwl54TvV7fES/xnUX6lLWWeVk8+ui09+TnZa3rqYObN49tkw3xLqAumtGkDukjKQgPX22b+fym27H5/E35Rq9KjvwsnaXDvpDaP5dTmqnsCAhMl40n9hyXDjG80d1ek2NUAkhCfUelkozoMhnkLfTpBPS4nV3kxDV2w/rHOLfJDZDEL3yFm7DkK+Uuo3VAwRY+mIgMr6lfDasMdar+

Dear Coq users,

I guess it's a stupid question, but...

I want to define a module with certain parts being hidden. For this I define a module type and then use opaque typing for the module. And the problem is that now I cannot compute functions of the module, their definitions are not accessible.

Please, find a simple example below.

Module Type Addition.
Parameter t : Type.
Parameter add : t -> t -> t.
End Addition.

Module MAddition : Addition with Definition t := nat.
Definition t := nat.
Definition add x y := x + y. (* I want this to be available *)
Definition priv_id (x : t) := x. (* This must be hidden *)
End MAddition.

(* priv_id is not available as desired *)
(* Compute (MAddition.priv_id 4). *)
(* add is available, but the call does not reduce to 7 *)
Compute (MAddition.add 3 4).

[Coq-Club] Opaque module typing with exposing function defs, Julia Belyakova, 04/26/2017
- Re: [Coq-Club] Opaque module typing with exposing function defs, ikdc, 04/26/2017
  - Re: [Coq-Club] Opaque module typing with exposing function defs, Julia Belyakova, 04/27/2017
    - Re: [Coq-Club] Opaque module typing with exposing function defs, Ralf Jung, 04/27/2017
      - Re: [Coq-Club] Opaque module typing with exposing function defs, Julia Belyakova, 04/27/2017
        
        Re: [Coq-Club] Opaque module typing with exposing function defs, Jason Gross, 04/27/2017
        
        Re: [Coq-Club] Opaque module typing with exposing function defs, Jason Gross, 04/27/2017
        
        Re: [Coq-Club] Opaque module typing with exposing function defs, Jason Gross, 04/27/2017
    - Re: [Coq-Club] Opaque module typing with exposing function defs, Gaetan Gilbert, 04/27/2017
      - Re: [Coq-Club] Opaque module typing with exposing function defs, Julia Belyakova, 04/27/2017
        
        Re: [Coq-Club] Opaque module typing with exposing function defs, Pierre Courtieu, 04/27/2017