git.iko.soy/Idris-dev
on 0338d39 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1491 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 deriving (Show, Eq)
408{-!
409deriving instance Binary FnOpt
410!-}
412type FnOpts = [FnOpt]
414inlinable :: FnOpts -> Bool
415inlinable = elem Inlinable
417data PDecl' t = PFix FC Fixity [String] -- fixity declaration
418 | PTy SyntaxInfo FC FnOpts Name t -- type declaration
419 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
420 | PData SyntaxInfo FC (PData' t) -- data declaration
421 | PParams FC [(Name, t)] [PDecl' t] -- params block
422 | PNamespace String [PDecl' t] -- new namespace
423 | PRecord SyntaxInfo FC Name t Name t -- record declaration
424 | PClass SyntaxInfo FC
425 [t] -- constraints
426 Name
427 [(Name, t)] -- parameters
428 [PDecl' t] -- declarations
429 | PInstance SyntaxInfo FC [t] -- constraints
430 Name -- class
431 [t] -- parameters
432 t -- full instance type
433 [PDecl' t]
434 | PDSL Name (DSL' t)
435 | PSyntax FC Syntax
436 | PDirective (Idris ())
437 deriving Functor
439data PClause' t = PClause FC Name t [t] t [PDecl' t]
440 | PWith FC Name t [t] t [PDecl' t]
441 | PClauseR FC [t] t [PDecl' t]
442 | PWithR FC [t] t [PDecl' t]
443 deriving Functor
445data PData' t = PDatadecl { d_name :: Name,
446 d_tcon :: t,
447 d_cons :: [(Name, t, FC)] }
448 deriving Functor
450-- Handy to get a free function for applying PTerm -> PTerm functions
451-- across a program, by deriving Functor
453type PDecl = PDecl' PTerm
454type PData = PData' PTerm
455type PClause = PClause' PTerm
457-- get all the names declared in a decl
459declared :: PDecl -> [Name]
460declared (PFix _ _ _) = []
461declared (PTy _ _ _ n t) = [n]
462declared (PClauses _ _ n _) = [] -- not a declaration
463declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
464 where fstt (a, _, _) = a
465declared (PParams _ _ ds) = concatMap declared ds
466declared (PNamespace _ ds) = concatMap declared ds
467-- declared (PImport _) = []
469updateN :: [(Name, Name)] -> Name -> Name
470updateN ns n | Just n' <- lookup n ns = n'
471updateN _ n = n
473updateNs :: [(Name, Name)] -> PTerm -> PTerm
474updateNs [] t = t
475updateNs ns t = mapPT updateRef t
476 where updateRef (PRef fc f) = PRef fc (updateN ns f)
477 updateRef t = t
479-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
480-- updateDNs [] t = t
481-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
482-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
483-- where updateCNs ns (PClause n l ts r ds)
484-- = PClause (updateN ns n) (fmap (updateNs ns) l)
485-- (map (fmap (updateNs ns)) ts)
486-- (fmap (updateNs ns) r)
487-- (map (updateDNs ns) ds)
488-- updateDNs ns c = c
490-- High level language terms
492data PTerm = PQuote Raw
493 | PRef FC Name
494 | PLam Name PTerm PTerm
495 | PPi Plicity Name PTerm PTerm
496 | PLet Name PTerm PTerm PTerm
497 | PTyped PTerm PTerm -- term with explicit type
498 | PApp FC PTerm [PArg]
499 | PCase FC PTerm [(PTerm, PTerm)]
500 | PTrue FC
501 | PFalse FC
502 | PRefl FC
503 | PResolveTC FC
504 | PEq FC PTerm PTerm
505 | PPair FC PTerm PTerm
506 | PDPair FC PTerm PTerm PTerm
507 | PAlternative [PTerm]
508 | PHidden PTerm -- irrelevant or hidden pattern
509 | PSet
510 | PConstant Const
511 | Placeholder
512 | PDoBlock [PDo]
513 | PIdiom FC PTerm
514 | PReturn FC
515 | PMetavar Name
516 | PProof [PTactic]
517 | PTactics [PTactic] -- as PProof, but no auto solving
518 | PElabError Err -- error to report on elaboration
519 | PImpossible -- special case for declaring when an LHS can't typecheck
520 deriving Eq
521{-!
522deriving instance Binary PTerm
523!-}
525mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
526mapPT f t = f (mpt t) where
527 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
528 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
529 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
530 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
531 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
532 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
533 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
534 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
535 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
536 mpt (PAlternative as) = PAlternative (map (mapPT f) as)
537 mpt (PHidden t) = PHidden (mapPT f t)
538 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
539 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
540 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
541 mpt x = x
544data PTactic' t = Intro [Name] | Intros | Focus Name
545 | Refine Name [Bool] | Rewrite t | LetTac Name t
546 | Exact t | Compute | Trivial
547 | Solve
548 | Attack
549 | ProofState | ProofTerm | Undo
550 | Try (PTactic' t) (PTactic' t)
551 | TSeq (PTactic' t) (PTactic' t)
552 | Qed | Abandon
553 deriving (Show, Eq, Functor)
554{-!
555deriving instance Binary PTactic'
556!-}
558type PTactic = PTactic' PTerm
560data PDo' t = DoExp FC t
561 | DoBind FC Name t
562 | DoBindP FC t t
563 | DoLet FC Name t t
564 | DoLetP FC t t
565 deriving (Eq, Functor)
566{-!
567deriving instance Binary PDo'
568!-}
570type PDo = PDo' PTerm
572-- The priority gives a hint as to elaboration order. Best to elaborate
573-- things early which will help give a more concrete type to other
574-- variables, e.g. a before (interpTy a).
576data PArg' t = PImp { priority :: Int,
577 lazyarg :: Bool, pname :: Name, getTm :: t }
578 | PExp { priority :: Int,
579 lazyarg :: Bool, getTm :: t }
580 | PConstraint { priority :: Int,
581 lazyarg :: Bool, getTm :: t }
582 | PTacImplicit { priority :: Int,
583 lazyarg :: Bool, pname :: Name,
584 getScript :: t,
585 getTm :: t }
586 deriving (Show, Eq, Functor)
587{-!
588deriving instance Binary PArg'
589!-}
591pimp = PImp 0 True
592pexp = PExp 0 False
593pconst = PConstraint 0 False
594ptacimp = PTacImplicit 0 True
596type PArg = PArg' PTerm
598-- Type class data
600data ClassInfo = CI { instanceName :: Name,
601 class_methods :: [(Name, (FnOpts, PTerm))],
602 class_defaults :: [(Name, Name)], -- method name -> default impl
603 class_params :: [Name],
604 class_instances :: [Name] }
605 deriving Show
606{-!
607deriving instance Binary ClassInfo
608!-}
610data OptInfo = Optimise { collapsible :: Bool,
611 forceable :: [Int], -- argument positions
612 recursive :: [Int] }
613 deriving Show
614{-!
615deriving instance Binary OptInfo
616!-}
619data TypeInfo = TI { con_names :: [Name] }
620 deriving Show
621{-!
622deriving instance Binary TypeInfo
623!-}
625-- Syntactic sugar info
627data DSL' t = DSL { dsl_bind :: t,
628 dsl_return :: t,
629 dsl_apply :: t,
630 dsl_pure :: t,
631 dsl_var :: Maybe t,
632 index_first :: Maybe t,
633 index_next :: Maybe t,
634 dsl_lambda :: Maybe t,
635 dsl_let :: Maybe t
636 }
637 deriving (Show, Functor)
638{-!
639deriving instance Binary DSL'
640!-}
642type DSL = DSL' PTerm
644data SynContext = PatternSyntax | TermSyntax | AnySyntax
645 deriving Show
646{-!
647deriving instance Binary SynContext
648!-}
650data Syntax = Rule [SSymbol] PTerm SynContext
651 deriving Show
652{-!
653deriving instance Binary Syntax
654!-}
656data SSymbol = Keyword Name
657 | Symbol String
658 | Expr Name
659 | SimpleExpr Name
660 deriving Show
661{-!
662deriving instance Binary SSymbol
663!-}
665initDSL = DSL (PRef f (UN ">>="))
666 (PRef f (UN "return"))
667 (PRef f (UN "<$>"))
668 (PRef f (UN "pure"))
669 Nothing
670 Nothing
671 Nothing
672 Nothing
673 Nothing
674 where f = FC "(builtin)" 0
676data SyntaxInfo = Syn { using :: [(Name, PTerm)],
677 syn_params :: [(Name, PTerm)],
678 syn_namespace :: [String],
679 no_imp :: [Name],
680 decoration :: Name -> Name,
681 inPattern :: Bool,
682 dsl_info :: DSL }
683 deriving Show
685defaultSyntax = Syn [] [] [] [] id False initDSL
687expandNS :: SyntaxInfo -> Name -> Name
688expandNS syn n@(NS _ _) = n
689expandNS syn n = case syn_namespace syn of
690 [] -> n
691 xs -> NS n xs
694--- Pretty printing declarations and terms
696instance Show PTerm where
697 show tm = showImp False tm
699instance Show PDecl where
700 show d = showDeclImp False d
702instance Show PClause where
703 show c = showCImp True c
705instance Show PData where
706 show d = showDImp False d
708showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
709showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty
710showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
711showDeclImp _ (PData _ _ d) = show d
713showCImp :: Bool -> PClause -> String
714showCImp impl (PClause _ n l ws r w)
715 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
716 ++ " where " ++ show w
717 where
718 showWs [] = ""
719 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
720showCImp impl (PWith _ n l ws r w)
721 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
722 ++ " { " ++ show w ++ " } "
723 where
724 showWs [] = ""
725 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
728showDImp :: Bool -> PData -> String
729showDImp impl (PDatadecl n ty cons)
730 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
731 ++ showSep "\n\t| "
732 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
734getImps :: [PArg] -> [(Name, PTerm)]
735getImps [] = []
736getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
737getImps (_ : xs) = getImps xs
739getExps :: [PArg] -> [PTerm]
740getExps [] = []
741getExps (PExp _ _ tm : xs) = tm : getExps xs
742getExps (_ : xs) = getExps xs
744getConsts :: [PArg] -> [PTerm]
745getConsts [] = []
746getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
747getConsts (_ : xs) = getConsts xs
749getAll :: [PArg] -> [PTerm]
750getAll = map getTm
752showImp :: Bool -> PTerm -> String
753showImp impl tm = se 10 tm where
754 se p (PQuote r) = "![" ++ show r ++ "]"
755 se p (PRef fc n) = if impl then show n ++ "[" ++ show fc ++ "]"
756 else showbasic n
757 where showbasic n@(UN _) = show n
758 showbasic (MN _ s) = s
759 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
760 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
761 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
762 " in " ++ se 10 sc
763 se p (PPi (Exp l s) n ty sc)
764 | n `elem` allNamesIn sc || impl
765 = bracket p 2 $
766 if l then "|(" else "(" ++
767 show n ++ " : " ++ se 10 ty ++
768 ") " ++ st ++
769 "-> " ++ se 10 sc
770 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
771 where st = case s of
772 Static -> "[static] "
773 _ -> ""
774 se p (PPi (Imp l s) n ty sc)
775 | impl = bracket p 2 $ if l then "|{" else "{" ++
776 show n ++ " : " ++ se 10 ty ++
777 "} " ++ st ++ "-> " ++ se 10 sc
778 | otherwise = se 10 sc
779 where st = case s of
780 Static -> "[static] "
781 _ -> ""
782 se p (PPi (Constraint _ _) n ty sc)
783 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
784 se p (PApp _ (PRef _ f) [])
785 | not impl = show f
786 se p (PApp _ (PRef _ op@(UN (f:_))) args)
787 | length (getExps args) == 2 && not impl && not (isAlpha f)
788 = let [l, r] = getExps args in
789 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
790 se p (PApp _ f as)
791 = let args = getExps as in
792 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
793 else concatMap seArg args
794 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
795 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
796 se p (PHidden tm) = "." ++ se 0 tm
797 se p (PRefl _) = "refl"
798 se p (PResolveTC _) = "resolvetc"
799 se p (PTrue _) = "()"
800 se p (PFalse _) = "_|_"
801 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
802 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
803 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
804 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
805 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
806 se p PSet = "Set"
807 se p (PConstant c) = show c
808 se p (PProof ts) = "proof { " ++ show ts ++ "}"
809 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
810 se p (PMetavar n) = "?" ++ show n
811 se p (PReturn f) = "return"
812 se p PImpossible = "impossible"
813 se p Placeholder = "_"
814 se p (PDoBlock _) = "do block show not implemented"
815 se p (PElabError s) = show s
816-- se p x = "Not implemented"
818 sArg (PImp _ _ n tm) = siArg (n, tm)
819 sArg (PExp _ _ tm) = seArg tm
820 sArg (PConstraint _ _ tm) = scArg tm
821 sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
823 seArg arg = " " ++ se 0 arg
824 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
825 scArg val = " {{" ++ se 10 val ++ "}}"
826 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
828 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
829 | otherwise = str
831allNamesIn :: PTerm -> [Name]
832allNamesIn tm = nub $ ni [] tm
833 where
834 ni env (PRef _ n)
835 | not (n `elem` env) = [n]
836 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
837 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
838 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
839 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
840 ni env (PHidden tm) = ni env tm
841 ni env (PEq _ l r) = ni env l ++ ni env r
842 ni env (PTyped l r) = ni env l ++ ni env r
843 ni env (PPair _ l r) = ni env l ++ ni env r
844 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
845 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
846 ni env (PAlternative ls) = concatMap (ni env) ls
847 ni env _ = []
849namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
850namesIn uvars ist tm = nub $ ni [] tm
851 where
852 ni env (PRef _ n)
853 | not (n `elem` env)
854 = case lookupTy Nothing n (tt_ctxt ist) of
855 [] -> [n]
856 _ -> if n `elem` (map fst uvars) then [n] else []
857 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
858 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
859 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
860 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
861 ni env (PEq _ l r) = ni env l ++ ni env r
862 ni env (PTyped l r) = ni env l ++ ni env r
863 ni env (PPair _ l r) = ni env l ++ ni env r
864 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
865 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
866 ni env (PAlternative as) = concatMap (ni env) as
867 ni env (PHidden tm) = ni env tm
868 ni env _ = []
870-- For inferring types of things
872bi = FC "builtin" 0
874inferTy = MN 0 "__Infer"
875inferCon = MN 0 "__infer"
876inferDecl = PDatadecl inferTy
877 PSet
878 [(inferCon, PPi impl (MN 0 "A") PSet (
879 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
880 (PRef bi inferTy)), bi)]
882infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
883infP = P (TCon 6 0) inferTy (Set (UVal 0))
885getInferTerm, getInferType :: Term -> Term
886getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
887getInferTerm (App (App _ _) tm) = tm
888getInferTerm tm = error ("getInferTerm " ++ show tm)
890getInferType (Bind n b sc) = Bind n b $ getInferType sc
891getInferType (App (App _ ty) _) = ty
893-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
895primNames = [unitTy, unitCon,
896 falseTy, pairTy, pairCon,
897 eqTy, eqCon, inferTy, inferCon]
899unitTy = MN 0 "__Unit"
900unitCon = MN 0 "__II"
901unitDecl = PDatadecl unitTy PSet
902 [(unitCon, PRef bi unitTy, bi)]
904falseTy = MN 0 "__False"
905falseDecl = PDatadecl falseTy PSet []
907pairTy = MN 0 "__Pair"
908pairCon = MN 0 "__MkPair"
909pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
910 [(pairCon, PPi impl (n "A") PSet (
911 PPi impl (n "B") PSet (
912 PPi expl (n "a") (PRef bi (n "A")) (
913 PPi expl (n "b") (PRef bi (n "B"))
914 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
915 pexp (PRef bi (n "B"))])))), bi)]
916 where n a = MN 0 a
918eqTy = UN "="
919eqCon = UN "refl"
920eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
921 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
922 PSet)
923 [(eqCon, PPi impl (n "a") PSet (
924 PPi impl (n "x") (PRef bi (n "a"))
925 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
926 pimp (n "b") Placeholder,
927 pexp (PRef bi (n "x")),
928 pexp (PRef bi (n "x"))])), bi)]
929 where n a = MN 0 a
931-- Defined in builtins.idr
932sigmaTy = UN "Exists"
933existsCon = UN "Ex_intro"
935piBind :: [(Name, PTerm)] -> PTerm -> PTerm
936piBind [] t = t
937piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
939tcname (UN ('@':_)) = True
940tcname (NS n _) = tcname n
941tcname _ = False
943-- Dealing with parameters
945expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
946expandParams dec ps ns tm = en tm
947 where
948 -- if we shadow a name (say in a lambda binding) that is used in a call to
949 -- a lifted function, we need access to both names - once in the scope of the
950 -- binding and once to call the lifted functions. So we'll explicitly shadow
951 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
952 -- but we didn't...)
954 mkShadow (UN n) = MN 0 n
955 mkShadow (MN i n) = MN (i+1) n
956 mkShadow (NS x s) = NS (mkShadow x) s
958 en (PLam n t s)
959 | n `elem` map fst ps
960 = let n' = mkShadow n in
961 PLam n' (en t) (en (shadow n n' s))
962 | otherwise = PLam n (en t) (en s)
963 en (PPi p n t s)
964 | n `elem` map fst ps
965 = let n' = mkShadow n in
966 PPi p n' (en t) (en (shadow n n' s))
967 | otherwise = PPi p n (en t) (en s)
968 en (PLet n ty v s)
969 | n `elem` map fst ps
970 = let n' = mkShadow n in
971 PLet n' (en ty) (en v) (en (shadow n n' s))
972 | otherwise = PLet n (en ty) (en v) (en s)
973 en (PEq f l r) = PEq f (en l) (en r)
974 en (PTyped l r) = PTyped (en l) (en r)
975 en (PPair f l r) = PPair f (en l) (en r)
976 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
977 en (PAlternative as) = PAlternative (map en as)
978 en (PHidden t) = PHidden (en t)
979 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
980 en (PProof ts) = PProof (map (fmap en) ts)
981 en (PTactics ts) = PTactics (map (fmap en) ts)
983 en (PQuote (Var n))
984 | n `elem` ns = PQuote (Var (dec n))
985 en (PApp fc (PRef fc' n) as)
986 | n `elem` ns = PApp fc (PRef fc' (dec n))
987 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
988 en (PRef fc n)
989 | n `elem` ns = PApp fc (PRef fc (dec n))
990 (map (pexp . (PRef fc)) (map fst ps))
991 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
992 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
993 en t = t
995expandParamsD :: IState ->
996 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
997expandParamsD ist dec ps ns (PTy syn fc o n ty)
998 = if n `elem` ns
999 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
1000 else PTy syn fc o n (expandParams dec ps ns ty)
1001expandParamsD ist dec ps ns (PClauses fc opts n cs)
1002 = let n' = if n `elem` ns then dec n else n in
1003 PClauses fc opts n' (map expandParamsC cs)
1004 where
1005 expandParamsC (PClause fc n lhs ws rhs ds)
1006 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1007 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1008 n' = if n `elem` ns then dec n else n in
1009 PClause fc n' (expandParams dec ps'' ns lhs)
1010 (map (expandParams dec ps'' ns) ws)
1011 (expandParams dec ps'' ns rhs)
1012 (map (expandParamsD ist dec ps'' ns) ds)
1013 expandParamsC (PWith fc n lhs ws wval ds)
1014 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1015 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1016 n' = if n `elem` ns then dec n else n in
1017 PWith fc n' (expandParams dec ps'' ns lhs)
1018 (map (expandParams dec ps'' ns) ws)
1019 (expandParams dec ps'' ns wval)
1020 (map (expandParamsD ist dec ps'' ns) ds)
1021 updateps yn nm [] = []
1022 updateps yn nm (((a, t), i):as)
1023 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1024 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
1026expandParamsD ist dec ps ns d = d
1028-- Calculate a priority for a type, for deciding elaboration order
1029-- * if it's just a type variable or concrete type, do it early (0)
1030-- * if there's only type variables and injective constructors, do it next (1)
1031-- * if there's a function type, next (2)
1032-- * finally, everything else (3)
1034getPriority :: IState -> PTerm -> Int
1035getPriority i tm = pri tm
1036 where
1037 pri (PRef _ n) =
1038 case lookupP Nothing n (tt_ctxt i) of
1039 ((P (DCon _ _) _ _):_) -> 1
1040 ((P (TCon _ _) _ _):_) -> 1
1041 ((P Ref _ _):_) -> 4
1042 [] -> 0 -- must be locally bound, if it's not an error...
1043 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1044 pri (PTrue _) = 0
1045 pri (PFalse _) = 0
1046 pri (PRefl _) = 1
1047 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1048 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1049 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1050 pri (PTyped l r) = pri l
1051 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
1052 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1053 pri (PAlternative as) = maximum (map pri as)
1054 pri (PConstant _) = 0
1055 pri Placeholder = 1
1056 pri _ = 3
1058addStatics :: Name -> Term -> PTerm -> Idris ()
1059addStatics n tm ptm =
1060 do let (statics, dynamics) = initStatics tm ptm
1061 let stnames = nub $ concatMap freeNames (map snd statics)
1062 let dnames = nub $ concatMap freeNames (map snd dynamics)
1063 when (not (null statics)) $
1064 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
1065 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1066 let statics' = nub $ map fst statics ++
1067 filter (\x -> not (elem x dnames)) stnames
1068 let stpos = staticList statics' tm
1069 i <- get
1070 put (i { idris_statics = addDef n stpos (idris_statics i) })
1071 addIBC (IBCStatic n)
1072 where
1073 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1074 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1075 if pstatic p == Static then ((n, ty) : static, dynamic)
1076 else (static, (n, ty) : dynamic)
1077 initStatics t pt = ([], [])
1079 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1080 staticList _ _ = []
1082-- Dealing with implicit arguments
1084-- Add implicit Pi bindings for any names in the term which appear in an
1085-- argument position.
1087-- This has become a right mess already. Better redo it some time...
1089implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1090implicit syn n ptm
1091 = do i <- get
1092 let (tm', impdata) = implicitise syn i ptm
1093-- let (tm'', spos) = findStatics i tm'
1094 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
1095 addIBC (IBCImp n)
1096 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1097-- i <- get
1098-- put (i { idris_statics = addDef n spos (idris_statics i) })
1099 return tm'
1101implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
1102implicitise syn ist tm
1103 = let (declimps, ns') = execState (imps True [] tm) ([], [])
1104 ns = ns' \\ (map fst pvars ++ no_imp syn) in
1105 if null ns
1106 then (tm, reverse declimps)
1107 else implicitise syn ist (pibind uvars ns tm)
1108 where
1109 uvars = using syn
1110 pvars = syn_params syn
1112 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1113 | otherwise = x : dropAll xs ys
1114 dropAll [] ys = []
1116 imps top env (PApp _ f as)
1117 = do (decls, ns) <- get
1118 let isn = concatMap (namesIn uvars ist) (map getTm as)
1119 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1120 imps top env (PPi (Imp l _) n ty sc)
1121 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1122 (decls , ns) <- get
1123 put (PImp (getPriority ist ty) l n ty : decls,
1124 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1125 imps True (n:env) sc
1126 imps top env (PPi (Exp l _) n ty sc)
1127 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1128 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1129 _ -> [])
1130 (decls, ns) <- get -- ignore decls in HO types
1131 put (PExp (getPriority ist ty) l ty : decls,
1132 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1133 imps True (n:env) sc
1134 imps top env (PPi (Constraint l _) n ty sc)
1135 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1136 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1137 _ -> [])
1138 (decls, ns) <- get -- ignore decls in HO types
1139 put (PConstraint 10 l ty : decls,
1140 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1141 imps True (n:env) sc
1142 imps top env (PPi (TacImp l _ scr) n ty sc)
1143 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1144 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1145 _ -> [])
1146 (decls, ns) <- get -- ignore decls in HO types
1147 put (PTacImplicit 10 l n scr ty : decls,
1148 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1149 imps True (n:env) sc
1150 imps top env (PEq _ l r)
1151 = do (decls, ns) <- get
1152 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1153 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1154 imps top env (PTyped l r)
1155 = imps top env l
1156 imps top env (PPair _ l r)
1157 = do (decls, ns) <- get
1158 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1159 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1160 imps top env (PDPair _ (PRef _ n) t r)
1161 = do (decls, ns) <- get
1162 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1163 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1164 imps top env (PDPair _ l t r)
1165 = do (decls, ns) <- get
1166 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1167 namesIn uvars ist r
1168 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1169 imps top env (PAlternative as)
1170 = do (decls, ns) <- get
1171 let isn = concatMap (namesIn uvars ist) as
1172 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1173 imps top env (PLam n ty sc)
1174 = do imps False env ty
1175 imps False (n:env) sc
1176 imps top env (PHidden tm) = imps False env tm
1177 imps top env _ = return ()
1179 pibind using [] sc = sc
1180 pibind using (n:ns) sc
1181 = case lookup n using of
1182 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
1183 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
1185-- Add implicit arguments in function calls
1186addImplPat :: IState -> PTerm -> PTerm
1187addImplPat = addImpl' True []
1189addImplBound :: IState -> [Name] -> PTerm -> PTerm
1190addImplBound ist ns = addImpl' False ns ist
1192addImpl :: IState -> PTerm -> PTerm
1193addImpl = addImpl' False []
1195-- TODO: in patterns, don't add implicits to function names guarded by constructors
1196-- and *not* inside a PHidden
1198addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1199addImpl' inpat env ist ptm = ai env ptm
1200 where
1201 ai env (PRef fc f)
1202 | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []
1203 ai env (PHidden (PRef fc f))
1204 | not (f `elem` env) = handleErr $ aiFn False ist fc f []
1205 ai env (PEq fc l r) = let l' = ai env l
1206 r' = ai env r in
1207 PEq fc l' r'
1208 ai env (PTyped l r) = let l' = ai env l
1209 r' = ai env r in
1210 PTyped l' r'
1211 ai env (PPair fc l r) = let l' = ai env l
1212 r' = ai env r in
1213 PPair fc l' r'
1214 ai env (PDPair fc l t r) = let l' = ai env l
1215 t' = ai env t
1216 r' = ai env r in
1217 PDPair fc l' t' r'
1218 ai env (PAlternative as) = let as' = map (ai env) as in
1219 PAlternative as'
1220 ai env (PApp fc (PRef _ f) as)
1221 | not (f `elem` env)
1222 = let as' = map (fmap (ai env)) as in
1223 handleErr $ aiFn False ist fc f as'
1224 ai env (PApp fc f as) = let f' = ai env f
1225 as' = map (fmap (ai env)) as in
1226 mkPApp fc 1 f' as'
1227 ai env (PCase fc c os) = let c' = ai env c
1228 os' = map (pmap (ai env)) os in
1229 PCase fc c' os'
1230 ai env (PLam n ty sc) = let ty' = ai env ty
1231 sc' = ai (n:env) sc in
1232 PLam n ty' sc'
1233 ai env (PLet n ty val sc)
1234 = let ty' = ai env ty
1235 val' = ai env val
1236 sc' = ai (n:env) sc in
1237 PLet n ty' val' sc'
1238 ai env (PPi p n ty sc) = let ty' = ai env ty
1239 sc' = ai (n:env) sc in
1240 PPi p n ty' sc'
1241 ai env (PHidden tm) = PHidden (ai env tm)
1242 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1243 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1244 ai env tm = tm
1246 handleErr (Left err) = PElabError err
1247 handleErr (Right x) = x
1249-- if in a pattern, and there are no arguments, and there's no possible
1250-- names with zero explicit arguments, don't add implicits.
1252aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1253aiFn True ist fc f []
1254 = case lookupCtxt Nothing f (idris_implicits ist) of
1255 [] -> Right $ PRef fc f
1256 alts -> if (any (all imp) alts)
1257 then aiFn False ist fc f [] -- use it as a constructor
1258 else Right $ PRef fc f
1259 where imp (PExp _ _ _) = False
1260 imp _ = True
1261aiFn inpat ist fc f as
1262 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1263aiFn inpat ist fc f as
1264 -- This is where namespaces get resolved by adding PAlternative
1265 = case lookupCtxtName Nothing f (idris_implicits ist) of
1266 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1267 [] -> if f `elem` idris_metavars ist
1268 then Right $ PApp fc (PRef fc f) as
1269 else Right $ mkPApp fc (length as) (PRef fc f) as
1270 alts -> Right $
1271 PAlternative $
1272 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1273 (insertImpl ns as)) alts
1274 where
1275 insertImpl :: [PArg] -> [PArg] -> [PArg]
1276 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1277 PExp p l tm : insertImpl ps given
1278 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1279 PConstraint p l tm : insertImpl ps given
1280 insertImpl (PConstraint p l ty : ps) given =
1281 PConstraint p l (PResolveTC fc) : insertImpl ps given
1282 insertImpl (PImp p l n ty : ps) given =
1283 case find n given [] of
1284 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
1285 Nothing -> PImp p l n Placeholder : insertImpl ps given
1286 insertImpl (PTacImplicit p l n sc ty : ps) given =
1287 case find n given [] of
1288 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1289 Nothing -> PTacImplicit p l n sc sc
1290 : insertImpl ps given
1291 insertImpl expected [] = []
1292 insertImpl _ given = given
1294 find n [] acc = Nothing
1295 find n (PImp _ _ n' t : gs) acc
1296 | n == n' = Just (t, reverse acc ++ gs)
1297 find n (g : gs) acc = find n gs (g : acc)
1299mkPApp fc a f [] = f
1300mkPApp fc a f as = let rest = drop a as in
1301 appRest fc (PApp fc f (take a as)) rest
1302 where
1303 appRest fc f [] = f
1304 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1306-- Find 'static' argument positions
1307-- (the declared ones, plus any names in argument position in the declared
1308-- statics)
1309-- FIXME: It's possible that this really has to happen after elaboration
1311findStatics :: IState -> PTerm -> (PTerm, [Bool])
1312findStatics ist tm = trace (showImp True tm) $
1313 let (ns, ss) = fs tm in
1314 runState (pos ns ss tm) []
1315 where fs (PPi p n t sc)
1316 | Static <- pstatic p
1317 = let (ns, ss) = fs sc in
1318 (namesIn [] ist t : ns, n : ss)
1319 | otherwise = let (ns, ss) = fs sc in
1320 (ns, ss)
1321 fs _ = ([], [])
1323 inOne n ns = length (filter id (map (elem n) ns)) == 1
1325 pos ns ss (PPi p n t sc)
1326 | elem n ss = do sc' <- pos ns ss sc
1327 spos <- get
1328 put (True : spos)
1329 return (PPi (p { pstatic = Static }) n t sc')
1330 | otherwise = do sc' <- pos ns ss sc
1331 spos <- get
1332 put (False : spos)
1333 return (PPi p n t sc')
1334 pos ns ss t = return t
1336-- Debugging/logging stuff
1338dumpDecls :: [PDecl] -> String
1339dumpDecls [] = ""
1340dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1342dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1343dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1344dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1345dumpDecl (PData _ _ d) = showDImp True d
1346dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1347dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1348dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1349dumpDecl (PClass _ _ cs n ps ds)
1350 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1351dumpDecl (PInstance _ _ cs n _ t ds)
1352 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1353dumpDecl _ = "..."
1354-- dumpDecl (PImport i) = "import " ++ i
1356-- for 6.12/7 compatibility
1357data EitherErr a b = LeftErr a | RightOK b
1359instance Monad (EitherErr a) where
1360 return = RightOK
1362 (LeftErr e) >>= k = LeftErr e
1363 RightOK v >>= k = k v
1365toEither (LeftErr e) = Left e
1366toEither (RightOK ho) = Right ho
1368-- syntactic match of a against b, returning pair of variables in a
1369-- and what they match. Returns the pair that failed if not a match.
1371matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1372matchClause = matchClause' False
1374matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1375matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1376 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1378 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1379 fullApp x = x
1381 match' x y = match (fullApp x) (fullApp y)
1382 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1383 | PConstant (I _) <- getTm x = match (getTm x) x'
1384 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1385 | PConstant (I _) <- getTm x = match (getTm x) x'
1386 match (PApp _ f args) (PApp _ f' args')
1387 | length args == length args'
1388 = do mf <- match' f f'
1389 ms <- zipWithM matchArg args args'
1390 return (mf ++ concat ms)
1391-- match (PRef _ n) (PRef _ n') | n == n' = return []
1392-- | otherwise = Nothing
1393 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1394 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1395 match (PRef _ n) (PRef _ n') | n == n' = return []
1396 match (PRef _ n) tm
1397 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1398 = return [(n, tm)]
1399 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1400 mr <- match' r r'
1401 return (ml ++ mr)
1402 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1403 mr <- match r r'
1404 return (ml ++ mr)
1405 match (PTyped l r) x = match l x
1406 match x (PTyped l r) = match x l
1407 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1408 mr <- match' r r'
1409 return (ml ++ mr)
1410 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1411 mt <- match' t t'
1412 mr <- match' r r'
1413 return (ml ++ mt ++ mr)
1414 match (PAlternative as) (PAlternative as')
1415 = do ms <- zipWithM match' as as'
1416 return (concat ms)
1417 match a@(PAlternative as) b
1418 = do let ms = zipWith match' as (repeat b)
1419 case (rights (map toEither ms)) of
1420 (x: _) -> return x
1421 _ -> LeftErr (a, b)
1422 match (PCase _ _ _) _ = return [] -- lifted out
1423 match (PMetavar _) _ = return [] -- modified
1424 match (PQuote _) _ = return []
1425 match (PProof _) _ = return []
1426 match (PTactics _) _ = return []
1427 match (PRefl _) (PRefl _) = return []
1428 match (PResolveTC _) (PResolveTC _) = return []
1429 match (PTrue _) (PTrue _) = return []
1430 match (PFalse _) (PFalse _) = return []
1431 match (PReturn _) (PReturn _) = return []
1432 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1433 ms <- match' s s'
1434 return (mt ++ ms)
1435 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1436 ms <- match' s s'
1437 return (mt ++ ms)
1438 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1439 mty <- match' ty ty'
1440 ms <- match' s s'
1441 return (mt ++ mty ++ ms)
1442 match (PHidden x) (PHidden y) = match' x y
1443 match Placeholder _ = return []
1444-- match _ Placeholder = return []
1445 match (PResolveTC _) _ = return []
1446 match a b | a == b = return []
1447 | otherwise = LeftErr (a, b)
1449 checkRpts (RightOK ms) = check ms where
1450 check ((n,t):xs)
1451 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1452 then Left (t, t')
1453 else check xs
1454 check (_:xs) = check xs
1455 check [] = Right ms
1456 checkRpts (LeftErr x) = Left x
1458substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1459substMatches [] t = t
1460substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1462substMatch :: Name -> PTerm -> PTerm -> PTerm
1463substMatch n tm t = sm t where
1464 sm (PRef _ n') | n == n' = tm
1465 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1466 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1467 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1468 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1469 sm (PEq f x y) = PEq f (sm x) (sm y)
1470 sm (PTyped x y) = PTyped (sm x) (sm y)
1471 sm (PPair f x y) = PPair f (sm x) (sm y)
1472 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1473 sm (PAlternative as) = PAlternative (map sm as)
1474 sm (PHidden x) = PHidden (sm x)
1475 sm x = x
1477shadow :: Name -> Name -> PTerm -> PTerm
1478shadow n n' t = sm t where
1479 sm (PRef fc x) | n == x = PRef fc n'
1480 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1481 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1482 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1483 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1484 sm (PEq f x y) = PEq f (sm x) (sm y)
1485 sm (PTyped x y) = PTyped (sm x) (sm y)
1486 sm (PPair f x y) = PPair f (sm x) (sm y)
1487 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1488 sm (PAlternative as) = PAlternative (map sm as)
1489 sm (PHidden x) = PHidden (sm x)
1490 sm x = x