00d7c69 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Work towards making {static} arguments and specialisation work properly

commit00d7c690fbb1ceecdce3c1de594702cc05ecfbfb authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 3 Feb 2012, 21:11 (15 years ago) parentae1cf53

5 files changed+73−15

compare with master

unifiedsplit

src/Core/Evaluate.hs+12−3 src/Core/TT.hs+10 src/Idris/AbsSyntax.hs+34−11 src/Idris/ElabTerm.hs+14 src/Idris/REPL.hs+3−1

src/Core/Evaluate.hs+12−3

@@ -19,7 +19,7 @@ import Data.Binary hiding (get, put)

1919import Core.TT

2020import Core.CaseTree

2121

22−type EvalState = ()

22+type EvalState = ()

2323type Eval a = State EvalState a

2424

2525data EvalOpt = Spec | HNF | Simplify | AtREPL

@@ -46,7 +46,7 @@ data HNF = HP NameType Name (TT Name)

4646 deriving Show

4747

4848instance Show Value where

49− show x = show $ evalState (quote 10 x) ()

49+ show x = show $ evalState (quote 100 x) ()

5050

5151instance Show (a -> b) where

5252 show x = "<<fn>>"

@@ -162,7 +162,7 @@ eval ctxt statics genv tm opts = ev [] True [] tm where

162162 app <- apply stk top env a' as

163163 wknV (-1) app

164164 apply stk False env f args

165− | spec = return $ unload env f args

165+ | spec = specApply stk env f args

166166 apply stk top env (VP Ref n ty) args

167167 | [(CaseOp inl _ _ ns tree _ _, Public)] <- lookupDefAcc Nothing n atRepl ctxt

168168 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

@@ -181,6 +181,15 @@ eval ctxt statics genv tm opts = ev [] True [] tm where

181181 apply stk top env f (a:as) = return $ unload env f (a:as)

182182 apply stk top env f [] = return f

183183

184+ specApply stk env f@(VP Ref n ty) args

185+ = case lookupCtxt Nothing n statics of

186+ [as] -> if or as

187+ then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $

188+ return $ unload env f args

189+ else return $ unload env f args

190+ _ -> return $ unload env f args

191+ specApply stk env f args = return $ unload env f args

192+

184193 unload env f [] = f

185194 unload env f (a:as) = unload env (VApp f a) as

186195

src/Core/TT.hs+10

@@ -395,6 +395,16 @@ noOccurrence n t = no' 0 t

395395 no' i (App f a) = no' i f && no' i a

396396 no' i _ = True

397397

398+-- Returns all names used free in the term

399+

400+freeNames :: Eq n => TT n -> [n]

401+freeNames (P _ n _) = [n]

402+freeNames (Bind n (Let t v) sc) = nub $ freeNames v ++ (freeNames sc \\ [n])

403+ ++ freeNames t

404+freeNames (Bind n b sc) = nub $ freeNames (binderTy b) ++ (freeNames sc \\ [n])

405+freeNames (App f a) = nub $ freeNames f ++ freeNames a

406+freeNames _ = []

407+

398408-- Return the arity of a (normalised) type

399409

400410arity :: TT n -> Int

src/Idris/AbsSyntax.hs+34−11

@@ -400,7 +400,7 @@ deriving instance Binary Plicity

400400

401401impl = Imp False Dynamic

402402expl = Exp False Dynamic

403−constraint = Constraint False Static

403+constraint = Constraint False Dynamic

404404tacimpl = TacImp False Dynamic

405405

406406data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen

@@ -1055,6 +1055,30 @@ getPriority i tm = pri tm

10551055 pri Placeholder = 1

10561056 pri _ = 3

10571057

1058+addStatics :: Name -> Term -> PTerm -> Idris ()

1059+addStatics n tm ptm =

1060+ do let (statics, dynamics) = initStatics tm ptm

1061+ let stnames = nub $ concatMap freeNames (map snd statics)

1062+ let dnames = nub $ concatMap freeNames (map snd dynamics)

1063+ when (not (null statics)) $

1064+ logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics

1065+ ++ "\n" ++ show stnames ++ "\n" ++ show dnames

1066+ let statics' = nub $ map fst statics ++

1067+ filter (\x -> not (elem x dnames)) stnames

1068+ let stpos = staticList statics' tm

1069+ i <- get

