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