822142a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2548 from david-christiansen/wip/tactical

Latest Elab reflection updates in preparation for upcoming release

commit822142ab0ae27969d08bdaec5da9dbf8fea78859 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 26 Aug 2015, 09:10 (11 years ago) parent7b58024 a297e02

6 files changed+90−25

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Elab.idr+32−6 src/Idris/Core/ProofState.hs+5−2 src/Idris/Elab/Term.hs+20 src/Idris/Prover.hs+17−14 src/Idris/Reflection.hs+14−1 test/meta002/Tacs.idr+2−2

libs/prelude/Language/Reflection/Elab.idr+32−6

@@ -13,8 +13,11 @@ import Prelude.Functor

1313import Prelude.List

1414import Prelude.Maybe

1515import Prelude.Monad

16+import Prelude.Nat

1617import Language.Reflection

1718

19+data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat

20+

1821||| Erasure annotations reflect Idris's idea of what is intended to be

1922||| erased.

2023data Erasure = Erased | NotErased

@@ -131,7 +134,7 @@ data Elab : Type -> Type where

131134 prim__Forall : TTName -> Raw -> Elab ()

132135 prim__PatVar : TTName -> Elab ()

133136 prim__PatBind : TTName -> Elab ()

134− -- TODO: letbind

137+ prim__LetBind : TTName -> Raw -> Raw -> Elab ()

135138

136139 prim__Compute : Elab ()

137140 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT

@@ -145,6 +148,8 @@ data Elab : Type -> Type where

145148 prim__Search : Int -> List TTName -> Elab ()

146149 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

147150

151+ prim__Fixity : String -> Elab Fixity

152+

148153 prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a

149154 prim__Metavar : TTName -> Elab ()

150155

@@ -247,7 +252,7 @@ namespace Tactics

247252 fill tm = prim__Fill tm

248253

249254 ||| Attempt to apply an operator to fill the current hole,

250− ||| potentially solving arugments by unification.

255+ ||| potentially solving arguments by unification.

251256 |||

252257 ||| The return value is a list of pairs of names, one for each input

253258 ||| argument. The first projection of these pairs is the original

@@ -321,10 +326,14 @@ namespace Tactics

321326 ||| the body. Requires that the hole be in binding form (use

322327 ||| `attack`).

323328 |||

324− ||| @ n the name to use for the argument, or `Nothing` to use the name

325− ||| in the corresponding hole type (a dependent function)

326− intro : (n : Maybe TTName) -> Elab ()

327− intro n = prim__Intro n

329+ ||| @ n the name to use for the argument

330+ intro : (n : TTName) -> Elab ()

331+ intro n = prim__Intro (Just n)

332+

333+ ||| Introduce a lambda binding around the current hole and focus on

334+ ||| the body, using the name provided by the type of the hole.

335+ intro' : Elab ()

336+ intro' = prim__Intro Nothing

328337

329338 ||| Introduce a dependent function type binding into the current hole,

330339 ||| and focus on the body.

@@ -339,6 +348,14 @@ namespace Tactics

339348 patbind : TTName -> Elab ()

340349 patbind n = prim__PatBind n

341350

351+ ||| Introduce a new let binding

352+ |||

353+ ||| @ n the name to let bind

354+ ||| @ ty the type of the term to be let-bound

355+ ||| @ tm the term to be bound

356+ letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()

357+ letbind n ty tm = prim__LetBind n ty tm

358+

342359 ||| Normalise the goal.

343360 compute : Elab ()

344361 compute = prim__Compute

@@ -418,6 +435,15 @@ namespace Tactics

418435 search' : (depth : Int) -> (hints : List TTName) -> Elab ()

419436 search' depth hints = prim__Search depth hints

420437

438+ ||| Look up the declared fixity for an operator.

439+ |||

440+ ||| The lookup fails if the operator does not yet have a fixity or

441+ ||| if the string is not a valid operator.

442+ |||

443+ ||| @ operator the operator string to look up

444+ operatorFixity : (operator : String) -> Elab Fixity

445+ operatorFixity operator = prim__Fixity operator

446+

421447 ||| Halt elaboration, dumping the internal state for inspection.

