%% predefined universe containing all types,

%% superclass of all other classes

class Type < Type

var s : Type; t : Type

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% invisible type "Unit" for formulae

type Unit

%% flat cpo with bottom

%% type aliases

type Pred __ : Type -> Type := \ t : Type- . t ->? Unit

type ? __ := \ t : Type . Unit ->? t

pred true, false : Unit

pred __/\__, __\/__, __=>__, __if__, __<=>__ : Unit * Unit

pred not : Unit

pred __=__ : s * s

%% =e=

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% (builtin) type (constructors)

type __->?__ : Type- -> Type+ -> Type

%% nested pairs are different from n-tupels (n > 2)

type __*__ : Type+ -> Type+ -> Type

type : Type+ -> Type+ -> Type+ -> Type

%% ...

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% "pred p args = e" abbreviates "op p args :? unit = e"

%% CASL requires "<=>" for pred-defn and disallows "()" as result

op def, tt : Pred s

var x : s

program (op def[_var_3_v3]

: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))

= \ (var x : s) : s_v1 . ()

%% def is also total (identical to tt)

program (op tt[_var_6_v6]

: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))

= \ (var x : s) : s_v1 . ()

%% tt is total "op tt(x: s): unit = ()"

program __ und __ (x, y : Unit) : Unit = ()

%% total function type

type __->__ : Type- -> Type+ -> Type

type __->__(s : Type)(t : Type) < s_v1 ->? t_v2

%% total functions

op __res__ : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1

= \ (var x : s, var y : t) .! (var x : s)

op fst : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1

= \ (var x : s, var y : t) .! (var x : s)

program snd (x : s, y : t) : t = y

%% trivial because its the strict function property

. (fun __=__[_var_16_v16 * _var_17_v17 ->? _var_16_v16]

: forall s : Type . s_v-1 * s_v-1 ->? Unit)

(op fst[_var_16_v16; _var_17_v17]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1,

op __res__[_var_16_v16; _var_17_v17]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Internal Logic

pred eq : s * s

. (fun __=__[_var_28_v28 ->? Unit]

: forall s : Type . s_v-1 * s_v-1 ->? Unit)

(\ (var x : s) : _var_28_v28

. (pred eq[s] : forall s : Type . s_v-1 * s_v-1)

(var x : s, var x : s),

op tt[_var_28_v28] : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))

. (fun __=__[s * s_v1 ->? s]

: forall s : Type . s_v-1 * s_v-1 ->? Unit)

(\ (var x : s, var y : s_v1)

. (op __res__[s; Unit]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)

(var x : s,

(pred eq[s] : forall s : Type . s_v-1 * s_v-1)

(var x : s, var y : s_v1)),

\ (var x : s, var y : s_v1)

. (op __res__[s; Unit]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)

(var y : s_v1,

(pred eq[s] : forall s : Type . s_v-1 * s_v-1)

(var x : s, var y : s_v1)))

%% then %def

%% notation "\ ." abbreviates "\bla:unit."

%% where "bla" is never used, but only "()" instead

%% for type inference

%% an implicit cast from s to ?s of a term "e" yields the term "\ . e"

type s < ? s_v1

program all (p : Pred (s)) : Pred Unit = eq (p, tt)

%% the cast from ?s to s is still done manually here (for the strict "und")

program And (x, y : Pred Unit) : Pred Unit = t1 () und t2 ()

%% use "And" instead of "und" to avoid cast from "?unit" to "unit"

program __ impl __ (x, y : Pred Unit) : Pred Unit = eq (x, x And y)

program __ or __ (x, y : Pred Unit) : Pred Unit =

all (\ r : Pred Unit . ((x impl r) und (y impl r)) impl r)

program ex (p : Pred (s)) : Pred Unit =

all (\ r : Pred Unit . all (\ x : s . p (x) impl r) impl r)

program ff () : Pred Unit = all (\ r : Pred Unit . r ())

program neg (r : Pred Unit) : Pred Unit = r impl ff

%% the type instance for the first "eq" should be "?t"

%% this is explicitely enforced by "\ .f(x)"

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"

type nat

class Cpo < Type

{var c : Cpo; pred __<<=__ : c * c; ;

pred isChain(s : nat -> c_v66) :? Unit

= all (\ n : nat . s (n) <<= s (Suc (n)));

pred isBound(x : c_v66; s : nat -> c_v66) :? Unit

= all (\ n : nat . s (n) <<= x);

op sup : (nat -> c) ->? c;}

class Pcpo < Cpo

{var p : Pcpo; op bottom : p;}

class instance Flatcpo < Cpo

{var f : Flatcpo; program __ <<= [f] __ = eq}

var c : Cpo; d : Cpo

