git.iko.soy/Idris-dev
on fcb66ca help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1258 lines 45 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntaxTree where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
10import IRTS.Lang
11import IRTS.CodegenCommon
12import Util.Pretty
13import Util.DynamicLinker
15import Paths_idris
17import System.Console.Haskeline
19import Control.Monad.Trans.State.Strict
21import Data.List
22import Data.Char
23import Data.Either
25import Debug.Trace
27data IOption = IOption { opt_logLevel :: Int,
28 opt_typecase :: Bool,
29 opt_typeintype :: Bool,
30 opt_coverage :: Bool,
31 opt_showimp :: Bool,
32 opt_errContext :: Bool,
33 opt_repl :: Bool,
34 opt_verbose :: Bool,
35 opt_quiet :: Bool,
36 opt_codegen :: Codegen,
37 opt_outputTy :: OutputType,
38 opt_ibcsubdir :: FilePath,
39 opt_importdirs :: [FilePath],
40 opt_triple :: String,
41 opt_cpu :: String,
42 opt_optLevel :: Int,
43 opt_cmdline :: [Opt] -- remember whole command line
44 }
45 deriving (Show, Eq)
47defaultOpts = IOption { opt_logLevel = 0
48 , opt_typecase = False
49 , opt_typeintype = False
50 , opt_coverage = True
51 , opt_showimp = False
52 , opt_errContext = False
53 , opt_repl = True
54 , opt_verbose = True
55 , opt_quiet = False
56 , opt_codegen = ViaC
57 , opt_outputTy = Executable
58 , opt_ibcsubdir = ""
59 , opt_importdirs = []
60 , opt_triple = ""
61 , opt_cpu = ""
62 , opt_optLevel = 2
63 , opt_cmdline = []
64 }
66data LanguageExt = TypeProviders deriving (Show, Eq, Read, Ord)
68-- | The output mode in use
69data OutputMode = RawOutput | IdeSlave Integer deriving Show
71-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
72-- without typechecking).
73-- This will include all the functions and data declarations, plus fixity declarations
74-- and syntax macros.
76-- | The global state used in the Idris monad
77data IState = IState {
78 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
79 idris_constraints :: [(UConstraint, FC)],
80 -- ^ A list of universe constraints and their corresponding source locations
81 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
82 idris_implicits :: Ctxt [PArg],
83 idris_statics :: Ctxt [Bool],
84 idris_classes :: Ctxt ClassInfo,
85 idris_dsls :: Ctxt DSL,
86 idris_optimisation :: Ctxt OptInfo,
87 idris_datatypes :: Ctxt TypeInfo,
88 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
89 -- ^ list of lhs/rhs, and a list of missing clauses
90 idris_flags :: Ctxt [FnOpt],
91 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
92 idris_calledgraph :: Ctxt [Name],
93 idris_docstrings :: Ctxt String,
94 idris_totcheck :: [(FC, Name)],
95 idris_log :: String,
96 idris_options :: IOption,
97 idris_name :: Int,
98 idris_metavars :: [Name], -- ^ The currently defined but not proven metavariables
99 idris_coercions :: [Name],
100 syntax_rules :: [Syntax],
101 syntax_keywords :: [String],
102 imported :: [FilePath], -- ^ The imported modules
103 idris_scprims :: [(Name, (Int, PrimFn))],
104 idris_objs :: [(Codegen, FilePath)],
105 idris_libs :: [(Codegen, String)],
106 idris_hdrs :: [(Codegen, String)],
107 proof_list :: [(Name, [String])],
108 errLine :: Maybe Int,
109 lastParse :: Maybe Name,
110 indent_stack :: [Int],
111 brace_stack :: [Maybe Int],
112 hide_list :: [(Name, Maybe Accessibility)],
113 default_access :: Accessibility,
114 default_total :: Bool,
115 ibc_write :: [IBCWrite],
116 compiled_so :: Maybe String,
117 idris_dynamic_libs :: [DynamicLib],
118 idris_language_extensions :: [LanguageExt],
119 idris_outputmode :: OutputMode
120 }
122data SizeChange = Smaller | Same | Bigger | Unknown
123 deriving (Show, Eq)
124{-!
125deriving instance Binary SizeChange
126!-}
128type SCGEntry = (Name, [Maybe (Int, SizeChange)])
130data CGInfo = CGInfo { argsdef :: [Name],
131 calls :: [(Name, [[Name]])],
132 scg :: [SCGEntry],
133 argsused :: [Name],
134 unusedpos :: [Int] }
135 deriving Show
136{-!
137deriving instance Binary CGInfo
138!-}
140primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]
142-- information that needs writing for the current module's .ibc file
143data IBCWrite = IBCFix FixDecl
144 | IBCImp Name
145 | IBCStatic Name
146 | IBCClass Name
147 | IBCInstance Bool Name Name
148 | IBCDSL Name
149 | IBCData Name
150 | IBCOpt Name
151 | IBCSyntax Syntax
152 | IBCKeyword String
153 | IBCImport FilePath
154 | IBCObj Codegen FilePath
155 | IBCLib Codegen String
156 | IBCDyLib String
157 | IBCHeader Codegen String
158 | IBCAccess Name Accessibility
159 | IBCTotal Name Totality
160 | IBCFlags Name [FnOpt]
161 | IBCCG Name
162 | IBCDoc Name
163 | IBCCoercion Name
164 | IBCDef Name -- i.e. main context
165 deriving Show
167idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
168 emptyContext emptyContext emptyContext emptyContext
169 emptyContext emptyContext emptyContext emptyContext
170 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []
171 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
173-- | The monad for the main REPL - reading and processing files and updating
174-- global state (hence the IO inner monad).
175--type Idris = WriterT [Either String (IO ())] (State IState a))
176type Idris = StateT IState IO
178-- Commands in the REPL
180data Codegen = ViaC
181 | ViaJava
182 | ViaNode
183 | ViaJavaScript
184 | ViaLLVM
185 | Bytecode
186 deriving (Show, Eq)
188-- | REPL commands
189data Command = Quit
190 | Help
191 | Eval PTerm
192 | Check PTerm
193 | DocStr Name
194 | TotCheck Name
195 | Reload
196 | Load FilePath
197 | ChangeDirectory FilePath
198 | ModImport String
199 | Edit
200 | Compile Codegen String
201 | Execute
202 | ExecVal PTerm
203 | NewCompile String
204 | Metavars
205 | Prove Name
206 | AddProof (Maybe Name)
207 | RmProof Name
208 | ShowProof Name
209 | Proofs
210 | Universes
211 | TTShell
212 | LogLvl Int
213 | Spec PTerm
214 | HNF PTerm
215 | Defn Name
216 | Info Name
217 | Missing Name
218 | DynamicLink FilePath
219 | ListDynamic
220 | Pattelab PTerm
221 | DebugInfo Name
222 | Search PTerm
223 | SetOpt Opt
224 | UnsetOpt Opt
225 | NOP
227data Opt = Filename String
228 | Ver
229 | Usage
230 | Quiet
231 | Ideslave
232 | ShowLibs
233 | ShowLibdir
234 | ShowIncs
235 | NoPrelude
236 | NoREPL
237 | OLogging Int
238 | Output String
239 | NewOutput String
240 | TypeCase
241 | TypeInType
242 | DefaultTotal
243 | DefaultPartial
244 | WarnPartial
245 | NoCoverage
246 | ErrContext
247 | ShowImpl
248 | Verbose
249 | IBCSubDir String
250 | ImportDir String
251 | PkgBuild String
252 | PkgInstall String
253 | PkgClean String
254 | WarnOnly
255 | Pkg String
256 | BCAsm String
257 | DumpDefun String
258 | DumpCases String
259 | FOVM String
260 | UseCodegen Codegen
261 | OutputTy OutputType
262 | Extension LanguageExt
263 | InterpretScript String
264 | TargetTriple String
265 | TargetCPU String
266 | OptLevel Int
267 deriving (Show, Eq)
269-- Parsed declarations
271data Fixity = Infixl { prec :: Int }
272 | Infixr { prec :: Int }
273 | InfixN { prec :: Int }
274 | PrefixN { prec :: Int }
275 deriving Eq
276{-!
277deriving instance Binary Fixity
278!-}
280instance Show Fixity where
281 show (Infixl i) = "infixl " ++ show i
282 show (Infixr i) = "infixr " ++ show i
283 show (InfixN i) = "infix " ++ show i
284 show (PrefixN i) = "prefix " ++ show i
286data FixDecl = Fix Fixity String
287 deriving Eq
289instance Show FixDecl where
290 show (Fix f s) = show f ++ " " ++ s
292{-!
293deriving instance Binary FixDecl
294!-}
296instance Ord FixDecl where
297 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
300data Static = Static | Dynamic
301 deriving (Show, Eq)
302{-!
303deriving instance Binary Static
304!-}
306-- Mark bindings with their explicitness, and laziness
307data Plicity = Imp { plazy :: Bool,
308 pstatic :: Static,
309 pdocstr :: String }
310 | Exp { plazy :: Bool,
311 pstatic :: Static,
312 pdocstr :: String }
313 | Constraint { plazy :: Bool,
314 pstatic :: Static,
315 pdocstr :: String }
316 | TacImp { plazy :: Bool,
317 pstatic :: Static,
318 pscript :: PTerm,
319 pdocstr :: String }
320 deriving (Show, Eq)
322{-!
323deriving instance Binary Plicity
324!-}
326impl = Imp False Dynamic ""
327expl = Exp False Dynamic ""
328constraint = Constraint False Dynamic ""
329tacimpl t = TacImp False Dynamic t ""
331data FnOpt = Inlinable | TotalFn | PartialFn
332 | Coinductive | AssertTotal | TCGen
333 | Implicit -- implicit coercion
334 | CExport String -- export, with a C name
335 | Specialise [Name] -- specialise it, freeze these names
336 deriving (Show, Eq)
337{-!
338deriving instance Binary FnOpt
339!-}
341type FnOpts = [FnOpt]
343inlinable :: FnOpts -> Bool
344inlinable = elem Inlinable
346-- | Top-level declarations such as compiler directives, definitions,
347-- datatypes and typeclasses.
348data PDecl' t
349 = PFix FC Fixity [String] -- ^ Fixity declaration
350 | PTy String SyntaxInfo FC FnOpts Name t -- ^ Type declaration
351 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate
352 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
353 | PCAF FC Name t -- ^ Top level constant
354 | PData String SyntaxInfo FC Bool (PData' t) -- ^ Data declaration. The Bool argument is True for codata.
355 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
356 | PNamespace String [PDecl' t] -- ^ New namespace
357 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration
358 | PClass String SyntaxInfo FC
359 [t] -- constraints
360 Name
361 [(Name, t)] -- parameters
362 [PDecl' t] -- declarations
363 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
364 -- class name, parameters, method declarations
365 | PInstance SyntaxInfo FC [t] -- constraints
366 Name -- class
367 [t] -- parameters
368 t -- full instance type
369 (Maybe Name) -- explicit name
370 [PDecl' t]
371 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
372 -- class name, parameters, full instance type, optional explicit name, and definitions
373 | PDSL Name (DSL' t) -- ^ DSL declaration
374 | PSyntax FC Syntax -- ^ Syntax definition
375 | PMutual FC [PDecl' t] -- ^ Mutual block
376 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
377 | PProvider SyntaxInfo FC Name t t -- ^ Type provider. The first t is the type, the second is the term
378 | PReflection FC Name -- type to reflect to
379 t -- type of variables
380 [PClause' t] -- ^ Pattern clauses
381 deriving Functor
382{-!
383deriving instance Binary PDecl'
384!-}
386-- | One clause of a top-level definition. Term arguments to constructors are:
387--
388-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
389--
390-- 2. The list of patterns
391--
392-- 3. The right-hand side
393--
394-- 4. The where block (PDecl' t)
395data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
396 | PWith FC Name t [t] t [PDecl' t]
397 | PClauseR FC [t] t [PDecl' t]
398 | PWithR FC [t] t [PDecl' t]
399 deriving Functor
400{-!
401deriving instance Binary PClause'
402!-}
404-- | Data declaration
405data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
406 d_tcon :: t, -- ^ Type constructor
407 d_cons :: [(String, Name, t, FC)] -- ^ Constructors
408 }
409 -- ^ Data declaration
410 | PLaterdecl { d_name :: Name, d_tcon :: t }
411 -- ^ "Placeholder" for data whose constructors are defined later
412 deriving Functor
413{-!
414deriving instance Binary PData'
415!-}
417-- Handy to get a free function for applying PTerm -> PTerm functions
418-- across a program, by deriving Functor
420type PDecl = PDecl' PTerm
421type PData = PData' PTerm
422type PClause = PClause' PTerm
424-- get all the names declared in a decl
426declared :: PDecl -> [Name]
427declared (PFix _ _ _) = []
428declared (PTy _ _ _ _ n t) = [n]
429declared (PPostulate _ _ _ _ n t) = [n]
430declared (PClauses _ _ n _) = [] -- not a declaration
431declared (PCAF _ n _) = [n]
432declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
433 where fstt (_, a, _, _) = a
434declared (PData _ _ _ _ (PLaterdecl n _)) = [n]
435declared (PParams _ _ ds) = concatMap declared ds
436declared (PNamespace _ ds) = concatMap declared ds
437declared (PRecord _ _ _ n _ _ c _) = [n, c]
438declared (PClass _ _ _ _ n _ ms) = n : concatMap declared ms
439declared (PInstance _ _ _ _ _ _ _ _) = []
440declared (PDSL n _) = [n]
441declared (PSyntax _ _) = []
442declared (PMutual _ ds) = concatMap declared ds
443declared (PDirective _) = []
445-- get the names declared, not counting nested parameter blocks
446tldeclared :: PDecl -> [Name]
447tldeclared (PFix _ _ _) = []
448tldeclared (PTy _ _ _ _ n t) = [n]
449tldeclared (PPostulate _ _ _ _ n t) = [n]
450tldeclared (PClauses _ _ n _) = [] -- not a declaration
451tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]
452tldeclared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
453 where fstt (_, a, _, _) = a
454tldeclared (PParams _ _ ds) = []
455tldeclared (PMutual _ ds) = concatMap tldeclared ds
456tldeclared (PNamespace _ ds) = concatMap tldeclared ds
459defined :: PDecl -> [Name]
460defined (PFix _ _ _) = []
461defined (PTy _ _ _ _ n t) = []
462defined (PPostulate _ _ _ _ n t) = []
463defined (PClauses _ _ n _) = [n] -- not a declaration
464defined (PCAF _ n _) = [n]
465defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
466 where fstt (_, a, _, _) = a
467defined (PData _ _ _ _ (PLaterdecl n _)) = []
468defined (PParams _ _ ds) = concatMap defined ds
469defined (PNamespace _ ds) = concatMap defined ds
470defined (PRecord _ _ _ n _ _ c _) = [n, c]
471defined (PClass _ _ _ _ n _ ms) = n : concatMap defined ms
472defined (PInstance _ _ _ _ _ _ _ _) = []
473defined (PDSL n _) = [n]
474defined (PSyntax _ _) = []
475defined (PMutual _ ds) = concatMap defined ds
476defined (PDirective _) = []
477--defined _ = []
479updateN :: [(Name, Name)] -> Name -> Name
480updateN ns n | Just n' <- lookup n ns = n'
481updateN _ n = n
483updateNs :: [(Name, Name)] -> PTerm -> PTerm
484updateNs [] t = t
485updateNs ns t = mapPT updateRef t
486 where updateRef (PRef fc f) = PRef fc (updateN ns f)
487 updateRef t = t
489-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
490-- updateDNs [] t = t
491-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
492-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
493-- where updateCNs ns (PClause n l ts r ds)
494-- = PClause (updateN ns n) (fmap (updateNs ns) l)
495-- (map (fmap (updateNs ns)) ts)
496-- (fmap (updateNs ns) r)
497-- (map (updateDNs ns) ds)
498-- updateDNs ns c = c
500-- | High level language terms
501data PTerm = PQuote Raw
502 | PRef FC Name
503 | PInferRef FC Name -- ^ A name to be defined later
504 | PPatvar FC Name
505 | PLam Name PTerm PTerm
506 | PPi Plicity Name PTerm PTerm
507 | PLet Name PTerm PTerm PTerm
508 | PTyped PTerm PTerm -- ^ Term with explicit type
509 | PApp FC PTerm [PArg]
510 | PMatchApp FC Name -- ^ Make an application by type matching
511 | PCase FC PTerm [(PTerm, PTerm)]
512 | PTrue FC
513 | PFalse FC
514 | PRefl FC PTerm
515 | PResolveTC FC
516 | PEq FC PTerm PTerm
517 | PRewrite FC PTerm PTerm (Maybe PTerm)
518 | PPair FC PTerm PTerm
519 | PDPair FC PTerm PTerm PTerm
520 | PAlternative Bool [PTerm] -- True if only one may work
521 | PHidden PTerm -- ^ Irrelevant or hidden pattern
522 | PType
523 | PConstant Const
524 | Placeholder
525 | PDoBlock [PDo]
526 | PIdiom FC PTerm
527 | PReturn FC
528 | PMetavar Name
529 | PProof [PTactic] -- ^ Proof script
530 | PTactics [PTactic] -- ^ As PProof, but no auto solving
531 | PElabError Err -- ^ Error to report on elaboration
532 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
533 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
534 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
535 deriving Eq
536{-!
537deriving instance Binary PTerm
538!-}
540mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
541mapPT f t = f (mpt t) where
542 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
543 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
544 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
545 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
546 (fmap (mapPT f) g)
547 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
548 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
549 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
550 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
551 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
552 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
553 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
554 mpt (PHidden t) = PHidden (mapPT f t)
555 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
556 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
557 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
558 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
559 mpt x = x
562data PTactic' t = Intro [Name] | Intros | Focus Name
563 | Refine Name [Bool] | Rewrite t
564 | Equiv t
565 | MatchRefine Name
566 | LetTac Name t | LetTacTy Name t t
567 | Exact t | Compute | Trivial
568 | Solve
569 | Attack
570 | ProofState | ProofTerm | Undo
571 | Try (PTactic' t) (PTactic' t)
572 | TSeq (PTactic' t) (PTactic' t)
573 | ApplyTactic t -- see Language.Reflection module
574 | Reflect t
575 | Fill t
576 | GoalType String (PTactic' t)
577 | Qed | Abandon
578 deriving (Show, Eq, Functor)
579{-!
580deriving instance Binary PTactic'
581!-}
583instance Sized a => Sized (PTactic' a) where
584 size (Intro nms) = 1 + size nms
585 size Intros = 1
586 size (Focus nm) = 1 + size nm
587 size (Refine nm bs) = 1 + size nm + length bs
588 size (Rewrite t) = 1 + size t
589 size (LetTac nm t) = 1 + size nm + size t
590 size (Exact t) = 1 + size t
591 size Compute = 1
592 size Trivial = 1
593 size Solve = 1
594 size Attack = 1
595 size ProofState = 1
596 size ProofTerm = 1
597 size Undo = 1
598 size (Try l r) = 1 + size l + size r
599 size (TSeq l r) = 1 + size l + size r
600 size (ApplyTactic t) = 1 + size t
601 size (Reflect t) = 1 + size t
602 size (Fill t) = 1 + size t
603 size Qed = 1
604 size Abandon = 1
606type PTactic = PTactic' PTerm
608data PDo' t = DoExp FC t
609 | DoBind FC Name t
610 | DoBindP FC t t
611 | DoLet FC Name t t
612 | DoLetP FC t t
613 deriving (Eq, Functor)
614{-!
615deriving instance Binary PDo'
616!-}
618instance Sized a => Sized (PDo' a) where
619 size (DoExp fc t) = 1 + size fc + size t
620 size (DoBind fc nm t) = 1 + size fc + size nm + size t
621 size (DoBindP fc l r) = 1 + size fc + size l + size r
622 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
623 size (DoLetP fc l r) = 1 + size fc + size l + size r
625type PDo = PDo' PTerm
627-- The priority gives a hint as to elaboration order. Best to elaborate
628-- things early which will help give a more concrete type to other
629-- variables, e.g. a before (interpTy a).
630-- TODO: priority no longer serves any purpose, drop it!
632data PArg' t = PImp { priority :: Int,
633 lazyarg :: Bool, pname :: Name, getTm :: t,
634 pargdoc :: String }
635 | PExp { priority :: Int,
636 lazyarg :: Bool, getTm :: t,
637 pargdoc :: String }
638 | PConstraint { priority :: Int,
639 lazyarg :: Bool, getTm :: t,
640 pargdoc :: String }
641 | PTacImplicit { priority :: Int,
642 lazyarg :: Bool, pname :: Name,
643 getScript :: t,
644 getTm :: t,
645 pargdoc :: String }
646 deriving (Show, Eq, Functor)
648instance Sized a => Sized (PArg' a) where
649 size (PImp p l nm trm _) = 1 + size nm + size trm
650 size (PExp p l trm _) = 1 + size trm
651 size (PConstraint p l trm _) = 1 + size trm
652 size (PTacImplicit p l nm scr trm _) = 1 + size nm + size scr + size trm
654{-!
655deriving instance Binary PArg'
656!-}
658pimp n t = PImp 0 True n t ""
659pexp t = PExp 0 False t ""
660pconst t = PConstraint 0 False t ""
661ptacimp n s t = PTacImplicit 0 True n s t ""
663type PArg = PArg' PTerm
665-- Type class data
667data ClassInfo = CI { instanceName :: Name,
668 class_methods :: [(Name, (FnOpts, PTerm))],
669 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
670 class_params :: [Name],
671 class_instances :: [Name] }
672 deriving Show
673{-!
674deriving instance Binary ClassInfo
675!-}
677data OptInfo = Optimise { collapsible :: Bool,
678 forceable :: [Int], -- argument positions
679 recursive :: [Int] }
680 deriving Show
681{-!
682deriving instance Binary OptInfo
683!-}
686data TypeInfo = TI { con_names :: [Name],
687 codata :: Bool,
688 param_pos :: [Int] }
689 deriving Show
690{-!
691deriving instance Binary TypeInfo
692!-}
694-- Syntactic sugar info
696data DSL' t = DSL { dsl_bind :: t,
697 dsl_return :: t,
698 dsl_apply :: t,
699 dsl_pure :: t,
700 dsl_var :: Maybe t,
701 index_first :: Maybe t,
702 index_next :: Maybe t,
703 dsl_lambda :: Maybe t,
704 dsl_let :: Maybe t
705 }
706 deriving (Show, Functor)
707{-!
708deriving instance Binary DSL'
709!-}
711type DSL = DSL' PTerm
713data SynContext = PatternSyntax | TermSyntax | AnySyntax
714 deriving Show
715{-!
716deriving instance Binary SynContext
717!-}
719data Syntax = Rule [SSymbol] PTerm SynContext
720 deriving Show
721{-!
722deriving instance Binary Syntax
723!-}
725data SSymbol = Keyword Name
726 | Symbol String
727 | Binding Name
728 | Expr Name
729 | SimpleExpr Name
730 deriving Show
731{-!
732deriving instance Binary SSymbol
733!-}
735initDSL = DSL (PRef f (UN ">>="))
736 (PRef f (UN "return"))
737 (PRef f (UN "<$>"))
738 (PRef f (UN "pure"))
739 Nothing
740 Nothing
741 Nothing
742 Nothing
743 Nothing
744 where f = FC "(builtin)" 0
746data Using = UImplicit Name PTerm
747 | UConstraint Name [Name]
748 deriving (Show, Eq)
749{-!
750deriving instance Binary Using
751!-}
753data SyntaxInfo = Syn { using :: [Using],
754 syn_params :: [(Name, PTerm)],
755 syn_namespace :: [String],
756 no_imp :: [Name],
757 decoration :: Name -> Name,
758 inPattern :: Bool,
759 implicitAllowed :: Bool,
760 dsl_info :: DSL }
761 deriving Show
762{-!
763deriving instance Binary SyntaxInfo
764!-}
766defaultSyntax = Syn [] [] [] [] id False False initDSL
768expandNS :: SyntaxInfo -> Name -> Name
769expandNS syn n@(NS _ _) = n
770expandNS syn n = case syn_namespace syn of
771 [] -> n
772 xs -> NS n xs
775--- Pretty printing declarations and terms
777instance Show PTerm where
778 show tm = showImp False tm
780instance Pretty PTerm where
781 pretty = prettyImp False
783instance Show PDecl where
784 show d = showDeclImp False d
786instance Show PClause where
787 show c = showCImp True c
789instance Show PData where
790 show d = showDImp False d
792showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
793showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty
794showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty
795showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
796showDeclImp _ (PData _ _ _ _ d) = show d
797showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++
798 showSep "\n" (map show ps)
801showCImp :: Bool -> PClause -> String
802showCImp impl (PClause _ n l ws r w)
803 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
804 ++ " where " ++ show w
805 where
806 showWs [] = ""
807 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
808showCImp impl (PWith _ n l ws r w)
809 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
810 ++ " { " ++ show w ++ " } "
811 where
812 showWs [] = ""
813 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
816showDImp :: Bool -> PData -> String
817showDImp impl (PDatadecl n ty cons)
818 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
819 ++ showSep "\n\t| "
820 (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
822getImps :: [PArg] -> [(Name, PTerm)]
823getImps [] = []
824getImps (PImp _ _ n tm _ : xs) = (n, tm) : getImps xs
825getImps (_ : xs) = getImps xs
827getExps :: [PArg] -> [PTerm]
828getExps [] = []
829getExps (PExp _ _ tm _ : xs) = tm : getExps xs
830getExps (_ : xs) = getExps xs
832getConsts :: [PArg] -> [PTerm]
833getConsts [] = []
834getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs
835getConsts (_ : xs) = getConsts xs
837getAll :: [PArg] -> [PTerm]
838getAll = map getTm
840prettyImp :: Bool -> PTerm -> Doc
841prettyImp impl = prettySe 10
842 where
843 prettySe p (PQuote r) =
844 if size r > breakingSize then
845 text "![" $$ pretty r <> text "]"
846 else
847 text "![" <> pretty r <> text "]"
848 prettySe p (PPatvar fc n) = pretty n
849 prettySe p (PRef fc n) =
850 if impl then
851 pretty n
852 else
853 prettyBasic n
854 where
855 prettyBasic n@(UN _) = pretty n
856 prettyBasic (MN _ s) = text s
857 prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
858 prettySe p (PLam n ty sc) =
859 bracket p 2 $
860 if size sc > breakingSize then
861 text "λ" <> pretty n <+> text "=>" $+$ pretty sc
862 else
863 text "λ" <> pretty n <+> text "=>" <+> pretty sc
864 prettySe p (PLet n ty v sc) =
865 bracket p 2 $
866 if size sc > breakingSize then
867 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
868 nest nestingSize (prettySe 10 sc)
869 else
870 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
871 prettySe 10 sc
872 prettySe p (PPi (Exp l s _) n ty sc)
873 | n `elem` allNamesIn sc || impl =
874 let open = if l then text "|" <> lparen else lparen in
875 bracket p 2 $
876 if size sc > breakingSize then
877 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
878 st <+> text "->" $+$ prettySe 10 sc
879 else
880 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
881 st <+> text "->" <+> prettySe 10 sc
882 | otherwise =
883 bracket p 2 $
884 if size sc > breakingSize then
885 prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
886 else
887 prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
888 where
889 st =
890 case s of
891 Static -> text "[static]"
892 _ -> empty
893 prettySe p (PPi (Imp l s _) n ty sc)
894 | impl =
895 let open = if l then text "|" <> lbrace else lbrace in
896 bracket p 2 $
897 if size sc > breakingSize then
898 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
899 st <+> text "->" <+> prettySe 10 sc
900 else
901 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
902 st <+> text "->" <+> prettySe 10 sc
903 | otherwise = prettySe 10 sc
904 where
905 st =
906 case s of
907 Static -> text $ "[static]"
908 _ -> empty
909 prettySe p (PPi (Constraint _ _ _) n ty sc) =
910 bracket p 2 $
911 if size sc > breakingSize then
912 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
913 else
914 prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
915 prettySe p (PPi (TacImp _ _ s _) n ty sc) =
916 bracket p 2 $
917 if size sc > breakingSize then
918 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
919 rbrace <+> text "->" $+$ prettySe 10 sc
920 else
921 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
922 rbrace <+> text "->" <+> prettySe 10 sc
923 prettySe p (PApp _ (PRef _ f) [])
924 | not impl = pretty f
925 prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
926 | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
927 let [l, r] = getExps args in
928 bracket p 1 $
929 if size r > breakingSize then
930 prettySe 1 l <+> pretty op $+$ prettySe 0 r
931 else
932 prettySe 1 l <+> pretty op <+> prettySe 0 r
933 prettySe p (PApp _ f as) =
934 let args = getExps as in
935 bracket p 1 $
936 prettySe 1 f <+>
937 if impl then
938 foldl' fS empty as
939 -- foldr (<+>) empty $ map prettyArgS as
940 else
941 foldl' fSe empty args
942 -- foldr (<+>) empty $ map prettyArgSe args
943 where
944 fS l r =
945 if size r > breakingSize then
946 l $+$ nest nestingSize (prettyArgS r)
947 else
948 l <+> prettyArgS r
950 fSe l r =
951 if size r > breakingSize then
952 l $+$ nest nestingSize (prettyArgSe r)
953 else
954 l <+> prettyArgSe r
955 prettySe p (PCase _ scr opts) =
956 text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
957 where
958 prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
960 sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
961 prettySe p (PHidden tm) = text "." <> prettySe 0 tm
962 prettySe p (PRefl _ _) = text "refl"
963 prettySe p (PResolveTC _) = text "resolvetc"
964 prettySe p (PTrue _) = text "()"
965 prettySe p (PFalse _) = text "_|_"
966 prettySe p (PEq _ l r) =
967 bracket p 2 $
968 if size r > breakingSize then
969 prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
970 else
971 prettySe 10 l <+> text "=" <+> prettySe 10 r
972 prettySe p (PRewrite _ l r _) =
973 bracket p 2 $
974 if size r > breakingSize then
975 text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)
976 else
977 text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r
978 prettySe p (PTyped l r) =
979 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
980 prettySe p (PPair _ l r) =
981 if size r > breakingSize then
982 lparen <> prettySe 10 l <> text "," $+$
983 prettySe 10 r <> rparen
984 else
985 lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
986 prettySe p (PDPair _ l t r) =
987 if size r > breakingSize then
988 lparen <> prettySe 10 l <+> text "**" $+$
989 prettySe 10 r <> rparen
990 else
991 lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
992 prettySe p (PAlternative a as) =
993 lparen <> text "|" <> prettyAs <> text "|" <> rparen
994 where
995 prettyAs =
996 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
997 prettySe p PType = text "Type"
998 prettySe p (PConstant c) = pretty c
999 -- XXX: add pretty for tactics
1000 prettySe p (PProof ts) =
1001 text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1002 prettySe p (PTactics ts) =
1003 text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1004 prettySe p (PMetavar n) = text "?" <> pretty n
1005 prettySe p (PReturn f) = text "return"
1006 prettySe p PImpossible = text "impossible"
1007 prettySe p Placeholder = text "_"
1008 prettySe p (PDoBlock _) = text "do block pretty not implemented"
1009 prettySe p (PElabError s) = pretty s
1011 prettySe p _ = text "test"
1013 prettyArgS (PImp _ _ n tm _) = prettyArgSi (n, tm)
1014 prettyArgS (PExp _ _ tm _) = prettyArgSe tm
1015 prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm
1016 prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)
1018 prettyArgSe arg = prettySe 0 arg
1019 prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1020 prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
1021 prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1023 bracket outer inner doc
1024 | inner > outer = lparen <> doc <> rparen
1025 | otherwise = doc
1027showImp :: Bool -> PTerm -> String
1028showImp impl tm = se 10 tm where
1029 se p (PQuote r) = "![" ++ show r ++ "]"
1030 se p (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1031 se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1032 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
1033 else showbasic n
1034 where showbasic n@(UN _) = show n
1035 showbasic (MN _ s) = s
1036 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1037 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
1038 (if impl then " : " ++ se 10 ty else "") ++ " => "
1039 ++ se 10 sc
1040 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
1041 " in " ++ se 10 sc
1042 se p (PPi (Exp l s _) n ty sc)
1043 | n `elem` allNamesIn sc || impl
1044 = bracket p 2 $
1045 (if l then "|(" else "(") ++
1046 show n ++ " : " ++ se 10 ty ++
1047 ") " ++ st ++
1048 "-> " ++ se 10 sc
1049 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
1050 where st = case s of
1051 Static -> "[static] "
1052 _ -> ""
1053 se p (PPi (Imp l s _) n ty sc)
1054 | impl = bracket p 2 $ (if l then "|{" else "{") ++
1055 show n ++ " : " ++ se 10 ty ++
1056 "} " ++ st ++ "-> " ++ se 10 sc
1057 | otherwise = se 10 sc
1058 where st = case s of
1059 Static -> "[static] "
1060 _ -> ""
1061 se p (PPi (Constraint _ _ _) n ty sc)
1062 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1063 se p (PPi (TacImp _ _ s _) n ty sc)
1064 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1065 se p e
1066 | Just str <- slist p e = str
1067 | Just num <- snat p e = show num
1068 se p (PMatchApp _ f) = "match " ++ show f
1069 se p (PApp _ (PRef _ f) [])
1070 | not impl = show f
1071 se p (PApp _ (PRef _ op@(UN (f:_))) args)
1072 | length (getExps args) == 2 && not impl && not (isAlpha f)
1073 = let [l, r] = getExps args in
1074 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
1075 se p (PApp _ f as)
1076 = let args = getExps as in
1077 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
1078 else concatMap seArg args
1079 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
1080 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
1081 se p (PHidden tm) = "." ++ se 0 tm
1082 se p (PRefl _ t)
1083 | not impl = "refl"
1084 | otherwise = "refl {" ++ se 10 t ++ "}"
1085 se p (PResolveTC _) = "resolvetc"
1086 se p (PTrue _) = "()"
1087 se p (PFalse _) = "_|_"
1088 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
1089 se p (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 l ++ " in " ++ se 10 r
1090 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
1091 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
1092 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
1093 se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
1094 se p PType = "Type"
1095 se p (PConstant c) = show c
1096 se p (PProof ts) = "proof { " ++ show ts ++ "}"
1097 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
1098 se p (PMetavar n) = "?" ++ show n
1099 se p (PReturn f) = "return"
1100 se p PImpossible = "impossible"
1101 se p Placeholder = "_"
1102 se p (PDoBlock _) = "do block show not implemented"
1103 se p (PElabError s) = show s
1104 se p (PCoerced t) = se p t
1105 se p (PUnifyLog t) = "%unifyLog " ++ se p t
1106-- se p x = "Not implemented"
1108 slist' p (PApp _ (PRef _ nil) _)
1109 | nsroot nil == UN "Nil" = Just []
1110 slist' p (PApp _ (PRef _ cons) args)
1111 | nsroot cons == UN "::",
1112 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1113 all isImp imps,
1114 Just tl' <- slist' p tl
1115 = Just (hd:tl')
1116 where
1117 isImp (PImp {}) = True
1118 isImp _ = False
1119 slist' _ _ = Nothing
1121 slist p e | Just es <- slist' p e = Just $
1122 case es of [] -> "[]"
1123 [x] -> "[" ++ se p x ++ "]"
1124 xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
1125 slist _ _ = Nothing
1127 -- since Prelude is always imported, S & O are unqualified iff they're the
1128 -- Nat ones.
1129 snat p (PRef _ o)
1130 | show o == (natns++"O") || show o == "O" = Just 0
1131 snat p (PApp _ s [PExp {getTm=n}])
1132 | show s == (natns++"S") || show s == "S",
1133 Just n' <- snat p n
1134 = Just $ 1 + n'
1135 snat _ _ = Nothing
1137 natns = "Prelude.Nat."
1139 sArg (PImp _ _ n tm _) = siArg (n, tm)
1140 sArg (PExp _ _ tm _) = seArg tm
1141 sArg (PConstraint _ _ tm _) = scArg tm
1142 sArg (PTacImplicit _ _ n _ tm _) = stiArg (n, tm)
1144 seArg arg = " " ++ se 0 arg
1145 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
1146 scArg val = " {{" ++ se 10 val ++ "}}"
1147 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
1149 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1150 | otherwise = str
1153instance Sized PTerm where
1154 size (PQuote rawTerm) = size rawTerm
1155 size (PRef fc name) = size name
1156 size (PLam name ty bdy) = 1 + size ty + size bdy
1157 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1158 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1159 size (PTyped trm ty) = 1 + size trm + size ty
1160 size (PApp fc name args) = 1 + size args
1161 size (PCase fc trm bdy) = 1 + size trm + size bdy
1162 size (PTrue fc) = 1
1163 size (PFalse fc) = 1
1164 size (PRefl fc _) = 1
1165 size (PResolveTC fc) = 1
1166 size (PEq fc left right) = 1 + size left + size right
1167 size (PRewrite fc left right _) = 1 + size left + size right
1168 size (PPair fc left right) = 1 + size left + size right
1169 size (PDPair fs left ty right) = 1 + size left + size ty + size right
1170 size (PAlternative a alts) = 1 + size alts
1171 size (PHidden hidden) = size hidden
1172 size (PUnifyLog tm) = size tm
1173 size PType = 1
1174 size (PConstant const) = 1 + size const
1175 size Placeholder = 1
1176 size (PDoBlock dos) = 1 + size dos
1177 size (PIdiom fc term) = 1 + size term
1178 size (PReturn fc) = 1
1179 size (PMetavar name) = 1
1180 size (PProof tactics) = size tactics
1181 size (PElabError err) = size err
1182 size PImpossible = 1
1184getPArity :: PTerm -> Int
1185getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1186getPArity _ = 0
1188-- Return all names, free or globally bound, in the given term.
1190allNamesIn :: PTerm -> [Name]
1191allNamesIn tm = nub $ ni [] tm
1192 where
1193 ni env (PRef _ n)
1194 | not (n `elem` env) = [n]
1195 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1196 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1197 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1198 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1199 ni env (PHidden tm) = ni env tm
1200 ni env (PEq _ l r) = ni env l ++ ni env r
1201 ni env (PRewrite _ 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 ls) = concatMap (ni env) ls
1207 ni env (PUnifyLog tm) = ni env tm
1208 ni env _ = []
1210-- Return names which are free in the given term.
1212namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1213namesIn uvars ist tm = nub $ ni [] tm
1214 where
1215 ni env (PRef _ n)
1216 | not (n `elem` env)
1217 = case lookupTy n (tt_ctxt ist) of
1218 [] -> [n]
1219 _ -> if n `elem` (map fst uvars) then [n] else []
1220 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1221 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1222 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1223 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1224 ni env (PEq _ l r) = ni env l ++ ni env r
1225 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1226 ni env (PTyped l r) = ni env l ++ ni env r
1227 ni env (PPair _ l r) = ni env l ++ ni env r
1228 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1229 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1230 ni env (PAlternative a as) = concatMap (ni env) as
1231 ni env (PHidden tm) = ni env tm
1232 ni env (PUnifyLog tm) = ni env tm
1233 ni env _ = []
1235-- Return which of the given names are used in the given term.
1237usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1238usedNamesIn vars ist tm = nub $ ni [] tm
1239 where
1240 ni env (PRef _ n)
1241 | n `elem` vars && not (n `elem` env)
1242 = case lookupTy n (tt_ctxt ist) of
1243 [] -> [n]
1244 _ -> []
1245 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1246 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1247 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1248 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1249 ni env (PEq _ l r) = ni env l ++ ni env r
1250 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1251 ni env (PTyped l r) = ni env l ++ ni env r
1252 ni env (PPair _ l r) = ni env l ++ ni env r
1253 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1254 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1255 ni env (PAlternative a as) = concatMap (ni env) as
1256 ni env (PHidden tm) = ni env tm
1257 ni env (PUnifyLog tm) = ni env tm
1258 ni env _ = []