422448 |||

423449 ||| This is intended for elaboration script developers, not for

src/Idris/Core/ProofState.hs+5−2

@@ -627,8 +627,11 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

627627 x@(Bind y (Pi _ s _) _) -> x

628628 _ -> hnf ctxt env t

629629 case t' of

630− Bind y (Pi _ s _) t -> -- trace ("in type " ++ show t') $

631− let t' = updsubst y (P Bound n s) t in

630+ Bind y (Pi _ s _) t ->

631+ -- It's important that this be subst and not updsubst,

632+ -- because we want to substitute even in portions of

633+ -- terms that we know do not contain holes.

634+ let t' = subst y (P Bound n s) t in

632635 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

633636 _ -> lift $ tfail $ CantIntroduce t'

634637intro n ctxt env _ = fail "Can't introduce here."

src/Idris/Elab/Term.hs+20

@@ -1909,6 +1909,12 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

19091909 = do n' <- reifyTTName n

19101910 patbind n'

19111911 returnUnit

1912+ | n == tacN "prim__LetBind", [n, ty, tm] <- args

1913+ = do n' <- reifyTTName n

1914+ ty' <- reifyRaw ty

1915+ tm' <- reifyRaw tm

1916+ letbind n' ty' tm'

1917+ returnUnit

19121918 | n == tacN "prim__Compute", [] <- args

19131919 = do compute ; returnUnit

19141920 | n == tacN "prim__Normalise", [env, tm] <- args

@@ -2009,6 +2015,20 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

20092015 defer unique_used mvn

20102016 solve

20112017 returnUnit

2018+ | n == tacN "prim__Fixity", [op'] <- args

2019+ = do opTm <- eval op'

2020+ case opTm of

2021+ Constant (Str op) ->

2022+ let opChars = ":!#$%&*+./<=>?@\\^|-~"

2023+ invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]

2024+ fixities = idris_infixes ist

2025+ in if not (all (flip elem opChars) op) || elem op invalidOperators

2026+ then lift . tfail . Msg $ "'" ++ op ++ "' is not a valid operator name."

2027+ else case nub [f | Fix f someOp <- fixities, someOp == op] of

2028+ [] -> lift . tfail . Msg $ "No fixity found for operator '" ++ op ++ "'."

2029+ [f] -> fmap fst . checkClosed $ reflectFixity f

2030+ many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many

2031+ _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm

20122032 | n == tacN "prim__Debug", [ty, msg] <- args

20132033 = do msg' <- eval msg

20142034 parts <- reifyReportParts msg

src/Idris/Prover.hs+17−14

@@ -5,7 +5,7 @@ module Idris.Prover (prover, showProof, showRunElab) where

55-- This exludes (<$>) as fmap, because wl-pprint uses it for newline

66import Prelude (Eq(..), Show(..),

77 Bool(..), Either(..), Maybe(..), String,

8− (.), ($), (++),

8+ (.), ($), (++), (||),

99 concatMap, id, elem, error, fst, flip, foldl, foldr, init,

1010 length, lines, map, not, null, repeat, reverse, tail, zip)

1111

@@ -150,7 +150,7 @@ dumpState ist menv ps | (h : hs) <- holes ps = do

150150 let OK ty = goalAtFocus ps

151151 let OK env = envAtFocus ps

152152 let state = prettyOtherGoals hs <> line <>

153− prettyAssumptions env <> line <>

153+ prettyAssumptions ty env <> line <>

154154 prettyMetaValues (reverse menv) <>

155155 prettyGoal (zip (assumptionNames env) (repeat False)) ty

156156 rendered <- iRender state

@@ -168,18 +168,18 @@ dumpState ist menv ps | (h : hs) <- holes ps = do

168168 assumptionNames :: Env -> [Name]

169169 assumptionNames = map fst

170170

171− prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation

172− prettyPs bnd [] = empty

173− prettyPs bnd ((n@(MN _ r), _) : bs)

174− | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs

175− prettyPs bnd ((n@(MN _ _), _) : bs)

176− | not (n `elem` freeEnvNames bs) = prettyPs bnd bs

177− prettyPs bnd ((n, Let t v) : bs) =

171+ prettyPs :: Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation

172+ prettyPs g bnd [] = empty

173+ prettyPs g bnd ((n@(MN _ r), _) : bs)

174+ | r == txt "rewrite_rule" = prettyPs g ((n, False):bnd) bs

175+ prettyPs g bnd ((n@(MN _ _), _) : bs)

176+ | not (n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs g bnd bs

177+ prettyPs g bnd ((n, Let t v) : bs) =

178178 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

179− align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs

180− prettyPs bnd ((n, b) : bs) =

179+ align (tPretty bnd t) <> prettyPs g ((n, False):bnd) bs

180+ prettyPs g bnd ((n, b) : bs) =

181181 line <> bindingOf n False <+> colon <+>

182− align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs

182+ align (tPretty bnd (binderTy b)) <> prettyPs g ((n, False):bnd) bs

183183

184184 prettyMetaValues [] = empty

185185 prettyMetaValues mvs =

@@ -196,6 +196,9 @@ dumpState ist menv ps | (h : hs) <- holes ps = do

196196

197197 kwd = annotate AnnKeyword . text

198198

199+ goalNames (Guess t v) = freeNames t ++ freeNames v

200+ goalNames b = freeNames (binderTy b)

201+

199202 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

200203 prettyG bnd b = tPretty bnd $ binderTy b

201204

@@ -203,12 +206,12 @@ dumpState ist menv ps | (h : hs) <- holes ps = do

203206 text "---------- Goal: ----------" <$$>

204207 bindingOf h False <+> colon <+> align (prettyG bnd ty)

205208

206− prettyAssumptions env =

209+ prettyAssumptions g env =

207210 if length env == 0 then

208211 empty

209212 else

210213 text "---------- Assumptions: ----------" <>

211− nest nestingSize (prettyPs [] $ reverse env)

214+ nest nestingSize (prettyPs g [] $ reverse env)

212215

213216 prettyOtherGoals hs =

214217 if length hs == 0 then

src/Idris/Reflection.hs+14−1

@@ -17,7 +17,7 @@ import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyEx

1717import Idris.Core.TT

1818

1919import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes),

20− PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..),

