git.iko.soy/Idris-dev
on bb76c6c help sign in
Idris-dev/src/Idris/AbsSyntax.hs
938 lines 38 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 = implicit' syn [] n ptm
531implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
532implicit' syn ignore n ptm
533 = do i <- get
534 let (tm', impdata) = implicitise syn ignore i ptm
535-- let (tm'', spos) = findStatics i tm'
536 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
537 addIBC (IBCImp n)
538 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
539-- i <- get
540-- put (i { idris_statics = addDef n spos (idris_statics i) })
541 return tm'
543implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
544implicitise syn ignore ist tm
545 = let (declimps, ns') = execState (imps True [] tm) ([], [])
546 ns = ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
547 if null ns
548 then (tm, reverse declimps)
549 else implicitise syn ignore ist (pibind uvars ns tm)
550 where
551 uvars = using syn
552 pvars = syn_params syn
554 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
555 | otherwise = x : dropAll xs ys
556 dropAll [] ys = []
558 imps top env (PApp _ f as)
559 = do (decls, ns) <- get
560 let isn = concatMap (namesIn uvars ist) (map getTm as)
561 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
562 imps top env (PPi (Imp l _) n ty sc)
563 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
564 (decls , ns) <- get
565 put (PImp (getPriority ist ty) l n ty : decls,
566 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
567 imps True (n:env) sc
568 imps top env (PPi (Exp l _) n ty sc)
569 = do let isn = nub (namesIn uvars ist ty ++ case sc of
570 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
571 _ -> [])
572 (decls, ns) <- get -- ignore decls in HO types
573 put (PExp (getPriority ist ty) l ty : decls,
574 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
575 imps True (n:env) sc
576 imps top env (PPi (Constraint l _) n ty sc)
577 = do let isn = nub (namesIn uvars ist ty ++ case sc of
578 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
579 _ -> [])
580 (decls, ns) <- get -- ignore decls in HO types
581 put (PConstraint 10 l ty : decls,
582 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
583 imps True (n:env) sc
584 imps top env (PPi (TacImp l _ scr) n ty sc)
585 = do let isn = nub (namesIn uvars ist ty ++ case sc of
586 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
587 _ -> [])
588 (decls, ns) <- get -- ignore decls in HO types
589 put (PTacImplicit 10 l n scr ty : decls,
590 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
591 imps True (n:env) sc
592 imps top env (PEq _ l r)
593 = do (decls, ns) <- get
594 let isn = namesIn uvars ist l ++ namesIn uvars ist r
595 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
596 imps top env (PTyped l r)
597 = imps top env l
598 imps top env (PPair _ l r)
599 = do (decls, ns) <- get
600 let isn = namesIn uvars ist l ++ namesIn uvars ist r
601 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
602 imps top env (PDPair _ (PRef _ n) t r)
603 = do (decls, ns) <- get
604 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
605 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
606 imps top env (PDPair _ l t r)
607 = do (decls, ns) <- get
608 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
609 namesIn uvars ist r
610 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
611 imps top env (PAlternative a as)
612 = do (decls, ns) <- get
613 let isn = concatMap (namesIn uvars ist) as
614 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
615 imps top env (PLam n ty sc)
616 = do imps False env ty
617 imps False (n:env) sc
618 imps top env (PHidden tm) = imps False env tm
619 imps top env _ = return ()
621 pibind using [] sc = sc
622 pibind using (n:ns) sc
623 = case lookup n using of
624 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
625 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
627-- Add implicit arguments in function calls
628addImplPat :: IState -> PTerm -> PTerm
629addImplPat = addImpl' True []
631addImplBound :: IState -> [Name] -> PTerm -> PTerm
632addImplBound ist ns = addImpl' False ns ist
634addImpl :: IState -> PTerm -> PTerm
635addImpl = addImpl' False []
637-- TODO: in patterns, don't add implicits to function names guarded by constructors
638-- and *not* inside a PHidden
640addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
641addImpl' inpat env ist ptm = ai env ptm
642 where
643 ai env (PRef fc f)
644 | not (f `elem` env) = handleErr $ aiFn inpat inpat ist fc f []
645 ai env (PHidden (PRef fc f))
646 | not (f `elem` env) = handleErr $ aiFn inpat False ist fc f []
647 ai env (PEq fc l r) = let l' = ai env l
648 r' = ai env r in
649 PEq fc l' r'
650 ai env (PTyped l r) = let l' = ai env l
651 r' = ai env r in
652 PTyped l' r'
653 ai env (PPair fc l r) = let l' = ai env l
654 r' = ai env r in
655 PPair fc l' r'
656 ai env (PDPair fc l t r) = let l' = ai env l
657 t' = ai env t
658 r' = ai env r in
659 PDPair fc l' t' r'
660 ai env (PAlternative a as) = let as' = map (ai env) as in
661 PAlternative a as'
662 ai env (PApp fc (PRef _ f) as)
663 | not (f `elem` env)
664 = let as' = map (fmap (ai env)) as in
665 handleErr $ aiFn inpat False ist fc f as'
666 ai env (PApp fc f as) = let f' = ai env f
667 as' = map (fmap (ai env)) as in
668 mkPApp fc 1 f' as'
669 ai env (PCase fc c os) = let c' = ai env c
670 os' = map (pmap (ai env)) os in
671 PCase fc c' os'
672 ai env (PLam n ty sc) = let ty' = ai env ty
673 sc' = ai (n:env) sc in
674 PLam n ty' sc'
675 ai env (PLet n ty val sc)
676 = let ty' = ai env ty
677 val' = ai env val
678 sc' = ai (n:env) sc in
679 PLet n ty' val' sc'
680 ai env (PPi p n ty sc) = let ty' = ai env ty
681 sc' = ai (n:env) sc in
682 PPi p n ty' sc'
683 ai env (PHidden tm) = PHidden (ai env tm)
684 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
685 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
686 ai env tm = tm
688 handleErr (Left err) = PElabError err
689 handleErr (Right x) = x
691-- if in a pattern, and there are no arguments, and there's no possible
692-- names with zero explicit arguments, don't add implicits.
694aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
695aiFn inpat True ist fc f []
696 = case lookupCtxt Nothing f (idris_implicits ist) of
697 [] -> Right $ PRef fc f
698 alts -> if (any (all imp) alts)
699 then aiFn inpat False ist fc f [] -- use it as a constructor
700 else Right $ PRef fc f
701 where imp (PExp _ _ _) = False
702 imp _ = True
703aiFn inpat expat ist fc f as
704 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
705aiFn inpat expat ist fc f as
706 -- This is where namespaces get resolved by adding PAlternative
707 = case lookupCtxtName Nothing f (idris_implicits ist) of
708 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
709 [] -> if f `elem` idris_metavars ist
710 then Right $ PApp fc (PRef fc f) as
711 else Right $ mkPApp fc (length as) (PRef fc f) as
712 alts -> Right $
713 PAlternative True $
714 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
715 (insertImpl ns as)) alts
716 where
717 insertImpl :: [PArg] -> [PArg] -> [PArg]
718 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
719 PExp p l tm : insertImpl ps given
720 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
721 PConstraint p l tm : insertImpl ps given
722 insertImpl (PConstraint p l ty : ps) given =
723 PConstraint p l (PResolveTC fc) : insertImpl ps given
724 insertImpl (PImp p l n ty : ps) given =
725 case find n given [] of
726 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
727 Nothing -> PImp p l n Placeholder : insertImpl ps given
728 insertImpl (PTacImplicit p l n sc ty : ps) given =
729 case find n given [] of
730 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
731 Nothing -> if inpat
732 then PTacImplicit p l n sc Placeholder : insertImpl ps given
733 else PTacImplicit p l n sc sc : insertImpl ps given
734 insertImpl expected [] = []
735 insertImpl _ given = given
737 find n [] acc = Nothing
738 find n (PImp _ _ n' t : gs) acc
739 | n == n' = Just (t, reverse acc ++ gs)
740 find n (PTacImplicit _ _ n' _ t : gs) acc
741 | n == n' = Just (t, reverse acc ++ gs)
742 find n (g : gs) acc = find n gs (g : acc)
744mkPApp fc a f [] = f
745mkPApp fc a f as = let rest = drop a as in
746 appRest fc (PApp fc f (take a as)) rest
747 where
748 appRest fc f [] = f
749 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
751-- Find 'static' argument positions
752-- (the declared ones, plus any names in argument position in the declared
753-- statics)
754-- FIXME: It's possible that this really has to happen after elaboration
756findStatics :: IState -> PTerm -> (PTerm, [Bool])
757findStatics ist tm = trace (showImp True tm) $
758 let (ns, ss) = fs tm in
759 runState (pos ns ss tm) []
760 where fs (PPi p n t sc)
761 | Static <- pstatic p
762 = let (ns, ss) = fs sc in
763 (namesIn [] ist t : ns, n : ss)
764 | otherwise = let (ns, ss) = fs sc in
765 (ns, ss)
766 fs _ = ([], [])
768 inOne n ns = length (filter id (map (elem n) ns)) == 1
770 pos ns ss (PPi p n t sc)
771 | elem n ss = do sc' <- pos ns ss sc
772 spos <- get
773 put (True : spos)
774 return (PPi (p { pstatic = Static }) n t sc')
775 | otherwise = do sc' <- pos ns ss sc
776 spos <- get
777 put (False : spos)
778 return (PPi p n t sc')
779 pos ns ss t = return t
781-- Debugging/logging stuff
783dumpDecls :: [PDecl] -> String
784dumpDecls [] = ""
785dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
787dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
788dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
789dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
790dumpDecl (PData _ _ d) = showDImp True d
791dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
792dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
793dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
794dumpDecl (PClass _ _ cs n ps ds)
795 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
796dumpDecl (PInstance _ _ cs n _ t _ ds)
797 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
798dumpDecl _ = "..."
799-- dumpDecl (PImport i) = "import " ++ i
801-- for 6.12/7 compatibility
802data EitherErr a b = LeftErr a | RightOK b
804instance Monad (EitherErr a) where
805 return = RightOK
807 (LeftErr e) >>= k = LeftErr e
808 RightOK v >>= k = k v
810toEither (LeftErr e) = Left e
811toEither (RightOK ho) = Right ho
813-- syntactic match of a against b, returning pair of variables in a
814-- and what they match. Returns the pair that failed if not a match.
816matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
817matchClause = matchClause' False
819matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
820matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
821 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
823 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
824 fullApp x = x
826 match' x y = match (fullApp x) (fullApp y)
827 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
828 | PConstant (I _) <- getTm x = match (getTm x) x'
829 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
830 | PConstant (I _) <- getTm x = match (getTm x) x'
831 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
832 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
833 match (PApp _ f args) (PApp _ f' args')
834 | length args == length args'
835 = do mf <- match' f f'
836 ms <- zipWithM matchArg args args'
837 return (mf ++ concat ms)
838-- match (PRef _ n) (PRef _ n') | n == n' = return []
839-- | otherwise = Nothing
840 match (PRef f n) (PApp _ x []) = match (PRef f n) x
841 match (PApp _ x []) (PRef f n) = match x (PRef f n)
842 match (PRef _ n) (PRef _ n') | n == n' = return []
843 match (PRef _ n) tm
844 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
845 = return [(n, tm)]
846 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
847 mr <- match' r r'
848 return (ml ++ mr)
849 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
850 mr <- match r r'
851 return (ml ++ mr)
852 match (PTyped l r) x = match l x
853 match x (PTyped l r) = match x l
854 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
855 mr <- match' r r'
856 return (ml ++ mr)
857 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
858 mt <- match' t t'
859 mr <- match' r r'
860 return (ml ++ mt ++ mr)
861 match (PAlternative a as) (PAlternative a' as')
862 = do ms <- zipWithM match' as as'
863 return (concat ms)
864 match a@(PAlternative _ as) b
865 = do let ms = zipWith match' as (repeat b)
866 case (rights (map toEither ms)) of
867 (x: _) -> return x
868 _ -> LeftErr (a, b)
869 match (PCase _ _ _) _ = return [] -- lifted out
870 match (PMetavar _) _ = return [] -- modified
871 match (PQuote _) _ = return []
872 match (PProof _) _ = return []
873 match (PTactics _) _ = return []
874 match (PRefl _) (PRefl _) = return []
875 match (PResolveTC _) (PResolveTC _) = return []
876 match (PTrue _) (PTrue _) = return []
877 match (PFalse _) (PFalse _) = return []
878 match (PReturn _) (PReturn _) = return []
879 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
880 ms <- match' s s'
881 return (mt ++ ms)
882 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
883 ms <- match' s s'
884 return (mt ++ ms)
885 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
886 mty <- match' ty ty'
887 ms <- match' s s'
888 return (mt ++ mty ++ ms)
889 match (PHidden x) (PHidden y) = match' x y
890 match Placeholder _ = return []
891-- match _ Placeholder = return []
892 match (PResolveTC _) _ = return []
893 match a b | a == b = return []
894 | otherwise = LeftErr (a, b)
896 checkRpts (RightOK ms) = check ms where
897 check ((n,t):xs)
898 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
899 then Left (t, t')
900 else check xs
901 check (_:xs) = check xs
902 check [] = Right ms
903 checkRpts (LeftErr x) = Left x
905substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
906substMatches [] t = t
907substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
909substMatch :: Name -> PTerm -> PTerm -> PTerm
910substMatch n tm t = sm t where
911 sm (PRef _ n') | n == n' = tm
912 sm (PLam x t sc) = PLam x (sm t) (sm sc)
913 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
914 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
915 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
916 sm (PEq f x y) = PEq f (sm x) (sm y)
917 sm (PTyped x y) = PTyped (sm x) (sm y)
918 sm (PPair f x y) = PPair f (sm x) (sm y)
919 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
920 sm (PAlternative a as) = PAlternative a (map sm as)
921 sm (PHidden x) = PHidden (sm x)
922 sm x = x
924shadow :: Name -> Name -> PTerm -> PTerm
925shadow n n' t = sm t where
926 sm (PRef fc x) | n == x = PRef fc n'
927 sm (PLam x t sc) = PLam x (sm t) (sm sc)
928 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
929 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
930 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
931 sm (PEq f x y) = PEq f (sm x) (sm y)
932 sm (PTyped x y) = PTyped (sm x) (sm y)
933 sm (PPair f x y) = PPair f (sm x) (sm y)
934 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
935 sm (PAlternative a as) = PAlternative a (map sm as)
936 sm (PHidden x) = PHidden (sm x)
937 sm x = x