git.iko.soy/Idris-dev
on 17d2cea help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1063 lines 42 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 IRTS.CodegenCommon
13import Paths_idris
15import System.Console.Haskeline
17import Control.Monad.State
19import Data.List
20import Data.Char
21import Data.Either
23import Debug.Trace
25import Util.Pretty
28getContext :: Idris Context
29getContext = do i <- get; return (tt_ctxt i)
31getObjectFiles :: Idris [FilePath]
32getObjectFiles = do i <- get; return (idris_objs i)
34addObjectFile :: FilePath -> Idris ()
35addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
37getLibs :: Idris [String]
38getLibs = do i <- get; return (idris_libs i)
40addLib :: String -> Idris ()
41addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
43addHdr :: String -> Idris ()
44addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
46totcheck :: (FC, Name) -> Idris ()
47totcheck n = do i <- get; put (i { idris_totcheck = idris_totcheck i ++ [n] })
49setFlags :: Name -> [FnOpt] -> Idris ()
50setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
52setAccessibility :: Name -> Accessibility -> Idris ()
53setAccessibility n a
54 = do i <- get
55 let ctxt = setAccess n a (tt_ctxt i)
56 put (i { tt_ctxt = ctxt })
58setTotality :: Name -> Totality -> Idris ()
59setTotality n a
60 = do i <- get
61 let ctxt = setTotal n a (tt_ctxt i)
62 put (i { tt_ctxt = ctxt })
64getTotality :: Name -> Idris Totality
65getTotality n
66 = do i <- get
67 case lookupTotal n (tt_ctxt i) of
68 [t] -> return t
69 _ -> return (Total [])
71addToCG :: Name -> CGInfo -> Idris ()
72addToCG n cg
73 = do i <- get
74 put (i { idris_callgraph = addDef n cg (idris_callgraph i) })
76addDocStr :: Name -> String -> Idris ()
77addDocStr n doc
78 = do i <- get
79 put (i { idris_docstrings = addDef n doc (idris_docstrings i) })
81addToCalledG :: Name -> [Name] -> Idris ()
82addToCalledG n ns = return () -- TODO
84-- Add a class instance function. Dodgy hack: Put integer instances first in the
85-- list so they are resolved by default.
86-- Dodgy hack 2: put constraint chasers (@@) last
88addInstance :: Bool -> Name -> Name -> Idris ()
89addInstance int n i
90 = do ist <- get
91 case lookupCtxt Nothing n (idris_classes ist) of
92 [CI a b c d ins] ->
93 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
94 put (ist { idris_classes = cs })
95 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
96 put (ist { idris_classes = cs })
97 where addI i ins | int = i : ins
98 | chaser n = ins ++ [i]
99 | otherwise = insI i ins
100 insI i [] = [i]
101 insI i (n : ns) | chaser n = i : n : ns
102 | otherwise = n : insI i ns
104 chaser (UN ('@':'@':_)) = True
105 chaser (NS n _) = chaser n
106 chaser _ = False
108addClass :: Name -> ClassInfo -> Idris ()
109addClass n i
110 = do ist <- get
111 let i' = case lookupCtxt Nothing n (idris_classes ist) of
112 [c] -> c { class_instances = class_instances i }
113 _ -> i
114 put (ist { idris_classes = addDef n i' (idris_classes ist) })
116addIBC :: IBCWrite -> Idris ()
117addIBC ibc@(IBCDef n)
118 = do i <- get
119 when (notDef (ibc_write i)) $
120 put (i { ibc_write = ibc : ibc_write i })
121 where notDef [] = True
122 notDef (IBCDef n': is) | n == n' = False
123 notDef (_ : is) = notDef is
124addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
126clearIBC :: Idris ()
127clearIBC = do i <- get; put (i { ibc_write = [] })
129getHdrs :: Idris [String]
130getHdrs = do i <- get; return (idris_hdrs i)
132setErrLine :: Int -> Idris ()
133setErrLine x = do i <- get;
134 case (errLine i) of
135 Nothing -> put (i { errLine = Just x })
136 Just _ -> return ()
138clearErr :: Idris ()
139clearErr = do i <- get
140 put (i { errLine = Nothing })
142getSO :: Idris (Maybe String)
143getSO = do i <- get
144 return (compiled_so i)
146setSO :: Maybe String -> Idris ()
147setSO s = do i <- get
148 put (i { compiled_so = s })
150getIState :: Idris IState
151getIState = get
153putIState :: IState -> Idris ()
154putIState = put
156getName :: Idris Int
157getName = do i <- get;
158 let idx = idris_name i;
159 put (i { idris_name = idx + 1 })
160 return idx
162checkUndefined :: FC -> Name -> Idris ()
163checkUndefined fc n
164 = do i <- getContext
165 case lookupTy Nothing n i of
166 (_:_) -> fail $ show fc ++ ":" ++
167 show n ++ " already defined"
168 _ -> return ()
170isUndefined :: FC -> Name -> Idris Bool
171isUndefined fc n
172 = do i <- getContext
173 case lookupTy Nothing n i of
174 (_:_) -> return False
175 _ -> return True
177setContext :: Context -> Idris ()
178setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
180updateContext :: (Context -> Context) -> Idris ()
181updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
183addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
184addConstraints fc (v, cs)
185 = do i <- get
186 let ctxt = tt_ctxt i
187 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
188 next_tvar = v }
189 let ics = zip cs (repeat fc) ++ idris_constraints i
190 put (i { tt_ctxt = ctxt', idris_constraints = ics })
192addDeferred :: [(Name, Type)] -> Idris ()
193addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
194 i <- get
195 put (i { idris_metavars = map fst ns ++ idris_metavars i })
196 where tidyNames used (Bind (MN i x) b sc)
197 = let n' = uniqueName (UN x) used in
198 Bind n' b $ tidyNames (n':used) sc
199 tidyNames used (Bind n b sc)
200 = let n' = uniqueName n used in
201 Bind n' b $ tidyNames (n':used) sc
202 tidyNames used b = b
204solveDeferred :: Name -> Idris ()
205solveDeferred n = do i <- get
206 put (i { idris_metavars = idris_metavars i \\ [n] })
208iputStrLn :: String -> Idris ()
209iputStrLn = liftIO . putStrLn
211iWarn :: FC -> String -> Idris ()
212iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
214setLogLevel :: Int -> Idris ()
215setLogLevel l = do i <- get
216 let opts = idris_options i
217 let opt' = opts { opt_logLevel = l }
218 put (i { idris_options = opt' } )
220setCmdLine :: [Opt] -> Idris ()
221setCmdLine opts = do i <- get
222 let iopts = idris_options i
223 put (i { idris_options = iopts { opt_cmdline = opts } })
225getDumpDefun :: Idris (Maybe FilePath)
226getDumpDefun = do i <- get
227 return $ findC (opt_cmdline (idris_options i))
228 where findC [] = Nothing
229 findC (DumpDefun x : _) = Just x
230 findC (_ : xs) = findC xs
232getDumpCases :: Idris (Maybe FilePath)
233getDumpCases = do i <- get
234 return $ findC (opt_cmdline (idris_options i))
235 where findC [] = Nothing
236 findC (DumpCases x : _) = Just x
237 findC (_ : xs) = findC xs
239logLevel :: Idris Int
240logLevel = do i <- get
241 return (opt_logLevel (idris_options i))
243setErrContext :: Bool -> Idris ()
244setErrContext t = do i <- get
245 let opts = idris_options i
246 let opt' = opts { opt_errContext = t }
247 put (i { idris_options = opt' })
249errContext :: Idris Bool
250errContext = do i <- get
251 return (opt_errContext (idris_options i))
253useREPL :: Idris Bool
254useREPL = do i <- get
255 return (opt_repl (idris_options i))
257setREPL :: Bool -> Idris ()
258setREPL t = do i <- get
259 let opts = idris_options i
260 let opt' = opts { opt_repl = t }
261 put (i { idris_options = opt' })
263setTarget :: Target -> Idris ()
264setTarget t = do i <- get
265 let opts = idris_options i
266 let opt' = opts { opt_target = t }
267 put (i { idris_options = opt' })
269target :: Idris Target
270target = do i <- get
271 return (opt_target (idris_options i))
273setOutputTy :: OutputType -> Idris ()
274setOutputTy t = do i <- get
275 let opts = idris_options i
276 let opt' = opts { opt_outputTy = t }
277 put (i { idris_options = opt' })
279outputTy :: Idris OutputType
280outputTy = do i <- get
281 return $ opt_outputTy $ idris_options i
283verbose :: Idris Bool
284verbose = do i <- get
285 return (opt_verbose (idris_options i))
287setVerbose :: Bool -> Idris ()
288setVerbose t = do i <- get
289 let opts = idris_options i
290 let opt' = opts { opt_verbose = t }
291 put (i { idris_options = opt' })
293typeInType :: Idris Bool
294typeInType = do i <- get
295 return (opt_typeintype (idris_options i))
297setTypeInType :: Bool -> Idris ()
298setTypeInType t = do i <- get
299 let opts = idris_options i
300 let opt' = opts { opt_typeintype = t }
301 put (i { idris_options = opt' })
303coverage :: Idris Bool
304coverage = do i <- get
305 return (opt_coverage (idris_options i))
307setCoverage :: Bool -> Idris ()
308setCoverage t = do i <- get
309 let opts = idris_options i
310 let opt' = opts { opt_coverage = t }
311 put (i { idris_options = opt' })
313setIBCSubDir :: FilePath -> Idris ()
314setIBCSubDir fp = do i <- get
315 let opts = idris_options i
316 let opt' = opts { opt_ibcsubdir = fp }
317 put (i { idris_options = opt' })
319valIBCSubDir :: IState -> Idris FilePath
320valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
322addImportDir :: FilePath -> Idris ()
323addImportDir fp = do i <- get
324 let opts = idris_options i
325 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
326 put (i { idris_options = opt' })
328setImportDirs :: [FilePath] -> Idris ()
329setImportDirs fps = do i <- get
330 let opts = idris_options i
331 let opt' = opts { opt_importdirs = fps }
332 put (i { idris_options = opt' })
334allImportDirs :: IState -> Idris [FilePath]
335allImportDirs i = do let optdirs = opt_importdirs (idris_options i)
336 return ("." : optdirs)
338impShow :: Idris Bool
339impShow = do i <- get
340 return (opt_showimp (idris_options i))
342setImpShow :: Bool -> Idris ()
343setImpShow t = do i <- get
344 let opts = idris_options i
345 let opt' = opts { opt_showimp = t }
346 put (i { idris_options = opt' })
348logLvl :: Int -> String -> Idris ()
349logLvl l str = do i <- get
350 let lvl = opt_logLevel (idris_options i)
351 when (lvl >= l)
352 $ do liftIO (putStrLn str)
353 put (i { idris_log = idris_log i ++ str ++ "\n" } )
355cmdOptSet :: Opt -> Idris Bool
356cmdOptSet x = do i <- get
357 return $ x `elem` opt_cmdline (idris_options i)
359iLOG :: String -> Idris ()
360iLOG = logLvl 1
362noErrors :: Idris Bool
363noErrors = do i <- get
364 case errLine i of
365 Nothing -> return True
366 _ -> return False
368setTypeCase :: Bool -> Idris ()
369setTypeCase t = do i <- get
370 let opts = idris_options i
371 let opt' = opts { opt_typecase = t }
372 put (i { idris_options = opt' })
375-- For inferring types of things
377bi = FC "builtin" 0
379inferTy = MN 0 "__Infer"
380inferCon = MN 0 "__infer"
381inferDecl = PDatadecl inferTy
382 PSet
383 [("", inferCon, PPi impl (MN 0 "A") PSet (
384 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
385 (PRef bi inferTy)), bi)]
387infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
388infP = P (TCon 6 0) inferTy (Set (UVal 0))
390getInferTerm, getInferType :: Term -> Term
391getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
392getInferTerm (App (App _ _) tm) = tm
393getInferTerm tm = error ("getInferTerm " ++ show tm)
395getInferType (Bind n b sc) = Bind n b $ getInferType sc
396getInferType (App (App _ ty) _) = ty
398-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
400primNames = [unitTy, unitCon,
401 falseTy, pairTy, pairCon,
402 eqTy, eqCon, inferTy, inferCon]
404unitTy = MN 0 "__Unit"
405unitCon = MN 0 "__II"
406unitDecl = PDatadecl unitTy PSet
407 [("", unitCon, PRef bi unitTy, bi)]
409falseTy = MN 0 "__False"
410falseDecl = PDatadecl falseTy PSet []
412pairTy = MN 0 "__Pair"
413pairCon = MN 0 "__MkPair"
414pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
415 [("", pairCon, PPi impl (n "A") PSet (
416 PPi impl (n "B") PSet (
417 PPi expl (n "a") (PRef bi (n "A")) (
418 PPi expl (n "b") (PRef bi (n "B"))
419 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
420 pexp (PRef bi (n "B"))])))), bi)]
421 where n a = MN 0 a
423eqTy = UN "="
424eqCon = UN "refl"
425eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
426 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
427 PSet)
428 [("", eqCon, PPi impl (n "a") PSet (
429 PPi impl (n "x") (PRef bi (n "a"))
430 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
431 pimp (n "b") Placeholder,
432 pexp (PRef bi (n "x")),
433 pexp (PRef bi (n "x"))])), bi)]
434 where n a = MN 0 a
436-- Defined in builtins.idr
437sigmaTy = UN "Exists"
438existsCon = UN "Ex_intro"
440piBind :: [(Name, PTerm)] -> PTerm -> PTerm
441piBind = piBindp expl
443piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
444piBindp p [] t = t
445piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)
447-- Dealing with parameters
449expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
450expandParams dec ps ns tm = en tm
451 where
452 -- if we shadow a name (say in a lambda binding) that is used in a call to
453 -- a lifted function, we need access to both names - once in the scope of the
454 -- binding and once to call the lifted functions. So we'll explicitly shadow
455 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
456 -- but we didn't...)
458 mkShadow (UN n) = MN 0 n
459 mkShadow (MN i n) = MN (i+1) n
460 mkShadow (NS x s) = NS (mkShadow x) s
462 en (PLam n t s)
463 | n `elem` map fst ps
464 = let n' = mkShadow n in
465 PLam n' (en t) (en (shadow n n' s))
466 | otherwise = PLam n (en t) (en s)
467 en (PPi p n t s)
468 | n `elem` map fst ps
469 = let n' = mkShadow n in
470 PPi p n' (en t) (en (shadow n n' s))
471 | otherwise = PPi p n (en t) (en s)
472 en (PLet n ty v s)
473 | n `elem` map fst ps
474 = let n' = mkShadow n in
475 PLet n' (en ty) (en v) (en (shadow n n' s))
476 | otherwise = PLet n (en ty) (en v) (en s)
477 en (PEq f l r) = PEq f (en l) (en r)
478 en (PTyped l r) = PTyped (en l) (en r)
479 en (PPair f l r) = PPair f (en l) (en r)
480 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
481 en (PAlternative a as) = PAlternative a (map en as)
482 en (PHidden t) = PHidden (en t)
483 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
484 en (PProof ts) = PProof (map (fmap en) ts)
485 en (PTactics ts) = PTactics (map (fmap en) ts)
487 en (PQuote (Var n))
488 | n `nselem` ns = PQuote (Var (dec n))
489 en (PApp fc (PRef fc' n) as)
490 | n `nselem` ns = PApp fc (PRef fc' (dec n))
491 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
492 en (PRef fc n)
493 | n `nselem` ns = PApp fc (PRef fc (dec n))
494 (map (pexp . (PRef fc)) (map fst ps))
495 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
496 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
497 en t = t
499 nselem x [] = False
500 nselem x (y : xs) | nseq x y = True
501 | otherwise = nselem x xs
503 nseq x y = nsroot x == nsroot y
505expandParamsD :: Bool -> -- True = RHS only
506 IState ->
507 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
508expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
509 = if n `elem` ns && (not rhsonly)
510 then -- trace (show (n, expandParams dec ps ns ty)) $
511 PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
512 else --trace (show (n, expandParams dec ps ns ty)) $
513 PTy doc syn fc o n (expandParams dec ps ns ty)
514expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
515 = let n' = if n `elem` ns then dec n else n in
516 PClauses fc opts n' (map expandParamsC cs)
517 where
518 expandParamsC (PClause fc n lhs ws rhs ds)
519 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
520 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
521 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns lhs)
522 n' = if n `elem` ns then dec n else n in
523 PClause fc n' lhs'
524 (map (expandParams dec ps'' ns) ws)
525 (expandParams dec ps'' ns rhs)
526 (map (expandParamsD True ist dec ps'' ns) ds)
527 expandParamsC (PWith fc n lhs ws wval ds)
528 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
529 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
530 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns lhs)
531 n' = if n `elem` ns then dec n else n in
532 PWith fc n' lhs'
533 (map (expandParams dec ps'' ns) ws)
534 (expandParams dec ps'' ns wval)
535 (map (expandParamsD rhsonly ist dec ps'' ns) ds)
536 updateps yn nm [] = []
537 updateps yn nm (((a, t), i):as)
538 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
539 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
540expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
541 = PData doc syn fc co (expandPData pd)
542 where
543 -- just do the type decl, leave constructors alone (parameters will be
544 -- added implicitly)
545 expandPData (PDatadecl n ty cons)
546 = if n `elem` ns
547 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns ty)) (map econ cons)
548 else PDatadecl n (expandParams dec ps ns ty) (map econ cons)
549 econ (doc, n, t, fc)
550 = (doc, dec n, piBindp expl ps (expandParams dec ps ns t), fc)
551expandParamsD rhs ist dec ps ns (PParams f params pds)
552 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns)) params)
553 (map (expandParamsD True ist dec ps ns) pds)
554-- (map (expandParamsD ist dec ps ns) pds)
555expandParamsD rhs ist dec ps ns (PMutual f pds)
556 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
557expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
558 = PClass doc info f
559 (map (expandParams dec ps ns) cs)
560 n
561 (map (mapsnd (expandParams dec ps ns)) params)
562 (map (expandParamsD rhs ist dec ps ns) decls)
563expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
564 = PInstance info f
565 (map (expandParams dec ps ns) cs)
566 n
567 (map (expandParams dec ps ns) params)
568 (expandParams dec ps ns ty)
569 cn
570 (map (expandParamsD rhs ist dec ps ns) decls)
571expandParamsD rhs ist dec ps ns d = d
573mapsnd f (x, t) = (x, f t)
575-- Calculate a priority for a type, for deciding elaboration order
576-- * if it's just a type variable or concrete type, do it early (0)
577-- * if there's only type variables and injective constructors, do it next (1)
578-- * if there's a function type, next (2)
579-- * finally, everything else (3)
581getPriority :: IState -> PTerm -> Int
582getPriority i tm = 1 -- pri tm
583 where
584 pri (PRef _ n) =
585 case lookupP Nothing n (tt_ctxt i) of
586 ((P (DCon _ _) _ _):_) -> 1
587 ((P (TCon _ _) _ _):_) -> 1
588 ((P Ref _ _):_) -> 1
589 [] -> 0 -- must be locally bound, if it's not an error...
590 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
591 pri (PTrue _) = 0
592 pri (PFalse _) = 0
593 pri (PRefl _ _) = 1
594 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
595 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
596 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
597 pri (PTyped l r) = pri l
598 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
599 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
600 pri (PAlternative a as) = maximum (map pri as)
601 pri (PConstant _) = 0
602 pri Placeholder = 1
603 pri _ = 3
605addStatics :: Name -> Term -> PTerm -> Idris ()
606addStatics n tm ptm =
607 do let (statics, dynamics) = initStatics tm ptm
608 let stnames = nub $ concatMap freeNames (map snd statics)
609 let dnames = nub $ concatMap freeNames (map snd dynamics)
610 when (not (null statics)) $
611 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
612 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
613 let statics' = nub $ map fst statics ++
614 filter (\x -> not (elem x dnames)) stnames
615 let stpos = staticList statics' tm
616 i <- get
617 put (i { idris_statics = addDef n stpos (idris_statics i) })
618 addIBC (IBCStatic n)
619 where
620 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
621 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
622 if pstatic p == Static then ((n, ty) : static, dynamic)
623 else (static, (n, ty) : dynamic)
624 initStatics t pt = ([], [])
626 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
627 staticList _ _ = []
629-- Dealing with implicit arguments
631-- Add implicit Pi bindings for any names in the term which appear in an
632-- argument position.
634-- This has become a right mess already. Better redo it some time...
636implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
637implicit syn n ptm = implicit' syn [] n ptm
639implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
640implicit' syn ignore n ptm
641 = do i <- get
642 let (tm', impdata) = implicitise syn ignore i ptm
643-- let (tm'', spos) = findStatics i tm'
644 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
645 addIBC (IBCImp n)
646 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
647-- i <- get
648-- put (i { idris_statics = addDef n spos (idris_statics i) })
649 return tm'
651implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
652implicitise syn ignore ist tm
653 = let (declimps, ns') = execState (imps True [] tm) ([], [])
654 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
655 ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
656 if null ns
657 then (tm, reverse declimps)
658 else implicitise syn ignore ist (pibind uvars ns tm)
659 where
660 uvars = using syn
661 pvars = syn_params syn
663 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
664 | otherwise = x : dropAll xs ys
665 dropAll [] ys = []
667 imps top env (PApp _ f as)
668 = do (decls, ns) <- get
669 let isn = concatMap (namesIn uvars ist) (map getTm as)
670 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
671 imps top env (PPi (Imp l _ doc) n ty sc)
672 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
673 (decls , ns) <- get
674 put (PImp (getPriority ist ty) l n ty doc : decls,
675 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
676 imps True (n:env) sc
677 imps top env (PPi (Exp l _ doc) n ty sc)
678 = do let isn = nub (namesIn uvars ist ty ++ case sc of
679 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
680 _ -> [])
681 (decls, ns) <- get -- ignore decls in HO types
682 put (PExp (getPriority ist ty) l ty doc : decls,
683 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
684 imps True (n:env) sc
685 imps top env (PPi (Constraint l _ doc) n ty sc)
686 = do let isn = nub (namesIn uvars ist ty ++ case sc of
687 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
688 _ -> [])
689 (decls, ns) <- get -- ignore decls in HO types
690 put (PConstraint 10 l ty doc : decls,
691 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
692 imps True (n:env) sc
693 imps top env (PPi (TacImp l _ scr doc) n ty sc)
694 = do let isn = nub (namesIn uvars ist ty ++ case sc of
695 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
696 _ -> [])
697 (decls, ns) <- get -- ignore decls in HO types
698 put (PTacImplicit 10 l n scr ty doc : decls,
699 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
700 imps True (n:env) sc
701 imps top env (PEq _ l r)
702 = do (decls, ns) <- get
703 let isn = namesIn uvars ist l ++ namesIn uvars ist r
704 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
705 imps top env (PTyped l r)
706 = imps top env l
707 imps top env (PPair _ l r)
708 = do (decls, ns) <- get
709 let isn = namesIn uvars ist l ++ namesIn uvars ist r
710 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
711 imps top env (PDPair _ (PRef _ n) t r)
712 = do (decls, ns) <- get
713 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
714 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
715 imps top env (PDPair _ l t r)
716 = do (decls, ns) <- get
717 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
718 namesIn uvars ist r
719 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
720 imps top env (PAlternative a as)
721 = do (decls, ns) <- get
722 let isn = concatMap (namesIn uvars ist) as
723 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
724 imps top env (PLam n ty sc)
725 = do imps False env ty
726 imps False (n:env) sc
727 imps top env (PHidden tm) = imps False env tm
728 imps top env _ = return ()
730 pibind using [] sc = sc
731 pibind using (n:ns) sc
732 = case lookup n using of
733 Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)
734 Nothing -> PPi (Imp False Dynamic "") n Placeholder
735 (pibind using ns sc)
737-- Add implicit arguments in function calls
738addImplPat :: IState -> PTerm -> PTerm
739addImplPat = addImpl' True []
741addImplBound :: IState -> [Name] -> PTerm -> PTerm
742addImplBound ist ns = addImpl' False ns ist
744addImpl :: IState -> PTerm -> PTerm
745addImpl = addImpl' False []
747-- TODO: in patterns, don't add implicits to function names guarded by constructors
748-- and *not* inside a PHidden
750addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
751addImpl' inpat env ist ptm = ai env ptm
752 where
753 ai env (PRef fc f)
754 | not (f `elem` env) = handleErr $ aiFn inpat inpat ist fc f []
755 ai env (PHidden (PRef fc f))
756 | not (f `elem` env) = handleErr $ aiFn inpat False ist fc f []
757 ai env (PEq fc l r) = let l' = ai env l
758 r' = ai env r in
759 PEq fc l' r'
760 ai env (PTyped l r) = let l' = ai env l
761 r' = ai env r in
762 PTyped l' r'
763 ai env (PPair fc l r) = let l' = ai env l
764 r' = ai env r in
765 PPair fc l' r'
766 ai env (PDPair fc l t r) = let l' = ai env l
767 t' = ai env t
768 r' = ai env r in
769 PDPair fc l' t' r'
770 ai env (PAlternative a as) = let as' = map (ai env) as in
771 PAlternative a as'
772 ai env (PApp fc (PRef _ f) as)
773 | not (f `elem` env)
774 = let as' = map (fmap (ai env)) as in
775 handleErr $ aiFn inpat False ist fc f as'
776 ai env (PApp fc f as) = let f' = ai env f
777 as' = map (fmap (ai env)) as in
778 mkPApp fc 1 f' as'
779 ai env (PCase fc c os) = let c' = ai env c
780 os' = map (pmap (ai env)) os in
781 PCase fc c' os'
782 ai env (PLam n ty sc) = let ty' = ai env ty
783 sc' = ai (n:env) sc in
784 PLam n ty' sc'
785 ai env (PLet n ty val sc)
786 = let ty' = ai env ty
787 val' = ai env val
788 sc' = ai (n:env) sc in
789 PLet n ty' val' sc'
790 ai env (PPi p n ty sc) = let ty' = ai env ty
791 sc' = ai (n:env) sc in
792 PPi p n ty' sc'
793 ai env (PHidden tm) = PHidden (ai env tm)
794 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
795 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
796 ai env tm = tm
798 handleErr (Left err) = PElabError err
799 handleErr (Right x) = x
801-- if in a pattern, and there are no arguments, and there's no possible
802-- names with zero explicit arguments, don't add implicits.
804aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
805aiFn inpat True ist fc f []
806 = case lookupDef Nothing f (tt_ctxt ist) of
807 [] -> Right $ PPatvar fc f
808 alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
809 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
810 if (not (vname f) || tcname f
811 || any constructor alts || any allImp ialts)
812 then aiFn inpat False ist fc f [] -- use it as a constructor
813 else Right $ PPatvar fc f
814 where imp (PExp _ _ _ _) = False
815 imp _ = True
816 allImp [] = False
817 allImp xs = all imp xs
818 constructor (TyDecl (DCon _ _) _) = True
819 constructor _ = False
821 vname (UN n) = True -- non qualified
822 vname _ = False
824aiFn inpat expat ist fc f as
825 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
826aiFn inpat expat ist fc f as
827 -- This is where namespaces get resolved by adding PAlternative
828 = case lookupCtxtName Nothing f (idris_implicits ist) of
829 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
830 [] -> if f `elem` idris_metavars ist
831 then Right $ PApp fc (PRef fc f) as
832 else Right $ mkPApp fc (length as) (PRef fc f) as
833 alts -> Right $
834 PAlternative True $
835 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
836 (insertImpl ns as)) alts
837 where
838 insertImpl :: [PArg] -> [PArg] -> [PArg]
839 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
840 PExp p l tm d : insertImpl ps given
841 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
842 PConstraint p l tm d : insertImpl ps given
843 insertImpl (PConstraint p l ty d : ps) given =
844 PConstraint p l (PResolveTC fc) d : insertImpl ps given
845 insertImpl (PImp p l n ty d : ps) given =
846 case find n given [] of
847 Just (tm, given') -> PImp p l n tm "" : insertImpl ps given'
848 Nothing -> PImp p l n Placeholder "" : insertImpl ps given
849 insertImpl (PTacImplicit p l n sc ty d : ps) given =
850 case find n given [] of
851 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
852 Nothing -> if inpat
853 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
854 else PTacImplicit p l n sc sc "" : insertImpl ps given
855 insertImpl expected [] = []
856 insertImpl _ given = given
858 find n [] acc = Nothing
859 find n (PImp _ _ n' t _ : gs) acc
860 | n == n' = Just (t, reverse acc ++ gs)
861 find n (PTacImplicit _ _ n' _ t _ : gs) acc
862 | n == n' = Just (t, reverse acc ++ gs)
863 find n (g : gs) acc = find n gs (g : acc)
865mkPApp fc a f [] = f
866mkPApp fc a f as = let rest = drop a as in
867 appRest fc (PApp fc f (take a as)) rest
868 where
869 appRest fc f [] = f
870 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
872-- Find 'static' argument positions
873-- (the declared ones, plus any names in argument position in the declared
874-- statics)
875-- FIXME: It's possible that this really has to happen after elaboration
877findStatics :: IState -> PTerm -> (PTerm, [Bool])
878findStatics ist tm = trace (showImp True tm) $
879 let (ns, ss) = fs tm in
880 runState (pos ns ss tm) []
881 where fs (PPi p n t sc)
882 | Static <- pstatic p
883 = let (ns, ss) = fs sc in
884 (namesIn [] ist t : ns, n : ss)
885 | otherwise = let (ns, ss) = fs sc in
886 (ns, ss)
887 fs _ = ([], [])
889 inOne n ns = length (filter id (map (elem n) ns)) == 1
891 pos ns ss (PPi p n t sc)
892 | elem n ss = do sc' <- pos ns ss sc
893 spos <- get
894 put (True : spos)
895 return (PPi (p { pstatic = Static }) n t sc')
896 | otherwise = do sc' <- pos ns ss sc
897 spos <- get
898 put (False : spos)
899 return (PPi p n t sc')
900 pos ns ss t = return t
902-- Debugging/logging stuff
904dumpDecls :: [PDecl] -> String
905dumpDecls [] = ""
906dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
908dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
909dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
910dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
911dumpDecl (PData _ _ _ _ d) = showDImp True d
912dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
913dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
914dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
915dumpDecl (PClass _ _ _ cs n ps ds)
916 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
917dumpDecl (PInstance _ _ cs n _ t _ ds)
918 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
919dumpDecl _ = "..."
920-- dumpDecl (PImport i) = "import " ++ i
922-- for 6.12/7 compatibility
923data EitherErr a b = LeftErr a | RightOK b
925instance Monad (EitherErr a) where
926 return = RightOK
928 (LeftErr e) >>= k = LeftErr e
929 RightOK v >>= k = k v
931toEither (LeftErr e) = Left e
932toEither (RightOK ho) = Right ho
934-- syntactic match of a against b, returning pair of variables in a
935-- and what they match. Returns the pair that failed if not a match.
937matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
938matchClause = matchClause' False
940matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
941matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
942 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
944 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
945 fullApp x = x
947 match' x y = match (fullApp x) (fullApp y)
948 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
949 | PConstant (I _) <- getTm x = match (getTm x) x'
950 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
951 | PConstant (I _) <- getTm x = match (getTm x) x'
952 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
953 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
954 match (PApp _ f args) (PApp _ f' args')
955 | length args == length args'
956 = do mf <- match' f f'
957 ms <- zipWithM matchArg args args'
958 return (mf ++ concat ms)
959-- match (PRef _ n) (PRef _ n') | n == n' = return []
960-- | otherwise = Nothing
961 match (PRef f n) (PApp _ x []) = match (PRef f n) x
962 match (PApp _ x []) (PRef f n) = match x (PRef f n)
963 match (PRef _ n) tm@(PRef _ n')
964 | n == n' && not names &&
965 (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
966 = return [(n, tm)]
967 | n == n' = return []
968 match (PRef _ n) tm
969 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
970 = return [(n, tm)]
971 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
972 mr <- match' r r'
973 return (ml ++ mr)
974 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
975 mr <- match r r'
976 return (ml ++ mr)
977 match (PTyped l r) x = match l x
978 match x (PTyped l r) = match x l
979 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
980 mr <- match' r r'
981 return (ml ++ mr)
982 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
983 mt <- match' t t'
984 mr <- match' r r'
985 return (ml ++ mt ++ mr)
986 match (PAlternative a as) (PAlternative a' as')
987 = do ms <- zipWithM match' as as'
988 return (concat ms)
989 match a@(PAlternative _ as) b
990 = do let ms = zipWith match' as (repeat b)
991 case (rights (map toEither ms)) of
992 (x: _) -> return x
993 _ -> LeftErr (a, b)
994 match (PCase _ _ _) _ = return [] -- lifted out
995 match (PMetavar _) _ = return [] -- modified
996 match (PQuote _) _ = return []
997 match (PProof _) _ = return []
998 match (PTactics _) _ = return []
999 match (PRefl _ _) (PRefl _ _) = return []
1000 match (PResolveTC _) (PResolveTC _) = return []
1001 match (PTrue _) (PTrue _) = return []
1002 match (PFalse _) (PFalse _) = return []
1003 match (PReturn _) (PReturn _) = return []
1004 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1005 ms <- match' s s'
1006 return (mt ++ ms)
1007 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1008 ms <- match' s s'
1009 return (mt ++ ms)
1010 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1011 mty <- match' ty ty'
1012 ms <- match' s s'
1013 return (mt ++ mty ++ ms)
1014 match (PHidden x) (PHidden y) = match' x y
1015 match Placeholder _ = return []
1016 match _ Placeholder = return []
1017 match (PResolveTC _) _ = return []
1018 match a b | a == b = return []
1019 | otherwise = LeftErr (a, b)
1021 checkRpts (RightOK ms) = check ms where
1022 check ((n,t):xs)
1023 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1024 then Left (t, t')
1025 else check xs
1026 check (_:xs) = check xs
1027 check [] = Right ms
1028 checkRpts (LeftErr x) = Left x
1030substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1031substMatches [] t = t
1032substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1034substMatch :: Name -> PTerm -> PTerm -> PTerm
1035substMatch n tm t = sm t where
1036 sm (PRef _ n') | n == n' = tm
1037 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1038 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1039 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1040 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1041 sm (PEq f x y) = PEq f (sm x) (sm y)
1042 sm (PTyped x y) = PTyped (sm x) (sm y)
1043 sm (PPair f x y) = PPair f (sm x) (sm y)
1044 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1045 sm (PAlternative a as) = PAlternative a (map sm as)
1046 sm (PHidden x) = PHidden (sm x)
1047 sm x = x
1049shadow :: Name -> Name -> PTerm -> PTerm
1050shadow n n' t = sm t where
1051 sm (PRef fc x) | n == x = PRef fc n'
1052 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1053 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1054 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1055 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1056 sm (PEq f x y) = PEq f (sm x) (sm y)
1057 sm (PTyped x y) = PTyped (sm x) (sm y)
1058 sm (PPair f x y) = PPair f (sm x) (sm y)
1059 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1060 sm (PAlternative a as) = PAlternative a (map sm as)
1061 sm (PHidden x) = PHidden (sm x)
1062 sm x = x