git.iko.soy/Idris-dev
on ddba413 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1016 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
144setLogLevel :: Int -> Idris ()
145setLogLevel l = do i <- get
146 let opts = idris_options i
147 let opt' = opts { opt_logLevel = l }
148 put (i { idris_options = opt' } )
150logLevel :: Idris Int
151logLevel = do i <- get
152 return (opt_logLevel (idris_options i))
154impShow :: Idris Bool
155impShow = do i <- get
156 return (opt_showimp (idris_options i))
158setImpShow :: Bool -> Idris ()
159setImpShow t = do i <- get
160 let opts = idris_options i
161 let opt' = opts { opt_showimp = t }
162 put (i { idris_options = opt' })
164logLvl :: Int -> String -> Idris ()
165logLvl l str = do i <- get
166 let lvl = opt_logLevel (idris_options i)
167 when (lvl >= l)
168 $ do lift (putStrLn str)
169 put (i { idris_log = idris_log i ++ str ++ "\n" } )
171iLOG :: String -> Idris ()
172iLOG = logLvl 1
174noErrors :: Idris Bool
175noErrors = do i <- get
176 case errLine i of
177 Nothing -> return True
178 _ -> return False
180setTypeCase :: Bool -> Idris ()
181setTypeCase t = do i <- get
182 let opts = idris_options i
183 let opt' = opts { opt_typecase = t }
184 put (i { idris_options = opt' })
186-- Commands in the REPL
188data Command = Quit | Help | Eval PTerm | Check PTerm | Reload | Edit
189 | Compile String | Execute String
190 | Metavars | Prove Name | AddProof | Universes
191 | TTShell
192 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name
193 | NOP
195-- Parsed declarations
197data Fixity = Infixl { prec :: Int }
198 | Infixr { prec :: Int }
199 | InfixN { prec :: Int }
200 | PrefixN { prec :: Int }
201 deriving Eq
203instance Show Fixity where
204 show (Infixl i) = "infixl " ++ show i
205 show (Infixr i) = "infixr " ++ show i
206 show (InfixN i) = "infix " ++ show i
207 show (PrefixN i) = "prefix " ++ show i
209data FixDecl = Fix Fixity String
210 deriving (Show, Eq)
212instance Ord FixDecl where
213 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
216data Static = Static | Dynamic
217 deriving (Show, Eq)
219-- Mark bindings with their explicitness, and laziness
220data Plicity = Imp { plazy :: Bool,
221 pstatic :: Static }
222 | Exp { plazy :: Bool,
223 pstatic :: Static }
224 | Constraint { plazy :: Bool,
225 pstatic :: Static }
226 deriving (Show, Eq)
228impl = Imp False Dynamic
229expl = Exp False Dynamic
230constraint = Constraint False Static
232type FnOpts = Bool -- just inlinable, for now
234inlinable :: FnOpts -> Bool
235inlinable x = x
237data PDecl' t = PFix FC Fixity [String] -- fixity declaration
238 | PTy SyntaxInfo FC Name t -- type declaration
239 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
240 | PData SyntaxInfo FC (PData' t) -- data declaration
241 | PParams FC [(Name, t)] [PDecl' t] -- params block
242 | PNamespace String [PDecl' t] -- new namespace
243 | PClass SyntaxInfo FC
244 [t] -- constraints
245 Name
246 [(Name, t)] -- parameters
247 [PDecl' t] -- declarations
248 | PInstance SyntaxInfo FC [t] -- constraints
249 Name -- class
250 [t] -- parameters
251 t -- full instance type
252 [PDecl' t]
253 | PSyntax FC Syntax
254 | PDirective (Idris ())
255 deriving Functor
257data PClause' t = PClause Name t [t] t [PDecl' t]
258 | PWith Name t [t] t [PDecl' t]
259 deriving Functor
261data PData' t = PDatadecl { d_name :: Name,
262 d_tcon :: t,
263 d_cons :: [(Name, t, FC)] }
264 deriving Functor
266-- Handy to get a free function for applying PTerm -> PTerm functions
267-- across a program, by deriving Functor
269type PDecl = PDecl' PTerm
270type PData = PData' PTerm
271type PClause = PClause' PTerm
273-- get all the names declared in a decl
275declared :: PDecl -> [Name]
276declared (PFix _ _ _) = []
277declared (PTy _ _ n t) = [n]
278declared (PClauses _ _ n _) = [] -- not a declaration
279declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
280 where fstt (a, _, _) = a
281declared (PParams _ _ ds) = concatMap declared ds
282declared (PNamespace _ ds) = concatMap declared ds
283-- declared (PImport _) = []
285updateN :: [(Name, Name)] -> Name -> Name
286updateN ns n | Just n' <- lookup n ns = n'
287updateN _ n = n
289updateNs :: [(Name, Name)] -> PTerm -> PTerm
290updateNs [] t = t
291updateNs ns t = mapPT updateRef t
292 where updateRef (PRef fc f) = PRef fc (updateN ns f)
293 updateRef t = t
295-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
296-- updateDNs [] t = t
297-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
298-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
299-- where updateCNs ns (PClause n l ts r ds)
300-- = PClause (updateN ns n) (fmap (updateNs ns) l)
301-- (map (fmap (updateNs ns)) ts)
302-- (fmap (updateNs ns) r)
303-- (map (updateDNs ns) ds)
304-- updateDNs ns c = c
306-- High level language terms
308data PTerm = PQuote Raw
309 | PRef FC Name
310 | PLam Name PTerm PTerm
311 | PPi Plicity Name PTerm PTerm
312 | PLet Name PTerm PTerm PTerm
313 | PApp FC PTerm [PArg]
314 | PTrue FC
315 | PFalse FC
316 | PRefl FC
317 | PResolveTC FC
318 | PEq FC PTerm PTerm
319 | PPair FC PTerm PTerm
320 | PDPair FC PTerm PTerm PTerm
321 | PAlternative [PTerm]
322 | PHidden PTerm -- irrelevant or hidden pattern
323 | PSet
324 | PConstant Const
325 | Placeholder
326 | PDoBlock [PDo]
327 | PReturn FC
328 | PMetavar Name
329 | PProof [PTactic]
330 | PTactics [PTactic] -- as PProof, but no auto solving
331 | PElabError String -- error to report on elaboration
332 deriving Eq
334mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
335mapPT f t = f (mpt t) where
336 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
337 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
338 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
339 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
340 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
341 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
342 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
343 mpt (PAlternative as) = PAlternative (map (mapPT f) as)
344 mpt (PHidden t) = PHidden (mapPT f t)
345 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
346 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
347 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
348 mpt x = x
351data PTactic' t = Intro [Name] | Focus Name
352 | Refine Name [Bool] | Rewrite t | LetTac Name t
353 | Exact t | Compute | Trivial
354 | Solve
355 | Attack
356 | ProofState | ProofTerm | Undo
357 | Try (PTactic' t) (PTactic' t)
358 | TSeq (PTactic' t) (PTactic' t)
359 | Qed
360 deriving (Show, Eq, Functor)
362type PTactic = PTactic' PTerm
364data PDo' t = DoExp FC t
365 | DoBind FC Name t
366 | DoLet FC Name t
367 deriving (Eq, Functor)
369type PDo = PDo' PTerm
371-- The priority gives a hint as to elaboration order. Best to elaborate
372-- things early which will help give a more concrete type to other
373-- variables, e.g. a before (interpTy a).
375data PArg' t = PImp { priority :: Int,
376 lazyarg :: Bool, pname :: Name, getTm :: t }
377 | PExp { priority :: Int,
378 lazyarg :: Bool, getTm :: t }
379 | PConstraint { priority :: Int,
380 lazyarg :: Bool, getTm :: t }
381 deriving (Show, Eq, Functor)
383pimp = PImp 0 False
384pexp = PExp 0 False
385pconst = PConstraint 0 False
387type PArg = PArg' PTerm
389-- Type class data
391data ClassInfo = CI { instanceName :: Name,
392 class_methods :: [(Name, PTerm)],
393 class_params :: [Name] }
394 deriving Show
396-- Syntactic sugar info
398data DSL = DSL { dsl_bind :: Name,
399 dsl_return :: Name }
400 deriving Show
402data SynContext = PatternSyntax | TermSyntax | AnySyntax
403 deriving Show
405data Syntax = Rule [SSymbol] PTerm SynContext
406 deriving Show
408data SSymbol = Keyword Name
409 | Symbol String
410 | Expr Name
411 deriving Show
413initDSL = DSL (UN ">>=") (UN "return")
415data SyntaxInfo = Syn { using :: [(Name, PTerm)],
416 syn_params :: [(Name, PTerm)],
417 syn_namespace :: [String],
418 no_imp :: [Name],
419 decoration :: Name -> Name,
420 inPattern :: Bool,
421 dsl_info :: DSL }
422 deriving Show
424defaultSyntax = Syn [] [] [] [] id False initDSL
426--- Pretty printing declarations and terms
428instance Show PTerm where
429 show tm = showImp False tm
431instance Show PDecl where
432 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
433 show (PTy _ _ n ty) = show n ++ " : " ++ show ty
434 show (PClauses _ _ n c) = showSep "\n" (map show c)
435 show (PData _ _ d) = show d
437instance Show PClause where
438 show c = showCImp True c
440instance Show PData where
441 show d = showDImp False d
443showCImp :: Bool -> PClause -> String
444showCImp impl (PClause n l ws r w)
445 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
446 ++ " where " ++ show w
447 where
448 showWs [] = ""
449 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
450showCImp impl (PWith n l ws r w)
451 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
452 ++ " { " ++ show w ++ " } "
453 where
454 showWs [] = ""
455 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
458showDImp :: Bool -> PData -> String
459showDImp impl (PDatadecl n ty cons)
460 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
461 ++ showSep "\n\t| "
462 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
464getImps :: [PArg] -> [(Name, PTerm)]
465getImps [] = []
466getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
467getImps (_ : xs) = getImps xs
469getExps :: [PArg] -> [PTerm]
470getExps [] = []
471getExps (PExp _ _ tm : xs) = tm : getExps xs
472getExps (_ : xs) = getExps xs
474getConsts :: [PArg] -> [PTerm]
475getConsts [] = []
476getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
477getConsts (_ : xs) = getConsts xs
479getAll :: [PArg] -> [PTerm]
480getAll = map getTm
482showImp :: Bool -> PTerm -> String
483showImp impl tm = se 10 tm where
484 se p (PQuote r) = "![" ++ show r ++ "]"
485 se p (PRef _ n) = show n
486 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
487 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
488 " in " ++ se 10 sc
489 se p (PPi (Exp l s) n ty sc)
490 | n `elem` allNamesIn sc = bracket p 2 $
491 if l then "|(" else "(" ++
492 show n ++ " : " ++ se 10 ty ++
493 ") " ++ st ++
494 "-> " ++ se 10 sc
495 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
496 where st = case s of
497 Static -> "[static] "
498 _ -> ""
499 se p (PPi (Imp l s) n ty sc)
500 | impl = bracket p 2 $ if l then "|{" else "{" ++
501 show n ++ " : " ++ se 10 ty ++
502 "} " ++ st ++ "-> " ++ se 10 sc
503 | otherwise = se 10 sc
504 where st = case s of
505 Static -> "[static] "
506 _ -> ""
507 se p (PPi (Constraint _ _) n ty sc)
508 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
509 se p (PApp _ (PRef _ f) [])
510 | not impl = show f
511 se p (PApp _ (PRef _ op@(UN (f:_))) args)
512 | length (getExps args) == 2 && not impl && not (isAlpha f)
513 = let [l, r] = getExps args in
514 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
515 se p (PApp _ f as)
516 = let args = getExps as in
517 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
518 else concatMap seArg args
519 se p (PHidden tm) = "." ++ se 0 tm
520 se p (PRefl _) = "refl"
521 se p (PResolveTC _) = "resolvetc"
522 se p (PTrue _) = "()"
523 se p (PFalse _) = "_|_"
524 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
525 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
526 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
527 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
528 se p PSet = "Set"
529 se p (PConstant c) = show c
530 se p (PProof ts) = "proof { " ++ show ts ++ "}"
531 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
532 se p (PMetavar n) = "?" ++ show n
533 se p Placeholder = "_"
535 sArg (PImp _ _ n tm) = siArg (n, tm)
536 sArg (PExp _ _ tm) = seArg tm
537 sArg (PConstraint _ _ tm) = scArg tm
539 seArg arg = " " ++ se 0 arg
540 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
541 scArg val = " {{" ++ se 10 val ++ "}}"
543 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
544 | otherwise = str
546allNamesIn :: PTerm -> [Name]
547allNamesIn tm = nub $ ni [] tm
548 where
549 ni env (PRef _ n)
550 | not (n `elem` env) = [n]
551 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
552 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
553 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
554 ni env (PHidden tm) = ni env tm
555 ni env (PEq _ l r) = ni env l ++ ni env r
556 ni env (PPair _ l r) = ni env l ++ ni env r
557 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
558 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
559 ni env (PAlternative ls) = concatMap (ni env) ls
560 ni env _ = []
562namesIn :: IState -> PTerm -> [Name]
563namesIn ist tm = nub $ ni [] tm
564 where
565 ni env (PRef _ n)
566 | not (n `elem` env)
567 = case lookupTy Nothing n (tt_ctxt ist) of
568 [] -> [n]
569 _ -> []
570 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
571 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
572 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
573 ni env (PEq _ l r) = ni env l ++ ni env r
574 ni env (PPair _ l r) = ni env l ++ ni env r
575 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
576 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
577 ni env (PAlternative as) = concatMap (ni env) as
578 ni env (PHidden tm) = ni env tm
579 ni env _ = []
581-- For inferring types of things
583bi = FC "builtin" 0
585inferTy = MN 0 "__Infer"
586inferCon = MN 0 "__infer"
587inferDecl = PDatadecl inferTy
588 PSet
589 [(inferCon, PPi impl (MN 0 "A") PSet (
590 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
591 (PRef bi inferTy)), bi)]
593infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
594infP = P (TCon 6 0) inferTy (Set (UVal 0))
596getInferTerm, getInferType :: Term -> Term
597getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
598getInferTerm (App (App _ _) tm) = tm
599getInferTerm tm = error ("getInferTerm " ++ show tm)
601getInferType (Bind n b sc) = Bind n b $ getInferType sc
602getInferType (App (App _ ty) _) = ty
604-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
606primNames = [unitTy, unitCon,
607 falseTy, pairTy, pairCon,
608 eqTy, eqCon, inferTy, inferCon]
610unitTy = MN 0 "__Unit"
611unitCon = MN 0 "__II"
612unitDecl = PDatadecl unitTy PSet
613 [(unitCon, PRef bi unitTy, bi)]
615falseTy = MN 0 "__False"
616falseDecl = PDatadecl falseTy PSet []
618pairTy = MN 0 "__Pair"
619pairCon = MN 0 "__MkPair"
620pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
621 [(pairCon, PPi impl (n "A") PSet (
622 PPi impl (n "B") PSet (
623 PPi expl (n "a") (PRef bi (n "A")) (
624 PPi expl (n "b") (PRef bi (n "B"))
625 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
626 pexp (PRef bi (n "B"))])))), bi)]
627 where n a = MN 0 a
629eqTy = UN "="
630eqCon = UN "refl"
631eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
632 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
633 PSet)
634 [(eqCon, PPi impl (n "a") PSet (
635 PPi impl (n "x") (PRef bi (n "a"))
636 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
637 pimp (n "b") Placeholder,
638 pexp (PRef bi (n "x")),
639 pexp (PRef bi (n "x"))])), bi)]
640 where n a = MN 0 a
642-- Defined in builtins.idr
643sigmaTy = UN "Exists"
644existsCon = UN "Ex_intro"
646piBind :: [(Name, PTerm)] -> PTerm -> PTerm
647piBind [] t = t
648piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
650-- Dealing with parameters
652expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
653expandParams dec ps ns tm = en tm
654 where
655 en (PLam n t s) = PLam n (en t) (en s)
656 en (PPi p n t s) = PPi p n (en t) (en s)
657 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)
658 en (PEq f l r) = PEq f (en l) (en r)
659 en (PPair f l r) = PPair f (en l) (en r)
660 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
661 en (PAlternative as) = PAlternative (map en as)
662 en (PHidden t) = PHidden (en t)
663 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
664 en (PProof ts) = PProof (map (fmap en) ts)
665 en (PTactics ts) = PTactics (map (fmap en) ts)
667 en (PQuote (Var n))
668 | n `elem` ns = PQuote (Var (dec n))
669 en (PApp fc (PRef fc' n) as)
670 | n `elem` ns = PApp fc (PRef fc' (dec n))
671 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
672 en (PRef fc n)
673 | n `elem` ns = PApp fc (PRef fc (dec n))
674 (map (pexp . (PRef fc)) (map fst ps))
675 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
676 en t = t
678expandParamsD :: IState ->
679 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
680expandParamsD ist dec ps ns (PTy syn fc n ty)
681 = if n `elem` ns
682 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
683 else PTy syn fc n (expandParams dec ps ns ty)
684expandParamsD ist dec ps ns (PClauses fc opts n cs)
685 = let n' = if n `elem` ns then dec n else n in
686 PClauses fc opts n' (map expandParamsC cs)
687 where
688 expandParamsC (PClause n lhs ws rhs ds)
689 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
690 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
691 n' = if n `elem` ns then dec n else n in
692 PClause n' (expandParams dec ps'' ns lhs)
693 (map (expandParams dec ps'' ns) ws)
694 (expandParams dec ps'' ns rhs)
695 (map (expandParamsD ist dec ps'' ns) ds)
696 expandParamsC (PWith n lhs ws wval ds)
697 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
698 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
699 n' = if n `elem` ns then dec n else n in
700 PWith n' (expandParams dec ps'' ns lhs)
701 (map (expandParams dec ps'' ns) ws)
702 (expandParams dec ps'' ns wval)
703 (map (expandParamsD ist dec ps'' ns) ds)
704 updateps yn nm [] = []
705 updateps yn nm (((a, t), i):as)
706 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
707 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
709expandParamsD ist dec ps ns d = d
711-- Calculate a priority for a type, for deciding elaboration order
712-- * if it's just a type variable or concrete type, do it early (0)
713-- * if there's only type variables and injective constructors, do it next (1)
714-- * if there's a function type, next (2)
715-- * finally, everything else (3)
717getPriority :: IState -> PTerm -> Int
718getPriority i tm = pri tm
719 where
720 pri (PRef _ n) =
721 case lookupP Nothing n (tt_ctxt i) of
722 ((P (DCon _ _) _ _):_) -> 1
723 ((P (TCon _ _) _ _):_) -> 1
724 ((P Ref _ _):_) -> 3
725 [] -> 0 -- must be locally bound, if it's not an error...
726 pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))
727 pri (PTrue _) = 0
728 pri (PFalse _) = 0
729 pri (PRefl _) = 1
730 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
731 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
732 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
733 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
734 pri (PAlternative as) = maximum (map pri as)
735 pri (PConstant _) = 0
736 pri Placeholder = 1
737 pri _ = 3
739-- Dealing with implicit arguments
741-- Add implicit Pi bindings for any names in the term which appear in an
742-- argument position.
744-- This has become a right mess already. Better redo it some time...
746implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
747implicit syn n ptm
748 = do i <- get
749 let (tm', impdata) = implicitise syn i ptm
750 let (tm'', spos) = findStatics i tm'
751 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
752 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
753 i <- get
754 put (i { idris_statics = addDef n spos (idris_statics i) })
755 return tm''
757implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
758implicitise syn ist tm
759 = let uvars = using syn
760 pvars = syn_params syn
761 (declimps, ns') = execState (imps True [] tm) ([], [])
762 ns = ns' \\ (map fst pvars ++ no_imp syn) in
763 if null ns
764 then (tm, reverse declimps)
765 else implicitise syn ist (pibind uvars ns tm)
766 where
767 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
768 | otherwise = x : dropAll xs ys
769 dropAll [] ys = []
771 imps top env (PApp _ f as)
772 = do (decls, ns) <- get
773 let isn = concatMap (namesIn ist) (map getTm as)
774 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
775 imps top env (PPi (Imp l _) n ty sc)
776 = do let isn = nub (namesIn ist ty) `dropAll` [n]
777 (decls , ns) <- get
778 put (PImp (getPriority ist ty) l n ty : decls,
779 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
780 imps True (n:env) sc
781 imps top env (PPi (Exp l _) n ty sc)
782 = do let isn = nub (namesIn ist ty ++ case sc of
783 (PRef _ x) -> namesIn ist sc `dropAll` [n]
784 _ -> [])
785 (decls, ns) <- get -- ignore decls in HO types
786 put (PExp (getPriority ist ty) l ty : decls,
787 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
788 imps True (n:env) sc
789 imps top env (PPi (Constraint l _) n ty sc)
790 = do let isn = nub (namesIn ist ty ++ case sc of
791 (PRef _ x) -> namesIn ist sc `dropAll` [n]
792 _ -> [])
793 (decls, ns) <- get -- ignore decls in HO types
794 put (PConstraint 10 l ty : decls,
795 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
796 imps True (n:env) sc
797 imps top env (PEq _ l r)
798 = do (decls, ns) <- get
799 let isn = namesIn ist l ++ namesIn ist r
800 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
801 imps top env (PPair _ 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 (PDPair _ (PRef _ n) t r)
806 = do (decls, ns) <- get
807 let isn = nub (namesIn ist t ++ namesIn ist r) \\ [n]
808 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
809 imps top env (PDPair _ l t r)
810 = do (decls, ns) <- get
811 let isn = namesIn ist l ++ namesIn ist t ++ namesIn ist r
812 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
813 imps top env (PAlternative as)
814 = do (decls, ns) <- get
815 let isn = concatMap (namesIn ist) as
816 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
817 imps top env (PLam n ty sc)
818 = do imps False env ty
819 imps False (n:env) sc
820 imps top env (PHidden tm) = imps False env tm
821 imps top env _ = return ()
823 pibind using [] sc = sc
824 pibind using (n:ns) sc
825 = case lookup n using of
826 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
827 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
829-- Add implicit arguments in function calls
831addImpl :: IState -> PTerm -> PTerm
832addImpl ist ptm = ai [] ptm
833 where
834 ai env (PRef fc f) = aiFn ist fc f []
835 ai env (PEq fc l r) = let l' = ai env l
836 r' = ai env r in
837 PEq fc l' r'
838 ai env (PPair fc l r) = let l' = ai env l
839 r' = ai env r in
840 PPair fc l' r'
841 ai env (PDPair fc l t r) = let l' = ai env l
842 t' = ai env t
843 r' = ai env r in
844 PDPair fc l' t' r'
845 ai env (PAlternative as) = let as' = map (ai env) as in
846 PAlternative as'
847 ai env (PApp fc (PRef _ f) as)
848 = let as' = map (fmap (ai env)) as in
849 aiFn ist fc f as'
850 ai env (PApp fc f as) = let f' = ai env f
851 as' = map (fmap (ai env)) as in
852 mkPApp fc 1 f' as'
853 ai env (PLam n ty sc) = let ty' = ai env ty
854 sc' = ai (n:env) sc in
855 PLam n ty' sc'
856 ai env (PLet n ty val sc)
857 = let ty' = ai env ty
858 val' = ai env val
859 sc' = ai (n:env) sc in
860 PLet n ty' val' sc'
861 ai env (PPi p n ty sc) = let ty' = ai env ty
862 sc' = ai (n:env) sc in
863 PPi p n ty' sc'
864 ai env (PHidden tm) = PHidden (ai env tm)
865 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
866 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
867 ai env tm = tm
869aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
870aiFn ist fc f as
871 | f `elem` primNames = PApp fc (PRef fc f) as
872aiFn ist fc f as
873 -- This is where namespaces get resolved by adding PAlternative
874 = case lookupCtxtName Nothing f (idris_implicits ist) of
875 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
876 [] -> mkPApp fc 1 (PRef fc f) as
877 alts -> PAlternative $
878 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
879 (insertImpl ns as)) alts
880 where
881 insertImpl :: [PArg] -> [PArg] -> [PArg]
882 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
883 PExp p l tm : insertImpl ps given
884 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
885 PConstraint p l tm : insertImpl ps given
886 insertImpl (PConstraint p l ty : ps) given =
887 PConstraint p l (PResolveTC fc) : insertImpl ps given
888 insertImpl (PImp p l n ty : ps) given =
889 case find n given [] of
890 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
891 Nothing -> PImp p l n Placeholder : insertImpl ps given
892 insertImpl expected [] = []
893 insertImpl _ given = given
895 find n [] acc = Nothing
896 find n (PImp _ _ n' t : gs) acc
897 | n == n' = Just (t, reverse acc ++ gs)
898 find n (g : gs) acc = find n gs (g : acc)
900mkPApp fc a f [] = f
901mkPApp fc a f as = let rest = drop a as in
902 appRest fc (PApp fc f (take a as)) rest
903 where
904 appRest fc f [] = f
905 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
907-- Find 'static' argument positions
908-- (the declared ones, plus any names in argument position in the declared
909-- statics)
910-- FIXME: It's possible that this really has to happen after elaboration
912findStatics :: IState -> PTerm -> (PTerm, [Bool])
913findStatics ist tm = let (ns, ss) = fs tm in
914 runState (pos ns ss tm) []
915 where fs (PPi p n t sc)
916 | Static <- pstatic p
917 = let (ns, ss) = fs sc in
918 (namesIn ist t : ns, namesIn ist t ++ n : ss)
919 | otherwise = let (ns, ss) = fs sc in
920 (namesIn ist t : ns, ss)
921 fs _ = ([], [])
923 inOne n ns = length (filter id (map (elem n) ns)) == 1
925 pos ns ss (PPi p n t sc)
926 | n `inOne` ns && elem n ss
927 = do sc' <- pos ns ss sc
928 spos <- get
929 put (True : spos)
930 return (PPi (p { pstatic = Static }) n t sc')
931 | otherwise = do sc' <- pos ns ss sc
932 spos <- get
933 put (False : spos)
934 return (PPi p n t sc')
935 pos ns ss t = return t
937-- Debugging/logging stuff
939dumpDecls :: [PDecl] -> String
940dumpDecls [] = ""
941dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
943dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
944dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
945dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
946dumpDecl (PData _ _ d) = showDImp True d
947dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
948dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
949dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
950dumpDecl (PClass _ _ cs n ps ds)
951 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
952dumpDecl (PInstance _ _ cs n _ t ds)
953 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
954dumpDecl _ = "..."
955-- dumpDecl (PImport i) = "import " ++ i
957-- syntactic match of a against b, returning pair of variables in a
958-- and what they match. Returns 'Nothing' if not a match.
960matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
961matchClause x y = match x y where
962 matchArg x y = match (getTm x) (getTm y)
964 match (PApp _ f args) (PApp _ f' args')
965 | length args == length args'
966 = do mf <- match f f'
967 ms <- zipWithM matchArg args args'
968 return (mf ++ concat ms)
969-- match (PRef _ n) (PRef _ n') | n == n' = return []
970-- | otherwise = Nothing
971 match (PRef _ n) tm = return [(n, tm)]
972 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
973 mr <- match r r'
974 return (ml ++ mr)
975 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
976 mr <- match r r'
977 return (ml ++ mr)
978 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match l l'
979 mt <- match t t'
980 mr <- match r r'
981 return (ml ++ mt ++ mr)
982 match (PAlternative as) (PAlternative as')
983 = do ms <- zipWithM match as as'
984 return (concat ms)
985 match (PRefl _) (PRefl _) = return []
986 match (PResolveTC _) (PResolveTC _) = return []
987 match (PTrue _) (PTrue _) = return []
988 match (PFalse _) (PFalse _) = return []
989 match (PReturn _) (PReturn _) = return []
990 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
991 ms <- match s s'
992 return (mt ++ ms)
993 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
994 ms <- match s s'
995 return (mt ++ ms)
996 match (PHidden x) (PHidden y) = match x y
997 match a b | a == b = return []
998 | otherwise = Nothing
1000substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1001substMatches [] t = t
1002substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1004substMatch :: Name -> PTerm -> PTerm -> PTerm
1005substMatch n tm t = sm t where
1006 sm (PRef _ n') | n == n' = tm
1007 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1008 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1009 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1010 sm (PEq f x y) = PEq f (sm x) (sm y)
1011 sm (PPair f x y) = PPair f (sm x) (sm y)
1012 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1013 sm (PAlternative as) = PAlternative (map sm as)
1014 sm (PHidden x) = PHidden (sm x)
1015 sm x = x