Prelude.hascasl.output revision 6cca02cb6a5ae882d887a879f8b7a71941c3715c
%% 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
type Pred __ : Type -> Type := \ t : Type- . t ->? Unit
type ? __ := \ t : Type . Unit ->? t
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
type : 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[_var_3_v3]
: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))
= \ (var x : s) : s_v1 . ()
%% def is also total (identical to tt)
program (op tt[_var_6_v6]
: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))
= \ (var x : s) : s_v1 . ()
%% tt is total "op tt(x: s): unit = ()"
program __ und __ (x, y : Unit) : Unit = ()
%% total function type
type __->__ : Type- -> Type+ -> Type
type __->__(s : Type)(t : Type) < s_v1 ->? t_v2
%% total functions
op __res__ : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1
= \ (var x : s, var y : t) .! (var x : s) as s_v1
op fst : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1
= \ (var x : s, var y : t) .! (var x : s) as s_v1
program snd (x : s, y : t) : t = y
%% trivial because its the strict function property
. (fun __=__[_var_27_v27 * _var_29_v29 ->? _var_27_v27]
: forall s : Type . s_v-1 * s_v-1 ->? Unit)
(op fst[_var_27_v27; _var_29_v29]
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1,
op __res__[_var_27_v27; _var_29_v29]
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Internal Logic
pred eq : s * s
. (fun __=__[s ->? Unit]
: forall s : Type . s_v-1 * s_v-1 ->? Unit)
(\ (var x : s) : s
. (pred eq[s] : forall s : Type . s_v-1 * s_v-1)
(var x : s, var x : s),
op tt[s] : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))
. (fun __=__[s * s ->? s]
: forall s : Type . s_v-1 * s_v-1 ->? Unit)
(\ (var x : s, var y : s)
. (op __res__[s; Unit]
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)
(var x : s,
(pred eq[s] : forall s : Type . s_v-1 * s_v-1)
(var x : s, var y : s)),
\ (var x : s, var y : s)
. (op __res__[s; Unit]
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)
(var y : s,
(pred eq[s] : forall s : Type . s_v-1 * s_v-1)
(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_v1
program all (p : Pred (s)) : Pred Unit = eq (p, tt)
%% the cast from ?s to s is still done manually here (for the strict "und")
program And (x, y : Pred Unit) : Pred Unit = t1 () und t2 ()
%% use "And" instead of "und" to avoid cast from "?unit" to "unit"
program __ impl __ (x, y : Pred Unit) : Pred Unit = eq (x, x And y)
program __ or __ (x, y : Pred Unit) : Pred Unit =
all (\ r : Pred Unit . ((x impl r) und (y impl r)) impl r)
program ex (p : Pred (s)) : Pred Unit =
all (\ r : Pred Unit . all (\ x : s . p (x) impl r) impl r)
program ff () : Pred Unit = all (\ r : Pred Unit . r ())
program neg (r : Pred Unit) : Pred Unit = r impl ff
%% 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(s : nat -> c_v98) :? Unit
= all (\ n : nat . s (n) <<= s (Suc (n)));
pred isBound(x : c_v98; s : nat -> c_v98) :? Unit
= all (\ n : nat . s (n) <<= x);
op sup : (nat -> c) ->? c;}
class Pcpo < Cpo
{var p : Pcpo; op bottom : p;}
class instance Flatcpo < Cpo
{var f : Flatcpo; program __ <<= [f] __ = eq}
var c : Cpo; d : Cpo
type instance __*__ : Cpo+ -> Cpo+ -> Cpo
var x1 : c; x2 : c; y1 : d; y2 : d
program (pred __<<=__[c * d] : forall c : Cpo . c_v-1 * c_v-1)
((var x1 : c, var y1 : d), (var x2 : c, var y2 : d))
= (x1 <<= x2) und (y1 <<= y2)
type instance __*__ : Pcpo+ -> Pcpo+ -> Pcpo
type Unit : Pcpo
%% Pcont
type instance __-->?__ : Cpo- -> Cpo+ -> Pcpo
type __-->?__(c : Cpo)(d : Cpo) < c_v98 ->? d_v103
program f <<= [c -->? d] g =
all (\ x : c . def (f x) impl f (x) <<= g (x))
%% Tcont
type instance __-->__ : Cpo- -> Cpo+ -> Cpo
type __-->__(c : Cpo)(d : Cpo) < c_v98 -->? d_v103
var f : c --> d; g : c --> d
program (pred __<<=__[c --> d] : forall c : Cpo . c_v-1 * c_v-1)
(var f : c --> d, var g : c --> d)
= f <<= [c -->? d] g
type instance __-->__ : Cpo- -> Pcpo+ -> Pcpo
op : (p -->? p) --> p
op undefined : c -->? p = Y (\ x : c -->? p .! x)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% user stuff
free type bool ::= true |
false
type bool : Flatcpo
type nat : Flatcpo
%% Classes ---------------------------------------------------------------
Cpo < Type
Flatcpo < Cpo
Pcpo < Cpo
%% Type Constructors -----------------------------------------------------
Logical : Type := Unit ->? Unit
Pred : Type -> Type := \ a : Type . a_v-1 ->? Unit
Unit : Pcpo
__*__
: (Cpo+ -> Cpo+ -> Cpo, Pcpo+ -> Pcpo+ -> Pcpo,
Type+ -> Type+ -> Type)
__-->__
: (Cpo- -> Cpo+ -> Cpo, Cpo- -> Pcpo+ -> Pcpo,
Type- -> Type+ -> Type) < (c_v98 -->? d_v103, __-->?__, __->__)
__-->?__
: (Cpo- -> Cpo+ -> Pcpo,
Type- -> Type+ -> Type) < (c_v98 ->? d_v103, __->?__)
__->__ : Type- -> Type+ -> Type < (s_v1 ->? t_v2, __->?__)
__->?__ : Type- -> Type+ -> Type
bool
: Flatcpo
%[free type bool
::= true : bool
false : bool]%
c : Cpo %(var_98)%
d : Cpo %(var_103)%
f : Flatcpo %(var_102)%
nat : Flatcpo
p : Pcpo %(var_101)%
s : Type %(var_1)%
t : Type %(var_2)%
%% Assumptions -----------------------------------------------------------
__/\__ : Unit * Unit ->? Unit %(fun)%
__<<=__ : forall c : Cpo . c_v-1 * c_v-1 ->? Unit %(pred)%
__<=>__ : Unit * Unit ->? Unit %(fun)%
__=__ : forall s : Type . s_v-1 * s_v-1 ->? Unit %(fun)%
__=>__ : Unit * Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__\/__ : Unit * Unit ->? Unit %(fun)%
__if__ : Unit * Unit ->? Unit %(fun)%
__res__
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1
%(op)% = \ (var x : s, var y : t) .! (var x : s) as s_v1
__when__else__
: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
bottom : forall p : Pcpo . p_v-1 %(fun)%
def : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit) %(op)%
def__ : forall a : Type . a_v-1 ->? Unit %(fun)%
eq : forall s : Type . s_v-1 * s_v-1 ->? Unit %(pred)%
f : c --> d %(var)%
false
: bool %(construct bool)%
: Unit ->? Unit %(pred)%
: Unit %(fun)%
fst
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1
%(op)% = \ (var x : s, var y : t) .! (var x : s) as s_v1
g : c --> d %(var)%
not : Unit ->? Unit %(pred)%
not__ : ? Unit ->? Unit %(fun)%
sup : forall c : Cpo . (nat -> c_v-1) ->? c_v-1 %(op)%
true
: bool %(construct bool)%
: Unit ->? Unit %(pred)%
: Unit %(fun)%
tt : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit) %(op)%
x : s %(var)%
x1 : c %(var)%
x2 : c %(var)%
y1 : d %(var)%
y2 : d %(var)%
�__ : ? Unit ->? Unit %(fun)%
%% Sentences -------------------------------------------------------------
program (op def[_var_3_v3]
: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))
= \ (var x : s) : s_v1 . () %(pe_def)%
program (op tt[_var_6_v6]
: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))
= \ (var x : s) : s_v1 . () %(pe_tt)%
forall x : s; y : t
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op __res__ : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)
(var x : s, var y : t),
(var x : s) as s_v1) %(def___res__)%
forall x : s; y : t
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op fst : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)
(var x : s, var y : t),
(var x : s) as s_v1) %(def_fst)%
(fun __=__[_var_27_v27 * _var_29_v29 ->? _var_27_v27]
: forall s : Type . s_v-1 * s_v-1 ->? Unit)
(op fst[_var_27_v27; _var_29_v29]
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1,
op __res__[_var_27_v27; _var_29_v29]
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)
(fun __=__[s ->? Unit] : forall s : Type . s_v-1 * s_v-1 ->? Unit)
(\ (var x : s) : s
. (pred eq[s] : forall s : Type . s_v-1 * s_v-1)
(var x : s, var x : s),
op tt[s] : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit))
(fun __=__[s * s ->? s] : forall s : Type . s_v-1 * s_v-1 ->? Unit)
(\ (var x : s, var y : s)
. (op __res__[s; Unit]
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)
(var x : s,
(pred eq[s] : forall s : Type . s_v-1 * s_v-1)
(var x : s, var y : s)),
\ (var x : s, var y : s)
. (op __res__[s; Unit]
: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1)
(var y : s,
(pred eq[s] : forall s : Type . s_v-1 * s_v-1)
(var x : s, var y : s)))
free type bool
::= true : bool
false : bool %(ga_bool)%
%% Diagnostics -----------------------------------------------------------
*** Error 4.7, illegal universe class declaration 'Type'
*** Hint 6.5, is type variable 's'
*** Hint 6.7, is type variable 't'
*** Hint 11.6, redeclared type 'Unit'
*** FatalError 14.11, illegal type pattern argument: __
*** FatalError 15.8, illegal type pattern argument: __
*** Error 17.6, illegal overloading of predefined identifier 'true'
*** Error 17.12, illegal overloading of predefined identifier 'false'
*** Error 19.9, illegal overloading of predefined identifier '__/\__'
*** Error 19.17, illegal overloading of predefined identifier '__\/__'
*** Error 19.25, illegal overloading of predefined identifier '__=>__'
*** Error 19.33, illegal overloading of predefined identifier '__if__'
*** Error 19.40, illegal overloading of predefined identifier '__<=>__'
*** Error 22.8, illegal overloading of predefined identifier '__=__'
*** Hint 27.8, redeclared type '__->?__'
*** Hint 30.8, redeclared type '__*__'
*** FatalError 31.6, illegal type pattern: __ * __ * __
*** Warning 42.16, variable shadows global name(s) 'x'
*** Warning 44.15, variable shadows global name(s) 'x'
*** Error 46.11, unexpected mixfix token: und
*** Hint 50.8, redeclared type '__->__'
*** Error 52.8, incompatible kind of: __->__
expected: Type- -> Type+ -> Type
found: Type -> Type -> Type
*** Error 54.42, ambiguous mixfix term
def__(f(x))
def(f)(x)
*** Error 54.32, unexpected mixfix token: all
*** Error 54.6, unexpected mixfix token: :
*** Hint 60.9, no type match for: snd
with (maximal) type: _var_9_v9 ->? t_v2
known types:
*** Hint 60.9, untypable application (with result type: t_v2)
'snd(x : s_v1, var y : t_v2)'
*** Error 60.9, no typing for 'snd(x : s_v1, var y : t_v2) : t_v2'
*** Error 65.18, ambiguous mixfix term
def(__res__(x, y))
def__(__res__(x, y))
*** Error 65.59, unexpected mixfix token: und
*** Warning 74.5, variable shadows global name(s) 'x'
*** Warning 75.6, variable shadows global name(s) 'x'
*** Warning 75.35, variable shadows global name(s) 'x'
*** Hint 85.6, redeclared type 's'
*** Error 85.6, merge: TypeVarDefn of 's'
*** Error 85.11, illegal supertype for variable '? s_v1'
*** Hint 87.9, no type match for: all
with (maximal) type: _var_91_v91 ->? Unit ->? Unit
known types:
*** Hint 87.9, untypable application (with result type: Unit ->? Unit)
'all(var p : s_v1 ->? Unit)'
*** Error 87.9, no typing for 'all(var p : s_v1 ->? Unit) : Unit ->? Unit'
*** Hint 90.9, no type match for: And
with (maximal) type: _var_92_v92 ->? Unit ->? Unit
known types:
*** Hint 90.9, untypable application (with result type: Unit ->? Unit)
'And(x, var y : Unit ->? Unit)'
*** Error 90.9, no typing for 'And(x, var y : Unit ->? Unit) : Unit ->? Unit'
*** Error 93.11, unexpected mixfix token: impl
*** Error 95.11, unexpected mixfix token: or
*** Hint 98.9, no type match for: ex
with (maximal) type: _var_93_v93 ->? Unit ->? Unit
known types:
*** Hint 98.9, untypable application (with result type: Unit ->? Unit)
'ex(var p : s_v1 ->? Unit)'
*** Error 98.9, no typing for 'ex(var p : s_v1 ->? Unit) : Unit ->? Unit'
*** Hint 101.9, no type match for: ff
with (maximal) type: _var_94_v94 ->? Unit ->? Unit
known types:
*** Hint 101.9, untypable application (with result type: Unit ->? Unit)
'ff()'
*** Error 101.9, no typing for 'ff() : Unit ->? Unit'
*** Hint 103.9, no type match for: neg
with (maximal) type: _var_95_v95 ->? Unit ->? Unit
known types:
*** Hint 103.9, untypable application (with result type: Unit ->? Unit)
'neg(var r : Unit ->? Unit)'
*** Error 103.9, no typing for 'neg(var r : Unit ->? Unit) : Unit ->? Unit'
*** 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 126.38, unexpected mixfix token: all
*** Error 131.42, unexpected mixfix token: isBound
*** Error 130.32, unexpected mixfix token: impl
*** Error 130.3, unexpected mixfix token: all
*** Error 134.20, unexpected mixfix token: isChain
*** Error 134.3, unexpected mixfix token: all
*** Hint 139.5, is type variable 'p'
*** Error 141.4, illegal overloading of predefined 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, redeclared type 'c'
*** Hint 153.8, is type variable 'd'
*** Error 159.45, unexpected mixfix token: und
*** Error 169.9, incompatible kind of: __-->?__
expected: Type- -> Type+ -> Type
found: Type -> Type -> Type
*** Error 171.35, unexpected mixfix token: und
*** Error 174.45, unexpected mixfix token: +
*** Error 173.40, unexpected mixfix token: und
*** Error 172.28, unexpected mixfix token: isChain
*** Error 171.9, unexpected mixfix token: all
*** Error 170.7, unexpected mixfix token: :
*** Hint 10.18, no type match for: __::__
with (maximal) type: _var_126_v126 ->? _var_124_v124 ->? _var_125_v125
known types:
*** Hint 10.18, untypable application (with result type: _var_124_v124 ->? _var_125_v125)
'__::__(c(var -->? : _var_116_v116)(var d : _var_117_v117), [])'
*** Error 10.18, untypable application '__::__(c(var -->? : _var_116_v116)(var d : _var_117_v117), [])
(var g : _var_118_v118)'
*** Error 176.13, untypable application '__<<=__
(var f : _var_115_v115,
__::__(c(var -->? : _var_116_v116)(var d : _var_117_v117), [])
(var g : _var_118_v118))'
*** Error 176.13, no typing for '__<<=__(var f : _var_115_v115,
__::__(c(var -->? : _var_116_v116)(var d : _var_117_v117), [])
(var g : _var_118_v118))'
*** Error 181.9, incompatible kind of: __-->__
expected: Type- -> Type+ -> Type
found: Type -> Type -> Type
*** Error 182.46, ambiguous mixfix term
def__(f(x))
def(f)(x)
*** Error 182.36, unexpected mixfix token: all
*** Error 182.7, unexpected mixfix token: :
*** Error 186.26, unexpected mixfix token: c
*** Error 190.9, incompatible kind of: p_v101 -->? p_v101
expected: Cpo-
found: Type
*** Error 193.32, unexpected mixfix token: impl
*** Error 192.27, unexpected mixfix token: Y
*** Error 192.3, unexpected mixfix token: all
*** Error 195.27, unexpected mixfix token: Y
*** Error 200.20, illegal overloading of predefined identifier 'true'
*** Error 200.27, illegal overloading of predefined identifier 'false'