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

git.iko.soy/Idris-dev

Record partial type inference info

Proof search now has access to this and can fill in some basic type information. Lots still to do though (especially dealing with type classes, properly spotting errors, and polymorphic type variables).

commit3848c07e2df54c12e4c6a36618bf172e8b549809 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 9 Feb 2014, 15:51 (13 years ago) parent6c4d0f1

6 files changed+109−21

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+47−1 src/Idris/AbsSyntaxTree.hs+5−2 src/Idris/Core/Unify.hs+2−2 src/Idris/ElabDecls.hs+32−13 src/Idris/ElabTerm.hs+13−2 src/Idris/ProofSearch.hs+10−1

src/Idris/AbsSyntax.hs+47−1

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

155155 = do i <- getIState

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

157157

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

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+

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

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

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

160206addFunctionErrorHandlers f arg hs =

161207 do i <- getIState

src/Idris/AbsSyntaxTree.hs+5−2

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

815815-- Type inference data

816816

817817data 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

819819 deriving Show

820820

821821-- An argument is conditionally forceable iff its forceability

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

959959getInferTerm (App (App _ _) tm) = tm

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

961961

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

963966getInferType (App (App _ ty) _) = ty

964967

965968

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

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

src/Idris/ElabDecls.hs+32−13

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

5050 return (tm, ty)

5151

5252

53−checkDef fc ns = checkAddDef False fc ns

53+checkDef fc ns = checkAddDef False True fc ns

5454

55−checkAddDef add fc [] = return []

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

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

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

5757 = do ctxt <- getContext

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

59− when add $ addDeferred [(n, (i, top, t, True))]

60− ns' <- checkAddDef add fc ns

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

60+ ns' <- checkAddDef add toplvl fc ns

6161 return ((n, (i, top, t')) : ns')

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

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

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

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

8787 (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

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

9093-- addDeferred ds'

9194 mapM_ (elabCaseBlock info opts) is

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

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

12721275 -- pattern bindings

12731276 i <- getIState

1277+ inf <- isTyInferred fname

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

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

12761280 [t] -> t

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

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

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

12861290

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

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

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

1289− (errAt "left hand side of " fname

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

1299+

12911300 let lhs_tm = orderPats (getInferTerm lhs')

12921301 let lhs_ty = getInferType lhs'

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

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

12951304

1296− (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)

12971310 let clhs = normalise ctxt [] clhs_c

12981311

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

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

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

13301343 logLvl 5 "STARTING CHECK"

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

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

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

13331346 (do pbinds lhs_tm

13341347 setNextName

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

13411354 mapM_ (elabCaseHole aux) hs

13421355 tt <- get_term

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

1344− return (tm, ds, is))

1357+ probs <- get_probs

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

1359+

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

1361+

13451362 logLvl 5 "DONE CHECK"

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

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

13611378 ctxt <- getContext

13621379 logLvl 5 $ "Rechecking"

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

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

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

1382+ then recheckC fc [] rhs'

1383+ else return (rhs', clhsty)

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

13661385 case converts ctxt [] clhsty crhsty of

13671386 OK _ -> return ()

src/Idris/ElabTerm.hs+13−2

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

src/Idris/ProofSearch.hs+10−1

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

3636

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

3838 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

4043 where

4144 maxDepth = 6

4245

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+

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

4453 psRec d = try' (trivial elab ist)

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