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