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

git.iko.soy/Idris-dev

on master help sign in

Look up operator fixity in Elab

766b73aDavid Raymond Christiansen11 years ago

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

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

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

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

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

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

419 search' depth hints = prim__Search depth hints

424 search' depth hints = prim__Search depth hints

420

425

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+

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

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

422 |||

436 |||

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

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

2182 defer unique_used mvn

2183 solve

2184 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

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

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

2186 = do msg' <- eval msg

2200 = do msg' <- eval msg

2187 parts <- reifyReportParts msg

2201 parts <- reifyReportParts msg

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,