8e6e14a · Idris-dev · git.iko.soy

CHANGELOG+6

compare with master

unifiedsplit

@@ -1,3 +1,9 @@

1+New in 0.9.12:

2+--------------

3+

4+* Proof search now works for metavariables in types, giving some interactive

5+ type inference.

6+

1New in 0.9.11:

7New in 0.9.11:

2--------------

8--------------

3

9

idris.cabal+5−1

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

1Name: idris

2−Version: 0.9.11.1

2+Version: 0.9.11.2

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -294,6 +294,10 @@ Extra-source-files:

294 test/interactive001/input

295 test/interactive001/*.idr

296 test/interactive001/expected

297+ test/interactive002/run

298+ test/interactive002/input

299+ test/interactive002/*.idr

300+ test/interactive002/expected

297

301

298 test/io001/run

302 test/io001/run

299 test/io001/*.idr

303 test/io001/*.idr

libs/base/Control/Isomorphism.idr−1

@@ -1,7 +1,6 @@

1module Control.Isomorphism

2

3import Syntax.PreorderReasoning

4−import Uninhabited

5

4

6%default total

5%default total

7

6

libs/base/base.ipkg−2

@@ -10,8 +10,6 @@ modules = System,

10

11 Decidable.Decidable, Decidable.Order,

12

13− Uninhabited,

14−

15 Providers,

13 Providers,

16

14

17 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,

15 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,

libs/prelude/Prelude.idr+1

@@ -20,6 +20,7 @@ import Prelude.Chars

20import Prelude.Traversable

21import Prelude.Bits

22import Prelude.Stream

23+import Prelude.Uninhabited

23

24

24import Decidable.Equality

25import Decidable.Equality

25

26

libs/base/Uninhabited.idr → libs/prelude/Prelude/Uninhabited.idrrenamed+1−1

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

1−module Uninhabited

1+module Prelude.Uninhabited

2

3class Uninhabited t where

4 total uninhabited : t -> _|_

libs/prelude/prelude.ipkg+2−1

@@ -1,13 +1,14 @@

1package prelude

2

3opts = "--nobuiltins --total"

4−modules = Builtins, Prelude, IO,

4+modules = Builtins, Prelude, IO,

5

6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

7 Prelude.Classes, Prelude.Nat, Prelude.Fin, Prelude.List,

8 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

9 Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Functor,

10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11+ Prelude.Uninhabited,

11

12

12 Decidable.Equality

13 Decidable.Equality

13

14

src/IRTS/CodegenJavaScript.hs+176−5

@@ -409,13 +409,30 @@ removeAllocations js = transformJS removeAllocations js

409

410isJSConstant :: JS -> Bool

411isJSConstant js

412− | JSString _ <- js = True

412+ | JSString _ <- js = True

413− | JSChar _ <- js = True

413+ | JSChar _ <- js = True

414− | JSNum _ <- js = True

414+ | JSNum _ <- js = True

415− | JSType _ <- js = True

415+ | JSType _ <- js = True

416− | JSNull <- js = True

416+ | JSNull <- js = True

417+ | JSArray vals <- js = all isJSConstant vals

417

418

418 | JSApp (JSIdent "__IDRRT__bigInt") _ <- js = True

419 | JSApp (JSIdent "__IDRRT__bigInt") _ <- js = True

420+

421+ | otherwise = False

422+

423+isJSConstantConstructor :: [String] -> JS -> Bool

424+isJSConstantConstructor constants js

425+ | isJSConstant js =

426+ True

427+ | JSArray vals <- js =

428+ all (isJSConstantConstructor constants) vals

429+ | JSNew "__IDRRT__Con" args <- js =

430+ all (isJSConstantConstructor constants) args

431+ | JSIndex (JSProj (JSIdent _) "vars") (JSNum _) <- js =

432+ True

433+ | JSIdent name <- js

434+ , name `elem` constants =

435+ True

419 | otherwise = False

436 | otherwise = False

420

437

421

438

@@ -1000,6 +1017,158 @@ optimizeJS = inlineLoop

1000 | otherwise = js

1017 | otherwise = js

1001

1018

1002

1019

1020+extractLocalConstructors :: [JS] -> [JS]

1021+extractLocalConstructors js =

1022+ concatMap extractLocalConstructors' js

1023+ where

1024+ globalCons :: [String]

1025+ globalCons = concatMap (getGlobalCons) js

1026+

1027+

1028+ extractLocalConstructors' :: JS -> [JS]

1029+ extractLocalConstructors' js@(JSAlloc fun (Just (JSFunction args body))) =

1030+ map allocCon cons ++ [foldr (uncurry jsSubst) js (reverse cons)]

1031+ where

1032+ cons :: [(JS, JS)]

1033+ cons = zipWith genName (foldJS match (++) [] body) [1..]

1034+ where

1035+ genName :: JS -> Int -> (JS, JS)

1036+ genName js id =

1037+ (js, JSIdent $ idrCTRNamespace ++ fun ++ "_" ++ show id)

1038+

1039+ match :: JS -> [JS]

1040+ match js

1041+ | JSNew "__IDRRT__Con" args <- js

1042+ , all isConstant args = [js]

1043+ | otherwise = []

1044+

1045+

1046+ allocCon :: (JS, JS) -> JS

1047+ allocCon (js, JSIdent name) =

1048+ JSAlloc name (Just js)

1049+

1050+

1051+ isConstant :: JS -> Bool

1052+ isConstant js

1053+ | JSNew "__IDRRT__Con" args <- js

1054+ , all isConstant args =

1055+ True

1056+ | otherwise =

1057+ isJSConstantConstructor globalCons js

1058+

1059+ extractLocalConstructors' js = [js]

1060+

1061+

1062+ getGlobalCons :: JS -> [String]

1063+ getGlobalCons js = foldJS match (++) [] js

1064+ where

1065+ match :: JS -> [String]

1066+ match js

1067+ | (JSAlloc name (Just (JSNew "__IDRRT__Con" _))) <- js =

1068+ [name]

1069+ | otherwise =

1070+ []

1071+

1072+

1073+evalCons :: [JS] -> [JS]

1074+evalCons js =

1075+ map (collapseCont . collapseTC . expandProj . evalCons') js

1076+ where

1077+ cons :: [(String, JS)]

1078+ cons = concatMap getGlobalCons js

1079+

1080+ evalCons' :: JS -> JS

1081+ evalCons' js = transformJS match js

1082+ where

1083+ match :: JS -> JS

1084+ match (JSApp (JSIdent "__IDRRT__EVALTC") [arg])

1085+ | JSIdent name <- arg

1086+ , Just (JSNew _ [_, JSNull, _, _]) <- lookupConstructor name cons =

1087+ arg

1088+

1089+ match (JSApp (JSIdent "__IDR__mEVAL0") [arg])

1090+ | JSIdent name <- arg

1091+ , Just (JSNew _ [_, JSNull, _, _]) <- lookupConstructor name cons =

1092+ arg

1093+

1094+ match js = transformJS match js

1095+

1096+

1097+ lookupConstructor :: String -> [(String, JS)] -> Maybe JS

1098+ lookupConstructor ctr cons

1099+ | Just (JSIdent name) <- lookup ctr cons = lookupConstructor name cons

1100+ | Just con@(JSNew _ _) <- lookup ctr cons = Just con

1101+ | otherwise = Nothing

1102+

1103+

1104+ expandProj :: JS -> JS

1105+ expandProj js = transformJS match js

1106+ where

1107+ match :: JS -> JS

1108+ match (

1109+ JSIndex (

1110+ JSProj (JSIdent name) "vars"

1111+ ) (

1112+ JSNum (JSInt idx)

1113+ )

1114+ )

1115+ | Just (JSNew _ [_, _, _, JSArray args]) <- lookup name cons =

1116+ args !! idx

1117+

1118+ match js = transformJS match js

1119+

1120+

1121+ collapseTC :: JS -> JS

1122+ collapseTC js = transformJS match js

1123+ where

1124+ match :: JS -> JS

1125+ match (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

1126+ JSReturn (JSIdent name)

1127+ )])

1128+ | Just _ <- lookup name cons = (JSIdent name)

1129+

1130+ match js = transformJS match js

1131+

1132+

1133+ collapseCont :: JS -> JS

1134+ collapseCont js = transformJS match js

1135+ where

1136+ match :: JS -> JS

1137+ match (JSNew "__IDRRT__Cont" [JSFunction [] (

1138+ JSReturn ret@(JSNew "__IDRRT__Cont" [JSFunction [] _])

1139+ )]) = collapseCont ret

1140+

1141+

1142+ match (JSNew "__IDRRT__Cont" [JSFunction [] (

1143+ JSReturn (JSIdent name)

1144+ )]) = JSIdent name

1145+

1146+ match (JSNew "__IDRRT__Cont" [JSFunction [] (

1147+ JSReturn ret@(JSNew "__IDRRT__Con" [_, _, _, JSArray args])

1148+ )])

1149+ | all collapsable args = ret

1150+ where

1151+ collapsable :: JS -> Bool

1152+ collapsable (JSIdent _) = True

1153+ collapsable js = isJSConstantConstructor (map fst cons) js

1154+

1155+

1156+ match js = transformJS match js

1157+

1158+

1159+getGlobalCons :: JS -> [(String, JS)]

1160+getGlobalCons js = foldJS match (++) [] js

1161+ where

1162+ match :: JS -> [(String, JS)]

1163+ match js

1164+ | (JSAlloc name (Just con@(JSNew "__IDRRT__Con" _))) <- js =

1165+ [(name, con)]

1166+ | (JSAlloc name (Just con@(JSIdent _))) <- js =

1167+ [(name, con)]

1168+ | otherwise =

1169+ []

1170+

1171+

1003codegenJavaScript

1172codegenJavaScript

1004 :: JSTarget

1173 :: JSTarget

1005 -> [(Name, SDecl)]

1174 -> [(Name, SDecl)]

@@ -1056,7 +1225,9 @@ codegenJavaScript target definitions filename outputType = do

1056 , map removeInstanceChecks

1225 , map removeInstanceChecks

1057 , inlineFunctions

1226 , inlineFunctions

1058 , map reduceContinuations

1227 , map reduceContinuations

1228+ , extractLocalConstructors

1059 , unfoldLookupTable

1229 , unfoldLookupTable

1230+ , evalCons

1060 ]

1231 ]

1061

1232

1062 prelude :: [JS]

1233 prelude :: [JS]

src/Idris/AbsSyntax.hs+75−2

@@ -66,10 +66,13 @@ addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f

66addDyLib :: [String] -> Idris (Either DynamicLib String)

67addDyLib libs = do i <- getIState

68 let ls = idris_dynamic_libs i

69+ let importdirs = opt_importdirs (idris_options i)

69 case mapMaybe (findDyLib ls) libs of

70 case mapMaybe (findDyLib ls) libs of

70 x:_ -> return (Left x)

71 x:_ -> return (Left x)

71 [] -> do

72 [] -> do

73+ handle <- lift . lift .

72− handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs

74+ mapM (\l -> catchIO (tryLoadLib importdirs l)

75+ (\_ -> return Nothing)) $ libs

73 case msum handle of

76 case msum handle of

74 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++

77 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++

75 concat (intersperse "," libs) ++ "\"")

78 concat (intersperse "," libs) ++ "\"")

@@ -155,7 +158,77 @@ addToCG n cg

155 = do i <- getIState

158 = do i <- getIState

156 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

159 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

157

160

161+addTyInferred :: Name -> Idris ()

162+addTyInferred n

163+ = do i <- getIState

164+ putIState $ i { idris_tyinfodata =

165+ addDef n TIPartial (idris_tyinfodata i) }

166+

167+addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()

168+addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

169+ mapM_ addConstraint ts

170+ return ()

171+ where addConstraint (x, y) = findMVApps x y

172+

173+ findMVApps x y

174+ = do let (fx, argsx) = unApply x

175+ let (fy, argsy) = unApply y

176+ if (not (fx == fy))

177+ then do

178+ tryAddMV fx y

179+ tryAddMV fy x

180+ else mapM_ addConstraint (zip argsx argsy)

181+

182+ tryAddMV (P _ mv _) y =

183+ do ist <- get

184+ case lookup mv (idris_metavars ist) of

185+ Just _ -> addConstraintRule mv y

186+ _ -> return ()

187+ tryAddMV _ _ = return ()

188+

189+ addConstraintRule :: Name -> Term -> Idris ()

190+ addConstraintRule n t

191+ = do ist <- get

192+ logLvl 1 $ "TI constraint: " ++ show (n, t)

193+ case lookupCtxt n (idris_tyinfodata ist) of

194+ [TISolution ts] ->

195+ do mapM_ (checkConsistent t) ts

196+ let ti' = addDef n (TISolution (t : ts))

197+ (idris_tyinfodata ist)

198+ put $ ist { idris_tyinfodata = ti' }

199+ _ ->

200+ do let ti' = addDef n (TISolution [t])

201+ (idris_tyinfodata ist)

202+ put $ ist { idris_tyinfodata = ti' }

203+

204+ -- Check a solution is consistent with previous solutions

205+ -- Meaning: If heads are both data types, they had better be the

206+ -- same.

207+ checkConsistent :: Term -> Term -> Idris ()

208+ checkConsistent x y =

209+ do let (fx, _) = unApply x

210+ let (fy, _) = unApply y

211+ case (fx, fy) of

212+ (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)

213+ (P (TCon _ _) n _, Constant _) -> errWhen True

214+ (Constant _, P (TCon _ _) n' _) -> errWhen True

215+ (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n)

216+ _ -> return ()

217+

218+ where errWhen True

219+ = throwError (At fc

220+ (CantUnify False x y (Msg "") [] 0))

221+ errWhen False = return ()

222+

223+isTyInferred :: Name -> Idris Bool

224+isTyInferred n

225+ = do i <- getIState

226+ case lookupCtxt n (idris_tyinfodata i) of

227+ [TIPartial] -> return True

228+ _ -> return False

229+

158−-- | Adds error handlers for a particular function and argument. If names are is ambiguous, all matching handlers are updated.

230+-- | Adds error handlers for a particular function and argument. If names are

231+-- ambiguous, all matching handlers are updated.

159addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()

232addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()

160addFunctionErrorHandlers f arg hs =

233addFunctionErrorHandlers f arg hs =

161 do i <- getIState

234 do i <- getIState

src/Idris/AbsSyntaxTree.hs+12−2

@@ -112,6 +112,7 @@ data IState = IState {

112 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

113 idris_calledgraph :: Ctxt [Name],

114 idris_docstrings :: Ctxt String,

115+ idris_tyinfodata :: Ctxt TIData,

115 idris_totcheck :: [(FC, Name)], -- names to check totality on

116 idris_totcheck :: [(FC, Name)], -- names to check totality on

116 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

117 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

117 idris_options :: IOption,

118 idris_options :: IOption,

@@ -216,7 +217,7 @@ idrisInit :: IState

216idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

217idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

217 emptyContext emptyContext emptyContext emptyContext

218 emptyContext emptyContext emptyContext emptyContext

219 emptyContext emptyContext emptyContext emptyContext

219− emptyContext

220+ emptyContext emptyContext

220 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

221 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

221 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

222 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

222 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

223 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

@@ -811,6 +812,12 @@ deriving instance Binary ClassInfo

811deriving instance NFData ClassInfo

812deriving instance NFData ClassInfo

812!-}

813!-}

813

814

815+-- Type inference data

816+

817+data TIData = TIPartial -- ^ a function with a partially defined type

818+ | TISolution [Term] -- ^ possible solutions to a metavariable in a type

819+ deriving Show

820+

814-- An argument is conditionally forceable iff its forceability

821-- An argument is conditionally forceable iff its forceability

815-- depends on the collapsibility of the whole type.

822-- depends on the collapsibility of the whole type.

816data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)

823data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)

@@ -952,7 +959,10 @@ getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

952getInferTerm (App (App _ _) tm) = tm

959getInferTerm (App (App _ _) tm) = tm

953getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

960getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

954

961

955−getInferType (Bind n b sc) = Bind n b $ getInferType sc

962+getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

963+ where toTy (Lam t) = Pi t

964+ toTy (PVar t) = PVTy t

965+ toTy b = b

956getInferType (App (App _ ty) _) = ty

966getInferType (App (App _ ty) _) = ty

957

967

958

968

src/Idris/Core/Elaborate.hs−2

@@ -466,8 +466,6 @@ apply' fillt fn imps =

466 do args <- prepare_apply fn (map fst imps)

467 -- _Don't_ solve the arguments we're specifying by hand.

468 -- (remove from unified list before calling end_unify)

469− -- HMMM: Actually, if we get it wrong, the typechecker will complain!

470− -- so do nothing

471 hs <- get_holes

469 hs <- get_holes

472 ES (p, a) s prev <- get

470 ES (p, a) s prev <- get

473 let dont = head hs : dontunify p ++

471 let dont = head hs : dontunify p ++

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

@@ -257,7 +257,7 @@ unify ctxt env topx topy dont holes =

257 then unifyTmpFail xtm tm

258 else do sc 1

259 checkCycle bnames (x, tm)

260− | not (injective xtm) && injective tm = unifyFail xtm tm

260+ | not (injective xtm) && injective tm = unifyTmpFail xtm tm

261 un' fn bnames tm ytm@(P _ y _)

262 | holeIn env y || y `elem` holes

263 = do UI s f <- get

@@ -268,7 +268,7 @@ unify ctxt env topx topy dont holes =

268 then unifyTmpFail tm ytm

269 else do sc 1

270 checkCycle bnames (y, tm)

271− | not (injective ytm) && injective tm = unifyFail ytm tm

271+ | not (injective ytm) && injective tm = unifyTmpFail tm ytm

272 un' fn bnames (V i) (P _ x _)

273 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

274 un' fn bnames (P _ x _) (V i)

@@ -379,9 +379,10 @@ unify ctxt env topx topy dont holes =

379 unArgs vs xs ys

380

381 metavarApp tm = let (f, args) = unApply tm in

382− metavar f &&

382+ (metavar f &&

383− all (\x -> metavarApp x) args

383+ all (\x -> metavarApp x) args

384− && nub args == args

384+ && nub args == args) ||

385+ globmetavar tm

385 metavarArgs tm = let (f, args) = unApply tm in

386 metavarArgs tm = let (f, args) = unApply tm in

386 all (\x -> metavar x || inenv x) args

387 all (\x -> metavar x || inenv x) args

387 && nub args == args

388 && nub args == args

@@ -413,14 +414,22 @@ unify ctxt env topx topy dont holes =

413

414

414 rigid (P (DCon _ _) _ _) = True

415 rigid (P (DCon _ _) _ _) = True

415 rigid (P (TCon _ _) _ _) = True

416 rigid (P (TCon _ _) _ _) = True

416− rigid t@(P Ref _ _) = inenv t

417+ rigid t@(P Ref _ _) = inenv t || globmetavar t

417 rigid (Constant _) = True

418 rigid (Constant _) = True

418 rigid (App f a) = rigid f && rigid a

419 rigid (App f a) = rigid f && rigid a

419− rigid t = not (metavar t)

420+ rigid t = not (metavar t) || globmetavar t

421+

422+ globmetavar t = case unApply t of

423+ (P _ x _, _) ->

424+ case lookupDef x ctxt of

425+ [TyDecl _ _] -> True

426+ _ -> False

427+ _ -> False

420

428

421 metavar t = case t of

429 metavar t = case t of

422− P _ x _ -> (x `elem` holes || holeIn env x) &&

430+ P _ x _ -> ((x `elem` holes || holeIn env x) &&

423− not (x `elem` dont)

431+ not (x `elem` dont))

432+ || globmetavar t

424 _ -> False

433 _ -> False

425 pat t = case t of

434 pat t = case t of

426 P _ x _ -> x `elem` holes || patIn env x

435 P _ x _ -> x `elem` holes || patIn env x

src/Idris/ElabDecls.hs+41−13

@@ -49,9 +49,18 @@ recheckC fc env t

49 addConstraints fc cs

50 return (tm, ty)

51

52+

53+checkDef fc ns = checkAddDef False True fc ns

54+

55+checkAddDef add toplvl fc [] = return []

56+checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

52−checkDef fc ns = do ctxt <- getContext

57+ = do ctxt <- getContext

58+ (t', _) <- recheckC fc [] t

59+ when add $ addDeferred [(n, (i, top, t, toplvl))]

60+ ns' <- checkAddDef add toplvl fc ns

61+ return ((n, (i, top, t')) : ns')

53− mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

62+-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

54− return (n, (i, top, t'))) ns

63+-- return (n, (i, top, t'))) ns

55

64

56-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

65-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

57elabType :: ElabInfo -> SyntaxInfo -> String ->

66elabType :: ElabInfo -> SyntaxInfo -> String ->

@@ -76,9 +85,12 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

76 ((tyT, defer, is), log) <-

85 ((tyT, defer, is), log) <-

77 tclift $ elaborate ctxt n (TType (UVal 0)) []

86 tclift $ elaborate ctxt n (TType (UVal 0)) []

78 (errAt "type of " n (erun fc (build i info False [] n ty)))

87 (errAt "type of " n (erun fc (build i info False [] n ty)))

79− ds <- checkDef fc defer

88+ ds <- checkAddDef True False fc defer

89+ -- if the type is not complete, note that we'll need to infer

90+ -- things later (for solving metavariables)

91+ when (not (null ds)) $ addTyInferred n

80− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

92+-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

81− addDeferred ds'

93+-- addDeferred ds'

82 mapM_ (elabCaseBlock info opts) is

94 mapM_ (elabCaseBlock info opts) is

83 ctxt <- getContext

95 ctxt <- getContext

84 logLvl 5 $ "Rechecking"

96 logLvl 5 $ "Rechecking"

@@ -1262,6 +1274,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1262 -- Build the LHS as an "Infer", and pull out its type and

1274 -- Build the LHS as an "Infer", and pull out its type and

1263 -- pattern bindings

1275 -- pattern bindings

1264 i <- getIState

1276 i <- getIState

1277+ inf <- isTyInferred fname

1265 -- get the parameters first, to pass through to any where block

1278 -- get the parameters first, to pass through to any where block

1266 let fn_ty = case lookupTy fname (tt_ctxt i) of

1279 let fn_ty = case lookupTy fname (tt_ctxt i) of

1267 [t] -> t

1280 [t] -> t

@@ -1275,16 +1288,25 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1275 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1288 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1276 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

1289 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

1277

1290

1278− ((lhs', dlhs, []), _) <-

1291+ (((lhs', dlhs, []), probs), _) <-

1279 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1292 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1280− (errAt "left hand side of " fname

1293+ (do res <- errAt "left hand side of " fname

1281− (erun fc (buildTC i info True opts fname (infTerm lhs))))

1294+ (erun fc (buildTC i info True opts fname (infTerm lhs)))

1295+ probs <- get_probs

1296+ return (res, probs))

1297+

1298+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)

1299+

1282 let lhs_tm = orderPats (getInferTerm lhs')

1300 let lhs_tm = orderPats (getInferTerm lhs')

1283 let lhs_ty = getInferType lhs'

1301 let lhs_ty = getInferType lhs'

1284 logLvl 3 ("Elaborated: " ++ show lhs_tm)

1302 logLvl 3 ("Elaborated: " ++ show lhs_tm)

1285 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

1303 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

1286

1304

1305+ -- If we're inferring metavariables in the type, don't recheck,

1306+ -- because we're only doing this to try to work out those metavariables

1307+ (clhs_c, clhsty) <- if not inf

1287− (clhs_c, clhsty) <- recheckC fc [] lhs_tm

1308+ then recheckC fc [] lhs_tm

1309+ else return (lhs_tm, lhs_ty)

1288 let clhs = normalise ctxt [] clhs_c

1310 let clhs = normalise ctxt [] clhs_c

1289

1311

1290 logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

1312 logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

@@ -1319,7 +1341,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1319 logLvl 2 $ "RHS: " ++ showTmImpls rhs

1341 logLvl 2 $ "RHS: " ++ showTmImpls rhs

1320 ctxt <- getContext -- new context with where block added

1342 ctxt <- getContext -- new context with where block added

1321 logLvl 5 "STARTING CHECK"

1343 logLvl 5 "STARTING CHECK"

1322− ((rhs', defer, is), _) <-

1344+ ((rhs', defer, is, probs), _) <-

1323 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

1345 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

1324 (do pbinds lhs_tm

1346 (do pbinds lhs_tm

1325 setNextName

1347 setNextName

@@ -1332,7 +1354,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1332 mapM_ (elabCaseHole aux) hs

1354 mapM_ (elabCaseHole aux) hs

1333 tt <- get_term

1355 tt <- get_term

1334 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

1356 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

1357+ probs <- get_probs

1335− return (tm, ds, is))

1358+ return (tm, ds, is, probs))

1359+

1360+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)

1361+

1336 logLvl 5 "DONE CHECK"

1362 logLvl 5 "DONE CHECK"

1337 logLvl 2 $ "---> " ++ show rhs'

1363 logLvl 2 $ "---> " ++ show rhs'

1338 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show (map fst defer)

1364 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show (map fst defer)

@@ -1352,7 +1378,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1352 ctxt <- getContext

1378 ctxt <- getContext

1353 logLvl 5 $ "Rechecking"

1379 logLvl 5 $ "Rechecking"

1354 logLvl 6 $ " ==> " ++ show (forget rhs')

1380 logLvl 6 $ " ==> " ++ show (forget rhs')

1381+ (crhs, crhsty) <- if not inf

1355− (crhs, crhsty) <- recheckC fc [] rhs'

1382+ then recheckC fc [] rhs'

1383+ else return (rhs', clhsty)

1356 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

1384 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

1357 case converts ctxt [] clhsty crhsty of

1385 case converts ctxt [] clhsty crhsty of

1358 OK _ -> return ()

1386 OK _ -> return ()

src/Idris/ElabTerm.hs+15−3

@@ -11,6 +11,7 @@ import Idris.ProofSearch

11import Idris.Core.Elaborate hiding (Tactic(..))

12import Idris.Core.TT

13import Idris.Core.Evaluate

14+import Idris.Core.Unify

14import Idris.Core.Typecheck (check)

15import Idris.Core.Typecheck (check)

15

16

16import Control.Applicative ((<$>))

17import Control.Applicative ((<$>))

@@ -46,6 +47,10 @@ build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

46 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

47 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

47build ist info pattern opts fn tm

48build ist info pattern opts fn tm

48 = do elab ist info pattern opts fn tm

49 = do elab ist info pattern opts fn tm

50+ let tmIn = tm

51+ let inf = case lookupCtxt fn (idris_tyinfodata ist) of

52+ [TIPartial] -> True

53+ _ -> False

49 ivs <- get_instances

54 ivs <- get_instances

50 hs <- get_holes

55 hs <- get_holes

51 ptm <- get_term

56 ptm <- get_term

@@ -70,7 +75,8 @@ build ist info pattern opts fn tm

70 probs <- get_probs

75 probs <- get_probs

71 case probs of

76 case probs of

72 [] -> return ()

77 [] -> return ()

78+ ((_,_,_,e):es) -> if inf then return ()

73− ((_,_,_,e):es) -> lift (Error e)

79+ else lift (Error e)

74 is <- getAux

80 is <- getAux

75 tt <- get_term

81 tt <- get_term

76 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

82 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

@@ -87,13 +93,18 @@ buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

87buildTC ist info pattern opts fn tm

93buildTC ist info pattern opts fn tm

88 = do -- set name supply to begin after highest index in tm

94 = do -- set name supply to begin after highest index in tm

89 let ns = allNamesIn tm

95 let ns = allNamesIn tm

96+ let tmIn = tm

97+ let inf = case lookupCtxt fn (idris_tyinfodata ist) of

98+ [TIPartial] -> True

99+ _ -> False

90 initNextNameFrom ns

100 initNextNameFrom ns

91 elab ist info pattern opts fn tm

101 elab ist info pattern opts fn tm

92 probs <- get_probs

102 probs <- get_probs

93 tm <- get_term

103 tm <- get_term

94 case probs of

104 case probs of

95 [] -> return ()

105 [] -> return ()

106+ ((_,_,_,e):es) -> if inf then return ()

96− ((_,_,_,e):es) -> lift (Error e)

107+ else lift (Error e)

97 is <- getAux

108 is <- getAux

98 tt <- get_term

109 tt <- get_term

99 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

110 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

@@ -841,7 +852,8 @@ collectDeferred :: Maybe Name ->

841 Term -> State [(Name, (Int, Maybe Name, Type))] Term

852 Term -> State [(Name, (Int, Maybe Name, Type))] Term

842collectDeferred top (Bind n (GHole i t) app) =

853collectDeferred top (Bind n (GHole i t) app) =

843 do ds <- get

854 do ds <- get

855+ t' <- collectDeferred top t

844− when (not (n `elem` map fst ds)) $ put ((n, (i, top, t)) : ds)

856+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])

845 collectDeferred top app

857 collectDeferred top app

846collectDeferred top (Bind n b t) = do b' <- cdb b

858collectDeferred top (Bind n b t) = do b' <- cdb b

847 t' <- collectDeferred top t

859 t' <- collectDeferred top t

src/Idris/ParseOps.hs+1−1

@@ -39,7 +39,7 @@ table fixes

39 [[backtick],

40 [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],

41 [binary "=" PEq AssocLeft],

42− [binary "->" (\fc x y -> PPi expl (sMN 42 "__pi_arg") x y) AssocRight]]

42+ [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]

43

44-- | Calculates table for fixtiy declarations

45toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

src/Idris/ProofSearch.hs+14−1

@@ -1,3 +1,5 @@

1+{-# LANGUAGE PatternGuards #-}

2+

1module Idris.ProofSearch(trivial, proofSearch) where

3module Idris.ProofSearch(trivial, proofSearch) where

2

4

3import Idris.Core.Elaborate hiding (Tactic(..))

5import Idris.Core.Elaborate hiding (Tactic(..))

@@ -36,10 +38,21 @@ trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

36

38

37proofSearch :: (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

39proofSearch :: (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

38 IState -> ElabD ()

40 IState -> ElabD ()

39−proofSearch elab fn nroot hints ist = psRec maxDepth

41+proofSearch elab fn nroot hints ist

42+ = case lookupCtxt nroot (idris_tyinfodata ist) of

43+ [TISolution ts] -> findInferredTy ts

44+ _ -> psRec maxDepth

40 where

45 where

41 maxDepth = 6

46 maxDepth = 6

42

47

48+ findInferredTy (t : _) = elab (delab ist (toUN t))

49+

50+ toUN t@(P nt (MN i n) ty)

51+ | ('_':xs) <- str n = t

52+ | otherwise = P nt (UN n) ty

53+ toUN (App f a) = App (toUN f) (toUN a)

54+ toUN t = t

55+

43 psRec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"

56 psRec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"

44 psRec d = try' (trivial elab ist)

57 psRec d = try' (trivial elab ist)

45 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

58 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

src/Idris/REPL.hs+5−3

@@ -8,6 +8,7 @@ import Idris.REPLParser

8import Idris.ElabDecls

9import Idris.ElabTerm

10import Idris.Error

11+import Idris.ErrReverse

11import Idris.Delaborate

12import Idris.Delaborate

12import Idris.Prover

13import Idris.Prover

13import Idris.Parser

14import Idris.Parser

@@ -486,7 +487,7 @@ process h fn (Check (PRef _ n))

486 where

487 where

487 showMetavarInfo imp ist n i

488 showMetavarInfo imp ist n i

488 = case lookupTy n (tt_ctxt ist) of

489 = case lookupTy n (tt_ctxt ist) of

489− (ty:_) -> putTy imp ist i [] (delab ist ty)

490+ (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))

490 putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

491 putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

491 putTy imp ist 0 bnd sc = putGoal imp ist bnd sc

492 putTy imp ist 0 bnd sc = putGoal imp ist bnd sc

492 putTy imp ist i bnd (PPi _ n t sc)

493 putTy imp ist i bnd (PPi _ n t sc)

@@ -894,8 +895,9 @@ process h fn (Missing n)

894 _ -> iPrintError $ "Ambiguous name"

895 _ -> iPrintError $ "Ambiguous name"

895process h fn (DynamicLink l)

896process h fn (DynamicLink l)

896 = do i <- getIState

897 = do i <- getIState

898+ let importdirs = opt_importdirs (idris_options i)

897− let lib = trim l

899+ lib = trim l

898− handle <- lift . lift $ tryLoadLib lib

900+ handle <- lift . lift $ tryLoadLib importdirs lib

899 case handle of

901 case handle of

900 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""

902 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""

901 Just x -> do let libs = idris_dynamic_libs i

903 Just x -> do let libs = idris_dynamic_libs i

src/Util/DynamicLinker.hs+38−18

@@ -1,7 +1,7 @@

1-- | Platform-specific dynamic linking support. Add new platforms to this file

2-- through conditional compilation.

3{-# LANGUAGE ExistentialQuantification, CPP #-}

4−module Util.DynamicLinker where

4+module Util.DynamicLinker (ForeignFun(..), DynamicLib(..), tryLoadLib, tryLoadFn) where

5

6#ifdef IDRIS_FFI

7import Foreign.LibFFI

@@ -9,11 +9,13 @@ import Foreign.Ptr (Ptr(), nullPtr, FunPtr, nullFunPtr, castPtrToFunPtr)

9import System.Directory

10#ifndef WINDOWS

11import System.Posix.DynamicLinker

12+import System.FilePath.Posix ((</>))

12#else

13#else

13import qualified Control.Exception as Exception (catch, IOException)

14import qualified Control.Exception as Exception (catch, IOException)

14import System.Win32.DLL

15import System.Win32.DLL

15import System.Win32.Types

16import System.Win32.Types

16type DL = HMODULE

17type DL = HMODULE

18+import System.FilePath.Windows ((</>))

17#endif

19#endif

18

20

19hostDynamicLibExt :: String

21hostDynamicLibExt :: String

@@ -45,14 +47,27 @@ data DynamicLib = Lib { lib_name :: String

45instance Eq DynamicLib where

47instance Eq DynamicLib where

46 (Lib a _) == (Lib b _) = a == b

48 (Lib a _) == (Lib b _) = a == b

47

49

50+firstExisting :: [FilePath] -> IO (Maybe FilePath)

51+firstExisting [] = return Nothing

52+firstExisting (f:fs) = do exists <- doesFileExist f

53+ if exists

54+ then return (Just f)

55+ else firstExisting fs

56+

57+libFileName :: [FilePath] -> String -> IO String

58+libFileName dirs lib = do let names = [lib, lib ++ "." ++ hostDynamicLibExt]

59+ cwd <- getCurrentDirectory

60+ found <- firstExisting $

61+ map ("."</>) names ++ [d </> f | d <- cwd:dirs, f <- names]

62+ return $ maybe (lib ++ "." ++ hostDynamicLibExt) id found

63+

48#ifndef WINDOWS

64#ifndef WINDOWS

49−tryLoadLib :: String -> IO (Maybe DynamicLib)

65+tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)

50−tryLoadLib lib = do exactName <- doesFileExist lib

66+tryLoadLib dirs lib = do filename <- libFileName dirs lib

51− let filename = if exactName then lib else lib ++ "." ++ hostDynamicLibExt

52− handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]

67+ handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]

53− if undl handle == nullPtr

68+ if undl handle == nullPtr

54− then return Nothing

69+ then return Nothing

55− else return . Just $ Lib lib handle

70+ else return . Just $ Lib lib handle

56

71

57

72

58tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)

73tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)

@@ -61,13 +76,12 @@ tryLoadFn fn (Lib _ h) = do cFn <- dlsym h fn

61 then return Nothing

76 then return Nothing

62 else return . Just $ Fun fn cFn

77 else return . Just $ Fun fn cFn

63#else

78#else

64−tryLoadLib :: String -> IO (Maybe DynamicLib)

79+tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)

65−tryLoadLib lib = do exactName <- doesFileExist lib

80+tryLoadLib dirs lib = do filename <- libFileName dirs lib

66− let filename = if exactName then lib else lib ++ "." ++ hostDynamicLibExt

67− handle <- Exception.catch (loadLibrary filename) nullPtrOnException

81+ handle <- Exception.catch (loadLibrary filename) nullPtrOnException

68− if handle == nullPtr

82+ if handle == nullPtr

69− then return Nothing

83+ then return Nothing

70− else return . Just $ Lib lib handle

84+ else return . Just $ Lib lib handle

71 where nullPtrOnException :: Exception.IOException -> IO DL

85 where nullPtrOnException :: Exception.IOException -> IO DL

72 nullPtrOnException e = return nullPtr

86 nullPtrOnException e = return nullPtr

73 -- `show e` will however give broken error message

87 -- `show e` will however give broken error message

@@ -86,11 +100,17 @@ data DynamicLib = Lib { lib_name :: String

86 }

100 }

87 deriving Eq

101 deriving Eq

88

102

89−tryLoadLib :: String -> IO (Maybe DynamicLib)

103+data ForeignFun = forall a. Fun { fun_name :: String

90−tryLoadLib lib = do putStrLn $ "WARNING: Cannot load '" ++ lib ++ "' at compile time because Idris was compiled without libffi support."

104+ , fun_handle :: ()

91− return Nothing

105+ }

92

106

107+tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)

108+tryLoadLib fps lib = do putStrLn $ "WARNING: Cannot load '" ++ lib ++ "' at compile time because Idris was compiled without libffi support."

109+ return Nothing

93

110

111+tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)

112+tryLoadFn fn lib = do putStrLn $ "WARNING: Cannot load '" ++ fn ++ "' at compile time because Idris was compiled without libffi support."

113+ return Nothing

94#endif

114#endif

95

115

96

116

test/dsl002/run+1−1

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

1#!/usr/bin/env bash

2idris $@ test014.idr -o test014

3./test014

4−rm -f test014 resimp.ibc test014.ibc

4+rm -f test014 Resimp.ibc test014.ibc

test/interactive002/expectednew file+11

@@ -0,0 +1,11 @@

1+Type checking ./interactive002.idr

2+Nat

3+Nat

4+Nat

5+Nat

6+Vect (n + m) a

7+Nat

8+Nat

9+S n

10+String

11+()

test/interactive002/inputnew file+11

@@ -0,0 +1,11 @@

1+:ps 2 foo_arg1

2+:ps 2 foo_arg2

3+:ps 2 foo_arg3

4+:ps 2 foo_ret

5+:ps 6 bar_out

6+:ps 9 plus_in1

7+:ps 9 plus_out

8+:ps 13 what

9+:ps 16 ifoo_arg1

10+:ps 16 ifoo_out

11+

test/interactive002/interactive002.idrnew file+20

@@ -0,0 +1,20 @@

1+

2+foo : ?foo_arg1 -> ?foo_arg2 -> ?foo_arg3 -> ?foo_ret

3+foo (S a) b c = plus (a + b + c) 42

4+foo Z b c = plus b c

5+

6+bar : Vect n a -> Vect m a -> ?bar_out

7+bar xs ys = xs ++ ys

8+

9+myplus : ?plus_in1 -> ?plus_in2 -> ?plus_out

10+myplus Z y = y

11+myplus (S k) y = S (myplus k y)

12+

13+vfun : a -> Vect n a -> Vect n a -> Vect ?what a

14+vfun v xs ys = v :: ys

15+

16+ifoo : ?ifoo_arg1 -> IO ?ifoo_out

17+ifoo x = do putStrLn x

18+ putStrLn "World"

19+

20+

test/interactive002/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --quiet interactive002.idr < input

3+rm -f *.ibc

test/proof003/run+1−1

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

1#!/usr/bin/env bash

2idris $@ test015.idr -o test015

3./test015

4−rm -f test015 parity.ibc test015.ibc

4+rm -f test015 Parity.ibc test015.ibc