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