%% predefined universe containing all types,

%% superclass of all other classes

class Type

vars s, t : Type

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

%% invisible type "Unit" for formulae

type Unit

%% flat cpo with bottom

%% type aliases

preds true, false : Unit

preds __/\__, __\/__, __=>__, __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

ops def, tt : Pred s

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

%% total function type

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

type __->__ < __->?__

%% total functions

op __res__(x : s; y : t) : s = x;

op fst(x : s; y : t) : s = x;

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

%% trivial because its the strict function property

. fst = __res__;

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

%% Internal Logic

pred eq : s * s

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

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

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

{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

program __ <<=[f] __ = eq;

}

vars c, d : Cpo

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

vars x1, x2 : c; y1, y2 : d

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

type Unit : Pcpo

%% Pcont

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

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

%% Tcont

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

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

vars f, g : c --> d

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

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

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

vars f : p --> p; x : p

. f (Y f) = Y f

. f x = x => Y f <<= x;

op undefined : c --> p =

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

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

%% user stuff

free type bool ::= true | false

type bool : Flatcpo

type nat : Flatcpo

classes

Flatcpo < Type;

Pcpo < Type

classes

Flatcpo < Cpo;

Pcpo < Cpo

types

Unit : Pcpo;

__*__ : +Pcpo -> +Pcpo -> Pcpo;

__-->__ : -Cpo -> +Pcpo -> Pcpo;

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

bool : Flatcpo;

nat : Flatcpo;

s : Type

vars

c : Cpo %(var_245)%;

d : Cpo %(var_246)%;

f : Flatcpo %(var_243)%;

p : Pcpo %(var_242)%;

t : Type %(var_2)%

op def : forall s : Type . Pred s

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

%[ = \ ((var x : s), (var y : t)) .! (var x : s) ]%

op 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

%[ =

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

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

(c --> p) --> c --> p) ]%

pred __<<=__ : forall c : Cpo . c * c

pred eq : forall s : Type . s * s

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

pred isChain : forall c : Cpo . nat -> c

pred not : Unit

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

vars

f : p --> p;

g : c --> d;

x : p;

x1 : c;

x2 : c;

y1 : d;

y2 : d

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

program tt = \ x : s . () %(pe_tt)%

forall s : Type; t : Type; x : s; y : t . x res y = x

forall s : Type; t : Type; x : s; y : t . fst (x, y) = x

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

. fst = __res__

forall s : Type . (\ x : s . eq (x, x)) = tt

forall s : Type

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

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

program __ <<=[f] __ = eq %(pe___<<=__)%

program f <<= g = f <<= g %(pe___<<=__)%

forall p : Pcpo; f : p --> p . f (Y f) = Y f

forall p : Pcpo; f : p --> p; x : p . f x = x => Y f <<= x

forall c : Cpo; p : Pcpo

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

free type bool ::= false | true %(ga_bool)%

4.7-4.10: ### Warning: void universe class declaration 'Type'

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

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

11.6-11.9: ### Hint: redeclared type 'Unit'

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

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

17.6-17.9: ### Warning:

ignoring declaration for builtin identifier 'true'

17.12-17.16: ### Warning:

ignoring declaration for builtin identifier 'false'

19.7-19.12: ### Warning:

ignoring declaration for builtin identifier '__/\__'

19.15-19.20: ### Warning:

ignoring declaration for builtin identifier '__\/__'

19.23-19.28: ### Warning:

ignoring declaration for builtin identifier '__=>__'

19.31-19.36: ### Warning:

ignoring declaration for builtin identifier '__if__'

19.38-19.44: ### Warning:

ignoring declaration for builtin identifier '__<=>__'

22.14: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

22.14: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

22.6-22.10: ### Warning:

ignoring declaration for builtin identifier '__=__'

27.6-27.12: ### Hint: redeclared type '__->?__'

30.6-30.10: ### Hint: redeclared type '__*__'

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

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

42.16: ### Hint: rebound variable 'x'

39.14-39.19: ### Hint:

repeated declaration of 'def' with type 'Pred s'

44.15: ### Hint: rebound variable 'x'

39.14-39.19: ### Hint:

repeated declaration of 'tt' with type 'Pred s'

46.11: *** Error: unexpected mixfix token: und

50.6-50.11: ### Hint: redeclared type '__->__'

52.6-52.11: ### Hint: redeclared type '__->__'

52.18-52.20: ### Hint: repeated supertype '__->?__'

54.42-54.49: *** Error:

ambiguous mixfix term

def (f x)

(def f) x

54.6: *** Error: unexpected mixfix token: :

