git.iko.soy/Idris-dev
on master help sign in
Finish WHNF for operators
a24c7d4Edwin Brady
src/Idris/Core/Evaluate.hs+9−2
compare with master
unifiedsplit
@@ -2,7 +2,7 @@
2 PatternGuards #-}
2 PatternGuards #-}
3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4
4
5−module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
5+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll, toValue, quoteTerm,
6 rt_simplify, simplify, specialise, hnf, convEq, convEq',
6 rt_simplify, simplify, specialise, hnf, convEq, convEq',
7 Def(..), CaseInfo(..), CaseDefs(..),
7 Def(..), CaseInfo(..), CaseDefs(..),
8 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),
8 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),
@@ -13,7 +13,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
13 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
13 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
14 mapDefCtxt,
14 mapDefCtxt,
15 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
15 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
16− Value(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
16+ Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
17 isUniverse) where
17 isUniverse) where
18
18
19import Debug.Trace
19import Debug.Trace
@@ -92,6 +92,13 @@ normaliseTrace tr ctxt env t
92 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []
92 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []
93 quote 0 val) initEval
93 quote 0 val) initEval
94
94
95+toValue :: Context -> Env -> TT Name -> Value
96+toValue ctxt env t
97+ = evalState (eval False ctxt [] (map finalEntry env) t []) initEval
98+
99+quoteTerm :: Value -> TT Name
100+quoteTerm val = evalState (quote 0 val) initEval
101+
95-- Return a specialised name, and an updated list of reductions available,
102-- Return a specialised name, and an updated list of reductions available,
96-- so that the caller can tell how much specialisation was achieved.
103-- so that the caller can tell how much specialisation was achieved.
97specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->
104specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->
src/Idris/Core/WHNF.hs+24−18
@@ -6,7 +6,8 @@ module Idris.Core.WHNF(whnf, WEnv) where
6
6
7import Idris.Core.TT
7import Idris.Core.TT
8import Idris.Core.CaseTree
8import Idris.Core.CaseTree
9−import Idris.Core.Evaluate
9+import Idris.Core.Evaluate hiding (quote)
10+import qualified Idris.Core.Evaluate as Evaluate
10
11
11import Debug.Trace
12import Debug.Trace
12
13
@@ -84,13 +85,9 @@ do_whnf ctxt env tm = eval env [] tm
84 Nothing -> unload wp stk
85 Nothing -> unload wp stk
85 Just (Operator _ i op) ->
86 Just (Operator _ i op) ->
86 if i <= length stk
87 if i <= length stk
87− then case runOp op (take i stk) of
88+ then case runOp env op (take i stk) (drop i stk) of
89+ Just v -> v
88− Nothing -> unload wp stk
90+ Nothing -> unload wp stk
89− -- Given that we can't apply constants
90− -- to things, and runOp only does
91− -- constants for now, this should
92− -- never happen...
93− Just v -> unload v (drop i stk)
94 else unload wp stk
91 else unload wp stk
95 _ -> unload wp stk
92 _ -> unload wp stk
96
93
@@ -98,16 +95,25 @@ do_whnf ctxt env tm = eval env [] tm
98 unload f [] = f
95 unload f [] = f
99 unload f (a : as) = unload (WApp f a) as
96 unload f (a : as) = unload (WApp f a) as
100
97
101− runOp :: ([Value] -> Maybe Value) -> Stack -> Maybe WHNF
98+ runOp :: WEnv -> ([Value] -> Maybe Value) -> Stack -> Stack -> Maybe WHNF
99+ runOp env op stk rest
102− runOp op stk = do vals <- mapM toValue stk
100+ = do vals <- mapM tmtoValue stk
103− case op vals of
101+ case op vals of
104− Just (VConstant c) -> Just (WConstant c)
102+ Just (VConstant c) -> Just $ unload (WConstant c) rest
103+ -- Operators run on values, so we have to convert back
104+ -- and forth. This is pretty ugly, but operators that
105+ -- aren't run on constants are themselves pretty ugly
106+ -- (it's prim__believe_me and prim__syntacticEq, for
107+ -- example) so let's not worry too much...
108+ Just val -> Just $ eval env rest (quoteTerm val)
105− _ -> Nothing
109+ _ -> Nothing
106−
110+
107− toValue :: (Term, WEnv) -> Maybe Value
111+ tmtoValue :: (Term, WEnv) -> Maybe Value
112+ tmtoValue (tm, tenv)
108− toValue (tm, tenv) = case eval tenv [] tm of
113+ = case eval tenv [] tm of
109− WConstant c -> Just (VConstant c)
114+ WConstant c -> Just (VConstant c)
110− _ -> Nothing
115+ _ -> let tm' = quoteEnv tenv tm in
116+ Just (toValue ctxt [] tm')
111
117
112 evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF
118 evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF
113 evalCase wenv@(WEnv d env) ns tree args
119 evalCase wenv@(WEnv d env) ns tree args