Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
20 May 2022, 15:51:20 UTC
Revision 64c24ed6d2c0b485818e0ae76c4be0ebde0e628a authored by Benjamin Gregoire on 26 April 2018, 18:31:53 UTC, committed by Benjamin Gregoire on 26 April 2018, 18:31:53 UTC 
improve "include" in module type and module.
 
The following is now possible:
type t, t', u, u', v, v'.

module type OT = {
  proc f(_: t): t'
  proc g1(_: t): t'
}.

module type MT (O : OT) = {
  include OT
  proc g(_: u): u'
}.

module type MT1 (O : OT) = {
  include OT [f]
  proc g(_: u): u'
}.

module type MT2 (O : OT) = {
  include OT [f] {O.f}
  proc g(_: u): u'
}.

module type MT3 (O : OT) = {
  include OT [f] {O.g1}
  proc g(_: u): u'
}.

module ((M : MT1):MT2) (O : OT) = {
  proc f = O.f

  proc g(x: u): u' = {
    return witness;
  }
}.

module M1 = {
  proc f () : unit = { }
  proc g () : unit = { }
}.

module M2 = {
  include M1
}.

module M3 = {
  include M1 [f]
}.

module M4 = {
  include M1 [+f]
}.

module M5 = {
  include M1 [-f]
}.

module F (O:OT) = {
  proc f1 () = {}
}.

module G (O:OT) = {
  include O
  include F(O)
}.

module G1 (O:OT) = {
  include O [-f]
  include F(O)
}.
1 parent 7f33e2a
Raw File
Tip revision: 64c24ed6d2c0b485818e0ae76c4be0ebde0e628a authored by Benjamin Gregoire on 26 April 2018, 18:31:53 UTC
improve "include" in module type and module.
Tip revision: 64c24ed
COPYRIGHT 
EasyCrypt (excluding the EasyCrypt standard library):
  Copyright (c) - 2012-2016 - IMDEA Software Institute
  Copyright (c) - 2012-2018 - Inria
  Copyright (c) - 2012-2018 - X
  Distributed under the terms of the CeCILL-C license

  http://www.cecill.info/licences/Licence_CeCILL-C_V1-en.txt

EasyCrypt standard library (theories/**/*.ec):
  Copyright (c) - 2012-2016 - IMDEA Software Institute
  Copyright (c) - 2012-2018 - Inria
  Copyright (c) - 2012-2018 - X
  Distributed under the terms of the CeCILL-B licence.

  http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt
back to top