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