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