%% 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) = \ (var x : s) . ()

%% def is also total (identical to tt)

program (op tt[s] : forall s : Type . Pred s) = \ (var x : s) . ()

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

%% trivial because its the strict function property

. (fun __=__[s * t ->? _v33] : forall s : Type . s * s ->? Unit)

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

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

. (fun __=__[_v73 * _v71 -> _v73] :

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

(((op fst[_v73; _v71] : forall s : Type; t : Type . s * t -> s),

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

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

%% Internal Logic

pred eq : s * s

. (fun __=__[s ->? Unit] : forall s : Type . s * s ->? Unit)

((\ (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)))

. (fun __=__[s * s ->? s] : forall s : Type . s * s ->? Unit)

((\ ((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

= \ (var s : nat -> c)

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

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

= \ ((var x : c), (var s : nat -> c))

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

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

. (fun __=__[p] : forall s : Type . s * s ->? Unit)

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

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

(((fun __=__[p] : forall s : Type . s * s ->? Unit)

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

? : +Type -> Type

Logical : Type := ? Unit

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

Unit : (Pcpo, Type)

__*__

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

+Type -> +Type -> Type)

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

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

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

__-->__

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

-Type -> +Type -> Type) < (__-->?__, __->__)

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

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

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

bool

: (Flatcpo, Type)

%[free type bool

::= true : bool

false : bool]%

nat : (Flatcpo, Type)

s : Type

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

c : Cpo %(var_199)%

d : Cpo %(var_200)%

f : Flatcpo %(var_198)%

p : Pcpo %(var_197)%

t : Type %(var_2)%

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

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

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

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

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

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

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

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

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

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

__res__

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

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

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

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

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

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

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

false

: bool %(construct bool)%

: Unit ->? Unit %(pred)%

: Unit %(fun)%

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

= \ ((var x : c), (var s : nat -> c))

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

isChain

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

%(pred)%

= \ (var s : nat -> c)

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

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

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

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

f : p --> p

g : c --> d

x : p

x1 : c

x2 : c

y1 : d

y2 : d

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

program def = \ x . () %(pe_def)%

program tt = \ x . () %(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)%

(\ (x, y) . def (x res y)) = (\ (x, y) . (def y) und (def x))

fst = __res__ ()

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

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

forall s : nat -> c

. (isChain (s)) =

(all (\ n : nat . s (n) <<= s (Suc (n))) as Unit) %(def_isChain)%

forall x : c; s : nat -> c

. (isBound (x, s)) =

(all (\ n : nat . s (n) <<= x) as Unit) %(def_isBound)%

(f (Y (f))) = (Y (f))

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

undefined =

(Y (\ x' . 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.32, unexpected mixfix token: all

*** Error 54.6, unexpected mixfix token: :

*** Hint 58.13, rebound variable 'x'

*** Hint 59.9, rebound variable 'x'

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

with (maximal) type: _v11 ->? t

known types:

*** Hint 60.9-60.24, untypable application (with result type: t)

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

*** Error 60.30, no typing for 'program snd(x : s, (var y : t)) : t = y'

*** Error 65.18-65.30, ambiguous mixfix term

def (__res__(x, y))

def__(__res__(x, y))

*** Error 65.59, unexpected mixfix token: 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.9, no type match for: all

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

known types:

*** Hint 87.9-87.15, untypable application (with result type: Pred Unit)

'all (var p : Pred s)'

*** Error 87.38, no typing for 'program all(var p : Pred s) : Pred Unit = eq (p, tt)'

*** Error 90.45, unexpected mixfix token: t1

*** Error 93.11, unexpected mixfix token: impl

*** Error 93.58, unexpected mixfix token: And

*** Error 95.11, unexpected mixfix token: or

*** Error 96.21, unexpected mixfix token: impl

*** Error 95.48, unexpected mixfix token: all

*** Error 99.32, unexpected mixfix token: impl

*** Error 99.17, unexpected mixfix token: all

*** Error 98.39, unexpected mixfix token: all

*** Error 101.29, unexpected mixfix token: all

*** Error 103.44, unexpected mixfix token: impl

*** 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 125.32-125.62, unexpected term 'all (\ n : nat . s (n) <<= s (Suc (n)))'

*** Hint 126.15, rebound variable 'x'

*** Error 126.38, unexpected mixfix token: all

*** Error 126.38-126.60, unexpected term 'all (\ n : nat . s (n) <<= x)'

*** Error 131.56, unexpected mixfix token: impl

*** Error 130.32, unexpected mixfix token: impl

*** Error 130.3, unexpected mixfix token: all

*** Error 134.31, unexpected mixfix token: impl

*** Error 134.3, unexpected mixfix token: all

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

*** Warning 141.4, ignoring declaration for builtin 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, 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'

*** Error 159.45, unexpected mixfix token: und

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

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

*** Error 171.35, unexpected mixfix token: und

*** Error 174.45, unexpected mixfix token: +

*** Error 173.40, unexpected mixfix token: und

*** Error 172.39, unexpected mixfix token: und

*** Error 171.9, unexpected mixfix token: all

*** Error 170.7, unexpected mixfix token: :

*** Error 176.51, unexpected mixfix token: impl

*** Error 176.31, unexpected mixfix token: all

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

*** Error 182.46-182.53, ambiguous mixfix term

def__(f x)

def f x

*** Error 182.36, unexpected mixfix token: all

*** Error 182.7, unexpected mixfix token: :

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

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

*** Error 186.26, unexpected mixfix token: c

*** Error 193.32, unexpected mixfix token: impl

*** Error 192.40, unexpected mixfix token: und

*** Error 192.3, unexpected mixfix token: all

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