%* This is the standard regression test file for the module system.
   It contains example declarations for every implemented feature. *%

%namespace "".
%namespace t2 = "test2.elf".
%namespace t3 = "test3.elf".

%% testing basic syntax
%* ... and preserved
comments *%
%sig R = {
  a : type.
  %* a constant declaration *% 
  c : a.
}.

%% a declaration with a different namespace
%namespace "logical_ns/test.elf".
%namespace t1 = "../test.elf".
%sig R = {%include t1.R.}.

%% testing includes of multiple signatures with the same name from different namespaces
%sig R' = {%include t1.R.}.
%sig S = {%include R. %include R'.}.
%% this currently causes a name error because it tries to generate structures s.R: t1.R and s.R:R
%% %sig T = {%struct s: S.}.

%namespace "../test.elf".

%% testing basic semantics, note why "test" is well-typed
%sig S = {
  a' : type.
  b' : a'.
  b'2: a'.
  %struct r' : R = {a := a'.}.
  c' : r'.a.
  d' : a' -> type.
  test : d' c'.
}.

%% testing instantiations of structures, try removing the instantantion of a'
%sig T = {
  a'' : type.
  b'' = a'' -> a''.
  %struct r'' : R = {a := a'' -> a''.}.
  %struct s'': S = {a' := b''. %struct r' := r''.}.
}.

%% testing a deep instantiation r''.c := f''', and a structure definition s''' = T.s'' t'''.
%% also try removing the instantiation of a''
%% note that the order of instantiations in a structure is not relevant
%sig U = {
  a''' : type.
  f''' : a''' -> a'''.
  %struct t''' : T = {r''.c := f'''. a'' := a'''.}.
  %struct s''' = T.s'' t'''.
  c''' : a'''.
}.

%% testing views
%view V : R -> R = {
  a := a -> a.
  c := [x] c.
}.

%% views with complex codomain

%view VV : R -> S T U = {
   a := a'''.
   c := c'''.
}.


%% testing views with structure instantiations; not so easy to type-check by hand anymore
%% note that type reconstruction works
%view W : S -> T = {
  a' := a'' -> a''.
  b' := [x] x.
  b'2 := r''.c.
  %struct r' := r''.
  c' := s''.c'.
  d' := [x: b''] (a'' -> s''.d' x).
  test := [x] s''.test.
}.

%% testing includes and subordination
%sig R' = {
  %include R.
  a' : type.
  c' : R.a.
  %% no subordination between R.a and R'.a'
}.

a : type.

%sig R'' = {
  %include R'.
  f : R.a -> R'.a'.   %% creates subordination
  c : a.                %% reference to a on toplevel
  a : type.             %% toplevel name shadowed
}.

%% include in a view
%sig X = {
  k : type.
  l : k.
}.

%sig X' = {
  %include X.
  k' : type.
}.

%view r : R -> X = {
  a := k.
  c := l.
}.

%view r' : R' -> X' = {
  %include r.  %%i.e., R.a := X.k. R.c := X.l
  a' := k'.
  c' := X.l.
}.

%% include in a structure
%sig Y = {
  a : type.
  %struct r : R = {a := a.}.        %% R.a mapped to Y.a
  %struct r' : R' = {%include r.}. %% r'(R.c : R.a) = r(R.c : R.a) = r.c : a
}.

%% structures of signatures that have includes
%sig QQQ = {
   q : type.
   %struct r : R.
   %struct r'  : R' = {R.a := q. R'.a' := q.}.
   %struct r'' : R'' = {%include r. R'.a' := q.}.
   %% referring to symbols included into an instantiated signature
   c : r''.R'.a'.
   d : r''.R.a.
   
}.

