git.iko.soy/Idris-dev
on 11dd660 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
975 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
209getDumpDefun :: Idris (Maybe FilePath)
210getDumpDefun = do i <- get
211 return $ findC (opt_cmdline (idris_options i))
212 where findC [] = Nothing
213 findC (DumpDefun x : _) = Just x
214 findC (_ : xs) = findC xs
216getDumpCases :: Idris (Maybe FilePath)
217getDumpCases = do i <- get
218 return $ findC (opt_cmdline (idris_options i))
219 where findC [] = Nothing
220 findC (DumpCases x : _) = Just x
221 findC (_ : xs) = findC xs
223logLevel :: Idris Int
224logLevel = do i <- get
225 return (opt_logLevel (idris_options i))
227setErrContext :: Bool -> Idris ()
228setErrContext t = do i <- get
229 let opts = idris_options i
230 let opt' = opts { opt_errContext = t }
231 put (i { idris_options = opt' })
233errContext :: Idris Bool
234errContext = do i <- get
235 return (opt_errContext (idris_options i))
237useREPL :: Idris Bool
238useREPL = do i <- get
239 return (opt_repl (idris_options i))
241setREPL :: Bool -> Idris ()
242setREPL t = do i <- get
243 let opts = idris_options i
244 let opt' = opts { opt_repl = t }
245 put (i { idris_options = opt' })
247verbose :: Idris Bool
248verbose = do i <- get
249 return (opt_verbose (idris_options i))
251setVerbose :: Bool -> Idris ()
252setVerbose t = do i <- get
253 let opts = idris_options i
254 let opt' = opts { opt_verbose = t }
255 put (i { idris_options = opt' })
257typeInType :: Idris Bool
258typeInType = do i <- get
259 return (opt_typeintype (idris_options i))
261setTypeInType :: Bool -> Idris ()
262setTypeInType t = do i <- get
263 let opts = idris_options i
264 let opt' = opts { opt_typeintype = t }
265 put (i { idris_options = opt' })
267coverage :: Idris Bool
268coverage = do i <- get
269 return (opt_coverage (idris_options i))
271setCoverage :: Bool -> Idris ()
272setCoverage t = do i <- get
273 let opts = idris_options i
274 let opt' = opts { opt_coverage = t }
275 put (i { idris_options = opt' })
277setIBCSubDir :: FilePath -> Idris ()
278setIBCSubDir fp = do i <- get
279 let opts = idris_options i
280 let opt' = opts { opt_ibcsubdir = fp }
281 put (i { idris_options = opt' })
283valIBCSubDir :: IState -> Idris FilePath
284valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
286addImportDir :: FilePath -> Idris ()
287addImportDir fp = do i <- get
288 let opts = idris_options i
289 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
290 put (i { idris_options = opt' })
292setImportDirs :: [FilePath] -> Idris ()
293setImportDirs fps = do i <- get
294 let opts = idris_options i
295 let opt' = opts { opt_importdirs = fps }
296 put (i { idris_options = opt' })
298allImportDirs :: IState -> Idris [FilePath]
299allImportDirs i = do let optdirs = opt_importdirs (idris_options i)
300 return ("." : optdirs)
302impShow :: Idris Bool
303impShow = do i <- get
304 return (opt_showimp (idris_options i))
306setImpShow :: Bool -> Idris ()
307setImpShow t = do i <- get
308 let opts = idris_options i
309 let opt' = opts { opt_showimp = t }
310 put (i { idris_options = opt' })
312logLvl :: Int -> String -> Idris ()
313logLvl l str = do i <- get
314 let lvl = opt_logLevel (idris_options i)
315 when (lvl >= l)
316 $ do liftIO (putStrLn str)
317 put (i { idris_log = idris_log i ++ str ++ "\n" } )
319iLOG :: String -> Idris ()
320iLOG = logLvl 1
322noErrors :: Idris Bool
323noErrors = do i <- get
324 case errLine i of
325 Nothing -> return True
326 _ -> return False
328setTypeCase :: Bool -> Idris ()
329setTypeCase t = do i <- get
330 let opts = idris_options i
331 let opt' = opts { opt_typecase = t }
332 put (i { idris_options = opt' })
335-- For inferring types of things
337bi = FC "builtin" 0
339inferTy = MN 0 "__Infer"
340inferCon = MN 0 "__infer"
341inferDecl = PDatadecl inferTy
342 PSet
343 [(inferCon, PPi impl (MN 0 "A") PSet (
344 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
345 (PRef bi inferTy)), bi)]
347infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
348infP = P (TCon 6 0) inferTy (Set (UVal 0))
350getInferTerm, getInferType :: Term -> Term
351getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
352getInferTerm (App (App _ _) tm) = tm
353getInferTerm tm = error ("getInferTerm " ++ show tm)
355getInferType (Bind n b sc) = Bind n b $ getInferType sc
356getInferType (App (App _ ty) _) = ty
358-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
360primNames = [unitTy, unitCon,
361 falseTy, pairTy, pairCon,
362 eqTy, eqCon, inferTy, inferCon]
364unitTy = MN 0 "__Unit"
365unitCon = MN 0 "__II"
366unitDecl = PDatadecl unitTy PSet
367 [(unitCon, PRef bi unitTy, bi)]
369falseTy = MN 0 "__False"
370falseDecl = PDatadecl falseTy PSet []
372pairTy = MN 0 "__Pair"
373pairCon = MN 0 "__MkPair"
374pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
375 [(pairCon, PPi impl (n "A") PSet (
376 PPi impl (n "B") PSet (
377 PPi expl (n "a") (PRef bi (n "A")) (
378 PPi expl (n "b") (PRef bi (n "B"))
379 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
380 pexp (PRef bi (n "B"))])))), bi)]
381 where n a = MN 0 a
383eqTy = UN "="
384eqCon = UN "refl"
385eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
386 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
387 PSet)
388 [(eqCon, PPi impl (n "a") PSet (
389 PPi impl (n "x") (PRef bi (n "a"))
390 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
391 pimp (n "b") Placeholder,
392 pexp (PRef bi (n "x")),
393 pexp (PRef bi (n "x"))])), bi)]
394 where n a = MN 0 a
396-- Defined in builtins.idr
397sigmaTy = UN "Exists"
398existsCon = UN "Ex_intro"
400piBind :: [(Name, PTerm)] -> PTerm -> PTerm
401piBind [] t = t
402piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
404tcname (UN ('@':_)) = True
405tcname (NS n _) = tcname n
406tcname _ = False
408-- Dealing with parameters
410expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
411expandParams dec ps ns tm = en tm
412 where
413 -- if we shadow a name (say in a lambda binding) that is used in a call to
414 -- a lifted function, we need access to both names - once in the scope of the
415 -- binding and once to call the lifted functions. So we'll explicitly shadow
416 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
417 -- but we didn't...)
419 mkShadow (UN n) = MN 0 n
420 mkShadow (MN i n) = MN (i+1) n
421 mkShadow (NS x s) = NS (mkShadow x) s
423 en (PLam n t s)
424 | n `elem` map fst ps
425 = let n' = mkShadow n in
426 PLam n' (en t) (en (shadow n n' s))
427 | otherwise = PLam n (en t) (en s)
428 en (PPi p n t s)
429 | n `elem` map fst ps
430 = let n' = mkShadow n in
431 PPi p n' (en t) (en (shadow n n' s))
432 | otherwise = PPi p n (en t) (en s)
433 en (PLet n ty v s)
434 | n `elem` map fst ps
435 = let n' = mkShadow n in
436 PLet n' (en ty) (en v) (en (shadow n n' s))
437 | otherwise = PLet n (en ty) (en v) (en s)
438 en (PEq f l r) = PEq f (en l) (en r)
439 en (PTyped l r) = PTyped (en l) (en r)
440 en (PPair f l r) = PPair f (en l) (en r)
441 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
442 en (PAlternative a as) = PAlternative a (map en as)
443 en (PHidden t) = PHidden (en t)
444 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
445 en (PProof ts) = PProof (map (fmap en) ts)
446 en (PTactics ts) = PTactics (map (fmap en) ts)
448 en (PQuote (Var n))
449 | n `elem` ns = PQuote (Var (dec n))
450 en (PApp fc (PRef fc' n) as)
451 | n `elem` ns = PApp fc (PRef fc' (dec n))
452 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
453 en (PRef fc n)
454 | n `elem` ns = PApp fc (PRef fc (dec n))
455 (map (pexp . (PRef fc)) (map fst ps))
456 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
457 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
458 en t = t
460expandParamsD :: IState ->
461 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
462expandParamsD ist dec ps ns (PTy syn fc o n ty)
463 = if n `elem` ns
464 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
465 else PTy syn fc o n (expandParams dec ps ns ty)
466expandParamsD ist dec ps ns (PClauses fc opts n cs)
467 = let n' = if n `elem` ns then dec n else n in
468 PClauses fc opts n' (map expandParamsC cs)
469 where
470 expandParamsC (PClause fc n lhs ws rhs ds)
471 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
472 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
473 n' = if n `elem` ns then dec n else n in
474 PClause fc n' (expandParams dec ps'' ns lhs)
475 (map (expandParams dec ps'' ns) ws)
476 (expandParams dec ps'' ns rhs)
477 (map (expandParamsD ist dec ps'' ns) ds)
478 expandParamsC (PWith fc n lhs ws wval ds)
479 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
480 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
481 n' = if n `elem` ns then dec n else n in
482 PWith fc n' (expandParams dec ps'' ns lhs)
483 (map (expandParams dec ps'' ns) ws)
484 (expandParams dec ps'' ns wval)
485 (map (expandParamsD ist dec ps'' ns) ds)
486 updateps yn nm [] = []
487 updateps yn nm (((a, t), i):as)
488 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
489 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
491expandParamsD ist dec ps ns d = d
493-- Calculate a priority for a type, for deciding elaboration order
494-- * if it's just a type variable or concrete type, do it early (0)
495-- * if there's only type variables and injective constructors, do it next (1)
496-- * if there's a function type, next (2)
497-- * finally, everything else (3)
499getPriority :: IState -> PTerm -> Int
500getPriority i tm = pri tm
501 where
502 pri (PRef _ n) =
503 case lookupP Nothing n (tt_ctxt i) of
504 ((P (DCon _ _) _ _):_) -> 1
505 ((P (TCon _ _) _ _):_) -> 1
506 ((P Ref _ _):_) -> 4
507 [] -> 0 -- must be locally bound, if it's not an error...
508 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
509 pri (PTrue _) = 0
510 pri (PFalse _) = 0
511 pri (PRefl _ _) = 1
512 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
513 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
514 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
515 pri (PTyped l r) = pri l
516 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
517 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
518 pri (PAlternative a as) = maximum (map pri as)
519 pri (PConstant _) = 0
520 pri Placeholder = 1
521 pri _ = 3
523addStatics :: Name -> Term -> PTerm -> Idris ()
524addStatics n tm ptm =
525 do let (statics, dynamics) = initStatics tm ptm
526 let stnames = nub $ concatMap freeNames (map snd statics)
527 let dnames = nub $ concatMap freeNames (map snd dynamics)
528 when (not (null statics)) $
529 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
530 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
531 let statics' = nub $ map fst statics ++
532 filter (\x -> not (elem x dnames)) stnames
533 let stpos = staticList statics' tm
534 i <- get
535 put (i { idris_statics = addDef n stpos (idris_statics i) })
536 addIBC (IBCStatic n)
537 where
538 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
539 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
540 if pstatic p == Static then ((n, ty) : static, dynamic)
541 else (static, (n, ty) : dynamic)
542 initStatics t pt = ([], [])
544 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
545 staticList _ _ = []
547-- Dealing with implicit arguments
549-- Add implicit Pi bindings for any names in the term which appear in an
550-- argument position.
552-- This has become a right mess already. Better redo it some time...
554implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
555implicit syn n ptm = implicit' syn [] n ptm
557implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
558implicit' syn ignore n ptm
559 = do i <- get
560 let (tm', impdata) = implicitise syn ignore i ptm
561-- let (tm'', spos) = findStatics i tm'
562 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
563 addIBC (IBCImp n)
564 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
565-- i <- get
566-- put (i { idris_statics = addDef n spos (idris_statics i) })
567 return tm'
569implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
570implicitise syn ignore ist tm
571 = let (declimps, ns') = execState (imps True [] tm) ([], [])
572 ns = ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
573 if null ns
574 then (tm, reverse declimps)
575 else implicitise syn ignore ist (pibind uvars ns tm)
576 where
577 uvars = using syn
578 pvars = syn_params syn
580 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
581 | otherwise = x : dropAll xs ys
582 dropAll [] ys = []
584 imps top env (PApp _ f as)
585 = do (decls, ns) <- get
586 let isn = concatMap (namesIn uvars ist) (map getTm as)
587 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
588 imps top env (PPi (Imp l _) n ty sc)
589 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
590 (decls , ns) <- get
591 put (PImp (getPriority ist ty) l n ty : decls,
592 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
593 imps True (n:env) sc
594 imps top env (PPi (Exp l _) n ty sc)
595 = do let isn = nub (namesIn uvars ist ty ++ case sc of
596 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
597 _ -> [])
598 (decls, ns) <- get -- ignore decls in HO types
599 put (PExp (getPriority ist ty) l ty : decls,
600 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
601 imps True (n:env) sc
602 imps top env (PPi (Constraint l _) n ty sc)
603 = do let isn = nub (namesIn uvars ist ty ++ case sc of
604 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
605 _ -> [])
606 (decls, ns) <- get -- ignore decls in HO types
607 put (PConstraint 10 l ty : decls,
608 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
609 imps True (n:env) sc
610 imps top env (PPi (TacImp l _ scr) n ty sc)
611 = do let isn = nub (namesIn uvars ist ty ++ case sc of
612 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
613 _ -> [])
614 (decls, ns) <- get -- ignore decls in HO types
615 put (PTacImplicit 10 l n scr ty : decls,
616 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
617 imps True (n:env) sc
618 imps top env (PEq _ l r)
619 = do (decls, ns) <- get
620 let isn = namesIn uvars ist l ++ namesIn uvars ist r
621 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
622 imps top env (PTyped l r)
623 = imps top env l
624 imps top env (PPair _ l r)
625 = do (decls, ns) <- get
626 let isn = namesIn uvars ist l ++ namesIn uvars ist r
627 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
628 imps top env (PDPair _ (PRef _ n) t r)
629 = do (decls, ns) <- get
630 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
631 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
632 imps top env (PDPair _ l t r)
633 = do (decls, ns) <- get
634 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
635 namesIn uvars ist r
636 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
637 imps top env (PAlternative a as)
638 = do (decls, ns) <- get
639 let isn = concatMap (namesIn uvars ist) as
640 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
641 imps top env (PLam n ty sc)
642 = do imps False env ty
643 imps False (n:env) sc
644 imps top env (PHidden tm) = imps False env tm
645 imps top env _ = return ()
647 pibind using [] sc = sc
648 pibind using (n:ns) sc
649 = case lookup n using of
650 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
651 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
653-- Add implicit arguments in function calls
654addImplPat :: IState -> PTerm -> PTerm
655addImplPat = addImpl' True []
657addImplBound :: IState -> [Name] -> PTerm -> PTerm
658addImplBound ist ns = addImpl' False ns ist
660addImpl :: IState -> PTerm -> PTerm
661addImpl = addImpl' False []
663-- TODO: in patterns, don't add implicits to function names guarded by constructors
664-- and *not* inside a PHidden
666addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
667addImpl' inpat env ist ptm = ai env ptm
668 where
669 ai env (PRef fc f)
670 | not (f `elem` env) = handleErr $ aiFn inpat inpat ist fc f []
671 ai env (PHidden (PRef fc f))
672 | not (f `elem` env) = handleErr $ aiFn inpat False ist fc f []
673 ai env (PEq fc l r) = let l' = ai env l
674 r' = ai env r in
675 PEq fc l' r'
676 ai env (PTyped l r) = let l' = ai env l
677 r' = ai env r in
678 PTyped l' r'
679 ai env (PPair fc l r) = let l' = ai env l
680 r' = ai env r in
681 PPair fc l' r'
682 ai env (PDPair fc l t r) = let l' = ai env l
683 t' = ai env t
684 r' = ai env r in
685 PDPair fc l' t' r'
686 ai env (PAlternative a as) = let as' = map (ai env) as in
687 PAlternative a as'
688 ai env (PApp fc (PRef _ f) as)
689 | not (f `elem` env)
690 = let as' = map (fmap (ai env)) as in
691 handleErr $ aiFn inpat False ist fc f as'
692 ai env (PApp fc f as) = let f' = ai env f
693 as' = map (fmap (ai env)) as in
694 mkPApp fc 1 f' as'
695 ai env (PCase fc c os) = let c' = ai env c
696 os' = map (pmap (ai env)) os in
697 PCase fc c' os'
698 ai env (PLam n ty sc) = let ty' = ai env ty
699 sc' = ai (n:env) sc in
700 PLam n ty' sc'
701 ai env (PLet n ty val sc)
702 = let ty' = ai env ty
703 val' = ai env val
704 sc' = ai (n:env) sc in
705 PLet n ty' val' sc'
706 ai env (PPi p n ty sc) = let ty' = ai env ty
707 sc' = ai (n:env) sc in
708 PPi p n ty' sc'
709 ai env (PHidden tm) = PHidden (ai env tm)
710 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
711 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
712 ai env tm = tm
714 handleErr (Left err) = PElabError err
715 handleErr (Right x) = x
717-- if in a pattern, and there are no arguments, and there's no possible
718-- names with zero explicit arguments, don't add implicits.
720aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
721aiFn inpat True ist fc f []
722 = case lookupDef Nothing f (tt_ctxt ist) of
723 [] -> Right $ PPatvar fc f
724 alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
725 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
726 if (not (vname f) || tcname f
727 || any constructor alts || any allImp ialts)
728 then aiFn inpat False ist fc f [] -- use it as a constructor
729 else Right $ PPatvar fc f
730 where imp (PExp _ _ _) = False
731 imp _ = True
732 allImp [] = False
733 allImp xs = all imp xs
734 constructor (TyDecl (DCon _ _) _) = True
735 constructor _ = False
737 vname (UN n) = True -- non qualified
738 vname _ = False
740aiFn inpat expat ist fc f as
741 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
742aiFn inpat expat ist fc f as
743 -- This is where namespaces get resolved by adding PAlternative
744 = case lookupCtxtName Nothing f (idris_implicits ist) of
745 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
746 [] -> if f `elem` idris_metavars ist
747 then Right $ PApp fc (PRef fc f) as
748 else Right $ mkPApp fc (length as) (PRef fc f) as
749 alts -> Right $
750 PAlternative True $
751 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
752 (insertImpl ns as)) alts
753 where
754 insertImpl :: [PArg] -> [PArg] -> [PArg]
755 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
756 PExp p l tm : insertImpl ps given
757 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
758 PConstraint p l tm : insertImpl ps given
759 insertImpl (PConstraint p l ty : ps) given =
760 PConstraint p l (PResolveTC fc) : insertImpl ps given
761 insertImpl (PImp p l n ty : ps) given =
762 case find n given [] of
763 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
764 Nothing -> PImp p l n Placeholder : insertImpl ps given
765 insertImpl (PTacImplicit p l n sc ty : ps) given =
766 case find n given [] of
767 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
768 Nothing -> if inpat
769 then PTacImplicit p l n sc Placeholder : insertImpl ps given
770 else PTacImplicit p l n sc sc : insertImpl ps given
771 insertImpl expected [] = []
772 insertImpl _ given = given
774 find n [] acc = Nothing
775 find n (PImp _ _ n' t : gs) acc
776 | n == n' = Just (t, reverse acc ++ gs)
777 find n (PTacImplicit _ _ n' _ t : gs) acc
778 | n == n' = Just (t, reverse acc ++ gs)
779 find n (g : gs) acc = find n gs (g : acc)
781mkPApp fc a f [] = f
782mkPApp fc a f as = let rest = drop a as in
783 appRest fc (PApp fc f (take a as)) rest
784 where
785 appRest fc f [] = f
786 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
788-- Find 'static' argument positions
789-- (the declared ones, plus any names in argument position in the declared
790-- statics)
791-- FIXME: It's possible that this really has to happen after elaboration
793findStatics :: IState -> PTerm -> (PTerm, [Bool])
794findStatics ist tm = trace (showImp True tm) $
795 let (ns, ss) = fs tm in
796 runState (pos ns ss tm) []
797 where fs (PPi p n t sc)
798 | Static <- pstatic p
799 = let (ns, ss) = fs sc in
800 (namesIn [] ist t : ns, n : ss)
801 | otherwise = let (ns, ss) = fs sc in
802 (ns, ss)
803 fs _ = ([], [])
805 inOne n ns = length (filter id (map (elem n) ns)) == 1
807 pos ns ss (PPi p n t sc)
808 | elem n ss = do sc' <- pos ns ss sc
809 spos <- get
810 put (True : spos)
811 return (PPi (p { pstatic = Static }) n t sc')
812 | otherwise = do sc' <- pos ns ss sc
813 spos <- get
814 put (False : spos)
815 return (PPi p n t sc')
816 pos ns ss t = return t
818-- Debugging/logging stuff
820dumpDecls :: [PDecl] -> String
821dumpDecls [] = ""
822dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
824dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
825dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
826dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
827dumpDecl (PData _ _ d) = showDImp True d
828dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
829dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
830dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
831dumpDecl (PClass _ _ cs n ps ds)
832 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
833dumpDecl (PInstance _ _ cs n _ t _ ds)
834 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
835dumpDecl _ = "..."
836-- dumpDecl (PImport i) = "import " ++ i
838-- for 6.12/7 compatibility
839data EitherErr a b = LeftErr a | RightOK b
841instance Monad (EitherErr a) where
842 return = RightOK
844 (LeftErr e) >>= k = LeftErr e
845 RightOK v >>= k = k v
847toEither (LeftErr e) = Left e
848toEither (RightOK ho) = Right ho
850-- syntactic match of a against b, returning pair of variables in a
851-- and what they match. Returns the pair that failed if not a match.
853matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
854matchClause = matchClause' False
856matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
857matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
858 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
860 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
861 fullApp x = x
863 match' x y = match (fullApp x) (fullApp y)
864 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
865 | PConstant (I _) <- getTm x = match (getTm x) x'
866 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
867 | PConstant (I _) <- getTm x = match (getTm x) x'
868 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
869 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
870 match (PApp _ f args) (PApp _ f' args')
871 | length args == length args'
872 = do mf <- match' f f'
873 ms <- zipWithM matchArg args args'
874 return (mf ++ concat ms)
875-- match (PRef _ n) (PRef _ n') | n == n' = return []
876-- | otherwise = Nothing
877 match (PRef f n) (PApp _ x []) = match (PRef f n) x
878 match (PApp _ x []) (PRef f n) = match x (PRef f n)
879 match (PRef _ n) (PRef _ n') | n == n' = return []
880 match (PRef _ n) tm
881 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
882 = return [(n, tm)]
883 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
884 mr <- match' r r'
885 return (ml ++ mr)
886 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
887 mr <- match r r'
888 return (ml ++ mr)
889 match (PTyped l r) x = match l x
890 match x (PTyped l r) = match x l
891 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
892 mr <- match' r r'
893 return (ml ++ mr)
894 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
895 mt <- match' t t'
896 mr <- match' r r'
897 return (ml ++ mt ++ mr)
898 match (PAlternative a as) (PAlternative a' as')
899 = do ms <- zipWithM match' as as'
900 return (concat ms)
901 match a@(PAlternative _ as) b
902 = do let ms = zipWith match' as (repeat b)
903 case (rights (map toEither ms)) of
904 (x: _) -> return x
905 _ -> LeftErr (a, b)
906 match (PCase _ _ _) _ = return [] -- lifted out
907 match (PMetavar _) _ = return [] -- modified
908 match (PQuote _) _ = return []
909 match (PProof _) _ = return []
910 match (PTactics _) _ = return []
911 match (PRefl _ _) (PRefl _ _) = return []
912 match (PResolveTC _) (PResolveTC _) = return []
913 match (PTrue _) (PTrue _) = return []
914 match (PFalse _) (PFalse _) = return []
915 match (PReturn _) (PReturn _) = return []
916 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
917 ms <- match' s s'
918 return (mt ++ ms)
919 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
920 ms <- match' s s'
921 return (mt ++ ms)
922 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
923 mty <- match' ty ty'
924 ms <- match' s s'
925 return (mt ++ mty ++ ms)
926 match (PHidden x) (PHidden y) = match' x y
927 match Placeholder _ = return []
928 match _ Placeholder = return []
929 match (PResolveTC _) _ = return []
930 match a b | a == b = return []
931 | otherwise = LeftErr (a, b)
933 checkRpts (RightOK ms) = check ms where
934 check ((n,t):xs)
935 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
936 then Left (t, t')
937 else check xs
938 check (_:xs) = check xs
939 check [] = Right ms
940 checkRpts (LeftErr x) = Left x
942substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
943substMatches [] t = t
944substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
946substMatch :: Name -> PTerm -> PTerm -> PTerm
947substMatch n tm t = sm t where
948 sm (PRef _ n') | n == n' = tm
949 sm (PLam x t sc) = PLam x (sm t) (sm sc)
950 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
951 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
952 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
953 sm (PEq f x y) = PEq f (sm x) (sm y)
954 sm (PTyped x y) = PTyped (sm x) (sm y)
955 sm (PPair f x y) = PPair f (sm x) (sm y)
956 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
957 sm (PAlternative a as) = PAlternative a (map sm as)
958 sm (PHidden x) = PHidden (sm x)
959 sm x = x
961shadow :: Name -> Name -> PTerm -> PTerm
962shadow n n' t = sm t where
963 sm (PRef fc x) | n == x = PRef fc n'
964 sm (PLam x t sc) = PLam x (sm t) (sm sc)
965 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
966 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
967 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
968 sm (PEq f x y) = PEq f (sm x) (sm y)
969 sm (PTyped x y) = PTyped (sm x) (sm y)
970 sm (PPair f x y) = PPair f (sm x) (sm y)
971 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
972 sm (PAlternative a as) = PAlternative a (map sm as)
973 sm (PHidden x) = PHidden (sm x)
974 sm x = x