Make FunDefn and FunClause polymorphic over TT and Raw

libs/prelude/Language/Reflection/Elab.idr

@@ -70,15 +70,15 @@ record TyDecl where
 
 
 ||| A single pattern-matching clause
-data FunClause : Type where
-  MkFunClause : (lhs, rhs : Raw) -> FunClause
-  MkImpossibleClause : (lhs : Raw) -> FunClause
+data FunClause : Type -> Type where
+  MkFunClause : (lhs, rhs : a) -> FunClause a
+  MkImpossibleClause : (lhs : a) -> FunClause a
 
 ||| A reflected function definition.
-record FunDefn where
+record FunDefn a where
   constructor DefineFun
   name : TTName
-  clauses : List FunClause
+  clauses : List (FunClause a)
 
 
 data CtorArg = CtorParameter FunArg | CtorField FunArg
@@ -115,7 +115,7 @@ data Elab : Type -> Type where
   Prim__Guess : Elab TT
   Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
   Prim__LookupDatatype : TTName -> Elab (List Datatype)
-  Prim__LookupFunDefn : TTName -> Elab (List FunDefn)
+  Prim__LookupFunDefn : TTName -> Elab (List (FunDefn TT))
   Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
 
   Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)
@@ -148,7 +148,7 @@ data Elab : Type -> Type where
   Prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()
 
   Prim__DeclareType : TyDecl -> Elab ()
-  Prim__DefineFunction : FunDefn -> Elab ()
+  Prim__DefineFunction : FunDefn Raw -> Elab ()
   Prim__AddInstance : TTName -> TTName -> Elab ()
   Prim__IsTCName : TTName -> Elab Bool
 
@@ -233,13 +233,13 @@ namespace Tactics
 
   ||| Find the reflected function definition of all functions whose names
   ||| are overloadings of some name.
-  lookupFunDefn : TTName -> Elab (List FunDefn)
+  lookupFunDefn : TTName -> Elab (List (FunDefn TT))
   lookupFunDefn n = Prim__LookupFunDefn n
 
   ||| Find the reflected function definition of a function, given its
   ||| fully-qualified name. Fail if the name does not uniquely resolve
   ||| to a function.
-  lookupFunDefnExact : TTName -> Elab FunDefn
+  lookupFunDefnExact : TTName -> Elab (FunDefn TT)
   lookupFunDefnExact n = case !(lookupFunDefn n) of
                            [res] => return res
                            []    => fail [TextPart "No function named", NamePart n]
@@ -465,7 +465,7 @@ namespace Tactics
   ||| Define a function in the global context. The function must have
   ||| already been declared, either in ordinary Idris code or using
   ||| `declareType`.
-  defineFunction : FunDefn -> Elab ()
+  defineFunction : FunDefn Raw -> Elab ()
   defineFunction defun = Prim__DefineFunction defun
 
   ||| Register a new instance for type class resolution.

libs/pruviloj/Pruviloj/Derive/DecEq.idr

@@ -183,7 +183,7 @@ deriveDecEq fn =
                     Nothing => return False
 
     partial -- mkRhs
