0819777 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Improved type-directed disambiguation

If disambiguation fails, then instead of reporting an error immediately, defer the elaboration until later. Fixes #2285. In the process, PAlternative now has a more descriptive argument than merely a Bool to say whether it's a proof search, or a disambiguation, and whether it's allowed to be delayed or not. IBCs need rebuilding.

commit0819777c73c6f00b48bbb202bf9de14c071760c7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 17 May 2015, 16:26 (11 years ago) parenta52c76e

11 files changed+166−25

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+1−1 src/Idris/AbsSyntaxTree.hs+5−2 src/Idris/Core/Elaborate.hs+2−2 src/Idris/DeepSeq.hs+4 src/Idris/Elab/Term.hs+43−13 src/Idris/Elab/Value.hs+1−1 src/Idris/IBC.hs+16−1 src/Idris/ParseExpr.hs+3−3 test/basic009/expected+1−2 test/reg064/reg064a.idr+89 test/reg064/run+1

src/Idris/AbsSyntax.hs+1−1

@@ -1659,7 +1659,7 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

16591659 then Right $ PApp fc (PRef ffc f) as

16601660 else Right $ mkPApp fc (length as) (PRef ffc f) as

16611661 alts -> Right $

1662− PAlternative True $

1662+ PAlternative (ExactlyOne True) $

16631663 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc (isImpName f f'))

16641664 (insertImpl ns as)) alts

16651665 where

src/Idris/AbsSyntaxTree.hs+5−2

@@ -677,7 +677,7 @@ data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

677677-- | For elaborator state

678678data EState = EState {

679679 case_decls :: [(Name, PDecl)],

680− delayed_elab :: [Elab' EState ()],

680+ delayed_elab :: [(Int, Elab' EState ())],

681681 new_tyDecls :: [RDeclInstructions],

682682 highlighting :: [(FC, OutputAnnotation)]

683683 }

@@ -835,7 +835,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

835835 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)

836836 | PDPair FC PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration)

837837 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only

838− | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

838+ | PAlternative PAltType [PTerm] -- ^ True if only one may work. (| A, B, C|)

839839 | PHidden PTerm -- ^ Irrelevant or hidden pattern

840840 | PType FC -- ^ 'Type' type

841841 | PUniverse Universe -- ^ Some universe

@@ -860,6 +860,9 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

860860 | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script

861861 deriving (Eq, Data, Typeable)

862862

863+data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

864+ | FirstSuccess

865+ deriving (Eq, Data, Typeable)

863866

864867{-!

865868deriving instance Binary PTerm

src/Idris/Core/Elaborate.hs+2−2

@@ -747,8 +747,8 @@ no_errors tac err

747747try :: Elab' aux a -> Elab' aux a -> Elab' aux a

748748try t1 t2 = try' t1 t2 False

749749

750−handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

751−handleError p t1 t2 proofSearch

750+handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a

751+handleError p t1 t2

752752 = do s <- get

753753 ps <- get_probs

754754 case runStateT t1 s of

src/Idris/DeepSeq.hs+4

@@ -263,6 +263,10 @@ instance NFData PTerm where

263263 rnf (PQuoteName x1) = rnf x1 `seq` ()

264264 rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

265265

266+instance NFData PAltType where

267+ rnf (ExactlyOne x1) = rnf x1 `seq` ()

268+ rnf FirstSuccess = ()

269+

266270instance (NFData t) => NFData (PTactic' t) where

267271 rnf (Intro x1) = rnf x1 `seq` ()

268272 rnf Intros = ()

src/Idris/Elab/Term.hs+43−13

@@ -217,7 +217,7 @@ elab ist info emode opts fn tm

217217 let fc = maybe "(unknown)"

218218 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

219219 est <- getAux

220− sequence_ (delayed_elab est)

220+ sequence_ (get_delayed_elab est)

221221 end_unify

222222 ptm <- get_term

223223 when pattern -- convert remaining holes to pattern vars

@@ -230,6 +230,10 @@ elab ist info emode opts fn tm

230230 pattern = emode == ELHS

231231 bindfree = emode == ETyDecl || emode == ELHS

232232

233+ get_delayed_elab est =

234+ let ds = delayed_elab est in

235+ map snd $ sortBy (\(p1, _) (p2, _) -> compare p1 p2) ds

236+

233237 tcgen = Dictionary `elem` opts

234238 reflection = Reflection `elem` opts

235239

@@ -287,7 +291,7 @@ elab ist info emode opts fn tm

287291 (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

288292 [pimp (sUN "t") Placeholder True,

289293 pimp (sUN "a") Placeholder True,

290− pexp ct])) True

294+ pexp ct]))

