HasCASL/test/BasicSpec.hascasl.output

	BasicSpec.hascasl.output revision 413db961f13e112716509b6d61d7a7bbf50c98b2
class Type < Type
var t : Type
class TYPE < Type
type Unit : TYPE
class a, b, c < Type
class a, b, c < Type;
      a < b
type s : c
pred tt : s
var x : s
program (pred tt : s) = \ (var x : s) . () : s ->? Unit
pred eq : s * s
type s < ? s
forall x : t; y : t
. %(..)%
  (var x : t) = (var y : t)
type s
op a : (? s)
type Data1 ::= a |
               b |
               c
type Data2 ::= Cons21 (Data1; Data2) |
               Cons22 (Data2; Data1) |
               type Data1
type Data3 ::= Cons31 (sel1 :? Data1; sel2 :? Data2) |
               Cons32 (sel2 :? Data2; sel1 :? Data1)
type Data4 ::= Cons41 (sel1 :? Data1; sel2 :? Data2)? |
               Cons42 (sel2 :? Data2; sel1 :? Data1)?
. true
forall x : s
forall x : s
%% Classes ---------------------------------------------------------------
TYPE < Type
a < b
b < Type
c < Type
%% Type Constructors -----------------------------------------------------
? : +Type -> Type
Data1
  : Type < Data2
     %[type Data1
         ::= a : Data1
             b : Data1
             c : Data1]%
Data2
  : Type
     %[type Data2
         ::= Cons21 : Data1 * Data2 -> Data2 (Data1; Data2)
             Cons22 : Data2 * Data1 -> Data2 (Data2; Data1)
             types Data1]%
Data3
  : Type
     %[type Data3
         ::= Cons31 : Data1 * Data2 -> Data3 (sel1 :? Data1; sel2 :? Data2)
             Cons32 : Data2 * Data1 -> Data3 (sel2 :? Data2; sel1 :? Data1)]%
Data4
  : Type
     %[type Data4
         ::= Cons41 : Data1 * Data2 ->? Data4 (sel1 :? Data1; sel2 :? Data2)
             Cons42 : Data2 * Data1 ->? Data4 (sel2 :? Data2; sel1 :? Data1)]%
Logical : Type := ? Unit
Pred : -Type -> Type := \ a : -Type . a ->? Unit
Unit : (TYPE, Type)
__*__ : +Type -> +Type -> Type
__*__*__ : +Type -> +Type -> +Type -> Type
__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type
__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type
__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)
__-->?__ : -Type -> +Type -> Type < __->?__
__->__ : -Type -> +Type -> Type < __->?__
__->?__ : -Type -> +Type -> Type
s : (Type, c)
%% Type Variables --------------------------------------------------------
t  : Type %(var_1)%
%% Assumptions -----------------------------------------------------------
Cons21 : Data1 * Data2 -> Data2 %(construct Data2)%
Cons22 : Data2 * Data1 -> Data2 %(construct Data2)%
Cons31 : Data1 * Data2 -> Data3 %(construct Data3)%
Cons32 : Data2 * Data1 -> Data3 %(construct Data3)%
Cons41 : Data1 * Data2 ->? Data4 %(construct Data4)%
Cons42 : Data2 * Data1 ->? Data4 %(construct Data4)%
__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=__ : forall a : Type . a * a ->? Unit %(fun)%
__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a * a ->? Unit %(fun)%
__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
__if__ : ? Unit * ? Unit ->? Unit %(fun)%
__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%
a : Data1 %(construct Data1)%
  : ? s %(op)%
b : Data1 %(construct Data1)%
bottom : forall a : Type . a %(fun)%
c : Data1 %(construct Data1)%
def__ : forall a : Type . a ->? Unit %(fun)%
eq : s * s ->? Unit %(pred)%
false : Unit %(fun)%
not__ : ? Unit ->? Unit %(fun)%
sel1
  : Data4 ->? Data1
    %(select from Data4 constructed by
    (Cons42 : Data2 * Data1 ->? Data4,
     Cons41 : Data1 * Data2 ->? Data4))%
  : Data3 ->? Data1
    %(select from Data3 constructed by
    (Cons32 : Data2 * Data1 -> Data3,
     Cons31 : Data1 * Data2 -> Data3))%
sel2
  : Data4 ->? Data2
    %(select from Data4 constructed by
    (Cons42 : Data2 * Data1 ->? Data4,
     Cons41 : Data1 * Data2 ->? Data4))%
  : Data3 ->? Data2
    %(select from Data3 constructed by
    (Cons32 : Data2 * Data1 -> Data3,
     Cons31 : Data1 * Data2 -> Data3))%
true : Unit %(fun)%
tt : s ->? Unit %(pred)%
�__ : ? Unit ->? Unit %(fun)%
%% Variables -------------------------------------------------------------
x : s
y : t
%% Sentences -------------------------------------------------------------
program tt = \ x . () : s ->? Unit
x = y
type Data1
  ::= a : Data1
      b : Data1
      c : Data1
