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