@@ -599,13 +599,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
599599 -- Look for 'static' names and generate new specialised
600600 -- definitions for them
601601
602− {- Not fully implemented yet!
602+ {-
603603 mapM_ (\ e -> case e of
604604 Left _ -> return ()
605− Right (l, r) -> elabPE info fc r) pats
606− -}
607−
608− -- TODO: Inlining on initial definition happens here.
605+ Right (l, r) -> elabPE info fc n r) pats
606+ -}
609607
610608 -- NOTE: Need to store original definition so that proofs which
611609 -- rely on its structure aren't affected by any changes to the
@@ -771,8 +769,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
771769 Just ns -> partial_eval (tt_ctxt ist) ns pats
772770
773771-- Find 'static' applications in a term and partially evaluate them
774−elabPE :: ElabInfo -> FC -> Term -> Idris ()
775−elabPE info fc r =
772+elabPE :: ElabInfo -> FC -> Name -> Term -> Idris ()
773+elabPE info fc caller r =
776774 do ist <- getIState
777775 let sa = getSpecApps ist [] r
778776 mapM_ (mkSpecialised ist) sa
@@ -789,11 +787,13 @@ elabPE info fc r =
789787 -- Apply that transformation after every PClauses elaboration
790788
791789 mkSpecialised ist specapp = do
790+ iputStrLn (show specapp)
792791 let specTy = getSpecTy ist specapp
793792 let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp
794793 let undef = case lookupDef newnm (tt_ctxt ist) of
795794 [] -> True
796795 _ -> False
796+ iputStrLn $ show (newnm, map (concreteArg ist) (snd specapp))
797797 when (undef && all (concreteArg ist) (snd specapp)) $ do
798798 let opts = [Specialise ((n, Nothing) :
799799 (mapMaybe specName (snd specapp)))]
@@ -820,6 +820,7 @@ elabPE info fc r =
820820 case lookupTy n (tt_ctxt ist) of
821821 [] -> False
822822 _ -> True
823+ concreteTm ist (Constant _) = True
823824 concreteTm ist _ = False
824825
825826 -- get the type of a specialised application
@@ -832,7 +833,8 @@ elabPE info fc r =
832833 _ -> error "Can't happen (getSpecTy)"
833834
834835 getSpecClause ist (n, args)
835− = let newnm = UN (show (nsroot n) ++ "__spectest") in -- UN (show n ++ show (map snd args)) in
836+ = let newnm = UN (show (nsroot n) ++ "_" ++ show (nsroot caller) ++
837+ "__spectest") in -- UN (show n ++ show (map snd args)) in
836838 (n, newnm, mkPE_TermDecl ist newnm n args)
837839
838840