git.iko.soy/Idris-dev
on 92bf28e help sign in
Idris-dev/src/Idris/AbsSyntax.hs
920 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
131setTypeCase :: Bool -> Idris ()
132setTypeCase t = do i <- get
133 let opts = idris_options i
134 let opt' = opts { opt_typecase = t }
135 put (i { idris_options = opt' })
137-- Commands in the REPL
139data Command = Quit | Help | Eval PTerm | Reload | Edit
140 | Compile String
141 | Metavars | Prove Name
142 | TTShell
143 | LogLvl Int | Spec PTerm | HNF PTerm
144 | NOP
146-- Parsed declarations
148data Fixity = Infixl { prec :: Int }
149 | Infixr { prec :: Int }
150 | InfixN { prec :: Int }
151 | PrefixN { prec :: Int }
152 deriving Eq
154instance Show Fixity where
155 show (Infixl i) = "infixl " ++ show i
156 show (Infixr i) = "infixr " ++ show i
157 show (InfixN i) = "infix " ++ show i
158 show (PrefixN i) = "prefix " ++ show i
160data FixDecl = Fix Fixity String
161 deriving (Show, Eq)
163instance Ord FixDecl where
164 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
167data Static = Static | Dynamic
168 deriving (Show, Eq)
170-- Mark bindings with their explicitness, and laziness
171data Plicity = Imp { plazy :: Bool,
172 pstatic :: Static }
173 | Exp { plazy :: Bool,
174 pstatic :: Static }
175 | Constraint { plazy :: Bool,
176 pstatic :: Static }
177 deriving (Show, Eq)
179impl = Imp False Dynamic
180expl = Exp False Dynamic
181constraint = Constraint False Static
183data PDecl' t = PFix FC Fixity [String] -- fixity declaration
184 | PTy SyntaxInfo FC Name t -- type declaration
185 | PClauses FC Name [PClause' t] -- pattern clause
186 | PData SyntaxInfo FC (PData' t) -- data declaration
187 | PParams FC [(Name, t)] [PDecl' t] -- params block
188 | PClass SyntaxInfo FC
189 [t] -- constraints
190 Name
191 [(Name, t)] -- parameters
192 [PDecl' t] -- declarations
193 | PInstance SyntaxInfo FC [t] -- constraints
194 Name -- class
195 [t] -- parameters
196 t -- full instance type
197 [PDecl' t]
198 | PSyntax FC Syntax
199 deriving Functor
201data PClause' t = PClause Name t [t] t [PDecl' t]
202 | PWith Name t [t] t [PDecl' t]
203 deriving Functor
205data PData' t = PDatadecl { d_name :: Name,
206 d_tcon :: t,
207 d_cons :: [(Name, t, FC)] }
208 deriving Functor
210-- Handy to get a free function for applying PTerm -> PTerm functions
211-- across a program, by deriving Functor
213type PDecl = PDecl' PTerm
214type PData = PData' PTerm
215type PClause = PClause' PTerm
217-- get all the names declared in a decl
219declared :: PDecl -> [Name]
220declared (PFix _ _ _) = []
221declared (PTy _ _ n t) = [n]
222declared (PClauses _ n _) = [] -- not a declaration
223declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
224 where fstt (a, _, _) = a
225declared (PParams _ _ ds) = concatMap declared ds
226-- declared (PImport _) = []
228updateN :: [(Name, Name)] -> Name -> Name
229updateN ns n | Just n' <- lookup n ns = n'
230updateN _ n = n
232updateNs :: [(Name, Name)] -> PTerm -> PTerm
233updateNs [] t = t
234updateNs ns t = mapPT updateRef t
235 where updateRef (PRef fc f) = PRef fc (updateN ns f)
236 updateRef t = t
238-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
239-- updateDNs [] t = t
240-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
241-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
242-- where updateCNs ns (PClause n l ts r ds)
243-- = PClause (updateN ns n) (fmap (updateNs ns) l)
244-- (map (fmap (updateNs ns)) ts)
245-- (fmap (updateNs ns) r)
246-- (map (updateDNs ns) ds)
247-- updateDNs ns c = c
249-- High level language terms
251data PTerm = PQuote Raw
252 | PRef FC Name
253 | PLam Name PTerm PTerm
254 | PPi Plicity Name PTerm PTerm
255 | PLet Name PTerm PTerm PTerm
256 | PApp FC PTerm [PArg]
257 | PTrue FC
258 | PFalse FC
259 | PRefl FC
260 | PResolveTC FC
261 | PEq FC PTerm PTerm
262 | PPair FC PTerm PTerm
263 | PDPair FC PTerm PTerm
264 | PHidden PTerm -- irrelevant or hidden pattern
265 | PSet
266 | PConstant Const
267 | Placeholder
268 | PDoBlock [PDo]
269 | PReturn FC
270 | PMetavar Name
271 | PProof [PTactic]
272 | PElabError String -- error to report on elaboration
273 deriving Eq
275mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
276mapPT f t = f (mpt t) where
277 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
278 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
279 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
280 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
281 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
282 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
283 mpt (PDPair fc l r) = PDPair fc (mapPT f l) (mapPT f r)
284 mpt (PHidden t) = PHidden (mapPT f t)
285 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
286 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
287 mpt x = x
290data PTactic' t = Intro [Name] | Focus Name
291 | Refine Name [Bool] | Rewrite t
292 | Exact t | Compute | Trivial
293 | Solve
294 | Attack
295 | ProofState | ProofTerm | Undo
296 | Qed
297 deriving (Show, Eq, Functor)
299type PTactic = PTactic' PTerm
301data PDo' t = DoExp FC t
302 | DoBind FC Name t
303 | DoLet FC Name t
304 deriving (Eq, Functor)
306type PDo = PDo' PTerm
308-- The priority gives a hint as to elaboration order. Best to elaborate
309-- things early which will help give a more concrete type to other
310-- variables, e.g. a before (interpTy a).
312data PArg' t = PImp { priority :: Int,
313 lazyarg :: Bool, pname :: Name, getTm :: t }
314 | PExp { priority :: Int,
315 lazyarg :: Bool, getTm :: t }
316 | PConstraint { priority :: Int,
317 lazyarg :: Bool, getTm :: t }
318 deriving (Show, Eq, Functor)
320pimp = PImp 0 False
321pexp = PExp 0 False
322pconst = PConstraint 0 False
324type PArg = PArg' PTerm
326-- Type class data
328data ClassInfo = CI { instanceName :: Name,
329 class_methods :: [(Name, PTerm)],
330 class_params :: [Name] }
333-- Syntactic sugar info (TODO: namespaces, modules)
335data DSL = DSL { dsl_bind :: Name,
336 dsl_return :: Name }
337 deriving Show
339data Syntax = Rule [SSymbol] PTerm
340 deriving Show
342data SSymbol = Keyword Name
343 | Symbol String
344 | Expr Name
345 deriving Show
347initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
349data SyntaxInfo = Syn { using :: [(Name, PTerm)],
350 syn_params :: [(Name, PTerm)],
351 no_imp :: [Name],
352 decoration :: Name -> Name,
353 dsl_info :: DSL }
354 deriving Show
356defaultSyntax = Syn [] [] [] id initDSL
358--- Pretty printing declarations and terms
360instance Show PTerm where
361 show tm = showImp False tm
363instance Show PDecl where
364 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
365 show (PTy _ _ n ty) = show n ++ " : " ++ show ty
366 show (PClauses _ n c) = showSep "\n" (map show c)
367 show (PData _ _ d) = show d
369instance Show PClause where
370 show c = showCImp True c
372instance Show PData where
373 show d = showDImp False d
375showCImp :: Bool -> PClause -> String
376showCImp impl (PClause n l ws r w)
377 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
378 ++ " where " ++ show w
379 where
380 showWs [] = ""
381 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
382showCImp impl (PWith n l ws r w)
383 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
384 ++ " { " ++ show w ++ " } "
385 where
386 showWs [] = ""
387 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
390showDImp :: Bool -> PData -> String
391showDImp impl (PDatadecl n ty cons)
392 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
393 ++ showSep "\n\t| "
394 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
396getImps :: [PArg] -> [(Name, PTerm)]
397getImps [] = []
398getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
399getImps (_ : xs) = getImps xs
401getExps :: [PArg] -> [PTerm]
402getExps [] = []
403getExps (PExp _ _ tm : xs) = tm : getExps xs
404getExps (_ : xs) = getExps xs
406getConsts :: [PArg] -> [PTerm]
407getConsts [] = []
408getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
409getConsts (_ : xs) = getConsts xs
411getAll :: [PArg] -> [PTerm]
412getAll = map getTm
414showImp :: Bool -> PTerm -> String
415showImp impl tm = se 10 tm where
416 se p (PQuote r) = "![" ++ show r ++ "]"
417 se p (PRef _ n) = show n
418 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
419 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
420 " in " ++ se 10 sc
421 se p (PPi (Exp l s) n ty sc)
422 | n `elem` allNamesIn sc = bracket p 2 $
423 if l then "|(" else "(" ++
424 show n ++ " : " ++ se 10 ty ++
425 ") " ++ st ++
426 "-> " ++ se 10 sc
427 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
428 where st = case s of
429 Static -> "[static] "
430 _ -> ""
431 se p (PPi (Imp l s) n ty sc)
432 | impl = bracket p 2 $ if l then "|{" else "{" ++
433 show n ++ " : " ++ se 10 ty ++
434 "} " ++ st ++ "-> " ++ se 10 sc
435 | otherwise = se 10 sc
436 where st = case s of
437 Static -> "[static] "
438 _ -> ""
439 se p (PPi (Constraint _ _) n ty sc)
440 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
441 se p (PApp _ (PRef _ f) [])
442 | not impl = show f
443 se p (PApp _ (PRef _ op@(UN [f:_])) args)
444 | length (getExps args) == 2 && not impl && not (isAlpha f)
445 = let [l, r] = getExps args in
446 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
447 se p (PApp _ f as)
448 = let args = getExps as in
449 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
450 else concatMap seArg args
451 se p (PHidden tm) = "." ++ se 0 tm
452 se p (PRefl _) = "refl"
453 se p (PResolveTC _) = "resolvetc"
454 se p (PTrue _) = "()"
455 se p (PFalse _) = "_|_"
456 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
457 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
458 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
459 se p PSet = "Set"
460 se p (PConstant c) = show c
461 se p (PProof ts) = "proof { " ++ show ts ++ "}"
462 se p (PMetavar n) = "?" ++ show n
463 se p Placeholder = "_"
465 sArg (PImp _ _ n tm) = siArg (n, tm)
466 sArg (PExp _ _ tm) = seArg tm
467 sArg (PConstraint _ _ tm) = scArg tm
469 seArg arg = " " ++ se 0 arg
470 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
471 scArg val = " {{" ++ se 10 val ++ "}}"
473 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
474 | otherwise = str
476allNamesIn :: PTerm -> [Name]
477allNamesIn tm = nub $ ni [] tm
478 where
479 ni env (PRef _ n)
480 | not (n `elem` env) = [n]
481 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
482 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
483 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
484 ni env (PHidden tm) = ni env tm
485 ni env (PEq _ l r) = ni env l ++ ni env r
486 ni env (PPair _ l r) = ni env l ++ ni env r
487 ni env (PDPair _ l r) = ni env l ++ ni env r
488 ni env _ = []
490namesIn :: IState -> PTerm -> [Name]
491namesIn ist tm = nub $ ni [] tm
492 where
493 ni env (PRef _ n)
494 | not (n `elem` env)
495 = case lookupCtxt n (idris_implicits ist) of
496 Nothing -> [n]
497 _ -> []
498 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
499 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
500 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
501 ni env (PEq _ l r) = ni env l ++ ni env r
502 ni env (PPair _ l r) = ni env l ++ ni env r
503 ni env (PDPair _ l r) = ni env l ++ ni env r
504 ni env (PHidden tm) = ni env tm
505 ni env _ = []
507-- For inferring types of things
509bi = FC "builtin" 0
511inferTy = MN 0 "__Infer"
512inferCon = MN 0 "__infer"
513inferDecl = PDatadecl inferTy
514 PSet
515 [(inferCon, PPi impl (MN 0 "A") PSet (
516 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
517 (PRef bi inferTy)), bi)]
519infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
520infP = P (TCon 6 0) inferTy (Set 0)
522getInferTerm, getInferType :: Term -> Term
523getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
524getInferTerm (App (App _ _) tm) = tm
525getInferTerm tm = error ("getInferTerm " ++ show tm)
527getInferType (Bind n b sc) = Bind n b $ getInferType sc
528getInferType (App (App _ ty) _) = ty
530-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
532primNames = [unitTy, unitCon,
533 falseTy, pairTy, pairCon,
534 eqTy, eqCon, inferTy, inferCon]
536unitTy = MN 0 "__Unit"
537unitCon = MN 0 "__II"
538unitDecl = PDatadecl unitTy PSet
539 [(unitCon, PRef bi unitTy, bi)]
541falseTy = MN 0 "__False"
542falseDecl = PDatadecl falseTy PSet []
544pairTy = MN 0 "__Pair"
545pairCon = MN 0 "__MkPair"
546pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
547 [(pairCon, PPi impl (n "A") PSet (
548 PPi impl (n "B") PSet (
549 PPi expl (n "a") (PRef bi (n "A")) (
550 PPi expl (n "b") (PRef bi (n "B"))
551 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
552 pexp (PRef bi (n "B"))])))), bi)]
553 where n a = MN 0 a
555eqTy = UN ["="]
556eqCon = UN ["refl"]
557eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
558 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
559 PSet)
560 [(eqCon, PPi impl (n "a") PSet (
561 PPi impl (n "x") (PRef bi (n "a"))
562 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
563 pimp (n "b") Placeholder,
564 pexp (PRef bi (n "x")),
565 pexp (PRef bi (n "x"))])), bi)]
566 where n a = MN 0 a
568-- Defined in builtins.idr
569sigmaTy = UN ["Sigma"]
570existsCon = UN ["Exists"]
572piBind :: [(Name, PTerm)] -> PTerm -> PTerm
573piBind [] t = t
574piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
576-- Dealing with parameters
578expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
579expandParams dec ps ns tm = en tm
580 where
581 en (PLam n t s) = PLam n (en t) (en s)
582 en (PPi p n t s) = PPi p n (en t) (en s)
583 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)
584 en (PEq f l r) = PEq f (en l) (en r)
585 en (PPair f l r) = PPair f (en l) (en r)
586 en (PDPair f l r) = PDPair f (en l) (en r)
587 en (PHidden t) = PHidden (en t)
588 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
589 en (PProof ts) = PProof (map (fmap en) ts)
591 en (PQuote (Var n))
592 | n `elem` ns = PQuote (Var (dec n))
593 en (PApp fc (PRef fc' n) as)
594 | n `elem` ns = PApp fc (PRef fc' (dec n))
595 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
596 en (PRef fc n)
597 | n `elem` ns = PApp fc (PRef fc (dec n))
598 (map (pexp . (PRef fc)) (map fst ps))
599 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
600 en t = t
602expandParamsD :: IState ->
603 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
604expandParamsD ist dec ps ns (PTy syn fc n ty)
605 = if n `elem` ns
606 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
607 else PTy syn fc n (expandParams dec ps ns ty)
608expandParamsD ist dec ps ns (PClauses fc n cs)
609 = let n' = if n `elem` ns then dec n else n in
610 PClauses fc n' (map expandParamsC cs)
611 where
612 expandParamsC (PClause n lhs ws rhs ds)
613 = let ps' = updateps True (namesIn ist rhs) (zip ps [0..])
614 ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])
615 n' = if n `elem` ns then dec n else n in
616 PClause n' (expandParams dec ps'' ns lhs)
617 (map (expandParams dec ps'' ns) ws)
618 (expandParams dec ps'' ns rhs)
619 (map (expandParamsD ist dec ps'' ns) ds)
620 expandParamsC (PWith n lhs ws wval ds)
621 = let ps' = updateps True (namesIn ist wval) (zip ps [0..])
622 ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])
623 n' = if n `elem` ns then dec n else n in
624 PWith n' (expandParams dec ps'' ns lhs)
625 (map (expandParams dec ps'' ns) ws)
626 (expandParams dec ps'' ns wval)
627 (map (expandParamsD ist dec ps'' ns) ds)
628 updateps yn nm [] = []
629 updateps yn nm (((a, t), i):as)
630 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
631 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
633expandParamsD ist dec ps ns d = d
635-- Calculate a priority for a type, for deciding elaboration order
636-- * if it's just a type variable or concrete type, do it early (0)
637-- * if there's only type variables and injective constructors, do it next (1)
638-- * if there's a function type, next (2)
639-- * finally, everything else (3)
641getPriority :: IState -> PTerm -> Int
642getPriority i tm = pri tm
643 where
644 pri (PRef _ n) =
645 case lookupP n (tt_ctxt i) of
646 Just (P (DCon _ _) _ _) -> 1
647 Just (P (TCon _ _) _ _) -> 1
648 Just (P Ref _ _) -> 3
649 Nothing -> 0 -- must be locally bound, if it's not an error...
650 pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))
651 pri (PTrue _) = 0
652 pri (PFalse _) = 0
653 pri (PRefl _) = 1
654 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
655 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
656 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
657 pri (PDPair _ l r) = max 1 (max (pri l) (pri r))
658 pri (PConstant _) = 0
659 pri Placeholder = 1
660 pri _ = 3
662-- Dealing with implicit arguments
664-- Add implicit Pi bindings for any names in the term which appear in an
665-- argument position.
667-- This has become a right mess already. Better redo it some time...
669implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
670implicit syn n ptm
671 = do i <- get
672 let (tm', impdata) = implicitise syn i ptm
673 let (tm'', spos) = findStatics i tm'
674 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
675 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
676 i <- get
677 put (i { idris_statics = addDef n spos (idris_statics i) })
678 return tm''
680implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
681implicitise syn ist tm
682 = let uvars = using syn
683 pvars = syn_params syn
684 (declimps, ns') = execState (imps True [] tm) ([], [])
685 ns = ns' \\ (map fst pvars ++ no_imp syn) in
686 if null ns
687 then (tm, reverse declimps)
688 else implicitise syn ist (pibind uvars ns tm)
689 where
690 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
691 | otherwise = x : dropAll xs ys
692 dropAll [] ys = []
694 imps top env (PApp _ f as)
695 = do (decls, ns) <- get
696 let isn = concatMap (namesIn ist) (map getTm as)
697 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
698 imps top env (PPi (Imp l _) n ty sc)
699 = do let isn = nub (namesIn ist ty) `dropAll` [n]
700 (decls , ns) <- get
701 put (PImp (getPriority ist ty) l n ty : decls,
702 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
703 imps True (n:env) sc
704 imps top env (PPi (Exp l _) n ty sc)
705 = do let isn = nub (namesIn ist ty ++ case sc of
706 (PRef _ x) -> namesIn ist sc `dropAll` [n]
707 _ -> [])
708 (decls, ns) <- get -- ignore decls in HO types
709 put (PExp (getPriority ist ty) l ty : decls,
710 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
711 imps True (n:env) sc
712 imps top env (PPi (Constraint l _) n ty sc)
713 = do let isn = nub (namesIn ist ty ++ case sc of
714 (PRef _ x) -> namesIn ist sc `dropAll` [n]
715 _ -> [])
716 (decls, ns) <- get -- ignore decls in HO types
717 put (PConstraint 10 l ty : decls,
718 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
719 imps True (n:env) sc
720 imps top env (PEq _ l r)
721 = do (decls, ns) <- get
722 let isn = namesIn ist l ++ namesIn ist r
723 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
724 imps top env (PPair _ l r)
725 = do (decls, ns) <- get
726 let isn = namesIn ist l ++ namesIn ist r
727 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
728 imps top env (PDPair _ (PRef _ n) r)
729 = do (decls, ns) <- get
730 let isn = nub (namesIn ist r) \\ [n]
731 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
732 imps top env (PDPair _ l r)
733 = do (decls, ns) <- get
734 let isn = namesIn ist l ++ namesIn ist r
735 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
736 imps top env (PLam n ty sc)
737 = do imps False env ty
738 imps False (n:env) sc
739 imps top env (PHidden tm) = imps False env tm
740 imps top env _ = return ()
742 pibind using [] sc = sc
743 pibind using (n:ns) sc
744 = case lookup n using of
745 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
746 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
748-- Add implicit arguments in function calls
750addImpl :: IState -> PTerm -> PTerm
751addImpl ist ptm = ai [] ptm
752 where
753 ai env (PRef fc f) = aiFn ist fc f []
754 ai env (PEq fc l r) = let l' = ai env l
755 r' = ai env r in
756 PEq fc l' r'
757 ai env (PPair fc l r) = let l' = ai env l
758 r' = ai env r in
759 PPair fc l' r'
760 ai env (PDPair fc l r) = let l' = ai env l
761 r' = ai env r in
762 PDPair fc l' r'
763 ai env (PApp fc (PRef _ f) as)
764 = let as' = map (fmap (ai env)) as in
765 aiFn ist fc f as'
766 ai env (PApp fc f as) = let f' = ai env f
767 as' = map (fmap (ai env)) as in
768 mkPApp fc 1 f' as'
769 ai env (PLam n ty sc) = let ty' = ai env ty
770 sc' = ai (n:env) sc in
771 PLam n ty' sc'
772 ai env (PLet n ty val sc)
773 = let ty' = ai env ty
774 val' = ai env val
775 sc' = ai (n:env) sc in
776 PLet n ty' val' sc'
777 ai env (PPi p n ty sc) = let ty' = ai env ty
778 sc' = ai (n:env) sc in
779 PPi p n ty' sc'
780 ai env (PHidden tm) = PHidden (ai env tm)
781 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
782 ai env tm = tm
784aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
785aiFn ist fc f as
786 | f `elem` primNames = PApp fc (PRef fc f) as
787aiFn ist fc f as
788 = case lookupCtxt f (idris_implicits ist) of
789 Just ns -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)
790 Nothing -> mkPApp fc 1 (PRef fc f) as
791 where
792 insertImpl :: [PArg] -> [PArg] -> [PArg]
793 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
794 PExp p l tm : insertImpl ps given
795 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
796 PConstraint p l tm : insertImpl ps given
797 insertImpl (PConstraint p l ty : ps) given =
798 PConstraint p l (PResolveTC fc) : insertImpl ps given
799 insertImpl (PImp p l n ty : ps) given =
800 case find n given [] of
801 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
802 Nothing -> PImp p l n Placeholder : insertImpl ps given
803 insertImpl expected [] = []
804 insertImpl [] given = given
806 find n [] acc = Nothing
807 find n (PImp _ _ n' t : gs) acc
808 | n == n' = Just (t, reverse acc ++ gs)
809 find n (g : gs) acc = find n gs (g : acc)
811mkPApp fc a f [] = f
812mkPApp fc a f as = let rest = drop a as in
813 appRest fc (PApp fc f (take a as)) rest
814 where
815 appRest fc f [] = f
816 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
818-- Find 'static' argument positions
819-- (the declared ones, plus any names in argument position in the declared
820-- statics)
821-- FIXME: It's possible that this really has to happen after elaboration
823findStatics :: IState -> PTerm -> (PTerm, [Bool])
824findStatics ist tm = let (ns, ss) = fs tm in
825 runState (pos ns ss tm) []
826 where fs (PPi p n t sc)
827 | Static <- pstatic p
828 = let (ns, ss) = fs sc in
829 (namesIn ist t : ns, namesIn ist t ++ n : ss)
830 | otherwise = let (ns, ss) = fs sc in
831 (namesIn ist t : ns, ss)
832 fs _ = ([], [])
834 inOne n ns = length (filter id (map (elem n) ns)) == 1
836 pos ns ss (PPi p n t sc)
837 | n `inOne` ns && elem n ss
838 = do sc' <- pos ns ss sc
839 spos <- get
840 put (True : spos)
841 return (PPi (p { pstatic = Static }) n t sc')
842 | otherwise = do sc' <- pos ns ss sc
843 spos <- get
844 put (False : spos)
845 return (PPi p n t sc')
846 pos ns ss t = return t
848-- Debugging/logging stuff
850dumpDecls :: [PDecl] -> String
851dumpDecls [] = ""
852dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
854dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
855dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
856dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
857dumpDecl (PData _ _ d) = showDImp True d
858dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
859dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
860dumpDecl (PClass _ _ cs n ps ds)
861 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
862dumpDecl (PInstance _ _ cs n _ t ds)
863 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
864-- dumpDecl (PImport i) = "import " ++ i
866-- syntactic match of a against b, returning pair of variables in a
867-- and what they match. Returns 'Nothing' if not a match.
869matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
870matchClause x y = match x y where
871 matchArg x y = match (getTm x) (getTm y)
873 match (PApp _ f args) (PApp _ f' args')
874 | length args == length args'
875 = do mf <- match f f'
876 ms <- zipWithM matchArg args args'
877 return (mf ++ concat ms)
878 match (PRef _ n) (PRef _ n') | n == n' = return []
879 | otherwise = Nothing
880 match (PRef _ n) tm = return [(n, tm)]
881 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
882 mr <- match r r'
883 return (ml ++ mr)
884 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
885 mr <- match r r'
886 return (ml ++ mr)
887 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
888 mr <- match r r'
889 return (ml ++ mr)
890 match (PRefl _) (PRefl _) = return []
891 match (PResolveTC _) (PResolveTC _) = return []
892 match (PTrue _) (PTrue _) = return []
893 match (PFalse _) (PFalse _) = return []
894 match (PReturn _) (PReturn _) = return []
895 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
896 ms <- match s s'
897 return (mt ++ ms)
898 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
899 ms <- match s s'
900 return (mt ++ ms)
901 match (PHidden x) (PHidden y) = match x y
902 match a b | a == b = return []
903 | otherwise = Nothing
905substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
906substMatches [] t = t
907substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
909substMatch :: Name -> PTerm -> PTerm -> PTerm
910substMatch n tm t = sm t where
911 sm (PRef _ n') | n == n' = tm
912 sm (PLam x t sc) = PLam x (sm t) (sm sc)
913 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
914 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
915 sm (PEq f x y) = PEq f (sm x) (sm y)
916 sm (PPair f x y) = PPair f (sm x) (sm y)
917 sm (PDPair f x y) = PDPair f (sm x) (sm y)
918 sm (PHidden x) = PHidden (sm x)
919 sm x = x