0819777 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improved type-directed disambiguation

0819777Edwin Brady11 years ago

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

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

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

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

1661 alts -> Right $

1662− PAlternative True $

1662+ PAlternative (ExactlyOne True) $

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

1664 (insertImpl ns as)) alts

1665 where

src/Idris/AbsSyntaxTree.hs+5−2

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

677-- | For elaborator state

678data EState = EState {

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

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

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

681 new_tyDecls :: [RDeclInstructions],

682 highlighting :: [(FC, OutputAnnotation)]

683 }

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

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

836 | 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)

837 | 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|)

839 | PHidden PTerm -- ^ Irrelevant or hidden pattern

840 | PType FC -- ^ 'Type' type

841 | PUniverse Universe -- ^ Some universe

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

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

861 deriving (Eq, Data, Typeable)

862

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

864+ | FirstSuccess

865+ deriving (Eq, Data, Typeable)

863

866

864{-!

867{-!

865deriving instance Binary PTerm

868deriving instance Binary PTerm

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

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

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

748try t1 t2 = try' t1 t2 False

749

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

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

751−handleError p t1 t2 proofSearch

751+handleError p t1 t2

752 = do s <- get

753 ps <- get_probs

754 case runStateT t1 s of

src/Idris/DeepSeq.hs+4

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

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

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

265

266+instance NFData PAltType where

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

268+ rnf FirstSuccess = ()

269+

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

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

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

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

268 rnf Intros = ()

272 rnf Intros = ()

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

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

217 let fc = maybe "(unknown)"

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

219 est <- getAux

220− sequence_ (delayed_elab est)

220+ sequence_ (get_delayed_elab est)

221 end_unify

222 ptm <- get_term

223 when pattern -- convert remaining holes to pattern vars

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

230 pattern = emode == ELHS

231 bindfree = emode == ETyDecl || emode == ELHS

232

233+ get_delayed_elab est =

234+ let ds = delayed_elab est in

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

236+

233 tcgen = Dictionary `elem` opts

237 tcgen = Dictionary `elem` opts

234 reflection = Reflection `elem` opts

238 reflection = Reflection `elem` opts

235

239

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

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

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

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

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

289 pimp (sUN "a") Placeholder True,

293 pimp (sUN "a") Placeholder True,

290− pexp ct])) True

294+ pexp ct]))

291

295

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

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

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

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

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

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

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

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

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

430 pexp l, pexp r])

434 pexp l, pexp r])

431− elab' ina fc (PAlternative True as)

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

432 = do hnf_compute

436 = do hnf_compute

433 ty <- goal

437 ty <- goal

434 ctxt <- get_context

438 ctxt <- get_context

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

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

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

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

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

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

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

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

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

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')))

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

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

443 showHd (PRef _ n) = n

459 showHd (PRef _ n) = n

444 showHd (PApp _ h _) = showHd h

460 showHd (PApp _ h _) = showHd h

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

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

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+

446− elab' ina fc (PAlternative False as)

469+ elab' ina fc (PAlternative FirstSuccess as)

447 = trySeq as

470 = trySeq as

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

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

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

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

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

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

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

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

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

1099 movelast h

1122 movelast h

1100− delayElab $ do focus h

1123+ delayElab 10 $ do focus h

1101− dotterm

1124+ dotterm

1102− elab' ina fc t

1125+ elab' ina fc t

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

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

1104 do attack

1127 do attack

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

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

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

1117 solve

1140 solve

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

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

1119

1142

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

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

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

1121

1150

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

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

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

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

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

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

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

1180 case tyh of

1209 case tyh of

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

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

1182− -> return (PAlternative False tries)

1211+ -> return (PAlternative FirstSuccess tries)

1183 _ -> return t

1212 _ -> return t

1184 where

1213 where

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

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

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

1197 notImplicitable (PRef _ n)

1226 notImplicitable (PRef _ n)

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

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

1199 = NoImplicit `elem` opts

1228 = NoImplicit `elem` opts

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

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

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

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

1202 -- they can go in the branches separately.

1231 -- they can go in the branches separately.

1203 notImplicitable (PCase _ _ _) = True

1232 notImplicitable (PCase _ _ _) = True

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

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

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

1241 (PCoerced tm, _) -> tm

1270 (PCoerced tm, _) -> tm

1242 (_, []) -> t

1271 (_, []) -> t

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

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

1273+ PAlternative (ExactlyOne False)

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

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

1245 return t'

1275 return t'

1246 where

1276 where

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

1277 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

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

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

121elabExec :: FC -> PTerm -> PTerm

122−elabExec fc tm = runtm (PAlternative False

122+elabExec fc tm = runtm (PAlternative FirstSuccess

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

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

125 tm,

src/Idris/IBC.hs+16−1

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

41import Util.Zlib (decompressEither)

43ibcVersion :: Word16

44−ibcVersion = 109

44+ibcVersion = 110

46data IBCFile = IBCFile { ver :: Word16,

47 sourcefile :: FilePath,

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

1778 return (PIfThenElse x1 x2 x3 x4)

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

1780

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+

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

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

1782 put x

1797 put x

1783 = case x of

1798 = case x of

src/Idris/ParseExpr.hs+3−3

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

445modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

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

447 | not (inPattern syn)

448− = PAlternative False

448+ = PAlternative FirstSuccess

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

450 : consts)

451− | otherwise = PAlternative False consts

451+ | otherwise = PAlternative FirstSuccess consts

452 where

453 consts = [ PConstant inFC (BI x)

454 , PConstant inFC (I (fromInteger x))

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

471-}

472alt :: SyntaxInfo -> IdrisParser PTerm

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

474− return (PAlternative False alts)

474+ return (PAlternative FirstSuccess alts)

475

476{- | Parses a possibly hidden simple expression

477@

test/basic009/expected+1−2

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

1MAIN-PASS

2Faulty.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

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

4Multiple.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 @@

1#!/usr/bin/env bash

2idris $@ reg064.idr --check

3+idris $@ reg064a.idr --check

3rm -f *.ibc

4rm -f *.ibc