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