git.iko.soy/Idris-dev
on 74183cb help sign in
Idris-dev/src/Idris/AbsSyntax.hs
946 lines 35 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate
9import Core.Typecheck
11import Control.Monad.State
12import Data.List
13import Data.Char
14import Debug.Trace
16import qualified Epic.Epic as E
18data IOption = IOption { opt_logLevel :: Int,
19 opt_typecase :: Bool
20 }
21 deriving (Show, Eq)
23defaultOpts = IOption 0 False
25-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
26-- without typechecking).
27-- This will include all the functions and data declarations, plus fixity declarations
28-- and syntax macros.
30data IState = IState { tt_ctxt :: Context,
31 idris_infixes :: [FixDecl],
32 idris_implicits :: Ctxt [PArg],
33 idris_statics :: Ctxt [Bool],
34 idris_classes :: Ctxt ClassInfo,
35 idris_log :: String,
36 idris_options :: IOption,
37 idris_name :: Int,
38 idris_metavars :: [Name],
39 syntax_rules :: [Syntax],
40 syntax_keywords :: [String],
41 imported :: [FilePath],
42 idris_prims :: [(Name, ([E.Name], E.Term))],
43 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 | PElabError String -- error to report on elaboration
299 deriving Eq
301mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
302mapPT f t = f (mpt t) where
303 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
304 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
305 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
306 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
307 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
308 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
309 mpt (PDPair fc l r) = PDPair fc (mapPT f l) (mapPT f r)
310 mpt (PHidden t) = PHidden (mapPT f t)
311 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
312 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
313 mpt x = x
316data PTactic' t = Intro [Name] | Focus Name
317 | Refine Name [Bool] | Rewrite t
318 | Exact t | Compute | Trivial
319 | Solve
320 | Attack
321 | ProofState | ProofTerm | Undo
322 | Qed
323 deriving (Show, Eq, Functor)
325type PTactic = PTactic' PTerm
327data PDo' t = DoExp FC t
328 | DoBind FC Name t
329 | DoLet FC Name t
330 deriving (Eq, Functor)
332type PDo = PDo' PTerm
334-- The priority gives a hint as to elaboration order. Best to elaborate
335-- things early which will help give a more concrete type to other
336-- variables, e.g. a before (interpTy a).
338data PArg' t = PImp { priority :: Int,
339 lazyarg :: Bool, pname :: Name, getTm :: t }
340 | PExp { priority :: Int,
341 lazyarg :: Bool, getTm :: t }
342 | PConstraint { priority :: Int,
343 lazyarg :: Bool, getTm :: t }
344 deriving (Show, Eq, Functor)
346pimp = PImp 0 False
347pexp = PExp 0 False
348pconst = PConstraint 0 False
350type PArg = PArg' PTerm
352-- Type class data
354data ClassInfo = CI { instanceName :: Name,
355 class_methods :: [(Name, PTerm)],
356 class_params :: [Name] }
359-- Syntactic sugar info (TODO: namespaces, modules)
361data DSL = DSL { dsl_bind :: Name,
362 dsl_return :: Name }
363 deriving Show
365data Syntax = Rule [SSymbol] PTerm
366 deriving Show
368data SSymbol = Keyword Name
369 | Symbol String
370 | Expr Name
371 deriving Show
373initDSL = DSL (UN [">>="]) (UN ["return"])
375data SyntaxInfo = Syn { using :: [(Name, PTerm)],
376 syn_params :: [(Name, PTerm)],
377 no_imp :: [Name],
378 decoration :: Name -> Name,
379 dsl_info :: DSL }
380 deriving Show
382defaultSyntax = Syn [] [] [] id initDSL
384--- Pretty printing declarations and terms
386instance Show PTerm where
387 show tm = showImp False tm
389instance Show PDecl where
390 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
391 show (PTy _ _ n ty) = show n ++ " : " ++ show ty
392 show (PClauses _ _ n c) = showSep "\n" (map show c)
393 show (PData _ _ d) = show d
395instance Show PClause where
396 show c = showCImp True c
398instance Show PData where
399 show d = showDImp False d
401showCImp :: Bool -> PClause -> String
402showCImp impl (PClause n l ws r w)
403 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
404 ++ " where " ++ show w
405 where
406 showWs [] = ""
407 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
408showCImp impl (PWith n l ws r w)
409 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
410 ++ " { " ++ show w ++ " } "
411 where
412 showWs [] = ""
413 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
416showDImp :: Bool -> PData -> String
417showDImp impl (PDatadecl n ty cons)
418 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
419 ++ showSep "\n\t| "
420 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
422getImps :: [PArg] -> [(Name, PTerm)]
423getImps [] = []
424getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
425getImps (_ : xs) = getImps xs
427getExps :: [PArg] -> [PTerm]
428getExps [] = []
429getExps (PExp _ _ tm : xs) = tm : getExps xs
430getExps (_ : xs) = getExps xs
432getConsts :: [PArg] -> [PTerm]
433getConsts [] = []
434getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
435getConsts (_ : xs) = getConsts xs
437getAll :: [PArg] -> [PTerm]
438getAll = map getTm
440showImp :: Bool -> PTerm -> String
441showImp impl tm = se 10 tm where
442 se p (PQuote r) = "![" ++ show r ++ "]"
443 se p (PRef _ n) = show n
444 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
445 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
446 " in " ++ se 10 sc
447 se p (PPi (Exp l s) n ty sc)
448 | n `elem` allNamesIn sc = bracket p 2 $
449 if l then "|(" else "(" ++
450 show n ++ " : " ++ se 10 ty ++
451 ") " ++ st ++
452 "-> " ++ se 10 sc
453 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
454 where st = case s of
455 Static -> "[static] "
456 _ -> ""
457 se p (PPi (Imp l s) n ty sc)
458 | impl = bracket p 2 $ if l then "|{" else "{" ++
459 show n ++ " : " ++ se 10 ty ++
460 "} " ++ st ++ "-> " ++ se 10 sc
461 | otherwise = se 10 sc
462 where st = case s of
463 Static -> "[static] "
464 _ -> ""
465 se p (PPi (Constraint _ _) n ty sc)
466 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
467 se p (PApp _ (PRef _ f) [])
468 | not impl = show f
469 se p (PApp _ (PRef _ op@(UN [f:_])) args)
470 | length (getExps args) == 2 && not impl && not (isAlpha f)
471 = let [l, r] = getExps args in
472 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
473 se p (PApp _ f as)
474 = let args = getExps as in
475 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
476 else concatMap seArg args
477 se p (PHidden tm) = "." ++ se 0 tm
478 se p (PRefl _) = "refl"
479 se p (PResolveTC _) = "resolvetc"
480 se p (PTrue _) = "()"
481 se p (PFalse _) = "_|_"
482 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
483 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
484 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
485 se p PSet = "Set"
486 se p (PConstant c) = show c
487 se p (PProof ts) = "proof { " ++ show ts ++ "}"
488 se p (PMetavar n) = "?" ++ show n
489 se p Placeholder = "_"
491 sArg (PImp _ _ n tm) = siArg (n, tm)
492 sArg (PExp _ _ tm) = seArg tm
493 sArg (PConstraint _ _ tm) = scArg tm
495 seArg arg = " " ++ se 0 arg
496 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
497 scArg val = " {{" ++ se 10 val ++ "}}"
499 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
500 | otherwise = str
502allNamesIn :: PTerm -> [Name]
503allNamesIn tm = nub $ ni [] tm
504 where
505 ni env (PRef _ n)
506 | not (n `elem` env) = [n]
507 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
508 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
509 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
510 ni env (PHidden tm) = ni env tm
511 ni env (PEq _ l r) = ni env l ++ ni env r
512 ni env (PPair _ l r) = ni env l ++ ni env r
513 ni env (PDPair _ l r) = ni env l ++ ni env r
514 ni env _ = []
516namesIn :: IState -> PTerm -> [Name]
517namesIn ist tm = nub $ ni [] tm
518 where
519 ni env (PRef _ n)
520 | not (n `elem` env)
521 = case lookupCtxt n (idris_implicits ist) of
522 Nothing -> [n]
523 _ -> []
524 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
525 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
526 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
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 _ l r) = ni env l ++ ni env r
530 ni env (PHidden tm) = ni env tm
531 ni env _ = []
533-- For inferring types of things
535bi = FC "builtin" 0
537inferTy = MN 0 "__Infer"
538inferCon = MN 0 "__infer"
539inferDecl = PDatadecl inferTy
540 PSet
541 [(inferCon, PPi impl (MN 0 "A") PSet (
542 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
543 (PRef bi inferTy)), bi)]
545infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
546infP = P (TCon 6 0) inferTy (Set 0)
548getInferTerm, getInferType :: Term -> Term
549getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
550getInferTerm (App (App _ _) tm) = tm
551getInferTerm tm = error ("getInferTerm " ++ show tm)
553getInferType (Bind n b sc) = Bind n b $ getInferType sc
554getInferType (App (App _ ty) _) = ty
556-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
558primNames = [unitTy, unitCon,
559 falseTy, pairTy, pairCon,
560 eqTy, eqCon, inferTy, inferCon]
562unitTy = MN 0 "__Unit"
563unitCon = MN 0 "__II"
564unitDecl = PDatadecl unitTy PSet
565 [(unitCon, PRef bi unitTy, bi)]
567falseTy = MN 0 "__False"
568falseDecl = PDatadecl falseTy PSet []
570pairTy = MN 0 "__Pair"
571pairCon = MN 0 "__MkPair"
572pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
573 [(pairCon, PPi impl (n "A") PSet (
574 PPi impl (n "B") PSet (
575 PPi expl (n "a") (PRef bi (n "A")) (
576 PPi expl (n "b") (PRef bi (n "B"))
577 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
578 pexp (PRef bi (n "B"))])))), bi)]
579 where n a = MN 0 a
581eqTy = UN ["="]
582eqCon = UN ["refl"]
583eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
584 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
585 PSet)
586 [(eqCon, PPi impl (n "a") PSet (
587 PPi impl (n "x") (PRef bi (n "a"))
588 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
589 pimp (n "b") Placeholder,
590 pexp (PRef bi (n "x")),
591 pexp (PRef bi (n "x"))])), bi)]
592 where n a = MN 0 a
594-- Defined in builtins.idr
595sigmaTy = UN ["Sigma"]
596existsCon = UN ["Exists"]
598piBind :: [(Name, PTerm)] -> PTerm -> PTerm
599piBind [] t = t
600piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
602-- Dealing with parameters
604expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
605expandParams dec ps ns tm = en tm
606 where
607 en (PLam n t s) = PLam n (en t) (en s)
608 en (PPi p n t s) = PPi p n (en t) (en s)
609 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)
610 en (PEq f l r) = PEq f (en l) (en r)
611 en (PPair f l r) = PPair f (en l) (en r)
612 en (PDPair f l r) = PDPair f (en l) (en r)
613 en (PHidden t) = PHidden (en t)
614 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
615 en (PProof ts) = PProof (map (fmap en) ts)
617 en (PQuote (Var n))
618 | n `elem` ns = PQuote (Var (dec n))
619 en (PApp fc (PRef fc' n) as)
620 | n `elem` ns = PApp fc (PRef fc' (dec n))
621 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
622 en (PRef fc n)
623 | n `elem` ns = PApp fc (PRef fc (dec n))
624 (map (pexp . (PRef fc)) (map fst ps))
625 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
626 en t = t
628expandParamsD :: IState ->
629 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
630expandParamsD ist dec ps ns (PTy syn fc n ty)
631 = if n `elem` ns
632 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
633 else PTy syn fc n (expandParams dec ps ns ty)
634expandParamsD ist dec ps ns (PClauses fc opts n cs)
635 = let n' = if n `elem` ns then dec n else n in
636 PClauses fc opts n' (map expandParamsC cs)
637 where
638 expandParamsC (PClause n lhs ws rhs ds)
639 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
640 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
641 n' = if n `elem` ns then dec n else n in
642 PClause n' (expandParams dec ps'' ns lhs)
643 (map (expandParams dec ps'' ns) ws)
644 (expandParams dec ps'' ns rhs)
645 (map (expandParamsD ist dec ps'' ns) ds)
646 expandParamsC (PWith n lhs ws wval ds)
647 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
648 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
649 n' = if n `elem` ns then dec n else n in
650 PWith n' (expandParams dec ps'' ns lhs)
651 (map (expandParams dec ps'' ns) ws)
652 (expandParams dec ps'' ns wval)
653 (map (expandParamsD ist dec ps'' ns) ds)
654 updateps yn nm [] = []
655 updateps yn nm (((a, t), i):as)
656 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
657 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
659expandParamsD ist dec ps ns d = d
661-- Calculate a priority for a type, for deciding elaboration order
662-- * if it's just a type variable or concrete type, do it early (0)
663-- * if there's only type variables and injective constructors, do it next (1)
664-- * if there's a function type, next (2)
665-- * finally, everything else (3)
667getPriority :: IState -> PTerm -> Int
668getPriority i tm = pri tm
669 where
670 pri (PRef _ n) =
671 case lookupP n (tt_ctxt i) of
672 Just (P (DCon _ _) _ _) -> 1
673 Just (P (TCon _ _) _ _) -> 1
674 Just (P Ref _ _) -> 3
675 Nothing -> 0 -- must be locally bound, if it's not an error...
676 pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))
677 pri (PTrue _) = 0
678 pri (PFalse _) = 0
679 pri (PRefl _) = 1
680 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
681 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
682 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
683 pri (PDPair _ l r) = max 1 (max (pri l) (pri r))
684 pri (PConstant _) = 0
685 pri Placeholder = 1
686 pri _ = 3
688-- Dealing with implicit arguments
690-- Add implicit Pi bindings for any names in the term which appear in an
691-- argument position.
693-- This has become a right mess already. Better redo it some time...
695implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
696implicit syn n ptm
697 = do i <- get
698 let (tm', impdata) = implicitise syn i ptm
699 let (tm'', spos) = findStatics i tm'
700 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
701 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
702 i <- get
703 put (i { idris_statics = addDef n spos (idris_statics i) })
704 return tm''
706implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
707implicitise syn ist tm
708 = let uvars = using syn
709 pvars = syn_params syn
710 (declimps, ns') = execState (imps True [] tm) ([], [])
711 ns = ns' \\ (map fst pvars ++ no_imp syn) in
712 if null ns
713 then (tm, reverse declimps)
714 else implicitise syn ist (pibind uvars ns tm)
715 where
716 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
717 | otherwise = x : dropAll xs ys
718 dropAll [] ys = []
720 imps top env (PApp _ f as)
721 = do (decls, ns) <- get
722 let isn = concatMap (namesIn ist) (map getTm as)
723 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
724 imps top env (PPi (Imp l _) n ty sc)
725 = do let isn = nub (namesIn ist ty) `dropAll` [n]
726 (decls , ns) <- get
727 put (PImp (getPriority ist ty) l n ty : decls,
728 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
729 imps True (n:env) sc
730 imps top env (PPi (Exp l _) n ty sc)
731 = do let isn = nub (namesIn ist ty ++ case sc of
732 (PRef _ x) -> namesIn ist sc `dropAll` [n]
733 _ -> [])
734 (decls, ns) <- get -- ignore decls in HO types
735 put (PExp (getPriority ist ty) l ty : decls,
736 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
737 imps True (n:env) sc
738 imps top env (PPi (Constraint l _) n ty sc)
739 = do let isn = nub (namesIn ist ty ++ case sc of
740 (PRef _ x) -> namesIn ist sc `dropAll` [n]
741 _ -> [])
742 (decls, ns) <- get -- ignore decls in HO types
743 put (PConstraint 10 l ty : decls,
744 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
745 imps True (n:env) sc
746 imps top env (PEq _ l r)
747 = do (decls, ns) <- get
748 let isn = namesIn ist l ++ namesIn ist r
749 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
750 imps top env (PPair _ l r)
751 = do (decls, ns) <- get
752 let isn = namesIn ist l ++ namesIn ist r
753 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
754 imps top env (PDPair _ (PRef _ n) r)
755 = do (decls, ns) <- get
756 let isn = nub (namesIn ist r) \\ [n]
757 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
758 imps top env (PDPair _ l r)
759 = do (decls, ns) <- get
760 let isn = namesIn ist l ++ namesIn ist r
761 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
762 imps top env (PLam n ty sc)
763 = do imps False env ty
764 imps False (n:env) sc
765 imps top env (PHidden tm) = imps False env tm
766 imps top env _ = return ()
768 pibind using [] sc = sc
769 pibind using (n:ns) sc
770 = case lookup n using of
771 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
772 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
774-- Add implicit arguments in function calls
776addImpl :: IState -> PTerm -> PTerm
777addImpl ist ptm = ai [] ptm
778 where
779 ai env (PRef fc f) = aiFn ist fc f []
780 ai env (PEq fc l r) = let l' = ai env l
781 r' = ai env r in
782 PEq fc l' r'
783 ai env (PPair fc l r) = let l' = ai env l
784 r' = ai env r in
785 PPair fc l' r'
786 ai env (PDPair fc l r) = let l' = ai env l
787 r' = ai env r in
788 PDPair fc l' r'
789 ai env (PApp fc (PRef _ f) as)
790 = let as' = map (fmap (ai env)) as in
791 aiFn ist fc f as'
792 ai env (PApp fc f as) = let f' = ai env f
793 as' = map (fmap (ai env)) as in
794 mkPApp fc 1 f' as'
795 ai env (PLam n ty sc) = let ty' = ai env ty
796 sc' = ai (n:env) sc in
797 PLam n ty' sc'
798 ai env (PLet n ty val sc)
799 = let ty' = ai env ty
800 val' = ai env val
801 sc' = ai (n:env) sc in
802 PLet n ty' val' sc'
803 ai env (PPi p n ty sc) = let ty' = ai env ty
804 sc' = ai (n:env) sc in
805 PPi p n ty' sc'
806 ai env (PHidden tm) = PHidden (ai env tm)
807 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
808 ai env tm = tm
810aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
811aiFn ist fc f as
812 | f `elem` primNames = PApp fc (PRef fc f) as
813aiFn ist fc f as
814 = case lookupCtxt f (idris_implicits ist) of
815 Just ns -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)
816 Nothing -> mkPApp fc 1 (PRef fc f) as
817 where
818 insertImpl :: [PArg] -> [PArg] -> [PArg]
819 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
820 PExp p l tm : insertImpl ps given
821 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
822 PConstraint p l tm : insertImpl ps given
823 insertImpl (PConstraint p l ty : ps) given =
824 PConstraint p l (PResolveTC fc) : insertImpl ps given
825 insertImpl (PImp p l n ty : ps) given =
826 case find n given [] of
827 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
828 Nothing -> PImp p l n Placeholder : insertImpl ps given
829 insertImpl expected [] = []
830 insertImpl [] given = given
832 find n [] acc = Nothing
833 find n (PImp _ _ n' t : gs) acc
834 | n == n' = Just (t, reverse acc ++ gs)
835 find n (g : gs) acc = find n gs (g : acc)
837mkPApp fc a f [] = f
838mkPApp fc a f as = let rest = drop a as in
839 appRest fc (PApp fc f (take a as)) rest
840 where
841 appRest fc f [] = f
842 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
844-- Find 'static' argument positions
845-- (the declared ones, plus any names in argument position in the declared
846-- statics)
847-- FIXME: It's possible that this really has to happen after elaboration
849findStatics :: IState -> PTerm -> (PTerm, [Bool])
850findStatics ist tm = let (ns, ss) = fs tm in
851 runState (pos ns ss tm) []
852 where fs (PPi p n t sc)
853 | Static <- pstatic p
854 = let (ns, ss) = fs sc in
855 (namesIn ist t : ns, namesIn ist t ++ n : ss)
856 | otherwise = let (ns, ss) = fs sc in
857 (namesIn ist t : ns, ss)
858 fs _ = ([], [])
860 inOne n ns = length (filter id (map (elem n) ns)) == 1
862 pos ns ss (PPi p n t sc)
863 | n `inOne` ns && elem n ss
864 = do sc' <- pos ns ss sc
865 spos <- get
866 put (True : spos)
867 return (PPi (p { pstatic = Static }) n t sc')
868 | otherwise = do sc' <- pos ns ss sc
869 spos <- get
870 put (False : spos)
871 return (PPi p n t sc')
872 pos ns ss t = return t
874-- Debugging/logging stuff
876dumpDecls :: [PDecl] -> String
877dumpDecls [] = ""
878dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
880dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
881dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
882dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
883dumpDecl (PData _ _ d) = showDImp True d
884dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
885dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
886dumpDecl (PClass _ _ cs n ps ds)
887 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
888dumpDecl (PInstance _ _ cs n _ t ds)
889 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
890-- dumpDecl (PImport i) = "import " ++ i
892-- syntactic match of a against b, returning pair of variables in a
893-- and what they match. Returns 'Nothing' if not a match.
895matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
896matchClause x y = match x y where
897 matchArg x y = match (getTm x) (getTm y)
899 match (PApp _ f args) (PApp _ f' args')
900 | length args == length args'
901 = do mf <- match f f'
902 ms <- zipWithM matchArg args args'
903 return (mf ++ concat ms)
904 match (PRef _ n) (PRef _ n') | n == n' = return []
905 | otherwise = Nothing
906 match (PRef _ n) tm = return [(n, tm)]
907 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
908 mr <- match r r'
909 return (ml ++ mr)
910 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
911 mr <- match r r'
912 return (ml ++ mr)
913 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
914 mr <- match r r'
915 return (ml ++ mr)
916 match (PRefl _) (PRefl _) = return []
917 match (PResolveTC _) (PResolveTC _) = return []
918 match (PTrue _) (PTrue _) = return []
919 match (PFalse _) (PFalse _) = return []
920 match (PReturn _) (PReturn _) = return []
921 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
922 ms <- match s s'
923 return (mt ++ ms)
924 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
925 ms <- match s s'
926 return (mt ++ ms)
927 match (PHidden x) (PHidden y) = match x y
928 match a b | a == b = return []
929 | otherwise = Nothing
931substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
932substMatches [] t = t
933substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
935substMatch :: Name -> PTerm -> PTerm -> PTerm
936substMatch n tm t = sm t where
937 sm (PRef _ n') | n == n' = tm
938 sm (PLam x t sc) = PLam x (sm t) (sm sc)
939 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
940 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
941 sm (PEq f x y) = PEq f (sm x) (sm y)
942 sm (PPair f x y) = PPair f (sm x) (sm y)
943 sm (PDPair f x y) = PDPair f (sm x) (sm y)
944 sm (PHidden x) = PHidden (sm x)
945 sm x = x