git.iko.soy/Idris-dev
on b92b12e help sign in
Idris-dev/src/Idris/Parser.hs
1537 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 <|> return opts
711addAcc :: Name -> Maybe Accessibility -> IParser ()
712addAcc n a = do i <- getState
713 setState (i { hide_list = (n, a) : hide_list i })
715pCaseExpr syn = do
716 reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
717 openBlock
718 pushIndent
719 opts <- many1 (do notEndBlock
720 x <- pCaseOpt syn
721 pKeepTerminator
722 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
723 popIndent
724 closeBlock
725 return (PCase fc scr opts)
727pProofExpr syn = do
728 reserved "proof"; lchar '{'
729 ts <- endBy (pTactic syn) (lchar ';')
730 lchar '}'
731 return (PProof ts)
733pTacticsExpr syn = do
734 reserved "tactics"; lchar '{'
735 ts <- endBy (pTactic syn) (lchar ';')
736 lchar '}'
737 return (PTactics ts)
739pSimpleExpr syn =
740 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
741 <|> do lchar '?'; x <- pName; return (PMetavar x)
742 <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
743 <|> do reserved "refl"; fc <- pfc;
744 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
745 return t)
746 return (PRefl fc tm)
747-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
748 <|> pProofExpr syn
749 <|> pTacticsExpr syn
750 <|> pCaseExpr syn
751 <|> try (do x <- pfName
752 fc <- pfc
753 return (PRef fc x))
754 <|> try (do lchar '!'; x <- pfName
755 fc <- pfc
756 return (PInferRef fc x))
757 <|> try (pList syn)
758 <|> try (pAlt syn)
759 <|> try (pIdiom syn)
760 <|> try (do lchar '('
761 bracketed (noImp syn))
762 <|> try (do c <- pConstant
763 fc <- pfc
764 return (modifyConst syn fc (PConstant c)))
765 <|> do reserved "Type"; return PType
766 <|> try (do symbol "()"
767 fc <- pfc
768 return (PTrue fc))
769 <|> try (do symbol "_|_"
770 fc <- pfc
771 return (PFalse fc))
772 <|> do lchar '_'; return Placeholder
773 <|> pSimpleExtExpr syn
775bracketed syn =
776 try (pPair syn)
777 <|> try (do e <- pExpr syn; lchar ')'; return e)
778-- <|> try (do reserved "typed"
779-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
780-- return (PTyped e t))
781 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
782 return $ PLam (MN 1000 "ARG") Placeholder
783 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
784 pexp e]))
785 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
786 return $ PLam (MN 1000 "ARG") Placeholder
787 (PApp fc (PRef fc (UN o)) [pexp e,
788 pexp (PRef fc (MN 1000 "ARG"))]))
790pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
791pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })
792 symbol "=>"; rhs <- pExpr syn
793 return (lhs, rhs)
795modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
796modifyConst syn fc (PConstant (I x))
797 | not (inPattern syn)
798 = PAlternative False
799 [PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))],
800 PConstant (I x), PConstant (BI (toEnum x))]
801 | otherwise = PAlternative False
802 [PConstant (I x), PConstant (BI (toEnum x))]
803modifyConst syn fc x = x
805pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
806 return (mkList fc xs)
807 where
808 mkList fc [] = PRef fc (UN "Nil")
809 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
811pPair syn = try (do l <- pExpr syn
812 fc <- pfc
813 rest <- restTuple
814 case rest of
815 [] -> return l
816 [Left r] -> return (PPair fc l r)
817 [Right r] -> return (PDPair fc l Placeholder r))
818 <|> try (do x <- ntuple
819 lchar ')'
820 return x)
821 <|> do ln <- pName; lchar ':'
822 lty <- pExpr syn
823 reservedOp "**"
824 fc <- pfc
825 r <- pExpr syn
826 lchar ')'
827 return (PDPair fc (PRef fc ln) lty r)
828 where
829 restTuple = do lchar ')'; return []
830 <|> do lchar ','
831 r <- pExpr syn
832 lchar ')'
833 return [Left r]
834 <|> do reservedOp "**"
835 r <- pExpr syn
836 lchar ')'
837 return [Right r]
838 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
839 rest <- ntuple
840 return (PPair fc l rest))
841 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
842 r <- pExpr syn
843 return (PPair fc l r))
845pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
846 return (PAlternative False alts)
848pHSimpleExpr syn
849 = do lchar '.'
850 e <- pSimpleExpr syn
851 return $ PHidden e
852 <|> pSimpleExpr syn
854pApp syn = do f <- pSimpleExpr syn
855 fc <- pfc
856 args <- many1 (do notEndApp
857 pArg syn)
858 i <- getState
859 return (dslify i $ PApp fc f args)
860 where
861 dslify i (PApp fc (PRef _ f) [a])
862 | [d] <- lookupCtxt Nothing f (idris_dsls i)
863 = desugar (syn { dsl_info = d }) i (getTm a)
864 dslify i t = t
866pArg :: SyntaxInfo -> IParser PArg
867pArg syn = try (pImplicitArg syn)
868 <|> try (pConstraintArg syn)
869 <|> do e <- pSimpleExpr syn
870 return (pexp e)
872pImplicitArg syn = do lchar '{'
873 n <- pName
874 fc <- pfc
875 v <- option (PRef fc n) (do lchar '='
876 pExpr syn)
877 lchar '}'
878 return (pimp n v)
880pConstraintArg syn = do symbol "@{"
881 e <- pExpr syn
882 symbol "}"
883 return (pconst e)
885pRecordType syn
886 = do reserved "record"
887 lchar '{'
888 fields <- sepBy1 pFieldType (lchar ',')
889 lchar '}'
890 fc <- pfc
891 rec <- option Nothing (do e <- pSimpleExpr syn
892 return (Just e))
893 case rec of
894 Nothing ->
895 return (PLam (MN 0 "fldx") Placeholder
896 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
897 Just v -> return (applyAll fc fields v)
898 where pFieldType = do n <- pfName
899 lchar '='
900 e <- pExpr syn
901 return (n, e)
902 applyAll fc [] x = x
903 applyAll fc ((n, e) : es) x
904 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
906mkType (UN n) = UN ("set_" ++ n)
907mkType (MN 0 n) = MN 0 ("set_" ++ n)
908mkType (NS n s) = NS (mkType n) s
910noImp syn = syn { implicitAllowed = False }
911impOK syn = syn { implicitAllowed = True }
913pTSig syn = do lchar ':'; pTExpr syn
915pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
916 sc <- pExpr syn
917 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
919pLambda syn = do lchar '\\'
920 try (do xt <- tyOptDeclList syn
921 symbol "=>"
922 sc <- pExpr syn
923 return (bindList PLam xt sc)
924 <|> (do ps <- sepBy (do fc <- pfc
925 e <- pSimpleExpr syn
926 return (fc, e)) (lchar ',')
927 symbol "=>"
928 sc <- pExpr syn
929 return (pmList (zip [0..] ps) sc)))
930 where pmList [] sc = sc
931 pmList ((i, (fc, x)) : xs) sc
932 = PLam (MN i "lamp") Placeholder
933 (PCase fc (PRef fc (MN i "lamp"))
934 [(x, pmList xs sc)])
936pLet syn = try (do reserved "let"; n <- pName;
937 ty <- option Placeholder (do lchar ':'; pExpr' syn)
938 lchar '='
939 v <- pExpr syn
940 reserved "in"; sc <- pExpr syn
941 return (PLet n ty v sc))
942 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
943 symbol "="; v <- pExpr syn
944 reserved "in"; sc <- pExpr syn
945 return (PCase fc v [(pat, sc)]))
947pPi syn =
948 try (do lazy <- option False (do lchar '|'; return True)
949 st <- pStatic
950 lchar '('; xt <- tyDeclList syn; lchar ')'
951 doc <- option "" (pDocComment '^')
952 symbol "->"
953 sc <- pExpr syn
954 return (bindList (PPi (Exp lazy st doc)) xt sc))
955 <|> try (if implicitAllowed syn
956 then do lazy <- option False (do lchar '|'
957 return True)
958 st <- pStatic
959 lchar '{'
960 xt <- tyDeclList syn
961 lchar '}'
962 symbol "->"
963 sc <- pExpr syn
964 return (bindList (PPi (Imp lazy st "")) xt sc)
965 else fail "No implicit arguments allowed here")
966 <|> try (do lchar '{'
967 reserved "auto"
968 xt <- tyDeclList syn
969 lchar '}'
970 symbol "->"
971 sc <- pExpr syn
972 return (bindList (PPi
973 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
974 <|> try (do lchar '{'
975 reserved "default"
976 script <- pSimpleExpr syn
977 xt <- tyDeclList syn
978 lchar '}'
979 symbol "->"
980 sc <- pExpr syn
981 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
982 <|> do --lazy <- option False (do lchar '|'; return True)
983 lchar '{'
984 reserved "static"
985 lchar '}'
986 t <- pExpr' syn
987 symbol "->"
988 sc <- pExpr syn
989 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
991pConstList :: SyntaxInfo -> IParser [PTerm]
992pConstList syn = try (do lchar '('
993 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
994 lchar ')'
995 reservedOp "=>"
996 return tys)
997 <|> try (do t <- pExpr (noImp syn)
998 reservedOp "=>"
999 return [t])
1000 <|> return []
1002tyDeclList syn = try (sepBy1 (do x <- pfName
1003 t <- pTSig (noImp syn)
1004 return (x,t))
1005 (lchar ','))
1006 <|> do ns <- sepBy1 pName (lchar ',')
1007 t <- pTSig (noImp syn)
1008 return (map (\x -> (x, t)) ns)
1010tyOptDeclList syn = sepBy1 (do x <- pfName;
1011 t <- option Placeholder (do lchar ':'
1012 pExpr syn)
1013 return (x,t))
1014 (lchar ',')
1016bindList b [] sc = sc
1017bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1019pComprehension syn
1020 = do lchar '['
1021 fc <- pfc
1022 pat <- pExpr syn
1023 lchar '|'
1024 qs <- sepBy1 (pDo syn) (lchar ',')
1025 lchar ']'
1026 return (PDoBlock (map addGuard qs ++
1027 [DoExp fc (PApp fc (PRef fc (UN "return"))
1028 [pexp pat])]))
1029 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1030 [pexp e])
1031 addGuard x = x
1033pDoBlock syn
1034 = do reserved "do"
1035 openBlock
1036 pushIndent
1037 ds <- many1 (do notEndBlock
1038 x <- pDo syn
1039 pKeepTerminator
1040 return x)
1041 popIndent
1042 closeBlock
1043 return (PDoBlock ds)
1045pDo syn
1046 = try (do reserved "let"
1047 i <- pName;
1048 ty <- option Placeholder (do lchar ':'
1049 pExpr' syn)
1050 reservedOp "="
1051 fc <- pfc
1052 e <- pExpr syn
1053 return (DoLet fc i ty e))
1054 <|> try (do reserved "let"
1055 i <- pExpr' syn
1056 reservedOp "="
1057 fc <- pfc
1058 sc <- pExpr syn
1059 return (DoLetP fc i sc))
1060 <|> try (do i <- pName
1061 symbol "<-"
1062 fc <- pfc
1063 e <- pExpr syn;
1064 return (DoBind fc i e))
1065 <|> try (do i <- pExpr' syn
1066 symbol "<-"
1067 fc <- pfc
1068 e <- pExpr syn;
1069 return (DoBindP fc i e))
1070 <|> try (do e <- pExpr syn
1071 fc <- pfc
1072 return (DoExp fc e))
1074pIdiom syn
1075 = do symbol "[|"
1076 fc <- pfc
1077 e <- pExpr syn
1078 symbol "|]"
1079 return (PIdiom fc e)
1081pConstant :: IParser Const
1082pConstant = do reserved "Integer";return BIType
1083 <|> do reserved "Int"; return IType
1084 <|> do reserved "Char"; return ChType
1085 <|> do reserved "Float"; return FlType
1086 <|> do reserved "String"; return StrType
1087 <|> do reserved "Ptr"; return PtrType
1088 <|> do reserved "Bits8"; return B8Type
1089 <|> do reserved "Bits16"; return B16Type
1090 <|> do reserved "Bits32"; return B32Type
1091 <|> do reserved "Bits64"; return B64Type
1092 <|> try (do f <- float; return $ Fl f)
1093-- <|> try (do i <- natural; lchar 'L'; return $ BI i)
1094 <|> try (do i <- natural; return $ I (fromInteger i))
1095 <|> try (do s <- strlit; return $ Str s)
1096 <|> try (do c <- chlit; return $ Ch c)
1098pStatic :: IParser Static
1099pStatic = do lchar '['
1100 reserved "static"
1101 lchar ']';
1102 return Static
1103 <|> return Dynamic
1105table fixes
1106 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1107 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
1108 ++ toTable (reverse fixes) ++
1109 [[backtick],
1110 [binary "=" PEq AssocLeft],
1111 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1113toTable fs = map (map toBin)
1114 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1115 where toBin (Fix (PrefixN _) op) = prefix op
1116 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1117 toBin (Fix f op)
1118 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1119 assoc (Infixl _) = AssocLeft
1120 assoc (Infixr _) = AssocRight
1121 assoc (InfixN _) = AssocNone
1123binary name f = Infix (do fc <- pfc
1124 reservedOp name
1125 doc <- option "" (pDocComment '^')
1126 return (f fc))
1127prefix name f = Prefix (do reservedOp name
1128 fc <- pfc;
1129 return (f fc))
1130backtick = Infix (do lchar '`'; n <- pfName
1131 lchar '`'
1132 fc <- pfc
1133 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1135--------- Data declarations ---------
1137-- (works for classes too - 'abstract' means the data/class is visible but members not)
1138accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1139accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1140 mapM_ (\n -> addAcc n (Just Hidden)) ns
1141accData a n ns = do addAcc n a
1142 mapM_ (`addAcc` a) ns
1144pRecord :: SyntaxInfo -> IParser PDecl
1145pRecord syn = do doc <- option "" (pDocComment '|')
1146 acc <- pAccessibility
1147 reserved "record"
1148 fc <- pfc
1149 tyn_in <- pfName
1150 ty <- pTSig (impOK syn)
1151 let tyn = expandNS syn tyn_in
1152 reserved "where"
1153 openBlock
1154 pushIndent
1155 (cdoc, cn, cty, _) <- pConstructor syn
1156 pKeepTerminator
1157 popIndent
1158 closeBlock
1159 accData acc tyn [cn]
1160 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1161 syn_namespace syn }
1162 let fns = getRecNames rsyn cty
1163 mapM_ (\n -> addAcc n acc) fns
1164 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1165 where
1166 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1167 ++ getRecNames syn sc
1168 getRecNames _ _ = []
1170 toFreeze (Just Frozen) = Just Hidden
1171 toFreeze x = x
1173pDataI = do reserved "data"; return False
1174 <|> do reserved "codata"; return True
1176pData :: SyntaxInfo -> IParser PDecl
1177pData syn = try (do doc <- option "" (pDocComment '|')
1178 acc <- pAccessibility
1179 co <- pDataI
1180 fc <- pfc
1181 tyn_in <- pfName
1182 ty <- pTSig (impOK syn)
1183 let tyn = expandNS syn tyn_in
1184 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1185 reserved "where"
1186 openBlock
1187 pushIndent
1188 cons <- many (do notEndBlock
1189 c <- pConstructor syn
1190 pKeepTerminator
1191 return c) -- (lchar '|')
1192 popIndent
1193 closeBlock
1194 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1195 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1196 <|> try (do doc <- option "" (pDocComment '|')
1197 pushIndent
1198 acc <- pAccessibility
1199 co <- pDataI
1200 fc <- pfc
1201 tyn_in <- pfName
1202 args <- many pName
1203 let ty = bindArgs (map (const PType) args) PType
1204 let tyn = expandNS syn tyn_in
1205 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1206 try (lchar '=') <|> do reserved "where"
1207 let kw = (if co then "co" else "") ++ "data "
1208 let n = show tyn_in ++ " "
1209 let s = kw ++ n
1210 let as = concat (intersperse " " $ map show args) ++ " "
1211 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1212 let ss = concat (intersperse " -> " $ map (const "Type") args)
1213 let fix1 = s ++ as ++ " = ..."
1214 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1215 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1216 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1218 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1219 pTerminator
1220 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1221 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1222 do let cty = bindArgs cargs conty
1223 return (doc, x, cty, cfc)) cons
1224 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1225 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1226 where
1227 mkPApp fc t [] = t
1228 mkPApp fc t xs = PApp fc t (map pexp xs)
1230bindArgs :: [PTerm] -> PTerm -> PTerm
1231bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1233pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1234pConstructor syn
1235 = do doc <- option "" (pDocComment '|')
1236 cn_in <- pfName; fc <- pfc
1237 let cn = expandNS syn cn_in
1238 ty <- pTSig (impOK syn)
1239-- ty' <- implicit syn cn ty
1240 return (doc, cn, ty, fc)
1243pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1244pSimpleCon syn
1245 = do cn_in <- pfName
1246 let cn = expandNS syn cn_in
1247 fc <- pfc
1248 args <- many (do notEndApp
1249 pSimpleExpr syn)
1250 doc <- option "" (pDocComment '^')
1251 return (doc, cn, args, fc)
1253--------- DSL syntax overloading ---------
1255pDSL :: SyntaxInfo -> IParser PDecl
1256pDSL syn = do reserved "dsl"
1257 n <- pfName
1258 openBlock
1259 pushIndent
1260 bs <- many1 (do notEndBlock
1261 b <- pOverload syn
1262 pKeepTerminator
1263 return b)
1264 popIndent; closeBlock
1265 let dsl = mkDSL bs (dsl_info syn)
1266 checkDSL dsl
1267 i <- getState
1268 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1269 return (PDSL n dsl)
1270 where mkDSL bs dsl = let var = lookup "variable" bs
1271 first = lookup "index_first" bs
1272 next = lookup "index_next" bs
1273 leto = lookup "let" bs
1274 lambda = lookup "lambda" bs in
1275 initDSL { dsl_var = var,
1276 index_first = first,
1277 index_next = next,
1278 dsl_lambda = lambda,
1279 dsl_let = leto }
1281checkDSL :: DSL -> IParser ()
1282checkDSL dsl = return ()
1284pOverload :: SyntaxInfo -> IParser (String, PTerm)
1285pOverload syn = do o <- identifier <|> do reserved "let"
1286 return "let"
1287 if o `notElem` overloadable
1288 then fail $ show o ++ " is not an overloading"
1289 else do
1290 lchar '='
1291 t <- pExpr syn
1292 return (o, t)
1293 where overloadable = ["let","lambda","index_first","index_next","variable"]
1295--------- Pattern match clauses ---------
1297pPattern :: SyntaxInfo -> IParser PDecl
1298pPattern syn = do fc <- pfc
1299 clause <- pClause syn
1300 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1302pCAF :: SyntaxInfo -> IParser PDecl
1303pCAF syn = do reserved "let"
1304 n_in <- pfName; let n = expandNS syn n_in
1305 lchar '='
1306 t <- pExpr syn
1307 pTerminator
1308 fc <- pfc
1309 return (PCAF fc n t)
1311pArgExpr syn = let syn' = syn { inPattern = True } in
1312 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1314pRHS :: SyntaxInfo -> Name -> IParser PTerm
1315pRHS syn n = do lchar '='; pExpr syn
1316 <|> do symbol "?="; rhs <- pExpr syn;
1317 return (addLet rhs)
1318 <|> do reserved "impossible"; return PImpossible
1319 where mkN (UN x) = UN (x++"_lemma_1")
1320 mkN (NS x n) = NS (mkN x) n
1321 n' = mkN n
1323 addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1324 addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1325 where addLetC (l, r) = (l, addLet r)
1326 addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1328pClause :: SyntaxInfo -> IParser PClause
1329pClause syn
1330 = try (do pushIndent
1331 n_in <- pfName; let n = expandNS syn n_in
1332 cargs <- many (pConstraintArg syn)
1333 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1334 fc <- pfc
1335 args <- many (pArgExpr syn)
1336 wargs <- many (pWExpr syn)
1337 rhs <- pRHS syn n
1338 ist <- getState
1339 let ctxt = tt_ctxt ist
1340 let wsyn = syn { syn_namespace = [] }
1341 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1342 popIndent
1343 return x,
1344 do pTerminator
1345 return ([], [])]
1346 let capp = PApp fc (PRef fc n)
1347 (iargs ++ cargs ++ map pexp args)
1348 ist <- getState
1349 setState (ist { lastParse = Just n })
1350 return $ PClause fc n capp wargs rhs wheres)
1351 <|> try (do pushIndent
1352 wargs <- many1 (pWExpr syn)
1353 ist <- getState
1354 n <- case lastParse ist of
1355 Just t -> return t
1356 Nothing -> fail "Invalid clause"
1357 fc <- pfc
1358 rhs <- pRHS syn n
1359 let ctxt = tt_ctxt ist
1360 let wsyn = syn { syn_namespace = [] }
1361 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1362 popIndent
1363 return x,
1364 do pTerminator
1365 return ([], [])]
1366 return $ PClauseR fc wargs rhs wheres)
1368 <|> try (do pushIndent
1369 n_in <- pfName; let n = expandNS syn n_in
1370 cargs <- many (pConstraintArg syn)
1371 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1372 fc <- pfc
1373 args <- many (pArgExpr syn)
1374 wargs <- many (pWExpr syn)
1375 let capp = PApp fc (PRef fc n)
1376 (iargs ++ cargs ++ map pexp args)
1377 ist <- getState
1378 setState (ist { lastParse = Just n })
1379 reserved "with"
1380 wval <- pSimpleExpr syn
1381 openBlock
1382 ds <- many1 $ pFunDecl syn
1383 let withs = map (fillLHSD n capp wargs) $ concat ds
1384 closeBlock
1385 popIndent
1386 return $ PWith fc n capp wargs wval withs)
1388 <|> try (do wargs <- many1 (pWExpr syn)
1389 fc <- pfc
1390 reserved "with"
1391 wval <- pSimpleExpr syn
1392 openBlock
1393 ds <- many1 $ pFunDecl syn
1394 let withs = concat ds
1395 closeBlock
1396 return $ PWithR fc wargs wval withs)
1398 <|> do pushIndent
1399 l <- pArgExpr syn
1400 op <- operator
1401 let n = expandNS syn (UN op)
1402 r <- pArgExpr syn
1403 fc <- pfc
1404 wargs <- many (pWExpr syn)
1405 rhs <- pRHS syn n
1406 let wsyn = syn { syn_namespace = [] }
1407 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1408 popIndent
1409 return x,
1410 do pTerminator
1411 return ([], [])]
1412 ist <- getState
1413 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1414 setState (ist { lastParse = Just n })
1415 return $ PClause fc n capp wargs rhs wheres
1417 <|> do l <- pArgExpr syn
1418 op <- operator
1419 let n = expandNS syn (UN op)
1420 r <- pArgExpr syn
1421 fc <- pfc
1422 wargs <- many (pWExpr syn)
1423 reserved "with"
1424 wval <- pSimpleExpr syn
1425 openBlock
1426 ds <- many1 $ pFunDecl syn
1427 closeBlock
1428 ist <- getState
1429 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1430 let withs = map (fillLHSD n capp wargs) $ concat ds
1431 setState (ist { lastParse = Just n })
1432 return $ PWith fc n capp wargs wval withs
1433 where
1434 fillLHS n capp owargs (PClauseR fc wargs v ws)
1435 = PClause fc n capp (owargs ++ wargs) v ws
1436 fillLHS n capp owargs (PWithR fc wargs v ws)
1437 = PWith fc n capp (owargs ++ wargs) v
1438 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1439 fillLHS _ _ _ c = c
1441 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1442 fillLHSD n c a x = x
1444pWExpr :: SyntaxInfo -> IParser PTerm
1445pWExpr syn = do lchar '|'
1446 pExpr' syn
1448pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1449pWhereblock n syn
1450 = do reserved "where"; openBlock
1451 ds <- many1 $ pDecl syn
1452 let dns = concatMap (concatMap declared) ds
1453 closeBlock
1454 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1456pDirective :: IParser [PDecl]
1457pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1458 return [PDirective (do addLib lib
1459 addIBC (IBCLib lib))])
1460 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1461 return [PDirective (do datadir <- liftIO getDataDir
1462 o <- liftIO $ findInPath [".", datadir] obj
1463 addIBC (IBCObj o)
1464 addObjectFile o)])
1465 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1466 return [PDirective (do addHdr hdr
1467 addIBC (IBCHeader hdr))])
1468 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1469 return [PDirective (do setAccessibility n Hidden
1470 addIBC (IBCAccess n Hidden))])
1471 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1472 return [PDirective (do setAccessibility n Frozen
1473 addIBC (IBCAccess n Frozen))])
1474 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1475 return [PDirective (do i <- getIState
1476 putIState (i { default_access = acc }))])
1477 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1478 i <- getState
1479 setState (i { default_total = tot } )
1480 return [PDirective (do i <- getIState
1481 putIState (i { default_total = tot }))])
1482 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1483 return [PDirective (setLogLevel (fromInteger i))])
1485pTactic :: SyntaxInfo -> IParser PTactic
1486pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1487 return $ Intro ns
1488 <|> do reserved "intros"; return Intros
1489 <|> try (do reserved "refine"; n <- pName
1490 imps <- many1 imp
1491 return $ Refine n imps)
1492 <|> do reserved "refine"; n <- pName
1493 i <- getState
1494 return $ Refine n []
1495 <|> do reserved "rewrite"; t <- pExpr syn;
1496 i <- getState
1497 return $ Rewrite (desugar syn i t)
1498 <|> try (do reserved "let"; n <- pName; lchar ':';
1499 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1500 i <- getState
1501 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1502 <|> try (do reserved "let"; n <- pName; lchar '=';
1503 t <- pExpr syn;
1504 i <- getState
1505 return $ LetTac n (desugar syn i t))
1506 <|> do reserved "focus"; n <- pName
1507 return $ Focus n
1508 <|> do reserved "exact"; t <- pExpr syn;
1509 i <- getState
1510 return $ Exact (desugar syn i t)
1511 <|> do reserved "reflect"; t <- pExpr syn;
1512 i <- getState
1513 return $ ReflectTac (desugar syn i t)
1514 <|> do reserved "try"; t <- pTactic syn;
1515 lchar '|';
1516 t1 <- pTactic syn
1517 return $ Try t t1
1518 <|> do lchar '{'
1519 t <- pTactic syn;
1520 lchar ';';
1521 t1 <- pTactic syn;
1522 lchar '}'
1523 return $ TSeq t t1
1524 <|> do reserved "compute"; return Compute
1525 <|> do reserved "trivial"; return Trivial
1526 <|> do reserved "solve"; return Solve
1527 <|> do reserved "attack"; return Attack
1528 <|> do reserved "state"; return ProofState
1529 <|> do reserved "term"; return ProofTerm
1530 <|> do reserved "undo"; return Undo
1531 <|> do reserved "qed"; return Qed
1532 <|> do reserved "abandon"; return Abandon
1533 <|> do lchar ':'; reserved "q"; return Abandon
1534 where
1535 imp = do lchar '?'; return False
1536 <|> do lchar '_'; return True