3848c07 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Record partial type inference info

3848c07Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+47−1

compare with master

unifiedsplit

@@ -155,7 +155,53 @@ addToCG n cg

155 = do i <- getIState

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

157

158+addTyInferred :: Name -> Idris ()

159+addTyInferred n

160+ = do i <- getIState

161+ putIState $ i { idris_tyinfodata =

162+ addDef n TIPartial (idris_tyinfodata i) }

163+

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

165+addTyInfConstraints ts = do -- iputStrLn (show ts)

166+ mapM_ (addConstraint True) ts

167+ return ()

168+ where addConstraint True (x, y) -- MV on the left

169+ | (P _ mv _, args) <- unApply x

170+ = do ist <- get

171+ case lookup mv (idris_metavars ist) of

172+ Just _ -> addConstraintRule mv y

173+ _ -> addConstraint False (x, y)

174+ addConstraint False (x, y)

175+ | (P _ mv _, args) <- unApply y

176+ = do ist <- get

177+ case lookup mv (idris_metavars ist) of

178+ Just _ -> addConstraintRule mv x

179+ _ -> return ()

180+ addConstraint _ _ = return () -- FIXME: report error?

181+

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

183+ addConstraintRule n t

184+ = do ist <- get

185+ logLvl 2 $ "TI constraint: " ++ show (n, t)

186+ case lookupCtxt n (idris_tyinfodata ist) of

187+ [TISolution ts] ->

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

189+ (idris_tyinfodata ist)

190+ put $ ist { idris_tyinfodata = ti' }

191+ _ ->

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

193+ (idris_tyinfodata ist)

194+ put $ ist { idris_tyinfodata = ti' }

195+

196+isTyInferred :: Name -> Idris Bool

197+isTyInferred n

198+ = do i <- getIState

199+ case lookupCtxt n (idris_tyinfodata i) of

200+ [TIPartial] -> return True

201+ _ -> return False

202+

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

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

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

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

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

160addFunctionErrorHandlers f arg hs =

206addFunctionErrorHandlers f arg hs =

161 do i <- getIState

207 do i <- getIState

src/Idris/AbsSyntaxTree.hs+5−2

@@ -815,7 +815,7 @@ deriving instance NFData ClassInfo

815-- Type inference data

816

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

818− | TISolution Term -- ^ solution to a metavariable in a type

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

819 deriving Show

820

821-- An argument is conditionally forceable iff its forceability

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

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

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

961

962−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

963getInferType (App (App _ ty) _) = ty

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

964

967

965

968

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

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

src/Idris/ElabDecls.hs+32−13

@@ -50,14 +50,14 @@ recheckC fc env t

50 return (tm, ty)

53−checkDef fc ns = checkAddDef False fc ns

53+checkDef fc ns = checkAddDef False True fc ns

55−checkAddDef add fc [] = return []

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

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

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, True))]

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

60− ns' <- checkAddDef add fc ns

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

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

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

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

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

88− ds <- checkAddDef True 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

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

90-- addDeferred ds'

93-- addDeferred ds'

91 mapM_ (elabCaseBlock info opts) is

94 mapM_ (elabCaseBlock info opts) is

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

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

1272 -- pattern bindings

1275 -- pattern bindings

1273 i <- getIState

1276 i <- getIState

1277+ inf <- isTyInferred fname

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

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

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

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

1276 [t] -> t

1280 [t] -> t

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

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

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

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

1286

1290

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

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

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

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

1289− (errAt "left hand side of " fname

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

1290− (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 (map (\(x,y,_,_) -> (x,y)) probs)

1299+

1291 let lhs_tm = orderPats (getInferTerm lhs')

1300 let lhs_tm = orderPats (getInferTerm lhs')

1292 let lhs_ty = getInferType lhs'

1301 let lhs_ty = getInferType lhs'

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

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

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

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

1295

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

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

1308+ then recheckC fc [] lhs_tm

1309+ else return (lhs_tm, lhs_ty)

1297 let clhs = normalise ctxt [] clhs_c

1310 let clhs = normalise ctxt [] clhs_c

1298

1311

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

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

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

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

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

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

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

1330 logLvl 5 "STARTING CHECK"

1343 logLvl 5 "STARTING CHECK"

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

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

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

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

1333 (do pbinds lhs_tm

1346 (do pbinds lhs_tm

1334 setNextName

1347 setNextName

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

1341 mapM_ (elabCaseHole aux) hs

1354 mapM_ (elabCaseHole aux) hs

1342 tt <- get_term

1355 tt <- get_term

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

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

1357+ probs <- get_probs

1344− return (tm, ds, is))

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

1359+

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

1361+

1345 logLvl 5 "DONE CHECK"

1362 logLvl 5 "DONE CHECK"

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

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

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

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

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

1361 ctxt <- getContext

1378 ctxt <- getContext

1362 logLvl 5 $ "Rechecking"

1379 logLvl 5 $ "Rechecking"

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

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

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

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

1382+ then recheckC fc [] rhs'

1383+ else return (rhs', clhsty)

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

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

1366 case converts ctxt [] clhsty crhsty of

1385 case converts ctxt [] clhsty crhsty of

1367 OK _ -> return ()

1386 OK _ -> return ()

src/Idris/ElabTerm.hs+13−2

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

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

src/Idris/ProofSearch.hs+10−1

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

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

38 IState -> ElabD ()

39−proofSearch elab fn nroot hints ist = psRec maxDepth

39+proofSearch elab fn nroot hints ist

40+ = case lookupCtxt nroot (idris_tyinfodata ist) of

41+ [TISolution ts] -> findInferredTy ts

42+ _ -> psRec maxDepth

40 where

43 where

41 maxDepth = 6

44 maxDepth = 6

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

47+

48+ toUN (P nt (MN i n) ty) = P nt (UN n) ty

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

50+ toUN t = t

51+

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

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

44 psRec d = try' (trivial elab ist)

53 psRec d = try' (trivial elab ist)

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

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