%% predefined universe containing all types,

%% superclass of all other classes

class 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 : Type-) . t ->? Unit

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

op true, false : Unit ->? Unit

op __/\__, __\/__, __=>__, __if__, __<=>__ : Unit � Unit ->? Unit

op not : Unit ->? Unit

op : forall s : Type . s � s ->? Unit

%% =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 : forall s : Type . s ->? Unit

var x : s

program def = \ x : s . ()

%% def is also total (identical to tt)

program tt = \ x : s . ()

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

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

%% total function type

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

type s->t < s ->? t

. (op __=__ : forall a : Type . a � a ->? Unit) (__ in s -> t,

\ f : s ->? t . all (\ x : s . def f (x)))

%% total functions

op __res__ : s � t ->? s = (var x : s)

op fst : s � t ->? s = (var x : s)

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

%% trivial because its the strict function property

. (op __=__ : forall a : Type . a � a ->? Unit) (\ (x : s,

y : t) . def (x res y),

\ (x : s, y : t) . (def y) und (def x))

. (op __=__ : forall a : Type . a � a ->? Unit) ((op fst : s �

t ->? s),

(op __res__ : s � t ->? s))

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

%% Internal Logic

op eq : forall s : Type . s � s ->? Unit

. (op __=__ : forall a : Type . a � a ->? Unit) (\ x : s . eq (x,

x),

(op tt : forall s : Type . s ->? Unit))

. (op __=__ : forall a : Type . a � a ->? Unit) (\ (x, y : s) . x

res eq (x, y),

\ (x, y : s) . y res eq (x, y))

%% 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

program all(p : s ->? Unit) : Unit ->? Unit =

(op eq : forall s : Type . s � s ->? Unit) ((var p : s ->? Unit),

(op tt : forall s : Type . s ->? Unit))

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

program And(x : _var_37, y : Unit ->? Unit) : Unit ->? Unit =

t1 () und t2 ()

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

program __ impl __

(x, y : Pred Unit) : Unit ->? Unit : Unit ->? Unit

= eq (x, x And y)

program __ or __ (x, y : Pred Unit) : Unit ->? Unit : Unit ->? Unit

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

program ex(p : s ->? Unit) : Unit ->? Unit =

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

program ff () : Unit ->? Unit : Unit ->? Unit =

all (\ r : Pred Unit . r ())

program neg(r : Unit ->? Unit) : Unit ->? 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; op __<<=__ : forall c : Cpo . c � c ->? Unit; ;

op isChain(s : nat -> c) :? Unit = all

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

op isBound(x : c, s : nat -> c) :? Unit = all

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

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

class Pcpo < Cpo

