a89330e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change meaning of 'data' in interfaces

A "data" declaration in an interface means "this must be implemented by something injective, so that unification can determine the arguments". This is slightly weaker than the existing definition, which required the definition to be an actual data type. It means that unification can learn less, but it is far more useful in practice, it turns out. This breaks the interfaces005 test, but it is not clear that this test is testing something that we want to do, and if we do want to do it, we can do it a different way...

commita89330e8184317bd41fc19e256634a7667b66a6a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 24 Mar 2017, 16:21 (10 years ago) parent92bac30

3 files changed+27−11

compare with master

unifiedsplit

src/Idris/Core/Unify.hs+18−2 test/TestData.hs+1−1 test/interfaces005/interfaces005.idr+8−8

src/Idris/Core/Unify.hs+18−2

@@ -303,11 +303,17 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

303303

304304 injective (P (DCon _ _ _) _ _) = True

305305 injective (P (TCon _ _) _ _) = True

306− injective (P Ref n _)

307− | Just i <- lookupInjectiveExact n ctxt = i

306+-- injective (P Ref n _)

307+-- | Just i <- lookupInjectiveExact n ctxt = i

308308 injective (App _ f a) = injective f -- && injective a

309309 injective _ = False

310310

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+

311317-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK

312318 injectiveVar (P _ n _) = n `elem` inj

313319 injectiveVar (App _ f a) = injectiveVar f -- && injective a

@@ -534,6 +540,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

534540 | (injectiveApp fx && injectiveApp fy)

535541 || (injectiveApp fx && metavarApp fy && ax == ay)

536542 || (injectiveApp fy && metavarApp fx && ax == ay)

543+ || (injectiveTC fx fy) -- data interface method

537544 = do let (headx, _) = unApply fx

538545 let (heady, _) = unApply fy

539546 -- fail quickly if the heads are disjoint

@@ -612,6 +619,15 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

612619

613620 notFn t = injective t || metavar t || inenv t

614621

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+

615631

616632 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]

617633 unifyTmpFail x y

test/TestData.hs+1−1

@@ -157,7 +157,7 @@ testFamiliesData = [

157157 ( 2, ANY ),

158158 ( 3, ANY ),

159159 ( 4, ANY ),

160− ( 5, ANY ),

160+-- ( 5, ANY ),

161161 ( 6, ANY ),

162162 ( 7, ANY )]),

163163 ("io", "IO monad",

test/interfaces005/interfaces005.idr+8−8

@@ -39,15 +39,15 @@ namespace TreeSet

3939using implementation TreeSet

4040

4141 test : Set Nat

42− test = insert 3 $

43− insert 2 $

44− insert 7 $

45− insert 3 $

46− insert 4 $

47− insert 5 new

42+ test = -- insert (the Nat 3) $

43+-- insert 2 $

44+-- insert 7 $

45+-- insert 3 $

46+-- insert 4 $

47+ insert {a = Nat} (the Nat 5) new

4848

4949 foo : Bool

50− foo = member 6 test

50+ foo = member (the Nat 6) test

5151

5252 bar : Bool

53− bar = member 3 test

53+ bar = member (the Nat 3) test