git.iko.soy/Idris-dev
on 8063cfd help sign in
Idris-dev/src/Idris/AbsSyntax.hs
968 lines 39 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 = n : idris_totcheck i })
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.
80addInstance :: Bool -> Name -> Name -> Idris ()
81addInstance int n i
82 = do ist <- get
83 case lookupCtxt Nothing n (idris_classes ist) of
84 [CI a b c d ins] ->
85 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
86 put (ist { idris_classes = cs })
87 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
88 put (ist { idris_classes = cs })
89 where addI i ins | int = i : ins
90 | otherwise = ins ++ [i]
92addClass :: Name -> ClassInfo -> Idris ()
93addClass n i
94 = do ist <- get
95 let i' = case lookupCtxt Nothing n (idris_classes ist) of
96 [c] -> c { class_instances = class_instances i }
97 _ -> i
98 put (ist { idris_classes = addDef n i' (idris_classes ist) })
100addIBC :: IBCWrite -> Idris ()
101addIBC ibc@(IBCDef n)
102 = do i <- get
103 when (notDef (ibc_write i)) $
104 put (i { ibc_write = ibc : ibc_write i })
105 where notDef [] = True
106 notDef (IBCDef n': is) | n == n' = False
107 notDef (_ : is) = notDef is
108addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
110clearIBC :: Idris ()
111clearIBC = do i <- get; put (i { ibc_write = [] })
113getHdrs :: Idris [String]
114getHdrs = do i <- get; return (idris_hdrs i)
116setErrLine :: Int -> Idris ()
117setErrLine x = do i <- get;
118 case (errLine i) of
119 Nothing -> put (i { errLine = Just x })
120 Just _ -> return ()
122clearErr :: Idris ()
123clearErr = do i <- get
124 put (i { errLine = Nothing })
126getSO :: Idris (Maybe String)
127getSO = do i <- get
128 return (compiled_so i)
130setSO :: Maybe String -> Idris ()
131setSO s = do i <- get
132 put (i { compiled_so = s })
134getIState :: Idris IState
135getIState = get
137putIState :: IState -> Idris ()
138putIState = put
140getName :: Idris Int
141getName = do i <- get;
142 let idx = idris_name i;
143 put (i { idris_name = idx + 1 })
144 return idx
146checkUndefined :: FC -> Name -> Idris ()
147checkUndefined fc n
148 = do i <- getContext
149 case lookupTy Nothing n i of
150 (_:_) -> fail $ show fc ++ ":" ++
151 show n ++ " already defined"
152 _ -> return ()
154setContext :: Context -> Idris ()
155setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
157updateContext :: (Context -> Context) -> Idris ()
158updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
160addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
161addConstraints fc (v, cs)
162 = do i <- get
163 let ctxt = tt_ctxt i
164 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
165 next_tvar = v }
166 let ics = zip cs (repeat fc) ++ idris_constraints i
167 put (i { tt_ctxt = ctxt', idris_constraints = ics })
169addDeferred :: [(Name, Type)] -> Idris ()
170addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
171 i <- get
172 put (i { idris_metavars = map fst ns ++ idris_metavars i })
173 where tidyNames used (Bind (MN i x) b sc)
174 = let n' = uniqueName (UN x) used in
175 Bind n' b $ tidyNames (n':used) sc
176 tidyNames used (Bind n b sc)
177 = let n' = uniqueName n used in
178 Bind n' b $ tidyNames (n':used) sc
179 tidyNames used b = b
181solveDeferred :: Name -> Idris ()
182solveDeferred n = do i <- get
183 put (i { idris_metavars = idris_metavars i \\ [n] })
185iputStrLn :: String -> Idris ()
186iputStrLn = liftIO . putStrLn
188iWarn :: FC -> String -> Idris ()
189iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
191setLogLevel :: Int -> Idris ()
192setLogLevel l = do i <- get
193 let opts = idris_options i
194 let opt' = opts { opt_logLevel = l }
195 put (i { idris_options = opt' } )
197setCmdLine :: [Opt] -> Idris ()
198setCmdLine opts = do i <- get
199 let iopts = idris_options i
200 put (i { idris_options = iopts { opt_cmdline = opts } })
202getDumpC :: Idris (Maybe FilePath)
203getDumpC = do i <- get
204 return $ findC (opt_cmdline (idris_options i))
205 where findC [] = Nothing
206 findC (DumpC x : _) = Just x
207 findC (_ : xs) = findC xs
209getDumpCases :: Idris (Maybe FilePath)
210getDumpCases = do i <- get
211 return $ findC (opt_cmdline (idris_options i))
212 where findC [] = Nothing
213 findC (DumpCases x : _) = Just x
214 findC (_ : xs) = findC xs
216logLevel :: Idris Int
217logLevel = do i <- get
218 return (opt_logLevel (idris_options i))
220setErrContext :: Bool -> Idris ()
221setErrContext t = do i <- get
222 let opts = idris_options i
223 let opt' = opts { opt_errContext = t }
224 put (i { idris_options = opt' })
226errContext :: Idris Bool
227errContext = do i <- get
228 return (opt_errContext (idris_options i))
230useREPL :: Idris Bool
231useREPL = do i <- get
232 return (opt_repl (idris_options i))
234setREPL :: Bool -> Idris ()
235setREPL t = do i <- get
236 let opts = idris_options i
237 let opt' = opts { opt_repl = t }
238 put (i { idris_options = opt' })
240verbose :: Idris Bool
241verbose = do i <- get
242 return (opt_verbose (idris_options i))
244setVerbose :: Bool -> Idris ()
245setVerbose t = do i <- get
246 let opts = idris_options i
247 let opt' = opts { opt_verbose = t }
248 put (i { idris_options = opt' })
250typeInType :: Idris Bool
251typeInType = do i <- get
252 return (opt_typeintype (idris_options i))
254setTypeInType :: Bool -> Idris ()
255setTypeInType t = do i <- get
256 let opts = idris_options i
257 let opt' = opts { opt_typeintype = t }
258 put (i { idris_options = opt' })
260coverage :: Idris Bool
261coverage = do i <- get
262 return (opt_coverage (idris_options i))
264setCoverage :: Bool -> Idris ()
265setCoverage t = do i <- get
266 let opts = idris_options i
267 let opt' = opts { opt_coverage = t }
268 put (i { idris_options = opt' })
270setIBCSubDir :: FilePath -> Idris ()
271setIBCSubDir fp = do i <- get
272 let opts = idris_options i
273 let opt' = opts { opt_ibcsubdir = fp }
274 put (i { idris_options = opt' })
276valIBCSubDir :: IState -> Idris FilePath
277valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
279addImportDir :: FilePath -> Idris ()
280addImportDir fp = do i <- get
281 let opts = idris_options i
282 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
283 put (i { idris_options = opt' })
285setImportDirs :: [FilePath] -> Idris ()
286setImportDirs fps = do i <- get
287 let opts = idris_options i
288 let opt' = opts { opt_importdirs = fps }
289 put (i { idris_options = opt' })
291allImportDirs :: IState -> Idris [FilePath]
292allImportDirs i = do let optdirs = opt_importdirs (idris_options i)
293 return ("." : optdirs)
295impShow :: Idris Bool
296impShow = do i <- get
297 return (opt_showimp (idris_options i))
299setImpShow :: Bool -> Idris ()
300setImpShow t = do i <- get
301 let opts = idris_options i
302 let opt' = opts { opt_showimp = t }
303 put (i { idris_options = opt' })
305logLvl :: Int -> String -> Idris ()
306logLvl l str = do i <- get
307 let lvl = opt_logLevel (idris_options i)
308 when (lvl >= l)
309 $ do liftIO (putStrLn str)
310 put (i { idris_log = idris_log i ++ str ++ "\n" } )
312iLOG :: String -> Idris ()
313iLOG = logLvl 1
315noErrors :: Idris Bool
316noErrors = do i <- get
317 case errLine i of
318 Nothing -> return True
319 _ -> return False
321setTypeCase :: Bool -> Idris ()
322setTypeCase t = do i <- get
323 let opts = idris_options i
324 let opt' = opts { opt_typecase = t }
325 put (i { idris_options = opt' })
328-- For inferring types of things
330bi = FC "builtin" 0
332inferTy = MN 0 "__Infer"
333inferCon = MN 0 "__infer"
334inferDecl = PDatadecl inferTy
335 PSet
336 [(inferCon, PPi impl (MN 0 "A") PSet (
337 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
338 (PRef bi inferTy)), bi)]
340infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
341infP = P (TCon 6 0) inferTy (Set (UVal 0))
343getInferTerm, getInferType :: Term -> Term
344getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
345getInferTerm (App (App _ _) tm) = tm
346getInferTerm tm = error ("getInferTerm " ++ show tm)
348getInferType (Bind n b sc) = Bind n b $ getInferType sc
349getInferType (App (App _ ty) _) = ty
351-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
353primNames = [unitTy, unitCon,
354 falseTy, pairTy, pairCon,
355 eqTy, eqCon, inferTy, inferCon]
357unitTy = MN 0 "__Unit"
358unitCon = MN 0 "__II"
359unitDecl = PDatadecl unitTy PSet
360 [(unitCon, PRef bi unitTy, bi)]
362falseTy = MN 0 "__False"
363falseDecl = PDatadecl falseTy PSet []
365pairTy = MN 0 "__Pair"
366pairCon = MN 0 "__MkPair"
367pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
368 [(pairCon, PPi impl (n "A") PSet (
369 PPi impl (n "B") PSet (
370 PPi expl (n "a") (PRef bi (n "A")) (
371 PPi expl (n "b") (PRef bi (n "B"))
372 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
373 pexp (PRef bi (n "B"))])))), bi)]
374 where n a = MN 0 a
376eqTy = UN "="
377eqCon = UN "refl"
378eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
379 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
380 PSet)
381 [(eqCon, PPi impl (n "a") PSet (
382 PPi impl (n "x") (PRef bi (n "a"))
383 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
384 pimp (n "b") Placeholder,
385 pexp (PRef bi (n "x")),
386 pexp (PRef bi (n "x"))])), bi)]
387 where n a = MN 0 a
389-- Defined in builtins.idr
390sigmaTy = UN "Exists"
391existsCon = UN "Ex_intro"
393piBind :: [(Name, PTerm)] -> PTerm -> PTerm
394piBind [] t = t
395piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
397tcname (UN ('@':_)) = True
398tcname (NS n _) = tcname n
399tcname _ = False
401-- Dealing with parameters
403expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
404expandParams dec ps ns tm = en tm
405 where
406 -- if we shadow a name (say in a lambda binding) that is used in a call to
407 -- a lifted function, we need access to both names - once in the scope of the
408 -- binding and once to call the lifted functions. So we'll explicitly shadow
409 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
410 -- but we didn't...)
412 mkShadow (UN n) = MN 0 n
413 mkShadow (MN i n) = MN (i+1) n
414 mkShadow (NS x s) = NS (mkShadow x) s
416 en (PLam n t s)
417 | n `elem` map fst ps
418 = let n' = mkShadow n in
419 PLam n' (en t) (en (shadow n n' s))
420 | otherwise = PLam n (en t) (en s)
421 en (PPi p n t s)
422 | n `elem` map fst ps
423 = let n' = mkShadow n in
424 PPi p n' (en t) (en (shadow n n' s))
425 | otherwise = PPi p n (en t) (en s)
426 en (PLet n ty v s)
427 | n `elem` map fst ps
428 = let n' = mkShadow n in
429 PLet n' (en ty) (en v) (en (shadow n n' s))
430 | otherwise = PLet n (en ty) (en v) (en s)
431 en (PEq f l r) = PEq f (en l) (en r)
432 en (PTyped l r) = PTyped (en l) (en r)
433 en (PPair f l r) = PPair f (en l) (en r)
434 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
435 en (PAlternative a as) = PAlternative a (map en as)
436 en (PHidden t) = PHidden (en t)
437 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
438 en (PProof ts) = PProof (map (fmap en) ts)
439 en (PTactics ts) = PTactics (map (fmap en) ts)
441 en (PQuote (Var n))
442 | n `elem` ns = PQuote (Var (dec n))
443 en (PApp fc (PRef fc' n) as)
444 | n `elem` ns = PApp fc (PRef fc' (dec n))
445 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
446 en (PRef fc n)
447 | n `elem` ns = PApp fc (PRef fc (dec n))
448 (map (pexp . (PRef fc)) (map fst ps))
449 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
450 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
451 en t = t
453expandParamsD :: IState ->
454 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
455expandParamsD ist dec ps ns (PTy syn fc o n ty)
456 = if n `elem` ns
457 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
458 else PTy syn fc o n (expandParams dec ps ns ty)
459expandParamsD ist dec ps ns (PClauses fc opts n cs)
460 = let n' = if n `elem` ns then dec n else n in
461 PClauses fc opts n' (map expandParamsC cs)
462 where
463 expandParamsC (PClause fc n lhs ws rhs ds)
464 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
465 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
466 n' = if n `elem` ns then dec n else n in
467 PClause fc n' (expandParams dec ps'' ns lhs)
468 (map (expandParams dec ps'' ns) ws)
469 (expandParams dec ps'' ns rhs)
470 (map (expandParamsD ist dec ps'' ns) ds)
471 expandParamsC (PWith fc n lhs ws wval ds)
472 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
473 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
474 n' = if n `elem` ns then dec n else n in
475 PWith fc n' (expandParams dec ps'' ns lhs)
476 (map (expandParams dec ps'' ns) ws)
477 (expandParams dec ps'' ns wval)
478 (map (expandParamsD ist dec ps'' ns) ds)
479 updateps yn nm [] = []
480 updateps yn nm (((a, t), i):as)
481 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
482 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
484expandParamsD ist dec ps ns d = d
486-- Calculate a priority for a type, for deciding elaboration order
487-- * if it's just a type variable or concrete type, do it early (0)
488-- * if there's only type variables and injective constructors, do it next (1)
489-- * if there's a function type, next (2)
490-- * finally, everything else (3)
492getPriority :: IState -> PTerm -> Int
493getPriority i tm = pri tm
494 where
495 pri (PRef _ n) =
496 case lookupP Nothing n (tt_ctxt i) of
497 ((P (DCon _ _) _ _):_) -> 1
498 ((P (TCon _ _) _ _):_) -> 1
499 ((P Ref _ _):_) -> 4
500 [] -> 0 -- must be locally bound, if it's not an error...
501 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
502 pri (PTrue _) = 0
503 pri (PFalse _) = 0
504 pri (PRefl _) = 1
505 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
506 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
507 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
508 pri (PTyped l r) = pri l
509 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
510 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
511 pri (PAlternative a as) = maximum (map pri as)
512 pri (PConstant _) = 0
513 pri Placeholder = 1
514 pri _ = 3
516addStatics :: Name -> Term -> PTerm -> Idris ()
517addStatics n tm ptm =
518 do let (statics, dynamics) = initStatics tm ptm
519 let stnames = nub $ concatMap freeNames (map snd statics)
520 let dnames = nub $ concatMap freeNames (map snd dynamics)
521 when (not (null statics)) $
522 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
523 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
524 let statics' = nub $ map fst statics ++
525 filter (\x -> not (elem x dnames)) stnames
526 let stpos = staticList statics' tm
527 i <- get
528 put (i { idris_statics = addDef n stpos (idris_statics i) })
529 addIBC (IBCStatic n)
530 where
531 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
532 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
533 if pstatic p == Static then ((n, ty) : static, dynamic)
534 else (static, (n, ty) : dynamic)
535 initStatics t pt = ([], [])
537 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
538 staticList _ _ = []
540-- Dealing with implicit arguments
542-- Add implicit Pi bindings for any names in the term which appear in an
543-- argument position.
545-- This has become a right mess already. Better redo it some time...
547implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
548implicit syn n ptm = implicit' syn [] n ptm
550implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
551implicit' syn ignore n ptm
552 = do i <- get
553 let (tm', impdata) = implicitise syn ignore i ptm
554-- let (tm'', spos) = findStatics i tm'
555 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
556 addIBC (IBCImp n)
557 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
558-- i <- get
559-- put (i { idris_statics = addDef n spos (idris_statics i) })
560 return tm'
562implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
563implicitise syn ignore ist tm
564 = let (declimps, ns') = execState (imps True [] tm) ([], [])
565 ns = ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
566 if null ns
567 then (tm, reverse declimps)
568 else implicitise syn ignore ist (pibind uvars ns tm)
569 where
570 uvars = using syn
571 pvars = syn_params syn
573 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
574 | otherwise = x : dropAll xs ys
575 dropAll [] ys = []
577 imps top env (PApp _ f as)
578 = do (decls, ns) <- get
579 let isn = concatMap (namesIn uvars ist) (map getTm as)
580 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
581 imps top env (PPi (Imp l _) n ty sc)
582 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
583 (decls , ns) <- get
584 put (PImp (getPriority ist ty) l n ty : decls,
585 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
586 imps True (n:env) sc
587 imps top env (PPi (Exp l _) n ty sc)
588 = do let isn = nub (namesIn uvars ist ty ++ case sc of
589 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
590 _ -> [])
591 (decls, ns) <- get -- ignore decls in HO types
592 put (PExp (getPriority ist ty) l ty : decls,
593 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
594 imps True (n:env) sc
595 imps top env (PPi (Constraint l _) n ty sc)
596 = do let isn = nub (namesIn uvars ist ty ++ case sc of
597 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
598 _ -> [])
599 (decls, ns) <- get -- ignore decls in HO types
600 put (PConstraint 10 l ty : decls,
601 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
602 imps True (n:env) sc
603 imps top env (PPi (TacImp l _ scr) n ty sc)
604 = do let isn = nub (namesIn uvars ist ty ++ case sc of
605 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
606 _ -> [])
607 (decls, ns) <- get -- ignore decls in HO types
608 put (PTacImplicit 10 l n scr ty : decls,
609 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
610 imps True (n:env) sc
611 imps top env (PEq _ l r)
612 = do (decls, ns) <- get
613 let isn = namesIn uvars ist l ++ namesIn uvars ist r
614 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
615 imps top env (PTyped l r)
616 = imps top env l
617 imps top env (PPair _ l r)
618 = do (decls, ns) <- get
619 let isn = namesIn uvars ist l ++ namesIn uvars ist r
620 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
621 imps top env (PDPair _ (PRef _ n) t r)
622 = do (decls, ns) <- get
623 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
624 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
625 imps top env (PDPair _ l t r)
626 = do (decls, ns) <- get
627 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
628 namesIn uvars ist r
629 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
630 imps top env (PAlternative a as)
631 = do (decls, ns) <- get
632 let isn = concatMap (namesIn uvars ist) as
633 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
634 imps top env (PLam n ty sc)
635 = do imps False env ty
636 imps False (n:env) sc
637 imps top env (PHidden tm) = imps False env tm
638 imps top env _ = return ()
640 pibind using [] sc = sc
641 pibind using (n:ns) sc
642 = case lookup n using of
643 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
644 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
646-- Add implicit arguments in function calls
647addImplPat :: IState -> PTerm -> PTerm
648addImplPat = addImpl' True []
650addImplBound :: IState -> [Name] -> PTerm -> PTerm
651addImplBound ist ns = addImpl' False ns ist
653addImpl :: IState -> PTerm -> PTerm
654addImpl = addImpl' False []
656-- TODO: in patterns, don't add implicits to function names guarded by constructors
657-- and *not* inside a PHidden
659addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
660addImpl' inpat env ist ptm = ai env ptm
661 where
662 ai env (PRef fc f)
663 | not (f `elem` env) = handleErr $ aiFn inpat inpat ist fc f []
664 ai env (PHidden (PRef fc f))
665 | not (f `elem` env) = handleErr $ aiFn inpat False ist fc f []
666 ai env (PEq fc l r) = let l' = ai env l
667 r' = ai env r in
668 PEq fc l' r'
669 ai env (PTyped l r) = let l' = ai env l
670 r' = ai env r in
671 PTyped l' r'
672 ai env (PPair fc l r) = let l' = ai env l
673 r' = ai env r in
674 PPair fc l' r'
675 ai env (PDPair fc l t r) = let l' = ai env l
676 t' = ai env t
677 r' = ai env r in
678 PDPair fc l' t' r'
679 ai env (PAlternative a as) = let as' = map (ai env) as in
680 PAlternative a as'
681 ai env (PApp fc (PRef _ f) as)
682 | not (f `elem` env)
683 = let as' = map (fmap (ai env)) as in
684 handleErr $ aiFn inpat False ist fc f as'
685 ai env (PApp fc f as) = let f' = ai env f
686 as' = map (fmap (ai env)) as in
687 mkPApp fc 1 f' as'
688 ai env (PCase fc c os) = let c' = ai env c
689 os' = map (pmap (ai env)) os in
690 PCase fc c' os'
691 ai env (PLam n ty sc) = let ty' = ai env ty
692 sc' = ai (n:env) sc in
693 PLam n ty' sc'
694 ai env (PLet n ty val sc)
695 = let ty' = ai env ty
696 val' = ai env val
697 sc' = ai (n:env) sc in
698 PLet n ty' val' sc'
699 ai env (PPi p n ty sc) = let ty' = ai env ty
700 sc' = ai (n:env) sc in
701 PPi p n ty' sc'
702 ai env (PHidden tm) = PHidden (ai env tm)
703 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
704 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
705 ai env tm = tm
707 handleErr (Left err) = PElabError err
708 handleErr (Right x) = x
710-- if in a pattern, and there are no arguments, and there's no possible
711-- names with zero explicit arguments, don't add implicits.
713aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
714aiFn inpat True ist fc f []
715 = case lookupDef Nothing f (tt_ctxt ist) of
716 [] -> Right $ PPatvar fc f
717 alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
718 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
719 if (not (vname f) || tcname f
720 || any constructor alts || any allImp ialts)
721 then aiFn inpat False ist fc f [] -- use it as a constructor
722 else Right $ PPatvar fc f
723 where imp (PExp _ _ _) = False
724 imp _ = True
725 allImp [] = False
726 allImp xs = all imp xs
727 constructor (TyDecl (DCon _ _) _) = True
728 constructor _ = False
730 vname (UN n) = True -- non qualified
731 vname _ = False
733aiFn inpat expat ist fc f as
734 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
735aiFn inpat expat ist fc f as
736 -- This is where namespaces get resolved by adding PAlternative
737 = case lookupCtxtName Nothing f (idris_implicits ist) of
738 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
739 [] -> if f `elem` idris_metavars ist
740 then Right $ PApp fc (PRef fc f) as
741 else Right $ mkPApp fc (length as) (PRef fc f) as
742 alts -> Right $
743 PAlternative True $
744 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
745 (insertImpl ns as)) alts
746 where
747 insertImpl :: [PArg] -> [PArg] -> [PArg]
748 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
749 PExp p l tm : insertImpl ps given
750 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
751 PConstraint p l tm : insertImpl ps given
752 insertImpl (PConstraint p l ty : ps) given =
753 PConstraint p l (PResolveTC fc) : insertImpl ps given
754 insertImpl (PImp p l n ty : ps) given =
755 case find n given [] of
756 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
757 Nothing -> PImp p l n Placeholder : insertImpl ps given
758 insertImpl (PTacImplicit p l n sc ty : ps) given =
759 case find n given [] of
760 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
761 Nothing -> if inpat
762 then PTacImplicit p l n sc Placeholder : insertImpl ps given
763 else PTacImplicit p l n sc sc : insertImpl ps given
764 insertImpl expected [] = []
765 insertImpl _ given = given
767 find n [] acc = Nothing
768 find n (PImp _ _ n' t : gs) acc
769 | n == n' = Just (t, reverse acc ++ gs)
770 find n (PTacImplicit _ _ n' _ t : gs) acc
771 | n == n' = Just (t, reverse acc ++ gs)
772 find n (g : gs) acc = find n gs (g : acc)
774mkPApp fc a f [] = f
775mkPApp fc a f as = let rest = drop a as in
776 appRest fc (PApp fc f (take a as)) rest
777 where
778 appRest fc f [] = f
779 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
781-- Find 'static' argument positions
782-- (the declared ones, plus any names in argument position in the declared
783-- statics)
784-- FIXME: It's possible that this really has to happen after elaboration
786findStatics :: IState -> PTerm -> (PTerm, [Bool])
787findStatics ist tm = trace (showImp True tm) $
788 let (ns, ss) = fs tm in
789 runState (pos ns ss tm) []
790 where fs (PPi p n t sc)
791 | Static <- pstatic p
792 = let (ns, ss) = fs sc in
793 (namesIn [] ist t : ns, n : ss)
794 | otherwise = let (ns, ss) = fs sc in
795 (ns, ss)
796 fs _ = ([], [])
798 inOne n ns = length (filter id (map (elem n) ns)) == 1
800 pos ns ss (PPi p n t sc)
801 | elem n ss = do sc' <- pos ns ss sc
802 spos <- get
803 put (True : spos)
804 return (PPi (p { pstatic = Static }) n t sc')
805 | otherwise = do sc' <- pos ns ss sc
806 spos <- get
807 put (False : spos)
808 return (PPi p n t sc')
809 pos ns ss t = return t
811-- Debugging/logging stuff
813dumpDecls :: [PDecl] -> String
814dumpDecls [] = ""
815dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
817dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
818dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
819dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
820dumpDecl (PData _ _ d) = showDImp True d
821dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
822dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
823dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
824dumpDecl (PClass _ _ cs n ps ds)
825 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
826dumpDecl (PInstance _ _ cs n _ t _ ds)
827 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
828dumpDecl _ = "..."
829-- dumpDecl (PImport i) = "import " ++ i
831-- for 6.12/7 compatibility
832data EitherErr a b = LeftErr a | RightOK b
834instance Monad (EitherErr a) where
835 return = RightOK
837 (LeftErr e) >>= k = LeftErr e
838 RightOK v >>= k = k v
840toEither (LeftErr e) = Left e
841toEither (RightOK ho) = Right ho
843-- syntactic match of a against b, returning pair of variables in a
844-- and what they match. Returns the pair that failed if not a match.
846matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
847matchClause = matchClause' False
849matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
850matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
851 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
853 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
854 fullApp x = x
856 match' x y = match (fullApp x) (fullApp y)
857 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
858 | PConstant (I _) <- getTm x = match (getTm x) x'
859 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
860 | PConstant (I _) <- getTm x = match (getTm x) x'
861 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
862 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
863 match (PApp _ f args) (PApp _ f' args')
864 | length args == length args'
865 = do mf <- match' f f'
866 ms <- zipWithM matchArg args args'
867 return (mf ++ concat ms)
868-- match (PRef _ n) (PRef _ n') | n == n' = return []
869-- | otherwise = Nothing
870 match (PRef f n) (PApp _ x []) = match (PRef f n) x
871 match (PApp _ x []) (PRef f n) = match x (PRef f n)
872 match (PRef _ n) (PRef _ n') | n == n' = return []
873 match (PRef _ n) tm
874 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
875 = return [(n, tm)]
876 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
877 mr <- match' r r'
878 return (ml ++ mr)
879 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
880 mr <- match r r'
881 return (ml ++ mr)
882 match (PTyped l r) x = match l x
883 match x (PTyped l r) = match x l
884 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
885 mr <- match' r r'
886 return (ml ++ mr)
887 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
888 mt <- match' t t'
889 mr <- match' r r'
890 return (ml ++ mt ++ mr)
891 match (PAlternative a as) (PAlternative a' as')
892 = do ms <- zipWithM match' as as'
893 return (concat ms)
894 match a@(PAlternative _ as) b
895 = do let ms = zipWith match' as (repeat b)
896 case (rights (map toEither ms)) of
897 (x: _) -> return x
898 _ -> LeftErr (a, b)
899 match (PCase _ _ _) _ = return [] -- lifted out
900 match (PMetavar _) _ = return [] -- modified
901 match (PQuote _) _ = return []
902 match (PProof _) _ = return []
903 match (PTactics _) _ = return []
904 match (PRefl _) (PRefl _) = return []
905 match (PResolveTC _) (PResolveTC _) = return []
906 match (PTrue _) (PTrue _) = return []
907 match (PFalse _) (PFalse _) = return []
908 match (PReturn _) (PReturn _) = return []
909 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
910 ms <- match' s s'
911 return (mt ++ ms)
912 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
913 ms <- match' s s'
914 return (mt ++ ms)
915 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
916 mty <- match' ty ty'
917 ms <- match' s s'
918 return (mt ++ mty ++ ms)
919 match (PHidden x) (PHidden y) = match' x y
920 match Placeholder _ = return []
921 match _ Placeholder = return []
922 match (PResolveTC _) _ = return []
923 match a b | a == b = return []
924 | otherwise = LeftErr (a, b)
926 checkRpts (RightOK ms) = check ms where
927 check ((n,t):xs)
928 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
929 then Left (t, t')
930 else check xs
931 check (_:xs) = check xs
932 check [] = Right ms
933 checkRpts (LeftErr x) = Left x
935substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
936substMatches [] t = t
937substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
939substMatch :: Name -> PTerm -> PTerm -> PTerm
940substMatch n tm t = sm t where
941 sm (PRef _ n') | n == n' = tm
942 sm (PLam x t sc) = PLam x (sm t) (sm sc)
943 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
944 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
945 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
946 sm (PEq f x y) = PEq f (sm x) (sm y)
947 sm (PTyped x y) = PTyped (sm x) (sm y)
948 sm (PPair f x y) = PPair f (sm x) (sm y)
949 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
950 sm (PAlternative a as) = PAlternative a (map sm as)
951 sm (PHidden x) = PHidden (sm x)
952 sm x = x
954shadow :: Name -> Name -> PTerm -> PTerm
955shadow n n' t = sm t where
956 sm (PRef fc x) | n == x = PRef fc n'
957 sm (PLam x t sc) = PLam x (sm t) (sm sc)
958 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
959 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
960 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
961 sm (PEq f x y) = PEq f (sm x) (sm y)
962 sm (PTyped x y) = PTyped (sm x) (sm y)
963 sm (PPair f x y) = PPair f (sm x) (sm y)
964 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
965 sm (PAlternative a as) = PAlternative a (map sm as)
966 sm (PHidden x) = PHidden (sm x)
967 sm x = x