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