git.iko.soy/Idris-dev
on 66ff954 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1288 lines 53 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
11import Idris.IdeSlave
12import IRTS.CodegenCommon
13import Util.DynamicLinker
15import Paths_idris
17import System.Console.Haskeline
19import Control.Monad.State
21import Data.List
22import Data.Char
23import Data.Either
25import Debug.Trace
27import Util.Pretty
28import Util.System
30getContext :: Idris Context
31getContext = do i <- getIState; return (tt_ctxt i)
33getObjectFiles :: Idris [FilePath]
34getObjectFiles = do i <- getIState; return (idris_objs i)
36addObjectFile :: FilePath -> Idris ()
37addObjectFile f = do i <- getIState; putIState $ i { idris_objs = f : idris_objs i }
39getLibs :: Idris [String]
40getLibs = do i <- getIState; return (idris_libs i)
42addLib :: String -> Idris ()
43addLib f = do i <- getIState; putIState $ i { idris_libs = f : idris_libs i }
45addDyLib :: [String] -> Idris (Either DynamicLib String)
46addDyLib libs = do i <- getIState
47 handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) libs
48 case msum handle of
49 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
50 concat (intersperse "," libs) ++ "\"")
51 Just x -> do let ls = idris_dynamic_libs i
52 putIState $ i { idris_dynamic_libs = x:ls }
53 return (Left x)
55addHdr :: String -> Idris ()
56addHdr f = do i <- getIState; putIState $ i { idris_hdrs = f : idris_hdrs i }
58addLangExt :: LanguageExt -> Idris ()
59addLangExt TypeProviders = do i <- getIState ; putIState $ i { idris_language_extensions = [TypeProviders] }
61totcheck :: (FC, Name) -> Idris ()
62totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
64setFlags :: Name -> [FnOpt] -> Idris ()
65setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
67setAccessibility :: Name -> Accessibility -> Idris ()
68setAccessibility n a
69 = do i <- getIState
70 let ctxt = setAccess n a (tt_ctxt i)
71 putIState $ i { tt_ctxt = ctxt }
73setTotality :: Name -> Totality -> Idris ()
74setTotality n a
75 = do i <- getIState
76 let ctxt = setTotal n a (tt_ctxt i)
77 putIState $ i { tt_ctxt = ctxt }
79getTotality :: Name -> Idris Totality
80getTotality n
81 = do i <- getIState
82 case lookupTotal n (tt_ctxt i) of
83 [t] -> return t
84 _ -> return (Total [])
86-- Get coercions which might return the required type
87getCoercionsTo :: IState -> Type -> [Name]
88getCoercionsTo i ty =
89 let cs = idris_coercions i
90 (fn,_) = unApply (getRetTy ty) in
91 findCoercions fn cs
92 where findCoercions t [] = []
93 findCoercions t (n : ns) =
94 let ps = case lookupTy n (tt_ctxt i) of
95 [ty] -> case unApply (getRetTy ty) of
96 (t', _) ->
97 if t == t' then [n] else []
98 _ -> [] in
99 ps ++ findCoercions t ns
101addToCG :: Name -> CGInfo -> Idris ()
102addToCG n cg
103 = do i <- getIState
104 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
106addCoercion :: Name -> Idris ()
107addCoercion n = do i <- getIState
108 putIState $ i { idris_coercions = n : idris_coercions i }
110addDocStr :: Name -> String -> Idris ()
111addDocStr n doc
112 = do i <- getIState
113 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
115addToCalledG :: Name -> [Name] -> Idris ()
116addToCalledG n ns = return () -- TODO
118-- Add a class instance function. Dodgy hack: Put integer instances first in the
119-- list so they are resolved by default.
120-- Dodgy hack 2: put constraint chasers (@@) last
122addInstance :: Bool -> Name -> Name -> Idris ()
123addInstance int n i
124 = do ist <- getIState
125 case lookupCtxt n (idris_classes ist) of
126 [CI a b c d ins] ->
127 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
128 putIState $ ist { idris_classes = cs }
129 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
130 putIState $ ist { idris_classes = cs }
131 where addI i ins | int = i : ins
132 | chaser n = ins ++ [i]
133 | otherwise = insI i ins
134 insI i [] = [i]
135 insI i (n : ns) | chaser n = i : n : ns
136 | otherwise = n : insI i ns
138 chaser (UN ('@':'@':_)) = True
139 chaser (NS n _) = chaser n
140 chaser _ = False
142addClass :: Name -> ClassInfo -> Idris ()
143addClass n i
144 = do ist <- getIState
145 let i' = case lookupCtxt n (idris_classes ist) of
146 [c] -> c { class_instances = class_instances i }
147 _ -> i
148 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
150addIBC :: IBCWrite -> Idris ()
151addIBC ibc@(IBCDef n)
152 = do i <- getIState
153 when (notDef (ibc_write i)) $
154 putIState $ i { ibc_write = ibc : ibc_write i }
155 where notDef [] = True
156 notDef (IBCDef n': is) | n == n' = False
157 notDef (_ : is) = notDef is
158addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
160clearIBC :: Idris ()
161clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
163getHdrs :: Idris [String]
164getHdrs = do i <- getIState; return (idris_hdrs i)
166setErrLine :: Int -> Idris ()
167setErrLine x = do i <- getIState;
168 case (errLine i) of
169 Nothing -> putIState $ i { errLine = Just x }
170 Just _ -> return ()
172clearErr :: Idris ()
173clearErr = do i <- getIState
174 putIState $ i { errLine = Nothing }
176getSO :: Idris (Maybe String)
177getSO = do i <- getIState
178 return (compiled_so i)
180setSO :: Maybe String -> Idris ()
181setSO s = do i <- getIState
182 putIState $ (i { compiled_so = s })
184getIState :: Idris IState
185getIState = get
187putIState :: IState -> Idris ()
188putIState = put
190getName :: Idris Int
191getName = do i <- getIState;
192 let idx = idris_name i;
193 putIState $ (i { idris_name = idx + 1 })
194 return idx
196checkUndefined :: FC -> Name -> Idris ()
197checkUndefined fc n
198 = do i <- getContext
199 case lookupTy n i of
200 (_:_) -> fail $ show fc ++ ":" ++
201 show n ++ " already defined"
202 _ -> return ()
204isUndefined :: FC -> Name -> Idris Bool
205isUndefined fc n
206 = do i <- getContext
207 case lookupTy n i of
208 (_:_) -> return False
209 _ -> return True
211setContext :: Context -> Idris ()
212setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
214updateContext :: (Context -> Context) -> Idris ()
215updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
217addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
218addConstraints fc (v, cs)
219 = do i <- getIState
220 let ctxt = tt_ctxt i
221 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
222 next_tvar = v }
223 let ics = zip cs (repeat fc) ++ idris_constraints i
224 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
226addDeferred = addDeferred' Ref
227addDeferredTyCon = addDeferred' (TCon 0 0)
229addDeferred' :: NameType -> [(Name, Type)] -> Idris ()
230addDeferred' nt ns
231 = do mapM_ (\(n, t) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
232 i <- getIState
233 putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }
234 where tidyNames used (Bind (MN i x) b sc)
235 = let n' = uniqueName (UN x) used in
236 Bind n' b $ tidyNames (n':used) sc
237 tidyNames used (Bind n b sc)
238 = let n' = uniqueName n used in
239 Bind n' b $ tidyNames (n':used) sc
240 tidyNames used b = b
242solveDeferred :: Name -> Idris ()
243solveDeferred n = do i <- getIState
244 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
246iResult :: String -> Idris ()
247iResult s = do i <- getIState
248 case idris_outputmode i of
249 RawOutput -> case s of
250 "" -> return ()
251 s -> liftIO $ putStrLn s
252 IdeSlave n ->
253 let good = SexpList [SymbolAtom "ok", toSExp s] in
254 liftIO $ putStrLn $ convSExp "return" good n
256iFail :: String -> Idris ()
257iFail s = do i <- getIState
258 case idris_outputmode i of
259 RawOutput -> case s of
260 "" -> return ()
261 s -> liftIO $ putStrLn s
262 IdeSlave n ->
263 let good = SexpList [SymbolAtom "error", toSExp s] in
264 liftIO $ putStrLn $ convSExp "return" good n
266iputStrLn :: String -> Idris ()
267iputStrLn s = do i <- getIState
268 case idris_outputmode i of
269 RawOutput -> liftIO $ putStrLn s
270 IdeSlave n ->
271 case span (/=':') s of
272 (fn, ':':rest) -> case span isDigit rest of
273 ([], ':':msg) -> write
274 ([], msg) -> write
275 (num, ':':msg) -> iWarn (FC fn (read num)) msg
276 _ -> write
277 where write = liftIO $ putStrLn $ convSExp "write-string" s n
279iWarn :: FC -> String -> Idris ()
280iWarn fc err = do i <- getIState
281 case idris_outputmode i of
282 RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)
283 IdeSlave n -> liftIO $ putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
285setLogLevel :: Int -> Idris ()
286setLogLevel l = do i <- getIState
287 let opts = idris_options i
288 let opt' = opts { opt_logLevel = l }
289 putIState $ i { idris_options = opt' }
291setCmdLine :: [Opt] -> Idris ()
292setCmdLine opts = do i <- getIState
293 let iopts = idris_options i
294 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
296getDumpDefun :: Idris (Maybe FilePath)
297getDumpDefun = do i <- getIState
298 return $ findC (opt_cmdline (idris_options i))
299 where findC [] = Nothing
300 findC (DumpDefun x : _) = Just x
301 findC (_ : xs) = findC xs
303getDumpCases :: Idris (Maybe FilePath)
304getDumpCases = do i <- getIState
305 return $ findC (opt_cmdline (idris_options i))
306 where findC [] = Nothing
307 findC (DumpCases x : _) = Just x
308 findC (_ : xs) = findC xs
310logLevel :: Idris Int
311logLevel = do i <- getIState
312 return (opt_logLevel (idris_options i))
314setErrContext :: Bool -> Idris ()
315setErrContext t = do i <- getIState
316 let opts = idris_options i
317 let opt' = opts { opt_errContext = t }
318 putIState $ i { idris_options = opt' }
320errContext :: Idris Bool
321errContext = do i <- getIState
322 return (opt_errContext (idris_options i))
324useREPL :: Idris Bool
325useREPL = do i <- getIState
326 return (opt_repl (idris_options i))
328setREPL :: Bool -> Idris ()
329setREPL t = do i <- getIState
330 let opts = idris_options i
331 let opt' = opts { opt_repl = t }
332 putIState $ i { idris_options = opt' }
334setQuiet :: Bool -> Idris ()
335setQuiet q = do i <- getIState
336 let opts = idris_options i
337 let opt' = opts { opt_quiet = q }
338 putIState $ i { idris_options = opt' }
340setTarget :: Target -> Idris ()
341setTarget t = do i <- getIState
342 let opts = idris_options i
343 let opt' = opts { opt_target = t }
344 putIState $ i { idris_options = opt' }
346target :: Idris Target
347target = do i <- getIState
348 return (opt_target (idris_options i))
350setOutputTy :: OutputType -> Idris ()
351setOutputTy t = do i <- getIState
352 let opts = idris_options i
353 let opt' = opts { opt_outputTy = t }
354 putIState $ i { idris_options = opt' }
356outputTy :: Idris OutputType
357outputTy = do i <- getIState
358 return $ opt_outputTy $ idris_options i
360setIdeSlave :: Bool -> Idris ()
361setIdeSlave True = do i <- getIState
362 putIState $ i { idris_outputmode = (IdeSlave 0) }
363setIdeSlave False = return ()
365verbose :: Idris Bool
366verbose = do i <- getIState
367 return (opt_verbose (idris_options i))
369setVerbose :: Bool -> Idris ()
370setVerbose t = do i <- getIState
371 let opts = idris_options i
372 let opt' = opts { opt_verbose = t }
373 putIState $ i { idris_options = opt' }
375typeInType :: Idris Bool
376typeInType = do i <- getIState
377 return (opt_typeintype (idris_options i))
379setTypeInType :: Bool -> Idris ()
380setTypeInType t = do i <- getIState
381 let opts = idris_options i
382 let opt' = opts { opt_typeintype = t }
383 putIState $ i { idris_options = opt' }
385coverage :: Idris Bool
386coverage = do i <- getIState
387 return (opt_coverage (idris_options i))
389setCoverage :: Bool -> Idris ()
390setCoverage t = do i <- getIState
391 let opts = idris_options i
392 let opt' = opts { opt_coverage = t }
393 putIState $ i { idris_options = opt' }
395setIBCSubDir :: FilePath -> Idris ()
396setIBCSubDir fp = do i <- getIState
397 let opts = idris_options i
398 let opt' = opts { opt_ibcsubdir = fp }
399 putIState $ i { idris_options = opt' }
401valIBCSubDir :: IState -> Idris FilePath
402valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
404addImportDir :: FilePath -> Idris ()
405addImportDir fp = do i <- getIState
406 let opts = idris_options i
407 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
408 putIState $ i { idris_options = opt' }
410setImportDirs :: [FilePath] -> Idris ()
411setImportDirs fps = do i <- getIState
412 let opts = idris_options i
413 let opt' = opts { opt_importdirs = fps }
414 putIState $ i { idris_options = opt' }
416allImportDirs :: IState -> Idris [FilePath]
417allImportDirs i = do let optdirs = opt_importdirs (idris_options i)
418 return ("." : reverse optdirs)
420impShow :: Idris Bool
421impShow = do i <- getIState
422 return (opt_showimp (idris_options i))
424setImpShow :: Bool -> Idris ()
425setImpShow t = do i <- getIState
426 let opts = idris_options i
427 let opt' = opts { opt_showimp = t }
428 putIState $ i { idris_options = opt' }
430logLvl :: Int -> String -> Idris ()
431logLvl l str = do i <- getIState
432 let lvl = opt_logLevel (idris_options i)
433 when (lvl >= l)
434 $ do liftIO (putStrLn str)
435 putIState $ i { idris_log = idris_log i ++ str ++ "\n" }
437cmdOptType :: Opt -> Idris Bool
438cmdOptType x = do i <- getIState
439 return $ x `elem` opt_cmdline (idris_options i)
441iLOG :: String -> Idris ()
442iLOG = logLvl 1
444noErrors :: Idris Bool
445noErrors = do i <- getIState
446 case errLine i of
447 Nothing -> return True
448 _ -> return False
450setTypeCase :: Bool -> Idris ()
451setTypeCase t = do i <- getIState
452 let opts = idris_options i
453 let opt' = opts { opt_typecase = t }
454 putIState $ i { idris_options = opt' }
457-- For inferring types of things
459bi = FC "builtin" 0
461inferTy = MN 0 "__Infer"
462inferCon = MN 0 "__infer"
463inferDecl = PDatadecl inferTy
464 PType
465 [("", inferCon, PPi impl (MN 0 "A") PType (
466 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
467 (PRef bi inferTy)), bi)]
469infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
470infP = P (TCon 6 0) inferTy (TType (UVal 0))
472getInferTerm, getInferType :: Term -> Term
473getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
474getInferTerm (App (App _ _) tm) = tm
475getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
477getInferType (Bind n b sc) = Bind n b $ getInferType sc
478getInferType (App (App _ ty) _) = ty
480-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
482primNames = [unitTy, unitCon,
483 falseTy, pairTy, pairCon,
484 eqTy, eqCon, inferTy, inferCon]
486unitTy = MN 0 "__Unit"
487unitCon = MN 0 "__II"
488unitDecl = PDatadecl unitTy PType
489 [("", unitCon, PRef bi unitTy, bi)]
491falseTy = MN 0 "__False"
492falseDecl = PDatadecl falseTy PType []
494pairTy = MN 0 "__Pair"
495pairCon = MN 0 "__MkPair"
496pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
497 [("", pairCon, PPi impl (n "A") PType (
498 PPi impl (n "B") PType (
499 PPi expl (n "a") (PRef bi (n "A")) (
500 PPi expl (n "b") (PRef bi (n "B"))
501 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
502 pexp (PRef bi (n "B"))])))), bi)]
503 where n a = MN 0 a
505eqTy = UN "="
506eqCon = UN "refl"
507eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
508 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
509 PType)
510 [("", eqCon, PPi impl (n "a") PType (
511 PPi impl (n "x") (PRef bi (n "a"))
512 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
513 pimp (n "b") Placeholder,
514 pexp (PRef bi (n "x")),
515 pexp (PRef bi (n "x"))])), bi)]
516 where n a = MN 0 a
518-- Defined in builtins.idr
519sigmaTy = UN "Exists"
520existsCon = UN "Ex_intro"
522piBind :: [(Name, PTerm)] -> PTerm -> PTerm
523piBind = piBindp expl
525piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
526piBindp p [] t = t
527piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)
529-- Dealing with parameters
531expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
532 [Name] -> -- all names
533 [Name] -> -- names with no declaration
534 PTerm -> PTerm
535expandParams dec ps ns infs tm = en tm
536 where
537 -- if we shadow a name (say in a lambda binding) that is used in a call to
538 -- a lifted function, we need access to both names - once in the scope of the
539 -- binding and once to call the lifted functions. So we'll explicitly shadow
540 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
541 -- but we didn't...)
543 mkShadow (UN n) = MN 0 n
544 mkShadow (MN i n) = MN (i+1) n
545 mkShadow (NS x s) = NS (mkShadow x) s
547 en (PLam n t s)
548 | n `elem` map fst ps
549 = let n' = mkShadow n in
550 PLam n' (en t) (en (shadow n n' s))
551 | otherwise = PLam n (en t) (en s)
552 en (PPi p n t s)
553 | n `elem` map fst ps
554 = let n' = mkShadow n in
555 PPi p n' (en t) (en (shadow n n' s))
556 | otherwise = PPi p n (en t) (en s)
557 en (PLet n ty v s)
558 | n `elem` map fst ps
559 = let n' = mkShadow n in
560 PLet n' (en ty) (en v) (en (shadow n n' s))
561 | otherwise = PLet n (en ty) (en v) (en s)
562 en (PEq f l r) = PEq f (en l) (en r)
563 en (PRewrite f l r) = PRewrite f (en l) (en r)
564 en (PTyped l r) = PTyped (en l) (en r)
565 en (PPair f l r) = PPair f (en l) (en r)
566 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
567 en (PAlternative a as) = PAlternative a (map en as)
568 en (PHidden t) = PHidden (en t)
569 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
570 en (PProof ts) = PProof (map (fmap en) ts)
571 en (PTactics ts) = PTactics (map (fmap en) ts)
573 en (PQuote (Var n))
574 | n `nselem` ns = PQuote (Var (dec n))
575 en (PApp fc (PInferRef fc' n) as)
576 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
577 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
578 en (PApp fc (PRef fc' n) as)
579 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
580 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
581 | n `nselem` ns = PApp fc (PRef fc' (dec n))
582 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
583 en (PRef fc n)
584 | n `elem` infs = PApp fc (PInferRef fc (dec n))
585 (map (pexp . (PRef fc)) (map fst ps))
586 | n `nselem` ns = PApp fc (PRef fc (dec n))
587 (map (pexp . (PRef fc)) (map fst ps))
588 en (PInferRef fc n)
589 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
590 (map (pexp . (PRef fc)) (map fst ps))
591 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
592 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
593 en t = t
595 nselem x [] = False
596 nselem x (y : xs) | nseq x y = True
597 | otherwise = nselem x xs
599 nseq x y = nsroot x == nsroot y
601expandParamsD :: Bool -> -- True = RHS only
602 IState ->
603 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
604expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
605 = if n `elem` ns && (not rhsonly)
606 then -- trace (show (n, expandParams dec ps ns ty)) $
607 PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns [] ty))
608 else --trace (show (n, expandParams dec ps ns ty)) $
609 PTy doc syn fc o n (expandParams dec ps ns [] ty)
610expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
611 = if n `elem` ns && (not rhsonly)
612 then -- trace (show (n, expandParams dec ps ns ty)) $
613 PPostulate doc syn fc o (dec n) (piBind ps
614 (expandParams dec ps ns [] ty))
615 else --trace (show (n, expandParams dec ps ns ty)) $
616 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
617expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
618 = let n' = if n `elem` ns then dec n else n in
619 PClauses fc opts n' (map expandParamsC cs)
620 where
621 expandParamsC (PClause fc n lhs ws rhs ds)
622 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
623 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
624 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
625 n' = if n `elem` ns then dec n else n in
626 PClause fc n' lhs'
627 (map (expandParams dec ps'' ns []) ws)
628 (expandParams dec ps'' ns [] rhs)
629 (map (expandParamsD True ist dec ps'' ns) ds)
630 expandParamsC (PWith fc n lhs ws wval ds)
631 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
632 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
633 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
634 n' = if n `elem` ns then dec n else n in
635 PWith fc n' lhs'
636 (map (expandParams dec ps'' ns []) ws)
637 (expandParams dec ps'' ns [] wval)
638 (map (expandParamsD rhsonly ist dec ps'' ns) ds)
639 updateps yn nm [] = []
640 updateps yn nm (((a, t), i):as)
641 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
642 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
643expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
644 = PData doc syn fc co (expandPData pd)
645 where
646 -- just do the type decl, leave constructors alone (parameters will be
647 -- added implicitly)
648 expandPData (PDatadecl n ty cons)
649 = if n `elem` ns
650 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
651 (map econ cons)
652 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
653 econ (doc, n, t, fc)
654 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
655expandParamsD rhs ist dec ps ns (PParams f params pds)
656 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
657 (map (expandParamsD True ist dec ps ns) pds)
658-- (map (expandParamsD ist dec ps ns) pds)
659expandParamsD rhs ist dec ps ns (PMutual f pds)
660 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
661expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
662 = PClass doc info f
663 (map (expandParams dec ps ns []) cs)
664 n
665 (map (mapsnd (expandParams dec ps ns [])) params)
666 (map (expandParamsD rhs ist dec ps ns) decls)
667expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
668 = PInstance info f
669 (map (expandParams dec ps ns []) cs)
670 n
671 (map (expandParams dec ps ns []) params)
672 (expandParams dec ps ns [] ty)
673 cn
674 (map (expandParamsD rhs ist dec ps ns) decls)
675expandParamsD rhs ist dec ps ns d = d
677mapsnd f (x, t) = (x, f t)
679-- Calculate a priority for a type, for deciding elaboration order
680-- * if it's just a type variable or concrete type, do it early (0)
681-- * if there's only type variables and injective constructors, do it next (1)
682-- * if there's a function type, next (2)
683-- * finally, everything else (3)
685getPriority :: IState -> PTerm -> Int
686getPriority i tm = 1 -- pri tm
687 where
688 pri (PRef _ n) =
689 case lookupP n (tt_ctxt i) of
690 ((P (DCon _ _) _ _):_) -> 1
691 ((P (TCon _ _) _ _):_) -> 1
692 ((P Ref _ _):_) -> 1
693 [] -> 0 -- must be locally bound, if it's not an error...
694 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
695 pri (PTrue _) = 0
696 pri (PFalse _) = 0
697 pri (PRefl _ _) = 1
698 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
699 pri (PRewrite _ l r) = max 1 (max (pri l) (pri r))
700 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
701 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
702 pri (PTyped l r) = pri l
703 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
704 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
705 pri (PAlternative a as) = maximum (map pri as)
706 pri (PConstant _) = 0
707 pri Placeholder = 1
708 pri _ = 3
710addStatics :: Name -> Term -> PTerm -> Idris ()
711addStatics n tm ptm =
712 do let (statics, dynamics) = initStatics tm ptm
713 let stnames = nub $ concatMap freeNames (map snd statics)
714 let dnames = nub $ concatMap freeNames (map snd dynamics)
715 when (not (null statics)) $
716 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
717 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
718 let statics' = nub $ map fst statics ++
719 filter (\x -> not (elem x dnames)) stnames
720 let stpos = staticList statics' tm
721 i <- getIState
722 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
723 addIBC (IBCStatic n)
724 where
725 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
726 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
727 if pstatic p == Static then ((n, ty) : static, dynamic)
728 else (static, (n, ty) : dynamic)
729 initStatics t pt = ([], [])
731 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
732 staticList _ _ = []
734-- Dealing with implicit arguments
736-- Add constraint bindings from using block
738addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
739addUsingConstraints syn fc t
740 = do ist <- get
741 let ns = namesIn [] ist t
742 let cs = getConstraints t -- check declared constraints
743 let addconsts = uconsts \\ cs
744 -- if all names in the arguments of addconsts appear in ns,
745 -- add the constraint implicitly
746 return (doAdd addconsts ns t)
747 where uconsts = filter uconst (using syn)
748 uconst (UConstraint _ _) = True
749 uconst _ = False
751 doAdd [] _ t = t
752 -- if all of args in ns, then add it
753 doAdd (UConstraint c args : cs) ns t
754 | all (\n -> elem n ns) args
755 = PPi (Constraint False Dynamic "") (MN 0 "cu")
756 (mkConst c args) (doAdd cs ns t)
757 | otherwise = doAdd cs ns t
759 mkConst c args = PApp fc (PRef fc c)
760 (map (\n -> PExp 0 False (PRef fc n) "") args)
762 getConstraints (PPi (Constraint _ _ _) _ c sc)
763 = getcapp c ++ getConstraints sc
764 getConstraints (PPi _ _ c sc) = getConstraints sc
765 getConstraints _ = []
767 getcapp (PApp _ (PRef _ c) args)
768 = do ns <- mapM getName args
769 return (UConstraint c ns)
770 getcapp _ = []
772 getName (PExp _ _ (PRef _ n) _) = return n
773 getName _ = []
775-- Add implicit Pi bindings for any names in the term which appear in an
776-- argument position.
778-- This has become a right mess already. Better redo it some time...
780implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
781implicit syn n ptm = implicit' syn [] n ptm
783implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
784implicit' syn ignore n ptm
785 = do i <- getIState
786 let (tm', impdata) = implicitise syn ignore i ptm
787-- let (tm'', spos) = findStatics i tm'
788 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
789 addIBC (IBCImp n)
790 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
791-- i <- get
792-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
793 return tm'
795implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
796implicitise syn ignore ist tm
797 = let (declimps, ns') = execState (imps True [] tm) ([], [])
798 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
799 ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
800 if null ns
801 then (tm, reverse declimps)
802 else implicitise syn ignore ist (pibind uvars ns tm)
803 where
804 uvars = map ipair (filter uimplicit (using syn))
805 pvars = syn_params syn
807 ipair (UImplicit x y) = (x, y)
808 uimplicit (UImplicit _ _) = True
809 uimplicit _ = False
811 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
812 | otherwise = x : dropAll xs ys
813 dropAll [] ys = []
815 imps top env (PApp _ f as)
816 = do (decls, ns) <- get
817 let isn = concatMap (namesIn uvars ist) (map getTm as)
818 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
819 imps top env (PPi (Imp l _ doc) n ty sc)
820 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
821 (decls , ns) <- get
822 put (PImp (getPriority ist ty) l n ty doc : decls,
823 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
824 imps True (n:env) sc
825 imps top env (PPi (Exp l _ doc) n ty sc)
826 = do let isn = nub (namesIn uvars ist ty ++ case sc of
827 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
828 _ -> [])
829 (decls, ns) <- get -- ignore decls in HO types
830 put (PExp (getPriority ist ty) l ty doc : decls,
831 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
832 imps True (n:env) sc
833 imps top env (PPi (Constraint l _ doc) n ty sc)
834 = do let isn = nub (namesIn uvars ist ty ++ case sc of
835 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
836 _ -> [])
837 (decls, ns) <- get -- ignore decls in HO types
838 put (PConstraint 10 l ty doc : decls,
839 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
840 imps True (n:env) sc
841 imps top env (PPi (TacImp l _ scr doc) n ty sc)
842 = do let isn = nub (namesIn uvars ist ty ++ case sc of
843 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
844 _ -> [])
845 (decls, ns) <- get -- ignore decls in HO types
846 put (PTacImplicit 10 l n scr ty doc : decls,
847 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
848 imps True (n:env) sc
849 imps top env (PEq _ l r)
850 = do (decls, ns) <- get
851 let isn = namesIn uvars ist l ++ namesIn uvars ist r
852 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
853 imps top env (PRewrite _ l r)
854 = do (decls, ns) <- get
855 let isn = namesIn uvars ist l ++ namesIn uvars ist r
856 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
857 imps top env (PTyped l r)
858 = imps top env l
859 imps top env (PPair _ l r)
860 = do (decls, ns) <- get
861 let isn = namesIn uvars ist l ++ namesIn uvars ist r
862 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
863 imps top env (PDPair _ (PRef _ n) t r)
864 = do (decls, ns) <- get
865 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
866 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
867 imps top env (PDPair _ l t r)
868 = do (decls, ns) <- get
869 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
870 namesIn uvars ist r
871 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
872 imps top env (PAlternative a as)
873 = do (decls, ns) <- get
874 let isn = concatMap (namesIn uvars ist) as
875 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
876 imps top env (PLam n ty sc)
877 = do imps False env ty
878 imps False (n:env) sc
879 imps top env (PHidden tm) = imps False env tm
880 imps top env _ = return ()
882 pibind using [] sc = sc
883 pibind using (n:ns) sc
884 = case lookup n using of
885 Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)
886 Nothing -> PPi (Imp False Dynamic "") n Placeholder
887 (pibind using ns sc)
889-- Add implicit arguments in function calls
890addImplPat :: IState -> PTerm -> PTerm
891addImplPat = addImpl' True [] []
893addImplBound :: IState -> [Name] -> PTerm -> PTerm
894addImplBound ist ns = addImpl' False ns [] ist
896addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
897addImplBoundInf ist ns inf = addImpl' False ns inf ist
899addImpl :: IState -> PTerm -> PTerm
900addImpl = addImpl' False [] []
902-- TODO: in patterns, don't add implicits to function names guarded by constructors
903-- and *not* inside a PHidden
905addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
906addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
907 where
908 ai env (PRef fc f)
909 | f `elem` infns = PInferRef fc f
910 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
911 ai env (PHidden (PRef fc f))
912 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
913 ai env (PEq fc l r) = let l' = ai env l
914 r' = ai env r in
915 PEq fc l' r'
916 ai env (PRewrite fc l r) = let l' = ai env l
917 r' = ai env r in
918 PRewrite fc l' r'
919 ai env (PTyped l r) = let l' = ai env l
920 r' = ai env r in
921 PTyped l' r'
922 ai env (PPair fc l r) = let l' = ai env l
923 r' = ai env r in
924 PPair fc l' r'
925 ai env (PDPair fc l t r) = let l' = ai env l
926 t' = ai env t
927 r' = ai env r in
928 PDPair fc l' t' r'
929 ai env (PAlternative a as) = let as' = map (ai env) as in
930 PAlternative a as'
931 ai env (PApp fc (PInferRef _ f) as)
932 = let as' = map (fmap (ai env)) as in
933 PApp fc (PInferRef fc f) as'
934 ai env (PApp fc ftm@(PRef _ f) as)
935 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
936 | not (f `elem` map fst env)
937 = let as' = map (fmap (ai env)) as in
938 handleErr $ aiFn inpat False ist fc f as'
939 | Just (Just ty) <- lookup f env
940 = let as' = map (fmap (ai env)) as
941 arity = getPArity ty in
942 mkPApp fc arity ftm as'
943 ai env (PApp fc f as) = let f' = ai env f
944 as' = map (fmap (ai env)) as in
945 mkPApp fc 1 f' as'
946 ai env (PCase fc c os) = let c' = ai env c
947 os' = map (pmap (ai env)) os in
948 PCase fc c' os'
949 ai env (PLam n ty sc) = let ty' = ai env ty
950 sc' = ai ((n, Just ty):env) sc in
951 PLam n ty' sc'
952 ai env (PLet n ty val sc)
953 = let ty' = ai env ty
954 val' = ai env val
955 sc' = ai ((n, Just ty):env) sc in
956 PLet n ty' val' sc'
957 ai env (PPi p n ty sc) = let ty' = ai env ty
958 sc' = ai ((n, Just ty):env) sc in
959 PPi p n ty' sc'
960 ai env (PHidden tm) = PHidden (ai env tm)
961 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
962 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
963 ai env tm = tm
965 handleErr (Left err) = PElabError err
966 handleErr (Right x) = x
968-- if in a pattern, and there are no arguments, and there's no possible
969-- names with zero explicit arguments, don't add implicits.
971aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
972aiFn inpat True ist fc f []
973 = case lookupDef f (tt_ctxt ist) of
974 [] -> Right $ PPatvar fc f
975 alts -> let ialts = lookupCtxt f (idris_implicits ist) in
976 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
977 if (not (vname f) || tcname f
978 || any constructor alts || any allImp ialts)
979 then aiFn inpat False ist fc f [] -- use it as a constructor
980 else Right $ PPatvar fc f
981 where imp (PExp _ _ _ _) = False
982 imp _ = True
983 allImp [] = False
984 allImp xs = all imp xs
985 constructor (TyDecl (DCon _ _) _) = True
986 constructor _ = False
988 vname (UN n) = True -- non qualified
989 vname _ = False
991aiFn inpat expat ist fc f as
992 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
993aiFn inpat expat ist fc f as
994 -- This is where namespaces get resolved by adding PAlternative
995 = case lookupCtxtName f (idris_implicits ist) of
996 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
997 [] -> if f `elem` idris_metavars ist
998 then Right $ PApp fc (PRef fc f) as
999 else Right $ mkPApp fc (length as) (PRef fc f) as
1000 alts -> Right $
1001 PAlternative True $
1002 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1003 (insertImpl ns as)) alts
1004 where
1005 insertImpl :: [PArg] -> [PArg] -> [PArg]
1006 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1007 PExp p l tm d : insertImpl ps given
1008 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1009 PConstraint p l tm d : insertImpl ps given
1010 insertImpl (PConstraint p l ty d : ps) given =
1011 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1012 insertImpl (PImp p l n ty d : ps) given =
1013 case find n given [] of
1014 Just (tm, given') -> PImp p l n tm "" : insertImpl ps given'
1015 Nothing -> PImp p l n Placeholder "" : insertImpl ps given
1016 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1017 case find n given [] of
1018 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1019 Nothing -> if inpat
1020 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1021 else PTacImplicit p l n sc sc "" : insertImpl ps given
1022 insertImpl expected [] = []
1023 insertImpl _ given = given
1025 find n [] acc = Nothing
1026 find n (PImp _ _ n' t _ : gs) acc
1027 | n == n' = Just (t, reverse acc ++ gs)
1028 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1029 | n == n' = Just (t, reverse acc ++ gs)
1030 find n (g : gs) acc = find n gs (g : acc)
1032-- replace non-linear occurrences with _
1033-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1034-- it is hard to get right!
1036stripLinear :: IState -> PTerm -> PTerm
1037stripLinear i tm = evalState (sl tm) [] where
1038 sl :: PTerm -> State [Name] PTerm
1039 sl (PRef fc f)
1040 | (_:_) <- lookupTy f (tt_ctxt i)
1041 = return $ PRef fc f
1042 | otherwise = do ns <- get
1043 if (f `elem` ns)
1044 then return Placeholder
1045 else do put (f : ns)
1046 return (PRef fc f)
1047 sl (PPatvar fc f)
1048 = do ns <- get
1049 if (f `elem` ns)
1050 then return Placeholder
1051 else do put (f : ns)
1052 return (PPatvar fc f)
1053 sl (PApp fc fn args) = do fn' <- sl fn
1054 args' <- mapM slA args
1055 return $ PApp fc fn' args'
1056 where slA (PImp p l n t d) = do t' <- sl t
1057 return $ PImp p l n t' d
1058 slA (PExp p l t d) = do t' <- sl t
1059 return $ PExp p l t' d
1060 slA (PConstraint p l t d)
1061 = do t' <- sl t
1062 return $ PConstraint p l t' d
1063 slA (PTacImplicit p l n sc t d)
1064 = do t' <- sl t
1065 return $ PTacImplicit p l n sc t' d
1066 sl x = return x
1068mkPApp fc a f [] = f
1069mkPApp fc a f as = let rest = drop a as in
1070 appRest fc (PApp fc f (take a as)) rest
1071 where
1072 appRest fc f [] = f
1073 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1075-- Find 'static' argument positions
1076-- (the declared ones, plus any names in argument position in the declared
1077-- statics)
1078-- FIXME: It's possible that this really has to happen after elaboration
1080findStatics :: IState -> PTerm -> (PTerm, [Bool])
1081findStatics ist tm = trace (showImp True tm) $
1082 let (ns, ss) = fs tm in
1083 runState (pos ns ss tm) []
1084 where fs (PPi p n t sc)
1085 | Static <- pstatic p
1086 = let (ns, ss) = fs sc in
1087 (namesIn [] ist t : ns, n : ss)
1088 | otherwise = let (ns, ss) = fs sc in
1089 (ns, ss)
1090 fs _ = ([], [])
1092 inOne n ns = length (filter id (map (elem n) ns)) == 1
1094 pos ns ss (PPi p n t sc)
1095 | elem n ss = do sc' <- pos ns ss sc
1096 spos <- get
1097 put (True : spos)
1098 return (PPi (p { pstatic = Static }) n t sc')
1099 | otherwise = do sc' <- pos ns ss sc
1100 spos <- get
1101 put (False : spos)
1102 return (PPi p n t sc')
1103 pos ns ss t = return t
1105-- Debugging/logging stuff
1107dumpDecls :: [PDecl] -> String
1108dumpDecls [] = ""
1109dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1111dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1112dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1113dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1114dumpDecl (PData _ _ _ _ d) = showDImp True d
1115dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1116dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1117dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1118dumpDecl (PClass _ _ _ cs n ps ds)
1119 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1120dumpDecl (PInstance _ _ cs n _ t _ ds)
1121 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1122dumpDecl _ = "..."
1123-- dumpDecl (PImport i) = "import " ++ i
1125-- for 6.12/7 compatibility
1126data EitherErr a b = LeftErr a | RightOK b
1128instance Monad (EitherErr a) where
1129 return = RightOK
1131 (LeftErr e) >>= k = LeftErr e
1132 RightOK v >>= k = k v
1134toEither (LeftErr e) = Left e
1135toEither (RightOK ho) = Right ho
1137-- syntactic match of a against b, returning pair of variables in a
1138-- and what they match. Returns the pair that failed if not a match.
1140matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1141matchClause = matchClause' False
1143matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1144matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1145 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1147 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1148 fullApp x = x
1150 match' x y = match (fullApp x) (fullApp y)
1151 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1152 | PConstant (I _) <- getTm x = match (getTm x) x'
1153 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1154 | PConstant (I _) <- getTm x = match (getTm x) x'
1155 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1156 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1157 match (PApp _ f args) (PApp _ f' args')
1158 | length args == length args'
1159 = do mf <- match' f f'
1160 ms <- zipWithM matchArg args args'
1161 return (mf ++ concat ms)
1162-- match (PRef _ n) (PRef _ n') | n == n' = return []
1163-- | otherwise = Nothing
1164 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1165 match (PPatvar f n) xr = match (PRef f n) xr
1166 match xr (PPatvar f n) = match xr (PRef f n)
1167 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1168 match (PRef _ n) tm@(PRef _ n')
1169 | n == n' && not names &&
1170 (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1171 = return [(n, tm)]
1172 | n == n' = return []
1173 match (PRef _ n) tm
1174 | not names && (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1175 = return [(n, tm)]
1176 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1177 mr <- match' r r'
1178 return (ml ++ mr)
1179 match (PRewrite _ l r) (PRewrite _ l' r')
1180 = do ml <- match' l l'
1181 mr <- match' r r'
1182 return (ml ++ mr)
1183 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1184 mr <- match r r'
1185 return (ml ++ mr)
1186 match (PTyped l r) x = match l x
1187 match x (PTyped l r) = match x l
1188 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1189 mr <- match' r r'
1190 return (ml ++ mr)
1191 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1192 mt <- match' t t'
1193 mr <- match' r r'
1194 return (ml ++ mt ++ mr)
1195 match (PAlternative a as) (PAlternative a' as')
1196 = do ms <- zipWithM match' as as'
1197 return (concat ms)
1198 match a@(PAlternative _ as) b
1199 = do let ms = zipWith match' as (repeat b)
1200 case (rights (map toEither ms)) of
1201 (x: _) -> return x
1202 _ -> LeftErr (a, b)
1203 match (PCase _ _ _) _ = return [] -- lifted out
1204 match (PMetavar _) _ = return [] -- modified
1205 match (PInferRef _ _) _ = return [] -- modified
1206 match (PQuote _) _ = return []
1207 match (PProof _) _ = return []
1208 match (PTactics _) _ = return []
1209 match (PRefl _ _) (PRefl _ _) = return []
1210 match (PResolveTC _) (PResolveTC _) = return []
1211 match (PTrue _) (PTrue _) = return []
1212 match (PFalse _) (PFalse _) = return []
1213 match (PReturn _) (PReturn _) = return []
1214 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1215 ms <- match' s s'
1216 return (mt ++ ms)
1217 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1218 ms <- match' s s'
1219 return (mt ++ ms)
1220 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1221 mty <- match' ty ty'
1222 ms <- match' s s'
1223 return (mt ++ mty ++ ms)
1224 match (PHidden x) (PHidden y) = match' x y
1225 match Placeholder _ = return []
1226 match _ Placeholder = return []
1227 match (PResolveTC _) _ = return []
1228 match a b | a == b = return []
1229 | otherwise = LeftErr (a, b)
1231 checkRpts (RightOK ms) = check ms where
1232 check ((n,t):xs)
1233 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1234 then Left (t, t')
1235 else check xs
1236 check (_:xs) = check xs
1237 check [] = Right ms
1238 checkRpts (LeftErr x) = Left x
1240substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1241substMatches ms = substMatchesShadow ms []
1243substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1244substMatchesShadow [] shs t = t
1245substMatchesShadow ((n,tm):ns) shs t
1246 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1248substMatch :: Name -> PTerm -> PTerm -> PTerm
1249substMatch n = substMatchShadow n []
1251substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1252substMatchShadow n shs tm t = sm shs t where
1253 sm xs (PRef _ n') | n == n' = tm
1254 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1255 sm xs (PPi p x t sc)
1256 | x `elem` xs
1257 = let x' = nextName x in
1258 PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))
1259 (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))
1260 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1261 sm xs (PApp f x as) = PApp f (sm xs x) (map (fmap (sm xs)) as)
1262 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1263 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1264 sm xs (PRewrite f x y) = PRewrite f (sm xs x) (sm xs y)
1265 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1266 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1267 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1268 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1269 sm xs (PHidden x) = PHidden (sm xs x)
1270 sm xs x = x
1272shadow :: Name -> Name -> PTerm -> PTerm
1273shadow n n' t = sm t where
1274 sm (PRef fc x) | n == x = PRef fc n'
1275 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1276 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1277 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1278 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1279 sm (PEq f x y) = PEq f (sm x) (sm y)
1280 sm (PRewrite f x y) = PRewrite f (sm x) (sm y)
1281 sm (PTyped x y) = PTyped (sm x) (sm y)
1282 sm (PPair f x y) = PPair f (sm x) (sm y)
1283 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1284 sm (PAlternative a as) = PAlternative a (map sm as)
1285 sm (PHidden x) = PHidden (sm x)
1286 sm x = x