type Data2
  ::= Cons21 : Data1 * Data2 -> Data2 (Data1; Data2)
      Cons22 : Data2 * Data1 -> Data2 (Data2; Data1)
      types Data1
forall x_1_1 : Data1; x_1_2 : Data2
  . (op sel1 : Data3 ->? Data1) (Cons31 (x_1_1, x_1_2)) = x_1_1
forall x_1_1 : Data1; x_1_2 : Data2
  . (op sel2 : Data3 ->? Data2) (Cons31 (x_1_1, x_1_2)) = x_1_2
forall x_1_1 : Data2; x_1_2 : Data1
  . (op sel2 : Data3 ->? Data2) (Cons32 (x_1_1, x_1_2)) = x_1_1
forall x_1_1 : Data2; x_1_2 : Data1
  . (op sel1 : Data3 ->? Data1) (Cons32 (x_1_1, x_1_2)) = x_1_2
type Data3
  ::= Cons31 : Data1 * Data2 -> Data3 (sel1 :? Data1; sel2 :? Data2)
      Cons32 : Data2 * Data1 -> Data3 (sel2 :? Data2; sel1 :? Data1)
forall x_1_1 : Data1; x_1_2 : Data2
  . (op sel1 : Data4 ->? Data1) (Cons41 (x_1_1, x_1_2)) = x_1_1
forall x_1_1 : Data1; x_1_2 : Data2
  . (op sel2 : Data4 ->? Data2) (Cons41 (x_1_1, x_1_2)) = x_1_2
forall x_1_1 : Data2; x_1_2 : Data1
  . (op sel2 : Data4 ->? Data2) (Cons42 (x_1_1, x_1_2)) = x_1_1
forall x_1_1 : Data2; x_1_2 : Data1
  . (op sel1 : Data4 ->? Data1) (Cons42 (x_1_1, x_1_2)) = x_1_2
type Data4
  ::= Cons41 : Data1 * Data2 ->? Data4 (sel1 :? Data1; sel2 :? Data2)
      Cons42 : Data2 * Data1 ->? Data4 (sel2 :? Data2; sel1 :? Data1)
true
%% Diagnostics -----------------------------------------------------------
*** Warning 1.7, void universe class declaration 'Type'
*** Hint 3.5, is type variable 't'
*** Error 7.11, illegal type pattern argument '__'
*** Error 11.16, not a class 'd'
*** Warning 11.7, unchanged class 'a'
*** Warning 11.10, unchanged class 'b'
*** Warning 11.13, unchanged class 'c'
*** Hint 11.19, refined class 'a'
*** Hint 16.7, not a class 's'
*** Hint 18.15, rebound variable 'x'
*** Error 20.12, unexpected mixfix token: res
*** Hint 21.1, no type match for: fst
  with (maximal) type: _v4 ->? s
  known types:

*** Hint 21.1-21.16, untypable application (with result type: s)
 'fst (x : s, (var y : t))'
*** Error 21.22, no typing for 'program fst (x : s, (var y : t)) : s = x'
*** Hint 22.1, no type match for: snd
  with (maximal) type: _v5 ->? t
  known types:

*** Hint 22.1-22.16, untypable application (with result type: t)
 'snd (x : s, (var y : t))'
*** Error 22.22, no typing for 'program snd (x : s, (var y : t)) : t = y'
*** Hint 28.9, no type match for: all
  with (maximal) type: _v6 ->? ? Unit
  known types:

*** Hint 28.9-28.15, untypable application (with result type: ? Unit)
 'all (var p : ? s)'
*** Error 28.33, no typing for 'program all (var p : ? s) : ? Unit = eq (p, tt)'
*** Error 30.40, unexpected mixfix token: t1
*** Error 32.12, unexpected mixfix token: impl
*** Error 32.45, unexpected mixfix token: And
*** Error 34.12, unexpected mixfix token: or
*** Error 35.21, unexpected mixfix token: impl
*** Error 34.44, unexpected mixfix token: all
*** Error 38.32, unexpected mixfix token: impl
*** Error 38.17, unexpected mixfix token: all
*** Error 37.27, unexpected mixfix token: all
*** Error 40.20, unexpected mixfix token: all
*** Hint 45.9, not a class 't'
*** Hint 45.8, rebound variable 'x'
*** Hint 45.16, not a class 't'
*** Hint 57.11, redeclared type 's'
*** Hint 66.22, not a class 's'
*** Hint 66.21, rebound variable 'x'
*** Error 66.25, unexpected mixfix token: e
*** Hint 67.9, not a class 's'
*** Hint 67.8, rebound variable 'x'
*** Error 67.12, unexpected mixfix token: e