git.iko.soy/Idris-dev
on 047be9e help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1821 lines 69 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
11import Paths_idris
13import System.Console.Haskeline
15import Control.Monad.State
17import Data.List
18import Data.Char
19import Data.Either
21import Debug.Trace
23import qualified Epic.Epic as E
25import Util.Pretty
27data IOption = IOption { opt_logLevel :: Int,
28 opt_typecase :: Bool,
29 opt_typeintype :: Bool,
30 opt_coverage :: Bool,
31 opt_showimp :: Bool,
32 opt_repl :: Bool,
33 opt_verbose :: Bool,
34 opt_ibcsubdir :: FilePath,
35 opt_importdirs :: [FilePath]
36 }
37 deriving (Show, Eq)
39defaultOpts = IOption 0 False False True False True True "" []
41-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
42-- without typechecking).
43-- This will include all the functions and data declarations, plus fixity declarations
44-- and syntax macros.
46data IState = IState { tt_ctxt :: Context,
47 idris_constraints :: [(UConstraint, FC)],
48 idris_infixes :: [FixDecl],
49 idris_implicits :: Ctxt [PArg],
50 idris_statics :: Ctxt [Bool],
51 idris_classes :: Ctxt ClassInfo,
52 idris_dsls :: Ctxt DSL,
53 idris_optimisation :: Ctxt OptInfo,
54 idris_datatypes :: Ctxt TypeInfo,
55 idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported
56 idris_flags :: Ctxt [FnOpt],
57 idris_callgraph :: Ctxt [Name],
58 idris_totcheck :: [(FC, Name)],
59 idris_log :: String,
60 idris_options :: IOption,
61 idris_name :: Int,
62 idris_metavars :: [Name],
63 syntax_rules :: [Syntax],
64 syntax_keywords :: [String],
65 imported :: [FilePath],
66 idris_prims :: [(Name, ([E.Name], E.Term))],
67 idris_objs :: [FilePath],
68 idris_libs :: [String],
69 idris_hdrs :: [String],
70 last_proof :: Maybe (Name, [String]),
71 errLine :: Maybe Int,
72 lastParse :: Maybe Name,
73 indent_stack :: [Int],
74 brace_stack :: [Maybe Int],
75 hide_list :: [(Name, Maybe Accessibility)],
76 default_access :: Accessibility,
77 ibc_write :: [IBCWrite],
78 compiled_so :: Maybe String
79 }
81-- information that needs writing for the current module's .ibc file
82data IBCWrite = IBCFix FixDecl
83 | IBCImp Name
84 | IBCStatic Name
85 | IBCClass Name
86 | IBCInstance Bool Name Name
87 | IBCDSL Name
88 | IBCData Name
89 | IBCOpt Name
90 | IBCSyntax Syntax
91 | IBCKeyword String
92 | IBCImport FilePath
93 | IBCObj FilePath
94 | IBCLib String
95 | IBCHeader String
96 | IBCAccess Name Accessibility
97 | IBCTotal Name Totality
98 | IBCFlags Name [FnOpt]
99 | IBCCG Name
100 | IBCDef Name -- i.e. main context
101 deriving Show
103idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
104 emptyContext emptyContext emptyContext emptyContext
105 emptyContext emptyContext
106 [] "" defaultOpts 6 [] [] [] [] [] [] [] []
107 Nothing Nothing Nothing [] [] [] Hidden [] Nothing
109-- The monad for the main REPL - reading and processing files and updating
110-- global state (hence the IO inner monad).
111type Idris = StateT IState (InputT IO)
113getContext :: Idris Context
114getContext = do i <- get; return (tt_ctxt i)
116getObjectFiles :: Idris [FilePath]
117getObjectFiles = do i <- get; return (idris_objs i)
119addObjectFile :: FilePath -> Idris ()
120addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
122getLibs :: Idris [String]
123getLibs = do i <- get; return (idris_libs i)
125addLib :: String -> Idris ()
126addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
128addHdr :: String -> Idris ()
129addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
131totcheck :: (FC, Name) -> Idris ()
132totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i })
134setFlags :: Name -> [FnOpt] -> Idris ()
135setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
137setAccessibility :: Name -> Accessibility -> Idris ()
138setAccessibility n a
139 = do i <- get
140 let ctxt = setAccess n a (tt_ctxt i)
141 put (i { tt_ctxt = ctxt })
143setTotality :: Name -> Totality -> Idris ()
144setTotality n a
145 = do i <- get
146 let ctxt = setTotal n a (tt_ctxt i)
147 put (i { tt_ctxt = ctxt })
149getTotality :: Name -> Idris Totality
150getTotality n
151 = do i <- get
152 case lookupTotal n (tt_ctxt i) of
153 [t] -> return t
154 _ -> return (Total [])
156addToCG :: Name -> [Name] -> Idris ()
157addToCG n ns = do i <- get
158 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })
160-- Add a class instance function. Dodgy hack: Put integer instances first in the
161-- list so they are resolved by default.
163addInstance :: Bool -> Name -> Name -> Idris ()
164addInstance int n i
165 = do ist <- get
166 case lookupCtxt Nothing n (idris_classes ist) of
167 [CI a b c d ins] ->
168 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
169 put (ist { idris_classes = cs })
170 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
171 put (ist { idris_classes = cs })
172 where addI i ins | int = i : ins
173 | otherwise = ins ++ [i]
175addClass :: Name -> ClassInfo -> Idris ()
176addClass n i
177 = do ist <- get
178 let i' = case lookupCtxt Nothing n (idris_classes ist) of
179 [c] -> c { class_instances = class_instances i }
180 _ -> i
181 put (ist { idris_classes = addDef n i' (idris_classes ist) })
183addIBC :: IBCWrite -> Idris ()
184addIBC ibc@(IBCDef n)
185 = do i <- get
186 when (notDef (ibc_write i)) $
187 put (i { ibc_write = ibc : ibc_write i })
188 where notDef [] = True
189 notDef (IBCDef n': is) | n == n' = False
190 notDef (_ : is) = notDef is
191addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
193clearIBC :: Idris ()
194clearIBC = do i <- get; put (i { ibc_write = [] })
196getHdrs :: Idris [String]
197getHdrs = do i <- get; return (idris_hdrs i)
199setErrLine :: Int -> Idris ()
200setErrLine x = do i <- get;
201 case (errLine i) of
202 Nothing -> put (i { errLine = Just x })
203 Just _ -> return ()
205clearErr :: Idris ()
206clearErr = do i <- get
207 put (i { errLine = Nothing })
209getSO :: Idris (Maybe String)
210getSO = do i <- get
211 return (compiled_so i)
213setSO :: Maybe String -> Idris ()
214setSO s = do i <- get
215 put (i { compiled_so = s })
217getIState :: Idris IState
218getIState = get
220putIState :: IState -> Idris ()
221putIState = put
223getName :: Idris Int
224getName = do i <- get;
225 let idx = idris_name i;
226 put (i { idris_name = idx + 1 })
227 return idx
229checkUndefined :: FC -> Name -> Idris ()
230checkUndefined fc n
231 = do i <- getContext
232 case lookupTy Nothing n i of
233 (_:_) -> fail $ show fc ++ ":" ++
234 show n ++ " already defined"
235 _ -> return ()
237setContext :: Context -> Idris ()
238setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
240updateContext :: (Context -> Context) -> Idris ()
241updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
243addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
244addConstraints fc (v, cs)
245 = do i <- get
246 let ctxt = tt_ctxt i
247 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
248 next_tvar = v }
249 let ics = zip cs (repeat fc) ++ idris_constraints i
250 put (i { tt_ctxt = ctxt', idris_constraints = ics })
252addDeferred :: [(Name, Type)] -> Idris ()
253addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
254 i <- get
255 put (i { idris_metavars = map fst ns ++ idris_metavars i })
256 where tidyNames used (Bind (MN i x) b sc)
257 = let n' = uniqueName (UN x) used in
258 Bind n' b $ tidyNames (n':used) sc
259 tidyNames used (Bind n b sc)
260 = let n' = uniqueName n used in
261 Bind n' b $ tidyNames (n':used) sc
262 tidyNames used b = b
264solveDeferred :: Name -> Idris ()
265solveDeferred n = do i <- get
266 put (i { idris_metavars = idris_metavars i \\ [n] })
268iputStrLn :: String -> Idris ()
269iputStrLn = liftIO . putStrLn
271iWarn :: FC -> String -> Idris ()
272iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
274setLogLevel :: Int -> Idris ()
275setLogLevel l = do i <- get
276 let opts = idris_options i
277 let opt' = opts { opt_logLevel = l }
278 put (i { idris_options = opt' } )
280logLevel :: Idris Int
281logLevel = do i <- get
282 return (opt_logLevel (idris_options i))
284useREPL :: Idris Bool
285useREPL = do i <- get
286 return (opt_repl (idris_options i))
288setREPL :: Bool -> Idris ()
289setREPL t = do i <- get
290 let opts = idris_options i
291 let opt' = opts { opt_repl = t }
292 put (i { idris_options = opt' })
294verbose :: Idris Bool
295verbose = do i <- get
296 return (opt_verbose (idris_options i))
298setVerbose :: Bool -> Idris ()
299setVerbose t = do i <- get
300 let opts = idris_options i
301 let opt' = opts { opt_verbose = t }
302 put (i { idris_options = opt' })
304typeInType :: Idris Bool
305typeInType = do i <- get
306 return (opt_typeintype (idris_options i))
308setTypeInType :: Bool -> Idris ()
309setTypeInType t = do i <- get
310 let opts = idris_options i
311 let opt' = opts { opt_typeintype = t }
312 put (i { idris_options = opt' })
314coverage :: Idris Bool
315coverage = do i <- get
316 return (opt_coverage (idris_options i))
318setCoverage :: Bool -> Idris ()
319setCoverage t = do i <- get
320 let opts = idris_options i
321 let opt' = opts { opt_coverage = t }
322 put (i { idris_options = opt' })
324setIBCSubDir :: FilePath -> Idris ()
325setIBCSubDir fp = do i <- get
326 let opts = idris_options i
327 let opt' = opts { opt_ibcsubdir = fp }
328 put (i { idris_options = opt' })
330valIBCSubDir :: IState -> Idris FilePath
331valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
333setImportDirs :: [FilePath] -> Idris ()
334setImportDirs fps = do i <- get
335 let opts = idris_options i
336 let opt' = opts { opt_importdirs = fps }
337 put (i { idris_options = opt' })
339allImportDirs :: IState -> Idris [FilePath]
340allImportDirs i = do datadir <- liftIO $ getDataDir
341 let optdirs = opt_importdirs (idris_options i)
342 return ("." : (optdirs ++ [datadir]))
344impShow :: Idris Bool
345impShow = do i <- get
346 return (opt_showimp (idris_options i))
348setImpShow :: Bool -> Idris ()
349setImpShow t = do i <- get
350 let opts = idris_options i
351 let opt' = opts { opt_showimp = t }
352 put (i { idris_options = opt' })
354logLvl :: Int -> String -> Idris ()
355logLvl l str = do i <- get
356 let lvl = opt_logLevel (idris_options i)
357 when (lvl >= l)
358 $ do liftIO (putStrLn str)
359 put (i { idris_log = idris_log i ++ str ++ "\n" } )
361iLOG :: String -> Idris ()
362iLOG = logLvl 1
364noErrors :: Idris Bool
365noErrors = do i <- get
366 case errLine i of
367 Nothing -> return True
368 _ -> return False
370setTypeCase :: Bool -> Idris ()
371setTypeCase t = do i <- get
372 let opts = idris_options i
373 let opt' = opts { opt_typecase = t }
374 put (i { idris_options = opt' })
376-- Commands in the REPL
378data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
379 | Reload | Edit
380 | Compile String | Execute | ExecVal PTerm
381 | Metavars | Prove Name | AddProof | Universes
382 | TTShell
383 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name
384 | Info Name | DebugInfo Name
385 | Search PTerm
386 | NOP
388-- Parsed declarations
390data Fixity = Infixl { prec :: Int }
391 | Infixr { prec :: Int }
392 | InfixN { prec :: Int }
393 | PrefixN { prec :: Int }
394 deriving Eq
395{-!
396deriving instance Binary Fixity
397!-}
399instance Show Fixity where
400 show (Infixl i) = "infixl " ++ show i
401 show (Infixr i) = "infixr " ++ show i
402 show (InfixN i) = "infix " ++ show i
403 show (PrefixN i) = "prefix " ++ show i
405data FixDecl = Fix Fixity String
406 deriving (Show, Eq)
407{-!
408deriving instance Binary FixDecl
409!-}
411instance Ord FixDecl where
412 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
415data Static = Static | Dynamic
416 deriving (Show, Eq)
417{-!
418deriving instance Binary Static
419!-}
421-- Mark bindings with their explicitness, and laziness
422data Plicity = Imp { plazy :: Bool,
423 pstatic :: Static }
424 | Exp { plazy :: Bool,
425 pstatic :: Static }
426 | Constraint { plazy :: Bool,
427 pstatic :: Static }
428 | TacImp { plazy :: Bool,
429 pstatic :: Static,
430 pscript :: PTerm }
431 deriving (Show, Eq)
433{-!
434deriving instance Binary Plicity
435!-}
437impl = Imp False Dynamic
438expl = Exp False Dynamic
439constraint = Constraint False Dynamic
440tacimpl = TacImp False Dynamic
442data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
443 | Specialise [Name] -- specialise it, freeze these names
444 deriving (Show, Eq)
445{-!
446deriving instance Binary FnOpt
447!-}
449type FnOpts = [FnOpt]
451inlinable :: FnOpts -> Bool
452inlinable = elem Inlinable
454data PDecl' t = PFix FC Fixity [String] -- fixity declaration
455 | PTy SyntaxInfo FC FnOpts Name t -- type declaration
456 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
457 | PData SyntaxInfo FC (PData' t) -- data declaration
458 | PParams FC [(Name, t)] [PDecl' t] -- params block
459 | PNamespace String [PDecl' t] -- new namespace
460 | PRecord SyntaxInfo FC Name t Name t -- record declaration
461 | PClass SyntaxInfo FC
462 [t] -- constraints
463 Name
464 [(Name, t)] -- parameters
465 [PDecl' t] -- declarations
466 | PInstance SyntaxInfo FC [t] -- constraints
467 Name -- class
468 [t] -- parameters
469 t -- full instance type
470 [PDecl' t]
471 | PDSL Name (DSL' t)
472 | PSyntax FC Syntax
473 | PDirective (Idris ())
474 deriving Functor
476data PClause' t = PClause FC Name t [t] t [PDecl' t]
477 | PWith FC Name t [t] t [PDecl' t]
478 | PClauseR FC [t] t [PDecl' t]
479 | PWithR FC [t] t [PDecl' t]
480 deriving Functor
482data PData' t = PDatadecl { d_name :: Name,
483 d_tcon :: t,
484 d_cons :: [(Name, t, FC)] }
485 deriving Functor
487-- Handy to get a free function for applying PTerm -> PTerm functions
488-- across a program, by deriving Functor
490type PDecl = PDecl' PTerm
491type PData = PData' PTerm
492type PClause = PClause' PTerm
494-- get all the names declared in a decl
496declared :: PDecl -> [Name]
497declared (PFix _ _ _) = []
498declared (PTy _ _ _ n t) = [n]
499declared (PClauses _ _ n _) = [] -- not a declaration
500declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
501 where fstt (a, _, _) = a
502declared (PParams _ _ ds) = concatMap declared ds
503declared (PNamespace _ ds) = concatMap declared ds
504-- declared (PImport _) = []
506defined :: PDecl -> [Name]
507defined (PFix _ _ _) = []
508defined (PTy _ _ _ n t) = []
509defined (PClauses _ _ n _) = [n] -- not a declaration
510defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
511 where fstt (a, _, _) = a
512defined (PParams _ _ ds) = concatMap defined ds
513defined (PNamespace _ ds) = concatMap defined ds
514-- declared (PImport _) = []
516updateN :: [(Name, Name)] -> Name -> Name
517updateN ns n | Just n' <- lookup n ns = n'
518updateN _ n = n
520updateNs :: [(Name, Name)] -> PTerm -> PTerm
521updateNs [] t = t
522updateNs ns t = mapPT updateRef t
523 where updateRef (PRef fc f) = PRef fc (updateN ns f)
524 updateRef t = t
526-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
527-- updateDNs [] t = t
528-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
529-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
530-- where updateCNs ns (PClause n l ts r ds)
531-- = PClause (updateN ns n) (fmap (updateNs ns) l)
532-- (map (fmap (updateNs ns)) ts)
533-- (fmap (updateNs ns) r)
534-- (map (updateDNs ns) ds)
535-- updateDNs ns c = c
537-- High level language terms
539data PTerm = PQuote Raw
540 | PRef FC Name
541 | PLam Name PTerm PTerm
542 | PPi Plicity Name PTerm PTerm
543 | PLet Name PTerm PTerm PTerm
544 | PTyped PTerm PTerm -- term with explicit type
545 | PApp FC PTerm [PArg]
546 | PCase FC PTerm [(PTerm, PTerm)]
547 | PTrue FC
548 | PFalse FC
549 | PRefl FC
550 | PResolveTC FC
551 | PEq FC PTerm PTerm
552 | PPair FC PTerm PTerm
553 | PDPair FC PTerm PTerm PTerm
554 | PAlternative Bool [PTerm] -- True if only one may work
555 | PHidden PTerm -- irrelevant or hidden pattern
556 | PSet
557 | PConstant Const
558 | Placeholder
559 | PDoBlock [PDo]
560 | PIdiom FC PTerm
561 | PReturn FC
562 | PMetavar Name
563 | PProof [PTactic]
564 | PTactics [PTactic] -- as PProof, but no auto solving
565 | PElabError Err -- error to report on elaboration
566 | PImpossible -- special case for declaring when an LHS can't typecheck
567 deriving Eq
568{-!
569deriving instance Binary PTerm
570!-}
572mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
573mapPT f t = f (mpt t) where
574 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
575 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
576 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
577 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
578 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
579 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
580 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
581 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
582 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
583 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
584 mpt (PHidden t) = PHidden (mapPT f t)
585 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
586 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
587 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
588 mpt x = x
591data PTactic' t = Intro [Name] | Intros | Focus Name
592 | Refine Name [Bool] | Rewrite t | LetTac Name t
593 | Exact t | Compute | Trivial
594 | Solve
595 | Attack
596 | ProofState | ProofTerm | Undo
597 | Try (PTactic' t) (PTactic' t)
598 | TSeq (PTactic' t) (PTactic' t)
599 | Qed | Abandon
600 deriving (Show, Eq, Functor)
601{-!
602deriving instance Binary PTactic'
603!-}
605instance Sized a => Sized (PTactic' a) where
606 size (Intro nms) = 1 + size nms
607 size Intros = 1
608 size (Focus nm) = 1 + size nm
609 size (Refine nm bs) = 1 + size nm + length bs
610 size (Rewrite t) = 1 + size t
611 size (LetTac nm t) = 1 + size nm + size t
612 size (Exact t) = 1 + size t
613 size Compute = 1
614 size Trivial = 1
615 size Solve = 1
616 size Attack = 1
617 size ProofState = 1
618 size ProofTerm = 1
619 size Undo = 1
620 size (Try l r) = 1 + size l + size r
621 size (TSeq l r) = 1 + size l + size r
622 size Qed = 1
623 size Abandon = 1
625type PTactic = PTactic' PTerm
627data PDo' t = DoExp FC t
628 | DoBind FC Name t
629 | DoBindP FC t t
630 | DoLet FC Name t t
631 | DoLetP FC t t
632 deriving (Eq, Functor)
633{-!
634deriving instance Binary PDo'
635!-}
637instance Sized a => Sized (PDo' a) where
638 size (DoExp fc t) = 1 + size fc + size t
639 size (DoBind fc nm t) = 1 + size fc + size nm + size t
640 size (DoBindP fc l r) = 1 + size fc + size l + size r
641 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
642 size (DoLetP fc l r) = 1 + size fc + size l + size r
644type PDo = PDo' PTerm
646-- The priority gives a hint as to elaboration order. Best to elaborate
647-- things early which will help give a more concrete type to other
648-- variables, e.g. a before (interpTy a).
650data PArg' t = PImp { priority :: Int,
651 lazyarg :: Bool, pname :: Name, getTm :: t }
652 | PExp { priority :: Int,
653 lazyarg :: Bool, getTm :: t }
654 | PConstraint { priority :: Int,
655 lazyarg :: Bool, getTm :: t }
656 | PTacImplicit { priority :: Int,
657 lazyarg :: Bool, pname :: Name,
658 getScript :: t,
659 getTm :: t }
660 deriving (Show, Eq, Functor)
662instance Sized a => Sized (PArg' a) where
663 size (PImp p l nm trm) = 1 + size nm + size trm
664 size (PExp p l trm) = 1 + size trm
665 size (PConstraint p l trm) = 1 + size trm
666 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
668{-!
669deriving instance Binary PArg'
670!-}
672pimp = PImp 0 True
673pexp = PExp 0 False
674pconst = PConstraint 0 False
675ptacimp = PTacImplicit 0 True
677type PArg = PArg' PTerm
679-- Type class data
681data ClassInfo = CI { instanceName :: Name,
682 class_methods :: [(Name, (FnOpts, PTerm))],
683 class_defaults :: [(Name, Name)], -- method name -> default impl
684 class_params :: [Name],
685 class_instances :: [Name] }
686 deriving Show
687{-!
688deriving instance Binary ClassInfo
689!-}
691data OptInfo = Optimise { collapsible :: Bool,
692 forceable :: [Int], -- argument positions
693 recursive :: [Int] }
694 deriving Show
695{-!
696deriving instance Binary OptInfo
697!-}
700data TypeInfo = TI { con_names :: [Name] }
701 deriving Show
702{-!
703deriving instance Binary TypeInfo
704!-}
706-- Syntactic sugar info
708data DSL' t = DSL { dsl_bind :: t,
709 dsl_return :: t,
710 dsl_apply :: t,
711 dsl_pure :: t,
712 dsl_var :: Maybe t,
713 index_first :: Maybe t,
714 index_next :: Maybe t,
715 dsl_lambda :: Maybe t,
716 dsl_let :: Maybe t
717 }
718 deriving (Show, Functor)
719{-!
720deriving instance Binary DSL'
721!-}
723type DSL = DSL' PTerm
725data SynContext = PatternSyntax | TermSyntax | AnySyntax
726 deriving Show
727{-!
728deriving instance Binary SynContext
729!-}
731data Syntax = Rule [SSymbol] PTerm SynContext
732 deriving Show
733{-!
734deriving instance Binary Syntax
735!-}
737data SSymbol = Keyword Name
738 | Symbol String
739 | Expr Name
740 | SimpleExpr Name
741 deriving Show
742{-!
743deriving instance Binary SSymbol
744!-}
746initDSL = DSL (PRef f (UN ">>="))
747 (PRef f (UN "return"))
748 (PRef f (UN "<$>"))
749 (PRef f (UN "pure"))
750 Nothing
751 Nothing
752 Nothing
753 Nothing
754 Nothing
755 where f = FC "(builtin)" 0
757data SyntaxInfo = Syn { using :: [(Name, PTerm)],
758 syn_params :: [(Name, PTerm)],
759 syn_namespace :: [String],
760 no_imp :: [Name],
761 decoration :: Name -> Name,
762 inPattern :: Bool,
763 dsl_info :: DSL }
764 deriving Show
766defaultSyntax = Syn [] [] [] [] id False initDSL
768expandNS :: SyntaxInfo -> Name -> Name
769expandNS syn n@(NS _ _) = n
770expandNS syn n = case syn_namespace syn of
771 [] -> n
772 xs -> NS n xs
775--- Pretty printing declarations and terms
777instance Show PTerm where
778 show tm = showImp False tm
780instance Pretty PTerm where
781 pretty = prettyImp False
783instance Show PDecl where
784 show d = showDeclImp False d
786instance Show PClause where
787 show c = showCImp True c
789instance Show PData where
790 show d = showDImp False d
792showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
793showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty
794showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
795showDeclImp _ (PData _ _ d) = show d
797showCImp :: Bool -> PClause -> String
798showCImp impl (PClause _ n l ws r w)
799 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
800 ++ " where " ++ show w
801 where
802 showWs [] = ""
803 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
804showCImp impl (PWith _ n l ws r w)
805 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
806 ++ " { " ++ show w ++ " } "
807 where
808 showWs [] = ""
809 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
812showDImp :: Bool -> PData -> String
813showDImp impl (PDatadecl n ty cons)
814 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
815 ++ showSep "\n\t| "
816 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
818getImps :: [PArg] -> [(Name, PTerm)]
819getImps [] = []
820getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
821getImps (_ : xs) = getImps xs
823getExps :: [PArg] -> [PTerm]
824getExps [] = []
825getExps (PExp _ _ tm : xs) = tm : getExps xs
826getExps (_ : xs) = getExps xs
828getConsts :: [PArg] -> [PTerm]
829getConsts [] = []
830getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
831getConsts (_ : xs) = getConsts xs
833getAll :: [PArg] -> [PTerm]
834getAll = map getTm
836prettyImp :: Bool -> PTerm -> Doc
837prettyImp impl = prettySe 10
838 where
839 prettySe p (PQuote r) =
840 if size r > breakingSize then
841 text "![" $$ pretty r <> text "]"
842 else
843 text "![" <> pretty r <> text "]"
844 prettySe p (PRef fc n) =
845 if impl then
846 pretty n
847 else
848 prettyBasic n
849 where
850 prettyBasic n@(UN _) = pretty n
851 prettyBasic (MN _ s) = text s
852 prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
853 prettySe p (PLam n ty sc) =
854 bracket p 2 $
855 if size sc > breakingSize then
856 text "λ" <> pretty n <+> text "=>" $+$ pretty sc
857 else
858 text "λ" <> pretty n <+> text "=>" <+> pretty sc
859 prettySe p (PLet n ty v sc) =
860 bracket p 2 $
861 if size sc > breakingSize then
862 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
863 nest nestingSize (prettySe 10 sc)
864 else
865 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
866 prettySe 10 sc
867 prettySe p (PPi (Exp l s) n ty sc)
868 | n `elem` allNamesIn sc || impl =
869 let open = if l then text "|" <> lparen else lparen in
870 bracket p 2 $
871 if size sc > breakingSize then
872 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
873 st <+> text "->" $+$ prettySe 10 sc
874 else
875 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
876 st <+> text "->" <+> prettySe 10 sc
877 | otherwise =
878 bracket p 2 $
879 if size sc > breakingSize then
880 prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
881 else
882 prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
883 where
884 st =
885 case s of
886 Static -> text "[static]"
887 _ -> empty
888 prettySe p (PPi (Imp l s) n ty sc)
889 | impl =
890 let open = if l then text "|" <> lbrace else lbrace in
891 bracket p 2 $
892 if size sc > breakingSize then
893 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
894 st <+> text "->" <+> prettySe 10 sc
895 else
896 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
897 st <+> text "->" <+> prettySe 10 sc
898 | otherwise = prettySe 10 sc
899 where
900 st =
901 case s of
902 Static -> text $ "[static]"
903 _ -> empty
904 prettySe p (PPi (Constraint _ _) n ty sc) =
905 bracket p 2 $
906 if size sc > breakingSize then
907 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
908 else
909 prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
910 prettySe p (PPi (TacImp _ _ s) n ty sc) =
911 bracket p 2 $
912 if size sc > breakingSize then
913 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
914 rbrace <+> text "->" $+$ prettySe 10 sc
915 else
916 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
917 rbrace <+> text "->" <+> prettySe 10 sc
918 prettySe p (PApp _ (PRef _ f) [])
919 | not impl = pretty f
920 prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
921 | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
922 let [l, r] = getExps args in
923 bracket p 1 $
924 if size r > breakingSize then
925 prettySe 1 l <+> pretty op $+$ prettySe 0 r
926 else
927 prettySe 1 l <+> pretty op <+> prettySe 0 r
928 prettySe p (PApp _ f as) =
929 let args = getExps as in
930 bracket p 1 $
931 prettySe 1 f <+>
932 if impl then
933 foldl fS empty as
934 -- foldr (<+>) empty $ map prettyArgS as
935 else
936 foldl fSe empty args
937 -- foldr (<+>) empty $ map prettyArgSe args
938 where
939 fS l r =
940 if size r > breakingSize then
941 l $+$ nest nestingSize (prettyArgS r)
942 else
943 l <+> prettyArgS r
945 fSe l r =
946 if size r > breakingSize then
947 l $+$ nest nestingSize (prettyArgSe r)
948 else
949 l <+> prettyArgSe r
950 prettySe p (PCase _ scr opts) =
951 text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
952 where
953 prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
955 sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
956 prettySe p (PHidden tm) = text "." <> prettySe 0 tm
957 prettySe p (PRefl _) = text "refl"
958 prettySe p (PResolveTC _) = text "resolvetc"
959 prettySe p (PTrue _) = text "()"
960 prettySe p (PFalse _) = text "_|_"
961 prettySe p (PEq _ l r) =
962 bracket p 2 $
963 if size r > breakingSize then
964 prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
965 else
966 prettySe 10 l <+> text "=" <+> prettySe 10 r
967 prettySe p (PTyped l r) =
968 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
969 prettySe p (PPair _ l r) =
970 if size r > breakingSize then
971 lparen <> prettySe 10 l <> text "," $+$
972 prettySe 10 r <> rparen
973 else
974 lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
975 prettySe p (PDPair _ l t r) =
976 if size r > breakingSize then
977 lparen <> prettySe 10 l <+> text "**" $+$
978 prettySe 10 r <> rparen
979 else
980 lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
981 prettySe p (PAlternative a as) =
982 lparen <> text "|" <> prettyAs <> text "|" <> rparen
983 where
984 prettyAs =
985 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
986 prettySe p PSet = text "Set"
987 prettySe p (PConstant c) = pretty c
988 -- XXX: add pretty for tactics
989 prettySe p (PProof ts) =
990 text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
991 prettySe p (PTactics ts) =
992 text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
993 prettySe p (PMetavar n) = text "?" <> pretty n
994 prettySe p (PReturn f) = text "return"
995 prettySe p PImpossible = text "impossible"
996 prettySe p Placeholder = text "_"
997 prettySe p (PDoBlock _) = text "do block pretty not implemented"
998 prettySe p (PElabError s) = pretty s
1000 prettySe p _ = text "test"
1002 prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
1003 prettyArgS (PExp _ _ tm) = prettyArgSe tm
1004 prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
1005 prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
1007 prettyArgSe arg = prettySe 0 arg
1008 prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1009 prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
1010 prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1012 bracket outer inner doc
1013 | inner > outer = lparen <> doc <> rparen
1014 | otherwise = doc
1016showImp :: Bool -> PTerm -> String
1017showImp impl tm = se 10 tm where
1018 se p (PQuote r) = "![" ++ show r ++ "]"
1019 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
1020 else showbasic n
1021 where showbasic n@(UN _) = show n
1022 showbasic (MN _ s) = s
1023 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1024 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
1025 (if impl then " : " ++ se 10 ty else "") ++ " => "
1026 ++ se 10 sc
1027 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
1028 " in " ++ se 10 sc
1029 se p (PPi (Exp l s) n ty sc)
1030 | n `elem` allNamesIn sc || impl
1031 = bracket p 2 $
1032 if l then "|(" else "(" ++
1033 show n ++ " : " ++ se 10 ty ++
1034 ") " ++ st ++
1035 "-> " ++ se 10 sc
1036 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
1037 where st = case s of
1038 Static -> "[static] "
1039 _ -> ""
1040 se p (PPi (Imp l s) n ty sc)
1041 | impl = bracket p 2 $ if l then "|{" else "{" ++
1042 show n ++ " : " ++ se 10 ty ++
1043 "} " ++ st ++ "-> " ++ se 10 sc
1044 | otherwise = se 10 sc
1045 where st = case s of
1046 Static -> "[static] "
1047 _ -> ""
1048 se p (PPi (Constraint _ _) n ty sc)
1049 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1050 se p (PPi (TacImp _ _ s) n ty sc)
1051 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1052 se p (PApp _ (PRef _ f) [])
1053 | not impl = show f
1054 se p (PApp _ (PRef _ op@(UN (f:_))) args)
1055 | length (getExps args) == 2 && not impl && not (isAlpha f)
1056 = let [l, r] = getExps args in
1057 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
1058 se p (PApp _ f as)
1059 = let args = getExps as in
1060 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
1061 else concatMap seArg args
1062 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
1063 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
1064 se p (PHidden tm) = "." ++ se 0 tm
1065 se p (PRefl _) = "refl"
1066 se p (PResolveTC _) = "resolvetc"
1067 se p (PTrue _) = "()"
1068 se p (PFalse _) = "_|_"
1069 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
1070 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
1071 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
1072 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
1073 se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
1074 se p PSet = "Set"
1075 se p (PConstant c) = show c
1076 se p (PProof ts) = "proof { " ++ show ts ++ "}"
1077 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
1078 se p (PMetavar n) = "?" ++ show n
1079 se p (PReturn f) = "return"
1080 se p PImpossible = "impossible"
1081 se p Placeholder = "_"
1082 se p (PDoBlock _) = "do block show not implemented"
1083 se p (PElabError s) = show s
1084-- se p x = "Not implemented"
1086 sArg (PImp _ _ n tm) = siArg (n, tm)
1087 sArg (PExp _ _ tm) = seArg tm
1088 sArg (PConstraint _ _ tm) = scArg tm
1089 sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
1091 seArg arg = " " ++ se 0 arg
1092 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
1093 scArg val = " {{" ++ se 10 val ++ "}}"
1094 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
1096 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1097 | otherwise = str
1100 PQuote Raw
1101 | PRef FC Name
1102 | PLam Name PTerm PTerm
1103 | PPi Plicity Name PTerm PTerm
1104 | PLet Name PTerm PTerm PTerm
1105 | PTyped PTerm PTerm -- term with explicit type
1106 | PApp FC PTerm [PArg]
1107 | PCase FC PTerm [(PTerm, PTerm)]
1108 | PTrue FC
1109 | PFalse FC
1110 | PRefl FC
1111 | PResolveTC FC
1112 | PEq FC PTerm PTerm
1113 | PPair FC PTerm PTerm
1114 | PDPair FC PTerm PTerm PTerm
1115 | PAlternative [PTerm]
1116 | PHidden PTerm -- irrelevant or hidden pattern
1117 | PSet
1118 | PConstant Const
1119 | Placeholder
1120 | PDoBlock [PDo]
1121 | PIdiom FC PTerm
1122 | PReturn FC
1123 | PMetavar Name
1124 | PProof [PTactic]
1125 | PTactics [PTactic] -- as PProof, but no auto solving
1126 | PElabError Err -- error to report on elaboration
1127 | PImpossible -- special case for declaring when an LHS can't typecheck
1130instance Sized PTerm where
1131 size (PQuote rawTerm) = size rawTerm
1132 size (PRef fc name) = size name
1133 size (PLam name ty bdy) = 1 + size ty + size bdy
1134 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1135 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1136 size (PTyped trm ty) = 1 + size trm + size ty
1137 size (PApp fc name args) = 1 + size args
1138 size (PCase fc trm bdy) = 1 + size trm + size bdy
1139 size (PTrue fc) = 1
1140 size (PFalse fc) = 1
1141 size (PRefl fc) = 1
1142 size (PResolveTC fc) = 1
1143 size (PEq fc left right) = 1 + size left + size right
1144 size (PPair fc left right) = 1 + size left + size right
1145 size (PDPair fs left ty right) = 1 + size left + size ty + size right
1146 size (PAlternative a alts) = 1 + size alts
1147 size (PHidden hidden) = size hidden
1148 size PSet = 1
1149 size (PConstant const) = 1 + size const
1150 size Placeholder = 1
1151 size (PDoBlock dos) = 1 + size dos
1152 size (PIdiom fc term) = 1 + size term
1153 size (PReturn fc) = 1
1154 size (PMetavar name) = 1
1155 size (PProof tactics) = size tactics
1156 size (PElabError err) = size err
1157 size PImpossible = 1
1159allNamesIn :: PTerm -> [Name]
1160allNamesIn tm = nub $ ni [] tm
1161 where
1162 ni env (PRef _ n)
1163 | not (n `elem` env) = [n]
1164 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1165 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1166 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1167 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1168 ni env (PHidden tm) = ni env tm
1169 ni env (PEq _ l r) = ni env l ++ ni env r
1170 ni env (PTyped l r) = ni env l ++ ni env r
1171 ni env (PPair _ l r) = ni env l ++ ni env r
1172 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1173 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1174 ni env (PAlternative a ls) = concatMap (ni env) ls
1175 ni env _ = []
1177namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1178namesIn uvars ist tm = nub $ ni [] tm
1179 where
1180 ni env (PRef _ n)
1181 | not (n `elem` env)
1182 = case lookupTy Nothing n (tt_ctxt ist) of
1183 [] -> [n]
1184 _ -> if n `elem` (map fst uvars) then [n] else []
1185 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1186 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1187 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1188 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1189 ni env (PEq _ l r) = ni env l ++ ni env r
1190 ni env (PTyped l r) = ni env l ++ ni env r
1191 ni env (PPair _ l r) = ni env l ++ ni env r
1192 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1193 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1194 ni env (PAlternative a as) = concatMap (ni env) as
1195 ni env (PHidden tm) = ni env tm
1196 ni env _ = []
1198-- For inferring types of things
1200bi = FC "builtin" 0
1202inferTy = MN 0 "__Infer"
1203inferCon = MN 0 "__infer"
1204inferDecl = PDatadecl inferTy
1205 PSet
1206 [(inferCon, PPi impl (MN 0 "A") PSet (
1207 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
1208 (PRef bi inferTy)), bi)]
1210infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
1211infP = P (TCon 6 0) inferTy (Set (UVal 0))
1213getInferTerm, getInferType :: Term -> Term
1214getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1215getInferTerm (App (App _ _) tm) = tm
1216getInferTerm tm = error ("getInferTerm " ++ show tm)
1218getInferType (Bind n b sc) = Bind n b $ getInferType sc
1219getInferType (App (App _ ty) _) = ty
1221-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1223primNames = [unitTy, unitCon,
1224 falseTy, pairTy, pairCon,
1225 eqTy, eqCon, inferTy, inferCon]
1227unitTy = MN 0 "__Unit"
1228unitCon = MN 0 "__II"
1229unitDecl = PDatadecl unitTy PSet
1230 [(unitCon, PRef bi unitTy, bi)]
1232falseTy = MN 0 "__False"
1233falseDecl = PDatadecl falseTy PSet []
1235pairTy = MN 0 "__Pair"
1236pairCon = MN 0 "__MkPair"
1237pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
1238 [(pairCon, PPi impl (n "A") PSet (
1239 PPi impl (n "B") PSet (
1240 PPi expl (n "a") (PRef bi (n "A")) (
1241 PPi expl (n "b") (PRef bi (n "B"))
1242 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1243 pexp (PRef bi (n "B"))])))), bi)]
1244 where n a = MN 0 a
1246eqTy = UN "="
1247eqCon = UN "refl"
1248eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
1249 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
1250 PSet)
1251 [(eqCon, PPi impl (n "a") PSet (
1252 PPi impl (n "x") (PRef bi (n "a"))
1253 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
1254 pimp (n "b") Placeholder,
1255 pexp (PRef bi (n "x")),
1256 pexp (PRef bi (n "x"))])), bi)]
1257 where n a = MN 0 a
1259-- Defined in builtins.idr
1260sigmaTy = UN "Exists"
1261existsCon = UN "Ex_intro"
1263piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1264piBind [] t = t
1265piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
1267tcname (UN ('@':_)) = True
1268tcname (NS n _) = tcname n
1269tcname _ = False
1271-- Dealing with parameters
1273expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1274expandParams dec ps ns tm = en tm
1275 where
1276 -- if we shadow a name (say in a lambda binding) that is used in a call to
1277 -- a lifted function, we need access to both names - once in the scope of the
1278 -- binding and once to call the lifted functions. So we'll explicitly shadow
1279 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1280 -- but we didn't...)
1282 mkShadow (UN n) = MN 0 n
1283 mkShadow (MN i n) = MN (i+1) n
1284 mkShadow (NS x s) = NS (mkShadow x) s
1286 en (PLam n t s)
1287 | n `elem` map fst ps
1288 = let n' = mkShadow n in
1289 PLam n' (en t) (en (shadow n n' s))
1290 | otherwise = PLam n (en t) (en s)
1291 en (PPi p n t s)
1292 | n `elem` map fst ps
1293 = let n' = mkShadow n in
1294 PPi p n' (en t) (en (shadow n n' s))
1295 | otherwise = PPi p n (en t) (en s)
1296 en (PLet n ty v s)
1297 | n `elem` map fst ps
1298 = let n' = mkShadow n in
1299 PLet n' (en ty) (en v) (en (shadow n n' s))
1300 | otherwise = PLet n (en ty) (en v) (en s)
1301 en (PEq f l r) = PEq f (en l) (en r)
1302 en (PTyped l r) = PTyped (en l) (en r)
1303 en (PPair f l r) = PPair f (en l) (en r)
1304 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
1305 en (PAlternative a as) = PAlternative a (map en as)
1306 en (PHidden t) = PHidden (en t)
1307 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
1308 en (PProof ts) = PProof (map (fmap en) ts)
1309 en (PTactics ts) = PTactics (map (fmap en) ts)
1311 en (PQuote (Var n))
1312 | n `elem` ns = PQuote (Var (dec n))
1313 en (PApp fc (PRef fc' n) as)
1314 | n `elem` ns = PApp fc (PRef fc' (dec n))
1315 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1316 en (PRef fc n)
1317 | n `elem` ns = PApp fc (PRef fc (dec n))
1318 (map (pexp . (PRef fc)) (map fst ps))
1319 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1320 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1321 en t = t
1323expandParamsD :: IState ->
1324 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1325expandParamsD ist dec ps ns (PTy syn fc o n ty)
1326 = if n `elem` ns
1327 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
1328 else PTy syn fc o n (expandParams dec ps ns ty)
1329expandParamsD ist dec ps ns (PClauses fc opts n cs)
1330 = let n' = if n `elem` ns then dec n else n in
1331 PClauses fc opts n' (map expandParamsC cs)
1332 where
1333 expandParamsC (PClause fc n lhs ws rhs ds)
1334 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1335 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1336 n' = if n `elem` ns then dec n else n in
1337 PClause fc n' (expandParams dec ps'' ns lhs)
1338 (map (expandParams dec ps'' ns) ws)
1339 (expandParams dec ps'' ns rhs)
1340 (map (expandParamsD ist dec ps'' ns) ds)
1341 expandParamsC (PWith fc n lhs ws wval ds)
1342 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1343 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1344 n' = if n `elem` ns then dec n else n in
1345 PWith fc n' (expandParams dec ps'' ns lhs)
1346 (map (expandParams dec ps'' ns) ws)
1347 (expandParams dec ps'' ns wval)
1348 (map (expandParamsD ist dec ps'' ns) ds)
1349 updateps yn nm [] = []
1350 updateps yn nm (((a, t), i):as)
1351 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1352 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
1354expandParamsD ist dec ps ns d = d
1356-- Calculate a priority for a type, for deciding elaboration order
1357-- * if it's just a type variable or concrete type, do it early (0)
1358-- * if there's only type variables and injective constructors, do it next (1)
1359-- * if there's a function type, next (2)
1360-- * finally, everything else (3)
1362getPriority :: IState -> PTerm -> Int
1363getPriority i tm = pri tm
1364 where
1365 pri (PRef _ n) =
1366 case lookupP Nothing n (tt_ctxt i) of
1367 ((P (DCon _ _) _ _):_) -> 1
1368 ((P (TCon _ _) _ _):_) -> 1
1369 ((P Ref _ _):_) -> 4
1370 [] -> 0 -- must be locally bound, if it's not an error...
1371 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1372 pri (PTrue _) = 0
1373 pri (PFalse _) = 0
1374 pri (PRefl _) = 1
1375 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1376 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1377 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1378 pri (PTyped l r) = pri l
1379 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
1380 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1381 pri (PAlternative a as) = maximum (map pri as)
1382 pri (PConstant _) = 0
1383 pri Placeholder = 1
1384 pri _ = 3
1386addStatics :: Name -> Term -> PTerm -> Idris ()
1387addStatics n tm ptm =
1388 do let (statics, dynamics) = initStatics tm ptm
1389 let stnames = nub $ concatMap freeNames (map snd statics)
1390 let dnames = nub $ concatMap freeNames (map snd dynamics)
1391 when (not (null statics)) $
1392 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
1393 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1394 let statics' = nub $ map fst statics ++
1395 filter (\x -> not (elem x dnames)) stnames
1396 let stpos = staticList statics' tm
1397 i <- get
1398 put (i { idris_statics = addDef n stpos (idris_statics i) })
1399 addIBC (IBCStatic n)
1400 where
1401 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1402 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1403 if pstatic p == Static then ((n, ty) : static, dynamic)
1404 else (static, (n, ty) : dynamic)
1405 initStatics t pt = ([], [])
1407 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1408 staticList _ _ = []
1410-- Dealing with implicit arguments
1412-- Add implicit Pi bindings for any names in the term which appear in an
1413-- argument position.
1415-- This has become a right mess already. Better redo it some time...
1417implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1418implicit syn n ptm
1419 = do i <- get
1420 let (tm', impdata) = implicitise syn i ptm
1421-- let (tm'', spos) = findStatics i tm'
1422 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
1423 addIBC (IBCImp n)
1424 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1425-- i <- get
1426-- put (i { idris_statics = addDef n spos (idris_statics i) })
1427 return tm'
1429implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
1430implicitise syn ist tm
1431 = let (declimps, ns') = execState (imps True [] tm) ([], [])
1432 ns = ns' \\ (map fst pvars ++ no_imp syn) in
1433 if null ns
1434 then (tm, reverse declimps)
1435 else implicitise syn ist (pibind uvars ns tm)
1436 where
1437 uvars = using syn
1438 pvars = syn_params syn
1440 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1441 | otherwise = x : dropAll xs ys
1442 dropAll [] ys = []
1444 imps top env (PApp _ f as)
1445 = do (decls, ns) <- get
1446 let isn = concatMap (namesIn uvars ist) (map getTm as)
1447 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1448 imps top env (PPi (Imp l _) n ty sc)
1449 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1450 (decls , ns) <- get
1451 put (PImp (getPriority ist ty) l n ty : decls,
1452 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1453 imps True (n:env) sc
1454 imps top env (PPi (Exp l _) n ty sc)
1455 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1456 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1457 _ -> [])
1458 (decls, ns) <- get -- ignore decls in HO types
1459 put (PExp (getPriority ist ty) l ty : decls,
1460 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1461 imps True (n:env) sc
1462 imps top env (PPi (Constraint l _) n ty sc)
1463 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1464 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1465 _ -> [])
1466 (decls, ns) <- get -- ignore decls in HO types
1467 put (PConstraint 10 l ty : decls,
1468 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1469 imps True (n:env) sc
1470 imps top env (PPi (TacImp l _ scr) n ty sc)
1471 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1472 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1473 _ -> [])
1474 (decls, ns) <- get -- ignore decls in HO types
1475 put (PTacImplicit 10 l n scr ty : decls,
1476 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1477 imps True (n:env) sc
1478 imps top env (PEq _ l r)
1479 = do (decls, ns) <- get
1480 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1481 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1482 imps top env (PTyped l r)
1483 = imps top env l
1484 imps top env (PPair _ l r)
1485 = do (decls, ns) <- get
1486 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1487 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1488 imps top env (PDPair _ (PRef _ n) t r)
1489 = do (decls, ns) <- get
1490 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1491 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1492 imps top env (PDPair _ l t r)
1493 = do (decls, ns) <- get
1494 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1495 namesIn uvars ist r
1496 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1497 imps top env (PAlternative a as)
1498 = do (decls, ns) <- get
1499 let isn = concatMap (namesIn uvars ist) as
1500 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1501 imps top env (PLam n ty sc)
1502 = do imps False env ty
1503 imps False (n:env) sc
1504 imps top env (PHidden tm) = imps False env tm
1505 imps top env _ = return ()
1507 pibind using [] sc = sc
1508 pibind using (n:ns) sc
1509 = case lookup n using of
1510 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
1511 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
1513-- Add implicit arguments in function calls
1514addImplPat :: IState -> PTerm -> PTerm
1515addImplPat = addImpl' True []
1517addImplBound :: IState -> [Name] -> PTerm -> PTerm
1518addImplBound ist ns = addImpl' False ns ist
1520addImpl :: IState -> PTerm -> PTerm
1521addImpl = addImpl' False []
1523-- TODO: in patterns, don't add implicits to function names guarded by constructors
1524-- and *not* inside a PHidden
1526addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1527addImpl' inpat env ist ptm = ai env ptm
1528 where
1529 ai env (PRef fc f)
1530 | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []
1531 ai env (PHidden (PRef fc f))
1532 | not (f `elem` env) = handleErr $ aiFn False ist fc f []
1533 ai env (PEq fc l r) = let l' = ai env l
1534 r' = ai env r in
1535 PEq fc l' r'
1536 ai env (PTyped l r) = let l' = ai env l
1537 r' = ai env r in
1538 PTyped l' r'
1539 ai env (PPair fc l r) = let l' = ai env l
1540 r' = ai env r in
1541 PPair fc l' r'
1542 ai env (PDPair fc l t r) = let l' = ai env l
1543 t' = ai env t
1544 r' = ai env r in
1545 PDPair fc l' t' r'
1546 ai env (PAlternative a as) = let as' = map (ai env) as in
1547 PAlternative a as'
1548 ai env (PApp fc (PRef _ f) as)
1549 | not (f `elem` env)
1550 = let as' = map (fmap (ai env)) as in
1551 handleErr $ aiFn False ist fc f as'
1552 ai env (PApp fc f as) = let f' = ai env f
1553 as' = map (fmap (ai env)) as in
1554 mkPApp fc 1 f' as'
1555 ai env (PCase fc c os) = let c' = ai env c
1556 os' = map (pmap (ai env)) os in
1557 PCase fc c' os'
1558 ai env (PLam n ty sc) = let ty' = ai env ty
1559 sc' = ai (n:env) sc in
1560 PLam n ty' sc'
1561 ai env (PLet n ty val sc)
1562 = let ty' = ai env ty
1563 val' = ai env val
1564 sc' = ai (n:env) sc in
1565 PLet n ty' val' sc'
1566 ai env (PPi p n ty sc) = let ty' = ai env ty
1567 sc' = ai (n:env) sc in
1568 PPi p n ty' sc'
1569 ai env (PHidden tm) = PHidden (ai env tm)
1570 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1571 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1572 ai env tm = tm
1574 handleErr (Left err) = PElabError err
1575 handleErr (Right x) = x
1577-- if in a pattern, and there are no arguments, and there's no possible
1578-- names with zero explicit arguments, don't add implicits.
1580aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1581aiFn True ist fc f []
1582 = case lookupCtxt Nothing f (idris_implicits ist) of
1583 [] -> Right $ PRef fc f
1584 alts -> if (any (all imp) alts)
1585 then aiFn False ist fc f [] -- use it as a constructor
1586 else Right $ PRef fc f
1587 where imp (PExp _ _ _) = False
1588 imp _ = True
1589aiFn inpat ist fc f as
1590 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1591aiFn inpat ist fc f as
1592 -- This is where namespaces get resolved by adding PAlternative
1593 = case lookupCtxtName Nothing f (idris_implicits ist) of
1594 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1595 [] -> if f `elem` idris_metavars ist
1596 then Right $ PApp fc (PRef fc f) as
1597 else Right $ mkPApp fc (length as) (PRef fc f) as
1598 alts -> Right $
1599 PAlternative True $
1600 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1601 (insertImpl ns as)) alts
1602 where
1603 insertImpl :: [PArg] -> [PArg] -> [PArg]
1604 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1605 PExp p l tm : insertImpl ps given
1606 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1607 PConstraint p l tm : insertImpl ps given
1608 insertImpl (PConstraint p l ty : ps) given =
1609 PConstraint p l (PResolveTC fc) : insertImpl ps given
1610 insertImpl (PImp p l n ty : ps) given =
1611 case find n given [] of
1612 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
1613 Nothing -> PImp p l n Placeholder : insertImpl ps given
1614 insertImpl (PTacImplicit p l n sc ty : ps) given =
1615 case find n given [] of
1616 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1617 Nothing -> PTacImplicit p l n sc sc
1618 : insertImpl ps given
1619 insertImpl expected [] = []
1620 insertImpl _ given = given
1622 find n [] acc = Nothing
1623 find n (PImp _ _ n' t : gs) acc
1624 | n == n' = Just (t, reverse acc ++ gs)
1625 find n (g : gs) acc = find n gs (g : acc)
1627mkPApp fc a f [] = f
1628mkPApp fc a f as = let rest = drop a as in
1629 appRest fc (PApp fc f (take a as)) rest
1630 where
1631 appRest fc f [] = f
1632 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1634-- Find 'static' argument positions
1635-- (the declared ones, plus any names in argument position in the declared
1636-- statics)
1637-- FIXME: It's possible that this really has to happen after elaboration
1639findStatics :: IState -> PTerm -> (PTerm, [Bool])
1640findStatics ist tm = trace (showImp True tm) $
1641 let (ns, ss) = fs tm in
1642 runState (pos ns ss tm) []
1643 where fs (PPi p n t sc)
1644 | Static <- pstatic p
1645 = let (ns, ss) = fs sc in
1646 (namesIn [] ist t : ns, n : ss)
1647 | otherwise = let (ns, ss) = fs sc in
1648 (ns, ss)
1649 fs _ = ([], [])
1651 inOne n ns = length (filter id (map (elem n) ns)) == 1
1653 pos ns ss (PPi p n t sc)
1654 | elem n ss = do sc' <- pos ns ss sc
1655 spos <- get
1656 put (True : spos)
1657 return (PPi (p { pstatic = Static }) n t sc')
1658 | otherwise = do sc' <- pos ns ss sc
1659 spos <- get
1660 put (False : spos)
1661 return (PPi p n t sc')
1662 pos ns ss t = return t
1664-- Debugging/logging stuff
1666dumpDecls :: [PDecl] -> String
1667dumpDecls [] = ""
1668dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1670dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1671dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1672dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1673dumpDecl (PData _ _ d) = showDImp True d
1674dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1675dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1676dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1677dumpDecl (PClass _ _ cs n ps ds)
1678 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1679dumpDecl (PInstance _ _ cs n _ t ds)
1680 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1681dumpDecl _ = "..."
1682-- dumpDecl (PImport i) = "import " ++ i
1684-- for 6.12/7 compatibility
1685data EitherErr a b = LeftErr a | RightOK b
1687instance Monad (EitherErr a) where
1688 return = RightOK
1690 (LeftErr e) >>= k = LeftErr e
1691 RightOK v >>= k = k v
1693toEither (LeftErr e) = Left e
1694toEither (RightOK ho) = Right ho
1696-- syntactic match of a against b, returning pair of variables in a
1697-- and what they match. Returns the pair that failed if not a match.
1699matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1700matchClause = matchClause' False
1702matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1703matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1704 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1706 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1707 fullApp x = x
1709 match' x y = match (fullApp x) (fullApp y)
1710 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1711 | PConstant (I _) <- getTm x = match (getTm x) x'
1712 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1713 | PConstant (I _) <- getTm x = match (getTm x) x'
1714 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1715 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1716 match (PApp _ f args) (PApp _ f' args')
1717 | length args == length args'
1718 = do mf <- match' f f'
1719 ms <- zipWithM matchArg args args'
1720 return (mf ++ concat ms)
1721-- match (PRef _ n) (PRef _ n') | n == n' = return []
1722-- | otherwise = Nothing
1723 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1724 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1725 match (PRef _ n) (PRef _ n') | n == n' = return []
1726 match (PRef _ n) tm
1727 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1728 = return [(n, tm)]
1729 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1730 mr <- match' r r'
1731 return (ml ++ mr)
1732 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1733 mr <- match r r'
1734 return (ml ++ mr)
1735 match (PTyped l r) x = match l x
1736 match x (PTyped l r) = match x l
1737 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1738 mr <- match' r r'
1739 return (ml ++ mr)
1740 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1741 mt <- match' t t'
1742 mr <- match' r r'
1743 return (ml ++ mt ++ mr)
1744 match (PAlternative a as) (PAlternative a' as')
1745 = do ms <- zipWithM match' as as'
1746 return (concat ms)
1747 match a@(PAlternative _ as) b
1748 = do let ms = zipWith match' as (repeat b)
1749 case (rights (map toEither ms)) of
1750 (x: _) -> return x
1751 _ -> LeftErr (a, b)
1752 match (PCase _ _ _) _ = return [] -- lifted out
1753 match (PMetavar _) _ = return [] -- modified
1754 match (PQuote _) _ = return []
1755 match (PProof _) _ = return []
1756 match (PTactics _) _ = return []
1757 match (PRefl _) (PRefl _) = return []
1758 match (PResolveTC _) (PResolveTC _) = return []
1759 match (PTrue _) (PTrue _) = return []
1760 match (PFalse _) (PFalse _) = return []
1761 match (PReturn _) (PReturn _) = return []
1762 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1763 ms <- match' s s'
1764 return (mt ++ ms)
1765 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1766 ms <- match' s s'
1767 return (mt ++ ms)
1768 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1769 mty <- match' ty ty'
1770 ms <- match' s s'
1771 return (mt ++ mty ++ ms)
1772 match (PHidden x) (PHidden y) = match' x y
1773 match Placeholder _ = return []
1774-- match _ Placeholder = return []
1775 match (PResolveTC _) _ = return []
1776 match a b | a == b = return []
1777 | otherwise = LeftErr (a, b)
1779 checkRpts (RightOK ms) = check ms where
1780 check ((n,t):xs)
1781 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1782 then Left (t, t')
1783 else check xs
1784 check (_:xs) = check xs
1785 check [] = Right ms
1786 checkRpts (LeftErr x) = Left x
1788substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1789substMatches [] t = t
1790substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1792substMatch :: Name -> PTerm -> PTerm -> PTerm
1793substMatch n tm t = sm t where
1794 sm (PRef _ n') | n == n' = tm
1795 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1796 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1797 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1798 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1799 sm (PEq f x y) = PEq f (sm x) (sm y)
1800 sm (PTyped x y) = PTyped (sm x) (sm y)
1801 sm (PPair f x y) = PPair f (sm x) (sm y)
1802 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1803 sm (PAlternative a as) = PAlternative a (map sm as)
1804 sm (PHidden x) = PHidden (sm x)
1805 sm x = x
1807shadow :: Name -> Name -> PTerm -> PTerm
1808shadow n n' t = sm t where
1809 sm (PRef fc x) | n == x = PRef fc n'
1810 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1811 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1812 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1813 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1814 sm (PEq f x y) = PEq f (sm x) (sm y)
1815 sm (PTyped x y) = PTyped (sm x) (sm y)
1816 sm (PPair f x y) = PPair f (sm x) (sm y)
1817 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1818 sm (PAlternative a as) = PAlternative a (map sm as)
1819 sm (PHidden x) = PHidden (sm x)
1820 sm x = x