766b73a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Look up operator fixity in Elab

This is necessary for deriving good Show instances on infix operators.

commit766b73a0a5c4fdef81cf5bd4a2fa3e360a1a506f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 21 Aug 2015, 17:52 (11 years ago) parentab63941

3 files changed+42−1

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Elab.idr+14 src/Idris/Elab/Term.hs+14 src/Idris/Reflection.hs+14−1

libs/prelude/Language/Reflection/Elab.idr+14

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

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

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

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

419424 search' depth hints = prim__Search depth hints

420425

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

427+ |||

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

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

430+ |||

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

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

433+ operatorFixity operator = prim__Fixity operator

434+

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

422436 |||

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

src/Idris/Elab/Term.hs+14

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

21822182 defer unique_used mvn

21832183 solve

21842184 returnUnit

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

2186+ = do opTm <- eval op'

2187+ case opTm of

2188+ Constant (Str op) ->

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

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

2191+ fixities = idris_infixes ist

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

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

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

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

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

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

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

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

21862200 = do msg' <- eval msg

21872201 parts <- reifyReportParts msg

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,