c1fabb1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Implement LookupFunDefn

c1fabb1Shea Levy11 years ago

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

compare with master

unifiedsplit

@@ -115,6 +115,7 @@ data Elab : Type -> Type where

115 Prim__Guess : Elab TT

116 Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))

117 Prim__LookupDatatype : TTName -> Elab (List Datatype)

118+ Prim__LookupFunDefn : TTName -> Elab (List FunDefn)

118 Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

119 Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

119

120

120 Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)

121 Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)

@@ -230,6 +231,19 @@ namespace Tactics

230 [] => fail [TextPart "No datatype named", NamePart n]

231 [] => fail [TextPart "No datatype named", NamePart n]

231 xs => fail [TextPart "More than one datatype named", NamePart n]

232 xs => fail [TextPart "More than one datatype named", NamePart n]

232

233

234+ ||| Find the reflected function definition of all functions whose names

235+ ||| are overloadings of some name.

236+ lookupFunDefn : TTName -> Elab (List FunDefn)

237+ lookupFunDefn n = Prim__LookupFunDefn n

238+

239+ ||| Find the reflected function definition of a function, given its

240+ ||| fully-qualified name. Fail if the name does not uniquely resolve

241+ ||| to a function.

242+ lookupFunDefnExact : TTName -> Elab FunDefn

243+ lookupFunDefnExact n = case !(lookupFunDefn n) of

244+ [res] => return res

245+ [] => fail [TextPart "No function named", NamePart n]

246+ xs => fail [TextPart "More than one function named", NamePart n]

233

247

234 ||| Get the argument specification for each overloading of a name.

248 ||| Get the argument specification for each overloading of a name.

235 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

249 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

src/Idris/Core/TT.hs+1

@@ -1107,6 +1107,7 @@ instantiate e = subst 0 where

1107 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

1108 subst i (App s f a) = App s (subst i f) (subst i a)

1109 subst i (Proj x idx) = Proj (subst i x) idx

1110+ -- If ever adding a clause here, please update mkFunClause in Idris/Reflection.hs

1110 subst i t = t

1111 subst i t = t

1111

1112

1112-- | As 'instantiate', but also decrement the indices of all de Bruijn variables

1113-- | As 'instantiate', but also decrement the indices of all de Bruijn variables

src/Idris/Elab/Term.hs+5

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

1862 fmap fst . checkClosed $

1863 rawList (Var (tacN "Datatype"))

1864 (map reflectDatatype (buildDatatypes ist n'))

1865+ | n == tacN "Prim__LookupFunDefn", [name] <- args

1866+ = do n' <- reifyTTName name

1867+ fmap fst . checkClosed $

1868+ rawList (Var (tacN "FunDefn"))

1869+ (map reflectFunDefn (buildFunDefns ist n'))

1865 | n == tacN "Prim__LookupArgs", [name] <- args

1870 | n == tacN "Prim__LookupArgs", [name] <- args

1866 = do n' <- reifyTTName name

1871 = do n' <- reifyTTName name

1867 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])

1872 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])

src/Idris/Reflection.hs+45−2

@@ -7,9 +7,11 @@ module Idris.Reflection where

8#if __GLASGOW_HASKELL__ < 710

9import Control.Applicative ((<$>), (<*>), pure)

10+import Prelude hiding (mapM)

11+import Data.Traversable (mapM)

10#endif

12#endif

11import Control.Monad (liftM, liftM2, liftM4)

13import Control.Monad (liftM, liftM2, liftM4)

12−import Control.Monad.State.Strict (lift)

14+import Control.Monad.State.Strict (lift, State, runState, put)

13import Data.Maybe (catMaybes)

15import Data.Maybe (catMaybes)

14import Data.List ((\\), findIndex)

16import Data.List ((\\), findIndex)

15import qualified Data.Text as T

17import qualified Data.Text as T

@@ -19,7 +21,7 @@ import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,

19import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)

21import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)

20import Idris.Core.TT

22import Idris.Core.TT

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

