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