1070+ put (i { idris_statics = addDef n stpos (idris_statics i) })

1071+ addIBC (IBCStatic n)

1072+ where

1073+ initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)

1074+ = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in

1075+ if pstatic p == Static then ((n, ty) : static, dynamic)

1076+ else (static, (n, ty) : dynamic)

1077+ initStatics t pt = ([], [])

1078+

1079+ staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc

1080+ staticList _ _ = []

1081+

10581082-- Dealing with implicit arguments

10591083

10601084-- Add implicit Pi bindings for any names in the term which appear in an

@@ -1066,14 +1090,13 @@ implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm

10661090implicit syn n ptm

10671091 = do i <- get

10681092 let (tm', impdata) = implicitise syn i ptm

1069− let (tm'', spos) = findStatics i tm'

1093+-- let (tm'', spos) = findStatics i tm'

10701094 put (i { idris_implicits = addDef n impdata (idris_implicits i) })

10711095 addIBC (IBCImp n)

10721096 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

1073− i <- get

1074− put (i { idris_statics = addDef n spos (idris_statics i) })

1075− addIBC (IBCStatic n)

1076− return tm''

1097+-- i <- get

1098+-- put (i { idris_statics = addDef n spos (idris_statics i) })

1099+ return tm'

10771100

10781101implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

10791102implicitise syn ist tm

@@ -1286,21 +1309,21 @@ mkPApp fc a f as = let rest = drop a as in

12861309-- FIXME: It's possible that this really has to happen after elaboration

12871310

12881311findStatics :: IState -> PTerm -> (PTerm, [Bool])

1289−findStatics ist tm = let (ns, ss) = fs tm in

1312+findStatics ist tm = trace (showImp True tm) $

1313+ let (ns, ss) = fs tm in

12901314 runState (pos ns ss tm) []

12911315 where fs (PPi p n t sc)

12921316 | Static <- pstatic p

12931317 = let (ns, ss) = fs sc in

1294− (namesIn [] ist t : ns, namesIn [] ist t ++ n : ss)

1318+ (namesIn [] ist t : ns, n : ss)

12951319 | otherwise = let (ns, ss) = fs sc in

1296− (namesIn [] ist t : ns, ss)

1320+ (ns, ss)

12971321 fs _ = ([], [])

12981322

12991323 inOne n ns = length (filter id (map (elem n) ns)) == 1

13001324

13011325 pos ns ss (PPi p n t sc)

1302− | n `inOne` ns && elem n ss

1303− = do sc' <- pos ns ss sc

1326+ | elem n ss = do sc' <- pos ns ss sc

13041327 spos <- get

13051328 put (True : spos)

13061329 return (PPi (p { pstatic = Static }) n t sc')

src/Idris/ElabTerm.hs+14

@@ -214,6 +214,7 @@ elab ist info pattern tcgen fn tm

214214 = do let args = {- case lookupCtxt f (inblock info) of

215215 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

216216 _ ->-} args'

217+ mkSpecialised ist fc f (map getTm args')

217218 ivs <- get_instances

218219 -- HACK: we shouldn't resolve type classes if we're defining an instance

219220 -- function or default definition.

@@ -497,3 +498,16 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

497498 runT x = fail $ "Not implemented " ++ show x

498499

499500solveAll = try (do solve; solveAll) (return ())

501+

502+-- If the function application is specialisable, make a new

503+-- top level function by normalising the application

504+-- and elaborating the new expression.

505+

506+mkSpecialised :: IState -> FC -> Name -> [PTerm] -> ElabD ()

507+mkSpecialised i fc n args

508+ = case lookupCtxt Nothing n (idris_statics i) of

509+ [] -> return ()

510+ [as] -> if (not (or as)) then return () else

511+ do return () -- trace (show (n, args)) $ return ()

512+

513+

src/Idris/REPL.hs+3−1

@@ -189,7 +189,9 @@ process fn (TotCheck n) = do i <- get

189189 _ -> return ()

190190process fn (Info n) = do i <- get

191191 let oi = lookupCtxt Nothing n (idris_optimisation i)

192− liftIO $ print oi

192+ when (not (null oi)) $ iputStrLn (show oi)

193+ let si = lookupCtxt Nothing n (idris_statics i)

194+ when (not (null si)) $ iputStrLn (show si)

193195process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

194196 ctxt <- getContext

195197 ist <- get