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