git.iko.soy/Idris-dev
on 1c49219 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
958 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
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 r) = PDPair fc (mapPT f l) (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 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 r) = ni env l ++ 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 r) = ni env l ++ 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 r) = PDPair f (en l) (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 r) = max 1 (max (pri l) (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) r)
765 = do (decls, ns) <- get
766 let isn = nub (namesIn ist r) \\ [n]
767 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
768 imps top env (PDPair _ l r)
769 = do (decls, ns) <- get
770 let isn = namesIn ist l ++ 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 r) = let l' = ai env l
797 r' = ai env r in
798 PDPair fc l' r'
799 ai env (PApp fc (PRef _ f) as)
800 = let as' = map (fmap (ai env)) as in
801 aiFn ist fc f as'
802 ai env (PApp fc f as) = let f' = ai env f
803 as' = map (fmap (ai env)) as in
804 mkPApp fc 1 f' as'
805 ai env (PLam n ty sc) = let ty' = ai env ty
806 sc' = ai (n:env) sc in
807 PLam n ty' sc'
808 ai env (PLet n ty val sc)
809 = let ty' = ai env ty
810 val' = ai env val
811 sc' = ai (n:env) sc in
812 PLet n ty' val' sc'
813 ai env (PPi p n ty sc) = let ty' = ai env ty
814 sc' = ai (n:env) sc in
815 PPi p n ty' sc'
816 ai env (PHidden tm) = PHidden (ai env tm)
817 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
818 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
819 ai env tm = tm
821aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
822aiFn ist fc f as
823 | f `elem` primNames = PApp fc (PRef fc f) as
824aiFn ist fc f as
825 = case lookupCtxt f (idris_implicits ist) of
826 Just ns -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)
827 Nothing -> mkPApp fc 1 (PRef fc f) as
828 where
829 insertImpl :: [PArg] -> [PArg] -> [PArg]
830 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
831 PExp p l tm : insertImpl ps given
832 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
833 PConstraint p l tm : insertImpl ps given
834 insertImpl (PConstraint p l ty : ps) given =
835 PConstraint p l (PResolveTC fc) : insertImpl ps given
836 insertImpl (PImp p l n ty : ps) given =
837 case find n given [] of
838 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
839 Nothing -> PImp p l n Placeholder : insertImpl ps given
840 insertImpl expected [] = []
841 insertImpl [] given = given
843 find n [] acc = Nothing
844 find n (PImp _ _ n' t : gs) acc
845 | n == n' = Just (t, reverse acc ++ gs)
846 find n (g : gs) acc = find n gs (g : acc)
848mkPApp fc a f [] = f
849mkPApp fc a f as = let rest = drop a as in
850 appRest fc (PApp fc f (take a as)) rest
851 where
852 appRest fc f [] = f
853 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
855-- Find 'static' argument positions
856-- (the declared ones, plus any names in argument position in the declared
857-- statics)
858-- FIXME: It's possible that this really has to happen after elaboration
860findStatics :: IState -> PTerm -> (PTerm, [Bool])
861findStatics ist tm = let (ns, ss) = fs tm in
862 runState (pos ns ss tm) []
863 where fs (PPi p n t sc)
864 | Static <- pstatic p
865 = let (ns, ss) = fs sc in
866 (namesIn ist t : ns, namesIn ist t ++ n : ss)
867 | otherwise = let (ns, ss) = fs sc in
868 (namesIn ist t : ns, ss)
869 fs _ = ([], [])
871 inOne n ns = length (filter id (map (elem n) ns)) == 1
873 pos ns ss (PPi p n t sc)
874 | n `inOne` ns && elem n ss
875 = do sc' <- pos ns ss sc
876 spos <- get
877 put (True : spos)
878 return (PPi (p { pstatic = Static }) n t sc')
879 | otherwise = do sc' <- pos ns ss sc
880 spos <- get
881 put (False : spos)
882 return (PPi p n t sc')
883 pos ns ss t = return t
885-- Debugging/logging stuff
887dumpDecls :: [PDecl] -> String
888dumpDecls [] = ""
889dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
891dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
892dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
893dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
894dumpDecl (PData _ _ d) = showDImp True d
895dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
896dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
897dumpDecl (PClass _ _ cs n ps ds)
898 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
899dumpDecl (PInstance _ _ cs n _ t ds)
900 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
901dumpDecl _ = "..."
902-- dumpDecl (PImport i) = "import " ++ i
904-- syntactic match of a against b, returning pair of variables in a
905-- and what they match. Returns 'Nothing' if not a match.
907matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
908matchClause x y = match x y where
909 matchArg x y = match (getTm x) (getTm y)
911 match (PApp _ f args) (PApp _ f' args')
912 | length args == length args'
913 = do mf <- match f f'
914 ms <- zipWithM matchArg args args'
915 return (mf ++ concat ms)
916 match (PRef _ n) (PRef _ n') | n == n' = return []
917 | otherwise = Nothing
918 match (PRef _ n) tm = return [(n, tm)]
919 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
920 mr <- match r r'
921 return (ml ++ mr)
922 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
923 mr <- match r r'
924 return (ml ++ mr)
925 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
926 mr <- match r r'
927 return (ml ++ mr)
928 match (PRefl _) (PRefl _) = return []
929 match (PResolveTC _) (PResolveTC _) = return []
930 match (PTrue _) (PTrue _) = return []
931 match (PFalse _) (PFalse _) = return []
932 match (PReturn _) (PReturn _) = return []
933 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
934 ms <- match s s'
935 return (mt ++ ms)
936 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
937 ms <- match s s'
938 return (mt ++ ms)
939 match (PHidden x) (PHidden y) = match x y
940 match a b | a == b = return []
941 | otherwise = Nothing
943substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
944substMatches [] t = t
945substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
947substMatch :: Name -> PTerm -> PTerm -> PTerm
948substMatch n tm t = sm t where
949 sm (PRef _ n') | n == n' = tm
950 sm (PLam x t sc) = PLam x (sm t) (sm sc)
951 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
952 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
953 sm (PEq f x y) = PEq f (sm x) (sm y)
954 sm (PPair f x y) = PPair f (sm x) (sm y)
955 sm (PDPair f x y) = PDPair f (sm x) (sm y)
956 sm (PHidden x) = PHidden (sm x)
957 sm x = x