git.iko.soy/Idris-dev
on 01dc619 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1833 lines 70 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
11import Paths_idris
13import System.Console.Haskeline
15import Control.Monad.State
17import Data.List
18import Data.Char
19import Data.Either
21import Debug.Trace
23import qualified Epic.Epic as E
25import Util.Pretty
27data IOption = IOption { opt_logLevel :: Int,
28 opt_typecase :: Bool,
29 opt_typeintype :: Bool,
30 opt_coverage :: Bool,
31 opt_showimp :: Bool,
32 opt_repl :: Bool,
33 opt_verbose :: Bool,
34 opt_ibcsubdir :: FilePath,
35 opt_importdirs :: [FilePath]
36 }
37 deriving (Show, Eq)
39defaultOpts = IOption 0 False False True False True True "" []
41-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
42-- without typechecking).
43-- This will include all the functions and data declarations, plus fixity declarations
44-- and syntax macros.
46data IState = IState { tt_ctxt :: Context,
47 idris_constraints :: [(UConstraint, FC)],
48 idris_infixes :: [FixDecl],
49 idris_implicits :: Ctxt [PArg],
50 idris_statics :: Ctxt [Bool],
51 idris_classes :: Ctxt ClassInfo,
52 idris_dsls :: Ctxt DSL,
53 idris_optimisation :: Ctxt OptInfo,
54 idris_datatypes :: Ctxt TypeInfo,
55 idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported
56 idris_flags :: Ctxt [FnOpt],
57 idris_callgraph :: Ctxt [Name],
58 idris_totcheck :: [(FC, Name)],
59 idris_log :: String,
60 idris_options :: IOption,
61 idris_name :: Int,
62 idris_metavars :: [Name],
63 syntax_rules :: [Syntax],
64 syntax_keywords :: [String],
65 imported :: [FilePath],
66 idris_prims :: [(Name, ([E.Name], E.Term))],
67 idris_objs :: [FilePath],
68 idris_libs :: [String],
69 idris_hdrs :: [String],
70 last_proof :: Maybe (Name, [String]),
71 errLine :: Maybe Int,
72 lastParse :: Maybe Name,
73 indent_stack :: [Int],
74 brace_stack :: [Maybe Int],
75 hide_list :: [(Name, Maybe Accessibility)],
76 default_access :: Accessibility,
77 ibc_write :: [IBCWrite],
78 compiled_so :: Maybe String
79 }
81-- information that needs writing for the current module's .ibc file
82data IBCWrite = IBCFix FixDecl
83 | IBCImp Name
84 | IBCStatic Name
85 | IBCClass Name
86 | IBCInstance Bool Name Name
87 | IBCDSL Name
88 | IBCData Name
89 | IBCOpt Name
90 | IBCSyntax Syntax
91 | IBCKeyword String
92 | IBCImport FilePath
93 | IBCObj FilePath
94 | IBCLib String
95 | IBCHeader String
96 | IBCAccess Name Accessibility
97 | IBCTotal Name Totality
98 | IBCFlags Name [FnOpt]
99 | IBCCG Name
100 | IBCDef Name -- i.e. main context
101 deriving Show
103idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
104 emptyContext emptyContext emptyContext emptyContext
105 emptyContext emptyContext
106 [] "" defaultOpts 6 [] [] [] [] [] [] [] []
107 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
109-- The monad for the main REPL - reading and processing files and updating
110-- global state (hence the IO inner monad).
111type Idris = StateT IState (InputT IO)
113getContext :: Idris Context
114getContext = do i <- get; return (tt_ctxt i)
116getObjectFiles :: Idris [FilePath]
117getObjectFiles = do i <- get; return (idris_objs i)
119addObjectFile :: FilePath -> Idris ()
120addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
122getLibs :: Idris [String]
123getLibs = do i <- get; return (idris_libs i)
125addLib :: String -> Idris ()
126addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
128addHdr :: String -> Idris ()
129addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
131totcheck :: (FC, Name) -> Idris ()
132totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i })
134setFlags :: Name -> [FnOpt] -> Idris ()
135setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
137setAccessibility :: Name -> Accessibility -> Idris ()
138setAccessibility n a
139 = do i <- get
140 let ctxt = setAccess n a (tt_ctxt i)
141 put (i { tt_ctxt = ctxt })
143setTotality :: Name -> Totality -> Idris ()
144setTotality n a
145 = do i <- get
146 let ctxt = setTotal n a (tt_ctxt i)
147 put (i { tt_ctxt = ctxt })
149getTotality :: Name -> Idris Totality
150getTotality n
151 = do i <- get
152 case lookupTotal n (tt_ctxt i) of
153 [t] -> return t
154 _ -> return (Total [])
156addToCG :: Name -> [Name] -> Idris ()
157addToCG n ns = do i <- get
158 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
160-- Add a class instance function. Dodgy hack: Put integer instances first in the
161-- list so they are resolved by default.
163addInstance :: Bool -> Name -> Name -> Idris ()
164addInstance int n i
165 = do ist <- get
166 case lookupCtxt Nothing n (idris_classes ist) of
167 [CI a b c d ins] ->
168 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
169 put (ist { idris_classes = cs })
170 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
171 put (ist { idris_classes = cs })
172 where addI i ins | int = i : ins
173 | otherwise = ins ++ [i]
175addClass :: Name -> ClassInfo -> Idris ()
176addClass n i
177 = do ist <- get
178 let i' = case lookupCtxt Nothing n (idris_classes ist) of
179 [c] -> c { class_instances = class_instances i }
180 _ -> i
181 put (ist { idris_classes = addDef n i' (idris_classes ist) })
183addIBC :: IBCWrite -> Idris ()
184addIBC ibc@(IBCDef n)
185 = do i <- get
186 when (notDef (ibc_write i)) $
187 put (i { ibc_write = ibc : ibc_write i })
188 where notDef [] = True
189 notDef (IBCDef n': is) | n == n' = False
190 notDef (_ : is) = notDef is
191addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
193clearIBC :: Idris ()
194clearIBC = do i <- get; put (i { ibc_write = [] })
196getHdrs :: Idris [String]
197getHdrs = do i <- get; return (idris_hdrs i)
199setErrLine :: Int -> Idris ()
200setErrLine x = do i <- get;
201 case (errLine i) of
202 Nothing -> put (i { errLine = Just x })
203 Just _ -> return ()
205clearErr :: Idris ()
206clearErr = do i <- get
207 put (i { errLine = Nothing })
209getSO :: Idris (Maybe String)
210getSO = do i <- get
211 return (compiled_so i)
213setSO :: Maybe String -> Idris ()
214setSO s = do i <- get
215 put (i { compiled_so = s })
217getIState :: Idris IState
218getIState = get
220putIState :: IState -> Idris ()
221putIState = put
223getName :: Idris Int
224getName = do i <- get;
225 let idx = idris_name i;
226 put (i { idris_name = idx + 1 })
227 return idx
229checkUndefined :: FC -> Name -> Idris ()
230checkUndefined fc n
231 = do i <- getContext
232 case lookupTy Nothing n i of
233 (_:_) -> fail $ show fc ++ ":" ++
234 show n ++ " already defined"
235 _ -> return ()
237setContext :: Context -> Idris ()
238setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
240updateContext :: (Context -> Context) -> Idris ()
241updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
243addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
244addConstraints fc (v, cs)
245 = do i <- get
246 let ctxt = tt_ctxt i
247 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
248 next_tvar = v }
249 let ics = zip cs (repeat fc) ++ idris_constraints i
250 put (i { tt_ctxt = ctxt', idris_constraints = ics })
252addDeferred :: [(Name, Type)] -> Idris ()
253addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
254 i <- get
255 put (i { idris_metavars = map fst ns ++ idris_metavars i })
256 where tidyNames used (Bind (MN i x) b sc)
257 = let n' = uniqueName (UN x) used in
258 Bind n' b $ tidyNames (n':used) sc
259 tidyNames used (Bind n b sc)
260 = let n' = uniqueName n used in
261 Bind n' b $ tidyNames (n':used) sc
262 tidyNames used b = b
264solveDeferred :: Name -> Idris ()
265solveDeferred n = do i <- get
266 put (i { idris_metavars = idris_metavars i \\ [n] })
268iputStrLn :: String -> Idris ()
269iputStrLn = liftIO . putStrLn
271iWarn :: FC -> String -> Idris ()
272iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
274setLogLevel :: Int -> Idris ()
275setLogLevel l = do i <- get
276 let opts = idris_options i
277 let opt' = opts { opt_logLevel = l }
278 put (i { idris_options = opt' } )
280logLevel :: Idris Int
281logLevel = do i <- get
282 return (opt_logLevel (idris_options i))
284useREPL :: Idris Bool
285useREPL = do i <- get
286 return (opt_repl (idris_options i))
288setREPL :: Bool -> Idris ()
289setREPL t = do i <- get
290 let opts = idris_options i
291 let opt' = opts { opt_repl = t }
292 put (i { idris_options = opt' })
294verbose :: Idris Bool
295verbose = do i <- get
296 return (opt_verbose (idris_options i))
298setVerbose :: Bool -> Idris ()
299setVerbose t = do i <- get
300 let opts = idris_options i
301 let opt' = opts { opt_verbose = t }
302 put (i { idris_options = opt' })
304typeInType :: Idris Bool
305typeInType = do i <- get
306 return (opt_typeintype (idris_options i))
308setTypeInType :: Bool -> Idris ()
309setTypeInType t = do i <- get
310 let opts = idris_options i
311 let opt' = opts { opt_typeintype = t }
312 put (i { idris_options = opt' })
314coverage :: Idris Bool
315coverage = do i <- get
316 return (opt_coverage (idris_options i))
318setCoverage :: Bool -> Idris ()
319setCoverage t = do i <- get
320 let opts = idris_options i
321 let opt' = opts { opt_coverage = t }
322 put (i { idris_options = opt' })
324setIBCSubDir :: FilePath -> Idris ()
325setIBCSubDir fp = do i <- get
326 let opts = idris_options i
327 let opt' = opts { opt_ibcsubdir = fp }
328 put (i { idris_options = opt' })
330valIBCSubDir :: IState -> Idris FilePath
331valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
333setImportDirs :: [FilePath] -> Idris ()
334setImportDirs fps = do i <- get
335 let opts = idris_options i
336 let opt' = opts { opt_importdirs = fps }
337 put (i { idris_options = opt' })
339allImportDirs :: IState -> Idris [FilePath]
340allImportDirs i = do datadir <- liftIO $ getDataDir
341 let optdirs = opt_importdirs (idris_options i)
342 return ("." : (optdirs ++ [datadir]))
344impShow :: Idris Bool
345impShow = do i <- get
346 return (opt_showimp (idris_options i))
348setImpShow :: Bool -> Idris ()
349setImpShow t = do i <- get
350 let opts = idris_options i
351 let opt' = opts { opt_showimp = t }
352 put (i { idris_options = opt' })
354logLvl :: Int -> String -> Idris ()
355logLvl l str = do i <- get
356 let lvl = opt_logLevel (idris_options i)
357 when (lvl >= l)
358 $ do liftIO (putStrLn str)
359 put (i { idris_log = idris_log i ++ str ++ "\n" } )
361iLOG :: String -> Idris ()
362iLOG = logLvl 1
364noErrors :: Idris Bool
365noErrors = do i <- get
366 case errLine i of
367 Nothing -> return True
368 _ -> return False
370setTypeCase :: Bool -> Idris ()
371setTypeCase t = do i <- get
372 let opts = idris_options i
373 let opt' = opts { opt_typecase = t }
374 put (i { idris_options = opt' })
376-- Commands in the REPL
378data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
379 | Reload | Edit
380 | Compile String | Execute | ExecVal PTerm
381 | Metavars | Prove Name | AddProof | Universes
382 | TTShell
383 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name
384 | Info Name | DebugInfo Name
385 | Search PTerm
386 | NOP
388-- Parsed declarations
390data Fixity = Infixl { prec :: Int }
391 | Infixr { prec :: Int }
392 | InfixN { prec :: Int }
393 | PrefixN { prec :: Int }
394 deriving Eq
395{-!
396deriving instance Binary Fixity
397!-}
399instance Show Fixity where
400 show (Infixl i) = "infixl " ++ show i
401 show (Infixr i) = "infixr " ++ show i
402 show (InfixN i) = "infix " ++ show i
403 show (PrefixN i) = "prefix " ++ show i
405data FixDecl = Fix Fixity String
406 deriving (Show, Eq)
407{-!
408deriving instance Binary FixDecl
409!-}
411instance Ord FixDecl where
412 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
415data Static = Static | Dynamic
416 deriving (Show, Eq)
417{-!
418deriving instance Binary Static
419!-}
421-- Mark bindings with their explicitness, and laziness
422data Plicity = Imp { plazy :: Bool,
423 pstatic :: Static }
424 | Exp { plazy :: Bool,
425 pstatic :: Static }
426 | Constraint { plazy :: Bool,
427 pstatic :: Static }
428 | TacImp { plazy :: Bool,
429 pstatic :: Static,
430 pscript :: PTerm }
431 deriving (Show, Eq)
433{-!
434deriving instance Binary Plicity
435!-}
437impl = Imp False Dynamic
438expl = Exp False Dynamic
439constraint = Constraint False Dynamic
440tacimpl = TacImp False Dynamic
442data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
443 | Specialise [Name] -- specialise it, freeze these names
444 deriving (Show, Eq)
445{-!
446deriving instance Binary FnOpt
447!-}
449type FnOpts = [FnOpt]
451inlinable :: FnOpts -> Bool
452inlinable = elem Inlinable
454data PDecl' t = PFix FC Fixity [String] -- fixity declaration
455 | PTy SyntaxInfo FC FnOpts Name t -- type declaration
456 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
457 | PData SyntaxInfo FC (PData' t) -- data declaration
458 | PParams FC [(Name, t)] [PDecl' t] -- params block
459 | PNamespace String [PDecl' t] -- new namespace
460 | PRecord SyntaxInfo FC Name t Name t -- record declaration
461 | PClass SyntaxInfo FC
462 [t] -- constraints
463 Name
464 [(Name, t)] -- parameters
465 [PDecl' t] -- declarations
466 | PInstance SyntaxInfo FC [t] -- constraints
467 Name -- class
468 [t] -- parameters
469 t -- full instance type
470 [PDecl' t]
471 | PDSL Name (DSL' t)
472 | PSyntax FC Syntax
473 | PDirective (Idris ())
474 deriving Functor
475{-!
476deriving instance Binary PDecl'
477!-}
479data PClause' t = PClause FC Name t [t] t [PDecl' t]
480 | PWith FC Name t [t] t [PDecl' t]
481 | PClauseR FC [t] t [PDecl' t]
482 | PWithR FC [t] t [PDecl' t]
483 deriving Functor
484{-!
485deriving instance Binary PClause'
486!-}
488data PData' t = PDatadecl { d_name :: Name,
489 d_tcon :: t,
490 d_cons :: [(Name, t, FC)] }
491 deriving Functor
492{-!
493deriving instance Binary PData'
494!-}
496-- Handy to get a free function for applying PTerm -> PTerm functions
497-- across a program, by deriving Functor
499type PDecl = PDecl' PTerm
500type PData = PData' PTerm
501type PClause = PClause' PTerm
503-- get all the names declared in a decl
505declared :: PDecl -> [Name]
506declared (PFix _ _ _) = []
507declared (PTy _ _ _ n t) = [n]
508declared (PClauses _ _ n _) = [] -- not a declaration
509declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
510 where fstt (a, _, _) = a
511declared (PParams _ _ ds) = concatMap declared ds
512declared (PNamespace _ ds) = concatMap declared ds
513-- declared (PImport _) = []
515defined :: PDecl -> [Name]
516defined (PFix _ _ _) = []
517defined (PTy _ _ _ n t) = []
518defined (PClauses _ _ n _) = [n] -- not a declaration
519defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
520 where fstt (a, _, _) = a
521defined (PParams _ _ ds) = concatMap defined ds
522defined (PNamespace _ ds) = concatMap defined ds
523-- declared (PImport _) = []
525updateN :: [(Name, Name)] -> Name -> Name
526updateN ns n | Just n' <- lookup n ns = n'
527updateN _ n = n
529updateNs :: [(Name, Name)] -> PTerm -> PTerm
530updateNs [] t = t
531updateNs ns t = mapPT updateRef t
532 where updateRef (PRef fc f) = PRef fc (updateN ns f)
533 updateRef t = t
535-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
536-- updateDNs [] t = t
537-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
538-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
539-- where updateCNs ns (PClause n l ts r ds)
540-- = PClause (updateN ns n) (fmap (updateNs ns) l)
541-- (map (fmap (updateNs ns)) ts)
542-- (fmap (updateNs ns) r)
543-- (map (updateDNs ns) ds)
544-- updateDNs ns c = c
546-- High level language terms
548data PTerm = PQuote Raw
549 | PRef FC Name
550 | PLam Name PTerm PTerm
551 | PPi Plicity Name PTerm PTerm
552 | PLet Name PTerm PTerm PTerm
553 | PTyped PTerm PTerm -- term with explicit type
554 | PApp FC PTerm [PArg]
555 | PCase FC PTerm [(PTerm, PTerm)]
556 | PTrue FC
557 | PFalse FC
558 | PRefl FC
559 | PResolveTC FC
560 | PEq FC PTerm PTerm
561 | PPair FC PTerm PTerm
562 | PDPair FC PTerm PTerm PTerm
563 | PAlternative Bool [PTerm] -- True if only one may work
564 | PHidden PTerm -- irrelevant or hidden pattern
565 | PSet
566 | PConstant Const
567 | Placeholder
568 | PDoBlock [PDo]
569 | PIdiom FC PTerm
570 | PReturn FC
571 | PMetavar Name
572 | PProof [PTactic]
573 | PTactics [PTactic] -- as PProof, but no auto solving
574 | PElabError Err -- error to report on elaboration
575 | PImpossible -- special case for declaring when an LHS can't typecheck
576 deriving Eq
577{-!
578deriving instance Binary PTerm
579!-}
581mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
582mapPT f t = f (mpt t) where
583 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
584 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
585 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
586 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
587 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
588 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
589 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
590 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
591 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
592 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
593 mpt (PHidden t) = PHidden (mapPT f t)
594 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
595 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
596 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
597 mpt x = x
600data PTactic' t = Intro [Name] | Intros | Focus Name
601 | Refine Name [Bool] | Rewrite t | LetTac Name t
602 | Exact t | Compute | Trivial
603 | Solve
604 | Attack
605 | ProofState | ProofTerm | Undo
606 | Try (PTactic' t) (PTactic' t)
607 | TSeq (PTactic' t) (PTactic' t)
608 | Qed | Abandon
609 deriving (Show, Eq, Functor)
610{-!
611deriving instance Binary PTactic'
612!-}
614instance Sized a => Sized (PTactic' a) where
615 size (Intro nms) = 1 + size nms
616 size Intros = 1
617 size (Focus nm) = 1 + size nm
618 size (Refine nm bs) = 1 + size nm + length bs
619 size (Rewrite t) = 1 + size t
620 size (LetTac nm t) = 1 + size nm + size t
621 size (Exact t) = 1 + size t
622 size Compute = 1
623 size Trivial = 1
624 size Solve = 1
625 size Attack = 1
626 size ProofState = 1
627 size ProofTerm = 1
628 size Undo = 1
629 size (Try l r) = 1 + size l + size r
630 size (TSeq l r) = 1 + size l + size r
631 size Qed = 1
632 size Abandon = 1
634type PTactic = PTactic' PTerm
636data PDo' t = DoExp FC t
637 | DoBind FC Name t
638 | DoBindP FC t t
639 | DoLet FC Name t t
640 | DoLetP FC t t
641 deriving (Eq, Functor)
642{-!
643deriving instance Binary PDo'
644!-}
646instance Sized a => Sized (PDo' a) where
647 size (DoExp fc t) = 1 + size fc + size t
648 size (DoBind fc nm t) = 1 + size fc + size nm + size t
649 size (DoBindP fc l r) = 1 + size fc + size l + size r
650 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
651 size (DoLetP fc l r) = 1 + size fc + size l + size r
653type PDo = PDo' PTerm
655-- The priority gives a hint as to elaboration order. Best to elaborate
656-- things early which will help give a more concrete type to other
657-- variables, e.g. a before (interpTy a).
659data PArg' t = PImp { priority :: Int,
660 lazyarg :: Bool, pname :: Name, getTm :: t }
661 | PExp { priority :: Int,
662 lazyarg :: Bool, getTm :: t }
663 | PConstraint { priority :: Int,
664 lazyarg :: Bool, getTm :: t }
665 | PTacImplicit { priority :: Int,
666 lazyarg :: Bool, pname :: Name,
667 getScript :: t,
668 getTm :: t }
669 deriving (Show, Eq, Functor)
671instance Sized a => Sized (PArg' a) where
672 size (PImp p l nm trm) = 1 + size nm + size trm
673 size (PExp p l trm) = 1 + size trm
674 size (PConstraint p l trm) = 1 + size trm
675 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
677{-!
678deriving instance Binary PArg'
679!-}
681pimp = PImp 0 True
682pexp = PExp 0 False
683pconst = PConstraint 0 False
684ptacimp = PTacImplicit 0 True
686type PArg = PArg' PTerm
688-- Type class data
690data ClassInfo = CI { instanceName :: Name,
691 class_methods :: [(Name, (FnOpts, PTerm))],
692 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
693 class_params :: [Name],
694 class_instances :: [Name] }
695 deriving Show
696{-!
697deriving instance Binary ClassInfo
698!-}
700data OptInfo = Optimise { collapsible :: Bool,
701 forceable :: [Int], -- argument positions
702 recursive :: [Int] }
703 deriving Show
704{-!
705deriving instance Binary OptInfo
706!-}
709data TypeInfo = TI { con_names :: [Name] }
710 deriving Show
711{-!
712deriving instance Binary TypeInfo
713!-}
715-- Syntactic sugar info
717data DSL' t = DSL { dsl_bind :: t,
718 dsl_return :: t,
719 dsl_apply :: t,
720 dsl_pure :: t,
721 dsl_var :: Maybe t,
722 index_first :: Maybe t,
723 index_next :: Maybe t,
724 dsl_lambda :: Maybe t,
725 dsl_let :: Maybe t
726 }
727 deriving (Show, Functor)
728{-!
729deriving instance Binary DSL'
730!-}
732type DSL = DSL' PTerm
734data SynContext = PatternSyntax | TermSyntax | AnySyntax
735 deriving Show
736{-!
737deriving instance Binary SynContext
738!-}
740data Syntax = Rule [SSymbol] PTerm SynContext
741 deriving Show
742{-!
743deriving instance Binary Syntax
744!-}
746data SSymbol = Keyword Name
747 | Symbol String
748 | Expr Name
749 | SimpleExpr Name
750 deriving Show
751{-!
752deriving instance Binary SSymbol
753!-}
755initDSL = DSL (PRef f (UN ">>="))
756 (PRef f (UN "return"))
757 (PRef f (UN "<$>"))
758 (PRef f (UN "pure"))
759 Nothing
760 Nothing
761 Nothing
762 Nothing
763 Nothing
764 where f = FC "(builtin)" 0
766data SyntaxInfo = Syn { using :: [(Name, PTerm)],
767 syn_params :: [(Name, PTerm)],
768 syn_namespace :: [String],
769 no_imp :: [Name],
770 decoration :: Name -> Name,
771 inPattern :: Bool,
772 dsl_info :: DSL }
773 deriving Show
774{-!
775deriving instance Binary SyntaxInfo
776!-}
778defaultSyntax = Syn [] [] [] [] id False initDSL
780expandNS :: SyntaxInfo -> Name -> Name
781expandNS syn n@(NS _ _) = n
782expandNS syn n = case syn_namespace syn of
783 [] -> n
784 xs -> NS n xs
787--- Pretty printing declarations and terms
789instance Show PTerm where
790 show tm = showImp False tm
792instance Pretty PTerm where
793 pretty = prettyImp False
795instance Show PDecl where
796 show d = showDeclImp False d
798instance Show PClause where
799 show c = showCImp True c
801instance Show PData where
802 show d = showDImp False d
804showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
805showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty
806showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
807showDeclImp _ (PData _ _ d) = show d
809showCImp :: Bool -> PClause -> String
810showCImp impl (PClause _ n l ws r w)
811 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
812 ++ " where " ++ show w
813 where
814 showWs [] = ""
815 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
816showCImp impl (PWith _ n l ws r w)
817 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
818 ++ " { " ++ show w ++ " } "
819 where
820 showWs [] = ""
821 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
824showDImp :: Bool -> PData -> String
825showDImp impl (PDatadecl n ty cons)
826 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
827 ++ showSep "\n\t| "
828 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
830getImps :: [PArg] -> [(Name, PTerm)]
831getImps [] = []
832getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
833getImps (_ : xs) = getImps xs
835getExps :: [PArg] -> [PTerm]
836getExps [] = []
837getExps (PExp _ _ tm : xs) = tm : getExps xs
838getExps (_ : xs) = getExps xs
840getConsts :: [PArg] -> [PTerm]
841getConsts [] = []
842getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
843getConsts (_ : xs) = getConsts xs
845getAll :: [PArg] -> [PTerm]
846getAll = map getTm
848prettyImp :: Bool -> PTerm -> Doc
849prettyImp impl = prettySe 10
850 where
851 prettySe p (PQuote r) =
852 if size r > breakingSize then
853 text "![" $$ pretty r <> text "]"
854 else
855 text "![" <> pretty r <> text "]"
856 prettySe p (PRef fc n) =
857 if impl then
858 pretty n
859 else
860 prettyBasic n
861 where
862 prettyBasic n@(UN _) = pretty n
863 prettyBasic (MN _ s) = text s
864 prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
865 prettySe p (PLam n ty sc) =
866 bracket p 2 $
867 if size sc > breakingSize then
868 text "λ" <> pretty n <+> text "=>" $+$ pretty sc
869 else
870 text "λ" <> pretty n <+> text "=>" <+> pretty sc
871 prettySe p (PLet n ty v sc) =
872 bracket p 2 $
873 if size sc > breakingSize then
874 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
875 nest nestingSize (prettySe 10 sc)
876 else
877 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
878 prettySe 10 sc
879 prettySe p (PPi (Exp l s) n ty sc)
880 | n `elem` allNamesIn sc || impl =
881 let open = if l then text "|" <> lparen else lparen in
882 bracket p 2 $
883 if size sc > breakingSize then
884 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
885 st <+> text "->" $+$ prettySe 10 sc
886 else
887 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
888 st <+> text "->" <+> prettySe 10 sc
889 | otherwise =
890 bracket p 2 $
891 if size sc > breakingSize then
892 prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
893 else
894 prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
895 where
896 st =
897 case s of
898 Static -> text "[static]"
899 _ -> empty
900 prettySe p (PPi (Imp l s) n ty sc)
901 | impl =
902 let open = if l then text "|" <> lbrace else lbrace in
903 bracket p 2 $
904 if size sc > breakingSize then
905 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
906 st <+> text "->" <+> prettySe 10 sc
907 else
908 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
909 st <+> text "->" <+> prettySe 10 sc
910 | otherwise = prettySe 10 sc
911 where
912 st =
913 case s of
914 Static -> text $ "[static]"
915 _ -> empty
916 prettySe p (PPi (Constraint _ _) n ty sc) =
917 bracket p 2 $
918 if size sc > breakingSize then
919 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
920 else
921 prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
922 prettySe p (PPi (TacImp _ _ s) n ty sc) =
923 bracket p 2 $
924 if size sc > breakingSize then
925 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
926 rbrace <+> text "->" $+$ prettySe 10 sc
927 else
928 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
929 rbrace <+> text "->" <+> prettySe 10 sc
930 prettySe p (PApp _ (PRef _ f) [])
931 | not impl = pretty f
932 prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
933 | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
934 let [l, r] = getExps args in
935 bracket p 1 $
936 if size r > breakingSize then
937 prettySe 1 l <+> pretty op $+$ prettySe 0 r
938 else
939 prettySe 1 l <+> pretty op <+> prettySe 0 r
940 prettySe p (PApp _ f as) =
941 let args = getExps as in
942 bracket p 1 $
943 prettySe 1 f <+>
944 if impl then
945 foldl fS empty as
946 -- foldr (<+>) empty $ map prettyArgS as
947 else
948 foldl fSe empty args
949 -- foldr (<+>) empty $ map prettyArgSe args
950 where
951 fS l r =
952 if size r > breakingSize then
953 l $+$ nest nestingSize (prettyArgS r)
954 else
955 l <+> prettyArgS r
957 fSe l r =
958 if size r > breakingSize then
959 l $+$ nest nestingSize (prettyArgSe r)
960 else
961 l <+> prettyArgSe r
962 prettySe p (PCase _ scr opts) =
963 text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
964 where
965 prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
967 sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
968 prettySe p (PHidden tm) = text "." <> prettySe 0 tm
969 prettySe p (PRefl _) = text "refl"
970 prettySe p (PResolveTC _) = text "resolvetc"
971 prettySe p (PTrue _) = text "()"
972 prettySe p (PFalse _) = text "_|_"
973 prettySe p (PEq _ l r) =
974 bracket p 2 $
975 if size r > breakingSize then
976 prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
977 else
978 prettySe 10 l <+> text "=" <+> prettySe 10 r
979 prettySe p (PTyped l r) =
980 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
981 prettySe p (PPair _ l r) =
982 if size r > breakingSize then
983 lparen <> prettySe 10 l <> text "," $+$
984 prettySe 10 r <> rparen
985 else
986 lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
987 prettySe p (PDPair _ l t r) =
988 if size r > breakingSize then
989 lparen <> prettySe 10 l <+> text "**" $+$
990 prettySe 10 r <> rparen
991 else
992 lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
993 prettySe p (PAlternative a as) =
994 lparen <> text "|" <> prettyAs <> text "|" <> rparen
995 where
996 prettyAs =
997 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
998 prettySe p PSet = text "Set"
999 prettySe p (PConstant c) = pretty c
1000 -- XXX: add pretty for tactics
1001 prettySe p (PProof ts) =
1002 text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1003 prettySe p (PTactics ts) =
1004 text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1005 prettySe p (PMetavar n) = text "?" <> pretty n
1006 prettySe p (PReturn f) = text "return"
1007 prettySe p PImpossible = text "impossible"
1008 prettySe p Placeholder = text "_"
1009 prettySe p (PDoBlock _) = text "do block pretty not implemented"
1010 prettySe p (PElabError s) = pretty s
1012 prettySe p _ = text "test"
1014 prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
1015 prettyArgS (PExp _ _ tm) = prettyArgSe tm
1016 prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
1017 prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
1019 prettyArgSe arg = prettySe 0 arg
1020 prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1021 prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
1022 prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1024 bracket outer inner doc
1025 | inner > outer = lparen <> doc <> rparen
1026 | otherwise = doc
1028showImp :: Bool -> PTerm -> String
1029showImp impl tm = se 10 tm where
1030 se p (PQuote r) = "![" ++ show r ++ "]"
1031 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
1032 else showbasic n
1033 where showbasic n@(UN _) = show n
1034 showbasic (MN _ s) = s
1035 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1036 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
1037 (if impl then " : " ++ se 10 ty else "") ++ " => "
1038 ++ se 10 sc
1039 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
1040 " in " ++ se 10 sc
1041 se p (PPi (Exp l s) n ty sc)
1042 | n `elem` allNamesIn sc || impl
1043 = bracket p 2 $
1044 if l then "|(" else "(" ++
1045 show n ++ " : " ++ se 10 ty ++
1046 ") " ++ st ++
1047 "-> " ++ se 10 sc
1048 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
1049 where st = case s of
1050 Static -> "[static] "
1051 _ -> ""
1052 se p (PPi (Imp l s) n ty sc)
1053 | impl = bracket p 2 $ if l then "|{" else "{" ++
1054 show n ++ " : " ++ se 10 ty ++
1055 "} " ++ st ++ "-> " ++ se 10 sc
1056 | otherwise = se 10 sc
1057 where st = case s of
1058 Static -> "[static] "
1059 _ -> ""
1060 se p (PPi (Constraint _ _) n ty sc)
1061 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1062 se p (PPi (TacImp _ _ s) n ty sc)
1063 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1064 se p (PApp _ (PRef _ f) [])
1065 | not impl = show f
1066 se p (PApp _ (PRef _ op@(UN (f:_))) args)
1067 | length (getExps args) == 2 && not impl && not (isAlpha f)
1068 = let [l, r] = getExps args in
1069 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
1070 se p (PApp _ f as)
1071 = let args = getExps as in
1072 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
1073 else concatMap seArg args
1074 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
1075 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
1076 se p (PHidden tm) = "." ++ se 0 tm
1077 se p (PRefl _) = "refl"
1078 se p (PResolveTC _) = "resolvetc"
1079 se p (PTrue _) = "()"
1080 se p (PFalse _) = "_|_"
1081 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
1082 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
1083 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
1084 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
1085 se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
1086 se p PSet = "Set"
1087 se p (PConstant c) = show c
1088 se p (PProof ts) = "proof { " ++ show ts ++ "}"
1089 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
1090 se p (PMetavar n) = "?" ++ show n
1091 se p (PReturn f) = "return"
1092 se p PImpossible = "impossible"
1093 se p Placeholder = "_"
1094 se p (PDoBlock _) = "do block show not implemented"
1095 se p (PElabError s) = show s
1096-- se p x = "Not implemented"
1098 sArg (PImp _ _ n tm) = siArg (n, tm)
1099 sArg (PExp _ _ tm) = seArg tm
1100 sArg (PConstraint _ _ tm) = scArg tm
1101 sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
1103 seArg arg = " " ++ se 0 arg
1104 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
1105 scArg val = " {{" ++ se 10 val ++ "}}"
1106 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
1108 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1109 | otherwise = str
1112 PQuote Raw
1113 | PRef FC Name
1114 | PLam Name PTerm PTerm
1115 | PPi Plicity Name PTerm PTerm
1116 | PLet Name PTerm PTerm PTerm
1117 | PTyped PTerm PTerm -- term with explicit type
1118 | PApp FC PTerm [PArg]
1119 | PCase FC PTerm [(PTerm, PTerm)]
1120 | PTrue FC
1121 | PFalse FC
1122 | PRefl FC
1123 | PResolveTC FC
1124 | PEq FC PTerm PTerm
1125 | PPair FC PTerm PTerm
1126 | PDPair FC PTerm PTerm PTerm
1127 | PAlternative [PTerm]
1128 | PHidden PTerm -- irrelevant or hidden pattern
1129 | PSet
1130 | PConstant Const
1131 | Placeholder
1132 | PDoBlock [PDo]
1133 | PIdiom FC PTerm
1134 | PReturn FC
1135 | PMetavar Name
1136 | PProof [PTactic]
1137 | PTactics [PTactic] -- as PProof, but no auto solving
1138 | PElabError Err -- error to report on elaboration
1139 | PImpossible -- special case for declaring when an LHS can't typecheck
1142instance Sized PTerm where
1143 size (PQuote rawTerm) = size rawTerm
1144 size (PRef fc name) = size name
1145 size (PLam name ty bdy) = 1 + size ty + size bdy
1146 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1147 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1148 size (PTyped trm ty) = 1 + size trm + size ty
1149 size (PApp fc name args) = 1 + size args
1150 size (PCase fc trm bdy) = 1 + size trm + size bdy
1151 size (PTrue fc) = 1
1152 size (PFalse fc) = 1
1153 size (PRefl fc) = 1
1154 size (PResolveTC fc) = 1
1155 size (PEq fc left right) = 1 + size left + size right
1156 size (PPair fc left right) = 1 + size left + size right
1157 size (PDPair fs left ty right) = 1 + size left + size ty + size right
1158 size (PAlternative a alts) = 1 + size alts
1159 size (PHidden hidden) = size hidden
1160 size PSet = 1
1161 size (PConstant const) = 1 + size const
1162 size Placeholder = 1
1163 size (PDoBlock dos) = 1 + size dos
1164 size (PIdiom fc term) = 1 + size term
1165 size (PReturn fc) = 1
1166 size (PMetavar name) = 1
1167 size (PProof tactics) = size tactics
1168 size (PElabError err) = size err
1169 size PImpossible = 1
1171allNamesIn :: PTerm -> [Name]
1172allNamesIn tm = nub $ ni [] tm
1173 where
1174 ni env (PRef _ n)
1175 | not (n `elem` env) = [n]
1176 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1177 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1178 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1179 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1180 ni env (PHidden tm) = ni env tm
1181 ni env (PEq _ l r) = ni env l ++ ni env r
1182 ni env (PTyped l r) = ni env l ++ ni env r
1183 ni env (PPair _ l r) = ni env l ++ ni env r
1184 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1185 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1186 ni env (PAlternative a ls) = concatMap (ni env) ls
1187 ni env _ = []
1189namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1190namesIn uvars ist tm = nub $ ni [] tm
1191 where
1192 ni env (PRef _ n)
1193 | not (n `elem` env)
1194 = case lookupTy Nothing n (tt_ctxt ist) of
1195 [] -> [n]
1196 _ -> if n `elem` (map fst uvars) then [n] else []
1197 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1198 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1199 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1200 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1201 ni env (PEq _ l r) = ni env l ++ ni env r
1202 ni env (PTyped l r) = ni env l ++ ni env r
1203 ni env (PPair _ l r) = ni env l ++ ni env r
1204 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1205 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1206 ni env (PAlternative a as) = concatMap (ni env) as
1207 ni env (PHidden tm) = ni env tm
1208 ni env _ = []
1210-- For inferring types of things
1212bi = FC "builtin" 0
1214inferTy = MN 0 "__Infer"
1215inferCon = MN 0 "__infer"
1216inferDecl = PDatadecl inferTy
1217 PSet
1218 [(inferCon, PPi impl (MN 0 "A") PSet (
1219 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
1220 (PRef bi inferTy)), bi)]
1222infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
1223infP = P (TCon 6 0) inferTy (Set (UVal 0))
1225getInferTerm, getInferType :: Term -> Term
1226getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1227getInferTerm (App (App _ _) tm) = tm
1228getInferTerm tm = error ("getInferTerm " ++ show tm)
1230getInferType (Bind n b sc) = Bind n b $ getInferType sc
1231getInferType (App (App _ ty) _) = ty
1233-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1235primNames = [unitTy, unitCon,
1236 falseTy, pairTy, pairCon,
1237 eqTy, eqCon, inferTy, inferCon]
1239unitTy = MN 0 "__Unit"
1240unitCon = MN 0 "__II"
1241unitDecl = PDatadecl unitTy PSet
1242 [(unitCon, PRef bi unitTy, bi)]
1244falseTy = MN 0 "__False"
1245falseDecl = PDatadecl falseTy PSet []
1247pairTy = MN 0 "__Pair"
1248pairCon = MN 0 "__MkPair"
1249pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
1250 [(pairCon, PPi impl (n "A") PSet (
1251 PPi impl (n "B") PSet (
1252 PPi expl (n "a") (PRef bi (n "A")) (
1253 PPi expl (n "b") (PRef bi (n "B"))
1254 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1255 pexp (PRef bi (n "B"))])))), bi)]
1256 where n a = MN 0 a
1258eqTy = UN "="
1259eqCon = UN "refl"
1260eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
1261 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
1262 PSet)
1263 [(eqCon, PPi impl (n "a") PSet (
1264 PPi impl (n "x") (PRef bi (n "a"))
1265 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
1266 pimp (n "b") Placeholder,
1267 pexp (PRef bi (n "x")),
1268 pexp (PRef bi (n "x"))])), bi)]
1269 where n a = MN 0 a
1271-- Defined in builtins.idr
1272sigmaTy = UN "Exists"
1273existsCon = UN "Ex_intro"
1275piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1276piBind [] t = t
1277piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
1279tcname (UN ('@':_)) = True
1280tcname (NS n _) = tcname n
1281tcname _ = False
1283-- Dealing with parameters
1285expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1286expandParams dec ps ns tm = en tm
1287 where
1288 -- if we shadow a name (say in a lambda binding) that is used in a call to
1289 -- a lifted function, we need access to both names - once in the scope of the
1290 -- binding and once to call the lifted functions. So we'll explicitly shadow
1291 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1292 -- but we didn't...)
1294 mkShadow (UN n) = MN 0 n
1295 mkShadow (MN i n) = MN (i+1) n
1296 mkShadow (NS x s) = NS (mkShadow x) s
1298 en (PLam n t s)
1299 | n `elem` map fst ps
1300 = let n' = mkShadow n in
1301 PLam n' (en t) (en (shadow n n' s))
1302 | otherwise = PLam n (en t) (en s)
1303 en (PPi p n t s)
1304 | n `elem` map fst ps
1305 = let n' = mkShadow n in
1306 PPi p n' (en t) (en (shadow n n' s))
1307 | otherwise = PPi p n (en t) (en s)
1308 en (PLet n ty v s)
1309 | n `elem` map fst ps
1310 = let n' = mkShadow n in
1311 PLet n' (en ty) (en v) (en (shadow n n' s))
1312 | otherwise = PLet n (en ty) (en v) (en s)
1313 en (PEq f l r) = PEq f (en l) (en r)
1314 en (PTyped l r) = PTyped (en l) (en r)
1315 en (PPair f l r) = PPair f (en l) (en r)
1316 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
1317 en (PAlternative a as) = PAlternative a (map en as)
1318 en (PHidden t) = PHidden (en t)
1319 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
1320 en (PProof ts) = PProof (map (fmap en) ts)
1321 en (PTactics ts) = PTactics (map (fmap en) ts)
1323 en (PQuote (Var n))
1324 | n `elem` ns = PQuote (Var (dec n))
1325 en (PApp fc (PRef fc' n) as)
1326 | n `elem` ns = PApp fc (PRef fc' (dec n))
1327 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1328 en (PRef fc n)
1329 | n `elem` ns = PApp fc (PRef fc (dec n))
1330 (map (pexp . (PRef fc)) (map fst ps))
1331 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1332 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1333 en t = t
1335expandParamsD :: IState ->
1336 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1337expandParamsD ist dec ps ns (PTy syn fc o n ty)
1338 = if n `elem` ns
1339 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
1340 else PTy syn fc o n (expandParams dec ps ns ty)
1341expandParamsD ist dec ps ns (PClauses fc opts n cs)
1342 = let n' = if n `elem` ns then dec n else n in
1343 PClauses fc opts n' (map expandParamsC cs)
1344 where
1345 expandParamsC (PClause fc n lhs ws rhs ds)
1346 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1347 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1348 n' = if n `elem` ns then dec n else n in
1349 PClause fc n' (expandParams dec ps'' ns lhs)
1350 (map (expandParams dec ps'' ns) ws)
1351 (expandParams dec ps'' ns rhs)
1352 (map (expandParamsD ist dec ps'' ns) ds)
1353 expandParamsC (PWith fc n lhs ws wval ds)
1354 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1355 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1356 n' = if n `elem` ns then dec n else n in
1357 PWith fc n' (expandParams dec ps'' ns lhs)
1358 (map (expandParams dec ps'' ns) ws)
1359 (expandParams dec ps'' ns wval)
1360 (map (expandParamsD ist dec ps'' ns) ds)
1361 updateps yn nm [] = []
1362 updateps yn nm (((a, t), i):as)
1363 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1364 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
1366expandParamsD ist dec ps ns d = d
1368-- Calculate a priority for a type, for deciding elaboration order
1369-- * if it's just a type variable or concrete type, do it early (0)
1370-- * if there's only type variables and injective constructors, do it next (1)
1371-- * if there's a function type, next (2)
1372-- * finally, everything else (3)
1374getPriority :: IState -> PTerm -> Int
1375getPriority i tm = pri tm
1376 where
1377 pri (PRef _ n) =
1378 case lookupP Nothing n (tt_ctxt i) of
1379 ((P (DCon _ _) _ _):_) -> 1
1380 ((P (TCon _ _) _ _):_) -> 1
1381 ((P Ref _ _):_) -> 4
1382 [] -> 0 -- must be locally bound, if it's not an error...
1383 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1384 pri (PTrue _) = 0
1385 pri (PFalse _) = 0
1386 pri (PRefl _) = 1
1387 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1388 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1389 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1390 pri (PTyped l r) = pri l
1391 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
1392 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1393 pri (PAlternative a as) = maximum (map pri as)
1394 pri (PConstant _) = 0
1395 pri Placeholder = 1
1396 pri _ = 3
1398addStatics :: Name -> Term -> PTerm -> Idris ()
1399addStatics n tm ptm =
1400 do let (statics, dynamics) = initStatics tm ptm
1401 let stnames = nub $ concatMap freeNames (map snd statics)
1402 let dnames = nub $ concatMap freeNames (map snd dynamics)
1403 when (not (null statics)) $
1404 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
1405 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1406 let statics' = nub $ map fst statics ++
1407 filter (\x -> not (elem x dnames)) stnames
1408 let stpos = staticList statics' tm
1409 i <- get
1410 put (i { idris_statics = addDef n stpos (idris_statics i) })
1411 addIBC (IBCStatic n)
1412 where
1413 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1414 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1415 if pstatic p == Static then ((n, ty) : static, dynamic)
1416 else (static, (n, ty) : dynamic)
1417 initStatics t pt = ([], [])
1419 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1420 staticList _ _ = []
1422-- Dealing with implicit arguments
1424-- Add implicit Pi bindings for any names in the term which appear in an
1425-- argument position.
1427-- This has become a right mess already. Better redo it some time...
1429implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1430implicit syn n ptm
1431 = do i <- get
1432 let (tm', impdata) = implicitise syn i ptm
1433-- let (tm'', spos) = findStatics i tm'
1434 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
1435 addIBC (IBCImp n)
1436 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1437-- i <- get
1438-- put (i { idris_statics = addDef n spos (idris_statics i) })
1439 return tm'
1441implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
1442implicitise syn ist tm
1443 = let (declimps, ns') = execState (imps True [] tm) ([], [])
1444 ns = ns' \\ (map fst pvars ++ no_imp syn) in
1445 if null ns
1446 then (tm, reverse declimps)
1447 else implicitise syn ist (pibind uvars ns tm)
1448 where
1449 uvars = using syn
1450 pvars = syn_params syn
1452 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1453 | otherwise = x : dropAll xs ys
1454 dropAll [] ys = []
1456 imps top env (PApp _ f as)
1457 = do (decls, ns) <- get
1458 let isn = concatMap (namesIn uvars ist) (map getTm as)
1459 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1460 imps top env (PPi (Imp l _) n ty sc)
1461 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1462 (decls , ns) <- get
1463 put (PImp (getPriority ist ty) l n ty : decls,
1464 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1465 imps True (n:env) sc
1466 imps top env (PPi (Exp l _) n ty sc)
1467 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1468 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1469 _ -> [])
1470 (decls, ns) <- get -- ignore decls in HO types
1471 put (PExp (getPriority ist ty) l ty : decls,
1472 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1473 imps True (n:env) sc
1474 imps top env (PPi (Constraint l _) n ty sc)
1475 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1476 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1477 _ -> [])
1478 (decls, ns) <- get -- ignore decls in HO types
1479 put (PConstraint 10 l ty : decls,
1480 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1481 imps True (n:env) sc
1482 imps top env (PPi (TacImp l _ scr) n ty sc)
1483 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1484 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1485 _ -> [])
1486 (decls, ns) <- get -- ignore decls in HO types
1487 put (PTacImplicit 10 l n scr ty : decls,
1488 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1489 imps True (n:env) sc
1490 imps top env (PEq _ l r)
1491 = do (decls, ns) <- get
1492 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1493 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1494 imps top env (PTyped l r)
1495 = imps top env l
1496 imps top env (PPair _ l r)
1497 = do (decls, ns) <- get
1498 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1499 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1500 imps top env (PDPair _ (PRef _ n) t r)
1501 = do (decls, ns) <- get
1502 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1503 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1504 imps top env (PDPair _ l t r)
1505 = do (decls, ns) <- get
1506 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1507 namesIn uvars ist r
1508 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1509 imps top env (PAlternative a as)
1510 = do (decls, ns) <- get
1511 let isn = concatMap (namesIn uvars ist) as
1512 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1513 imps top env (PLam n ty sc)
1514 = do imps False env ty
1515 imps False (n:env) sc
1516 imps top env (PHidden tm) = imps False env tm
1517 imps top env _ = return ()
1519 pibind using [] sc = sc
1520 pibind using (n:ns) sc
1521 = case lookup n using of
1522 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
1523 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
1525-- Add implicit arguments in function calls
1526addImplPat :: IState -> PTerm -> PTerm
1527addImplPat = addImpl' True []
1529addImplBound :: IState -> [Name] -> PTerm -> PTerm
1530addImplBound ist ns = addImpl' False ns ist
1532addImpl :: IState -> PTerm -> PTerm
1533addImpl = addImpl' False []
1535-- TODO: in patterns, don't add implicits to function names guarded by constructors
1536-- and *not* inside a PHidden
1538addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1539addImpl' inpat env ist ptm = ai env ptm
1540 where
1541 ai env (PRef fc f)
1542 | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []
1543 ai env (PHidden (PRef fc f))
1544 | not (f `elem` env) = handleErr $ aiFn False ist fc f []
1545 ai env (PEq fc l r) = let l' = ai env l
1546 r' = ai env r in
1547 PEq fc l' r'
1548 ai env (PTyped l r) = let l' = ai env l
1549 r' = ai env r in
1550 PTyped l' r'
1551 ai env (PPair fc l r) = let l' = ai env l
1552 r' = ai env r in
1553 PPair fc l' r'
1554 ai env (PDPair fc l t r) = let l' = ai env l
1555 t' = ai env t
1556 r' = ai env r in
1557 PDPair fc l' t' r'
1558 ai env (PAlternative a as) = let as' = map (ai env) as in
1559 PAlternative a as'
1560 ai env (PApp fc (PRef _ f) as)
1561 | not (f `elem` env)
1562 = let as' = map (fmap (ai env)) as in
1563 handleErr $ aiFn False ist fc f as'
1564 ai env (PApp fc f as) = let f' = ai env f
1565 as' = map (fmap (ai env)) as in
1566 mkPApp fc 1 f' as'
1567 ai env (PCase fc c os) = let c' = ai env c
1568 os' = map (pmap (ai env)) os in
1569 PCase fc c' os'
1570 ai env (PLam n ty sc) = let ty' = ai env ty
1571 sc' = ai (n:env) sc in
1572 PLam n ty' sc'
1573 ai env (PLet n ty val sc)
1574 = let ty' = ai env ty
1575 val' = ai env val
1576 sc' = ai (n:env) sc in
1577 PLet n ty' val' sc'
1578 ai env (PPi p n ty sc) = let ty' = ai env ty
1579 sc' = ai (n:env) sc in
1580 PPi p n ty' sc'
1581 ai env (PHidden tm) = PHidden (ai env tm)
1582 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1583 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1584 ai env tm = tm
1586 handleErr (Left err) = PElabError err
1587 handleErr (Right x) = x
1589-- if in a pattern, and there are no arguments, and there's no possible
1590-- names with zero explicit arguments, don't add implicits.
1592aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1593aiFn True ist fc f []
1594 = case lookupCtxt Nothing f (idris_implicits ist) of
1595 [] -> Right $ PRef fc f
1596 alts -> if (any (all imp) alts)
1597 then aiFn False ist fc f [] -- use it as a constructor
1598 else Right $ PRef fc f
1599 where imp (PExp _ _ _) = False
1600 imp _ = True
1601aiFn inpat ist fc f as
1602 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1603aiFn inpat ist fc f as
1604 -- This is where namespaces get resolved by adding PAlternative
1605 = case lookupCtxtName Nothing f (idris_implicits ist) of
1606 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1607 [] -> if f `elem` idris_metavars ist
1608 then Right $ PApp fc (PRef fc f) as
1609 else Right $ mkPApp fc (length as) (PRef fc f) as
1610 alts -> Right $
1611 PAlternative True $
1612 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1613 (insertImpl ns as)) alts
1614 where
1615 insertImpl :: [PArg] -> [PArg] -> [PArg]
1616 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1617 PExp p l tm : insertImpl ps given
1618 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1619 PConstraint p l tm : insertImpl ps given
1620 insertImpl (PConstraint p l ty : ps) given =
1621 PConstraint p l (PResolveTC fc) : insertImpl ps given
1622 insertImpl (PImp p l n ty : ps) given =
1623 case find n given [] of
1624 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
1625 Nothing -> PImp p l n Placeholder : insertImpl ps given
1626 insertImpl (PTacImplicit p l n sc ty : ps) given =
1627 case find n given [] of
1628 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1629 Nothing -> PTacImplicit p l n sc sc
1630 : insertImpl ps given
1631 insertImpl expected [] = []
1632 insertImpl _ given = given
1634 find n [] acc = Nothing
1635 find n (PImp _ _ n' t : gs) acc
1636 | n == n' = Just (t, reverse acc ++ gs)
1637 find n (g : gs) acc = find n gs (g : acc)
1639mkPApp fc a f [] = f
1640mkPApp fc a f as = let rest = drop a as in
1641 appRest fc (PApp fc f (take a as)) rest
1642 where
1643 appRest fc f [] = f
1644 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1646-- Find 'static' argument positions
1647-- (the declared ones, plus any names in argument position in the declared
1648-- statics)
1649-- FIXME: It's possible that this really has to happen after elaboration
1651findStatics :: IState -> PTerm -> (PTerm, [Bool])
1652findStatics ist tm = trace (showImp True tm) $
1653 let (ns, ss) = fs tm in
1654 runState (pos ns ss tm) []
1655 where fs (PPi p n t sc)
1656 | Static <- pstatic p
1657 = let (ns, ss) = fs sc in
1658 (namesIn [] ist t : ns, n : ss)
1659 | otherwise = let (ns, ss) = fs sc in
1660 (ns, ss)
1661 fs _ = ([], [])
1663 inOne n ns = length (filter id (map (elem n) ns)) == 1
1665 pos ns ss (PPi p n t sc)
1666 | elem n ss = do sc' <- pos ns ss sc
1667 spos <- get
1668 put (True : spos)
1669 return (PPi (p { pstatic = Static }) n t sc')
1670 | otherwise = do sc' <- pos ns ss sc
1671 spos <- get
1672 put (False : spos)
1673 return (PPi p n t sc')
1674 pos ns ss t = return t
1676-- Debugging/logging stuff
1678dumpDecls :: [PDecl] -> String
1679dumpDecls [] = ""
1680dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1682dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1683dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1684dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1685dumpDecl (PData _ _ d) = showDImp True d
1686dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1687dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1688dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1689dumpDecl (PClass _ _ cs n ps ds)
1690 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1691dumpDecl (PInstance _ _ cs n _ t ds)
1692 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1693dumpDecl _ = "..."
1694-- dumpDecl (PImport i) = "import " ++ i
1696-- for 6.12/7 compatibility
1697data EitherErr a b = LeftErr a | RightOK b
1699instance Monad (EitherErr a) where
1700 return = RightOK
1702 (LeftErr e) >>= k = LeftErr e
1703 RightOK v >>= k = k v
1705toEither (LeftErr e) = Left e
1706toEither (RightOK ho) = Right ho
1708-- syntactic match of a against b, returning pair of variables in a
1709-- and what they match. Returns the pair that failed if not a match.
1711matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1712matchClause = matchClause' False
1714matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1715matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1716 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1718 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1719 fullApp x = x
1721 match' x y = match (fullApp x) (fullApp y)
1722 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1723 | PConstant (I _) <- getTm x = match (getTm x) x'
1724 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1725 | PConstant (I _) <- getTm x = match (getTm x) x'
1726 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1727 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1728 match (PApp _ f args) (PApp _ f' args')
1729 | length args == length args'
1730 = do mf <- match' f f'
1731 ms <- zipWithM matchArg args args'
1732 return (mf ++ concat ms)
1733-- match (PRef _ n) (PRef _ n') | n == n' = return []
1734-- | otherwise = Nothing
1735 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1736 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1737 match (PRef _ n) (PRef _ n') | n == n' = return []
1738 match (PRef _ n) tm
1739 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1740 = return [(n, tm)]
1741 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1742 mr <- match' r r'
1743 return (ml ++ mr)
1744 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1745 mr <- match r r'
1746 return (ml ++ mr)
1747 match (PTyped l r) x = match l x
1748 match x (PTyped l r) = match x l
1749 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1750 mr <- match' r r'
1751 return (ml ++ mr)
1752 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1753 mt <- match' t t'
1754 mr <- match' r r'
1755 return (ml ++ mt ++ mr)
1756 match (PAlternative a as) (PAlternative a' as')
1757 = do ms <- zipWithM match' as as'
1758 return (concat ms)
1759 match a@(PAlternative _ as) b
1760 = do let ms = zipWith match' as (repeat b)
1761 case (rights (map toEither ms)) of
1762 (x: _) -> return x
1763 _ -> LeftErr (a, b)
1764 match (PCase _ _ _) _ = return [] -- lifted out
1765 match (PMetavar _) _ = return [] -- modified
1766 match (PQuote _) _ = return []
1767 match (PProof _) _ = return []
1768 match (PTactics _) _ = return []
1769 match (PRefl _) (PRefl _) = return []
1770 match (PResolveTC _) (PResolveTC _) = return []
1771 match (PTrue _) (PTrue _) = return []
1772 match (PFalse _) (PFalse _) = return []
1773 match (PReturn _) (PReturn _) = return []
1774 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1775 ms <- match' s s'
1776 return (mt ++ ms)
1777 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1778 ms <- match' s s'
1779 return (mt ++ ms)
1780 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1781 mty <- match' ty ty'
1782 ms <- match' s s'
1783 return (mt ++ mty ++ ms)
1784 match (PHidden x) (PHidden y) = match' x y
1785 match Placeholder _ = return []
1786-- match _ Placeholder = return []
1787 match (PResolveTC _) _ = return []
1788 match a b | a == b = return []
1789 | otherwise = LeftErr (a, b)
1791 checkRpts (RightOK ms) = check ms where
1792 check ((n,t):xs)
1793 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1794 then Left (t, t')
1795 else check xs
1796 check (_:xs) = check xs
1797 check [] = Right ms
1798 checkRpts (LeftErr x) = Left x
1800substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1801substMatches [] t = t
1802substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1804substMatch :: Name -> PTerm -> PTerm -> PTerm
1805substMatch n tm t = sm t where
1806 sm (PRef _ n') | n == n' = tm
1807 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1808 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1809 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1810 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1811 sm (PEq f x y) = PEq f (sm x) (sm y)
1812 sm (PTyped x y) = PTyped (sm x) (sm y)
1813 sm (PPair f x y) = PPair f (sm x) (sm y)
1814 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1815 sm (PAlternative a as) = PAlternative a (map sm as)
1816 sm (PHidden x) = PHidden (sm x)
1817 sm x = x
1819shadow :: Name -> Name -> PTerm -> PTerm
1820shadow n n' t = sm t where
1821 sm (PRef fc x) | n == x = PRef fc n'
1822 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1823 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1824 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1825 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1826 sm (PEq f x y) = PEq f (sm x) (sm y)
1827 sm (PTyped x y) = PTyped (sm x) (sm y)
1828 sm (PPair f x y) = PPair f (sm x) (sm y)
1829 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1830 sm (PAlternative a as) = PAlternative a (map sm as)
1831 sm (PHidden x) = PHidden (sm x)
1832 sm x = x