git.iko.soy/Idris-dev
on ca684b6 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1053 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 :: IState ->
506 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
507expandParamsD ist dec ps ns (PTy doc syn fc o n ty)
508 = if n `elem` ns
509 then PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
510 else PTy doc syn fc o n (expandParams dec ps ns ty)
511expandParamsD ist dec ps ns (PClauses fc opts n cs)
512 = let n' = if n `elem` ns then dec n else n in
513 PClauses fc opts n' (map expandParamsC cs)
514 where
515 expandParamsC (PClause fc n lhs ws rhs ds)
516 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
517 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
518 n' = if n `elem` ns then dec n else n in
519 PClause fc n' (expandParams dec ps'' ns lhs)
520 (map (expandParams dec ps'' ns) ws)
521 (expandParams dec ps'' ns rhs)
522 (map (expandParamsD ist dec ps'' ns) ds)
523 expandParamsC (PWith fc n lhs ws wval ds)
524 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
525 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
526 n' = if n `elem` ns then dec n else n in
527 PWith fc n' (expandParams dec ps'' ns lhs)
528 (map (expandParams dec ps'' ns) ws)
529 (expandParams dec ps'' ns wval)
530 (map (expandParamsD ist dec ps'' ns) ds)
531 updateps yn nm [] = []
532 updateps yn nm (((a, t), i):as)
533 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
534 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
535expandParamsD ist dec ps ns (PData doc syn fc co pd)
536 = PData doc syn fc co (expandPData pd)
537 where
538 -- just do the type decl, leave constructors alone (parameters will be
539 -- added implicitly)
540 expandPData (PDatadecl n ty cons)
541 = if n `elem` ns
542 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns ty)) (map econ cons)
543 else PDatadecl n (expandParams dec ps ns ty) (map econ cons)
544 econ (doc, n, t, fc)
545 = (doc, dec n, piBindp expl ps (expandParams dec ps ns t), fc)
546expandParamsD ist dec ps ns (PParams f params pds)
547 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns)) params) pds
548-- (map (expandParamsD ist dec ps ns) pds)
549expandParamsD ist dec ps ns (PMutual f pds)
550 = PMutual f (map (expandParamsD ist dec ps ns) pds)
551expandParamsD ist dec ps ns (PClass doc info f cs n params decls)
552 = PClass doc info f
553 (map (expandParams dec ps ns) cs)
554 n
555 (map (mapsnd (expandParams dec ps ns)) params)
556 (map (expandParamsD ist dec ps ns) decls)
557expandParamsD ist dec ps ns (PInstance info f cs n params ty cn decls)
558 = PInstance info f
559 (map (expandParams dec ps ns) cs)
560 n
561 (map (expandParams dec ps ns) params)
562 (expandParams dec ps ns ty)
563 cn
564 (map (expandParamsD ist dec ps ns) decls)
565expandParamsD ist dec ps ns d = d
567mapsnd f (x, t) = (x, f t)
569-- Calculate a priority for a type, for deciding elaboration order
570-- * if it's just a type variable or concrete type, do it early (0)
571-- * if there's only type variables and injective constructors, do it next (1)
572-- * if there's a function type, next (2)
573-- * finally, everything else (3)
575getPriority :: IState -> PTerm -> Int
576getPriority i tm = pri tm
577 where
578 pri (PRef _ n) =
579 case lookupP Nothing n (tt_ctxt i) of
580 ((P (DCon _ _) _ _):_) -> 1
581 ((P (TCon _ _) _ _):_) -> 1
582 ((P Ref _ _):_) -> 4
583 [] -> 0 -- must be locally bound, if it's not an error...
584 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
585 pri (PTrue _) = 0
586 pri (PFalse _) = 0
587 pri (PRefl _ _) = 1
588 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
589 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
590 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
591 pri (PTyped l r) = pri l
592 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
593 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
594 pri (PAlternative a as) = maximum (map pri as)
595 pri (PConstant _) = 0
596 pri Placeholder = 1
597 pri _ = 3
599addStatics :: Name -> Term -> PTerm -> Idris ()
600addStatics n tm ptm =
601 do let (statics, dynamics) = initStatics tm ptm
602 let stnames = nub $ concatMap freeNames (map snd statics)
603 let dnames = nub $ concatMap freeNames (map snd dynamics)
604 when (not (null statics)) $
605 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
606 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
607 let statics' = nub $ map fst statics ++
608 filter (\x -> not (elem x dnames)) stnames
609 let stpos = staticList statics' tm
610 i <- get
611 put (i { idris_statics = addDef n stpos (idris_statics i) })
612 addIBC (IBCStatic n)
613 where
614 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
615 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
616 if pstatic p == Static then ((n, ty) : static, dynamic)
617 else (static, (n, ty) : dynamic)
618 initStatics t pt = ([], [])
620 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
621 staticList _ _ = []
623-- Dealing with implicit arguments
625-- Add implicit Pi bindings for any names in the term which appear in an
626-- argument position.
628-- This has become a right mess already. Better redo it some time...
630implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
631implicit syn n ptm = implicit' syn [] n ptm
633implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
634implicit' syn ignore n ptm
635 = do i <- get
636 let (tm', impdata) = implicitise syn ignore i ptm
637-- let (tm'', spos) = findStatics i tm'
638 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
639 addIBC (IBCImp n)
640 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
641-- i <- get
642-- put (i { idris_statics = addDef n spos (idris_statics i) })
643 return tm'
645implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
646implicitise syn ignore ist tm
647 = let (declimps, ns') = execState (imps True [] tm) ([], [])
648 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
649 ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
650 if null ns
651 then (tm, reverse declimps)
652 else implicitise syn ignore ist (pibind uvars ns tm)
653 where
654 uvars = using syn
655 pvars = syn_params syn
657 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
658 | otherwise = x : dropAll xs ys
659 dropAll [] ys = []
661 imps top env (PApp _ f as)
662 = do (decls, ns) <- get
663 let isn = concatMap (namesIn uvars ist) (map getTm as)
664 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
665 imps top env (PPi (Imp l _ doc) n ty sc)
666 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
667 (decls , ns) <- get
668 put (PImp (getPriority ist ty) l n ty doc : decls,
669 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
670 imps True (n:env) sc
671 imps top env (PPi (Exp l _ doc) n ty sc)
672 = do let isn = nub (namesIn uvars ist ty ++ case sc of
673 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
674 _ -> [])
675 (decls, ns) <- get -- ignore decls in HO types
676 put (PExp (getPriority ist ty) l ty doc : decls,
677 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
678 imps True (n:env) sc
679 imps top env (PPi (Constraint l _ doc) n ty sc)
680 = do let isn = nub (namesIn uvars ist ty ++ case sc of
681 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
682 _ -> [])
683 (decls, ns) <- get -- ignore decls in HO types
684 put (PConstraint 10 l ty doc : decls,
685 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
686 imps True (n:env) sc
687 imps top env (PPi (TacImp l _ scr doc) n ty sc)
688 = do let isn = nub (namesIn uvars ist ty ++ case sc of
689 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
690 _ -> [])
691 (decls, ns) <- get -- ignore decls in HO types
692 put (PTacImplicit 10 l n scr ty doc : decls,
693 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
694 imps True (n:env) sc
695 imps top env (PEq _ l r)
696 = do (decls, ns) <- get
697 let isn = namesIn uvars ist l ++ namesIn uvars ist r
698 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
699 imps top env (PTyped l r)
700 = imps top env l
701 imps top env (PPair _ 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 (PDPair _ (PRef _ n) t r)
706 = do (decls, ns) <- get
707 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
708 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
709 imps top env (PDPair _ l t r)
710 = do (decls, ns) <- get
711 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
712 namesIn uvars ist r
713 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
714 imps top env (PAlternative a as)
715 = do (decls, ns) <- get
716 let isn = concatMap (namesIn uvars ist) as
717 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
718 imps top env (PLam n ty sc)
719 = do imps False env ty
720 imps False (n:env) sc
721 imps top env (PHidden tm) = imps False env tm
722 imps top env _ = return ()
724 pibind using [] sc = sc
725 pibind using (n:ns) sc
726 = case lookup n using of
727 Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)
728 Nothing -> PPi (Imp False Dynamic "") n Placeholder
729 (pibind using ns sc)
731-- Add implicit arguments in function calls
732addImplPat :: IState -> PTerm -> PTerm
733addImplPat = addImpl' True []
735addImplBound :: IState -> [Name] -> PTerm -> PTerm
736addImplBound ist ns = addImpl' False ns ist
738addImpl :: IState -> PTerm -> PTerm
739addImpl = addImpl' False []
741-- TODO: in patterns, don't add implicits to function names guarded by constructors
742-- and *not* inside a PHidden
744addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
745addImpl' inpat env ist ptm = ai env ptm
746 where
747 ai env (PRef fc f)
748 | not (f `elem` env) = handleErr $ aiFn inpat inpat ist fc f []
749 ai env (PHidden (PRef fc f))
750 | not (f `elem` env) = handleErr $ aiFn inpat False ist fc f []
751 ai env (PEq fc l r) = let l' = ai env l
752 r' = ai env r in
753 PEq fc l' r'
754 ai env (PTyped l r) = let l' = ai env l
755 r' = ai env r in
756 PTyped l' r'
757 ai env (PPair fc l r) = let l' = ai env l
758 r' = ai env r in
759 PPair fc l' r'
760 ai env (PDPair fc l t r) = let l' = ai env l
761 t' = ai env t
762 r' = ai env r in
763 PDPair fc l' t' r'
764 ai env (PAlternative a as) = let as' = map (ai env) as in
765 PAlternative a as'
766 ai env (PApp fc (PRef _ f) as)
767 | not (f `elem` env)
768 = let as' = map (fmap (ai env)) as in
769 handleErr $ aiFn inpat False ist fc f as'
770 ai env (PApp fc f as) = let f' = ai env f
771 as' = map (fmap (ai env)) as in
772 mkPApp fc 1 f' as'
773 ai env (PCase fc c os) = let c' = ai env c
774 os' = map (pmap (ai env)) os in
775 PCase fc c' os'
776 ai env (PLam n ty sc) = let ty' = ai env ty
777 sc' = ai (n:env) sc in
778 PLam n ty' sc'
779 ai env (PLet n ty val sc)
780 = let ty' = ai env ty
781 val' = ai env val
782 sc' = ai (n:env) sc in
783 PLet n ty' val' sc'
784 ai env (PPi p n ty sc) = let ty' = ai env ty
785 sc' = ai (n:env) sc in
786 PPi p n ty' sc'
787 ai env (PHidden tm) = PHidden (ai env tm)
788 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
789 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
790 ai env tm = tm
792 handleErr (Left err) = PElabError err
793 handleErr (Right x) = x
795-- if in a pattern, and there are no arguments, and there's no possible
796-- names with zero explicit arguments, don't add implicits.
798aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
799aiFn inpat True ist fc f []
800 = case lookupDef Nothing f (tt_ctxt ist) of
801 [] -> Right $ PPatvar fc f
802 alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
803 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
804 if (not (vname f) || tcname f
805 || any constructor alts || any allImp ialts)
806 then aiFn inpat False ist fc f [] -- use it as a constructor
807 else Right $ PPatvar fc f
808 where imp (PExp _ _ _ _) = False
809 imp _ = True
810 allImp [] = False
811 allImp xs = all imp xs
812 constructor (TyDecl (DCon _ _) _) = True
813 constructor _ = False
815 vname (UN n) = True -- non qualified
816 vname _ = False
818aiFn inpat expat ist fc f as
819 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
820aiFn inpat expat ist fc f as
821 -- This is where namespaces get resolved by adding PAlternative
822 = case lookupCtxtName Nothing f (idris_implicits ist) of
823 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
824 [] -> if f `elem` idris_metavars ist
825 then Right $ PApp fc (PRef fc f) as
826 else Right $ mkPApp fc (length as) (PRef fc f) as
827 alts -> Right $
828 PAlternative True $
829 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
830 (insertImpl ns as)) alts
831 where
832 insertImpl :: [PArg] -> [PArg] -> [PArg]
833 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
834 PExp p l tm d : insertImpl ps given
835 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
836 PConstraint p l tm d : insertImpl ps given
837 insertImpl (PConstraint p l ty d : ps) given =
838 PConstraint p l (PResolveTC fc) d : insertImpl ps given
839 insertImpl (PImp p l n ty d : ps) given =
840 case find n given [] of
841 Just (tm, given') -> PImp p l n tm "" : insertImpl ps given'
842 Nothing -> PImp p l n Placeholder "" : insertImpl ps given
843 insertImpl (PTacImplicit p l n sc ty d : ps) given =
844 case find n given [] of
845 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
846 Nothing -> if inpat
847 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
848 else PTacImplicit p l n sc sc "" : insertImpl ps given
849 insertImpl expected [] = []
850 insertImpl _ given = given
852 find n [] acc = Nothing
853 find n (PImp _ _ n' t _ : gs) acc
854 | n == n' = Just (t, reverse acc ++ gs)
855 find n (PTacImplicit _ _ n' _ t _ : gs) acc
856 | n == n' = Just (t, reverse acc ++ gs)
857 find n (g : gs) acc = find n gs (g : acc)
859mkPApp fc a f [] = f
860mkPApp fc a f as = let rest = drop a as in
861 appRest fc (PApp fc f (take a as)) rest
862 where
863 appRest fc f [] = f
864 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
866-- Find 'static' argument positions
867-- (the declared ones, plus any names in argument position in the declared
868-- statics)
869-- FIXME: It's possible that this really has to happen after elaboration
871findStatics :: IState -> PTerm -> (PTerm, [Bool])
872findStatics ist tm = trace (showImp True tm) $
873 let (ns, ss) = fs tm in
874 runState (pos ns ss tm) []
875 where fs (PPi p n t sc)
876 | Static <- pstatic p
877 = let (ns, ss) = fs sc in
878 (namesIn [] ist t : ns, n : ss)
879 | otherwise = let (ns, ss) = fs sc in
880 (ns, ss)
881 fs _ = ([], [])
883 inOne n ns = length (filter id (map (elem n) ns)) == 1
885 pos ns ss (PPi p n t sc)
886 | elem n ss = do sc' <- pos ns ss sc
887 spos <- get
888 put (True : spos)
889 return (PPi (p { pstatic = Static }) n t sc')
890 | otherwise = do sc' <- pos ns ss sc
891 spos <- get
892 put (False : spos)
893 return (PPi p n t sc')
894 pos ns ss t = return t
896-- Debugging/logging stuff
898dumpDecls :: [PDecl] -> String
899dumpDecls [] = ""
900dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
902dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
903dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
904dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
905dumpDecl (PData _ _ _ _ d) = showDImp True d
906dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
907dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
908dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
909dumpDecl (PClass _ _ _ cs n ps ds)
910 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
911dumpDecl (PInstance _ _ cs n _ t _ ds)
912 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
913dumpDecl _ = "..."
914-- dumpDecl (PImport i) = "import " ++ i
916-- for 6.12/7 compatibility
917data EitherErr a b = LeftErr a | RightOK b
919instance Monad (EitherErr a) where
920 return = RightOK
922 (LeftErr e) >>= k = LeftErr e
923 RightOK v >>= k = k v
925toEither (LeftErr e) = Left e
926toEither (RightOK ho) = Right ho
928-- syntactic match of a against b, returning pair of variables in a
929-- and what they match. Returns the pair that failed if not a match.
931matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
932matchClause = matchClause' False
934matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
935matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
936 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
938 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
939 fullApp x = x
941 match' x y = match (fullApp x) (fullApp y)
942 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
943 | PConstant (I _) <- getTm x = match (getTm x) x'
944 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
945 | PConstant (I _) <- getTm x = match (getTm x) x'
946 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
947 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
948 match (PApp _ f args) (PApp _ f' args')
949 | length args == length args'
950 = do mf <- match' f f'
951 ms <- zipWithM matchArg args args'
952 return (mf ++ concat ms)
953-- match (PRef _ n) (PRef _ n') | n == n' = return []
954-- | otherwise = Nothing
955 match (PRef f n) (PApp _ x []) = match (PRef f n) x
956 match (PApp _ x []) (PRef f n) = match x (PRef f n)
957 match (PRef _ n) (PRef _ n') | n == n' = return []
958 match (PRef _ n) tm
959 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
960 = return [(n, tm)]
961 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
962 mr <- match' r r'
963 return (ml ++ mr)
964 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
965 mr <- match r r'
966 return (ml ++ mr)
967 match (PTyped l r) x = match l x
968 match x (PTyped l r) = match x l
969 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
970 mr <- match' r r'
971 return (ml ++ mr)
972 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
973 mt <- match' t t'
974 mr <- match' r r'
975 return (ml ++ mt ++ mr)
976 match (PAlternative a as) (PAlternative a' as')
977 = do ms <- zipWithM match' as as'
978 return (concat ms)
979 match a@(PAlternative _ as) b
980 = do let ms = zipWith match' as (repeat b)
981 case (rights (map toEither ms)) of
982 (x: _) -> return x
983 _ -> LeftErr (a, b)
984 match (PCase _ _ _) _ = return [] -- lifted out
985 match (PMetavar _) _ = return [] -- modified
986 match (PQuote _) _ = return []
987 match (PProof _) _ = return []
988 match (PTactics _) _ = return []
989 match (PRefl _ _) (PRefl _ _) = return []
990 match (PResolveTC _) (PResolveTC _) = return []
991 match (PTrue _) (PTrue _) = return []
992 match (PFalse _) (PFalse _) = return []
993 match (PReturn _) (PReturn _) = return []
994 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
995 ms <- match' s s'
996 return (mt ++ ms)
997 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
998 ms <- match' s s'
999 return (mt ++ ms)
1000 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1001 mty <- match' ty ty'
1002 ms <- match' s s'
1003 return (mt ++ mty ++ ms)
1004 match (PHidden x) (PHidden y) = match' x y
1005 match Placeholder _ = return []
1006 match _ Placeholder = return []
1007 match (PResolveTC _) _ = return []
1008 match a b | a == b = return []
1009 | otherwise = LeftErr (a, b)
1011 checkRpts (RightOK ms) = check ms where
1012 check ((n,t):xs)
1013 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1014 then Left (t, t')
1015 else check xs
1016 check (_:xs) = check xs
1017 check [] = Right ms
1018 checkRpts (LeftErr x) = Left x
1020substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1021substMatches [] t = t
1022substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1024substMatch :: Name -> PTerm -> PTerm -> PTerm
1025substMatch n tm t = sm t where
1026 sm (PRef _ n') | n == n' = tm
1027 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1028 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1029 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1030 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1031 sm (PEq f x y) = PEq f (sm x) (sm y)
1032 sm (PTyped x y) = PTyped (sm x) (sm y)
1033 sm (PPair f x y) = PPair f (sm x) (sm y)
1034 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1035 sm (PAlternative a as) = PAlternative a (map sm as)
1036 sm (PHidden x) = PHidden (sm x)
1037 sm x = x
1039shadow :: Name -> Name -> PTerm -> PTerm
1040shadow n n' t = sm t where
1041 sm (PRef fc x) | n == x = PRef fc n'
1042 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1043 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1044 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1045 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1046 sm (PEq f x y) = PEq f (sm x) (sm y)
1047 sm (PTyped x y) = PTyped (sm x) (sm y)
1048 sm (PPair f x y) = PPair f (sm x) (sm y)
1049 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1050 sm (PAlternative a as) = PAlternative a (map sm as)
1051 sm (PHidden x) = PHidden (sm x)
1052 sm x = x