@@ -599,13 +599,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
599 -- Look for 'static' names and generate new specialised
599 -- Look for 'static' names and generate new specialised
600 -- definitions for them
600 -- definitions for them
602− {- Not fully implemented yet!
602+ {-
603 mapM_ (\ e -> case e of
603 mapM_ (\ e -> case e of
604 Left _ -> return ()
604 Left _ -> return ()
605− Right (l, r) -> elabPE info fc r) pats
605+ Right (l, r) -> elabPE info fc n r) pats
608− -- TODO: Inlining on initial definition happens here.
610 -- NOTE: Need to store original definition so that proofs which
608 -- NOTE: Need to store original definition so that proofs which
611 -- rely on its structure aren't affected by any changes to the
609 -- 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
771 Just ns -> partial_eval (tt_ctxt ist) ns pats
769 Just ns -> partial_eval (tt_ctxt ist) ns pats
773-- Find 'static' applications in a term and partially evaluate them
771-- Find 'static' applications in a term and partially evaluate them
774−elabPE :: ElabInfo -> FC -> Term -> Idris ()
772+elabPE :: ElabInfo -> FC -> Name -> Term -> Idris ()
775−elabPE info fc r =
773+elabPE info fc caller r =
776 do ist <- getIState
774 do ist <- getIState
777 let sa = getSpecApps ist [] r
775 let sa = getSpecApps ist [] r
778 mapM_ (mkSpecialised ist) sa
776 mapM_ (mkSpecialised ist) sa
@@ -789,11 +787,13 @@ elabPE info fc r =
789 -- Apply that transformation after every PClauses elaboration
787 -- Apply that transformation after every PClauses elaboration
791 mkSpecialised ist specapp = do
789 mkSpecialised ist specapp = do
790+ iputStrLn (show specapp)
792 let specTy = getSpecTy ist specapp
791 let specTy = getSpecTy ist specapp
793 let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp
792 let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp
794 let undef = case lookupDef newnm (tt_ctxt ist) of
793 let undef = case lookupDef newnm (tt_ctxt ist) of
795 [] -> True
794 [] -> True
796 _ -> False
795 _ -> False
796+ iputStrLn $ show (newnm, map (concreteArg ist) (snd specapp))
797 when (undef && all (concreteArg ist) (snd specapp)) $ do
797 when (undef && all (concreteArg ist) (snd specapp)) $ do
798 let opts = [Specialise ((n, Nothing) :
798 let opts = [Specialise ((n, Nothing) :
799 (mapMaybe specName (snd specapp)))]
799 (mapMaybe specName (snd specapp)))]
@@ -820,6 +820,7 @@ elabPE info fc r =
820 case lookupTy n (tt_ctxt ist) of
820 case lookupTy n (tt_ctxt ist) of
821 [] -> False
821 [] -> False
822 _ -> True
822 _ -> True
823+ concreteTm ist (Constant _) = True
823 concreteTm ist _ = False
824 concreteTm ist _ = False
825 -- get the type of a specialised application
826 -- get the type of a specialised application
@@ -832,7 +833,8 @@ elabPE info fc r =
832 _ -> error "Can't happen (getSpecTy)"
833 _ -> error "Can't happen (getSpecTy)"
834 getSpecClause ist (n, args)
835 getSpecClause ist (n, args)
836+ = let newnm = UN (show (nsroot n) ++ "_" ++ show (nsroot caller) ++
835− = let newnm = UN (show (nsroot n) ++ "__spectest") in -- UN (show n ++ show (map snd args)) in
837+ "__spectest") in -- UN (show n ++ show (map snd args)) in
836 (n, newnm, mkPE_TermDecl ist newnm n args)
838 (n, newnm, mkPE_TermDecl ist newnm n args)