@@ -6,9 +6,9 @@ quoters and unquoters along with some supporting datatypes.
66module Idris.Reflection where
77
88import Control.Applicative ((<$>), (<*>), pure)
9−import Control.Monad (liftM, liftM2, liftM3)
9+import Control.Monad (liftM, liftM2, liftM4)
1010import Data.Maybe (catMaybes)
11−import Data.List ((\\))
11+import Data.List ((\\), findIndex)
1212import qualified Data.Text as T
1313
1414import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
@@ -23,27 +23,33 @@ import Idris.Delaborate (delab)
2323
2424data RErasure = RErased | RNotErased deriving Show
2525
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 }
26+data RPlicity = RExplicit | RImplicit | RConstraint deriving Show
27+
28+data RFunArg = RFunArg { argName :: Name
29+ , argTy :: Raw
30+ , argPlicity :: RPlicity
31+ , erasure :: RErasure
32+ }
2933 deriving Show
3034
31−data RTyDecl = RDeclare Name [RArg] Raw deriving Show
35+data RTyDecl = RDeclare Name [RFunArg] Raw deriving Show
3236
33−data RTyConArg = RParameter { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
34− | RIndex { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
37+data RTyConArg = RParameter RFunArg
38+ | RIndex RFunArg
3539 deriving Show
3640
37−data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RArg], Raw)] deriving Show
41+data RCtorArg = RCtorParameter RFunArg | RCtorField RFunArg deriving Show
42+
43+data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)] deriving Show
3844
3945rArgOpts :: RErasure -> [ArgOpt]
4046rArgOpts RErased = [InaccessibleArg]
4147rArgOpts _ = []
4248
43−rArgToPArg :: RArg -> PArg
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
49+rFunArgToPArg :: RFunArg -> PArg
50+rFunArgToPArg (RFunArg n _ RExplicit e) = PExp 0 (rArgOpts e) n Placeholder
51+rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder
52+rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder
4753
4854data RFunClause = RMkFunClause Raw Raw
4955 | RMkImpossibleClause Raw
@@ -795,6 +801,9 @@ reflectEnv = foldr consToEnvList emptyEnvList
795801 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
796802 [envTupleType]
797803
804+reifyEnv :: Term -> ElabD Env
805+reifyEnv = reifyList (reifyPair reifyTTName (reifyTTBinder reifyTT (reflm "TT")))
806+
798807-- | Reflect an error into the internal datatype of Idris -- TODO
799808rawBool :: Bool -> Raw
800809rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
@@ -977,29 +986,31 @@ reifyErasure (P (DCon _ _ _) n _)
977986 | n == tacN "NotErased" = return RNotErased
978987reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."
979988
989+reifyPlicity :: Term -> ElabD RPlicity
990+reifyPlicity (P (DCon _ _ _) n _)
991+ | n == tacN "Explicit" = return RExplicit
992+ | n == tacN "Implicit" = return RImplicit
993+ | n == tacN "Constraint" = return RConstraint
994+reifyPlicity tm = fail $ "Couldn't reify " ++ show tm ++ " as RPlicity."
995+
996+reifyRFunArg :: Term -> ElabD RFunArg
997+reifyRFunArg (App _ (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argTy) argPl) argE)
998+ | n == tacN "MkFunArg" = liftM4 RFunArg
999+ (reifyTTName argN)
1000+ (reifyRaw argTy)
1001+ (reifyPlicity argPl)
1002+ (reifyErasure argE)
1003+reifyRFunArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
1004+
9801005reifyTyDecl :: Term -> ElabD RTyDecl
9811006reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
9821007 | n == tacN "Declare" =
9831008 do tyN' <- reifyTTName tyN
9841009 args' <- case unList args of
9851010 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
986− Just xs -> mapM reifyRArg xs
1011+ Just xs -> mapM reifyRFunArg xs
9871012 ret' <- reifyRaw ret
9881013 return $ RDeclare tyN' args' ret'
989− where reifyRArg :: Term -> ElabD RArg
990− reifyRArg (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argE) argTy)
991− | n == tacN "Explicit" = liftM3 RExplicit
992− (reifyTTName argN)
993− (reifyErasure argE)
994− (reifyRaw argTy)
995− | n == tacN "Implicit" = liftM3 RImplicit
996− (reifyTTName argN)
997− (reifyErasure argE)
998− (reifyRaw argTy) | n == tacN "Constraint" = liftM3 RConstraint
999− (reifyTTName argN)
1000− (reifyErasure argE)
1001− (reifyRaw argTy)
1002− reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
10031014reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
10041015
10051016reifyFunDefn :: Term -> ElabD RFunDefn
@@ -1028,19 +1039,25 @@ envTupleType
10281039
10291040-- | Apply Idris's implicit info to get a signature. The [PArg] should
10301041-- come from a lookup in idris_implicits on IState.
1031−getArgs :: [PArg] -> Raw -> ([RArg], Raw)
1042+getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)
10321043getArgs [] r = ([], r)
10331044getArgs (a:as) (RBind n (Pi _ ty _) sc) =
10341045 let (args, res) = getArgs as sc
10351046 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased
10361047 arg' = case a of
1037− PImp {} -> RImplicit n erased ty
1038− PExp {} -> RExplicit n erased ty
1039− PConstraint {} -> RConstraint n erased ty
1040− PTacImplicit {} -> RImplicit n erased ty -- TODO?
1048+ PImp {} -> RFunArg n ty RImplicit erased
1049+ PExp {} -> RFunArg n ty RExplicit erased
1050+ PConstraint {} -> RFunArg n ty RConstraint erased
1051+ PTacImplicit {} -> RFunArg n ty RImplicit erased
10411052 in (arg':args, res)
10421053getArgs _ r = ([], r)
10431054
1055+unApplyRaw :: Raw -> (Raw, [Raw])
1056+unApplyRaw tm = ua [] tm
1057+ where
1058+ ua args (RApp f a) = ua (a:args) f
1059+ ua args t = (t, args)
1060+
10441061-- | Build the reflected datatype definition(s) that correspond(s) to
10451062-- a provided unqualified name
10461063buildDatatypes :: IState -> Name -> [RDatatype]
@@ -1052,44 +1069,62 @@ buildDatatypes ist n =
10521069 ctxt = tt_ctxt ist
10531070 impls = idris_implicits ist
10541071
1055− ctorSig cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1056− argInfo <- lookupCtxtExact cn impls
1057− let (args, res) = getArgs argInfo cty
1058− return (cn, args, res)
1072+ ctorSig params cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1073+ argInfo <- lookupCtxtExact cn impls
1074+ let (args, res) = getArgs argInfo cty
1075+ return (cn, ctorArgsStatus args res params, res)
1076+
1077+ argPos n [] res = findPos n res
1078+ where findPos n app = case unApplyRaw app of
1079+ (_, argL) -> findIndex (== Var n) argL
1080+ argPos n (arg:args) res = if n == argName arg
1081+ then Nothing
1082+ else argPos n args res
1083+
1084+ ctorArgsStatus :: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
1085+ ctorArgsStatus [] _ _ = []
1086+ ctorArgsStatus (arg:args) res params =
1087+ case argPos (argName arg) args res of
1088+ Nothing -> RCtorField arg : ctorArgsStatus args res params
1089+ Just i -> if i `elem` params
1090+ then RCtorParameter arg : ctorArgsStatus args res params
1091+ else RCtorField arg : ctorArgsStatus args res params
10591092
10601093 mkDataType name (TI {param_pos = params, con_names = constrs}) =
10611094 do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
10621095 implInfo <- lookupCtxtExact name impls
1063− let (tcargs, tcres) = getTCArgs params implInfo (forget ty) 0
1064− ctors <- mapM ctorSig constrs
1096+ let (tcargs, tcres) = getTCArgs params implInfo (forget ty)
1097+ ctors <- mapM (ctorSig params) constrs
10651098 return $ RDatatype name tcargs tcres ctors
10661099
1067− getTCArgs params implInfo (RBind an (Pi _ ty _) body) i =
1068− let (erased, implInfo') = case implInfo of
1069− [] -> (RNotErased, [])
1070− (a:as) -> (if InaccessibleArg `elem` argopts a
1071− then RErased
1072− else RNotErased,
1073− as)
1074− (args, res) = getTCArgs params implInfo' body (i+1)
1075− in if i `elem` params
1076− then (RParameter an erased ty : args, res )
1077− else (RIndex an erased ty : args, res)
1078− getTCArgs _ implInfo tm _ = ([], tm)
1100+ getTCArgs :: [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)
1101+ getTCArgs params implInfo tcTy =
1102+ let (args, res) = getArgs implInfo tcTy
1103+ in (tcArg args 0, res)
1104+ where tcArg [] _ = []
1105+ tcArg (arg:args) i | i `elem` params = RParameter arg : tcArg args (i+1)
1106+ | otherwise = RIndex arg : tcArg args (i+1)
1107+
10791108
10801109reflectErasure :: RErasure -> Raw
10811110reflectErasure RErased = Var (tacN "Erased")
10821111reflectErasure RNotErased = Var (tacN "NotErased")
10831112
1084−reflectArg :: RArg -> Raw
1085−reflectArg arg =
1086− RApp (RApp (RApp (Var con) (reflectName $ argName arg))
1087− (reflectErasure $ argErased arg))
1088− (reflectRaw $ argTy arg)
1089− where con = case arg of
1090− RExplicit{} -> tacN "Explicit"
1091− RImplicit{} -> tacN "Implicit"
1092− RConstraint{} -> tacN "Constraint"
1113+reflectPlicity :: RPlicity -> Raw
1114+reflectPlicity RExplicit = Var (tacN "Explicit")
1115+reflectPlicity RImplicit = Var (tacN "Implicit")
1116+reflectPlicity RConstraint = Var (tacN "Constraint")
1117+
1118+reflectArg :: RFunArg -> Raw
1119+reflectArg (RFunArg n ty plic erasure) =
1120+ RApp (RApp (RApp (RApp (Var $ tacN "MkFunArg") (reflectName n))
1121+ (reflectRaw ty))
1122+ (reflectPlicity plic))
1123+ (reflectErasure erasure)
1124+
1125+reflectCtorArg :: RCtorArg -> Raw
1126+reflectCtorArg (RCtorParameter arg) = RApp (Var $ tacN "CtorParameter") (reflectArg arg)
1127+reflectCtorArg (RCtorField arg) = RApp (Var $ tacN "CtorField") (reflectArg arg)
10931128
10941129reflectDatatype :: RDatatype -> Raw
10951130reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
@@ -1097,18 +1132,18 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
10971132 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
10981133 , reflectRaw tyConRes
10991134 , rawList (rawTripleTy (Var $ reflm "TTName")
1100− (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg"))
1135+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "CtorArg"))
11011136 (Var $ reflm "Raw"))
11021137 [ rawTriple ((Var $ reflm "TTName"),
1103− (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg")),
1138+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "CtorArg")),
11041139 (Var $ reflm "Raw"))
11051140 (reflectName cn,
1106− rawList (Var $ tacN "Arg") (map reflectArg cargs),
1141+ rawList (Var $ tacN "CtorArg") (map reflectCtorArg cargs),
11071142 reflectRaw cty)
11081143 | (cn, cargs, cty) <- constrs
11091144 ]
11101145 ]
1111− where reflectConArg (RParameter n e t) =
1112− raw_apply (Var $ tacN "Parameter") [reflectName n, reflectErasure e, reflectRaw t]
1113− reflectConArg (RIndex n e t) =
1114− raw_apply (Var $ tacN "Index") [reflectName n, reflectErasure e, reflectRaw t]
1146+ where reflectConArg (RParameter a) =
1147+ RApp (Var $ tacN "TyConParameter") (reflectArg a)
1148+ reflectConArg (RIndex a) =
1149+ RApp (Var $ tacN "TyConIndex") (reflectArg a)