24+import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes, idris_patdefs),

23 PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..), Fixity (..),

25 PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..), Fixity (..),

24 initEState, pairCon, pairTy)

26 initEState, pairCon, pairTy)

25import Idris.Delaborate (delab)

27import Idris.Delaborate (delab)

@@ -1074,6 +1076,40 @@ unApplyRaw tm = ua [] tm

1074 ua args (RApp f a) = ua (a:args) f

1076 ua args (RApp f a) = ua (a:args) f

1075 ua args t = (t, args)

1077 ua args t = (t, args)

1076

1078

1079+-- | Build the reflected function definition(s) that correspond(s) to

1080+-- a provided unqualifed name

1081+buildFunDefns :: IState -> Name -> [RFunDefn]

1082+buildFunDefns ist n =

1083+ [ mkFunDefn name clauses

1084+ | (name, (clauses, _)) <- lookupCtxtName n $ idris_patdefs ist

1085+ ]

1086+ where mkFunDefn name clauses = RDefineFun name (map (mkFunClause name) clauses)

1087+

1088+ mkFunClause :: Name -> ([Name], Term, Term) -> RFunClause

1089+ mkFunClause _ ([], lhs, Impossible) = RMkImpossibleClause (forget lhs)

1090+ mkFunClause _ ([], lhs, rhs) = RMkFunClause (forget lhs) (forget rhs)

1091+ mkFunClause name ((n : ns), lhs, rhs) = mkFunClause name (ns, lhs', rhs') where

1092+ (lhs', ty) = case (runState (subst 0 lhs) Nothing) of

1093+ (_, Nothing) -> error $ "Patvar " ++ show n ++ " not bound on the LHS of " ++ show name

1094+ (tm', Just ty) -> (Bind n (PVar ty) tm', ty)

1095+

1096+ rhs' = case (runState (subst 0 rhs) (Just ty)) of

1097+ (tm', _) -> Bind n (PVar ty) tm'

1098+

1099+ subst :: Int -> Term -> State (Maybe Term) Term

1100+ subst i (P nt n' ty) | n' == n && nt == Bound = put (Just ty) >> return (V i)

1101+ | otherwise = subst i ty >>= return . P nt n'

1102+ subst i t@(Bind n' b sc) | n == n = return t -- The name is shadowed, so we won't find it here

1103+ | otherwise = do b' <- mapM (subst i) b

1104+ sc' <- subst (i + 1) sc

1105+ return $ Bind n' b' sc'

1106+ subst i (App s f a) = do f' <- subst i f

1107+ a' <- subst i a

1108+ return $ App s f' a'

1109+ subst i (Proj x idx) = do x' <- subst i x

1110+ return $ Proj x' idx

1111+ subst i t = return t

1112+

1077-- | Build the reflected datatype definition(s) that correspond(s) to

1113-- | Build the reflected datatype definition(s) that correspond(s) to

1078-- a provided unqualified name

1114-- a provided unqualified name

1079buildDatatypes :: IState -> Name -> [RDatatype]

1115buildDatatypes :: IState -> Name -> [RDatatype]

@@ -1163,3 +1199,10 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

1163 RApp (Var $ tacN "TyConParameter") (reflectArg a)

1199 RApp (Var $ tacN "TyConParameter") (reflectArg a)

1164 reflectConArg (RIndex a) =

1200 reflectConArg (RIndex a) =

1165 RApp (Var $ tacN "TyConIndex") (reflectArg a)

1201 RApp (Var $ tacN "TyConIndex") (reflectArg a)

1202+

1203+reflectFunClause :: RFunClause -> Raw

1204+reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") [ lhs, rhs ]

1205+reflectFunClause (RMkImpossibleClause lhs) = RApp (Var $ tacN "MkImpossibleClause") lhs

1206+

1207+reflectFunDefn :: RFunDefn -> Raw

1208+reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [reflectName name, rawList (Var $ tacN "FunClause") (map reflectFunClause clauses)]