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