BasicSpec.hascasl.output revision 096b050a106eefe1093eb7659e4924b1d7850aa4
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachclass Type < Type
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettclass TYPE < {x . x < t}
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimbletttype : Type- -> Type; Unit : TYPE
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederclass a, b, c < Type
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachclass a, b, c < Type; a < b
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachpredfun tt : s ->? Unit
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram tt : s ->? Unit = \ x : s . ()
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettprogram __ res __ (x : s, y : t) : s : s = x;
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett fst (x : s, y : t) : s = x; snd (x : s, y : t) : t = y
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maederpredfun eq : s � s ->? Unit
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram all (p : (? s)) : (? Unit) = eq (p, tt)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram And (x, y : (? Unit)) : (? Unit) = t1 () res t2 ()
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram __ impl __ (x, y : (? Unit)) = eq (x, x And y)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram __ or __ (x, y : (? Unit)) : ? Unit : ? Unit =
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett all (\ r : (? Unit) . ((x impl r) res (y impl r)) impl r);
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett ex (p : (? s)) : (? Unit) =
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett all (\ r : (? Unit) . all (\ x : s . p (x) impl r) impl r);
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett ff () : ? Unit : ? Unit = all (\ r : (? Unit) . r ())
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettforall x : t; y : t
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (fun __=__ : forall a : Type . a � a ->? Unit) ((var x : t),
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachtype Data1 ::= a |
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachtype Data2 ::= Cons21 (Data1; Data2) |
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Cons22 (Data2; Data1) |
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimbletttype Data3 ::= Cons31 (sel1:? Data1; sel2:? Data2) |
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Cons32 (sel2:? Data2; sel1:? Data1)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachtype Data4 ::= Cons41 (sel1:? Data1; sel2:? Data2) ? |
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder Cons42 (sel2:? Data2; sel1:? Data1) ?
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett. (fun true : Unit)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett%% Classes ---------------------------------------------------------------
06dd4e7c29f33f6122a910719e3bd9062256e397Andy GimblettTYPE < {x . x < t}
a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'Reilly%% Type Constructors -----------------------------------------------------
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederData1 : Type %[type __ ::=
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederData2 : Type %[type __ ::=
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder Cons21 : Data1 �
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder Data2 -> __ (%(Data2.Cons21.sel_[1,1])% :? Data1)(%(Data2.Cons21.sel_[2,1])% :? Data2)
a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'Reilly Cons22 : Data2 �
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Data1 -> __ (%(Data2.Cons22.sel_[1,1])% :? Data2)(%(Data2.Cons22.sel_[2,1])% :? Data1)]%
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettData3 : Type %[type __ ::=
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Cons31 : Data1 � Data2 -> __ (sel1 :? Data1)(sel2 :? Data2)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Cons32 : Data2 � Data1 -> __ (sel2 :? Data2)(sel1 :? Data1)]%
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy GimblettData4 : Type %[type __ ::=
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Cons41 : Data1 � Data2 ->? __ (sel1 :? Data1)(sel2 :? Data2)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Cons42 : Data2 � Data1 ->? __ (sel2 :? Data2)(sel1 :? Data1)]%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettPred : Type -> Type := \ a : Type . a ->? Unit
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettUnit : TYPE := Unit
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett__-->__ : Type- -> Type+ -> Type
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett__-->?__ : Type- -> Type+ -> Type
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett__->__ : Type- -> Type+ -> Type
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett__->?__ : Type- -> Type+ -> Type
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett__�__ : Type+ -> Type+ -> Type
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettt : Type %(var)%
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett%% Assumptions -----------------------------------------------------------
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett%(Data2.Cons21.sel_[1,1])% : Data2 ->? Data1 %(select from Data2 constructed by
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Cons21 : Data1 � Data2 -> Data2)%
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett%(Data2.Cons21.sel_[2,1])% : Data2 ->? Data2 %(select from Data2 constructed by
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett Cons21 : Data1 � Data2 -> Data2)%
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett%(Data2.Cons22.sel_[1,1])% : Data2 ->? Data2 %(select from Data2 constructed by
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Cons22 : Data2 � Data1 -> Data2)%
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett%(Data2.Cons22.sel_[2,1])% : Data2 ->? Data1 %(select from Data2 constructed by
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Cons22 : Data2 � Data1 -> Data2)%
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettCons21 : Data1 � Data2 -> Data2 %(construct Data2)%
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCons22 : Data2 � Data1 -> Data2 %(construct Data2)%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettCons31 : Data1 � Data2 -> Data3 %(construct Data3)%
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCons32 : Data2 � Data1 -> Data3 %(construct Data3)%
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettCons41 : Data1 � Data2 ->? Data4 %(construct Data4)%
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy GimblettCons42 : Data2 � Data1 ->? Data4 %(construct Data4)%
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett__/\__ : Unit � Unit ->? Unit %(Fun)%
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett__<=>__ : Unit � Unit ->? Unit %(Fun)%
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett__=__ : forall a : Type . a � a ->? Unit %(Fun)%
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett__=>__ : Unit � Unit ->? Unit %(Fun)%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett__=e=__ : forall a : Type . a � a ->? Unit %(Fun)%
820947bd01ca952c3909eaa0366c6914c87cc1cbTill Mossakowski__\/__ : Unit � Unit ->? Unit %(Fun)%
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett__if__ : Unit � Unit ->? Unit %(Fun)%
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett__when__else__ : forall a : Type . a � Unit � a ->? a %(Fun)%
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimbletta : Data1 %(construct Data1)%
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettb : Data1 %(construct Data1)%
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettc : Data1 %(construct Data1)%
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettdef__ : forall a : Type . a ->? Unit %(Fun)%
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimbletteq : s � s ->? Unit %(Pred)%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettfalse : Unit %(Fun)%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettif__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettnot__ : Unit ->? Unit %(Fun)%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettsel1 : Data4 ->? Data1 %(select from Data4 constructed by
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (Cons41 : Data1 � Data2 ->? Data4,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Cons42 : Data2 � Data1 ->? Data4))%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett : Data3 ->? Data1 %(select from Data3 constructed by
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (Cons31 : Data1 � Data2 -> Data3,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Cons32 : Data2 � Data1 -> Data3))%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettsel2 : Data4 ->? Data2 %(select from Data4 constructed by
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (Cons41 : Data1 � Data2 ->? Data4,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Cons42 : Data2 � Data1 ->? Data4))%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett : Data3 ->? Data2 %(select from Data3 constructed by
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (Cons31 : Data1 � Data2 -> Data3,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Cons32 : Data2 � Data1 -> Data3))%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimbletttrue : Unit %(Fun)%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimbletttt : s ->? Unit %(Op)% = \ x : s . ()
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett%% Sentences -------------------------------------------------------------
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach(fun __=__ : forall a : Type . a � a ->? Unit) ((var x : t),
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (var y : t)) %()%
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett(fun true : Unit) %()%
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett%% Diagnostics -----------------------------------------------------------
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Error 1.7, illegal universe class declaration 'Type'
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Hint 3.5, is type variable 't'
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** FatalError 7.11, illegal type pattern argument: __
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Error 11.16, undeclared class 'd'
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett*** Warning 11.7, redeclared class 'a'
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Warning 11.10, redeclared class 'b'
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett*** Warning 11.13, redeclared class 'c'
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Warning 11.19, redeclared class 'a'
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett*** Error 20.12, unexpected mixfix token: res
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett*** Error 20.10, unexpected pattern '__ res __ (x : s, y : t)'
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett*** Error 20.37, unexpected mixfix token: x
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett*** Hint 21.1, no type match for: fst
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett with type: '_var_4 ->? s' (line 21, column 20)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Hint 21.1, wrong result type 's' (line 21, column 20)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett for application 'fst (x : s, y : t)'
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Error 21.1, no typing for 'fst(x : s, y : t) : s'
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett*** Hint 22.1, no type match for: snd
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett with type: '_var_5 ->? t' (line 22, column 20)
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett*** Hint 22.1, wrong result type 't' (line 22, column 20)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett for application 'snd (x : s, y : t)'
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Error 22.1, no typing for 'snd(x : s, y : t) : t'
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett*** Error 26.11, cyclic super type '? s'
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Hint 28.9, no type match for: all
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett with type: '_var_6 ->? ? Unit' (line 28, column 26)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Hint 28.9, wrong result type '? Unit' (line 28, column 26)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett for application 'all (p : ? s)'
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett*** Error 28.9, no typing for 'all(p : ? s) : ? Unit'
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett*** Hint 30.9, no type match for: And
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett with type: '_var_8 ->? ? Unit' (line 30, column 31)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett*** Hint 30.9, wrong result type '? Unit' (line 30, column 31)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett for application 'And (x : _var_7, y : ? Unit)'
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett*** Error 30.9, no typing for 'And(x : _var_7, y : ? Unit) : ? Unit'
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett*** Error 32.12, unexpected mixfix token: impl
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett*** Error 34.12, unexpected mixfix token: or
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett*** Error 34.10, unexpected pattern '__ or __ (x, y : (? Unit))'
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett*** Error 35.19, unexpected mixfix token: x
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett*** Error 34.44, unexpected mixfix token: all
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett*** Hint 37.3, no type match for: ex
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett with type: '_var_10 ->? ? Unit' (line 37, column 18)
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett*** Hint 37.3, wrong result type '? Unit' (line 37, column 18)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett for application 'ex (p : ? s)'
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett*** Error 37.3, no typing for 'ex(p : ? s) : ? Unit'
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett*** Error 40.7, unexpected mixfix token: )
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett*** Error 40.3, unexpected pattern 'ff ()'
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett*** Error 40.20, unexpected mixfix token: all
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett*** Error 66.25, unexpected mixfix token: e
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett*** Error 67.12, unexpected mixfix token: e