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

CHANGELOG+6

@@ -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+

17New in 0.9.11:

28--------------

39

idris.cabal+5−1

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

11Name: idris

2−Version: 0.9.11.1

2+Version: 0.9.11.2

33License: BSD3

44License-file: LICENSE

55Author: Edwin Brady

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

294294 test/interactive001/input

295295 test/interactive001/*.idr

296296 test/interactive001/expected

297+ test/interactive002/run

298+ test/interactive002/input

299+ test/interactive002/*.idr

300+ test/interactive002/expected

297301

298302 test/io001/run

299303 test/io001/*.idr

libs/base/Control/Isomorphism.idr−1

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

11module Control.Isomorphism

22

33import Syntax.PreorderReasoning

4−import Uninhabited

54

65%default total

76

libs/base/base.ipkg−2

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

1010

1111 Decidable.Decidable, Decidable.Order,

1212

13− Uninhabited,

14−

1513 Providers,

1614

1715 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,

libs/prelude/Prelude.idr+1

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

2020import Prelude.Traversable

2121import Prelude.Bits

2222import Prelude.Stream

23+import Prelude.Uninhabited

2324

2425import Decidable.Equality

2526

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

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

1−module Uninhabited

1+module Prelude.Uninhabited

22

33class Uninhabited t where

44 total uninhabited : t -> _|_

libs/prelude/prelude.ipkg+2−1

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

11package prelude

22

33opts = "--nobuiltins --total"

4−modules = Builtins, Prelude, IO,

4+modules = Builtins, Prelude, IO,

55

66 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

77 Prelude.Classes, Prelude.Nat, Prelude.Fin, Prelude.List,

88 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

99 Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Functor,

1010 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11+ Prelude.Uninhabited,

1112

1213 Decidable.Equality

1314

src/IRTS/CodegenJavaScript.hs+176−5

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

409409

410410isJSConstant :: JS -> Bool

411411isJSConstant js

412− | JSString _ <- js = True

413− | JSChar _ <- js = True

414− | JSNum _ <- js = True

415− | JSType _ <- js = True

416− | JSNull <- js = True

412+ | JSString _ <- js = True

413+ | JSChar _ <- js = True

414+ | JSNum _ <- js = True

415+ | JSType _ <- js = True

416+ | JSNull <- js = True

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

417418

418419 | 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

419436 | otherwise = False

420437

421438

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

10001017 | otherwise = js

10011018

10021019

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+

10031172codegenJavaScript

10041173 :: JSTarget

10051174 -> [(Name, SDecl)]

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

10561225 , map removeInstanceChecks

10571226 , inlineFunctions

10581227 , map reduceContinuations

1228+ , extractLocalConstructors

10591229 , unfoldLookupTable

1230+ , evalCons

10601231 ]

10611232

10621233 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

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

6767addDyLib libs = do i <- getIState

6868 let ls = idris_dynamic_libs i

69+ let importdirs = opt_importdirs (idris_options i)

6970 case mapMaybe (findDyLib ls) libs of

7071 x:_ -> return (Left x)

7172 [] -> do

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

73+ handle <- lift . lift .

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

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

7376 case msum handle of

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

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

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

155158 = do i <- getIState

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

157160

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

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+

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

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

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

160233addFunctionErrorHandlers f arg hs =

161234 do i <- getIState

src/Idris/AbsSyntaxTree.hs+12−2

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

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

113113 idris_calledgraph :: Ctxt [Name],

114114 idris_docstrings :: Ctxt String,

115+ idris_tyinfodata :: Ctxt TIData,

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

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

117118 idris_options :: IOption,

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

216217idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

217218 emptyContext emptyContext emptyContext emptyContext

218219 emptyContext emptyContext emptyContext emptyContext

219− emptyContext

220+ emptyContext emptyContext

220221 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

221222 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

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

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

811812deriving instance NFData ClassInfo

812813!-}

813814

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+

814821-- An argument is conditionally forceable iff its forceability

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

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

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

952959getInferTerm (App (App _ _) tm) = tm

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

954961

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

956966getInferType (App (App _ ty) _) = ty

957967

958968

src/Idris/Core/Elaborate.hs−2

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

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

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

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

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

470− -- so do nothing

471469 hs <- get_holes

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

473471 let dont = head hs : dontunify p ++

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

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

257257 then unifyTmpFail xtm tm

258258 else do sc 1

259259 checkCycle bnames (x, tm)

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

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

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

262262 | holeIn env y || y `elem` holes

263263 = do UI s f <- get

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

268268 then unifyTmpFail tm ytm

269269 else do sc 1

270270 checkCycle bnames (y, tm)

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

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

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

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

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

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

379379 unArgs vs xs ys

380380

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

382− metavar f &&

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

384− && nub args == args

382+ (metavar f &&

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

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

385+ globmetavar tm

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

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

387388 && nub args == args

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

413414

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

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

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

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

417418 rigid (Constant _) = True

418419 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

420428

421429 metavar t = case t of

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

423− not (x `elem` dont)

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

431+ not (x `elem` dont))

432+ || globmetavar t

424433 _ -> False

425434 pat t = case t of

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

src/Idris/ElabDecls.hs+41−13

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

4949 addConstraints fc cs

5050 return (tm, ty)

5151

52−checkDef fc ns = do ctxt <- getContext

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

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

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)

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

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

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

5564

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

5766elabType :: ElabInfo -> SyntaxInfo -> String ->

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

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

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

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

79− ds <- checkDef fc defer

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

81− addDeferred ds'

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

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

93+-- addDeferred ds'

8294 mapM_ (elabCaseBlock info opts) is

8395 ctxt <- getContext

8496 logLvl 5 $ "Rechecking"

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

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

12631275 -- pattern bindings

12641276 i <- getIState

1277+ inf <- isTyInferred fname

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

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

12671280 [t] -> t

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

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

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

12771290

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

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

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

1280− (errAt "left hand side of " fname

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

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

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+

12821300 let lhs_tm = orderPats (getInferTerm lhs')

12831301 let lhs_ty = getInferType lhs'

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

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

12861304

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

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

1308+ then recheckC fc [] lhs_tm

1309+ else return (lhs_tm, lhs_ty)

12881310 let clhs = normalise ctxt [] clhs_c

12891311

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

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

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

13211343 logLvl 5 "STARTING CHECK"

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

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

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

13241346 (do pbinds lhs_tm

13251347 setNextName

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

13321354 mapM_ (elabCaseHole aux) hs

13331355 tt <- get_term

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

1335− return (tm, ds, is))

1357+ probs <- get_probs

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

1359+

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

1361+

13361362 logLvl 5 "DONE CHECK"

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

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

13521378 ctxt <- getContext

13531379 logLvl 5 $ "Rechecking"

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

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

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

1382+ then recheckC fc [] rhs'

1383+ else return (rhs', clhsty)

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

13571385 case converts ctxt [] clhsty crhsty of

13581386 OK _ -> return ()

src/Idris/ElabTerm.hs+15−3

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

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

1212import Idris.Core.TT

1313import Idris.Core.Evaluate

14+import Idris.Core.Unify

1415import Idris.Core.Typecheck (check)

1516

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

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

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

4748build ist info pattern opts fn tm

4849 = 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

4954 ivs <- get_instances

5055 hs <- get_holes

5156 ptm <- get_term

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

7075 probs <- get_probs

7176 case probs of

7277 [] -> return ()

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

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

79+ else lift (Error e)

7480 is <- getAux

7581 tt <- get_term

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

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

8793buildTC ist info pattern opts fn tm

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

8995 let ns = allNamesIn tm

96+ let tmIn = tm

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

98+ [TIPartial] -> True

99+ _ -> False

90100 initNextNameFrom ns

91101 elab ist info pattern opts fn tm

92102 probs <- get_probs

93103 tm <- get_term

94104 case probs of

95105 [] -> return ()

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

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

107+ else lift (Error e)

97108 is <- getAux

98109 tt <- get_term

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

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

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

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

843854 do ds <- get

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

855+ t' <- collectDeferred top t

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

845857 collectDeferred top app

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

847859 t' <- collectDeferred top t

src/Idris/ParseOps.hs+1−1

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

3939 [[backtick],

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

4141 [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]]

4343

4444-- | Calculates table for fixtiy declarations

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

src/Idris/ProofSearch.hs+14−1

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

1+{-# LANGUAGE PatternGuards #-}

2+

13module Idris.ProofSearch(trivial, proofSearch) where

24

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

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

3638

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

3840 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

4045 where

4146 maxDepth = 6

4247

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+

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

4457 psRec d = try' (trivial elab ist)

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

src/Idris/REPL.hs+5−3

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

88import Idris.ElabDecls

99import Idris.ElabTerm

1010import Idris.Error

11+import Idris.ErrReverse

1112import Idris.Delaborate

1213import Idris.Prover

1314import Idris.Parser

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

486487 where

487488 showMetavarInfo imp ist n i

488489 = 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))

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

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

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

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

894895 _ -> iPrintError $ "Ambiguous name"

895896process h fn (DynamicLink l)

896897 = do i <- getIState

897− let lib = trim l

898− handle <- lift . lift $ tryLoadLib lib

898+ let importdirs = opt_importdirs (idris_options i)

899+ lib = trim l

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

899901 case handle of

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

901903 Just x -> do let libs = idris_dynamic_libs i

src/Util/DynamicLinker.hs+38−18

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

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

22-- through conditional compilation.

33{-# LANGUAGE ExistentialQuantification, CPP #-}

4−module Util.DynamicLinker where

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

55

66#ifdef IDRIS_FFI

77import Foreign.LibFFI

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

99import System.Directory

1010#ifndef WINDOWS

1111import System.Posix.DynamicLinker

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

1213#else

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

1415import System.Win32.DLL

1516import System.Win32.Types

1617type DL = HMODULE

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

1719#endif

1820

1921hostDynamicLibExt :: String

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

4547instance Eq DynamicLib where

4648 (Lib a _) == (Lib b _) = a == b

4749

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+

4864#ifndef WINDOWS

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

50−tryLoadLib lib = do exactName <- doesFileExist lib

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

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

53− if undl handle == nullPtr

54− then return Nothing

55− else return . Just $ Lib lib handle

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

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

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

68+ if undl handle == nullPtr

69+ then return Nothing

70+ else return . Just $ Lib lib handle

5671

5772

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

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

6176 then return Nothing

6277 else return . Just $ Fun fn cFn

6378#else

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

65−tryLoadLib lib = do exactName <- doesFileExist lib

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

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

68− if handle == nullPtr

69− then return Nothing

70− else return . Just $ Lib lib handle

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

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

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

82+ if handle == nullPtr

83+ then return Nothing

84+ else return . Just $ Lib lib handle

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

7286 nullPtrOnException e = return nullPtr

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

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

86100 }

87101 deriving Eq

88102

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

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

91− return Nothing

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

104+ , fun_handle :: ()

105+ }

92106

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

93110

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

94114#endif

95115

96116

test/dsl002/run+1−1

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

11#!/usr/bin/env bash

22idris $@ test014.idr -o test014

33./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 @@

11#!/usr/bin/env bash

22idris $@ test015.idr -o test015

33./test015

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

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