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

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

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 4.7, illegal universe class declaration 'Type'

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

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

*** Warning 11.6, redeclared type 'Unit'

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

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

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

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

*** Error 46.11, unexpected mixfix token: und

*** Error 46.9, unexpected pattern '__ und __ (x, y : Unit)'

*** Error 46.9, illegal toplevel pattern '__ und __ (x, y : Unit)'

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

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

expected: Type- -> Type+ -> Type

found: Type -> Type -> Type

*** Error 54.3, expected further mixfix token: ["/\\","<=>","=","=>","=e="]

*** Error 54.42, ambiguous mixfix term

(def__)(f x)

def f x

*** Error 54.32, unexpected mixfix token: all

*** Error 54.3, unexpected term '__'

*** Hint 54.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 54.16, wrong result type 'Unit'

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

*** Error 54.16, no typing for '(__=__)(__ in s -> t, \ f : s ->? t . all (\ x : s . def f (x)))'

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

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

known types:

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

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

*** Error 60.9, no typing for 'snd(x : s, y : t) : t'

*** Error 65.18, ambiguous mixfix term

def ((__res__)(x, y))

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

*** Error 65.59, unexpected mixfix token: und

*** Error 65.18, unexpected term 'def (x res y)'

*** Error 65.52, unexpected term '(def y) und (def x)'

*** Error 75.17, ambiguous mixfix term

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

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

*** Error 75.46, ambiguous mixfix term

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

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

*** Error , undeclared type '_var_45'

*** Error 75.15, unexpected term 'x res eq (x, y)'

*** Error , undeclared type '_var_46'

*** Error 75.44, unexpected term 'y res eq (x, y)'

*** Warning 85.6, redeclared type 's'

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

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

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

known types:

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

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

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

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

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

known types:

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

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

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

*** Error 93.11, unexpected mixfix token: impl

*** Error 93.9, unexpected pattern '__ impl __ (x, y : Pred Unit)'

*** Error 93.53, unexpected mixfix token: x

*** Error 95.11, unexpected mixfix token: or

*** Error 95.9, unexpected pattern '__ or __ (x, y : Pred Unit)'

*** Error 96.19, unexpected mixfix token: x

*** Error 95.48, unexpected mixfix token: all

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

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

known types:

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

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

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

*** Error 101.13, unexpected mixfix token: )

*** Error 101.9, unexpected pattern 'ff ()'

*** Error 101.29, unexpected mixfix token: all

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

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

known types:

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

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

*** Error 103.9, no typing for 'neg(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.50, ambiguous mixfix term

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

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

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

*** Warning 153.5, redeclared type 'c'

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

*** Error , undeclared type '_var_75'

*** Error , undeclared type '_var_76'

*** Error , undeclared type '_var_77'

*** Error , undeclared type '_var_78'

*** Error 159.45, unexpected mixfix token: und

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

expected: Type- -> Type+ -> Type

found: Type -> Type -> Type

*** Error 170.4, expected further mixfix token: ["/\\","<<=","<=>","=","=>"]

*** 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.4, unexpected term '__'

*** Hint 171.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 170.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 170.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 176.16, unexpected mixfix token: [

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

expected: Type- -> Type+ -> Type

found: Type -> Type -> Type

*** Error 182.4, expected further mixfix token: ["/\\","<<=","<=>","=","=>"]

*** Error 182.46, ambiguous mixfix term

(def__)(f x)

def f x

*** Error 182.36, unexpected mixfix token: all

*** Error 182.4, unexpected term '__'

*** Hint 182.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 182.18, wrong result type 'Unit'

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

*** Error 182.18, no typing for '(__=__)(__ in c --> d, \ f : c -->? d . all (\ x : c . def f (x)))'

*** Error , undeclared type '_var_103'

*** Error , undeclared type '_var_104'

*** Error 186.25, unexpected mixfix token: [

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

expected: Cpo-

found: Type

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

expected: Cpo-

found: Type

*** Error 193.32, unexpected mixfix token: impl

*** Error 192.40, unexpected mixfix token: und

*** Error 192.3, unexpected mixfix token: all