// Organizarea programelor mari
include "lib.dfy"

module Z
{
  import opened X

  function f(x : int) : int
  {
    creste(x) * scade(x)
  }
}

module Y
{
  import X

  function f(x : int) : int
  {
    X.creste(x) * X.scade(x)
  }
}

module Z1
{
  import MyModule = X

  const X : int := 42

  function f(x : int) : int
  {
    MyModule.creste(x) * MyModule.scade(x)
  }
}

// varianta 1 de imbricare de module (de preferat)
// module Constants
// {
//   const magic : int := 42

//   module Primes
//   {
//     const prime1 : int := 7
//     const prime2 : int := 101
//   }
// }

// varianta 2 de imbricare (de evitat)
module Constants
{
  const magic : int := 42
}

module Constants.Primes
{
  const prime1 : int := 7
  const prime2 : int := 101
}

// circuitele nu sunt permise
// module X1
// {
//   import X2
// }
// module X2
// {
//   import X1
// }


// tot codul Dafny merge intr-un modul global, implicit,
// care nu are un nume
method asdf() // orice metoda din toplevel merge intr-un
              // modul predefinit (numit in implementarea sistemul Dafny "_default", nu am nicio posibilitate sa-l accesez explicit)
{
}

// Conceptul de modul abstract

abstract module ProcesareNumere
{
  function cresteNumar(x : int) : int
    ensures cresteNumar(x) > x
  // {
  //   x + 42
  // }
}

abstract module ProcesareNumere' refines ProcesareNumere
{
  function cresteNumar(x : int) : int
    ensures cresteNumar(x) > x + 9
  // {
  //   x + 42
  // }
}

module ProcesareNumere1 refines ProcesareNumere'
{
  function cresteNumar(x : int) : int
    ensures cresteNumar(x) > x + 10
  {
    x + 42
  }
}

module ProcesareNumere2 refines ProcesareNumere
{
  function cresteNumar(x : int) : int
    ensures cresteNumar(x) > x + 5
  {
    x + 7
  }
}

abstract module Exemplu
{
  import InstantaProcesareNumere : ProcesareNumere

  method exemplu(x : int) returns (r : int)
    ensures r == InstantaProcesareNumere.cresteNumar(x)
  {
    r := InstantaProcesareNumere.cresteNumar(x);
  }
}

module Exemplu1 refines Exemplu
{
  import InstantaProcesareNumere = ProcesareNumere1

  method exemplu1(x : int) returns (r : int)
    ensures r == InstantaProcesareNumere.cresteNumar(x)
  {
    r := exemplu(x);
  }
}

module Exemplu2 refines Exemplu
{
  import InstantaProcesareNumere = ProcesareNumere2

  method exemplu2(x : int) returns (r : int)
    ensures r == InstantaProcesareNumere.cresteNumar(x)
  {
    r := exemplu(x);
  }
}

method Main()
{
  var x := Exemplu1.exemplu1(10); // should print 52
  assert x == 52;
  print x;
  var y := Exemplu2.exemplu2(10); // should print 17
  assert y == 17;
  print y;
}

// Eroare:
// nu este permis ca un modul care implementeaza
// un modul abstract sa nu respecte specificatia:
// module ProcesareNumere3 refines ProcesareNumere
// {
//   function cresteNumar(x : int) : int
//   {
//     x - 10
//   }
// }


/*
   Vizibilitatea identificatorilor dintr-un modul
 */

module Liste
{
  export reveals List, sum, sumAux provides count

  datatype List = Empty | Cons(hd : int, tl : List)

  // function sum(l : List) : int
  // {
  //   if l == Empty then
  //     0
  //   else
  //     l.hd + sum(l.tl)
// }

  function sumAux(l : List, aux : int) : int
  {
    if l == Empty then
      aux
    else
      sumAux(l.tl, aux + l.hd)
  }

  function sum(l : List) : int
  {
    sumAux(l, 0)
  }

  function count(l : List) : int
    ensures count(l) >= 0
  {
    if l == Empty then
      0
    else
      1 + count(l.tl)
  }
}

module User
{
  import Liste

  method asdf()
  {
    var l := Liste.Cons(10, Liste.Cons(42, Liste.Empty));
    var s := Liste.sum(l);
    var s' := Liste.sumAux(l, 1);
    var c : int := Liste.count(l);
    // assert c == 2; // esueaza, fiindca definitia lui conut
    // nu este vizibila
    assert c >= 0;
    assert s == 52;
  }
}

module Constante
{
  const a : int := 10
  const b : int := 11
  const c : int := 12

  // declar mai multe "export set-uri"
  export A reveals a
  export AB extends A provides b
  export AC extends A provides c
}

module User1 // foloseste constantele a, b
             // nu fie vizibila constanta c
{
  import Constante`AB // caracterul "backtick", langa "1"
                      // a nu se confunda cu ' sau "
  method test1()
  {
    assert Constante.a == 10;
    // fails check: assert Constante.b == 11;
    // fails syntax: assert Constante.c == 12;
  }
}

module User2 // foloseste constantele a, c
             // nu fie vizibila constanta b
{
  import opened X = Constante`AC
  method test1()
  {
    assert X.a == 10;
    assert a == 10;
    // assert Constante.b == 11;
    // fails check: assert Constante.c == 12;
  }
}

module User3 // foloseste constantele a, c
             // nu fie vizibila constanta b
{
  import opened Constante`{AB,AC}
  method test1()
  {
    assert a == 10;
    assert b == b;
    assert c == c;
    // assert Constante.b == 11;
    // fails check: assert Constante.c == 12;
  }
}

module AAA
{
  module BBB
  {
    const x : int := 42
  }
}

module BBB
{
  const x : int := 10
}

module CCC
{
  import BBB
  import opened AAA

  method test1()
  {
    assert BBB.x == 10;
  }
}

/*
   module
   abstract module
   import (opened) (Nume = ) module
   export set-uri
   sortare topologica
   */