type instance __*__ : Cpo+ -> Cpo+ -> Cpo

var x1 : c; x2 : c; y1 : d; y2 : d

program (pred __<<=__[c * d] : forall c : Cpo . c_v-1 * c_v-1)

((var x1 : c, var y1 : d), (var x2 : c, var y2 : d))

= (x1 <<= x2) und (y1 <<= y2)

type instance __*__ : Pcpo+ -> Pcpo+ -> Pcpo

type Unit : Pcpo

%% Pcont

type instance __-->?__ : Cpo- -> Cpo+ -> Pcpo

type __-->?__(c : Cpo)(d : Cpo) < c_v66 ->? d_v71

program f <<= [c -->? d] g =

all (\ x : c . def (f x) impl f (x) <<= g (x))

%% Tcont

type instance __-->__ : Cpo- -> Cpo+ -> Cpo

type __-->__(c : Cpo)(d : Cpo) < c_v66 -->? d_v71

var f : c --> d; g : c --> d

program (pred __<<=__[c --> d] : forall c : Cpo . c_v-1 * c_v-1)

(var f : c --> d, var g : c --> d)

= f <<= [c -->? d] g

type instance __-->__ : Cpo- -> Pcpo+ -> Pcpo

op : (p -->? p) --> p

op undefined : c -->? p = Y (\ x : c -->? p .! x)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% user stuff

free type bool ::= true |

false

type bool : Flatcpo

type nat : Flatcpo

%% Classes ---------------------------------------------------------------

Cpo < Type

Flatcpo < Cpo

Pcpo < Cpo

%% Type Constructors -----------------------------------------------------

Logical : Type := Unit ->? Unit

Pred : Type -> Type := \ a : Type . a_v-1 ->? Unit

Unit : Pcpo := Unit

__*__

: (Cpo+ -> Cpo+ -> Cpo, Pcpo+ -> Pcpo+ -> Pcpo,

Type+ -> Type+ -> Type)

__-->__

: (Cpo- -> Cpo+ -> Cpo, Cpo- -> Pcpo+ -> Pcpo,

Type- -> Type+ -> Type) < c_v66 -->? d_v71

__-->?__

: (Cpo- -> Cpo+ -> Pcpo, Type- -> Type+ -> Type) < c_v66 ->? d_v71

__->__ : Type- -> Type+ -> Type < s_v1 ->? t_v2

__->?__ : Type- -> Type+ -> Type

bool

: Flatcpo

%[free type bool

::= true : bool

false : bool]%

c : Cpo %(var_66)%

d : Cpo %(var_71)%

f : Flatcpo %(var_70)%

nat : Flatcpo

p : Pcpo %(var_69)%

s : Type %(var_1)%

t : Type %(var_2)%

%% Assumptions -----------------------------------------------------------

__/\__ : Unit * Unit ->? Unit %(fun)%

__<<=__ : forall c : Cpo . c_v-1 * c_v-1 ->? Unit %(pred)%

__<=>__ : Unit * Unit ->? Unit %(fun)%

__=__ : forall s : Type . s_v-1 * s_v-1 ->? Unit %(fun)%

__=>__ : Unit * Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__\/__ : Unit * Unit ->? Unit %(fun)%

__if__ : Unit * Unit ->? Unit %(fun)%

__res__

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1

%(op)% = \ (var x : s, var y : t) .! (var x : s)

__when__else__

: forall a : Type . a_v-1 * Unit * a_v-1 ->? a_v-1 %(fun)%

bottom : forall p : Pcpo . p_v-1 %(fun)%

def : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit) %(op)%

def__ : forall a : Type . a_v-1 ->? Unit %(fun)%

eq : forall s : Type . s_v-1 * s_v-1 ->? Unit %(pred)%

f : c --> d %(var)%

false

: bool %(construct bool)%

: Unit ->? Unit %(pred)%

: Unit %(fun)%

fst

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1

%(op)% = \ (var x : s, var y : t) .! (var x : s)

g : c --> d %(var)%

not : Unit ->? Unit %(pred)%

not__ : Unit ->? Unit %(fun)%

sup : forall c : Cpo . (nat -> c_v-1) ->? c_v-1 %(op)%

true

: bool %(construct bool)%

: Unit ->? Unit %(pred)%

: Unit %(fun)%

tt : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit) %(op)%

x : s %(var)%

x1 : c %(var)%

x2 : c %(var)%

y1 : d %(var)%

y2 : d %(var)%

�__ : Unit ->? Unit %(fun)%

%% Sentences -------------------------------------------------------------

program (op def[_var_3_v3]

: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))

= \ (var x : s) : s_v1 . () %(pe_def)%

