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

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

%% ...

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

%% "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[s] : forall s : Type . Pred s) : Pred s =

\ (var x : s) . () : s ->? Unit

%% def is also total (identical to tt)

program

(op tt[s] : forall s : Type . Pred s) : Pred s =

\ (var x : s) . () : s ->? Unit

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

%% total function type

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

type __->__ < __->?__

%% total functions

op __res__ : forall s : Type; t : Type . s * t -> s =

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

op fst : forall s : Type; t : Type . s * t -> s =

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

program

(var snd : s * t ->? t) ((var x : s), (var y : t) : t) : t =

(var y : t)

%% trivial because its the strict function property

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

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

. (op fst[_v90; _v88] : forall s : Type; t : Type . s * t -> s) =

(op __res__[_v90; _v88] : forall s : Type; t : Type . s * t -> s)

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

%% Internal Logic

pred eq : s * s

. (\ (var x : s) .

(pred eq[s] : forall s : Type . s * s) ((var x : s), (var x : s)))

= (op tt[s] : forall s : Type . Pred s)

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

(op __res__[s; Unit] : forall s : Type; t : Type . s * t -> s)

((var x : s),

(pred eq[s] : forall s : Type . s * s) ((var x : s), (var y : s))))

=

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

(op __res__[s; Unit] : forall s : Type; t : Type . s * t -> s)

((var y : s),

(pred eq[s] : forall s : Type . s * s) ((var x : s), (var y : s))))

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

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

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

%% 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 : forall c : Cpo . nat -> c;

pred isBound : forall c : Cpo . c * (nat -> c);

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

}

class Pcpo < Cpo

{var p : Pcpo;

op bottom : p;

}

class instance

Flatcpo < Cpo

{var f : Flatcpo;}

var c : Cpo; d : Cpo

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

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

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

type Unit : Pcpo

%% Pcont

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

type __-->?__ < __->?__

%% Tcont

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

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

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

fun Y : (p --> p) --> p

var f : p --> p; x : p

. (var f : p --> p)

((fun Y[p] : forall p : Pcpo . (p --> p) --> p) (var f : p --> p))

= (fun Y[p] : forall p : Pcpo . (p --> p) --> p) (var f : p --> p)

. (var f : p --> p) (var x : p) = (var x : p) =>

(pred __<<=__[p] : forall c : Cpo . c * c)

((fun Y[p] : forall p : Pcpo . (p --> p) --> p) (var f : p --> p),

(var x : p))

op undefined : forall p : Pcpo; c : Cpo . c --> p =

(fun Y[c --> p] : forall p : Pcpo . (p --> p) --> p)

(\ (var x' : c --> p) . (var x' : c --> p) as

(c --> p) --> c --> p)

as c --> p

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

%% user stuff

free type bool ::= true | false

type bool : Flatcpo

type nat : Flatcpo

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

Cpo < Type

Flatcpo < Cpo

Pcpo < Cpo

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

bool

: (Flatcpo, Type)

%[free type bool ::=

true : bool

false : bool]%

nat : (Flatcpo, Type)

s : Type

%% Type Variables --------------------------------------------------------

c : Cpo %(var_363)%

d : Cpo %(var_364)%

f : Flatcpo %(var_362)%

p : Pcpo %(var_360)%

t : Type %(var_2)%

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

Y : forall p : Pcpo . (p --> p) --> p %(fun)%

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

__res__

: forall s : Type; t : Type . s * t -> s

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

def : forall s : Type . Pred s %(op)%

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

fst

: forall s : Type; t : Type . s * t -> s

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

isBound : forall c : Cpo . c * (nat -> c) ->? Unit %(pred)%

isChain : forall c : Cpo . (nat -> c) ->? Unit %(pred)%

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

snd : s * t ->? t %(op)%

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

tt : forall s : Type . Pred s %(op)%

undefined

: forall p : Pcpo; c : Cpo . c --> p

%(op)% =

(fun Y[c --> p] : forall p : Pcpo . (p --> p) --> p)

(\ (var x' : c --> p) . (var x' : c --> p) as

(c --> p) --> c --> p)

as c --> p

%% Variables -------------------------------------------------------------

f : p --> p

g : c --> d

x : p

x1 : c

x2 : c

y1 : d

y2 : d

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

program def : Pred s = \ x . () : s ->? Unit %(pe_def)%

program tt : Pred s = \ x . () : s ->? Unit %(pe_tt)%

