8858c1a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Basic handling of elaborator debugger invocations

8858c1aDavid Raymond Christiansen12 years ago

libs/prelude/Language/Reflection/Tactical.idr+8

compare with master

unifiedsplit

@@ -39,6 +39,8 @@ data Tactical : Type -> Type where

39 prim__Claim : TTName -> Raw -> Tactical ()

40 prim__Intro : Maybe TTName -> Tactical ()

42+ prim__Debug : {a : Type} -> Maybe String -> Tactical a

43+

42-------------

44-------------

43-- Public API

45-- Public API

44-------------

46-------------

@@ -114,3 +116,9 @@ sourceLocation = do loc <- getSourceLocation

114

116

115rewriteWith : Raw -> Tactical ()

117rewriteWith : Raw -> Tactical ()

116rewriteWith rule = prim__Rewrite rule

118rewriteWith 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

778 recoverableErr (ProofSearchFail _) = False

779 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

780 recoverableErr (At _ e) = recoverableErr e

781+ recoverableErr (ElabDebug _ _ _) = False

781 recoverableErr _ = True

782 recoverableErr _ = True

782

783

783tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

784tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

src/Idris/Delaborate.hs+10−2

@@ -1,4 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

2module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr) where

3module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr) where

4-- Convert core TT back into high level syntax, primarily for display

5-- Convert core TT back into high level syntax, primarily for display

@@ -32,6 +33,7 @@ delabTy i n

32 (ty:_) -> case lookupCtxt n (idris_implicits i) of

33 (ty:_) -> case lookupCtxt n (idris_implicits i) of

33 (imps:_) -> delabTy' i imps ty False False

34 (imps:_) -> delabTy' i imps ty False False

34 _ -> delabTy' i [] ty False False

35 _ -> delabTy' i [] ty False False

36+ [] -> error "delabTy: got non-existing name"

36delab' :: IState -> Term -> Bool -> Bool -> PTerm

38delab' :: IState -> Term -> Bool -> Bool -> PTerm

37delab' i t f mvs = delabTy' i [] t f mvs

39delab' i t f mvs = delabTy' i [] t f mvs

@@ -86,6 +88,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

86 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

88 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

87 de env plic (Bind n bb sc) = de ((n,n):env) [] sc

89 de env plic (Bind n bb sc) = de ((n,n):env) [] sc

88 de env _ (Constant i) = PConstant i

90 de env _ (Constant i) = PConstant i

91+ de env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"

89 de env _ Erased = Placeholder

92 de env _ Erased = Placeholder

90 de env _ Impossible = Placeholder

93 de env _ Impossible = Placeholder

91 de env _ (TType i) = PType

94 de env _ (TType i) = PType

@@ -183,6 +186,7 @@ pprintDelabTy i n

183 case lookupCtxt n (idris_implicits i) of

186 case lookupCtxt n (idris_implicits i) of

184 (imps:_) -> delabTy' i imps ty False False

187 (imps:_) -> delabTy' i imps ty False False

185 _ -> delabTy' i [] ty False False

188 _ -> delabTy' i [] ty False False

189+ [] -> error "pprintDelabTy got a name that doesn't exist"

186

190

187pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

191pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

188pprintTerm ist = pprintTerm' ist []

192pprintTerm ist = pprintTerm' ist []

@@ -335,10 +339,14 @@ pprintErr' i (ReflectionFailed msg err) =

335 text "When attempting to perform error reflection, the following internal error occurred:" <>

339 text "When attempting to perform error reflection, the following internal error occurred:" <>

336 indented (pprintErr' i err) <>

340 indented (pprintErr' i err) <>

337 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

341 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"

338

347

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

340-- that any names which differ internally also differ visibly

349-- that any names which differ internally also differ visibly

341−

342renameMNs :: Term -> Term -> (Term, Term, [Name])

350renameMNs :: Term -> Term -> (Term, Term, [Name])

343renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

351renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

344 newnames = evalState (getRenames [] ns) 1 in

352 newnames = evalState (getRenames [] ns) 1 in

src/Idris/ElabTerm.hs+6

@@ -1596,6 +1596,12 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1596 Just name -> fmap Just $ reifyTTName name

1597 intro n

1598 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

1599 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x

1605 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x

1600

1606

1601-- Running tactics directly

1607-- Running tactics directly