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