Changeset 11856
- Timestamp:
- 30.06.2009 17:12:48 (9 months ago)
- Location:
- trunk/HasCASL
- Files:
-
- 7 modified
-
TypeCheck.hs (modified) (1 diff)
-
test/BasicSpec.hascasl.output (modified) (3 diffs)
-
test/Classical.hascasl.output (modified) (3 diffs)
-
test/Coproducts.hascasl.output (modified) (1 diff)
-
test/FunctorMonadTransformer.hascasl.output (modified) (14 diffs)
-
test/Prelude.hascasl.output (modified) (13 diffs)
-
test/StateMonad.hascasl.output (modified) (2 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/HasCASL/TypeCheck.hs
r11855 r11856 403 403 (s, cs, typ, QuantifiedTerm quant decls tr ps)) rs 404 404 LambdaTerm pats part resTrm ps -> do 405 pvs <- mapM freshTypeVar pats 406 rty <- freshTypeVar resTrm 407 let myty = getFunType rty part pvs 408 ls <- checkList True (map Just pvs) pats 409 rs <- mapM ( \ ( s, cs, _, nps) -> do 405 ls <- checkList True (map (const Nothing) pats) pats 406 rs <- mapM ( \ ( s, cs, pats, nps) -> do 410 407 mapM_ (addLocalVar True) $ concatMap extractVars nps 411 es <- fmap (addSuperType $ subst s rty) 412 $ infer False resTrm 408 es <- infer False resTrm 413 409 putLocalVars vs 414 return $ map ( \ (s2, cr, _, rtm) ->410 return $ map ( \ (s2, cr, rty, rtm) -> 415 411 let s3 = compSubst s s2 416 typ = subst s3 myty in 417 (s3, joinC (substC s2 cs) cr, typ, 412 typ = getFunType (subst s rty) 413 part $ map (subst s2) pats 414 in 415 (s3, joinC (substC s2 cs) $ substC s cr 416 , typ, 418 417 TypedTerm 419 418 (LambdaTerm nps part rtm ps) -
trunk/HasCASL/test/BasicSpec.hascasl.output
r11855 r11856 171 171 ### Hint 30.40, no type found for 't1' 172 172 ### Hint 30.40, no type found for 't1' 173 ### Hint 30.40, untypeable term (with type: ? _v 61) 't1'173 ### Hint 30.40, untypeable term (with type: ? _v59) 't1' 174 174 ### Hint 30.40-30.52, 175 untypeable term (with type: ? _v5 5 * ? _v57_b) '(t1 (), t2 ())'175 untypeable term (with type: ? _v53 * ? _v55_b) '(t1 (), t2 ())' 176 176 *** Error 30.38, 177 177 no typing for … … 180 180 *** Error 34.12, unexpected mixfix token: or 181 181 ### Hint 37.27, no type found for 'all' 182 ### Hint 37.27, untypeable term (with type: _v 71 ->? _v72) 'all'182 ### Hint 37.27, untypeable term (with type: _v69 ->? _v70) 'all' 183 183 *** Error 37.25, 184 184 no typing for … … 186 186 = all \ r : ? Unit . (all \ x : s . p x impl r) impl r' 187 187 ### Hint 40.20, no type found for 'all' 188 ### Hint 40.20, untypeable term (with type: _v7 9 ->? _v80) 'all'188 ### Hint 40.20, untypeable term (with type: _v77 ->? _v78) 'all' 189 189 ### Hint 40.3, rebound variable 'ff' 190 190 ### Hint 40.20, no type found for 'all' 191 ### Hint 40.20, untypeable term (with type: _v 81 ->? _v82) 'all'191 ### Hint 40.20, untypeable term (with type: _v79 ->? _v80) 'all' 192 192 *** Error 40.18, 193 193 no typing for 'program ff () : ? Unit = all \ r : ? Unit . r ()' -
trunk/HasCASL/test/Classical.hascasl.output
r11855 r11856 21 21 . p \/ not p; %implied 22 22 var 23 t : Type %(var_ 92)%23 t : Type %(var_88)% 24 24 op choose : forall t : Type . Pred t ->? t %(op)% 25 25 op epsilon : forall t : Type . Pred t -> t %(op)% … … 63 63 in type of '(var a : Logical)' 64 64 typename 'Unit' 65 is not unifiable with type 'Unit ->? _v1 24' (14.32)65 is not unifiable with type 'Unit ->? _v116' (14.32) 66 66 ### Hint 18.23, not a class 'Logical' 67 67 ### Hint 18.41, 68 68 in type of '(var a : Logical)' 69 69 typename 'Unit' 70 is not unifiable with type 'Unit ->? _v1 62' (18.41)70 is not unifiable with type 'Unit ->? _v154' (18.41) 71 71 ### Hint 18.55, 72 72 in type of '(var a : Logical)' 73 73 typename 'Unit' 74 is not unifiable with type 'Unit ->? _v16 8' (18.55)74 is not unifiable with type 'Unit ->? _v160' (18.55) 75 75 ### Hint 18.63, 76 76 in type of '(var a : Logical)' 77 77 typename 'Unit' 78 is not unifiable with type 'Unit ->? _v16 9' (18.63)78 is not unifiable with type 'Unit ->? _v161' (18.63) 79 79 ### Hint 20.13, not a class 't' 80 80 ### Hint 20.36, not a class 'Logical' … … 83 83 in type of '(var a : Logical)' 84 84 typename 'Unit' 85 is not unifiable with type 'Unit ->? _v1 90' (21.30)85 is not unifiable with type 'Unit ->? _v182' (21.30) 86 86 ### Hint 21.38, 87 87 in type of '(var a : Logical)' 88 88 typename 'Unit' 89 is not unifiable with type 'Unit ->? _v1 91' (21.38)89 is not unifiable with type 'Unit ->? _v183' (21.38) 90 90 ### Hint 23.7, not a class 't' 91 91 ### Hint 23.10, not a class 't' -
trunk/HasCASL/test/Coproducts.hascasl.output
r11855 r11856 102 102 (op inl : forall a : Type; b : Type . a -> Sum a b) ())' 103 103 typename 'Unit' (19.23) 104 is not unifiable with type 'Sum Unit _v2 66_b' (19.18)104 is not unifiable with type 'Sum Unit _v250_b' (19.18) 105 105 ### Hint 24.8-24.21, 106 106 in type of '((op False : Bool), 107 107 (op inr : forall a : Type; b : Type . b -> Sum a b) ())' 108 108 typename 'Unit' (19.23) 109 is not unifiable with type 'Sum _v2 88_a Unit' (19.18)109 is not unifiable with type 'Sum _v272_a Unit' (19.18) -
trunk/HasCASL/test/FunctorMonadTransformer.hascasl.output
r11855 r11856 46 46 ST := \ state : Type . \ a : Type . state ->? a * state 47 47 vars 48 a : Type %(var_ 955)%;49 b : Type %(var_9 56)%;50 c : Type %(var_1 10)%;48 a : Type %(var_899)%; 49 b : Type %(var_900)%; 50 c : Type %(var_106)%; 51 51 f : Functor %(var_1)%; 52 m : Monad %(var_6 87)%;53 state : Type %(var_ 953)%;54 t : MonadT %(var_6 86)%52 m : Monad %(var_651)%; 53 state : Type %(var_897)%; 54 t : MonadT %(var_650)% 55 55 op __>>=__ : forall m : Monad; a : Type; b : Type 56 56 . m a * (a -> m b) -> m b … … 146 146 (var q : a ->? m b))' 147 147 ### Hint 14.14-14.24, 148 untypeable term (with type: _v14 6_v133_m _v134_a * (_v134_a -> _v146_v133_m _v135_b))148 untypeable term (with type: _v142_v129_m _v130_a * (_v130_a -> _v142_v129_m _v131_b)) 149 149 '(ret x, q)' 150 150 ### Hint 15.12, rebound variable 'x' … … 154 154 (var r : b ->? m c))' 155 155 ### Hint 15.19-15.33, 156 untypeable term (with type: _v2 24_v211_m _v212_a * (_v212_a -> _v224_v211_m _v213_b))156 untypeable term (with type: _v218_v205_m _v206_a * (_v206_a -> _v218_v205_m _v207_b)) 157 157 '(ret (f x), r)' 158 158 ### Hint 15.3-15.33, … … 165 165 (var r : b ->? m c)))' 166 166 ### Hint 15.3-15.26, 167 untypeable term (with type: _v19 6_v183_m _v184_a * (_v184_a -> _v196_v183_m _v185_b))167 untypeable term (with type: _v192_v179_m _v180_a * (_v180_a -> _v192_v179_m _v181_b)) 168 168 '(p, \ x : a . ret (f x) >>= r)' 169 169 ### Hint 15.12, rebound variable 'x' … … 173 173 (var r : b ->? m c))' 174 174 ### Hint 15.19-15.33, 175 untypeable term (with type: _v2 70_v257_m _v258_a * (_v258_a -> _v270_v257_m _v259_b))175 untypeable term (with type: _v260_v247_m _v248_a * (_v248_a -> _v260_v247_m _v249_b)) 176 176 '(ret (f x), r)' 177 177 ### Hint 16.13, rebound variable 'x' … … 180 180 \ x : a . (var r : b ->? m c) ((var f : a ->? b) (var x : a)))' 181 181 ### Hint 16.5-16.25, 182 untypeable term (with type: _v3 14_v301_m _v302_a * (_v302_a -> _v314_v301_m _v303_b))182 untypeable term (with type: _v302_v289_m _v290_a * (_v290_a -> _v302_v289_m _v291_b)) 183 183 '(p, \ x : a . r (f x))' 184 184 ### Hint 16.13, rebound variable 'x' … … 186 186 rejected '__->?__ < __->__' of '((var p : m a), (var q : a ->? m b))' 187 187 ### Hint 18.4-18.10, 188 untypeable term (with type: _v4 34_v421_m _v422_a * (_v422_a -> _v434_v421_m _v423_b))188 untypeable term (with type: _v414_v401_m _v402_a * (_v402_a -> _v414_v401_m _v403_b)) 189 189 '(p, q)' 190 190 ### Hint 18.3-18.17, … … 194 194 (var r : b ->? m c))' 195 195 ### Hint 18.3-18.17, 196 untypeable term (with type: _v 408_v395_m _v396_a * (_v396_a -> _v408_v395_m _v397_b))196 untypeable term (with type: _v388_v375_m _v376_a * (_v376_a -> _v388_v375_m _v377_b)) 197 197 '(p >>= q, r)' 198 198 ### Hint 18.4-18.10, 199 199 rejected '__->?__ < __->__' of '((var p : m a), (var q : a ->? m b))' 200 200 ### Hint 18.4-18.10, 201 untypeable term (with type: _v4 60_v447_m _v448_a * (_v448_a -> _v460_v447_m _v449_b))201 untypeable term (with type: _v440_v427_m _v428_a * (_v428_a -> _v440_v427_m _v429_b)) 202 202 '(p, q)' 203 203 ### Hint 18.29, rebound variable 'x' … … 205 205 rejected '__->?__ < __->__' of '((var q : a ->? m b) (var x : a), (var r : b ->? m c))' 206 206 ### Hint 18.36-18.44, 207 untypeable term (with type: _v 514_v501_m _v502_a * (_v502_a -> _v514_v501_m _v503_b))207 untypeable term (with type: _v492_v479_m _v480_a * (_v480_a -> _v492_v479_m _v481_b)) 208 208 '(q x, r)' 209 209 ### Hint 18.21-18.44, … … 214 214 ((var q : a ->? m b) (var x : a), (var r : b ->? m c)))' 215 215 ### Hint 18.21-18.36, 216 untypeable term (with type: _v4 86_v473_m _v474_a * (_v474_a -> _v486_v473_m _v475_b))216 untypeable term (with type: _v466_v453_m _v454_a * (_v454_a -> _v466_v453_m _v455_b)) 217 217 '(p, \ x : a . q x >>= r)' 218 218 ### Hint 18.29, rebound variable 'x' … … 220 220 rejected '__->?__ < __->__' of '((var q : a ->? m b) (var x : a), (var r : b ->? m c))' 221 221 ### Hint 18.36-18.44, 222 untypeable term (with type: _v5 52_v539_m _v540_a * (_v540_a -> _v552_v539_m _v541_b))222 untypeable term (with type: _v526_v513_m _v514_a * (_v514_a -> _v526_v513_m _v515_b)) 223 223 '(q x, r)' 224 224 ### Warning 20.16, refined class 'Monad' … … 242 242 ((var f : a -> b) (var y : a)))' 243 243 ### Hint 22.13-22.35, 244 untypeable term (with type: _v6 49_v636_m _v637_a * (_v637_a -> _v649_v636_m _v638_b))244 untypeable term (with type: _v621_v608_m _v609_a * (_v609_a -> _v621_v608_m _v610_b)) 245 245 '(x, \ y : a . ret (f y))' 246 246 ### Hint 22.21, rebound variable 'y' … … 296 296 is not unifiable with type 'a * state' (35.25) 297 297 ### Hint 37.3-37.9, 298 untypeable term (with type: _v 1006_v993_m _v994_a * (_v994_a -> _v1006_v993_m _v995_b))298 untypeable term (with type: _v945_v932_m _v933_a * (_v933_a -> _v945_v932_m _v934_b)) 299 299 '(p, q)' 300 300 ### Hint 37.3-37.9, … … 303 303 is not unifiable with type 'a * state' (35.25) 304 304 ### Hint 37.3-37.9, 305 untypeable term (with type: _v 1015_v996_m _v997_a * (_v997_a ->? _v1015_v996_m _v998_b))305 untypeable term (with type: _v954_v935_m _v936_a * (_v936_a ->? _v954_v935_m _v937_b)) 306 306 '(p, q)' 307 307 ### Hint 37.5-37.54, 308 untypeable term (with type: ? _v9 87_a * ? _v987_a)308 untypeable term (with type: ? _v926_a * ? _v926_a) 309 309 '(p >>= q, \ s1 : state . let (z, s2) = p s1 in q z s2)' 310 310 *** Error 37.5, -
trunk/HasCASL/test/Prelude.hascasl.output
r11855 r11856 132 132 s : Type 133 133 vars 134 c : Cpo %(var_ 515)%;135 d : Cpo %(var_ 516)%;136 f : Flatcpo %(var_ 513)%;137 p : Pcpo %(var_ 510)%;134 c : Cpo %(var_457)%; 135 d : Cpo %(var_458)%; 136 f : Flatcpo %(var_455)%; 137 p : Pcpo %(var_452)%; 138 138 t : Type %(var_2)% 139 139 op Y : forall p : Pcpo . (p --> p) --> p %(fun)% … … 263 263 in term '(op fst : forall s : Type; t : Type . s * t -> s) = __res__' 264 264 are uninstantiated type variables 265 '[_v 87_v79_t, _v88_v78_s]'265 '[_v63_v55_t, _v64_v54_s]' 266 266 ### Hint 72.11, 267 267 no kind found for 's' … … 292 292 ### Hint 90.45, no type found for 't1' 293 293 ### Hint 90.45, no type found for 't1' 294 ### Hint 90.45, untypeable term (with type: ? _v 419) 't1'294 ### Hint 90.45, untypeable term (with type: ? _v361) 't1' 295 295 ### Hint 90.45-90.47, 296 untypeable term (with type: _v 417 ->? _v418) 't1 ()'296 untypeable term (with type: _v359 ->? _v360) 't1 ()' 297 297 ### Hint 90.45-90.50, 298 untypeable term (with type: _v 415 ->? _v416) 't1 () und'298 untypeable term (with type: _v357 ->? _v358) 't1 () und' 299 299 ### Hint 90.45, no type found for 't1' 300 300 ### Hint 90.45, no type found for 't1' 301 ### Hint 90.45, untypeable term (with type: ? _v 424) 't1'301 ### Hint 90.45, untypeable term (with type: ? _v366) 't1' 302 302 ### Hint 90.45-90.47, 303 untypeable term (with type: _v 422 ->? _v423) 't1 ()'303 untypeable term (with type: _v364 ->? _v365) 't1 ()' 304 304 ### Hint 90.45-90.50, 305 untypeable term (with type: _v 420 ->? _v421) 't1 () und'305 untypeable term (with type: _v362 ->? _v363) 't1 () und' 306 306 ### Hint 90.45-90.54, 307 untypeable term (with type: ? _v 414) 't1 () und t2'307 untypeable term (with type: ? _v356) 't1 () und t2' 308 308 *** Error 90.43, 309 309 no typing for … … 312 312 *** Error 95.11, unexpected mixfix token: or 313 313 ### Hint 98.39, no type found for 'all' 314 ### Hint 98.39, untypeable term (with type: _v 443 ->? _v444) 'all'314 ### Hint 98.39, untypeable term (with type: _v385 ->? _v386) 'all' 315 315 *** Error 98.37, 316 316 no typing for … … 318 318 = all \ r : Pred Unit . (all \ x : s . p x impl r) impl r' 319 319 ### Hint 101.29, no type found for 'all' 320 ### Hint 101.29, untypeable term (with type: _v 457 ->? _v458) 'all'320 ### Hint 101.29, untypeable term (with type: _v399 ->? _v400) 'all' 321 321 ### Hint 101.9, rebound variable 'ff' 322 322 ### Hint 101.29, no type found for 'all' 323 ### Hint 101.29, untypeable term (with type: _v4 59 ->? _v460) 'all'323 ### Hint 101.29, untypeable term (with type: _v401 ->? _v402) 'all' 324 324 *** Error 101.27, 325 325 no typing for … … 328 328 ### Hint 103.44, untypeable term (with type: Unit) 'impl' 329 329 ### Hint 103.42-103.44, 330 untypeable term (with type: _v4 77 ->? _v478) 'r impl'330 untypeable term (with type: _v419 ->? _v420) 'r impl' 331 331 *** Error 103.40, 332 332 no typing for 'program neg (r : Pred Unit) : Pred Unit = r impl ff' 333 333 ### Hint 108.3, no type found for 'all' 334 ### Hint 108.3, untypeable term (with type: _v4 83 ->? _v484) 'all'334 ### Hint 108.3, untypeable term (with type: _v425 ->? _v426) 'all' 335 335 *** Error 108.3-108.63, 336 336 no typing for … … 345 345 found: {Cpo} 346 346 ### Hint 121.3, no type found for 'all' 347 ### Hint 121.3, untypeable term (with type: _v4 86 ->? _v487) 'all'347 ### Hint 121.3, untypeable term (with type: _v428 ->? _v429) 'all' 348 348 *** Error 121.3-121.16, no typing for 'all \ x : c . x <<= x' 349 349 ### Hint 122.3, no type found for 'all' 350 ### Hint 122.3, untypeable term (with type: _v4 90 ->? _v491) 'all'350 ### Hint 122.3, untypeable term (with type: _v432 ->? _v433) 'all' 351 351 *** Error 122.3-122.44, 352 352 no typing for 353 353 'all \ (x, y, z : c) . (x <<= y) und (y <<= z) impl x <<= z' 354 354 ### Hint 123.3, no type found for 'all' 355 ### Hint 123.3, untypeable term (with type: _v4 94 ->? _v495) 'all'355 ### Hint 123.3, untypeable term (with type: _v436 ->? _v437) 'all' 356 356 *** Error 123.3-123.57, 357 357 no typing for 358 358 'all \ (x, y, z : c) . (x <<= y) und (y <<= x) impl eq (x, y)' 359 359 ### Hint 125.32, no type found for 'all' 360 ### Hint 125.32, untypeable term (with type: _v4 98 ->? _v499) 'all'360 ### Hint 125.32, untypeable term (with type: _v440 ->? _v441) 'all' 361 361 *** Error 125.14-125.46, 362 362 no typing for '(all \ n : nat . s n <<= s (Suc n)) as Unit' 363 363 ### Hint 126.15, rebound variable 'x' 364 364 ### Hint 126.38, no type found for 'all' 365 ### Hint 126.38, untypeable term (with type: _v 502 ->? _v503) 'all'365 ### Hint 126.38, untypeable term (with type: _v444 ->? _v445) 'all' 366 366 *** Error 126.14-126.52, 367 367 no typing for '(all \ n : nat . s n <<= x) as Unit' … … 375 375 (\ x : c . ((((isBound (x, s)) impl) sup) s) <<= x)) 376 376 ### Hint 130.3, no type found for 'all' 377 ### Hint 130.3, untypeable term (with type: _v 505 ->? _v506) 'all'377 ### Hint 130.3, untypeable term (with type: _v447 ->? _v448) 'all' 378 378 *** Error 130.3-131.74, 379 379 no typing for … … 384 384 (\ x : c . isBound (x, s) impl sup (s) <<= x))' 385 385 ### Hint 134.3, no type found for 'all' 386 ### Hint 134.3, untypeable term (with type: _v 508 ->? _v509) 'all'386 ### Hint 134.3, untypeable term (with type: _v450 ->? _v451) 'all' 387 387 *** Error 134.3-134.46, 388 388 no typing for 'all \ s : nat -> c . isChain s impl def (sup s)' … … 391 391 ignoring declaration for builtin identifier 'bottom' 392 392 ### Hint 143.3, no type found for 'all' 393 ### Hint 143.3, untypeable term (with type: _v 511 ->? _v512) 'all'393 ### Hint 143.3, untypeable term (with type: _v453 ->? _v454) 'all' 394 394 *** Error 143.3-143.22, no typing for 'all \ x : p . bottom <<= x' 395 395 ### Hint 148.6, is type variable 'f' … … 413 413 ((var x1 : c), (var x2 : c))' 414 414 typename 'Unit' (119.14) 415 is not unifiable with type '_v 528 ->? _v529' (159.45)415 is not unifiable with type '_v470 ->? _v471' (159.45) 416 416 ### Hint 159.37, 417 untypeable term (with type: _v 528 ->? _v529) 'x1 <<= x2'417 untypeable term (with type: _v470 ->? _v471) 'x1 <<= x2' 418 418 ### Hint 159.33-159.45, 419 untypeable term (with type: _v 526 ->? _v527) '(x1 <<= x2) und'419 untypeable term (with type: _v468 ->? _v469) '(x1 <<= x2) und' 420 420 *** Error 159.31, 421 421 no typing for … … 442 442 ### Warning 176.11, variable also known as type variable 'f' 443 443 ### Hint 176.31, no type found for 'all' 444 ### Hint 176.31, untypeable term (with type: _v5 58 ->? _v559) 'all'444 ### Hint 176.31, untypeable term (with type: _v500 ->? _v501) 'all' 445 445 *** Error 176.29, 446 446 no typing for … … 489 489 found: {Pcpo} 490 490 ### Hint 192.3, no type found for 'all' 491 ### Hint 192.3, untypeable term (with type: _v5 79 ->? _v580) 'all'491 ### Hint 192.3, untypeable term (with type: _v521 ->? _v522) 'all' 492 492 *** Error 192.3-193.47, 493 493 no typing for -
trunk/HasCASL/test/StateMonad.hascasl.output
r11855 r11856 14 14 vars 15 15 a : Type %(var_2)%; 16 b : Type %(var_ 43)%;16 b : Type %(var_38)%; 17 17 m : Type -> Type %(var_1)%; 18 18 state : Type %(var_3)% … … 56 56 is not unifiable with type 'a * state' (10.18) 57 57 ### Hint 13.3-13.9, 58 untypeable term (with type: _v 64_v54_m _v55_a * (_v55_a -> _v64_v54_m _v56_b))58 untypeable term (with type: _v59_v49_m _v50_a * (_v50_a -> _v59_v49_m _v51_b)) 59 59 '(p, q)' 60 60 ### Hint 13.5-13.54, 61 untypeable term (with type: ? _v4 8_a * ? _v48_a)61 untypeable term (with type: ? _v43_a * ? _v43_a) 62 62 '(p >>= q, \ s2 : state . let (z, s2) = p s1 in q z s2)' 63 63 *** Error 13.5,
