git.iko.soy/Idris-dev
on d9a7b37 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1428 lines 59 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
10import Idris.AbsSyntaxTree
11import Idris.IdeSlave
12import Idris.Colours
13import IRTS.CodegenCommon
14import Util.DynamicLinker
16import Paths_idris
18import System.Console.Haskeline
20import Control.Monad.State
22import Data.List
23import Data.Char
24import Data.Either
25import Data.Maybe
27import Debug.Trace
29import Util.Pretty
30import Util.System
32getContext :: Idris Context
33getContext = do i <- getIState; return (tt_ctxt i)
35forCodegen :: Codegen -> [(Codegen, a)] -> [a]
36forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
38getObjectFiles :: Codegen -> Idris [FilePath]
39getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
41addObjectFile :: Codegen -> FilePath -> Idris ()
42addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
44getLibs :: Codegen -> Idris [String]
45getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
47addLib :: Codegen -> String -> Idris ()
48addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
50getFlags :: Codegen -> Idris [String]
51getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
53addFlag :: Codegen -> String -> Idris ()
54addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
56addDyLib :: [String] -> Idris (Either DynamicLib String)
57addDyLib libs = do i <- getIState
58 let ls = idris_dynamic_libs i
59 case mapMaybe (findDyLib ls) libs of
60 x:_ -> return (Left x)
61 [] -> do
62 handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
63 case msum handle of
64 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
65 concat (intersperse "," libs) ++ "\"")
66 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
67 return (Left x)
68 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
69 findDyLib [] l = Nothing
70 findDyLib (lib:libs) l | l == lib_name lib = Just lib
71 | otherwise = findDyLib libs l
74addHdr :: Codegen -> String -> Idris ()
75addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
77addLangExt :: LanguageExt -> Idris ()
78addLangExt TypeProviders = do i <- getIState ; putIState $ i { idris_language_extensions = [TypeProviders] }
80addTrans :: (Term, Term) -> Idris ()
81addTrans t = do i <- getIState
82 putIState $ i { idris_transforms = t : idris_transforms i }
84totcheck :: (FC, Name) -> Idris ()
85totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
87clear_totcheck :: Idris ()
88clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
90setFlags :: Name -> [FnOpt] -> Idris ()
91setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
93setAccessibility :: Name -> Accessibility -> Idris ()
94setAccessibility n a
95 = do i <- getIState
96 let ctxt = setAccess n a (tt_ctxt i)
97 putIState $ i { tt_ctxt = ctxt }
99setTotality :: Name -> Totality -> Idris ()
100setTotality n a
101 = do i <- getIState
102 let ctxt = setTotal n a (tt_ctxt i)
103 putIState $ i { tt_ctxt = ctxt }
105getTotality :: Name -> Idris Totality
106getTotality n
107 = do i <- getIState
108 case lookupTotal n (tt_ctxt i) of
109 [t] -> return t
110 _ -> return (Total [])
112-- Get coercions which might return the required type
113getCoercionsTo :: IState -> Type -> [Name]
114getCoercionsTo i ty =
115 let cs = idris_coercions i
116 (fn,_) = unApply (getRetTy ty) in
117 findCoercions fn cs
118 where findCoercions t [] = []
119 findCoercions t (n : ns) =
120 let ps = case lookupTy n (tt_ctxt i) of
121 [ty] -> case unApply (getRetTy ty) of
122 (t', _) ->
123 if t == t' then [n] else []
124 _ -> [] in
125 ps ++ findCoercions t ns
127addToCG :: Name -> CGInfo -> Idris ()
128addToCG n cg
129 = do i <- getIState
130 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
132addCoercion :: Name -> Idris ()
133addCoercion n = do i <- getIState
134 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
136addDocStr :: Name -> String -> Idris ()
137addDocStr n doc
138 = do i <- getIState
139 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
141addToCalledG :: Name -> [Name] -> Idris ()
142addToCalledG n ns = return () -- TODO
144-- Add a class instance function. Dodgy hack: Put integer instances first in the
145-- list so they are resolved by default.
146-- Dodgy hack 2: put constraint chasers (@@) last
148addInstance :: Bool -> Name -> Name -> Idris ()
149addInstance int n i
150 = do ist <- getIState
151 case lookupCtxt n (idris_classes ist) of
152 [CI a b c d ins] ->
153 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
154 putIState $ ist { idris_classes = cs }
155 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
156 putIState $ ist { idris_classes = cs }
157 where addI i ins | int = i : ins
158 | chaser n = ins ++ [i]
159 | otherwise = insI i ins
160 insI i [] = [i]
161 insI i (n : ns) | chaser n = i : n : ns
162 | otherwise = n : insI i ns
164 chaser (UN ('@':'@':_)) = True
165 chaser (NS n _) = chaser n
166 chaser _ = False
168addClass :: Name -> ClassInfo -> Idris ()
169addClass n i
170 = do ist <- getIState
171 let i' = case lookupCtxt n (idris_classes ist) of
172 [c] -> c { class_instances = class_instances i }
173 _ -> i
174 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
176addIBC :: IBCWrite -> Idris ()
177addIBC ibc@(IBCDef n)
178 = do i <- getIState
179 when (notDef (ibc_write i)) $
180 putIState $ i { ibc_write = ibc : ibc_write i }
181 where notDef [] = True
182 notDef (IBCDef n': is) | n == n' = False
183 notDef (_ : is) = notDef is
184addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
186clearIBC :: Idris ()
187clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
189getHdrs :: Codegen -> Idris [String]
190getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
192setErrLine :: Int -> Idris ()
193setErrLine x = do i <- getIState;
194 case (errLine i) of
195 Nothing -> putIState $ i { errLine = Just x }
196 Just _ -> return ()
198clearErr :: Idris ()
199clearErr = do i <- getIState
200 putIState $ i { errLine = Nothing }
202getSO :: Idris (Maybe String)
203getSO = do i <- getIState
204 return (compiled_so i)
206setSO :: Maybe String -> Idris ()
207setSO s = do i <- getIState
208 putIState $ (i { compiled_so = s })
210getIState :: Idris IState
211getIState = get
213putIState :: IState -> Idris ()
214putIState = put
216getName :: Idris Int
217getName = do i <- getIState;
218 let idx = idris_name i;
219 putIState $ (i { idris_name = idx + 1 })
220 return idx
222checkUndefined :: FC -> Name -> Idris ()
223checkUndefined fc n
224 = do i <- getContext
225 case lookupTy n i of
226 (_:_) -> fail $ show fc ++ ":" ++
227 show n ++ " already defined"
228 _ -> return ()
230isUndefined :: FC -> Name -> Idris Bool
231isUndefined fc n
232 = do i <- getContext
233 case lookupTy n i of
234 (_:_) -> return False
235 _ -> return True
237setContext :: Context -> Idris ()
238setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
240updateContext :: (Context -> Context) -> Idris ()
241updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
243addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
244addConstraints fc (v, cs)
245 = do i <- getIState
246 let ctxt = tt_ctxt i
247 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
248 next_tvar = v }
249 let ics = zip cs (repeat fc) ++ idris_constraints i
250 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
252addDeferred = addDeferred' Ref
253addDeferredTyCon = addDeferred' (TCon 0 0)
255addDeferred' :: NameType -> [(Name, Type)] -> Idris ()
256addDeferred' nt ns
257 = do mapM_ (\(n, t) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
258 i <- getIState
259 putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }
260 where tidyNames used (Bind (MN i x) b sc)
261 = let n' = uniqueName (UN x) used in
262 Bind n' b $ tidyNames (n':used) sc
263 tidyNames used (Bind n b sc)
264 = let n' = uniqueName n used in
265 Bind n' b $ tidyNames (n':used) sc
266 tidyNames used b = b
268solveDeferred :: Name -> Idris ()
269solveDeferred n = do i <- getIState
270 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
272iResult :: String -> Idris ()
273iResult s = do i <- getIState
274 case idris_outputmode i of
275 RawOutput -> case s of
276 "" -> return ()
277 s -> liftIO $ putStrLn s
278 IdeSlave n ->
279 let good = SexpList [SymbolAtom "ok", toSExp s] in
280 liftIO $ putStrLn $ convSExp "return" good n
282iFail :: String -> Idris ()
283iFail s = do i <- getIState
284 case idris_outputmode i of
285 RawOutput -> case s of
286 "" -> return ()
287 s -> liftIO $ putStrLn s
288 IdeSlave n ->
289 let good = SexpList [SymbolAtom "error", toSExp s] in
290 liftIO . putStrLn $ convSExp "return" good n
292iputStrLn :: String -> Idris ()
293iputStrLn s = do i <- getIState
294 case idris_outputmode i of
295 RawOutput -> liftIO $ putStrLn s
296 IdeSlave n ->
297 case span (/=':') s of
298 (fn, ':':rest) -> case span isDigit rest of
299 ([], ':':msg) -> write
300 ([], msg) -> write
301 (num, ':':msg) -> iWarn (FC fn (read num)) msg
302 _ -> write
303 where write = liftIO . putStrLn $ convSExp "write-string" s n
305ideslavePutSExp :: SExpable a => String -> a -> Idris ()
306ideslavePutSExp cmd info = do i <- getIState
307 case idris_outputmode i of
308 IdeSlave n -> liftIO . putStrLn $ convSExp cmd info n
309 _ -> return ()
311-- this needs some typing magic and more structured output towards emacs
312iputGoal :: String -> Idris ()
313iputGoal s = do i <- getIState
314 case idris_outputmode i of
315 RawOutput -> liftIO $ putStrLn s
316 IdeSlave n -> liftIO . putStrLn $ convSExp "write-goal" s n
318isetPrompt :: String -> Idris ()
319isetPrompt p = do i <- getIState
320 case idris_outputmode i of
321 IdeSlave n -> liftIO . putStrLn $ convSExp "set-prompt" p n
323iWarn :: FC -> String -> Idris ()
324iWarn fc err = do i <- getIState
325 case idris_outputmode i of
326 RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)
327 IdeSlave n -> liftIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
329setLogLevel :: Int -> Idris ()
330setLogLevel l = do i <- getIState
331 let opts = idris_options i
332 let opt' = opts { opt_logLevel = l }
333 putIState $ i { idris_options = opt' }
335setCmdLine :: [Opt] -> Idris ()
336setCmdLine opts = do i <- getIState
337 let iopts = idris_options i
338 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
340getCmdLine :: Idris [Opt]
341getCmdLine = do i <- getIState
342 return (opt_cmdline (idris_options i))
344getDumpDefun :: Idris (Maybe FilePath)
345getDumpDefun = do i <- getIState
346 return $ findC (opt_cmdline (idris_options i))
347 where findC [] = Nothing
348 findC (DumpDefun x : _) = Just x
349 findC (_ : xs) = findC xs
351getDumpCases :: Idris (Maybe FilePath)
352getDumpCases = do i <- getIState
353 return $ findC (opt_cmdline (idris_options i))
354 where findC [] = Nothing
355 findC (DumpCases x : _) = Just x
356 findC (_ : xs) = findC xs
358logLevel :: Idris Int
359logLevel = do i <- getIState
360 return (opt_logLevel (idris_options i))
362setErrContext :: Bool -> Idris ()
363setErrContext t = do i <- getIState
364 let opts = idris_options i
365 let opt' = opts { opt_errContext = t }
366 putIState $ i { idris_options = opt' }
368errContext :: Idris Bool
369errContext = do i <- getIState
370 return (opt_errContext (idris_options i))
372useREPL :: Idris Bool
373useREPL = do i <- getIState
374 return (opt_repl (idris_options i))
376setREPL :: Bool -> Idris ()
377setREPL t = do i <- getIState
378 let opts = idris_options i
379 let opt' = opts { opt_repl = t }
380 putIState $ i { idris_options = opt' }
382setQuiet :: Bool -> Idris ()
383setQuiet q = do i <- getIState
384 let opts = idris_options i
385 let opt' = opts { opt_quiet = q }
386 putIState $ i { idris_options = opt' }
388getQuiet :: Idris Bool
389getQuiet = do i <- getIState
390 let opts = idris_options i
391 return (opt_quiet opts)
393setCodegen :: Codegen -> Idris ()
394setCodegen t = do i <- getIState
395 let opts = idris_options i
396 let opt' = opts { opt_codegen = t }
397 putIState $ i { idris_options = opt' }
399codegen :: Idris Codegen
400codegen = do i <- getIState
401 return (opt_codegen (idris_options i))
403setOutputTy :: OutputType -> Idris ()
404setOutputTy t = do i <- getIState
405 let opts = idris_options i
406 let opt' = opts { opt_outputTy = t }
407 putIState $ i { idris_options = opt' }
409outputTy :: Idris OutputType
410outputTy = do i <- getIState
411 return $ opt_outputTy $ idris_options i
413setIdeSlave :: Bool -> Idris ()
414setIdeSlave True = do i <- getIState
415 putIState $ i { idris_outputmode = (IdeSlave 0) }
416setIdeSlave False = return ()
418setTargetTriple :: String -> Idris ()
419setTargetTriple t = do i <- getIState
420 let opts = idris_options i
421 opt' = opts { opt_triple = t }
422 putIState $ i { idris_options = opt' }
424targetTriple :: Idris String
425targetTriple = do i <- getIState
426 return (opt_triple (idris_options i))
428setTargetCPU :: String -> Idris ()
429setTargetCPU t = do i <- getIState
430 let opts = idris_options i
431 opt' = opts { opt_cpu = t }
432 putIState $ i { idris_options = opt' }
434targetCPU :: Idris String
435targetCPU = do i <- getIState
436 return (opt_cpu (idris_options i))
438setOptLevel :: Int -> Idris ()
439setOptLevel t = do i <- getIState
440 let opts = idris_options i
441 opt' = opts { opt_optLevel = t }
442 putIState $ i { idris_options = opt' }
444optLevel :: Idris Int
445optLevel = do i <- getIState
446 return (opt_optLevel (idris_options i))
448verbose :: Idris Bool
449verbose = do i <- getIState
450 return (opt_verbose (idris_options i))
452setVerbose :: Bool -> Idris ()
453setVerbose t = do i <- getIState
454 let opts = idris_options i
455 let opt' = opts { opt_verbose = t }
456 putIState $ i { idris_options = opt' }
458typeInType :: Idris Bool
459typeInType = do i <- getIState
460 return (opt_typeintype (idris_options i))
462setTypeInType :: Bool -> Idris ()
463setTypeInType t = do i <- getIState
464 let opts = idris_options i
465 let opt' = opts { opt_typeintype = t }
466 putIState $ i { idris_options = opt' }
468coverage :: Idris Bool
469coverage = do i <- getIState
470 return (opt_coverage (idris_options i))
472setCoverage :: Bool -> Idris ()
473setCoverage t = do i <- getIState
474 let opts = idris_options i
475 let opt' = opts { opt_coverage = t }
476 putIState $ i { idris_options = opt' }
478setIBCSubDir :: FilePath -> Idris ()
479setIBCSubDir fp = do i <- getIState
480 let opts = idris_options i
481 let opt' = opts { opt_ibcsubdir = fp }
482 putIState $ i { idris_options = opt' }
484valIBCSubDir :: IState -> Idris FilePath
485valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
487addImportDir :: FilePath -> Idris ()
488addImportDir fp = do i <- getIState
489 let opts = idris_options i
490 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
491 putIState $ i { idris_options = opt' }
493setImportDirs :: [FilePath] -> Idris ()
494setImportDirs fps = do i <- getIState
495 let opts = idris_options i
496 let opt' = opts { opt_importdirs = fps }
497 putIState $ i { idris_options = opt' }
499allImportDirs :: Idris [FilePath]
500allImportDirs = do i <- getIState
501 let optdirs = opt_importdirs (idris_options i)
502 return ("." : reverse optdirs)
504colourise :: Idris Bool
505colourise = do i <- getIState
506 return $ idris_colourRepl i
508setColourise :: Bool -> Idris ()
509setColourise b = do i <- getIState
510 putIState $ i { idris_colourRepl = b }
512impShow :: Idris Bool
513impShow = do i <- getIState
514 return (opt_showimp (idris_options i))
516setImpShow :: Bool -> Idris ()
517setImpShow t = do i <- getIState
518 let opts = idris_options i
519 let opt' = opts { opt_showimp = t }
520 putIState $ i { idris_options = opt' }
522setColour :: ColourType -> IdrisColour -> Idris ()
523setColour ct c = do i <- getIState
524 let newTheme = setColour' ct c (idris_colourTheme i)
525 putIState $ i { idris_colourTheme = newTheme }
526 where setColour' KeywordColour c t = t { keywordColour = c }
527 setColour' BoundVarColour c t = t { boundVarColour = c }
528 setColour' ImplicitColour c t = t { implicitColour = c }
529 setColour' FunctionColour c t = t { functionColour = c }
530 setColour' TypeColour c t = t { typeColour = c }
531 setColour' DataColour c t = t { dataColour = c }
532 setColour' PromptColour c t = t { promptColour = c }
534logLvl :: Int -> String -> Idris ()
535logLvl l str = do i <- getIState
536 let lvl = opt_logLevel (idris_options i)
537 when (lvl >= l)
538 $ do liftIO (putStrLn str)
539 putIState $ i { idris_log = idris_log i ++ str ++ "\n" }
541cmdOptType :: Opt -> Idris Bool
542cmdOptType x = do i <- getIState
543 return $ x `elem` opt_cmdline (idris_options i)
545iLOG :: String -> Idris ()
546iLOG = logLvl 1
548noErrors :: Idris Bool
549noErrors = do i <- getIState
550 case errLine i of
551 Nothing -> return True
552 _ -> return False
554setTypeCase :: Bool -> Idris ()
555setTypeCase t = do i <- getIState
556 let opts = idris_options i
557 let opt' = opts { opt_typecase = t }
558 putIState $ i { idris_options = opt' }
561-- For inferring types of things
563bi = FC "builtin" 0
565inferTy = MN 0 "__Infer"
566inferCon = MN 0 "__infer"
567inferDecl = PDatadecl inferTy
568 PType
569 [("", inferCon, PPi impl (MN 0 "A") PType (
570 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
571 (PRef bi inferTy)), bi)]
573infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
574infP = P (TCon 6 0) inferTy (TType (UVal 0))
576getInferTerm, getInferType :: Term -> Term
577getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
578getInferTerm (App (App _ _) tm) = tm
579getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
581getInferType (Bind n b sc) = Bind n b $ getInferType sc
582getInferType (App (App _ ty) _) = ty
584-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
586primNames = [unitTy, unitCon,
587 falseTy, pairTy, pairCon,
588 eqTy, eqCon, inferTy, inferCon]
590unitTy = MN 0 "__Unit"
591unitCon = MN 0 "__II"
592unitDecl = PDatadecl unitTy PType
593 [("", unitCon, PRef bi unitTy, bi)]
595falseTy = MN 0 "__False"
596falseDecl = PDatadecl falseTy PType []
598pairTy = MN 0 "__Pair"
599pairCon = MN 0 "__MkPair"
600pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
601 [("", pairCon, PPi impl (n "A") PType (
602 PPi impl (n "B") PType (
603 PPi expl (n "a") (PRef bi (n "A")) (
604 PPi expl (n "b") (PRef bi (n "B"))
605 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
606 pexp (PRef bi (n "B"))])))), bi)]
607 where n a = MN 0 a
609eqTy = UN "="
610eqCon = UN "refl"
611eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
612 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
613 PType)
614 [("", eqCon, PPi impl (n "a") PType (
615 PPi impl (n "x") (PRef bi (n "a"))
616 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
617 pimp (n "b") Placeholder,
618 pexp (PRef bi (n "x")),
619 pexp (PRef bi (n "x"))])), bi)]
620 where n a = MN 0 a
622-- Defined in builtins.idr
623sigmaTy = UN "Exists"
624existsCon = UN "Ex_intro"
626piBind :: [(Name, PTerm)] -> PTerm -> PTerm
627piBind = piBindp expl
629piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
630piBindp p [] t = t
631piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)
633-- Dealing with parameters
635expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
636 [Name] -> -- all names
637 [Name] -> -- names with no declaration
638 PTerm -> PTerm
639expandParams dec ps ns infs tm = en tm
640 where
641 -- if we shadow a name (say in a lambda binding) that is used in a call to
642 -- a lifted function, we need access to both names - once in the scope of the
643 -- binding and once to call the lifted functions. So we'll explicitly shadow
644 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
645 -- but we didn't...)
647 mkShadow (UN n) = MN 0 n
648 mkShadow (MN i n) = MN (i+1) n
649 mkShadow (NS x s) = NS (mkShadow x) s
651 en (PLam n t s)
652 | n `elem` (map fst ps ++ ns)
653 = let n' = mkShadow n in
654 PLam n' (en t) (en (shadow n n' s))
655 | otherwise = PLam n (en t) (en s)
656 en (PPi p n t s)
657 | n `elem` (map fst ps ++ ns)
658 = let n' = mkShadow n in
659 PPi p n' (en t) (en (shadow n n' s))
660 | otherwise = PPi p n (en t) (en s)
661 en (PLet n ty v s)
662 | n `elem` (map fst ps ++ ns)
663 = let n' = mkShadow n in
664 PLet n' (en ty) (en v) (en (shadow n n' s))
665 | otherwise = PLet n (en ty) (en v) (en s)
666 -- FIXME: Should only do this in a type signature!
667 en (PDPair f (PRef f' n) t r)
668 | n `elem` (map fst ps ++ ns) && t /= Placeholder
669 = let n' = mkShadow n in
670 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
671 en (PEq f l r) = PEq f (en l) (en r)
672 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
673 en (PTyped l r) = PTyped (en l) (en r)
674 en (PPair f l r) = PPair f (en l) (en r)
675 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
676 en (PAlternative a as) = PAlternative a (map en as)
677 en (PHidden t) = PHidden (en t)
678 en (PUnifyLog t) = PUnifyLog (en t)
679 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
680 en (PProof ts) = PProof (map (fmap en) ts)
681 en (PTactics ts) = PTactics (map (fmap en) ts)
683 en (PQuote (Var n))
684 | n `nselem` ns = PQuote (Var (dec n))
685 en (PApp fc (PInferRef fc' n) as)
686 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
687 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
688 en (PApp fc (PRef fc' n) as)
689 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
690 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
691 | n `nselem` ns = PApp fc (PRef fc' (dec n))
692 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
693 en (PRef fc n)
694 | n `elem` infs = PApp fc (PInferRef fc (dec n))
695 (map (pexp . (PRef fc)) (map fst ps))
696 | n `nselem` ns = PApp fc (PRef fc (dec n))
697 (map (pexp . (PRef fc)) (map fst ps))
698 en (PInferRef fc n)
699 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
700 (map (pexp . (PRef fc)) (map fst ps))
701 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
702 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
703 en t = t
705 nselem x [] = False
706 nselem x (y : xs) | nseq x y = True
707 | otherwise = nselem x xs
709 nseq x y = nsroot x == nsroot y
711expandParamsD :: Bool -> -- True = RHS only
712 IState ->
713 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
714expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
715 = if n `elem` ns && (not rhsonly)
716 then -- trace (show (n, expandParams dec ps ns ty)) $
717 PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns [] ty))
718 else --trace (show (n, expandParams dec ps ns ty)) $
719 PTy doc syn fc o n (expandParams dec ps ns [] ty)
720expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
721 = if n `elem` ns && (not rhsonly)
722 then -- trace (show (n, expandParams dec ps ns ty)) $
723 PPostulate doc syn fc o (dec n) (piBind ps
724 (expandParams dec ps ns [] ty))
725 else --trace (show (n, expandParams dec ps ns ty)) $
726 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
727expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
728 = let n' = if n `elem` ns then dec n else n in
729 PClauses fc opts n' (map expandParamsC cs)
730 where
731 expandParamsC (PClause fc n lhs ws rhs ds)
732 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
733 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
734 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
735 n' = if n `elem` ns then dec n else n
736 -- names bound on the lhs should not be expanded on the rhs
737 ns' = removeBound lhs ns in
738 PClause fc n' lhs'
739 (map (expandParams dec ps'' ns' []) ws)
740 (expandParams dec ps'' ns' [] rhs)
741 (map (expandParamsD True ist dec ps'' ns') ds)
742 expandParamsC (PWith fc n lhs ws wval ds)
743 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
744 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
745 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
746 n' = if n `elem` ns then dec n else n
747 ns' = removeBound lhs ns in
748 PWith fc n' lhs'
749 (map (expandParams dec ps'' ns' []) ws)
750 (expandParams dec ps'' ns' [] wval)
751 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
752 updateps yn nm [] = []
753 updateps yn nm (((a, t), i):as)
754 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
755 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
757 removeBound lhs ns = ns \\ nub (bnames lhs)
759 bnames (PRef _ n) = [n]
760 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
761 bnames (PPair _ l r) = bnames l ++ bnames r
762 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
763 bnames _ = []
765expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
766 = PData doc syn fc co (expandPData pd)
767 where
768 -- just do the type decl, leave constructors alone (parameters will be
769 -- added implicitly)
770 expandPData (PDatadecl n ty cons)
771 = if n `elem` ns
772 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
773 (map econ cons)
774 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
775 econ (doc, n, t, fc)
776 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
777expandParamsD rhs ist dec ps ns (PParams f params pds)
778 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
779 (map (expandParamsD True ist dec ps ns) pds)
780-- (map (expandParamsD ist dec ps ns) pds)
781expandParamsD rhs ist dec ps ns (PMutual f pds)
782 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
783expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
784 = PClass doc info f
785 (map (expandParams dec ps ns []) cs)
786 n
787 (map (mapsnd (expandParams dec ps ns [])) params)
788 (map (expandParamsD rhs ist dec ps ns) decls)
789expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
790 = PInstance info f
791 (map (expandParams dec ps ns []) cs)
792 n
793 (map (expandParams dec ps ns []) params)
794 (expandParams dec ps ns [] ty)
795 cn
796 (map (expandParamsD rhs ist dec ps ns) decls)
797expandParamsD rhs ist dec ps ns d = d
799mapsnd f (x, t) = (x, f t)
801-- Calculate a priority for a type, for deciding elaboration order
802-- * if it's just a type variable or concrete type, do it early (0)
803-- * if there's only type variables and injective constructors, do it next (1)
804-- * if there's a function type, next (2)
805-- * finally, everything else (3)
807getPriority :: IState -> PTerm -> Int
808getPriority i tm = 1 -- pri tm
809 where
810 pri (PRef _ n) =
811 case lookupP n (tt_ctxt i) of
812 ((P (DCon _ _) _ _):_) -> 1
813 ((P (TCon _ _) _ _):_) -> 1
814 ((P Ref _ _):_) -> 1
815 [] -> 0 -- must be locally bound, if it's not an error...
816 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
817 pri (PTrue _) = 0
818 pri (PFalse _) = 0
819 pri (PRefl _ _) = 1
820 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
821 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
822 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
823 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
824 pri (PTyped l r) = pri l
825 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
826 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
827 pri (PAlternative a as) = maximum (map pri as)
828 pri (PConstant _) = 0
829 pri Placeholder = 1
830 pri _ = 3
832addStatics :: Name -> Term -> PTerm -> Idris ()
833addStatics n tm ptm =
834 do let (statics, dynamics) = initStatics tm ptm
835 let stnames = nub $ concatMap freeNames (map snd statics)
836 let dnames = nub $ concatMap freeNames (map snd dynamics)
837 when (not (null statics)) $
838 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
839 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
840 let statics' = nub $ map fst statics ++
841 filter (\x -> not (elem x dnames)) stnames
842 let stpos = staticList statics' tm
843 i <- getIState
844 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
845 addIBC (IBCStatic n)
846 where
847 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
848 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
849 if pstatic p == Static then ((n, ty) : static, dynamic)
850 else (static, (n, ty) : dynamic)
851 initStatics t pt = ([], [])
853 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
854 staticList _ _ = []
856-- Dealing with implicit arguments
858-- Add constraint bindings from using block
860addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
861addUsingConstraints syn fc t
862 = do ist <- get
863 let ns = namesIn [] ist t
864 let cs = getConstraints t -- check declared constraints
865 let addconsts = uconsts \\ cs
866 -- if all names in the arguments of addconsts appear in ns,
867 -- add the constraint implicitly
868 return (doAdd addconsts ns t)
869 where uconsts = filter uconst (using syn)
870 uconst (UConstraint _ _) = True
871 uconst _ = False
873 doAdd [] _ t = t
874 -- if all of args in ns, then add it
875 doAdd (UConstraint c args : cs) ns t
876 | all (\n -> elem n ns) args
877 = PPi (Constraint False Dynamic "") (MN 0 "cu")
878 (mkConst c args) (doAdd cs ns t)
879 | otherwise = doAdd cs ns t
881 mkConst c args = PApp fc (PRef fc c)
882 (map (\n -> PExp 0 False (PRef fc n) "") args)
884 getConstraints (PPi (Constraint _ _ _) _ c sc)
885 = getcapp c ++ getConstraints sc
886 getConstraints (PPi _ _ c sc) = getConstraints sc
887 getConstraints _ = []
889 getcapp (PApp _ (PRef _ c) args)
890 = do ns <- mapM getName args
891 return (UConstraint c ns)
892 getcapp _ = []
894 getName (PExp _ _ (PRef _ n) _) = return n
895 getName _ = []
897-- Add implicit Pi bindings for any names in the term which appear in an
898-- argument position.
900-- This has become a right mess already. Better redo it some time...
902implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
903implicit syn n ptm = implicit' syn [] n ptm
905implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
906implicit' syn ignore n ptm
907 = do i <- getIState
908 let (tm', impdata) = implicitise syn ignore i ptm
909-- let (tm'', spos) = findStatics i tm'
910 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
911 addIBC (IBCImp n)
912 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
913-- i <- get
914-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
915 return tm'
917implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
918implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
919 let (declimps, ns') = execState (imps True [] tm) ([], [])
920 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
921 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
922 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
923 if null ns
924 then (tm, reverse declimps)
925 else implicitise syn ignore ist (pibind uvars nsOrder tm)
926 where
927 uvars = map ipair (filter uimplicit (using syn))
928 pvars = syn_params syn
930 inUsing n = n `elem` map fst uvars
932 ipair (UImplicit x y) = (x, y)
933 uimplicit (UImplicit _ _) = True
934 uimplicit _ = False
936 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
937 | otherwise = x : dropAll xs ys
938 dropAll [] ys = []
940 imps top env (PApp _ f as)
941 = do (decls, ns) <- get
942 let isn = concatMap (namesIn uvars ist) (map getTm as)
943 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
944 imps top env (PPi (Imp l _ doc) n ty sc)
945 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
946 (decls , ns) <- get
947 put (PImp (getPriority ist ty) l n ty doc : decls,
948 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
949 imps True (n:env) sc
950 imps top env (PPi (Exp l _ doc) n ty sc)
951 = do let isn = nub (namesIn uvars ist ty ++ case sc of
952 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
953 _ -> [])
954 (decls, ns) <- get -- ignore decls in HO types
955 put (PExp (getPriority ist ty) l ty doc : decls,
956 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
957 imps True (n:env) sc
958 imps top env (PPi (Constraint l _ doc) n ty sc)
959 = do let isn = nub (namesIn uvars ist ty ++ case sc of
960 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
961 _ -> [])
962 (decls, ns) <- get -- ignore decls in HO types
963 put (PConstraint 10 l ty doc : decls,
964 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
965 imps True (n:env) sc
966 imps top env (PPi (TacImp l _ scr doc) n ty sc)
967 = do let isn = nub (namesIn uvars ist ty ++ case sc of
968 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
969 _ -> [])
970 (decls, ns) <- get -- ignore decls in HO types
971 put (PTacImplicit 10 l n scr ty doc : decls,
972 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
973 imps True (n:env) sc
974 imps top env (PEq _ l r)
975 = do (decls, ns) <- get
976 let isn = namesIn uvars ist l ++ namesIn uvars ist r
977 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
978 imps top env (PRewrite _ l r _)
979 = do (decls, ns) <- get
980 let isn = namesIn uvars ist l ++ namesIn uvars ist r
981 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
982 imps top env (PTyped l r)
983 = imps top env l
984 imps top env (PPair _ l r)
985 = do (decls, ns) <- get
986 let isn = namesIn uvars ist l ++ namesIn uvars ist r
987 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
988 imps top env (PDPair _ (PRef _ n) t r)
989 = do (decls, ns) <- get
990 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
991 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
992 imps top env (PDPair _ l t r)
993 = do (decls, ns) <- get
994 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
995 namesIn uvars ist r
996 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
997 imps top env (PAlternative a as)
998 = do (decls, ns) <- get
999 let isn = concatMap (namesIn uvars ist) as
1000 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1001 imps top env (PLam n ty sc)
1002 = do imps False env ty
1003 imps False (n:env) sc
1004 imps top env (PHidden tm) = imps False env tm
1005 imps top env (PUnifyLog tm) = imps False env tm
1006 imps top env _ = return ()
1008 pibind using [] sc = sc
1009 pibind using (n:ns) sc
1010 = case lookup n using of
1011 Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)
1012 Nothing -> PPi (Imp False Dynamic "") n Placeholder
1013 (pibind using ns sc)
1015-- Add implicit arguments in function calls
1016addImplPat :: IState -> PTerm -> PTerm
1017addImplPat = addImpl' True [] []
1019addImplBound :: IState -> [Name] -> PTerm -> PTerm
1020addImplBound ist ns = addImpl' False ns [] ist
1022addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1023addImplBoundInf ist ns inf = addImpl' False ns inf ist
1025addImpl :: IState -> PTerm -> PTerm
1026addImpl = addImpl' False [] []
1028-- TODO: in patterns, don't add implicits to function names guarded by constructors
1029-- and *not* inside a PHidden
1031addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1032addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1033 where
1034 ai env (PRef fc f)
1035 | f `elem` infns = PInferRef fc f
1036 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1037 ai env (PHidden (PRef fc f))
1038 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1039 ai env (PEq fc l r) = let l' = ai env l
1040 r' = ai env r in
1041 PEq fc l' r'
1042 ai env (PRewrite fc l r g) = let l' = ai env l
1043 r' = ai env r
1044 g' = fmap (ai env) g in
1045 PRewrite fc l' r' g'
1046 ai env (PTyped l r) = let l' = ai env l
1047 r' = ai env r in
1048 PTyped l' r'
1049 ai env (PPair fc l r) = let l' = ai env l
1050 r' = ai env r in
1051 PPair fc l' r'
1052 ai env (PDPair fc l t r) = let l' = ai env l
1053 t' = ai env t
1054 r' = ai env r in
1055 PDPair fc l' t' r'
1056 ai env (PAlternative a as) = let as' = map (ai env) as in
1057 PAlternative a as'
1058 ai env (PApp fc (PInferRef _ f) as)
1059 = let as' = map (fmap (ai env)) as in
1060 PApp fc (PInferRef fc f) as'
1061 ai env (PApp fc ftm@(PRef _ f) as)
1062 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1063 | not (f `elem` map fst env)
1064 = let as' = map (fmap (ai env)) as in
1065 handleErr $ aiFn inpat False ist fc f as'
1066 | Just (Just ty) <- lookup f env
1067 = let as' = map (fmap (ai env)) as
1068 arity = getPArity ty in
1069 mkPApp fc arity ftm as'
1070 ai env (PApp fc f as) = let f' = ai env f
1071 as' = map (fmap (ai env)) as in
1072 mkPApp fc 1 f' as'
1073 ai env (PCase fc c os) = let c' = ai env c
1074 os' = map (pmap (ai env)) os in
1075 PCase fc c' os'
1076 ai env (PLam n ty sc) = let ty' = ai env ty
1077 sc' = ai ((n, Just ty):env) sc in
1078 PLam n ty' sc'
1079 ai env (PLet n ty val sc)
1080 = let ty' = ai env ty
1081 val' = ai env val
1082 sc' = ai ((n, Just ty):env) sc in
1083 PLet n ty' val' sc'
1084 ai env (PPi p n ty sc) = let ty' = ai env ty
1085 sc' = ai ((n, Just ty):env) sc in
1086 PPi p n ty' sc'
1087 ai env (PGoal fc r n sc) = let r' = ai env r
1088 sc' = ai ((n, Nothing):env) sc in
1089 PGoal fc r' n sc'
1090 ai env (PHidden tm) = PHidden (ai env tm)
1091 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1092 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1093 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1094 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1095 ai env tm = tm
1097 handleErr (Left err) = PElabError err
1098 handleErr (Right x) = x
1100-- if in a pattern, and there are no arguments, and there's no possible
1101-- names with zero explicit arguments, don't add implicits.
1103aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1104aiFn inpat True ist fc f []
1105 = case lookupDef f (tt_ctxt ist) of
1106 [] -> Right $ PPatvar fc f
1107 alts -> let ialts = lookupCtxt f (idris_implicits ist) in
1108 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1109 if (not (vname f) || tcname f
1110 || any constructor alts || any allImp ialts)
1111 then aiFn inpat False ist fc f [] -- use it as a constructor
1112 else Right $ PPatvar fc f
1113 where imp (PExp _ _ _ _) = False
1114 imp _ = True
1115 allImp [] = False
1116 allImp xs = all imp xs
1117 constructor (TyDecl (DCon _ _) _) = True
1118 constructor _ = False
1120 vname (UN n) = True -- non qualified
1121 vname _ = False
1123aiFn inpat expat ist fc f as
1124 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1125aiFn inpat expat ist fc f as
1126 -- This is where namespaces get resolved by adding PAlternative
1127 = case lookupCtxtName f (idris_implicits ist) of
1128 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1129 [] -> if f `elem` idris_metavars ist
1130 then Right $ PApp fc (PRef fc f) as
1131 else Right $ mkPApp fc (length as) (PRef fc f) as
1132 alts -> Right $
1133 PAlternative True $
1134 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1135 (insertImpl ns as)) alts
1136 where
1137 insertImpl :: [PArg] -> [PArg] -> [PArg]
1138 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1139 PExp p l tm d : insertImpl ps given
1140 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1141 PConstraint p l tm d : insertImpl ps given
1142 insertImpl (PConstraint p l ty d : ps) given =
1143 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1144 insertImpl (PImp p l n ty d : ps) given =
1145 case find n given [] of
1146 Just (tm, given') -> PImp p l n tm "" : insertImpl ps given'
1147 Nothing -> PImp p l n Placeholder "" : insertImpl ps given
1148 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1149 case find n given [] of
1150 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1151 Nothing -> if inpat
1152 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1153 else PTacImplicit p l n sc sc "" : insertImpl ps given
1154 insertImpl expected [] = []
1155 insertImpl _ given = given
1157 find n [] acc = Nothing
1158 find n (PImp _ _ n' t _ : gs) acc
1159 | n == n' = Just (t, reverse acc ++ gs)
1160 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1161 | n == n' = Just (t, reverse acc ++ gs)
1162 find n (g : gs) acc = find n gs (g : acc)
1164-- replace non-linear occurrences with _
1165-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1166-- it is hard to get right!
1168stripLinear :: IState -> PTerm -> PTerm
1169stripLinear i tm = evalState (sl tm) [] where
1170 sl :: PTerm -> State [Name] PTerm
1171 sl (PRef fc f)
1172 | (_:_) <- lookupTy f (tt_ctxt i)
1173 = return $ PRef fc f
1174 | otherwise = do ns <- get
1175 if (f `elem` ns)
1176 then return Placeholder
1177 else do put (f : ns)
1178 return (PRef fc f)
1179 sl (PPatvar fc f)
1180 = do ns <- get
1181 if (f `elem` ns)
1182 then return Placeholder
1183 else do put (f : ns)
1184 return (PPatvar fc f)
1185 sl (PApp fc fn args) = do fn' <- sl fn
1186 args' <- mapM slA args
1187 return $ PApp fc fn' args'
1188 where slA (PImp p l n t d) = do t' <- sl t
1189 return $ PImp p l n t' d
1190 slA (PExp p l t d) = do t' <- sl t
1191 return $ PExp p l t' d
1192 slA (PConstraint p l t d)
1193 = do t' <- sl t
1194 return $ PConstraint p l t' d
1195 slA (PTacImplicit p l n sc t d)
1196 = do t' <- sl t
1197 return $ PTacImplicit p l n sc t' d
1198 sl x = return x
1200mkPApp fc a f [] = f
1201mkPApp fc a f as = let rest = drop a as in
1202 appRest fc (PApp fc f (take a as)) rest
1203 where
1204 appRest fc f [] = f
1205 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1207-- Find 'static' argument positions
1208-- (the declared ones, plus any names in argument position in the declared
1209-- statics)
1210-- FIXME: It's possible that this really has to happen after elaboration
1212findStatics :: IState -> PTerm -> (PTerm, [Bool])
1213findStatics ist tm = trace (showImp Nothing True False tm) $
1214 let (ns, ss) = fs tm in
1215 runState (pos ns ss tm) []
1216 where fs (PPi p n t sc)
1217 | Static <- pstatic p
1218 = let (ns, ss) = fs sc in
1219 (namesIn [] ist t : ns, n : ss)
1220 | otherwise = let (ns, ss) = fs sc in
1221 (ns, ss)
1222 fs _ = ([], [])
1224 inOne n ns = length (filter id (map (elem n) ns)) == 1
1226 pos ns ss (PPi p n t sc)
1227 | elem n ss = do sc' <- pos ns ss sc
1228 spos <- get
1229 put (True : spos)
1230 return (PPi (p { pstatic = Static }) n t sc')
1231 | otherwise = do sc' <- pos ns ss sc
1232 spos <- get
1233 put (False : spos)
1234 return (PPi p n t sc')
1235 pos ns ss t = return t
1237-- Debugging/logging stuff
1239dumpDecls :: [PDecl] -> String
1240dumpDecls [] = ""
1241dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1243dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1244dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t
1245dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1246dumpDecl (PData _ _ _ _ d) = showDImp True d
1247dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1248dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1249dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1250dumpDecl (PClass _ _ _ cs n ps ds)
1251 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1252dumpDecl (PInstance _ _ cs n _ t _ ds)
1253 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1254dumpDecl _ = "..."
1255-- dumpDecl (PImport i) = "import " ++ i
1257-- for 6.12/7 compatibility
1258data EitherErr a b = LeftErr a | RightOK b
1260instance Monad (EitherErr a) where
1261 return = RightOK
1263 (LeftErr e) >>= k = LeftErr e
1264 RightOK v >>= k = k v
1266toEither (LeftErr e) = Left e
1267toEither (RightOK ho) = Right ho
1269-- syntactic match of a against b, returning pair of variables in a
1270-- and what they match. Returns the pair that failed if not a match.
1272matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1273matchClause = matchClause' False
1275matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1276matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1277 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1279 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1280 fullApp x = x
1282 match' x y = match (fullApp x) (fullApp y)
1283 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1284 | PConstant (I _) <- getTm x = match (getTm x) x'
1285 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1286 | PConstant (I _) <- getTm x = match (getTm x) x'
1287 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1288 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1289 match (PApp _ f args) (PApp _ f' args')
1290 | length args == length args'
1291 = do mf <- match' f f'
1292 ms <- zipWithM matchArg args args'
1293 return (mf ++ concat ms)
1294-- match (PRef _ n) (PRef _ n') | n == n' = return []
1295-- | otherwise = Nothing
1296 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1297 match (PPatvar f n) xr = match (PRef f n) xr
1298 match xr (PPatvar f n) = match xr (PRef f n)
1299 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1300 match (PRef _ n) tm@(PRef _ n')
1301 | n == n' && not names &&
1302 (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1303 = return [(n, tm)]
1304 | n == n' = return []
1305 match (PRef _ n) tm
1306 | not names && (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1307 = return [(n, tm)]
1308 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1309 mr <- match' r r'
1310 return (ml ++ mr)
1311 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1312 = do ml <- match' l l'
1313 mr <- match' r r'
1314 return (ml ++ mr)
1315 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1316 mr <- match r r'
1317 return (ml ++ mr)
1318 match (PTyped l r) x = match l x
1319 match x (PTyped l r) = match x l
1320 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1321 mr <- match' r r'
1322 return (ml ++ mr)
1323 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1324 mt <- match' t t'
1325 mr <- match' r r'
1326 return (ml ++ mt ++ mr)
1327 match (PAlternative a as) (PAlternative a' as')
1328 = do ms <- zipWithM match' as as'
1329 return (concat ms)
1330 match a@(PAlternative _ as) b
1331 = do let ms = zipWith match' as (repeat b)
1332 case (rights (map toEither ms)) of
1333 (x: _) -> return x
1334 _ -> LeftErr (a, b)
1335 match (PCase _ _ _) _ = return [] -- lifted out
1336 match (PMetavar _) _ = return [] -- modified
1337 match (PInferRef _ _) _ = return [] -- modified
1338 match (PQuote _) _ = return []
1339 match (PProof _) _ = return []
1340 match (PTactics _) _ = return []
1341 match (PRefl _ _) (PRefl _ _) = return []
1342 match (PResolveTC _) (PResolveTC _) = return []
1343 match (PTrue _) (PTrue _) = return []
1344 match (PFalse _) (PFalse _) = return []
1345 match (PReturn _) (PReturn _) = return []
1346 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1347 ms <- match' s s'
1348 return (mt ++ ms)
1349 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1350 ms <- match' s s'
1351 return (mt ++ ms)
1352 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1353 mty <- match' ty ty'
1354 ms <- match' s s'
1355 return (mt ++ mty ++ ms)
1356 match (PHidden x) (PHidden y) = match' x y
1357 match (PUnifyLog x) y = match' x y
1358 match x (PUnifyLog y) = match' x y
1359 match Placeholder _ = return []
1360 match _ Placeholder = return []
1361 match (PResolveTC _) _ = return []
1362 match a b | a == b = return []
1363 | otherwise = LeftErr (a, b)
1365 checkRpts (RightOK ms) = check ms where
1366 check ((n,t):xs)
1367 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1368 then Left (t, t')
1369 else check xs
1370 check (_:xs) = check xs
1371 check [] = Right ms
1372 checkRpts (LeftErr x) = Left x
1374substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1375substMatches ms = substMatchesShadow ms []
1377substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1378substMatchesShadow [] shs t = t
1379substMatchesShadow ((n,tm):ns) shs t
1380 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1382substMatch :: Name -> PTerm -> PTerm -> PTerm
1383substMatch n = substMatchShadow n []
1385substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1386substMatchShadow n shs tm t = sm shs t where
1387 sm xs (PRef _ n') | n == n' = tm
1388 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1389 sm xs (PPi p x t sc)
1390 | x `elem` xs
1391 = let x' = nextName x in
1392 PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))
1393 (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))
1394 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1395 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1396 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1397 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1398 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1399 (fmap (sm xs) tm)
1400 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1401 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1402 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1403 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1404 sm xs (PHidden x) = PHidden (sm xs x)
1405 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1406 sm xs x = x
1408 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1409 fullApp x = x
1411shadow :: Name -> Name -> PTerm -> PTerm
1412shadow n n' t = sm t where
1413 sm (PRef fc x) | n == x = PRef fc n'
1414 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1415 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1416 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1417 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1418 sm (PEq f x y) = PEq f (sm x) (sm y)
1419 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1420 sm (PTyped x y) = PTyped (sm x) (sm y)
1421 sm (PPair f x y) = PPair f (sm x) (sm y)
1422 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1423 sm (PAlternative a as) = PAlternative a (map sm as)
1424 sm (PHidden x) = PHidden (sm x)
1425 sm (PUnifyLog x) = PUnifyLog (sm x)
1426 sm x = x