git.iko.soy/Idris-dev
on master help sign in
Reflected elab: look up datatypes

Now, a reflected version of datatype definitions can be looked up.

commitc51241f415422402bc80504554a7721b64959a6c authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 16 Apr 2015, 16:22 (12 years ago) parentd97715e
3 files changed+74−5
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+20 src/Idris/Elab/Term.hs+8−1 src/Idris/Reflection.hs+46−4
libs/prelude/Language/Reflection/Elab.idr+20
@@ -23,6 +23,16 @@ data FunClause : Type where
2323data FunDefn : Type where
2424 DefineFun : TTName -> List FunClause -> FunDefn
2525
26+data TyConArg : Type where
27+ Parameter : TTName -> Raw -> TyConArg
28+ Index : TTName -> Raw -> TyConArg
29+
30+data Datatype : Type where
31+ MkDatatype : (familyName : TTName) ->
32+ (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->
33+ (constrs : List (TTName, Raw)) ->
34+ Datatype
35+
2636abstract
2737data Elab : Type -> Type where
2838 -- obligatory control stuff
@@ -37,6 +47,7 @@ data Elab : Type -> Type where
3747 prim__Holes : Elab (List TTName)
3848 prim__Guess : Elab (Maybe TT)
3949 prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
50+ prim__LookupDatatype : TTName -> Elab (List Datatype)
4051
4152 prim__SourceLocation : Elab SourceLocation
4253
@@ -106,6 +117,15 @@ lookupTyExact n = case !(lookupTy n) of
106117 [] => fail [NamePart n, TextPart "is not defined."]
107118 xs => fail [NamePart n, TextPart "is ambiguous."]
108119
120+lookupDatatype : TTName -> Elab (List Datatype)
121+lookupDatatype n = prim__LookupDatatype n
122+
123+lookupDatatypeExact : TTName -> Elab Datatype
124+lookupDatatypeExact n = case !(lookupDatatype n) of
125+ [res] => return res
126+ [] => fail [TextPart "No datatype named", NamePart n]
127+ xs => fail [TextPart "More than one datatype named", NamePart n]
128+
109129forgetTypes : TT -> Elab Raw
110130forgetTypes tt = prim__Forget tt
111131
src/Idris/Elab/Term.hs+8−1
@@ -28,7 +28,7 @@ import Control.Monad
2828import Control.Monad.State.Strict
2929import Data.List
3030import qualified Data.Map as M
31−import Data.Maybe (mapMaybe, fromMaybe)
31+import Data.Maybe (mapMaybe, fromMaybe, catMaybes)
3232import qualified Data.Set as S
3333import qualified Data.Text as T
3434
@@ -1683,6 +1683,13 @@ runTactical fc env tm = do tm' <- eval tm
16831683 , raw_apply (Var pairTy) [ Var (reflm "NameType")
16841684 , Var (reflm "TT")]])
16851685 defs
1686+ | n == tacN "prim__LookupDatatype", [name] <- args
1687+ = do n' <- reifyTTName name
1688+ datatypes <- get_datatypes
1689+ ctxt <- get_context
1690+ fmap fst . get_type_val $
1691+ rawList (Var (tacN "Datatype"))
1692+ (map reflectDatatype (buildDatatypes ctxt datatypes n'))
16861693 | n == tacN "prim__SourceLocation", [] <- args
16871694 = fmap fst . get_type_val $
16881695 reflectFC fc
src/Idris/Reflection.hs+46−4
@@ -6,23 +6,31 @@ quoters and unquoters along with some supporting datatypes.
66module Idris.Reflection where
77
88import Control.Monad (liftM, liftM2)
9+import Data.Maybe (catMaybes)
910import Data.List ((\\))
1011import qualified Data.Text as T
1112
1213import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
1314 movelast, runElab, solve)
14−import Idris.Core.Evaluate (initContext)
15+import Idris.Core.Evaluate (Context, Def(TyDecl), initContext, lookupDefExact, lookupTyExact)
1516import Idris.Core.TT
1617
1718import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),
1819 PTerm(..), initEState, pairCon, pairTy)
1920import Idris.Delaborate (delab)
2021
21−data RArg = RExplicit { argName :: Name, argTy :: Raw }
22− | RImplicit { argName :: Name, argTy :: Raw }
22+data RArg = RExplicit { argName :: Name, argTy :: Raw }
23+ | RImplicit { argName :: Name, argTy :: Raw }
2324 | RConstraint { argName :: Name, argTy :: Raw }
25+ deriving Show
2426
25−data RTyDecl = RDeclare Name [RArg] Raw
27+data RTyDecl = RDeclare Name [RArg] Raw deriving Show
28+
29+data RTyConArg = RParameter { tcArgName :: Name, tcArgTy :: Raw }
30+ | RIndex { tcArgName :: Name, tcArgTy :: Raw }
31+ deriving Show
32+
33+data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, Raw)] deriving Show
2634
2735rArgToPArg :: RArg -> PArg
2836rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
@@ -896,3 +904,37 @@ envTupleType
896904 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
897905 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
898906 ]
907+
908+-- | Build the reflected datatype definition(s) that correspond(s) to
909+-- a provided unqualified name
910+buildDatatypes :: Context -> Ctxt TypeInfo -> Name -> [RDatatype]
911+buildDatatypes ctxt datatypes n =
912+ catMaybes [ mkDataType dn ti
913+ | (dn, ti) <- lookupCtxtName n datatypes
914+ ]
915+ where mkDataType name (TI {param_pos = params, con_names = constrs}) =
916+ do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
917+ let (tcargs, tcres) = getArgs params (forget ty) 0
918+ conTys <- mapM (fmap forget . flip lookupTyExact ctxt) constrs
919+ return $ RDatatype name tcargs tcres $ zip constrs conTys
920+
921+ getArgs params (RBind an (Pi _ ty _) body) i =
922+ let (args, res) = getArgs params body (i+1)
923+ in if i `elem` params
924+ then (RParameter an ty : args, res )
925+ else (RIndex an ty : args, res)
926+ getArgs _ tm _ = ([], tm)
927+
928+reflectDatatype :: RDatatype -> Raw
929+reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
930+ raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn
931+ , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
932+ , reflectRaw tyConRes
933+ , rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "Raw"))
934+ [ rawPair ((Var $ reflm "TTName"), (Var $ reflm "Raw"))
935+ (reflectName cn, reflectRaw cty)
936+ | (cn, cty) <- constrs
937+ ]
938+ ]
939+ where reflectConArg (RParameter n t) = raw_apply (Var $ tacN "Parameter") [reflectName n, reflectRaw t]
940+ reflectConArg (RIndex n t) = raw_apply (Var $ tacN "Index") [reflectName n, reflectRaw t]