58.13: ### Hint: rebound variable 'x'

58.4-58.10: ### Warning:

ignoring declaration for builtin identifier '__res__'

59.9: ### Hint: rebound variable 'x'

60.14: ### Hint: rebound variable 'x'

60.14: ### Hint: rebound variable 'x'

60.9-60.26: ### Warning:

illegal lhs pattern

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

65.18-65.30: *** Error:

ambiguous mixfix term

def (x res y)

def (x res y)

65.51-65.69: *** Error:

ambiguous mixfix term

(def y) und

(def y) und

65.7: ### Hint: rebound variable 'x'

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

65.40: ### Hint: rebound variable 'x'

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

65.7: ### Hint: rebound variable 'x'

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

65.40: ### Hint: rebound variable 'x'

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

65.33: *** Error:

ambiguous typings

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

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

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

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

66.7: *** Error:

in term '(op fst : forall s : Type; t : Type . s * t -> s) = __res__'

are uninstantiated type variables

'[_v46_v38_t, _v47_v37_s]'

72.11: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

72.11: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

74.5: ### Hint: rebound variable 'x'

74.5: ### Hint: rebound variable 'x'

75.6: ### Hint: rebound variable 'x'

75.35: ### Hint: rebound variable 'x'

75.35: ### Hint: rebound variable 'x'

75.6: ### Hint: rebound variable 'x'

75.35: ### Hint: rebound variable 'x'

75.35: ### Hint: rebound variable 'x'

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

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

87.40-87.47: ### Hint:

in type of '(pred eq : forall s : Type . s * s)

((var p : Pred s), (op tt : forall s : Type . Pred s))'

typename 'Unit' (72.12)

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

87.38: *** Error:

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

90.14: ### Hint: rebound variable 'x'

90.45-90.46: ### Hint: no type found for 't1'

90.45-90.46: ### Hint: untypeable term 't1'

90.45-90.46: ### Hint: untypeable term 't1 ()'

90.45-90.52: ### Hint: untypeable term 't1 () und'

90.45-90.55: ### Hint: untypeable term 't1 () und t2'

90.43: *** Error:

no typing for

'program And (x, y : Pred Unit) : Pred Unit = t1 () und t2 ()'

93.11: *** Error: unexpected mixfix token: impl

95.11: *** Error: unexpected mixfix token: or

98.39-98.41: ### Hint: no type found for 'all'

98.39-98.41: ### Hint: untypeable term 'all'

98.37: *** Error:

no typing for

'program ex (p : Pred s) : Pred Unit

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

101.29-101.31: ### Hint: no type found for 'all'

101.29-101.31: ### Hint: untypeable term 'all'

101.27: *** Error:

no typing for

'program ff () : Pred Unit = all \ r : Pred Unit . r ()'

103.44-103.47: ### Hint: no type found for 'impl'

103.44-103.47: ### Hint: untypeable term (with type: Unit) 'impl'

103.42-103.47: ### Hint: untypeable term 'r impl'

103.40: *** Error:

no typing for 'program neg (r : Pred Unit) : Pred Unit = r impl ff'

108.3-108.5: ### Hint: no type found for 'all'

108.3-108.5: ### Hint: untypeable term 'all'

108.3-108.62: *** Error:

no typing for

'all

\ (f, g) : s ->? t

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

115.7-115.9: ### Warning: unchanged class 'Cpo'

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

119.16: ### Hint:

no kind found for 'c'

expected: {Cppo}

found: {Cpo}

121.3-121.5: ### Hint: no type found for 'all'

121.3-121.5: ### Hint: untypeable term 'all'

121.3-121.18: *** Error: no typing for 'all \ x : c . x <<= x'

122.3-122.5: ### Hint: no type found for 'all'

122.3-122.5: ### Hint: untypeable term 'all'

122.3-122.55: *** Error:

no typing for

'all \ (x, y, z : c) . (x <<= y) und (y <<= z) impl x <<= z'

123.3-123.5: ### Hint: no type found for 'all'

123.3-123.5: ### Hint: untypeable term 'all'

123.3-123.56: *** Error:

no typing for

'all \ (x, y, z : c) . (x <<= y) und (y <<= x) impl eq (x, y)'

125.32-125.34: ### Hint: no type found for 'all'

125.32-125.34: ### Hint: untypeable term 'all'

125.14-125.51: *** Error:

no typing for '(all \ n : nat . s n <<= s (Suc n)) as Unit'

126.15: ### Hint: rebound variable 'x'

126.38-126.40: ### Hint: no type found for 'all'

