git.iko.soy/Idris-dev
on 2c05448 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
945 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 deriving Functor
226data PClause' t = PClause Name t [t] t [PDecl' t]
227 | PWith Name t [t] t [PDecl' t]
228 deriving Functor
230data PData' t = PDatadecl { d_name :: Name,
231 d_tcon :: t,
232 d_cons :: [(Name, t, FC)] }
233 deriving Functor
235-- Handy to get a free function for applying PTerm -> PTerm functions
236-- across a program, by deriving Functor
238type PDecl = PDecl' PTerm
239type PData = PData' PTerm
240type PClause = PClause' PTerm
242-- get all the names declared in a decl
244declared :: PDecl -> [Name]
245declared (PFix _ _ _) = []
246declared (PTy _ _ n t) = [n]
247declared (PClauses _ _ n _) = [] -- not a declaration
248declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
249 where fstt (a, _, _) = a
250declared (PParams _ _ ds) = concatMap declared ds
251-- declared (PImport _) = []
253updateN :: [(Name, Name)] -> Name -> Name
254updateN ns n | Just n' <- lookup n ns = n'
255updateN _ n = n
257updateNs :: [(Name, Name)] -> PTerm -> PTerm
258updateNs [] t = t
259updateNs ns t = mapPT updateRef t
260 where updateRef (PRef fc f) = PRef fc (updateN ns f)
261 updateRef t = t
263-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
264-- updateDNs [] t = t
265-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
266-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
267-- where updateCNs ns (PClause n l ts r ds)
268-- = PClause (updateN ns n) (fmap (updateNs ns) l)
269-- (map (fmap (updateNs ns)) ts)
270-- (fmap (updateNs ns) r)
271-- (map (updateDNs ns) ds)
272-- updateDNs ns c = c
274-- High level language terms
276data PTerm = PQuote Raw
277 | PRef FC Name
278 | PLam Name PTerm PTerm
279 | PPi Plicity Name PTerm PTerm
280 | PLet Name PTerm PTerm PTerm
281 | PApp FC PTerm [PArg]
282 | PTrue FC
283 | PFalse FC
284 | PRefl FC
285 | PResolveTC FC
286 | PEq FC PTerm PTerm
287 | PPair FC PTerm PTerm
288 | PDPair FC PTerm PTerm
289 | PHidden PTerm -- irrelevant or hidden pattern
290 | PSet
291 | PConstant Const
292 | Placeholder
293 | PDoBlock [PDo]
294 | PReturn FC
295 | PMetavar Name
296 | PProof [PTactic]
297 | PElabError String -- error to report on elaboration
298 deriving Eq
300mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
301mapPT f t = f (mpt t) where
302 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
303 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
304 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
305 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
306 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
307 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
308 mpt (PDPair fc l r) = PDPair fc (mapPT f l) (mapPT f r)
309 mpt (PHidden t) = PHidden (mapPT f t)
310 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
311 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
312 mpt x = x
315data PTactic' t = Intro [Name] | Focus Name
316 | Refine Name [Bool] | Rewrite t
317 | Exact t | Compute | Trivial
318 | Solve
319 | Attack
320 | ProofState | ProofTerm | Undo
321 | Qed
322 deriving (Show, Eq, Functor)
324type PTactic = PTactic' PTerm
326data PDo' t = DoExp FC t
327 | DoBind FC Name t
328 | DoLet FC Name t
329 deriving (Eq, Functor)
331type PDo = PDo' PTerm
333-- The priority gives a hint as to elaboration order. Best to elaborate
334-- things early which will help give a more concrete type to other
335-- variables, e.g. a before (interpTy a).
337data PArg' t = PImp { priority :: Int,
338 lazyarg :: Bool, pname :: Name, getTm :: t }
339 | PExp { priority :: Int,
340 lazyarg :: Bool, getTm :: t }
341 | PConstraint { priority :: Int,
342 lazyarg :: Bool, getTm :: t }
343 deriving (Show, Eq, Functor)
345pimp = PImp 0 False
346pexp = PExp 0 False
347pconst = PConstraint 0 False
349type PArg = PArg' PTerm
351-- Type class data
353data ClassInfo = CI { instanceName :: Name,
354 class_methods :: [(Name, PTerm)],
355 class_params :: [Name] }
358-- Syntactic sugar info (TODO: namespaces, modules)
360data DSL = DSL { dsl_bind :: Name,
361 dsl_return :: Name }
362 deriving Show
364data Syntax = Rule [SSymbol] PTerm
365 deriving Show
367data SSymbol = Keyword Name
368 | Symbol String
369 | Expr Name
370 deriving Show
372initDSL = DSL (UN [">>="]) (UN ["return"])
374data SyntaxInfo = Syn { using :: [(Name, PTerm)],
375 syn_params :: [(Name, PTerm)],
376 no_imp :: [Name],
377 decoration :: Name -> Name,
378 dsl_info :: DSL }
379 deriving Show
381defaultSyntax = Syn [] [] [] id initDSL
383--- Pretty printing declarations and terms
385instance Show PTerm where
386 show tm = showImp False tm
388instance Show PDecl where
389 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
390 show (PTy _ _ n ty) = show n ++ " : " ++ show ty
391 show (PClauses _ _ n c) = showSep "\n" (map show c)
392 show (PData _ _ d) = show d
394instance Show PClause where
395 show c = showCImp True c
397instance Show PData where
398 show d = showDImp False d
400showCImp :: Bool -> PClause -> String
401showCImp impl (PClause n l ws r w)
402 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
403 ++ " where " ++ show w
404 where
405 showWs [] = ""
406 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
407showCImp impl (PWith n l ws r w)
408 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
409 ++ " { " ++ show w ++ " } "
410 where
411 showWs [] = ""
412 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
415showDImp :: Bool -> PData -> String
416showDImp impl (PDatadecl n ty cons)
417 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
418 ++ showSep "\n\t| "
419 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
421getImps :: [PArg] -> [(Name, PTerm)]
422getImps [] = []
423getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
424getImps (_ : xs) = getImps xs
426getExps :: [PArg] -> [PTerm]
427getExps [] = []
428getExps (PExp _ _ tm : xs) = tm : getExps xs
429getExps (_ : xs) = getExps xs
431getConsts :: [PArg] -> [PTerm]
432getConsts [] = []
433getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
434getConsts (_ : xs) = getConsts xs
436getAll :: [PArg] -> [PTerm]
437getAll = map getTm
439showImp :: Bool -> PTerm -> String
440showImp impl tm = se 10 tm where
441 se p (PQuote r) = "![" ++ show r ++ "]"
442 se p (PRef _ n) = show n
443 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
444 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
445 " in " ++ se 10 sc
446 se p (PPi (Exp l s) n ty sc)
447 | n `elem` allNamesIn sc = bracket p 2 $
448 if l then "|(" else "(" ++
449 show n ++ " : " ++ se 10 ty ++
450 ") " ++ st ++
451 "-> " ++ se 10 sc
452 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
453 where st = case s of
454 Static -> "[static] "
455 _ -> ""
456 se p (PPi (Imp l s) n ty sc)
457 | impl = bracket p 2 $ if l then "|{" else "{" ++
458 show n ++ " : " ++ se 10 ty ++
459 "} " ++ st ++ "-> " ++ se 10 sc
460 | otherwise = se 10 sc
461 where st = case s of
462 Static -> "[static] "
463 _ -> ""
464 se p (PPi (Constraint _ _) n ty sc)
465 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
466 se p (PApp _ (PRef _ f) [])
467 | not impl = show f
468 se p (PApp _ (PRef _ op@(UN [f:_])) args)
469 | length (getExps args) == 2 && not impl && not (isAlpha f)
470 = let [l, r] = getExps args in
471 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
472 se p (PApp _ f as)
473 = let args = getExps as in
474 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
475 else concatMap seArg args
476 se p (PHidden tm) = "." ++ se 0 tm
477 se p (PRefl _) = "refl"
478 se p (PResolveTC _) = "resolvetc"
479 se p (PTrue _) = "()"
480 se p (PFalse _) = "_|_"
481 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
482 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
483 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
484 se p PSet = "Set"
485 se p (PConstant c) = show c
486 se p (PProof ts) = "proof { " ++ show ts ++ "}"
487 se p (PMetavar n) = "?" ++ show n
488 se p Placeholder = "_"
490 sArg (PImp _ _ n tm) = siArg (n, tm)
491 sArg (PExp _ _ tm) = seArg tm
492 sArg (PConstraint _ _ tm) = scArg tm
494 seArg arg = " " ++ se 0 arg
495 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
496 scArg val = " {{" ++ se 10 val ++ "}}"
498 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
499 | otherwise = str
501allNamesIn :: PTerm -> [Name]
502allNamesIn tm = nub $ ni [] tm
503 where
504 ni env (PRef _ n)
505 | not (n `elem` env) = [n]
506 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
507 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
508 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
509 ni env (PHidden tm) = ni env tm
510 ni env (PEq _ l r) = ni env l ++ ni env r
511 ni env (PPair _ l r) = ni env l ++ ni env r
512 ni env (PDPair _ l r) = ni env l ++ ni env r
513 ni env _ = []
515namesIn :: IState -> PTerm -> [Name]
516namesIn ist tm = nub $ ni [] tm
517 where
518 ni env (PRef _ n)
519 | not (n `elem` env)
520 = case lookupCtxt n (idris_implicits ist) of
521 Nothing -> [n]
522 _ -> []
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 (PEq _ l r) = ni env l ++ ni env r
527 ni env (PPair _ l r) = ni env l ++ ni env r
528 ni env (PDPair _ l r) = ni env l ++ ni env r
529 ni env (PHidden tm) = ni env tm
530 ni env _ = []
532-- For inferring types of things
534bi = FC "builtin" 0
536inferTy = MN 0 "__Infer"
537inferCon = MN 0 "__infer"
538inferDecl = PDatadecl inferTy
539 PSet
540 [(inferCon, PPi impl (MN 0 "A") PSet (
541 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
542 (PRef bi inferTy)), bi)]
544infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
545infP = P (TCon 6 0) inferTy (Set 0)
547getInferTerm, getInferType :: Term -> Term
548getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
549getInferTerm (App (App _ _) tm) = tm
550getInferTerm tm = error ("getInferTerm " ++ show tm)
552getInferType (Bind n b sc) = Bind n b $ getInferType sc
553getInferType (App (App _ ty) _) = ty
555-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
557primNames = [unitTy, unitCon,
558 falseTy, pairTy, pairCon,
559 eqTy, eqCon, inferTy, inferCon]
561unitTy = MN 0 "__Unit"
562unitCon = MN 0 "__II"
563unitDecl = PDatadecl unitTy PSet
564 [(unitCon, PRef bi unitTy, bi)]
566falseTy = MN 0 "__False"
567falseDecl = PDatadecl falseTy PSet []
569pairTy = MN 0 "__Pair"
570pairCon = MN 0 "__MkPair"
571pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
572 [(pairCon, PPi impl (n "A") PSet (
573 PPi impl (n "B") PSet (
574 PPi expl (n "a") (PRef bi (n "A")) (
575 PPi expl (n "b") (PRef bi (n "B"))
576 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
577 pexp (PRef bi (n "B"))])))), bi)]
578 where n a = MN 0 a
580eqTy = UN ["="]
581eqCon = UN ["refl"]
582eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
583 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
584 PSet)
585 [(eqCon, PPi impl (n "a") PSet (
586 PPi impl (n "x") (PRef bi (n "a"))
587 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
588 pimp (n "b") Placeholder,
589 pexp (PRef bi (n "x")),
590 pexp (PRef bi (n "x"))])), bi)]
591 where n a = MN 0 a
593-- Defined in builtins.idr
594sigmaTy = UN ["Sigma"]
595existsCon = UN ["Exists"]
597piBind :: [(Name, PTerm)] -> PTerm -> PTerm
598piBind [] t = t
599piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
601-- Dealing with parameters
603expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
604expandParams dec ps ns tm = en tm
605 where
606 en (PLam n t s) = PLam n (en t) (en s)
607 en (PPi p n t s) = PPi p n (en t) (en s)
608 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)
609 en (PEq f l r) = PEq f (en l) (en r)
610 en (PPair f l r) = PPair f (en l) (en r)
611 en (PDPair f l r) = PDPair f (en l) (en r)
612 en (PHidden t) = PHidden (en t)
613 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
614 en (PProof ts) = PProof (map (fmap en) ts)
616 en (PQuote (Var n))
617 | n `elem` ns = PQuote (Var (dec n))
618 en (PApp fc (PRef fc' n) as)
619 | n `elem` ns = PApp fc (PRef fc' (dec n))
620 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
621 en (PRef fc n)
622 | n `elem` ns = PApp fc (PRef fc (dec n))
623 (map (pexp . (PRef fc)) (map fst ps))
624 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
625 en t = t
627expandParamsD :: IState ->
628 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
629expandParamsD ist dec ps ns (PTy syn fc n ty)
630 = if n `elem` ns
631 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
632 else PTy syn fc n (expandParams dec ps ns ty)
633expandParamsD ist dec ps ns (PClauses fc opts n cs)
634 = let n' = if n `elem` ns then dec n else n in
635 PClauses fc opts n' (map expandParamsC cs)
636 where
637 expandParamsC (PClause n lhs ws rhs ds)
638 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
639 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
640 n' = if n `elem` ns then dec n else n in
641 PClause n' (expandParams dec ps'' ns lhs)
642 (map (expandParams dec ps'' ns) ws)
643 (expandParams dec ps'' ns rhs)
644 (map (expandParamsD ist dec ps'' ns) ds)
645 expandParamsC (PWith n lhs ws wval ds)
646 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
647 ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
648 n' = if n `elem` ns then dec n else n in
649 PWith n' (expandParams dec ps'' ns lhs)
650 (map (expandParams dec ps'' ns) ws)
651 (expandParams dec ps'' ns wval)
652 (map (expandParamsD ist dec ps'' ns) ds)
653 updateps yn nm [] = []
654 updateps yn nm (((a, t), i):as)
655 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
656 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
658expandParamsD ist dec ps ns d = d
660-- Calculate a priority for a type, for deciding elaboration order
661-- * if it's just a type variable or concrete type, do it early (0)
662-- * if there's only type variables and injective constructors, do it next (1)
663-- * if there's a function type, next (2)
664-- * finally, everything else (3)
666getPriority :: IState -> PTerm -> Int
667getPriority i tm = pri tm
668 where
669 pri (PRef _ n) =
670 case lookupP n (tt_ctxt i) of
671 Just (P (DCon _ _) _ _) -> 1
672 Just (P (TCon _ _) _ _) -> 1
673 Just (P Ref _ _) -> 3
674 Nothing -> 0 -- must be locally bound, if it's not an error...
675 pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))
676 pri (PTrue _) = 0
677 pri (PFalse _) = 0
678 pri (PRefl _) = 1
679 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
680 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
681 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
682 pri (PDPair _ l r) = max 1 (max (pri l) (pri r))
683 pri (PConstant _) = 0
684 pri Placeholder = 1
685 pri _ = 3
687-- Dealing with implicit arguments
689-- Add implicit Pi bindings for any names in the term which appear in an
690-- argument position.
692-- This has become a right mess already. Better redo it some time...
694implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
695implicit syn n ptm
696 = do i <- get
697 let (tm', impdata) = implicitise syn i ptm
698 let (tm'', spos) = findStatics i tm'
699 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
700 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
701 i <- get
702 put (i { idris_statics = addDef n spos (idris_statics i) })
703 return tm''
705implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
706implicitise syn ist tm
707 = let uvars = using syn
708 pvars = syn_params syn
709 (declimps, ns') = execState (imps True [] tm) ([], [])
710 ns = ns' \\ (map fst pvars ++ no_imp syn) in
711 if null ns
712 then (tm, reverse declimps)
713 else implicitise syn ist (pibind uvars ns tm)
714 where
715 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
716 | otherwise = x : dropAll xs ys
717 dropAll [] ys = []
719 imps top env (PApp _ f as)
720 = do (decls, ns) <- get
721 let isn = concatMap (namesIn ist) (map getTm as)
722 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
723 imps top env (PPi (Imp l _) n ty sc)
724 = do let isn = nub (namesIn ist ty) `dropAll` [n]
725 (decls , ns) <- get
726 put (PImp (getPriority ist ty) l n ty : decls,
727 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
728 imps True (n:env) sc
729 imps top env (PPi (Exp l _) n ty sc)
730 = do let isn = nub (namesIn ist ty ++ case sc of
731 (PRef _ x) -> namesIn ist sc `dropAll` [n]
732 _ -> [])
733 (decls, ns) <- get -- ignore decls in HO types
734 put (PExp (getPriority ist ty) l ty : decls,
735 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
736 imps True (n:env) sc
737 imps top env (PPi (Constraint l _) n ty sc)
738 = do let isn = nub (namesIn ist ty ++ case sc of
739 (PRef _ x) -> namesIn ist sc `dropAll` [n]
740 _ -> [])
741 (decls, ns) <- get -- ignore decls in HO types
742 put (PConstraint 10 l ty : decls,
743 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
744 imps True (n:env) sc
745 imps top env (PEq _ l r)
746 = do (decls, ns) <- get
747 let isn = namesIn ist l ++ namesIn ist r
748 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
749 imps top env (PPair _ l r)
750 = do (decls, ns) <- get
751 let isn = namesIn ist l ++ namesIn ist r
752 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
753 imps top env (PDPair _ (PRef _ n) r)
754 = do (decls, ns) <- get
755 let isn = nub (namesIn ist r) \\ [n]
756 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
757 imps top env (PDPair _ l r)
758 = do (decls, ns) <- get
759 let isn = namesIn ist l ++ namesIn ist r
760 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
761 imps top env (PLam n ty sc)
762 = do imps False env ty
763 imps False (n:env) sc
764 imps top env (PHidden tm) = imps False env tm
765 imps top env _ = return ()
767 pibind using [] sc = sc
768 pibind using (n:ns) sc
769 = case lookup n using of
770 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
771 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
773-- Add implicit arguments in function calls
775addImpl :: IState -> PTerm -> PTerm
776addImpl ist ptm = ai [] ptm
777 where
778 ai env (PRef fc f) = aiFn ist fc f []
779 ai env (PEq fc l r) = let l' = ai env l
780 r' = ai env r in
781 PEq fc l' r'
782 ai env (PPair fc l r) = let l' = ai env l
783 r' = ai env r in
784 PPair fc l' r'
785 ai env (PDPair fc l r) = let l' = ai env l
786 r' = ai env r in
787 PDPair fc l' r'
788 ai env (PApp fc (PRef _ f) as)
789 = let as' = map (fmap (ai env)) as in
790 aiFn ist fc f as'
791 ai env (PApp fc f as) = let f' = ai env f
792 as' = map (fmap (ai env)) as in
793 mkPApp fc 1 f' as'
794 ai env (PLam n ty sc) = let ty' = ai env ty
795 sc' = ai (n:env) sc in
796 PLam n ty' sc'
797 ai env (PLet n ty val sc)
798 = let ty' = ai env ty
799 val' = ai env val
800 sc' = ai (n:env) sc in
801 PLet n ty' val' sc'
802 ai env (PPi p n ty sc) = let ty' = ai env ty
803 sc' = ai (n:env) sc in
804 PPi p n ty' sc'
805 ai env (PHidden tm) = PHidden (ai env tm)
806 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
807 ai env tm = tm
809aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
810aiFn ist fc f as
811 | f `elem` primNames = PApp fc (PRef fc f) as
812aiFn ist fc f as
813 = case lookupCtxt f (idris_implicits ist) of
814 Just ns -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)
815 Nothing -> mkPApp fc 1 (PRef fc f) as
816 where
817 insertImpl :: [PArg] -> [PArg] -> [PArg]
818 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
819 PExp p l tm : insertImpl ps given
820 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
821 PConstraint p l tm : insertImpl ps given
822 insertImpl (PConstraint p l ty : ps) given =
823 PConstraint p l (PResolveTC fc) : insertImpl ps given
824 insertImpl (PImp p l n ty : ps) given =
825 case find n given [] of
826 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
827 Nothing -> PImp p l n Placeholder : insertImpl ps given
828 insertImpl expected [] = []
829 insertImpl [] given = given
831 find n [] acc = Nothing
832 find n (PImp _ _ n' t : gs) acc
833 | n == n' = Just (t, reverse acc ++ gs)
834 find n (g : gs) acc = find n gs (g : acc)
836mkPApp fc a f [] = f
837mkPApp fc a f as = let rest = drop a as in
838 appRest fc (PApp fc f (take a as)) rest
839 where
840 appRest fc f [] = f
841 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
843-- Find 'static' argument positions
844-- (the declared ones, plus any names in argument position in the declared
845-- statics)
846-- FIXME: It's possible that this really has to happen after elaboration
848findStatics :: IState -> PTerm -> (PTerm, [Bool])
849findStatics ist tm = let (ns, ss) = fs tm in
850 runState (pos ns ss tm) []
851 where fs (PPi p n t sc)
852 | Static <- pstatic p
853 = let (ns, ss) = fs sc in
854 (namesIn ist t : ns, namesIn ist t ++ n : ss)
855 | otherwise = let (ns, ss) = fs sc in
856 (namesIn ist t : ns, ss)
857 fs _ = ([], [])
859 inOne n ns = length (filter id (map (elem n) ns)) == 1
861 pos ns ss (PPi p n t sc)
862 | n `inOne` ns && elem n ss
863 = do sc' <- pos ns ss sc
864 spos <- get
865 put (True : spos)
866 return (PPi (p { pstatic = Static }) n t sc')
867 | otherwise = do sc' <- pos ns ss sc
868 spos <- get
869 put (False : spos)
870 return (PPi p n t sc')
871 pos ns ss t = return t
873-- Debugging/logging stuff
875dumpDecls :: [PDecl] -> String
876dumpDecls [] = ""
877dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
879dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
880dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
881dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
882dumpDecl (PData _ _ d) = showDImp True d
883dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
884dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
885dumpDecl (PClass _ _ cs n ps ds)
886 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
887dumpDecl (PInstance _ _ cs n _ t ds)
888 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
889-- dumpDecl (PImport i) = "import " ++ i
891-- syntactic match of a against b, returning pair of variables in a
892-- and what they match. Returns 'Nothing' if not a match.
894matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
895matchClause x y = match x y where
896 matchArg x y = match (getTm x) (getTm y)
898 match (PApp _ f args) (PApp _ f' args')
899 | length args == length args'
900 = do mf <- match f f'
901 ms <- zipWithM matchArg args args'
902 return (mf ++ concat ms)
903 match (PRef _ n) (PRef _ n') | n == n' = return []
904 | otherwise = Nothing
905 match (PRef _ n) tm = return [(n, tm)]
906 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
907 mr <- match r r'
908 return (ml ++ mr)
909 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
910 mr <- match r r'
911 return (ml ++ mr)
912 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
913 mr <- match r r'
914 return (ml ++ mr)
915 match (PRefl _) (PRefl _) = return []
916 match (PResolveTC _) (PResolveTC _) = return []
917 match (PTrue _) (PTrue _) = return []
918 match (PFalse _) (PFalse _) = return []
919 match (PReturn _) (PReturn _) = return []
920 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
921 ms <- match s s'
922 return (mt ++ ms)
923 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
924 ms <- match s s'
925 return (mt ++ ms)
926 match (PHidden x) (PHidden y) = match x y
927 match a b | a == b = return []
928 | otherwise = Nothing
930substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
931substMatches [] t = t
932substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
934substMatch :: Name -> PTerm -> PTerm -> PTerm
935substMatch n tm t = sm t where
936 sm (PRef _ n') | n == n' = tm
937 sm (PLam x t sc) = PLam x (sm t) (sm sc)
938 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
939 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
940 sm (PEq f x y) = PEq f (sm x) (sm y)
941 sm (PPair f x y) = PPair f (sm x) (sm y)
942 sm (PDPair f x y) = PDPair f (sm x) (sm y)
943 sm (PHidden x) = PHidden (sm x)
944 sm x = x