git.iko.soy/Idris-dev
on master help sign in
Finish WHNF for operators

It's a bit ugly for non-constant operators, but non-constant operators are ugly anyway, and unusual, so I'm not going to worry too much about that... This should now be good enough to use in place of the old evaluator for things which only need the constructor at the head (which includes conversion, unification and partial evaluation.)

commita24c7d4f72ca474574b45c6b1c6bbe15c8d1e082 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 24 Jul 2015, 01:43 (11 years ago) parent89566a8
2 files changed+33−20
compare with master
unifiedsplit
src/Idris/Core/Evaluate.hs+9−2 src/Idris/Core/WHNF.hs+24−18
src/Idris/Core/Evaluate.hs+9−2
@@ -2,7 +2,7 @@
22 PatternGuards #-}
33{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
44
5−module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
5+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll, toValue, quoteTerm,
66 rt_simplify, simplify, specialise, hnf, convEq, convEq',
77 Def(..), CaseInfo(..), CaseDefs(..),
88 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),
@@ -13,7 +13,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
1313 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
1414 mapDefCtxt,
1515 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
16− Value(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
16+ Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
1717 isUniverse) where
1818
1919import Debug.Trace
@@ -92,6 +92,13 @@ normaliseTrace tr ctxt env t
9292 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []
9393 quote 0 val) initEval
9494
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+
95102-- Return a specialised name, and an updated list of reductions available,
96103-- so that the caller can tell how much specialisation was achieved.
97104specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->
src/Idris/Core/WHNF.hs+24−18
@@ -6,7 +6,8 @@ module Idris.Core.WHNF(whnf, WEnv) where
66
77import Idris.Core.TT
88import Idris.Core.CaseTree
9−import Idris.Core.Evaluate
9+import Idris.Core.Evaluate hiding (quote)
10+import qualified Idris.Core.Evaluate as Evaluate
1011
1112import Debug.Trace
1213
@@ -84,13 +85,9 @@ do_whnf ctxt env tm = eval env [] tm
8485 Nothing -> unload wp stk
8586 Just (Operator _ i op) ->
8687 if i <= length stk
87− then case runOp op (take i stk) of
88− 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)
88+ then case runOp env op (take i stk) (drop i stk) of
89+ Just v -> v
90+ Nothing -> unload wp stk
9491 else unload wp stk
9592 _ -> unload wp stk
9693
@@ -98,16 +95,25 @@ do_whnf ctxt env tm = eval env [] tm
9895 unload f [] = f
9996 unload f (a : as) = unload (WApp f a) as
10097
101− runOp :: ([Value] -> Maybe Value) -> Stack -> Maybe WHNF
102− runOp op stk = do vals <- mapM toValue stk
103− case op vals of
104− Just (VConstant c) -> Just (WConstant c)
105− _ -> Nothing
106−
107− toValue :: (Term, WEnv) -> Maybe Value
108− toValue (tm, tenv) = case eval tenv [] tm of
109− WConstant c -> Just (VConstant c)
110− _ -> Nothing
98+ runOp :: WEnv -> ([Value] -> Maybe Value) -> Stack -> Stack -> Maybe WHNF
99+ runOp env op stk rest
100+ = do vals <- mapM tmtoValue stk
101+ case op vals of
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)
109+ _ -> Nothing
110+
111+ tmtoValue :: (Term, WEnv) -> Maybe Value
112+ tmtoValue (tm, tenv)
113+ = case eval tenv [] tm of
114+ WConstant c -> Just (VConstant c)
115+ _ -> let tm' = quoteEnv tenv tm in
116+ Just (toValue ctxt [] tm')
111117
112118 evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF
113119 evalCase wenv@(WEnv d env) ns tree args