126.38-126.40: ### Hint: untypeable term 'all'

126.14-126.57: *** Error:

no typing for '(all \ n : nat . s n <<= x) as Unit'

130.21-131.74: *** Error:

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

130.3-130.5: ### Hint: no type found for 'all'

130.3-130.5: ### Hint: untypeable term 'all'

130.3-131.74: *** Error:

no typing for

'all

\ s : nat -> c

. def (sup s) impl

(isBound (sup s, s) und all

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

134.3-134.5: ### Hint: no type found for 'all'

134.3-134.5: ### Hint: untypeable term 'all'

134.3-134.44: *** Error:

no typing for 'all \ s : nat -> c . isChain s impl def (sup s)'

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

141.4-141.9: ### Warning:

ignoring declaration for builtin identifier 'bottom'

143.3-143.5: ### Hint: no type found for 'all'

143.3-143.5: ### Hint: untypeable term 'all'

143.3-143.24: *** Error: no typing for 'all \ x : p . bottom <<= x'

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

150.15-150.17: ### Hint: is type list '[f]'

119.14-119.18: ### Hint:

repeated declaration of '__<<=__' with type 'c * c ->? Unit'

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

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

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

155.15-155.19: ### Hint: redeclared type '__*__'

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

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

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

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

159.10-159.11: ### Hint: rebound variable 'x1'

159.14-159.15: ### Hint: rebound variable 'y1'

159.23-159.24: ### Hint: rebound variable 'x2'

159.27-159.28: ### Hint: rebound variable 'y2'

159.37-159.47: ### Hint: untypeable term '(x1 <<= x2) und'

159.31: *** Error:

no typing for

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

169.7-169.14: ### Hint: redeclared type '__-->?__'

169.20-169.22: ### Hint: repeated supertype '__->?__'

171.24-171.61: *** Error:

ambiguous mixfix term

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

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

174.45: *** Error: unexpected mixfix token: +

173.28-174.61: *** Error:

ambiguous mixfix term

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

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

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

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

170.7: *** Error: unexpected mixfix token: :

176.16-176.25: ### Hint: is type list '[c -->? d]'

176.41-176.68: *** Error:

ambiguous mixfix term

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

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

176.11: ### Warning: variable also known as type variable 'f'

176.31-176.33: ### Hint: no type found for 'all'

176.31-176.33: ### Hint: untypeable term 'all'

176.29: *** Error:

no typing for

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

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

179.15-179.21: ### Hint: redeclared type '__-->__'

181.17-181.23: ### Warning: non-unique kind for '__ -->? __'

181.7-181.13: ### Hint: redeclared type '__-->__'

181.19-181.22: ### Hint: repeated supertype '__-->?__'

182.16: ### Hint:

no kind found for 'd'

expected: {Cppo}

found: {Cpo}

182.46-182.53: *** Error:

ambiguous mixfix term

def (f x)

(def f) x

182.7: *** Error: unexpected mixfix token: :

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

184.19: ### Hint:

no kind found for 'd'

expected: {Cppo}

found: {Cpo}

184.6: ### Warning: variable also known as type variable 'f'

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

184.19: ### Hint:

no kind found for 'd'

expected: {Cppo}

found: {Cpo}

186.25-186.34: ### Hint: is type list '[c -->? d]'

186.10: ### Hint: rebound variable 'f'

186.10: ### Warning: variable also known as type variable 'f'

186.16: ### Hint: rebound variable 'g'

186.10: ### Hint: rebound variable 'f'

186.10: ### Warning: variable also known as type variable 'f'

186.16: ### Hint: rebound variable 'g'

119.14-119.18: ### Hint:

repeated declaration of '__<<=__' with type 'c * c ->? Unit'

190.16: ### Hint:

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

190.23: ### Hint:

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

192.3-192.5: ### Hint: no type found for 'all'

192.3-192.5: ### Hint: untypeable term 'all'

192.3-193.44: *** Error:

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'

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

195.15: ### Hint:

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

195.5: ### Hint: rebound variable 'f'

195.5: ### Warning: variable also known as type variable 'f'

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

195.18: ### Hint: rebound variable 'x'

199.22: ### Hint:

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

199.40: ### Hint:

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

199.58: ### Hint:

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

199.71: ### Hint:

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

199.65-199.71: ### Hint:

no kind found for 'c --> p'

expected: {Cppo}

found: {Pcpo}

204.20-204.23: ### Warning:

ignoring declaration for builtin identifier 'true'

204.27-204.31: ### Warning:

ignoring declaration for builtin identifier 'false'