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