git.iko.soy/Idris-dev
on da674d3 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1805 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 [(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 | Info Name
370 | NOP
372-- Parsed declarations
374data Fixity = Infixl { prec :: Int }
375 | Infixr { prec :: Int }
376 | InfixN { prec :: Int }
377 | PrefixN { prec :: Int }
378 deriving Eq
379{-!
380deriving instance Binary Fixity
381!-}
383instance Show Fixity where
384 show (Infixl i) = "infixl " ++ show i
385 show (Infixr i) = "infixr " ++ show i
386 show (InfixN i) = "infix " ++ show i
387 show (PrefixN i) = "prefix " ++ show i
389data FixDecl = Fix Fixity String
390 deriving (Show, Eq)
391{-!
392deriving instance Binary FixDecl
393!-}
395instance Ord FixDecl where
396 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
399data Static = Static | Dynamic
400 deriving (Show, Eq)
401{-!
402deriving instance Binary Static
403!-}
405-- Mark bindings with their explicitness, and laziness
406data Plicity = Imp { plazy :: Bool,
407 pstatic :: Static }
408 | Exp { plazy :: Bool,
409 pstatic :: Static }
410 | Constraint { plazy :: Bool,
411 pstatic :: Static }
412 | TacImp { plazy :: Bool,
413 pstatic :: Static,
414 pscript :: PTerm }
415 deriving (Show, Eq)
417{-!
418deriving instance Binary Plicity
419!-}
421impl = Imp False Dynamic
422expl = Exp False Dynamic
423constraint = Constraint False Dynamic
424tacimpl = TacImp False Dynamic
426data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
427 | Specialise [Name] -- specialise it, freeze these names
428 deriving (Show, Eq)
429{-!
430deriving instance Binary FnOpt
431!-}
433type FnOpts = [FnOpt]
435inlinable :: FnOpts -> Bool
436inlinable = elem Inlinable
438data PDecl' t = PFix FC Fixity [String] -- fixity declaration
439 | PTy SyntaxInfo FC FnOpts Name t -- type declaration
440 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
441 | PData SyntaxInfo FC (PData' t) -- data declaration
442 | PParams FC [(Name, t)] [PDecl' t] -- params block
443 | PNamespace String [PDecl' t] -- new namespace
444 | PRecord SyntaxInfo FC Name t Name t -- record declaration
445 | PClass SyntaxInfo FC
446 [t] -- constraints
447 Name
448 [(Name, t)] -- parameters
449 [PDecl' t] -- declarations
450 | PInstance SyntaxInfo FC [t] -- constraints
451 Name -- class
452 [t] -- parameters
453 t -- full instance type
454 [PDecl' t]
455 | PDSL Name (DSL' t)
456 | PSyntax FC Syntax
457 | PDirective (Idris ())
458 deriving Functor
460data PClause' t = PClause FC Name t [t] t [PDecl' t]
461 | PWith FC Name t [t] t [PDecl' t]
462 | PClauseR FC [t] t [PDecl' t]
463 | PWithR FC [t] t [PDecl' t]
464 deriving Functor
466data PData' t = PDatadecl { d_name :: Name,
467 d_tcon :: t,
468 d_cons :: [(Name, t, FC)] }
469 deriving Functor
471-- Handy to get a free function for applying PTerm -> PTerm functions
472-- across a program, by deriving Functor
474type PDecl = PDecl' PTerm
475type PData = PData' PTerm
476type PClause = PClause' PTerm
478-- get all the names declared in a decl
480declared :: PDecl -> [Name]
481declared (PFix _ _ _) = []
482declared (PTy _ _ _ n t) = [n]
483declared (PClauses _ _ n _) = [] -- not a declaration
484declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
485 where fstt (a, _, _) = a
486declared (PParams _ _ ds) = concatMap declared ds
487declared (PNamespace _ ds) = concatMap declared ds
488-- declared (PImport _) = []
490defined :: PDecl -> [Name]
491defined (PFix _ _ _) = []
492defined (PTy _ _ _ n t) = []
493defined (PClauses _ _ n _) = [n] -- not a declaration
494defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
495 where fstt (a, _, _) = a
496defined (PParams _ _ ds) = concatMap defined ds
497defined (PNamespace _ ds) = concatMap defined ds
498-- declared (PImport _) = []
500updateN :: [(Name, Name)] -> Name -> Name
501updateN ns n | Just n' <- lookup n ns = n'
502updateN _ n = n
504updateNs :: [(Name, Name)] -> PTerm -> PTerm
505updateNs [] t = t
506updateNs ns t = mapPT updateRef t
507 where updateRef (PRef fc f) = PRef fc (updateN ns f)
508 updateRef t = t
510-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
511-- updateDNs [] t = t
512-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
513-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
514-- where updateCNs ns (PClause n l ts r ds)
515-- = PClause (updateN ns n) (fmap (updateNs ns) l)
516-- (map (fmap (updateNs ns)) ts)
517-- (fmap (updateNs ns) r)
518-- (map (updateDNs ns) ds)
519-- updateDNs ns c = c
521-- High level language terms
523data PTerm = PQuote Raw
524 | PRef FC Name
525 | PLam Name PTerm PTerm
526 | PPi Plicity Name PTerm PTerm
527 | PLet Name PTerm PTerm PTerm
528 | PTyped PTerm PTerm -- term with explicit type
529 | PApp FC PTerm [PArg]
530 | PCase FC PTerm [(PTerm, PTerm)]
531 | PTrue FC
532 | PFalse FC
533 | PRefl FC
534 | PResolveTC FC
535 | PEq FC PTerm PTerm
536 | PPair FC PTerm PTerm
537 | PDPair FC PTerm PTerm PTerm
538 | PAlternative [PTerm]
539 | PHidden PTerm -- irrelevant or hidden pattern
540 | PSet
541 | PConstant Const
542 | Placeholder
543 | PDoBlock [PDo]
544 | PIdiom FC PTerm
545 | PReturn FC
546 | PMetavar Name
547 | PProof [PTactic]
548 | PTactics [PTactic] -- as PProof, but no auto solving
549 | PElabError Err -- error to report on elaboration
550 | PImpossible -- special case for declaring when an LHS can't typecheck
551 deriving Eq
552{-!
553deriving instance Binary PTerm
554!-}
556mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
557mapPT f t = f (mpt t) where
558 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
559 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
560 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
561 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
562 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
563 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
564 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
565 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
566 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
567 mpt (PAlternative as) = PAlternative (map (mapPT f) as)
568 mpt (PHidden t) = PHidden (mapPT f t)
569 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
570 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
571 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
572 mpt x = x
575data PTactic' t = Intro [Name] | Intros | Focus Name
576 | Refine Name [Bool] | Rewrite t | LetTac Name t
577 | Exact t | Compute | Trivial
578 | Solve
579 | Attack
580 | ProofState | ProofTerm | Undo
581 | Try (PTactic' t) (PTactic' t)
582 | TSeq (PTactic' t) (PTactic' t)
583 | Qed | Abandon
584 deriving (Show, Eq, Functor)
585{-!
586deriving instance Binary PTactic'
587!-}
589instance Sized a => Sized (PTactic' a) where
590 size (Intro nms) = 1 + size nms
591 size Intros = 1
592 size (Focus nm) = 1 + size nm
593 size (Refine nm bs) = 1 + size nm + length bs
594 size (Rewrite t) = 1 + size t
595 size (LetTac nm t) = 1 + size nm + size t
596 size (Exact t) = 1 + size t
597 size Compute = 1
598 size Trivial = 1
599 size Solve = 1
600 size Attack = 1
601 size ProofState = 1
602 size ProofTerm = 1
603 size Undo = 1
604 size (Try l r) = 1 + size l + size r
605 size (TSeq l r) = 1 + size l + size r
606 size Qed = 1
607 size Abandon = 1
609type PTactic = PTactic' PTerm
611data PDo' t = DoExp FC t
612 | DoBind FC Name t
613 | DoBindP FC t t
614 | DoLet FC Name t t
615 | DoLetP FC t t
616 deriving (Eq, Functor)
617{-!
618deriving instance Binary PDo'
619!-}
621instance Sized a => Sized (PDo' a) where
622 size (DoExp fc t) = 1 + size fc + size t
623 size (DoBind fc nm t) = 1 + size fc + size nm + size t
624 size (DoBindP fc l r) = 1 + size fc + size l + size r
625 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
626 size (DoLetP fc l r) = 1 + size fc + size l + size r
628type PDo = PDo' PTerm
630-- The priority gives a hint as to elaboration order. Best to elaborate
631-- things early which will help give a more concrete type to other
632-- variables, e.g. a before (interpTy a).
634data PArg' t = PImp { priority :: Int,
635 lazyarg :: Bool, pname :: Name, getTm :: t }
636 | PExp { priority :: Int,
637 lazyarg :: Bool, getTm :: t }
638 | PConstraint { priority :: Int,
639 lazyarg :: Bool, getTm :: t }
640 | PTacImplicit { priority :: Int,
641 lazyarg :: Bool, pname :: Name,
642 getScript :: t,
643 getTm :: t }
644 deriving (Show, Eq, Functor)
646instance Sized a => Sized (PArg' a) where
647 size (PImp p l nm trm) = 1 + size nm + size trm
648 size (PExp p l trm) = 1 + size trm
649 size (PConstraint p l trm) = 1 + size trm
650 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
652{-!
653deriving instance Binary PArg'
654!-}
656pimp = PImp 0 True
657pexp = PExp 0 False
658pconst = PConstraint 0 False
659ptacimp = PTacImplicit 0 True
661type PArg = PArg' PTerm
663-- Type class data
665data ClassInfo = CI { instanceName :: Name,
666 class_methods :: [(Name, (FnOpts, PTerm))],
667 class_defaults :: [(Name, Name)], -- method name -> default impl
668 class_params :: [Name],
669 class_instances :: [Name] }
670 deriving Show
671{-!
672deriving instance Binary ClassInfo
673!-}
675data OptInfo = Optimise { collapsible :: Bool,
676 forceable :: [Int], -- argument positions
677 recursive :: [Int] }
678 deriving Show
679{-!
680deriving instance Binary OptInfo
681!-}
684data TypeInfo = TI { con_names :: [Name] }
685 deriving Show
686{-!
687deriving instance Binary TypeInfo
688!-}
690-- Syntactic sugar info
692data DSL' t = DSL { dsl_bind :: t,
693 dsl_return :: t,
694 dsl_apply :: t,
695 dsl_pure :: t,
696 dsl_var :: Maybe t,
697 index_first :: Maybe t,
698 index_next :: Maybe t,
699 dsl_lambda :: Maybe t,
700 dsl_let :: Maybe t
701 }
702 deriving (Show, Functor)
703{-!
704deriving instance Binary DSL'
705!-}
707type DSL = DSL' PTerm
709data SynContext = PatternSyntax | TermSyntax | AnySyntax
710 deriving Show
711{-!
712deriving instance Binary SynContext
713!-}
715data Syntax = Rule [SSymbol] PTerm SynContext
716 deriving Show
717{-!
718deriving instance Binary Syntax
719!-}
721data SSymbol = Keyword Name
722 | Symbol String
723 | Expr Name
724 | SimpleExpr Name
725 deriving Show
726{-!
727deriving instance Binary SSymbol
728!-}
730initDSL = DSL (PRef f (UN ">>="))
731 (PRef f (UN "return"))
732 (PRef f (UN "<$>"))
733 (PRef f (UN "pure"))
734 Nothing
735 Nothing
736 Nothing
737 Nothing
738 Nothing
739 where f = FC "(builtin)" 0
741data SyntaxInfo = Syn { using :: [(Name, PTerm)],
742 syn_params :: [(Name, PTerm)],
743 syn_namespace :: [String],
744 no_imp :: [Name],
745 decoration :: Name -> Name,
746 inPattern :: Bool,
747 dsl_info :: DSL }
748 deriving Show
750defaultSyntax = Syn [] [] [] [] id False initDSL
752expandNS :: SyntaxInfo -> Name -> Name
753expandNS syn n@(NS _ _) = n
754expandNS syn n = case syn_namespace syn of
755 [] -> n
756 xs -> NS n xs
759--- Pretty printing declarations and terms
761instance Show PTerm where
762 show tm = showImp False tm
764instance Pretty PTerm where
765 pretty = prettyImp False
767instance Show PDecl where
768 show d = showDeclImp False d
770instance Show PClause where
771 show c = showCImp True c
773instance Show PData where
774 show d = showDImp False d
776showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
777showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty
778showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
779showDeclImp _ (PData _ _ d) = show d
781showCImp :: Bool -> PClause -> String
782showCImp impl (PClause _ n l ws r w)
783 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
784 ++ " where " ++ show w
785 where
786 showWs [] = ""
787 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
788showCImp impl (PWith _ n l ws r w)
789 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
790 ++ " { " ++ show w ++ " } "
791 where
792 showWs [] = ""
793 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
796showDImp :: Bool -> PData -> String
797showDImp impl (PDatadecl n ty cons)
798 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
799 ++ showSep "\n\t| "
800 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
802getImps :: [PArg] -> [(Name, PTerm)]
803getImps [] = []
804getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
805getImps (_ : xs) = getImps xs
807getExps :: [PArg] -> [PTerm]
808getExps [] = []
809getExps (PExp _ _ tm : xs) = tm : getExps xs
810getExps (_ : xs) = getExps xs
812getConsts :: [PArg] -> [PTerm]
813getConsts [] = []
814getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
815getConsts (_ : xs) = getConsts xs
817getAll :: [PArg] -> [PTerm]
818getAll = map getTm
820prettyImp :: Bool -> PTerm -> Doc
821prettyImp impl = prettySe 10
822 where
823 prettySe p (PQuote r) =
824 if size r > breakingSize then
825 text "![" $$ pretty r <> text "]"
826 else
827 text "![" <> pretty r <> text "]"
828 prettySe p (PRef fc n) =
829 if impl then
830 pretty n
831 else
832 prettyBasic n
833 where
834 prettyBasic n@(UN _) = pretty n
835 prettyBasic (MN _ s) = text s
836 prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
837 prettySe p (PLam n ty sc) =
838 bracket p 2 $
839 if size sc > breakingSize then
840 text "λ" <> pretty n <+> text "=>" $+$ pretty sc
841 else
842 text "λ" <> pretty n <+> text "=>" <+> pretty sc
843 prettySe p (PLet n ty v sc) =
844 bracket p 2 $
845 if size sc > breakingSize then
846 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
847 nest nestingSize (prettySe 10 sc)
848 else
849 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
850 prettySe 10 sc
851 prettySe p (PPi (Exp l s) n ty sc)
852 | n `elem` allNamesIn sc || impl =
853 let open = if l then text "|" <> lparen else lparen in
854 bracket p 2 $
855 if size sc > breakingSize then
856 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
857 st <+> text "->" $+$ prettySe 10 sc
858 else
859 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
860 st <+> text "->" <+> prettySe 10 sc
861 | otherwise =
862 bracket p 2 $
863 if size sc > breakingSize then
864 prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
865 else
866 prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
867 where
868 st =
869 case s of
870 Static -> text "[static]"
871 _ -> empty
872 prettySe p (PPi (Imp l s) n ty sc)
873 | impl =
874 let open = if l then text "|" <> lbrace else lbrace in
875 bracket p 2 $
876 if size sc > breakingSize then
877 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
878 st <+> text "->" <+> prettySe 10 sc
879 else
880 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
881 st <+> text "->" <+> prettySe 10 sc
882 | otherwise = prettySe 10 sc
883 where
884 st =
885 case s of
886 Static -> text $ "[static]"
887 _ -> empty
888 prettySe p (PPi (Constraint _ _) n ty sc) =
889 bracket p 2 $
890 if size sc > breakingSize then
891 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
892 else
893 prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
894 prettySe p (PPi (TacImp _ _ s) n ty sc) =
895 bracket p 2 $
896 if size sc > breakingSize then
897 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
898 rbrace <+> text "->" $+$ prettySe 10 sc
899 else
900 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
901 rbrace <+> text "->" <+> prettySe 10 sc
902 prettySe p (PApp _ (PRef _ f) [])
903 | not impl = pretty f
904 prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
905 | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
906 let [l, r] = getExps args in
907 bracket p 1 $
908 if size r > breakingSize then
909 prettySe 1 l <+> pretty op $+$ prettySe 0 r
910 else
911 prettySe 1 l <+> pretty op <+> prettySe 0 r
912 prettySe p (PApp _ f as) =
913 let args = getExps as in
914 bracket p 1 $
915 prettySe 1 f <+>
916 if impl then
917 foldl fS empty as
918 -- foldr (<+>) empty $ map prettyArgS as
919 else
920 foldl fSe empty args
921 -- foldr (<+>) empty $ map prettyArgSe args
922 where
923 fS l r =
924 if size r > breakingSize then
925 l $+$ nest nestingSize (prettyArgS r)
926 else
927 l <+> prettyArgS r
929 fSe l r =
930 if size r > breakingSize then
931 l $+$ nest nestingSize (prettyArgSe r)
932 else
933 l <+> prettyArgSe r
934 prettySe p (PCase _ scr opts) =
935 text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
936 where
937 prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
939 sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
940 prettySe p (PHidden tm) = text "." <> prettySe 0 tm
941 prettySe p (PRefl _) = text "refl"
942 prettySe p (PResolveTC _) = text "resolvetc"
943 prettySe p (PTrue _) = text "()"
944 prettySe p (PFalse _) = text "_|_"
945 prettySe p (PEq _ l r) =
946 bracket p 2 $
947 if size r > breakingSize then
948 prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
949 else
950 prettySe 10 l <+> text "=" <+> prettySe 10 r
951 prettySe p (PTyped l r) =
952 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
953 prettySe p (PPair _ l r) =
954 if size r > breakingSize then
955 lparen <> prettySe 10 l <> text "," $+$
956 prettySe 10 r <> rparen
957 else
958 lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
959 prettySe p (PDPair _ l t r) =
960 if size r > breakingSize then
961 lparen <> prettySe 10 l <+> text "**" $+$
962 prettySe 10 r <> rparen
963 else
964 lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
965 prettySe p (PAlternative as) =
966 lparen <> text "|" <> prettyAs <> text "|" <> rparen
967 where
968 prettyAs =
969 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
970 prettySe p PSet = text "Set"
971 prettySe p (PConstant c) = pretty c
972 -- XXX: add pretty for tactics
973 prettySe p (PProof ts) =
974 text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
975 prettySe p (PTactics ts) =
976 text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
977 prettySe p (PMetavar n) = text "?" <> pretty n
978 prettySe p (PReturn f) = text "return"
979 prettySe p PImpossible = text "impossible"
980 prettySe p Placeholder = text "_"
981 prettySe p (PDoBlock _) = text "do block pretty not implemented"
982 prettySe p (PElabError s) = pretty s
984 prettySe p _ = text "test"
986 prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
987 prettyArgS (PExp _ _ tm) = prettyArgSe tm
988 prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
989 prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
991 prettyArgSe arg = prettySe 0 arg
992 prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
993 prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
994 prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
996 bracket outer inner doc
997 | inner > outer = lparen <> doc <> rparen
998 | otherwise = doc
1000showImp :: Bool -> PTerm -> String
1001showImp impl tm = se 10 tm where
1002 se p (PQuote r) = "![" ++ show r ++ "]"
1003 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
1004 else showbasic n
1005 where showbasic n@(UN _) = show n
1006 showbasic (MN _ s) = s
1007 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1008 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
1009 (if impl then " : " ++ se 10 ty else "") ++ " => "
1010 ++ se 10 sc
1011 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
1012 " in " ++ se 10 sc
1013 se p (PPi (Exp l s) n ty sc)
1014 | n `elem` allNamesIn sc || impl
1015 = bracket p 2 $
1016 if l then "|(" else "(" ++
1017 show n ++ " : " ++ se 10 ty ++
1018 ") " ++ st ++
1019 "-> " ++ se 10 sc
1020 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
1021 where st = case s of
1022 Static -> "[static] "
1023 _ -> ""
1024 se p (PPi (Imp l s) n ty sc)
1025 | impl = bracket p 2 $ if l then "|{" else "{" ++
1026 show n ++ " : " ++ se 10 ty ++
1027 "} " ++ st ++ "-> " ++ se 10 sc
1028 | otherwise = se 10 sc
1029 where st = case s of
1030 Static -> "[static] "
1031 _ -> ""
1032 se p (PPi (Constraint _ _) n ty sc)
1033 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1034 se p (PPi (TacImp _ _ s) n ty sc)
1035 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1036 se p (PApp _ (PRef _ f) [])
1037 | not impl = show f
1038 se p (PApp _ (PRef _ op@(UN (f:_))) args)
1039 | length (getExps args) == 2 && not impl && not (isAlpha f)
1040 = let [l, r] = getExps args in
1041 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
1042 se p (PApp _ f as)
1043 = let args = getExps as in
1044 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
1045 else concatMap seArg args
1046 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
1047 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
1048 se p (PHidden tm) = "." ++ se 0 tm
1049 se p (PRefl _) = "refl"
1050 se p (PResolveTC _) = "resolvetc"
1051 se p (PTrue _) = "()"
1052 se p (PFalse _) = "_|_"
1053 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
1054 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
1055 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
1056 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
1057 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
1058 se p PSet = "Set"
1059 se p (PConstant c) = show c
1060 se p (PProof ts) = "proof { " ++ show ts ++ "}"
1061 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
1062 se p (PMetavar n) = "?" ++ show n
1063 se p (PReturn f) = "return"
1064 se p PImpossible = "impossible"
1065 se p Placeholder = "_"
1066 se p (PDoBlock _) = "do block show not implemented"
1067 se p (PElabError s) = show s
1068-- se p x = "Not implemented"
1070 sArg (PImp _ _ n tm) = siArg (n, tm)
1071 sArg (PExp _ _ tm) = seArg tm
1072 sArg (PConstraint _ _ tm) = scArg tm
1073 sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
1075 seArg arg = " " ++ se 0 arg
1076 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
1077 scArg val = " {{" ++ se 10 val ++ "}}"
1078 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
1080 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1081 | otherwise = str
1084 PQuote Raw
1085 | PRef FC Name
1086 | PLam Name PTerm PTerm
1087 | PPi Plicity Name PTerm PTerm
1088 | PLet Name PTerm PTerm PTerm
1089 | PTyped PTerm PTerm -- term with explicit type
1090 | PApp FC PTerm [PArg]
1091 | PCase FC PTerm [(PTerm, PTerm)]
1092 | PTrue FC
1093 | PFalse FC
1094 | PRefl FC
1095 | PResolveTC FC
1096 | PEq FC PTerm PTerm
1097 | PPair FC PTerm PTerm
1098 | PDPair FC PTerm PTerm PTerm
1099 | PAlternative [PTerm]
1100 | PHidden PTerm -- irrelevant or hidden pattern
1101 | PSet
1102 | PConstant Const
1103 | Placeholder
1104 | PDoBlock [PDo]
1105 | PIdiom FC PTerm
1106 | PReturn FC
1107 | PMetavar Name
1108 | PProof [PTactic]
1109 | PTactics [PTactic] -- as PProof, but no auto solving
1110 | PElabError Err -- error to report on elaboration
1111 | PImpossible -- special case for declaring when an LHS can't typecheck
1114instance Sized PTerm where
1115 size (PQuote rawTerm) = size rawTerm
1116 size (PRef fc name) = size name
1117 size (PLam name ty bdy) = 1 + size ty + size bdy
1118 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1119 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1120 size (PTyped trm ty) = 1 + size trm + size ty
1121 size (PApp fc name args) = 1 + size args
1122 size (PCase fc trm bdy) = 1 + size trm + size bdy
1123 size (PTrue fc) = 1
1124 size (PFalse fc) = 1
1125 size (PRefl fc) = 1
1126 size (PResolveTC fc) = 1
1127 size (PEq fc left right) = 1 + size left + size right
1128 size (PPair fc left right) = 1 + size left + size right
1129 size (PDPair fs left ty right) = 1 + size left + size ty + size right
1130 size (PAlternative alts) = 1 + size alts
1131 size (PHidden hidden) = size hidden
1132 size PSet = 1
1133 size (PConstant const) = 1 + size const
1134 size Placeholder = 1
1135 size (PDoBlock dos) = 1 + size dos
1136 size (PIdiom fc term) = 1 + size term
1137 size (PReturn fc) = 1
1138 size (PMetavar name) = 1
1139 size (PProof tactics) = size tactics
1140 size (PElabError err) = size err
1141 size PImpossible = 1
1143allNamesIn :: PTerm -> [Name]
1144allNamesIn tm = nub $ ni [] tm
1145 where
1146 ni env (PRef _ n)
1147 | not (n `elem` env) = [n]
1148 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1149 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1150 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1151 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1152 ni env (PHidden tm) = ni env tm
1153 ni env (PEq _ l r) = ni env l ++ ni env r
1154 ni env (PTyped l r) = ni env l ++ ni env r
1155 ni env (PPair _ l r) = ni env l ++ ni env r
1156 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1157 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1158 ni env (PAlternative ls) = concatMap (ni env) ls
1159 ni env _ = []
1161namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1162namesIn uvars ist tm = nub $ ni [] tm
1163 where
1164 ni env (PRef _ n)
1165 | not (n `elem` env)
1166 = case lookupTy Nothing n (tt_ctxt ist) of
1167 [] -> [n]
1168 _ -> if n `elem` (map fst uvars) then [n] else []
1169 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1170 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1171 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1172 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1173 ni env (PEq _ l r) = ni env l ++ ni env r
1174 ni env (PTyped l r) = ni env l ++ ni env r
1175 ni env (PPair _ l r) = ni env l ++ ni env r
1176 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1177 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1178 ni env (PAlternative as) = concatMap (ni env) as
1179 ni env (PHidden tm) = ni env tm
1180 ni env _ = []
1182-- For inferring types of things
1184bi = FC "builtin" 0
1186inferTy = MN 0 "__Infer"
1187inferCon = MN 0 "__infer"
1188inferDecl = PDatadecl inferTy
1189 PSet
1190 [(inferCon, PPi impl (MN 0 "A") PSet (
1191 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
1192 (PRef bi inferTy)), bi)]
1194infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
1195infP = P (TCon 6 0) inferTy (Set (UVal 0))
1197getInferTerm, getInferType :: Term -> Term
1198getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1199getInferTerm (App (App _ _) tm) = tm
1200getInferTerm tm = error ("getInferTerm " ++ show tm)
1202getInferType (Bind n b sc) = Bind n b $ getInferType sc
1203getInferType (App (App _ ty) _) = ty
1205-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1207primNames = [unitTy, unitCon,
1208 falseTy, pairTy, pairCon,
1209 eqTy, eqCon, inferTy, inferCon]
1211unitTy = MN 0 "__Unit"
1212unitCon = MN 0 "__II"
1213unitDecl = PDatadecl unitTy PSet
1214 [(unitCon, PRef bi unitTy, bi)]
1216falseTy = MN 0 "__False"
1217falseDecl = PDatadecl falseTy PSet []
1219pairTy = MN 0 "__Pair"
1220pairCon = MN 0 "__MkPair"
1221pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
1222 [(pairCon, PPi impl (n "A") PSet (
1223 PPi impl (n "B") PSet (
1224 PPi expl (n "a") (PRef bi (n "A")) (
1225 PPi expl (n "b") (PRef bi (n "B"))
1226 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1227 pexp (PRef bi (n "B"))])))), bi)]
1228 where n a = MN 0 a
1230eqTy = UN "="
1231eqCon = UN "refl"
1232eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
1233 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
1234 PSet)
1235 [(eqCon, PPi impl (n "a") PSet (
1236 PPi impl (n "x") (PRef bi (n "a"))
1237 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
1238 pimp (n "b") Placeholder,
1239 pexp (PRef bi (n "x")),
1240 pexp (PRef bi (n "x"))])), bi)]
1241 where n a = MN 0 a
1243-- Defined in builtins.idr
1244sigmaTy = UN "Exists"
1245existsCon = UN "Ex_intro"
1247piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1248piBind [] t = t
1249piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
1251tcname (UN ('@':_)) = True
1252tcname (NS n _) = tcname n
1253tcname _ = False
1255-- Dealing with parameters
1257expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1258expandParams dec ps ns tm = en tm
1259 where
1260 -- if we shadow a name (say in a lambda binding) that is used in a call to
1261 -- a lifted function, we need access to both names - once in the scope of the
1262 -- binding and once to call the lifted functions. So we'll explicitly shadow
1263 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1264 -- but we didn't...)
1266 mkShadow (UN n) = MN 0 n
1267 mkShadow (MN i n) = MN (i+1) n
1268 mkShadow (NS x s) = NS (mkShadow x) s
1270 en (PLam n t s)
1271 | n `elem` map fst ps
1272 = let n' = mkShadow n in
1273 PLam n' (en t) (en (shadow n n' s))
1274 | otherwise = PLam n (en t) (en s)
1275 en (PPi p n t s)
1276 | n `elem` map fst ps
1277 = let n' = mkShadow n in
1278 PPi p n' (en t) (en (shadow n n' s))
1279 | otherwise = PPi p n (en t) (en s)
1280 en (PLet n ty v s)
1281 | n `elem` map fst ps
1282 = let n' = mkShadow n in
1283 PLet n' (en ty) (en v) (en (shadow n n' s))
1284 | otherwise = PLet n (en ty) (en v) (en s)
1285 en (PEq f l r) = PEq f (en l) (en r)
1286 en (PTyped l r) = PTyped (en l) (en r)
1287 en (PPair f l r) = PPair f (en l) (en r)
1288 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
1289 en (PAlternative as) = PAlternative (map en as)
1290 en (PHidden t) = PHidden (en t)
1291 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
1292 en (PProof ts) = PProof (map (fmap en) ts)
1293 en (PTactics ts) = PTactics (map (fmap en) ts)
1295 en (PQuote (Var n))
1296 | n `elem` ns = PQuote (Var (dec n))
1297 en (PApp fc (PRef fc' n) as)
1298 | n `elem` ns = PApp fc (PRef fc' (dec n))
1299 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1300 en (PRef fc n)
1301 | n `elem` ns = PApp fc (PRef fc (dec n))
1302 (map (pexp . (PRef fc)) (map fst ps))
1303 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1304 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1305 en t = t
1307expandParamsD :: IState ->
1308 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1309expandParamsD ist dec ps ns (PTy syn fc o n ty)
1310 = if n `elem` ns
1311 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
1312 else PTy syn fc o n (expandParams dec ps ns ty)
1313expandParamsD ist dec ps ns (PClauses fc opts n cs)
1314 = let n' = if n `elem` ns then dec n else n in
1315 PClauses fc opts n' (map expandParamsC cs)
1316 where
1317 expandParamsC (PClause fc n lhs ws rhs ds)
1318 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1319 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1320 n' = if n `elem` ns then dec n else n in
1321 PClause fc n' (expandParams dec ps'' ns lhs)
1322 (map (expandParams dec ps'' ns) ws)
1323 (expandParams dec ps'' ns rhs)
1324 (map (expandParamsD ist dec ps'' ns) ds)
1325 expandParamsC (PWith fc n lhs ws wval ds)
1326 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1327 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1328 n' = if n `elem` ns then dec n else n in
1329 PWith fc n' (expandParams dec ps'' ns lhs)
1330 (map (expandParams dec ps'' ns) ws)
1331 (expandParams dec ps'' ns wval)
1332 (map (expandParamsD ist dec ps'' ns) ds)
1333 updateps yn nm [] = []
1334 updateps yn nm (((a, t), i):as)
1335 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1336 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
1338expandParamsD ist dec ps ns d = d
1340-- Calculate a priority for a type, for deciding elaboration order
1341-- * if it's just a type variable or concrete type, do it early (0)
1342-- * if there's only type variables and injective constructors, do it next (1)
1343-- * if there's a function type, next (2)
1344-- * finally, everything else (3)
1346getPriority :: IState -> PTerm -> Int
1347getPriority i tm = pri tm
1348 where
1349 pri (PRef _ n) =
1350 case lookupP Nothing n (tt_ctxt i) of
1351 ((P (DCon _ _) _ _):_) -> 1
1352 ((P (TCon _ _) _ _):_) -> 1
1353 ((P Ref _ _):_) -> 4
1354 [] -> 0 -- must be locally bound, if it's not an error...
1355 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1356 pri (PTrue _) = 0
1357 pri (PFalse _) = 0
1358 pri (PRefl _) = 1
1359 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1360 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1361 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1362 pri (PTyped l r) = pri l
1363 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
1364 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1365 pri (PAlternative as) = maximum (map pri as)
1366 pri (PConstant _) = 0
1367 pri Placeholder = 1
1368 pri _ = 3
1370addStatics :: Name -> Term -> PTerm -> Idris ()
1371addStatics n tm ptm =
1372 do let (statics, dynamics) = initStatics tm ptm
1373 let stnames = nub $ concatMap freeNames (map snd statics)
1374 let dnames = nub $ concatMap freeNames (map snd dynamics)
1375 when (not (null statics)) $
1376 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
1377 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1378 let statics' = nub $ map fst statics ++
1379 filter (\x -> not (elem x dnames)) stnames
1380 let stpos = staticList statics' tm
1381 i <- get
1382 put (i { idris_statics = addDef n stpos (idris_statics i) })
1383 addIBC (IBCStatic n)
1384 where
1385 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1386 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1387 if pstatic p == Static then ((n, ty) : static, dynamic)
1388 else (static, (n, ty) : dynamic)
1389 initStatics t pt = ([], [])
1391 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1392 staticList _ _ = []
1394-- Dealing with implicit arguments
1396-- Add implicit Pi bindings for any names in the term which appear in an
1397-- argument position.
1399-- This has become a right mess already. Better redo it some time...
1401implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1402implicit syn n ptm
1403 = do i <- get
1404 let (tm', impdata) = implicitise syn i ptm
1405-- let (tm'', spos) = findStatics i tm'
1406 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
1407 addIBC (IBCImp n)
1408 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1409-- i <- get
1410-- put (i { idris_statics = addDef n spos (idris_statics i) })
1411 return tm'
1413implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
1414implicitise syn ist tm
1415 = let (declimps, ns') = execState (imps True [] tm) ([], [])
1416 ns = ns' \\ (map fst pvars ++ no_imp syn) in
1417 if null ns
1418 then (tm, reverse declimps)
1419 else implicitise syn ist (pibind uvars ns tm)
1420 where
1421 uvars = using syn
1422 pvars = syn_params syn
1424 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1425 | otherwise = x : dropAll xs ys
1426 dropAll [] ys = []
1428 imps top env (PApp _ f as)
1429 = do (decls, ns) <- get
1430 let isn = concatMap (namesIn uvars ist) (map getTm as)
1431 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1432 imps top env (PPi (Imp l _) n ty sc)
1433 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1434 (decls , ns) <- get
1435 put (PImp (getPriority ist ty) l n ty : decls,
1436 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1437 imps True (n:env) sc
1438 imps top env (PPi (Exp l _) n ty sc)
1439 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1440 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1441 _ -> [])
1442 (decls, ns) <- get -- ignore decls in HO types
1443 put (PExp (getPriority ist ty) l ty : decls,
1444 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1445 imps True (n:env) sc
1446 imps top env (PPi (Constraint l _) n ty sc)
1447 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1448 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1449 _ -> [])
1450 (decls, ns) <- get -- ignore decls in HO types
1451 put (PConstraint 10 l ty : decls,
1452 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1453 imps True (n:env) sc
1454 imps top env (PPi (TacImp l _ scr) n ty sc)
1455 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1456 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1457 _ -> [])
1458 (decls, ns) <- get -- ignore decls in HO types
1459 put (PTacImplicit 10 l n scr ty : decls,
1460 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1461 imps True (n:env) sc
1462 imps top env (PEq _ l r)
1463 = do (decls, ns) <- get
1464 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1465 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1466 imps top env (PTyped l r)
1467 = imps top env l
1468 imps top env (PPair _ l r)
1469 = do (decls, ns) <- get
1470 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1471 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1472 imps top env (PDPair _ (PRef _ n) t r)
1473 = do (decls, ns) <- get
1474 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1475 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1476 imps top env (PDPair _ l t r)
1477 = do (decls, ns) <- get
1478 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1479 namesIn uvars ist r
1480 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1481 imps top env (PAlternative as)
1482 = do (decls, ns) <- get
1483 let isn = concatMap (namesIn uvars ist) as
1484 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1485 imps top env (PLam n ty sc)
1486 = do imps False env ty
1487 imps False (n:env) sc
1488 imps top env (PHidden tm) = imps False env tm
1489 imps top env _ = return ()
1491 pibind using [] sc = sc
1492 pibind using (n:ns) sc
1493 = case lookup n using of
1494 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
1495 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
1497-- Add implicit arguments in function calls
1498addImplPat :: IState -> PTerm -> PTerm
1499addImplPat = addImpl' True []
1501addImplBound :: IState -> [Name] -> PTerm -> PTerm
1502addImplBound ist ns = addImpl' False ns ist
1504addImpl :: IState -> PTerm -> PTerm
1505addImpl = addImpl' False []
1507-- TODO: in patterns, don't add implicits to function names guarded by constructors
1508-- and *not* inside a PHidden
1510addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1511addImpl' inpat env ist ptm = ai env ptm
1512 where
1513 ai env (PRef fc f)
1514 | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []
1515 ai env (PHidden (PRef fc f))
1516 | not (f `elem` env) = handleErr $ aiFn False ist fc f []
1517 ai env (PEq fc l r) = let l' = ai env l
1518 r' = ai env r in
1519 PEq fc l' r'
1520 ai env (PTyped l r) = let l' = ai env l
1521 r' = ai env r in
1522 PTyped l' r'
1523 ai env (PPair fc l r) = let l' = ai env l
1524 r' = ai env r in
1525 PPair fc l' r'
1526 ai env (PDPair fc l t r) = let l' = ai env l
1527 t' = ai env t
1528 r' = ai env r in
1529 PDPair fc l' t' r'
1530 ai env (PAlternative as) = let as' = map (ai env) as in
1531 PAlternative as'
1532 ai env (PApp fc (PRef _ f) as)
1533 | not (f `elem` env)
1534 = let as' = map (fmap (ai env)) as in
1535 handleErr $ aiFn False ist fc f as'
1536 ai env (PApp fc f as) = let f' = ai env f
1537 as' = map (fmap (ai env)) as in
1538 mkPApp fc 1 f' as'
1539 ai env (PCase fc c os) = let c' = ai env c
1540 os' = map (pmap (ai env)) os in
1541 PCase fc c' os'
1542 ai env (PLam n ty sc) = let ty' = ai env ty
1543 sc' = ai (n:env) sc in
1544 PLam n ty' sc'
1545 ai env (PLet n ty val sc)
1546 = let ty' = ai env ty
1547 val' = ai env val
1548 sc' = ai (n:env) sc in
1549 PLet n ty' val' sc'
1550 ai env (PPi p n ty sc) = let ty' = ai env ty
1551 sc' = ai (n:env) sc in
1552 PPi p n ty' sc'
1553 ai env (PHidden tm) = PHidden (ai env tm)
1554 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1555 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1556 ai env tm = tm
1558 handleErr (Left err) = PElabError err
1559 handleErr (Right x) = x
1561-- if in a pattern, and there are no arguments, and there's no possible
1562-- names with zero explicit arguments, don't add implicits.
1564aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1565aiFn True ist fc f []
1566 = case lookupCtxt Nothing f (idris_implicits ist) of
1567 [] -> Right $ PRef fc f
1568 alts -> if (any (all imp) alts)
1569 then aiFn False ist fc f [] -- use it as a constructor
1570 else Right $ PRef fc f
1571 where imp (PExp _ _ _) = False
1572 imp _ = True
1573aiFn inpat ist fc f as
1574 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1575aiFn inpat ist fc f as
1576 -- This is where namespaces get resolved by adding PAlternative
1577 = case lookupCtxtName Nothing f (idris_implicits ist) of
1578 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1579 [] -> if f `elem` idris_metavars ist
1580 then Right $ PApp fc (PRef fc f) as
1581 else Right $ mkPApp fc (length as) (PRef fc f) as
1582 alts -> Right $
1583 PAlternative $
1584 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1585 (insertImpl ns as)) alts
1586 where
1587 insertImpl :: [PArg] -> [PArg] -> [PArg]
1588 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1589 PExp p l tm : insertImpl ps given
1590 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1591 PConstraint p l tm : insertImpl ps given
1592 insertImpl (PConstraint p l ty : ps) given =
1593 PConstraint p l (PResolveTC fc) : insertImpl ps given
1594 insertImpl (PImp p l n ty : ps) given =
1595 case find n given [] of
1596 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
1597 Nothing -> PImp p l n Placeholder : insertImpl ps given
1598 insertImpl (PTacImplicit p l n sc ty : ps) given =
1599 case find n given [] of
1600 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1601 Nothing -> PTacImplicit p l n sc sc
1602 : insertImpl ps given
1603 insertImpl expected [] = []
1604 insertImpl _ given = given
1606 find n [] acc = Nothing
1607 find n (PImp _ _ n' t : gs) acc
1608 | n == n' = Just (t, reverse acc ++ gs)
1609 find n (g : gs) acc = find n gs (g : acc)
1611mkPApp fc a f [] = f
1612mkPApp fc a f as = let rest = drop a as in
1613 appRest fc (PApp fc f (take a as)) rest
1614 where
1615 appRest fc f [] = f
1616 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1618-- Find 'static' argument positions
1619-- (the declared ones, plus any names in argument position in the declared
1620-- statics)
1621-- FIXME: It's possible that this really has to happen after elaboration
1623findStatics :: IState -> PTerm -> (PTerm, [Bool])
1624findStatics ist tm = trace (showImp True tm) $
1625 let (ns, ss) = fs tm in
1626 runState (pos ns ss tm) []
1627 where fs (PPi p n t sc)
1628 | Static <- pstatic p
1629 = let (ns, ss) = fs sc in
1630 (namesIn [] ist t : ns, n : ss)
1631 | otherwise = let (ns, ss) = fs sc in
1632 (ns, ss)
1633 fs _ = ([], [])
1635 inOne n ns = length (filter id (map (elem n) ns)) == 1
1637 pos ns ss (PPi p n t sc)
1638 | elem n ss = do sc' <- pos ns ss sc
1639 spos <- get
1640 put (True : spos)
1641 return (PPi (p { pstatic = Static }) n t sc')
1642 | otherwise = do sc' <- pos ns ss sc
1643 spos <- get
1644 put (False : spos)
1645 return (PPi p n t sc')
1646 pos ns ss t = return t
1648-- Debugging/logging stuff
1650dumpDecls :: [PDecl] -> String
1651dumpDecls [] = ""
1652dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1654dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1655dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1656dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1657dumpDecl (PData _ _ d) = showDImp True d
1658dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1659dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1660dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1661dumpDecl (PClass _ _ cs n ps ds)
1662 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1663dumpDecl (PInstance _ _ cs n _ t ds)
1664 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1665dumpDecl _ = "..."
1666-- dumpDecl (PImport i) = "import " ++ i
1668-- for 6.12/7 compatibility
1669data EitherErr a b = LeftErr a | RightOK b
1671instance Monad (EitherErr a) where
1672 return = RightOK
1674 (LeftErr e) >>= k = LeftErr e
1675 RightOK v >>= k = k v
1677toEither (LeftErr e) = Left e
1678toEither (RightOK ho) = Right ho
1680-- syntactic match of a against b, returning pair of variables in a
1681-- and what they match. Returns the pair that failed if not a match.
1683matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1684matchClause = matchClause' False
1686matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1687matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1688 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1690 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1691 fullApp x = x
1693 match' x y = match (fullApp x) (fullApp y)
1694 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1695 | PConstant (I _) <- getTm x = match (getTm x) x'
1696 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1697 | PConstant (I _) <- getTm x = match (getTm x) x'
1698 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1699 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1700 match (PApp _ f args) (PApp _ f' args')
1701 | length args == length args'
1702 = do mf <- match' f f'
1703 ms <- zipWithM matchArg args args'
1704 return (mf ++ concat ms)
1705-- match (PRef _ n) (PRef _ n') | n == n' = return []
1706-- | otherwise = Nothing
1707 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1708 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1709 match (PRef _ n) (PRef _ n') | n == n' = return []
1710 match (PRef _ n) tm
1711 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1712 = return [(n, tm)]
1713 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1714 mr <- match' r r'
1715 return (ml ++ mr)
1716 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1717 mr <- match r r'
1718 return (ml ++ mr)
1719 match (PTyped l r) x = match l x
1720 match x (PTyped l r) = match x l
1721 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1722 mr <- match' r r'
1723 return (ml ++ mr)
1724 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1725 mt <- match' t t'
1726 mr <- match' r r'
1727 return (ml ++ mt ++ mr)
1728 match (PAlternative as) (PAlternative as')
1729 = do ms <- zipWithM match' as as'
1730 return (concat ms)
1731 match a@(PAlternative as) b
1732 = do let ms = zipWith match' as (repeat b)
1733 case (rights (map toEither ms)) of
1734 (x: _) -> return x
1735 _ -> LeftErr (a, b)
1736 match (PCase _ _ _) _ = return [] -- lifted out
1737 match (PMetavar _) _ = return [] -- modified
1738 match (PQuote _) _ = return []
1739 match (PProof _) _ = return []
1740 match (PTactics _) _ = return []
1741 match (PRefl _) (PRefl _) = return []
1742 match (PResolveTC _) (PResolveTC _) = return []
1743 match (PTrue _) (PTrue _) = return []
1744 match (PFalse _) (PFalse _) = return []
1745 match (PReturn _) (PReturn _) = return []
1746 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1747 ms <- match' s s'
1748 return (mt ++ ms)
1749 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1750 ms <- match' s s'
1751 return (mt ++ ms)
1752 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1753 mty <- match' ty ty'
1754 ms <- match' s s'
1755 return (mt ++ mty ++ ms)
1756 match (PHidden x) (PHidden y) = match' x y
1757 match Placeholder _ = return []
1758-- match _ Placeholder = return []
1759 match (PResolveTC _) _ = return []
1760 match a b | a == b = return []
1761 | otherwise = LeftErr (a, b)
1763 checkRpts (RightOK ms) = check ms where
1764 check ((n,t):xs)
1765 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1766 then Left (t, t')
1767 else check xs
1768 check (_:xs) = check xs
1769 check [] = Right ms
1770 checkRpts (LeftErr x) = Left x
1772substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1773substMatches [] t = t
1774substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1776substMatch :: Name -> PTerm -> PTerm -> PTerm
1777substMatch n tm t = sm t where
1778 sm (PRef _ n') | n == n' = tm
1779 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1780 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1781 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1782 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1783 sm (PEq f x y) = PEq f (sm x) (sm y)
1784 sm (PTyped x y) = PTyped (sm x) (sm y)
1785 sm (PPair f x y) = PPair f (sm x) (sm y)
1786 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1787 sm (PAlternative as) = PAlternative (map sm as)
1788 sm (PHidden x) = PHidden (sm x)
1789 sm x = x
1791shadow :: Name -> Name -> PTerm -> PTerm
1792shadow n n' t = sm t where
1793 sm (PRef fc x) | n == x = PRef fc n'
1794 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1795 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1796 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1797 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1798 sm (PEq f x y) = PEq f (sm x) (sm y)
1799 sm (PTyped x y) = PTyped (sm x) (sm y)
1800 sm (PPair f x y) = PPair f (sm x) (sm y)
1801 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1802 sm (PAlternative as) = PAlternative (map sm as)
1803 sm (PHidden x) = PHidden (sm x)
1804 sm x = x