git.iko.soy/Idris-dev
on 00052c8 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
849 lines 32 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances #-}
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
297data PArg' t = PImp { lazyarg :: Bool, pname :: Name, getTm :: t }
298 | PExp { lazyarg :: Bool, getTm :: t }
299 | PConstraint { lazyarg :: Bool, getTm :: t }
300 deriving (Show, Eq, Functor)
302pimp = PImp False
303pexp = PExp False
304pconst = PConstraint False
306type PArg = PArg' PTerm
308-- Syntactic sugar info (TODO: namespaces, modules)
310data DSL = DSL { dsl_bind :: Name,
311 dsl_return :: Name }
312 deriving Show
314data Syntax = Rule [SSymbol] PTerm
315 deriving Show
317data SSymbol = Keyword Name
318 | Symbol String
319 | Expr Name
320 deriving Show
322initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
324data SyntaxInfo = Syn { using :: [(Name, PTerm)],
325 syn_params :: [(Name, PTerm)],
326 no_imp :: [Name],
327 decoration :: Name -> Name,
328 dsl_info :: DSL }
329 deriving Show
331defaultSyntax = Syn [] [] [] id initDSL
333--- Pretty printing declarations and terms
335instance Show PTerm where
336 show tm = showImp False tm
338instance Show PDecl where
339 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
340 show (PTy _ _ n ty) = show n ++ " : " ++ show ty
341 show (PClauses _ n c) = showSep "\n" (map show c)
342 show (PData _ _ d) = show d
344instance Show PClause where
345 show c = showCImp True c
347instance Show PData where
348 show d = showDImp False d
350showCImp :: Bool -> PClause -> String
351showCImp impl (PClause n l ws r w)
352 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
353 ++ " where " ++ show w
354 where
355 showWs [] = ""
356 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
357showCImp impl (PWith n l ws r w)
358 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
359 ++ " { " ++ show w ++ " } "
360 where
361 showWs [] = ""
362 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
365showDImp :: Bool -> PData -> String
366showDImp impl (PDatadecl n ty cons)
367 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
368 ++ showSep "\n\t| "
369 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
371getImps :: [PArg] -> [(Name, PTerm)]
372getImps [] = []
373getImps (PImp _ n tm : xs) = (n, tm) : getImps xs
374getImps (_ : xs) = getImps xs
376getExps :: [PArg] -> [PTerm]
377getExps [] = []
378getExps (PExp _ tm : xs) = tm : getExps xs
379getExps (_ : xs) = getExps xs
381getConsts :: [PArg] -> [PTerm]
382getConsts [] = []
383getConsts (PConstraint _ tm : xs) = tm : getConsts xs
384getConsts (_ : xs) = getConsts xs
386getAll :: [PArg] -> [PTerm]
387getAll = map getTm
389showImp :: Bool -> PTerm -> String
390showImp impl tm = se 10 tm where
391 se p (PQuote r) = "![" ++ show r ++ "]"
392 se p (PRef _ n) = show n
393 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
394 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
395 " in " ++ se 10 sc
396 se p (PPi (Exp l s) n ty sc)
397 | n `elem` allNamesIn sc = bracket p 2 $
398 if l then "|(" else "(" ++
399 show n ++ " : " ++ se 10 ty ++
400 ") " ++ st ++
401 "-> " ++ se 10 sc
402 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
403 where st = case s of
404 Static -> "[static] "
405 _ -> ""
406 se p (PPi (Imp l s) n ty sc)
407 | impl = bracket p 2 $ if l then "|{" else "{" ++
408 show n ++ " : " ++ se 10 ty ++
409 "} " ++ st ++ "-> " ++ se 10 sc
410 | otherwise = se 10 sc
411 where st = case s of
412 Static -> "[static] "
413 _ -> ""
414 se p (PPi (Constraint _ _) n ty sc)
415 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
416 se p (PApp _ (PRef _ f) [])
417 | not impl = show f
418 se p (PApp _ (PRef _ op@(UN [f:_])) args)
419 | length (getExps args) == 2 && not impl && not (isAlpha f)
420 = let [l, r] = getExps args in
421 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
422 se p (PApp _ f as)
423 = let (imps, cs, args) = (getImps as, getConsts as, getExps as) in
424 bracket p 1 $ se 1 f ++ concatMap scArg cs
425 ++ (if impl then concatMap siArg imps else "")
426 ++ concatMap seArg args
427 se p (PHidden tm) = "." ++ se 0 tm
428 se p (PRefl _) = "refl"
429 se p (PResolveTC _) = "resolvetc"
430 se p (PTrue _) = "()"
431 se p (PFalse _) = "_|_"
432 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
433 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
434 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
435 se p PSet = "Set"
436 se p (PConstant c) = show c
437 se p (PProof ts) = "proof { " ++ show ts ++ "}"
438 se p (PMetavar n) = "?" ++ show n
439 se p Placeholder = "_"
441 seArg arg = " " ++ se 0 arg
442 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
443 scArg val = " {{" ++ se 10 val ++ "}}"
445 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
446 | otherwise = str
448allNamesIn :: PTerm -> [Name]
449allNamesIn tm = nub $ ni [] tm
450 where
451 ni env (PRef _ n)
452 | not (n `elem` env) = [n]
453 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
454 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
455 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
456 ni env (PHidden tm) = ni env tm
457 ni env (PEq _ l r) = ni env l ++ ni env r
458 ni env (PPair _ l r) = ni env l ++ ni env r
459 ni env (PDPair _ l r) = ni env l ++ ni env r
460 ni env _ = []
462namesIn :: IState -> PTerm -> [Name]
463namesIn ist tm = nub $ ni [] tm
464 where
465 ni env (PRef _ n)
466 | not (n `elem` env)
467 = case lookupCtxt n (idris_implicits ist) of
468 Nothing -> [n]
469 _ -> []
470 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
471 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
472 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
473 ni env (PEq _ l r) = ni env l ++ ni env r
474 ni env (PPair _ l r) = ni env l ++ ni env r
475 ni env (PDPair _ l r) = ni env l ++ ni env r
476 ni env (PHidden tm) = ni env tm
477 ni env _ = []
479-- For inferring types of things
481bi = FC "builtin" 0
483inferTy = MN 0 "__Infer"
484inferCon = MN 0 "__infer"
485inferDecl = PDatadecl inferTy
486 PSet
487 [(inferCon, PPi impl (MN 0 "A") PSet (
488 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
489 (PRef bi inferTy)), bi)]
491infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
492infP = P (TCon 6 0) inferTy (Set 0)
494getInferTerm, getInferType :: Term -> Term
495getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
496getInferTerm (App (App _ _) tm) = tm
497getInferTerm tm = error ("getInferTerm " ++ show tm)
499getInferType (Bind n b sc) = Bind n b $ getInferType sc
500getInferType (App (App _ ty) _) = ty
502-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
504primNames = [unitTy, unitCon,
505 falseTy, pairTy, pairCon,
506 eqTy, eqCon, inferTy, inferCon]
508unitTy = MN 0 "__Unit"
509unitCon = MN 0 "__II"
510unitDecl = PDatadecl unitTy PSet
511 [(unitCon, PRef bi unitTy, bi)]
513falseTy = MN 0 "__False"
514falseDecl = PDatadecl falseTy PSet []
516pairTy = MN 0 "__Pair"
517pairCon = MN 0 "__MkPair"
518pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
519 [(pairCon, PPi impl (n "A") PSet (
520 PPi impl (n "B") PSet (
521 PPi expl (n "a") (PRef bi (n "A")) (
522 PPi expl (n "b") (PRef bi (n "B"))
523 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
524 pexp (PRef bi (n "B"))])))), bi)]
525 where n a = MN 0 a
527eqTy = UN ["="]
528eqCon = UN ["refl"]
529eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
530 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
531 PSet)
532 [(eqCon, PPi impl (n "a") PSet (
533 PPi impl (n "x") (PRef bi (n "a"))
534 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
535 pimp (n "b") Placeholder,
536 pexp (PRef bi (n "x")),
537 pexp (PRef bi (n "x"))])), bi)]
538 where n a = MN 0 a
540-- Defined in builtins.idr
541sigmaTy = UN ["Sigma"]
542existsCon = UN ["Exists"]
544piBind :: [(Name, PTerm)] -> PTerm -> PTerm
545piBind [] t = t
546piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
548-- Dealing with parameters
550expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
551expandParams dec ps ns tm = en tm
552 where
553 en (PLam n t s) = PLam n (en t) (en s)
554 en (PPi p n t s) = PPi p n (en t) (en s)
555 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)
556 en (PEq f l r) = PEq f (en l) (en r)
557 en (PPair f l r) = PPair f (en l) (en r)
558 en (PDPair f l r) = PDPair f (en l) (en r)
559 en (PHidden t) = PHidden (en t)
560 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
561 en (PProof ts) = PProof (map (fmap en) ts)
563 en (PApp fc (PRef fc' n) as)
564 | n `elem` ns = PApp fc (PRef fc' (dec n))
565 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
566 en (PRef fc n)
567 | n `elem` ns = PApp fc (PRef fc (dec n))
568 (map (pexp . (PRef fc)) (map fst ps))
569 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
570 en t = t
572expandParamsD :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
573expandParamsD dec ps ns (PTy syn fc n ty)
574 = if n `elem` ns
575 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))
576 else PTy syn fc n (expandParams dec ps ns ty)
577expandParamsD dec ps ns (PClauses fc n cs)
578 = let n' = if n `elem` ns then dec n else n in
579 PClauses fc n' (map expandParamsC cs)
580 where
581 expandParamsC (PClause n lhs ws rhs ds)
582 = let n' = if n `elem` ns then dec n else n in
583 PClause n' (expandParams dec ps ns lhs)
584 (map (expandParams dec ps ns) ws)
585 (expandParams dec ps ns rhs)
586 (map (expandParamsD dec ps ns) ds)
587 expandParamsC (PWith n lhs ws wval ds)
588 = let n' = if n `elem` ns then dec n else n in
589 PWith n' (expandParams dec ps ns lhs)
590 (map (expandParams dec ps ns) ws)
591 (expandParams dec ps ns wval)
592 (map (expandParamsD dec ps ns) ds)
593expandParamsD dec ps ns d = d
595-- Dealing with implicit arguments
597-- Add implicit Pi bindings for any names in the term which appear in an
598-- argument position.
600-- This has become a right mess already. Better redo it some time...
602implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
603implicit syn n ptm
604 = do i <- get
605 let (tm', impdata) = implicitise syn i ptm
606 let (tm'', spos) = findStatics i tm'
607 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
608 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
609 i <- get
610 put (i { idris_statics = addDef n spos (idris_statics i) })
611 return tm''
613implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
614implicitise syn ist tm
615 = let uvars = using syn
616 pvars = syn_params syn
617 (declimps, ns') = execState (imps True [] tm) ([], [])
618 ns = ns' \\ (map fst pvars ++ no_imp syn) in
619 if null ns
620 then (tm, reverse declimps)
621 else implicitise syn ist (pibind uvars ns tm)
622 where
623 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
624 | otherwise = x : dropAll xs ys
625 dropAll [] ys = []
627 imps top env (PApp _ f as)
628 = do (decls, ns) <- get
629 let isn = concatMap (namesIn ist) (map getTm as)
630 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
631 imps top env (PPi (Imp l _) n ty sc)
632 = do let isn = nub (namesIn ist ty) `dropAll` [n]
633 (decls , ns) <- get
634 put (PImp l n ty : decls,
635 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
636 imps True (n:env) sc
637 imps top env (PPi (Exp l _) n ty sc)
638 = do let isn = nub (namesIn ist ty ++ case sc of
639 (PRef _ x) -> namesIn ist sc `dropAll` [n]
640 _ -> [])
641 (decls, ns) <- get -- ignore decls in HO types
642 put (PExp l ty : decls,
643 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
644 imps True (n:env) sc
645 imps top env (PPi (Constraint l _) n ty sc)
646 = do let isn = nub (namesIn ist ty ++ case sc of
647 (PRef _ x) -> namesIn ist sc `dropAll` [n]
648 _ -> [])
649 (decls, ns) <- get -- ignore decls in HO types
650 put (PConstraint l ty : decls,
651 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
652 imps True (n:env) sc
653 imps top env (PEq _ l r)
654 = do (decls, ns) <- get
655 let isn = namesIn ist l ++ namesIn ist r
656 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
657 imps top env (PPair _ l r)
658 = do (decls, ns) <- get
659 let isn = namesIn ist l ++ namesIn ist r
660 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
661 imps top env (PDPair _ (PRef _ n) r)
662 = do (decls, ns) <- get
663 let isn = nub (namesIn ist r) \\ [n]
664 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
665 imps top env (PDPair _ l r)
666 = do (decls, ns) <- get
667 let isn = namesIn ist l ++ namesIn ist r
668 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
669 imps top env (PLam n ty sc)
670 = do imps False env ty
671 imps False (n:env) sc
672 imps top env (PHidden tm) = imps False env tm
673 imps top env _ = return ()
675 pibind using [] sc = sc
676 pibind using (n:ns) sc
677 = case lookup n using of
678 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
679 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
681-- Add implicit arguments in function calls
683addImpl :: IState -> PTerm -> PTerm
684addImpl ist ptm = ai [] ptm
685 where
686 ai env (PRef fc f) = aiFn ist fc f []
687 ai env (PEq fc l r) = let l' = ai env l
688 r' = ai env r in
689 PEq fc l' r'
690 ai env (PPair fc l r) = let l' = ai env l
691 r' = ai env r in
692 PPair fc l' r'
693 ai env (PDPair fc l r) = let l' = ai env l
694 r' = ai env r in
695 PDPair fc l' r'
696 ai env (PApp fc (PRef _ f) as)
697 = let as' = map (fmap (ai env)) as in
698 aiFn ist fc f as'
699 ai env (PApp fc f as) = let f' = ai env f
700 as' = map (fmap (ai env)) as in
701 mkPApp fc 1 f' as'
702 ai env (PLam n ty sc) = let ty' = ai env ty
703 sc' = ai (n:env) sc in
704 PLam n ty' sc'
705 ai env (PLet n ty val sc)
706 = let ty' = ai env ty
707 val' = ai env val
708 sc' = ai (n:env) sc in
709 PLet n ty' val' sc'
710 ai env (PPi p n ty sc) = let ty' = ai env ty
711 sc' = ai (n:env) sc in
712 PPi p n ty' sc'
713 ai env (PHidden tm) = PHidden (ai env tm)
714 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
715 ai env tm = tm
717aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
718aiFn ist fc f as
719 | f `elem` primNames = PApp fc (PRef fc f) as
720aiFn ist fc f as
721 = case lookupCtxt f (idris_implicits ist) of
722 Just ns -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)
723 Nothing -> mkPApp fc 1 (PRef fc f) as
724 where
725 insertImpl :: [PArg] -> [PArg] -> [PArg]
726 insertImpl (PExp l ty : ps) (PExp _ tm : given) =
727 PExp l tm : insertImpl ps given
728 insertImpl (PConstraint l ty : ps) (PConstraint _ tm : given) =
729 PConstraint l tm : insertImpl ps given
730 insertImpl (PConstraint l ty : ps) given =
731 PConstraint l (PResolveTC fc) : insertImpl ps given
732 insertImpl (PImp l n ty : ps) given =
733 case find n given [] of
734 Just (tm, given') -> PImp l n tm : insertImpl ps given'
735 Nothing -> PImp l n Placeholder : insertImpl ps given
736 insertImpl expected [] = []
737 insertImpl [] given = given
739 find n [] acc = Nothing
740 find n (PImp _ n' t : gs) acc
741 | n == n' = Just (t, reverse acc ++ gs)
742 find n (g : gs) acc = find n gs (g : acc)
744mkPApp fc a f [] = f
745mkPApp fc a f as = let rest = drop a as in
746 appRest fc (PApp fc f (take a as)) rest
747 where
748 appRest fc f [] = f
749 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
751-- Find 'static' argument positions
752-- (the declared ones, plus any names in argument position in the declared
753-- statics)
754-- FIXME: It's possible that this really has to happen after elaboration
756findStatics :: IState -> PTerm -> (PTerm, [Bool])
757findStatics ist tm = let (ns, ss) = fs tm in
758 runState (pos ns ss tm) []
759 where fs (PPi p n t sc)
760 | Static <- pstatic p
761 = let (ns, ss) = fs sc in
762 (namesIn ist t : ns, namesIn ist t ++ n : ss)
763 | otherwise = let (ns, ss) = fs sc in
764 (namesIn ist t : ns, ss)
765 fs _ = ([], [])
767 inOne n ns = length (filter id (map (elem n) ns)) == 1
769 pos ns ss (PPi p n t sc)
770 | n `inOne` ns && elem n ss
771 = do sc' <- pos ns ss sc
772 spos <- get
773 put (True : spos)
774 return (PPi (p { pstatic = Static }) n t sc')
775 | otherwise = do sc' <- pos ns ss sc
776 spos <- get
777 put (False : spos)
778 return (PPi p n t sc')
779 pos ns ss t = return t
781-- Debugging/logging stuff
783dumpDecls :: [PDecl] -> String
784dumpDecls [] = ""
785dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
787dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
788dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
789dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
790dumpDecl (PData _ _ d) = showDImp True d
791dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
792dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
793-- dumpDecl (PImport i) = "import " ++ i
795-- syntactic match of a against b, returning pair of variables in a
796-- and what they match. Returns 'Nothing' if not a match.
798matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
799matchClause x y = match x y where
800 matchArg x y = match (getTm x) (getTm y)
802 match (PApp _ f args) (PApp _ f' args')
803 | length args == length args'
804 = do mf <- match f f'
805 ms <- zipWithM matchArg args args'
806 return (mf ++ concat ms)
807 match (PRef _ n) (PRef _ n') | n == n' = return []
808 | otherwise = Nothing
809 match (PRef _ n) tm = return [(n, tm)]
810 match (PEq _ l r) (PEq _ l' r') = do ml <- match l l'
811 mr <- match r r'
812 return (ml ++ mr)
813 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
814 mr <- match r r'
815 return (ml ++ mr)
816 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
817 mr <- match r r'
818 return (ml ++ mr)
819 match (PRefl _) (PRefl _) = return []
820 match (PResolveTC _) (PResolveTC _) = return []
821 match (PTrue _) (PTrue _) = return []
822 match (PFalse _) (PFalse _) = return []
823 match (PReturn _) (PReturn _) = return []
824 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
825 ms <- match s s'
826 return (mt ++ ms)
827 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
828 ms <- match s s'
829 return (mt ++ ms)
830 match (PHidden x) (PHidden y) = match x y
831 match a b | a == b = return []
832 | otherwise = Nothing
834substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
835substMatches [] t = t
836substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
838substMatch :: Name -> PTerm -> PTerm -> PTerm
839substMatch n tm t = sm t where
840 sm (PRef _ n') | n == n' = tm
841 sm (PLam x t sc) = PLam x (sm t) (sm sc)
842 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
843 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
844 sm (PEq f x y) = PEq f (sm x) (sm y)
845 sm (PPair f x y) = PPair f (sm x) (sm y)
846 sm (PDPair f x y) = PDPair f (sm x) (sm y)
847 sm (PHidden x) = PHidden (sm x)
848 sm x = x