ff742fe · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Actually track applications in the elaborator wrt unification fails

commitff742fe429accde22108df76a96e4020593aba69 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 20 Mar 2014, 12:47 (13 years ago) parentb38bc03

4 files changed+45−27

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+14 src/Idris/Core/ProofState.hs+19−16 src/Idris/Core/TT.hs+1 src/Idris/ElabTerm.hs+11−11

src/Idris/Core/Elaborate.hs+14

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

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

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

133133

134+-- | Modify the auxiliary state

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

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

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

137138

139+-- | Get the auxiliary state

138140getAux :: Elab' aux aux

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

140142 return $! a

141143

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

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

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

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

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

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

155158 return $! ()

156159

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+

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

158172

159173-- get the global context

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

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

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

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

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

9− dropGiven, keepGiven) where

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

9+ doneElaboratingArgPS, dropGiven, keepGiven) where

1010

1111import Idris.Core.Typecheck

1212import Idris.Core.Evaluate

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

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

225225 updateInj [] inj = inj

226226

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

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

229− put ps {

230− while_elaborating = FailContext fc f arg : while_elaborating ps

231− }

232−

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

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

240− | otherwise = dropUntil p xs

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

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

229+

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

231+dropUntil p [] = []

232+dropUntil p (x:xs) | p x = 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' }

241244

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

243246getName tag = do ps <- get

src/Idris/Core/TT.hs+1

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

140140 | NoRewriting t

141141 | At FC (Err' t)

142142 | Elaborating String Name (Err' t)

143+ | ElaboratingArg Name Name (Err' t)

143144 | ProviderError String

144145 | LoadingFailed String (Err' t)

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

src/Idris/ElabTerm.hs+11−11

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

158158

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

160160 elabE ina t =

161−-- do g <- goal

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

161+ --do g <- goal

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

163163 do ct <- insertCoerce ina t

164164 t' <- insertLazy ct

165165 g <- goal

166166 tm <- get_term

167167 ps <- get_probs

168168 hs <- get_holes

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

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

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

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

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

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

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

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

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

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

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

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

175175 let fc = fileFC "Force"

176176 handleError forceErr

177177 (elab' ina t')

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

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

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

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

697−

698697

699698 insertCoerce ina t =

700699 do ty <- goal

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

737736 pexp t])

738737 | otherwise = elabArg argName holeName t

739738 where elabArg argName holeName t =

740− reflectFunctionErrors ist f argName $

741− do hs <- get_holes

739+ do now_elaborating fc f argName

740+ hs <- get_holes

742741 tm <- get_term

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

744743 -- recursively!)

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

748747 case holeName `elem` hs of

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

750749 False -> return failed

750+ done_elaborating_arg f argName

751751 elabArgs ist ina failed fc r f ns force args

752752

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