forall x : s; y : t . (x res y) = (x as s) %(def___res__)%

forall x : s; y : t . fst (x, y) = (x as s) %(def_fst)%

program (var snd : s * t ->? t) (x, y : t) : t = y %(pe_snd)%

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

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

fst = __res__

(\ x . eq (x, x)) = tt

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

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

f (Y f) = Y f

f x = x => ((Y f) <<= x)

undefined =

(Y (\ x' : c --> p . x' as (c --> p) --> c --> p) as c --> p)

%(def_undefined)%

free type bool ::=

true : bool

false : bool %(ga_bool)%

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

### Warning 4.7, void universe class declaration 'Type'

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

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

### Hint 11.6, redeclared type 'Unit'

*** Error 14.11, illegal type pattern argument '__'

*** Error 15.8, illegal type pattern argument '__'

### Warning 17.6, ignoring declaration for builtin identifier 'true'

### Warning 17.12, ignoring declaration for builtin identifier 'false'

### Warning 19.9, ignoring declaration for builtin identifier '__/\__'

### Warning 19.17, ignoring declaration for builtin identifier '__\/__'

### Warning 19.25, ignoring declaration for builtin identifier '__=>__'

### Warning 19.33, ignoring declaration for builtin identifier '__if__'

### Warning 19.40, ignoring declaration for builtin identifier '__<=>__'

### Warning 22.8, ignoring declaration for builtin identifier '__=__'

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

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

*** Error 31.6-31.12, illegal type pattern '__ * __ * __'

### Hint 40.7, not a class 's'

### Hint 42.16, rebound variable 'x'

### Hint 44.15, rebound variable 'x'

*** Error 46.11, unexpected mixfix token: und

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

### Hint 52.8, redeclared type '__->__'

### Hint, repeated supertype '__->?__'

*** Error 54.42-54.49, ambiguous mixfix term

def (f x)

(def f) x

*** Error 54.6, unexpected mixfix token: :

### Hint 58.13, rebound variable 'x'

### Hint 59.9, rebound variable 'x'

### Hint 60.14, rebound variable 'x'

### Hint 60.14, rebound variable 'x'

### Warning 60.13-60.24, illegal lhs pattern '(var snd : s * t ->? t) ((var x : s), (var y : t))'

*** Error 65.18-65.30, ambiguous mixfix term

def (x res y)

def (x res y)

*** Error 65.51-65.69, ambiguous mixfix term

(def y) und

(def y) und

### Hint 65.7, rebound variable 'x'

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

### Hint 65.40, rebound variable 'x'

*** Error 65.51-65.69, unexpected term '(def y) und (def x)'

### Hint 74.5, rebound variable 'x'

### Hint 75.6, rebound variable 'x'

### Hint 75.35, rebound variable 'x'

### Warning 85.6, new type shadows type variable 's'

*** Error 85.11, illegal type variable as supertype 's'

### Hint 87.40, in type of '(pred eq[_v230] : forall s : Type . s * s)'

typename 'Unit'

is not unifiable with type 'Unit ->? Unit' (87.33)

### Hint 87.40-87.46, untypable application (with result type: Pred Unit)

'eq (p, tt)'

*** Error 87.38, no typing for 'program (var all : _v206) ((var p : _v207) : Pred s) : Pred Unit

= eq (p, tt)'

### Hint 90.14, rebound variable 'x'

### Hint 90.45, no type match for: t1

with (maximal) type: _v265 ->? _v264 ->? _v263 ->? _v262 ->? Pred Unit

known types:

### Hint 90.45-90.47, untypable application (with result type: _v264 ->? _v263 ->? _v262 ->? Pred Unit)

't1'

### Hint 90.45-90.50, untypable application (with result type: _v263 ->? _v262 ->? Pred Unit)

't1 und'

### Hint 90.45-90.54, untypable application (with result type: _v262 ->? Pred Unit)

't1 und t2'

### Hint 90.45-90.57, untypable application (with result type: Pred Unit)

't1 und t2 ()'

*** Error 90.43, no typing for 'program (var And : _v231) (x, (var y : _v232) : Pred Unit) :

Pred Unit

= t1 und t2 ()'

*** Error 93.11, unexpected mixfix token: impl

*** Error 95.11, unexpected mixfix token: or

### Hint 98.39, no type match for: all

with (maximal) type: _v291 ->? Pred Unit