program (op tt[_var_6_v6]

: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))

= \ (var x : s) : s_v1 . () %(pe_tt)%

forall x : s; y : t

. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op __res__ : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)

(var x : s, var y : t),

var x : s) %(def___res__)%

forall x : s; y : t

. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op fst : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)

(var x : s, var y : t),

var x : s) %(def_fst)%

(fun __=__[_var_16_v16 * _var_17_v17 ->? _var_16_v16]

: forall s : Type . s_v-1 * s_v-1 ->? Unit)

(op fst[_var_16_v16; _var_17_v17]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1,

op __res__[_var_16_v16; _var_17_v17]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)

(fun __=__[_var_28_v28 ->? Unit]

: forall s : Type . s_v-1 * s_v-1 ->? Unit)

(\ (var x : s) : _var_28_v28

. (pred eq[s] : forall s : Type . s_v-1 * s_v-1)

(var x : s, var x : s),

op tt[_var_28_v28] : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))

(fun __=__[s * s_v1 ->? s]

: forall s : Type . s_v-1 * s_v-1 ->? Unit)

(\ (var x : s, var y : s_v1)

. (op __res__[s; Unit]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)

(var x : s,

(pred eq[s] : forall s : Type . s_v-1 * s_v-1)

(var x : s, var y : s_v1)),

\ (var x : s, var y : s_v1)

. (op __res__[s; Unit]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)

(var y : s_v1,

(pred eq[s] : forall s : Type . s_v-1 * s_v-1)

(var x : s, var y : s_v1)))

free type bool

::= true : bool

false : bool %(ga_bool)%

%% Diagnostics -----------------------------------------------------------

*** Error 4.7, illegal universe class declaration 'Type'

*** Hint 6.5, is type variable 's'

*** Hint 6.7, is type variable 't'

*** Hint 11.6, redeclared type 'Unit'

*** FatalError 14.11, illegal type pattern argument: __

*** FatalError 15.8, illegal type pattern argument: __

*** Error 17.6, illegal overloading of predefined identifier 'true'

*** Error 17.12, illegal overloading of predefined identifier 'false'

*** Error 19.9, illegal overloading of predefined identifier '__/\__'

*** Error 19.17, illegal overloading of predefined identifier '__\/__'

*** Error 19.25, illegal overloading of predefined identifier '__=>__'

*** Error 19.33, illegal overloading of predefined identifier '__if__'

*** Error 19.40, illegal overloading of predefined identifier '__<=>__'

*** Error 22.8, illegal overloading of predefined identifier '__=__'

*** Hint 27.8, redeclared type '__->?__'

*** Hint 30.8, redeclared type '__*__'

*** FatalError 31.6, illegal type pattern: __ * __ * __

*** Error 46.11, unexpected mixfix token: und

*** Hint 50.8, redeclared type '__->__'

*** Error 52.8, incompatible kind of: __->__

expected: Type- -> Type+ -> Type

found: Type -> Type -> Type

*** Error 54.42, ambiguous mixfix term

def__(f(x))

def(f)(x)

*** Error 54.32, unexpected mixfix token: all

*** Error 54.6, unexpected mixfix token: :

*** Hint 60.9, no type match for: snd

with type: '_var_9_v9 ->? t_v2' (60.14)

known types:

*** Hint 60.9, wrong result type 't_v2' (60.28)

for application 'snd(x : s_v1, var y : t_v2)'

*** Error 60.9, no typing for 'snd(x : s_v1, var y : t_v2) : t_v2'

*** Error 65.18, ambiguous mixfix term

def(__res__(x, y))

def__(__res__(x, y))

*** Error 65.59, unexpected mixfix token: und

*** Hint 85.6, redeclared type 's'

*** Error 85.6, merge: TypeVarDefn of 's'

*** Error 85.11, illegal supertype for variable '? s_v1'

*** Hint 87.9, no type match for: all

with type: '_var_59_v59 ->? Unit ->? Unit' (87.14)

known types:

*** Hint 87.9, wrong result type 'Unit ->? Unit'

for application 'all(var p : s_v1 ->? Unit)'

*** Error 87.9, no typing for 'all(var p : s_v1 ->? Unit) : Unit ->? Unit'

*** Hint 90.9, no type match for: And

with type: '_var_60_v60 ->? Unit ->? Unit' (90.14)

known types:

*** Hint 90.9, wrong result type 'Unit ->? Unit'

for application 'And(x, var y : Unit ->? Unit)'

*** Error 90.9, no typing for 'And(x, var y : Unit ->? Unit) : Unit ->? Unit'

*** Error 93.11, unexpected mixfix token: impl

*** Error 95.11, unexpected mixfix token: or

