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