known types:

### Hint 98.39-99.45, untypable application (with result type: Pred Unit)

'all

(\ (var r : _v269) : Pred Unit .

all (\ x : s . p x impl r) impl r)'

*** Error 98.37, no typing for 'program (var ex : _v267) ((var p : _v268) : Pred s) : Pred Unit =

all

(\ (var r : _v269) : Pred Unit .

all (\ x : s . p x impl r) impl r)'

### Hint 101.29, no type match for: all

with (maximal) type: _v303 ->? Pred Unit

known types:

### Hint 101.29-101.50, untypable application (with result type: Pred Unit)

'all (\ (var r : _v293) : Pred Unit . r)'

*** Error 101.27, no typing for 'program (var ff : _v292) () : Pred Unit =

all (\ (var r : _v293) : Pred Unit . r)'

### Hint 103.44, no type match for: impl

with (maximal) type: _v328

known types:

### Hint 103.42-103.44, untypable application (with result type: _v327 ->? Pred Unit)

'r impl'

### Hint 103.42-103.49, untypable application (with result type: Pred Unit)

'r impl ff'

*** Error 103.40, no typing for 'program (var neg : _v304) ((var r : _v305) : Pred Unit) :

Pred Unit

= r impl ff'

### Hint 108.3, no type match for: all

with (maximal) type: _v339 ->? Unit

known types:

### Hint 108.3-108.63, untypable application (with result type: Unit)

'all

(\ ((var f : _v337), (var g : _v338)) : s ->? t .

all (\ x : s . eq (\ () . f x, g x) impl eq (f, g)))'

*** Error 108.3-108.63, no typing for 'all

(\ ((var f : _v337), (var g : _v338)) : s ->? t .

all (\ x : s . eq (\ () . f x, g x) impl eq (f, g)))'

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

### Hint 121.3, no type match for: all

with (maximal) type: _v341 ->? Unit

known types:

### Hint 121.3-121.16, untypable application (with result type: Unit)

'all (\ x : c . x <<= x)'

*** Error 121.3-121.16, no typing for 'all (\ x : c . x <<= x)'

### Hint 122.3, no type match for: all

with (maximal) type: _v344 ->? Unit

known types:

### Hint 122.3-122.44, untypable application (with result type: Unit)

'all

(\ (x, (var y : _v342), (var z : _v343) : c) .

((x <<= y) und (y <<= z) impl x) <<= z)'

*** Error 122.3-122.44, no typing for 'all

(\ (x, (var y : _v342), (var z : _v343) : c) .

((x <<= y) und (y <<= z) impl x) <<= z)'

### Hint 123.3, no type match for: all

with (maximal) type: _v347 ->? Unit

known types:

### Hint 123.3-123.57, untypable application (with result type: Unit)

'all

(\ (x, (var y : _v345), (var z : _v346) : c) .

(x <<= y) und (y <<= x) impl eq (x, y))'

*** Error 123.3-123.57, no typing for 'all

(\ (x, (var y : _v345), (var z : _v346) : c) .

(x <<= y) und (y <<= x) impl eq (x, y))'

### Hint 125.32, no type match for: all

with (maximal) type: _v350 ->? _v351

known types:

### Hint 125.32-125.46, untypable application 'all (\ (var n : _v348) : nat . (s n) <<= (s (Suc n)))'

*** Error 125.14-125.46, no typing for 'all (\ (var n : _v348) : nat . (s n) <<= (s (Suc n))) as Unit'

### Hint 126.15, rebound variable 'x'

### Hint 126.38, no type match for: all

with (maximal) type: _v354 ->? _v355

known types:

### Hint 126.38-126.52, untypable application 'all (\ (var n : _v352) : nat . (s n) <<= x)'

*** Error 126.14-126.52, no typing for 'all (\ (var n : _v352) : nat . (s n) <<= x) as Unit'

*** Error 130.21-131.74, ambiguous mixfix term

def

(((sup s) impl)

((((isBound (sup s, s)) und) all)

(\ x : c . ((((isBound (x, s)) impl) sup) s) <<= x)))

((def (sup s)) impl)

((((isBound (sup s, s)) und) all)

(\ x : c . ((((isBound (x, s)) impl) sup) s) <<= x))

### Hint 130.3, no type match for: all

with (maximal) type: _v357 ->? Unit

known types:

### Hint 130.3-131.74, untypable application (with result type: Unit)

