git.iko.soy/Idris-dev
on 0bc69fb help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1110 lines 41 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 Control.Monad.State
12import Data.List
13import Data.Char
14import Debug.Trace
16import qualified Epic.Epic as E
18data IOption = IOption { opt_logLevel :: Int,
19 opt_typecase :: Bool,
20 opt_typeintype :: Bool,
21 opt_showimp :: Bool,
22 opt_repl :: Bool
23 }
24 deriving (Show, Eq)
26defaultOpts = IOption 0 False False False True
28-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
29-- without typechecking).
30-- This will include all the functions and data declarations, plus fixity declarations
31-- and syntax macros.
33data IState = IState { tt_ctxt :: Context,
34 idris_constraints :: [(UConstraint, FC)],
35 idris_infixes :: [FixDecl],
36 idris_implicits :: Ctxt [PArg],
37 idris_statics :: Ctxt [Bool],
38 idris_classes :: Ctxt ClassInfo,
39 idris_log :: String,
40 idris_options :: IOption,
41 idris_name :: Int,
42 idris_metavars :: [Name],
43 syntax_rules :: [Syntax],
44 syntax_keywords :: [String],
45 imported :: [FilePath],
46 idris_prims :: [(Name, ([E.Name], E.Term))],
47 idris_objs :: [FilePath],
48 idris_libs :: [String],
49 idris_hdrs :: [String],
50 last_proof :: Maybe (Name, [String]),
51 errLine :: Maybe Int,
52 ibc_write :: [IBCWrite]
53 }
55-- information that needs writing for the current module's .ibc file
56data IBCWrite = IBCFix FixDecl
57 | IBCImp Name
58 | IBCStatic Name
59 | IBCClass Name
60 | IBCSyntax Syntax
61 | IBCKeyword String
62 | IBCImport FilePath
63 | IBCObj FilePath
64 | IBCLib String
65 | IBCHeader String
66 | IBCDef Name -- i.e. main context
67 deriving Show
69idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
70 "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing []
72-- The monad for the main REPL - reading and processing files and updating
73-- global state (hence the IO inner monad).
74type Idris a = StateT IState IO a
76getContext :: Idris Context
77getContext = do i <- get; return (tt_ctxt i)
79getObjectFiles :: Idris [FilePath]
80getObjectFiles = do i <- get; return (idris_objs i)
82addObjectFile :: FilePath -> Idris ()
83addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
85getLibs :: Idris [String]
86getLibs = do i <- get; return (idris_libs i)
88addLib :: String -> Idris ()
89addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
91addHdr :: String -> Idris ()
92addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
94addIBC :: IBCWrite -> Idris ()
95addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
97clearIBC :: Idris ()
98clearIBC = do i <- get; put (i { ibc_write = [] })
100getHdrs :: Idris [String]
101getHdrs = do i <- get; return (idris_hdrs i)
103setErrLine :: Int -> Idris ()
104setErrLine x = do i <- get;
105 case (errLine i) of
106 Nothing -> put (i { errLine = Just x })
107 Just _ -> return ()
109clearErr :: Idris ()
110clearErr = do i <- get
111 put (i { errLine = Nothing })
113getIState :: Idris IState
114getIState = get
116putIState :: IState -> Idris ()
117putIState = put
119getName :: Idris Int
120getName = do i <- get;
121 let idx = idris_name i;
122 put (i { idris_name = idx + 1 })
123 return idx
125checkUndefined :: FC -> Name -> Idris ()
126checkUndefined fc n
127 = do i <- getContext
128 case lookupTy Nothing n i of
129 (_:_) -> fail $ show fc ++ ":" ++
130 show n ++ " already defined"
131 _ -> return ()
133setContext :: Context -> Idris ()
134setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
136updateContext :: (Context -> Context) -> Idris ()
137updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
139addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
140addConstraints fc (v, cs)
141 = do i <- get
142 let ctxt = tt_ctxt i
143 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
144 next_tvar = v }
145 let ics = zip cs (repeat fc) ++ idris_constraints i
146 put (i { tt_ctxt = ctxt', idris_constraints = ics })
148addDeferred :: [(Name, Type)] -> Idris ()
149addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
150 i <- get
151 put (i { idris_metavars = map fst ns ++ idris_metavars i })
152 where tidyNames used (Bind (MN i x) b sc)
153 = let n' = uniqueName (UN x) used in
154 Bind n' b $ tidyNames (n':used) sc
155 tidyNames used (Bind n b sc)
156 = let n' = uniqueName n used in
157 Bind n' b $ tidyNames (n':used) sc
158 tidyNames used b = b
160solveDeferred :: Name -> Idris ()
161solveDeferred n = do i <- get
162 put (i { idris_metavars = idris_metavars i \\ [n] })
164iputStrLn :: String -> Idris ()
165iputStrLn = lift.putStrLn
167iWarn :: FC -> String -> Idris ()
168iWarn fc err = do lift $ putStrLn (show fc ++ ":" ++ err)
170setLogLevel :: Int -> Idris ()
171setLogLevel l = do i <- get
172 let opts = idris_options i
173 let opt' = opts { opt_logLevel = l }
174 put (i { idris_options = opt' } )
176logLevel :: Idris Int
177logLevel = do i <- get
178 return (opt_logLevel (idris_options i))
180useREPL :: Idris Bool
181useREPL = do i <- get
182 return (opt_repl (idris_options i))
184setREPL :: Bool -> Idris ()
185setREPL t = do i <- get
186 let opts = idris_options i
187 let opt' = opts { opt_repl = t }
188 put (i { idris_options = opt' })
190typeInType :: Idris Bool
191typeInType = do i <- get
192 return (opt_typeintype (idris_options i))
194setTypeInType :: Bool -> Idris ()
195setTypeInType t = do i <- get
196 let opts = idris_options i
197 let opt' = opts { opt_typeintype = t }
198 put (i { idris_options = opt' })
200impShow :: Idris Bool
201impShow = do i <- get
202 return (opt_showimp (idris_options i))
204setImpShow :: Bool -> Idris ()
205setImpShow t = do i <- get
206 let opts = idris_options i
207 let opt' = opts { opt_showimp = t }
208 put (i { idris_options = opt' })
210logLvl :: Int -> String -> Idris ()
211logLvl l str = do i <- get
212 let lvl = opt_logLevel (idris_options i)
213 when (lvl >= l)
214 $ do lift (putStrLn str)
215 put (i { idris_log = idris_log i ++ str ++ "\n" } )
217iLOG :: String -> Idris ()
218iLOG = logLvl 1
220noErrors :: Idris Bool
221noErrors = do i <- get
222 case errLine i of
223 Nothing -> return True
224 _ -> return False
226setTypeCase :: Bool -> Idris ()
227setTypeCase t = do i <- get
228 let opts = idris_options i
229 let opt' = opts { opt_typecase = t }
230 put (i { idris_options = opt' })
232-- Commands in the REPL
234data Command = Quit | Help | Eval PTerm | Check PTerm | Reload | Edit
235 | Compile String | Execute String
236 | Metavars | Prove Name | AddProof | Universes
237 | TTShell
238 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name
239 | NOP
241-- Parsed declarations
243data Fixity = Infixl { prec :: Int }
244 | Infixr { prec :: Int }
245 | InfixN { prec :: Int }
246 | PrefixN { prec :: Int }
247 deriving Eq
248{-!
249deriving instance Binary Fixity
250!-}
252instance Show Fixity where
253 show (Infixl i) = "infixl " ++ show i
254 show (Infixr i) = "infixr " ++ show i
255 show (InfixN i) = "infix " ++ show i
256 show (PrefixN i) = "prefix " ++ show i
258data FixDecl = Fix Fixity String
259 deriving (Show, Eq)
260{-!
261deriving instance Binary FixDecl
262!-}
264instance Ord FixDecl where
265 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
268data Static = Static | Dynamic
269 deriving (Show, Eq)
270{-!
271deriving instance Binary Static
272!-}
274-- Mark bindings with their explicitness, and laziness
275data Plicity = Imp { plazy :: Bool,
276 pstatic :: Static }
277 | Exp { plazy :: Bool,
278 pstatic :: Static }
279 | Constraint { plazy :: Bool,
280 pstatic :: Static }
281 deriving (Show, Eq)
283{-!
284deriving instance Binary Plicity
285!-}
287impl = Imp False Dynamic
288expl = Exp False Dynamic
289constraint = Constraint False Static
291data FnOpt = Inlinable | Partial | Abstract | Private
292 deriving (Show, Eq)
294type FnOpts = [FnOpt]
296inlinable :: FnOpts -> Bool
297inlinable = elem Inlinable
299data PDecl' t = PFix FC Fixity [String] -- fixity declaration
300 | PTy SyntaxInfo FC Name t -- type declaration
301 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
302 | PData SyntaxInfo FC (PData' t) -- data declaration
303 | PParams FC [(Name, t)] [PDecl' t] -- params block
304 | PNamespace String [PDecl' t] -- new namespace
305 | PClass SyntaxInfo FC
306 [t] -- constraints
307 Name
308 [(Name, t)] -- parameters
309 [PDecl' t] -- declarations
310 | PInstance SyntaxInfo FC [t] -- constraints
311 Name -- class
312 [t] -- parameters
313 t -- full instance type
314 [PDecl' t]
315 | PSyntax FC Syntax
316 | PDirective (Idris ())
317 deriving Functor
319data PClause' t = PClause Name t [t] t [PDecl' t]
320 | PWith Name t [t] t [PDecl' t]
321 deriving Functor
323data PData' t = PDatadecl { d_name :: Name,
324 d_tcon :: t,
325 d_cons :: [(Name, t, FC)] }
326 deriving Functor
328-- Handy to get a free function for applying PTerm -> PTerm functions
329-- across a program, by deriving Functor
331type PDecl = PDecl' PTerm
332type PData = PData' PTerm
333type PClause = PClause' PTerm
335-- get all the names declared in a decl
337declared :: PDecl -> [Name]
338declared (PFix _ _ _) = []
339declared (PTy _ _ n t) = [n]
340declared (PClauses _ _ n _) = [] -- not a declaration
341declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
342 where fstt (a, _, _) = a
343declared (PParams _ _ ds) = concatMap declared ds
344declared (PNamespace _ ds) = concatMap declared ds
345-- declared (PImport _) = []
347updateN :: [(Name, Name)] -> Name -> Name
348updateN ns n | Just n' <- lookup n ns = n'
349updateN _ n = n
351updateNs :: [(Name, Name)] -> PTerm -> PTerm
352updateNs [] t = t
353updateNs ns t = mapPT updateRef t
354 where updateRef (PRef fc f) = PRef fc (updateN ns f)
355 updateRef t = t
357-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
358-- updateDNs [] t = t
359-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
360-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
361-- where updateCNs ns (PClause n l ts r ds)
362-- = PClause (updateN ns n) (fmap (updateNs ns) l)
363-- (map (fmap (updateNs ns)) ts)
364-- (fmap (updateNs ns) r)
365-- (map (updateDNs ns) ds)
366-- updateDNs ns c = c
368-- High level language terms
370data PTerm = PQuote Raw
371 | PRef FC Name
372 | PLam Name PTerm PTerm
373 | PPi Plicity Name PTerm PTerm
374 | PLet Name PTerm PTerm PTerm
375 | PApp FC PTerm [PArg]
376 | PTrue FC
377 | PFalse FC
378 | PRefl FC
379 | PResolveTC FC
380 | PEq FC PTerm PTerm
381 | PPair FC PTerm PTerm
382 | PDPair FC PTerm PTerm PTerm
383 | PAlternative [PTerm]
384 | PHidden PTerm -- irrelevant or hidden pattern
385 | PSet
386 | PConstant Const
387 | Placeholder
388 | PDoBlock [PDo]
389 | PReturn FC
390 | PMetavar Name
391 | PProof [PTactic]
392 | PTactics [PTactic] -- as PProof, but no auto solving
393 | PElabError String -- error to report on elaboration
394 | PImpossible -- special case for declaring when an LHS can't typecheck
395 deriving Eq
396{-!
397deriving instance Binary PTerm
398!-}
400mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
401mapPT f t = f (mpt t) where
402 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
403 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
404 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
405 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
406 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
407 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
408 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
409 mpt (PAlternative as) = PAlternative (map (mapPT f) as)
410 mpt (PHidden t) = PHidden (mapPT f t)
411 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
412 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
413 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
414 mpt x = x
417data PTactic' t = Intro [Name] | Focus Name
418 | Refine Name [Bool] | Rewrite t | LetTac Name t
419 | Exact t | Compute | Trivial
420 | Solve
421 | Attack
422 | ProofState | ProofTerm | Undo
423 | Try (PTactic' t) (PTactic' t)
424 | TSeq (PTactic' t) (PTactic' t)
425 | Qed
426 deriving (Show, Eq, Functor)
427{-!
428deriving instance Binary PTactic'
429!-}
431type PTactic = PTactic' PTerm
433data PDo' t = DoExp FC t
434 | DoBind FC Name t
435 | DoLet FC Name t
436 deriving (Eq, Functor)
437{-!
438deriving instance Binary PDo'
439!-}
441type PDo = PDo' PTerm
443-- The priority gives a hint as to elaboration order. Best to elaborate
444-- things early which will help give a more concrete type to other
445-- variables, e.g. a before (interpTy a).
447data PArg' t = PImp { priority :: Int,
448 lazyarg :: Bool, pname :: Name, getTm :: t }
449 | PExp { priority :: Int,
450 lazyarg :: Bool, getTm :: t }
451 | PConstraint { priority :: Int,
452 lazyarg :: Bool, getTm :: t }
453 deriving (Show, Eq, Functor)
454{-!
455deriving instance Binary PArg'
456!-}
458pimp = PImp 0 False
459pexp = PExp 0 False
460pconst = PConstraint 0 False
462type PArg = PArg' PTerm
464-- Type class data
466data ClassInfo = CI { instanceName :: Name,
467 class_methods :: [(Name, PTerm)],
468 class_defaults :: [(Name, Name)], -- method name -> default impl
469 class_params :: [Name] }
470 deriving Show
471{-!
472deriving instance Binary ClassInfo
473!-}
475-- Syntactic sugar info
477data DSL = DSL { dsl_bind :: Name,
478 dsl_return :: Name }
479 deriving Show
481data SynContext = PatternSyntax | TermSyntax | AnySyntax
482 deriving Show
483{-!
484deriving instance Binary SynContext
485!-}
487data Syntax = Rule [SSymbol] PTerm SynContext
488 deriving Show
489{-!
490deriving instance Binary Syntax
491!-}
493data SSymbol = Keyword Name
494 | Symbol String
495 | Expr Name
496 deriving Show
497{-!
498deriving instance Binary SSymbol
499!-}
501initDSL = DSL (UN ">>=") (UN "return")
503data SyntaxInfo = Syn { using :: [(Name, PTerm)],
504 syn_params :: [(Name, PTerm)],
505 syn_namespace :: [String],
506 no_imp :: [Name],
507 decoration :: Name -> Name,
508 inPattern :: Bool,
509 dsl_info :: DSL }
510 deriving Show
512defaultSyntax = Syn [] [] [] [] id False initDSL
514--- Pretty printing declarations and terms
516instance Show PTerm where
517 show tm = showImp False tm
519instance Show PDecl where
520 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
521 show (PTy _ _ n ty) = show n ++ " : " ++ show ty
522 show (PClauses _ _ n c) = showSep "\n" (map show c)
523 show (PData _ _ d) = show d
525instance Show PClause where
526 show c = showCImp True c
528instance Show PData where
529 show d = showDImp False d
531showCImp :: Bool -> PClause -> String
532showCImp impl (PClause n l ws r w)
533 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
534 ++ " where " ++ show w
535 where
536 showWs [] = ""
537 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
538showCImp impl (PWith n l ws r w)
539 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
540 ++ " { " ++ show w ++ " } "
541 where
542 showWs [] = ""
543 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
546showDImp :: Bool -> PData -> String
547showDImp impl (PDatadecl n ty cons)
548 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
549 ++ showSep "\n\t| "
550 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
552getImps :: [PArg] -> [(Name, PTerm)]
553getImps [] = []
554getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
555getImps (_ : xs) = getImps xs
557getExps :: [PArg] -> [PTerm]
558getExps [] = []
559getExps (PExp _ _ tm : xs) = tm : getExps xs
560getExps (_ : xs) = getExps xs
562getConsts :: [PArg] -> [PTerm]
563getConsts [] = []
564getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
565getConsts (_ : xs) = getConsts xs
567getAll :: [PArg] -> [PTerm]
568getAll = map getTm
570showImp :: Bool -> PTerm -> String
571showImp impl tm = se 10 tm where
572 se p (PQuote r) = "![" ++ show r ++ "]"
573 se p (PRef _ n) = if impl then show n
574 else showbasic n
575 where showbasic n@(UN _) = show n
576 showbasic (MN _ s) = s
577 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
578 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
579 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
580 " in " ++ se 10 sc
581 se p (PPi (Exp l s) n ty sc)
582 | n `elem` allNamesIn sc = bracket p 2 $
583 if l then "|(" else "(" ++
584 show n ++ " : " ++ se 10 ty ++
585 ") " ++ st ++
586 "-> " ++ se 10 sc
587 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
588 where st = case s of
589 Static -> "[static] "
590 _ -> ""
591 se p (PPi (Imp l s) n ty sc)
592 | impl = bracket p 2 $ if l then "|{" else "{" ++
593 show n ++ " : " ++ se 10 ty ++
594 "} " ++ st ++ "-> " ++ se 10 sc
595 | otherwise = se 10 sc
596 where st = case s of
597 Static -> "[static] "
598 _ -> ""
599 se p (PPi (Constraint _ _) n ty sc)
600 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
601 se p (PApp _ (PRef _ f) [])
602 | not impl = show f
603 se p (PApp _ (PRef _ op@(UN (f:_))) args)
604 | length (getExps args) == 2 && not impl && not (isAlpha f)
605 = let [l, r] = getExps args in
606 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
607 se p (PApp _ f as)
608 = let args = getExps as in
609 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
610 else concatMap seArg args
611 se p (PHidden tm) = "." ++ se 0 tm
612 se p (PRefl _) = "refl"
613 se p (PResolveTC _) = "resolvetc"
614 se p (PTrue _) = "()"
615 se p (PFalse _) = "_|_"
616 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
617 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
618 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
619 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
620 se p PSet = "Set"
621 se p (PConstant c) = show c
622 se p (PProof ts) = "proof { " ++ show ts ++ "}"
623 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
624 se p (PMetavar n) = "?" ++ show n
625 se p Placeholder = "_"
627 sArg (PImp _ _ n tm) = siArg (n, tm)
628 sArg (PExp _ _ tm) = seArg tm
629 sArg (PConstraint _ _ tm) = scArg tm
631 seArg arg = " " ++ se 0 arg
632 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
633 scArg val = " {{" ++ se 10 val ++ "}}"
635 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
636 | otherwise = str
638allNamesIn :: PTerm -> [Name]
639allNamesIn tm = nub $ ni [] tm
640 where
641 ni env (PRef _ n)
642 | not (n `elem` env) = [n]
643 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
644 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
645 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
646 ni env (PHidden tm) = ni env tm
647 ni env (PEq _ l r) = ni env l ++ ni env r
648 ni env (PPair _ l r) = ni env l ++ ni env r
649 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
650 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
651 ni env (PAlternative ls) = concatMap (ni env) ls
652 ni env _ = []
654namesIn :: IState -> PTerm -> [Name]
655namesIn ist tm = nub $ ni [] tm
656 where
657 ni env (PRef _ n)
658 | not (n `elem` env)
659 = case lookupTy Nothing n (tt_ctxt ist) of
660 [] -> [n]
661 _ -> []
662 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
663 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
664 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
665 ni env (PEq _ l r) = ni env l ++ ni env r
666 ni env (PPair _ l r) = ni env l ++ ni env r
667 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
668 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
669 ni env (PAlternative as) = concatMap (ni env) as
670 ni env (PHidden tm) = ni env tm
671 ni env _ = []
673-- For inferring types of things
675bi = FC "builtin" 0
677inferTy = MN 0 "__Infer"
678inferCon = MN 0 "__infer"
679inferDecl = PDatadecl inferTy
680 PSet
681 [(inferCon, PPi impl (MN 0 "A") PSet (
682 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
683 (PRef bi inferTy)), bi)]
685infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
686infP = P (TCon 6 0) inferTy (Set (UVal 0))
688getInferTerm, getInferType :: Term -> Term
689getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
690getInferTerm (App (App _ _) tm) = tm
691getInferTerm tm = error ("getInferTerm " ++ show tm)
693getInferType (Bind n b sc) = Bind n b $ getInferType sc
694getInferType (App (App _ ty) _) = ty
696-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
698primNames = [unitTy, unitCon,
699 falseTy, pairTy, pairCon,
700 eqTy, eqCon, inferTy, inferCon]
702unitTy = MN 0 "__Unit"
703unitCon = MN 0 "__II"
704unitDecl = PDatadecl unitTy PSet
705 [(unitCon, PRef bi unitTy, bi)]
707falseTy = MN 0 "__False"
708falseDecl = PDatadecl falseTy PSet []
710pairTy = MN 0 "__Pair"
711pairCon = MN 0 "__MkPair"
712pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
713 [(pairCon, PPi impl (n "A") PSet (
714 PPi impl (n "B") PSet (
715 PPi expl (n "a") (PRef bi (n "A")) (
716 PPi expl (n "b") (PRef bi (n "B"))
717 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
718 pexp (PRef bi (n "B"))])))), bi)]
719 where n a = MN 0 a
721eqTy = UN "="
722eqCon = UN "refl"
723eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
724 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
725 PSet)
726 [(eqCon, PPi impl (n "a") PSet (
727 PPi impl (n "x") (PRef bi (n "a"))
728 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
729 pimp (n "b") Placeholder,
730 pexp (PRef bi (n "x")),
731 pexp (PRef bi (n "x"))])), bi)]
732 where n a = MN 0 a
734-- Defined in builtins.idr
735sigmaTy = UN "Exists"
736existsCon = UN "Ex_intro"
738piBind :: [(Name, PTerm)] -> PTerm -> PTerm
739piBind [] t = t
740piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
742-- Dealing with parameters
744expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
745expandParams dec ps ns tm = en tm
746 where
747 en (PLam n t s) = PLam n (en t) (en s)
748 en (PPi p n t s) = PPi p n (en t) (en s)
749 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)
750 en (PEq f l r) = PEq f (en l) (en r)
751 en (PPair f l r) = PPair f (en l) (en r)
752 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
753 en (PAlternative as) = PAlternative (map en as)
754 en (PHidden t) = PHidden (en t)
755 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
756 en (PProof ts) = PProof (map (fmap en) ts)
757 en (PTactics ts) = PTactics (map (fmap en) ts)
759 en (PQuote (Var n))
760 | n `elem` ns = PQuote (Var (dec n))
761 en (PApp fc (PRef fc' n) as)
762 | n `elem` ns = PApp fc (PRef fc' (dec n))
763 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
764 en (PRef fc n)
765 | n `elem` ns = PApp fc (PRef fc (dec n))
766 (map (pexp . (PRef fc)) (map fst ps))
767 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
768 en t = t
770expandParamsD :: IState ->
771 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
772expandParamsD ist dec ps ns (PTy syn fc n ty)
773 = if n `elem` ns
774 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
775 else PTy syn fc n (expandParams dec ps ns ty)
776expandParamsD ist dec ps ns (PClauses fc opts n cs)
777 = let n' = if n `elem` ns then dec n else n in
778 PClauses fc opts n' (map expandParamsC cs)
779 where
780 expandParamsC (PClause n lhs ws rhs ds)
781 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
782 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
783 n' = if n `elem` ns then dec n else n in
784 PClause n' (expandParams dec ps'' ns lhs)
785 (map (expandParams dec ps'' ns) ws)
786 (expandParams dec ps'' ns rhs)
787 (map (expandParamsD ist dec ps'' ns) ds)
788 expandParamsC (PWith n lhs ws wval ds)
789 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
790 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
791 n' = if n `elem` ns then dec n else n in
792 PWith n' (expandParams dec ps'' ns lhs)
793 (map (expandParams dec ps'' ns) ws)
794 (expandParams dec ps'' ns wval)
795 (map (expandParamsD ist dec ps'' ns) ds)
796 updateps yn nm [] = []
797 updateps yn nm (((a, t), i):as)
798 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
799 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
801expandParamsD ist dec ps ns d = d
803-- Calculate a priority for a type, for deciding elaboration order
804-- * if it's just a type variable or concrete type, do it early (0)
805-- * if there's only type variables and injective constructors, do it next (1)
806-- * if there's a function type, next (2)
807-- * finally, everything else (3)
809getPriority :: IState -> PTerm -> Int
810getPriority i tm = pri tm
811 where
812 pri (PRef _ n) =
813 case lookupP Nothing n (tt_ctxt i) of
814 ((P (DCon _ _) _ _):_) -> 1
815 ((P (TCon _ _) _ _):_) -> 1
816 ((P Ref _ _):_) -> 3
817 [] -> 0 -- must be locally bound, if it's not an error...
818 pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))
819 pri (PTrue _) = 0
820 pri (PFalse _) = 0
821 pri (PRefl _) = 1
822 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
823 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
824 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
825 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
826 pri (PAlternative as) = maximum (map pri as)
827 pri (PConstant _) = 0
828 pri Placeholder = 1
829 pri _ = 3
831-- Dealing with implicit arguments
833-- Add implicit Pi bindings for any names in the term which appear in an
834-- argument position.
836-- This has become a right mess already. Better redo it some time...
838implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
839implicit syn n ptm
840 = do i <- get
841 let (tm', impdata) = implicitise syn i ptm
842 let (tm'', spos) = findStatics i tm'
843 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
844 addIBC (IBCImp n)
845 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
846 i <- get
847 put (i { idris_statics = addDef n spos (idris_statics i) })
848 addIBC (IBCStatic n)
849 return tm''
851implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
852implicitise syn ist tm
853 = let uvars = using syn
854 pvars = syn_params syn
855 (declimps, ns') = execState (imps True [] tm) ([], [])
856 ns = ns' \\ (map fst pvars ++ no_imp syn) in
857 if null ns
858 then (tm, reverse declimps)
859 else implicitise syn ist (pibind uvars ns tm)
860 where
861 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
862 | otherwise = x : dropAll xs ys
863 dropAll [] ys = []
865 imps top env (PApp _ f as)
866 = do (decls, ns) <- get
867 let isn = concatMap (namesIn ist) (map getTm as)
868 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
869 imps top env (PPi (Imp l _) n ty sc)
870 = do let isn = nub (namesIn ist ty) `dropAll` [n]
871 (decls , ns) <- get
872 put (PImp (getPriority ist ty) l n ty : decls,
873 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
874 imps True (n:env) sc
875 imps top env (PPi (Exp l _) n ty sc)
876 = do let isn = nub (namesIn ist ty ++ case sc of
877 (PRef _ x) -> namesIn ist sc `dropAll` [n]
878 _ -> [])
879 (decls, ns) <- get -- ignore decls in HO types
880 put (PExp (getPriority ist ty) l ty : decls,
881 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
882 imps True (n:env) sc
883 imps top env (PPi (Constraint l _) n ty sc)
884 = do let isn = nub (namesIn ist ty ++ case sc of
885 (PRef _ x) -> namesIn ist sc `dropAll` [n]
886 _ -> [])
887 (decls, ns) <- get -- ignore decls in HO types
888 put (PConstraint 10 l ty : decls,
889 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
890 imps True (n:env) sc
891 imps top env (PEq _ l r)
892 = do (decls, ns) <- get
893 let isn = namesIn ist l ++ namesIn ist r
894 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
895 imps top env (PPair _ l r)
896 = do (decls, ns) <- get
897 let isn = namesIn ist l ++ namesIn ist r
898 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
899 imps top env (PDPair _ (PRef _ n) t r)
900 = do (decls, ns) <- get
901 let isn = nub (namesIn ist t ++ namesIn ist r) \\ [n]
902 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
903 imps top env (PDPair _ l t r)
904 = do (decls, ns) <- get
905 let isn = namesIn ist l ++ namesIn ist t ++ namesIn ist r
906 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
907 imps top env (PAlternative as)
908 = do (decls, ns) <- get
909 let isn = concatMap (namesIn ist) as
910 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
911 imps top env (PLam n ty sc)
912 = do imps False env ty
913 imps False (n:env) sc
914 imps top env (PHidden tm) = imps False env tm
915 imps top env _ = return ()
917 pibind using [] sc = sc
918 pibind using (n:ns) sc
919 = case lookup n using of
920 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
921 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
923-- Add implicit arguments in function calls
925addImpl :: IState -> PTerm -> PTerm
926addImpl ist ptm = ai [] ptm
927 where
928 ai env (PRef fc f) = aiFn ist fc f []
929 ai env (PEq fc l r) = let l' = ai env l
930 r' = ai env r in
931 PEq fc l' r'
932 ai env (PPair fc l r) = let l' = ai env l
933 r' = ai env r in
934 PPair fc l' r'
935 ai env (PDPair fc l t r) = let l' = ai env l
936 t' = ai env t
937 r' = ai env r in
938 PDPair fc l' t' r'
939 ai env (PAlternative as) = let as' = map (ai env) as in
940 PAlternative as'
941 ai env (PApp fc (PRef _ f) as)
942 = let as' = map (fmap (ai env)) as in
943 aiFn ist fc f as'
944 ai env (PApp fc f as) = let f' = ai env f
945 as' = map (fmap (ai env)) as in
946 mkPApp fc 1 f' as'
947 ai env (PLam n ty sc) = let ty' = ai env ty
948 sc' = ai (n:env) sc in
949 PLam n ty' sc'
950 ai env (PLet n ty val sc)
951 = let ty' = ai env ty
952 val' = ai env val
953 sc' = ai (n:env) sc in
954 PLet n ty' val' sc'
955 ai env (PPi p n ty sc) = let ty' = ai env ty
956 sc' = ai (n:env) sc in
957 PPi p n ty' sc'
958 ai env (PHidden tm) = PHidden (ai env tm)
959 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
960 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
961 ai env tm = tm
963aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
964aiFn ist fc f as
965 | f `elem` primNames = PApp fc (PRef fc f) as
966aiFn ist fc f as
967 -- This is where namespaces get resolved by adding PAlternative
968 = case lookupCtxtName Nothing f (idris_implicits ist) of
969 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
970 [] -> mkPApp fc 1 (PRef fc f) as
971 alts -> PAlternative $
972 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
973 (insertImpl ns as)) alts
974 where
975 insertImpl :: [PArg] -> [PArg] -> [PArg]
976 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
977 PExp p l tm : insertImpl ps given
978 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
979 PConstraint p l tm : insertImpl ps given
980 insertImpl (PConstraint p l ty : ps) given =
981 PConstraint p l (PResolveTC fc) : insertImpl ps given
982 insertImpl (PImp p l n ty : ps) given =
983 case find n given [] of
984 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
985 Nothing -> PImp p l n Placeholder : insertImpl ps given
986 insertImpl expected [] = []
987 insertImpl _ given = given
989 find n [] acc = Nothing
990 find n (PImp _ _ n' t : gs) acc
991 | n == n' = Just (t, reverse acc ++ gs)
992 find n (g : gs) acc = find n gs (g : acc)
994mkPApp fc a f [] = f
995mkPApp fc a f as = let rest = drop a as in
996 appRest fc (PApp fc f (take a as)) rest
997 where
998 appRest fc f [] = f
999 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1001-- Find 'static' argument positions
1002-- (the declared ones, plus any names in argument position in the declared
1003-- statics)
1004-- FIXME: It's possible that this really has to happen after elaboration
1006findStatics :: IState -> PTerm -> (PTerm, [Bool])
1007findStatics ist tm = let (ns, ss) = fs tm in
1008 runState (pos ns ss tm) []
1009 where fs (PPi p n t sc)
1010 | Static <- pstatic p
1011 = let (ns, ss) = fs sc in
1012 (namesIn ist t : ns, namesIn ist t ++ n : ss)
1013 | otherwise = let (ns, ss) = fs sc in
1014 (namesIn ist t : ns, ss)
1015 fs _ = ([], [])
1017 inOne n ns = length (filter id (map (elem n) ns)) == 1
1019 pos ns ss (PPi p n t sc)
1020 | n `inOne` ns && elem n ss
1021 = do sc' <- pos ns ss sc
1022 spos <- get
1023 put (True : spos)
1024 return (PPi (p { pstatic = Static }) n t sc')
1025 | otherwise = do sc' <- pos ns ss sc
1026 spos <- get
1027 put (False : spos)
1028 return (PPi p n t sc')
1029 pos ns ss t = return t
1031-- Debugging/logging stuff
1033dumpDecls :: [PDecl] -> String
1034dumpDecls [] = ""
1035dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1037dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1038dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1039dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1040dumpDecl (PData _ _ d) = showDImp True d
1041dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1042dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1043dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1044dumpDecl (PClass _ _ cs n ps ds)
1045 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1046dumpDecl (PInstance _ _ cs n _ t ds)
1047 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1048dumpDecl _ = "..."
1049-- dumpDecl (PImport i) = "import " ++ i
1051-- syntactic match of a against b, returning pair of variables in a
1052-- and what they match. Returns 'Nothing' if not a match.
1054matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
1055matchClause x y = match x y where
1056 matchArg x y = match (getTm x) (getTm y)
1058 match (PApp _ f args) (PApp _ f' args')
1059 | length args == length args'
1060 = do mf <- match f f'
1061 ms <- zipWithM matchArg args args'
1062 return (mf ++ concat ms)
1063-- match (PRef _ n) (PRef _ n') | n == n' = return []
1064-- | otherwise = Nothing
1065 match (PRef _ n) tm = return [(n, tm)]
1066 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
1067 mr <- match r r'
1068 return (ml ++ mr)
1069 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
1070 mr <- match r r'
1071 return (ml ++ mr)
1072 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match l l'
1073 mt <- match t t'
1074 mr <- match r r'
1075 return (ml ++ mt ++ mr)
1076 match (PAlternative as) (PAlternative as')
1077 = do ms <- zipWithM match as as'
1078 return (concat ms)
1079 match (PRefl _) (PRefl _) = return []
1080 match (PResolveTC _) (PResolveTC _) = return []
1081 match (PTrue _) (PTrue _) = return []
1082 match (PFalse _) (PFalse _) = return []
1083 match (PReturn _) (PReturn _) = return []
1084 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
1085 ms <- match s s'
1086 return (mt ++ ms)
1087 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
1088 ms <- match s s'
1089 return (mt ++ ms)
1090 match (PHidden x) (PHidden y) = match x y
1091 match a b | a == b = return []
1092 | otherwise = Nothing
1094substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1095substMatches [] t = t
1096substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1098substMatch :: Name -> PTerm -> PTerm -> PTerm
1099substMatch n tm t = sm t where
1100 sm (PRef _ n') | n == n' = tm
1101 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1102 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1103 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1104 sm (PEq f x y) = PEq f (sm x) (sm y)
1105 sm (PPair f x y) = PPair f (sm x) (sm y)
1106 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1107 sm (PAlternative as) = PAlternative (map sm as)
1108 sm (PHidden x) = PHidden (sm x)
1109 sm x = x