20+ PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..), Fixity (..),

2121 initEState, pairCon, pairTy)

2222import Idris.Delaborate (delab)

2323

@@ -398,6 +398,19 @@ claimTy n ty = do n' <- getNameFrom n

398398 claim n' ty

399399 return n'

400400

401+intToReflectedNat :: Int -> Raw

402+intToReflectedNat i = if i <= 0

403+ then Var (natN "Z")

404+ else RApp (Var (natN "S")) (intToReflectedNat (i - 1))

405+ where natN :: String -> Name

406+ natN n = sNS (sUN n) ["Nat", "Prelude"]

407+

408+reflectFixity :: Fixity -> Raw

409+reflectFixity (Infixl p) = RApp (Var (tacN "Infixl")) (intToReflectedNat p)

410+reflectFixity (Infixr p) = RApp (Var (tacN "Infixr")) (intToReflectedNat p)

411+reflectFixity (InfixN p) = RApp (Var (tacN "InfixN")) (intToReflectedNat p)

412+reflectFixity (PrefixN p) = RApp (Var (tacN "PrefixN")) (intToReflectedNat p)

413+

401414-- | Convert a reflected term to a more suitable form for pattern-matching.

402415-- In particular, the less-interesting bits are elaborated to _ patterns. This

403416-- happens to NameTypes, universe levels, names that are bound but not used,

test/meta002/Tacs.idr+2−2

@@ -24,11 +24,11 @@ import Language.Reflection.Utils

2424intros : Elab ()

2525intros = do g <- getGoal

2626 case snd g of

27− `(~_ -> ~_) => intro Nothing

27+ `(~_ -> ~_) => intro'

2828 _ => return ()

2929

3030foo : Nat -> Nat

31−foo = %runElab (do intro (Just (UN "fnord"))

31+foo = %runElab (do intro (UN "fnord")

3232 fill `(plus ~(Var (UN "fnord")) ~(Var (UN "fnord")))

3333 solve)

3434