git.iko.soy/Idris-dev
on f29a167 help sign in
Idris-dev/src/Idris/Parser.hs
1538 lines 61 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Parser where
5import Idris.AbsSyntax
6import Idris.DSL
7import Idris.Imports
8import Idris.Error
9import Idris.ElabDecls
10import Idris.ElabTerm
11import Idris.Coverage
12import Idris.IBC
13import Idris.Unlit
14import Paths_idris
16import Core.CoreParser
17import Core.TT
18import Core.Evaluate
20import Text.Parsec
21import Text.Parsec.Error
22import Text.Parsec.Expr
23import Text.Parsec.Language
24import Text.Parsec.String
25import qualified Text.Parsec.Token as PTok
27import Data.List
28import Data.List.Split(splitOn)
29import Control.Monad.State
30import Debug.Trace
31import Data.Maybe
32import System.FilePath
34type TokenParser a = PTok.TokenParser a
36type IParser = GenParser Char IState
38lexer :: TokenParser IState
39lexer = idrisLexer
41whiteSpace = PTok.whiteSpace lexer
42lexeme = PTok.lexeme lexer
43symbol = PTok.symbol lexer
44natural = PTok.natural lexer
45parens = PTok.parens lexer
46semi = PTok.semi lexer
47comma = PTok.comma lexer
48identifier = PTok.identifier lexer
49reserved = PTok.reserved lexer
50operator = PTok.operator lexer
51reservedOp = PTok.reservedOp lexer
52integer = PTok.integer lexer
53float = PTok.float lexer
54strlit = PTok.stringLiteral lexer
55chlit = PTok.charLiteral lexer
56lchar = lexeme.char
58fixErrorMsg :: String -> [String] -> String
59fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
61-- Loading modules
63loadModule :: FilePath -> Idris String
64loadModule f
65 = idrisCatch (do i <- getIState
66 let file = takeWhile (/= ' ') f
67 ibcsd <- valIBCSubDir i
68 ids <- allImportDirs i
69 fp <- liftIO $ findImport ids ibcsd file
70 if file `elem` imported i
71 then iLOG $ "Already read " ++ file
72 else do putIState (i { imported = file : imported i })
73 case fp of
74 IDR fn -> loadSource False fn
75 LIDR fn -> loadSource True fn
76 IBC fn src ->
77 idrisCatch (loadIBC fn)
78 (\c -> do iLOG $ fn ++ " failed " ++ show c
79 case src of
80 IDR sfn -> loadSource False sfn
81 LIDR sfn -> loadSource True sfn)
82 let (dir, fh) = splitFileName file
83 return (dropExtension fh))
84 (\e -> do let msg = show e
85 setErrLine (getErrLine msg)
86 iputStrLn msg
87 return "")
89loadSource :: Bool -> FilePath -> Idris ()
90loadSource lidr f
91 = do iLOG ("Reading " ++ f)
92 i <- getIState
93 let def_total = default_total i
94 file_in <- liftIO $ readFile f
95 file <- if lidr then tclift $ unlit f file_in else return file_in
96 (mname, modules, rest, pos) <- parseImports f file
97 i <- getIState
98 putIState (i { default_access = Hidden })
99 mapM_ loadModule modules
100 clearIBC -- start a new .ibc file
101 mapM_ (addIBC . IBCImport) modules
102 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
103 f rest pos
104 unless (null ds') $ do
105 let ds = namespaces mname ds'
106 logLvl 3 (dumpDecls ds)
107 i <- getIState
108 logLvl 10 (show (toAlist (idris_implicits i)))
109 logLvl 3 (show (idris_infixes i))
110 -- Now add all the declarations to the context
111 v <- verbose
112 when v $ iputStrLn $ "Type checking " ++ f
113 elabDecls toplevel ds
114 i <- getIState
115 -- simplify every definition do give the totality checker
116 -- a better chance
117 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
118 updateContext (simplifyCasedef n))
119 (map snd (idris_totcheck i))
120 -- build size change graph from simplified definitions
121 iLOG "Totality checking"
122 i <- getIState
123 mapM_ buildSCG (idris_totcheck i)
124 mapM_ checkDeclTotality (idris_totcheck i)
125 iLOG ("Finished " ++ f)
126 ibcsd <- valIBCSubDir i
127 let ibc = ibcPathNoFallback ibcsd f
128 iLOG "Universe checking"
129 iucheck
130 i <- getIState
131 addHides (hide_list i)
132 ok <- noErrors
133 when ok $
134 idrisCatch (do writeIBC f ibc; clearIBC)
135 (\c -> return ()) -- failure is harmless
136 i <- getIState
137 putIState (i { default_total = def_total,
138 hide_list = [] })
139 return ()
140 return ()
141 where
142 namespaces [] ds = ds
143 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
145addHides :: [(Name, Maybe Accessibility)] -> Idris ()
146addHides xs = do i <- getIState
147 let defh = default_access i
148 let (hs, as) = partition isNothing xs
149 unless (null as) $
150 mapM_ doHide
151 (map (\ (n, _) -> (n, defh)) hs ++
152 map (\ (n, Just a) -> (n, a)) as)
153 where isNothing (_, Nothing) = True
154 isNothing _ = False
156 doHide (n, a) = do setAccessibility n a
157 addIBC (IBCAccess n a)
159parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
160parseTac i = runParser (do t <- pTactic defaultSyntax
161 eof
162 return t) i "(proof)"
164parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
165parseImports fname input
166 = do i <- getIState
167 case runParser (do whiteSpace
168 mname <- pHeader
169 ps <- many pImport
170 rest <- getInput
171 pos <- getPosition
172 return ((mname, ps, rest, pos), i)) i fname input of
173 Left err -> fail (show err)
174 Right (x, i) -> do putIState i
175 return x
177pHeader :: IParser [String]
178pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
179 return (parseName i))
180 <|> return []
181 where parseName x = case span (/='.') x of
182 (x, "") -> [x]
183 (x, '.':y) -> x : parseName y
185pushIndent :: IParser ()
186pushIndent = do pos <- getPosition
187 ist <- getState
188 setState (ist { indent_stack = sourceColumn pos :
189 indent_stack ist })
191lastIndent :: IParser Int
192lastIndent = do ist <- getState
193 case indent_stack ist of
194 (x : xs) -> return x
195 _ -> return 1
197indent :: IParser Int
198indent = liftM sourceColumn getPosition
200popIndent :: IParser ()
201popIndent = do ist <- getState
202 let (x : xs) = indent_stack ist
203 setState (ist { indent_stack = xs })
205openBlock :: IParser ()
206openBlock = do lchar '{'
207 ist <- getState
208 setState (ist { brace_stack = Nothing : brace_stack ist })
209 <|> do ist <- getState
210 lvl <- indent
211 setState (ist { brace_stack = Just lvl : brace_stack ist })
213closeBlock :: IParser ()
214closeBlock = do ist <- getState
215 bs <- case brace_stack ist of
216 Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])
217 Just lvl : xs -> (do i <- indent
218 inp <- getInput
219-- trace (show (take 10 inp, i, lvl)) $
220 if i >= lvl && take 1 inp /= ")"
221 then fail "Not end of block"
222 else return xs) <|> (eof >> return [])
223 setState (ist { brace_stack = bs })
225pTerminator = do lchar ';'; popIndent
226 <|> do c <- indent; l <- lastIndent
227 if c <= l
228 then popIndent
229 else fail "Not a terminator"
230 <|> do i <- getInput
231 if "}" `isPrefixOf` i || ")" `isPrefixOf` i
232 then popIndent
233 else fail "Not a terminator"
234 <|> lookAhead eof
236pBarTerminator
237 = do lchar '|'; return ()
238 <|> do c <- indent; l <- lastIndent
239 unless (c <= l) $ fail "Not a terminator"
240 <|> lookAhead eof
242pKeepTerminator
243 = do lchar ';'; return ()
244 <|> do c <- indent; l <- lastIndent
245 unless (c <= l) $ fail "Not a terminator"
246 <|> do i <- getInput
247 let h = take 1 i
248 unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
249 <|> lookAhead eof
251notEndApp = do c <- indent; l <- lastIndent
252 i <- getInput
253 when (c <= l) $ fail "Terminator"
255notEndBlock = do ist <- getState
256 case brace_stack ist of
257 Just lvl : xs -> do i <- indent
258 inp <- getInput
259 when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
260 _ -> return ()
262pfc :: IParser FC
263pfc = do s <- getPosition
264 let (dir, file) = splitFileName (sourceName s)
265 let f = if dir == addTrailingPathSeparator "." then file else sourceName s
266 return $ FC f (sourceLine s)
268pImport :: IParser String
269pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
270 return (toPath f)
271 where toPath n = foldl1 (</>) $ splitOn "." n
273-- a program is a list of declarations, possibly with associated
274-- documentation strings
276parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->
277 Idris [PDecl]
278parseProg syn fname input pos
279 = do i <- getIState
280 case runParser (do setPosition pos
281 whiteSpace
282 ps <- many (pDecl syn)
283 eof
284 i' <- getState
285 return (concat ps, i')) i fname input of
286 Left err -> do iputStrLn (show err)
287 return []
288 Right (x, i) -> do putIState i
289 return (collect x)
291-- Collect PClauses with the same function name
293collect :: [PDecl] -> [PDecl]
294collect (c@(PClauses _ o _ _) : ds)
295 = clauses (cname c) [] (c : ds)
296 where clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
297 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
298 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
299 | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
300 clauses (Just n) acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
301 clauses Nothing acc (x:xs) = collect xs
302 clauses Nothing acc [] = []
304 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
305 cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
306 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
307 cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
308 getfc (PClauses fc _ _ _) = fc
310collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
311collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
312collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
313collect (PClass doc f s cs n ps ds : ds')
314 = PClass doc f s cs n ps (collect ds) : collect ds'
315collect (PInstance f s cs n ps t en ds : ds')
316 = PInstance f s cs n ps t en (collect ds) : collect ds'
317collect (d : ds) = d : collect ds
318collect [] = []
320pFullExpr :: SyntaxInfo -> IParser PTerm
321pFullExpr syn
322 = do x <- pExpr syn; eof;
323 i <- getState
324 return $ desugar syn i x
326pDecl :: SyntaxInfo -> IParser [PDecl]
327pDecl syn = do notEndBlock
328 pDeclBody where
329 pDeclBody
330 = do d <- pDecl' syn
331 i <- getState
332 let d' = fmap (desugar syn i) d
333 return [d']
334 <|> pUsing syn
335 <|> pParams syn
336 <|> pMutual syn
337 <|> pNamespace syn
338 <|> pClass syn
339 <|> pInstance syn
340 <|> do d <- pDSL syn; return [d]
341 <|> pDirective
342 <|> try (do reserved "import"; fp <- identifier
343 fail "imports must be at the top of file")
345pFunDecl :: SyntaxInfo -> IParser [PDecl]
346pFunDecl syn
347 = try (do notEndBlock
348 d <- pFunDecl' syn
349 i <- getState
350 let d' = fmap (desugar syn i) d
351 return [d'])
353--------- Top Level Declarations ---------
355pDecl' :: SyntaxInfo -> IParser PDecl
356pDecl' syn
357 = try pFixity
358 <|> try (pFunDecl' syn)
359 <|> try (pData syn)
360 <|> try (pRecord syn)
361 <|> try (pSyntaxDecl syn)
363pSyntaxDecl :: SyntaxInfo -> IParser PDecl
364pSyntaxDecl syn
365 = do s <- pSyntaxRule syn
366 i <- getState
367 let rs = syntax_rules i
368 let ns = syntax_keywords i
369 let ibc = ibc_write i
370 let ks = map show (names s)
371 setState (i { syntax_rules = s : rs,
372 syntax_keywords = ks ++ ns,
373 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
374 })
375 fc <- pfc
376 return (PSyntax fc s)
377 where
378 names (Rule syms _ _) = mapMaybe ename syms
379 ename (Keyword n) = Just n
380 ename _ = Nothing
382pSyntaxRule :: SyntaxInfo -> IParser Syntax
383pSyntaxRule syn
384 = do pushIndent
385 sty <- option AnySyntax (do reserved "term"; return TermSyntax
386 <|> do reserved "pattern"; return PatternSyntax)
387 reserved "syntax"
388 syms <- many1 pSynSym
389 when (all expr syms) $ fail "No keywords in syntax rule"
390 let ns = mapMaybe name syms
391 when (length ns /= length (nub ns))
392 $ fail "Repeated variable in syntax rule"
393 lchar '='
394 tm <- pTExpr (impOK syn)
395 pTerminator
396 return (Rule (mkSimple syms) tm sty)
397 where
398 expr (Expr _) = True
399 expr _ = False
400 name (Expr n) = Just n
401 name _ = Nothing
403 -- Can't parse two full expressions (i.e. expressions with application) in a row
404 -- so change the first to a simple expression
406 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
407 mkSimple xs = mkSimple' xs
409 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : mkSimple' (Expr e1 : es)
410 mkSimple' (e : es) = e : mkSimple' es
411 mkSimple' [] = []
413pSynSym :: IParser SSymbol
414pSynSym = try (do lchar '['; n <- pName; lchar ']'
415 return (Expr n))
416 <|> try (do lchar '{'; n <- pName; lchar '}'
417 return (Binding n))
418 <|> do n <- iName []
419 return (Keyword n)
420 <|> do sym <- strlit
421 return (Symbol sym)
423pFunDecl' :: SyntaxInfo -> IParser PDecl
424pFunDecl' syn = try (do doc <- option "" (pDocComment '|')
425 pushIndent
426 ist <- getState
427 let initOpts = if default_total ist
428 then [TotalFn]
429 else []
430 opts <- pFnOpts initOpts
431 acc <- pAccessibility
432 opts' <- pFnOpts opts
433 n_in <- pfName
434 let n = expandNS syn n_in
435 fc <- pfc
436 ty <- pTSig (impOK syn)
437 pTerminator
438-- ty' <- implicit syn n ty
439 addAcc n acc
440 return (PTy doc syn fc opts' n ty))
441 <|> try (pPostulate syn)
442 <|> try (pPattern syn)
443 <|> try (pCAF syn)
445pPostulate :: SyntaxInfo -> IParser PDecl
446pPostulate syn = do doc <- option "" (pDocComment '|')
447 pushIndent
448 reserved "postulate"
449 ist <- getState
450 let initOpts = if default_total ist
451 then [TotalFn]
452 else []
453 opts <- pFnOpts initOpts
454 acc <- pAccessibility
455 opts' <- pFnOpts opts
456 n_in <- pfName
457 let n = expandNS syn n_in
458 ty <- pTSig (impOK syn)
459 fc <- pfc
460 pTerminator
461 addAcc n acc
462 return (PPostulate doc syn fc opts' n ty)
465pUsing :: SyntaxInfo -> IParser [PDecl]
466pUsing syn =
467 do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'
468 openBlock
469 let uvars = using syn
470 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
471 closeBlock
472 return (concat ds)
474pParams :: SyntaxInfo -> IParser [PDecl]
475pParams syn =
476 do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'
477 openBlock
478 let pvars = syn_params syn
479 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
480 closeBlock
481 fc <- pfc
482 return [PParams fc ns (concat ds)]
484pMutual :: SyntaxInfo -> IParser [PDecl]
485pMutual syn =
486 do reserved "mutual"
487 openBlock
488 let pvars = syn_params syn
489 ds <- many1 (pDecl syn)
490 closeBlock
491 fc <- pfc
492 return [PMutual fc (concat ds)]
494pNamespace :: SyntaxInfo -> IParser [PDecl]
495pNamespace syn =
496 do reserved "namespace"; n <- identifier;
497 openBlock
498 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
499 closeBlock
500 return [PNamespace n (concat ds)]
502--------- Fixity ---------
504pFixity :: IParser PDecl
505pFixity = do pushIndent
506 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
507 pTerminator
508 let prec = fromInteger i
509 istate <- getState
510 let infixes = idris_infixes istate
511 let fs = map (Fix (f prec)) ops
512 let redecls = map (alreadyDeclared infixes) fs
513 let ill = filter (not . checkValidity) redecls
514 if null ill
515 then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)
516 , ibc_write = map IBCFix fs ++ ibc_write istate
517 })
518 fc <- pfc
519 return (PFix fc (f prec) ops)
520 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
521 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
522 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
523 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
525 checkValidity :: (FixDecl, [FixDecl]) -> Bool
526 checkValidity (f, fs) = all (== f) fs
528 extractName :: FixDecl -> String
529 extractName (Fix _ n) = n
531fixity :: IParser (Int -> Fixity)
532fixity = try (do reserved "infixl"; return Infixl)
533 <|> try (do reserved "infixr"; return Infixr)
534 <|> try (do reserved "infix"; return InfixN)
535 <|> try (do reserved "prefix"; return PrefixN)
537--------- Type classes ---------
539pClass :: SyntaxInfo -> IParser [PDecl]
540pClass syn = do doc <- option "" (pDocComment '|')
541 acc <- pAccessibility
542 reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
543 let n = expandNS syn n_in
544 cs <- many1 carg
545 reserved "where"; openBlock
546 ds <- many $ pFunDecl syn
547 closeBlock
548 let allDs = concat ds
549 accData acc n (concatMap declared allDs)
550 return [PClass doc syn fc cons n cs allDs]
551 where
552 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
553 return (i, ty)
554 <|> do i <- pName;
555 return (i, PType)
557pInstance :: SyntaxInfo -> IParser [PDecl]
558pInstance syn = do reserved "instance"; fc <- pfc
559 en <- option Nothing
560 (do lchar '['; n_in <- pfName; lchar ']'
561 let n = expandNS syn n_in
562 return (Just n))
563 cs <- pConstList syn
564 cn <- pName
565 args <- many1 (pSimpleExpr syn)
566 let sc = PApp fc (PRef fc cn) (map pexp args)
567 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
568 reserved "where"; openBlock
569 ds <- many $ pFunDecl syn
570 closeBlock
571 return [PInstance syn fc cs cn args t en (concat ds)]
573--------- Expressions ---------
575pExpr syn = do i <- getState
576 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
578pExpr' :: SyntaxInfo -> IParser PTerm
579pExpr' syn
580 = try (pExtExpr syn)
581 <|> pNoExtExpr syn
583pExtExpr :: SyntaxInfo -> IParser PTerm
584pExtExpr syn = do i <- getState
585 pExtensions syn (syntax_rules i)
587pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
588pSimpleExtExpr syn = do i <- getState
589 pExtensions syn (filter simple (syntax_rules i))
590 where
591 simple (Rule (Expr x:xs) _ _) = False
592 simple (Rule (SimpleExpr x:xs) _ _) = False
593 simple (Rule [Keyword _] _ _) = True
594 simple (Rule [Symbol _] _ _) = True
595 simple (Rule (_:xs) _ _) = case last xs of
596 Keyword _ -> True
597 Symbol _ -> True
598 _ -> False
599 simple _ = False
601pNoExtExpr syn =
602 try (pApp syn)
603 <|> pRecordType syn
604 <|> try (pSimpleExpr syn)
605 <|> pLambda syn
606 <|> pLet syn
607 <|> pPi syn
608 <|> pDoBlock syn
609 <|> pComprehension syn
611pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
612pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
613 where
614 valid (Rule _ _ AnySyntax) = True
615 valid (Rule _ _ PatternSyntax) = inPattern syn
616 valid (Rule _ _ TermSyntax) = not (inPattern syn)
619data SynMatch = SynTm PTerm | SynBind Name
621pExt :: SyntaxInfo -> Syntax -> IParser PTerm
622pExt syn (Rule ssym ptm _)
623 = do smap <- mapM pSymbol ssym
624 let ns = mapMaybe id smap
625 return (update ns ptm) -- updated with smap
626 where
627 pSymbol (Keyword n) = do reserved (show n); return Nothing
628 pSymbol (Expr n) = do tm <- pExpr syn
629 return $ Just (n, SynTm tm)
630 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
631 return $ Just (n, SynTm tm)
632 pSymbol (Binding n) = do b <- pName
633 return $ Just (n, SynBind b)
634 pSymbol (Symbol s) = do symbol s
635 return Nothing
636 dropn n [] = []
637 dropn n ((x,t) : xs) | n == x = xs
638 | otherwise = (x,t):dropn n xs
640 updateB ns n = case lookup n ns of
641 Just (SynBind t) -> t
642 _ -> n
644 update ns (PRef fc n) = case lookup n ns of
645 Just (SynTm t) -> t
646 _ -> PRef fc n
647 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
648 update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
649 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
650 (update (dropn n ns) sc)
651 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
652 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
653 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
654 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
655 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
656 update ns (PHidden t) = PHidden (update ns t)
657 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
658 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
659 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
660 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
661 : upd (dropn n ns) ds
662 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
663 : upd ns ds
664 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
665 : upd ns ds
666 update ns t = t
668pName = do i <- getState
669 iName (syntax_keywords i)
670 <|> do reserved "instance"
671 i <- getState
672 UN n <- iName (syntax_keywords i)
673 return (UN ('@':n))
675-- Parser for an operator in function position, i.e. enclosed by `()', with an
676-- optional namespace.
677pOpFront = maybeWithNS pOpFrontNoNS False []
678 where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
680pfName = try pOpFront
681 <|> pName
683pTotality :: IParser Bool
684pTotality
685 = do reserved "total"; return True
686 <|> do reserved "partial"; return False
688pAccessibility' :: IParser Accessibility
689pAccessibility'
690 = do reserved "public"; return Public
691 <|> do reserved "abstract"; return Frozen
692 <|> do reserved "private"; return Hidden
694pAccessibility :: IParser (Maybe Accessibility)
695pAccessibility
696 = do acc <- pAccessibility'; return (Just acc)
697 <|> return Nothing
699pFnOpts :: [FnOpt] -> IParser [FnOpt]
700pFnOpts opts
701 = do reserved "total"; pFnOpts (TotalFn : opts)
702 <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))
703 <|> try (do lchar '%'; reserved "export"; c <- strlit;
704 pFnOpts (CExport c : opts))
705 <|> do lchar '%'; reserved "assert_total"; pFnOpts (AssertTotal : opts)
706 <|> do lchar '%'; reserved "specialise";
707 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'
708 pFnOpts (Specialise ns : opts)
709 <|> do reserved "implicit"; pFnOpts (Implicit : opts)
710 <|> return opts
712addAcc :: Name -> Maybe Accessibility -> IParser ()
713addAcc n a = do i <- getState
714 setState (i { hide_list = (n, a) : hide_list i })
716pCaseExpr syn = do
717 reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
718 openBlock
719 pushIndent
720 opts <- many1 (do notEndBlock
721 x <- pCaseOpt syn
722 pKeepTerminator
723 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
724 popIndent
725 closeBlock
726 return (PCase fc scr opts)
728pProofExpr syn = do
729 reserved "proof"; lchar '{'
730 ts <- endBy (pTactic syn) (lchar ';')
731 lchar '}'
732 return (PProof ts)
734pTacticsExpr syn = do
735 reserved "tactics"; lchar '{'
736 ts <- endBy (pTactic syn) (lchar ';')
737 lchar '}'
738 return (PTactics ts)
740pSimpleExpr syn =
741 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
742 <|> do lchar '?'; x <- pName; return (PMetavar x)
743 <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
744 <|> do reserved "refl"; fc <- pfc;
745 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
746 return t)
747 return (PRefl fc tm)
748-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
749 <|> pProofExpr syn
750 <|> pTacticsExpr syn
751 <|> pCaseExpr syn
752 <|> try (do x <- pfName
753 fc <- pfc
754 return (PRef fc x))
755 <|> try (do lchar '!'; x <- pfName
756 fc <- pfc
757 return (PInferRef fc x))
758 <|> try (pList syn)
759 <|> try (pAlt syn)
760 <|> try (pIdiom syn)
761 <|> try (do lchar '('
762 bracketed (noImp syn))
763 <|> try (do c <- pConstant
764 fc <- pfc
765 return (modifyConst syn fc (PConstant c)))
766 <|> do reserved "Type"; return PType
767 <|> try (do symbol "()"
768 fc <- pfc
769 return (PTrue fc))
770 <|> try (do symbol "_|_"
771 fc <- pfc
772 return (PFalse fc))
773 <|> do lchar '_'; return Placeholder
774 <|> pSimpleExtExpr syn
776bracketed syn =
777 try (pPair syn)
778 <|> try (do e <- pExpr syn; lchar ')'; return e)
779-- <|> try (do reserved "typed"
780-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
781-- return (PTyped e t))
782 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
783 return $ PLam (MN 1000 "ARG") Placeholder
784 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
785 pexp e]))
786 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
787 return $ PLam (MN 1000 "ARG") Placeholder
788 (PApp fc (PRef fc (UN o)) [pexp e,
789 pexp (PRef fc (MN 1000 "ARG"))]))
791pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
792pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })
793 symbol "=>"; rhs <- pExpr syn
794 return (lhs, rhs)
796modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
797modifyConst syn fc (PConstant (I x))
798 | not (inPattern syn)
799 = PAlternative False
800 [PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))],
801 PConstant (I x), PConstant (BI (toEnum x))]
802 | otherwise = PAlternative False
803 [PConstant (I x), PConstant (BI (toEnum x))]
804modifyConst syn fc x = x
806pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
807 return (mkList fc xs)
808 where
809 mkList fc [] = PRef fc (UN "Nil")
810 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
812pPair syn = try (do l <- pExpr syn
813 fc <- pfc
814 rest <- restTuple
815 case rest of
816 [] -> return l
817 [Left r] -> return (PPair fc l r)
818 [Right r] -> return (PDPair fc l Placeholder r))
819 <|> try (do x <- ntuple
820 lchar ')'
821 return x)
822 <|> do ln <- pName; lchar ':'
823 lty <- pExpr syn
824 reservedOp "**"
825 fc <- pfc
826 r <- pExpr syn
827 lchar ')'
828 return (PDPair fc (PRef fc ln) lty r)
829 where
830 restTuple = do lchar ')'; return []
831 <|> do lchar ','
832 r <- pExpr syn
833 lchar ')'
834 return [Left r]
835 <|> do reservedOp "**"
836 r <- pExpr syn
837 lchar ')'
838 return [Right r]
839 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
840 rest <- ntuple
841 return (PPair fc l rest))
842 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
843 r <- pExpr syn
844 return (PPair fc l r))
846pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
847 return (PAlternative False alts)
849pHSimpleExpr syn
850 = do lchar '.'
851 e <- pSimpleExpr syn
852 return $ PHidden e
853 <|> pSimpleExpr syn
855pApp syn = do f <- pSimpleExpr syn
856 fc <- pfc
857 args <- many1 (do notEndApp
858 pArg syn)
859 i <- getState
860 return (dslify i $ PApp fc f args)
861 where
862 dslify i (PApp fc (PRef _ f) [a])
863 | [d] <- lookupCtxt Nothing f (idris_dsls i)
864 = desugar (syn { dsl_info = d }) i (getTm a)
865 dslify i t = t
867pArg :: SyntaxInfo -> IParser PArg
868pArg syn = try (pImplicitArg syn)
869 <|> try (pConstraintArg syn)
870 <|> do e <- pSimpleExpr syn
871 return (pexp e)
873pImplicitArg syn = do lchar '{'
874 n <- pName
875 fc <- pfc
876 v <- option (PRef fc n) (do lchar '='
877 pExpr syn)
878 lchar '}'
879 return (pimp n v)
881pConstraintArg syn = do symbol "@{"
882 e <- pExpr syn
883 symbol "}"
884 return (pconst e)
886pRecordType syn
887 = do reserved "record"
888 lchar '{'
889 fields <- sepBy1 pFieldType (lchar ',')
890 lchar '}'
891 fc <- pfc
892 rec <- option Nothing (do e <- pSimpleExpr syn
893 return (Just e))
894 case rec of
895 Nothing ->
896 return (PLam (MN 0 "fldx") Placeholder
897 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
898 Just v -> return (applyAll fc fields v)
899 where pFieldType = do n <- pfName
900 lchar '='
901 e <- pExpr syn
902 return (n, e)
903 applyAll fc [] x = x
904 applyAll fc ((n, e) : es) x
905 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
907mkType (UN n) = UN ("set_" ++ n)
908mkType (MN 0 n) = MN 0 ("set_" ++ n)
909mkType (NS n s) = NS (mkType n) s
911noImp syn = syn { implicitAllowed = False }
912impOK syn = syn { implicitAllowed = True }
914pTSig syn = do lchar ':'; pTExpr syn
916pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
917 sc <- pExpr syn
918 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
920pLambda syn = do lchar '\\'
921 try (do xt <- tyOptDeclList syn
922 symbol "=>"
923 sc <- pExpr syn
924 return (bindList PLam xt sc)
925 <|> (do ps <- sepBy (do fc <- pfc
926 e <- pSimpleExpr syn
927 return (fc, e)) (lchar ',')
928 symbol "=>"
929 sc <- pExpr syn
930 return (pmList (zip [0..] ps) sc)))
931 where pmList [] sc = sc
932 pmList ((i, (fc, x)) : xs) sc
933 = PLam (MN i "lamp") Placeholder
934 (PCase fc (PRef fc (MN i "lamp"))
935 [(x, pmList xs sc)])
937pLet syn = try (do reserved "let"; n <- pName;
938 ty <- option Placeholder (do lchar ':'; pExpr' syn)
939 lchar '='
940 v <- pExpr syn
941 reserved "in"; sc <- pExpr syn
942 return (PLet n ty v sc))
943 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
944 symbol "="; v <- pExpr syn
945 reserved "in"; sc <- pExpr syn
946 return (PCase fc v [(pat, sc)]))
948pPi syn =
949 try (do lazy <- option False (do lchar '|'; return True)
950 st <- pStatic
951 lchar '('; xt <- tyDeclList syn; lchar ')'
952 doc <- option "" (pDocComment '^')
953 symbol "->"
954 sc <- pExpr syn
955 return (bindList (PPi (Exp lazy st doc)) xt sc))
956 <|> try (if implicitAllowed syn
957 then do lazy <- option False (do lchar '|'
958 return True)
959 st <- pStatic
960 lchar '{'
961 xt <- tyDeclList syn
962 lchar '}'
963 symbol "->"
964 sc <- pExpr syn
965 return (bindList (PPi (Imp lazy st "")) xt sc)
966 else fail "No implicit arguments allowed here")
967 <|> try (do lchar '{'
968 reserved "auto"
969 xt <- tyDeclList syn
970 lchar '}'
971 symbol "->"
972 sc <- pExpr syn
973 return (bindList (PPi
974 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
975 <|> try (do lchar '{'
976 reserved "default"
977 script <- pSimpleExpr syn
978 xt <- tyDeclList syn
979 lchar '}'
980 symbol "->"
981 sc <- pExpr syn
982 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
983 <|> do --lazy <- option False (do lchar '|'; return True)
984 lchar '{'
985 reserved "static"
986 lchar '}'
987 t <- pExpr' syn
988 symbol "->"
989 sc <- pExpr syn
990 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
992pConstList :: SyntaxInfo -> IParser [PTerm]
993pConstList syn = try (do lchar '('
994 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
995 lchar ')'
996 reservedOp "=>"
997 return tys)
998 <|> try (do t <- pExpr (noImp syn)
999 reservedOp "=>"
1000 return [t])
1001 <|> return []
1003tyDeclList syn = try (sepBy1 (do x <- pfName
1004 t <- pTSig (noImp syn)
1005 return (x,t))
1006 (lchar ','))
1007 <|> do ns <- sepBy1 pName (lchar ',')
1008 t <- pTSig (noImp syn)
1009 return (map (\x -> (x, t)) ns)
1011tyOptDeclList syn = sepBy1 (do x <- pfName;
1012 t <- option Placeholder (do lchar ':'
1013 pExpr syn)
1014 return (x,t))
1015 (lchar ',')
1017bindList b [] sc = sc
1018bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1020pComprehension syn
1021 = do lchar '['
1022 fc <- pfc
1023 pat <- pExpr syn
1024 lchar '|'
1025 qs <- sepBy1 (pDo syn) (lchar ',')
1026 lchar ']'
1027 return (PDoBlock (map addGuard qs ++
1028 [DoExp fc (PApp fc (PRef fc (UN "return"))
1029 [pexp pat])]))
1030 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1031 [pexp e])
1032 addGuard x = x
1034pDoBlock syn
1035 = do reserved "do"
1036 openBlock
1037 pushIndent
1038 ds <- many1 (do notEndBlock
1039 x <- pDo syn
1040 pKeepTerminator
1041 return x)
1042 popIndent
1043 closeBlock
1044 return (PDoBlock ds)
1046pDo syn
1047 = try (do reserved "let"
1048 i <- pName;
1049 ty <- option Placeholder (do lchar ':'
1050 pExpr' syn)
1051 reservedOp "="
1052 fc <- pfc
1053 e <- pExpr syn
1054 return (DoLet fc i ty e))
1055 <|> try (do reserved "let"
1056 i <- pExpr' syn
1057 reservedOp "="
1058 fc <- pfc
1059 sc <- pExpr syn
1060 return (DoLetP fc i sc))
1061 <|> try (do i <- pName
1062 symbol "<-"
1063 fc <- pfc
1064 e <- pExpr syn;
1065 return (DoBind fc i e))
1066 <|> try (do i <- pExpr' syn
1067 symbol "<-"
1068 fc <- pfc
1069 e <- pExpr syn;
1070 return (DoBindP fc i e))
1071 <|> try (do e <- pExpr syn
1072 fc <- pfc
1073 return (DoExp fc e))
1075pIdiom syn
1076 = do symbol "[|"
1077 fc <- pfc
1078 e <- pExpr syn
1079 symbol "|]"
1080 return (PIdiom fc e)
1082pConstant :: IParser Const
1083pConstant = do reserved "Integer";return BIType
1084 <|> do reserved "Int"; return IType
1085 <|> do reserved "Char"; return ChType
1086 <|> do reserved "Float"; return FlType
1087 <|> do reserved "String"; return StrType
1088 <|> do reserved "Ptr"; return PtrType
1089 <|> do reserved "Bits8"; return B8Type
1090 <|> do reserved "Bits16"; return B16Type
1091 <|> do reserved "Bits32"; return B32Type
1092 <|> do reserved "Bits64"; return B64Type
1093 <|> try (do f <- float; return $ Fl f)
1094-- <|> try (do i <- natural; lchar 'L'; return $ BI i)
1095 <|> try (do i <- natural; return $ I (fromInteger i))
1096 <|> try (do s <- strlit; return $ Str s)
1097 <|> try (do c <- chlit; return $ Ch c)
1099pStatic :: IParser Static
1100pStatic = do lchar '['
1101 reserved "static"
1102 lchar ']';
1103 return Static
1104 <|> return Dynamic
1106table fixes
1107 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1108 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
1109 ++ toTable (reverse fixes) ++
1110 [[backtick],
1111 [binary "=" PEq AssocLeft],
1112 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1114toTable fs = map (map toBin)
1115 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1116 where toBin (Fix (PrefixN _) op) = prefix op
1117 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1118 toBin (Fix f op)
1119 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1120 assoc (Infixl _) = AssocLeft
1121 assoc (Infixr _) = AssocRight
1122 assoc (InfixN _) = AssocNone
1124binary name f = Infix (do fc <- pfc
1125 reservedOp name
1126 doc <- option "" (pDocComment '^')
1127 return (f fc))
1128prefix name f = Prefix (do reservedOp name
1129 fc <- pfc;
1130 return (f fc))
1131backtick = Infix (do lchar '`'; n <- pfName
1132 lchar '`'
1133 fc <- pfc
1134 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1136--------- Data declarations ---------
1138-- (works for classes too - 'abstract' means the data/class is visible but members not)
1139accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1140accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1141 mapM_ (\n -> addAcc n (Just Hidden)) ns
1142accData a n ns = do addAcc n a
1143 mapM_ (`addAcc` a) ns
1145pRecord :: SyntaxInfo -> IParser PDecl
1146pRecord syn = do doc <- option "" (pDocComment '|')
1147 acc <- pAccessibility
1148 reserved "record"
1149 fc <- pfc
1150 tyn_in <- pfName
1151 ty <- pTSig (impOK syn)
1152 let tyn = expandNS syn tyn_in
1153 reserved "where"
1154 openBlock
1155 pushIndent
1156 (cdoc, cn, cty, _) <- pConstructor syn
1157 pKeepTerminator
1158 popIndent
1159 closeBlock
1160 accData acc tyn [cn]
1161 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1162 syn_namespace syn }
1163 let fns = getRecNames rsyn cty
1164 mapM_ (\n -> addAcc n acc) fns
1165 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1166 where
1167 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1168 ++ getRecNames syn sc
1169 getRecNames _ _ = []
1171 toFreeze (Just Frozen) = Just Hidden
1172 toFreeze x = x
1174pDataI = do reserved "data"; return False
1175 <|> do reserved "codata"; return True
1177pData :: SyntaxInfo -> IParser PDecl
1178pData syn = try (do doc <- option "" (pDocComment '|')
1179 acc <- pAccessibility
1180 co <- pDataI
1181 fc <- pfc
1182 tyn_in <- pfName
1183 ty <- pTSig (impOK syn)
1184 let tyn = expandNS syn tyn_in
1185 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1186 reserved "where"
1187 openBlock
1188 pushIndent
1189 cons <- many (do notEndBlock
1190 c <- pConstructor syn
1191 pKeepTerminator
1192 return c) -- (lchar '|')
1193 popIndent
1194 closeBlock
1195 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1196 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1197 <|> try (do doc <- option "" (pDocComment '|')
1198 pushIndent
1199 acc <- pAccessibility
1200 co <- pDataI
1201 fc <- pfc
1202 tyn_in <- pfName
1203 args <- many pName
1204 let ty = bindArgs (map (const PType) args) PType
1205 let tyn = expandNS syn tyn_in
1206 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1207 try (lchar '=') <|> do reserved "where"
1208 let kw = (if co then "co" else "") ++ "data "
1209 let n = show tyn_in ++ " "
1210 let s = kw ++ n
1211 let as = concat (intersperse " " $ map show args) ++ " "
1212 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1213 let ss = concat (intersperse " -> " $ map (const "Type") args)
1214 let fix1 = s ++ as ++ " = ..."
1215 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1216 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1217 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1219 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1220 pTerminator
1221 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1222 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1223 do let cty = bindArgs cargs conty
1224 return (doc, x, cty, cfc)) cons
1225 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1226 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1227 where
1228 mkPApp fc t [] = t
1229 mkPApp fc t xs = PApp fc t (map pexp xs)
1231bindArgs :: [PTerm] -> PTerm -> PTerm
1232bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1234pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1235pConstructor syn
1236 = do doc <- option "" (pDocComment '|')
1237 cn_in <- pfName; fc <- pfc
1238 let cn = expandNS syn cn_in
1239 ty <- pTSig (impOK syn)
1240-- ty' <- implicit syn cn ty
1241 return (doc, cn, ty, fc)
1244pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1245pSimpleCon syn
1246 = do cn_in <- pfName
1247 let cn = expandNS syn cn_in
1248 fc <- pfc
1249 args <- many (do notEndApp
1250 pSimpleExpr syn)
1251 doc <- option "" (pDocComment '^')
1252 return (doc, cn, args, fc)
1254--------- DSL syntax overloading ---------
1256pDSL :: SyntaxInfo -> IParser PDecl
1257pDSL syn = do reserved "dsl"
1258 n <- pfName
1259 openBlock
1260 pushIndent
1261 bs <- many1 (do notEndBlock
1262 b <- pOverload syn
1263 pKeepTerminator
1264 return b)
1265 popIndent; closeBlock
1266 let dsl = mkDSL bs (dsl_info syn)
1267 checkDSL dsl
1268 i <- getState
1269 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1270 return (PDSL n dsl)
1271 where mkDSL bs dsl = let var = lookup "variable" bs
1272 first = lookup "index_first" bs
1273 next = lookup "index_next" bs
1274 leto = lookup "let" bs
1275 lambda = lookup "lambda" bs in
1276 initDSL { dsl_var = var,
1277 index_first = first,
1278 index_next = next,
1279 dsl_lambda = lambda,
1280 dsl_let = leto }
1282checkDSL :: DSL -> IParser ()
1283checkDSL dsl = return ()
1285pOverload :: SyntaxInfo -> IParser (String, PTerm)
1286pOverload syn = do o <- identifier <|> do reserved "let"
1287 return "let"
1288 if o `notElem` overloadable
1289 then fail $ show o ++ " is not an overloading"
1290 else do
1291 lchar '='
1292 t <- pExpr syn
1293 return (o, t)
1294 where overloadable = ["let","lambda","index_first","index_next","variable"]
1296--------- Pattern match clauses ---------
1298pPattern :: SyntaxInfo -> IParser PDecl
1299pPattern syn = do fc <- pfc
1300 clause <- pClause syn
1301 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1303pCAF :: SyntaxInfo -> IParser PDecl
1304pCAF syn = do reserved "let"
1305 n_in <- pfName; let n = expandNS syn n_in
1306 lchar '='
1307 t <- pExpr syn
1308 pTerminator
1309 fc <- pfc
1310 return (PCAF fc n t)
1312pArgExpr syn = let syn' = syn { inPattern = True } in
1313 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1315pRHS :: SyntaxInfo -> Name -> IParser PTerm
1316pRHS syn n = do lchar '='; pExpr syn
1317 <|> do symbol "?="; rhs <- pExpr syn;
1318 return (addLet rhs)
1319 <|> do reserved "impossible"; return PImpossible
1320 where mkN (UN x) = UN (x++"_lemma_1")
1321 mkN (NS x n) = NS (mkN x) n
1322 n' = mkN n
1324 addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1325 addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1326 where addLetC (l, r) = (l, addLet r)
1327 addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1329pClause :: SyntaxInfo -> IParser PClause
1330pClause syn
1331 = try (do pushIndent
1332 n_in <- pfName; let n = expandNS syn n_in
1333 cargs <- many (pConstraintArg syn)
1334 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1335 fc <- pfc
1336 args <- many (pArgExpr syn)
1337 wargs <- many (pWExpr syn)
1338 rhs <- pRHS syn n
1339 ist <- getState
1340 let ctxt = tt_ctxt ist
1341 let wsyn = syn { syn_namespace = [] }
1342 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1343 popIndent
1344 return x,
1345 do pTerminator
1346 return ([], [])]
1347 let capp = PApp fc (PRef fc n)
1348 (iargs ++ cargs ++ map pexp args)
1349 ist <- getState
1350 setState (ist { lastParse = Just n })
1351 return $ PClause fc n capp wargs rhs wheres)
1352 <|> try (do pushIndent
1353 wargs <- many1 (pWExpr syn)
1354 ist <- getState
1355 n <- case lastParse ist of
1356 Just t -> return t
1357 Nothing -> fail "Invalid clause"
1358 fc <- pfc
1359 rhs <- pRHS syn n
1360 let ctxt = tt_ctxt ist
1361 let wsyn = syn { syn_namespace = [] }
1362 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1363 popIndent
1364 return x,
1365 do pTerminator
1366 return ([], [])]
1367 return $ PClauseR fc wargs rhs wheres)
1369 <|> try (do pushIndent
1370 n_in <- pfName; let n = expandNS syn n_in
1371 cargs <- many (pConstraintArg syn)
1372 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1373 fc <- pfc
1374 args <- many (pArgExpr syn)
1375 wargs <- many (pWExpr syn)
1376 let capp = PApp fc (PRef fc n)
1377 (iargs ++ cargs ++ map pexp args)
1378 ist <- getState
1379 setState (ist { lastParse = Just n })
1380 reserved "with"
1381 wval <- pSimpleExpr syn
1382 openBlock
1383 ds <- many1 $ pFunDecl syn
1384 let withs = map (fillLHSD n capp wargs) $ concat ds
1385 closeBlock
1386 popIndent
1387 return $ PWith fc n capp wargs wval withs)
1389 <|> try (do wargs <- many1 (pWExpr syn)
1390 fc <- pfc
1391 reserved "with"
1392 wval <- pSimpleExpr syn
1393 openBlock
1394 ds <- many1 $ pFunDecl syn
1395 let withs = concat ds
1396 closeBlock
1397 return $ PWithR fc wargs wval withs)
1399 <|> do pushIndent
1400 l <- pArgExpr syn
1401 op <- operator
1402 let n = expandNS syn (UN op)
1403 r <- pArgExpr syn
1404 fc <- pfc
1405 wargs <- many (pWExpr syn)
1406 rhs <- pRHS syn n
1407 let wsyn = syn { syn_namespace = [] }
1408 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1409 popIndent
1410 return x,
1411 do pTerminator
1412 return ([], [])]
1413 ist <- getState
1414 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1415 setState (ist { lastParse = Just n })
1416 return $ PClause fc n capp wargs rhs wheres
1418 <|> do l <- pArgExpr syn
1419 op <- operator
1420 let n = expandNS syn (UN op)
1421 r <- pArgExpr syn
1422 fc <- pfc
1423 wargs <- many (pWExpr syn)
1424 reserved "with"
1425 wval <- pSimpleExpr syn
1426 openBlock
1427 ds <- many1 $ pFunDecl syn
1428 closeBlock
1429 ist <- getState
1430 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1431 let withs = map (fillLHSD n capp wargs) $ concat ds
1432 setState (ist { lastParse = Just n })
1433 return $ PWith fc n capp wargs wval withs
1434 where
1435 fillLHS n capp owargs (PClauseR fc wargs v ws)
1436 = PClause fc n capp (owargs ++ wargs) v ws
1437 fillLHS n capp owargs (PWithR fc wargs v ws)
1438 = PWith fc n capp (owargs ++ wargs) v
1439 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1440 fillLHS _ _ _ c = c
1442 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1443 fillLHSD n c a x = x
1445pWExpr :: SyntaxInfo -> IParser PTerm
1446pWExpr syn = do lchar '|'
1447 pExpr' syn
1449pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1450pWhereblock n syn
1451 = do reserved "where"; openBlock
1452 ds <- many1 $ pDecl syn
1453 let dns = concatMap (concatMap declared) ds
1454 closeBlock
1455 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1457pDirective :: IParser [PDecl]
1458pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1459 return [PDirective (do addLib lib
1460 addIBC (IBCLib lib))])
1461 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1462 return [PDirective (do datadir <- liftIO getDataDir
1463 o <- liftIO $ findInPath [".", datadir] obj
1464 addIBC (IBCObj o)
1465 addObjectFile o)])
1466 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1467 return [PDirective (do addHdr hdr
1468 addIBC (IBCHeader hdr))])
1469 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1470 return [PDirective (do setAccessibility n Hidden
1471 addIBC (IBCAccess n Hidden))])
1472 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1473 return [PDirective (do setAccessibility n Frozen
1474 addIBC (IBCAccess n Frozen))])
1475 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1476 return [PDirective (do i <- getIState
1477 putIState (i { default_access = acc }))])
1478 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1479 i <- getState
1480 setState (i { default_total = tot } )
1481 return [PDirective (do i <- getIState
1482 putIState (i { default_total = tot }))])
1483 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1484 return [PDirective (setLogLevel (fromInteger i))])
1486pTactic :: SyntaxInfo -> IParser PTactic
1487pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1488 return $ Intro ns
1489 <|> do reserved "intros"; return Intros
1490 <|> try (do reserved "refine"; n <- pName
1491 imps <- many1 imp
1492 return $ Refine n imps)
1493 <|> do reserved "refine"; n <- pName
1494 i <- getState
1495 return $ Refine n []
1496 <|> do reserved "rewrite"; t <- pExpr syn;
1497 i <- getState
1498 return $ Rewrite (desugar syn i t)
1499 <|> try (do reserved "let"; n <- pName; lchar ':';
1500 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1501 i <- getState
1502 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1503 <|> try (do reserved "let"; n <- pName; lchar '=';
1504 t <- pExpr syn;
1505 i <- getState
1506 return $ LetTac n (desugar syn i t))
1507 <|> do reserved "focus"; n <- pName
1508 return $ Focus n
1509 <|> do reserved "exact"; t <- pExpr syn;
1510 i <- getState
1511 return $ Exact (desugar syn i t)
1512 <|> do reserved "reflect"; t <- pExpr syn;
1513 i <- getState
1514 return $ ReflectTac (desugar syn i t)
1515 <|> do reserved "try"; t <- pTactic syn;
1516 lchar '|';
1517 t1 <- pTactic syn
1518 return $ Try t t1
1519 <|> do lchar '{'
1520 t <- pTactic syn;
1521 lchar ';';
1522 t1 <- pTactic syn;
1523 lchar '}'
1524 return $ TSeq t t1
1525 <|> do reserved "compute"; return Compute
1526 <|> do reserved "trivial"; return Trivial
1527 <|> do reserved "solve"; return Solve
1528 <|> do reserved "attack"; return Attack
1529 <|> do reserved "state"; return ProofState
1530 <|> do reserved "term"; return ProofTerm
1531 <|> do reserved "undo"; return Undo
1532 <|> do reserved "qed"; return Qed
1533 <|> do reserved "abandon"; return Abandon
1534 <|> do lchar ':'; reserved "q"; return Abandon
1535 where
1536 imp = do lchar '?'; return False
1537 <|> do lchar '_'; return True