ff742fe · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Actually track applications in the elaborator wrt unification fails

ff742feDavid Raymond Christiansen13 years ago

src/Idris/Core/Elaborate.hs+14

compare with master

unifiedsplit

@@ -131,14 +131,17 @@ force_term :: Elab' aux ()

131force_term = do ES (ps, a) l p <- get

132 put (ES (ps { pterm = force (pterm ps) }, a) l p)

133

134+-- | Modify the auxiliary state

134updateAux :: (aux -> aux) -> Elab' aux ()

135updateAux :: (aux -> aux) -> Elab' aux ()

135updateAux f = do ES (ps, a) l p <- get

136updateAux f = do ES (ps, a) l p <- get

136 put (ES (ps, f a) l p)

137 put (ES (ps, f a) l p)

137

138

139+-- | Get the auxiliary state

138getAux :: Elab' aux aux

140getAux :: Elab' aux aux

139getAux = do ES (ps, a) _ _ <- get

141getAux = do ES (ps, a) _ _ <- get

140 return $! a

142 return $! a

141

143

144+-- | Set whether to show the unifier log

142unifyLog :: Bool -> Elab' aux ()

145unifyLog :: Bool -> Elab' aux ()

143unifyLog log = do ES (ps, a) l p <- get

146unifyLog log = do ES (ps, a) l p <- get

144 put (ES (ps { unifylog = log }, a) l p)

147 put (ES (ps { unifylog = log }, a) l p)

@@ -154,6 +157,17 @@ processTactic' t = do ES (p, a) logs prev <- get

