git.iko.soy/Idris-dev
on master help sign in
Tinker with specialisation
4bcfa68Edwin Brady
src/Core/Evaluate.hs+121−97
compare with master
unifiedsplit
@@ -19,12 +19,15 @@ import Data.Binary hiding (get, put)
19import Core.TT
19import Core.TT
20import Core.CaseTree
20import Core.CaseTree
21
21
22−type EvalState = ()
22+data EvalState = ES { limited :: [(Name, Int)],
23+ steps :: Int }
23type Eval a = State EvalState a
24type Eval a = State EvalState a
24
25
25data EvalOpt = Spec | HNF | Simplify | AtREPL
26data EvalOpt = Spec | HNF | Simplify | AtREPL
26 deriving (Show, Eq)
27 deriving (Show, Eq)
27
28
29+initEval = ES [] 0
30+
28-- VALUES (as HOAS) ---------------------------------------------------------
31-- VALUES (as HOAS) ---------------------------------------------------------
29
32
30data Value = VP NameType Name Value
33data Value = VP NameType Name Value
@@ -46,7 +49,7 @@ data HNF = HP NameType Name (TT Name)
46 deriving Show
49 deriving Show
47
50
48instance Show Value where
51instance Show Value where
49− show x = show $ evalState (quote 100 x) ()
52+ show x = show $ evalState (quote 100 x) initEval
50
53
51instance Show (a -> b) where
54instance Show (a -> b) where
52 show x = "<<fn>>"
55 show x = "<<fn>>"
@@ -60,36 +63,36 @@ instance Show (a -> b) where
60
63
61normaliseC :: Context -> Env -> TT Name -> TT Name
64normaliseC :: Context -> Env -> TT Name -> TT Name
62normaliseC ctxt env t
65normaliseC ctxt env t
63− = evalState (do val <- eval ctxt emptyContext env t []
66+ = evalState (do val <- eval ctxt [] env t []
64− quote 0 val) ()
67+ quote 0 val) initEval
65
68
66normaliseAll :: Context -> Env -> TT Name -> TT Name
69normaliseAll :: Context -> Env -> TT Name -> TT Name
67normaliseAll ctxt env t
70normaliseAll ctxt env t
68− = evalState (do val <- eval ctxt emptyContext env t [AtREPL]
71+ = evalState (do val <- eval ctxt [] env t [AtREPL]
69− quote 0 val) ()
72+ quote 0 val) initEval
70
73
71normalise :: Context -> Env -> TT Name -> TT Name
74normalise :: Context -> Env -> TT Name -> TT Name
72normalise ctxt env t
75normalise ctxt env t
73− = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []
76+ = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) []
74− quote 0 val) ()
77+ quote 0 val) initEval
75
78
76−specialise :: Context -> Ctxt [Bool] -> TT Name -> TT Name
79+specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
77−specialise ctxt statics t
80+specialise ctxt env limits t
78− = evalState (do val <- eval ctxt statics [] (finalise t) [Spec]
81+ = evalState (do val <- eval ctxt limits (map finalEntry env) (finalise t) []
79− quote 0 val) ()
82+ quote 0 val) (initEval { limited = limits })
80
83
81-- Like normalise, but we only reduce functions that are marked as okay to
84-- Like normalise, but we only reduce functions that are marked as okay to
82-- inline (and probably shouldn't reduce lets?)
85-- inline (and probably shouldn't reduce lets?)
83
86
84simplify :: Context -> Env -> TT Name -> TT Name
87simplify :: Context -> Env -> TT Name -> TT Name
85simplify ctxt env t
88simplify ctxt env t
86− = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [Simplify]
89+ = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [Simplify]
87− quote 0 val) ()
90+ quote 0 val) initEval
88
91
89hnf :: Context -> Env -> TT Name -> TT Name
92hnf :: Context -> Env -> TT Name -> TT Name
90hnf ctxt env t
93hnf ctxt env t
91− = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]
94+ = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [HNF]
92− quote 0 val) ()
95+ quote 0 val) initEval
93
96
94
97
95-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
98-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
@@ -106,120 +109,141 @@ unbindEnv :: EnvTT n -> TT n -> TT n
106unbindEnv [] tm = tm
109unbindEnv [] tm = tm
107unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
110unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
108
111
112+usable :: Name -> [(Name, Int)] -> (Bool, [(Name, Int)])
113+usable n [] = (True, [])
114+usable n ns = case lookup n ns of
115+ Just 0 -> (False, ns)
116+ Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
117+ _ -> (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
118+
119+reduction :: Eval ()
120+reduction = do ES ns s <- get
121+ put (ES ns (s+1))
122+
109-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
123-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
110-- such as we might have during construction of a proof)
124-- such as we might have during construction of a proof)
111
125
112−eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value
126+eval :: Context -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value
113−eval ctxt statics genv tm opts = ev [] True [] tm where
127+eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
114 spec = Spec `elem` opts
128 spec = Spec `elem` opts
115 simpl = Simplify `elem` opts
129 simpl = Simplify `elem` opts
116 atRepl = AtREPL `elem` opts
130 atRepl = AtREPL `elem` opts
117
131
118− ev stk top env (P _ n ty)
132+ ev ntimes stk top env (P _ n ty)
119− | Just (Let t v) <- lookup n genv = ev stk top env v
133+ | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
134+ ev ntimes_in stk top env (P Ref n ty)
135+ | (True, ntimes) <- usable n ntimes_in
120− ev stk top env (P Ref n ty) = case lookupDefAcc Nothing n atRepl ctxt of
136+ = do let val = lookupDefAcc Nothing n atRepl ctxt
137+ case val of
121− [(Function _ tm, Public)] ->
138+ [(Function _ tm, Public)] ->
122− ev (n:stk) True env tm
139+ ev ntimes (n:stk) True env tm
123− [(TyDecl nt ty, _)] -> do vty <- ev stk True env ty
140+ [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
124− return $ VP nt n vty
141+ return $ VP nt n vty
125− [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version
142+ [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version
126− if simpl && (not inl || elem n stk)
143+ if simpl && (not inl || elem n stk)
127− then liftM (VP Ref n) (ev stk top env ty)
144+ then liftM (VP Ref n) (ev ntimes stk top env ty)
128− else do c <- evCase (n:stk) top env [] [] tree
145+ else do c <- evCase ntimes (n:stk) top env [] [] tree
129− case c of
146+ case c of
130− (Nothing, _) -> liftM (VP Ref n) (ev stk top env ty)
147+ (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
131− (Just v, _) -> return v
148+ (Just v, _) -> return v
132− _ -> liftM (VP Ref n) (ev stk top env ty)
149+ _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
133− ev stk top env (P nt n ty) = liftM (VP nt n) (ev stk top env ty)
150+ ev ntimes stk top env (P nt n ty) = liftM (VP nt n) (ev ntimes stk top env ty)
134− ev stk top env (V i) | i < length env = return $ env !! i
151+ ev ntimes stk top env (V i) | i < length env = return $ env !! i
135 | otherwise = return $ VV i
152 | otherwise = return $ VV i
136− ev stk top env (Bind n (Let t v) sc)
153+ ev ntimes stk top env (Bind n (Let t v) sc)
137− = do v' <- ev stk top env v --(finalise v)
154+ = do v' <- ev ntimes stk top env v --(finalise v)
138− sc' <- ev stk top (v' : env) sc
155+ sc' <- ev ntimes stk top (v' : env) sc
139 wknV (-1) sc'
156 wknV (-1) sc'
140− ev stk top env (Bind n (NLet t v) sc)
157+ ev ntimes stk top env (Bind n (NLet t v) sc)
141− = do t' <- ev stk top env (finalise t)
158+ = do t' <- ev ntimes stk top env (finalise t)
142− v' <- ev stk top env (finalise v)
159+ v' <- ev ntimes stk top env (finalise v)
143− sc' <- ev stk top (v' : env) sc
160+ sc' <- ev ntimes stk top (v' : env) sc
144 return $ VBind n (Let t' v') (\x -> return sc')
161 return $ VBind n (Let t' v') (\x -> return sc')
145− ev stk top env (Bind n b sc)
162+ ev ntimes stk top env (Bind n b sc)
146 = do b' <- vbind env b
163 = do b' <- vbind env b
147− return $ VBind n b' (\x -> ev stk top (x:env) sc)
164+ return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
148− where vbind env t = fmapMB (\tm -> ev stk top env (finalise tm)) t
165+ where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
149− ev stk top env (App f a) = do f' <- ev stk top env f
166+ ev ntimes stk top env (App f a)
167+ = do f' <- ev ntimes stk top env f
150− a' <- ev stk False env a
168+ a' <- ev ntimes stk False env a
151− evApply stk top env [a'] f'
169+ evApply ntimes stk top env [a'] f'
152− ev stk top env (Constant c) = return $ VConstant c
170+ ev ntimes stk top env (Constant c) = return $ VConstant c
153− ev stk top env Erased = return VErased
171+ ev ntimes stk top env Erased = return VErased
154− ev stk top env (Set i) = return $ VSet i
172+ ev ntimes stk top env (Set i) = return $ VSet i
155
173
156− evApply stk top env args (VApp f a) =
174+ evApply ntimes stk top env args (VApp f a) =
157− evApply stk top env (a:args) f
175+ evApply ntimes stk top env (a:args) f
158− evApply stk top env args f = apply stk top env f args
176+ evApply ntimes stk top env args f = apply ntimes stk top env f args
159
177
160− apply stk top env (VBind n (Lam t) sc) (a:as)
178+ apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
161 = do a' <- sc a
179 = do a' <- sc a
162− app <- apply stk top env a' as
180+ app <- apply ntimes stk top env a' as
163 wknV (-1) app
181 wknV (-1) app
164− apply stk False env f args
182+-- apply ntimes stk False env f args
165− | spec = specApply stk env f args
183+-- | spec = specApply ntimes stk env f args
166− apply stk top env (VP Ref n ty) args
184+ apply ntimes_in stk top env f@(VP Ref n ty) args
185+ | (True, ntimes) <- usable n ntimes_in
167− | [(CaseOp inl _ _ ns tree _ _, Public)] <- lookupDefAcc Nothing n atRepl ctxt
186+ = do let val = lookupDefAcc Nothing n atRepl ctxt
168− = -- traceWhen (n == UN ["interp"]) (show (n, args)) $
187+ case val of
188+ [(CaseOp inl _ _ ns tree _ _, Public)] ->
169− if simpl && (not inl || elem n stk)
189+ if simpl && (not inl || elem n stk)
170− then return $ unload env (VP Ref n ty) args
190+ then return $ unload env (VP Ref n ty) args
171− else do c <- evCase (n:stk) top env ns args tree
191+ else do c <- evCase ntimes (n:stk) top env ns args tree
172− case c of
192+ case c of
173− (Nothing, _) -> return $ unload env (VP Ref n ty) args
193+ (Nothing, _) -> return $ unload env (VP Ref n ty) args
174− (Just v, rest) -> evApply stk top env rest v
194+ (Just v, rest) -> evApply ntimes stk top env rest v
175− | [Operator _ i op] <- lookupDef Nothing n ctxt
195+ [(Operator _ i op, _)] ->
176− = if (i <= length args)
196+ if (i <= length args)
177− then case op (take i args) of
197+ then case op (take i args) of
178− Nothing -> return $ unload env (VP Ref n ty) args
198+ Nothing -> return $ unload env (VP Ref n ty) args
179− Just v -> evApply stk top env (drop i args) v
199+ Just v -> evApply ntimes stk top env (drop i args) v
180− else return $ unload env (VP Ref n ty) args
200+ else return $ unload env (VP Ref n ty) args
201+ _ -> case args of
202+ [] -> return f
203+ _ -> return $ unload env f args
181− apply stk top env f (a:as) = return $ unload env f (a:as)
204+ apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
182− apply stk top env f [] = return f
205+ apply ntimes stk top env f [] = return f
183−
206+
184− specApply stk env f@(VP Ref n ty) args
207+-- specApply stk env f@(VP Ref n ty) args
185− = case lookupCtxt Nothing n statics of
208+-- = case lookupCtxt Nothing n statics of
186− [as] -> if or as
209+-- [as] -> if or as
187− then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
210+-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
188− return $ unload env f args
211+-- return $ unload env f args
189− else return $ unload env f args
212+-- else return $ unload env f args
190− _ -> return $ unload env f args
213+-- _ -> return $ unload env f args
191− specApply stk env f args = return $ unload env f args
214+-- specApply stk env f args = return $ unload env f args
192
215
193 unload env f [] = f
216 unload env f [] = f
194 unload env f (a:as) = unload env (VApp f a) as
217 unload env f (a:as) = unload env (VApp f a) as
195
218
196− evCase stk top env ns args tree
219+ evCase ntimes stk top env ns args tree
197 | length ns <= length args
220 | length ns <= length args
198 = do let args' = take (length ns) args
221 = do let args' = take (length ns) args
199 let rest = drop (length ns) args
222 let rest = drop (length ns) args
200− t <- evTree stk top env (zipWith (\n t -> (n, t)) ns args') tree
223+ t <- evTree ntimes stk top env (zipWith (\n t -> (n, t)) ns args') tree
201 return (t, rest)
224 return (t, rest)
202 | otherwise = return (Nothing, args)
225 | otherwise = return (Nothing, args)
203
226
227+ evTree :: [(Name, Int)] -> [Name] -> Bool ->
204− evTree :: [Name] -> Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
228+ [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
205− evTree stk top env amap (UnmatchedCase str) = return Nothing
229+ evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing
206− evTree stk top env amap (STerm tm)
230+ evTree ntimes stk top env amap (STerm tm)
207 = do let etm = pToVs (map fst amap) tm
231 = do let etm = pToVs (map fst amap) tm
208− etm' <- ev stk top (map snd amap ++ env) etm
232+ etm' <- ev ntimes stk top (map snd amap ++ env) etm
209 return $ Just etm'
233 return $ Just etm'
210− evTree stk top env amap (Case n alts)
234+ evTree ntimes stk top env amap (Case n alts)
211 = case lookup n amap of
235 = case lookup n amap of
212 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
236 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
213 case c of
237 case c of
214− Just (altmap, sc) -> evTree stk top env altmap sc
238+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc
215− _ -> do c' <- chooseAlt' stk env v (getValArgs v) alts amap
239+ _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
216 case c' of
240 case c' of
217− Just (altmap, sc) -> evTree stk top env altmap sc
241+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc
218 _ -> return Nothing
242 _ -> return Nothing
219 _ -> return Nothing
243 _ -> return Nothing
220
244
221− chooseAlt' stk env _ (f, args) alts amap
245+ chooseAlt' ntimes stk env _ (f, args) alts amap
222− = do f' <- apply stk True env f args
246+ = do f' <- apply ntimes stk True env f args
223 chooseAlt env f' (getValArgs f') alts amap
247 chooseAlt env f' (getValArgs f') alts amap
224
248
225 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
249 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
@@ -571,7 +595,7 @@ initContext = MkContext [] 0 emptyContext
571ctxtAlist :: Context -> [(Name, Def)]
595ctxtAlist :: Context -> [(Name, Def)]
572ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
596ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
573
597
574−veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()
598+veval ctxt env t = evalState (eval ctxt [] env t []) initEval
575
599
576addToCtxt :: Name -> Term -> Type -> Context -> Context
600addToCtxt :: Name -> Term -> Type -> Context -> Context
577addToCtxt n tm ty uctxt
601addToCtxt n tm ty uctxt
src/Core/ProofState.hs+1−1
@@ -284,7 +284,7 @@ fill _ _ _ _ = fail "Can't fill here."
284
284
285prep_fill :: Name -> [Name] -> RunTactic
285prep_fill :: Name -> [Name] -> RunTactic
286prep_fill f as ctxt env (Bind x (Hole ty) sc) =
286prep_fill f as ctxt env (Bind x (Hole ty) sc) =
287− do let val = mkApp (P Ref f undefined) (map (\n -> P Ref n undefined) as)
287+ do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
288 return $ Bind x (Guess ty val) sc
288 return $ Bind x (Guess ty val) sc
289prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
289prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
290
290
src/Idris/AbsSyntax.hs+2−1
@@ -404,6 +404,7 @@ constraint = Constraint False Dynamic
404tacimpl = TacImp False Dynamic
404tacimpl = TacImp False Dynamic
405
405
406data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
406data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
407+ | Specialise [Name] -- specialise it, freeze these names
407 deriving (Show, Eq)
408 deriving (Show, Eq)
408{-!
409{-!
409deriving instance Binary FnOpt
410deriving instance Binary FnOpt
@@ -752,7 +753,7 @@ getAll = map getTm
752showImp :: Bool -> PTerm -> String
753showImp :: Bool -> PTerm -> String
753showImp impl tm = se 10 tm where
754showImp impl tm = se 10 tm where
754 se p (PQuote r) = "![" ++ show r ++ "]"
755 se p (PQuote r) = "![" ++ show r ++ "]"
755− se p (PRef fc n) = if impl then show n ++ "[" ++ show fc ++ "]"
756+ se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
756 else showbasic n
757 else showbasic n
757 where showbasic n@(UN _) = show n
758 where showbasic n@(UN _) = show n
758 showbasic (MN _ s) = s
759 showbasic (MN _ s) = s
src/Idris/ElabDecls.hs+2−2
@@ -293,8 +293,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
293 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
293 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
294 i <- get
294 i <- get
295 case lookupDef Nothing n (tt_ctxt i) of
295 case lookupDef Nothing n (tt_ctxt i) of
296− (CaseOp _ _ _ _ sc _ _ : _) ->
296+ (CaseOp _ _ _ scargs sc _ _ : _) ->
297− do let ns = namesUsed sc
297+ do let ns = namesUsed sc \\ scargs
298 logLvl 2 $ "Called names: " ++ show ns
298 logLvl 2 $ "Called names: " ++ show ns
299 addToCG n ns
299 addToCG n ns
300 addIBC (IBCCG n)
300 addIBC (IBCCG n)
src/Idris/ElabTerm.hs+42−11
@@ -210,11 +210,11 @@ elab ist info pattern tcgen fn tm
210-- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist)
210-- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist)
211-- = let dsl' = expandDo d (getTm arg) in
211-- = let dsl' = expandDo d (getTm arg) in
212-- trace (show dsl') $ elab' ina dsl'
212-- trace (show dsl') $ elab' ina dsl'
213− elab' (ina, g) (PApp fc (PRef _ f) args')
213+ elab' (ina, g) tm@(PApp fc (PRef _ f) args')
214 = do let args = {- case lookupCtxt f (inblock info) of
214 = do let args = {- case lookupCtxt f (inblock info) of
215 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
215 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
216 _ ->-} args'
216 _ ->-} args'
217− mkSpecialised ist fc f (map getTm args')
217+-- newtm <- mkSpecialised ist fc f (map getTm args') tm
218 ivs <- get_instances
218 ivs <- get_instances
219 -- 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
220 -- function or default definition.
220 -- function or default definition.
@@ -222,7 +222,6 @@ elab ist info pattern tcgen fn tm
222 ctxt <- get_context
222 ctxt <- get_context
223 let guarded = isConName Nothing f ctxt
223 let guarded = isConName Nothing f ctxt
224 try (do ns <- apply (Var f) (map isph args)
224 try (do ns <- apply (Var f) (map isph args)
225− solve
226 let (ns', eargs)
225 let (ns', eargs)
227 = unzip $
226 = unzip $
228 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))
227 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))
@@ -231,8 +230,11 @@ elab ist info pattern tcgen fn tm
231 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))
230 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))
232 (elabArgs (ina || not isinf, guarded)
231 (elabArgs (ina || not isinf, guarded)
233 [] False (reverse ns')
232 [] False (reverse ns')
234− (map (\x -> (lazyarg x, getTm x)) (reverse eargs))))
233+ (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))
234+ mkSpecialised ist fc f (map getTm args') tm
235+ solve)
235 (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)
236 (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)
237+ mkSpecialised ist fc f (map getTm args') tm
236 solve)
238 solve)
237 ivs' <- get_instances
239 ivs' <- get_instances
238 when (not pattern || (ina && not tcgen)) $
240 when (not pattern || (ina && not tcgen)) $
@@ -503,11 +505,40 @@ solveAll = try (do solve; solveAll) (return ())
503-- top level function by normalising the application
505-- top level function by normalising the application
504-- and elaborating the new expression.
506-- and elaborating the new expression.
505
507
506−mkSpecialised :: IState -> FC -> Name -> [PTerm] -> ElabD ()
508+mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm
507−mkSpecialised i fc n args
509+mkSpecialised i fc n args def
510+ = do let tm' = def
508− = case lookupCtxt Nothing n (idris_statics i) of
511+ case lookupCtxt Nothing n (idris_statics i) of
509− [] -> return ()
512+ [] -> return tm'
510− [as] -> if (not (or as)) then return () else
513+ [as] -> if (not (or as)) then return tm' else
514+ mkSpecDecl i n (zip args as) tm'
515+
516+mkSpecDecl :: IState -> Name -> [(PTerm, Bool)] -> PTerm -> ElabD PTerm
517+mkSpecDecl i n pargs tm'
518+ = do t <- goal
519+ g <- get_guess
520+ let (f, args) = unApply g
521+ let sargs = zip args (map snd pargs)
522+ let staticArgs = map fst (filter (\ (_,x) -> x) sargs)
523+ let ns = group (sort (concatMap staticFnNames staticArgs))
524+ let ntimes = map (\xs -> (head xs, length xs - 1)) ns
525+ if (not (null ns)) then
526+ do env <- get_env
527+ let g' = g -- specialise ctxt env ntimes g
528+ return tm'
511− do return () -- trace (show (n, args)) $ return ()
529+-- trace (show t ++ "\n" ++
512−
530+-- show ntimes ++ "\n" ++
531+-- show (delab i g) ++ "\n" ++ show (delab i g')) $ return tm' -- TODO
532+ else return tm'
533+ where
534+ ctxt = tt_ctxt i
535+ cg = idris_callgraph i
536+
537+ staticFnNames tm | (P _ f _, as) <- unApply tm
538+ = if not (isFnName Nothing f ctxt) then []
539+ else case lookupCtxt Nothing f cg of
540+ [ns] -> f : f : [] --(ns \\ [f])
541+ [] -> [f,f]
542+ _ -> []
543+ staticFnNames _ = []
513
544
src/Idris/IBC.hs+4
@@ -704,6 +704,8 @@ instance Binary FnOpt where
704 TotalFn -> putWord8 1
704 TotalFn -> putWord8 1
705 TCGen -> putWord8 2
705 TCGen -> putWord8 2
706 AssertTotal -> putWord8 3
706 AssertTotal -> putWord8 3
707+ Specialise x -> do putWord8 4
708+ put x
707 get
709 get
708 = do i <- getWord8
710 = do i <- getWord8
709 case i of
711 case i of
@@ -711,6 +713,8 @@ instance Binary FnOpt where
711 1 -> return TotalFn
713 1 -> return TotalFn
712 2 -> return TCGen
714 2 -> return TCGen
713 3 -> return AssertTotal
715 3 -> return AssertTotal
716+ 4 -> do x <- get
717+ return (Specialise x)
714 _ -> error "Corrupted binary data for FnOpt"
718 _ -> error "Corrupted binary data for FnOpt"
715
719
716instance Binary Fixity where
720instance Binary Fixity where
src/Idris/Parser.hs+4
@@ -615,6 +615,10 @@ pAccessibility
615pFnOpts :: IParser [FnOpt]
615pFnOpts :: IParser [FnOpt]
616pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)
616pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)
617 <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs)
617 <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs)
618+ <|> do lchar '%'; reserved "specialise";
619+ lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'
620+ xs <- pFnOpts
621+ return (Specialise ns : xs)
618 <|> return []
622 <|> return []
619
623
620addAcc :: Name -> Maybe Accessibility -> IParser ()
624addAcc :: Name -> Maybe Accessibility -> IParser ()
src/Idris/REPL.hs+1−1
@@ -195,7 +195,7 @@ process fn (Info n) = do i <- get
195process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
195process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
196 ctxt <- getContext
196 ctxt <- getContext
197 ist <- get
197 ist <- get
198− let tm' = specialise ctxt (idris_statics ist) tm
198+ let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm
199 iputStrLn (show (delab ist tm'))
199 iputStrLn (show (delab ist tm'))
200process fn (Prove n) = do prover (lit fn) n
200process fn (Prove n) = do prover (lit fn) n
201 -- recheck totality
201 -- recheck totality