'all

(\ (var s : _v356) : nat -> c .

def (sup s) impl

(isBound (sup s, s) und all

(\ x : c . isBound (x, s) impl sup (s) <<= x)))'

*** Error 130.3-131.74, no typing for 'all

(\ (var s : _v356) : nat -> c .

def (sup s) impl

(isBound (sup s, s) und all

(\ x : c . isBound (x, s) impl sup (s) <<= x)))'

### Hint 134.3, no type match for: all

with (maximal) type: _v359 ->? Unit

known types:

### Hint 134.3-134.46, untypable application (with result type: Unit)

'all (\ (var s : _v358) : nat -> c . isChain s impl def (sup s))'

*** Error 134.3-134.46, no typing for 'all (\ (var s : _v358) : nat -> c . isChain s impl def (sup s))'

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

### Warning 141.4, ignoring declaration for builtin identifier 'bottom'

### Hint 143.3, no type match for: all

with (maximal) type: _v361 ->? Unit

known types:

### Hint 143.3-143.22, untypable application (with result type: Unit)

'all (\ x : p . bottom <<= x)'

*** Error 143.3-143.22, no typing for 'all (\ x : p . bottom <<= x)'

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

*** Error 150.15, unexpected mixfix token: [

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

### Hint 153.5, rebound type variable 'c'

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

### Hint 157.7, not a class 'c'

### Hint 157.11, not a class 'c'

### Hint 157.18, not a class 'd'

### Hint 157.23, not a class 'd'

### Hint 159.10, rebound variable 'x1'

### Hint 159.14, rebound variable 'y1'

### Hint 159.23, rebound variable 'x2'

### Hint 159.27, rebound variable 'y2'

### Hint 159.37, in type of '(pred __<<=__[_v387] : forall c : Cpo . c * c)'

typename 'Unit'

is not unifiable with type '_v385 ->? _v384 ->? Unit' (159.53)

### Hint 159.34-159.41, untypable application (with result type: _v385 ->? _v384 ->? Unit)

'x1 <<= x2'

### Hint 159.33-159.45, untypable application (with result type: _v384 ->? Unit)

'(x1 <<= x2) und'

### Hint 159.33-159.59, untypable application (with result type: Unit)

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

*** Error 159.31, no typing for 'program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2)'

### Hint 169.9, redeclared type '__-->?__'

### Hint, repeated supertype '__->?__'

*** Error 171.24-171.61, ambiguous mixfix term

(def (((f x) und) x)) <<= y

(((def (f x)) und) x) <<= y

*** Error 174.45, unexpected mixfix token: +

*** Error 173.28-174.61, ambiguous mixfix term

def

((((f (s m)) und) eq)

(sup (\ (var n : _v392) : nat .! f (s (n + m))), f (sup s)))

((((def f) (s m)) und) eq)

(sup (\ (var n : _v392) : nat .! f (s (n + m))), f (sup s))

*** Error 170.7, unexpected mixfix token: :

*** Error 176.19, unexpected mixfix token: -->?

*** Error 176.41-176.68, ambiguous mixfix term

(def ((((f x) impl) f) x)) <<= (g x)

((((def (f x)) impl) f) x) <<= (g x)

*** Error 181.9, non-unique kind for '__-->__'

*** Error 182.46-182.53, ambiguous mixfix term

def (f x)

(def f) x

*** Error 182.7, unexpected mixfix token: :

### Hint 184.7, not a kind 'c --> d'

### Hint 184.11, not a kind 'c --> d'

*** Error 186.28, unexpected mixfix token: -->?

### Hint 192.3, no type match for: all

with (maximal) type: _v394 ->? Unit

known types:

### Hint 192.3-193.47, untypable application (with result type: Unit)

'all

(\ f : p -->? p .

eq (f (Y f), Y f) und all

(\ x : p . (eq (f x, x) impl Y f) <<= x))'

*** Error 192.3-193.47, no typing for 'all

(\ f : p -->? p .

eq (f (Y f), Y f) und all

(\ x : p . (eq (f x, x) impl Y f) <<= x))'

### Hint 195.7, not a kind 'p --> p'

### Hint 195.5, rebound variable 'f'

### Hint 195.20, not a class 'p'

### Hint 195.18, rebound variable 'x'

### Warning 204.20, ignoring declaration for builtin identifier 'true'

### Warning 204.27, ignoring declaration for builtin identifier 'false'