c1fabb1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Implement LookupFunDefn

Not working currently due to type erasure. Impossible clauses fail due to "imp" var.

commitc1fabb1c817b77544dc5e1842ad9205d4dd45477 authorShea Levy <shea@shealevy.com> dateThu 26 Nov 2015, 20:54 (11 years ago) parenta7754a0

4 files changed+65−2

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Elab.idr+14 src/Idris/Core/TT.hs+1 src/Idris/Elab/Term.hs+5 src/Idris/Reflection.hs+45−2

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

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

115115 Prim__Guess : Elab TT

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

117117 Prim__LookupDatatype : TTName -> Elab (List Datatype)

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

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

119120

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

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

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

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

232233

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]

233247

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

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

src/Idris/Core/TT.hs+1

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

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

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

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

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

11101111 subst i t = t

11111112

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

18621862 fmap fst . checkClosed $

18631863 rawList (Var (tacN "Datatype"))

18641864 (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'))

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

18661871 = do n' <- reifyTTName name

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

src/Idris/Reflection.hs+45−2

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

88#if __GLASGOW_HASKELL__ < 710

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

10+import Prelude hiding (mapM)

11+import Data.Traversable (mapM)

1012#endif

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

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

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

1315import Data.Maybe (catMaybes)

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

1517import qualified Data.Text as T

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

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

2022import Idris.Core.TT

2123

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),

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

2426 initEState, pairCon, pairTy)

2527import Idris.Delaborate (delab)

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

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

10751077 ua args t = (t, args)

10761078

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+

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

10781114-- a provided unqualified name

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

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

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

11641200 reflectConArg (RIndex a) =

11651201 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)]