5aceed326fe593ff15bef79c5a86eef2df62a2baChristian Maeder

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maeder%% predefined universe containing all types,

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maeder%% superclass of all other classes

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maederclass Type

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maedervars s, t : Type

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maeder

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maeder%% invisible type "Unit" for formulae

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maedertype Unit

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maeder %% flat cpo with bottom

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maeder

1d2c2ebba52ca5c89ca40181064ab30e2ef26403Christian Maeder%% type aliases

1d2c2ebba52ca5c89ca40181064ab30e2ef26403Christian Maederpreds true, false : Unit

1d2c2ebba52ca5c89ca40181064ab30e2ef26403Christian Maederpreds __/\__, __\/__, __=>__, __if__, __<=>__ : Unit * Unit

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maederpred not : Unit

3fa78cc4ca8d77d7aa06b0d907d3abd809c96666Christian Maederpred __=__ : s * s

1d2c2ebba52ca5c89ca40181064ab30e2ef26403Christian Maeder %% =e=

1d2c2ebba52ca5c89ca40181064ab30e2ef26403Christian Maeder

1d2c2ebba52ca5c89ca40181064ab30e2ef26403Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1d2c2ebba52ca5c89ca40181064ab30e2ef26403Christian Maeder%% (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_465)%;

d : Cpo %(var_466)%;

f : Flatcpo %(var_463)%;

p : Pcpo %(var_461)%;

t : Type %(var_2)%

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

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

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

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

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

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

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

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

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

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

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

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

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

%[op=

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

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

as c --> 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 x : s; y : t . x res y = (x as s)

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

program (var snd : s * t ->? t) (x, y : t) : 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

. undefined

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

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

### 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 '__<=>__'

### Hint 22.14,

no kind found for 's'

expected: {Cpo}

found: {Type}

### Hint 22.14,

no kind found for 's'

expected: {Cppo}

found: {Type}

### 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 39.14-39.19,

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

### Hint 44.15, rebound variable 'x'

### Hint 39.14-39.19,

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

*** Error 46.11, unexpected mixfix token: und

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

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

### Hint 52.18, 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'

### Warning 58.6,

ignoring declaration for builtin identifier '__res__'

### Hint 59.9, rebound variable 'x'

### Hint 60.14, rebound variable 'x'

### Hint 60.14, rebound variable 'x'

### Warning 60.9-60.26,

illegal lhs pattern

'(var snd : s * t ->? t) ((var x : s), (var y : t)) : 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 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)'

*** Error 65.16,

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)

### Hint 72.11,

no kind found for 's'

expected: {Cpo}

found: {Type}

### Hint 72.11,

no kind found for 's'

expected: {Cppo}

found: {Type}

### Hint 74.5, rebound variable 'x'

### Hint 74.5, rebound variable 'x'

### Hint 75.6, rebound variable 'x'

### Hint 75.35, rebound variable 'x'

### Hint 75.35, rebound variable 'x'

### Hint 75.6, rebound variable 'x'

### Hint 75.35, 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 : forall s : Type . s * s)'

typename 'Unit' (72.9)

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

### Hint 87.40,

untypeable term (with type: _v371 ->? Pred Unit) 'eq'

*** Error 87.38,

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

### Hint 90.14, rebound variable 'x'

### Hint 90.45, no type found for 't1'

### Hint 90.45, no type found for 't1'

### Hint 90.45,

untypeable term (with type: ? (_v390 ->? _v389 ->? Unit ->? Pred Unit))

't1'

### Hint 90.45-90.47,

untypeable term (with type: _v390 ->? _v389 ->? Unit ->? Pred Unit)

't1 ()'

### Hint 90.45-90.50,

untypeable term (with type: _v389 ->? Unit ->? Pred Unit)

't1 () und'

### Hint 90.45, no type found for 't1'

### Hint 90.45, no type found for 't1'

### Hint 90.45,

untypeable term (with type: ? (_v392 ->? _v391 ->? ? Pred Unit))

't1'

### Hint 90.45-90.47,

untypeable term (with type: _v392 ->? _v391 ->? ? Pred Unit)

't1 ()'

### Hint 90.45-90.50,

untypeable term (with type: _v391 ->? ? Pred Unit) 't1 () und'

### Hint 90.45-90.54,

untypeable term (with type: ? Pred Unit) 't1 () und t2'

*** Error 90.43,

no typing for

'program And (x, y : 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 found for 'all'

### Hint 98.39,

untypeable term (with type: _v409 ->? Pred Unit) 'all'

*** Error 98.37,

no typing for

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

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

### Hint 101.29, no type found for 'all'

### Hint 101.29,

untypeable term (with type: _v420 ->? Pred Unit) 'all'

