@@ -6,37 +6,44 @@ quoters and unquoters along with some supporting datatypes.
66module Idris.Reflection where
77
88import Control.Applicative ((<$>), (<*>), pure)
9−import Control.Monad (liftM, liftM2)
9+import Control.Monad (liftM, liftM2, liftM3)
1010import Data.Maybe (catMaybes)
1111import Data.List ((\\))
1212import qualified Data.Text as T
1313
1414import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
1515 movelast, runElab, solve)
16−import Idris.Core.Evaluate (Context, Def(TyDecl), initContext, lookupDefExact, lookupTyExact)
16+import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)
1717import Idris.Core.TT
1818
19−import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),
20− PTerm(..), initEState, pairCon, pairTy)
19+import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes),
20+ PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..),
21+ initEState, pairCon, pairTy)
2122import Idris.Delaborate (delab)
2223
23−data RArg = RExplicit { argName :: Name, argTy :: Raw }
24− | RImplicit { argName :: Name, argTy :: Raw }
25− | RConstraint { argName :: Name, argTy :: Raw }
24+data RErasure = RErased | RNotErased deriving Show
25+
26+data RArg = RExplicit { argName :: Name, argErased :: RErasure, argTy :: Raw }
27+ | RImplicit { argName :: Name, argErased :: RErasure, argTy :: Raw }
28+ | RConstraint { argName :: Name, argErased :: RErasure, argTy :: Raw }
2629 deriving Show
2730
2831data RTyDecl = RDeclare Name [RArg] Raw deriving Show
2932
30−data RTyConArg = RParameter { tcArgName :: Name, tcArgTy :: Raw }
31− | RIndex { tcArgName :: Name, tcArgTy :: Raw }
33+data RTyConArg = RParameter { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
34+ | RIndex { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
3235 deriving Show
3336
34−data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, Raw)] deriving Show
37+data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RArg], Raw)] deriving Show
38+
39+rArgOpts :: RErasure -> [ArgOpt]
40+rArgOpts RErased = [InaccessibleArg]
41+rArgOpts _ = []
3542
3643rArgToPArg :: RArg -> PArg
37−rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
38−rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
39−rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder
44+rArgToPArg (RExplicit n e _) = PExp 0 (rArgOpts e) n Placeholder
45+rArgToPArg (RImplicit n e _) = PImp 0 False (rArgOpts e) n Placeholder
46+rArgToPArg (RConstraint n e _) = PConstraint 0 (rArgOpts e) n Placeholder
4047
4148data RFunClause = RMkFunClause Raw Raw
4249 | RMkImpossibleClause Raw
@@ -780,6 +787,13 @@ rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
780787rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
781788rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
782789
790+-- | Idris tuples nest to the right
791+rawTripleTy :: Raw -> Raw -> Raw -> Raw
792+rawTripleTy a b c = rawPairTy a (rawPairTy b c)
793+
794+rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw
795+rawTriple (a, b, c) (x, y, z) = rawPair (a, rawPairTy b c) (x, rawPair (b, c) (y, z))
796+
783797reflectCtxt :: [(Name, Type)] -> Raw
784798reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
785799 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
@@ -929,6 +943,12 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
929943 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
930944reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
931945
946+reifyErasure :: Term -> ElabD RErasure
947+reifyErasure (P (DCon _ _ _) n _)
948+ | n == tacN "Erased" = return RErased
949+ | n == tacN "NotErased" = return RNotErased
950+reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."
951+
932952reifyTyDecl :: Term -> ElabD RTyDecl
933953reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
934954 | n == tacN "Declare" =
@@ -939,14 +959,17 @@ reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
939959 ret' <- reifyRaw ret
940960 return $ RDeclare tyN' args' ret'
941961 where reifyRArg :: Term -> ElabD RArg
942− reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)
943− | n == tacN "Explicit" = liftM2 RExplicit
962+ reifyRArg (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argE) argTy)
963+ | n == tacN "Explicit" = liftM3 RExplicit
944964 (reifyTTName argN)
965+ (reifyErasure argE)
945966 (reifyRaw argTy)
946− | n == tacN "Implicit" = liftM2 RImplicit
967+ | n == tacN "Implicit" = liftM3 RImplicit
947968 (reifyTTName argN)
948− (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
969+ (reifyErasure argE)
970+ (reifyRaw argTy) | n == tacN "Constraint" = liftM3 RConstraint
949971 (reifyTTName argN)
972+ (reifyErasure argE)
950973 (reifyRaw argTy)
951974 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
952975reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
@@ -975,38 +998,89 @@ envTupleType
975998 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
976999 ]
9771000
1001+-- | Apply Idris's implicit info to get a signature. The [PArg] should
1002+-- come from a lookup in idris_implicits on IState.
1003+getArgs :: [PArg] -> Raw -> ([RArg], Raw)
1004+getArgs [] r = ([], r)
1005+getArgs (a:as) (RBind n (Pi _ ty _) sc) =
1006+ let (args, res) = getArgs as sc
1007+ erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased
1008+ arg' = case a of
1009+ PImp {} -> RImplicit n erased ty
1010+ PExp {} -> RExplicit n erased ty
1011+ PConstraint {} -> RConstraint n erased ty
1012+ PTacImplicit {} -> RImplicit n erased ty -- TODO?
1013+ in (arg':args, res)
1014+getArgs _ r = ([], r)
1015+
9781016-- | Build the reflected datatype definition(s) that correspond(s) to
9791017-- a provided unqualified name
980−buildDatatypes :: Context -> Ctxt TypeInfo -> Name -> [RDatatype]
981−buildDatatypes ctxt datatypes n =
1018+buildDatatypes :: IState -> Name -> [RDatatype]
1019+buildDatatypes ist n =
9821020 catMaybes [ mkDataType dn ti
9831021 | (dn, ti) <- lookupCtxtName n datatypes
9841022 ]
985− where mkDataType name (TI {param_pos = params, con_names = constrs}) =
986− do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
987− let (tcargs, tcres) = getArgs params (forget ty) 0
988− conTys <- mapM (fmap forget . flip lookupTyExact ctxt) constrs
989− return $ RDatatype name tcargs tcres $ zip constrs conTys
1023+ where datatypes = idris_datatypes ist
1024+ ctxt = tt_ctxt ist
1025+ impls = idris_implicits ist
9901026
991− getArgs params (RBind an (Pi _ ty _) body) i =
992− let (args, res) = getArgs params body (i+1)
1027+ ctorSig cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1028+ argInfo <- lookupCtxtExact cn impls
1029+ let (args, res) = getArgs argInfo cty
1030+ return (cn, args, res)
1031+
1032+ mkDataType name (TI {param_pos = params, con_names = constrs}) =
1033+ do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
1034+ implInfo <- lookupCtxtExact name impls
1035+ let (tcargs, tcres) = getTCArgs params implInfo (forget ty) 0
1036+ ctors <- mapM ctorSig constrs
1037+ return $ RDatatype name tcargs tcres ctors
1038+
1039+ getTCArgs params implInfo (RBind an (Pi _ ty _) body) i =
1040+ let (erased, implInfo') = case implInfo of
1041+ [] -> (RNotErased, [])
1042+ (a:as) -> (if InaccessibleArg `elem` argopts a
1043+ then RErased
1044+ else RNotErased,
1045+ as)
1046+ (args, res) = getTCArgs params implInfo' body (i+1)
9931047 in if i `elem` params
994− then (RParameter an ty : args, res )
995− else (RIndex an ty : args, res)
996− getArgs _ tm _ = ([], tm)
1048+ then (RParameter an erased ty : args, res )
1049+ else (RIndex an erased ty : args, res)
1050+ getTCArgs _ implInfo tm _ = ([], tm)
1051+
1052+reflectErasure :: RErasure -> Raw
1053+reflectErasure RErased = Var (tacN "Erased")
1054+reflectErasure RNotErased = Var (tacN "NotErased")
1055+
1056+reflectArg :: RArg -> Raw
1057+reflectArg arg =
1058+ RApp (RApp (RApp (Var con) (reflectName $ argName arg))
1059+ (reflectErasure $ argErased arg))
1060+ (reflectRaw $ argTy arg)
1061+ where con = case arg of
1062+ RExplicit{} -> tacN "Explicit"
1063+ RImplicit{} -> tacN "Implicit"
1064+ RConstraint{} -> tacN "Constraint"
9971065
9981066reflectDatatype :: RDatatype -> Raw
9991067reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
10001068 raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn
10011069 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
10021070 , reflectRaw tyConRes
1003− , rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "Raw"))
1004− [ rawPair ((Var $ reflm "TTName"), (Var $ reflm "Raw"))
1005− (reflectName cn, reflectRaw cty)
1006− | (cn, cty) <- constrs
1071+ , rawList (rawTripleTy (Var $ reflm "TTName")
1072+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg"))
1073+ (Var $ reflm "Raw"))
1074+ [ rawTriple ((Var $ reflm "TTName"),
1075+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg")),
1076+ (Var $ reflm "Raw"))
1077+ (reflectName cn,
1078+ rawList (Var $ tacN "Arg") (map reflectArg cargs),
1079+ reflectRaw cty)
1080+ | (cn, cargs, cty) <- constrs
10071081 ]
10081082 ]
1009− where reflectConArg (RParameter n t) =
1010− raw_apply (Var $ tacN "Parameter") [reflectName n, reflectRaw t]
1011− reflectConArg (RIndex n t) =
1012− raw_apply (Var $ tacN "Index") [reflectName n, reflectRaw t]
1083+ where reflectConArg (RParameter n e t) =
1084+ raw_apply (Var $ tacN "Parameter") [reflectName n, reflectErasure e, reflectRaw t]
1085+ reflectConArg (RIndex n e t) =
1086+ raw_apply (Var $ tacN "Index") [reflectName n, reflectErasure e, reflectRaw t]