git.iko.soy/Idris-dev
on df4ee4f help sign in
Idris-dev/src/Idris/AbsSyntax.hs
886 lines 33 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_log :: String,
35 idris_options :: IOption,
36 idris_name :: Int,
37 idris_metavars :: [Name],
38 syntax_rules :: [Syntax],
39 syntax_keywords :: [String],
40 imported :: [FilePath],
41 idris_prims :: [(Name, ([E.Name], E.Term))],
42 errLine :: Maybe Int
43 }
45idrisInit = IState emptyContext [] emptyContext emptyContext
46 "" defaultOpts 6 [] [] [] [] [] Nothing
48-- The monad for the main REPL - reading and processing files and updating
49-- global state (hence the IO inner monad).
50type Idris a = StateT IState IO a
52getContext :: Idris Context
53getContext = do i <- get; return (tt_ctxt i)
55setErrLine :: Int -> Idris ()
56setErrLine x = do i <- get;
57 case (errLine i) of
58 Nothing -> put (i { errLine = Just x })
59 Just _ -> return ()
61clearErr :: Idris ()
62clearErr = do i <- get
63 put (i { errLine = Nothing })
65getIState :: Idris IState
66getIState = get
68putIState :: IState -> Idris ()
69putIState = put
71getName :: Idris Int
72getName = do i <- get;
73 let idx = idris_name i;
74 put (i { idris_name = idx + 1 })
75 return idx
77checkUndefined :: FC -> Name -> Idris ()
78checkUndefined fc n
79 = do i <- getContext
80 case lookupCtxt n i of
81 Just _ -> fail $ show fc ++ ":" ++
82 show n ++ " already defined"
83 _ -> return ()
85setContext :: Context -> Idris ()
86setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
88updateContext :: (Context -> Context) -> Idris ()
89updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
91addDeferred :: [(Name, Type)] -> Idris ()
92addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
93 i <- get
94 put (i { idris_metavars = map fst ns ++ idris_metavars i })
95 where tidyNames used (Bind (MN i x) b sc)
96 = let n' = uniqueName (UN [x]) used in
97 Bind n' b $ tidyNames (n':used) sc
98 tidyNames used (Bind n b sc)
99 = let n' = uniqueName n used in
100 Bind n' b $ tidyNames (n':used) sc
101 tidyNames used b = b
103solveDeferred :: Name -> Idris ()
104solveDeferred n = do i <- get
105 put (i { idris_metavars = idris_metavars i \\ [n] })
107iputStrLn :: String -> Idris ()
108iputStrLn = lift.putStrLn
110setLogLevel :: Int -> Idris ()
111setLogLevel l = do i <- get
112 let opts = idris_options i
113 let opt' = opts { opt_logLevel = l }
114 put (i { idris_options = opt' } )
116logLevel :: Idris Int
117logLevel = do i <- get
118 return (opt_logLevel (idris_options i))
120logLvl :: Int -> String -> Idris ()
121logLvl l str = do i <- get
122 let lvl = opt_logLevel (idris_options i)
123 when (lvl >= l)
124 $ do lift (putStrLn str)
125 put (i { idris_log = idris_log i ++ str ++ "\n" } )
127iLOG :: String -> Idris ()
128iLOG = logLvl 1
130setTypeCase :: Bool -> Idris ()
131setTypeCase t = do i <- get
132 let opts = idris_options i
133 let opt' = opts { opt_typecase = t }
134 put (i { idris_options = opt' })
136-- Commands in the REPL
138data Command = Quit | Help | Eval PTerm | Reload | Edit
139 | Compile String
140 | Metavars | Prove Name
141 | TTShell
142 | LogLvl Int | Spec PTerm | HNF PTerm
143 | NOP
145-- Parsed declarations
147data Fixity = Infixl { prec :: Int }
148 | Infixr { prec :: Int }
149 | InfixN { prec :: Int }
150 | PrefixN { prec :: Int }
151 deriving Eq
153instance Show Fixity where
154 show (Infixl i) = "infixl " ++ show i
155 show (Infixr i) = "infixr " ++ show i
156 show (InfixN i) = "infix " ++ show i
157 show (PrefixN i) = "prefix " ++ show i
159data FixDecl = Fix Fixity String
160 deriving (Show, Eq)
162instance Ord FixDecl where
163 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
166data Static = Static | Dynamic
167 deriving (Show, Eq)
169-- Mark bindings with their explicitness, and laziness
170data Plicity = Imp { plazy :: Bool,
171 pstatic :: Static }
172 | Exp { plazy :: Bool,
173 pstatic :: Static }
174 | Constraint { plazy :: Bool,
175 pstatic :: Static }
176 deriving (Show, Eq)
178impl = Imp False Dynamic
179expl = Exp False Dynamic
180constraint = Constraint False Static
182data PDecl' t = PFix FC Fixity [String] -- fixity declaration
183 | PTy SyntaxInfo FC Name t -- type declaration
184 | PClauses FC Name [PClause' t] -- pattern clause
185 | PData SyntaxInfo FC (PData' t) -- data declaration
186 | PParams FC [(Name, t)] [PDecl' t] -- params block
187 | PSyntax FC Syntax
188 deriving Functor
190data PClause' t = PClause Name t [t] t [PDecl' t]
191 | PWith Name t [t] t [PDecl' t]
192 deriving Functor
194data PData' t = PDatadecl { d_name :: Name,
195 d_tcon :: t,
196 d_cons :: [(Name, t, FC)] }
197 deriving Functor
199-- Handy to get a free function for applying PTerm -> PTerm functions
200-- across a program, by deriving Functor
202type PDecl = PDecl' PTerm
203type PData = PData' PTerm
204type PClause = PClause' PTerm
206-- get all the names declared in a decl
208declared :: PDecl -> [Name]
209declared (PFix _ _ _) = []
210declared (PTy _ _ n t) = [n]
211declared (PClauses _ n _) = [] -- not a declaration
212declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
213 where fstt (a, _, _) = a
214declared (PParams _ _ ds) = concatMap declared ds
215-- declared (PImport _) = []
217updateN :: [(Name, Name)] -> Name -> Name
218updateN ns n | Just n' <- lookup n ns = n'
219updateN _ n = n
221updateNs :: [(Name, Name)] -> PTerm -> PTerm
222updateNs [] t = t
223updateNs ns t = mapPT updateRef t
224 where updateRef (PRef fc f) = PRef fc (updateN ns f)
225 updateRef t = t
227-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
228-- updateDNs [] t = t
229-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
230-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
231-- where updateCNs ns (PClause n l ts r ds)
232-- = PClause (updateN ns n) (fmap (updateNs ns) l)
233-- (map (fmap (updateNs ns)) ts)
234-- (fmap (updateNs ns) r)
235-- (map (updateDNs ns) ds)
236-- updateDNs ns c = c
238-- High level language terms
240data PTerm = PQuote Raw
241 | PRef FC Name
242 | PLam Name PTerm PTerm
243 | PPi Plicity Name PTerm PTerm
244 | PLet Name PTerm PTerm PTerm
245 | PApp FC PTerm [PArg]
246 | PTrue FC
247 | PFalse FC
248 | PRefl FC
249 | PResolveTC FC
250 | PEq FC PTerm PTerm
251 | PPair FC PTerm PTerm
252 | PDPair FC PTerm PTerm
253 | PHidden PTerm -- irrelevant or hidden pattern
254 | PSet
255 | PConstant Const
256 | Placeholder
257 | PDoBlock [PDo]
258 | PReturn FC
259 | PMetavar Name
260 | PProof [PTactic]
261 | PElabError String -- error to report on elaboration
262 deriving Eq
264mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
265mapPT f t = f (mpt t) where
266 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
267 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
268 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
269 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
270 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
271 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
272 mpt (PDPair fc l r) = PDPair fc (mapPT f l) (mapPT f r)
273 mpt (PHidden t) = PHidden (mapPT f t)
274 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
275 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
276 mpt x = x
279data PTactic' t = Intro [Name] | Focus Name
280 | Refine Name [Bool] | Rewrite t
281 | Exact t | Compute | Trivial
282 | Solve
283 | Attack
284 | ProofState | ProofTerm | Undo
285 | Qed
286 deriving (Show, Eq, Functor)
288type PTactic = PTactic' PTerm
290data PDo' t = DoExp FC t
291 | DoBind FC Name t
292 | DoLet FC Name t
293 deriving (Eq, Functor)
295type PDo = PDo' PTerm
297-- The priority gives a hint as to elaboration order. Best to elaborate
298-- things early which will help give a more concrete type to other
299-- variables, e.g. a before (interpTy a).
301data PArg' t = PImp { priority :: Int,
302 lazyarg :: Bool, pname :: Name, getTm :: t }
303 | PExp { priority :: Int,
304 lazyarg :: Bool, getTm :: t }
305 | PConstraint { priority :: Int,
306 lazyarg :: Bool, getTm :: t }
307 deriving (Show, Eq, Functor)
309pimp = PImp 0 False
310pexp = PExp 0 False
311pconst = PConstraint 0 False
313type PArg = PArg' PTerm
315-- Syntactic sugar info (TODO: namespaces, modules)
317data DSL = DSL { dsl_bind :: Name,
318 dsl_return :: Name }
319 deriving Show
321data Syntax = Rule [SSymbol] PTerm
322 deriving Show
324data SSymbol = Keyword Name
325 | Symbol String
326 | Expr Name
327 deriving Show
329initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
331data SyntaxInfo = Syn { using :: [(Name, PTerm)],
332 syn_params :: [(Name, PTerm)],
333 no_imp :: [Name],
334 decoration :: Name -> Name,
335 dsl_info :: DSL }
336 deriving Show
338defaultSyntax = Syn [] [] [] id initDSL
340--- Pretty printing declarations and terms
342instance Show PTerm where
343 show tm = showImp False tm
345instance Show PDecl where
346 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
347 show (PTy _ _ n ty) = show n ++ " : " ++ show ty
348 show (PClauses _ n c) = showSep "\n" (map show c)
349 show (PData _ _ d) = show d
351instance Show PClause where
352 show c = showCImp True c
354instance Show PData where
355 show d = showDImp False d
357showCImp :: Bool -> PClause -> String
358showCImp impl (PClause n l ws r w)
359 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
360 ++ " where " ++ show w
361 where
362 showWs [] = ""
363 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
364showCImp impl (PWith n l ws r w)
365 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
366 ++ " { " ++ show w ++ " } "
367 where
368 showWs [] = ""
369 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
372showDImp :: Bool -> PData -> String
373showDImp impl (PDatadecl n ty cons)
374 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
375 ++ showSep "\n\t| "
376 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
378getImps :: [PArg] -> [(Name, PTerm)]
379getImps [] = []
380getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
381getImps (_ : xs) = getImps xs
383getExps :: [PArg] -> [PTerm]
384getExps [] = []
385getExps (PExp _ _ tm : xs) = tm : getExps xs
386getExps (_ : xs) = getExps xs
388getConsts :: [PArg] -> [PTerm]
389getConsts [] = []
390getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
391getConsts (_ : xs) = getConsts xs
393getAll :: [PArg] -> [PTerm]
394getAll = map getTm
396showImp :: Bool -> PTerm -> String
397showImp impl tm = se 10 tm where
398 se p (PQuote r) = "![" ++ show r ++ "]"
399 se p (PRef _ n) = show n
400 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
401 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
402 " in " ++ se 10 sc
403 se p (PPi (Exp l s) n ty sc)
404 | n `elem` allNamesIn sc = bracket p 2 $
405 if l then "|(" else "(" ++
406 show n ++ " : " ++ se 10 ty ++
407 ") " ++ st ++
408 "-> " ++ se 10 sc
409 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
410 where st = case s of
411 Static -> "[static] "
412 _ -> ""
413 se p (PPi (Imp l s) n ty sc)
414 | impl = bracket p 2 $ if l then "|{" else "{" ++
415 show n ++ " : " ++ se 10 ty ++
416 "} " ++ st ++ "-> " ++ se 10 sc
417 | otherwise = se 10 sc
418 where st = case s of
419 Static -> "[static] "
420 _ -> ""
421 se p (PPi (Constraint _ _) n ty sc)
422 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
423 se p (PApp _ (PRef _ f) [])
424 | not impl = show f
425 se p (PApp _ (PRef _ op@(UN [f:_])) args)
426 | length (getExps args) == 2 && not impl && not (isAlpha f)
427 = let [l, r] = getExps args in
428 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
429 se p (PApp _ f as)
430 = let args = getExps as in
431 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
432 else concatMap seArg args
433 se p (PHidden tm) = "." ++ se 0 tm
434 se p (PRefl _) = "refl"
435 se p (PResolveTC _) = "resolvetc"
436 se p (PTrue _) = "()"
437 se p (PFalse _) = "_|_"
438 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
439 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
440 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
441 se p PSet = "Set"
442 se p (PConstant c) = show c
443 se p (PProof ts) = "proof { " ++ show ts ++ "}"
444 se p (PMetavar n) = "?" ++ show n
445 se p Placeholder = "_"
447 sArg (PImp _ _ n tm) = siArg (n, tm)
448 sArg (PExp _ _ tm) = seArg tm
449 sArg (PConstraint _ _ tm) = scArg tm
451 seArg arg = " " ++ se 0 arg
452 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
453 scArg val = " {{" ++ se 10 val ++ "}}"
455 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
456 | otherwise = str
458allNamesIn :: PTerm -> [Name]
459allNamesIn tm = nub $ ni [] tm
460 where
461 ni env (PRef _ n)
462 | not (n `elem` env) = [n]
463 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
464 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
465 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
466 ni env (PHidden tm) = ni env tm
467 ni env (PEq _ l r) = ni env l ++ ni env r
468 ni env (PPair _ l r) = ni env l ++ ni env r
469 ni env (PDPair _ l r) = ni env l ++ ni env r
470 ni env _ = []
472namesIn :: IState -> PTerm -> [Name]
473namesIn ist tm = nub $ ni [] tm
474 where
475 ni env (PRef _ n)
476 | not (n `elem` env)
477 = case lookupCtxt n (idris_implicits ist) of
478 Nothing -> [n]
479 _ -> []
480 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
481 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
482 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
483 ni env (PEq _ l r) = ni env l ++ ni env r
484 ni env (PPair _ l r) = ni env l ++ ni env r
485 ni env (PDPair _ l r) = ni env l ++ ni env r
486 ni env (PHidden tm) = ni env tm
487 ni env _ = []
489-- For inferring types of things
491bi = FC "builtin" 0
493inferTy = MN 0 "__Infer"
494inferCon = MN 0 "__infer"
495inferDecl = PDatadecl inferTy
496 PSet
497 [(inferCon, PPi impl (MN 0 "A") PSet (
498 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
499 (PRef bi inferTy)), bi)]
501infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
502infP = P (TCon 6 0) inferTy (Set 0)
504getInferTerm, getInferType :: Term -> Term
505getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
506getInferTerm (App (App _ _) tm) = tm
507getInferTerm tm = error ("getInferTerm " ++ show tm)
509getInferType (Bind n b sc) = Bind n b $ getInferType sc
510getInferType (App (App _ ty) _) = ty
512-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
514primNames = [unitTy, unitCon,
515 falseTy, pairTy, pairCon,
516 eqTy, eqCon, inferTy, inferCon]
518unitTy = MN 0 "__Unit"
519unitCon = MN 0 "__II"
520unitDecl = PDatadecl unitTy PSet
521 [(unitCon, PRef bi unitTy, bi)]
523falseTy = MN 0 "__False"
524falseDecl = PDatadecl falseTy PSet []
526pairTy = MN 0 "__Pair"
527pairCon = MN 0 "__MkPair"
528pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
529 [(pairCon, PPi impl (n "A") PSet (
530 PPi impl (n "B") PSet (
531 PPi expl (n "a") (PRef bi (n "A")) (
532 PPi expl (n "b") (PRef bi (n "B"))
533 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
534 pexp (PRef bi (n "B"))])))), bi)]
535 where n a = MN 0 a
537eqTy = UN ["="]
538eqCon = UN ["refl"]
539eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
540 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
541 PSet)
542 [(eqCon, PPi impl (n "a") PSet (
543 PPi impl (n "x") (PRef bi (n "a"))
544 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
545 pimp (n "b") Placeholder,
546 pexp (PRef bi (n "x")),
547 pexp (PRef bi (n "x"))])), bi)]
548 where n a = MN 0 a
550-- Defined in builtins.idr
551sigmaTy = UN ["Sigma"]
552existsCon = UN ["Exists"]
554piBind :: [(Name, PTerm)] -> PTerm -> PTerm
555piBind [] t = t
556piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
558-- Dealing with parameters
560expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
561expandParams dec ps ns tm = en tm
562 where
563 en (PLam n t s) = PLam n (en t) (en s)
564 en (PPi p n t s) = PPi p n (en t) (en s)
565 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)
566 en (PEq f l r) = PEq f (en l) (en r)
567 en (PPair f l r) = PPair f (en l) (en r)
568 en (PDPair f l r) = PDPair f (en l) (en r)
569 en (PHidden t) = PHidden (en t)
570 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
571 en (PProof ts) = PProof (map (fmap en) ts)
573 en (PApp fc (PRef fc' n) as)
574 | n `elem` ns = PApp fc (PRef fc' (dec n))
575 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
576 en (PRef fc n)
577 | n `elem` ns = PApp fc (PRef fc (dec n))
578 (map (pexp . (PRef fc)) (map fst ps))
579 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
580 en t = t
582expandParamsD :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
583expandParamsD dec ps ns (PTy syn fc n ty)
584 = if n `elem` ns
585 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
586 else PTy syn fc n (expandParams dec ps ns ty)
587expandParamsD dec ps ns (PClauses fc n cs)
588 = let n' = if n `elem` ns then dec n else n in
589 PClauses fc n' (map expandParamsC cs)
590 where
591 expandParamsC (PClause n lhs ws rhs ds)
592 = let n' = if n `elem` ns then dec n else n in
593 PClause n' (expandParams dec ps ns lhs)
594 (map (expandParams dec ps ns) ws)
595 (expandParams dec ps ns rhs)
596 (map (expandParamsD dec ps ns) ds)
597 expandParamsC (PWith n lhs ws wval ds)
598 = let n' = if n `elem` ns then dec n else n in
599 PWith n' (expandParams dec ps ns lhs)
600 (map (expandParams dec ps ns) ws)
601 (expandParams dec ps ns wval)
602 (map (expandParamsD dec ps ns) ds)
603expandParamsD dec ps ns d = d
605-- Calculate a priority for a type, for deciding elaboration order
606-- * if it's just a type variable or concrete type, do it early (0)
607-- * if there's only type variables and injective constructors, do it next (1)
608-- * if there's a function type, next (2)
609-- * finally, everything else (3)
611getPriority :: IState -> PTerm -> Int
612getPriority i tm = pri tm
613 where
614 pri (PRef _ n) =
615 case lookupP n (tt_ctxt i) of
616 Just (P (DCon _ _) _ _) -> 1
617 Just (P (TCon _ _) _ _) -> 1
618 Just (P Ref _ _) -> 3
619 Nothing -> 0 -- must be locally bound, if it's not an error...
620 pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))
621 pri (PTrue _) = 0
622 pri (PFalse _) = 0
623 pri (PRefl _) = 1
624 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
625 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
626 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
627 pri (PDPair _ l r) = max 1 (max (pri l) (pri r))
628 pri (PConstant _) = 0
629 pri Placeholder = 1
630 pri _ = 3
632-- Dealing with implicit arguments
634-- Add implicit Pi bindings for any names in the term which appear in an
635-- argument position.
637-- This has become a right mess already. Better redo it some time...
639implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
640implicit syn n ptm
641 = do i <- get
642 let (tm', impdata) = implicitise syn i ptm
643 let (tm'', spos) = findStatics i tm'
644 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
645 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
646 i <- get
647 put (i { idris_statics = addDef n spos (idris_statics i) })
648 return tm''
650implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
651implicitise syn ist tm
652 = let uvars = using syn
653 pvars = syn_params syn
654 (declimps, ns') = execState (imps True [] tm) ([], [])
655 ns = ns' \\ (map fst pvars ++ no_imp syn) in
656 if null ns
657 then (tm, reverse declimps)
658 else implicitise syn ist (pibind uvars ns tm)
659 where
660 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
661 | otherwise = x : dropAll xs ys
662 dropAll [] ys = []
664 imps top env (PApp _ f as)
665 = do (decls, ns) <- get
666 let isn = concatMap (namesIn ist) (map getTm as)
667 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
668 imps top env (PPi (Imp l _) n ty sc)
669 = do let isn = nub (namesIn ist ty) `dropAll` [n]
670 (decls , ns) <- get
671 put (PImp (getPriority ist ty) l n ty : decls,
672 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
673 imps True (n:env) sc
674 imps top env (PPi (Exp l _) n ty sc)
675 = do let isn = nub (namesIn ist ty ++ case sc of
676 (PRef _ x) -> namesIn ist sc `dropAll` [n]
677 _ -> [])
678 (decls, ns) <- get -- ignore decls in HO types
679 put (PExp (getPriority ist ty) l ty : decls,
680 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
681 imps True (n:env) sc
682 imps top env (PPi (Constraint l _) n ty sc)
683 = do let isn = nub (namesIn ist ty ++ case sc of
684 (PRef _ x) -> namesIn ist sc `dropAll` [n]
685 _ -> [])
686 (decls, ns) <- get -- ignore decls in HO types
687 put (PConstraint 10 l ty : decls,
688 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
689 imps True (n:env) sc
690 imps top env (PEq _ l r)
691 = do (decls, ns) <- get
692 let isn = namesIn ist l ++ namesIn ist r
693 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
694 imps top env (PPair _ l r)
695 = do (decls, ns) <- get
696 let isn = namesIn ist l ++ namesIn ist r
697 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
698 imps top env (PDPair _ (PRef _ n) r)
699 = do (decls, ns) <- get
700 let isn = nub (namesIn ist r) \\ [n]
701 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
702 imps top env (PDPair _ l r)
703 = do (decls, ns) <- get
704 let isn = namesIn ist l ++ namesIn ist r
705 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
706 imps top env (PLam n ty sc)
707 = do imps False env ty
708 imps False (n:env) sc
709 imps top env (PHidden tm) = imps False env tm
710 imps top env _ = return ()
712 pibind using [] sc = sc
713 pibind using (n:ns) sc
714 = case lookup n using of
715 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
716 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
718-- Add implicit arguments in function calls
720addImpl :: IState -> PTerm -> PTerm
721addImpl ist ptm = ai [] ptm
722 where
723 ai env (PRef fc f) = aiFn ist fc f []
724 ai env (PEq fc l r) = let l' = ai env l
725 r' = ai env r in
726 PEq fc l' r'
727 ai env (PPair fc l r) = let l' = ai env l
728 r' = ai env r in
729 PPair fc l' r'
730 ai env (PDPair fc l r) = let l' = ai env l
731 r' = ai env r in
732 PDPair fc l' r'
733 ai env (PApp fc (PRef _ f) as)
734 = let as' = map (fmap (ai env)) as in
735 aiFn ist fc f as'
736 ai env (PApp fc f as) = let f' = ai env f
737 as' = map (fmap (ai env)) as in
738 mkPApp fc 1 f' as'
739 ai env (PLam n ty sc) = let ty' = ai env ty
740 sc' = ai (n:env) sc in
741 PLam n ty' sc'
742 ai env (PLet n ty val sc)
743 = let ty' = ai env ty
744 val' = ai env val
745 sc' = ai (n:env) sc in
746 PLet n ty' val' sc'
747 ai env (PPi p n ty sc) = let ty' = ai env ty
748 sc' = ai (n:env) sc in
749 PPi p n ty' sc'
750 ai env (PHidden tm) = PHidden (ai env tm)
751 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
752 ai env tm = tm
754aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
755aiFn ist fc f as
756 | f `elem` primNames = PApp fc (PRef fc f) as
757aiFn ist fc f as
758 = case lookupCtxt f (idris_implicits ist) of
759 Just ns -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)
760 Nothing -> mkPApp fc 1 (PRef fc f) as
761 where
762 insertImpl :: [PArg] -> [PArg] -> [PArg]
763 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
764 PExp p l tm : insertImpl ps given
765 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
766 PConstraint p l tm : insertImpl ps given
767 insertImpl (PConstraint p l ty : ps) given =
768 PConstraint p l (PResolveTC fc) : insertImpl ps given
769 insertImpl (PImp p l n ty : ps) given =
770 case find n given [] of
771 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
772 Nothing -> PImp p l n Placeholder : insertImpl ps given
773 insertImpl expected [] = []
774 insertImpl [] given = given
776 find n [] acc = Nothing
777 find n (PImp _ _ n' t : gs) acc
778 | n == n' = Just (t, reverse acc ++ gs)
779 find n (g : gs) acc = find n gs (g : acc)
781mkPApp fc a f [] = f
782mkPApp fc a f as = let rest = drop a as in
783 appRest fc (PApp fc f (take a as)) rest
784 where
785 appRest fc f [] = f
786 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
788-- Find 'static' argument positions
789-- (the declared ones, plus any names in argument position in the declared
790-- statics)
791-- FIXME: It's possible that this really has to happen after elaboration
793findStatics :: IState -> PTerm -> (PTerm, [Bool])
794findStatics ist tm = let (ns, ss) = fs tm in
795 runState (pos ns ss tm) []
796 where fs (PPi p n t sc)
797 | Static <- pstatic p
798 = let (ns, ss) = fs sc in
799 (namesIn ist t : ns, namesIn ist t ++ n : ss)
800 | otherwise = let (ns, ss) = fs sc in
801 (namesIn ist t : ns, ss)
802 fs _ = ([], [])
804 inOne n ns = length (filter id (map (elem n) ns)) == 1
806 pos ns ss (PPi p n t sc)
807 | n `inOne` ns && elem n ss
808 = do sc' <- pos ns ss sc
809 spos <- get
810 put (True : spos)
811 return (PPi (p { pstatic = Static }) n t sc')
812 | otherwise = do sc' <- pos ns ss sc
813 spos <- get
814 put (False : spos)
815 return (PPi p n t sc')
816 pos ns ss t = return t
818-- Debugging/logging stuff
820dumpDecls :: [PDecl] -> String
821dumpDecls [] = ""
822dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
824dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
825dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
826dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
827dumpDecl (PData _ _ d) = showDImp True d
828dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
829dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
830-- dumpDecl (PImport i) = "import " ++ i
832-- syntactic match of a against b, returning pair of variables in a
833-- and what they match. Returns 'Nothing' if not a match.
835matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
836matchClause x y = match x y where
837 matchArg x y = match (getTm x) (getTm y)
839 match (PApp _ f args) (PApp _ f' args')
840 | length args == length args'
841 = do mf <- match f f'
842 ms <- zipWithM matchArg args args'
843 return (mf ++ concat ms)
844 match (PRef _ n) (PRef _ n') | n == n' = return []
845 | otherwise = Nothing
846 match (PRef _ n) tm = return [(n, tm)]
847 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
848 mr <- match r r'
849 return (ml ++ mr)
850 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
851 mr <- match r r'
852 return (ml ++ mr)
853 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
854 mr <- match r r'
855 return (ml ++ mr)
856 match (PRefl _) (PRefl _) = return []
857 match (PResolveTC _) (PResolveTC _) = return []
858 match (PTrue _) (PTrue _) = return []
859 match (PFalse _) (PFalse _) = return []
860 match (PReturn _) (PReturn _) = return []
861 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
862 ms <- match s s'
863 return (mt ++ ms)
864 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
865 ms <- match s s'
866 return (mt ++ ms)
867 match (PHidden x) (PHidden y) = match x y
868 match a b | a == b = return []
869 | otherwise = Nothing
871substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
872substMatches [] t = t
873substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
875substMatch :: Name -> PTerm -> PTerm -> PTerm
876substMatch n tm t = sm t where
877 sm (PRef _ n') | n == n' = tm
878 sm (PLam x t sc) = PLam x (sm t) (sm sc)
879 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
880 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
881 sm (PEq f x y) = PEq f (sm x) (sm y)
882 sm (PPair f x y) = PPair f (sm x) (sm y)
883 sm (PDPair f x y) = PDPair f (sm x) (sm y)
884 sm (PHidden x) = PHidden (sm x)
885 sm x = x