git.iko.soy/Idris-dev
on dcba960 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1497 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 Bool 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) })
151-- Add a class instance function. Dodgy hack: Put integer instances first in the
152-- list so they are resolved by default.
154addInstance :: Bool -> Name -> Name -> Idris ()
155addInstance int n i
156 = do ist <- get
157 case lookupCtxt Nothing n (idris_classes ist) of
158 [CI a b c d ins] ->
159 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
160 put (ist { idris_classes = cs })
161 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
162 put (ist { idris_classes = cs })
163 where addI i ins | int = i : ins
164 | otherwise = ins ++ [i]
166addClass :: Name -> ClassInfo -> Idris ()
167addClass n i
168 = do ist <- get
169 let i' = case lookupCtxt Nothing n (idris_classes ist) of
170 [c] -> c { class_instances = class_instances i }
171 _ -> i
172 put (ist { idris_classes = addDef n i' (idris_classes ist) })
174addIBC :: IBCWrite -> Idris ()
175addIBC ibc@(IBCDef n)
176 = do i <- get
177 when (notDef (ibc_write i)) $
178 put (i { ibc_write = ibc : ibc_write i })
179 where notDef [] = True
180 notDef (IBCDef n': is) | n == n' = False
181 notDef (_ : is) = notDef is
182addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
184clearIBC :: Idris ()
185clearIBC = do i <- get; put (i { ibc_write = [] })
187getHdrs :: Idris [String]
188getHdrs = do i <- get; return (idris_hdrs i)
190setErrLine :: Int -> Idris ()
191setErrLine x = do i <- get;
192 case (errLine i) of
193 Nothing -> put (i { errLine = Just x })
194 Just _ -> return ()
196clearErr :: Idris ()
197clearErr = do i <- get
198 put (i { errLine = Nothing })
200getSO :: Idris (Maybe String)
201getSO = do i <- get
202 return (compiled_so i)
204setSO :: Maybe String -> Idris ()
205setSO s = do i <- get
206 put (i { compiled_so = s })
208getIState :: Idris IState
209getIState = get
211putIState :: IState -> Idris ()
212putIState = put
214getName :: Idris Int
215getName = do i <- get;
216 let idx = idris_name i;
217 put (i { idris_name = idx + 1 })
218 return idx
220checkUndefined :: FC -> Name -> Idris ()
221checkUndefined fc n
222 = do i <- getContext
223 case lookupTy Nothing n i of
224 (_:_) -> fail $ show fc ++ ":" ++
225 show n ++ " already defined"
226 _ -> return ()
228setContext :: Context -> Idris ()
229setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
231updateContext :: (Context -> Context) -> Idris ()
232updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
234addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
235addConstraints fc (v, cs)
236 = do i <- get
237 let ctxt = tt_ctxt i
238 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
239 next_tvar = v }
240 let ics = zip cs (repeat fc) ++ idris_constraints i
241 put (i { tt_ctxt = ctxt', idris_constraints = ics })
243addDeferred :: [(Name, Type)] -> Idris ()
244addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
245 i <- get
246 put (i { idris_metavars = map fst ns ++ idris_metavars i })
247 where tidyNames used (Bind (MN i x) b sc)
248 = let n' = uniqueName (UN x) used in
249 Bind n' b $ tidyNames (n':used) sc
250 tidyNames used (Bind n b sc)
251 = let n' = uniqueName n used in
252 Bind n' b $ tidyNames (n':used) sc
253 tidyNames used b = b
255solveDeferred :: Name -> Idris ()
256solveDeferred n = do i <- get
257 put (i { idris_metavars = idris_metavars i \\ [n] })
259iputStrLn :: String -> Idris ()
260iputStrLn = liftIO . putStrLn
262iWarn :: FC -> String -> Idris ()
263iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
265setLogLevel :: Int -> Idris ()
266setLogLevel l = do i <- get
267 let opts = idris_options i
268 let opt' = opts { opt_logLevel = l }
269 put (i { idris_options = opt' } )
271logLevel :: Idris Int
272logLevel = do i <- get
273 return (opt_logLevel (idris_options i))
275useREPL :: Idris Bool
276useREPL = do i <- get
277 return (opt_repl (idris_options i))
279setREPL :: Bool -> Idris ()
280setREPL t = do i <- get
281 let opts = idris_options i
282 let opt' = opts { opt_repl = t }
283 put (i { idris_options = opt' })
285verbose :: Idris Bool
286verbose = do i <- get
287 return (opt_verbose (idris_options i))
289setVerbose :: Bool -> Idris ()
290setVerbose t = do i <- get
291 let opts = idris_options i
292 let opt' = opts { opt_verbose = t }
293 put (i { idris_options = opt' })
295typeInType :: Idris Bool
296typeInType = do i <- get
297 return (opt_typeintype (idris_options i))
299setTypeInType :: Bool -> Idris ()
300setTypeInType t = do i <- get
301 let opts = idris_options i
302 let opt' = opts { opt_typeintype = t }
303 put (i { idris_options = opt' })
305coverage :: Idris Bool
306coverage = do i <- get
307 return (opt_coverage (idris_options i))
309setCoverage :: Bool -> Idris ()
310setCoverage t = do i <- get
311 let opts = idris_options i
312 let opt' = opts { opt_coverage = t }
313 put (i { idris_options = opt' })
315impShow :: Idris Bool
316impShow = do i <- get
317 return (opt_showimp (idris_options i))
319setImpShow :: Bool -> Idris ()
320setImpShow t = do i <- get
321 let opts = idris_options i
322 let opt' = opts { opt_showimp = t }
323 put (i { idris_options = opt' })
325logLvl :: Int -> String -> Idris ()
326logLvl l str = do i <- get
327 let lvl = opt_logLevel (idris_options i)
328 when (lvl >= l)
329 $ do liftIO (putStrLn str)
330 put (i { idris_log = idris_log i ++ str ++ "\n" } )
332iLOG :: String -> Idris ()
333iLOG = logLvl 1
335noErrors :: Idris Bool
336noErrors = do i <- get
337 case errLine i of
338 Nothing -> return True
339 _ -> return False
341setTypeCase :: Bool -> Idris ()
342setTypeCase t = do i <- get
343 let opts = idris_options i
344 let opt' = opts { opt_typecase = t }
345 put (i { idris_options = opt' })
347-- Commands in the REPL
349data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
350 | Reload | Edit
351 | Compile String | Execute | ExecVal PTerm
352 | Metavars | Prove Name | AddProof | Universes
353 | TTShell
354 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name | Info Name
355 | NOP
357-- Parsed declarations
359data Fixity = Infixl { prec :: Int }
360 | Infixr { prec :: Int }
361 | InfixN { prec :: Int }
362 | PrefixN { prec :: Int }
363 deriving Eq
364{-!
365deriving instance Binary Fixity
366!-}
368instance Show Fixity where
369 show (Infixl i) = "infixl " ++ show i
370 show (Infixr i) = "infixr " ++ show i
371 show (InfixN i) = "infix " ++ show i
372 show (PrefixN i) = "prefix " ++ show i
374data FixDecl = Fix Fixity String
375 deriving (Show, Eq)
376{-!
377deriving instance Binary FixDecl
378!-}
380instance Ord FixDecl where
381 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
384data Static = Static | Dynamic
385 deriving (Show, Eq)
386{-!
387deriving instance Binary Static
388!-}
390-- Mark bindings with their explicitness, and laziness
391data Plicity = Imp { plazy :: Bool,
392 pstatic :: Static }
393 | Exp { plazy :: Bool,
394 pstatic :: Static }
395 | Constraint { plazy :: Bool,
396 pstatic :: Static }
397 | TacImp { plazy :: Bool,
398 pstatic :: Static,
399 pscript :: PTerm }
400 deriving (Show, Eq)
402{-!
403deriving instance Binary Plicity
404!-}
406impl = Imp False Dynamic
407expl = Exp False Dynamic
408constraint = Constraint False Dynamic
409tacimpl = TacImp False Dynamic
411data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
412 | Specialise [Name] -- specialise it, freeze these names
413 deriving (Show, Eq)
414{-!
415deriving instance Binary FnOpt
416!-}
418type FnOpts = [FnOpt]
420inlinable :: FnOpts -> Bool
421inlinable = elem Inlinable
423data PDecl' t = PFix FC Fixity [String] -- fixity declaration
424 | PTy SyntaxInfo FC FnOpts Name t -- type declaration
425 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
426 | PData SyntaxInfo FC (PData' t) -- data declaration
427 | PParams FC [(Name, t)] [PDecl' t] -- params block
428 | PNamespace String [PDecl' t] -- new namespace
429 | PRecord SyntaxInfo FC Name t Name t -- record declaration
430 | PClass SyntaxInfo FC
431 [t] -- constraints
432 Name
433 [(Name, t)] -- parameters
434 [PDecl' t] -- declarations
435 | PInstance SyntaxInfo FC [t] -- constraints
436 Name -- class
437 [t] -- parameters
438 t -- full instance type
439 [PDecl' t]
440 | PDSL Name (DSL' t)
441 | PSyntax FC Syntax
442 | PDirective (Idris ())
443 deriving Functor
445data PClause' t = PClause FC Name t [t] t [PDecl' t]
446 | PWith FC Name t [t] t [PDecl' t]
447 | PClauseR FC [t] t [PDecl' t]
448 | PWithR FC [t] t [PDecl' t]
449 deriving Functor
451data PData' t = PDatadecl { d_name :: Name,
452 d_tcon :: t,
453 d_cons :: [(Name, t, FC)] }
454 deriving Functor
456-- Handy to get a free function for applying PTerm -> PTerm functions
457-- across a program, by deriving Functor
459type PDecl = PDecl' PTerm
460type PData = PData' PTerm
461type PClause = PClause' PTerm
463-- get all the names declared in a decl
465declared :: PDecl -> [Name]
466declared (PFix _ _ _) = []
467declared (PTy _ _ _ n t) = [n]
468declared (PClauses _ _ n _) = [] -- not a declaration
469declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
470 where fstt (a, _, _) = a
471declared (PParams _ _ ds) = concatMap declared ds
472declared (PNamespace _ ds) = concatMap declared ds
473-- declared (PImport _) = []
475updateN :: [(Name, Name)] -> Name -> Name
476updateN ns n | Just n' <- lookup n ns = n'
477updateN _ n = n
479updateNs :: [(Name, Name)] -> PTerm -> PTerm
480updateNs [] t = t
481updateNs ns t = mapPT updateRef t
482 where updateRef (PRef fc f) = PRef fc (updateN ns f)
483 updateRef t = t
485-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
486-- updateDNs [] t = t
487-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
488-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
489-- where updateCNs ns (PClause n l ts r ds)
490-- = PClause (updateN ns n) (fmap (updateNs ns) l)
491-- (map (fmap (updateNs ns)) ts)
492-- (fmap (updateNs ns) r)
493-- (map (updateDNs ns) ds)
494-- updateDNs ns c = c
496-- High level language terms
498data PTerm = PQuote Raw
499 | PRef FC Name
500 | PLam Name PTerm PTerm
501 | PPi Plicity Name PTerm PTerm
502 | PLet Name PTerm PTerm PTerm
503 | PTyped PTerm PTerm -- term with explicit type
504 | PApp FC PTerm [PArg]
505 | PCase FC PTerm [(PTerm, PTerm)]
506 | PTrue FC
507 | PFalse FC
508 | PRefl FC
509 | PResolveTC FC
510 | PEq FC PTerm PTerm
511 | PPair FC PTerm PTerm
512 | PDPair FC PTerm PTerm PTerm
513 | PAlternative [PTerm]
514 | PHidden PTerm -- irrelevant or hidden pattern
515 | PSet
516 | PConstant Const
517 | Placeholder
518 | PDoBlock [PDo]
519 | PIdiom FC PTerm
520 | PReturn FC
521 | PMetavar Name
522 | PProof [PTactic]
523 | PTactics [PTactic] -- as PProof, but no auto solving
524 | PElabError Err -- error to report on elaboration
525 | PImpossible -- special case for declaring when an LHS can't typecheck
526 deriving Eq
527{-!
528deriving instance Binary PTerm
529!-}
531mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
532mapPT f t = f (mpt t) where
533 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
534 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
535 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
536 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
537 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
538 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
539 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
540 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
541 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
542 mpt (PAlternative as) = PAlternative (map (mapPT f) as)
543 mpt (PHidden t) = PHidden (mapPT f t)
544 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
545 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
546 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
547 mpt x = x
550data PTactic' t = Intro [Name] | Intros | Focus Name
551 | Refine Name [Bool] | Rewrite t | LetTac Name t
552 | Exact t | Compute | Trivial
553 | Solve
554 | Attack
555 | ProofState | ProofTerm | Undo
556 | Try (PTactic' t) (PTactic' t)
557 | TSeq (PTactic' t) (PTactic' t)
558 | Qed | Abandon
559 deriving (Show, Eq, Functor)
560{-!
561deriving instance Binary PTactic'
562!-}
564type PTactic = PTactic' PTerm
566data PDo' t = DoExp FC t
567 | DoBind FC Name t
568 | DoBindP FC t t
569 | DoLet FC Name t t
570 | DoLetP FC t t
571 deriving (Eq, Functor)
572{-!
573deriving instance Binary PDo'
574!-}
576type PDo = PDo' PTerm
578-- The priority gives a hint as to elaboration order. Best to elaborate
579-- things early which will help give a more concrete type to other
580-- variables, e.g. a before (interpTy a).
582data PArg' t = PImp { priority :: Int,
583 lazyarg :: Bool, pname :: Name, getTm :: t }
584 | PExp { priority :: Int,
585 lazyarg :: Bool, getTm :: t }
586 | PConstraint { priority :: Int,
587 lazyarg :: Bool, getTm :: t }
588 | PTacImplicit { priority :: Int,
589 lazyarg :: Bool, pname :: Name,
590 getScript :: t,
591 getTm :: t }
592 deriving (Show, Eq, Functor)
593{-!
594deriving instance Binary PArg'
595!-}
597pimp = PImp 0 True
598pexp = PExp 0 False
599pconst = PConstraint 0 False
600ptacimp = PTacImplicit 0 True
602type PArg = PArg' PTerm
604-- Type class data
606data ClassInfo = CI { instanceName :: Name,
607 class_methods :: [(Name, (FnOpts, PTerm))],
608 class_defaults :: [(Name, Name)], -- method name -> default impl
609 class_params :: [Name],
610 class_instances :: [Name] }
611 deriving Show
612{-!
613deriving instance Binary ClassInfo
614!-}
616data OptInfo = Optimise { collapsible :: Bool,
617 forceable :: [Int], -- argument positions
618 recursive :: [Int] }
619 deriving Show
620{-!
621deriving instance Binary OptInfo
622!-}
625data TypeInfo = TI { con_names :: [Name] }
626 deriving Show
627{-!
628deriving instance Binary TypeInfo
629!-}
631-- Syntactic sugar info
633data DSL' t = DSL { dsl_bind :: t,
634 dsl_return :: t,
635 dsl_apply :: t,
636 dsl_pure :: t,
637 dsl_var :: Maybe t,
638 index_first :: Maybe t,
639 index_next :: Maybe t,
640 dsl_lambda :: Maybe t,
641 dsl_let :: Maybe t
642 }
643 deriving (Show, Functor)
644{-!
645deriving instance Binary DSL'
646!-}
648type DSL = DSL' PTerm
650data SynContext = PatternSyntax | TermSyntax | AnySyntax
651 deriving Show
652{-!
653deriving instance Binary SynContext
654!-}
656data Syntax = Rule [SSymbol] PTerm SynContext
657 deriving Show
658{-!
659deriving instance Binary Syntax
660!-}
662data SSymbol = Keyword Name
663 | Symbol String
664 | Expr Name
665 | SimpleExpr Name
666 deriving Show
667{-!
668deriving instance Binary SSymbol
669!-}
671initDSL = DSL (PRef f (UN ">>="))
672 (PRef f (UN "return"))
673 (PRef f (UN "<$>"))
674 (PRef f (UN "pure"))
675 Nothing
676 Nothing
677 Nothing
678 Nothing
679 Nothing
680 where f = FC "(builtin)" 0
682data SyntaxInfo = Syn { using :: [(Name, PTerm)],
683 syn_params :: [(Name, PTerm)],
684 syn_namespace :: [String],
685 no_imp :: [Name],
686 decoration :: Name -> Name,
687 inPattern :: Bool,
688 dsl_info :: DSL }
689 deriving Show
691defaultSyntax = Syn [] [] [] [] id False initDSL
693expandNS :: SyntaxInfo -> Name -> Name
694expandNS syn n@(NS _ _) = n
695expandNS syn n = case syn_namespace syn of
696 [] -> n
697 xs -> NS n xs
700--- Pretty printing declarations and terms
702instance Show PTerm where
703 show tm = showImp False tm
705instance Show PDecl where
706 show d = showDeclImp False d
708instance Show PClause where
709 show c = showCImp True c
711instance Show PData where
712 show d = showDImp False d
714showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
715showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty
716showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
717showDeclImp _ (PData _ _ d) = show d
719showCImp :: Bool -> PClause -> String
720showCImp impl (PClause _ n l ws r w)
721 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
722 ++ " where " ++ show w
723 where
724 showWs [] = ""
725 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
726showCImp impl (PWith _ n l ws r w)
727 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
728 ++ " { " ++ show w ++ " } "
729 where
730 showWs [] = ""
731 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
734showDImp :: Bool -> PData -> String
735showDImp impl (PDatadecl n ty cons)
736 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
737 ++ showSep "\n\t| "
738 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
740getImps :: [PArg] -> [(Name, PTerm)]
741getImps [] = []
742getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
743getImps (_ : xs) = getImps xs
745getExps :: [PArg] -> [PTerm]
746getExps [] = []
747getExps (PExp _ _ tm : xs) = tm : getExps xs
748getExps (_ : xs) = getExps xs
750getConsts :: [PArg] -> [PTerm]
751getConsts [] = []
752getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
753getConsts (_ : xs) = getConsts xs
755getAll :: [PArg] -> [PTerm]
756getAll = map getTm
758showImp :: Bool -> PTerm -> String
759showImp impl tm = se 10 tm where
760 se p (PQuote r) = "![" ++ show r ++ "]"
761 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
762 else showbasic n
763 where showbasic n@(UN _) = show n
764 showbasic (MN _ s) = s
765 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
766 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
767 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
768 " in " ++ se 10 sc
769 se p (PPi (Exp l s) n ty sc)
770 | n `elem` allNamesIn sc || impl
771 = bracket p 2 $
772 if l then "|(" else "(" ++
773 show n ++ " : " ++ se 10 ty ++
774 ") " ++ st ++
775 "-> " ++ se 10 sc
776 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
777 where st = case s of
778 Static -> "[static] "
779 _ -> ""
780 se p (PPi (Imp l s) n ty sc)
781 | impl = bracket p 2 $ if l then "|{" else "{" ++
782 show n ++ " : " ++ se 10 ty ++
783 "} " ++ st ++ "-> " ++ se 10 sc
784 | otherwise = se 10 sc
785 where st = case s of
786 Static -> "[static] "
787 _ -> ""
788 se p (PPi (Constraint _ _) n ty sc)
789 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
790 se p (PApp _ (PRef _ f) [])
791 | not impl = show f
792 se p (PApp _ (PRef _ op@(UN (f:_))) args)
793 | length (getExps args) == 2 && not impl && not (isAlpha f)
794 = let [l, r] = getExps args in
795 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
796 se p (PApp _ f as)
797 = let args = getExps as in
798 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
799 else concatMap seArg args
800 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
801 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
802 se p (PHidden tm) = "." ++ se 0 tm
803 se p (PRefl _) = "refl"
804 se p (PResolveTC _) = "resolvetc"
805 se p (PTrue _) = "()"
806 se p (PFalse _) = "_|_"
807 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
808 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
809 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
810 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
811 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
812 se p PSet = "Set"
813 se p (PConstant c) = show c
814 se p (PProof ts) = "proof { " ++ show ts ++ "}"
815 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
816 se p (PMetavar n) = "?" ++ show n
817 se p (PReturn f) = "return"
818 se p PImpossible = "impossible"
819 se p Placeholder = "_"
820 se p (PDoBlock _) = "do block show not implemented"
821 se p (PElabError s) = show s
822-- se p x = "Not implemented"
824 sArg (PImp _ _ n tm) = siArg (n, tm)
825 sArg (PExp _ _ tm) = seArg tm
826 sArg (PConstraint _ _ tm) = scArg tm
827 sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
829 seArg arg = " " ++ se 0 arg
830 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
831 scArg val = " {{" ++ se 10 val ++ "}}"
832 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
834 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
835 | otherwise = str
837allNamesIn :: PTerm -> [Name]
838allNamesIn tm = nub $ ni [] tm
839 where
840 ni env (PRef _ n)
841 | not (n `elem` env) = [n]
842 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
843 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
844 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
845 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
846 ni env (PHidden tm) = ni env tm
847 ni env (PEq _ l r) = ni env l ++ ni env r
848 ni env (PTyped l r) = ni env l ++ ni env r
849 ni env (PPair _ l r) = ni env l ++ ni env r
850 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
851 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
852 ni env (PAlternative ls) = concatMap (ni env) ls
853 ni env _ = []
855namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
856namesIn uvars ist tm = nub $ ni [] tm
857 where
858 ni env (PRef _ n)
859 | not (n `elem` env)
860 = case lookupTy Nothing n (tt_ctxt ist) of
861 [] -> [n]
862 _ -> if n `elem` (map fst uvars) then [n] else []
863 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
864 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
865 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
866 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
867 ni env (PEq _ l r) = ni env l ++ ni env r
868 ni env (PTyped l r) = ni env l ++ ni env r
869 ni env (PPair _ l r) = ni env l ++ ni env r
870 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
871 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
872 ni env (PAlternative as) = concatMap (ni env) as
873 ni env (PHidden tm) = ni env tm
874 ni env _ = []
876-- For inferring types of things
878bi = FC "builtin" 0
880inferTy = MN 0 "__Infer"
881inferCon = MN 0 "__infer"
882inferDecl = PDatadecl inferTy
883 PSet
884 [(inferCon, PPi impl (MN 0 "A") PSet (
885 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
886 (PRef bi inferTy)), bi)]
888infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
889infP = P (TCon 6 0) inferTy (Set (UVal 0))
891getInferTerm, getInferType :: Term -> Term
892getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
893getInferTerm (App (App _ _) tm) = tm
894getInferTerm tm = error ("getInferTerm " ++ show tm)
896getInferType (Bind n b sc) = Bind n b $ getInferType sc
897getInferType (App (App _ ty) _) = ty
899-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
901primNames = [unitTy, unitCon,
902 falseTy, pairTy, pairCon,
903 eqTy, eqCon, inferTy, inferCon]
905unitTy = MN 0 "__Unit"
906unitCon = MN 0 "__II"
907unitDecl = PDatadecl unitTy PSet
908 [(unitCon, PRef bi unitTy, bi)]
910falseTy = MN 0 "__False"
911falseDecl = PDatadecl falseTy PSet []
913pairTy = MN 0 "__Pair"
914pairCon = MN 0 "__MkPair"
915pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
916 [(pairCon, PPi impl (n "A") PSet (
917 PPi impl (n "B") PSet (
918 PPi expl (n "a") (PRef bi (n "A")) (
919 PPi expl (n "b") (PRef bi (n "B"))
920 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
921 pexp (PRef bi (n "B"))])))), bi)]
922 where n a = MN 0 a
924eqTy = UN "="
925eqCon = UN "refl"
926eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
927 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
928 PSet)
929 [(eqCon, PPi impl (n "a") PSet (
930 PPi impl (n "x") (PRef bi (n "a"))
931 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
932 pimp (n "b") Placeholder,
933 pexp (PRef bi (n "x")),
934 pexp (PRef bi (n "x"))])), bi)]
935 where n a = MN 0 a
937-- Defined in builtins.idr
938sigmaTy = UN "Exists"
939existsCon = UN "Ex_intro"
941piBind :: [(Name, PTerm)] -> PTerm -> PTerm
942piBind [] t = t
943piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
945tcname (UN ('@':_)) = True
946tcname (NS n _) = tcname n
947tcname _ = False
949-- Dealing with parameters
951expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
952expandParams dec ps ns tm = en tm
953 where
954 -- if we shadow a name (say in a lambda binding) that is used in a call to
955 -- a lifted function, we need access to both names - once in the scope of the
956 -- binding and once to call the lifted functions. So we'll explicitly shadow
957 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
958 -- but we didn't...)
960 mkShadow (UN n) = MN 0 n
961 mkShadow (MN i n) = MN (i+1) n
962 mkShadow (NS x s) = NS (mkShadow x) s
964 en (PLam n t s)
965 | n `elem` map fst ps
966 = let n' = mkShadow n in
967 PLam n' (en t) (en (shadow n n' s))
968 | otherwise = PLam n (en t) (en s)
969 en (PPi p n t s)
970 | n `elem` map fst ps
971 = let n' = mkShadow n in
972 PPi p n' (en t) (en (shadow n n' s))
973 | otherwise = PPi p n (en t) (en s)
974 en (PLet n ty v s)
975 | n `elem` map fst ps
976 = let n' = mkShadow n in
977 PLet n' (en ty) (en v) (en (shadow n n' s))
978 | otherwise = PLet n (en ty) (en v) (en s)
979 en (PEq f l r) = PEq f (en l) (en r)
980 en (PTyped l r) = PTyped (en l) (en r)
981 en (PPair f l r) = PPair f (en l) (en r)
982 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
983 en (PAlternative as) = PAlternative (map en as)
984 en (PHidden t) = PHidden (en t)
985 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
986 en (PProof ts) = PProof (map (fmap en) ts)
987 en (PTactics ts) = PTactics (map (fmap en) ts)
989 en (PQuote (Var n))
990 | n `elem` ns = PQuote (Var (dec n))
991 en (PApp fc (PRef fc' n) as)
992 | n `elem` ns = PApp fc (PRef fc' (dec n))
993 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
994 en (PRef fc n)
995 | n `elem` ns = PApp fc (PRef fc (dec n))
996 (map (pexp . (PRef fc)) (map fst ps))
997 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
998 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
999 en t = t
1001expandParamsD :: IState ->
1002 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1003expandParamsD ist dec ps ns (PTy syn fc o n ty)
1004 = if n `elem` ns
1005 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
1006 else PTy syn fc o n (expandParams dec ps ns ty)
1007expandParamsD ist dec ps ns (PClauses fc opts n cs)
1008 = let n' = if n `elem` ns then dec n else n in
1009 PClauses fc opts n' (map expandParamsC cs)
1010 where
1011 expandParamsC (PClause fc n lhs ws rhs ds)
1012 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1013 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1014 n' = if n `elem` ns then dec n else n in
1015 PClause fc n' (expandParams dec ps'' ns lhs)
1016 (map (expandParams dec ps'' ns) ws)
1017 (expandParams dec ps'' ns rhs)
1018 (map (expandParamsD ist dec ps'' ns) ds)
1019 expandParamsC (PWith fc n lhs ws wval ds)
1020 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1021 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1022 n' = if n `elem` ns then dec n else n in
1023 PWith fc n' (expandParams dec ps'' ns lhs)
1024 (map (expandParams dec ps'' ns) ws)
1025 (expandParams dec ps'' ns wval)
1026 (map (expandParamsD ist dec ps'' ns) ds)
1027 updateps yn nm [] = []
1028 updateps yn nm (((a, t), i):as)
1029 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1030 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
1032expandParamsD ist dec ps ns d = d
1034-- Calculate a priority for a type, for deciding elaboration order
1035-- * if it's just a type variable or concrete type, do it early (0)
1036-- * if there's only type variables and injective constructors, do it next (1)
1037-- * if there's a function type, next (2)
1038-- * finally, everything else (3)
1040getPriority :: IState -> PTerm -> Int
1041getPriority i tm = pri tm
1042 where
1043 pri (PRef _ n) =
1044 case lookupP Nothing n (tt_ctxt i) of
1045 ((P (DCon _ _) _ _):_) -> 1
1046 ((P (TCon _ _) _ _):_) -> 1
1047 ((P Ref _ _):_) -> 4
1048 [] -> 0 -- must be locally bound, if it's not an error...
1049 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1050 pri (PTrue _) = 0
1051 pri (PFalse _) = 0
1052 pri (PRefl _) = 1
1053 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1054 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1055 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1056 pri (PTyped l r) = pri l
1057 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
1058 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1059 pri (PAlternative as) = maximum (map pri as)
1060 pri (PConstant _) = 0
1061 pri Placeholder = 1
1062 pri _ = 3
1064addStatics :: Name -> Term -> PTerm -> Idris ()
1065addStatics n tm ptm =
1066 do let (statics, dynamics) = initStatics tm ptm
1067 let stnames = nub $ concatMap freeNames (map snd statics)
1068 let dnames = nub $ concatMap freeNames (map snd dynamics)
1069 when (not (null statics)) $
1070 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
1071 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1072 let statics' = nub $ map fst statics ++
1073 filter (\x -> not (elem x dnames)) stnames
1074 let stpos = staticList statics' tm
1075 i <- get
1076 put (i { idris_statics = addDef n stpos (idris_statics i) })
1077 addIBC (IBCStatic n)
1078 where
1079 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1080 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1081 if pstatic p == Static then ((n, ty) : static, dynamic)
1082 else (static, (n, ty) : dynamic)
1083 initStatics t pt = ([], [])
1085 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1086 staticList _ _ = []
1088-- Dealing with implicit arguments
1090-- Add implicit Pi bindings for any names in the term which appear in an
1091-- argument position.
1093-- This has become a right mess already. Better redo it some time...
1095implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1096implicit syn n ptm
1097 = do i <- get
1098 let (tm', impdata) = implicitise syn i ptm
1099-- let (tm'', spos) = findStatics i tm'
1100 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
1101 addIBC (IBCImp n)
1102 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1103-- i <- get
1104-- put (i { idris_statics = addDef n spos (idris_statics i) })
1105 return tm'
1107implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
1108implicitise syn ist tm
1109 = let (declimps, ns') = execState (imps True [] tm) ([], [])
1110 ns = ns' \\ (map fst pvars ++ no_imp syn) in
1111 if null ns
1112 then (tm, reverse declimps)
1113 else implicitise syn ist (pibind uvars ns tm)
1114 where
1115 uvars = using syn
1116 pvars = syn_params syn
1118 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1119 | otherwise = x : dropAll xs ys
1120 dropAll [] ys = []
1122 imps top env (PApp _ f as)
1123 = do (decls, ns) <- get
1124 let isn = concatMap (namesIn uvars ist) (map getTm as)
1125 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1126 imps top env (PPi (Imp l _) n ty sc)
1127 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1128 (decls , ns) <- get
1129 put (PImp (getPriority ist ty) l n ty : decls,
1130 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1131 imps True (n:env) sc
1132 imps top env (PPi (Exp l _) n ty sc)
1133 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1134 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1135 _ -> [])
1136 (decls, ns) <- get -- ignore decls in HO types
1137 put (PExp (getPriority ist ty) l ty : decls,
1138 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1139 imps True (n:env) sc
1140 imps top env (PPi (Constraint l _) n ty sc)
1141 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1142 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1143 _ -> [])
1144 (decls, ns) <- get -- ignore decls in HO types
1145 put (PConstraint 10 l ty : decls,
1146 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1147 imps True (n:env) sc
1148 imps top env (PPi (TacImp l _ scr) n ty sc)
1149 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1150 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1151 _ -> [])
1152 (decls, ns) <- get -- ignore decls in HO types
1153 put (PTacImplicit 10 l n scr ty : decls,
1154 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1155 imps True (n:env) sc
1156 imps top env (PEq _ 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 (PTyped l r)
1161 = imps top env l
1162 imps top env (PPair _ l r)
1163 = do (decls, ns) <- get
1164 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1165 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1166 imps top env (PDPair _ (PRef _ n) t r)
1167 = do (decls, ns) <- get
1168 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1169 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1170 imps top env (PDPair _ l t r)
1171 = do (decls, ns) <- get
1172 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1173 namesIn uvars ist r
1174 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1175 imps top env (PAlternative as)
1176 = do (decls, ns) <- get
1177 let isn = concatMap (namesIn uvars ist) as
1178 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1179 imps top env (PLam n ty sc)
1180 = do imps False env ty
1181 imps False (n:env) sc
1182 imps top env (PHidden tm) = imps False env tm
1183 imps top env _ = return ()
1185 pibind using [] sc = sc
1186 pibind using (n:ns) sc
1187 = case lookup n using of
1188 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
1189 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
1191-- Add implicit arguments in function calls
1192addImplPat :: IState -> PTerm -> PTerm
1193addImplPat = addImpl' True []
1195addImplBound :: IState -> [Name] -> PTerm -> PTerm
1196addImplBound ist ns = addImpl' False ns ist
1198addImpl :: IState -> PTerm -> PTerm
1199addImpl = addImpl' False []
1201-- TODO: in patterns, don't add implicits to function names guarded by constructors
1202-- and *not* inside a PHidden
1204addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1205addImpl' inpat env ist ptm = ai env ptm
1206 where
1207 ai env (PRef fc f)
1208 | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []
1209 ai env (PHidden (PRef fc f))
1210 | not (f `elem` env) = handleErr $ aiFn False ist fc f []
1211 ai env (PEq fc l r) = let l' = ai env l
1212 r' = ai env r in
1213 PEq fc l' r'
1214 ai env (PTyped l r) = let l' = ai env l
1215 r' = ai env r in
1216 PTyped l' r'
1217 ai env (PPair fc l r) = let l' = ai env l
1218 r' = ai env r in
1219 PPair fc l' r'
1220 ai env (PDPair fc l t r) = let l' = ai env l
1221 t' = ai env t
1222 r' = ai env r in
1223 PDPair fc l' t' r'
1224 ai env (PAlternative as) = let as' = map (ai env) as in
1225 PAlternative as'
1226 ai env (PApp fc (PRef _ f) as)
1227 | not (f `elem` env)
1228 = let as' = map (fmap (ai env)) as in
1229 handleErr $ aiFn False ist fc f as'
1230 ai env (PApp fc f as) = let f' = ai env f
1231 as' = map (fmap (ai env)) as in
1232 mkPApp fc 1 f' as'
1233 ai env (PCase fc c os) = let c' = ai env c
1234 os' = map (pmap (ai env)) os in
1235 PCase fc c' os'
1236 ai env (PLam n ty sc) = let ty' = ai env ty
1237 sc' = ai (n:env) sc in
1238 PLam n ty' sc'
1239 ai env (PLet n ty val sc)
1240 = let ty' = ai env ty
1241 val' = ai env val
1242 sc' = ai (n:env) sc in
1243 PLet n ty' val' sc'
1244 ai env (PPi p n ty sc) = let ty' = ai env ty
1245 sc' = ai (n:env) sc in
1246 PPi p n ty' sc'
1247 ai env (PHidden tm) = PHidden (ai env tm)
1248 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1249 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1250 ai env tm = tm
1252 handleErr (Left err) = PElabError err
1253 handleErr (Right x) = x
1255-- if in a pattern, and there are no arguments, and there's no possible
1256-- names with zero explicit arguments, don't add implicits.
1258aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1259aiFn True ist fc f []
1260 = case lookupCtxt Nothing f (idris_implicits ist) of
1261 [] -> Right $ PRef fc f
1262 alts -> if (any (all imp) alts)
1263 then aiFn False ist fc f [] -- use it as a constructor
1264 else Right $ PRef fc f
1265 where imp (PExp _ _ _) = False
1266 imp _ = True
1267aiFn inpat ist fc f as
1268 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1269aiFn inpat ist fc f as
1270 -- This is where namespaces get resolved by adding PAlternative
1271 = case lookupCtxtName Nothing f (idris_implicits ist) of
1272 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1273 [] -> if f `elem` idris_metavars ist
1274 then Right $ PApp fc (PRef fc f) as
1275 else Right $ mkPApp fc (length as) (PRef fc f) as
1276 alts -> Right $
1277 PAlternative $
1278 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1279 (insertImpl ns as)) alts
1280 where
1281 insertImpl :: [PArg] -> [PArg] -> [PArg]
1282 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1283 PExp p l tm : insertImpl ps given
1284 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1285 PConstraint p l tm : insertImpl ps given
1286 insertImpl (PConstraint p l ty : ps) given =
1287 PConstraint p l (PResolveTC fc) : insertImpl ps given
1288 insertImpl (PImp p l n ty : ps) given =
1289 case find n given [] of
1290 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
1291 Nothing -> PImp p l n Placeholder : insertImpl ps given
1292 insertImpl (PTacImplicit p l n sc ty : ps) given =
1293 case find n given [] of
1294 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1295 Nothing -> PTacImplicit p l n sc sc
1296 : insertImpl ps given
1297 insertImpl expected [] = []
1298 insertImpl _ given = given
1300 find n [] acc = Nothing
1301 find n (PImp _ _ n' t : gs) acc
1302 | n == n' = Just (t, reverse acc ++ gs)
1303 find n (g : gs) acc = find n gs (g : acc)
1305mkPApp fc a f [] = f
1306mkPApp fc a f as = let rest = drop a as in
1307 appRest fc (PApp fc f (take a as)) rest
1308 where
1309 appRest fc f [] = f
1310 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1312-- Find 'static' argument positions
1313-- (the declared ones, plus any names in argument position in the declared
1314-- statics)
1315-- FIXME: It's possible that this really has to happen after elaboration
1317findStatics :: IState -> PTerm -> (PTerm, [Bool])
1318findStatics ist tm = trace (showImp True tm) $
1319 let (ns, ss) = fs tm in
1320 runState (pos ns ss tm) []
1321 where fs (PPi p n t sc)
1322 | Static <- pstatic p
1323 = let (ns, ss) = fs sc in
1324 (namesIn [] ist t : ns, n : ss)
1325 | otherwise = let (ns, ss) = fs sc in
1326 (ns, ss)
1327 fs _ = ([], [])
1329 inOne n ns = length (filter id (map (elem n) ns)) == 1
1331 pos ns ss (PPi p n t sc)
1332 | elem n ss = do sc' <- pos ns ss sc
1333 spos <- get
1334 put (True : spos)
1335 return (PPi (p { pstatic = Static }) n t sc')
1336 | otherwise = do sc' <- pos ns ss sc
1337 spos <- get
1338 put (False : spos)
1339 return (PPi p n t sc')
1340 pos ns ss t = return t
1342-- Debugging/logging stuff
1344dumpDecls :: [PDecl] -> String
1345dumpDecls [] = ""
1346dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1348dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1349dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1350dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1351dumpDecl (PData _ _ d) = showDImp True d
1352dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1353dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1354dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1355dumpDecl (PClass _ _ cs n ps ds)
1356 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1357dumpDecl (PInstance _ _ cs n _ t ds)
1358 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1359dumpDecl _ = "..."
1360-- dumpDecl (PImport i) = "import " ++ i
1362-- for 6.12/7 compatibility
1363data EitherErr a b = LeftErr a | RightOK b
1365instance Monad (EitherErr a) where
1366 return = RightOK
1368 (LeftErr e) >>= k = LeftErr e
1369 RightOK v >>= k = k v
1371toEither (LeftErr e) = Left e
1372toEither (RightOK ho) = Right ho
1374-- syntactic match of a against b, returning pair of variables in a
1375-- and what they match. Returns the pair that failed if not a match.
1377matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1378matchClause = matchClause' False
1380matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1381matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1382 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1384 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1385 fullApp x = x
1387 match' x y = match (fullApp x) (fullApp y)
1388 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1389 | PConstant (I _) <- getTm x = match (getTm x) x'
1390 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1391 | PConstant (I _) <- getTm x = match (getTm x) x'
1392 match (PApp _ f args) (PApp _ f' args')
1393 | length args == length args'
1394 = do mf <- match' f f'
1395 ms <- zipWithM matchArg args args'
1396 return (mf ++ concat ms)
1397-- match (PRef _ n) (PRef _ n') | n == n' = return []
1398-- | otherwise = Nothing
1399 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1400 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1401 match (PRef _ n) (PRef _ n') | n == n' = return []
1402 match (PRef _ n) tm
1403 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1404 = return [(n, tm)]
1405 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1406 mr <- match' r r'
1407 return (ml ++ mr)
1408 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1409 mr <- match r r'
1410 return (ml ++ mr)
1411 match (PTyped l r) x = match l x
1412 match x (PTyped l r) = match x l
1413 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1414 mr <- match' r r'
1415 return (ml ++ mr)
1416 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1417 mt <- match' t t'
1418 mr <- match' r r'
1419 return (ml ++ mt ++ mr)
1420 match (PAlternative as) (PAlternative as')
1421 = do ms <- zipWithM match' as as'
1422 return (concat ms)
1423 match a@(PAlternative as) b
1424 = do let ms = zipWith match' as (repeat b)
1425 case (rights (map toEither ms)) of
1426 (x: _) -> return x
1427 _ -> LeftErr (a, b)
1428 match (PCase _ _ _) _ = return [] -- lifted out
1429 match (PMetavar _) _ = return [] -- modified
1430 match (PQuote _) _ = return []
1431 match (PProof _) _ = return []
1432 match (PTactics _) _ = return []
1433 match (PRefl _) (PRefl _) = return []
1434 match (PResolveTC _) (PResolveTC _) = return []
1435 match (PTrue _) (PTrue _) = return []
1436 match (PFalse _) (PFalse _) = return []
1437 match (PReturn _) (PReturn _) = return []
1438 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1439 ms <- match' s s'
1440 return (mt ++ ms)
1441 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1442 ms <- match' s s'
1443 return (mt ++ ms)
1444 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1445 mty <- match' ty ty'
1446 ms <- match' s s'
1447 return (mt ++ mty ++ ms)
1448 match (PHidden x) (PHidden y) = match' x y
1449 match Placeholder _ = return []
1450-- match _ Placeholder = return []
1451 match (PResolveTC _) _ = return []
1452 match a b | a == b = return []
1453 | otherwise = LeftErr (a, b)
1455 checkRpts (RightOK ms) = check ms where
1456 check ((n,t):xs)
1457 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1458 then Left (t, t')
1459 else check xs
1460 check (_:xs) = check xs
1461 check [] = Right ms
1462 checkRpts (LeftErr x) = Left x
1464substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1465substMatches [] t = t
1466substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1468substMatch :: Name -> PTerm -> PTerm -> PTerm
1469substMatch n tm t = sm t where
1470 sm (PRef _ n') | n == n' = tm
1471 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1472 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1473 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1474 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1475 sm (PEq f x y) = PEq f (sm x) (sm y)
1476 sm (PTyped x y) = PTyped (sm x) (sm y)
1477 sm (PPair f x y) = PPair f (sm x) (sm y)
1478 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1479 sm (PAlternative as) = PAlternative (map sm as)
1480 sm (PHidden x) = PHidden (sm x)
1481 sm x = x
1483shadow :: Name -> Name -> PTerm -> PTerm
1484shadow n n' t = sm t where
1485 sm (PRef fc x) | n == x = PRef fc n'
1486 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1487 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1488 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1489 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1490 sm (PEq f x y) = PEq f (sm x) (sm y)
1491 sm (PTyped x y) = PTyped (sm x) (sm y)
1492 sm (PPair f x y) = PPair f (sm x) (sm y)
1493 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1494 sm (PAlternative as) = PAlternative (map sm as)
1495 sm (PHidden x) = PHidden (sm x)
1496 sm x = x