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