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