git.iko.soy/Idris-dev
on 79e6bf7 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
933 lines 37 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 RTS.SC
13import Paths_idris
15import System.Console.Haskeline
17import Control.Monad.State
19import Data.List
20import Data.Char
21import Data.Either
23import Debug.Trace
25import qualified Epic.Epic as E
27import Util.Pretty
30getContext :: Idris Context
31getContext = do i <- get; return (tt_ctxt i)
33getObjectFiles :: Idris [FilePath]
34getObjectFiles = do i <- get; return (idris_objs i)
36addObjectFile :: FilePath -> Idris ()
37addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
39getLibs :: Idris [String]
40getLibs = do i <- get; return (idris_libs i)
42addLib :: String -> Idris ()
43addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
45addHdr :: String -> Idris ()
46addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
48totcheck :: (FC, Name) -> Idris ()
49totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i })
51setFlags :: Name -> [FnOpt] -> Idris ()
52setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
54setAccessibility :: Name -> Accessibility -> Idris ()
55setAccessibility n a
56 = do i <- get
57 let ctxt = setAccess n a (tt_ctxt i)
58 put (i { tt_ctxt = ctxt })
60setTotality :: Name -> Totality -> Idris ()
61setTotality n a
62 = do i <- get
63 let ctxt = setTotal n a (tt_ctxt i)
64 put (i { tt_ctxt = ctxt })
66getTotality :: Name -> Idris Totality
67getTotality n
68 = do i <- get
69 case lookupTotal n (tt_ctxt i) of
70 [t] -> return t
71 _ -> return (Total [])
73addToCG :: Name -> [Name] -> Idris ()
74addToCG n ns = do i <- get
75 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
77addToCalledG :: Name -> [Name] -> Idris ()
78addToCalledG n ns = return () -- TODO
80-- Add a class instance function. Dodgy hack: Put integer instances first in the
81-- list so they are resolved by default.
83addInstance :: Bool -> Name -> Name -> Idris ()
84addInstance int n i
85 = do ist <- get
86 case lookupCtxt Nothing n (idris_classes ist) of
87 [CI a b c d ins] ->
88 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
89 put (ist { idris_classes = cs })
90 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
91 put (ist { idris_classes = cs })
92 where addI i ins | int = i : ins
93 | otherwise = ins ++ [i]
95addClass :: Name -> ClassInfo -> Idris ()
96addClass n i
97 = do ist <- get
98 let i' = case lookupCtxt Nothing n (idris_classes ist) of
99 [c] -> c { class_instances = class_instances i }
100 _ -> i
101 put (ist { idris_classes = addDef n i' (idris_classes ist) })
103addIBC :: IBCWrite -> Idris ()
104addIBC ibc@(IBCDef n)
105 = do i <- get
106 when (notDef (ibc_write i)) $
107 put (i { ibc_write = ibc : ibc_write i })
108 where notDef [] = True
109 notDef (IBCDef n': is) | n == n' = False
110 notDef (_ : is) = notDef is
111addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
113clearIBC :: Idris ()
114clearIBC = do i <- get; put (i { ibc_write = [] })
116getHdrs :: Idris [String]
117getHdrs = do i <- get; return (idris_hdrs i)
119setErrLine :: Int -> Idris ()
120setErrLine x = do i <- get;
121 case (errLine i) of
122 Nothing -> put (i { errLine = Just x })
123 Just _ -> return ()
125clearErr :: Idris ()
126clearErr = do i <- get
127 put (i { errLine = Nothing })
129getSO :: Idris (Maybe String)
130getSO = do i <- get
131 return (compiled_so i)
133setSO :: Maybe String -> Idris ()
134setSO s = do i <- get
135 put (i { compiled_so = s })
137getIState :: Idris IState
138getIState = get
140putIState :: IState -> Idris ()
141putIState = put
143getName :: Idris Int
144getName = do i <- get;
145 let idx = idris_name i;
146 put (i { idris_name = idx + 1 })
147 return idx
149checkUndefined :: FC -> Name -> Idris ()
150checkUndefined fc n
151 = do i <- getContext
152 case lookupTy Nothing n i of
153 (_:_) -> fail $ show fc ++ ":" ++
154 show n ++ " already defined"
155 _ -> return ()
157setContext :: Context -> Idris ()
158setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
160updateContext :: (Context -> Context) -> Idris ()
161updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
163addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
164addConstraints fc (v, cs)
165 = do i <- get
166 let ctxt = tt_ctxt i
167 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
168 next_tvar = v }
169 let ics = zip cs (repeat fc) ++ idris_constraints i
170 put (i { tt_ctxt = ctxt', idris_constraints = ics })
172addDeferred :: [(Name, Type)] -> Idris ()
173addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
174 i <- get
175 put (i { idris_metavars = map fst ns ++ idris_metavars i })
176 where tidyNames used (Bind (MN i x) b sc)
177 = let n' = uniqueName (UN x) used in
178 Bind n' b $ tidyNames (n':used) sc
179 tidyNames used (Bind n b sc)
180 = let n' = uniqueName n used in
181 Bind n' b $ tidyNames (n':used) sc
182 tidyNames used b = b
184solveDeferred :: Name -> Idris ()
185solveDeferred n = do i <- get
186 put (i { idris_metavars = idris_metavars i \\ [n] })
188iputStrLn :: String -> Idris ()
189iputStrLn = liftIO . putStrLn
191iWarn :: FC -> String -> Idris ()
192iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
194setLogLevel :: Int -> Idris ()
195setLogLevel l = do i <- get
196 let opts = idris_options i
197 let opt' = opts { opt_logLevel = l }
198 put (i { idris_options = opt' } )
200logLevel :: Idris Int
201logLevel = do i <- get
202 return (opt_logLevel (idris_options i))
204setErrContext :: Bool -> Idris ()
205setErrContext t = do i <- get
206 let opts = idris_options i
207 let opt' = opts { opt_errContext = t }
208 put (i { idris_options = opt' })
210errContext :: Idris Bool
211errContext = do i <- get
212 return (opt_errContext (idris_options i))
214useREPL :: Idris Bool
215useREPL = do i <- get
216 return (opt_repl (idris_options i))
218setREPL :: Bool -> Idris ()
219setREPL t = do i <- get
220 let opts = idris_options i
221 let opt' = opts { opt_repl = t }
222 put (i { idris_options = opt' })
224verbose :: Idris Bool
225verbose = do i <- get
226 return (opt_verbose (idris_options i))
228setVerbose :: Bool -> Idris ()
229setVerbose t = do i <- get
230 let opts = idris_options i
231 let opt' = opts { opt_verbose = t }
232 put (i { idris_options = opt' })
234typeInType :: Idris Bool
235typeInType = do i <- get
236 return (opt_typeintype (idris_options i))
238setTypeInType :: Bool -> Idris ()
239setTypeInType t = do i <- get
240 let opts = idris_options i
241 let opt' = opts { opt_typeintype = t }
242 put (i { idris_options = opt' })
244coverage :: Idris Bool
245coverage = do i <- get
246 return (opt_coverage (idris_options i))
248setCoverage :: Bool -> Idris ()
249setCoverage t = do i <- get
250 let opts = idris_options i
251 let opt' = opts { opt_coverage = t }
252 put (i { idris_options = opt' })
254setIBCSubDir :: FilePath -> Idris ()
255setIBCSubDir fp = do i <- get
256 let opts = idris_options i
257 let opt' = opts { opt_ibcsubdir = fp }
258 put (i { idris_options = opt' })
260valIBCSubDir :: IState -> Idris FilePath
261valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
263setImportDirs :: [FilePath] -> Idris ()
264setImportDirs fps = do i <- get
265 let opts = idris_options i
266 let opt' = opts { opt_importdirs = fps }
267 put (i { idris_options = opt' })
269allImportDirs :: IState -> Idris [FilePath]
270allImportDirs i = do datadir <- liftIO $ getDataDir
271 let optdirs = opt_importdirs (idris_options i)
272 return ("." : (optdirs ++ [datadir]))
274impShow :: Idris Bool
275impShow = do i <- get
276 return (opt_showimp (idris_options i))
278setImpShow :: Bool -> Idris ()
279setImpShow t = do i <- get
280 let opts = idris_options i
281 let opt' = opts { opt_showimp = t }
282 put (i { idris_options = opt' })
284logLvl :: Int -> String -> Idris ()
285logLvl l str = do i <- get
286 let lvl = opt_logLevel (idris_options i)
287 when (lvl >= l)
288 $ do liftIO (putStrLn str)
289 put (i { idris_log = idris_log i ++ str ++ "\n" } )
291iLOG :: String -> Idris ()
292iLOG = logLvl 1
294noErrors :: Idris Bool
295noErrors = do i <- get
296 case errLine i of
297 Nothing -> return True
298 _ -> return False
300setTypeCase :: Bool -> Idris ()
301setTypeCase t = do i <- get
302 let opts = idris_options i
303 let opt' = opts { opt_typecase = t }
304 put (i { idris_options = opt' })
307-- For inferring types of things
309bi = FC "builtin" 0
311inferTy = MN 0 "__Infer"
312inferCon = MN 0 "__infer"
313inferDecl = PDatadecl inferTy
314 PSet
315 [(inferCon, PPi impl (MN 0 "A") PSet (
316 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
317 (PRef bi inferTy)), bi)]
319infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
320infP = P (TCon 6 0) inferTy (Set (UVal 0))
322getInferTerm, getInferType :: Term -> Term
323getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
324getInferTerm (App (App _ _) tm) = tm
325getInferTerm tm = error ("getInferTerm " ++ show tm)
327getInferType (Bind n b sc) = Bind n b $ getInferType sc
328getInferType (App (App _ ty) _) = ty
330-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
332primNames = [unitTy, unitCon,
333 falseTy, pairTy, pairCon,
334 eqTy, eqCon, inferTy, inferCon]
336unitTy = MN 0 "__Unit"
337unitCon = MN 0 "__II"
338unitDecl = PDatadecl unitTy PSet
339 [(unitCon, PRef bi unitTy, bi)]
341falseTy = MN 0 "__False"
342falseDecl = PDatadecl falseTy PSet []
344pairTy = MN 0 "__Pair"
345pairCon = MN 0 "__MkPair"
346pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
347 [(pairCon, PPi impl (n "A") PSet (
348 PPi impl (n "B") PSet (
349 PPi expl (n "a") (PRef bi (n "A")) (
350 PPi expl (n "b") (PRef bi (n "B"))
351 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
352 pexp (PRef bi (n "B"))])))), bi)]
353 where n a = MN 0 a
355eqTy = UN "="
356eqCon = UN "refl"
357eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
358 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
359 PSet)
360 [(eqCon, PPi impl (n "a") PSet (
361 PPi impl (n "x") (PRef bi (n "a"))
362 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
363 pimp (n "b") Placeholder,
364 pexp (PRef bi (n "x")),
365 pexp (PRef bi (n "x"))])), bi)]
366 where n a = MN 0 a
368-- Defined in builtins.idr
369sigmaTy = UN "Exists"
370existsCon = UN "Ex_intro"
372piBind :: [(Name, PTerm)] -> PTerm -> PTerm
373piBind [] t = t
374piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
376tcname (UN ('@':_)) = True
377tcname (NS n _) = tcname n
378tcname _ = False
380-- Dealing with parameters
382expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
383expandParams dec ps ns tm = en tm
384 where
385 -- if we shadow a name (say in a lambda binding) that is used in a call to
386 -- a lifted function, we need access to both names - once in the scope of the
387 -- binding and once to call the lifted functions. So we'll explicitly shadow
388 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
389 -- but we didn't...)
391 mkShadow (UN n) = MN 0 n
392 mkShadow (MN i n) = MN (i+1) n
393 mkShadow (NS x s) = NS (mkShadow x) s
395 en (PLam n t s)
396 | n `elem` map fst ps
397 = let n' = mkShadow n in
398 PLam n' (en t) (en (shadow n n' s))
399 | otherwise = PLam n (en t) (en s)
400 en (PPi p n t s)
401 | n `elem` map fst ps
402 = let n' = mkShadow n in
403 PPi p n' (en t) (en (shadow n n' s))
404 | otherwise = PPi p n (en t) (en s)
405 en (PLet n ty v s)
406 | n `elem` map fst ps
407 = let n' = mkShadow n in
408 PLet n' (en ty) (en v) (en (shadow n n' s))
409 | otherwise = PLet n (en ty) (en v) (en s)
410 en (PEq f l r) = PEq f (en l) (en r)
411 en (PTyped l r) = PTyped (en l) (en r)
412 en (PPair f l r) = PPair f (en l) (en r)
413 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
414 en (PAlternative a as) = PAlternative a (map en as)
415 en (PHidden t) = PHidden (en t)
416 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
417 en (PProof ts) = PProof (map (fmap en) ts)
418 en (PTactics ts) = PTactics (map (fmap en) ts)
420 en (PQuote (Var n))
421 | n `elem` ns = PQuote (Var (dec n))
422 en (PApp fc (PRef fc' n) as)
423 | n `elem` ns = PApp fc (PRef fc' (dec n))
424 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
425 en (PRef fc n)
426 | n `elem` ns = PApp fc (PRef fc (dec n))
427 (map (pexp . (PRef fc)) (map fst ps))
428 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
429 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
430 en t = t
432expandParamsD :: IState ->
433 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
434expandParamsD ist dec ps ns (PTy syn fc o n ty)
435 = if n `elem` ns
436 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
437 else PTy syn fc o n (expandParams dec ps ns ty)
438expandParamsD ist dec ps ns (PClauses fc opts n cs)
439 = let n' = if n `elem` ns then dec n else n in
440 PClauses fc opts n' (map expandParamsC cs)
441 where
442 expandParamsC (PClause fc n lhs ws rhs ds)
443 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
444 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
445 n' = if n `elem` ns then dec n else n in
446 PClause fc n' (expandParams dec ps'' ns lhs)
447 (map (expandParams dec ps'' ns) ws)
448 (expandParams dec ps'' ns rhs)
449 (map (expandParamsD ist dec ps'' ns) ds)
450 expandParamsC (PWith fc n lhs ws wval ds)
451 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
452 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
453 n' = if n `elem` ns then dec n else n in
454 PWith fc n' (expandParams dec ps'' ns lhs)
455 (map (expandParams dec ps'' ns) ws)
456 (expandParams dec ps'' ns wval)
457 (map (expandParamsD ist dec ps'' ns) ds)
458 updateps yn nm [] = []
459 updateps yn nm (((a, t), i):as)
460 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
461 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
463expandParamsD ist dec ps ns d = d
465-- Calculate a priority for a type, for deciding elaboration order
466-- * if it's just a type variable or concrete type, do it early (0)
467-- * if there's only type variables and injective constructors, do it next (1)
468-- * if there's a function type, next (2)
469-- * finally, everything else (3)
471getPriority :: IState -> PTerm -> Int
472getPriority i tm = pri tm
473 where
474 pri (PRef _ n) =
475 case lookupP Nothing n (tt_ctxt i) of
476 ((P (DCon _ _) _ _):_) -> 1
477 ((P (TCon _ _) _ _):_) -> 1
478 ((P Ref _ _):_) -> 4
479 [] -> 0 -- must be locally bound, if it's not an error...
480 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
481 pri (PTrue _) = 0
482 pri (PFalse _) = 0
483 pri (PRefl _) = 1
484 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
485 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
486 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
487 pri (PTyped l r) = pri l
488 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
489 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
490 pri (PAlternative a as) = maximum (map pri as)
491 pri (PConstant _) = 0
492 pri Placeholder = 1
493 pri _ = 3
495addStatics :: Name -> Term -> PTerm -> Idris ()
496addStatics n tm ptm =
497 do let (statics, dynamics) = initStatics tm ptm
498 let stnames = nub $ concatMap freeNames (map snd statics)
499 let dnames = nub $ concatMap freeNames (map snd dynamics)
500 when (not (null statics)) $
501 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
502 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
503 let statics' = nub $ map fst statics ++
504 filter (\x -> not (elem x dnames)) stnames
505 let stpos = staticList statics' tm
506 i <- get
507 put (i { idris_statics = addDef n stpos (idris_statics i) })
508 addIBC (IBCStatic n)
509 where
510 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
511 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
512 if pstatic p == Static then ((n, ty) : static, dynamic)
513 else (static, (n, ty) : dynamic)
514 initStatics t pt = ([], [])
516 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
517 staticList _ _ = []
519-- Dealing with implicit arguments
521-- Add implicit Pi bindings for any names in the term which appear in an
522-- argument position.
524-- This has become a right mess already. Better redo it some time...
526implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
527implicit syn n ptm
528 = do i <- get
529 let (tm', impdata) = implicitise syn i ptm
530-- let (tm'', spos) = findStatics i tm'
531 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
532 addIBC (IBCImp n)
533 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
534-- i <- get
535-- put (i { idris_statics = addDef n spos (idris_statics i) })
536 return tm'
538implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
539implicitise syn ist tm
540 = let (declimps, ns') = execState (imps True [] tm) ([], [])
541 ns = ns' \\ (map fst pvars ++ no_imp syn) in
542 if null ns
543 then (tm, reverse declimps)
544 else implicitise syn ist (pibind uvars ns tm)
545 where
546 uvars = using syn
547 pvars = syn_params syn
549 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
550 | otherwise = x : dropAll xs ys
551 dropAll [] ys = []
553 imps top env (PApp _ f as)
554 = do (decls, ns) <- get
555 let isn = concatMap (namesIn uvars ist) (map getTm as)
556 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
557 imps top env (PPi (Imp l _) n ty sc)
558 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
559 (decls , ns) <- get
560 put (PImp (getPriority ist ty) l n ty : decls,
561 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
562 imps True (n:env) sc
563 imps top env (PPi (Exp l _) n ty sc)
564 = do let isn = nub (namesIn uvars ist ty ++ case sc of
565 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
566 _ -> [])
567 (decls, ns) <- get -- ignore decls in HO types
568 put (PExp (getPriority ist ty) l ty : decls,
569 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
570 imps True (n:env) sc
571 imps top env (PPi (Constraint l _) n ty sc)
572 = do let isn = nub (namesIn uvars ist ty ++ case sc of
573 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
574 _ -> [])
575 (decls, ns) <- get -- ignore decls in HO types
576 put (PConstraint 10 l ty : decls,
577 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
578 imps True (n:env) sc
579 imps top env (PPi (TacImp l _ scr) n ty sc)
580 = do let isn = nub (namesIn uvars ist ty ++ case sc of
581 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
582 _ -> [])
583 (decls, ns) <- get -- ignore decls in HO types
584 put (PTacImplicit 10 l n scr ty : decls,
585 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
586 imps True (n:env) sc
587 imps top env (PEq _ l r)
588 = do (decls, ns) <- get
589 let isn = namesIn uvars ist l ++ namesIn uvars ist r
590 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
591 imps top env (PTyped l r)
592 = imps top env l
593 imps top env (PPair _ l r)
594 = do (decls, ns) <- get
595 let isn = namesIn uvars ist l ++ namesIn uvars ist r
596 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
597 imps top env (PDPair _ (PRef _ n) t r)
598 = do (decls, ns) <- get
599 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
600 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
601 imps top env (PDPair _ l t r)
602 = do (decls, ns) <- get
603 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
604 namesIn uvars ist r
605 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
606 imps top env (PAlternative a as)
607 = do (decls, ns) <- get
608 let isn = concatMap (namesIn uvars ist) as
609 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
610 imps top env (PLam n ty sc)
611 = do imps False env ty
612 imps False (n:env) sc
613 imps top env (PHidden tm) = imps False env tm
614 imps top env _ = return ()
616 pibind using [] sc = sc
617 pibind using (n:ns) sc
618 = case lookup n using of
619 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
620 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
622-- Add implicit arguments in function calls
623addImplPat :: IState -> PTerm -> PTerm
624addImplPat = addImpl' True []
626addImplBound :: IState -> [Name] -> PTerm -> PTerm
627addImplBound ist ns = addImpl' False ns ist
629addImpl :: IState -> PTerm -> PTerm
630addImpl = addImpl' False []
632-- TODO: in patterns, don't add implicits to function names guarded by constructors
633-- and *not* inside a PHidden
635addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
636addImpl' inpat env ist ptm = ai env ptm
637 where
638 ai env (PRef fc f)
639 | not (f `elem` env) = handleErr $ aiFn inpat inpat ist fc f []
640 ai env (PHidden (PRef fc f))
641 | not (f `elem` env) = handleErr $ aiFn inpat False ist fc f []
642 ai env (PEq fc l r) = let l' = ai env l
643 r' = ai env r in
644 PEq fc l' r'
645 ai env (PTyped l r) = let l' = ai env l
646 r' = ai env r in
647 PTyped l' r'
648 ai env (PPair fc l r) = let l' = ai env l
649 r' = ai env r in
650 PPair fc l' r'
651 ai env (PDPair fc l t r) = let l' = ai env l
652 t' = ai env t
653 r' = ai env r in
654 PDPair fc l' t' r'
655 ai env (PAlternative a as) = let as' = map (ai env) as in
656 PAlternative a as'
657 ai env (PApp fc (PRef _ f) as)
658 | not (f `elem` env)
659 = let as' = map (fmap (ai env)) as in
660 handleErr $ aiFn inpat False ist fc f as'
661 ai env (PApp fc f as) = let f' = ai env f
662 as' = map (fmap (ai env)) as in
663 mkPApp fc 1 f' as'
664 ai env (PCase fc c os) = let c' = ai env c
665 os' = map (pmap (ai env)) os in
666 PCase fc c' os'
667 ai env (PLam n ty sc) = let ty' = ai env ty
668 sc' = ai (n:env) sc in
669 PLam n ty' sc'
670 ai env (PLet n ty val sc)
671 = let ty' = ai env ty
672 val' = ai env val
673 sc' = ai (n:env) sc in
674 PLet n ty' val' sc'
675 ai env (PPi p n ty sc) = let ty' = ai env ty
676 sc' = ai (n:env) sc in
677 PPi p n ty' sc'
678 ai env (PHidden tm) = PHidden (ai env tm)
679 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
680 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
681 ai env tm = tm
683 handleErr (Left err) = PElabError err
684 handleErr (Right x) = x
686-- if in a pattern, and there are no arguments, and there's no possible
687-- names with zero explicit arguments, don't add implicits.
689aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
690aiFn inpat True ist fc f []
691 = case lookupCtxt Nothing f (idris_implicits ist) of
692 [] -> Right $ PRef fc f
693 alts -> if (any (all imp) alts)
694 then aiFn inpat False ist fc f [] -- use it as a constructor
695 else Right $ PRef fc f
696 where imp (PExp _ _ _) = False
697 imp _ = True
698aiFn inpat expat ist fc f as
699 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
700aiFn inpat expat ist fc f as
701 -- This is where namespaces get resolved by adding PAlternative
702 = case lookupCtxtName Nothing f (idris_implicits ist) of
703 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
704 [] -> if f `elem` idris_metavars ist
705 then Right $ PApp fc (PRef fc f) as
706 else Right $ mkPApp fc (length as) (PRef fc f) as
707 alts -> Right $
708 PAlternative True $
709 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
710 (insertImpl ns as)) alts
711 where
712 insertImpl :: [PArg] -> [PArg] -> [PArg]
713 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
714 PExp p l tm : insertImpl ps given
715 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
716 PConstraint p l tm : insertImpl ps given
717 insertImpl (PConstraint p l ty : ps) given =
718 PConstraint p l (PResolveTC fc) : insertImpl ps given
719 insertImpl (PImp p l n ty : ps) given =
720 case find n given [] of
721 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
722 Nothing -> PImp p l n Placeholder : insertImpl ps given
723 insertImpl (PTacImplicit p l n sc ty : ps) given =
724 case find n given [] of
725 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
726 Nothing -> if inpat
727 then PTacImplicit p l n sc Placeholder : insertImpl ps given
728 else PTacImplicit p l n sc sc : insertImpl ps given
729 insertImpl expected [] = []
730 insertImpl _ given = given
732 find n [] acc = Nothing
733 find n (PImp _ _ n' t : gs) acc
734 | n == n' = Just (t, reverse acc ++ gs)
735 find n (PTacImplicit _ _ n' _ t : gs) acc
736 | n == n' = Just (t, reverse acc ++ gs)
737 find n (g : gs) acc = find n gs (g : acc)
739mkPApp fc a f [] = f
740mkPApp fc a f as = let rest = drop a as in
741 appRest fc (PApp fc f (take a as)) rest
742 where
743 appRest fc f [] = f
744 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
746-- Find 'static' argument positions
747-- (the declared ones, plus any names in argument position in the declared
748-- statics)
749-- FIXME: It's possible that this really has to happen after elaboration
751findStatics :: IState -> PTerm -> (PTerm, [Bool])
752findStatics ist tm = trace (showImp True tm) $
753 let (ns, ss) = fs tm in
754 runState (pos ns ss tm) []
755 where fs (PPi p n t sc)
756 | Static <- pstatic p
757 = let (ns, ss) = fs sc in
758 (namesIn [] ist t : ns, n : ss)
759 | otherwise = let (ns, ss) = fs sc in
760 (ns, ss)
761 fs _ = ([], [])
763 inOne n ns = length (filter id (map (elem n) ns)) == 1
765 pos ns ss (PPi p n t sc)
766 | elem n ss = do sc' <- pos ns ss sc
767 spos <- get
768 put (True : spos)
769 return (PPi (p { pstatic = Static }) n t sc')
770 | otherwise = do sc' <- pos ns ss sc
771 spos <- get
772 put (False : spos)
773 return (PPi p n t sc')
774 pos ns ss t = return t
776-- Debugging/logging stuff
778dumpDecls :: [PDecl] -> String
779dumpDecls [] = ""
780dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
782dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
783dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
784dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
785dumpDecl (PData _ _ d) = showDImp True d
786dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
787dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
788dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
789dumpDecl (PClass _ _ cs n ps ds)
790 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
791dumpDecl (PInstance _ _ cs n _ t _ ds)
792 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
793dumpDecl _ = "..."
794-- dumpDecl (PImport i) = "import " ++ i
796-- for 6.12/7 compatibility
797data EitherErr a b = LeftErr a | RightOK b
799instance Monad (EitherErr a) where
800 return = RightOK
802 (LeftErr e) >>= k = LeftErr e
803 RightOK v >>= k = k v
805toEither (LeftErr e) = Left e
806toEither (RightOK ho) = Right ho
808-- syntactic match of a against b, returning pair of variables in a
809-- and what they match. Returns the pair that failed if not a match.
811matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
812matchClause = matchClause' False
814matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
815matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
816 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
818 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
819 fullApp x = x
821 match' x y = match (fullApp x) (fullApp y)
822 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
823 | PConstant (I _) <- getTm x = match (getTm x) x'
824 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
825 | PConstant (I _) <- getTm x = match (getTm x) x'
826 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
827 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
828 match (PApp _ f args) (PApp _ f' args')
829 | length args == length args'
830 = do mf <- match' f f'
831 ms <- zipWithM matchArg args args'
832 return (mf ++ concat ms)
833-- match (PRef _ n) (PRef _ n') | n == n' = return []
834-- | otherwise = Nothing
835 match (PRef f n) (PApp _ x []) = match (PRef f n) x
836 match (PApp _ x []) (PRef f n) = match x (PRef f n)
837 match (PRef _ n) (PRef _ n') | n == n' = return []
838 match (PRef _ n) tm
839 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
840 = return [(n, tm)]
841 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
842 mr <- match' r r'
843 return (ml ++ mr)
844 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
845 mr <- match r r'
846 return (ml ++ mr)
847 match (PTyped l r) x = match l x
848 match x (PTyped l r) = match x l
849 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
850 mr <- match' r r'
851 return (ml ++ mr)
852 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
853 mt <- match' t t'
854 mr <- match' r r'
855 return (ml ++ mt ++ mr)
856 match (PAlternative a as) (PAlternative a' as')
857 = do ms <- zipWithM match' as as'
858 return (concat ms)
859 match a@(PAlternative _ as) b
860 = do let ms = zipWith match' as (repeat b)
861 case (rights (map toEither ms)) of
862 (x: _) -> return x
863 _ -> LeftErr (a, b)
864 match (PCase _ _ _) _ = return [] -- lifted out
865 match (PMetavar _) _ = return [] -- modified
866 match (PQuote _) _ = return []
867 match (PProof _) _ = return []
868 match (PTactics _) _ = return []
869 match (PRefl _) (PRefl _) = return []
870 match (PResolveTC _) (PResolveTC _) = return []
871 match (PTrue _) (PTrue _) = return []
872 match (PFalse _) (PFalse _) = return []
873 match (PReturn _) (PReturn _) = return []
874 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
875 ms <- match' s s'
876 return (mt ++ ms)
877 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
878 ms <- match' s s'
879 return (mt ++ ms)
880 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
881 mty <- match' ty ty'
882 ms <- match' s s'
883 return (mt ++ mty ++ ms)
884 match (PHidden x) (PHidden y) = match' x y
885 match Placeholder _ = return []
886-- match _ Placeholder = return []
887 match (PResolveTC _) _ = return []
888 match a b | a == b = return []
889 | otherwise = LeftErr (a, b)
891 checkRpts (RightOK ms) = check ms where
892 check ((n,t):xs)
893 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
894 then Left (t, t')
895 else check xs
896 check (_:xs) = check xs
897 check [] = Right ms
898 checkRpts (LeftErr x) = Left x
900substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
901substMatches [] t = t
902substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
904substMatch :: Name -> PTerm -> PTerm -> PTerm
905substMatch n tm t = sm t where
906 sm (PRef _ n') | n == n' = tm
907 sm (PLam x t sc) = PLam x (sm t) (sm sc)
908 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
909 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
910 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
911 sm (PEq f x y) = PEq f (sm x) (sm y)
912 sm (PTyped x y) = PTyped (sm x) (sm y)
913 sm (PPair f x y) = PPair f (sm x) (sm y)
914 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
915 sm (PAlternative a as) = PAlternative a (map sm as)
916 sm (PHidden x) = PHidden (sm x)
917 sm x = x
919shadow :: Name -> Name -> PTerm -> PTerm
920shadow n n' t = sm t where
921 sm (PRef fc x) | n == x = PRef fc n'
922 sm (PLam x t sc) = PLam x (sm t) (sm sc)
923 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
924 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
925 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
926 sm (PEq f x y) = PEq f (sm x) (sm y)
927 sm (PTyped x y) = PTyped (sm x) (sm y)
928 sm (PPair f x y) = PPair f (sm x) (sm y)
929 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
930 sm (PAlternative a as) = PAlternative a (map sm as)
931 sm (PHidden x) = PHidden (sm x)
932 sm x = x