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