git.iko.soy/Idris-dev
on master help sign in
Heuristic for generating better metavar types
289c05fEdwin Brady
src/Idris/Elab/Clause.hs+1−1
compare with master
unifiedsplit
@@ -670,7 +670,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
670 aux <- getAux
670 aux <- getAux
671 mapM_ (elabCaseHole (case_decls aux)) hs
671 mapM_ (elabCaseHole (case_decls aux)) hs
672 tt <- get_term
672 tt <- get_term
673− let (tm, ds) = runState (collectDeferred (Just fname) tt) []
673+ let (tm, ds) = runState (collectDeferred (Just fname) ctxt tt) []
674 probs <- get_probs
674 probs <- get_probs
675 return (tm, ds, is, probs, ctxt', newDecls))
675 return (tm, ds, is, probs, ctxt', newDecls))
676 setContext ctxt'
676 setContext ctxt'
src/Idris/Elab/Term.hs+34−17
@@ -129,9 +129,9 @@ build ist info emode opts fn tm
129 update_term orderPats)
129 update_term orderPats)
130 EState is _ impls <- getAux
130 EState is _ impls <- getAux
131 tt <- get_term
131 tt <- get_term
132− let (tm, ds) = runState (collectDeferred (Just fn) tt) []
133− log <- getLog
134 ctxt <- get_context
132 ctxt <- get_context
133+ let (tm, ds) = runState (collectDeferred (Just fn) ctxt tt) []
134+ log <- getLog
135 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
135 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
136 else return (ElabResult tm ds is ctxt impls)
136 else return (ElabResult tm ds is ctxt impls)
137 where pattern = emode == ELHS
137 where pattern = emode == ELHS
@@ -171,9 +171,9 @@ buildTC ist info emode opts fn tm
171 lift (Error (CantMatch (getInferTerm tm)))
171 lift (Error (CantMatch (getInferTerm tm)))
172 EState is _ impls <- getAux
172 EState is _ impls <- getAux
173 tt <- get_term
173 tt <- get_term
174− let (tm, ds) = runState (collectDeferred (Just fn) tt) []
175− log <- getLog
176 ctxt <- get_context
174 ctxt <- get_context
175+ let (tm, ds) = runState (collectDeferred (Just fn) ctxt tt) []
176+ log <- getLog
177 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
177 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
178 else return (ElabResult tm ds is ctxt impls)
178 else return (ElabResult tm ds is ctxt impls)
179 where pattern = emode == ELHS
179 where pattern = emode == ELHS
@@ -1563,23 +1563,40 @@ resTC' tcs defaultOn topholes depth topg fn ist
1563 where isImp (PImp p _ _ _ _) = (True, p)
1563 where isImp (PImp p _ _ _ _) = (True, p)
1564 isImp arg = (False, priority arg)
1564 isImp arg = (False, priority arg)
1565
1565
1566−collectDeferred :: Maybe Name ->
1566+collectDeferred :: Maybe Name -> Context ->
1567 Term -> State [(Name, (Int, Maybe Name, Type))] Term
1567 Term -> State [(Name, (Int, Maybe Name, Type))] Term
1568−collectDeferred top (Bind n (GHole i t) app) =
1568+collectDeferred top ctxt (Bind n (GHole i t) app) =
1569 do ds <- get
1569 do ds <- get
1570− t' <- collectDeferred top t
1570+ t' <- collectDeferred top ctxt t
1571− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])
1571+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))])
1572− collectDeferred top app
1572+ collectDeferred top ctxt app
1573+ where
1574+ -- Evaluate the top level functions in arguments, if possible, so that
1575+ -- any immediate specialisation of the function applied to constructors
1576+ -- can be done
1577+ tidyArg env (Bind n b@(Pi im t k) sc)
1578+ = Bind n (Pi im (tidy ctxt env t) k)
1579+ (tidyArg ((n, b) : env) sc)
1580+ tidyArg env t = t
1581+
1582+ tidy ctxt env t | (f, args) <- unApply t,
1583+ P _ n _ <- getFn f
1584+ = fst $ specialise ctxt env [(n, 99999)] t
1585+ tidy ctxt env t = t
1586+
1587+ getFn (Bind n (Lam _) t) = getFn t
1588+ getFn t | (f, a) <- unApply t = f
1589+
1573−collectDeferred top (Bind n b t) = do b' <- cdb b
1590+collectDeferred top ctxt (Bind n b t) = do b' <- cdb b
1574− t' <- collectDeferred top t
1591+ t' <- collectDeferred top ctxt t
1575− return (Bind n b' t')
1592+ return (Bind n b' t')
1576 where
1593 where
1577− cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)
1594+ cdb (Let t v) = liftM2 Let (collectDeferred top ctxt t) (collectDeferred top ctxt v)
1578− cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)
1595+ cdb (Guess t v) = liftM2 Guess (collectDeferred top ctxt t) (collectDeferred top ctxt v)
1579− cdb b = do ty' <- collectDeferred top (binderTy b)
1596+ cdb b = do ty' <- collectDeferred top ctxt (binderTy b)
1580 return (b { binderTy = ty' })
1597 return (b { binderTy = ty' })
1581−collectDeferred top (App s f a) = liftM2 (App s) (collectDeferred top f) (collectDeferred top a)
1598+collectDeferred top ctxt (App s f a) = liftM2 (App s) (collectDeferred top ctxt f) (collectDeferred top ctxt a)
1582−collectDeferred top t = return t
1599+collectDeferred top ctxt t = return t
1583
1600
1584case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
1601case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
1585case_ ind autoSolve ist fn tm = do
1602case_ ind autoSolve ist fn tm = do
src/Idris/Elab/Transform.hs+1−1
@@ -75,7 +75,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
75 (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)
75 (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)
76 erun fc $ psolve lhs_tm
76 erun fc $ psolve lhs_tm
77 tt <- get_term
77 tt <- get_term
78− let (rhs', defer) = runState (collectDeferred Nothing tt) []
78+ let (rhs', defer) = runState (collectDeferred Nothing ctxt tt) []
79 return (rhs', defer, ctxt', newDecls))
79 return (rhs', defer, ctxt', newDecls))
80 setContext ctxt'
80 setContext ctxt'
81 processTacticDecls newDecls
81 processTacticDecls newDecls