BasicSpec.hascasl.output revision 48708376ccab0e56251f53b0ec21499a277e9102
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder%% Classes ---------------------------------------------------------------
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian MaederTYPE = Type
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elknera < d
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskib < d
c34f9e8091bab44a6956db9bf4f2ae5d77d818fbChristian Maederc < d
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescud
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeder%% Type Constructors -----------------------------------------------------
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederData1 : Type %[type __ ::=
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeder a : -> __
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeder b : -> __
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder c : -> __]%
f97523766972a5b9dfb6e357ba3a9c71aa3afca9Christian MaederData2 : Type %[type __ ::=
c7c90bab17cfec4793ecf70b20c39f1622977a7eChristian Maeder Cons21 : Data1 �
9e6ce33401d2bbbe82156d59f6a9be0331d9a4b7Christian Maeder Data2 -> __ (%(Data2.Cons21.sel_[1,1])% :? Data1)(%(Data2.Cons21.sel_[2,1])% :? Data2)
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder Cons22 : Data2 �
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder Data1 -> __ (%(Data2.Cons22.sel_[1,1])% :? Data2)(%(Data2.Cons22.sel_[2,1])% :? Data1)]%
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian MaederData3 : Type %[type __ ::=
9e6ce33401d2bbbe82156d59f6a9be0331d9a4b7Christian Maeder Cons31 : Data1 � Data2 -> __ (sel1 :? Data1)(sel2 :? Data2)
c7c90bab17cfec4793ecf70b20c39f1622977a7eChristian Maeder Cons32 : Data2 � Data1 -> __ (sel2 :? Data2)(sel1 :? Data1)]%
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian MaederData4 : Type %[type __ ::=
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeder Cons41 : Data1 � Data2 ->? __ (sel1 :? Data1)(sel2 :? Data2)
9e6ce33401d2bbbe82156d59f6a9be0331d9a4b7Christian Maeder Cons42 : Data2 � Data1 ->? __ (sel2 :? Data2)(sel1 :? Data1)]%
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian MaederPred : Type- -> Type
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederPred__ : Type- -> Type
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederUnit : TYPE
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeders : (c, Type) < ? s
9e6ce33401d2bbbe82156d59f6a9be0331d9a4b7Christian Maedert : Type %(var)%
c7c90bab17cfec4793ecf70b20c39f1622977a7eChristian Maeder%% Assumptions -----------------------------------------------------------
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeder%(Data2.Cons21.sel_[1,1])% : Data2 ->? Data1 %(select from Data2 constructed by
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeder Cons21 : Data1 � Data2 -> Data2)%
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeder%(Data2.Cons21.sel_[2,1])% : Data2 ->? Data2 %(select from Data2 constructed by
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeder Cons21 : Data1 � Data2 -> Data2)%
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder%(Data2.Cons22.sel_[1,1])% : Data2 ->? Data2 %(select from Data2 constructed by
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian Maeder Cons22 : Data2 � Data1 -> Data2)%
59597e83448c2fc763557b56e0319615b33518d9Christian Maeder%(Data2.Cons22.sel_[2,1])% : Data2 ->? Data1 %(select from Data2 constructed by
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder Cons22 : Data2 � Data1 -> Data2)%
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederCons21 : Data1 � Data2 -> Data2 %(construct Data2)%
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederCons22 : Data2 � Data1 -> Data2 %(construct Data2)%
c1e44804ab02be8fa720960cfd1f2355dd8c0bbeChristian MaederCons31 : Data1 � Data2 -> Data3 %(construct Data3)%
c1e44804ab02be8fa720960cfd1f2355dd8c0bbeChristian MaederCons32 : Data2 � Data1 -> Data3 %(construct Data3)%
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederCons41 : Data1 � Data2 ->? Data4 %(construct Data4)%
993cbe47cbad455281db80ce9194d75ffe3f6febChristian MaederCons42 : Data2 � Data1 ->? Data4 %(construct Data4)%
152c178f9f9969ce729361a5c61aa4ff2c9ed840Christian Maedera : Data1 %(construct Data1)%
f27958e3207806f9fd3d579018e1921ce4f33b75Klaus Luettich : ? s
db3b74383c0afcd7a0aec50c263aec4f4e09df8dcmaederb : Data1 %(construct Data1)%
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maederc : Data1 %(construct Data1)%
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maedereq : s � s ->? Unit
681f20df85992a619d03e1adb933232a9515d7fcChristian Maedersel1 : Data4 ->? Data1 %(select from Data4 constructed by
8e58d2c3037f6bdd26e2f2c1e499cb6121ea806eChristian Maeder (Cons41 : Data1 � Data2 ->? Data4,
392581ea95e3a242153594d6d911c1aa5e0b0875Klaus Luettich Cons42 : Data2 � Data1 ->? Data4))%
075f71723257906d689c71a8b2fa6cce4b386317Christian Maeder : Data3 ->? Data1 %(select from Data3 constructed by
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder (Cons31 : Data1 � Data2 -> Data3,
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder Cons32 : Data2 � Data1 -> Data3))%
ad270004874ce1d0697fb30d7309f180553bb315Christian Maedersel2 : Data4 ->? Data2 %(select from Data4 constructed by
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder (Cons41 : Data1 � Data2 ->? Data4,
392581ea95e3a242153594d6d911c1aa5e0b0875Klaus Luettich Cons42 : Data2 � Data1 ->? Data4))%
8ecdb62fa2cef068eb4dbce59f3219a8e3adc0baChristian Maeder : Data3 ->? Data2 %(select from Data3 constructed by
9db318e6d01634c66e10dd0c6eb66c96305cb4f9Christian Maeder (Cons31 : Data1 � Data2 -> Data3,
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder Cons32 : Data2 � Data1 -> Data3))%
1a38107941725211e7c3f051f7a8f5e12199f03acmaedertt : s ->? Unit = \ x : s . ()
1a38107941725211e7c3f051f7a8f5e12199f03acmaederx : s %(var)%
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder%% Diagnostics -----------------------------------------------------------
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 1, column 7) illegal universe class declaration 'Type'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederWarning (line 5, column 32) unchecked type 't'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederWarning (line 5, column 20) redeclared class 'TYPE'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 5, column 20) inconsistent redefinition of 'TYPE'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederWarning (line 11, column 16) implicit declaration of superclass 'd'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederWarning (line 11, column 7) redeclared class 'a'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederWarning (line 11, column 10) redeclared class 'b'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederWarning (line 11, column 13) redeclared class 'c'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederWarning (line 11, column 19) redeclared class 'a'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 11, column 19) class cannot become an alias class 'a'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederHint (line 16, column 9) not a class 's'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 20, column 12) unexpected mixfix token 'res'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 21, column 5) unexpected mixfix token '('
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 22, column 5) unexpected mixfix token '('
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 28, column 13) unexpected mixfix token '('
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 30, column 13) unexpected mixfix token '('
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 32, column 12) unexpected mixfix token 'impl'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 34, column 12) unexpected mixfix token 'or'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 37, column 6) unexpected mixfix token '('
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 40, column 6) unexpected mixfix token '('
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederHint (line 45, column 11) not a class 't'
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian MaederError (line 45, column 8) wrong type scheme of 'x'
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian Maeder expected: s
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian Maeder found: t
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederHint (line 45, column 18) not a class 't'
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian MaederError (line 47, column 5) unexpected mixfix token '='
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederWarning (line 57, column 11) redeclared type 's'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 61, column 36) undeclared type 'Data2'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 61, column 52) undeclared type 'Data2'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederWarning (line 61, column 73) data subtype ignored
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 66, column 8) unexpected mixfix token 'true'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederHint (line 66, column 23) not a class 's'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 66, column 25) unexpected mixfix token 'e'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederHint (line 67, column 10) not a class 's'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaederError (line 67, column 12) unexpected mixfix token 'e'
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder