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