git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Elab/Value.hs
124 lines 4.8 kB history raw
1{-|
2Module : Idris.Elab.Value
3Description : Code to elaborate values.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10module Idris.Elab.Value(
11 elabVal, elabValBind, elabDocTerms
12 , elabExec, elabREPL
13 ) where
15import Idris.AbsSyntax
16import Idris.Core.Elaborate hiding (Tactic(..))
17import Idris.Core.Evaluate hiding (Unchecked)
18import Idris.Core.TT
19import Idris.Docstrings
20import Idris.Elab.Term
21import Idris.Elab.Utils
22import Idris.Error
23import Idris.Output (sendHighlighting)
25import Prelude hiding (id, (.))
27import Control.Category
28import Data.Char (toLower)
29import qualified Data.Set as S ()
30import qualified Data.Traversable as Traversable
32-- | Elaborate a value, returning any new bindings created (this will only
33-- happen if elaborating as a pattern clause)
34elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
35elabValBind info aspat norm tm_in
36 = do ctxt <- getContext
37 i <- getIState
38 let tm = addImpl [] i tm_in
39 logElab 10 (showTmImpls tm)
40 -- try:
41 -- * ordinary elaboration
42 -- * elaboration as a Type
43 -- * elaboration as a function a -> b
45 (ElabResult tm' defer is ctxt' newDecls highlights newGName, _) <-
46 tclift (elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "val") infP initEState
47 (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))
49 -- Extend the context with new definitions created
50 setContext ctxt'
51 processTacticDecls info newDecls
52 sendHighlighting highlights
53 updateIState $ \i -> i { idris_name = newGName }
55 let vtm = orderPats (getInferTerm tm')
57 def' <- checkDef info (fileFC "(input)") iderr True defer
58 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) def'
59 addDeferred def''
60 mapM_ (elabCaseBlock info []) is
62 logElab 3 ("Value: " ++ show vtm)
63 (vtm_in, vty) <- recheckC (constraintNS info) (fileFC "(input)") id [] vtm
65 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in
66 else vtm_in
67 let bargs = getPBtys vtm
69 return (vtm, vty, bargs)
71elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)
72elabVal info aspat tm_in
73 = do (tm, ty, _) <- elabValBind info aspat False tm_in
74 return (tm, ty)
78elabDocTerms :: ElabInfo -> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
79elabDocTerms info str = do typechecked <- Traversable.mapM decorate str
80 return $ checkDocstring mkDocTerm typechecked
81 where decorate (Left err) = return (Left err)
82 decorate (Right pt) = fmap (fmap fst) (tryElabVal info ERHS pt)
84 tryElabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Either Err (Term, Type))
85 tryElabVal info aspat tm_in
86 = idrisCatch (fmap Right $ elabVal info aspat tm_in)
87 (return . Left)
89 mkDocTerm :: String -> [String] -> String -> Either Err Term -> DocTerm
90 mkDocTerm lang attrs src (Left err)
91 | map toLower lang == "idris" = Failing err
92 | otherwise = Unchecked
93 mkDocTerm lang attrs src (Right tm)
94 | map toLower lang == "idris" = if "example" `elem` map (map toLower) attrs
95 then Example tm
96 else Checked tm
97 | otherwise = Unchecked
99-- | Try running the term directly (as IO ()) or with >>= printLn appended
100-- (for other IO _), then printing it as an Integer (as a default numeric
101-- type), then printing it as any Showable thing
102elabExec :: FC -> PTerm -> PTerm
103elabExec fc tm = runtm (PAlternative [] FirstSuccess
104 [printtm (PApp fc (PRef fc [] (sUN "the"))
105 [pexp (PConstant NoFC (AType (ATInt ITBig))), pexp tm]),
106 tm,
107 PApp fc (PRef fc [] (sUN ">>="))
108 [pexp tm, pexp (PRef fc [] (sUN "printLn"))],
109 printtm tm
110 ])
111 where
112 runtm t = PApp fc (PRef fc [] (sUN "run__IO"))
113 [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]
114 printtm t = PApp fc (PRef fc [] (sUN "printLn")) [pexp t]
116elabREPL :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)
117elabREPL info aspat tm
118 = idrisCatch (elabVal info aspat tm) catchAmbig
119 where
120 catchAmbig (CantResolveAlts _)
121 = elabVal info aspat (PDisamb [[txt "List"]] tm)
122 catchAmbig (NoValidAlts _)
123 = elabVal info aspat (PDisamb [[txt "List"]] tm)
124 catchAmbig e = ierror e