291295

292296 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

293297 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

@@ -428,7 +432,7 @@ elab ist info emode opts fn tm

428432 [pimp (sMN 0 "a") t False,

429433 pimp (sMN 0 "P") Placeholder True,

430434 pexp l, pexp r])

431− elab' ina fc (PAlternative True as)

435+ elab' ina fc (PAlternative (ExactlyOne delayok) as)

432436 = do hnf_compute

433437 ty <- goal

434438 ctxt <- get_context

@@ -438,12 +442,31 @@ elab ist info emode opts fn tm

438442-- trace (-- show tc ++ " " ++ show as ++ "\n ==> " ++

439443-- show (length as') ++ "\n" ++

440444-- showSep ", " (map showTmImpls as') ++ "\nEND") $

441− tryAll (zip (map (elab' ina fc) as') (map showHd as'))

445+ (h : hs) <- get_holes

446+ case as' of

447+ [x] -> elab' ina fc x

448+ -- If there's options, try now, and if that fails, postpone

449+ -- to later.

450+ _ -> handleError isAmbiguous

451+ (tryAll (zip (map (elab' ina fc) as')

452+ (map showHd as')))

453+ (do movelast h

454+ delayElab 5 $ do

455+ focus h

456+ tryAll (zip (map (elab' ina fc) as')

457+ (map showHd as')))

442458 where showHd (PApp _ (PRef _ n) _) = n

443459 showHd (PRef _ n) = n

444460 showHd (PApp _ h _) = showHd h

445461 showHd x = NErased -- We probably should do something better than this here

446− elab' ina fc (PAlternative False as)

462+

463+ isAmbiguous (CantResolveAlts _) = delayok

464+ isAmbiguous (Elaborating _ _ e) = isAmbiguous e

465+ isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e

466+ isAmbiguous (At _ e) = isAmbiguous e

467+ isAmbiguous _ = False

468+

469+ elab' ina fc (PAlternative FirstSuccess as)

447470 = trySeq as

448471 where -- if none work, take the error from the first

449472 trySeq (x : xs) = let e1 = elab' ina fc x in

@@ -1097,9 +1120,9 @@ elab ist info emode opts fn tm

10971120 -- Delay dotted things to the end, then when we elaborate them

10981121 -- we can check the result against what was inferred

10991122 movelast h

1100− delayElab $ do focus h

1101− dotterm

1102− elab' ina fc t

1123+ delayElab 10 $ do focus h

1124+ dotterm

1125+ elab' ina fc t

11031126 elab' ina fc (PRunElab fc' tm) =

11041127 do attack

11051128 n <- getNameFrom (sMN 0 "tacticScript")

@@ -1117,7 +1140,13 @@ elab ist info emode opts fn tm

11171140 solve

11181141 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

11191142

1120− delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })

1143+ -- delay elaboration of 't', with priority 'pri' until after everything

1144+ -- else is done.

1145+ -- The delayed things with lower numbered priority will be elaborated

1146+ -- first. (In practice, this means delayed alternatives, then PHidden

1147+ -- things.)

1148+ delayElab pri t

1149+ = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

11211150

11221151 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

11231152 isScr (PRef _ n) (n', b) = (n', (n == n', b))

@@ -1179,7 +1208,7 @@ elab ist info emode opts fn tm

11791208 let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]

11801209 case tyh of

11811210 P _ (UN l) _ | l == txt "Lazy'"

1182− -> return (PAlternative False tries)

1211+ -> return (PAlternative FirstSuccess tries)

11831212 _ -> return t

11841213 where

11851214 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)

@@ -1197,7 +1226,7 @@ elab ist info emode opts fn tm

11971226 notImplicitable (PRef _ n)

11981227 | [opts] <- lookupCtxt n (idris_flags ist)

11991228 = NoImplicit `elem` opts

1200− notImplicitable (PAlternative True as) = any notImplicitable as

1229+ notImplicitable (PAlternative (ExactlyOne _) as) = any notImplicitable as

12011230 -- case is tricky enough without implicit coercions! If they are needed,

12021231 -- they can go in the branches separately.

12031232 notImplicitable (PCase _ _ _) = True

@@ -1240,8 +1269,9 @@ elab ist info emode opts fn tm

12401269 let t' = case (t, cs) of

12411270 (PCoerced tm, _) -> tm

12421271 (_, []) -> t

1243− (_, cs) -> PAlternative False [t ,

1244− PAlternative True (map (mkCoerce env t) cs)]

1272+ (_, cs) -> PAlternative FirstSuccess [t ,

1273+ PAlternative (ExactlyOne False)

1274+ (map (mkCoerce env t) cs)]

12451275 return t'

12461276 where

12471277 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

src/Idris/Elab/Value.hs+1−1

@@ -119,7 +119,7 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

119119-- Try running the term directly (as IO ()), then printing it as an Integer

120120-- (as a default numeric tye), then printing it as any Showable thing

121121elabExec :: FC -> PTerm -> PTerm

122−elabExec fc tm = runtm (PAlternative False

122+elabExec fc tm = runtm (PAlternative FirstSuccess

123123 [printtm (PApp fc (PRef fc (sUN "the"))

124124 [pexp (PConstant NoFC (AType (ATInt ITBig))), pexp tm]),

125125 tm,

src/Idris/IBC.hs+16−1

@@ -41,7 +41,7 @@ import Codec.Archive.Zip

4141import Util.Zlib (decompressEither)

4242

4343ibcVersion :: Word16

44−ibcVersion = 109

44+ibcVersion = 110

4545

4646data IBCFile = IBCFile { ver :: Word16,

4747 sourcefile :: FilePath,

@@ -1778,6 +1778,21 @@ instance Binary PTerm where

17781778 return (PIfThenElse x1 x2 x3 x4)

17791779 _ -> error "Corrupted binary data for PTerm"

17801780

1781+instance Binary PAltType where

1782+ put x

1783+ = case x of

1784+ ExactlyOne x1 -> do putWord8 0

1785+ put x1

1786+ FirstSuccess -> putWord8 1

1787+ get

1788+ = do i <- getWord8

1789+ case i of

1790+ 0 -> do x1 <- get

1791+ return (ExactlyOne x1)

1792+ 1 -> return FirstSuccess

1793+ _ -> error "Corrupted binary data for PAltType"

1794+

1795+

17811796instance (Binary t) => Binary (PTactic' t) where

17821797 put x

17831798 = case x of

src/Idris/ParseExpr.hs+3−3

@@ -445,10 +445,10 @@ bracketedExpr syn e =

445445modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

446446modifyConst syn fc (PConstant inFC (BI x))

447447 | not (inPattern syn)

448− = PAlternative False

448+ = PAlternative FirstSuccess

449449 (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]

450450 : consts)

451− | otherwise = PAlternative False consts

451+ | otherwise = PAlternative FirstSuccess consts

452452 where

453453 consts = [ PConstant inFC (BI x)

454454 , PConstant inFC (I (fromInteger x))

@@ -471,7 +471,7 @@ modifyConst syn fc x = x

471471-}

472472alt :: SyntaxInfo -> IdrisParser PTerm

473473alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"

474− return (PAlternative False alts)

474+ return (PAlternative FirstSuccess alts)

475475

476476{- | Parses a possibly hidden simple expression

477477@

test/basic009/expected+1−2

@@ -1,5 +1,4 @@

11MAIN-PASS

22Faulty.idr:6:7:When elaborating type of Faulty.fault:

3−When elaborating argument x to type constructor =:

4− Can't disambiguate name: A.num, B.C.num

3+Can't disambiguate name: A.num, B.C.num

54Multiple.idr:3:1:import alias not unique: "X"

test/reg064/reg064a.idrnew file+89

@@ -0,0 +1,89 @@

1+import Data.Vect

2+import Data.Fin

3+import Control.Isomorphism

5+Dec0 : Type -> Type

6+Dec0 = Dec

8+Dec1 : {A : Type} -> (P : A -> Type) -> Type

9+Dec1 {A} P = (a : A) -> Dec0 (P a)

10+

11+Unique : Type -> Type

12+Unique t = (p : t) -> (q : t) -> p = q

13+

14+Unique0 : Type -> Type

15+Unique0 = Unique

16+

17+Unique1 : (t0 -> Type) -> Type

18+Unique1 {t0} t1 = (v : t0) -> Unique0 (t1 v)

19+

20+namespace Iso

21+

22+ from : {A, B : Type} -> Iso A B -> (B -> A)

23+ from (MkIso to from toFrom fromTo) = from

24+

25+namespace Fin

26+

27+ ||| 'Tail' of a finite function

28+ tail : {A : Type} -> {n : Nat} ->

29+ (Fin (S n) -> A) -> (Fin n -> A)

30+ tail f k = f (FS k)

31+

32+ ||| Maps a finite function to a vector

33+ toVect : {A : Type} -> {n : Nat} ->

34+ (Fin n -> A) -> Vect n A

35+ toVect {n = Z} _ = Nil

36+ toVect {n = S m} f = (f FZ) :: (toVect (tail f))

37+

38+namespace Finite

39+

40+ ||| Notion of finiteness for types

41+ Finite : Type -> Type

42+ Finite A = Exists (\ n => Iso A (Fin n))

43+

44+ ||| Cardinality of finite types

45+ card : {A : Type} -> (fA : Finite A) -> Nat

46+ card = getWitness

47+

48+ ||| Maps a finite type |A| of cardinality |n| to a vector of |A|-values of length |n|

49+ toVect : {A : Type} -> (fA : Finite A) -> Vect (card fA) A

50+ toVect (Evidence n iso) = toVect (from iso)

51+

52+||| Filters a vector on a decidable property and pairs elements with proofs

53+filterTag : {A : Type} ->

54+ {P : A -> Type} ->

55+ Dec1 P ->

56+ Vect n A ->

57+ Sigma Nat (\ m => Vect m (Sigma A P))

58+filterTag d1P Nil = (_ ** Nil)

59+filterTag d1P (a :: as) with (filterTag d1P as)

60+ | (_ ** tail) with (d1P a)

61+ | (Yes p) = (_ ** (a ** p) :: tail)

62+ | (No _) = (_ ** tail)

63+

64+||| Maps a finite type |A| and a decidable predicate |P| to a vector |Sigma A P| values

65+toVect : {A : Type} ->

66+ {P : A -> Type} ->

67+ Finite A ->

68+ Dec1 P ->

69+ (n : Nat ** Vect n (Sigma A P))

70+toVect fA d1P = filterTag d1P (toVect fA)

71+

72+sigmaUniqueLemma1 : {A : Type} ->

73+ {P : A -> Type} ->

74+ Unique1 {t0 = A} P ->

75+ (a : A) ->

76+ (p : P a) ->

77+ (ss : Vect n (Sigma A P)) ->

78+ Elem a (map getWitness ss) ->

79+ Elem (a ** p) ss

80+

81+toVectComplete : {A : Type} ->

82+ {P : A -> Type} ->

83+ (fA : Finite A) ->

84+ (d1P : Dec1 P) ->

85+ Unique1 {t0 = A} P ->

86+ (s : Sigma A P) ->

87+ Elem s (getProof (toVect fA d1P))

88+

89+

test/reg064/run+1

@@ -1,3 +1,4 @@

11#!/usr/bin/env bash

22idris $@ reg064.idr --check

3+idris $@ reg064a.idr --check

34rm -f *.ibc