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

predfun true, false : Unit ->? Unit

predfun __/\__, __\/__, __=>__, __if__, __<=>__ : Unit �

Unit ->? Unit

predfun not : Unit ->? Unit

predfun __=__ : 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 : forall s : Type . s ->? Unit = \ x : s . ()

%% def is also total (identical to tt)

program tt : forall s : Type . s ->? Unit = \ 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 : Type)(t : Type) < s ->? t

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

%% trivial because its the strict function property

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

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

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

. (predfun __=__ : forall a : Type . a �

a ->? Unit) ((op fst : s � t ->? s),

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

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

%% Internal Logic

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

. (predfun __=__ : forall a : Type . a �

a ->? Unit) (\ x : s . (predfun eq : forall s : Type . s �

s ->? Unit) ((var x : s),

(var x : s)),

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

. (predfun __=__ : forall a : Type . a �

a ->? Unit) (\ (x : _var_45, y : s) . x res eq (x, y),

\ (x : _var_46, 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 : 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) : 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 : Pred (s)) : Pred 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 : 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; predfun __<<=__ : forall c : Cpo . c � c ->? Unit; ;

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

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

predfun 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 __<<=__ : forall c : Cpo . c � c ->? Unit ((x1 : _var_75,

y1 : _var_76),

(x2 : _var_77, y2 : _var_78))

= (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 ->? d

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 -->? d

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

program __<<=__ : forall c : Cpo . c � c ->? Unit (f : _var_103,

g : _var_104)

= 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 .! (var x : c -->? p))

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

%% user stuff

free type bool ::= true |

false

type bool : Flatcpo

type nat : Flatcpo

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

Cpo < Type

Flatcpo < Cpo

Pcpo < Cpo

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

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

Unit : Pcpo := Unit

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

Type+ -> Type+ -> Type)

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

Type- -> Type+ -> Type) < c -->? d

__-->?__ : (Cpo- -> Cpo+ -> Pcpo, Type- -> Type+ -> Type) < c ->? d

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

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

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

bool : Flatcpo %[free type __ ::=

true : -> __

false : -> __]%

c : Cpo %(var)%

d : Cpo %(var)%

f : Flatcpo %(var)%

nat : Flatcpo

p : Pcpo %(var)%

s : Type < ? s %(var)%

t : Type %(var)%

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

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

__/\__ : Unit � Unit ->? Unit %(Pred)%

__<<=__ : forall c : Cpo . c � c ->? Unit %(Pred)%

__<=>__ : Unit � Unit ->? Unit %(Pred)%

__=__ : forall a : Type . a � a ->? Unit %(Pred)%

__=>__ : Unit � Unit ->? Unit %(Pred)%

__=e=__ : forall a : Type . a � a ->? Unit %(Fun)%

__\/__ : Unit � Unit ->? Unit %(Pred)%

__if__ : Unit � Unit ->? Unit %(Pred)%

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

bottom : forall p : Pcpo . p %(Op)%

def : forall s : Type . s ->? Unit %(Op)% = \ x : s . ()

def__ : forall a : Type . a ->? Unit %(Fun)%

eq : forall s : Type . s � s ->? Unit %(Pred)%

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

false : bool %(construct bool)%

: Unit ->? Unit %(Pred)%

: Unit %(Fun)%

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

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

if__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%

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

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

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

true : bool %(construct bool)%

: Unit ->? Unit %(Pred)%

: Unit %(Fun)%

tt : forall s : Type . s ->? Unit %(Op)% = \ x : s . ()

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

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

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

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

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

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

t ->? s),

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

(predfun __=__ : forall a : Type . a �

a ->? Unit) (\ x : s . (predfun eq : forall s : Type . s �

s ->? Unit) ((var x : s),

(var x : s)),

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

(predfun __=__ : forall a : Type . a �

a ->? Unit) (\ (x : _var_45, y : s) . x res eq (x, y),

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

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

FatalError (line 14, column 11) illegal type pattern argument: __

FatalError (line 15, column 8) illegal type pattern argument: __

Warning (line 27, column 8) redeclared type '__->?__'

FatalError (line 31, column 6) illegal type pattern: __ * __ * __

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

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

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

Warning (line 50, column 8) redeclared type '__->__'

Error (line 52, column 8) incompatible kind of: __->__

expected: Type- -> Type+ -> Type

found: Type -> Type -> Type

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 54, column 3) unexpected term '__'

Hint (line 54, column 32) in type of '\ f : s ->? t . all (\ x : s . def f (x))'

type 'Unit'

is not unifiable with type '_var_13 ->? _var_14'

Hint (line 54, column 16) wrong result type 'Unit'

for application '(__=__) (__ in s -> t, \ f : s ->? t . all (\ x : s . def f (x)))'

Error (line 54, column 16) no typing for '(__=__)(__ in s -> t, \ f : s ->? t . all (\ x : s . def f (x)))'

Hint (line 60, column 9) no type match for: snd

with type: '_var_15 ->? t' (line 60, column 28)

known types:

Hint (line 60, column 9) wrong result type 't' (line 60, column 28)

for application 'snd (x : s, y : t)'

Error (line 60, column 9) no typing for 'snd(x : s, y : t) : t'

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 65, column 18) unexpected term 'def (x res y)'