{var p : Pcpo; op bottom : forall p : Pcpo . 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 (__<<=__)((x1 : _var_42, y1 : _var_43),

(x2 : _var_44, y2 : _var_45))

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

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

type Unit : Pcpo

%% Pcont

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

type c-->?d < c ->? d

. (op __=__ : forall a : Type . a � a ->? Unit) (__ in c -->? d,

\ f : c ->? d . all

(\ (x, y : c) . (def (f x) und x

<<= y)

impl def (f y))

und all

(\ s : nat -> c . (isChain (s) und

def f

(sup (s)))

impl ex

(\ m : nat . def

f

(s

(m))

und

eq

(sup

(\ n : nat .! f

(s

(n

+

m))),

f

(sup

(s))))))

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

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

%% Tcont

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

type c-->d < c -->? d

. (op __=__ : forall a : Type . a � a ->? Unit) (__ in c --> d,

\ f : c -->? d . all (\ x : c . def f (x)))

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

program (__<<=__)(f : _var_59, g : _var_60) = f <<= [c -->? d] g

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

op Y : forall p : Pcpo . (p -->? p) --> p

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

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

%% user stuff

free type bool ::= true |

false

type bool : Flatcpo

type nat : Flatcpo

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

Cpo

Flatcpo < Cpo

Pcpo < Cpo

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

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

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

Pred : (Type -> Type, Type- -> Type) := \ a : Type . a ->? Unit

Pred__ : Type- -> Type := \ (t : Type)(t : Type-) . t ->? Unit

Unit : (Type, Pcpo)

__*__ : (Type+ -> Type+ -> Type, Pcpo+ -> Pcpo+ -> Pcpo,

Cpo+ -> Cpo+ -> Cpo)

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

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

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

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

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

bool : (Type, Flatcpo) %[free type __ ::=

true : -> __

false : -> __]%

c : Cpo %(var)%

c-->d : Type < c -->? d

c-->?d : Type < c ->? d

d : Cpo %(var)%

f : Flatcpo %(var)%

nat : (Type, Flatcpo)

p : Pcpo %(var)%

s : Type < ? s %(var)%

s->t : Type < s ->? t

t : Type %(var)%

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

Y : forall p : Pcpo . (p -->? p) --> p

__/\__ : Unit � Unit ->? Unit

__<<=__ : forall c : Cpo . c � c ->? Unit

__<=>__ : Unit � Unit ->? Unit

__=__ : forall a : Type . a � a ->? Unit

__=>__ : Unit � Unit ->? Unit

__=e=__ : forall a : Type . a � a ->? Unit

__\/__ : Unit � Unit ->? Unit

__if__ : Unit � Unit ->? Unit

__res__ : s � t ->? s = \ (x : s, y : t) .! (var x : s)

bottom : forall p : Pcpo . p

def : forall s : Type . s ->? Unit

def__ : forall a : Type . a ->? Unit

eq : forall s : Type . s � s ->? Unit

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

false : bool %(construct bool)%

: Unit ->? Unit

fst : s � t ->? s = \ (x : s, y : t) .! (var x : s)

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

if__then__else__ : forall a : Type . Unit � a � a ->? a

not : Unit ->? Unit

not__ : Unit ->? Unit

sup : forall c : Cpo . (nat -> c) ->? c

true : bool %(construct bool)%

: Unit ->? Unit

tt : forall s : Type . s ->? Unit

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

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

(op __=__ : forall a : Type . a � a ->? Unit) (__ in s -> t,

\ f : s ->? t . all (\ x : s . def f (x))) %()%

(op __=__ : forall a : Type . a � a ->? Unit) (\ (x : s,

y : t) . def (x res y),

\ (x : s, y : t) . (def y) und (def x)) %()%

(op __=__ : forall a : Type . a � a ->? Unit) ((op fst : s �

t ->? s),

(op __res__ : s � t ->? s)) %()%

(op __=__ : forall a : Type . a � a ->? Unit) (\ x : s . eq (x,

x),

(op tt : forall s : Type . s ->? Unit)) %()%

(op __=__ : forall a : Type . a � a ->? Unit) (\ (x, y : s) . x

res eq (x, y),

\ (x, y : s) . y res eq (x, y)) %()%

(op __=__ : forall a : Type . a � a ->? Unit) (__ in c -->? d,

\ f : c ->? d . all

(\ (x, y : c) . (def (f x) und x <<=

y)

impl def (f y))

und all

(\ s : nat -> c . (isChain (s) und

def f (sup (s)))

impl ex

(\ m : nat . def f

(s

(m))

und

eq

(sup

(\ n : nat .! f

(s

(n

+

m))),

f

(sup

(s)))))) %()%

(op __=__ : forall a : Type . a � a ->? Unit) (__ in c --> d,

\ f : c -->? d . all (\ x : c . def f (x))) %()%

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

Error (line 4, column 7) illegal universe class declaration 'Type'

Hint (line 6, column 5) is type variable 's'

Hint (line 6, column 7) is type variable 't'

Warning (line 11, column 6) redeclared type 'Unit'

Error (line 14, column 44) incompatible kind of: t ->? Unit

expected: Type

found: Type -> Type

Warning (line 15, column 16) redeclared type 't'

Error (line 22, column 8) wrong type scheme of '__=__'

expected: forall a : Type . a � a ->? Unit

found: forall s : Type . s � s ->? Unit

Error (line 46, column 11) unexpected mixfix token: und

Error (line 46, column 9) no toplevel pattern '__ und __ (x, y : Unit) : Unit : Unit'

Error (line 54, column 3) expected further mixfix token: ["/\\","<=>","=","=>","=e="]

Error (line 54, column 42) ambiguous mixfix term

def f x

(def__)(f) x

Error (line 54, column 32) unexpected mixfix token: all

Error (line 65, column 18) ambiguous mixfix term

def ((__res__)(x, y))

(def__)((__res__)(x, y))

Error (line 65, column 59) unexpected mixfix token: und

Error (line 75, column 15) ambiguous mixfix term

(__res__)(x, eq (x, y))

(__res__)(x, eq) (x, y)

Error (line 75, column 44) ambiguous mixfix term

(__res__)(y, eq (x, y))

(__res__)(y, eq) (x, y)

Warning (line 85, column 6) redeclared type 's'

Error (line 90, column 45) unexpected mixfix token: t1

Error (line 93, column 11) unexpected mixfix token: impl

Error (line 93, column 53) unexpected mixfix token: x

Error (line 95, column 11) unexpected mixfix token: or

Error (line 96, column 19) unexpected mixfix token: x

Error (line 95, column 48) unexpected mixfix token: all

Error (line 99, column 32) unexpected mixfix token: impl

Error (line 99, column 17) unexpected mixfix token: all

Error (line 98, column 39) unexpected mixfix token: all

Error (line 101, column 13) unexpected mixfix token: )

