git.iko.soy/Idris-dev
on 3c42704 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1396 lines 53 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_log :: String,
50 idris_options :: IOption,
51 idris_name :: Int,
52 idris_metavars :: [Name],
53 syntax_rules :: [Syntax],
54 syntax_keywords :: [String],
55 imported :: [FilePath],
56 idris_prims :: [(Name, ([E.Name], E.Term))],
57 idris_objs :: [FilePath],
58 idris_libs :: [String],
59 idris_hdrs :: [String],
60 last_proof :: Maybe (Name, [String]),
61 errLine :: Maybe Int,
62 lastParse :: Maybe Name,
63 indent_stack :: [Int],
64 brace_stack :: [Maybe Int],
65 hide_list :: [(Name, Maybe Accessibility)],
66 default_access :: Accessibility,
67 ibc_write :: [IBCWrite],
68 compiled_so :: Maybe String
69 }
71-- information that needs writing for the current module's .ibc file
72data IBCWrite = IBCFix FixDecl
73 | IBCImp Name
74 | IBCStatic Name
75 | IBCClass Name
76 | IBCDSL Name
77 | IBCData Name
78 | IBCOpt Name
79 | IBCSyntax Syntax
80 | IBCKeyword String
81 | IBCImport FilePath
82 | IBCObj FilePath
83 | IBCLib String
84 | IBCHeader String
85 | IBCAccess Name Accessibility
86 | IBCTotal Name Totality
87 | IBCFlags Name [FnOpt]
88 | IBCCG Name
89 | IBCDef Name -- i.e. main context
90 deriving Show
92idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
93 emptyContext emptyContext emptyContext emptyContext
94 emptyContext emptyContext
95 "" defaultOpts 6 [] [] [] [] [] [] [] []
96 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
98-- The monad for the main REPL - reading and processing files and updating
99-- global state (hence the IO inner monad).
100type Idris = StateT IState (InputT IO)
102getContext :: Idris Context
103getContext = do i <- get; return (tt_ctxt i)
105getObjectFiles :: Idris [FilePath]
106getObjectFiles = do i <- get; return (idris_objs i)
108addObjectFile :: FilePath -> Idris ()
109addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
111getLibs :: Idris [String]
112getLibs = do i <- get; return (idris_libs i)
114addLib :: String -> Idris ()
115addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
117addHdr :: String -> Idris ()
118addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
120setFlags :: Name -> [FnOpt] -> Idris ()
121setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
123setAccessibility :: Name -> Accessibility -> Idris ()
124setAccessibility n a
125 = do i <- get
126 let ctxt = setAccess n a (tt_ctxt i)
127 put (i { tt_ctxt = ctxt })
129setTotality :: Name -> Totality -> Idris ()
130setTotality n a
131 = do i <- get
132 let ctxt = setTotal n a (tt_ctxt i)
133 put (i { tt_ctxt = ctxt })
135addToCG :: Name -> [Name] -> Idris ()
136addToCG n ns = do i <- get
137 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
139addIBC :: IBCWrite -> Idris ()
140addIBC ibc@(IBCDef n)
141 = do i <- get
142 when (notDef (ibc_write i)) $
143 put (i { ibc_write = ibc : ibc_write i })
144 where notDef [] = True
145 notDef (IBCDef n': is) | n == n' = False
146 notDef (_ : is) = notDef is
147addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
149clearIBC :: Idris ()
150clearIBC = do i <- get; put (i { ibc_write = [] })
152getHdrs :: Idris [String]
153getHdrs = do i <- get; return (idris_hdrs i)
155setErrLine :: Int -> Idris ()
156setErrLine x = do i <- get;
157 case (errLine i) of
158 Nothing -> put (i { errLine = Just x })
159 Just _ -> return ()
161clearErr :: Idris ()
162clearErr = do i <- get
163 put (i { errLine = Nothing })
165getSO :: Idris (Maybe String)
166getSO = do i <- get
167 return (compiled_so i)
169setSO :: Maybe String -> Idris ()
170setSO s = do i <- get
171 put (i { compiled_so = s })
173getIState :: Idris IState
174getIState = get
176putIState :: IState -> Idris ()
177putIState = put
179getName :: Idris Int
180getName = do i <- get;
181 let idx = idris_name i;
182 put (i { idris_name = idx + 1 })
183 return idx
185checkUndefined :: FC -> Name -> Idris ()
186checkUndefined fc n
187 = do i <- getContext
188 case lookupTy Nothing n i of
189 (_:_) -> fail $ show fc ++ ":" ++
190 show n ++ " already defined"
191 _ -> return ()
193setContext :: Context -> Idris ()
194setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
196updateContext :: (Context -> Context) -> Idris ()
197updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
199addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
200addConstraints fc (v, cs)
201 = do i <- get
202 let ctxt = tt_ctxt i
203 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
204 next_tvar = v }
205 let ics = zip cs (repeat fc) ++ idris_constraints i
206 put (i { tt_ctxt = ctxt', idris_constraints = ics })
208addDeferred :: [(Name, Type)] -> Idris ()
209addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
210 i <- get
211 put (i { idris_metavars = map fst ns ++ idris_metavars i })
212 where tidyNames used (Bind (MN i x) b sc)
213 = let n' = uniqueName (UN x) used in
214 Bind n' b $ tidyNames (n':used) sc
215 tidyNames used (Bind n b sc)
216 = let n' = uniqueName n used in
217 Bind n' b $ tidyNames (n':used) sc
218 tidyNames used b = b
220solveDeferred :: Name -> Idris ()
221solveDeferred n = do i <- get
222 put (i { idris_metavars = idris_metavars i \\ [n] })
224iputStrLn :: String -> Idris ()
225iputStrLn = liftIO . putStrLn
227iWarn :: FC -> String -> Idris ()
228iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
230setLogLevel :: Int -> Idris ()
231setLogLevel l = do i <- get
232 let opts = idris_options i
233 let opt' = opts { opt_logLevel = l }
234 put (i { idris_options = opt' } )
236logLevel :: Idris Int
237logLevel = do i <- get
238 return (opt_logLevel (idris_options i))
240useREPL :: Idris Bool
241useREPL = do i <- get
242 return (opt_repl (idris_options i))
244setREPL :: Bool -> Idris ()
245setREPL t = do i <- get
246 let opts = idris_options i
247 let opt' = opts { opt_repl = t }
248 put (i { idris_options = opt' })
250verbose :: Idris Bool
251verbose = do i <- get
252 return (opt_verbose (idris_options i))
254setVerbose :: Bool -> Idris ()
255setVerbose t = do i <- get
256 let opts = idris_options i
257 let opt' = opts { opt_verbose = t }
258 put (i { idris_options = opt' })
260typeInType :: Idris Bool
261typeInType = do i <- get
262 return (opt_typeintype (idris_options i))
264setTypeInType :: Bool -> Idris ()
265setTypeInType t = do i <- get
266 let opts = idris_options i
267 let opt' = opts { opt_typeintype = t }
268 put (i { idris_options = opt' })
270coverage :: Idris Bool
271coverage = do i <- get
272 return (opt_coverage (idris_options i))
274setCoverage :: Bool -> Idris ()
275setCoverage t = do i <- get
276 let opts = idris_options i
277 let opt' = opts { opt_coverage = t }
278 put (i { idris_options = opt' })
280impShow :: Idris Bool
281impShow = do i <- get
282 return (opt_showimp (idris_options i))
284setImpShow :: Bool -> Idris ()
285setImpShow t = do i <- get
286 let opts = idris_options i
287 let opt' = opts { opt_showimp = t }
288 put (i { idris_options = opt' })
290logLvl :: Int -> String -> Idris ()
291logLvl l str = do i <- get
292 let lvl = opt_logLevel (idris_options i)
293 when (lvl >= l)
294 $ do liftIO (putStrLn str)
295 put (i { idris_log = idris_log i ++ str ++ "\n" } )
297iLOG :: String -> Idris ()
298iLOG = logLvl 1
300noErrors :: Idris Bool
301noErrors = do i <- get
302 case errLine i of
303 Nothing -> return True
304 _ -> return False
306setTypeCase :: Bool -> Idris ()
307setTypeCase t = do i <- get
308 let opts = idris_options i
309 let opt' = opts { opt_typecase = t }
310 put (i { idris_options = opt' })
312-- Commands in the REPL
314data Command = Quit | Help | Eval PTerm | Check PTerm | Reload | Edit
315 | Compile String | Execute | ExecVal PTerm
316 | Metavars | Prove Name | AddProof | Universes
317 | TTShell
318 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name | Info Name
319 | NOP
321-- Parsed declarations
323data Fixity = Infixl { prec :: Int }
324 | Infixr { prec :: Int }
325 | InfixN { prec :: Int }
326 | PrefixN { prec :: Int }
327 deriving Eq
328{-!
329deriving instance Binary Fixity
330!-}
332instance Show Fixity where
333 show (Infixl i) = "infixl " ++ show i
334 show (Infixr i) = "infixr " ++ show i
335 show (InfixN i) = "infix " ++ show i
336 show (PrefixN i) = "prefix " ++ show i
338data FixDecl = Fix Fixity String
339 deriving (Show, Eq)
340{-!
341deriving instance Binary FixDecl
342!-}
344instance Ord FixDecl where
345 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
348data Static = Static | Dynamic
349 deriving (Show, Eq)
350{-!
351deriving instance Binary Static
352!-}
354-- Mark bindings with their explicitness, and laziness
355data Plicity = Imp { plazy :: Bool,
356 pstatic :: Static }
357 | Exp { plazy :: Bool,
358 pstatic :: Static }
359 | Constraint { plazy :: Bool,
360 pstatic :: Static }
361 | TacImp { plazy :: Bool,
362 pstatic :: Static,
363 pscript :: PTerm }
364 deriving (Show, Eq)
366{-!
367deriving instance Binary Plicity
368!-}
370impl = Imp False Dynamic
371expl = Exp False Dynamic
372constraint = Constraint False Static
373tacimpl = TacImp False Dynamic
375data FnOpt = Inlinable | TotalFn | TCGen
376 deriving (Show, Eq)
377{-!
378deriving instance Binary FnOpt
379!-}
381type FnOpts = [FnOpt]
383inlinable :: FnOpts -> Bool
384inlinable = elem Inlinable
386data PDecl' t = PFix FC Fixity [String] -- fixity declaration
387 | PTy SyntaxInfo FC FnOpts Name t -- type declaration
388 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
389 | PData SyntaxInfo FC (PData' t) -- data declaration
390 | PParams FC [(Name, t)] [PDecl' t] -- params block
391 | PNamespace String [PDecl' t] -- new namespace
392 | PRecord SyntaxInfo FC Name t Name t -- record declaration
393 | PClass SyntaxInfo FC
394 [t] -- constraints
395 Name
396 [(Name, t)] -- parameters
397 [PDecl' t] -- declarations
398 | PInstance SyntaxInfo FC [t] -- constraints
399 Name -- class
400 [t] -- parameters
401 t -- full instance type
402 [PDecl' t]
403 | PDSL Name (DSL' t)
404 | PSyntax FC Syntax
405 | PDirective (Idris ())
406 deriving Functor
408data PClause' t = PClause Name t [t] t [PDecl' t]
409 | PWith Name t [t] t [PDecl' t]
410 | PClauseR [t] t [PDecl' t]
411 | PWithR [t] t [PDecl' t]
412 deriving Functor
414data PData' t = PDatadecl { d_name :: Name,
415 d_tcon :: t,
416 d_cons :: [(Name, t, FC)] }
417 deriving Functor
419-- Handy to get a free function for applying PTerm -> PTerm functions
420-- across a program, by deriving Functor
422type PDecl = PDecl' PTerm
423type PData = PData' PTerm
424type PClause = PClause' PTerm
426-- get all the names declared in a decl
428declared :: PDecl -> [Name]
429declared (PFix _ _ _) = []
430declared (PTy _ _ _ n t) = [n]
431declared (PClauses _ _ n _) = [] -- not a declaration
432declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
433 where fstt (a, _, _) = a
434declared (PParams _ _ ds) = concatMap declared ds
435declared (PNamespace _ ds) = concatMap declared ds
436-- declared (PImport _) = []
438updateN :: [(Name, Name)] -> Name -> Name
439updateN ns n | Just n' <- lookup n ns = n'
440updateN _ n = n
442updateNs :: [(Name, Name)] -> PTerm -> PTerm
443updateNs [] t = t
444updateNs ns t = mapPT updateRef t
445 where updateRef (PRef fc f) = PRef fc (updateN ns f)
446 updateRef t = t
448-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
449-- updateDNs [] t = t
450-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
451-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
452-- where updateCNs ns (PClause n l ts r ds)
453-- = PClause (updateN ns n) (fmap (updateNs ns) l)
454-- (map (fmap (updateNs ns)) ts)
455-- (fmap (updateNs ns) r)
456-- (map (updateDNs ns) ds)
457-- updateDNs ns c = c
459-- High level language terms
461data PTerm = PQuote Raw
462 | PRef FC Name
463 | PLam Name PTerm PTerm
464 | PPi Plicity Name PTerm PTerm
465 | PLet Name PTerm PTerm PTerm
466 | PTyped PTerm PTerm -- term with explicit type
467 | PApp FC PTerm [PArg]
468 | PCase FC PTerm [(PTerm, PTerm)]
469 | PTrue FC
470 | PFalse FC
471 | PRefl FC
472 | PResolveTC FC
473 | PEq FC PTerm PTerm
474 | PPair FC PTerm PTerm
475 | PDPair FC PTerm PTerm PTerm
476 | PAlternative [PTerm]
477 | PHidden PTerm -- irrelevant or hidden pattern
478 | PSet
479 | PConstant Const
480 | Placeholder
481 | PDoBlock [PDo]
482 | PIdiom FC PTerm
483 | PReturn FC
484 | PMetavar Name
485 | PProof [PTactic]
486 | PTactics [PTactic] -- as PProof, but no auto solving
487 | PElabError String -- error to report on elaboration
488 | PImpossible -- special case for declaring when an LHS can't typecheck
489 deriving Eq
490{-!
491deriving instance Binary PTerm
492!-}
494mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
495mapPT f t = f (mpt t) where
496 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
497 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
498 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
499 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
500 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
501 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
502 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
503 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
504 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
505 mpt (PAlternative as) = PAlternative (map (mapPT f) as)
506 mpt (PHidden t) = PHidden (mapPT f t)
507 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
508 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
509 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
510 mpt x = x
513data PTactic' t = Intro [Name] | Intros | Focus Name
514 | Refine Name [Bool] | Rewrite t | LetTac Name t
515 | Exact t | Compute | Trivial
516 | Solve
517 | Attack
518 | ProofState | ProofTerm | Undo
519 | Try (PTactic' t) (PTactic' t)
520 | TSeq (PTactic' t) (PTactic' t)
521 | Qed | Abandon
522 deriving (Show, Eq, Functor)
523{-!
524deriving instance Binary PTactic'
525!-}
527type PTactic = PTactic' PTerm
529data PDo' t = DoExp FC t
530 | DoBind FC Name t
531 | DoBindP FC t t
532 | DoLet FC Name t t
533 | DoLetP FC t t
534 deriving (Eq, Functor)
535{-!
536deriving instance Binary PDo'
537!-}
539type PDo = PDo' PTerm
541-- The priority gives a hint as to elaboration order. Best to elaborate
542-- things early which will help give a more concrete type to other
543-- variables, e.g. a before (interpTy a).
545data PArg' t = PImp { priority :: Int,
546 lazyarg :: Bool, pname :: Name, getTm :: t }
547 | PExp { priority :: Int,
548 lazyarg :: Bool, getTm :: t }
549 | PConstraint { priority :: Int,
550 lazyarg :: Bool, getTm :: t }
551 | PTacImplicit { priority :: Int,
552 lazyarg :: Bool, pname :: Name,
553 getScript :: t,
554 getTm :: t }
555 deriving (Show, Eq, Functor)
556{-!
557deriving instance Binary PArg'
558!-}
560pimp = PImp 0 True
561pexp = PExp 0 False
562pconst = PConstraint 0 False
563ptacimp = PTacImplicit 0 True
565type PArg = PArg' PTerm
567-- Type class data
569data ClassInfo = CI { instanceName :: Name,
570 class_methods :: [(Name, PTerm)],
571 class_defaults :: [(Name, Name)], -- method name -> default impl
572 class_params :: [Name] }
573 deriving Show
574{-!
575deriving instance Binary ClassInfo
576!-}
578data OptInfo = Optimise { collapsible :: Bool,
579 forceable :: [Int], -- argument positions
580 recursive :: [Int] }
581 deriving Show
582{-!
583deriving instance Binary OptInfo
584!-}
587data TypeInfo = TI { con_names :: [Name] }
588 deriving Show
589{-!
590deriving instance Binary TypeInfo
591!-}
593-- Syntactic sugar info
595data DSL' t = DSL { dsl_bind :: t,
596 dsl_return :: t,
597 dsl_apply :: t,
598 dsl_pure :: t,
599 dsl_var :: Maybe t,
600 index_first :: Maybe t,
601 index_next :: Maybe t,
602 dsl_lambda :: Maybe t,
603 dsl_let :: Maybe t
604 }
605 deriving (Show, Functor)
606{-!
607deriving instance Binary DSL'
608!-}
610type DSL = DSL' PTerm
612data SynContext = PatternSyntax | TermSyntax | AnySyntax
613 deriving Show
614{-!
615deriving instance Binary SynContext
616!-}
618data Syntax = Rule [SSymbol] PTerm SynContext
619 deriving Show
620{-!
621deriving instance Binary Syntax
622!-}
624data SSymbol = Keyword Name
625 | Symbol String
626 | Expr Name
627 | SimpleExpr Name
628 deriving Show
629{-!
630deriving instance Binary SSymbol
631!-}
633initDSL = DSL (PRef f (UN ">>="))
634 (PRef f (UN "return"))
635 (PRef f (UN "<$>"))
636 (PRef f (UN "pure"))
637 Nothing
638 Nothing
639 Nothing
640 Nothing
641 Nothing
642 where f = FC "(builtin)" 0
644data SyntaxInfo = Syn { using :: [(Name, PTerm)],
645 syn_params :: [(Name, PTerm)],
646 syn_namespace :: [String],
647 no_imp :: [Name],
648 decoration :: Name -> Name,
649 inPattern :: Bool,
650 dsl_info :: DSL }
651 deriving Show
653defaultSyntax = Syn [] [] [] [] id False initDSL
655--- Pretty printing declarations and terms
657instance Show PTerm where
658 show tm = showImp False tm
660instance Show PDecl where
661 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
662 show (PTy _ _ _ n ty) = show n ++ " : " ++ show ty
663 show (PClauses _ _ n c) = showSep "\n" (map show c)
664 show (PData _ _ d) = show d
666instance Show PClause where
667 show c = showCImp True c
669instance Show PData where
670 show d = showDImp False d
672showCImp :: Bool -> PClause -> String
673showCImp impl (PClause n l ws r w)
674 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
675 ++ " where " ++ show w
676 where
677 showWs [] = ""
678 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
679showCImp impl (PWith n l ws r w)
680 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
681 ++ " { " ++ show w ++ " } "
682 where
683 showWs [] = ""
684 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
687showDImp :: Bool -> PData -> String
688showDImp impl (PDatadecl n ty cons)
689 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
690 ++ showSep "\n\t| "
691 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
693getImps :: [PArg] -> [(Name, PTerm)]
694getImps [] = []
695getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
696getImps (_ : xs) = getImps xs
698getExps :: [PArg] -> [PTerm]
699getExps [] = []
700getExps (PExp _ _ tm : xs) = tm : getExps xs
701getExps (_ : xs) = getExps xs
703getConsts :: [PArg] -> [PTerm]
704getConsts [] = []
705getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
706getConsts (_ : xs) = getConsts xs
708getAll :: [PArg] -> [PTerm]
709getAll = map getTm
711showImp :: Bool -> PTerm -> String
712showImp impl tm = se 10 tm where
713 se p (PQuote r) = "![" ++ show r ++ "]"
714 se p (PRef _ n) = if impl then show n
715 else showbasic n
716 where showbasic n@(UN _) = show n
717 showbasic (MN _ s) = s
718 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
719 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
720 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
721 " in " ++ se 10 sc
722 se p (PPi (Exp l s) n ty sc)
723 | n `elem` allNamesIn sc = bracket p 2 $
724 if l then "|(" else "(" ++
725 show n ++ " : " ++ se 10 ty ++
726 ") " ++ st ++
727 "-> " ++ se 10 sc
728 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
729 where st = case s of
730 Static -> "[static] "
731 _ -> ""
732 se p (PPi (Imp l s) n ty sc)
733 | impl = bracket p 2 $ if l then "|{" else "{" ++
734 show n ++ " : " ++ se 10 ty ++
735 "} " ++ st ++ "-> " ++ se 10 sc
736 | otherwise = se 10 sc
737 where st = case s of
738 Static -> "[static] "
739 _ -> ""
740 se p (PPi (Constraint _ _) n ty sc)
741 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
742 se p (PApp _ (PRef _ f) [])
743 | not impl = show f
744 se p (PApp _ (PRef _ op@(UN (f:_))) args)
745 | length (getExps args) == 2 && not impl && not (isAlpha f)
746 = let [l, r] = getExps args in
747 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
748 se p (PApp _ f as)
749 = let args = getExps as in
750 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
751 else concatMap seArg args
752 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
753 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
754 se p (PHidden tm) = "." ++ se 0 tm
755 se p (PRefl _) = "refl"
756 se p (PResolveTC _) = "resolvetc"
757 se p (PTrue _) = "()"
758 se p (PFalse _) = "_|_"
759 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
760 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
761 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
762 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
763 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
764 se p PSet = "Set"
765 se p (PConstant c) = show c
766 se p (PProof ts) = "proof { " ++ show ts ++ "}"
767 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
768 se p (PMetavar n) = "?" ++ show n
769 se p (PReturn f) = "return"
770 se p PImpossible = "impossible"
771 se p Placeholder = "_"
772 se p (PDoBlock _) = "do block show not implemented"
773 se p (PElabError s) = s
774-- se p x = "Not implemented"
776 sArg (PImp _ _ n tm) = siArg (n, tm)
777 sArg (PExp _ _ tm) = seArg tm
778 sArg (PConstraint _ _ tm) = scArg tm
779 sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
781 seArg arg = " " ++ se 0 arg
782 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
783 scArg val = " {{" ++ se 10 val ++ "}}"
784 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
786 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
787 | otherwise = str
789allNamesIn :: PTerm -> [Name]
790allNamesIn tm = nub $ ni [] tm
791 where
792 ni env (PRef _ n)
793 | not (n `elem` env) = [n]
794 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
795 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
796 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
797 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
798 ni env (PHidden tm) = ni env tm
799 ni env (PEq _ l r) = ni env l ++ ni env r
800 ni env (PTyped l r) = ni env l ++ ni env r
801 ni env (PPair _ l r) = ni env l ++ ni env r
802 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
803 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
804 ni env (PAlternative ls) = concatMap (ni env) ls
805 ni env _ = []
807namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
808namesIn uvars ist tm = nub $ ni [] tm
809 where
810 ni env (PRef _ n)
811 | not (n `elem` env)
812 = case lookupTy Nothing n (tt_ctxt ist) of
813 [] -> [n]
814 _ -> if n `elem` (map fst uvars) then [n] else []
815 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
816 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
817 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
818 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
819 ni env (PEq _ l r) = ni env l ++ ni env r
820 ni env (PTyped l r) = ni env l ++ ni env r
821 ni env (PPair _ l r) = ni env l ++ ni env r
822 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
823 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
824 ni env (PAlternative as) = concatMap (ni env) as
825 ni env (PHidden tm) = ni env tm
826 ni env _ = []
828-- For inferring types of things
830bi = FC "builtin" 0
832inferTy = MN 0 "__Infer"
833inferCon = MN 0 "__infer"
834inferDecl = PDatadecl inferTy
835 PSet
836 [(inferCon, PPi impl (MN 0 "A") PSet (
837 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
838 (PRef bi inferTy)), bi)]
840infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
841infP = P (TCon 6 0) inferTy (Set (UVal 0))
843getInferTerm, getInferType :: Term -> Term
844getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
845getInferTerm (App (App _ _) tm) = tm
846getInferTerm tm = error ("getInferTerm " ++ show tm)
848getInferType (Bind n b sc) = Bind n b $ getInferType sc
849getInferType (App (App _ ty) _) = ty
851-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
853primNames = [unitTy, unitCon,
854 falseTy, pairTy, pairCon,
855 eqTy, eqCon, inferTy, inferCon]
857unitTy = MN 0 "__Unit"
858unitCon = MN 0 "__II"
859unitDecl = PDatadecl unitTy PSet
860 [(unitCon, PRef bi unitTy, bi)]
862falseTy = MN 0 "__False"
863falseDecl = PDatadecl falseTy PSet []
865pairTy = MN 0 "__Pair"
866pairCon = MN 0 "__MkPair"
867pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
868 [(pairCon, PPi impl (n "A") PSet (
869 PPi impl (n "B") PSet (
870 PPi expl (n "a") (PRef bi (n "A")) (
871 PPi expl (n "b") (PRef bi (n "B"))
872 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
873 pexp (PRef bi (n "B"))])))), bi)]
874 where n a = MN 0 a
876eqTy = UN "="
877eqCon = UN "refl"
878eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
879 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
880 PSet)
881 [(eqCon, PPi impl (n "a") PSet (
882 PPi impl (n "x") (PRef bi (n "a"))
883 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
884 pimp (n "b") Placeholder,
885 pexp (PRef bi (n "x")),
886 pexp (PRef bi (n "x"))])), bi)]
887 where n a = MN 0 a
889-- Defined in builtins.idr
890sigmaTy = UN "Exists"
891existsCon = UN "Ex_intro"
893piBind :: [(Name, PTerm)] -> PTerm -> PTerm
894piBind [] t = t
895piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
897tcname (UN ('@':_)) = True
898tcname (NS n _) = tcname n
899tcname _ = False
901-- Dealing with parameters
903expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
904expandParams dec ps ns tm = en tm
905 where
906 -- if we shadow a name (say in a lambda binding) that is used in a call to
907 -- a lifted function, we need access to both names - once in the scope of the
908 -- binding and once to call the lifted functions. So we'll explicitly shadow
909 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
910 -- but we didn't...)
912 mkShadow (UN n) = MN 0 n
913 mkShadow (MN i n) = MN (i+1) n
914 mkShadow (NS x s) = NS (mkShadow x) s
916 en (PLam n t s)
917 | n `elem` map fst ps
918 = let n' = mkShadow n in
919 PLam n' (en t) (en (shadow n n' s))
920 | otherwise = PLam n (en t) (en s)
921 en (PPi p n t s)
922 | n `elem` map fst ps
923 = let n' = mkShadow n in
924 PPi p n' (en t) (en (shadow n n' s))
925 | otherwise = PPi p n (en t) (en s)
926 en (PLet n ty v s)
927 | n `elem` map fst ps
928 = let n' = mkShadow n in
929 PLet n' (en ty) (en v) (en (shadow n n' s))
930 | otherwise = PLet n (en ty) (en v) (en s)
931 en (PEq f l r) = PEq f (en l) (en r)
932 en (PTyped l r) = PTyped (en l) (en r)
933 en (PPair f l r) = PPair f (en l) (en r)
934 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
935 en (PAlternative as) = PAlternative (map en as)
936 en (PHidden t) = PHidden (en t)
937 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
938 en (PProof ts) = PProof (map (fmap en) ts)
939 en (PTactics ts) = PTactics (map (fmap en) ts)
941 en (PQuote (Var n))
942 | n `elem` ns = PQuote (Var (dec n))
943 en (PApp fc (PRef fc' n) as)
944 | n `elem` ns = PApp fc (PRef fc' (dec n))
945 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
946 en (PRef fc n)
947 | n `elem` ns = PApp fc (PRef fc (dec n))
948 (map (pexp . (PRef fc)) (map fst ps))
949 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
950 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
951 en t = t
953expandParamsD :: IState ->
954 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
955expandParamsD ist dec ps ns (PTy syn fc o n ty)
956 = if n `elem` ns
957 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
958 else PTy syn fc o n (expandParams dec ps ns ty)
959expandParamsD ist dec ps ns (PClauses fc opts n cs)
960 = let n' = if n `elem` ns then dec n else n in
961 PClauses fc opts n' (map expandParamsC cs)
962 where
963 expandParamsC (PClause n lhs ws rhs ds)
964 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
965 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
966 n' = if n `elem` ns then dec n else n in
967 PClause n' (expandParams dec ps'' ns lhs)
968 (map (expandParams dec ps'' ns) ws)
969 (expandParams dec ps'' ns rhs)
970 (map (expandParamsD ist dec ps'' ns) ds)
971 expandParamsC (PWith n lhs ws wval ds)
972 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
973 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
974 n' = if n `elem` ns then dec n else n in
975 PWith n' (expandParams dec ps'' ns lhs)
976 (map (expandParams dec ps'' ns) ws)
977 (expandParams dec ps'' ns wval)
978 (map (expandParamsD ist dec ps'' ns) ds)
979 updateps yn nm [] = []
980 updateps yn nm (((a, t), i):as)
981 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
982 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
984expandParamsD ist dec ps ns d = d
986-- Calculate a priority for a type, for deciding elaboration order
987-- * if it's just a type variable or concrete type, do it early (0)
988-- * if there's only type variables and injective constructors, do it next (1)
989-- * if there's a function type, next (2)
990-- * finally, everything else (3)
992getPriority :: IState -> PTerm -> Int
993getPriority i tm = pri tm
994 where
995 pri (PRef _ n) =
996 case lookupP Nothing n (tt_ctxt i) of
997 ((P (DCon _ _) _ _):_) -> 1
998 ((P (TCon _ _) _ _):_) -> 1
999 ((P Ref _ _):_) -> 4
1000 [] -> 0 -- must be locally bound, if it's not an error...
1001 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1002 pri (PTrue _) = 0
1003 pri (PFalse _) = 0
1004 pri (PRefl _) = 1
1005 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1006 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1007 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1008 pri (PTyped l r) = pri l
1009 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
1010 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1011 pri (PAlternative as) = maximum (map pri as)
1012 pri (PConstant _) = 0
1013 pri Placeholder = 1
1014 pri _ = 3
1016-- Dealing with implicit arguments
1018-- Add implicit Pi bindings for any names in the term which appear in an
1019-- argument position.
1021-- This has become a right mess already. Better redo it some time...
1023implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1024implicit syn n ptm
1025 = do i <- get
1026 let (tm', impdata) = implicitise syn i ptm
1027 let (tm'', spos) = findStatics i tm'
1028 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
1029 addIBC (IBCImp n)
1030 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1031 i <- get
1032 put (i { idris_statics = addDef n spos (idris_statics i) })
1033 addIBC (IBCStatic n)
1034 return tm''
1036implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
1037implicitise syn ist tm
1038 = let (declimps, ns') = execState (imps True [] tm) ([], [])
1039 ns = ns' \\ (map fst pvars ++ no_imp syn) in
1040 if null ns
1041 then (tm, reverse declimps)
1042 else implicitise syn ist (pibind uvars ns tm)
1043 where
1044 uvars = using syn
1045 pvars = syn_params syn
1047 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1048 | otherwise = x : dropAll xs ys
1049 dropAll [] ys = []
1051 imps top env (PApp _ f as)
1052 = do (decls, ns) <- get
1053 let isn = concatMap (namesIn uvars ist) (map getTm as)
1054 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1055 imps top env (PPi (Imp l _) n ty sc)
1056 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1057 (decls , ns) <- get
1058 put (PImp (getPriority ist ty) l n ty : decls,
1059 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1060 imps True (n:env) sc
1061 imps top env (PPi (Exp l _) n ty sc)
1062 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1063 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1064 _ -> [])
1065 (decls, ns) <- get -- ignore decls in HO types
1066 put (PExp (getPriority ist ty) l ty : decls,
1067 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1068 imps True (n:env) sc
1069 imps top env (PPi (Constraint l _) n ty sc)
1070 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1071 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1072 _ -> [])
1073 (decls, ns) <- get -- ignore decls in HO types
1074 put (PConstraint 10 l ty : decls,
1075 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1076 imps True (n:env) sc
1077 imps top env (PPi (TacImp l _ scr) n ty sc)
1078 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1079 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1080 _ -> [])
1081 (decls, ns) <- get -- ignore decls in HO types
1082 put (PTacImplicit 10 l n scr ty : decls,
1083 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1084 imps True (n:env) sc
1085 imps top env (PEq _ l r)
1086 = do (decls, ns) <- get
1087 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1088 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1089 imps top env (PTyped l r)
1090 = imps top env l
1091 imps top env (PPair _ l r)
1092 = do (decls, ns) <- get
1093 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1094 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1095 imps top env (PDPair _ (PRef _ n) t r)
1096 = do (decls, ns) <- get
1097 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1098 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1099 imps top env (PDPair _ l t r)
1100 = do (decls, ns) <- get
1101 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1102 namesIn uvars ist r
1103 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1104 imps top env (PAlternative as)
1105 = do (decls, ns) <- get
1106 let isn = concatMap (namesIn uvars ist) as
1107 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1108 imps top env (PLam n ty sc)
1109 = do imps False env ty
1110 imps False (n:env) sc
1111 imps top env (PHidden tm) = imps False env tm
1112 imps top env _ = return ()
1114 pibind using [] sc = sc
1115 pibind using (n:ns) sc
1116 = case lookup n using of
1117 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
1118 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
1120-- Add implicit arguments in function calls
1122addImpl :: IState -> PTerm -> PTerm
1123addImpl ist ptm = ai [] ptm
1124 where
1125 ai env (PRef fc f)
1126 | not (f `elem` env) = aiFn ist fc f []
1127 ai env (PEq fc l r) = let l' = ai env l
1128 r' = ai env r in
1129 PEq fc l' r'
1130 ai env (PTyped l r) = let l' = ai env l
1131 r' = ai env r in
1132 PTyped l' r'
1133 ai env (PPair fc l r) = let l' = ai env l
1134 r' = ai env r in
1135 PPair fc l' r'
1136 ai env (PDPair fc l t r) = let l' = ai env l
1137 t' = ai env t
1138 r' = ai env r in
1139 PDPair fc l' t' r'
1140 ai env (PAlternative as) = let as' = map (ai env) as in
1141 PAlternative as'
1142 ai env (PApp fc (PRef _ f) as)
1143 | not (f `elem` env)
1144 = let as' = map (fmap (ai env)) as in
1145 aiFn ist fc f as'
1146 ai env (PApp fc f as) = let f' = ai env f
1147 as' = map (fmap (ai env)) as in
1148 mkPApp fc 1 f' as'
1149 ai env (PCase fc c os) = let c' = ai env c
1150 os' = map (pmap (ai env)) os in
1151 PCase fc c' os'
1152 ai env (PLam n ty sc) = let ty' = ai env ty
1153 sc' = ai (n:env) sc in
1154 PLam n ty' sc'
1155 ai env (PLet n ty val sc)
1156 = let ty' = ai env ty
1157 val' = ai env val
1158 sc' = ai (n:env) sc in
1159 PLet n ty' val' sc'
1160 ai env (PPi p n ty sc) = let ty' = ai env ty
1161 sc' = ai (n:env) sc in
1162 PPi p n ty' sc'
1163 ai env (PHidden tm) = PHidden (ai env tm)
1164 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1165 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1166 ai env tm = tm
1168aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
1169aiFn ist fc f as
1170 | f `elem` primNames = PApp fc (PRef fc f) as
1171aiFn ist fc f as
1172 -- This is where namespaces get resolved by adding PAlternative
1173 = case lookupCtxtName Nothing f (idris_implicits ist) of
1174 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1175 [] -> if f `elem` idris_metavars ist
1176 then PApp fc (PRef fc f) as
1177 else mkPApp fc (length as) (PRef fc f) as
1178 alts -> PAlternative $
1179 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1180 (insertImpl ns as)) alts
1181 where
1182 insertImpl :: [PArg] -> [PArg] -> [PArg]
1183 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1184 PExp p l tm : insertImpl ps given
1185 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1186 PConstraint p l tm : insertImpl ps given
1187 insertImpl (PConstraint p l ty : ps) given =
1188 PConstraint p l (PResolveTC fc) : insertImpl ps given
1189 insertImpl (PImp p l n ty : ps) given =
1190 case find n given [] of
1191 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
1192 Nothing -> PImp p l n Placeholder : insertImpl ps given
1193 insertImpl (PTacImplicit p l n sc ty : ps) given =
1194 case find n given [] of
1195 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1196 Nothing -> PTacImplicit p l n sc sc
1197 : insertImpl ps given
1198 insertImpl expected [] = []
1199 insertImpl _ given = given
1201 find n [] acc = Nothing
1202 find n (PImp _ _ n' t : gs) acc
1203 | n == n' = Just (t, reverse acc ++ gs)
1204 find n (g : gs) acc = find n gs (g : acc)
1206mkPApp fc a f [] = f
1207mkPApp fc a f as = let rest = drop a as in
1208 appRest fc (PApp fc f (take a as)) rest
1209 where
1210 appRest fc f [] = f
1211 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1213-- Find 'static' argument positions
1214-- (the declared ones, plus any names in argument position in the declared
1215-- statics)
1216-- FIXME: It's possible that this really has to happen after elaboration
1218findStatics :: IState -> PTerm -> (PTerm, [Bool])
1219findStatics ist tm = let (ns, ss) = fs tm in
1220 runState (pos ns ss tm) []
1221 where fs (PPi p n t sc)
1222 | Static <- pstatic p
1223 = let (ns, ss) = fs sc in
1224 (namesIn [] ist t : ns, namesIn [] ist t ++ n : ss)
1225 | otherwise = let (ns, ss) = fs sc in
1226 (namesIn [] ist t : ns, ss)
1227 fs _ = ([], [])
1229 inOne n ns = length (filter id (map (elem n) ns)) == 1
1231 pos ns ss (PPi p n t sc)
1232 | n `inOne` ns && elem n ss
1233 = do sc' <- pos ns ss sc
1234 spos <- get
1235 put (True : spos)
1236 return (PPi (p { pstatic = Static }) n t sc')
1237 | otherwise = do sc' <- pos ns ss sc
1238 spos <- get
1239 put (False : spos)
1240 return (PPi p n t sc')
1241 pos ns ss t = return t
1243-- Debugging/logging stuff
1245dumpDecls :: [PDecl] -> String
1246dumpDecls [] = ""
1247dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1249dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1250dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1251dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1252dumpDecl (PData _ _ d) = showDImp True d
1253dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1254dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1255dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1256dumpDecl (PClass _ _ cs n ps ds)
1257 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1258dumpDecl (PInstance _ _ cs n _ t ds)
1259 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1260dumpDecl _ = "..."
1261-- dumpDecl (PImport i) = "import " ++ i
1263-- for 6.12/7 compatibility
1264data EitherErr a b = LeftErr a | RightOK b
1266instance Monad (EitherErr a) where
1267 return = RightOK
1269 (LeftErr e) >>= k = LeftErr e
1270 RightOK v >>= k = k v
1272toEither (LeftErr e) = Left e
1273toEither (RightOK ho) = Right ho
1275-- syntactic match of a against b, returning pair of variables in a
1276-- and what they match. Returns the pair that failed if not a match.
1278matchClause :: PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1279matchClause = matchClause' False
1281matchClause' :: Bool -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1282matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where
1283 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1285 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1286 fullApp x = x
1288 match' x y = match (fullApp x) (fullApp y)
1289 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1290 | PConstant (I _) <- getTm x = match (getTm x) x'
1291 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1292 | PConstant (I _) <- getTm x = match (getTm x) x'
1293 match (PApp _ f args) (PApp _ f' args')
1294 | length args == length args'
1295 = do mf <- match' f f'
1296 ms <- zipWithM matchArg args args'
1297 return (mf ++ concat ms)
1298-- match (PRef _ n) (PRef _ n') | n == n' = return []
1299-- | otherwise = Nothing
1300 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1301 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1302 match (PRef _ n) (PRef _ n') | n == n' = return []
1303 match (PRef _ n) tm | not names = return [(n, tm)]
1304 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1305 mr <- match' r r'
1306 return (ml ++ mr)
1307 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1308 mr <- match r r'
1309 return (ml ++ mr)
1310 match (PTyped l r) x = match l x
1311 match x (PTyped l r) = match x l
1312 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1313 mr <- match' r r'
1314 return (ml ++ mr)
1315 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1316 mt <- match' t t'
1317 mr <- match' r r'
1318 return (ml ++ mt ++ mr)
1319 match (PAlternative as) (PAlternative as')
1320 = do ms <- zipWithM match' as as'
1321 return (concat ms)
1322 match a@(PAlternative as) b
1323 = do let ms = zipWith match' as (repeat b)
1324 case (rights (map toEither ms)) of
1325 (x: _) -> return x
1326 _ -> LeftErr (a, b)
1327 match (PCase _ _ _) _ = return [] -- lifted out
1328 match (PMetavar _) _ = return [] -- modified
1329 match (PQuote _) _ = return []
1330 match (PProof _) _ = return []
1331 match (PTactics _) _ = return []
1332 match (PRefl _) (PRefl _) = return []
1333 match (PResolveTC _) (PResolveTC _) = return []
1334 match (PTrue _) (PTrue _) = return []
1335 match (PFalse _) (PFalse _) = return []
1336 match (PReturn _) (PReturn _) = return []
1337 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1338 ms <- match' s s'
1339 return (mt ++ ms)
1340 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1341 ms <- match' s s'
1342 return (mt ++ ms)
1343 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1344 mty <- match' ty ty'
1345 ms <- match' s s'
1346 return (mt ++ mty ++ ms)
1347 match (PHidden x) (PHidden y) = match' x y
1348 match Placeholder _ = return []
1349 match _ Placeholder = return []
1350 match (PResolveTC _) _ = return []
1351 match a b | a == b = return []
1352 | otherwise = LeftErr (a, b)
1354 checkRpts (RightOK ms) = check ms where
1355 check ((n,t):xs)
1356 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1357 then Left (t, t')
1358 else check xs
1359 check (_:xs) = check xs
1360 check [] = Right ms
1361 checkRpts (LeftErr x) = Left x
1363substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1364substMatches [] t = t
1365substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1367substMatch :: Name -> PTerm -> PTerm -> PTerm
1368substMatch n tm t = sm t where
1369 sm (PRef _ n') | n == n' = tm
1370 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1371 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1372 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1373 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1374 sm (PEq f x y) = PEq f (sm x) (sm y)
1375 sm (PTyped x y) = PTyped (sm x) (sm y)
1376 sm (PPair f x y) = PPair f (sm x) (sm y)
1377 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1378 sm (PAlternative as) = PAlternative (map sm as)
1379 sm (PHidden x) = PHidden (sm x)
1380 sm x = x
1382shadow :: Name -> Name -> PTerm -> PTerm
1383shadow n n' t = sm t where
1384 sm (PRef fc x) | n == x = PRef fc n'
1385 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1386 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1387 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1388 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1389 sm (PEq f x y) = PEq f (sm x) (sm y)
1390 sm (PTyped x y) = PTyped (sm x) (sm y)
1391 sm (PPair f x y) = PPair f (sm x) (sm y)
1392 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1393 sm (PAlternative as) = PAlternative (map sm as)
1394 sm (PHidden x) = PHidden (sm x)
1395 sm x = x