git.iko.soy/Idris-dev
on 067f4fa help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1795 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 ++
999 (if impl then " : " ++ se 10 ty else "") ++ " => "
1000 ++ se 10 sc
1001 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
1002 " in " ++ se 10 sc
1003 se p (PPi (Exp l s) n ty sc)
1004 | n `elem` allNamesIn sc || impl
1005 = bracket p 2 $
1006 if l then "|(" else "(" ++
1007 show n ++ " : " ++ se 10 ty ++
1008 ") " ++ st ++
1009 "-> " ++ se 10 sc
1010 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
1011 where st = case s of
1012 Static -> "[static] "
1013 _ -> ""
1014 se p (PPi (Imp l s) n ty sc)
1015 | impl = bracket p 2 $ if l then "|{" else "{" ++
1016 show n ++ " : " ++ se 10 ty ++
1017 "} " ++ st ++ "-> " ++ se 10 sc
1018 | otherwise = se 10 sc
1019 where st = case s of
1020 Static -> "[static] "
1021 _ -> ""
1022 se p (PPi (Constraint _ _) n ty sc)
1023 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1024 se p (PPi (TacImp _ _ s) n ty sc)
1025 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1026 se p (PApp _ (PRef _ f) [])
1027 | not impl = show f
1028 se p (PApp _ (PRef _ op@(UN (f:_))) args)
1029 | length (getExps args) == 2 && not impl && not (isAlpha f)
1030 = let [l, r] = getExps args in
1031 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
1032 se p (PApp _ f as)
1033 = let args = getExps as in
1034 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
1035 else concatMap seArg args
1036 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
1037 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
1038 se p (PHidden tm) = "." ++ se 0 tm
1039 se p (PRefl _) = "refl"
1040 se p (PResolveTC _) = "resolvetc"
1041 se p (PTrue _) = "()"
1042 se p (PFalse _) = "_|_"
1043 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
1044 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
1045 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
1046 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
1047 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
1048 se p PSet = "Set"
1049 se p (PConstant c) = show c
1050 se p (PProof ts) = "proof { " ++ show ts ++ "}"
1051 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
1052 se p (PMetavar n) = "?" ++ show n
1053 se p (PReturn f) = "return"
1054 se p PImpossible = "impossible"
1055 se p Placeholder = "_"
1056 se p (PDoBlock _) = "do block show not implemented"
1057 se p (PElabError s) = show s
1058-- se p x = "Not implemented"
1060 sArg (PImp _ _ n tm) = siArg (n, tm)
1061 sArg (PExp _ _ tm) = seArg tm
1062 sArg (PConstraint _ _ tm) = scArg tm
1063 sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
1065 seArg arg = " " ++ se 0 arg
1066 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
1067 scArg val = " {{" ++ se 10 val ++ "}}"
1068 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
1070 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1071 | otherwise = str
1074 PQuote Raw
1075 | PRef FC Name
1076 | PLam Name PTerm PTerm
1077 | PPi Plicity Name PTerm PTerm
1078 | PLet Name PTerm PTerm PTerm
1079 | PTyped PTerm PTerm -- term with explicit type
1080 | PApp FC PTerm [PArg]
1081 | PCase FC PTerm [(PTerm, PTerm)]
1082 | PTrue FC
1083 | PFalse FC
1084 | PRefl FC
1085 | PResolveTC FC
1086 | PEq FC PTerm PTerm
1087 | PPair FC PTerm PTerm
1088 | PDPair FC PTerm PTerm PTerm
1089 | PAlternative [PTerm]
1090 | PHidden PTerm -- irrelevant or hidden pattern
1091 | PSet
1092 | PConstant Const
1093 | Placeholder
1094 | PDoBlock [PDo]
1095 | PIdiom FC PTerm
1096 | PReturn FC
1097 | PMetavar Name
1098 | PProof [PTactic]
1099 | PTactics [PTactic] -- as PProof, but no auto solving
1100 | PElabError Err -- error to report on elaboration
1101 | PImpossible -- special case for declaring when an LHS can't typecheck
1104instance Sized PTerm where
1105 size (PQuote rawTerm) = size rawTerm
1106 size (PRef fc name) = size name
1107 size (PLam name ty bdy) = 1 + size ty + size bdy
1108 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1109 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1110 size (PTyped trm ty) = 1 + size trm + size ty
1111 size (PApp fc name args) = 1 + size args
1112 size (PCase fc trm bdy) = 1 + size trm + size bdy
1113 size (PTrue fc) = 1
1114 size (PFalse fc) = 1
1115 size (PRefl fc) = 1
1116 size (PResolveTC fc) = 1
1117 size (PEq fc left right) = 1 + size left + size right
1118 size (PPair fc left right) = 1 + size left + size right
1119 size (PDPair fs left ty right) = 1 + size left + size ty + size right
1120 size (PAlternative alts) = 1 + size alts
1121 size (PHidden hidden) = size hidden
1122 size PSet = 1
1123 size (PConstant const) = 1 + size const
1124 size Placeholder = 1
1125 size (PDoBlock dos) = 1 + size dos
1126 size (PIdiom fc term) = 1 + size term
1127 size (PReturn fc) = 1
1128 size (PMetavar name) = 1
1129 size (PProof tactics) = size tactics
1130 size (PElabError err) = size err
1131 size PImpossible = 1
1133allNamesIn :: PTerm -> [Name]
1134allNamesIn tm = nub $ ni [] tm
1135 where
1136 ni env (PRef _ n)
1137 | not (n `elem` env) = [n]
1138 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1139 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1140 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1141 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1142 ni env (PHidden tm) = ni env tm
1143 ni env (PEq _ l r) = ni env l ++ ni env r
1144 ni env (PTyped l r) = ni env l ++ ni env r
1145 ni env (PPair _ l r) = ni env l ++ ni env r
1146 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1147 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1148 ni env (PAlternative ls) = concatMap (ni env) ls
1149 ni env _ = []
1151namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1152namesIn uvars ist tm = nub $ ni [] tm
1153 where
1154 ni env (PRef _ n)
1155 | not (n `elem` env)
1156 = case lookupTy Nothing n (tt_ctxt ist) of
1157 [] -> [n]
1158 _ -> if n `elem` (map fst uvars) then [n] else []
1159 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1160 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1161 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1162 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1163 ni env (PEq _ l r) = ni env l ++ ni env r
1164 ni env (PTyped l r) = ni env l ++ ni env r
1165 ni env (PPair _ l r) = ni env l ++ ni env r
1166 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1167 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1168 ni env (PAlternative as) = concatMap (ni env) as
1169 ni env (PHidden tm) = ni env tm
1170 ni env _ = []
1172-- For inferring types of things
1174bi = FC "builtin" 0
1176inferTy = MN 0 "__Infer"
1177inferCon = MN 0 "__infer"
1178inferDecl = PDatadecl inferTy
1179 PSet
1180 [(inferCon, PPi impl (MN 0 "A") PSet (
1181 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
1182 (PRef bi inferTy)), bi)]
1184infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
1185infP = P (TCon 6 0) inferTy (Set (UVal 0))
1187getInferTerm, getInferType :: Term -> Term
1188getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1189getInferTerm (App (App _ _) tm) = tm
1190getInferTerm tm = error ("getInferTerm " ++ show tm)
1192getInferType (Bind n b sc) = Bind n b $ getInferType sc
1193getInferType (App (App _ ty) _) = ty
1195-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1197primNames = [unitTy, unitCon,
1198 falseTy, pairTy, pairCon,
1199 eqTy, eqCon, inferTy, inferCon]
1201unitTy = MN 0 "__Unit"
1202unitCon = MN 0 "__II"
1203unitDecl = PDatadecl unitTy PSet
1204 [(unitCon, PRef bi unitTy, bi)]
1206falseTy = MN 0 "__False"
1207falseDecl = PDatadecl falseTy PSet []
1209pairTy = MN 0 "__Pair"
1210pairCon = MN 0 "__MkPair"
1211pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
1212 [(pairCon, PPi impl (n "A") PSet (
1213 PPi impl (n "B") PSet (
1214 PPi expl (n "a") (PRef bi (n "A")) (
1215 PPi expl (n "b") (PRef bi (n "B"))
1216 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1217 pexp (PRef bi (n "B"))])))), bi)]
1218 where n a = MN 0 a
1220eqTy = UN "="
1221eqCon = UN "refl"
1222eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),
1223 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
1224 PSet)
1225 [(eqCon, PPi impl (n "a") PSet (
1226 PPi impl (n "x") (PRef bi (n "a"))
1227 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
1228 pimp (n "b") Placeholder,
1229 pexp (PRef bi (n "x")),
1230 pexp (PRef bi (n "x"))])), bi)]
1231 where n a = MN 0 a
1233-- Defined in builtins.idr
1234sigmaTy = UN "Exists"
1235existsCon = UN "Ex_intro"
1237piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1238piBind [] t = t
1239piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)
1241tcname (UN ('@':_)) = True
1242tcname (NS n _) = tcname n
1243tcname _ = False
1245-- Dealing with parameters
1247expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1248expandParams dec ps ns tm = en tm
1249 where
1250 -- if we shadow a name (say in a lambda binding) that is used in a call to
1251 -- a lifted function, we need access to both names - once in the scope of the
1252 -- binding and once to call the lifted functions. So we'll explicitly shadow
1253 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
1254 -- but we didn't...)
1256 mkShadow (UN n) = MN 0 n
1257 mkShadow (MN i n) = MN (i+1) n
1258 mkShadow (NS x s) = NS (mkShadow x) s
1260 en (PLam n t s)
1261 | n `elem` map fst ps
1262 = let n' = mkShadow n in
1263 PLam n' (en t) (en (shadow n n' s))
1264 | otherwise = PLam n (en t) (en s)
1265 en (PPi p n t s)
1266 | n `elem` map fst ps
1267 = let n' = mkShadow n in
1268 PPi p n' (en t) (en (shadow n n' s))
1269 | otherwise = PPi p n (en t) (en s)
1270 en (PLet n ty v s)
1271 | n `elem` map fst ps
1272 = let n' = mkShadow n in
1273 PLet n' (en ty) (en v) (en (shadow n n' s))
1274 | otherwise = PLet n (en ty) (en v) (en s)
1275 en (PEq f l r) = PEq f (en l) (en r)
1276 en (PTyped l r) = PTyped (en l) (en r)
1277 en (PPair f l r) = PPair f (en l) (en r)
1278 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
1279 en (PAlternative as) = PAlternative (map en as)
1280 en (PHidden t) = PHidden (en t)
1281 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
1282 en (PProof ts) = PProof (map (fmap en) ts)
1283 en (PTactics ts) = PTactics (map (fmap en) ts)
1285 en (PQuote (Var n))
1286 | n `elem` ns = PQuote (Var (dec n))
1287 en (PApp fc (PRef fc' n) as)
1288 | n `elem` ns = PApp fc (PRef fc' (dec n))
1289 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
1290 en (PRef fc n)
1291 | n `elem` ns = PApp fc (PRef fc (dec n))
1292 (map (pexp . (PRef fc)) (map fst ps))
1293 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1294 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1295 en t = t
1297expandParamsD :: IState ->
1298 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1299expandParamsD ist dec ps ns (PTy syn fc o n ty)
1300 = if n `elem` ns
1301 then PTy syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
1302 else PTy syn fc o n (expandParams dec ps ns ty)
1303expandParamsD ist dec ps ns (PClauses fc opts n cs)
1304 = let n' = if n `elem` ns then dec n else n in
1305 PClauses fc opts n' (map expandParamsC cs)
1306 where
1307 expandParamsC (PClause fc n lhs ws rhs ds)
1308 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1309 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1310 n' = if n `elem` ns then dec n else n in
1311 PClause fc n' (expandParams dec ps'' ns lhs)
1312 (map (expandParams dec ps'' ns) ws)
1313 (expandParams dec ps'' ns rhs)
1314 (map (expandParamsD ist dec ps'' ns) ds)
1315 expandParamsC (PWith fc n lhs ws wval ds)
1316 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1317 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1318 n' = if n `elem` ns then dec n else n in
1319 PWith fc n' (expandParams dec ps'' ns lhs)
1320 (map (expandParams dec ps'' ns) ws)
1321 (expandParams dec ps'' ns wval)
1322 (map (expandParamsD ist dec ps'' ns) ds)
1323 updateps yn nm [] = []
1324 updateps yn nm (((a, t), i):as)
1325 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1326 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
1328expandParamsD ist dec ps ns d = d
1330-- Calculate a priority for a type, for deciding elaboration order
1331-- * if it's just a type variable or concrete type, do it early (0)
1332-- * if there's only type variables and injective constructors, do it next (1)
1333-- * if there's a function type, next (2)
1334-- * finally, everything else (3)
1336getPriority :: IState -> PTerm -> Int
1337getPriority i tm = pri tm
1338 where
1339 pri (PRef _ n) =
1340 case lookupP Nothing n (tt_ctxt i) of
1341 ((P (DCon _ _) _ _):_) -> 1
1342 ((P (TCon _ _) _ _):_) -> 1
1343 ((P Ref _ _):_) -> 4
1344 [] -> 0 -- must be locally bound, if it's not an error...
1345 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1346 pri (PTrue _) = 0
1347 pri (PFalse _) = 0
1348 pri (PRefl _) = 1
1349 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1350 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1351 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1352 pri (PTyped l r) = pri l
1353 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
1354 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1355 pri (PAlternative as) = maximum (map pri as)
1356 pri (PConstant _) = 0
1357 pri Placeholder = 1
1358 pri _ = 3
1360addStatics :: Name -> Term -> PTerm -> Idris ()
1361addStatics n tm ptm =
1362 do let (statics, dynamics) = initStatics tm ptm
1363 let stnames = nub $ concatMap freeNames (map snd statics)
1364 let dnames = nub $ concatMap freeNames (map snd dynamics)
1365 when (not (null statics)) $
1366 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
1367 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1368 let statics' = nub $ map fst statics ++
1369 filter (\x -> not (elem x dnames)) stnames
1370 let stpos = staticList statics' tm
1371 i <- get
1372 put (i { idris_statics = addDef n stpos (idris_statics i) })
1373 addIBC (IBCStatic n)
1374 where
1375 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1376 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1377 if pstatic p == Static then ((n, ty) : static, dynamic)
1378 else (static, (n, ty) : dynamic)
1379 initStatics t pt = ([], [])
1381 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1382 staticList _ _ = []
1384-- Dealing with implicit arguments
1386-- Add implicit Pi bindings for any names in the term which appear in an
1387-- argument position.
1389-- This has become a right mess already. Better redo it some time...
1391implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1392implicit syn n ptm
1393 = do i <- get
1394 let (tm', impdata) = implicitise syn i ptm
1395-- let (tm'', spos) = findStatics i tm'
1396 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
1397 addIBC (IBCImp n)
1398 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1399-- i <- get
1400-- put (i { idris_statics = addDef n spos (idris_statics i) })
1401 return tm'
1403implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
1404implicitise syn ist tm
1405 = let (declimps, ns') = execState (imps True [] tm) ([], [])
1406 ns = ns' \\ (map fst pvars ++ no_imp syn) in
1407 if null ns
1408 then (tm, reverse declimps)
1409 else implicitise syn ist (pibind uvars ns tm)
1410 where
1411 uvars = using syn
1412 pvars = syn_params syn
1414 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1415 | otherwise = x : dropAll xs ys
1416 dropAll [] ys = []
1418 imps top env (PApp _ f as)
1419 = do (decls, ns) <- get
1420 let isn = concatMap (namesIn uvars ist) (map getTm as)
1421 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1422 imps top env (PPi (Imp l _) n ty sc)
1423 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1424 (decls , ns) <- get
1425 put (PImp (getPriority ist ty) l n ty : decls,
1426 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1427 imps True (n:env) sc
1428 imps top env (PPi (Exp l _) n ty sc)
1429 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1430 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1431 _ -> [])
1432 (decls, ns) <- get -- ignore decls in HO types
1433 put (PExp (getPriority ist ty) l ty : decls,
1434 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1435 imps True (n:env) sc
1436 imps top env (PPi (Constraint l _) n ty sc)
1437 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1438 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1439 _ -> [])
1440 (decls, ns) <- get -- ignore decls in HO types
1441 put (PConstraint 10 l ty : decls,
1442 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1443 imps True (n:env) sc
1444 imps top env (PPi (TacImp l _ scr) n ty sc)
1445 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1446 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1447 _ -> [])
1448 (decls, ns) <- get -- ignore decls in HO types
1449 put (PTacImplicit 10 l n scr ty : decls,
1450 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1451 imps True (n:env) sc
1452 imps top env (PEq _ l r)
1453 = do (decls, ns) <- get
1454 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1455 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1456 imps top env (PTyped l r)
1457 = imps top env l
1458 imps top env (PPair _ l r)
1459 = do (decls, ns) <- get
1460 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1461 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1462 imps top env (PDPair _ (PRef _ n) t r)
1463 = do (decls, ns) <- get
1464 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1465 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1466 imps top env (PDPair _ l t r)
1467 = do (decls, ns) <- get
1468 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1469 namesIn uvars ist r
1470 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1471 imps top env (PAlternative as)
1472 = do (decls, ns) <- get
1473 let isn = concatMap (namesIn uvars ist) as
1474 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1475 imps top env (PLam n ty sc)
1476 = do imps False env ty
1477 imps False (n:env) sc
1478 imps top env (PHidden tm) = imps False env tm
1479 imps top env _ = return ()
1481 pibind using [] sc = sc
1482 pibind using (n:ns) sc
1483 = case lookup n using of
1484 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
1485 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
1487-- Add implicit arguments in function calls
1488addImplPat :: IState -> PTerm -> PTerm
1489addImplPat = addImpl' True []
1491addImplBound :: IState -> [Name] -> PTerm -> PTerm
1492addImplBound ist ns = addImpl' False ns ist
1494addImpl :: IState -> PTerm -> PTerm
1495addImpl = addImpl' False []
1497-- TODO: in patterns, don't add implicits to function names guarded by constructors
1498-- and *not* inside a PHidden
1500addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1501addImpl' inpat env ist ptm = ai env ptm
1502 where
1503 ai env (PRef fc f)
1504 | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []
1505 ai env (PHidden (PRef fc f))
1506 | not (f `elem` env) = handleErr $ aiFn False ist fc f []
1507 ai env (PEq fc l r) = let l' = ai env l
1508 r' = ai env r in
1509 PEq fc l' r'
1510 ai env (PTyped l r) = let l' = ai env l
1511 r' = ai env r in
1512 PTyped l' r'
1513 ai env (PPair fc l r) = let l' = ai env l
1514 r' = ai env r in
1515 PPair fc l' r'
1516 ai env (PDPair fc l t r) = let l' = ai env l
1517 t' = ai env t
1518 r' = ai env r in
1519 PDPair fc l' t' r'
1520 ai env (PAlternative as) = let as' = map (ai env) as in
1521 PAlternative as'
1522 ai env (PApp fc (PRef _ f) as)
1523 | not (f `elem` env)
1524 = let as' = map (fmap (ai env)) as in
1525 handleErr $ aiFn False ist fc f as'
1526 ai env (PApp fc f as) = let f' = ai env f
1527 as' = map (fmap (ai env)) as in
1528 mkPApp fc 1 f' as'
1529 ai env (PCase fc c os) = let c' = ai env c
1530 os' = map (pmap (ai env)) os in
1531 PCase fc c' os'
1532 ai env (PLam n ty sc) = let ty' = ai env ty
1533 sc' = ai (n:env) sc in
1534 PLam n ty' sc'
1535 ai env (PLet n ty val sc)
1536 = let ty' = ai env ty
1537 val' = ai env val
1538 sc' = ai (n:env) sc in
1539 PLet n ty' val' sc'
1540 ai env (PPi p n ty sc) = let ty' = ai env ty
1541 sc' = ai (n:env) sc in
1542 PPi p n ty' sc'
1543 ai env (PHidden tm) = PHidden (ai env tm)
1544 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1545 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1546 ai env tm = tm
1548 handleErr (Left err) = PElabError err
1549 handleErr (Right x) = x
1551-- if in a pattern, and there are no arguments, and there's no possible
1552-- names with zero explicit arguments, don't add implicits.
1554aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1555aiFn True ist fc f []
1556 = case lookupCtxt Nothing f (idris_implicits ist) of
1557 [] -> Right $ PRef fc f
1558 alts -> if (any (all imp) alts)
1559 then aiFn False ist fc f [] -- use it as a constructor
1560 else Right $ PRef fc f
1561 where imp (PExp _ _ _) = False
1562 imp _ = True
1563aiFn inpat ist fc f as
1564 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1565aiFn inpat ist fc f as
1566 -- This is where namespaces get resolved by adding PAlternative
1567 = case lookupCtxtName Nothing f (idris_implicits ist) of
1568 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1569 [] -> if f `elem` idris_metavars ist
1570 then Right $ PApp fc (PRef fc f) as
1571 else Right $ mkPApp fc (length as) (PRef fc f) as
1572 alts -> Right $
1573 PAlternative $
1574 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1575 (insertImpl ns as)) alts
1576 where
1577 insertImpl :: [PArg] -> [PArg] -> [PArg]
1578 insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1579 PExp p l tm : insertImpl ps given
1580 insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1581 PConstraint p l tm : insertImpl ps given
1582 insertImpl (PConstraint p l ty : ps) given =
1583 PConstraint p l (PResolveTC fc) : insertImpl ps given
1584 insertImpl (PImp p l n ty : ps) given =
1585 case find n given [] of
1586 Just (tm, given') -> PImp p l n tm : insertImpl ps given'
1587 Nothing -> PImp p l n Placeholder : insertImpl ps given
1588 insertImpl (PTacImplicit p l n sc ty : ps) given =
1589 case find n given [] of
1590 Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1591 Nothing -> PTacImplicit p l n sc sc
1592 : insertImpl ps given
1593 insertImpl expected [] = []
1594 insertImpl _ given = given
1596 find n [] acc = Nothing
1597 find n (PImp _ _ n' t : gs) acc
1598 | n == n' = Just (t, reverse acc ++ gs)
1599 find n (g : gs) acc = find n gs (g : acc)
1601mkPApp fc a f [] = f
1602mkPApp fc a f as = let rest = drop a as in
1603 appRest fc (PApp fc f (take a as)) rest
1604 where
1605 appRest fc f [] = f
1606 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1608-- Find 'static' argument positions
1609-- (the declared ones, plus any names in argument position in the declared
1610-- statics)
1611-- FIXME: It's possible that this really has to happen after elaboration
1613findStatics :: IState -> PTerm -> (PTerm, [Bool])
1614findStatics ist tm = trace (showImp True tm) $
1615 let (ns, ss) = fs tm in
1616 runState (pos ns ss tm) []
1617 where fs (PPi p n t sc)
1618 | Static <- pstatic p
1619 = let (ns, ss) = fs sc in
1620 (namesIn [] ist t : ns, n : ss)
1621 | otherwise = let (ns, ss) = fs sc in
1622 (ns, ss)
1623 fs _ = ([], [])
1625 inOne n ns = length (filter id (map (elem n) ns)) == 1
1627 pos ns ss (PPi p n t sc)
1628 | elem n ss = do sc' <- pos ns ss sc
1629 spos <- get
1630 put (True : spos)
1631 return (PPi (p { pstatic = Static }) n t sc')
1632 | otherwise = do sc' <- pos ns ss sc
1633 spos <- get
1634 put (False : spos)
1635 return (PPi p n t sc')
1636 pos ns ss t = return t
1638-- Debugging/logging stuff
1640dumpDecls :: [PDecl] -> String
1641dumpDecls [] = ""
1642dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1644dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1645dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
1646dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1647dumpDecl (PData _ _ d) = showDImp True d
1648dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1649dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1650dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1651dumpDecl (PClass _ _ cs n ps ds)
1652 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1653dumpDecl (PInstance _ _ cs n _ t ds)
1654 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1655dumpDecl _ = "..."
1656-- dumpDecl (PImport i) = "import " ++ i
1658-- for 6.12/7 compatibility
1659data EitherErr a b = LeftErr a | RightOK b
1661instance Monad (EitherErr a) where
1662 return = RightOK
1664 (LeftErr e) >>= k = LeftErr e
1665 RightOK v >>= k = k v
1667toEither (LeftErr e) = Left e
1668toEither (RightOK ho) = Right ho
1670-- syntactic match of a against b, returning pair of variables in a
1671-- and what they match. Returns the pair that failed if not a match.
1673matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1674matchClause = matchClause' False
1676matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1677matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1678 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1680 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1681 fullApp x = x
1683 match' x y = match (fullApp x) (fullApp y)
1684 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1685 | PConstant (I _) <- getTm x = match (getTm x) x'
1686 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1687 | PConstant (I _) <- getTm x = match (getTm x) x'
1688 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1689 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1690 match (PApp _ f args) (PApp _ f' args')
1691 | length args == length args'
1692 = do mf <- match' f f'
1693 ms <- zipWithM matchArg args args'
1694 return (mf ++ concat ms)
1695-- match (PRef _ n) (PRef _ n') | n == n' = return []
1696-- | otherwise = Nothing
1697 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1698 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1699 match (PRef _ n) (PRef _ n') | n == n' = return []
1700 match (PRef _ n) tm
1701 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1702 = return [(n, tm)]
1703 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1704 mr <- match' r r'
1705 return (ml ++ mr)
1706 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1707 mr <- match r r'
1708 return (ml ++ mr)
1709 match (PTyped l r) x = match l x
1710 match x (PTyped l r) = match x l
1711 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1712 mr <- match' r r'
1713 return (ml ++ mr)
1714 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1715 mt <- match' t t'
1716 mr <- match' r r'
1717 return (ml ++ mt ++ mr)
1718 match (PAlternative as) (PAlternative as')
1719 = do ms <- zipWithM match' as as'
1720 return (concat ms)
1721 match a@(PAlternative as) b
1722 = do let ms = zipWith match' as (repeat b)
1723 case (rights (map toEither ms)) of
1724 (x: _) -> return x
1725 _ -> LeftErr (a, b)
1726 match (PCase _ _ _) _ = return [] -- lifted out
1727 match (PMetavar _) _ = return [] -- modified
1728 match (PQuote _) _ = return []
1729 match (PProof _) _ = return []
1730 match (PTactics _) _ = return []
1731 match (PRefl _) (PRefl _) = return []
1732 match (PResolveTC _) (PResolveTC _) = return []
1733 match (PTrue _) (PTrue _) = return []
1734 match (PFalse _) (PFalse _) = return []
1735 match (PReturn _) (PReturn _) = return []
1736 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1737 ms <- match' s s'
1738 return (mt ++ ms)
1739 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1740 ms <- match' s s'
1741 return (mt ++ ms)
1742 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1743 mty <- match' ty ty'
1744 ms <- match' s s'
1745 return (mt ++ mty ++ ms)
1746 match (PHidden x) (PHidden y) = match' x y
1747 match Placeholder _ = return []
1748-- match _ Placeholder = return []
1749 match (PResolveTC _) _ = return []
1750 match a b | a == b = return []
1751 | otherwise = LeftErr (a, b)
1753 checkRpts (RightOK ms) = check ms where
1754 check ((n,t):xs)
1755 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1756 then Left (t, t')
1757 else check xs
1758 check (_:xs) = check xs
1759 check [] = Right ms
1760 checkRpts (LeftErr x) = Left x
1762substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1763substMatches [] t = t
1764substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
1766substMatch :: Name -> PTerm -> PTerm -> PTerm
1767substMatch n tm t = sm t where
1768 sm (PRef _ n') | n == n' = tm
1769 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1770 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1771 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1772 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1773 sm (PEq f x y) = PEq f (sm x) (sm y)
1774 sm (PTyped x y) = PTyped (sm x) (sm y)
1775 sm (PPair f x y) = PPair f (sm x) (sm y)
1776 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1777 sm (PAlternative as) = PAlternative (map sm as)
1778 sm (PHidden x) = PHidden (sm x)
1779 sm x = x
1781shadow :: Name -> Name -> PTerm -> PTerm
1782shadow n n' t = sm t where
1783 sm (PRef fc x) | n == x = PRef fc n'
1784 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1785 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1786 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1787 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1788 sm (PEq f x y) = PEq f (sm x) (sm y)
1789 sm (PTyped x y) = PTyped (sm x) (sm y)
1790 sm (PPair f x y) = PPair f (sm x) (sm y)
1791 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1792 sm (PAlternative as) = PAlternative (map sm as)
1793 sm (PHidden x) = PHidden (sm x)
1794 sm x = x