git.iko.soy/Idris-dev
on fb3160e help sign in
Idris-dev/src/Core/Evaluate.hs
596 lines 25 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
4module Core.Evaluate(normalise, normaliseC, normaliseAll,
5 simplify, specialise, hnf,
6 Def(..), Accessibility(..),
7 Context, initContext, ctxtAlist, uconstraints, next_tvar,
8 addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype,
9 addCasedef, addOperator,
10 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv, isConName,
11 Value(..)) where
13import Debug.Trace
14import Control.Monad.State
15import qualified Data.Binary as B
16import Data.Binary hiding (get, put)
18import Core.TT
19import Core.CaseTree
21type EvalState = ()
22type Eval a = State EvalState a
24data EvalOpt = Spec | HNF | Simplify | AtREPL
25 deriving (Show, Eq)
27-- VALUES (as HOAS) ---------------------------------------------------------
29data Value = VP NameType Name Value
30 | VV Int
31 | VBind Name (Binder Value) (Value -> Eval Value)
32 | VApp Value Value
33 | VSet UExp
34 | VErased
35 | VConstant Const
36 | VTmp Int
38data HNF = HP NameType Name (TT Name)
39 | HV Int
40 | HBind Name (Binder HNF) (HNF -> Eval HNF)
41 | HApp HNF [HNF] [TT Name]
42 | HSet UExp
43 | HConstant Const
44 | HTmp Int
45 deriving Show
47instance Show Value where
48 show x = show $ evalState (quote 10 x) ()
50instance Show (a -> b) where
51 show x = "<<fn>>"
53-- THE EVALUATOR ------------------------------------------------------------
55-- The environment is assumed to be "locally named" - i.e., not de Bruijn
56-- indexed.
57-- i.e. it's an intermediate environment that we have while type checking or
58-- while building a proof.
60normaliseC :: Context -> Env -> TT Name -> TT Name
61normaliseC ctxt env t
62 = evalState (do val <- eval ctxt emptyContext env t []
63 quote 0 val) ()
65normaliseAll :: Context -> Env -> TT Name -> TT Name
66normaliseAll ctxt env t
67 = evalState (do val <- eval ctxt emptyContext env t [AtREPL]
68 quote 0 val) ()
70normalise :: Context -> Env -> TT Name -> TT Name
71normalise ctxt env t
72 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []
73 quote 0 val) ()
75specialise :: Context -> Ctxt [Bool] -> TT Name -> TT Name
76specialise ctxt statics t
77 = evalState (do val <- eval ctxt statics [] (finalise t) [Spec]
78 quote 0 val) ()
80-- Like normalise, but we only reduce functions that are marked as okay to
81-- inline (and probably shouldn't reduce lets?)
83simplify :: Context -> Env -> TT Name -> TT Name
84simplify ctxt env t
85 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [Simplify]
86 quote 0 val) ()
88hnf :: Context -> Env -> TT Name -> TT Name
89hnf ctxt env t
90 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]
91 quote 0 val) ()
94-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
96finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
97finalEntry (n, b) = (n, fmap finalise b)
99bindEnv :: EnvTT n -> TT n -> TT n
100bindEnv [] tm = tm
101bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
102bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
104unbindEnv :: EnvTT n -> TT n -> TT n
105unbindEnv [] tm = tm
106unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
108-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
109-- such as we might have during construction of a proof)
111eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value
112eval ctxt statics genv tm opts = ev [] True [] tm where
113 spec = Spec `elem` opts
114 simpl = Simplify `elem` opts
115 atRepl = AtREPL `elem` opts
117 ev stk top env (P _ n ty)
118 | Just (Let t v) <- lookup n genv = ev stk top env v
119 ev stk top env (P Ref n ty) = case lookupDefAcc Nothing n atRepl ctxt of
120 [(Function _ tm, Public)] ->
121 ev (n:stk) True env tm
122 [(TyDecl nt ty, _)] -> do vty <- ev stk True env ty
123 return $ VP nt n vty
124 [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version
125 if simpl && (not inl || elem n stk)
126 then liftM (VP Ref n) (ev stk top env ty)
127 else do c <- evCase (n:stk) top env [] [] tree
128 case c of
129 (Nothing, _) -> liftM (VP Ref n) (ev stk top env ty)
130 (Just v, _) -> return v
131 _ -> liftM (VP Ref n) (ev stk top env ty)
132 ev stk top env (P nt n ty) = liftM (VP nt n) (ev stk top env ty)
133 ev stk top env (V i) | i < length env = return $ env !! i
134 | otherwise = return $ VV i
135 ev stk top env (Bind n (Let t v) sc)
136 = do v' <- ev stk top env v --(finalise v)
137 sc' <- ev stk top (v' : env) sc
138 wknV (-1) sc'
139 ev stk top env (Bind n (NLet t v) sc)
140 = do t' <- ev stk top env (finalise t)
141 v' <- ev stk top env (finalise v)
142 sc' <- ev stk top (v' : env) sc
143 return $ VBind n (Let t' v') (\x -> return sc')
144 ev stk top env (Bind n b sc)
145 = do b' <- vbind env b
146 return $ VBind n b' (\x -> ev stk top (x:env) sc)
147 where vbind env t = fmapMB (\tm -> ev stk top env (finalise tm)) t
148 ev stk top env (App f a) = do f' <- ev stk top env f
149 a' <- ev stk False env a
150 evApply stk top env [a'] f'
151 ev stk top env (Constant c) = return $ VConstant c
152 ev stk top env Erased = return VErased
153 ev stk top env (Set i) = return $ VSet i
155 evApply stk top env args (VApp f a) =
156 evApply stk top env (a:args) f
157 evApply stk top env args f = apply stk top env f args
159 apply stk top env (VBind n (Lam t) sc) (a:as)
160 = do a' <- sc a
161 app <- apply stk top env a' as
162 wknV (-1) app
163 apply stk False env f args
164 | spec = return $ unload env f args
165 apply stk top env (VP Ref n ty) args
166 | [(CaseOp inl _ _ ns tree _ _, Public)] <- lookupDefAcc Nothing n atRepl ctxt
167 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $
168 if simpl && (not inl || elem n stk)
169 then return $ unload env (VP Ref n ty) args
170 else do c <- evCase (n:stk) top env ns args tree
171 case c of
172 (Nothing, _) -> return $ unload env (VP Ref n ty) args
173 (Just v, rest) -> evApply stk top env rest v
174 | [Operator _ i op] <- lookupDef Nothing n ctxt
175 = if (i <= length args)
176 then case op (take i args) of
177 Nothing -> return $ unload env (VP Ref n ty) args
178 Just v -> evApply stk top env (drop i args) v
179 else return $ unload env (VP Ref n ty) args
180 apply stk top env f (a:as) = return $ unload env f (a:as)
181 apply stk top env f [] = return f
183 unload env f [] = f
184 unload env f (a:as) = unload env (VApp f a) as
186 evCase stk top env ns args tree
187 | length ns <= length args
188 = do let args' = take (length ns) args
189 let rest = drop (length ns) args
190 t <- evTree stk top env (zipWith (\n t -> (n, t)) ns args') tree
191 return (t, rest)
192 | otherwise = return (Nothing, args)
194 evTree :: [Name] -> Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
195 evTree stk top env amap (UnmatchedCase str) = return Nothing
196 evTree stk top env amap (STerm tm)
197 = do let etm = pToVs (map fst amap) tm
198 etm' <- ev stk top (map snd amap ++ env) etm
199 return $ Just etm'
200 evTree stk top env amap (Case n alts)
201 = case lookup n amap of
202 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
203 case c of
204 Just (altmap, sc) -> evTree stk top env altmap sc
205 _ -> do c' <- chooseAlt' stk env v (getValArgs v) alts amap
206 case c' of
207 Just (altmap, sc) -> evTree stk top env altmap sc
208 _ -> return Nothing
209 _ -> return Nothing
211 chooseAlt' stk env _ (f, args) alts amap
212 = do f' <- apply stk True env f args
213 chooseAlt env f' (getValArgs f') alts amap
215 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
216 Eval (Maybe ([(Name, Value)], SC))
217 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
218 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
219 | Just v <- findDefault alts = return $ Just (amap, v)
220 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
221 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
222 | Just v <- findDefault alts = return $ Just (amap, v)
223 chooseAlt env _ (VConstant c, []) alts amap
224 | Just v <- findConst c alts = return $ Just (amap, v)
225 | Just v <- findDefault alts = return $ Just (amap, v)
226 chooseAlt _ _ _ _ _ = return Nothing
228 -- Replace old variable names in the map with new matches
229 -- (This is possibly unnecessary since we make unique names and don't
230 -- allow repeated variables...?)
231 updateAmap newm amap
232 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
233 findTag i [] = Nothing
234 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
235 findTag i (_ : xs) = findTag i xs
237 findDefault [] = Nothing
238 findDefault (DefaultCase sc : xs) = Just sc
239 findDefault (_ : xs) = findDefault xs
241 findConst c [] = Nothing
242 findConst c (ConstCase c' v : xs) | c == c' = Just v
243 findConst IType (ConCase n 1 [] v : xs) = Just v
244 findConst FlType (ConCase n 2 [] v : xs) = Just v
245 findConst ChType (ConCase n 3 [] v : xs) = Just v
246 findConst StrType (ConCase n 4 [] v : xs) = Just v
247 findConst PtrType (ConCase n 5 [] v : xs) = Just v
248 findConst c (_ : xs) = findConst c xs
250 getValArgs tm = getValArgs' tm []
251 getValArgs' (VApp f a) as = getValArgs' f (a:as)
252 getValArgs' f as = (f, as)
254class Quote a where
255 quote :: Int -> a -> Eval (TT Name)
257instance Quote Value where
258 quote i (VP nt n v) = liftM (P nt n) (quote i v)
259 quote i (VV x) = return $ V x
260 quote i (VBind n b sc) = do sc' <- sc (VTmp i)
261 b' <- quoteB b
262 liftM (Bind n b') (quote (i+1) sc')
263 where quoteB t = fmapMB (quote i) t
264 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
265 quote i (VSet u) = return $ Set u
266 quote i VErased = return $ Erased
267 quote i (VConstant c) = return $ Constant c
268 quote i (VTmp x) = return $ V (i - x - 1)
270instance Quote HNF where
271 quote i (HP nt n t) = return (P nt n t)
272 quote i (HV x) = return $ V x
273 quote i (HBind n b sc) = do sc' <- sc (HTmp i)
274 b' <- quoteB b
275 liftM (Bind n b') (quote (i+1) sc')
276 where quoteB t = fmapMB (quote i) t
277 quote i (HApp f env as) = do f' <- quote i f
278 as' <- mapM (iEnv env) as
279 return $ mkApp f' as'
280 where iEnv [] a = return a
281 iEnv (x:xs) a = do x' <- quote i x
282 iEnv xs (weakenTm (-1) (instantiate x' a))
283 quote i (HSet u) = return $ Set u
284 quote i (HConstant c) = return $ Constant c
285 quote i (HTmp x) = return $ V (i - x - 1)
287wknV :: Int -> Value -> Eval Value
288wknV i (VV x) = return $ VV (x + i)
289wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
290 return $ VBind n b' (\x -> do x' <- sc x
291 wknV i x')
292wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
293wknV i t = return t
295wknH :: Int -> HNF -> Eval HNF
296wknH i (HV x) = return $ HV (x + i)
297wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
298 return $ HBind n b' (\x -> do x' <- sc x
299 wknH i x')
300wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
301 (return as)
302wknH i t = return t
304-- HEAD NORMAL FORM ---------------------------------------------------------
306eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
307eval_hnf ctxt statics genv tm = ev [] tm where
308 ev :: [HNF] -> TT Name -> Eval HNF
309 ev env (P _ n ty)
310 | Just (Let t v) <- lookup n genv = ev env v
311 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of
312 [Function _ t] -> ev env t
313 [TyDecl nt ty] -> return $ HP nt n ty
314 [CaseOp inl _ _ [] tree _ _] ->
315 do c <- evCase env [] [] tree
316 case c of
317 (Nothing, _, _) -> return $ HP Ref n ty
318 (Just v, _, _) -> return v
319 _ -> return $ HP Ref n ty
320 ev env (P nt n ty) = return $ HP nt n ty
321 ev env (V i) | i < length env = return $ env !! i
322 | otherwise = return $ HV i
323 ev env (Bind n (Let t v) sc)
324 = do v' <- ev env (finalise v)
325 sc' <- ev (v' : env) sc
326 wknH (-1) sc'
327 ev env (Bind n b sc)
328 = do b' <- hbind env b
329 return $ HBind n b' (\x -> ev (x : env) sc)
330 where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
331 ev env (App f a) = evApply env [a] f
332 ev env (Constant c) = return $ HConstant c
333 ev env (Set i) = return $ HSet i
335 evApply env args (App f a) = evApply env (a : args) f
336 evApply env args f = do f' <- ev env f
337 apply env f' args
339 apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
340 sc' <- sc a'
341 app <- apply env sc' as
342 wknH (-1) app
343 apply env (HP Ref n ty) args
344 | [CaseOp _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt
345 = do c <- evCase env ns args tree
346 case c of
347 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
348 (Just v, rest, env') -> do v' <- quote 0 v
349 apply env' v rest
350-- | Just (Operator _ i op) <- lookupDef n ctxt
351-- = if (i <= length args)
352-- then case op (take i args) of
353-- Nothing -> return $ unload env (HP Ref n ty) args
354-- Just v -> evApply env (drop i args) v
355-- else return $ unload env (HP Ref n ty) args
356 apply env f (a:as) = return $ unload env f (a:as)
357 apply env f [] = return f
359 unload env f [] = f
360 unload env f as = HApp f env as
362 evCase env ns args tree
363 | length ns <= length args
364 = do let args' = take (length ns) args
365 let rest = drop (length ns) args
366 (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
367 return (t, rest, env')
368 | otherwise = return (Nothing, args, env)
370 evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
371 evTree env amap (UnmatchedCase str) = return (Nothing, env)
372 evTree env amap (STerm tm)
373 = do let etm = pToVs (map fst amap) tm
374 amap' <- mapM (ev env) (map snd amap)
375 envw <- mapM (wknH (length amap)) env
376 let env' = amap' ++ envw
377 etm' <- trace (show etm) $ ev env' etm
378 etmq <- quote 0 etm'
379 trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
380 evTree env amap (Case n alts)
381 = case lookup n amap of
382 Just v -> do v' <- ev env v
383 case chooseAlt v' (getValArgs v') alts amap of
384 Just (altmap, sc) -> evTree env altmap sc
385 _ -> return (Nothing, env)
387 chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
388 [CaseAlt] -> [(Name, TT Name)] ->
389 Maybe ([(Name, TT Name)], SC)
390 chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
391 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
392 | Just v <- findDefault alts = Just (amap, v)
393 chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
394 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
395 | Just v <- findDefault alts = Just (amap, v)
396 chooseAlt _ (HConstant c, env, []) alts amap
397 | Just v <- findConst c alts = Just (amap, v)
398 | Just v <- findDefault alts = Just (amap, v)
399 chooseAlt _ _ _ _ = Nothing
401 -- Replace old variable names in the map with new matches
402 -- (This is possibly unnecessary since we make unique names and don't
403 -- allow repeated variables...?)
404 updateAmap newm amap
405 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
406 findTag i [] = Nothing
407 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
408 findTag i (_ : xs) = findTag i xs
410 findDefault [] = Nothing
411 findDefault (DefaultCase sc : xs) = Just sc
412 findDefault (_ : xs) = findDefault xs
414 findConst c [] = Nothing
415 findConst c (ConstCase c' v : xs) | c == c' = Just v
416 findConst IType (ConCase n 1 [] v : xs) = Just v
417 findConst FlType (ConCase n 2 [] v : xs) = Just v
418 findConst ChType (ConCase n 3 [] v : xs) = Just v
419 findConst StrType (ConCase n 4 [] v : xs) = Just v
420 findConst PtrType (ConCase n 5 [] v : xs) = Just v
421 findConst c (_ : xs) = findConst c xs
423 getValArgs (HApp t env args) = (t, env, args)
424 getValArgs t = (t, [], [])
426-- SPECIALISATION -----------------------------------------------------------
427-- We need too much control to be able to do this by tweaking the main
428-- evaluator
430spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
431spec ctxt statics genv tm = error "spec undefined"
433-- CONTEXTS -----------------------------------------------------------------
435{- A definition is either a simple function (just an expression with a type),
436 a constant, which could be a data or type constructor, an axiom or as an
437 yet undefined function, or an Operator.
438 An Operator is a function which explains how to reduce.
439 A CaseOp is a function defined by a simple case tree -}
441data Def = Function Type Term
442 | TyDecl NameType Type
443 | Operator Type Int ([Value] -> Maybe Value)
444 | CaseOp Bool Type [(Term, Term)] -- Bool for inlineable
445 [Name] SC -- Compile time case definition
446 [Name] SC -- Run time cae definitions
447{-!
448deriving instance Binary Def
449!-}
451instance Show Def where
452 show (Function ty tm) = "Function: " ++ show (ty, tm)
453 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
454 show (Operator ty _ _) = "Operator: " ++ show ty
455 show (CaseOp _ ty ps ns sc ns' sc')
456 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
457 show ns ++ " " ++ show sc ++ "\n" ++
458 show ns' ++ " " ++ show sc'
459-- We need this for serialising Def. Fortunately, it never gets used because
460-- we'll never serialise a primitive operator
462instance Binary (a -> b) where
463 put x = return ()
464 get = error "Getting a function"
466-------
468-- Frozen => doesn't reduce
469-- Hidden => doesn't reduce and invisible to type checker
471data Accessibility = Public | Frozen | Hidden
472 deriving (Show, Eq)
473{-!
474deriving instance Binary Accessibility
475!-}
477data Context = MkContext { uconstraints :: [UConstraint],
478 next_tvar :: Int,
479 definitions :: Ctxt (Def, Accessibility) }
481initContext = MkContext [] 0 emptyContext
483ctxtAlist :: Context -> [(Name, Def)]
484ctxtAlist ctxt = map (\(n, (d, a)) -> (n, d)) $ toAlist (definitions ctxt)
486veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()
488addToCtxt :: Name -> Term -> Type -> Context -> Context
489addToCtxt n tm ty uctxt
490 = let ctxt = definitions uctxt
491 ctxt' = addDef n (Function ty tm, Public) ctxt in
492 uctxt { definitions = ctxt' }
494setAccess :: Name -> Accessibility -> Context -> Context
495setAccess n a uctxt
496 = let ctxt = definitions uctxt
497 ctxt' = updateDef n (\ (d, _) -> (d, a)) ctxt in
498 uctxt { definitions = ctxt' }
500addCtxtDef :: Name -> Def -> Context -> Context
501addCtxtDef n d c = let ctxt = definitions c
502 ctxt' = addDef n (d, Public) ctxt in
503 c { definitions = ctxt' }
505addTyDecl :: Name -> Type -> Context -> Context
506addTyDecl n ty uctxt
507 = let ctxt = definitions uctxt
508 ctxt' = addDef n (TyDecl Ref ty, Public) ctxt in
509 uctxt { definitions = ctxt' }
511addDatatype :: Datatype Name -> Context -> Context
512addDatatype (Data n tag ty cons) uctxt
513 = let ctxt = definitions uctxt
514 ty' = normalise uctxt [] ty
515 ctxt' = addCons 0 cons (addDef n
516 (TyDecl (TCon tag (arity ty')) ty, Public) ctxt) in
517 uctxt { definitions = ctxt' }
518 where
519 addCons tag [] ctxt = ctxt
520 addCons tag ((n, ty) : cons) ctxt
521 = let ty' = normalise uctxt [] ty in
522 addCons (tag+1) cons (addDef n
523 (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)
525addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->
526 Type -> Context -> Context
527addCasedef n alwaysInline tcase covering ps psrt ty uctxt
528 = let ctxt = definitions uctxt
529 ps' = ps -- simpl ps in
530 ctxt' = case (simpleCase tcase covering ps',
531 simpleCase tcase covering psrt) of
532 (CaseDef args sc _, CaseDef args' sc' _) ->
533 let inl = alwaysInline in
534 addDef n (CaseOp inl ty ps args sc args' sc',
535 Public) ctxt in
536 uctxt { definitions = ctxt' }
537 where simpl [] = []
538 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs
540addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context
541addOperator n ty a op uctxt
542 = let ctxt = definitions uctxt
543 ctxt' = addDef n (Operator ty a op, Public) ctxt in
544 uctxt { definitions = ctxt' }
546lookupTy :: Maybe [String] -> Name -> Context -> [Type]
547lookupTy root n ctxt
548 = do def <- lookupCtxt root n (definitions ctxt)
549 case fst def of
550 (Function ty _) -> return ty
551 (TyDecl _ ty) -> return ty
552 (Operator ty _ _) -> return ty
553 (CaseOp _ ty _ _ _ _ _) -> return ty
555isConName :: Maybe [String] -> Name -> Context -> Bool
556isConName root n ctxt
557 = or $ do def <- lookupCtxt root n (definitions ctxt)
558 case fst def of
559 (TyDecl (DCon _ _) _) -> return True
560 (TyDecl (TCon _ _) _) -> return True
561 _ -> return False
563lookupP :: Maybe [String] -> Name -> Context -> [Term]
564lookupP root n ctxt
565 = do def <- lookupCtxt root n (definitions ctxt)
566 p <- case def of
567 (Function ty tm, a) -> return (P Ref n ty, a)
568 (TyDecl nt ty, a) -> return (P nt n ty, a)
569 (CaseOp _ ty _ _ _ _ _, a) -> return (P Ref n ty, a)
570 (Operator ty _ _, a) -> return (P Ref n ty, a)
571 case snd p of
572 Hidden -> []
573 _ -> return (fst p)
575lookupDef :: Maybe [String] -> Name -> Context -> [Def]
576lookupDef root n ctxt = map fst $ lookupCtxt root n (definitions ctxt)
578lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context -> [(Def, Accessibility)]
579lookupDefAcc root n mkpublic ctxt
580 = map mkp $ lookupCtxt root n (definitions ctxt)
581 where mkp (d, a) = if mkpublic then (d, Public) else (d, a)
583lookupVal :: Maybe [String] -> Name -> Context -> [Value]
584lookupVal root n ctxt
585 = do def <- lookupCtxt root n (definitions ctxt)
586 case fst def of
587 (Function _ htm) -> return (veval ctxt [] htm)
588 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
590lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
591lookupTyEnv n env = li n 0 env where
592 li n i [] = Nothing
593 li n i ((x, b): xs)
594 | n == x = Just (i, binderTy b)
595 | otherwise = li n (i+1) xs