git.iko.soy/Idris-dev
on master help sign in
Basic handling of elaborator debugger invocations
commit8858c1a9a3994b587a822ce06d94ffed98365ed8 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 10 Mar 2015, 02:46 (12 years ago) parent02d0078
4 files changed+25−2
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Tactical.idr+8 src/Idris/Core/Elaborate.hs+1 src/Idris/Delaborate.hs+10−2 src/Idris/ElabTerm.hs+6
libs/prelude/Language/Reflection/Tactical.idr+8
@@ -39,6 +39,8 @@ data Tactical : Type -> Type where
3939 prim__Claim : TTName -> Raw -> Tactical ()
4040 prim__Intro : Maybe TTName -> Tactical ()
4141
42+ prim__Debug : {a : Type} -> Maybe String -> Tactical a
43+
4244-------------
4345-- Public API
4446-------------
@@ -114,3 +116,9 @@ sourceLocation = do loc <- getSourceLocation
114116
115117rewriteWith : Raw -> Tactical ()
116118rewriteWith rule = prim__Rewrite rule
119+
120+debug : Tactical a
121+debug = prim__Debug Nothing
122+
123+debugMessage : String -> Tactical a
124+debugMessage msg = prim__Debug (Just msg)
src/Idris/Core/Elaborate.hs+1
@@ -778,6 +778,7 @@ try' t1 t2 proofSearch
778778 recoverableErr (ProofSearchFail _) = False
779779 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e
780780 recoverableErr (At _ e) = recoverableErr e
781+ recoverableErr (ElabDebug _ _ _) = False
781782 recoverableErr _ = True
782783
783784tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
src/Idris/Delaborate.hs+10−2
@@ -1,4 +1,5 @@
11{-# LANGUAGE PatternGuards #-}
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
23module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr) where
34
45-- Convert core TT back into high level syntax, primarily for display
@@ -32,6 +33,7 @@ delabTy i n
3233 (ty:_) -> case lookupCtxt n (idris_implicits i) of
3334 (imps:_) -> delabTy' i imps ty False False
3435 _ -> delabTy' i [] ty False False
36+ [] -> error "delabTy: got non-existing name"
3537
3638delab' :: IState -> Term -> Bool -> Bool -> PTerm
3739delab' i t f mvs = delabTy' i [] t f mvs
@@ -86,6 +88,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
8688 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc
8789 de env plic (Bind n bb sc) = de ((n,n):env) [] sc
8890 de env _ (Constant i) = PConstant i
91+ de env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"
8992 de env _ Erased = Placeholder
9093 de env _ Impossible = Placeholder
9194 de env _ (TType i) = PType
@@ -183,6 +186,7 @@ pprintDelabTy i n
183186 case lookupCtxt n (idris_implicits i) of
184187 (imps:_) -> delabTy' i imps ty False False
185188 _ -> delabTy' i [] ty False False
189+ [] -> error "pprintDelabTy got a name that doesn't exist"
186190
187191pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
188192pprintTerm ist = pprintTerm' ist []
@@ -335,10 +339,14 @@ pprintErr' i (ReflectionFailed msg err) =
335339 text "When attempting to perform error reflection, the following internal error occurred:" <>
336340 indented (pprintErr' i err) <>
337341 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
342+pprintErr' i (ElabDebug mstr tm holes) =
343+ text "Elaboration halted." <>
344+ maybe empty (indented . text) mstr <>
345+ text "Term: TODO PRINT TERM" <>
346+ text "Holes: TODO PRINT AND PRESERVE"
338347
339−-- Make sure the machine invented names are shown helpfully to the user, so
348+-- | Make sure the machine invented names are shown helpfully to the user, so
340349-- that any names which differ internally also differ visibly
341−
342350renameMNs :: Term -> Term -> (Term, Term, [Name])
343351renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y
344352 newnames = evalState (getRenames [] ns) 1 in
src/Idris/ElabTerm.hs+6
@@ -1596,6 +1596,12 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15961596 Just name -> fmap Just $ reifyTTName name
15971597 intro n
15981598 returnUnit
1599+ | n == tacN "prim__Debug", [ty, msg] <- args
1600+ = do let msg' = fromTTMaybe msg
1601+ case msg' of
1602+ Nothing -> debugElaborator Nothing
1603+ Just (Constant (Str m)) -> debugElaborator (Just m)
1604+ Just x -> lift . tfail . InternalMsg $ "Can't reify message for debugging: " ++ show x
15991605 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
16001606
16011607-- Running tactics directly