git.iko.soy/Idris-dev
on f2e3a76 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1020 lines 39 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_showimp :: Bool
21 }
22 deriving (Show, Eq)
24defaultOpts = IOption 0 False False
26-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
27-- without typechecking).
28-- This will include all the functions and data declarations, plus fixity declarations
29-- and syntax macros.
31data IState = IState { tt_ctxt :: Context,
32 idris_constraints :: [(UConstraint, FC)],
33 idris_infixes :: [FixDecl],
34 idris_implicits :: Ctxt [PArg],
35 idris_statics :: Ctxt [Bool],
36 idris_classes :: Ctxt ClassInfo,
37 idris_log :: String,
38 idris_options :: IOption,
39 idris_name :: Int,
40 idris_metavars :: [Name],
41 syntax_rules :: [Syntax],
42 syntax_keywords :: [String],
43 imported :: [FilePath],
44 idris_prims :: [(Name, ([E.Name], E.Term))],
45 idris_objs :: [FilePath],
46 idris_libs :: [String],
47 idris_hdrs :: [String],
48 last_proof :: Maybe (Name, [String]),
49 errLine :: Maybe Int
50 }
52idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
53 "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing
55-- The monad for the main REPL - reading and processing files and updating
56-- global state (hence the IO inner monad).
57type Idris a = StateT IState IO a
59getContext :: Idris Context
60getContext = do i <- get; return (tt_ctxt i)
62getObjectFiles :: Idris [FilePath]
63getObjectFiles = do i <- get; return (idris_objs i)
65addObjectFile :: FilePath -> Idris ()
66addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
68getLibs :: Idris [String]
69getLibs = do i <- get; return (idris_libs i)
71addLib :: String -> Idris ()
72addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
74addHdr :: String -> Idris ()
75addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
77getHdrs :: Idris [String]
78getHdrs = do i <- get; return (idris_hdrs i)
80setErrLine :: Int -> Idris ()
81setErrLine x = do i <- get;
82 case (errLine i) of
83 Nothing -> put (i { errLine = Just x })
84 Just _ -> return ()
86clearErr :: Idris ()
87clearErr = do i <- get
88 put (i { errLine = Nothing })
90getIState :: Idris IState
91getIState = get
93putIState :: IState -> Idris ()
94putIState = put
96getName :: Idris Int
97getName = do i <- get;
98 let idx = idris_name i;
99 put (i { idris_name = idx + 1 })
100 return idx
102checkUndefined :: FC -> Name -> Idris ()
103checkUndefined fc n
104 = do i <- getContext
105 case lookupTy Nothing n i of
106 (_:_) -> fail $ show fc ++ ":" ++
107 show n ++ " already defined"
108 _ -> return ()
110setContext :: Context -> Idris ()
111setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
113updateContext :: (Context -> Context) -> Idris ()
114updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
116addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
117addConstraints fc (v, cs)
118 = do i <- get
119 let ctxt = tt_ctxt i
120 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
121 next_tvar = v }
122 let ics = zip cs (repeat fc) ++ idris_constraints i
123 put (i { tt_ctxt = ctxt', idris_constraints = ics })
125addDeferred :: [(Name, Type)] -> Idris ()
126addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
127 i <- get
128 put (i { idris_metavars = map fst ns ++ idris_metavars i })
129 where tidyNames used (Bind (MN i x) b sc)
130 = let n' = uniqueName (UN x) used in
131 Bind n' b $ tidyNames (n':used) sc
132 tidyNames used (Bind n b sc)
133 = let n' = uniqueName n used in
134 Bind n' b $ tidyNames (n':used) sc
135 tidyNames used b = b
137solveDeferred :: Name -> Idris ()
138solveDeferred n = do i <- get
139 put (i { idris_metavars = idris_metavars i \\ [n] })
141iputStrLn :: String -> Idris ()
142iputStrLn = lift.putStrLn
144iWarn :: FC -> String -> Idris ()
145iWarn fc err = do lift $ putStrLn (show fc ++ ":" ++ err)
147setLogLevel :: Int -> Idris ()
148setLogLevel l = do i <- get
149 let opts = idris_options i
150 let opt' = opts { opt_logLevel = l }
151 put (i { idris_options = opt' } )
153logLevel :: Idris Int
154logLevel = do i <- get
155 return (opt_logLevel (idris_options i))
157impShow :: Idris Bool
158impShow = do i <- get
159 return (opt_showimp (idris_options i))
161setImpShow :: Bool -> Idris ()
162setImpShow t = do i <- get
163 let opts = idris_options i
164 let opt' = opts { opt_showimp = t }
165 put (i { idris_options = opt' })
167logLvl :: Int -> String -> Idris ()
168logLvl l str = do i <- get
169 let lvl = opt_logLevel (idris_options i)
170 when (lvl >= l)
171 $ do lift (putStrLn str)
172 put (i { idris_log = idris_log i ++ str ++ "\n" } )
174iLOG :: String -> Idris ()
175iLOG = logLvl 1
177noErrors :: Idris Bool
178noErrors = do i <- get
179 case errLine i of
180 Nothing -> return True
181 _ -> return False
183setTypeCase :: Bool -> Idris ()
184setTypeCase t = do i <- get
185 let opts = idris_options i
186 let opt' = opts { opt_typecase = t }
187 put (i { idris_options = opt' })
189-- Commands in the REPL
191data Command = Quit | Help | Eval PTerm | Check PTerm | Reload | Edit
192 | Compile String | Execute String
193 | Metavars | Prove Name | AddProof | Universes
194 | TTShell
195 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name
196 | NOP
198-- Parsed declarations
200data Fixity = Infixl { prec :: Int }
201 | Infixr { prec :: Int }
202 | InfixN { prec :: Int }
203 | PrefixN { prec :: Int }
204 deriving Eq
206instance Show Fixity where
207 show (Infixl i) = "infixl " ++ show i
208 show (Infixr i) = "infixr " ++ show i
209 show (InfixN i) = "infix " ++ show i
210 show (PrefixN i) = "prefix " ++ show i
212data FixDecl = Fix Fixity String
213 deriving (Show, Eq)
215instance Ord FixDecl where
216 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
219data Static = Static | Dynamic
220 deriving (Show, Eq)
222-- Mark bindings with their explicitness, and laziness
223data Plicity = Imp { plazy :: Bool,
224 pstatic :: Static }
225 | Exp { plazy :: Bool,
226 pstatic :: Static }
227 | Constraint { plazy :: Bool,
228 pstatic :: Static }
229 deriving (Show, Eq)
231impl = Imp False Dynamic
232expl = Exp False Dynamic
233constraint = Constraint False Static
235type FnOpts = Bool -- just inlinable, for now
237inlinable :: FnOpts -> Bool
238inlinable x = x
240data PDecl' t = PFix FC Fixity [String] -- fixity declaration
241 | PTy SyntaxInfo FC Name t -- type declaration
242 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
243 | PData SyntaxInfo FC (PData' t) -- data declaration
244 | PParams FC [(Name, t)] [PDecl' t] -- params block
245 | PNamespace String [PDecl' t] -- new namespace
246 | PClass SyntaxInfo FC
247 [t] -- constraints
248 Name
249 [(Name, t)] -- parameters
250 [PDecl' t] -- declarations
251 | PInstance SyntaxInfo FC [t] -- constraints
252 Name -- class
253 [t] -- parameters
254 t -- full instance type
255 [PDecl' t]
256 | PSyntax FC Syntax
257 | PDirective (Idris ())
258 deriving Functor
260data PClause' t = PClause Name t [t] t [PDecl' t]
261 | PWith Name t [t] t [PDecl' t]
262 deriving Functor
264data PData' t = PDatadecl { d_name :: Name,
265 d_tcon :: t,
266 d_cons :: [(Name, t, FC)] }
267 deriving Functor
269-- Handy to get a free function for applying PTerm -> PTerm functions
270-- across a program, by deriving Functor
272type PDecl = PDecl' PTerm
273type PData = PData' PTerm
274type PClause = PClause' PTerm
276-- get all the names declared in a decl
278declared :: PDecl -> [Name]
279declared (PFix _ _ _) = []
280declared (PTy _ _ n t) = [n]
281declared (PClauses _ _ n _) = [] -- not a declaration
282declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
283 where fstt (a, _, _) = a
284declared (PParams _ _ ds) = concatMap declared ds
285declared (PNamespace _ ds) = concatMap declared ds
286-- declared (PImport _) = []
288updateN :: [(Name, Name)] -> Name -> Name
289updateN ns n | Just n' <- lookup n ns = n'
290updateN _ n = n
292updateNs :: [(Name, Name)] -> PTerm -> PTerm
293updateNs [] t = t
294updateNs ns t = mapPT updateRef t
295 where updateRef (PRef fc f) = PRef fc (updateN ns f)
296 updateRef t = t
298-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
299-- updateDNs [] t = t
300-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
301-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
302-- where updateCNs ns (PClause n l ts r ds)
303-- = PClause (updateN ns n) (fmap (updateNs ns) l)
304-- (map (fmap (updateNs ns)) ts)
305-- (fmap (updateNs ns) r)
306-- (map (updateDNs ns) ds)
307-- updateDNs ns c = c
309-- High level language terms
311data PTerm = PQuote Raw
312 | PRef FC Name
313 | PLam Name PTerm PTerm
314 | PPi Plicity Name PTerm PTerm
315 | PLet Name PTerm PTerm PTerm
316 | PApp FC PTerm [PArg]
317 | PTrue FC
318 | PFalse FC
319 | PRefl FC
320 | PResolveTC FC
321 | PEq FC PTerm PTerm
322 | PPair FC PTerm PTerm
323 | PDPair FC PTerm PTerm PTerm
324 | PAlternative [PTerm]
325 | PHidden PTerm -- irrelevant or hidden pattern
326 | PSet
327 | PConstant Const
328 | Placeholder
329 | PDoBlock [PDo]
330 | PReturn FC
331 | PMetavar Name
332 | PProof [PTactic]
333 | PTactics [PTactic] -- as PProof, but no auto solving
334 | PElabError String -- error to report on elaboration
335 deriving Eq
337mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
338mapPT f t = f (mpt t) where
339 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
340 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
341 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
342 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
343 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
344 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
345 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
346 mpt (PAlternative as) = PAlternative (map (mapPT f) as)
347 mpt (PHidden t) = PHidden (mapPT f t)
348 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
349 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
350 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
351 mpt x = x
354data PTactic' t = Intro [Name] | Focus Name
355 | Refine Name [Bool] | Rewrite t | LetTac Name t
356 | Exact t | Compute | Trivial
357 | Solve
358 | Attack
359 | ProofState | ProofTerm | Undo
360 | Try (PTactic' t) (PTactic' t)
361 | TSeq (PTactic' t) (PTactic' t)
362 | Qed
363 deriving (Show, Eq, Functor)
365type PTactic = PTactic' PTerm
367data PDo' t = DoExp FC t
368 | DoBind FC Name t
369 | DoLet FC Name t
370 deriving (Eq, Functor)
372type PDo = PDo' PTerm
374-- The priority gives a hint as to elaboration order. Best to elaborate
375-- things early which will help give a more concrete type to other
376-- variables, e.g. a before (interpTy a).
378data PArg' t = PImp { priority :: Int,
379 lazyarg :: Bool, pname :: Name, getTm :: t }
380 | PExp { priority :: Int,
381 lazyarg :: Bool, getTm :: t }
382 | PConstraint { priority :: Int,
383 lazyarg :: Bool, getTm :: t }
384 deriving (Show, Eq, Functor)
386pimp = PImp 0 False
387pexp = PExp 0 False
388pconst = PConstraint 0 False
390type PArg = PArg' PTerm
392-- Type class data
394data ClassInfo = CI { instanceName :: Name,
395 class_methods :: [(Name, PTerm)],
396 class_defaults :: [(Name, Name)], -- method name -> default impl
397 class_params :: [Name] }
398 deriving Show
400-- Syntactic sugar info
402data DSL = DSL { dsl_bind :: Name,
403 dsl_return :: Name }
404 deriving Show
406data SynContext = PatternSyntax | TermSyntax | AnySyntax
407 deriving Show
409data Syntax = Rule [SSymbol] PTerm SynContext
410 deriving Show
412data SSymbol = Keyword Name
413 | Symbol String
414 | Expr Name
415 deriving Show
417initDSL = DSL (UN ">>=") (UN "return")
419data SyntaxInfo = Syn { using :: [(Name, PTerm)],
420 syn_params :: [(Name, PTerm)],
421 syn_namespace :: [String],
422 no_imp :: [Name],
423 decoration :: Name -> Name,
424 inPattern :: Bool,
425 dsl_info :: DSL }
426 deriving Show
428defaultSyntax = Syn [] [] [] [] id False initDSL
430--- Pretty printing declarations and terms
432instance Show PTerm where
433 show tm = showImp False tm
435instance Show PDecl where
436 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
437 show (PTy _ _ n ty) = show n ++ " : " ++ show ty
438 show (PClauses _ _ n c) = showSep "\n" (map show c)
439 show (PData _ _ d) = show d
441instance Show PClause where
442 show c = showCImp True c
444instance Show PData where
445 show d = showDImp False d
447showCImp :: Bool -> PClause -> String
448showCImp impl (PClause n l ws r w)
449 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
450 ++ " where " ++ show w
451 where
452 showWs [] = ""
453 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
454showCImp impl (PWith n l ws r w)
455 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
456 ++ " { " ++ show w ++ " } "
457 where
458 showWs [] = ""
459 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
462showDImp :: Bool -> PData -> String
463showDImp impl (PDatadecl n ty cons)
464 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
465 ++ showSep "\n\t| "
466 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
468getImps :: [PArg] -> [(Name, PTerm)]
469getImps [] = []
470getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
471getImps (_ : xs) = getImps xs
473getExps :: [PArg] -> [PTerm]
474getExps [] = []
475getExps (PExp _ _ tm : xs) = tm : getExps xs
476getExps (_ : xs) = getExps xs
478getConsts :: [PArg] -> [PTerm]
479getConsts [] = []
480getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
481getConsts (_ : xs) = getConsts xs
483getAll :: [PArg] -> [PTerm]
484getAll = map getTm
486showImp :: Bool -> PTerm -> String
487showImp impl tm = se 10 tm where
488 se p (PQuote r) = "![" ++ show r ++ "]"
489 se p (PRef _ n) = show n
490 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
491 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
492 " in " ++ se 10 sc
493 se p (PPi (Exp l s) n ty sc)
494 | n `elem` allNamesIn sc = bracket p 2 $
495 if l then "|(" else "(" ++
496 show n ++ " : " ++ se 10 ty ++
497 ") " ++ st ++
498 "-> " ++ se 10 sc
499 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
500 where st = case s of
501 Static -> "[static] "
502 _ -> ""
503 se p (PPi (Imp l s) n ty sc)
504 | impl = bracket p 2 $ if l then "|{" else "{" ++
505 show n ++ " : " ++ se 10 ty ++
506 "} " ++ st ++ "-> " ++ se 10 sc
507 | otherwise = se 10 sc
508 where st = case s of
509 Static -> "[static] "
510 _ -> ""
511 se p (PPi (Constraint _ _) n ty sc)
512 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
513 se p (PApp _ (PRef _ f) [])
514 | not impl = show f
515 se p (PApp _ (PRef _ op@(UN (f:_))) args)
516 | length (getExps args) == 2 && not impl && not (isAlpha f)
517 = let [l, r] = getExps args in
518 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
519 se p (PApp _ f as)
520 = let args = getExps as in
521 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
522 else concatMap seArg args
523 se p (PHidden tm) = "." ++ se 0 tm
524 se p (PRefl _) = "refl"
525 se p (PResolveTC _) = "resolvetc"
526 se p (PTrue _) = "()"
527 se p (PFalse _) = "_|_"
528 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
529 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
530 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
531 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
532 se p PSet = "Set"
533 se p (PConstant c) = show c
534 se p (PProof ts) = "proof { " ++ show ts ++ "}"
535 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
536 se p (PMetavar n) = "?" ++ show n
537 se p Placeholder = "_"
539 sArg (PImp _ _ n tm) = siArg (n, tm)
540 sArg (PExp _ _ tm) = seArg tm
541 sArg (PConstraint _ _ tm) = scArg tm
543 seArg arg = " " ++ se 0 arg
544 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
545 scArg val = " {{" ++ se 10 val ++ "}}"
547 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
548 | otherwise = str
550allNamesIn :: PTerm -> [Name]
551allNamesIn tm = nub $ ni [] tm
552 where
553 ni env (PRef _ n)
554 | not (n `elem` env) = [n]
555 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
556 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
557 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
558 ni env (PHidden tm) = ni env tm
559 ni env (PEq _ l r) = ni env l ++ ni env r
560 ni env (PPair _ l r) = ni env l ++ ni env r
561 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
562 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
563 ni env (PAlternative ls) = concatMap (ni env) ls
564 ni env _ = []
566namesIn :: IState -> PTerm -> [Name]
567namesIn ist tm = nub $ ni [] tm
568 where
569 ni env (PRef _ n)
570 | not (n `elem` env)
571 = case lookupTy Nothing n (tt_ctxt ist) of
572 [] -> [n]
573 _ -> []
574 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
575 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
576 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
577 ni env (PEq _ l r) = ni env l ++ ni env r
578 ni env (PPair _ l r) = ni env l ++ ni env r
579 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
580 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
581 ni env (PAlternative as) = concatMap (ni env) as
582 ni env (PHidden tm) = ni env tm
583 ni env _ = []
585-- For inferring types of things
587bi = FC "builtin" 0
589inferTy = MN 0 "__Infer"
590inferCon = MN 0 "__infer"
591inferDecl = PDatadecl inferTy
592 PSet
593 [(inferCon, PPi impl (MN 0 "A") PSet (
594 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
595 (PRef bi inferTy)), bi)]
597infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
598infP = P (TCon 6 0) inferTy (Set (UVal 0))
600getInferTerm, getInferType :: Term -> Term
601getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
602getInferTerm (App (App _ _) tm) = tm
603getInferTerm tm = error ("getInferTerm " ++ show tm)
605getInferType (Bind n b sc) = Bind n b $ getInferType sc
606getInferType (App (App _ ty) _) = ty
608-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
610primNames = [unitTy, unitCon,
611 falseTy, pairTy, pairCon,
612 eqTy, eqCon, inferTy, inferCon]
614unitTy = MN 0 "__Unit"
615unitCon = MN 0 "__II"
616unitDecl = PDatadecl unitTy PSet
617 [(unitCon, PRef bi unitTy, bi)]
619falseTy = MN 0 "__False"
620falseDecl = PDatadecl falseTy PSet []
622pairTy = MN 0 "__Pair"
623pairCon = MN 0 "__MkPair"
624pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
625 [(pairCon, PPi impl (n "A") PSet (
626 PPi impl (n "B") PSet (
627 PPi expl (n "a") (PRef bi (n "A")) (
628 PPi expl (n "b") (PRef bi (n "B"))
629 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
630 pexp (PRef bi (n "B"))])))), bi)]
631 where n a = MN 0 a
633eqTy = UN "="
634eqCon = UN "refl"
635eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
636 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
637 PSet)
638 [(eqCon, PPi impl (n "a") PSet (
639 PPi impl (n "x") (PRef bi (n "a"))
640 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
641 pimp (n "b") Placeholder,
642 pexp (PRef bi (n "x")),
643 pexp (PRef bi (n "x"))])), bi)]
644 where n a = MN 0 a
646-- Defined in builtins.idr
647sigmaTy = UN "Exists"
648existsCon = UN "Ex_intro"
650piBind :: [(Name, PTerm)] -> PTerm -> PTerm
651piBind [] t = t
652piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
654-- Dealing with parameters
656expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
657expandParams dec ps ns tm = en tm
658 where
659 en (PLam n t s) = PLam n (en t) (en s)
660 en (PPi p n t s) = PPi p n (en t) (en s)
661 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)
662 en (PEq f l r) = PEq f (en l) (en r)
663 en (PPair f l r) = PPair f (en l) (en r)
664 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
665 en (PAlternative as) = PAlternative (map en as)
666 en (PHidden t) = PHidden (en t)
667 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
668 en (PProof ts) = PProof (map (fmap en) ts)
669 en (PTactics ts) = PTactics (map (fmap en) ts)
671 en (PQuote (Var n))
672 | n `elem` ns = PQuote (Var (dec n))
673 en (PApp fc (PRef fc' n) as)
674 | n `elem` ns = PApp fc (PRef fc' (dec n))
675 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
676 en (PRef fc n)
677 | n `elem` ns = PApp fc (PRef fc (dec n))
678 (map (pexp . (PRef fc)) (map fst ps))
679 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
680 en t = t
682expandParamsD :: IState ->
683 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
684expandParamsD ist dec ps ns (PTy syn fc n ty)
685 = if n `elem` ns
686 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
687 else PTy syn fc n (expandParams dec ps ns ty)
688expandParamsD ist dec ps ns (PClauses fc opts n cs)
689 = let n' = if n `elem` ns then dec n else n in
690 PClauses fc opts n' (map expandParamsC cs)
691 where
692 expandParamsC (PClause n lhs ws rhs ds)
693 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
694 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
695 n' = if n `elem` ns then dec n else n in
696 PClause n' (expandParams dec ps'' ns lhs)
697 (map (expandParams dec ps'' ns) ws)
698 (expandParams dec ps'' ns rhs)
699 (map (expandParamsD ist dec ps'' ns) ds)
700 expandParamsC (PWith n lhs ws wval ds)
701 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
702 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
703 n' = if n `elem` ns then dec n else n in
704 PWith n' (expandParams dec ps'' ns lhs)
705 (map (expandParams dec ps'' ns) ws)
706 (expandParams dec ps'' ns wval)
707 (map (expandParamsD ist dec ps'' ns) ds)
708 updateps yn nm [] = []
709 updateps yn nm (((a, t), i):as)
710 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
711 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
713expandParamsD ist dec ps ns d = d
715-- Calculate a priority for a type, for deciding elaboration order
716-- * if it's just a type variable or concrete type, do it early (0)
717-- * if there's only type variables and injective constructors, do it next (1)
718-- * if there's a function type, next (2)
719-- * finally, everything else (3)
721getPriority :: IState -> PTerm -> Int
722getPriority i tm = pri tm
723 where
724 pri (PRef _ n) =
725 case lookupP Nothing n (tt_ctxt i) of
726 ((P (DCon _ _) _ _):_) -> 1
727 ((P (TCon _ _) _ _):_) -> 1
728 ((P Ref _ _):_) -> 3
729 [] -> 0 -- must be locally bound, if it's not an error...
730 pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))
731 pri (PTrue _) = 0
732 pri (PFalse _) = 0
733 pri (PRefl _) = 1
734 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
735 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
736 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
737 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
738 pri (PAlternative as) = maximum (map pri as)
739 pri (PConstant _) = 0
740 pri Placeholder = 1
741 pri _ = 3
743-- Dealing with implicit arguments
745-- Add implicit Pi bindings for any names in the term which appear in an
746-- argument position.
748-- This has become a right mess already. Better redo it some time...
750implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
751implicit syn n ptm
752 = do i <- get
753 let (tm', impdata) = implicitise syn i ptm
754 let (tm'', spos) = findStatics i tm'
755 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
756 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
757 i <- get
758 put (i { idris_statics = addDef n spos (idris_statics i) })
759 return tm''
761implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
762implicitise syn ist tm
763 = let uvars = using syn
764 pvars = syn_params syn
765 (declimps, ns') = execState (imps True [] tm) ([], [])
766 ns = ns' \\ (map fst pvars ++ no_imp syn) in
767 if null ns
768 then (tm, reverse declimps)
769 else implicitise syn ist (pibind uvars ns tm)
770 where
771 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
772 | otherwise = x : dropAll xs ys
773 dropAll [] ys = []
775 imps top env (PApp _ f as)
776 = do (decls, ns) <- get
777 let isn = concatMap (namesIn ist) (map getTm as)
778 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
779 imps top env (PPi (Imp l _) n ty sc)
780 = do let isn = nub (namesIn ist ty) `dropAll` [n]
781 (decls , ns) <- get
782 put (PImp (getPriority ist ty) l n ty : decls,
783 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
784 imps True (n:env) sc
785 imps top env (PPi (Exp l _) n ty sc)
786 = do let isn = nub (namesIn ist ty ++ case sc of
787 (PRef _ x) -> namesIn ist sc `dropAll` [n]
788 _ -> [])
789 (decls, ns) <- get -- ignore decls in HO types
790 put (PExp (getPriority ist ty) l ty : decls,
791 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
792 imps True (n:env) sc
793 imps top env (PPi (Constraint l _) n ty sc)
794 = do let isn = nub (namesIn ist ty ++ case sc of
795 (PRef _ x) -> namesIn ist sc `dropAll` [n]
796 _ -> [])
797 (decls, ns) <- get -- ignore decls in HO types
798 put (PConstraint 10 l ty : decls,
799 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
800 imps True (n:env) sc
801 imps top env (PEq _ l r)
802 = do (decls, ns) <- get
803 let isn = namesIn ist l ++ namesIn ist r
804 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
805 imps top env (PPair _ l r)
806 = do (decls, ns) <- get
807 let isn = namesIn ist l ++ namesIn ist r
808 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
809 imps top env (PDPair _ (PRef _ n) t r)
810 = do (decls, ns) <- get
811 let isn = nub (namesIn ist t ++ namesIn ist r) \\ [n]
812 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
813 imps top env (PDPair _ l t r)
814 = do (decls, ns) <- get
815 let isn = namesIn ist l ++ namesIn ist t ++ namesIn ist r
816 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
817 imps top env (PAlternative as)
818 = do (decls, ns) <- get
819 let isn = concatMap (namesIn ist) as
820 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
821 imps top env (PLam n ty sc)
822 = do imps False env ty
823 imps False (n:env) sc
824 imps top env (PHidden tm) = imps False env tm
825 imps top env _ = return ()
827 pibind using [] sc = sc
828 pibind using (n:ns) sc
829 = case lookup n using of
830 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
831 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
833-- Add implicit arguments in function calls
835addImpl :: IState -> PTerm -> PTerm
836addImpl ist ptm = ai [] ptm
837 where
838 ai env (PRef fc f) = aiFn ist fc f []
839 ai env (PEq fc l r) = let l' = ai env l
840 r' = ai env r in
841 PEq fc l' r'
842 ai env (PPair fc l r) = let l' = ai env l
843 r' = ai env r in
844 PPair fc l' r'
845 ai env (PDPair fc l t r) = let l' = ai env l
846 t' = ai env t
847 r' = ai env r in
848 PDPair fc l' t' r'
849 ai env (PAlternative as) = let as' = map (ai env) as in
850 PAlternative as'
851 ai env (PApp fc (PRef _ f) as)
852 = let as' = map (fmap (ai env)) as in
853 aiFn ist fc f as'
854 ai env (PApp fc f as) = let f' = ai env f
855 as' = map (fmap (ai env)) as in
856 mkPApp fc 1 f' as'
857 ai env (PLam n ty sc) = let ty' = ai env ty
858 sc' = ai (n:env) sc in
859 PLam n ty' sc'
860 ai env (PLet n ty val sc)
861 = let ty' = ai env ty
862 val' = ai env val
863 sc' = ai (n:env) sc in
864 PLet n ty' val' sc'
865 ai env (PPi p n ty sc) = let ty' = ai env ty
866 sc' = ai (n:env) sc in
867 PPi p n ty' sc'
868 ai env (PHidden tm) = PHidden (ai env tm)
869 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
870 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
871 ai env tm = tm
873aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
874aiFn ist fc f as
875 | f `elem` primNames = PApp fc (PRef fc f) as
876aiFn ist fc f as
877 -- This is where namespaces get resolved by adding PAlternative
878 = case lookupCtxtName Nothing f (idris_implicits ist) of
879 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
880 [] -> mkPApp fc 1 (PRef fc f) as
881 alts -> PAlternative $
882 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
883 (insertImpl ns as)) alts
884 where
885 insertImpl :: [PArg] -> [PArg] -> [PArg]
886 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
887 PExp p l tm : insertImpl ps given
888 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
889 PConstraint p l tm : insertImpl ps given
890 insertImpl (PConstraint p l ty : ps) given =
891 PConstraint p l (PResolveTC fc) : insertImpl ps given
892 insertImpl (PImp p l n ty : ps) given =
893 case find n given [] of
894 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
895 Nothing -> PImp p l n Placeholder : insertImpl ps given
896 insertImpl expected [] = []
897 insertImpl _ given = given
899 find n [] acc = Nothing
900 find n (PImp _ _ n' t : gs) acc
901 | n == n' = Just (t, reverse acc ++ gs)
902 find n (g : gs) acc = find n gs (g : acc)
904mkPApp fc a f [] = f
905mkPApp fc a f as = let rest = drop a as in
906 appRest fc (PApp fc f (take a as)) rest
907 where
908 appRest fc f [] = f
909 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
911-- Find 'static' argument positions
912-- (the declared ones, plus any names in argument position in the declared
913-- statics)
914-- FIXME: It's possible that this really has to happen after elaboration
916findStatics :: IState -> PTerm -> (PTerm, [Bool])
917findStatics ist tm = let (ns, ss) = fs tm in
918 runState (pos ns ss tm) []
919 where fs (PPi p n t sc)
920 | Static <- pstatic p
921 = let (ns, ss) = fs sc in
922 (namesIn ist t : ns, namesIn ist t ++ n : ss)
923 | otherwise = let (ns, ss) = fs sc in
924 (namesIn ist t : ns, ss)
925 fs _ = ([], [])
927 inOne n ns = length (filter id (map (elem n) ns)) == 1
929 pos ns ss (PPi p n t sc)
930 | n `inOne` ns && elem n ss
931 = do sc' <- pos ns ss sc
932 spos <- get
933 put (True : spos)
934 return (PPi (p { pstatic = Static }) n t sc')
935 | otherwise = do sc' <- pos ns ss sc
936 spos <- get
937 put (False : spos)
938 return (PPi p n t sc')
939 pos ns ss t = return t
941-- Debugging/logging stuff
943dumpDecls :: [PDecl] -> String
944dumpDecls [] = ""
945dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
947dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
948dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
949dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
950dumpDecl (PData _ _ d) = showDImp True d
951dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
952dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
953dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
954dumpDecl (PClass _ _ cs n ps ds)
955 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
956dumpDecl (PInstance _ _ cs n _ t ds)
957 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
958dumpDecl _ = "..."
959-- dumpDecl (PImport i) = "import " ++ i
961-- syntactic match of a against b, returning pair of variables in a
962-- and what they match. Returns 'Nothing' if not a match.
964matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
965matchClause x y = match x y where
966 matchArg x y = match (getTm x) (getTm y)
968 match (PApp _ f args) (PApp _ f' args')
969 | length args == length args'
970 = do mf <- match f f'
971 ms <- zipWithM matchArg args args'
972 return (mf ++ concat ms)
973-- match (PRef _ n) (PRef _ n') | n == n' = return []
974-- | otherwise = Nothing
975 match (PRef _ n) tm = return [(n, tm)]
976 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
977 mr <- match r r'
978 return (ml ++ mr)
979 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
980 mr <- match r r'
981 return (ml ++ mr)
982 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match l l'
983 mt <- match t t'
984 mr <- match r r'
985 return (ml ++ mt ++ mr)
986 match (PAlternative as) (PAlternative as')
987 = do ms <- zipWithM match as as'
988 return (concat ms)
989 match (PRefl _) (PRefl _) = return []
990 match (PResolveTC _) (PResolveTC _) = return []
991 match (PTrue _) (PTrue _) = return []
992 match (PFalse _) (PFalse _) = return []
993 match (PReturn _) (PReturn _) = return []
994 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
995 ms <- match s s'
996 return (mt ++ ms)
997 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
998 ms <- match s s'
999 return (mt ++ ms)
1000 match (PHidden x) (PHidden y) = match x y
1001 match a b | a == b = return []
1002 | otherwise = Nothing
1004substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1005substMatches [] t = t
1006substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1008substMatch :: Name -> PTerm -> PTerm -> PTerm
1009substMatch n tm t = sm t where
1010 sm (PRef _ n') | n == n' = tm
1011 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1012 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1013 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1014 sm (PEq f x y) = PEq f (sm x) (sm y)
1015 sm (PPair f x y) = PPair f (sm x) (sm y)
1016 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1017 sm (PAlternative as) = PAlternative (map sm as)
1018 sm (PHidden x) = PHidden (sm x)
1019 sm x = x