154 put (ES (p', a) (logs ++ log) prev)

157 put (ES (p', a) (logs ++ log) prev)

155 return $! ()

158 return $! ()

156

159

160+updatePS :: (ProofState -> ProofState) -> Elab' aux ()

161+updatePS f = do ES (ps, a) logs prev <- get

162+ put $ ES (f ps, a) logs prev

163+

164+now_elaborating :: FC -> Name -> Name -> Elab' aux ()

165+now_elaborating fc f a = updatePS (nowElaboratingPS fc f a)

166+done_elaborating_app :: Name -> Elab' aux ()

167+done_elaborating_app f = updatePS (doneElaboratingAppPS f)

168+done_elaborating_arg :: Name -> Name -> Elab' aux ()

169+done_elaborating_arg f a = updatePS (doneElaboratingArgPS f a)

170+

157-- Some handy gadgets for pulling out bits of state

171-- Some handy gadgets for pulling out bits of state

158

172

159-- get the global context

173-- get the global context

src/Idris/Core/ProofState.hs+19−16

@@ -5,8 +5,8 @@

5 evaluation/checking inside the proof system, etc. --}

7module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

8− Tactic(..), Goal(..), processTactic, now_elaborating, done_elaborating,

8+ Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,

9− dropGiven, keepGiven) where

9+ doneElaboratingArgPS, dropGiven, keepGiven) where

11import Idris.Core.Typecheck

12import Idris.Core.Evaluate

@@ -224,20 +224,23 @@ unify' ctxt env topx topy =

224 updateInj (_ : us) inj = updateInj us inj

225 updateInj [] inj = inj

226

227−now_elaborating :: Monad m => FC -> Name -> Name -> StateT TState m ()

227+nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState

228−now_elaborating fc f arg = do ps <- get

229− put ps {

230− while_elaborating = FailContext fc f arg : while_elaborating ps

228+nowElaboratingPS fc f arg ps = ps { while_elaborating = FailContext fc f arg : while_elaborating ps }

231− }

229+

232−

230+dropUntil :: (a -> Bool) -> [a] -> [a]

233−done_elaborating :: Monad m => Name -> Name -> StateT TState m ()

234−done_elaborating f x = do ps <- get

235− let while = while_elaborating ps

236− let while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while

237− put ps { while_elaborating = while' }

238− where dropUntil p [] = []

231+dropUntil p [] = []

239− dropUntil p (x:xs) | p x = xs

232+dropUntil p (x:xs) | p x = xs

240− | otherwise = dropUntil p xs

233+ | otherwise = dropUntil p xs

234+

235+doneElaboratingAppPS :: Name -> ProofState -> ProofState

236+doneElaboratingAppPS f ps = let while = while_elaborating ps

237+ while' = dropUntil (\ (FailContext _ f' _) -> f == f') while

238+ in ps { while_elaborating = while' }

239+

240+doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState

241+doneElaboratingArgPS f x ps = let while = while_elaborating ps

242+ while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while

243+ in ps { while_elaborating = while' }

241

244

242getName :: Monad m => String -> StateT TState m Name

245getName :: Monad m => String -> StateT TState m Name

243getName tag = do ps <- get

246getName tag = do ps <- get

src/Idris/Core/TT.hs+1

@@ -140,6 +140,7 @@ data Err' t

140 | NoRewriting t

141 | At FC (Err' t)

142 | Elaborating String Name (Err' t)

143+ | ElaboratingArg Name Name (Err' t)

143 | ProviderError String

144 | ProviderError String

144 | LoadingFailed String (Err' t)

145 | LoadingFailed String (Err' t)

145 | ReflectionError [[ErrorReportPart]] (Err' t)

146 | ReflectionError [[ErrorReportPart]] (Err' t)

src/Idris/ElabTerm.hs+11−11

@@ -158,20 +158,20 @@ elab ist info pattern opts fn tm

158

159 elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()

160 elabE ina t =

161−-- do g <- goal

161+ --do g <- goal

162−-- trace ("Elaborating " ++ show t ++ " : " ++ show g) $

162+ --trace ("Elaborating " ++ show t ++ " : " ++ show g) $

163 do ct <- insertCoerce ina t

164 t' <- insertLazy ct

165 g <- goal

166 tm <- get_term

167 ps <- get_probs

168 hs <- get_holes

169−-- trace ("Elaborating " ++ show t' ++ " in " ++ show g

169+ --trace ("Elaborating " ++ show t' ++ " in " ++ show g

170−-- -- ++ "\n" ++ show tm

170+ -- ++ "\n" ++ show tm

171−-- ++ "\nholes " ++ show hs

171+ -- ++ "\nholes " ++ show hs

172−-- ++ "\nproblems " ++ show ps

172+ -- ++ "\nproblems " ++ show ps

173−-- ++ "\n-----------\n") $

173+ -- ++ "\n-----------\n") $

174−-- trace ("ELAB " ++ show t') $

174+ --trace ("ELAB " ++ show t') $

175 let fc = fileFC "Force"

176 handleError forceErr

177 (elab' ina t')

@@ -694,7 +694,6 @@ elab ist info pattern opts fn tm

694 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

695 mkDelay t = let fc = fileFC "Delay" in

696 addImpl ist (PApp fc (PRef fc (sUN "Delay")) [pexp t])

697−

698

697

699 insertCoerce ina t =

698 insertCoerce ina t =

700 do ty <- goal

699 do ty <- goal

@@ -737,8 +736,8 @@ elab ist info pattern opts fn tm

737 pexp t])

736 pexp t])

738 | otherwise = elabArg argName holeName t

737 | otherwise = elabArg argName holeName t

739 where elabArg argName holeName t =

738 where elabArg argName holeName t =

740− reflectFunctionErrors ist f argName $

739+ do now_elaborating fc f argName

741− do hs <- get_holes

740+ hs <- get_holes

742 tm <- get_term

741 tm <- get_term

743 -- No coercing under an explicit Force (or it can Force/Delay

742 -- No coercing under an explicit Force (or it can Force/Delay

744 -- recursively!)

743 -- recursively!)

@@ -748,6 +747,7 @@ elab ist info pattern opts fn tm

748 case holeName `elem` hs of

747 case holeName `elem` hs of

749 True -> do focus holeName; elab ina t; return failed

748 True -> do focus holeName; elab ina t; return failed

750 False -> return failed

749 False -> return failed

750+ done_elaborating_arg f argName

751 elabArgs ist ina failed fc r f ns force args

752

753-- | Perform error reflection for function applicaitons with specific error handlers