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

git.iko.soy/Idris-dev

on master help sign in

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

822142aDavid Christiansen11 years ago

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

compare with master

unifiedsplit

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

13import Prelude.List

14import Prelude.Maybe

15import Prelude.Monad

16+import Prelude.Nat

16import Language.Reflection

17import Language.Reflection

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

20+

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

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

19||| erased.

22||| erased.

20data Erasure = Erased | NotErased

23data Erasure = Erased | NotErased

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

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

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

132 prim__PatVar : TTName -> Elab ()

135 prim__PatVar : TTName -> Elab ()

133 prim__PatBind : TTName -> Elab ()

136 prim__PatBind : TTName -> Elab ()

134− -- TODO: letbind

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

135

138

136 prim__Compute : Elab ()

139 prim__Compute : Elab ()

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

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

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

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

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

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

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

147

150

151+ prim__Fixity : String -> Elab Fixity

152+

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

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

149 prim__Metavar : TTName -> Elab ()

154 prim__Metavar : TTName -> Elab ()

150

155

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

247 fill tm = prim__Fill tm

252 fill tm = prim__Fill tm

248

253

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

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

250− ||| potentially solving arugments by unification.

255+ ||| potentially solving arguments by unification.

251 |||

256 |||

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

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

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

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

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

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

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

322 ||| `attack`).

327 ||| `attack`).

323 |||

328 |||

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

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

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

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.

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

335+ intro' : Elab ()

327− intro n = prim__Intro n

336+ intro' = prim__Intro Nothing

328

337

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

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

330 ||| and focus on the body.

339 ||| and focus on the body.

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

339 patbind : TTName -> Elab ()

348 patbind : TTName -> Elab ()

340 patbind n = prim__PatBind n

349 patbind n = prim__PatBind n

341

350

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+

342 ||| Normalise the goal.

359 ||| Normalise the goal.

343 compute : Elab ()

360 compute : Elab ()

344 compute = prim__Compute

361 compute = prim__Compute

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

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

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

419 search' depth hints = prim__Search depth hints

436 search' depth hints = prim__Search depth hints

420

437

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+

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

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

422 |||

448 |||

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

449 ||| 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' =

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

628 _ -> hnf ctxt env t

629 case t' of

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

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.

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

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

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

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

633 _ -> lift $ tfail $ CantIntroduce t'

636 _ -> lift $ tfail $ CantIntroduce t'

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

637intro 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

1909 = do n' <- reifyTTName n

1910 patbind n'

1911 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

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

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

1913 = do compute ; returnUnit

1919 = do compute ; returnUnit

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

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

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

2009 defer unique_used mvn

2015 defer unique_used mvn

2010 solve

2016 solve

2011 returnUnit

2017 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

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

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

2013 = do msg' <- eval msg

2033 = do msg' <- eval msg

2014 parts <- reifyReportParts msg

2034 parts <- reifyReportParts msg

src/Idris/Prover.hs+17−14

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

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

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

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

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

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

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

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

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

150 let OK ty = goalAtFocus ps

151 let OK env = envAtFocus ps

152 let state = prettyOtherGoals hs <> line <>

153− prettyAssumptions env <> line <>

153+ prettyAssumptions ty env <> line <>

154 prettyMetaValues (reverse menv) <>

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

156 rendered <- iRender state

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

168 assumptionNames :: Env -> [Name]

169 assumptionNames = map fst

170

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

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

172− prettyPs bnd [] = empty

172+ prettyPs g bnd [] = empty

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

181 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

183

184 prettyMetaValues [] = empty

185 prettyMetaValues mvs =

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

196

197 kwd = annotate AnnKeyword . text

198

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

200+ goalNames b = freeNames (binderTy b)

201+

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

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

200 prettyG bnd b = tPretty bnd $ binderTy b

203 prettyG bnd b = tPretty bnd $ binderTy b

201

204

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

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

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

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

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

205

208

206− prettyAssumptions env =

209+ prettyAssumptions g env =

207 if length env == 0 then

210 if length env == 0 then

208 empty

211 empty

209 else

212 else

210 text "---------- Assumptions: ----------" <>

213 text "---------- Assumptions: ----------" <>

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

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

212

215

213 prettyOtherGoals hs =

216 prettyOtherGoals hs =

214 if length hs == 0 then

217 if length hs == 0 then

src/Idris/Reflection.hs+14−1

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

17import Idris.Core.TT

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

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

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

21 initEState, pairCon, pairTy)

22import Idris.Delaborate (delab)

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

398 claim n' ty

399 return n'

400

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+

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

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

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

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

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

416-- 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

24intros : Elab ()

25intros = do g <- getGoal

26 case snd g of

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

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

28 _ => return ()

30foo : Nat -> Nat

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

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

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

33 solve)