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