Error (line 65, column 52) unexpected term '(def y) und (def x)'

Error (line 75, column 17) ambiguous mixfix term

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

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

Error (line 75, column 46) ambiguous mixfix term

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

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

Error (line 0, column 0) undeclared type '_var_45'

Error (line 75, column 15) unexpected term 'x res eq (x, y)'

Error (line 0, column 0) undeclared type '_var_46'

Error (line 75, column 44) unexpected term 'y res eq (x, y)'

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

Error (line 85, column 6) merge: TypeVarDefn of 's'

Hint (line 87, column 9) no type match for: all

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

known types:

Hint (line 87, column 9) wrong result type 'Unit ->? Unit'

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

Error (line 87, column 9) no typing for 'all(p : s ->? Unit) : Unit ->? Unit'

Hint (line 90, column 9) no type match for: And

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

known types:

Hint (line 90, column 9) wrong result type 'Unit ->? Unit'

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

Error (line 90, column 9) no typing for 'And(x : _var_62, y : Unit ->? Unit) : Unit ->? Unit'

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

Error (line 93, column 9) unexpected pattern '__ impl __ (x, y : Pred Unit)'

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

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

Error (line 95, column 9) unexpected pattern '__ or __ (x, y : Pred Unit)'

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

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

Hint (line 98, column 9) no type match for: ex

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

known types:

Hint (line 98, column 9) wrong result type 'Unit ->? Unit'

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

Error (line 98, column 9) no typing for 'ex(p : s ->? Unit) : Unit ->? Unit'

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

Error (line 101, column 9) unexpected pattern 'ff ()'

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

Hint (line 103, column 9) no type match for: neg

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

known types:

Hint (line 103, column 9) wrong result type 'Unit ->? Unit'

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

Error (line 103, column 9) no typing for 'neg(r : Unit ->? Unit) : Unit ->? Unit'

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

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 0, column 0) undeclared type '_var_75'

Error (line 0, column 0) undeclared type '_var_76'

Error (line 0, column 0) undeclared type '_var_77'

Error (line 0, column 0) undeclared type '_var_78'

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

Error (line 169, column 9) incompatible kind of: __-->?__

expected: Type- -> Type+ -> Type

found: Type -> Type -> Type

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 170, column 4) unexpected term '__'

Hint (line 171, column 9) in type of '\ 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)))))'

type 'Unit'

is not unifiable with type '_var_94 ->? _var_95'

Hint (line 170, column 20) wrong result type 'Unit'

for application '(__=__) (__ 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))))))'

Error (line 170, column 20) no typing for '(__=__)(__ 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))))))'

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

Error (line 181, column 9) incompatible kind of: __-->__

expected: Type- -> Type+ -> Type

found: Type -> Type -> Type

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 182, column 4) unexpected term '__'

Hint (line 182, column 36) in type of '\ f : c -->? d . all (\ x : c . def f (x))'

type 'Unit'

is not unifiable with type '_var_101 ->? _var_102'

Hint (line 182, column 18) wrong result type 'Unit'

for application '(__=__) (__ in c --> d, \ f : c -->? d . all (\ x : c . def f (x)))'

Error (line 182, column 18) no typing for '(__=__)(__ in c --> d, \ f : c -->? d . all (\ x : c . def f (x)))'

Error (line 0, column 0) undeclared type '_var_103'

Error (line 0, column 0) undeclared type '_var_104'

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

Error (line 190, column 9) incompatible kind of: p -->? p

expected: Cpo-

found: Type

Error (line 190, column 9) incompatible kind of: p -->? p

expected: Cpo-

found: Type

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