### Hint 101.9, rebound variable 'ff'

### Hint 101.29, no type found for 'all'

### Hint 101.29,

untypeable term (with type: _v421 ->? Pred Unit) 'all'

*** Error 101.27,

no typing for

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

### Hint 103.42,

in type of '(var r : Unit ->? Unit)'

typename 'Unit'

is not unifiable with type '_v436 ->? Pred Unit' (103.49)

### Hint 103.42,

untypeable term (with type: _v437 ->? _v436 ->? Pred Unit) 'r'

### Hint 103.42-103.44,

untypeable term (with type: _v436 ->? Pred Unit) 'r impl'

*** Error 103.40,

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

### Hint 108.3, no type found for 'all'

### Hint 108.3, untypeable term (with type: _v440 ->? Unit) 'all'

*** Error 108.3-108.63,

no typing for

'all

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

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

### Warning 115.7, unchanged class 'Cpo'

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

### Hint 119.16,

no kind found for 'c'

expected: {Cppo}

found: {Cpo}

### Hint 121.3, no type found for 'all'

### Hint 121.3, untypeable term (with type: _v442 ->? Unit) 'all'

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

### Hint 122.3, no type found for 'all'

### Hint 122.3, untypeable term (with type: _v445 ->? Unit) 'all'

*** Error 122.3-122.44,

no typing for

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

### Hint 123.3, no type found for 'all'

### Hint 123.3, untypeable term (with type: _v448 ->? Unit) 'all'

*** Error 123.3-123.57,

no typing for

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

### Hint 125.32, no type found for 'all'

### Hint 125.32, untypeable term (with type: _v451 ->? _v452) 'all'

*** Error 125.14-125.46,

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

### Hint 126.15, rebound variable 'x'

### Hint 126.38, no type found for 'all'

### Hint 126.38, untypeable term (with type: _v455 ->? _v456) 'all'

*** Error 126.14-126.52,

no typing for '(all \ n : 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 found for 'all'

### Hint 130.3, untypeable term (with type: _v458 ->? Unit) 'all'

*** Error 130.3-131.74,

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

### Hint 134.3, no type found for 'all'

### Hint 134.3, untypeable term (with type: _v460 ->? Unit) 'all'

*** Error 134.3-134.46,

no typing for 'all \ s : 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 found for 'all'

### Hint 143.3, untypeable term (with type: _v462 ->? Unit) 'all'

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

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

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

### Hint 119.14-119.18,

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

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

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

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

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

### 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 __<<=__ : forall c : Cpo . c * c)'

typename 'Unit' (119.14)

is not unifiable with type '_v477 ->? _v476 ->? Unit' (159.53)

### Hint 159.37,

untypeable term (with type: _v478 ->? _v477 ->? _v476 ->? Unit)

'__<<=__'

### Hint 159.37,

untypeable term (with type: _v477 ->? _v476 ->? Unit) 'x1 <<= x2'

### Hint 159.33-159.45,

untypeable term (with type: _v476 ->? Unit) '(x1 <<= x2) und'

*** Error 159.31,

no typing for

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

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

### Hint 169.20, 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 (\ 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))

*** Error 170.7, unexpected mixfix token: :

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

*** Error 176.41-176.68,

ambiguous mixfix term

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

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

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

### Hint 176.31, no type found for 'all'

### Hint 176.31, untypeable term (with type: _v502 ->? Unit) 'all'

*** Error 176.29,

no typing for

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

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

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

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

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

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

### Hint 182.16,

no kind found for 'd'

expected: {Cppo}

found: {Cpo}

*** 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.19,

no kind found for 'd'

expected: {Cppo}

found: {Cpo}

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

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

### Hint 184.19,

no kind found for 'd'

expected: {Cppo}

found: {Cpo}

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

### Hint 186.10, rebound variable 'f'

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

### Hint 186.16, rebound variable 'g'

### Hint 186.10, rebound variable 'f'

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

### Hint 186.16, rebound variable 'g'

### Hint 119.14-119.18,

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

### Hint 190.16,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 190.23,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 192.3, no type found for 'all'

### Hint 192.3, untypeable term (with type: _v521 ->? Unit) 'all'

*** 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.15,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 195.5, rebound variable 'f'

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

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

### Hint 195.18, rebound variable 'x'

### Hint 199.22,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 199.40,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 199.58,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 199.71,

no kind found for 'p'

expected: {Cppo}

found: {Pcpo}

### Hint 199.65-199.71,

no kind found for 'c --> p'

expected: {Cppo}

found: {Pcpo}

### Warning 204.20,

ignoring declaration for builtin identifier 'true'

### Warning 204.27,

ignoring declaration for builtin identifier 'false'