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