%% multiple includes: %% S12 includes S0 twice
%sig S0  = {a : type. c: a. a' = a.}.
%sig S1  = {%include S0 %open a'. c: S0.a.}.
%sig S2  = {%include S0.          c: S0.a.}.
%sig S12 = {
   %include S1.
   %include S2.
   %% c' = c.    %% reference to c would be ambiguous between S1.c and S2.c
   c : a'.       %% reference to a' is inambiguously S0.a'
   c' = c.       %% reference to c is resolved locally
}.
%sig SX  = {a : type. c : a.}.
%view V0  : S0  -> SX = {a := a. c := c.}.
%sig SY  = {%struct k: SX. %struct k' = V0 k.}.
%view V1  : S1  -> SY = {%include V0 k. c := k.c.}.
%view V2  : S2  -> SY = {%include k'. c := k'.c.}.
%% V12 includes two views from S0 to SY: V0 SY.k and SY.k'
%% they must be equal, which is seen after definition expansion
%view V12 : S12 -> SY = {%include V1. %include V2. c := k.c.}.

%% testing opens
%sig Z = {
  %include Y.
  %include R %open a c %as c'.
  d = c' : a.
  %struct s : S %open a' b'.
  e = b' : a'.
  k : r.a. %% failed lookup, retried in Y.
}.

%% testing nested signatures and views
%sig L0 = {
  c : a.          %% a refers to toplevel a
  a : type.
  c' : a.         %% a refers to L0.a
  %sig L1 = {
    c : a.        %% a refers to L0.a
    a : type.
    d1 : a.       %% a refers to L1.a
    d0 : L0.a.    %% a refers to L0.a
    %sig L11 = {a:type.}.
  }.
  b : type.
  %sig L2 = {
     a : b.
     %% c : L1.a.   %% fails, L1 invisible
     %include L1.
     %%struct l : L11. %% could be permitted if ancestors and included signatures were unified internally
     c : L1.a.
  }.
  %view L1-2 : L1 -> L2 = {
     c  := L0.L1.c.
     a  := b.
     d1 := a.
     d0 := L1.c.
  }.
}.

%% testing implicit morphisms
%% b : type. %% makes the "upward view" c below fail 
%sig A = {}.
%sig B = {
  %struct %implicit x : X.
}.
%view %implicit c : A -> X = {}.
%sig C = {
  %struct a : A.
}.
%sig D = {
  %struct b : B.
  %struct c : C = {%struct a := b.}. %% b is coerced to c B.x b.
}.

%% testing dynamic loading of modules   
%sig R3 = {
  %include R.
  %include t2.R2.
  %struct r : t2.R2.
  b : R.a.
  c : t2.R2.a.
  d : r.a.
  e : r.r.a.
}.

%sig R3' = {
   %include t3.ReadTwice.
}.

%% testing logical relations
%sig LS = {
    a: type.
    c : a.
    f : a -> a.
    b : a -> a -> type.
    g : b XX (f XX). 
}.
%sig LT = {
   a1: type. c1: a1.
   a2: type. c2: a2.
   j : a1 -> a2 -> type.
   p : j c1 c2.
   q : {f1}{f2} j XX XY -> j (f1 XX) (f2 XY).
   u: type.
   *: u.
   eq: u -> u -> type.
   uniq : eq UU *.
}.
%view m1 : LS -> LT = {
   a := a1. c := c1. f := [x] x.
   b := [x][y] u. g := [XX] *.
}.
%view m2 : LS -> LT = {
   a := a2. c := c2. f := [x] c2.
   b := [x][y] (u -> u). g := [XX] ([x] x).
}.
%rel Rho : m1 -> m2 = {
   a := j.                    %% j : m1(a) -> m2(a) -> type.
   c := p.                    %% p : Rho(a) m1(c) m2(c)
   f := [x1][x2][v: j x1 x2] (q ([x]x) ([x]c2) v). %% f maps related arguments to related results
   b := [x1][x2][v: j x1 x2][y1][y2][w: j y1 y2][b1][b2] {x:u} eq (b2 x) b1.
        %% b1:(m1(b) x1 y1) and b2:(m2(b) x2 y2) are related if b2 is the constant function returning b1 (still quite a trivial example)
   g := [x1][x2][v: j x1 x2] [x:u] uniq.           %% g maps related arguments to related results
}.
%% testing module system for logical relations: extend LS to LS', then adapt m1, m2, Rho accordingly
%sig LS' = {
   %include LS.
   %struct ls : LS.
   q : type.
   c : q.
}.
%view m1' : LS' -> LT = {
   %include m1.
   %struct ls := m1.
   q := u.
   c := *.
}.
%view m2' : LS' -> LT = {
   %include m2.
   %struct ls := m2.
   q := u.
   c := *.
}.

%* testing warnings and error recovery *%

%* two preserved in a row - warning *%
%sig QW =  {a:type.}.
%sig QW' = {a:type.}.
%% a partial view
%view QW'' : QW -> QW' = {}.
%% if a partial view is used lateron, we get a real an unrecoverable error for now
%% %sig QW''' = {%include QW'. %struct s = QW''.}. 

%sig PQ = {
   a : type.
   c : a.
   f : a -> a.
   d : a = f.
   e : a.
}.

%.
%rel Rho' : m1' -> m2' = {
   %include Rho.
   %struct ls := Rho.  %% This would type-check if equality of morphisms were implemented better
   q := [x][y] eq x y.                  
   c := uniq.
}.

%% testing pre-functors
%sig Domain = {
   a : type.
}.
%sig Codomain = {
   b : type.
   c : b.
}.
%sig Functor = {
   %sig Interface = {
      %include Domain.
      param : a.
   }.
   %view Body : Codomain -> Interface = {
      b := a.
      c := param.
   }.
}.