@@ -11,7 +11,7 @@ import Prelude hiding (mapM)
1111import Data.Traversable (mapM)
1212#endif
1313import Control.Monad (liftM, liftM2, liftM4)
14−import Control.Monad.State.Strict (lift, State, runState, put)
14+import Control.Monad.State.Strict (lift)
1515import Data.Maybe (catMaybes)
1616import Data.List ((\\), findIndex)
1717import qualified Data.Text as T
@@ -57,11 +57,11 @@ rFunArgToPArg (RFunArg n _ RExplicit e) = PExp 0 (rArgOpts e) n Placeholder
5757rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder
5858rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder
5959
60−data RFunClause = RMkFunClause Raw Raw
61− | RMkImpossibleClause Raw
62− deriving Show
60+data RFunClause a = RMkFunClause a a
61+ | RMkImpossibleClause a
62+ deriving Show
6363
64−data RFunDefn = RDefineFun Name [RFunClause] deriving Show
64+data RFunDefn a = RDefineFun Name [RFunClause a] deriving Show
6565
6666-- | Prefix a name with the "Language.Reflection" namespace
6767reflm :: String -> Name
@@ -1025,21 +1025,21 @@ reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
10251025 return $ RDeclare tyN' args' ret'
10261026reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
10271027
1028−reifyFunDefn :: Term -> ElabD RFunDefn
1029−reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)
1030− | n == tacN "DefineFun" =
1028+reifyFunDefn :: Term -> ElabD (RFunDefn Raw)
1029+reifyFunDefn (App _ (App _ (App _ (P _ n _) (P _ t _)) fnN) clauses)
1030+ | n == tacN "DefineFun" && t == reflm "Raw" =
10311031 do fnN' <- reifyTTName fnN
10321032 clauses' <- case unList clauses of
10331033 Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
10341034 Just cs -> mapM reifyC cs
10351035 return $ RDefineFun fnN' clauses'
1036− where reifyC :: Term -> ElabD RFunClause
1037− reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)
1038− | n == tacN "MkFunClause" = liftM2 RMkFunClause
1036+ where reifyC :: Term -> ElabD (RFunClause Raw)
1037+ reifyC (App _ (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs) rhs)
1038+ | n == tacN "MkFunClause" && t == reflm "Raw" = liftM2 RMkFunClause
10391039 (reifyRaw lhs)
10401040 (reifyRaw rhs)
1041− reifyC (App _ (P (DCon _ _ _) n _) lhs)
1042− | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
1041+ reifyC (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs)
1042+ | n == tacN "MkImpossibleClause" && t == reflm "Raw" = fmap RMkImpossibleClause $ reifyRaw lhs
10431043 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
10441044reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
10451045
@@ -1078,37 +1078,19 @@ unApplyRaw tm = ua [] tm
10781078
10791079-- | Build the reflected function definition(s) that correspond(s) to
10801080-- a provided unqualifed name
1081−buildFunDefns :: IState -> Name -> [RFunDefn]
1081+buildFunDefns :: IState -> Name -> [RFunDefn Term]
10821082buildFunDefns ist n =
10831083 [ mkFunDefn name clauses
10841084 | (name, (clauses, _)) <- lookupCtxtName n $ idris_patdefs ist
10851085 ]
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
1086+
1087+ where mkFunDefn name clauses = RDefineFun name (map mkFunClause clauses)
1088+
1089+ mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs
1090+ mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs
1091+ mkFunClause ((n : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where
1092+ bind Impossible = Impossible
1093+ bind tm = Bind n (PVar Erased) tm
11121094
11131095-- | Build the reflected datatype definition(s) that correspond(s) to
11141096-- a provided unqualified name
@@ -1200,9 +1182,12 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
12001182 reflectConArg (RIndex a) =
12011183 RApp (Var $ tacN "TyConIndex") (reflectArg a)
12021184
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
1185+reflectFunClause :: RFunClause Term -> Raw
1186+reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]
1187+reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause") $ [ Var $ reflm "TT", reflect lhs ]
12061188
1207−reflectFunDefn :: RFunDefn -> Raw
1208−reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [reflectName name, rawList (Var $ tacN "FunClause") (map reflectFunClause clauses)]
1189+reflectFunDefn :: RFunDefn Term -> Raw
1190+reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [ Var $ reflm "TT"
1191+ , reflectName name
1192+ , rawList (RApp (Var $ tacN "FunClause") (Var $ reflm "TT")) (map reflectFunClause clauses)
1193+ ]