Treat out-of-scope variables as holes
[ghc.git] / compiler / typecheck / TcTypeNats.hs
1 module TcTypeNats
2 ( typeNatTyCons
3 , typeNatCoAxiomRules
4 , BuiltInSynFamily(..)
5
6 , typeNatAddTyCon
7 , typeNatMulTyCon
8 , typeNatExpTyCon
9 , typeNatLeqTyCon
10 , typeNatSubTyCon
11 , typeNatCmpTyCon
12 , typeSymbolCmpTyCon
13 ) where
14
15 import Type
16 import Pair
17 import TcType ( TcType, tcEqType )
18 import TyCon ( TyCon, FamTyConFlav(..), mkFamilyTyCon, TyConParent(..) )
19 import Coercion ( Role(..) )
20 import TcRnTypes ( Xi )
21 import CoAxiom ( CoAxiomRule(..), BuiltInSynFamily(..) )
22 import Name ( Name, BuiltInSyntax(..) )
23 import TysWiredIn ( typeNatKind, typeSymbolKind
24 , mkWiredInTyConName
25 , promotedBoolTyCon
26 , promotedFalseDataCon, promotedTrueDataCon
27 , promotedOrderingTyCon
28 , promotedLTDataCon
29 , promotedEQDataCon
30 , promotedGTDataCon
31 )
32 import TysPrim ( tyVarList, mkArrowKinds )
33 import PrelNames ( gHC_TYPELITS
34 , typeNatAddTyFamNameKey
35 , typeNatMulTyFamNameKey
36 , typeNatExpTyFamNameKey
37 , typeNatLeqTyFamNameKey
38 , typeNatSubTyFamNameKey
39 , typeNatCmpTyFamNameKey
40 , typeSymbolCmpTyFamNameKey
41 )
42 import FastString ( FastString, fsLit )
43 import qualified Data.Map as Map
44 import Data.Maybe ( isJust )
45
46 {-------------------------------------------------------------------------------
47 Built-in type constructors for functions on type-lelve nats
48 -}
49
50 typeNatTyCons :: [TyCon]
51 typeNatTyCons =
52 [ typeNatAddTyCon
53 , typeNatMulTyCon
54 , typeNatExpTyCon
55 , typeNatLeqTyCon
56 , typeNatSubTyCon
57 , typeNatCmpTyCon
58 , typeSymbolCmpTyCon
59 ]
60
61 typeNatAddTyCon :: TyCon
62 typeNatAddTyCon = mkTypeNatFunTyCon2 name
63 BuiltInSynFamily
64 { sfMatchFam = matchFamAdd
65 , sfInteractTop = interactTopAdd
66 , sfInteractInert = interactInertAdd
67 }
68 where
69 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+")
70 typeNatAddTyFamNameKey typeNatAddTyCon
71
72 typeNatSubTyCon :: TyCon
73 typeNatSubTyCon = mkTypeNatFunTyCon2 name
74 BuiltInSynFamily
75 { sfMatchFam = matchFamSub
76 , sfInteractTop = interactTopSub
77 , sfInteractInert = interactInertSub
78 }
79 where
80 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "-")
81 typeNatSubTyFamNameKey typeNatSubTyCon
82
83 typeNatMulTyCon :: TyCon
84 typeNatMulTyCon = mkTypeNatFunTyCon2 name
85 BuiltInSynFamily
86 { sfMatchFam = matchFamMul
87 , sfInteractTop = interactTopMul
88 , sfInteractInert = interactInertMul
89 }
90 where
91 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "*")
92 typeNatMulTyFamNameKey typeNatMulTyCon
93
94 typeNatExpTyCon :: TyCon
95 typeNatExpTyCon = mkTypeNatFunTyCon2 name
96 BuiltInSynFamily
97 { sfMatchFam = matchFamExp
98 , sfInteractTop = interactTopExp
99 , sfInteractInert = interactInertExp
100 }
101 where
102 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^")
103 typeNatExpTyFamNameKey typeNatExpTyCon
104
105 typeNatLeqTyCon :: TyCon
106 typeNatLeqTyCon =
107 mkFamilyTyCon name
108 (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind)
109 (take 2 $ tyVarList typeNatKind)
110 (BuiltInSynFamTyCon ops)
111 NoParentTyCon
112
113 where
114 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?")
115 typeNatLeqTyFamNameKey typeNatLeqTyCon
116 ops = BuiltInSynFamily
117 { sfMatchFam = matchFamLeq
118 , sfInteractTop = interactTopLeq
119 , sfInteractInert = interactInertLeq
120 }
121
122 typeNatCmpTyCon :: TyCon
123 typeNatCmpTyCon =
124 mkFamilyTyCon name
125 (mkArrowKinds [ typeNatKind, typeNatKind ] orderingKind)
126 (take 2 $ tyVarList typeNatKind)
127 (BuiltInSynFamTyCon ops)
128 NoParentTyCon
129
130 where
131 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpNat")
132 typeNatCmpTyFamNameKey typeNatCmpTyCon
133 ops = BuiltInSynFamily
134 { sfMatchFam = matchFamCmpNat
135 , sfInteractTop = interactTopCmpNat
136 , sfInteractInert = \_ _ _ _ -> []
137 }
138
139 typeSymbolCmpTyCon :: TyCon
140 typeSymbolCmpTyCon =
141 mkFamilyTyCon name
142 (mkArrowKinds [ typeSymbolKind, typeSymbolKind ] orderingKind)
143 (take 2 $ tyVarList typeSymbolKind)
144 (BuiltInSynFamTyCon ops)
145 NoParentTyCon
146
147 where
148 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpSymbol")
149 typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon
150 ops = BuiltInSynFamily
151 { sfMatchFam = matchFamCmpSymbol
152 , sfInteractTop = interactTopCmpSymbol
153 , sfInteractInert = \_ _ _ _ -> []
154 }
155
156
157
158
159
160 -- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
161 mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
162 mkTypeNatFunTyCon2 op tcb =
163 mkFamilyTyCon op
164 (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
165 (take 2 $ tyVarList typeNatKind)
166 (BuiltInSynFamTyCon tcb)
167 NoParentTyCon
168
169
170
171
172 {-------------------------------------------------------------------------------
173 Built-in rules axioms
174 -------------------------------------------------------------------------------}
175
176 -- If you add additional rules, please remember to add them to
177 -- `typeNatCoAxiomRules` also.
178 axAddDef
179 , axMulDef
180 , axExpDef
181 , axLeqDef
182 , axCmpNatDef
183 , axCmpSymbolDef
184 , axAdd0L
185 , axAdd0R
186 , axMul0L
187 , axMul0R
188 , axMul1L
189 , axMul1R
190 , axExp1L
191 , axExp0R
192 , axExp1R
193 , axLeqRefl
194 , axCmpNatRefl
195 , axCmpSymbolRefl
196 , axLeq0L
197 , axSubDef
198 , axSub0R
199 :: CoAxiomRule
200
201 axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
202 \x y -> Just $ num (x + y)
203
204 axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $
205 \x y -> Just $ num (x * y)
206
207 axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
208 \x y -> Just $ num (x ^ y)
209
210 axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
211 \x y -> Just $ bool (x <= y)
212
213 axCmpNatDef = mkBinAxiom "CmpNatDef" typeNatCmpTyCon
214 $ \x y -> Just $ ordering (compare x y)
215
216 axCmpSymbolDef =
217 CoAxiomRule
218 { coaxrName = fsLit "CmpSymbolDef"
219 , coaxrTypeArity = 2
220 , coaxrAsmpRoles = []
221 , coaxrRole = Nominal
222 , coaxrProves = \ts cs ->
223 case (ts,cs) of
224 ([s,t],[]) ->
225 do x <- isStrLitTy s
226 y <- isStrLitTy t
227 return (mkTyConApp typeSymbolCmpTyCon [s,t] ===
228 ordering (compare x y))
229 _ -> Nothing
230 }
231
232 axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon $
233 \x y -> fmap num (minus x y)
234
235 axAdd0L = mkAxiom1 "Add0L" $ \t -> (num 0 .+. t) === t
236 axAdd0R = mkAxiom1 "Add0R" $ \t -> (t .+. num 0) === t
237 axSub0R = mkAxiom1 "Sub0R" $ \t -> (t .-. num 0) === t
238 axMul0L = mkAxiom1 "Mul0L" $ \t -> (num 0 .*. t) === num 0
239 axMul0R = mkAxiom1 "Mul0R" $ \t -> (t .*. num 0) === num 0
240 axMul1L = mkAxiom1 "Mul1L" $ \t -> (num 1 .*. t) === t
241 axMul1R = mkAxiom1 "Mul1R" $ \t -> (t .*. num 1) === t
242 axExp1L = mkAxiom1 "Exp1L" $ \t -> (num 1 .^. t) === num 1
243 axExp0R = mkAxiom1 "Exp0R" $ \t -> (t .^. num 0) === num 1
244 axExp1R = mkAxiom1 "Exp1R" $ \t -> (t .^. num 1) === t
245 axLeqRefl = mkAxiom1 "LeqRefl" $ \t -> (t <== t) === bool True
246 axCmpNatRefl = mkAxiom1 "CmpNatRefl"
247 $ \t -> (cmpNat t t) === ordering EQ
248 axCmpSymbolRefl = mkAxiom1 "CmpSymbolRefl"
249 $ \t -> (cmpSymbol t t) === ordering EQ
250 axLeq0L = mkAxiom1 "Leq0L" $ \t -> (num 0 <== t) === bool True
251
252 typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule
253 typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
254 [ axAddDef
255 , axMulDef
256 , axExpDef
257 , axLeqDef
258 , axCmpNatDef
259 , axCmpSymbolDef
260 , axAdd0L
261 , axAdd0R
262 , axMul0L
263 , axMul0R
264 , axMul1L
265 , axMul1R
266 , axExp1L
267 , axExp0R
268 , axExp1R
269 , axLeqRefl
270 , axCmpNatRefl
271 , axCmpSymbolRefl
272 , axLeq0L
273 , axSubDef
274 ]
275
276
277
278 {-------------------------------------------------------------------------------
279 Various utilities for making axioms and types
280 -------------------------------------------------------------------------------}
281
282 (.+.) :: Type -> Type -> Type
283 s .+. t = mkTyConApp typeNatAddTyCon [s,t]
284
285 (.-.) :: Type -> Type -> Type
286 s .-. t = mkTyConApp typeNatSubTyCon [s,t]
287
288 (.*.) :: Type -> Type -> Type
289 s .*. t = mkTyConApp typeNatMulTyCon [s,t]
290
291 (.^.) :: Type -> Type -> Type
292 s .^. t = mkTyConApp typeNatExpTyCon [s,t]
293
294 (<==) :: Type -> Type -> Type
295 s <== t = mkTyConApp typeNatLeqTyCon [s,t]
296
297 cmpNat :: Type -> Type -> Type
298 cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t]
299
300 cmpSymbol :: Type -> Type -> Type
301 cmpSymbol s t = mkTyConApp typeSymbolCmpTyCon [s,t]
302
303 (===) :: Type -> Type -> Pair Type
304 x === y = Pair x y
305
306 num :: Integer -> Type
307 num = mkNumLitTy
308
309 boolKind :: Kind
310 boolKind = mkTyConApp promotedBoolTyCon []
311
312 bool :: Bool -> Type
313 bool b = if b then mkTyConApp promotedTrueDataCon []
314 else mkTyConApp promotedFalseDataCon []
315
316 isBoolLitTy :: Type -> Maybe Bool
317 isBoolLitTy tc =
318 do (tc,[]) <- splitTyConApp_maybe tc
319 case () of
320 _ | tc == promotedFalseDataCon -> return False
321 | tc == promotedTrueDataCon -> return True
322 | otherwise -> Nothing
323
324 orderingKind :: Kind
325 orderingKind = mkTyConApp promotedOrderingTyCon []
326
327 ordering :: Ordering -> Type
328 ordering o =
329 case o of
330 LT -> mkTyConApp promotedLTDataCon []
331 EQ -> mkTyConApp promotedEQDataCon []
332 GT -> mkTyConApp promotedGTDataCon []
333
334 isOrderingLitTy :: Type -> Maybe Ordering
335 isOrderingLitTy tc =
336 do (tc1,[]) <- splitTyConApp_maybe tc
337 case () of
338 _ | tc1 == promotedLTDataCon -> return LT
339 | tc1 == promotedEQDataCon -> return EQ
340 | tc1 == promotedGTDataCon -> return GT
341 | otherwise -> Nothing
342
343 known :: (Integer -> Bool) -> TcType -> Bool
344 known p x = case isNumLitTy x of
345 Just a -> p a
346 Nothing -> False
347
348
349
350
351 -- For the definitional axioms
352 mkBinAxiom :: String -> TyCon ->
353 (Integer -> Integer -> Maybe Type) -> CoAxiomRule
354 mkBinAxiom str tc f =
355 CoAxiomRule
356 { coaxrName = fsLit str
357 , coaxrTypeArity = 2
358 , coaxrAsmpRoles = []
359 , coaxrRole = Nominal
360 , coaxrProves = \ts cs ->
361 case (ts,cs) of
362 ([s,t],[]) -> do x <- isNumLitTy s
363 y <- isNumLitTy t
364 z <- f x y
365 return (mkTyConApp tc [s,t] === z)
366 _ -> Nothing
367 }
368
369
370
371 mkAxiom1 :: String -> (Type -> Pair Type) -> CoAxiomRule
372 mkAxiom1 str f =
373 CoAxiomRule
374 { coaxrName = fsLit str
375 , coaxrTypeArity = 1
376 , coaxrAsmpRoles = []
377 , coaxrRole = Nominal
378 , coaxrProves = \ts cs ->
379 case (ts,cs) of
380 ([s],[]) -> return (f s)
381 _ -> Nothing
382 }
383
384
385 {-------------------------------------------------------------------------------
386 Evaluation
387 -------------------------------------------------------------------------------}
388
389 matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
390 matchFamAdd [s,t]
391 | Just 0 <- mbX = Just (axAdd0L, [t], t)
392 | Just 0 <- mbY = Just (axAdd0R, [s], s)
393 | Just x <- mbX, Just y <- mbY =
394 Just (axAddDef, [s,t], num (x + y))
395 where mbX = isNumLitTy s
396 mbY = isNumLitTy t
397 matchFamAdd _ = Nothing
398
399 matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
400 matchFamSub [s,t]
401 | Just 0 <- mbY = Just (axSub0R, [s], s)
402 | Just x <- mbX, Just y <- mbY, Just z <- minus x y =
403 Just (axSubDef, [s,t], num z)
404 where mbX = isNumLitTy s
405 mbY = isNumLitTy t
406 matchFamSub _ = Nothing
407
408 matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
409 matchFamMul [s,t]
410 | Just 0 <- mbX = Just (axMul0L, [t], num 0)
411 | Just 0 <- mbY = Just (axMul0R, [s], num 0)
412 | Just 1 <- mbX = Just (axMul1L, [t], t)
413 | Just 1 <- mbY = Just (axMul1R, [s], s)
414 | Just x <- mbX, Just y <- mbY =
415 Just (axMulDef, [s,t], num (x * y))
416 where mbX = isNumLitTy s
417 mbY = isNumLitTy t
418 matchFamMul _ = Nothing
419
420 matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
421 matchFamExp [s,t]
422 | Just 0 <- mbY = Just (axExp0R, [s], num 1)
423 | Just 1 <- mbX = Just (axExp1L, [t], num 1)
424 | Just 1 <- mbY = Just (axExp1R, [s], s)
425 | Just x <- mbX, Just y <- mbY =
426 Just (axExpDef, [s,t], num (x ^ y))
427 where mbX = isNumLitTy s
428 mbY = isNumLitTy t
429 matchFamExp _ = Nothing
430
431 matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
432 matchFamLeq [s,t]
433 | Just 0 <- mbX = Just (axLeq0L, [t], bool True)
434 | Just x <- mbX, Just y <- mbY =
435 Just (axLeqDef, [s,t], bool (x <= y))
436 | tcEqType s t = Just (axLeqRefl, [s], bool True)
437 where mbX = isNumLitTy s
438 mbY = isNumLitTy t
439 matchFamLeq _ = Nothing
440
441 matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
442 matchFamCmpNat [s,t]
443 | Just x <- mbX, Just y <- mbY =
444 Just (axCmpNatDef, [s,t], ordering (compare x y))
445 | tcEqType s t = Just (axCmpNatRefl, [s], ordering EQ)
446 where mbX = isNumLitTy s
447 mbY = isNumLitTy t
448 matchFamCmpNat _ = Nothing
449
450 matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
451 matchFamCmpSymbol [s,t]
452 | Just x <- mbX, Just y <- mbY =
453 Just (axCmpSymbolDef, [s,t], ordering (compare x y))
454 | tcEqType s t = Just (axCmpSymbolRefl, [s], ordering EQ)
455 where mbX = isStrLitTy s
456 mbY = isStrLitTy t
457 matchFamCmpSymbol _ = Nothing
458
459
460 {-------------------------------------------------------------------------------
461 Interact with axioms
462 -------------------------------------------------------------------------------}
463
464 interactTopAdd :: [Xi] -> Xi -> [Pair Type]
465 interactTopAdd [s,t] r
466 | Just 0 <- mbZ = [ s === num 0, t === num 0 ] -- (s + t ~ 0) => (s ~ 0, t ~ 0)
467 | Just x <- mbX, Just z <- mbZ, Just y <- minus z x = [t === num y] -- (5 + t ~ 8) => (t ~ 3)
468 | Just y <- mbY, Just z <- mbZ, Just x <- minus z y = [s === num x] -- (s + 5 ~ 8) => (s ~ 3)
469 where
470 mbX = isNumLitTy s
471 mbY = isNumLitTy t
472 mbZ = isNumLitTy r
473 interactTopAdd _ _ = []
474
475 {-
476 Note [Weakened interaction rule for subtraction]
477 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
478
479 A simpler interaction here might be:
480
481 `s - t ~ r` --> `t + r ~ s`
482
483 This would enable us to reuse all the code for addition.
484 Unfortunately, this works a little too well at the moment.
485 Consider the following example:
486
487 0 - 5 ~ r --> 5 + r ~ 0 --> (5 = 0, r = 0)
488
489 This (correctly) spots that the constraint cannot be solved.
490
491 However, this may be a problem if the constraint did not
492 need to be solved in the first place! Consider the following example:
493
494 f :: Proxy (If (5 <=? 0) (0 - 5) (5 - 0)) -> Proxy 5
495 f = id
496
497 Currently, GHC is strict while evaluating functions, so this does not
498 work, because even though the `If` should evaluate to `5 - 0`, we
499 also evaluate the "then" branch which generates the constraint `0 - 5 ~ r`,
500 which fails.
501
502 So, for the time being, we only add an improvement when the RHS is a constant,
503 which happens to work OK for the moment, although clearly we need to do
504 something more general.
505 -}
506 interactTopSub :: [Xi] -> Xi -> [Pair Type]
507 interactTopSub [s,t] r
508 | Just z <- mbZ = [ s === (num z .+. t) ] -- (s - t ~ 5) => (5 + t ~ s)
509 where
510 mbZ = isNumLitTy r
511 interactTopSub _ _ = []
512
513
514
515
516
517 interactTopMul :: [Xi] -> Xi -> [Pair Type]
518 interactTopMul [s,t] r
519 | Just 1 <- mbZ = [ s === num 1, t === num 1 ] -- (s * t ~ 1) => (s ~ 1, t ~ 1)
520 | Just x <- mbX, Just z <- mbZ, Just y <- divide z x = [t === num y] -- (3 * t ~ 15) => (t ~ 5)
521 | Just y <- mbY, Just z <- mbZ, Just x <- divide z y = [s === num x] -- (s * 3 ~ 15) => (s ~ 5)
522 where
523 mbX = isNumLitTy s
524 mbY = isNumLitTy t
525 mbZ = isNumLitTy r
526 interactTopMul _ _ = []
527
528 interactTopExp :: [Xi] -> Xi -> [Pair Type]
529 interactTopExp [s,t] r
530 | Just 0 <- mbZ = [ s === num 0 ] -- (s ^ t ~ 0) => (s ~ 0)
531 | Just x <- mbX, Just z <- mbZ, Just y <- logExact z x = [t === num y] -- (2 ^ t ~ 8) => (t ~ 3)
532 | Just y <- mbY, Just z <- mbZ, Just x <- rootExact z y = [s === num x] -- (s ^ 2 ~ 9) => (s ~ 3)
533 where
534 mbX = isNumLitTy s
535 mbY = isNumLitTy t
536 mbZ = isNumLitTy r
537 interactTopExp _ _ = []
538
539 interactTopLeq :: [Xi] -> Xi -> [Pair Type]
540 interactTopLeq [s,t] r
541 | Just 0 <- mbY, Just True <- mbZ = [ s === num 0 ] -- (s <= 0) => (s ~ 0)
542 where
543 mbY = isNumLitTy t
544 mbZ = isBoolLitTy r
545 interactTopLeq _ _ = []
546
547 interactTopCmpNat :: [Xi] -> Xi -> [Pair Type]
548 interactTopCmpNat [s,t] r
549 | Just EQ <- isOrderingLitTy r = [ s === t ]
550 interactTopCmpNat _ _ = []
551
552 interactTopCmpSymbol :: [Xi] -> Xi -> [Pair Type]
553 interactTopCmpSymbol [s,t] r
554 | Just EQ <- isOrderingLitTy r = [ s === t ]
555 interactTopCmpSymbol _ _ = []
556
557
558
559
560 {-------------------------------------------------------------------------------
561 Interaction with inerts
562 -------------------------------------------------------------------------------}
563
564 interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
565 interactInertAdd [x1,y1] z1 [x2,y2] z2
566 | sameZ && tcEqType x1 x2 = [ y1 === y2 ]
567 | sameZ && tcEqType y1 y2 = [ x1 === x2 ]
568 where sameZ = tcEqType z1 z2
569 interactInertAdd _ _ _ _ = []
570
571 interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
572 interactInertSub [x1,y1] z1 [x2,y2] z2
573 | sameZ && tcEqType x1 x2 = [ y1 === y2 ]
574 | sameZ && tcEqType y1 y2 = [ x1 === x2 ]
575 where sameZ = tcEqType z1 z2
576 interactInertSub _ _ _ _ = []
577
578 interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
579 interactInertMul [x1,y1] z1 [x2,y2] z2
580 | sameZ && known (/= 0) x1 && tcEqType x1 x2 = [ y1 === y2 ]
581 | sameZ && known (/= 0) y1 && tcEqType y1 y2 = [ x1 === x2 ]
582 where sameZ = tcEqType z1 z2
583
584 interactInertMul _ _ _ _ = []
585
586 interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
587 interactInertExp [x1,y1] z1 [x2,y2] z2
588 | sameZ && known (> 1) x1 && tcEqType x1 x2 = [ y1 === y2 ]
589 | sameZ && known (> 0) y1 && tcEqType y1 y2 = [ x1 === x2 ]
590 where sameZ = tcEqType z1 z2
591
592 interactInertExp _ _ _ _ = []
593
594
595 interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
596 interactInertLeq [x1,y1] z1 [x2,y2] z2
597 | bothTrue && tcEqType x1 y2 && tcEqType y1 x2 = [ x1 === y1 ]
598 | bothTrue && tcEqType y1 x2 = [ (x1 <== y2) === bool True ]
599 | bothTrue && tcEqType y2 x1 = [ (x2 <== y1) === bool True ]
600 where bothTrue = isJust $ do True <- isBoolLitTy z1
601 True <- isBoolLitTy z2
602 return ()
603
604 interactInertLeq _ _ _ _ = []
605
606
607
608
609
610
611
612
613 {- -----------------------------------------------------------------------------
614 These inverse functions are used for simplifying propositions using
615 concrete natural numbers.
616 ----------------------------------------------------------------------------- -}
617
618 -- | Subtract two natural numbers.
619 minus :: Integer -> Integer -> Maybe Integer
620 minus x y = if x >= y then Just (x - y) else Nothing
621
622 -- | Compute the exact logarithm of a natural number.
623 -- The logarithm base is the second argument.
624 logExact :: Integer -> Integer -> Maybe Integer
625 logExact x y = do (z,True) <- genLog x y
626 return z
627
628
629 -- | Divide two natural numbers.
630 divide :: Integer -> Integer -> Maybe Integer
631 divide _ 0 = Nothing
632 divide x y = case divMod x y of
633 (a,0) -> Just a
634 _ -> Nothing
635
636 -- | Compute the exact root of a natural number.
637 -- The second argument specifies which root we are computing.
638 rootExact :: Integer -> Integer -> Maybe Integer
639 rootExact x y = do (z,True) <- genRoot x y
640 return z
641
642
643
644 {- | Compute the the n-th root of a natural number, rounded down to
645 the closest natural number. The boolean indicates if the result
646 is exact (i.e., True means no rounding was done, False means rounded down).
647 The second argument specifies which root we are computing. -}
648 genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
649 genRoot _ 0 = Nothing
650 genRoot x0 1 = Just (x0, True)
651 genRoot x0 root = Just (search 0 (x0+1))
652 where
653 search from to = let x = from + div (to - from) 2
654 a = x ^ root
655 in case compare a x0 of
656 EQ -> (x, True)
657 LT | x /= from -> search x to
658 | otherwise -> (from, False)
659 GT | x /= to -> search from x
660 | otherwise -> (from, False)
661
662 {- | Compute the logarithm of a number in the given base, rounded down to the
663 closest integer. The boolean indicates if we the result is exact
664 (i.e., True means no rounding happened, False means we rounded down).
665 The logarithm base is the second argument. -}
666 genLog :: Integer -> Integer -> Maybe (Integer, Bool)
667 genLog x 0 = if x == 1 then Just (0, True) else Nothing
668 genLog _ 1 = Nothing
669 genLog 0 _ = Nothing
670 genLog x base = Just (exactLoop 0 x)
671 where
672 exactLoop s i
673 | i == 1 = (s,True)
674 | i < base = (s,False)
675 | otherwise =
676 let s1 = s + 1
677 in s1 `seq` case divMod i base of
678 (j,r)
679 | r == 0 -> exactLoop s1 j
680 | otherwise -> (underLoop s1 j, False)
681
682 underLoop s i
683 | i < base = s
684 | otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i base)
685
686
687
688
689
690
691