2362N/A%% predefined universe containing all types,
0N/A%% superclass of all other classes
2362N/A%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0N/A%% invisible type "Unit" for formulae
0N/A %% flat cpo with bottom
0N/Apreds true, false : Unit
0N/Apreds __/\__, __\/__, __=>__, __if__, __<=>__ : Unit * Unit
2362N/A%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2362N/A%% (builtin) type (constructors)
2362N/Atype __->?__ : -Type -> +Type -> Type
0N/A%% nested pairs are different from n-tupels (n > 2)
0N/Atype __*__ : +Type -> +Type -> Type
0N/A%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0N/A%% "pred p args = e" abbreviates "op p args :? unit = e"
0N/A%% CASL requires "<=>" for pred-defn and disallows "()" as result
0N/A%% def is also total (identical to tt)
0N/A%% tt is total "op tt(x: s): unit = ()"
0N/A%% total function type
0N/Atype __->__ : -Type -> +Type -> Type
0N/Atype __->__ < __->?__
0N/Aop __res__(x : s; y : t) : s = x;
0N/Aop fst(x : s; y : t) : s = x;
0N/Aprogram snd (x : s, y : t) : t = y;
0N/A%% trivial because its the strict function property
0N/A. (\ (x : s, y : t) . def (x res y))
0N/A = \ (x : s, y : t) . (def y) und (def x)
0N/A%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0N/A. (\ x : s . eq (x, x)) = tt
0N/A. (\ (x, y : s) . x res eq (x, y))
0N/A = \ (x, y : s) . y res eq (x, y);
0N/A%% notation "\ ." abbreviates "\bla:unit."
0N/A%% where "bla" is never used, but only "()" instead
0N/A%% for type inference
0N/A%% an implicit cast from s to ?s of a term "e" yields the term "\ . e"
0N/A%% the cast from ?s to s is still done manually here (for the strict "und")
0N/A%% use "And" instead of "und" to avoid cast from "?unit" to "unit"
0N/A%% the type instance for the first "eq" should be "?t"
0N/A%% this is explicitely enforced by "\ .f(x)"
0N/A%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0N/A%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"
0N/A pred __<<=__ : c * c
0N/A pred isChain : forall c : Cpo . nat -> c
0N/A pred isBound : forall c : Cpo . c * (nat -> c)
0N/A op sup : (nat -> c) ->? c
0N/Aprogram __<<=[f] = eq;
0N/Atype instance __*__ : +Cpo -> +Cpo -> Cpo
0N/Avars x1, x2 : c; y1, y2 : d
0N/Atype instance __*__ : +Pcpo -> +Pcpo -> Pcpo
0N/Atype instance __-->?__ : -Cpo -> +Cpo -> Pcpo
0N/Atype __-->?__ < __->?__
0N/Atype instance __-->__ : -Cpo -> +Cpo -> Cpo
0N/Aprogram f <<= g = f <<=[c -->? d] g;
0N/Atype instance __-->__ : -Cpo -> +Pcpo -> Pcpo
0N/Afun Y : (p --> p) --> p
0N/Avars f : p --> p; x : p
0N/A. f x = x => Y f <<= x;
0N/Aop undefined : c --> p =
0N/A Y ((\ x' : c --> p . x') as (c --> p) --> c --> p);
0N/A%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0N/Afree type bool ::= true | false
0N/A%% Classes ---------------------------------------------------------------
0N/A%% Type Constructors -----------------------------------------------------
0N/Abool : Flatcpo %[free type bool ::= false | true]%
0N/A%% Type Variables --------------------------------------------------------
0N/Af : Flatcpo %(var_366)%
0N/A%% Assumptions -----------------------------------------------------------
0N/AY : forall p : Pcpo . (p --> p) --> p %(fun)%
0N/A__<<=__ : forall c : Cpo . c * c ->? Unit %(pred)%
0N/A__res__ : forall s : Type; t : Type . s * t -> s
0N/A %(op)% = \ ((var x : s), (var y : t)) .! (var x : s)
0N/Abottom : forall p : Pcpo . p %(op)%
0N/Adef : forall s : Type . Pred s %(op)%
0N/Aeq : forall s : Type . s * s ->? Unit %(pred)%
0N/Afst : forall s : Type; t : Type . s * t -> s
0N/A %(op)% = \ ((var x : s), (var y : t)) .! (var x : s)
0N/AisBound : forall c : Cpo . c * (nat -> c) ->? Unit %(pred)%
0N/AisChain : forall c : Cpo . (nat -> c) ->? Unit %(pred)%
0N/Anot : Unit ->? Unit %(pred)%
0N/Asnd : s * t ->? t %(op)%
0N/Asup : forall c : Cpo . (nat -> c) ->? c %(op)%
0N/Att : forall s : Type . Pred s %(op)%
0N/Aundefined : forall p : Pcpo; c : Cpo . c --> p
0N/A (fun Y : forall p : Pcpo . (p --> p) --> p)
0N/A ((\ (var x' : c --> p) . (var x' : c --> p)) as
0N/A (c --> p) --> c --> p)
0N/A%% Variables -------------------------------------------------------------
0N/A%% Sentences -------------------------------------------------------------
0N/Aprogram def : Pred s = (\ x . ()) : s ->? Unit %(pe_def)%
0N/Aprogram tt : Pred s = (\ x . ()) : s ->? Unit %(pe_tt)%
0N/Aforall x : s; y : t . x res y = (x as s) %(def___res__)%
0N/Aforall x : s; y : t . fst (x, y) = (x as s) %(def_fst)%
0N/Aprogram (var snd : s * t ->? t) (x, y : t) : t = y %(pe_snd)%
0N/A(\ (x, y : t) . def (x res y)) = \ (x, y : t) . (def y) und (def x)
0N/A(\ x . eq (x, x)) = tt
0N/A(\ (x, y : s) . x res eq (x, y)) = \ (x, y : s) . y res eq (x, y)
0N/Aprogram __<<=__ : f * f ->? Unit = eq : f * f ->? Unit
0N/Aprogram (__<<=__ : (c --> d) * (c --> d) ->? Unit) (f, g) : Unit
0N/A = (__<<=__ : (c -->? d) * (c -->? d) ->? Unit) (f, g) : Unit
0N/A= (Y ((\ x' : c --> p . x') as (c --> p) --> c --> p) as c --> p)
0N/Afree type bool ::= false | true %(ga_bool)%
0N/A%% Diagnostics -----------------------------------------------------------
0N/A### Warning 4.7, void universe class declaration 'Type'
0N/A### Hint 6.5, is type variable 's'
0N/A### Hint 6.7, is type variable 't'
0N/A### Hint 11.6, redeclared type 'Unit'
0N/A*** Error 14.11, illegal type pattern argument '__'
0N/A*** Error 15.8, illegal type pattern argument '__'
0N/A### Warning 17.6, ignoring declaration for builtin identifier 'true'
0N/A### Warning 17.12, ignoring declaration for builtin identifier 'false'
0N/A### Warning 19.9, ignoring declaration for builtin identifier '__/\__'
0N/A### Warning 19.17, ignoring declaration for builtin identifier '__\/__'
0N/A### Warning 19.25, ignoring declaration for builtin identifier '__=>__'
0N/A### Warning 19.33, ignoring declaration for builtin identifier '__if__'
0N/A### Warning 19.40, ignoring declaration for builtin identifier '__<=>__'
0N/A### Warning 22.8, ignoring declaration for builtin identifier '__=__'
0N/A### Hint 27.8, redeclared type '__->?__'
0N/A### Hint 30.8, redeclared type '__*__'
0N/A*** Error 31.6-31.12, illegal type pattern '__ * __ * __'
0N/A### Hint 40.7, not a class 's'
0N/A### Hint 42.16, rebound variable 'x'
0N/A### Hint 42.9, repeated declaration of 'def'
0N/A### Hint 44.15, rebound variable 'x'
0N/A### Hint 44.9, repeated declaration of 'tt'
0N/A*** Error 46.11, unexpected mixfix token: und
0N/A### Hint 50.8, redeclared type '__->__'
0N/A### Hint 52.8, redeclared type '__->__'
0N/A### Hint, repeated supertype '__->?__'
0N/A*** Error 54.42-54.49, ambiguous mixfix term
0N/A*** Error 54.6, unexpected mixfix token: :
0N/A### Hint 58.13, rebound variable 'x'
0N/A### Hint 59.9, rebound variable 'x'
0N/A### Hint 60.14, rebound variable 'x'
0N/A### Hint 60.14, rebound variable 'x'
0N/A### Warning 60.13-60.24, illegal lhs pattern '(var snd : s * t ->? t) ((var x : s), (var y : t))'
0N/A*** Error 65.18-65.30, ambiguous mixfix term
0N/A*** Error 65.51-65.69, ambiguous mixfix term
0N/A### Hint 65.7, rebound variable 'x'
0N/A*** Error 65.18-65.30, unexpected term 'def (x res y)'
0N/A### Hint 65.40, rebound variable 'x'
0N/A*** Error 65.51-65.69, unexpected term '(def y) und (def x)'
0N/A*** Error 65.16, in term '(\ ((var x : s), (var y : t)) . def (x res y))
0N/A= \ ((var x : s), (var y : t)) . (def y) und (def x)'
0N/A are uninstantiated type variables '[_v50]'
0N/A*** Error 66.7, in term '(op fst : forall s : Type; t : Type . s * t -> s)
0N/A= (op __res__ : forall s : Type; t : Type . s * t -> s)'
0N/A are uninstantiated type variables '[_v88, _v90]'
0N/A### Hint 74.5, rebound variable 'x'
0N/A### Hint 75.6, rebound variable 'x'
0N/A### Hint 75.35, rebound variable 'x'
0N/A### Warning 85.6, new type shadows type variable 's'
0N/A*** Error 85.11, illegal type variable as supertype 's'
0N/A### Hint 87.40, in type of '(pred eq : forall s : Type . s * s)'
0N/A is not unifiable with type 'Unit ->? Unit' (87.33)
0N/A### Hint 87.40, untypable term (with type: _v229 ->? Pred Unit)
0N/A*** Error 87.38, no typing for 'program all (p : Pred s) : Pred Unit = eq (p, tt)'
0N/A### Hint 90.14, rebound variable 'x'
0N/A### Hint 90.45, no type found for 't1'
0N/A### Hint 90.45, no type found for 't1'
0N/A### Hint 90.45, untypable term (with type: ? (_v263 ->? _v262 ->? Unit ->? Pred Unit))
0N/A### Hint 90.45-90.47, untypable term (with type: _v263 ->? _v262 ->? Unit ->? Pred Unit)
0N/A### Hint 90.45-90.50, untypable term (with type: _v262 ->? Unit ->? Pred Unit)
0N/A### Hint 90.45, no type found for 't1'
0N/A### Hint 90.45, no type found for 't1'
0N/A### Hint 90.45, untypable term (with type: ? (_v265 ->? _v264 ->? ? (Pred Unit)))
0N/A### Hint 90.45-90.47, untypable term (with type: _v265 ->? _v264 ->? ? (Pred Unit))
0N/A### Hint 90.45-90.50, untypable term (with type: _v264 ->? ? (Pred Unit))
0N/A### Hint 90.45-90.54, untypable term (with type: ? (Pred Unit))
0N/A*** Error 90.43, no typing for 'program And (x, y : Pred Unit) : Pred Unit = t1 () und t2 ()'
0N/A*** Error 93.11, unexpected mixfix token: impl
0N/A*** Error 95.11, unexpected mixfix token: or
0N/A### Hint 98.39, no type found for 'all'
0N/A### Hint 98.39, untypable term (with type: _v291 ->? Pred Unit)
0N/A*** Error 98.37, no typing for 'program ex (p : Pred s) : Pred Unit
0N/A = all \ r : Pred Unit . (all \ x : s . p x impl r) impl r'
0N/A### Hint 101.29, no type found for 'all'
0N/A### Hint 101.29, untypable term (with type: _v306 ->? Pred Unit)
0N/A### Hint 101.9, rebound variable 'ff'
0N/A### Hint 101.29, no type found for 'all'
0N/A### Hint 101.29, untypable term (with type: _v307 ->? Pred Unit)
0N/A*** Error 101.27, no typing for 'program ff () : Pred Unit = all \ r : Pred Unit . r ()'
0N/A### Hint 103.44, no type found for 'impl'
0N/A### Hint 103.44, untypable term (with type: _v332)
0N/A### Hint 103.42-103.44, untypable term (with type: _v331 ->? Pred Unit)
0N/A*** Error 103.40, no typing for 'program neg (r : Pred Unit) : Pred Unit = r impl ff'
0N/A### Hint 108.3, no type found for 'all'
0N/A### Hint 108.3, untypable term (with type: _v343 ->? Unit)
0N/A*** Error 108.3-108.63, no typing for 'all
0N/A . all \ x : s . eq (\ () . f x, g x) impl eq (f, g)'
0N/A### Hint 117.5, is type variable 'c'
0N/A### Hint 121.3, no type found for 'all'
0N/A### Hint 121.3, untypable term (with type: _v345 ->? Unit)
0N/A*** Error 121.3-121.16, no typing for 'all \ x : c . x <<= x'
0N/A### Hint 122.3, no type found for 'all'
0N/A### Hint 122.3, untypable term (with type: _v348 ->? Unit)
0N/A*** Error 122.3-122.44, no typing for 'all \ (x, y, z : c) . (x <<= y) und (y <<= z) impl x <<= z'
0N/A### Hint 123.3, no type found for 'all'
0N/A### Hint 123.3, untypable term (with type: _v351 ->? Unit)
0N/A*** Error 123.3-123.57, no typing for 'all \ (x, y, z : c) . (x <<= y) und (y <<= x) impl eq (x, y)'
0N/A### Hint 125.32, no type found for 'all'
0N/A### Hint 125.32, untypable term (with type: _v354 ->? _v355)
0N/A*** Error 125.14-125.46, no typing for 'all \ n : nat . s n <<= s (Suc n) as Unit'
0N/A### Hint 126.15, rebound variable 'x'
0N/A### Hint 126.38, no type found for 'all'
0N/A### Hint 126.38, untypable term (with type: _v358 ->? _v359)
0N/A*** Error 126.14-126.52, no typing for 'all \ n : nat . s n <<= x as Unit'
0N/A*** Error 130.21-131.74, ambiguous mixfix term
0N/A ((((isBound (sup s, s)) und) all)
0N/A (\ x : c . ((((isBound (x, s)) impl) sup) s) <<= x)))
0N/A ((def (sup s)) impl)
0N/A((((isBound (sup s, s)) und) all)
0N/A (\ x : c . ((((isBound (x, s)) impl) sup) s) <<= x))
0N/A### Hint 130.3, no type found for 'all'
0N/A### Hint 130.3, untypable term (with type: _v361 ->? Unit)
0N/A*** Error 130.3-131.74, no typing for 'all
0N/A (isBound (sup s, s) und all
0N/A (\ x : c . isBound (x, s) impl sup (s) <<= x))'
0N/A### Hint 134.3, no type found for 'all'
0N/A### Hint 134.3, untypable term (with type: _v363 ->? Unit)
0N/A*** Error 134.3-134.46, no typing for 'all \ s : nat -> c . isChain s impl def (sup s)'
0N/A### Hint 139.5, is type variable 'p'
0N/A### Hint 143.3, no type found for 'all'
0N/A### Hint 143.3, untypable term (with type: _v365 ->? Unit)
0N/A*** Error 143.3-143.22, no typing for 'all \ x : p . bottom <<= x'
0N/A### Hint 148.6, is type variable 'f'
0N/A### Hint 150.15-150.17, is type list '[f]'
0N/A### Hint 150.12, repeated declaration of '__<<=__'
0N/A### Hint 153.5, is type variable 'c'
0N/A### Hint 153.5, rebound type variable 'c'
0N/A### Hint 153.8, is type variable 'd'
0N/A### Hint 157.7, not a class 'c'
0N/A### Hint 157.11, not a class 'c'
0N/A### Hint 157.18, not a class 'd'
0N/A### Hint 157.23, not a class 'd'
0N/A### Hint 159.10, rebound variable 'x1'
0N/A### Hint 159.14, rebound variable 'y1'
0N/A### Hint 159.23, rebound variable 'x2'
0N/A### Hint 159.27, rebound variable 'y2'
0N/A### Hint 159.37, in type of '(pred __<<=__ : forall c : Cpo . c * c)'
0N/A is not unifiable with type '_v390 ->? _v389 ->? Unit' (159.53)
0N/A### Hint 159.37, untypable term (with type: _v391 ->? _v390 ->? _v389 ->? Unit)
0N/A### Hint 159.37, untypable term (with type: _v390 ->? _v389 ->? Unit)
0N/A### Hint 159.33-159.45, untypable term (with type: _v389 ->? Unit)
0N/A*** Error 159.31, no typing for 'program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2)'
0N/A### Hint 169.9, redeclared type '__-->?__'
0N/A### Hint, repeated supertype '__->?__'
0N/A*** Error 171.24-171.61, ambiguous mixfix term
0N/A (def (((f x) und) x)) <<= y
0N/A (((def (f x)) und) x) <<= y
0N/A*** Error 174.45, unexpected mixfix token: +
0N/A*** Error 173.28-174.61, ambiguous mixfix term
0N/A def ((((f (s m)) und) eq)
0N/A (sup (\ n : nat .! f (s (n + m))), f (sup s)))
0N/A ((((def f) (s m)) und) eq)
0N/A(sup (\ n : nat .! f (s (n + m))), f (sup s))
0N/A*** Error 170.7, unexpected mixfix token: :
0N/A### Hint 176.16-176.25, is type list '[c -->? d]'
0N/A*** Error 176.41-176.68, ambiguous mixfix term
0N/A (def ((((f x) impl) f) x)) <<= (g x)
0N/A ((((def (f x)) impl) f) x) <<= (g x)
0N/A### Hint 176.31, no type found for 'all'
0N/A### Hint 176.31, untypable term (with type: _v422 ->? Unit)
0N/A*** Error 176.29, no typing for 'program f <<=[c -->? d] g
0N/A = all \ x : c . def (f x) impl f (x) <<= g (x)'
0N/A*** Error 181.17-181.23, non-unique kind for '__ -->? __'
0N/A*** Error 182.46-182.53, ambiguous mixfix term
0N/A*** Error 182.7, unexpected mixfix token: :
0N/A### Hint 184.7, not a kind 'c --> d'
0N/A### Hint 184.11, not a kind 'c --> d'
0N/A### Hint 186.25-186.34, is type list '[c -->? d]'
0N/A### Hint 186.10, rebound variable 'f'
0N/A### Hint 186.16, rebound variable 'g'
0N/A### Hint 186.10, rebound variable 'f'
0N/A### Hint 186.16, rebound variable 'g'
0N/A### Hint 186.12, repeated declaration of '__<<=__'
0N/A### Hint 192.3, no type found for 'all'
0N/A### Hint 192.3, untypable term (with type: _v456 ->? Unit)
0N/A*** Error 192.3-193.47, no typing for 'all
0N/A . eq (f (Y f), Y f) und all \ x : p . eq (f x, x) impl Y f <<= x'
0N/A### Hint 195.7, not a kind 'p --> p'
0N/A### Hint 195.5, rebound variable 'f'
0N/A### Hint 195.20, not a class 'p'
0N/A### Hint 195.18, rebound variable 'x'
0N/A### Warning 204.20, ignoring declaration for builtin identifier 'true'
0N/A### Warning 204.27, ignoring declaration for builtin identifier 'false'