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