-    mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe FunClause)
+    mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe (FunClause Raw))
     mkCase k fam (cn1, args1, _) (cn2, args2, _) =
         perhaps $ elabPatternClause
           (do (h2 :: h1 :: _) <- reverse <$>

libs/pruviloj/Pruviloj/Derive/Eliminators.idr

@@ -134,7 +134,7 @@ instance Show ElimArg where
   show (NormalArgument x) = "NormalArgument " ++ show x
 
 getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->
-                (TTName, List CtorArg, Raw) -> Nat -> Elab FunClause
+                (TTName, List CtorArg, Raw) -> Nat -> Elab (FunClause Raw)
 getElimClause info elimn methCount (cn, args, resTy) whichCon =
   elabPatternClause
     (do -- Establish a hole for each parameter
@@ -242,13 +242,13 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
         bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x
 
 getElimClauses : TyConInfo -> (elimn : TTName) ->
-                 List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+                 List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
 getElimClauses info elimn ctors =
   let methodCount = length ctors
   in traverse (\(i, con) => getElimClause info elimn methodCount con i)
               (enumerate ctors)
 
-instance Show FunClause where
+instance (Show a) => Show (FunClause a) where
   show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"
 
 abstract

libs/pruviloj/Pruviloj/Internals.idr

@@ -101,7 +101,7 @@ bindPatTys ((n, b)::bs) res = RBind n (PVTy (getBinderTy b)) $ bindPatTys bs res
 |||       It will be run in a context where the pattern variables are
 |||       already bound, and should leave behind no holes.
 partial
-elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause
+elabPatternClause : (lhs, rhs : Elab ()) -> Elab (FunClause Raw)
 elabPatternClause lhs rhs =
   do -- Elaborate the LHS in a context where its type will be solved via unification
      (pat, _) <- runElab `(Infer) $

src/Idris/Core/TT.hs

@@ -1107,7 +1107,6 @@ instantiate e = subst 0 where
     subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
     subst i (App s f a) = App s (subst i f) (subst i a)
     subst i (Proj x idx) = Proj (subst i x) idx
-    -- If ever adding a clause here, please update mkFunClause in Idris/Reflection.hs
     subst i t = t
 
 -- | As 'instantiate', but also decrement the indices of all de Bruijn variables

src/Idris/Elab/Term.hs

@@ -1770,7 +1770,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
     pullVars :: (Term, Term) -> ([Name], Term, Term)
     pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
 
-    defineFunction :: RFunDefn -> ElabD ()
+    defineFunction :: RFunDefn Raw -> ElabD ()
     defineFunction (RDefineFun n clauses) =
       do ctxt <- get_context
          ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
@@ -1865,7 +1865,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
       | n == tacN "Prim__LookupFunDefn", [name] <- args
       = do n' <- reifyTTName name
            fmap fst . checkClosed $
-             rawList (Var (tacN "FunDefn"))
+             rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
                (map reflectFunDefn (buildFunDefns ist n'))
       | n == tacN "Prim__LookupArgs", [name] <- args
       = do n' <- reifyTTName name

src/Idris/Reflection.hs

@@ -11,7 +11,7 @@ import Prelude hiding (mapM)
 import Data.Traversable (mapM)
 #endif
 import Control.Monad (liftM, liftM2, liftM4)
-import Control.Monad.State.Strict (lift, State, runState, put)
+import Control.Monad.State.Strict (lift)
 import Data.Maybe (catMaybes)
 import Data.List ((\\), findIndex)
 import qualified Data.Text as T
@@ -57,11 +57,11 @@ rFunArgToPArg (RFunArg n _ RExplicit e) = PExp 0 (rArgOpts e) n Placeholder
 rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder
 rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder
 
-data RFunClause = RMkFunClause Raw Raw
-                | RMkImpossibleClause Raw
-                deriving Show
+data RFunClause a = RMkFunClause a a
+                  | RMkImpossibleClause a
+                  deriving Show
 
-data RFunDefn = RDefineFun Name [RFunClause] deriving Show
+data RFunDefn a = RDefineFun Name [RFunClause a] deriving Show
 
 -- | Prefix a name with the "Language.Reflection" namespace
 reflm :: String -> Name
@@ -1025,21 +1025,21 @@ reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
      return $ RDeclare tyN' args' ret'
 reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
 
-reifyFunDefn :: Term -> ElabD RFunDefn
-reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)
-  | n == tacN "DefineFun" =
+reifyFunDefn :: Term -> ElabD (RFunDefn Raw)
+reifyFunDefn (App _ (App _ (App _ (P _ n _) (P _ t _)) fnN) clauses)
+  | n == tacN "DefineFun" && t == reflm "Raw" =
   do fnN' <- reifyTTName fnN
      clauses' <- case unList clauses of
                    Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
                    Just cs -> mapM reifyC cs
      return $ RDefineFun fnN' clauses'
-  where reifyC :: Term -> ElabD RFunClause
-        reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)
-          | n == tacN "MkFunClause" = liftM2 RMkFunClause
+  where reifyC :: Term -> ElabD (RFunClause Raw)
+        reifyC (App _ (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs) rhs)
+          | n == tacN "MkFunClause" && t == reflm "Raw" = liftM2 RMkFunClause
                                              (reifyRaw lhs)
                                              (reifyRaw rhs)
-        reifyC (App _ (P (DCon _ _ _) n _) lhs)
-          | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
+        reifyC (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs)
+          | n == tacN "MkImpossibleClause" && t == reflm "Raw" = fmap RMkImpossibleClause $ reifyRaw lhs
         reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
 reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
 
@@ -1078,37 +1078,19 @@ unApplyRaw tm = ua [] tm
 
 -- | Build the reflected function definition(s) that correspond(s) to
 -- a provided unqualifed name
-buildFunDefns :: IState -> Name -> [RFunDefn]
+buildFunDefns :: IState -> Name -> [RFunDefn Term]
 buildFunDefns ist n =
   [ mkFunDefn name clauses
   | (name, (clauses, _)) <- lookupCtxtName n $ idris_patdefs ist
   ]
-  where mkFunDefn name clauses = RDefineFun name (map (mkFunClause name) clauses)
-
-        mkFunClause :: Name -> ([Name], Term, Term) -> RFunClause
-        mkFunClause _ ([], lhs, Impossible) = RMkImpossibleClause (forget lhs)
-        mkFunClause _ ([], lhs, rhs) = RMkFunClause (forget lhs) (forget rhs)
-        mkFunClause name ((n : ns), lhs, rhs) = mkFunClause name (ns, lhs', rhs') where
-          (lhs', ty) = case (runState (subst 0 lhs) Nothing) of
-                        (_, Nothing) -> error $ "Patvar " ++ show n ++ " not bound on the LHS of " ++ show name
-                        (tm', Just ty) -> (Bind n (PVar ty) tm', ty)
-
-          rhs' = case (runState (subst 0 rhs) (Just ty)) of
-                   (tm', _) -> Bind n (PVar ty) tm'
-
-          subst :: Int -> Term -> State (Maybe Term) Term
-          subst i (P nt n' ty) | n' == n && nt == Bound = put (Just ty) >> return (V i)
-                               | otherwise = subst i ty >>= return . P nt n'
-          subst i t@(Bind n' b sc) | n == n = return t -- The name is shadowed, so we won't find it here
-                                   | otherwise = do b' <- mapM (subst i) b
-                                                    sc' <- subst (i + 1) sc
-                                                    return $ Bind n' b' sc'
-          subst i (App s f a) = do f' <- subst i f
-                                   a' <- subst i a
-                                   return $ App s f' a'
-          subst i (Proj x idx) = do x' <- subst i x
-                                    return $ Proj x' idx
-          subst i t = return t
+
+  where mkFunDefn name clauses = RDefineFun name (map mkFunClause clauses)
+
+        mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs
+        mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs
+        mkFunClause ((n : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where
+          bind Impossible = Impossible
+          bind tm = Bind n (PVar Erased) tm
 
 -- | Build the reflected datatype definition(s) that correspond(s) to
 -- a provided unqualified name
@@ -1200,9 +1182,12 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
         reflectConArg (RIndex a) =
           RApp (Var $ tacN "TyConIndex") (reflectArg a)
 
-reflectFunClause :: RFunClause -> Raw
-reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") [ lhs, rhs ]
-reflectFunClause (RMkImpossibleClause lhs) = RApp (Var $ tacN "MkImpossibleClause") lhs
+reflectFunClause :: RFunClause Term -> Raw
+reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]
+reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause") $ [ Var $ reflm "TT", reflect lhs ]
 
-reflectFunDefn :: RFunDefn -> Raw
-reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [reflectName name, rawList (Var $ tacN "FunClause") (map reflectFunClause clauses)]
+reflectFunDefn :: RFunDefn Term -> Raw
+reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [ Var $ reflm "TT"
+                                                                              , reflectName name
+                                                                              , rawList (RApp (Var $ tacN "FunClause") (Var $ reflm "TT")) (map reflectFunClause clauses)
+                                                                              ]

test/meta001/Finite.idr

@@ -29,7 +29,7 @@ mkFin (S k) (S j) = do i <- mkFin k j
 
 mkToClause : TTName -> (size, i : Nat) ->
              (constr : (TTName, List CtorArg, Raw)) ->
-             Elab FunClause
+             Elab (FunClause Raw)
 mkToClause fn size i (n, [], Var ty) =
   MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
 mkToClause fn size i (n, _, ty) =
@@ -38,22 +38,22 @@ mkToClause fn size i (n, _, ty) =
 
 mkFromClause : TTName -> (size, i : Nat) ->
                (constr : (TTName, List CtorArg, Raw)) ->
-               Elab FunClause
+               Elab (FunClause Raw)
 mkFromClause fn size i (n, [], Var ty) =
   return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
 mkFromClause fn size i (n, _, ty) =
   fail [TextPart "unsupported constructor", NamePart n]
 
 
-mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause
+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)
 mkOk1Clause fn size i (n, [], Var ty) =
   return $ MkFunClause (RApp (Var fn) (Var n))
                        [| (Var (UN "Refl")) (Var ty) (Var n) |]
 mkOk1Clause fn size i (n, _, ty) =
   fail [TextPart "unsupported constructor", NamePart n]
 
 
-mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause
+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)
 mkOk2Clause fn size i (n, [], Var ty) =
   return $ MkFunClause (RApp (Var fn) !(mkFin size i))
                        [| (Var "Refl") `(Fin ~(quote size))
@@ -62,9 +62,9 @@ mkOk2Clause fn size i (n, _, ty) =
   fail [TextPart "unsupported constructor", NamePart n]
 
 
-mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
 mkToClauses fn size xs = mkToClauses' Z xs
-  where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+  where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
         mkToClauses' k []        = return []
         mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
                                       clause <- mkToClause fn size k x
@@ -76,7 +76,7 @@ mkToClauses fn size xs = mkToClauses' Z xs
 ||| This is to satisfy the totality checker, because `impossible`
 ||| clauses are still
 mkAbsurdFinClause : (fn : TTName) -> (goal : Raw -> Raw) -> (size : Nat) ->
-                    Elab FunClause
+                    Elab (FunClause Raw)
 mkAbsurdFinClause fn goal size =
   do pv <- gensym "badfin"
      lhsArg <- lhsBody pv size
@@ -92,26 +92,26 @@ mkAbsurdFinClause fn goal size =
 
 
 mkFromClauses : TTName -> TTName -> Nat ->
-                List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+                List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
 mkFromClauses fn ty size xs = mkFromClauses' Z xs
-  where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+  where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
         mkFromClauses' k []        =
              return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
         mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
                                         clause <- mkFromClause fn size k x
                                         return $ clause :: rest
 
-mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
 mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
-  where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+  where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
         mkOk1Clauses' k []        = return []
         mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
                                        clause <- mkOk1Clause fn size k x
                                        return $ clause :: rest
 
-mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
+mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List (FunClause Raw))
 mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
-  where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+  where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
         mkOk2Clauses' k []        = return [!(mkAbsurdFinClause fn resTy size)]
         mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
                                        clause <- mkOk2Clause fn size k x