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