c51241f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Reflected elab: look up datatypes

c51241fDavid Raymond Christiansen12 years ago

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

compare with master

unifiedsplit

@@ -23,6 +23,16 @@ data FunClause : Type where

23data FunDefn : Type where

24 DefineFun : TTName -> List FunClause -> FunDefn

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+

26abstract

36abstract

27data Elab : Type -> Type where

37data Elab : Type -> Type where

28 -- obligatory control stuff

38 -- obligatory control stuff

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

37 prim__Holes : Elab (List TTName)

47 prim__Holes : Elab (List TTName)

38 prim__Guess : Elab (Maybe TT)

48 prim__Guess : Elab (Maybe TT)

39 prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))

49 prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))

50+ prim__LookupDatatype : TTName -> Elab (List Datatype)

41 prim__SourceLocation : Elab SourceLocation

52 prim__SourceLocation : Elab SourceLocation

@@ -106,6 +117,15 @@ lookupTyExact n = case !(lookupTy n) of

106 [] => fail [NamePart n, TextPart "is not defined."]

117 [] => fail [NamePart n, TextPart "is not defined."]

107 xs => fail [NamePart n, TextPart "is ambiguous."]

118 xs => fail [NamePart n, TextPart "is ambiguous."]

108

119

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+

109forgetTypes : TT -> Elab Raw

129forgetTypes : TT -> Elab Raw

110forgetTypes tt = prim__Forget tt

130forgetTypes tt = prim__Forget tt

111

131

src/Idris/Elab/Term.hs+8−1

@@ -28,7 +28,7 @@ import Control.Monad

28import Control.Monad.State.Strict

29import Data.List

30import qualified Data.Map as M

31−import Data.Maybe (mapMaybe, fromMaybe)

31+import Data.Maybe (mapMaybe, fromMaybe, catMaybes)

32import qualified Data.Set as S

33import qualified Data.Text as T

@@ -1683,6 +1683,13 @@ runTactical fc env tm = do tm' <- eval tm

1683 , raw_apply (Var pairTy) [ Var (reflm "NameType")

1684 , Var (reflm "TT")]])

1685 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'))

1686 | n == tacN "prim__SourceLocation", [] <- args

1693 | n == tacN "prim__SourceLocation", [] <- args

1687 = fmap fst . get_type_val $

1694 = fmap fst . get_type_val $

1688 reflectFC fc

1695 reflectFC fc

src/Idris/Reflection.hs+46−4

@@ -6,23 +6,31 @@ quoters and unquoters along with some supporting datatypes.

6module Idris.Reflection where

8import Control.Monad (liftM, liftM2)

9+import Data.Maybe (catMaybes)

9import Data.List ((\\))

10import Data.List ((\\))

10import qualified Data.Text as T

11import qualified Data.Text as T

12import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,

13import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,

13 movelast, runElab, solve)

14 movelast, runElab, solve)

14−import Idris.Core.Evaluate (initContext)

15+import Idris.Core.Evaluate (Context, Def(TyDecl), initContext, lookupDefExact, lookupTyExact)

15import Idris.Core.TT

16import Idris.Core.TT

17import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),

18import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),

18 PTerm(..), initEState, pairCon, pairTy)

19 PTerm(..), initEState, pairCon, pairTy)

19import Idris.Delaborate (delab)

20import Idris.Delaborate (delab)

21−data RArg = RExplicit { argName :: Name, argTy :: Raw }

22+data RArg = RExplicit { argName :: Name, argTy :: Raw }

22− | RImplicit { argName :: Name, argTy :: Raw }

23+ | RImplicit { argName :: Name, argTy :: Raw }

23 | RConstraint { argName :: Name, argTy :: Raw }

24 | RConstraint { argName :: Name, argTy :: Raw }

25+ deriving Show

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

27rArgToPArg :: RArg -> PArg

35rArgToPArg :: RArg -> PArg

28rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

36rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

@@ -896,3 +904,37 @@ envTupleType

896 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

904 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

897 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))

905 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))

898 ]

906 ]

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]