git.iko.soy/Idris-dev
on 02ef050 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1507 lines 58 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 System.Console.Haskeline
12import Control.Monad.State
13import Data.List
14import Data.Char
15import Data.Either
16import Debug.Trace
18import qualified Epic.Epic as E
20data IOption = IOption { opt_logLevel :: Int,
21 opt_typecase :: Bool,
22 opt_typeintype :: Bool,
23 opt_coverage :: Bool,
24 opt_showimp :: Bool,
25 opt_repl :: Bool,
26 opt_verbose :: Bool
27 }
28 deriving (Show, Eq)
30defaultOpts = IOption 0 False False True False True True
32-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
33-- without typechecking).
34-- This will include all the functions and data declarations, plus fixity declarations
35-- and syntax macros.
37data IState = IState { tt_ctxt :: Context,
38 idris_constraints :: [(UConstraint, FC)],
39 idris_infixes :: [FixDecl],
40 idris_implicits :: Ctxt [PArg],
41 idris_statics :: Ctxt [Bool],
42 idris_classes :: Ctxt ClassInfo,
43 idris_dsls :: Ctxt DSL,
44 idris_optimisation :: Ctxt OptInfo,
45 idris_datatypes :: Ctxt TypeInfo,
46 idris_patdefs :: Ctxt [(Term, Term)], -- not exported
47 idris_flags :: Ctxt [FnOpt],
48 idris_callgraph :: Ctxt [Name],
49 idris_totcheck :: [(FC, Name)],
50 idris_log :: String,
51 idris_options :: IOption,
52 idris_name :: Int,
53 idris_metavars :: [Name],
54 syntax_rules :: [Syntax],
55 syntax_keywords :: [String],
56 imported :: [FilePath],
57 idris_prims :: [(Name, ([E.Name], E.Term))],
58 idris_objs :: [FilePath],
59 idris_libs :: [String],
60 idris_hdrs :: [String],
61 last_proof :: Maybe (Name, [String]),
62 errLine :: Maybe Int,
63 lastParse :: Maybe Name,
64 indent_stack :: [Int],
65 brace_stack :: [Maybe Int],
66 hide_list :: [(Name, Maybe Accessibility)],
67 default_access :: Accessibility,
68 ibc_write :: [IBCWrite],
69 compiled_so :: Maybe String
70 }
72-- information that needs writing for the current module's .ibc file
73data IBCWrite = IBCFix FixDecl
74 | IBCImp Name
75 | IBCStatic Name
76 | IBCClass Name
77 | IBCInstance Bool Name Name
78 | IBCDSL Name
79 | IBCData Name
80 | IBCOpt Name
81 | IBCSyntax Syntax
82 | IBCKeyword String
83 | IBCImport FilePath
84 | IBCObj FilePath
85 | IBCLib String
86 | IBCHeader String
87 | IBCAccess Name Accessibility
88 | IBCTotal Name Totality
89 | IBCFlags Name [FnOpt]
90 | IBCCG Name
91 | IBCDef Name -- i.e. main context
92 deriving Show
94idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
95 emptyContext emptyContext emptyContext emptyContext
96 emptyContext emptyContext
97 [] "" defaultOpts 6 [] [] [] [] [] [] [] []
98 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
100-- The monad for the main REPL - reading and processing files and updating
101-- global state (hence the IO inner monad).
102type Idris = StateT IState (InputT IO)
104getContext :: Idris Context
105getContext = do i <- get; return (tt_ctxt i)
107getObjectFiles :: Idris [FilePath]
108getObjectFiles = do i <- get; return (idris_objs i)
110addObjectFile :: FilePath -> Idris ()
111addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
113getLibs :: Idris [String]
114getLibs = do i <- get; return (idris_libs i)
116addLib :: String -> Idris ()
117addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
119addHdr :: String -> Idris ()
120addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
122totcheck :: (FC, Name) -> Idris ()
123totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i })
125setFlags :: Name -> [FnOpt] -> Idris ()
126setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
128setAccessibility :: Name -> Accessibility -> Idris ()
129setAccessibility n a
130 = do i <- get
131 let ctxt = setAccess n a (tt_ctxt i)
132 put (i { tt_ctxt = ctxt })
134setTotality :: Name -> Totality -> Idris ()
135setTotality n a
136 = do i <- get
137 let ctxt = setTotal n a (tt_ctxt i)
138 put (i { tt_ctxt = ctxt })
140getTotality :: Name -> Idris Totality
141getTotality n
142 = do i <- get
143 case lookupTotal n (tt_ctxt i) of
144 [t] -> return t
145 _ -> return (Total [])
147addToCG :: Name -> [Name] -> Idris ()
148addToCG n ns = do i <- get
149 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
151-- Add a class instance function. Dodgy hack: Put integer instances first in the
152-- list so they are resolved by default.
154addInstance :: Bool -> Name -> Name -> Idris ()
155addInstance int n i
156 = do ist <- get
157 case lookupCtxt Nothing n (idris_classes ist) of
158 [CI a b c d ins] ->
159 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
160 put (ist { idris_classes = cs })
161 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
162 put (ist { idris_classes = cs })
163 where addI i ins | int = i : ins
164 | otherwise = ins ++ [i]
166addClass :: Name -> ClassInfo -> Idris ()
167addClass n i
168 = do ist <- get
169 let i' = case lookupCtxt Nothing n (idris_classes ist) of
170 [c] -> c { class_instances = class_instances i }
171 _ -> i
172 put (ist { idris_classes = addDef n i' (idris_classes ist) })
174addIBC :: IBCWrite -> Idris ()
175addIBC ibc@(IBCDef n)
176 = do i <- get
177 when (notDef (ibc_write i)) $
178 put (i { ibc_write = ibc : ibc_write i })
179 where notDef [] = True
180 notDef (IBCDef n': is) | n == n' = False
181 notDef (_ : is) = notDef is
182addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
184clearIBC :: Idris ()
185clearIBC = do i <- get; put (i { ibc_write = [] })
187getHdrs :: Idris [String]
188getHdrs = do i <- get; return (idris_hdrs i)
190setErrLine :: Int -> Idris ()
191setErrLine x = do i <- get;
192 case (errLine i) of
193 Nothing -> put (i { errLine = Just x })
194 Just _ -> return ()
196clearErr :: Idris ()
197clearErr = do i <- get
198 put (i { errLine = Nothing })
200getSO :: Idris (Maybe String)
201getSO = do i <- get
202 return (compiled_so i)
204setSO :: Maybe String -> Idris ()
205setSO s = do i <- get
206 put (i { compiled_so = s })
208getIState :: Idris IState
209getIState = get
211putIState :: IState -> Idris ()
212putIState = put
214getName :: Idris Int
215getName = do i <- get;
216 let idx = idris_name i;
217 put (i { idris_name = idx + 1 })
218 return idx
220checkUndefined :: FC -> Name -> Idris ()
221checkUndefined fc n
222 = do i <- getContext
223 case lookupTy Nothing n i of
224 (_:_) -> fail $ show fc ++ ":" ++
225 show n ++ " already defined"
226 _ -> return ()
228setContext :: Context -> Idris ()
229setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
231updateContext :: (Context -> Context) -> Idris ()
232updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
234addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
235addConstraints fc (v, cs)
236 = do i <- get
237 let ctxt = tt_ctxt i
238 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
239 next_tvar = v }
240 let ics = zip cs (repeat fc) ++ idris_constraints i
241 put (i { tt_ctxt = ctxt', idris_constraints = ics })
243addDeferred :: [(Name, Type)] -> Idris ()
244addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
245 i <- get
246 put (i { idris_metavars = map fst ns ++ idris_metavars i })
247 where tidyNames used (Bind (MN i x) b sc)
248 = let n' = uniqueName (UN x) used in
249 Bind n' b $ tidyNames (n':used) sc
250 tidyNames used (Bind n b sc)
251 = let n' = uniqueName n used in
252 Bind n' b $ tidyNames (n':used) sc
253 tidyNames used b = b
255solveDeferred :: Name -> Idris ()
256solveDeferred n = do i <- get
257 put (i { idris_metavars = idris_metavars i \\ [n] })
259iputStrLn :: String -> Idris ()
260iputStrLn = liftIO . putStrLn
262iWarn :: FC -> String -> Idris ()
263iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
265setLogLevel :: Int -> Idris ()
266setLogLevel l = do i <- get
267 let opts = idris_options i
268 let opt' = opts { opt_logLevel = l }
269 put (i { idris_options = opt' } )
271logLevel :: Idris Int
272logLevel = do i <- get
273 return (opt_logLevel (idris_options i))
275useREPL :: Idris Bool
276useREPL = do i <- get
277 return (opt_repl (idris_options i))
279setREPL :: Bool -> Idris ()
280setREPL t = do i <- get
281 let opts = idris_options i
282 let opt' = opts { opt_repl = t }
283 put (i { idris_options = opt' })
285verbose :: Idris Bool
286verbose = do i <- get
287 return (opt_verbose (idris_options i))
289setVerbose :: Bool -> Idris ()
290setVerbose t = do i <- get
291 let opts = idris_options i
292 let opt' = opts { opt_verbose = t }
293 put (i { idris_options = opt' })
295typeInType :: Idris Bool
296typeInType = do i <- get
297 return (opt_typeintype (idris_options i))
299setTypeInType :: Bool -> Idris ()
300setTypeInType t = do i <- get
301 let opts = idris_options i
302 let opt' = opts { opt_typeintype = t }
303 put (i { idris_options = opt' })
305coverage :: Idris Bool
306coverage = do i <- get
307 return (opt_coverage (idris_options i))
309setCoverage :: Bool -> Idris ()
310setCoverage t = do i <- get
311 let opts = idris_options i
312 let opt' = opts { opt_coverage = t }
313 put (i { idris_options = opt' })
315impShow :: Idris Bool
316impShow = do i <- get
317 return (opt_showimp (idris_options i))
319setImpShow :: Bool -> Idris ()
320setImpShow t = do i <- get
321 let opts = idris_options i
322 let opt' = opts { opt_showimp = t }
323 put (i { idris_options = opt' })
325logLvl :: Int -> String -> Idris ()
326logLvl l str = do i <- get
327 let lvl = opt_logLevel (idris_options i)
328 when (lvl >= l)
329 $ do liftIO (putStrLn str)
330 put (i { idris_log = idris_log i ++ str ++ "\n" } )
332iLOG :: String -> Idris ()
333iLOG = logLvl 1
335noErrors :: Idris Bool
336noErrors = do i <- get
337 case errLine i of
338 Nothing -> return True
339 _ -> return False
341setTypeCase :: Bool -> Idris ()
342setTypeCase t = do i <- get
343 let opts = idris_options i
344 let opt' = opts { opt_typecase = t }
345 put (i { idris_options = opt' })
347-- Commands in the REPL
349data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
350 | Reload | Edit
351 | Compile String | Execute | ExecVal PTerm
352 | Metavars | Prove Name | AddProof | Universes
353 | TTShell
354 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name | Info Name
355 | NOP
357-- Parsed declarations
359data Fixity = Infixl { prec :: Int }
360 | Infixr { prec :: Int }
361 | InfixN { prec :: Int }
362 | PrefixN { prec :: Int }
363 deriving Eq
364{-!
365deriving instance Binary Fixity
366!-}
368instance Show Fixity where
369 show (Infixl i) = "infixl " ++ show i
370 show (Infixr i) = "infixr " ++ show i
371 show (InfixN i) = "infix " ++ show i
372 show (PrefixN i) = "prefix " ++ show i
374data FixDecl = Fix Fixity String
375 deriving (Show, Eq)
376{-!
377deriving instance Binary FixDecl
378!-}
380instance Ord FixDecl where
381 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
384data Static = Static | Dynamic
385 deriving (Show, Eq)
386{-!
387deriving instance Binary Static
388!-}
390-- Mark bindings with their explicitness, and laziness
391data Plicity = Imp { plazy :: Bool,
392 pstatic :: Static }
393 | Exp { plazy :: Bool,
394 pstatic :: Static }
395 | Constraint { plazy :: Bool,
396 pstatic :: Static }
397 | TacImp { plazy :: Bool,
398 pstatic :: Static,
399 pscript :: PTerm }
400 deriving (Show, Eq)
402{-!
403deriving instance Binary Plicity
404!-}
406impl = Imp False Dynamic
407expl = Exp False Dynamic
408constraint = Constraint False Dynamic
409tacimpl = TacImp False Dynamic
411data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
412 | Specialise [Name] -- specialise it, freeze these names
413 deriving (Show, Eq)
414{-!
415deriving instance Binary FnOpt
416!-}
418type FnOpts = [FnOpt]
420inlinable :: FnOpts -> Bool
421inlinable = elem Inlinable
423data PDecl' t = PFix FC Fixity [String] -- fixity declaration
424 | PTy SyntaxInfo FC FnOpts Name t -- type declaration
425 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
426 | PData SyntaxInfo FC (PData' t) -- data declaration
427 | PParams FC [(Name, t)] [PDecl' t] -- params block
428 | PNamespace String [PDecl' t] -- new namespace
429 | PRecord SyntaxInfo FC Name t Name t -- record declaration
430 | PClass SyntaxInfo FC
431 [t] -- constraints
432 Name
433 [(Name, t)] -- parameters
434 [PDecl' t] -- declarations
435 | PInstance SyntaxInfo FC [t] -- constraints
436 Name -- class
437 [t] -- parameters
438 t -- full instance type
439 [PDecl' t]
440 | PDSL Name (DSL' t)
441 | PSyntax FC Syntax
442 | PDirective (Idris ())
443 deriving Functor
445data PClause' t = PClause FC Name t [t] t [PDecl' t]
446 | PWith FC Name t [t] t [PDecl' t]
447 | PClauseR FC [t] t [PDecl' t]
448 | PWithR FC [t] t [PDecl' t]
449 deriving Functor
451data PData' t = PDatadecl { d_name :: Name,
452 d_tcon :: t,
453 d_cons :: [(Name, t, FC)] }
454 deriving Functor
456-- Handy to get a free function for applying PTerm -> PTerm functions
457-- across a program, by deriving Functor
459type PDecl = PDecl' PTerm
460type PData = PData' PTerm
461type PClause = PClause' PTerm
463-- get all the names declared in a decl
465declared :: PDecl -> [Name]
466declared (PFix _ _ _) = []
467declared (PTy _ _ _ n t) = [n]
468declared (PClauses _ _ n _) = [] -- not a declaration
469declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
470 where fstt (a, _, _) = a
471declared (PParams _ _ ds) = concatMap declared ds
472declared (PNamespace _ ds) = concatMap declared ds
473-- declared (PImport _) = []
475defined :: PDecl -> [Name]
476defined (PFix _ _ _) = []
477defined (PTy _ _ _ n t) = []
478defined (PClauses _ _ n _) = [n] -- not a declaration
479defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
480 where fstt (a, _, _) = a
481defined (PParams _ _ ds) = concatMap defined ds
482defined (PNamespace _ ds) = concatMap defined ds
483-- declared (PImport _) = []
485updateN :: [(Name, Name)] -> Name -> Name
486updateN ns n | Just n' <- lookup n ns = n'
487updateN _ n = n
489updateNs :: [(Name, Name)] -> PTerm -> PTerm
490updateNs [] t = t
491updateNs ns t = mapPT updateRef t
492 where updateRef (PRef fc f) = PRef fc (updateN ns f)
493 updateRef t = t
495-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
496-- updateDNs [] t = t
497-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
498-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
499-- where updateCNs ns (PClause n l ts r ds)
500-- = PClause (updateN ns n) (fmap (updateNs ns) l)
501-- (map (fmap (updateNs ns)) ts)
502-- (fmap (updateNs ns) r)
503-- (map (updateDNs ns) ds)
504-- updateDNs ns c = c
506-- High level language terms
508data PTerm = PQuote Raw
509 | PRef FC Name
510 | PLam Name PTerm PTerm
511 | PPi Plicity Name PTerm PTerm
512 | PLet Name PTerm PTerm PTerm
513 | PTyped PTerm PTerm -- term with explicit type
514 | PApp FC PTerm [PArg]
515 | PCase FC PTerm [(PTerm, PTerm)]
516 | PTrue FC
517 | PFalse FC
518 | PRefl FC
519 | PResolveTC FC
520 | PEq FC PTerm PTerm
521 | PPair FC PTerm PTerm
522 | PDPair FC PTerm PTerm PTerm
523 | PAlternative [PTerm]
524 | PHidden PTerm -- irrelevant or hidden pattern
525 | PSet
526 | PConstant Const
527 | Placeholder
528 | PDoBlock [PDo]
529 | PIdiom FC PTerm
530 | PReturn FC
531 | PMetavar Name
532 | PProof [PTactic]
533 | PTactics [PTactic] -- as PProof, but no auto solving
534 | PElabError Err -- error to report on elaboration
535 | PImpossible -- special case for declaring when an LHS can't typecheck
536 deriving Eq
537{-!
538deriving instance Binary PTerm
539!-}
541mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
542mapPT f t = f (mpt t) where
543 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
544 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
545 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
546 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
547 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
548 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
549 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
550 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
551 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
552 mpt (PAlternative as) = PAlternative (map (mapPT f) as)
553 mpt (PHidden t) = PHidden (mapPT f t)
554 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
555 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
556 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
557 mpt x = x
560data PTactic' t = Intro [Name] | Intros | Focus Name
561 | Refine Name [Bool] | Rewrite t | LetTac Name t
562 | Exact t | Compute | Trivial
563 | Solve
564 | Attack
565 | ProofState | ProofTerm | Undo
566 | Try (PTactic' t) (PTactic' t)
567 | TSeq (PTactic' t) (PTactic' t)
568 | Qed | Abandon
569 deriving (Show, Eq, Functor)
570{-!
571deriving instance Binary PTactic'
572!-}
574type PTactic = PTactic' PTerm
576data PDo' t = DoExp FC t
577 | DoBind FC Name t
578 | DoBindP FC t t
579 | DoLet FC Name t t
580 | DoLetP FC t t
581 deriving (Eq, Functor)
582{-!
583deriving instance Binary PDo'
584!-}
586type PDo = PDo' PTerm
588-- The priority gives a hint as to elaboration order. Best to elaborate
589-- things early which will help give a more concrete type to other
590-- variables, e.g. a before (interpTy a).
592data PArg' t = PImp { priority :: Int,
593 lazyarg :: Bool, pname :: Name, getTm :: t }
594 | PExp { priority :: Int,
595 lazyarg :: Bool, getTm :: t }
596 | PConstraint { priority :: Int,
597 lazyarg :: Bool, getTm :: t }
598 | PTacImplicit { priority :: Int,
599 lazyarg :: Bool, pname :: Name,
600 getScript :: t,
601 getTm :: t }
602 deriving (Show, Eq, Functor)
603{-!
604deriving instance Binary PArg'
605!-}
607pimp = PImp 0 True
608pexp = PExp 0 False
609pconst = PConstraint 0 False
610ptacimp = PTacImplicit 0 True
612type PArg = PArg' PTerm
614-- Type class data
616data ClassInfo = CI { instanceName :: Name,
617 class_methods :: [(Name, (FnOpts, PTerm))],
618 class_defaults :: [(Name, Name)], -- method name -> default impl
619 class_params :: [Name],
620 class_instances :: [Name] }
621 deriving Show
622{-!
623deriving instance Binary ClassInfo
624!-}
626data OptInfo = Optimise { collapsible :: Bool,
627 forceable :: [Int], -- argument positions
628 recursive :: [Int] }
629 deriving Show
630{-!
631deriving instance Binary OptInfo
632!-}
635data TypeInfo = TI { con_names :: [Name] }
636 deriving Show
637{-!
638deriving instance Binary TypeInfo
639!-}
641-- Syntactic sugar info
643data DSL' t = DSL { dsl_bind :: t,
644 dsl_return :: t,
645 dsl_apply :: t,
646 dsl_pure :: t,
647 dsl_var :: Maybe t,
648 index_first :: Maybe t,
649 index_next :: Maybe t,
650 dsl_lambda :: Maybe t,
651 dsl_let :: Maybe t
652 }
653 deriving (Show, Functor)
654{-!
655deriving instance Binary DSL'
656!-}
658type DSL = DSL' PTerm
660data SynContext = PatternSyntax | TermSyntax | AnySyntax
661 deriving Show
662{-!
663deriving instance Binary SynContext
664!-}
666data Syntax = Rule [SSymbol] PTerm SynContext
667 deriving Show
668{-!
669deriving instance Binary Syntax
670!-}
672data SSymbol = Keyword Name
673 | Symbol String
674 | Expr Name
675 | SimpleExpr Name
676 deriving Show
677{-!
678deriving instance Binary SSymbol
679!-}
681initDSL = DSL (PRef f (UN ">>="))
682 (PRef f (UN "return"))
683 (PRef f (UN "<$>"))
684 (PRef f (UN "pure"))
685 Nothing
686 Nothing
687 Nothing
688 Nothing
689 Nothing
690 where f = FC "(builtin)" 0
692data SyntaxInfo = Syn { using :: [(Name, PTerm)],
693 syn_params :: [(Name, PTerm)],
694 syn_namespace :: [String],
695 no_imp :: [Name],
696 decoration :: Name -> Name,
697 inPattern :: Bool,
698 dsl_info :: DSL }
699 deriving Show
701defaultSyntax = Syn [] [] [] [] id False initDSL
703expandNS :: SyntaxInfo -> Name -> Name
704expandNS syn n@(NS _ _) = n
705expandNS syn n = case syn_namespace syn of
706 [] -> n
707 xs -> NS n xs
710--- Pretty printing declarations and terms
712instance Show PTerm where
713 show tm = showImp False tm
715instance Show PDecl where
716 show d = showDeclImp False d
718instance Show PClause where
719 show c = showCImp True c
721instance Show PData where
722 show d = showDImp False d
724showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
725showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty
726showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
727showDeclImp _ (PData _ _ d) = show d
729showCImp :: Bool -> PClause -> String
730showCImp impl (PClause _ n l ws r w)
731 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
732 ++ " where " ++ show w
733 where
734 showWs [] = ""
735 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
736showCImp impl (PWith _ n l ws r w)
737 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
738 ++ " { " ++ show w ++ " } "
739 where
740 showWs [] = ""
741 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
744showDImp :: Bool -> PData -> String
745showDImp impl (PDatadecl n ty cons)
746 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
747 ++ showSep "\n\t| "
748 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
750getImps :: [PArg] -> [(Name, PTerm)]
751getImps [] = []
752getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
753getImps (_ : xs) = getImps xs
755getExps :: [PArg] -> [PTerm]
756getExps [] = []
757getExps (PExp _ _ tm : xs) = tm : getExps xs
758getExps (_ : xs) = getExps xs
760getConsts :: [PArg] -> [PTerm]
761getConsts [] = []
762getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
763getConsts (_ : xs) = getConsts xs
765getAll :: [PArg] -> [PTerm]
766getAll = map getTm
768showImp :: Bool -> PTerm -> String
769showImp impl tm = se 10 tm where
770 se p (PQuote r) = "![" ++ show r ++ "]"
771 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
772 else showbasic n
773 where showbasic n@(UN _) = show n
774 showbasic (MN _ s) = s
775 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
776 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
777 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
778 " in " ++ se 10 sc
779 se p (PPi (Exp l s) n ty sc)
780 | n `elem` allNamesIn sc || impl
781 = bracket p 2 $
782 if l then "|(" else "(" ++
783 show n ++ " : " ++ se 10 ty ++
784 ") " ++ st ++
785 "-> " ++ se 10 sc
786 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
787 where st = case s of
788 Static -> "[static] "
789 _ -> ""
790 se p (PPi (Imp l s) n ty sc)
791 | impl = bracket p 2 $ if l then "|{" else "{" ++
792 show n ++ " : " ++ se 10 ty ++
793 "} " ++ st ++ "-> " ++ se 10 sc
794 | otherwise = se 10 sc
795 where st = case s of
796 Static -> "[static] "
797 _ -> ""
798 se p (PPi (Constraint _ _) n ty sc)
799 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
800 se p (PApp _ (PRef _ f) [])
801 | not impl = show f
802 se p (PApp _ (PRef _ op@(UN (f:_))) args)
803 | length (getExps args) == 2 && not impl && not (isAlpha f)
804 = let [l, r] = getExps args in
805 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
806 se p (PApp _ f as)
807 = let args = getExps as in
808 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
809 else concatMap seArg args
810 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
811 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
812 se p (PHidden tm) = "." ++ se 0 tm
813 se p (PRefl _) = "refl"
814 se p (PResolveTC _) = "resolvetc"
815 se p (PTrue _) = "()"
816 se p (PFalse _) = "_|_"
817 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
818 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
819 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
820 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
821 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
822 se p PSet = "Set"
823 se p (PConstant c) = show c
824 se p (PProof ts) = "proof { " ++ show ts ++ "}"
825 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
826 se p (PMetavar n) = "?" ++ show n
827 se p (PReturn f) = "return"
828 se p PImpossible = "impossible"
829 se p Placeholder = "_"
830 se p (PDoBlock _) = "do block show not implemented"
831 se p (PElabError s) = show s
832-- se p x = "Not implemented"
834 sArg (PImp _ _ n tm) = siArg (n, tm)
835 sArg (PExp _ _ tm) = seArg tm
836 sArg (PConstraint _ _ tm) = scArg tm
837 sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
839 seArg arg = " " ++ se 0 arg
840 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
841 scArg val = " {{" ++ se 10 val ++ "}}"
842 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
844 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
845 | otherwise = str
847allNamesIn :: PTerm -> [Name]
848allNamesIn tm = nub $ ni [] tm
849 where
850 ni env (PRef _ n)
851 | not (n `elem` env) = [n]
852 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
853 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
854 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
855 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
856 ni env (PHidden tm) = ni env tm
857 ni env (PEq _ l r) = ni env l ++ ni env r
858 ni env (PTyped l r) = ni env l ++ ni env r
859 ni env (PPair _ l r) = ni env l ++ ni env r
860 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
861 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
862 ni env (PAlternative ls) = concatMap (ni env) ls
863 ni env _ = []
865namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
866namesIn uvars ist tm = nub $ ni [] tm
867 where
868 ni env (PRef _ n)
869 | not (n `elem` env)
870 = case lookupTy Nothing n (tt_ctxt ist) of
871 [] -> [n]
872 _ -> if n `elem` (map fst uvars) then [n] else []
873 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
874 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
875 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
876 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
877 ni env (PEq _ l r) = ni env l ++ ni env r
878 ni env (PTyped l r) = ni env l ++ ni env r
879 ni env (PPair _ l r) = ni env l ++ ni env r
880 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
881 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
882 ni env (PAlternative as) = concatMap (ni env) as
883 ni env (PHidden tm) = ni env tm
884 ni env _ = []
886-- For inferring types of things
888bi = FC "builtin" 0
890inferTy = MN 0 "__Infer"
891inferCon = MN 0 "__infer"
892inferDecl = PDatadecl inferTy
893 PSet
894 [(inferCon, PPi impl (MN 0 "A") PSet (
895 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
896 (PRef bi inferTy)), bi)]
898infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
899infP = P (TCon 6 0) inferTy (Set (UVal 0))
901getInferTerm, getInferType :: Term -> Term
902getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
903getInferTerm (App (App _ _) tm) = tm
904getInferTerm tm = error ("getInferTerm " ++ show tm)
906getInferType (Bind n b sc) = Bind n b $ getInferType sc
907getInferType (App (App _ ty) _) = ty
909-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
911primNames = [unitTy, unitCon,
912 falseTy, pairTy, pairCon,
913 eqTy, eqCon, inferTy, inferCon]
915unitTy = MN 0 "__Unit"
916unitCon = MN 0 "__II"
917unitDecl = PDatadecl unitTy PSet
918 [(unitCon, PRef bi unitTy, bi)]
920falseTy = MN 0 "__False"
921falseDecl = PDatadecl falseTy PSet []
923pairTy = MN 0 "__Pair"
924pairCon = MN 0 "__MkPair"
925pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
926 [(pairCon, PPi impl (n "A") PSet (
927 PPi impl (n "B") PSet (
928 PPi expl (n "a") (PRef bi (n "A")) (
929 PPi expl (n "b") (PRef bi (n "B"))
930 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
931 pexp (PRef bi (n "B"))])))), bi)]
932 where n a = MN 0 a
934eqTy = UN "="
935eqCon = UN "refl"
936eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
937 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
938 PSet)
939 [(eqCon, PPi impl (n "a") PSet (
940 PPi impl (n "x") (PRef bi (n "a"))
941 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
942 pimp (n "b") Placeholder,
943 pexp (PRef bi (n "x")),
944 pexp (PRef bi (n "x"))])), bi)]
945 where n a = MN 0 a
947-- Defined in builtins.idr
948sigmaTy = UN "Exists"
949existsCon = UN "Ex_intro"
951piBind :: [(Name, PTerm)] -> PTerm -> PTerm
952piBind [] t = t
953piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
955tcname (UN ('@':_)) = True
956tcname (NS n _) = tcname n
957tcname _ = False
959-- Dealing with parameters
961expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
962expandParams dec ps ns tm = en tm
963 where
964 -- if we shadow a name (say in a lambda binding) that is used in a call to
965 -- a lifted function, we need access to both names - once in the scope of the
966 -- binding and once to call the lifted functions. So we'll explicitly shadow
967 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
968 -- but we didn't...)
970 mkShadow (UN n) = MN 0 n
971 mkShadow (MN i n) = MN (i+1) n
972 mkShadow (NS x s) = NS (mkShadow x) s
974 en (PLam n t s)
975 | n `elem` map fst ps
976 = let n' = mkShadow n in
977 PLam n' (en t) (en (shadow n n' s))
978 | otherwise = PLam n (en t) (en s)
979 en (PPi p n t s)
980 | n `elem` map fst ps
981 = let n' = mkShadow n in
982 PPi p n' (en t) (en (shadow n n' s))
983 | otherwise = PPi p n (en t) (en s)
984 en (PLet n ty v s)
985 | n `elem` map fst ps
986 = let n' = mkShadow n in
987 PLet n' (en ty) (en v) (en (shadow n n' s))
988 | otherwise = PLet n (en ty) (en v) (en s)
989 en (PEq f l r) = PEq f (en l) (en r)
990 en (PTyped l r) = PTyped (en l) (en r)
991 en (PPair f l r) = PPair f (en l) (en r)
992 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
993 en (PAlternative as) = PAlternative (map en as)
994 en (PHidden t) = PHidden (en t)
995 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
996 en (PProof ts) = PProof (map (fmap en) ts)
997 en (PTactics ts) = PTactics (map (fmap en) ts)
999 en (PQuote (Var n))
1000 | n `elem` ns = PQuote (Var (dec n))
1001 en (PApp fc (PRef fc' n) as)
1002 | n `elem` ns = PApp fc (PRef fc' (dec n))
1003 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1004 en (PRef fc n)
1005 | n `elem` ns = PApp fc (PRef fc (dec n))
1006 (map (pexp . (PRef fc)) (map fst ps))
1007 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1008 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1009 en t = t
1011expandParamsD :: IState ->
1012 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1013expandParamsD ist dec ps ns (PTy syn fc o n ty)
1014 = if n `elem` ns
1015 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
1016 else PTy syn fc o n (expandParams dec ps ns ty)
1017expandParamsD ist dec ps ns (PClauses fc opts n cs)
1018 = let n' = if n `elem` ns then dec n else n in
1019 PClauses fc opts n' (map expandParamsC cs)
1020 where
1021 expandParamsC (PClause fc n lhs ws rhs ds)
1022 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1023 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1024 n' = if n `elem` ns then dec n else n in
1025 PClause fc n' (expandParams dec ps'' ns lhs)
1026 (map (expandParams dec ps'' ns) ws)
1027 (expandParams dec ps'' ns rhs)
1028 (map (expandParamsD ist dec ps'' ns) ds)
1029 expandParamsC (PWith fc n lhs ws wval ds)
1030 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1031 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1032 n' = if n `elem` ns then dec n else n in
1033 PWith fc n' (expandParams dec ps'' ns lhs)
1034 (map (expandParams dec ps'' ns) ws)
1035 (expandParams dec ps'' ns wval)
1036 (map (expandParamsD ist dec ps'' ns) ds)
1037 updateps yn nm [] = []
1038 updateps yn nm (((a, t), i):as)
1039 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1040 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
1042expandParamsD ist dec ps ns d = d
1044-- Calculate a priority for a type, for deciding elaboration order
1045-- * if it's just a type variable or concrete type, do it early (0)
1046-- * if there's only type variables and injective constructors, do it next (1)
1047-- * if there's a function type, next (2)
1048-- * finally, everything else (3)
1050getPriority :: IState -> PTerm -> Int
1051getPriority i tm = pri tm
1052 where
1053 pri (PRef _ n) =
1054 case lookupP Nothing n (tt_ctxt i) of
1055 ((P (DCon _ _) _ _):_) -> 1
1056 ((P (TCon _ _) _ _):_) -> 1
1057 ((P Ref _ _):_) -> 4
1058 [] -> 0 -- must be locally bound, if it's not an error...
1059 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1060 pri (PTrue _) = 0
1061 pri (PFalse _) = 0
1062 pri (PRefl _) = 1
1063 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1064 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1065 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1066 pri (PTyped l r) = pri l
1067 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
1068 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1069 pri (PAlternative as) = maximum (map pri as)
1070 pri (PConstant _) = 0
1071 pri Placeholder = 1
1072 pri _ = 3
1074addStatics :: Name -> Term -> PTerm -> Idris ()
1075addStatics n tm ptm =
1076 do let (statics, dynamics) = initStatics tm ptm
1077 let stnames = nub $ concatMap freeNames (map snd statics)
1078 let dnames = nub $ concatMap freeNames (map snd dynamics)
1079 when (not (null statics)) $
1080 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
1081 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1082 let statics' = nub $ map fst statics ++
1083 filter (\x -> not (elem x dnames)) stnames
1084 let stpos = staticList statics' tm
1085 i <- get
1086 put (i { idris_statics = addDef n stpos (idris_statics i) })
1087 addIBC (IBCStatic n)
1088 where
1089 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1090 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1091 if pstatic p == Static then ((n, ty) : static, dynamic)
1092 else (static, (n, ty) : dynamic)
1093 initStatics t pt = ([], [])
1095 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1096 staticList _ _ = []
1098-- Dealing with implicit arguments
1100-- Add implicit Pi bindings for any names in the term which appear in an
1101-- argument position.
1103-- This has become a right mess already. Better redo it some time...
1105implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1106implicit syn n ptm
1107 = do i <- get
1108 let (tm', impdata) = implicitise syn i ptm
1109-- let (tm'', spos) = findStatics i tm'
1110 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
1111 addIBC (IBCImp n)
1112 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1113-- i <- get
1114-- put (i { idris_statics = addDef n spos (idris_statics i) })
1115 return tm'
1117implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
1118implicitise syn ist tm
1119 = let (declimps, ns') = execState (imps True [] tm) ([], [])
1120 ns = ns' \\ (map fst pvars ++ no_imp syn) in
1121 if null ns
1122 then (tm, reverse declimps)
1123 else implicitise syn ist (pibind uvars ns tm)
1124 where
1125 uvars = using syn
1126 pvars = syn_params syn
1128 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1129 | otherwise = x : dropAll xs ys
1130 dropAll [] ys = []
1132 imps top env (PApp _ f as)
1133 = do (decls, ns) <- get
1134 let isn = concatMap (namesIn uvars ist) (map getTm as)
1135 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1136 imps top env (PPi (Imp l _) n ty sc)
1137 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1138 (decls , ns) <- get
1139 put (PImp (getPriority ist ty) l n ty : decls,
1140 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1141 imps True (n:env) sc
1142 imps top env (PPi (Exp l _) n ty sc)
1143 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1144 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1145 _ -> [])
1146 (decls, ns) <- get -- ignore decls in HO types
1147 put (PExp (getPriority ist ty) l ty : decls,
1148 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1149 imps True (n:env) sc
1150 imps top env (PPi (Constraint l _) n ty sc)
1151 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1152 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1153 _ -> [])
1154 (decls, ns) <- get -- ignore decls in HO types
1155 put (PConstraint 10 l ty : decls,
1156 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1157 imps True (n:env) sc
1158 imps top env (PPi (TacImp l _ scr) n ty sc)
1159 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1160 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1161 _ -> [])
1162 (decls, ns) <- get -- ignore decls in HO types
1163 put (PTacImplicit 10 l n scr ty : decls,
1164 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1165 imps True (n:env) sc
1166 imps top env (PEq _ l r)
1167 = do (decls, ns) <- get
1168 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1169 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1170 imps top env (PTyped l r)
1171 = imps top env l
1172 imps top env (PPair _ l r)
1173 = do (decls, ns) <- get
1174 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1175 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1176 imps top env (PDPair _ (PRef _ n) t r)
1177 = do (decls, ns) <- get
1178 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1179 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1180 imps top env (PDPair _ l t r)
1181 = do (decls, ns) <- get
1182 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1183 namesIn uvars ist r
1184 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1185 imps top env (PAlternative as)
1186 = do (decls, ns) <- get
1187 let isn = concatMap (namesIn uvars ist) as
1188 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1189 imps top env (PLam n ty sc)
1190 = do imps False env ty
1191 imps False (n:env) sc
1192 imps top env (PHidden tm) = imps False env tm
1193 imps top env _ = return ()
1195 pibind using [] sc = sc
1196 pibind using (n:ns) sc
1197 = case lookup n using of
1198 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
1199 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
1201-- Add implicit arguments in function calls
1202addImplPat :: IState -> PTerm -> PTerm
1203addImplPat = addImpl' True []
1205addImplBound :: IState -> [Name] -> PTerm -> PTerm
1206addImplBound ist ns = addImpl' False ns ist
1208addImpl :: IState -> PTerm -> PTerm
1209addImpl = addImpl' False []
1211-- TODO: in patterns, don't add implicits to function names guarded by constructors
1212-- and *not* inside a PHidden
1214addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1215addImpl' inpat env ist ptm = ai env ptm
1216 where
1217 ai env (PRef fc f)
1218 | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []
1219 ai env (PHidden (PRef fc f))
1220 | not (f `elem` env) = handleErr $ aiFn False ist fc f []
1221 ai env (PEq fc l r) = let l' = ai env l
1222 r' = ai env r in
1223 PEq fc l' r'
1224 ai env (PTyped l r) = let l' = ai env l
1225 r' = ai env r in
1226 PTyped l' r'
1227 ai env (PPair fc l r) = let l' = ai env l
1228 r' = ai env r in
1229 PPair fc l' r'
1230 ai env (PDPair fc l t r) = let l' = ai env l
1231 t' = ai env t
1232 r' = ai env r in
1233 PDPair fc l' t' r'
1234 ai env (PAlternative as) = let as' = map (ai env) as in
1235 PAlternative as'
1236 ai env (PApp fc (PRef _ f) as)
1237 | not (f `elem` env)
1238 = let as' = map (fmap (ai env)) as in
1239 handleErr $ aiFn False ist fc f as'
1240 ai env (PApp fc f as) = let f' = ai env f
1241 as' = map (fmap (ai env)) as in
1242 mkPApp fc 1 f' as'
1243 ai env (PCase fc c os) = let c' = ai env c
1244 os' = map (pmap (ai env)) os in
1245 PCase fc c' os'
1246 ai env (PLam n ty sc) = let ty' = ai env ty
1247 sc' = ai (n:env) sc in
1248 PLam n ty' sc'
1249 ai env (PLet n ty val sc)
1250 = let ty' = ai env ty
1251 val' = ai env val
1252 sc' = ai (n:env) sc in
1253 PLet n ty' val' sc'
1254 ai env (PPi p n ty sc) = let ty' = ai env ty
1255 sc' = ai (n:env) sc in
1256 PPi p n ty' sc'
1257 ai env (PHidden tm) = PHidden (ai env tm)
1258 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1259 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1260 ai env tm = tm
1262 handleErr (Left err) = PElabError err
1263 handleErr (Right x) = x
1265-- if in a pattern, and there are no arguments, and there's no possible
1266-- names with zero explicit arguments, don't add implicits.
1268aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1269aiFn True ist fc f []
1270 = case lookupCtxt Nothing f (idris_implicits ist) of
1271 [] -> Right $ PRef fc f
1272 alts -> if (any (all imp) alts)
1273 then aiFn False ist fc f [] -- use it as a constructor
1274 else Right $ PRef fc f
1275 where imp (PExp _ _ _) = False
1276 imp _ = True
1277aiFn inpat ist fc f as
1278 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1279aiFn inpat ist fc f as
1280 -- This is where namespaces get resolved by adding PAlternative
1281 = case lookupCtxtName Nothing f (idris_implicits ist) of
1282 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1283 [] -> if f `elem` idris_metavars ist
1284 then Right $ PApp fc (PRef fc f) as
1285 else Right $ mkPApp fc (length as) (PRef fc f) as
1286 alts -> Right $
1287 PAlternative $
1288 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1289 (insertImpl ns as)) alts
1290 where
1291 insertImpl :: [PArg] -> [PArg] -> [PArg]
1292 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1293 PExp p l tm : insertImpl ps given
1294 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1295 PConstraint p l tm : insertImpl ps given
1296 insertImpl (PConstraint p l ty : ps) given =
1297 PConstraint p l (PResolveTC fc) : insertImpl ps given
1298 insertImpl (PImp p l n ty : ps) given =
1299 case find n given [] of
1300 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
1301 Nothing -> PImp p l n Placeholder : insertImpl ps given
1302 insertImpl (PTacImplicit p l n sc ty : ps) given =
1303 case find n given [] of
1304 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1305 Nothing -> PTacImplicit p l n sc sc
1306 : insertImpl ps given
1307 insertImpl expected [] = []
1308 insertImpl _ given = given
1310 find n [] acc = Nothing
1311 find n (PImp _ _ n' t : gs) acc
1312 | n == n' = Just (t, reverse acc ++ gs)
1313 find n (g : gs) acc = find n gs (g : acc)
1315mkPApp fc a f [] = f
1316mkPApp fc a f as = let rest = drop a as in
1317 appRest fc (PApp fc f (take a as)) rest
1318 where
1319 appRest fc f [] = f
1320 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1322-- Find 'static' argument positions
1323-- (the declared ones, plus any names in argument position in the declared
1324-- statics)
1325-- FIXME: It's possible that this really has to happen after elaboration
1327findStatics :: IState -> PTerm -> (PTerm, [Bool])
1328findStatics ist tm = trace (showImp True tm) $
1329 let (ns, ss) = fs tm in
1330 runState (pos ns ss tm) []
1331 where fs (PPi p n t sc)
1332 | Static <- pstatic p
1333 = let (ns, ss) = fs sc in
1334 (namesIn [] ist t : ns, n : ss)
1335 | otherwise = let (ns, ss) = fs sc in
1336 (ns, ss)
1337 fs _ = ([], [])
1339 inOne n ns = length (filter id (map (elem n) ns)) == 1
1341 pos ns ss (PPi p n t sc)
1342 | elem n ss = do sc' <- pos ns ss sc
1343 spos <- get
1344 put (True : spos)
1345 return (PPi (p { pstatic = Static }) n t sc')
1346 | otherwise = do sc' <- pos ns ss sc
1347 spos <- get
1348 put (False : spos)
1349 return (PPi p n t sc')
1350 pos ns ss t = return t
1352-- Debugging/logging stuff
1354dumpDecls :: [PDecl] -> String
1355dumpDecls [] = ""
1356dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1358dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1359dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1360dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1361dumpDecl (PData _ _ d) = showDImp True d
1362dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1363dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1364dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1365dumpDecl (PClass _ _ cs n ps ds)
1366 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1367dumpDecl (PInstance _ _ cs n _ t ds)
1368 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1369dumpDecl _ = "..."
1370-- dumpDecl (PImport i) = "import " ++ i
1372-- for 6.12/7 compatibility
1373data EitherErr a b = LeftErr a | RightOK b
1375instance Monad (EitherErr a) where
1376 return = RightOK
1378 (LeftErr e) >>= k = LeftErr e
1379 RightOK v >>= k = k v
1381toEither (LeftErr e) = Left e
1382toEither (RightOK ho) = Right ho
1384-- syntactic match of a against b, returning pair of variables in a
1385-- and what they match. Returns the pair that failed if not a match.
1387matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1388matchClause = matchClause' False
1390matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1391matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1392 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1394 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1395 fullApp x = x
1397 match' x y = match (fullApp x) (fullApp y)
1398 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1399 | PConstant (I _) <- getTm x = match (getTm x) x'
1400 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1401 | PConstant (I _) <- getTm x = match (getTm x) x'
1402 match (PApp _ f args) (PApp _ f' args')
1403 | length args == length args'
1404 = do mf <- match' f f'
1405 ms <- zipWithM matchArg args args'
1406 return (mf ++ concat ms)
1407-- match (PRef _ n) (PRef _ n') | n == n' = return []
1408-- | otherwise = Nothing
1409 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1410 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1411 match (PRef _ n) (PRef _ n') | n == n' = return []
1412 match (PRef _ n) tm
1413 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1414 = return [(n, tm)]
1415 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1416 mr <- match' r r'
1417 return (ml ++ mr)
1418 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1419 mr <- match r r'
1420 return (ml ++ mr)
1421 match (PTyped l r) x = match l x
1422 match x (PTyped l r) = match x l
1423 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1424 mr <- match' r r'
1425 return (ml ++ mr)
1426 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1427 mt <- match' t t'
1428 mr <- match' r r'
1429 return (ml ++ mt ++ mr)
1430 match (PAlternative as) (PAlternative as')
1431 = do ms <- zipWithM match' as as'
1432 return (concat ms)
1433 match a@(PAlternative as) b
1434 = do let ms = zipWith match' as (repeat b)
1435 case (rights (map toEither ms)) of
1436 (x: _) -> return x
1437 _ -> LeftErr (a, b)
1438 match (PCase _ _ _) _ = return [] -- lifted out
1439 match (PMetavar _) _ = return [] -- modified
1440 match (PQuote _) _ = return []
1441 match (PProof _) _ = return []
1442 match (PTactics _) _ = return []
1443 match (PRefl _) (PRefl _) = return []
1444 match (PResolveTC _) (PResolveTC _) = return []
1445 match (PTrue _) (PTrue _) = return []
1446 match (PFalse _) (PFalse _) = return []
1447 match (PReturn _) (PReturn _) = return []
1448 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1449 ms <- match' s s'
1450 return (mt ++ ms)
1451 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1452 ms <- match' s s'
1453 return (mt ++ ms)
1454 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1455 mty <- match' ty ty'
1456 ms <- match' s s'
1457 return (mt ++ mty ++ ms)
1458 match (PHidden x) (PHidden y) = match' x y
1459 match Placeholder _ = return []
1460-- match _ Placeholder = return []
1461 match (PResolveTC _) _ = return []
1462 match a b | a == b = return []
1463 | otherwise = LeftErr (a, b)
1465 checkRpts (RightOK ms) = check ms where
1466 check ((n,t):xs)
1467 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1468 then Left (t, t')
1469 else check xs
1470 check (_:xs) = check xs
1471 check [] = Right ms
1472 checkRpts (LeftErr x) = Left x
1474substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1475substMatches [] t = t
1476substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1478substMatch :: Name -> PTerm -> PTerm -> PTerm
1479substMatch n tm t = sm t where
1480 sm (PRef _ n') | n == n' = tm
1481 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1482 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1483 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1484 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1485 sm (PEq f x y) = PEq f (sm x) (sm y)
1486 sm (PTyped x y) = PTyped (sm x) (sm y)
1487 sm (PPair f x y) = PPair f (sm x) (sm y)
1488 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1489 sm (PAlternative as) = PAlternative (map sm as)
1490 sm (PHidden x) = PHidden (sm x)
1491 sm x = x
1493shadow :: Name -> Name -> PTerm -> PTerm
1494shadow n n' t = sm t where
1495 sm (PRef fc x) | n == x = PRef fc n'
1496 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1497 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1498 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1499 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1500 sm (PEq f x y) = PEq f (sm x) (sm y)
1501 sm (PTyped x y) = PTyped (sm x) (sm y)
1502 sm (PPair f x y) = PPair f (sm x) (sm y)
1503 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1504 sm (PAlternative as) = PAlternative (map sm as)
1505 sm (PHidden x) = PHidden (sm x)
1506 sm x = x