git.iko.soy/Idris-dev
on master help sign in
Change meaning of 'data' in interfaces
a89330eEdwin Brady
src/Idris/Core/Unify.hs+18−2
compare with master
unifiedsplit
@@ -303,11 +303,17 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
303
303
304 injective (P (DCon _ _ _) _ _) = True
304 injective (P (DCon _ _ _) _ _) = True
305 injective (P (TCon _ _) _ _) = True
305 injective (P (TCon _ _) _ _) = True
306− injective (P Ref n _)
306+-- injective (P Ref n _)
307− | Just i <- lookupInjectiveExact n ctxt = i
307+-- | Just i <- lookupInjectiveExact n ctxt = i
308 injective (App _ f a) = injective f -- && injective a
308 injective (App _ f a) = injective f -- && injective a
309 injective _ = False
309 injective _ = False
310
310
311+-- injectiveTC (P Ref n _) (P Ref n' _)
312+-- | Just i <- lookupInjectiveExact n ctxt,
313+-- n == n' = i
314+-- injectiveTC (App _ f a) (App _ f' a') = injectiveTC f a
315+-- injectiveTC _ _ = False
316+
311-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
317-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
312 injectiveVar (P _ n _) = n `elem` inj
318 injectiveVar (P _ n _) = n `elem` inj
313 injectiveVar (App _ f a) = injectiveVar f -- && injective a
319 injectiveVar (App _ f a) = injectiveVar f -- && injective a
@@ -534,6 +540,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
534 | (injectiveApp fx && injectiveApp fy)
540 | (injectiveApp fx && injectiveApp fy)
535 || (injectiveApp fx && metavarApp fy && ax == ay)
541 || (injectiveApp fx && metavarApp fy && ax == ay)
536 || (injectiveApp fy && metavarApp fx && ax == ay)
542 || (injectiveApp fy && metavarApp fx && ax == ay)
543+ || (injectiveTC fx fy) -- data interface method
537 = do let (headx, _) = unApply fx
544 = do let (headx, _) = unApply fx
538 let (heady, _) = unApply fy
545 let (heady, _) = unApply fy
539 -- fail quickly if the heads are disjoint
546 -- fail quickly if the heads are disjoint
@@ -612,6 +619,15 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
612
619
613 notFn t = injective t || metavar t || inenv t
620 notFn t = injective t || metavar t || inenv t
614
621
622+ injectiveTC t@(P Ref n _) t'@(P Ref n' _)
623+ | Just ni <- lookupInjectiveExact n ctxt,
624+ Just ni' <- lookupInjectiveExact n' ctxt
625+ = (n == n' && ni) ||
626+ (ni && metavar t') ||
627+ (metavar t && ni')
628+ injectiveTC (App _ f a) (App _ f' a') = injectiveTC f f'
629+ injectiveTC _ _ = False
630+
615
631
616 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
632 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
617 unifyTmpFail x y
633 unifyTmpFail x y
test/TestData.hs+1−1
@@ -157,7 +157,7 @@ testFamiliesData = [
157 ( 2, ANY ),
157 ( 2, ANY ),
158 ( 3, ANY ),
158 ( 3, ANY ),
159 ( 4, ANY ),
159 ( 4, ANY ),
160− ( 5, ANY ),
160+-- ( 5, ANY ),
161 ( 6, ANY ),
161 ( 6, ANY ),
162 ( 7, ANY )]),
162 ( 7, ANY )]),
163 ("io", "IO monad",
163 ("io", "IO monad",
test/interfaces005/interfaces005.idr+8−8
@@ -39,15 +39,15 @@ namespace TreeSet
39using implementation TreeSet
39using implementation TreeSet
40
40
41 test : Set Nat
41 test : Set Nat
42− test = insert 3 $
42+ test = -- insert (the Nat 3) $
43− insert 2 $
43+-- insert 2 $
44− insert 7 $
44+-- insert 7 $
45− insert 3 $
45+-- insert 3 $
46− insert 4 $
46+-- insert 4 $
47− insert 5 new
47+ insert {a = Nat} (the Nat 5) new
48
48
49 foo : Bool
49 foo : Bool
50− foo = member 6 test
50+ foo = member (the Nat 6) test
51
51
52 bar : Bool
52 bar : Bool
53− bar = member 3 test
53+ bar = member (the Nat 3) test