git.iko.soy/Idris-dev
on d676ca6 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
926 lines 35 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 }
21 deriving (Show, Eq)
23defaultOpts = IOption 0 False
25-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
26-- without typechecking).
27-- This will include all the functions and data declarations, plus fixity declarations
28-- and syntax macros.
30data IState = IState { tt_ctxt :: Context,
31 idris_infixes :: [FixDecl],
32 idris_implicits :: Ctxt [PArg],
33 idris_statics :: Ctxt [Bool],
34 idris_classes :: Ctxt ClassInfo,
35 idris_log :: String,
36 idris_options :: IOption,
37 idris_name :: Int,
38 idris_metavars :: [Name],
39 syntax_rules :: [Syntax],
40 syntax_keywords :: [String],
41 imported :: [FilePath],
42 idris_prims :: [(Name, ([E.Name], E.Term))],
43 errLine :: Maybe Int
44 }
46idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext
47 "" defaultOpts 6 [] [] [] [] [] Nothing
49-- The monad for the main REPL - reading and processing files and updating
50-- global state (hence the IO inner monad).
51type Idris a = StateT IState IO a
53getContext :: Idris Context
54getContext = do i <- get; return (tt_ctxt i)
56setErrLine :: Int -> Idris ()
57setErrLine x = do i <- get;
58 case (errLine i) of
59 Nothing -> put (i { errLine = Just x })
60 Just _ -> return ()
62clearErr :: Idris ()
63clearErr = do i <- get
64 put (i { errLine = Nothing })
66getIState :: Idris IState
67getIState = get
69putIState :: IState -> Idris ()
70putIState = put
72getName :: Idris Int
73getName = do i <- get;
74 let idx = idris_name i;
75 put (i { idris_name = idx + 1 })
76 return idx
78checkUndefined :: FC -> Name -> Idris ()
79checkUndefined fc n
80 = do i <- getContext
81 case lookupCtxt n i of
82 Just _ -> fail $ show fc ++ ":" ++
83 show n ++ " already defined"
84 _ -> return ()
86setContext :: Context -> Idris ()
87setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
89updateContext :: (Context -> Context) -> Idris ()
90updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
92addDeferred :: [(Name, Type)] -> Idris ()
93addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
94 i <- get
95 put (i { idris_metavars = map fst ns ++ idris_metavars i })
96 where tidyNames used (Bind (MN i x) b sc)
97 = let n' = uniqueName (UN [x]) used in
98 Bind n' b $ tidyNames (n':used) sc
99 tidyNames used (Bind n b sc)
100 = let n' = uniqueName n used in
101 Bind n' b $ tidyNames (n':used) sc
102 tidyNames used b = b
104solveDeferred :: Name -> Idris ()
105solveDeferred n = do i <- get
106 put (i { idris_metavars = idris_metavars i \\ [n] })
108iputStrLn :: String -> Idris ()
109iputStrLn = lift.putStrLn
111setLogLevel :: Int -> Idris ()
112setLogLevel l = do i <- get
113 let opts = idris_options i
114 let opt' = opts { opt_logLevel = l }
115 put (i { idris_options = opt' } )
117logLevel :: Idris Int
118logLevel = do i <- get
119 return (opt_logLevel (idris_options i))
121logLvl :: Int -> String -> Idris ()
122logLvl l str = do i <- get
123 let lvl = opt_logLevel (idris_options i)
124 when (lvl >= l)
125 $ do lift (putStrLn str)
126 put (i { idris_log = idris_log i ++ str ++ "\n" } )
128iLOG :: String -> Idris ()
129iLOG = logLvl 1
131noErrors :: Idris Bool
132noErrors = do i <- get
133 case errLine i of
134 Nothing -> return True
135 _ -> return False
137setTypeCase :: Bool -> Idris ()
138setTypeCase t = do i <- get
139 let opts = idris_options i
140 let opt' = opts { opt_typecase = t }
141 put (i { idris_options = opt' })
143-- Commands in the REPL
145data Command = Quit | Help | Eval PTerm | Check PTerm | Reload | Edit
146 | Compile String | Execute String
147 | Metavars | Prove Name
148 | TTShell
149 | LogLvl Int | Spec PTerm | HNF PTerm
150 | NOP
152-- Parsed declarations
154data Fixity = Infixl { prec :: Int }
155 | Infixr { prec :: Int }
156 | InfixN { prec :: Int }
157 | PrefixN { prec :: Int }
158 deriving Eq
160instance Show Fixity where
161 show (Infixl i) = "infixl " ++ show i
162 show (Infixr i) = "infixr " ++ show i
163 show (InfixN i) = "infix " ++ show i
164 show (PrefixN i) = "prefix " ++ show i
166data FixDecl = Fix Fixity String
167 deriving (Show, Eq)
169instance Ord FixDecl where
170 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
173data Static = Static | Dynamic
174 deriving (Show, Eq)
176-- Mark bindings with their explicitness, and laziness
177data Plicity = Imp { plazy :: Bool,
178 pstatic :: Static }
179 | Exp { plazy :: Bool,
180 pstatic :: Static }
181 | Constraint { plazy :: Bool,
182 pstatic :: Static }
183 deriving (Show, Eq)
185impl = Imp False Dynamic
186expl = Exp False Dynamic
187constraint = Constraint False Static
189data PDecl' t = PFix FC Fixity [String] -- fixity declaration
190 | PTy SyntaxInfo FC Name t -- type declaration
191 | PClauses FC Name [PClause' t] -- pattern clause
192 | PData SyntaxInfo FC (PData' t) -- data declaration
193 | PParams FC [(Name, t)] [PDecl' t] -- params block
194 | PClass SyntaxInfo FC
195 [t] -- constraints
196 Name
197 [(Name, t)] -- parameters
198 [PDecl' t] -- declarations
199 | PInstance SyntaxInfo FC [t] -- constraints
200 Name -- class
201 [t] -- parameters
202 t -- full instance type
203 [PDecl' t]
204 | PSyntax FC Syntax
205 deriving Functor
207data PClause' t = PClause Name t [t] t [PDecl' t]
208 | PWith Name t [t] t [PDecl' t]
209 deriving Functor
211data PData' t = PDatadecl { d_name :: Name,
212 d_tcon :: t,
213 d_cons :: [(Name, t, FC)] }
214 deriving Functor
216-- Handy to get a free function for applying PTerm -> PTerm functions
217-- across a program, by deriving Functor
219type PDecl = PDecl' PTerm
220type PData = PData' PTerm
221type PClause = PClause' PTerm
223-- get all the names declared in a decl
225declared :: PDecl -> [Name]
226declared (PFix _ _ _) = []
227declared (PTy _ _ n t) = [n]
228declared (PClauses _ n _) = [] -- not a declaration
229declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
230 where fstt (a, _, _) = a
231declared (PParams _ _ ds) = concatMap declared ds
232-- declared (PImport _) = []
234updateN :: [(Name, Name)] -> Name -> Name
235updateN ns n | Just n' <- lookup n ns = n'
236updateN _ n = n
238updateNs :: [(Name, Name)] -> PTerm -> PTerm
239updateNs [] t = t
240updateNs ns t = mapPT updateRef t
241 where updateRef (PRef fc f) = PRef fc (updateN ns f)
242 updateRef t = t
244-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
245-- updateDNs [] t = t
246-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
247-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
248-- where updateCNs ns (PClause n l ts r ds)
249-- = PClause (updateN ns n) (fmap (updateNs ns) l)
250-- (map (fmap (updateNs ns)) ts)
251-- (fmap (updateNs ns) r)
252-- (map (updateDNs ns) ds)
253-- updateDNs ns c = c
255-- High level language terms
257data PTerm = PQuote Raw
258 | PRef FC Name
259 | PLam Name PTerm PTerm
260 | PPi Plicity Name PTerm PTerm
261 | PLet Name PTerm PTerm PTerm
262 | PApp FC PTerm [PArg]
263 | PTrue FC
264 | PFalse FC
265 | PRefl FC
266 | PResolveTC FC
267 | PEq FC PTerm PTerm
268 | PPair FC PTerm PTerm
269 | PDPair FC PTerm PTerm
270 | PHidden PTerm -- irrelevant or hidden pattern
271 | PSet
272 | PConstant Const
273 | Placeholder
274 | PDoBlock [PDo]
275 | PReturn FC
276 | PMetavar Name
277 | PProof [PTactic]
278 | PElabError String -- error to report on elaboration
279 deriving Eq
281mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
282mapPT f t = f (mpt t) where
283 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
284 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
285 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
286 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
287 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
288 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
289 mpt (PDPair fc l r) = PDPair fc (mapPT f l) (mapPT f r)
290 mpt (PHidden t) = PHidden (mapPT f t)
291 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
292 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
293 mpt x = x
296data PTactic' t = Intro [Name] | Focus Name
297 | Refine Name [Bool] | Rewrite t
298 | Exact t | Compute | Trivial
299 | Solve
300 | Attack
301 | ProofState | ProofTerm | Undo
302 | Qed
303 deriving (Show, Eq, Functor)
305type PTactic = PTactic' PTerm
307data PDo' t = DoExp FC t
308 | DoBind FC Name t
309 | DoLet FC Name t
310 deriving (Eq, Functor)
312type PDo = PDo' PTerm
314-- The priority gives a hint as to elaboration order. Best to elaborate
315-- things early which will help give a more concrete type to other
316-- variables, e.g. a before (interpTy a).
318data PArg' t = PImp { priority :: Int,
319 lazyarg :: Bool, pname :: Name, getTm :: t }
320 | PExp { priority :: Int,
321 lazyarg :: Bool, getTm :: t }
322 | PConstraint { priority :: Int,
323 lazyarg :: Bool, getTm :: t }
324 deriving (Show, Eq, Functor)
326pimp = PImp 0 False
327pexp = PExp 0 False
328pconst = PConstraint 0 False
330type PArg = PArg' PTerm
332-- Type class data
334data ClassInfo = CI { instanceName :: Name,
335 class_methods :: [(Name, PTerm)],
336 class_params :: [Name] }
339-- Syntactic sugar info (TODO: namespaces, modules)
341data DSL = DSL { dsl_bind :: Name,
342 dsl_return :: Name }
343 deriving Show
345data Syntax = Rule [SSymbol] PTerm
346 deriving Show
348data SSymbol = Keyword Name
349 | Symbol String
350 | Expr Name
351 deriving Show
353initDSL = DSL (UN [">>="]) (UN ["return"])
355data SyntaxInfo = Syn { using :: [(Name, PTerm)],
356 syn_params :: [(Name, PTerm)],
357 no_imp :: [Name],
358 decoration :: Name -> Name,
359 dsl_info :: DSL }
360 deriving Show
362defaultSyntax = Syn [] [] [] id initDSL
364--- Pretty printing declarations and terms
366instance Show PTerm where
367 show tm = showImp False tm
369instance Show PDecl where
370 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
371 show (PTy _ _ n ty) = show n ++ " : " ++ show ty
372 show (PClauses _ n c) = showSep "\n" (map show c)
373 show (PData _ _ d) = show d
375instance Show PClause where
376 show c = showCImp True c
378instance Show PData where
379 show d = showDImp False d
381showCImp :: Bool -> PClause -> String
382showCImp impl (PClause n l ws r w)
383 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
384 ++ " where " ++ show w
385 where
386 showWs [] = ""
387 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
388showCImp impl (PWith n l ws r w)
389 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
390 ++ " { " ++ show w ++ " } "
391 where
392 showWs [] = ""
393 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
396showDImp :: Bool -> PData -> String
397showDImp impl (PDatadecl n ty cons)
398 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
399 ++ showSep "\n\t| "
400 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
402getImps :: [PArg] -> [(Name, PTerm)]
403getImps [] = []
404getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
405getImps (_ : xs) = getImps xs
407getExps :: [PArg] -> [PTerm]
408getExps [] = []
409getExps (PExp _ _ tm : xs) = tm : getExps xs
410getExps (_ : xs) = getExps xs
412getConsts :: [PArg] -> [PTerm]
413getConsts [] = []
414getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
415getConsts (_ : xs) = getConsts xs
417getAll :: [PArg] -> [PTerm]
418getAll = map getTm
420showImp :: Bool -> PTerm -> String
421showImp impl tm = se 10 tm where
422 se p (PQuote r) = "![" ++ show r ++ "]"
423 se p (PRef _ n) = show n
424 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
425 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
426 " in " ++ se 10 sc
427 se p (PPi (Exp l s) n ty sc)
428 | n `elem` allNamesIn sc = bracket p 2 $
429 if l then "|(" else "(" ++
430 show n ++ " : " ++ se 10 ty ++
431 ") " ++ st ++
432 "-> " ++ se 10 sc
433 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
434 where st = case s of
435 Static -> "[static] "
436 _ -> ""
437 se p (PPi (Imp l s) n ty sc)
438 | impl = bracket p 2 $ if l then "|{" else "{" ++
439 show n ++ " : " ++ se 10 ty ++
440 "} " ++ st ++ "-> " ++ se 10 sc
441 | otherwise = se 10 sc
442 where st = case s of
443 Static -> "[static] "
444 _ -> ""
445 se p (PPi (Constraint _ _) n ty sc)
446 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
447 se p (PApp _ (PRef _ f) [])
448 | not impl = show f
449 se p (PApp _ (PRef _ op@(UN [f:_])) args)
450 | length (getExps args) == 2 && not impl && not (isAlpha f)
451 = let [l, r] = getExps args in
452 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
453 se p (PApp _ f as)
454 = let args = getExps as in
455 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
456 else concatMap seArg args
457 se p (PHidden tm) = "." ++ se 0 tm
458 se p (PRefl _) = "refl"
459 se p (PResolveTC _) = "resolvetc"
460 se p (PTrue _) = "()"
461 se p (PFalse _) = "_|_"
462 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
463 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
464 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
465 se p PSet = "Set"
466 se p (PConstant c) = show c
467 se p (PProof ts) = "proof { " ++ show ts ++ "}"
468 se p (PMetavar n) = "?" ++ show n
469 se p Placeholder = "_"
471 sArg (PImp _ _ n tm) = siArg (n, tm)
472 sArg (PExp _ _ tm) = seArg tm
473 sArg (PConstraint _ _ tm) = scArg tm
475 seArg arg = " " ++ se 0 arg
476 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
477 scArg val = " {{" ++ se 10 val ++ "}}"
479 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
480 | otherwise = str
482allNamesIn :: PTerm -> [Name]
483allNamesIn tm = nub $ ni [] tm
484 where
485 ni env (PRef _ n)
486 | not (n `elem` env) = [n]
487 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
488 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
489 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
490 ni env (PHidden tm) = ni env tm
491 ni env (PEq _ l r) = ni env l ++ ni env r
492 ni env (PPair _ l r) = ni env l ++ ni env r
493 ni env (PDPair _ l r) = ni env l ++ ni env r
494 ni env _ = []
496namesIn :: IState -> PTerm -> [Name]
497namesIn ist tm = nub $ ni [] tm
498 where
499 ni env (PRef _ n)
500 | not (n `elem` env)
501 = case lookupCtxt n (idris_implicits ist) of
502 Nothing -> [n]
503 _ -> []
504 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
505 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
506 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
507 ni env (PEq _ l r) = ni env l ++ ni env r
508 ni env (PPair _ l r) = ni env l ++ ni env r
509 ni env (PDPair _ l r) = ni env l ++ ni env r
510 ni env (PHidden tm) = ni env tm
511 ni env _ = []
513-- For inferring types of things
515bi = FC "builtin" 0
517inferTy = MN 0 "__Infer"
518inferCon = MN 0 "__infer"
519inferDecl = PDatadecl inferTy
520 PSet
521 [(inferCon, PPi impl (MN 0 "A") PSet (
522 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
523 (PRef bi inferTy)), bi)]
525infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
526infP = P (TCon 6 0) inferTy (Set 0)
528getInferTerm, getInferType :: Term -> Term
529getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
530getInferTerm (App (App _ _) tm) = tm
531getInferTerm tm = error ("getInferTerm " ++ show tm)
533getInferType (Bind n b sc) = Bind n b $ getInferType sc
534getInferType (App (App _ ty) _) = ty
536-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
538primNames = [unitTy, unitCon,
539 falseTy, pairTy, pairCon,
540 eqTy, eqCon, inferTy, inferCon]
542unitTy = MN 0 "__Unit"
543unitCon = MN 0 "__II"
544unitDecl = PDatadecl unitTy PSet
545 [(unitCon, PRef bi unitTy, bi)]
547falseTy = MN 0 "__False"
548falseDecl = PDatadecl falseTy PSet []
550pairTy = MN 0 "__Pair"
551pairCon = MN 0 "__MkPair"
552pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
553 [(pairCon, PPi impl (n "A") PSet (
554 PPi impl (n "B") PSet (
555 PPi expl (n "a") (PRef bi (n "A")) (
556 PPi expl (n "b") (PRef bi (n "B"))
557 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
558 pexp (PRef bi (n "B"))])))), bi)]
559 where n a = MN 0 a
561eqTy = UN ["="]
562eqCon = UN ["refl"]
563eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
564 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
565 PSet)
566 [(eqCon, PPi impl (n "a") PSet (
567 PPi impl (n "x") (PRef bi (n "a"))
568 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
569 pimp (n "b") Placeholder,
570 pexp (PRef bi (n "x")),
571 pexp (PRef bi (n "x"))])), bi)]
572 where n a = MN 0 a
574-- Defined in builtins.idr
575sigmaTy = UN ["Sigma"]
576existsCon = UN ["Exists"]
578piBind :: [(Name, PTerm)] -> PTerm -> PTerm
579piBind [] t = t
580piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
582-- Dealing with parameters
584expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
585expandParams dec ps ns tm = en tm
586 where
587 en (PLam n t s) = PLam n (en t) (en s)
588 en (PPi p n t s) = PPi p n (en t) (en s)
589 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)
590 en (PEq f l r) = PEq f (en l) (en r)
591 en (PPair f l r) = PPair f (en l) (en r)
592 en (PDPair f l r) = PDPair f (en l) (en r)
593 en (PHidden t) = PHidden (en t)
594 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
595 en (PProof ts) = PProof (map (fmap en) ts)
597 en (PQuote (Var n))
598 | n `elem` ns = PQuote (Var (dec n))
599 en (PApp fc (PRef fc' n) as)
600 | n `elem` ns = PApp fc (PRef fc' (dec n))
601 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
602 en (PRef fc n)
603 | n `elem` ns = PApp fc (PRef fc (dec n))
604 (map (pexp . (PRef fc)) (map fst ps))
605 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
606 en t = t
608expandParamsD :: IState ->
609 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
610expandParamsD ist dec ps ns (PTy syn fc n ty)
611 = if n `elem` ns
612 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
613 else PTy syn fc n (expandParams dec ps ns ty)
614expandParamsD ist dec ps ns (PClauses fc n cs)
615 = let n' = if n `elem` ns then dec n else n in
616 PClauses fc n' (map expandParamsC cs)
617 where
618 expandParamsC (PClause n lhs ws rhs ds)
619 = let ps' = updateps True (namesIn ist rhs) (zip ps [0..])
620 ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])
621 n' = if n `elem` ns then dec n else n in
622 PClause n' (expandParams dec ps'' ns lhs)
623 (map (expandParams dec ps'' ns) ws)
624 (expandParams dec ps'' ns rhs)
625 (map (expandParamsD ist dec ps'' ns) ds)
626 expandParamsC (PWith n lhs ws wval ds)
627 = let ps' = updateps True (namesIn ist wval) (zip ps [0..])
628 ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])
629 n' = if n `elem` ns then dec n else n in
630 PWith n' (expandParams dec ps'' ns lhs)
631 (map (expandParams dec ps'' ns) ws)
632 (expandParams dec ps'' ns wval)
633 (map (expandParamsD ist dec ps'' ns) ds)
634 updateps yn nm [] = []
635 updateps yn nm (((a, t), i):as)
636 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
637 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
639expandParamsD ist dec ps ns d = d
641-- Calculate a priority for a type, for deciding elaboration order
642-- * if it's just a type variable or concrete type, do it early (0)
643-- * if there's only type variables and injective constructors, do it next (1)
644-- * if there's a function type, next (2)
645-- * finally, everything else (3)
647getPriority :: IState -> PTerm -> Int
648getPriority i tm = pri tm
649 where
650 pri (PRef _ n) =
651 case lookupP n (tt_ctxt i) of
652 Just (P (DCon _ _) _ _) -> 1
653 Just (P (TCon _ _) _ _) -> 1
654 Just (P Ref _ _) -> 3
655 Nothing -> 0 -- must be locally bound, if it's not an error...
656 pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))
657 pri (PTrue _) = 0
658 pri (PFalse _) = 0
659 pri (PRefl _) = 1
660 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
661 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
662 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
663 pri (PDPair _ l r) = max 1 (max (pri l) (pri r))
664 pri (PConstant _) = 0
665 pri Placeholder = 1
666 pri _ = 3
668-- Dealing with implicit arguments
670-- Add implicit Pi bindings for any names in the term which appear in an
671-- argument position.
673-- This has become a right mess already. Better redo it some time...
675implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
676implicit syn n ptm
677 = do i <- get
678 let (tm', impdata) = implicitise syn i ptm
679 let (tm'', spos) = findStatics i tm'
680 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
681 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
682 i <- get
683 put (i { idris_statics = addDef n spos (idris_statics i) })
684 return tm''
686implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
687implicitise syn ist tm
688 = let uvars = using syn
689 pvars = syn_params syn
690 (declimps, ns') = execState (imps True [] tm) ([], [])
691 ns = ns' \\ (map fst pvars ++ no_imp syn) in
692 if null ns
693 then (tm, reverse declimps)
694 else implicitise syn ist (pibind uvars ns tm)
695 where
696 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
697 | otherwise = x : dropAll xs ys
698 dropAll [] ys = []
700 imps top env (PApp _ f as)
701 = do (decls, ns) <- get
702 let isn = concatMap (namesIn ist) (map getTm as)
703 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
704 imps top env (PPi (Imp l _) n ty sc)
705 = do let isn = nub (namesIn ist ty) `dropAll` [n]
706 (decls , ns) <- get
707 put (PImp (getPriority ist ty) l n ty : decls,
708 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
709 imps True (n:env) sc
710 imps top env (PPi (Exp l _) n ty sc)
711 = do let isn = nub (namesIn ist ty ++ case sc of
712 (PRef _ x) -> namesIn ist sc `dropAll` [n]
713 _ -> [])
714 (decls, ns) <- get -- ignore decls in HO types
715 put (PExp (getPriority ist ty) l ty : decls,
716 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
717 imps True (n:env) sc
718 imps top env (PPi (Constraint l _) n ty sc)
719 = do let isn = nub (namesIn ist ty ++ case sc of
720 (PRef _ x) -> namesIn ist sc `dropAll` [n]
721 _ -> [])
722 (decls, ns) <- get -- ignore decls in HO types
723 put (PConstraint 10 l ty : decls,
724 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
725 imps True (n:env) sc
726 imps top env (PEq _ l r)
727 = do (decls, ns) <- get
728 let isn = namesIn ist l ++ namesIn ist r
729 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
730 imps top env (PPair _ l r)
731 = do (decls, ns) <- get
732 let isn = namesIn ist l ++ namesIn ist r
733 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
734 imps top env (PDPair _ (PRef _ n) r)
735 = do (decls, ns) <- get
736 let isn = nub (namesIn ist r) \\ [n]
737 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
738 imps top env (PDPair _ l r)
739 = do (decls, ns) <- get
740 let isn = namesIn ist l ++ namesIn ist r
741 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
742 imps top env (PLam n ty sc)
743 = do imps False env ty
744 imps False (n:env) sc
745 imps top env (PHidden tm) = imps False env tm
746 imps top env _ = return ()
748 pibind using [] sc = sc
749 pibind using (n:ns) sc
750 = case lookup n using of
751 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
752 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
754-- Add implicit arguments in function calls
756addImpl :: IState -> PTerm -> PTerm
757addImpl ist ptm = ai [] ptm
758 where
759 ai env (PRef fc f) = aiFn ist fc f []
760 ai env (PEq fc l r) = let l' = ai env l
761 r' = ai env r in
762 PEq fc l' r'
763 ai env (PPair fc l r) = let l' = ai env l
764 r' = ai env r in
765 PPair fc l' r'
766 ai env (PDPair fc l r) = let l' = ai env l
767 r' = ai env r in
768 PDPair fc l' r'
769 ai env (PApp fc (PRef _ f) as)
770 = let as' = map (fmap (ai env)) as in
771 aiFn ist fc f as'
772 ai env (PApp fc f as) = let f' = ai env f
773 as' = map (fmap (ai env)) as in
774 mkPApp fc 1 f' as'
775 ai env (PLam n ty sc) = let ty' = ai env ty
776 sc' = ai (n:env) sc in
777 PLam n ty' sc'
778 ai env (PLet n ty val sc)
779 = let ty' = ai env ty
780 val' = ai env val
781 sc' = ai (n:env) sc in
782 PLet n ty' val' sc'
783 ai env (PPi p n ty sc) = let ty' = ai env ty
784 sc' = ai (n:env) sc in
785 PPi p n ty' sc'
786 ai env (PHidden tm) = PHidden (ai env tm)
787 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
788 ai env tm = tm
790aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
791aiFn ist fc f as
792 | f `elem` primNames = PApp fc (PRef fc f) as
793aiFn ist fc f as
794 = case lookupCtxt f (idris_implicits ist) of
795 Just ns -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)
796 Nothing -> mkPApp fc 1 (PRef fc f) as
797 where
798 insertImpl :: [PArg] -> [PArg] -> [PArg]
799 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
800 PExp p l tm : insertImpl ps given
801 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
802 PConstraint p l tm : insertImpl ps given
803 insertImpl (PConstraint p l ty : ps) given =
804 PConstraint p l (PResolveTC fc) : insertImpl ps given
805 insertImpl (PImp p l n ty : ps) given =
806 case find n given [] of
807 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
808 Nothing -> PImp p l n Placeholder : insertImpl ps given
809 insertImpl expected [] = []
810 insertImpl [] given = given
812 find n [] acc = Nothing
813 find n (PImp _ _ n' t : gs) acc
814 | n == n' = Just (t, reverse acc ++ gs)
815 find n (g : gs) acc = find n gs (g : acc)
817mkPApp fc a f [] = f
818mkPApp fc a f as = let rest = drop a as in
819 appRest fc (PApp fc f (take a as)) rest
820 where
821 appRest fc f [] = f
822 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
824-- Find 'static' argument positions
825-- (the declared ones, plus any names in argument position in the declared
826-- statics)
827-- FIXME: It's possible that this really has to happen after elaboration
829findStatics :: IState -> PTerm -> (PTerm, [Bool])
830findStatics ist tm = let (ns, ss) = fs tm in
831 runState (pos ns ss tm) []
832 where fs (PPi p n t sc)
833 | Static <- pstatic p
834 = let (ns, ss) = fs sc in
835 (namesIn ist t : ns, namesIn ist t ++ n : ss)
836 | otherwise = let (ns, ss) = fs sc in
837 (namesIn ist t : ns, ss)
838 fs _ = ([], [])
840 inOne n ns = length (filter id (map (elem n) ns)) == 1
842 pos ns ss (PPi p n t sc)
843 | n `inOne` ns && elem n ss
844 = do sc' <- pos ns ss sc
845 spos <- get
846 put (True : spos)
847 return (PPi (p { pstatic = Static }) n t sc')
848 | otherwise = do sc' <- pos ns ss sc
849 spos <- get
850 put (False : spos)
851 return (PPi p n t sc')
852 pos ns ss t = return t
854-- Debugging/logging stuff
856dumpDecls :: [PDecl] -> String
857dumpDecls [] = ""
858dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
860dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
861dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
862dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
863dumpDecl (PData _ _ d) = showDImp True d
864dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
865dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
866dumpDecl (PClass _ _ cs n ps ds)
867 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
868dumpDecl (PInstance _ _ cs n _ t ds)
869 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
870-- dumpDecl (PImport i) = "import " ++ i
872-- syntactic match of a against b, returning pair of variables in a
873-- and what they match. Returns 'Nothing' if not a match.
875matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
876matchClause x y = match x y where
877 matchArg x y = match (getTm x) (getTm y)
879 match (PApp _ f args) (PApp _ f' args')
880 | length args == length args'
881 = do mf <- match f f'
882 ms <- zipWithM matchArg args args'
883 return (mf ++ concat ms)
884 match (PRef _ n) (PRef _ n') | n == n' = return []
885 | otherwise = Nothing
886 match (PRef _ n) tm = return [(n, tm)]
887 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
888 mr <- match r r'
889 return (ml ++ mr)
890 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
891 mr <- match r r'
892 return (ml ++ mr)
893 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
894 mr <- match r r'
895 return (ml ++ mr)
896 match (PRefl _) (PRefl _) = return []
897 match (PResolveTC _) (PResolveTC _) = return []
898 match (PTrue _) (PTrue _) = return []
899 match (PFalse _) (PFalse _) = return []
900 match (PReturn _) (PReturn _) = return []
901 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
902 ms <- match s s'
903 return (mt ++ ms)
904 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
905 ms <- match s s'
906 return (mt ++ ms)
907 match (PHidden x) (PHidden y) = match x y
908 match a b | a == b = return []
909 | otherwise = Nothing
911substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
912substMatches [] t = t
913substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
915substMatch :: Name -> PTerm -> PTerm -> PTerm
916substMatch n tm t = sm t where
917 sm (PRef _ n') | n == n' = tm
918 sm (PLam x t sc) = PLam x (sm t) (sm sc)
919 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
920 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
921 sm (PEq f x y) = PEq f (sm x) (sm y)
922 sm (PPair f x y) = PPair f (sm x) (sm y)
923 sm (PDPair f x y) = PDPair f (sm x) (sm y)
924 sm (PHidden x) = PHidden (sm x)
925 sm x = x