Error (line 101, column 29) unexpected mixfix token: all

Error (line 103, column 44) unexpected mixfix token: impl

Error (line 108, column 51) unexpected mixfix token: impl

Error (line 108, column 22) unexpected mixfix token: all

Error (line 108, column 3) unexpected mixfix token: all

Warning (line 115, column 13) redundant universe class

Hint (line 117, column 5) is type variable 'c'

Error (line 121, column 3) unexpected mixfix token: all

Error (line 122, column 31) unexpected mixfix token: und

Error (line 122, column 3) unexpected mixfix token: all

Error (line 123, column 31) unexpected mixfix token: und

Error (line 123, column 3) unexpected mixfix token: all

Error (line 125, column 55) unexpected mixfix token: Suc

Error (line 125, column 32) unexpected mixfix token: all

Error (line 126, column 50) ambiguous mixfix term

s ((__<<=__)(n, x))

(__<<=__)(s n, x)

Error (line 126, column 38) unexpected mixfix token: all

Error (line 131, column 42) unexpected mixfix token: isBound

Error (line 130, column 32) unexpected mixfix token: impl

Error (line 130, column 3) unexpected mixfix token: all

Error (line 134, column 20) unexpected mixfix token: isChain

Error (line 134, column 3) unexpected mixfix token: all

Hint (line 139, column 5) is type variable 'p'

Error (line 143, column 3) unexpected mixfix token: all

Hint (line 148, column 6) is type variable 'f'

Error (line 150, column 15) unexpected mixfix token: [

Hint (line 153, column 5) is type variable 'c'

Warning (line 153, column 5) redeclared type 'c'

Hint (line 153, column 8) is type variable 'd'

Error (line 159, column 45) unexpected mixfix token: und

Error (line 170, column 4) expected further mixfix token: ["/\\","<<=","<=>","=","=>"]

Error (line 171, column 35) unexpected mixfix token: und

Error (line 174, column 45) unexpected mixfix token: +

Error (line 173, column 40) unexpected mixfix token: und

Error (line 172, column 28) unexpected mixfix token: isChain

Error (line 171, column 9) unexpected mixfix token: all

Error (line 176, column 16) unexpected mixfix token: [

Error (line 182, column 4) expected further mixfix token: ["/\\","<<=","<=>","=","=>"]

Error (line 182, column 46) ambiguous mixfix term

def f x

(def__)(f) x

Error (line 182, column 36) unexpected mixfix token: all

Error (line 186, column 25) unexpected mixfix token: [

Error (line 193, column 32) unexpected mixfix token: impl

Error (line 192, column 40) unexpected mixfix token: und

Error (line 192, column 3) unexpected mixfix token: all