*** Hint 98.9, no type match for: ex

with type: '_var_61_v61 ->? Unit ->? Unit' (98.13)

known types:

*** Hint 98.9, wrong result type 'Unit ->? Unit'

for application 'ex(var p : s_v1 ->? Unit)'

*** Error 98.9, no typing for 'ex(var p : s_v1 ->? Unit) : Unit ->? Unit'

*** Hint 101.9, no type match for: ff

with type: '_var_62_v62 ->? Unit ->? Unit'

known types:

*** Hint 101.9, wrong result type 'Unit ->? Unit'

for application 'ff()'

*** Error 101.9, no typing for 'ff() : Unit ->? Unit'

*** Hint 103.9, no type match for: neg

with type: '_var_63_v63 ->? Unit ->? Unit' (103.14)

known types:

*** Hint 103.9, wrong result type 'Unit ->? Unit'

for application 'neg(var r : Unit ->? Unit)'

*** Error 103.9, no typing for 'neg(var r : Unit ->? Unit) : Unit ->? Unit'

*** Error 108.51, unexpected mixfix token: impl

*** Error 108.22, unexpected mixfix token: all

*** Error 108.3, unexpected mixfix token: all

*** Hint 117.5, is type variable 'c'

*** Error 121.3, unexpected mixfix token: all

*** Error 122.31, unexpected mixfix token: und

*** Error 122.3, unexpected mixfix token: all

*** Error 123.31, unexpected mixfix token: und

*** Error 123.3, unexpected mixfix token: all

*** Error 125.55, unexpected mixfix token: Suc

*** Error 125.32, unexpected mixfix token: all

*** Error 126.38, unexpected mixfix token: all

*** Error 131.42, unexpected mixfix token: isBound

*** Error 130.32, unexpected mixfix token: impl

*** Error 130.3, unexpected mixfix token: all

*** Error 134.20, unexpected mixfix token: isChain

*** Error 134.3, unexpected mixfix token: all

*** Hint 139.5, is type variable 'p'

*** Error 141.4, illegal overloading of predefined identifier 'bottom'

*** Error 143.3, unexpected mixfix token: all

*** Hint 148.6, is type variable 'f'

*** Error 150.15, unexpected mixfix token: [

*** Hint 153.5, is type variable 'c'

*** Hint 153.5, redeclared type 'c'

*** Hint 153.8, is type variable 'd'

*** Error 159.45, unexpected mixfix token: und

*** Error 169.9, incompatible kind of: __-->?__

expected: Type- -> Type+ -> Type

found: Type -> Type -> Type

*** Error 171.35, unexpected mixfix token: und

*** Error 174.45, unexpected mixfix token: +

*** Error 173.40, unexpected mixfix token: und

*** Error 172.28, unexpected mixfix token: isChain

*** Error 171.9, unexpected mixfix token: all

*** Error 170.7, unexpected mixfix token: :

*** Hint 10.18, no type match for: __::__

with type: '_var_91_v91 ->? _var_90_v90 ->? _var_81_v81' (176.17)

known types:

*** Hint 10.18, wrong result type '_var_90_v90 ->? _var_81_v81' (176.27)

for application '__::__(c(var -->? : _var_82_v82)(var d : _var_83_v83), [])'

*** Hint 10.18, wrong result type '_var_81_v81' (176.11)

for application '__::__(c(var -->? : _var_82_v82)(var d : _var_83_v83), [])

(var g : _var_84_v84)'

*** Error 176.13, wrongly typed application '__<<=__

(var f : _var_81_v81,

__::__(c(var -->? : _var_82_v82)(var d : _var_83_v83), [])

(var g : _var_84_v84))'

*** Error 176.13, no typing for '__<<=__(var f : _var_81_v81,

__::__(c(var -->? : _var_82_v82)(var d : _var_83_v83), [])

(var g : _var_84_v84))'

*** Error 181.9, incompatible kind of: __-->__

expected: Type- -> Type+ -> Type

found: Type -> Type -> Type

*** Error 182.46, ambiguous mixfix term

def__(f(x))

def(f)(x)

*** Error 182.36, unexpected mixfix token: all

*** Error 182.7, unexpected mixfix token: :

*** Error 186.26, unexpected mixfix token: c

*** Error 190.9, incompatible kind of: p_v69 -->? p_v69

expected: Cpo-

found: Type

*** Error 193.32, unexpected mixfix token: impl

*** Error 192.27, unexpected mixfix token: Y

*** Error 192.3, unexpected mixfix token: all

*** Error 195.27, unexpected mixfix token: Y

*** Error 200.20, illegal overloading of predefined identifier 'true'

*** Error 200.27, illegal overloading of predefined identifier 'false'