Changeset 11877 for trunk/HasCASL/test/Prelude.hascasl
- Timestamp:
- 03.07.2009 18:38:45 (5 months ago)
- Files:
-
- 1 modified
-
trunk/HasCASL/test/Prelude.hascasl (modified) (15 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/HasCASL/test/Prelude.hascasl
r4544 r11877 1 %% predefined universe containing all types, 1 %% predefined universe containing all types, 2 2 %% superclass of all other classes 3 3 4 4 class Type 5 5 6 var s,t : Type 6 var s,t : Type 7 7 8 8 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% … … 12 12 13 13 %% type aliases 14 type Pred __ : Type -> Type := \ t: -Type . t ->? Unit15 type ? __ := \ t:Type .Unit ->? t14 type Pred __ (t: -Type) := t ->? Unit 15 type ? __ (t:Type) := Unit ->? t 16 16 17 17 pred true, false : Unit … … 34 34 35 35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 36 %% "pred p args = e" abbreviates "op p args :? unit = e" 36 %% "pred p args = e" abbreviates "op p args :? unit = e" 37 37 %% CASL requires "<=>" for pred-defn and disallows "()" as result 38 38 … … 40 40 var x : s 41 41 42 program def = \x: s . () %% def is also total (identical to tt) 42 program def = \x: s . () %% def is also total (identical to tt) 43 43 44 44 program tt = \x: s . () %% tt is total "op tt(x: s): unit = ()" … … 48 48 49 49 %% total function type 50 type __->__ : -Type -> +Type -> Type 50 type __->__ : -Type -> +Type -> Type 51 51 52 52 type __->__ < __ ->? __ … … 56 56 57 57 %% total functions 58 op __res__ (x: s; y: t) : s = x 59 op fst (x: s; y: t) : s = x 60 program snd (x: s, y: t) : t = y 58 op __res__ (x: s; y: t) : s = x 59 op fst (x: s; y: t) : s = x 60 program snd (x: s, y: t) : t = y 61 61 62 62 63 63 %% trivial because its the strict function property 64 64 65 . (\ (x:s, y:t). def (x res y)) = (\ (x:s, y:t). (def y) und (def x)) 65 . (\ (x:s, y:t). def (x res y)) = (\ (x:s, y:t). (def y) und (def x)) 66 66 . fst = (__ res__) 67 67 … … 77 77 %% then %def 78 78 79 %% notation "\ ." abbreviates "\bla:unit." 79 %% notation "\ ." abbreviates "\bla:unit." 80 80 %% where "bla" is never used, but only "()" instead 81 81 82 %% for type inference 82 %% for type inference 83 83 %% an implicit cast from s to ?s of a term "e" yields the term "\ . e" 84 84 … … 93 93 program __impl__ (x, y: Pred Unit) : Pred Unit = eq(x, x And y) 94 94 95 program __or__ (x, y: Pred Unit) : Pred Unit = all(\r: Pred Unit. 95 program __or__ (x, y: Pred Unit) : Pred Unit = all(\r: Pred Unit. 96 96 ((x impl r) und (y impl r)) impl r) 97 97 … … 103 103 program neg (r: Pred Unit) : Pred Unit = r impl ff 104 104 105 %% the type instance for the first "eq" should be "?t" 105 %% the type instance for the first "eq" should be "?t" 106 106 %% this is explicitely enforced by "\ .f(x)" 107 107 … … 109 109 110 110 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 111 %% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+" 111 %% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+" 112 112 113 113 type nat … … 124 124 125 125 pred isChain (s: nat -> c) <=> all(\n:nat. s(n) <<= s(Suc(n))) 126 pred isBound (x: c; s: nat -> c) <=> all(\n:nat. s(n) <<= x) 126 pred isBound (x: c; s: nat -> c) <=> all(\n:nat. s(n) <<= x) 127 127 128 128 op sup : (nat -> c) ->? c … … 139 139 var p : Pcpo 140 140 141 op bottom : p 142 143 . all(\x : p. bottom <<= x) 141 op bottom : p 142 143 . all(\x : p. bottom <<= x) 144 144 } 145 145 146 146 class instance Flatcpo < Cpo 147 147 { 148 var f : Flatcpo 148 var f : Flatcpo 149 149 150 150 program __<<=[f]__ = eq … … 155 155 type instance __*__ : +Cpo -> +Cpo -> Cpo 156 156 157 var x1,x2 : c; y1, y2 : d 158 159 program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2) 160 161 162 type instance __*__ : +Pcpo -> +Pcpo -> Pcpo 157 var x1,x2 : c; y1, y2 : d 158 159 program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2) 160 161 162 type instance __*__ : +Pcpo -> +Pcpo -> Pcpo 163 163 164 164 type Unit : Pcpo 165 165 166 166 %% Pcont 167 type instance __-->?__ : -Cpo -> +Cpo -> Pcpo 167 type instance __-->?__ : -Cpo -> +Cpo -> Pcpo 168 168 169 169 type __-->?__ < __->?__ 170 . __ in c -->? d = \f : c ->? d . 170 . __ in c -->? d = \f : c ->? d . 171 171 all(\(x,y: c). (def (f x) und x <<= y) impl def (f y)) und 172 all(\s: nat -> c. (isChain(s) und def f(sup(s))) impl 173 ex(\m:nat. def f(s(m)) und 172 all(\s: nat -> c. (isChain(s) und def f(sup(s))) impl 173 ex(\m:nat. def f(s(m)) und 174 174 eq(sup(\n:nat.!f(s(n+m))), f(sup(s))))) 175 175 … … 179 179 type instance __-->__ : -Cpo -> +Cpo -> Cpo 180 180 181 type __-->__ < __-->?__ 181 type __-->__ < __-->?__ 182 182 . __ in c --> d = \f : c -->? d . all(\x:c. def f(x)) 183 183 184 184 var f, g : c --> d 185 185 186 program f <<= g = f <<=[c -->? d] g 186 program f <<= g = f <<=[c -->? d] g 187 187 188 188 type instance __-->__ : -Cpo -> +Pcpo -> Pcpo … … 195 195 var f : p --> p; x : p 196 196 . f(Y(f)) = Y(f) 197 . f(x) = x => Y(f) <<= x 197 . f(x) = x => Y(f) <<= x 198 198 199 199 op undefined : c --> p = Y((\x': c --> p . x') as (c --> p) --> c --> p)
