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

git.iko.soy/Idris-dev

on master help sign in

Work towards making {static} arguments and specialisation work properly

00d7c69Edwin Brady15 years ago

src/Core/Evaluate.hs+12−3

compare with master

unifiedsplit

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

19import Core.TT

20import Core.CaseTree

22−type EvalState = ()

22+type EvalState = ()

23type Eval a = State EvalState a

25data EvalOpt = Spec | HNF | Simplify | AtREPL

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

46 deriving Show

48instance Show Value where

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

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

51instance Show (a -> b) where

52 show x = "<<fn>>"

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

162 app <- apply stk top env a' as

163 wknV (-1) app

164 apply stk False env f args

165− | spec = return $ unload env f args

165+ | spec = specApply stk env f args

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

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

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

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

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

182 apply stk top env f [] = return f

183

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+

184 unload env f [] = f

193 unload env f [] = f

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

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

186

195

src/Core/TT.hs+10

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

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

396 no' i _ = True

397

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+

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

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

399

409

400arity :: TT n -> Int

410arity :: TT n -> Int

src/Idris/AbsSyntax.hs+34−11

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

400

401impl = Imp False Dynamic

402expl = Exp False Dynamic

403−constraint = Constraint False Static

403+constraint = Constraint False Dynamic

404tacimpl = TacImp False Dynamic

405

406data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen

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

1055 pri Placeholder = 1

1056 pri _ = 3

1057

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+

1058-- Dealing with implicit arguments

1082-- Dealing with implicit arguments

1059

1083

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

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

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

1066implicit syn n ptm

1090implicit syn n ptm

1067 = do i <- get

1091 = do i <- get

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

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

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

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

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

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

1071 addIBC (IBCImp n)

1095 addIBC (IBCImp n)

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

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

1073− i <- get

1097+-- i <- get

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

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

1075− addIBC (IBCStatic n)

1076− return tm''

1099+ return tm'

1077

1100

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

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

1079implicitise syn ist tm

1102implicitise syn ist tm

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

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

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

1287

1310

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

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

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

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

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

1290 runState (pos ns ss tm) []

1314 runState (pos ns ss tm) []

1291 where fs (PPi p n t sc)

1315 where fs (PPi p n t sc)

1292 | Static <- pstatic p

1316 | Static <- pstatic p

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

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

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

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

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

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

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

1320+ (ns, ss)

1297 fs _ = ([], [])

1321 fs _ = ([], [])

1298

1322

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

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

1300

1324

1301 pos ns ss (PPi p n t sc)

1325 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

1304 spos <- get

1327 spos <- get

1305 put (True : spos)

1328 put (True : spos)

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

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

src/Idris/ElabTerm.hs+14

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

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

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

216 _ ->-} args'

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

217 ivs <- get_instances

218 ivs <- get_instances

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

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

219 -- function or default definition.

220 -- function or default definition.

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

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

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

498

499

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

500solveAll = 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

189 _ -> return ()

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

191 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)

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

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

194 ctxt <- getContext

196 ctxt <- getContext

195 ist <- get

197 ist <- get