git.iko.soy/Idris-dev
on 42dcbab help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1576 lines 60 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate
9import Core.Typecheck
11import System.Console.Haskeline
13import Control.Monad.State
15import Data.List
16import Data.Char
17import Data.Either
19import Debug.Trace
21import qualified Epic.Epic as E
23import Util.Pretty
25data IOption = IOption { opt_logLevel :: Int,
26 opt_typecase :: Bool,
27 opt_typeintype :: Bool,
28 opt_coverage :: Bool,
29 opt_showimp :: Bool,
30 opt_repl :: Bool,
31 opt_verbose :: Bool
32 }
33 deriving (Show, Eq)
35defaultOpts = IOption 0 False False True False True True
37-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
38-- without typechecking).
39-- This will include all the functions and data declarations, plus fixity declarations
40-- and syntax macros.
42data IState = IState { tt_ctxt :: Context,
43 idris_constraints :: [(UConstraint, FC)],
44 idris_infixes :: [FixDecl],
45 idris_implicits :: Ctxt [PArg],
46 idris_statics :: Ctxt [Bool],
47 idris_classes :: Ctxt ClassInfo,
48 idris_dsls :: Ctxt DSL,
49 idris_optimisation :: Ctxt OptInfo,
50 idris_datatypes :: Ctxt TypeInfo,
51 idris_patdefs :: Ctxt [(Term, Term)], -- not exported
52 idris_flags :: Ctxt [FnOpt],
53 idris_callgraph :: Ctxt [Name],
54 idris_totcheck :: [(FC, Name)],
55 idris_log :: String,
56 idris_options :: IOption,
57 idris_name :: Int,
58 idris_metavars :: [Name],
59 syntax_rules :: [Syntax],
60 syntax_keywords :: [String],
61 imported :: [FilePath],
62 idris_prims :: [(Name, ([E.Name], E.Term))],
63 idris_objs :: [FilePath],
64 idris_libs :: [String],
65 idris_hdrs :: [String],
66 last_proof :: Maybe (Name, [String]),
67 errLine :: Maybe Int,
68 lastParse :: Maybe Name,
69 indent_stack :: [Int],
70 brace_stack :: [Maybe Int],
71 hide_list :: [(Name, Maybe Accessibility)],
72 default_access :: Accessibility,
73 ibc_write :: [IBCWrite],
74 compiled_so :: Maybe String
75 }
77-- information that needs writing for the current module's .ibc file
78data IBCWrite = IBCFix FixDecl
79 | IBCImp Name
80 | IBCStatic Name
81 | IBCClass Name
82 | IBCInstance Bool Name Name
83 | IBCDSL Name
84 | IBCData Name
85 | IBCOpt Name
86 | IBCSyntax Syntax
87 | IBCKeyword String
88 | IBCImport FilePath
89 | IBCObj FilePath
90 | IBCLib String
91 | IBCHeader String
92 | IBCAccess Name Accessibility
93 | IBCTotal Name Totality
94 | IBCFlags Name [FnOpt]
95 | IBCCG Name
96 | IBCDef Name -- i.e. main context
97 deriving Show
99idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
100 emptyContext emptyContext emptyContext emptyContext
101 emptyContext emptyContext
102 [] "" defaultOpts 6 [] [] [] [] [] [] [] []
103 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
105-- The monad for the main REPL - reading and processing files and updating
106-- global state (hence the IO inner monad).
107type Idris = StateT IState (InputT IO)
109getContext :: Idris Context
110getContext = do i <- get; return (tt_ctxt i)
112getObjectFiles :: Idris [FilePath]
113getObjectFiles = do i <- get; return (idris_objs i)
115addObjectFile :: FilePath -> Idris ()
116addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
118getLibs :: Idris [String]
119getLibs = do i <- get; return (idris_libs i)
121addLib :: String -> Idris ()
122addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
124addHdr :: String -> Idris ()
125addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
127totcheck :: (FC, Name) -> Idris ()
128totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i })
130setFlags :: Name -> [FnOpt] -> Idris ()
131setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
133setAccessibility :: Name -> Accessibility -> Idris ()
134setAccessibility n a
135 = do i <- get
136 let ctxt = setAccess n a (tt_ctxt i)
137 put (i { tt_ctxt = ctxt })
139setTotality :: Name -> Totality -> Idris ()
140setTotality n a
141 = do i <- get
142 let ctxt = setTotal n a (tt_ctxt i)
143 put (i { tt_ctxt = ctxt })
145getTotality :: Name -> Idris Totality
146getTotality n
147 = do i <- get
148 case lookupTotal n (tt_ctxt i) of
149 [t] -> return t
150 _ -> return (Total [])
152addToCG :: Name -> [Name] -> Idris ()
153addToCG n ns = do i <- get
154 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
156-- Add a class instance function. Dodgy hack: Put integer instances first in the
157-- list so they are resolved by default.
159addInstance :: Bool -> Name -> Name -> Idris ()
160addInstance int n i
161 = do ist <- get
162 case lookupCtxt Nothing n (idris_classes ist) of
163 [CI a b c d ins] ->
164 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
165 put (ist { idris_classes = cs })
166 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
167 put (ist { idris_classes = cs })
168 where addI i ins | int = i : ins
169 | otherwise = ins ++ [i]
171addClass :: Name -> ClassInfo -> Idris ()
172addClass n i
173 = do ist <- get
174 let i' = case lookupCtxt Nothing n (idris_classes ist) of
175 [c] -> c { class_instances = class_instances i }
176 _ -> i
177 put (ist { idris_classes = addDef n i' (idris_classes ist) })
179addIBC :: IBCWrite -> Idris ()
180addIBC ibc@(IBCDef n)
181 = do i <- get
182 when (notDef (ibc_write i)) $
183 put (i { ibc_write = ibc : ibc_write i })
184 where notDef [] = True
185 notDef (IBCDef n': is) | n == n' = False
186 notDef (_ : is) = notDef is
187addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
189clearIBC :: Idris ()
190clearIBC = do i <- get; put (i { ibc_write = [] })
192getHdrs :: Idris [String]
193getHdrs = do i <- get; return (idris_hdrs i)
195setErrLine :: Int -> Idris ()
196setErrLine x = do i <- get;
197 case (errLine i) of
198 Nothing -> put (i { errLine = Just x })
199 Just _ -> return ()
201clearErr :: Idris ()
202clearErr = do i <- get
203 put (i { errLine = Nothing })
205getSO :: Idris (Maybe String)
206getSO = do i <- get
207 return (compiled_so i)
209setSO :: Maybe String -> Idris ()
210setSO s = do i <- get
211 put (i { compiled_so = s })
213getIState :: Idris IState
214getIState = get
216putIState :: IState -> Idris ()
217putIState = put
219getName :: Idris Int
220getName = do i <- get;
221 let idx = idris_name i;
222 put (i { idris_name = idx + 1 })
223 return idx
225checkUndefined :: FC -> Name -> Idris ()
226checkUndefined fc n
227 = do i <- getContext
228 case lookupTy Nothing n i of
229 (_:_) -> fail $ show fc ++ ":" ++
230 show n ++ " already defined"
231 _ -> return ()
233setContext :: Context -> Idris ()
234setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
236updateContext :: (Context -> Context) -> Idris ()
237updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
239addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
240addConstraints fc (v, cs)
241 = do i <- get
242 let ctxt = tt_ctxt i
243 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
244 next_tvar = v }
245 let ics = zip cs (repeat fc) ++ idris_constraints i
246 put (i { tt_ctxt = ctxt', idris_constraints = ics })
248addDeferred :: [(Name, Type)] -> Idris ()
249addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
250 i <- get
251 put (i { idris_metavars = map fst ns ++ idris_metavars i })
252 where tidyNames used (Bind (MN i x) b sc)
253 = let n' = uniqueName (UN x) used in
254 Bind n' b $ tidyNames (n':used) sc
255 tidyNames used (Bind n b sc)
256 = let n' = uniqueName n used in
257 Bind n' b $ tidyNames (n':used) sc
258 tidyNames used b = b
260solveDeferred :: Name -> Idris ()
261solveDeferred n = do i <- get
262 put (i { idris_metavars = idris_metavars i \\ [n] })
264iputStrLn :: String -> Idris ()
265iputStrLn = liftIO . putStrLn
267iWarn :: FC -> String -> Idris ()
268iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
270setLogLevel :: Int -> Idris ()
271setLogLevel l = do i <- get
272 let opts = idris_options i
273 let opt' = opts { opt_logLevel = l }
274 put (i { idris_options = opt' } )
276logLevel :: Idris Int
277logLevel = do i <- get
278 return (opt_logLevel (idris_options i))
280useREPL :: Idris Bool
281useREPL = do i <- get
282 return (opt_repl (idris_options i))
284setREPL :: Bool -> Idris ()
285setREPL t = do i <- get
286 let opts = idris_options i
287 let opt' = opts { opt_repl = t }
288 put (i { idris_options = opt' })
290verbose :: Idris Bool
291verbose = do i <- get
292 return (opt_verbose (idris_options i))
294setVerbose :: Bool -> Idris ()
295setVerbose t = do i <- get
296 let opts = idris_options i
297 let opt' = opts { opt_verbose = t }
298 put (i { idris_options = opt' })
300typeInType :: Idris Bool
301typeInType = do i <- get
302 return (opt_typeintype (idris_options i))
304setTypeInType :: Bool -> Idris ()
305setTypeInType t = do i <- get
306 let opts = idris_options i
307 let opt' = opts { opt_typeintype = t }
308 put (i { idris_options = opt' })
310coverage :: Idris Bool
311coverage = do i <- get
312 return (opt_coverage (idris_options i))
314setCoverage :: Bool -> Idris ()
315setCoverage t = do i <- get
316 let opts = idris_options i
317 let opt' = opts { opt_coverage = t }
318 put (i { idris_options = opt' })
320impShow :: Idris Bool
321impShow = do i <- get
322 return (opt_showimp (idris_options i))
324setImpShow :: Bool -> Idris ()
325setImpShow t = do i <- get
326 let opts = idris_options i
327 let opt' = opts { opt_showimp = t }
328 put (i { idris_options = opt' })
330logLvl :: Int -> String -> Idris ()
331logLvl l str = do i <- get
332 let lvl = opt_logLevel (idris_options i)
333 when (lvl >= l)
334 $ do liftIO (putStrLn str)
335 put (i { idris_log = idris_log i ++ str ++ "\n" } )
337iLOG :: String -> Idris ()
338iLOG = logLvl 1
340noErrors :: Idris Bool
341noErrors = do i <- get
342 case errLine i of
343 Nothing -> return True
344 _ -> return False
346setTypeCase :: Bool -> Idris ()
347setTypeCase t = do i <- get
348 let opts = idris_options i
349 let opt' = opts { opt_typecase = t }
350 put (i { idris_options = opt' })
352-- Commands in the REPL
354data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
355 | Reload | Edit
356 | Compile String | Execute | ExecVal PTerm
357 | Metavars | Prove Name | AddProof | Universes
358 | TTShell
359 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name | Info Name
360 | NOP
362-- Parsed declarations
364data Fixity = Infixl { prec :: Int }
365 | Infixr { prec :: Int }
366 | InfixN { prec :: Int }
367 | PrefixN { prec :: Int }
368 deriving Eq
369{-!
370deriving instance Binary Fixity
371!-}
373instance Show Fixity where
374 show (Infixl i) = "infixl " ++ show i
375 show (Infixr i) = "infixr " ++ show i
376 show (InfixN i) = "infix " ++ show i
377 show (PrefixN i) = "prefix " ++ show i
379data FixDecl = Fix Fixity String
380 deriving (Show, Eq)
381{-!
382deriving instance Binary FixDecl
383!-}
385instance Ord FixDecl where
386 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
389data Static = Static | Dynamic
390 deriving (Show, Eq)
391{-!
392deriving instance Binary Static
393!-}
395-- Mark bindings with their explicitness, and laziness
396data Plicity = Imp { plazy :: Bool,
397 pstatic :: Static }
398 | Exp { plazy :: Bool,
399 pstatic :: Static }
400 | Constraint { plazy :: Bool,
401 pstatic :: Static }
402 | TacImp { plazy :: Bool,
403 pstatic :: Static,
404 pscript :: PTerm }
405 deriving (Show, Eq)
407{-!
408deriving instance Binary Plicity
409!-}
411impl = Imp False Dynamic
412expl = Exp False Dynamic
413constraint = Constraint False Dynamic
414tacimpl = TacImp False Dynamic
416data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
417 | Specialise [Name] -- specialise it, freeze these names
418 deriving (Show, Eq)
419{-!
420deriving instance Binary FnOpt
421!-}
423type FnOpts = [FnOpt]
425inlinable :: FnOpts -> Bool
426inlinable = elem Inlinable
428data PDecl' t = PFix FC Fixity [String] -- fixity declaration
429 | PTy SyntaxInfo FC FnOpts Name t -- type declaration
430 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
431 | PData SyntaxInfo FC (PData' t) -- data declaration
432 | PParams FC [(Name, t)] [PDecl' t] -- params block
433 | PNamespace String [PDecl' t] -- new namespace
434 | PRecord SyntaxInfo FC Name t Name t -- record declaration
435 | PClass SyntaxInfo FC
436 [t] -- constraints
437 Name
438 [(Name, t)] -- parameters
439 [PDecl' t] -- declarations
440 | PInstance SyntaxInfo FC [t] -- constraints
441 Name -- class
442 [t] -- parameters
443 t -- full instance type
444 [PDecl' t]
445 | PDSL Name (DSL' t)
446 | PSyntax FC Syntax
447 | PDirective (Idris ())
448 deriving Functor
450data PClause' t = PClause FC Name t [t] t [PDecl' t]
451 | PWith FC Name t [t] t [PDecl' t]
452 | PClauseR FC [t] t [PDecl' t]
453 | PWithR FC [t] t [PDecl' t]
454 deriving Functor
456data PData' t = PDatadecl { d_name :: Name,
457 d_tcon :: t,
458 d_cons :: [(Name, t, FC)] }
459 deriving Functor
461-- Handy to get a free function for applying PTerm -> PTerm functions
462-- across a program, by deriving Functor
464type PDecl = PDecl' PTerm
465type PData = PData' PTerm
466type PClause = PClause' PTerm
468-- get all the names declared in a decl
470declared :: PDecl -> [Name]
471declared (PFix _ _ _) = []
472declared (PTy _ _ _ n t) = [n]
473declared (PClauses _ _ n _) = [] -- not a declaration
474declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
475 where fstt (a, _, _) = a
476declared (PParams _ _ ds) = concatMap declared ds
477declared (PNamespace _ ds) = concatMap declared ds
478-- declared (PImport _) = []
480defined :: PDecl -> [Name]
481defined (PFix _ _ _) = []
482defined (PTy _ _ _ n t) = []
483defined (PClauses _ _ n _) = [n] -- not a declaration
484defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
485 where fstt (a, _, _) = a
486defined (PParams _ _ ds) = concatMap defined ds
487defined (PNamespace _ ds) = concatMap defined ds
488-- declared (PImport _) = []
490updateN :: [(Name, Name)] -> Name -> Name
491updateN ns n | Just n' <- lookup n ns = n'
492updateN _ n = n
494updateNs :: [(Name, Name)] -> PTerm -> PTerm
495updateNs [] t = t
496updateNs ns t = mapPT updateRef t
497 where updateRef (PRef fc f) = PRef fc (updateN ns f)
498 updateRef t = t
500-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
501-- updateDNs [] t = t
502-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
503-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
504-- where updateCNs ns (PClause n l ts r ds)
505-- = PClause (updateN ns n) (fmap (updateNs ns) l)
506-- (map (fmap (updateNs ns)) ts)
507-- (fmap (updateNs ns) r)
508-- (map (updateDNs ns) ds)
509-- updateDNs ns c = c
511-- High level language terms
513data PTerm = PQuote Raw
514 | PRef FC Name
515 | PLam Name PTerm PTerm
516 | PPi Plicity Name PTerm PTerm
517 | PLet Name PTerm PTerm PTerm
518 | PTyped PTerm PTerm -- term with explicit type
519 | PApp FC PTerm [PArg]
520 | PCase FC PTerm [(PTerm, PTerm)]
521 | PTrue FC
522 | PFalse FC
523 | PRefl FC
524 | PResolveTC FC
525 | PEq FC PTerm PTerm
526 | PPair FC PTerm PTerm
527 | PDPair FC PTerm PTerm PTerm
528 | PAlternative [PTerm]
529 | PHidden PTerm -- irrelevant or hidden pattern
530 | PSet
531 | PConstant Const
532 | Placeholder
533 | PDoBlock [PDo]
534 | PIdiom FC PTerm
535 | PReturn FC
536 | PMetavar Name
537 | PProof [PTactic]
538 | PTactics [PTactic] -- as PProof, but no auto solving
539 | PElabError Err -- error to report on elaboration
540 | PImpossible -- special case for declaring when an LHS can't typecheck
541 deriving Eq
542{-!
543deriving instance Binary PTerm
544!-}
546mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
547mapPT f t = f (mpt t) where
548 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
549 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
550 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
551 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
552 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
553 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
554 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
555 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
556 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
557 mpt (PAlternative as) = PAlternative (map (mapPT f) as)
558 mpt (PHidden t) = PHidden (mapPT f t)
559 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
560 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
561 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
562 mpt x = x
565data PTactic' t = Intro [Name] | Intros | Focus Name
566 | Refine Name [Bool] | Rewrite t | LetTac Name 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 | Qed | Abandon
574 deriving (Show, Eq, Functor)
575{-!
576deriving instance Binary PTactic'
577!-}
579type PTactic = PTactic' PTerm
581data PDo' t = DoExp FC t
582 | DoBind FC Name t
583 | DoBindP FC t t
584 | DoLet FC Name t t
585 | DoLetP FC t t
586 deriving (Eq, Functor)
587{-!
588deriving instance Binary PDo'
589!-}
591type PDo = PDo' PTerm
593-- The priority gives a hint as to elaboration order. Best to elaborate
594-- things early which will help give a more concrete type to other
595-- variables, e.g. a before (interpTy a).
597data PArg' t = PImp { priority :: Int,
598 lazyarg :: Bool, pname :: Name, getTm :: t }
599 | PExp { priority :: Int,
600 lazyarg :: Bool, getTm :: t }
601 | PConstraint { priority :: Int,
602 lazyarg :: Bool, getTm :: t }
603 | PTacImplicit { priority :: Int,
604 lazyarg :: Bool, pname :: Name,
605 getScript :: t,
606 getTm :: t }
607 deriving (Show, Eq, Functor)
608{-!
609deriving instance Binary PArg'
610!-}
612pimp = PImp 0 True
613pexp = PExp 0 False
614pconst = PConstraint 0 False
615ptacimp = PTacImplicit 0 True
617type PArg = PArg' PTerm
619-- Type class data
621data ClassInfo = CI { instanceName :: Name,
622 class_methods :: [(Name, (FnOpts, PTerm))],
623 class_defaults :: [(Name, Name)], -- method name -> default impl
624 class_params :: [Name],
625 class_instances :: [Name] }
626 deriving Show
627{-!
628deriving instance Binary ClassInfo
629!-}
631data OptInfo = Optimise { collapsible :: Bool,
632 forceable :: [Int], -- argument positions
633 recursive :: [Int] }
634 deriving Show
635{-!
636deriving instance Binary OptInfo
637!-}
640data TypeInfo = TI { con_names :: [Name] }
641 deriving Show
642{-!
643deriving instance Binary TypeInfo
644!-}
646-- Syntactic sugar info
648data DSL' t = DSL { dsl_bind :: t,
649 dsl_return :: t,
650 dsl_apply :: t,
651 dsl_pure :: t,
652 dsl_var :: Maybe t,
653 index_first :: Maybe t,
654 index_next :: Maybe t,
655 dsl_lambda :: Maybe t,
656 dsl_let :: Maybe t
657 }
658 deriving (Show, Functor)
659{-!
660deriving instance Binary DSL'
661!-}
663type DSL = DSL' PTerm
665data SynContext = PatternSyntax | TermSyntax | AnySyntax
666 deriving Show
667{-!
668deriving instance Binary SynContext
669!-}
671data Syntax = Rule [SSymbol] PTerm SynContext
672 deriving Show
673{-!
674deriving instance Binary Syntax
675!-}
677data SSymbol = Keyword Name
678 | Symbol String
679 | Expr Name
680 | SimpleExpr Name
681 deriving Show
682{-!
683deriving instance Binary SSymbol
684!-}
686initDSL = DSL (PRef f (UN ">>="))
687 (PRef f (UN "return"))
688 (PRef f (UN "<$>"))
689 (PRef f (UN "pure"))
690 Nothing
691 Nothing
692 Nothing
693 Nothing
694 Nothing
695 where f = FC "(builtin)" 0
697data SyntaxInfo = Syn { using :: [(Name, PTerm)],
698 syn_params :: [(Name, PTerm)],
699 syn_namespace :: [String],
700 no_imp :: [Name],
701 decoration :: Name -> Name,
702 inPattern :: Bool,
703 dsl_info :: DSL }
704 deriving Show
706defaultSyntax = Syn [] [] [] [] id False initDSL
708expandNS :: SyntaxInfo -> Name -> Name
709expandNS syn n@(NS _ _) = n
710expandNS syn n = case syn_namespace syn of
711 [] -> n
712 xs -> NS n xs
715--- Pretty printing declarations and terms
717instance Show PTerm where
718 show tm = showImp False tm
720instance Show PDecl where
721 show d = showDeclImp False d
723instance Show PClause where
724 show c = showCImp True c
726instance Show PData where
727 show d = showDImp False d
729showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
730showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty
731showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
732showDeclImp _ (PData _ _ d) = show d
734showCImp :: Bool -> PClause -> String
735showCImp impl (PClause _ n l ws r w)
736 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
737 ++ " where " ++ show w
738 where
739 showWs [] = ""
740 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
741showCImp impl (PWith _ n l ws r w)
742 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
743 ++ " { " ++ show w ++ " } "
744 where
745 showWs [] = ""
746 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
749showDImp :: Bool -> PData -> String
750showDImp impl (PDatadecl n ty cons)
751 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
752 ++ showSep "\n\t| "
753 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
755getImps :: [PArg] -> [(Name, PTerm)]
756getImps [] = []
757getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
758getImps (_ : xs) = getImps xs
760getExps :: [PArg] -> [PTerm]
761getExps [] = []
762getExps (PExp _ _ tm : xs) = tm : getExps xs
763getExps (_ : xs) = getExps xs
765getConsts :: [PArg] -> [PTerm]
766getConsts [] = []
767getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
768getConsts (_ : xs) = getConsts xs
770getAll :: [PArg] -> [PTerm]
771getAll = map getTm
773showImp :: Bool -> PTerm -> String
774showImp impl tm = se 10 tm where
775 se p (PQuote r) = "![" ++ show r ++ "]"
776 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
777 else showbasic n
778 where showbasic n@(UN _) = show n
779 showbasic (MN _ s) = s
780 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
781 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
782 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
783 " in " ++ se 10 sc
784 se p (PPi (Exp l s) n ty sc)
785 | n `elem` allNamesIn sc || impl
786 = bracket p 2 $
787 if l then "|(" else "(" ++
788 show n ++ " : " ++ se 10 ty ++
789 ") " ++ st ++
790 "-> " ++ se 10 sc
791 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
792 where st = case s of
793 Static -> "[static] "
794 _ -> ""
795 se p (PPi (Imp l s) n ty sc)
796 | impl = bracket p 2 $ if l then "|{" else "{" ++
797 show n ++ " : " ++ se 10 ty ++
798 "} " ++ st ++ "-> " ++ se 10 sc
799 | otherwise = se 10 sc
800 where st = case s of
801 Static -> "[static] "
802 _ -> ""
803 se p (PPi (Constraint _ _) n ty sc)
804 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
805 se p (PPi (TacImp _ _ s) n ty sc)
806 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
807 se p (PApp _ (PRef _ f) [])
808 | not impl = show f
809 se p (PApp _ (PRef _ op@(UN (f:_))) args)
810 | length (getExps args) == 2 && not impl && not (isAlpha f)
811 = let [l, r] = getExps args in
812 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
813 se p (PApp _ f as)
814 = let args = getExps as in
815 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
816 else concatMap seArg args
817 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
818 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
819 se p (PHidden tm) = "." ++ se 0 tm
820 se p (PRefl _) = "refl"
821 se p (PResolveTC _) = "resolvetc"
822 se p (PTrue _) = "()"
823 se p (PFalse _) = "_|_"
824 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
825 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
826 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
827 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
828 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
829 se p PSet = "Set"
830 se p (PConstant c) = show c
831 se p (PProof ts) = "proof { " ++ show ts ++ "}"
832 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
833 se p (PMetavar n) = "?" ++ show n
834 se p (PReturn f) = "return"
835 se p PImpossible = "impossible"
836 se p Placeholder = "_"
837 se p (PDoBlock _) = "do block show not implemented"
838 se p (PElabError s) = show s
839-- se p x = "Not implemented"
841 sArg (PImp _ _ n tm) = siArg (n, tm)
842 sArg (PExp _ _ tm) = seArg tm
843 sArg (PConstraint _ _ tm) = scArg tm
844 sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
846 seArg arg = " " ++ se 0 arg
847 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
848 scArg val = " {{" ++ se 10 val ++ "}}"
849 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
851 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
852 | otherwise = str
854{-
855 PQuote Raw
856 | PRef FC Name
857 | PLam Name PTerm PTerm
858 | PPi Plicity Name PTerm PTerm
859 | PLet Name PTerm PTerm PTerm
860 | PTyped PTerm PTerm -- term with explicit type
861 | PApp FC PTerm [PArg]
862 | PCase FC PTerm [(PTerm, PTerm)]
863 | PTrue FC
864 | PFalse FC
865 | PRefl FC
866 | PResolveTC FC
867 | PEq FC PTerm PTerm
868 | PPair FC PTerm PTerm
869 | PDPair FC PTerm PTerm PTerm
870 | PAlternative [PTerm]
871 | PHidden PTerm -- irrelevant or hidden pattern
872 | PSet
873 | PConstant Const
874 | Placeholder
875 | PDoBlock [PDo]
876 | PIdiom FC PTerm
877 | PReturn FC
878 | PMetavar Name
879 | PProof [PTactic]
880 | PTactics [PTactic] -- as PProof, but no auto solving
881 | PElabError Err -- error to report on elaboration
882 | PImpossible -- special case for declaring when an LHS can't typecheck
883-}
885instance Sized PTerm where
886 size (PQuote rawTerm) = size rawTerm
887 size (PRef fc name) = size name
888 size (PLam name ty bdy) = 1 + size ty + size bdy
889 size (PPi name ty bdy) = 1 + size ty + size bdy
890 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
891 size (PTyped trm ty) = 1 + size trm + size ty
892 size (PApp fc name args) = 1 + size args
893 size (PCase fc trm bdy) = 1 + size trm + size bdy
894 size (PTrue fc) = 1
895 size (PFalse fc) = 1
896 size (PRefl fc) = 1
897 size (PResolveTC fc) = 1
898 size (PEq fc left right) = 1 + size left + size right
899 size (PPair fc left right) = 1 + size left + size right
900 size (PDPair fs left right) = 1 + size left + size right
901 size (PAlternative alts) = 1 + size alts
902 size (PHidden hidden) = size hidden
903 size PSet = 1
904 size (PConstant const) = 1 + size const
905 size Placeholder = 1
906 size (PDoBlock dos) = 1 + size dos
907 size (PIdiom fc term) = 1 + size term
908 size (PReturn fc) = 1
909 size (PMetavar name) = 1
910 size (PProof tactics) = size tactics
911 size (PElabError err) = size err
912 size PImpossible = 1
914allNamesIn :: PTerm -> [Name]
915allNamesIn tm = nub $ ni [] tm
916 where
917 ni env (PRef _ n)
918 | not (n `elem` env) = [n]
919 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
920 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
921 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
922 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
923 ni env (PHidden tm) = ni env tm
924 ni env (PEq _ l r) = ni env l ++ ni env r
925 ni env (PTyped l r) = ni env l ++ ni env r
926 ni env (PPair _ l r) = ni env l ++ ni env r
927 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
928 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
929 ni env (PAlternative ls) = concatMap (ni env) ls
930 ni env _ = []
932namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
933namesIn uvars ist tm = nub $ ni [] tm
934 where
935 ni env (PRef _ n)
936 | not (n `elem` env)
937 = case lookupTy Nothing n (tt_ctxt ist) of
938 [] -> [n]
939 _ -> if n `elem` (map fst uvars) then [n] else []
940 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
941 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
942 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
943 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
944 ni env (PEq _ l r) = ni env l ++ ni env r
945 ni env (PTyped l r) = ni env l ++ ni env r
946 ni env (PPair _ l r) = ni env l ++ ni env r
947 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
948 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
949 ni env (PAlternative as) = concatMap (ni env) as
950 ni env (PHidden tm) = ni env tm
951 ni env _ = []
953-- For inferring types of things
955bi = FC "builtin" 0
957inferTy = MN 0 "__Infer"
958inferCon = MN 0 "__infer"
959inferDecl = PDatadecl inferTy
960 PSet
961 [(inferCon, PPi impl (MN 0 "A") PSet (
962 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
963 (PRef bi inferTy)), bi)]
965infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
966infP = P (TCon 6 0) inferTy (Set (UVal 0))
968getInferTerm, getInferType :: Term -> Term
969getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
970getInferTerm (App (App _ _) tm) = tm
971getInferTerm tm = error ("getInferTerm " ++ show tm)
973getInferType (Bind n b sc) = Bind n b $ getInferType sc
974getInferType (App (App _ ty) _) = ty
976-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
978primNames = [unitTy, unitCon,
979 falseTy, pairTy, pairCon,
980 eqTy, eqCon, inferTy, inferCon]
982unitTy = MN 0 "__Unit"
983unitCon = MN 0 "__II"
984unitDecl = PDatadecl unitTy PSet
985 [(unitCon, PRef bi unitTy, bi)]
987falseTy = MN 0 "__False"
988falseDecl = PDatadecl falseTy PSet []
990pairTy = MN 0 "__Pair"
991pairCon = MN 0 "__MkPair"
992pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
993 [(pairCon, PPi impl (n "A") PSet (
994 PPi impl (n "B") PSet (
995 PPi expl (n "a") (PRef bi (n "A")) (
996 PPi expl (n "b") (PRef bi (n "B"))
997 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
998 pexp (PRef bi (n "B"))])))), bi)]
999 where n a = MN 0 a
1001eqTy = UN "="
1002eqCon = UN "refl"
1003eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
1004 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
1005 PSet)
1006 [(eqCon, PPi impl (n "a") PSet (
1007 PPi impl (n "x") (PRef bi (n "a"))
1008 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
1009 pimp (n "b") Placeholder,
1010 pexp (PRef bi (n "x")),
1011 pexp (PRef bi (n "x"))])), bi)]
1012 where n a = MN 0 a
1014-- Defined in builtins.idr
1015sigmaTy = UN "Exists"
1016existsCon = UN "Ex_intro"
1018piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1019piBind [] t = t
1020piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
1022tcname (UN ('@':_)) = True
1023tcname (NS n _) = tcname n
1024tcname _ = False
1026-- Dealing with parameters
1028expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1029expandParams dec ps ns tm = en tm
1030 where
1031 -- if we shadow a name (say in a lambda binding) that is used in a call to
1032 -- a lifted function, we need access to both names - once in the scope of the
1033 -- binding and once to call the lifted functions. So we'll explicitly shadow
1034 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1035 -- but we didn't...)
1037 mkShadow (UN n) = MN 0 n
1038 mkShadow (MN i n) = MN (i+1) n
1039 mkShadow (NS x s) = NS (mkShadow x) s
1041 en (PLam n t s)
1042 | n `elem` map fst ps
1043 = let n' = mkShadow n in
1044 PLam n' (en t) (en (shadow n n' s))
1045 | otherwise = PLam n (en t) (en s)
1046 en (PPi p n t s)
1047 | n `elem` map fst ps
1048 = let n' = mkShadow n in
1049 PPi p n' (en t) (en (shadow n n' s))
1050 | otherwise = PPi p n (en t) (en s)
1051 en (PLet n ty v s)
1052 | n `elem` map fst ps
1053 = let n' = mkShadow n in
1054 PLet n' (en ty) (en v) (en (shadow n n' s))
1055 | otherwise = PLet n (en ty) (en v) (en s)
1056 en (PEq f l r) = PEq f (en l) (en r)
1057 en (PTyped l r) = PTyped (en l) (en r)
1058 en (PPair f l r) = PPair f (en l) (en r)
1059 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
1060 en (PAlternative as) = PAlternative (map en as)
1061 en (PHidden t) = PHidden (en t)
1062 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
1063 en (PProof ts) = PProof (map (fmap en) ts)
1064 en (PTactics ts) = PTactics (map (fmap en) ts)
1066 en (PQuote (Var n))
1067 | n `elem` ns = PQuote (Var (dec n))
1068 en (PApp fc (PRef fc' n) as)
1069 | n `elem` ns = PApp fc (PRef fc' (dec n))
1070 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1071 en (PRef fc n)
1072 | n `elem` ns = PApp fc (PRef fc (dec n))
1073 (map (pexp . (PRef fc)) (map fst ps))
1074 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1075 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1076 en t = t
1078expandParamsD :: IState ->
1079 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1080expandParamsD ist dec ps ns (PTy syn fc o n ty)
1081 = if n `elem` ns
1082 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
1083 else PTy syn fc o n (expandParams dec ps ns ty)
1084expandParamsD ist dec ps ns (PClauses fc opts n cs)
1085 = let n' = if n `elem` ns then dec n else n in
1086 PClauses fc opts n' (map expandParamsC cs)
1087 where
1088 expandParamsC (PClause fc n lhs ws rhs ds)
1089 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1090 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1091 n' = if n `elem` ns then dec n else n in
1092 PClause fc n' (expandParams dec ps'' ns lhs)
1093 (map (expandParams dec ps'' ns) ws)
1094 (expandParams dec ps'' ns rhs)
1095 (map (expandParamsD ist dec ps'' ns) ds)
1096 expandParamsC (PWith fc n lhs ws wval ds)
1097 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1098 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1099 n' = if n `elem` ns then dec n else n in
1100 PWith fc n' (expandParams dec ps'' ns lhs)
1101 (map (expandParams dec ps'' ns) ws)
1102 (expandParams dec ps'' ns wval)
1103 (map (expandParamsD ist dec ps'' ns) ds)
1104 updateps yn nm [] = []
1105 updateps yn nm (((a, t), i):as)
1106 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1107 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
1109expandParamsD ist dec ps ns d = d
1111-- Calculate a priority for a type, for deciding elaboration order
1112-- * if it's just a type variable or concrete type, do it early (0)
1113-- * if there's only type variables and injective constructors, do it next (1)
1114-- * if there's a function type, next (2)
1115-- * finally, everything else (3)
1117getPriority :: IState -> PTerm -> Int
1118getPriority i tm = pri tm
1119 where
1120 pri (PRef _ n) =
1121 case lookupP Nothing n (tt_ctxt i) of
1122 ((P (DCon _ _) _ _):_) -> 1
1123 ((P (TCon _ _) _ _):_) -> 1
1124 ((P Ref _ _):_) -> 4
1125 [] -> 0 -- must be locally bound, if it's not an error...
1126 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1127 pri (PTrue _) = 0
1128 pri (PFalse _) = 0
1129 pri (PRefl _) = 1
1130 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1131 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1132 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1133 pri (PTyped l r) = pri l
1134 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
1135 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1136 pri (PAlternative as) = maximum (map pri as)
1137 pri (PConstant _) = 0
1138 pri Placeholder = 1
1139 pri _ = 3
1141addStatics :: Name -> Term -> PTerm -> Idris ()
1142addStatics n tm ptm =
1143 do let (statics, dynamics) = initStatics tm ptm
1144 let stnames = nub $ concatMap freeNames (map snd statics)
1145 let dnames = nub $ concatMap freeNames (map snd dynamics)
1146 when (not (null statics)) $
1147 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
1148 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1149 let statics' = nub $ map fst statics ++
1150 filter (\x -> not (elem x dnames)) stnames
1151 let stpos = staticList statics' tm
1152 i <- get
1153 put (i { idris_statics = addDef n stpos (idris_statics i) })
1154 addIBC (IBCStatic n)
1155 where
1156 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1157 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1158 if pstatic p == Static then ((n, ty) : static, dynamic)
1159 else (static, (n, ty) : dynamic)
1160 initStatics t pt = ([], [])
1162 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1163 staticList _ _ = []
1165-- Dealing with implicit arguments
1167-- Add implicit Pi bindings for any names in the term which appear in an
1168-- argument position.
1170-- This has become a right mess already. Better redo it some time...
1172implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1173implicit syn n ptm
1174 = do i <- get
1175 let (tm', impdata) = implicitise syn i ptm
1176-- let (tm'', spos) = findStatics i tm'
1177 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
1178 addIBC (IBCImp n)
1179 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1180-- i <- get
1181-- put (i { idris_statics = addDef n spos (idris_statics i) })
1182 return tm'
1184implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
1185implicitise syn ist tm
1186 = let (declimps, ns') = execState (imps True [] tm) ([], [])
1187 ns = ns' \\ (map fst pvars ++ no_imp syn) in
1188 if null ns
1189 then (tm, reverse declimps)
1190 else implicitise syn ist (pibind uvars ns tm)
1191 where
1192 uvars = using syn
1193 pvars = syn_params syn
1195 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1196 | otherwise = x : dropAll xs ys
1197 dropAll [] ys = []
1199 imps top env (PApp _ f as)
1200 = do (decls, ns) <- get
1201 let isn = concatMap (namesIn uvars ist) (map getTm as)
1202 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1203 imps top env (PPi (Imp l _) n ty sc)
1204 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1205 (decls , ns) <- get
1206 put (PImp (getPriority ist ty) l n ty : decls,
1207 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1208 imps True (n:env) sc
1209 imps top env (PPi (Exp l _) n ty sc)
1210 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1211 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1212 _ -> [])
1213 (decls, ns) <- get -- ignore decls in HO types
1214 put (PExp (getPriority ist ty) l ty : decls,
1215 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1216 imps True (n:env) sc
1217 imps top env (PPi (Constraint l _) n ty sc)
1218 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1219 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1220 _ -> [])
1221 (decls, ns) <- get -- ignore decls in HO types
1222 put (PConstraint 10 l ty : decls,
1223 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1224 imps True (n:env) sc
1225 imps top env (PPi (TacImp l _ scr) n ty sc)
1226 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1227 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1228 _ -> [])
1229 (decls, ns) <- get -- ignore decls in HO types
1230 put (PTacImplicit 10 l n scr ty : decls,
1231 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1232 imps True (n:env) sc
1233 imps top env (PEq _ l r)
1234 = do (decls, ns) <- get
1235 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1236 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1237 imps top env (PTyped l r)
1238 = imps top env l
1239 imps top env (PPair _ l r)
1240 = do (decls, ns) <- get
1241 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1242 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1243 imps top env (PDPair _ (PRef _ n) t r)
1244 = do (decls, ns) <- get
1245 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1246 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1247 imps top env (PDPair _ l t r)
1248 = do (decls, ns) <- get
1249 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1250 namesIn uvars ist r
1251 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1252 imps top env (PAlternative as)
1253 = do (decls, ns) <- get
1254 let isn = concatMap (namesIn uvars ist) as
1255 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1256 imps top env (PLam n ty sc)
1257 = do imps False env ty
1258 imps False (n:env) sc
1259 imps top env (PHidden tm) = imps False env tm
1260 imps top env _ = return ()
1262 pibind using [] sc = sc
1263 pibind using (n:ns) sc
1264 = case lookup n using of
1265 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
1266 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
1268-- Add implicit arguments in function calls
1269addImplPat :: IState -> PTerm -> PTerm
1270addImplPat = addImpl' True []
1272addImplBound :: IState -> [Name] -> PTerm -> PTerm
1273addImplBound ist ns = addImpl' False ns ist
1275addImpl :: IState -> PTerm -> PTerm
1276addImpl = addImpl' False []
1278-- TODO: in patterns, don't add implicits to function names guarded by constructors
1279-- and *not* inside a PHidden
1281addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1282addImpl' inpat env ist ptm = ai env ptm
1283 where
1284 ai env (PRef fc f)
1285 | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []
1286 ai env (PHidden (PRef fc f))
1287 | not (f `elem` env) = handleErr $ aiFn False ist fc f []
1288 ai env (PEq fc l r) = let l' = ai env l
1289 r' = ai env r in
1290 PEq fc l' r'
1291 ai env (PTyped l r) = let l' = ai env l
1292 r' = ai env r in
1293 PTyped l' r'
1294 ai env (PPair fc l r) = let l' = ai env l
1295 r' = ai env r in
1296 PPair fc l' r'
1297 ai env (PDPair fc l t r) = let l' = ai env l
1298 t' = ai env t
1299 r' = ai env r in
1300 PDPair fc l' t' r'
1301 ai env (PAlternative as) = let as' = map (ai env) as in
1302 PAlternative as'
1303 ai env (PApp fc (PRef _ f) as)
1304 | not (f `elem` env)
1305 = let as' = map (fmap (ai env)) as in
1306 handleErr $ aiFn False ist fc f as'
1307 ai env (PApp fc f as) = let f' = ai env f
1308 as' = map (fmap (ai env)) as in
1309 mkPApp fc 1 f' as'
1310 ai env (PCase fc c os) = let c' = ai env c
1311 os' = map (pmap (ai env)) os in
1312 PCase fc c' os'
1313 ai env (PLam n ty sc) = let ty' = ai env ty
1314 sc' = ai (n:env) sc in
1315 PLam n ty' sc'
1316 ai env (PLet n ty val sc)
1317 = let ty' = ai env ty
1318 val' = ai env val
1319 sc' = ai (n:env) sc in
1320 PLet n ty' val' sc'
1321 ai env (PPi p n ty sc) = let ty' = ai env ty
1322 sc' = ai (n:env) sc in
1323 PPi p n ty' sc'
1324 ai env (PHidden tm) = PHidden (ai env tm)
1325 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1326 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1327 ai env tm = tm
1329 handleErr (Left err) = PElabError err
1330 handleErr (Right x) = x
1332-- if in a pattern, and there are no arguments, and there's no possible
1333-- names with zero explicit arguments, don't add implicits.
1335aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1336aiFn True ist fc f []
1337 = case lookupCtxt Nothing f (idris_implicits ist) of
1338 [] -> Right $ PRef fc f
1339 alts -> if (any (all imp) alts)
1340 then aiFn False ist fc f [] -- use it as a constructor
1341 else Right $ PRef fc f
1342 where imp (PExp _ _ _) = False
1343 imp _ = True
1344aiFn inpat ist fc f as
1345 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1346aiFn inpat ist fc f as
1347 -- This is where namespaces get resolved by adding PAlternative
1348 = case lookupCtxtName Nothing f (idris_implicits ist) of
1349 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1350 [] -> if f `elem` idris_metavars ist
1351 then Right $ PApp fc (PRef fc f) as
1352 else Right $ mkPApp fc (length as) (PRef fc f) as
1353 alts -> Right $
1354 PAlternative $
1355 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1356 (insertImpl ns as)) alts
1357 where
1358 insertImpl :: [PArg] -> [PArg] -> [PArg]
1359 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1360 PExp p l tm : insertImpl ps given
1361 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1362 PConstraint p l tm : insertImpl ps given
1363 insertImpl (PConstraint p l ty : ps) given =
1364 PConstraint p l (PResolveTC fc) : insertImpl ps given
1365 insertImpl (PImp p l n ty : ps) given =
1366 case find n given [] of
1367 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
1368 Nothing -> PImp p l n Placeholder : insertImpl ps given
1369 insertImpl (PTacImplicit p l n sc ty : ps) given =
1370 case find n given [] of
1371 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1372 Nothing -> PTacImplicit p l n sc sc
1373 : insertImpl ps given
1374 insertImpl expected [] = []
1375 insertImpl _ given = given
1377 find n [] acc = Nothing
1378 find n (PImp _ _ n' t : gs) acc
1379 | n == n' = Just (t, reverse acc ++ gs)
1380 find n (g : gs) acc = find n gs (g : acc)
1382mkPApp fc a f [] = f
1383mkPApp fc a f as = let rest = drop a as in
1384 appRest fc (PApp fc f (take a as)) rest
1385 where
1386 appRest fc f [] = f
1387 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1389-- Find 'static' argument positions
1390-- (the declared ones, plus any names in argument position in the declared
1391-- statics)
1392-- FIXME: It's possible that this really has to happen after elaboration
1394findStatics :: IState -> PTerm -> (PTerm, [Bool])
1395findStatics ist tm = trace (showImp True tm) $
1396 let (ns, ss) = fs tm in
1397 runState (pos ns ss tm) []
1398 where fs (PPi p n t sc)
1399 | Static <- pstatic p
1400 = let (ns, ss) = fs sc in
1401 (namesIn [] ist t : ns, n : ss)
1402 | otherwise = let (ns, ss) = fs sc in
1403 (ns, ss)
1404 fs _ = ([], [])
1406 inOne n ns = length (filter id (map (elem n) ns)) == 1
1408 pos ns ss (PPi p n t sc)
1409 | elem n ss = do sc' <- pos ns ss sc
1410 spos <- get
1411 put (True : spos)
1412 return (PPi (p { pstatic = Static }) n t sc')
1413 | otherwise = do sc' <- pos ns ss sc
1414 spos <- get
1415 put (False : spos)
1416 return (PPi p n t sc')
1417 pos ns ss t = return t
1419-- Debugging/logging stuff
1421dumpDecls :: [PDecl] -> String
1422dumpDecls [] = ""
1423dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1425dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1426dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1427dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1428dumpDecl (PData _ _ d) = showDImp True d
1429dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1430dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1431dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1432dumpDecl (PClass _ _ cs n ps ds)
1433 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1434dumpDecl (PInstance _ _ cs n _ t ds)
1435 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1436dumpDecl _ = "..."
1437-- dumpDecl (PImport i) = "import " ++ i
1439-- for 6.12/7 compatibility
1440data EitherErr a b = LeftErr a | RightOK b
1442instance Monad (EitherErr a) where
1443 return = RightOK
1445 (LeftErr e) >>= k = LeftErr e
1446 RightOK v >>= k = k v
1448toEither (LeftErr e) = Left e
1449toEither (RightOK ho) = Right ho
1451-- syntactic match of a against b, returning pair of variables in a
1452-- and what they match. Returns the pair that failed if not a match.
1454matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1455matchClause = matchClause' False
1457matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1458matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1459 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1461 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1462 fullApp x = x
1464 match' x y = match (fullApp x) (fullApp y)
1465 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1466 | PConstant (I _) <- getTm x = match (getTm x) x'
1467 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1468 | PConstant (I _) <- getTm x = match (getTm x) x'
1469 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1470 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1471 match (PApp _ f args) (PApp _ f' args')
1472 | length args == length args'
1473 = do mf <- match' f f'
1474 ms <- zipWithM matchArg args args'
1475 return (mf ++ concat ms)
1476-- match (PRef _ n) (PRef _ n') | n == n' = return []
1477-- | otherwise = Nothing
1478 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1479 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1480 match (PRef _ n) (PRef _ n') | n == n' = return []
1481 match (PRef _ n) tm
1482 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1483 = return [(n, tm)]
1484 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1485 mr <- match' r r'
1486 return (ml ++ mr)
1487 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1488 mr <- match r r'
1489 return (ml ++ mr)
1490 match (PTyped l r) x = match l x
1491 match x (PTyped l r) = match x l
1492 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1493 mr <- match' r r'
1494 return (ml ++ mr)
1495 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1496 mt <- match' t t'
1497 mr <- match' r r'
1498 return (ml ++ mt ++ mr)
1499 match (PAlternative as) (PAlternative as')
1500 = do ms <- zipWithM match' as as'
1501 return (concat ms)
1502 match a@(PAlternative as) b
1503 = do let ms = zipWith match' as (repeat b)
1504 case (rights (map toEither ms)) of
1505 (x: _) -> return x
1506 _ -> LeftErr (a, b)
1507 match (PCase _ _ _) _ = return [] -- lifted out
1508 match (PMetavar _) _ = return [] -- modified
1509 match (PQuote _) _ = return []
1510 match (PProof _) _ = return []
1511 match (PTactics _) _ = return []
1512 match (PRefl _) (PRefl _) = return []
1513 match (PResolveTC _) (PResolveTC _) = return []
1514 match (PTrue _) (PTrue _) = return []
1515 match (PFalse _) (PFalse _) = return []
1516 match (PReturn _) (PReturn _) = return []
1517 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1518 ms <- match' s s'
1519 return (mt ++ ms)
1520 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1521 ms <- match' s s'
1522 return (mt ++ ms)
1523 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1524 mty <- match' ty ty'
1525 ms <- match' s s'
1526 return (mt ++ mty ++ ms)
1527 match (PHidden x) (PHidden y) = match' x y
1528 match Placeholder _ = return []
1529-- match _ Placeholder = return []
1530 match (PResolveTC _) _ = return []
1531 match a b | a == b = return []
1532 | otherwise = LeftErr (a, b)
1534 checkRpts (RightOK ms) = check ms where
1535 check ((n,t):xs)
1536 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1537 then Left (t, t')
1538 else check xs
1539 check (_:xs) = check xs
1540 check [] = Right ms
1541 checkRpts (LeftErr x) = Left x
1543substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1544substMatches [] t = t
1545substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1547substMatch :: Name -> PTerm -> PTerm -> PTerm
1548substMatch n tm t = sm t where
1549 sm (PRef _ n') | n == n' = tm
1550 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1551 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1552 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1553 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1554 sm (PEq f x y) = PEq f (sm x) (sm y)
1555 sm (PTyped x y) = PTyped (sm x) (sm y)
1556 sm (PPair f x y) = PPair f (sm x) (sm y)
1557 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1558 sm (PAlternative as) = PAlternative (map sm as)
1559 sm (PHidden x) = PHidden (sm x)
1560 sm x = x
1562shadow :: Name -> Name -> PTerm -> PTerm
1563shadow n n' t = sm t where
1564 sm (PRef fc x) | n == x = PRef fc n'
1565 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1566 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1567 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1568 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1569 sm (PEq f x y) = PEq f (sm x) (sm y)
1570 sm (PTyped x y) = PTyped (sm x) (sm y)
1571 sm (PPair f x y) = PPair f (sm x) (sm y)
1572 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1573 sm (PAlternative as) = PAlternative (map sm as)
1574 sm (PHidden x) = PHidden (sm x)
1575 sm x = x