git.iko.soy/Idris-dev
on 5242001 help sign in
Idris-dev/src/Idris/Parser.hs
1663 lines 67 kB history raw
1{-# LANGUAGE PatternGuards, ScopedTypeVariables #-}
2-- | Parse the full Idris language.
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 Idris.Providers
15import Paths_idris
17import Util.DynamicLinker
19import Core.CoreParser
20import Core.TT
21import Core.Evaluate
23import Text.Parsec
24import Text.Parsec.Error
25import Text.Parsec.Expr
26import Text.Parsec.Language
27import Text.Parsec.String
28import qualified Text.Parsec.Token as PTok
30import Data.List
31import Data.List.Split(splitOn)
32import Control.Monad.State
33import Control.Monad.Error
34import Debug.Trace
35import Data.Maybe
36import System.FilePath
38type TokenParser a = PTok.TokenParser a
40type IParser = GenParser Char IState
42lexer :: TokenParser IState
43lexer = idrisLexer
45whiteSpace = PTok.whiteSpace lexer
46lexeme = PTok.lexeme lexer
47symbol = PTok.symbol lexer
48natural = PTok.natural lexer
49parens = PTok.parens lexer
50semi = PTok.semi lexer
51comma = PTok.comma lexer
52identifier = PTok.identifier lexer
53reserved = PTok.reserved lexer
54operator = PTok.operator lexer
55reservedOp = PTok.reservedOp lexer
56integer = PTok.integer lexer
57float = PTok.float lexer
58strlit = PTok.stringLiteral lexer
59chlit = PTok.charLiteral lexer
60lchar = lexeme.char
62fixErrorMsg :: String -> [String] -> String
63fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
65-- Loading modules
67loadModule :: FilePath -> Idris String
68loadModule f
69 = idrisCatch (do i <- getIState
70 let file = takeWhile (/= ' ') f
71 ibcsd <- valIBCSubDir i
72 ids <- allImportDirs i
73 fp <- liftIO $ findImport ids ibcsd file
74 if file `elem` imported i
75 then iLOG $ "Already read " ++ file
76 else do putIState (i { imported = file : imported i })
77 case fp of
78 IDR fn -> loadSource False fn
79 LIDR fn -> loadSource True fn
80 IBC fn src ->
81 idrisCatch (loadIBC fn)
82 (\c -> do iLOG $ fn ++ " failed " ++ show c
83 case src of
84 IDR sfn -> loadSource False sfn
85 LIDR sfn -> loadSource True sfn)
86 let (dir, fh) = splitFileName file
87 return (dropExtension fh))
88 (\e -> do let msg = show e
89 setErrLine (getErrLine msg)
90 iputStrLn msg
91 return "")
93loadSource :: Bool -> FilePath -> Idris ()
94loadSource lidr f
95 = do iLOG ("Reading " ++ f)
96 i <- getIState
97 let def_total = default_total i
98 file_in <- liftIO $ readFile f
99 file <- if lidr then tclift $ unlit f file_in else return file_in
100 (mname, modules, rest, pos) <- parseImports f file
101 i <- getIState
102 putIState (i { default_access = Hidden })
103 mapM_ loadModule modules
104 clearIBC -- start a new .ibc file
105 mapM_ (addIBC . IBCImport) modules
106 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
107 f rest pos
108 unless (null ds') $ do
109 let ds = namespaces mname ds'
110 logLvl 3 (dumpDecls ds)
111 i <- getIState
112 logLvl 10 (show (toAlist (idris_implicits i)))
113 logLvl 3 (show (idris_infixes i))
114 -- Now add all the declarations to the context
115 v <- verbose
116 when v $ iputStrLn $ "Type checking " ++ f
117 elabDecls toplevel ds
118 i <- getIState
119 -- simplify every definition do give the totality checker
120 -- a better chance
121 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
122 updateContext (simplifyCasedef n))
123 (map snd (idris_totcheck i))
124 -- build size change graph from simplified definitions
125 iLOG "Totality checking"
126 i <- getIState
127 mapM_ buildSCG (idris_totcheck i)
128 mapM_ checkDeclTotality (idris_totcheck i)
129 iLOG ("Finished " ++ f)
130 ibcsd <- valIBCSubDir i
131 let ibc = ibcPathNoFallback ibcsd f
132 iLOG "Universe checking"
133 iucheck
134 i <- getIState
135 addHides (hide_list i)
136 ok <- noErrors
137 when ok $
138 idrisCatch (do writeIBC f ibc; clearIBC)
139 (\c -> return ()) -- failure is harmless
140 i <- getIState
141 putIState (i { default_total = def_total,
142 hide_list = [] })
143 return ()
144 return ()
145 where
146 namespaces [] ds = ds
147 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
149addHides :: [(Name, Maybe Accessibility)] -> Idris ()
150addHides xs = do i <- getIState
151 let defh = default_access i
152 let (hs, as) = partition isNothing xs
153 unless (null as) $
154 mapM_ doHide
155 (map (\ (n, _) -> (n, defh)) hs ++
156 map (\ (n, Just a) -> (n, a)) as)
157 where isNothing (_, Nothing) = True
158 isNothing _ = False
160 doHide (n, a) = do setAccessibility n a
161 addIBC (IBCAccess n a)
163parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
164parseTac i = runParser (do t <- pTactic defaultSyntax
165 eof
166 return t) i "(proof)"
168parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
169parseImports fname input
170 = do i <- getIState
171 case runParser (do whiteSpace
172 mname <- pHeader
173 ps <- many pImport
174 rest <- getInput
175 pos <- getPosition
176 return ((mname, ps, rest, pos), i)) i fname input of
177 Left err -> fail (show err)
178 Right (x, i) -> do putIState i
179 return x
181pHeader :: IParser [String]
182pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
183 return (parseName i))
184 <|> return []
185 where parseName x = case span (/='.') x of
186 (x, "") -> [x]
187 (x, '.':y) -> x : parseName y
189pushIndent :: IParser ()
190pushIndent = do pos <- getPosition
191 ist <- getState
192 setState (ist { indent_stack = sourceColumn pos :
193 indent_stack ist })
195lastIndent :: IParser Int
196lastIndent = do ist <- getState
197 case indent_stack ist of
198 (x : xs) -> return x
199 _ -> return 1
201indent :: IParser Int
202indent = liftM sourceColumn getPosition
204popIndent :: IParser ()
205popIndent = do ist <- getState
206 let (x : xs) = indent_stack ist
207 setState (ist { indent_stack = xs })
209openBlock :: IParser ()
210openBlock = do lchar '{'
211 ist <- getState
212 setState (ist { brace_stack = Nothing : brace_stack ist })
213 <|> do ist <- getState
214 lvl <- indent
215 setState (ist { brace_stack = Just lvl : brace_stack ist })
217closeBlock :: IParser ()
218closeBlock = do ist <- getState
219 bs <- case brace_stack ist of
220 [] -> eof >> return []
221 Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])
222 Just lvl : xs -> (do i <- indent
223 inp <- getInput
224-- trace (show (take 10 inp, i, lvl)) $
225 if i >= lvl && take 1 inp /= ")"
226 then fail "Not end of block"
227 else return xs) <|> (eof >> return [])
228 setState (ist { brace_stack = bs })
230pTerminator = do lchar ';'; popIndent
231 <|> do c <- indent; l <- lastIndent
232 if c <= l
233 then popIndent
234 else fail "Not a terminator"
235 <|> do i <- getInput
236 if "}" `isPrefixOf` i || ")" `isPrefixOf` i
237 then popIndent
238 else fail "Not a terminator"
239 <|> lookAhead eof
241pBarTerminator
242 = do lchar '|'; return ()
243 <|> do c <- indent; l <- lastIndent
244 unless (c <= l) $ fail "Not a terminator"
245 <|> lookAhead eof
247pKeepTerminator
248 = do lchar ';'; return ()
249 <|> do c <- indent; l <- lastIndent
250 unless (c <= l) $ fail "Not a terminator"
251 <|> do i <- getInput
252 let h = take 1 i
253 unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"
254 <|> lookAhead eof
256notEndApp = do c <- indent; l <- lastIndent
257 i <- getInput
258 when (c <= l) $ fail "Terminator"
260notEndBlock = do ist <- getState
261 case brace_stack ist of
262 Just lvl : xs -> do i <- indent
263 inp <- getInput
264 when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"
265 _ -> return ()
267-- | Use Parsec's internal state to construct a source code position
268pfc :: IParser FC
269pfc = do s <- getPosition
270 let (dir, file) = splitFileName (sourceName s)
271 let f = if dir == addTrailingPathSeparator "." then file else sourceName s
272 return $ FC f (sourceLine s)
274pImport :: IParser String
275pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')
276 return (toPath f)
277 where toPath n = foldl1' (</>) $ splitOn "." n
279-- | A program is a list of declarations, possibly with associated
280-- documentation strings.
281parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->
282 Idris [PDecl]
283parseProg syn fname input pos
284 = do i <- getIState
285 case runParser (do setPosition pos
286 whiteSpace
287 ps <- many (pDecl syn)
288 eof
289 i' <- getState
290 return (concat ps, i')) i fname input of
291 Left err -> do iputStrLn (show err)
292 return []
293 Right (x, i) -> do putIState i
294 return (collect x)
296-- | Collect 'PClauses' with the same function name
297collect :: [PDecl] -> [PDecl]
298collect (c@(PClauses _ o _ _) : ds)
299 = clauses (cname c) [] (c : ds)
300 where clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
301 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
302 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
303 | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
304 clauses (Just n) acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
305 clauses Nothing acc (x:xs) = collect xs
306 clauses Nothing acc [] = []
308 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
309 cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
310 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
311 cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
312 getfc (PClauses fc _ _ _) = fc
314collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
315collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
316collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
317collect (PClass doc f s cs n ps ds : ds')
318 = PClass doc f s cs n ps (collect ds) : collect ds'
319collect (PInstance f s cs n ps t en ds : ds')
320 = PInstance f s cs n ps t en (collect ds) : collect ds'
321collect (d : ds) = d : collect ds
322collect [] = []
324pFullExpr :: SyntaxInfo -> IParser PTerm
325pFullExpr syn
326 = do x <- pExpr syn; eof;
327 i <- getState
328 return $ desugar syn i x
330-- | Parse a top-level declaration
331pDecl :: SyntaxInfo -> IParser [PDecl]
332pDecl syn = do notEndBlock
333 pDeclBody where
334 pDeclBody
335 = do d <- pDecl' syn
336 i <- getState
337 let d' = fmap (desugar syn i) d
338 return [d']
339 <|> pUsing syn
340 <|> pParams syn
341 <|> pMutual syn
342 <|> pNamespace syn
343 <|> pClass syn
344 <|> pInstance syn
345 <|> do d <- pDSL syn; return [d]
346 <|> pDirective syn
347 <|> pProvider syn
348 <|> try (do reserved "import"; fp <- identifier
349 fail "imports must be at the top of file")
351pFunDecl :: SyntaxInfo -> IParser [PDecl]
352pFunDecl syn
353 = try (do notEndBlock
354 d <- pFunDecl' syn
355 i <- getState
356 let d' = fmap (desugar syn i) d
357 return [d'])
359--------- Top Level Declarations ---------
361pDecl' :: SyntaxInfo -> IParser PDecl
362pDecl' syn
363 = try pFixity
364 <|> try (pFunDecl' syn)
365 <|> try (pData syn)
366 <|> try (pRecord syn)
367 <|> try (pSyntaxDecl syn)
369pSyntaxDecl :: SyntaxInfo -> IParser PDecl
370pSyntaxDecl syn
371 = do s <- pSyntaxRule syn
372 i <- getState
373 let rs = syntax_rules i
374 let ns = syntax_keywords i
375 let ibc = ibc_write i
376 let ks = map show (names s)
377 setState (i { syntax_rules = s : rs,
378 syntax_keywords = ks ++ ns,
379 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
380 })
381 fc <- pfc
382 return (PSyntax fc s)
383 where
384 names (Rule syms _ _) = mapMaybe ename syms
385 ename (Keyword n) = Just n
386 ename _ = Nothing
388pSyntaxRule :: SyntaxInfo -> IParser Syntax
389pSyntaxRule syn
390 = do pushIndent
391 sty <- option AnySyntax (do reserved "term"; return TermSyntax
392 <|> do reserved "pattern"; return PatternSyntax)
393 reserved "syntax"
394 syms <- many1 pSynSym
395 when (all expr syms) $ fail "No keywords in syntax rule"
396 let ns = mapMaybe name syms
397 when (length ns /= length (nub ns))
398 $ fail "Repeated variable in syntax rule"
399 lchar '='
400 tm <- pTExpr (impOK syn)
401 pTerminator
402 return (Rule (mkSimple syms) tm sty)
403 where
404 expr (Expr _) = True
405 expr _ = False
406 name (Expr n) = Just n
407 name _ = Nothing
409 -- Can't parse two full expressions (i.e. expressions with application) in a row
410 -- so change them both to a simple expression
412 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
413 mkSimple xs = mkSimple' xs
415 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
416 mkSimple es
417 mkSimple' (e : es) = e : mkSimple' es
418 mkSimple' [] = []
420pSynSym :: IParser SSymbol
421pSynSym = try (do lchar '['; n <- pName; lchar ']'
422 return (Expr n))
423 <|> try (do lchar '{'; n <- pName; lchar '}'
424 return (Binding n))
425 <|> do n <- iName []
426 return (Keyword n)
427 <|> do sym <- strlit
428 return (Symbol sym)
430pFunDecl' :: SyntaxInfo -> IParser PDecl
431pFunDecl' syn = try (do doc <- option "" (pDocComment '|')
432 pushIndent
433 ist <- getState
434 let initOpts = if default_total ist
435 then [TotalFn]
436 else []
437 opts <- pFnOpts initOpts
438 acc <- pAccessibility
439 opts' <- pFnOpts opts
440 n_in <- pfName
441 let n = expandNS syn n_in
442 fc <- pfc
443 ty <- pTSig (impOK syn)
444 pTerminator
445-- ty' <- implicit syn n ty
446 addAcc n acc
447 return (PTy doc syn fc opts' n ty))
448 <|> try (pPostulate syn)
449 <|> try (pPattern syn)
450 <|> try (pCAF syn)
452pPostulate :: SyntaxInfo -> IParser PDecl
453pPostulate syn = do doc <- option "" (pDocComment '|')
454 pushIndent
455 reserved "postulate"
456 ist <- getState
457 let initOpts = if default_total ist
458 then [TotalFn]
459 else []
460 opts <- pFnOpts initOpts
461 acc <- pAccessibility
462 opts' <- pFnOpts opts
463 n_in <- pfName
464 let n = expandNS syn n_in
465 ty <- pTSig (impOK syn)
466 fc <- pfc
467 pTerminator
468 addAcc n acc
469 return (PPostulate doc syn fc opts' n ty)
472pUsing :: SyntaxInfo -> IParser [PDecl]
473pUsing syn =
474 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
475 openBlock
476 let uvars = using syn
477 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
478 closeBlock
479 return (concat ds)
481pParams :: SyntaxInfo -> IParser [PDecl]
482pParams syn =
483 do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'
484 openBlock
485 let pvars = syn_params syn
486 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
487 closeBlock
488 fc <- pfc
489 return [PParams fc ns (concat ds)]
491pMutual :: SyntaxInfo -> IParser [PDecl]
492pMutual syn =
493 do reserved "mutual"
494 openBlock
495 let pvars = syn_params syn
496 ds <- many1 (pDecl syn)
497 closeBlock
498 fc <- pfc
499 return [PMutual fc (concat ds)]
501pNamespace :: SyntaxInfo -> IParser [PDecl]
502pNamespace syn =
503 do reserved "namespace"; n <- identifier;
504 openBlock
505 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
506 closeBlock
507 return [PNamespace n (concat ds)]
509--------- Fixity ---------
511pFixity :: IParser PDecl
512pFixity = do pushIndent
513 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
514 pTerminator
515 let prec = fromInteger i
516 istate <- getState
517 let infixes = idris_infixes istate
518 let fs = map (Fix (f prec)) ops
519 let redecls = map (alreadyDeclared infixes) fs
520 let ill = filter (not . checkValidity) redecls
521 if null ill
522 then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes)
523 , ibc_write = map IBCFix fs ++ ibc_write istate
524 })
525 fc <- pfc
526 return (PFix fc (f prec) ops)
527 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
528 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
529 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
530 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
532 checkValidity :: (FixDecl, [FixDecl]) -> Bool
533 checkValidity (f, fs) = all (== f) fs
535 extractName :: FixDecl -> String
536 extractName (Fix _ n) = n
538fixity :: IParser (Int -> Fixity)
539fixity = try (do reserved "infixl"; return Infixl)
540 <|> try (do reserved "infixr"; return Infixr)
541 <|> try (do reserved "infix"; return InfixN)
542 <|> try (do reserved "prefix"; return PrefixN)
544--------- Type classes ---------
546pClass :: SyntaxInfo -> IParser [PDecl]
547pClass syn = do doc <- option "" (pDocComment '|')
548 acc <- pAccessibility
549 reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName
550 let n = expandNS syn n_in
551 cs <- many carg
552 reserved "where"; openBlock
553 ds <- many $ pFunDecl syn
554 closeBlock
555 let allDs = concat ds
556 accData acc n (concatMap declared allDs)
557 return [PClass doc syn fc cons n cs allDs]
558 where
559 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
560 return (i, ty)
561 <|> do i <- pName;
562 return (i, PType)
564pInstance :: SyntaxInfo -> IParser [PDecl]
565pInstance syn = do reserved "instance"; fc <- pfc
566 en <- option Nothing
567 (do lchar '['; n_in <- pfName; lchar ']'
568 let n = expandNS syn n_in
569 return (Just n))
570 cs <- pConstList syn
571 cn <- pName
572 args <- many (pSimpleExpr syn)
573 let sc = PApp fc (PRef fc cn) (map pexp args)
574 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
575 reserved "where"; openBlock
576 ds <- many $ pFunDecl syn
577 closeBlock
578 return [PInstance syn fc cs cn args t en (concat ds)]
580--------- Expressions ---------
582pExpr syn = do i <- getState
583 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
585pExpr' :: SyntaxInfo -> IParser PTerm
586pExpr' syn
587 = try (pExtExpr syn)
588 <|> pNoExtExpr syn
590pExtExpr :: SyntaxInfo -> IParser PTerm
591pExtExpr syn = do i <- getState
592 pExtensions syn (syntax_rules i)
594pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
595pSimpleExtExpr syn = do i <- getState
596 pExtensions syn (filter simple (syntax_rules i))
597 where
598 simple (Rule (Expr x:xs) _ _) = False
599 simple (Rule (SimpleExpr x:xs) _ _) = False
600 simple (Rule [Keyword _] _ _) = True
601 simple (Rule [Symbol _] _ _) = True
602 simple (Rule (_:xs) _ _) = case last xs of
603 Keyword _ -> True
604 Symbol _ -> True
605 _ -> False
606 simple _ = False
608pNoExtExpr syn =
609 try (pApp syn)
610 <|> try (pMatchApp syn)
611 <|> try (pUnifyLog syn)
612 <|> pRecordType syn
613 <|> try (pSimpleExpr syn)
614 <|> pLambda syn
615 <|> pLet syn
616 <|> pRewriteTerm syn
617 <|> pPi syn
618 <|> pDoBlock syn
620pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
621pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))
622 where
623 valid (Rule _ _ AnySyntax) = True
624 valid (Rule _ _ PatternSyntax) = inPattern syn
625 valid (Rule _ _ TermSyntax) = not (inPattern syn)
628data SynMatch = SynTm PTerm | SynBind Name
630pExt :: SyntaxInfo -> Syntax -> IParser PTerm
631pExt syn (Rule ssym ptm _)
632 = do smap <- mapM pSymbol ssym
633 let ns = mapMaybe id smap
634 return (update ns ptm) -- updated with smap
635 where
636 pSymbol (Keyword n) = do reserved (show n); return Nothing
637 pSymbol (Expr n) = do tm <- pExpr syn
638 return $ Just (n, SynTm tm)
639 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
640 return $ Just (n, SynTm tm)
641 pSymbol (Binding n) = do b <- pName
642 return $ Just (n, SynBind b)
643 pSymbol (Symbol s) = do symbol s
644 return Nothing
645 dropn n [] = []
646 dropn n ((x,t) : xs) | n == x = xs
647 | otherwise = (x,t):dropn n xs
649 updateB ns n = case lookup n ns of
650 Just (SynBind t) -> t
651 _ -> n
653 update ns (PRef fc n) = case lookup n ns of
654 Just (SynTm t) -> t
655 _ -> PRef fc n
656 update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
657 update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
658 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
659 (update (dropn n ns) sc)
660 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
661 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
662 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
663 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
664 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
665 update ns (PHidden t) = PHidden (update ns t)
666 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
667 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
668 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
669 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
670 : upd (dropn n ns) ds
671 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
672 : upd ns ds
673 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
674 : upd ns ds
675 update ns t = t
677pName = do i <- getState
678 iName (syntax_keywords i)
679 <|> do reserved "instance"
680 i <- getState
681 UN n <- iName (syntax_keywords i)
682 return (UN ('@':n))
684-- | Parser for an operator in function position, i.e. enclosed by `()', with an
685-- optional namespace.
686pOpFront = maybeWithNS pOpFrontNoNS False []
687 where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o
689pfName = try pOpFront
690 <|> pName
692pTotality :: IParser Bool
693pTotality
694 = do reserved "total"; return True
695 <|> do reserved "partial"; return False
697pAccessibility' :: IParser Accessibility
698pAccessibility'
699 = do reserved "public"; return Public
700 <|> do reserved "abstract"; return Frozen
701 <|> do reserved "private"; return Hidden
703pAccessibility :: IParser (Maybe Accessibility)
704pAccessibility
705 = do acc <- pAccessibility'; return (Just acc)
706 <|> return Nothing
708pFnOpts :: [FnOpt] -> IParser [FnOpt]
709pFnOpts opts
710 = do reserved "total"; pFnOpts (TotalFn : opts)
711 <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))
712 <|> try (do lchar '%'; reserved "export"; c <- strlit;
713 pFnOpts (CExport c : opts))
714 <|> do lchar '%'; reserved "assert_total"; pFnOpts (AssertTotal : opts)
715 <|> do lchar '%'; reserved "specialise";
716 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'
717 pFnOpts (Specialise ns : opts)
718 <|> do reserved "implicit"; pFnOpts (Implicit : opts)
719 <|> return opts
721addAcc :: Name -> Maybe Accessibility -> IParser ()
722addAcc n a = do i <- getState
723 setState (i { hide_list = (n, a) : hide_list i })
725pCaseExpr syn = do
726 reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
727 openBlock
728 pushIndent
729 opts <- many1 (do notEndBlock
730 x <- pCaseOpt syn
731 pKeepTerminator
732 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
733 popIndent
734 closeBlock
735 return (PCase fc scr opts)
737pProofExpr syn = do
738 reserved "proof"; lchar '{'
739 ts <- endBy (pTactic syn) (lchar ';')
740 lchar '}'
741 return (PProof ts)
743pTacticsExpr syn = do
744 reserved "tactics"; lchar '{'
745 ts <- endBy (pTactic syn) (lchar ';')
746 lchar '}'
747 return (PTactics ts)
749pSimpleExpr syn =
750 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
751 <|> do lchar '?'; x <- pName; return (PMetavar x)
752 <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
753 <|> do reserved "refl"; fc <- pfc;
754 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
755 return t)
756 return (PRefl fc tm)
757-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
758 <|> pProofExpr syn
759 <|> pTacticsExpr syn
760 <|> pCaseExpr syn
761 <|> try (do x <- pfName
762 fc <- pfc
763 return (PRef fc x))
764 <|> try (do lchar '!'; x <- pfName
765 fc <- pfc
766 return (PInferRef fc x))
767 <|> try (pList syn)
768 <|> try (pComprehension syn)
769 <|> try (pAlt syn)
770 <|> try (pIdiom syn)
771 <|> try (do lchar '('
772 bracketed (noImp syn))
773 <|> try (do c <- pConstant
774 fc <- pfc
775 return (modifyConst syn fc (PConstant c)))
776 <|> do reserved "Type"; return PType
777 <|> try (do symbol "()"
778 fc <- pfc
779 return (PTrue fc))
780 <|> try (do symbol "_|_"
781 fc <- pfc
782 return (PFalse fc))
783 <|> do lchar '_'; return Placeholder
784 <|> pSimpleExtExpr syn
786bracketed syn =
787 try (pPair syn)
788 <|> try (do e <- pExpr syn; lchar ')'; return e)
789-- <|> try (do reserved "typed"
790-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
791-- return (PTyped e t))
792 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
793 return $ PLam (MN 1000 "ARG") Placeholder
794 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
795 pexp e]))
796 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
797 return $ PLam (MN 1000 "ARG") Placeholder
798 (PApp fc (PRef fc (UN o)) [pexp e,
799 pexp (PRef fc (MN 1000 "ARG"))]))
801pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
802pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })
803 symbol "=>"; rhs <- pExpr syn
804 return (lhs, rhs)
806-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
807-- big integer, otherwise try fromInteger and the constants as alternatives.
808-- a better solution would be to fix fromInteger to work with Integer, as the
809-- name suggests, rather than Int
811modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
812modifyConst syn fc (PConstant (BI x))
813 | not (inPattern syn)
814 = PAlternative False
815 (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
816 : consts)
817 | otherwise = PAlternative False consts
818 where
819 consts = [ PConstant (BI x)
820 , PConstant (I (fromInteger x))
821 , PConstant (B8 (fromInteger x))
822 , PConstant (B16 (fromInteger x))
823 , PConstant (B32 (fromInteger x))
824 , PConstant (B64 (fromInteger x))
825 ]
826modifyConst syn fc x = x
829pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
830 return (mkList fc xs)
831 where
832 mkList fc [] = PRef fc (UN "Nil")
833 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
835pPair syn = try (do l <- pExpr syn
836 fc <- pfc
837 rest <- restTuple
838 case rest of
839 [] -> return l
840 [Left r] -> return (PPair fc l r)
841 [Right r] -> return (PDPair fc l Placeholder r))
842 <|> try (do x <- ntuple
843 lchar ')'
844 return x)
845 <|> do ln <- pName; lchar ':'
846 lty <- pExpr syn
847 reservedOp "**"
848 fc <- pfc
849 r <- pExpr syn
850 lchar ')'
851 return (PDPair fc (PRef fc ln) lty r)
852 where
853 restTuple = do lchar ')'; return []
854 <|> do lchar ','
855 r <- pExpr syn
856 lchar ')'
857 return [Left r]
858 <|> do reservedOp "**"
859 r <- pExpr syn
860 lchar ')'
861 return [Right r]
862 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
863 rest <- ntuple
864 return (PPair fc l rest))
865 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
866 r <- pExpr syn
867 return (PPair fc l r))
869pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"
870 return (PAlternative False alts)
872pHSimpleExpr syn
873 = do lchar '.'
874 e <- pSimpleExpr syn
875 return $ PHidden e
876 <|> pSimpleExpr syn
878pMatchApp syn = do ty <- pSimpleExpr syn
879 symbol "<=="
880 fc <- pfc
881 f <- pfName
882 return (PLet (MN 0 "match")
883 ty
884 (PMatchApp fc f)
885 (PRef fc (MN 0 "match")))
887pUnifyLog syn = do lchar '%'; reserved "unifyLog";
888 tm <- pSimpleExpr syn
889 return (PUnifyLog tm)
891pApp syn = do f <- pSimpleExpr syn
892 fc <- pfc
893 args <- many1 (do notEndApp
894 pArg syn)
895 i <- getState
896 return (dslify i $ PApp fc f args)
897 where
898 dslify i (PApp fc (PRef _ f) [a])
899 | [d] <- lookupCtxt f (idris_dsls i)
900 = desugar (syn { dsl_info = d }) i (getTm a)
901 dslify i t = t
903pArg :: SyntaxInfo -> IParser PArg
904pArg syn = try (pImplicitArg syn)
905 <|> try (pConstraintArg syn)
906 <|> do e <- pSimpleExpr syn
907 return (pexp e)
909pImplicitArg syn = do lchar '{'
910 n <- pName
911 fc <- pfc
912 v <- option (PRef fc n) (do lchar '='
913 pExpr syn)
914 lchar '}'
915 return (pimp n v)
917pConstraintArg syn = do symbol "@{"
918 e <- pExpr syn
919 symbol "}"
920 return (pconst e)
922pRecordType syn
923 = do reserved "record"
924 lchar '{'
925 fields <- sepBy1 pFieldType (lchar ',')
926 lchar '}'
927 fc <- pfc
928 rec <- option Nothing (do e <- pSimpleExpr syn
929 return (Just e))
930 case rec of
931 Nothing ->
932 return (PLam (MN 0 "fldx") Placeholder
933 (applyAll fc fields (PRef fc (MN 0 "fldx"))))
934 Just v -> return (applyAll fc fields v)
935 where pFieldType = do n <- pfName
936 lchar '='
937 e <- pExpr syn
938 return (n, e)
939 applyAll fc [] x = x
940 applyAll fc ((n, e) : es) x
941 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
943mkType (UN n) = UN ("set_" ++ n)
944mkType (MN 0 n) = MN 0 ("set_" ++ n)
945mkType (NS n s) = NS (mkType n) s
947noImp syn = syn { implicitAllowed = False }
948impOK syn = syn { implicitAllowed = True }
950pTSig syn = do lchar ':'; pTExpr syn
952pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
953 sc <- pExpr syn
954 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
956pLambda syn = do lchar '\\'
957 try (do xt <- tyOptDeclList syn
958 symbol "=>"
959 sc <- pExpr syn
960 return (bindList PLam xt sc)
961 <|> (do ps <- sepBy (do fc <- pfc
962 e <- pSimpleExpr syn
963 return (fc, e)) (lchar ',')
964 symbol "=>"
965 sc <- pExpr syn
966 return (pmList (zip [0..] ps) sc)))
967 where pmList [] sc = sc
968 pmList ((i, (fc, x)) : xs) sc
969 = PLam (MN i "lamp") Placeholder
970 (PCase fc (PRef fc (MN i "lamp"))
971 [(x, pmList xs sc)])
973pRewriteTerm syn =
974 do reserved "rewrite"
975 fc <- pfc
976 prf <- pExpr syn
977 giving <- option Nothing
978 (do symbol "==>"; tm <- pExpr' syn
979 return (Just tm))
980 reserved "in"; sc <- pExpr syn
981 return (PRewrite fc
982 (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
983 giving)
985pLet syn = try (do reserved "let"; n <- pName;
986 ty <- option Placeholder (do lchar ':'; pExpr' syn)
987 lchar '='
988 v <- pExpr syn
989 reserved "in"; sc <- pExpr syn
990 return (PLet n ty v sc))
991 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )
992 symbol "="; v <- pExpr syn
993 reserved "in"; sc <- pExpr syn
994 return (PCase fc v [(pat, sc)]))
996pPi syn =
997 try (do lazy <- if implicitAllowed syn -- laziness is top level only
998 then option False (do lchar '|'; return True)
999 else return False
1000 st <- pStatic
1001 lchar '('; xt <- tyDeclList syn; lchar ')'
1002 doc <- option "" (pDocComment '^')
1003 symbol "->"
1004 sc <- pExpr syn
1005 return (bindList (PPi (Exp lazy st doc)) xt sc))
1006 <|> try (if implicitAllowed syn
1007 then do lazy <- option False (do lchar '|'
1008 return True)
1009 st <- pStatic
1010 lchar '{'
1011 xt <- tyDeclList syn
1012 lchar '}'
1013 symbol "->"
1014 sc <- pExpr syn
1015 return (bindList (PPi (Imp lazy st "")) xt sc)
1016 else fail "No implicit arguments allowed here")
1017 <|> try (do lchar '{'
1018 reserved "auto"
1019 xt <- tyDeclList syn
1020 lchar '}'
1021 symbol "->"
1022 sc <- pExpr syn
1023 return (bindList (PPi
1024 (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1025 <|> try (do lchar '{'
1026 reserved "default"
1027 script <- pSimpleExpr syn
1028 xt <- tyDeclList syn
1029 lchar '}'
1030 symbol "->"
1031 sc <- pExpr syn
1032 return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1033 <|> do --lazy <- option False (do lchar '|'; return True)
1034 lchar '{'
1035 reserved "static"
1036 lchar '}'
1037 t <- pExpr' syn
1038 symbol "->"
1039 sc <- pExpr syn
1040 return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1042pConstList :: SyntaxInfo -> IParser [PTerm]
1043pConstList syn = try (do lchar '('
1044 tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')
1045 lchar ')'
1046 reservedOp "=>"
1047 return tys)
1048 <|> try (do t <- pExpr (noImp syn)
1049 reservedOp "=>"
1050 return [t])
1051 <|> return []
1053usingDeclList syn
1054 = try (sepBy1 (usingDecl syn) (lchar ','))
1055 <|> do ns <- sepBy1 pName (lchar ',')
1056 t <- pTSig (noImp syn)
1057 return (map (\x -> UImplicit x t) ns)
1059usingDecl syn = try (do x <- pfName
1060 t <- pTSig (noImp syn)
1061 return (UImplicit x t))
1062 <|> do c <- pfName
1063 xs <- many1 pfName
1064 return (UConstraint c xs)
1066tyDeclList syn = try (sepBy1 (do x <- pfName
1067 t <- pTSig (noImp syn)
1068 return (x,t))
1069 (lchar ','))
1070 <|> do ns <- sepBy1 pName (lchar ',')
1071 t <- pTSig (noImp syn)
1072 return (map (\x -> (x, t)) ns)
1074tyOptDeclList syn = sepBy1 (do x <- pfName;
1075 t <- option Placeholder (do lchar ':'
1076 pExpr syn)
1077 return (x,t))
1078 (lchar ',')
1080bindList b [] sc = sc
1081bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
1083pComprehension syn
1084 = do lchar '['
1085 fc <- pfc
1086 pat <- pExpr syn
1087 lchar '|'
1088 qs <- sepBy1 (pDo syn) (lchar ',')
1089 lchar ']'
1090 return (PDoBlock (map addGuard qs ++
1091 [DoExp fc (PApp fc (PRef fc (UN "return"))
1092 [pexp pat])]))
1093 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1094 [pexp e])
1095 addGuard x = x
1097pDoBlock syn
1098 = do reserved "do"
1099 openBlock
1100 pushIndent
1101 ds <- many1 (do notEndBlock
1102 x <- pDo syn
1103 pKeepTerminator
1104 return x)
1105 popIndent
1106 closeBlock
1107 return (PDoBlock ds)
1109pDo syn
1110 = try (do reserved "let"
1111 i <- pName;
1112 ty <- option Placeholder (do lchar ':'
1113 pExpr' syn)
1114 reservedOp "="
1115 fc <- pfc
1116 e <- pExpr syn
1117 return (DoLet fc i ty e))
1118 <|> try (do reserved "let"
1119 i <- pExpr' syn
1120 reservedOp "="
1121 fc <- pfc
1122 sc <- pExpr syn
1123 return (DoLetP fc i sc))
1124 <|> try (do i <- pName
1125 symbol "<-"
1126 fc <- pfc
1127 e <- pExpr syn;
1128 return (DoBind fc i e))
1129 <|> try (do i <- pExpr' syn
1130 symbol "<-"
1131 fc <- pfc
1132 e <- pExpr syn;
1133 return (DoBindP fc i e))
1134 <|> try (do e <- pExpr syn
1135 fc <- pfc
1136 return (DoExp fc e))
1138pIdiom syn
1139 = do symbol "[|"
1140 fc <- pfc
1141 e <- pExpr syn
1142 symbol "|]"
1143 return (PIdiom fc e)
1145pConstant :: IParser Const
1146pConstant = do reserved "Integer";return (AType (ATInt ITBig))
1147 <|> do reserved "Int"; return (AType (ATInt ITNative))
1148 <|> do reserved "Char"; return (AType (ATInt ITChar))
1149 <|> do reserved "Float"; return (AType ATFloat)
1150 <|> do reserved "String"; return StrType
1151 <|> do reserved "Ptr"; return PtrType
1152 <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
1153 <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
1154 <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
1155 <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))
1156 <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))
1157 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
1158 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
1159 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1160 <|> try (do f <- float; return $ Fl f)
1161 <|> try (do i <- natural; return $ BI i)
1162 <|> try (do s <- strlit; return $ Str s)
1163 <|> try (do c <- chlit; return $ Ch c)
1165pStatic :: IParser Static
1166pStatic = do lchar '['
1167 reserved "static"
1168 lchar ']';
1169 return Static
1170 <|> return Dynamic
1172table fixes
1173 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
1174 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
1175 ++ toTable (reverse fixes) ++
1176 [[backtick],
1177 [binary "=" PEq AssocLeft],
1178 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
1180toTable fs = map (map toBin)
1181 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
1182 where toBin (Fix (PrefixN _) op) = prefix op
1183 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
1184 toBin (Fix f op)
1185 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
1186 assoc (Infixl _) = AssocLeft
1187 assoc (Infixr _) = AssocRight
1188 assoc (InfixN _) = AssocNone
1190binary name f = Infix (do fc <- pfc
1191 reservedOp name
1192 doc <- option "" (pDocComment '^')
1193 return (f fc))
1194prefix name f = Prefix (do reservedOp name
1195 fc <- pfc;
1196 return (f fc))
1197backtick = Infix (do lchar '`'; n <- pfName
1198 lchar '`'
1199 fc <- pfc
1200 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
1202--------- Data declarations ---------
1204-- (works for classes too - 'abstract' means the data/class is visible but members not)
1205accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
1206accData (Just Frozen) n ns = do addAcc n (Just Frozen)
1207 mapM_ (\n -> addAcc n (Just Hidden)) ns
1208accData a n ns = do addAcc n a
1209 mapM_ (`addAcc` a) ns
1211pRecord :: SyntaxInfo -> IParser PDecl
1212pRecord syn = do doc <- option "" (pDocComment '|')
1213 acc <- pAccessibility
1214 reserved "record"
1215 fc <- pfc
1216 tyn_in <- pfName
1217 ty <- pTSig (impOK syn)
1218 let tyn = expandNS syn tyn_in
1219 reserved "where"
1220 openBlock
1221 pushIndent
1222 (cdoc, cn, cty, _) <- pConstructor syn
1223 pKeepTerminator
1224 popIndent
1225 closeBlock
1226 accData acc tyn [cn]
1227 let rsyn = syn { syn_namespace = show (nsroot tyn) :
1228 syn_namespace syn }
1229 let fns = getRecNames rsyn cty
1230 mapM_ (\n -> addAcc n acc) fns
1231 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
1232 where
1233 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
1234 ++ getRecNames syn sc
1235 getRecNames _ _ = []
1237 toFreeze (Just Frozen) = Just Hidden
1238 toFreeze x = x
1240pDataI = do reserved "data"; return False
1241 <|> do reserved "codata"; return True
1243pData :: SyntaxInfo -> IParser PDecl
1244pData syn = try (do doc <- option "" (pDocComment '|')
1245 acc <- pAccessibility
1246 co <- pDataI
1247 fc <- pfc
1248 tyn_in <- pfName
1249 ty <- pTSig (impOK syn)
1250 let tyn = expandNS syn tyn_in
1251 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1252 reserved "where"
1253 openBlock
1254 pushIndent
1255 cons <- many (do notEndBlock
1256 c <- pConstructor syn
1257 pKeepTerminator
1258 return c) -- (lchar '|')
1259 popIndent
1260 closeBlock
1261 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1262 return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1263 <|> try (do doc <- option "" (pDocComment '|')
1264 pushIndent
1265 acc <- pAccessibility
1266 co <- pDataI
1267 fc <- pfc
1268 tyn_in <- pfName
1269 args <- many pName
1270 let ty = bindArgs (map (const PType) args) PType
1271 let tyn = expandNS syn tyn_in
1272 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1273 try (lchar '=') <|> do reserved "where"
1274 let kw = (if co then "co" else "") ++ "data "
1275 let n = show tyn_in ++ " "
1276 let s = kw ++ n
1277 let as = concat (intersperse " " $ map show args) ++ " "
1278 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
1279 let ss = concat (intersperse " -> " $ map (const "Type") args)
1280 let fix1 = s ++ as ++ " = ..."
1281 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
1282 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
1283 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
1285 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
1286 pTerminator
1287 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
1288 cons' <- mapM (\ (doc, x, cargs, cfc) ->
1289 do let cty = bindArgs cargs conty
1290 return (doc, x, cty, cfc)) cons
1291 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
1292 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
1293 where
1294 mkPApp fc t [] = t
1295 mkPApp fc t xs = PApp fc t (map pexp xs)
1297bindArgs :: [PTerm] -> PTerm -> PTerm
1298bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
1300pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)
1301pConstructor syn
1302 = do doc <- option "" (pDocComment '|')
1303 cn_in <- pfName; fc <- pfc
1304 let cn = expandNS syn cn_in
1305 ty <- pTSig (impOK syn)
1306-- ty' <- implicit syn cn ty
1307 return (doc, cn, ty, fc)
1310pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)
1311pSimpleCon syn
1312 = do cn_in <- pfName
1313 let cn = expandNS syn cn_in
1314 fc <- pfc
1315 args <- many (do notEndApp
1316 pSimpleExpr syn)
1317 doc <- option "" (pDocComment '^')
1318 return (doc, cn, args, fc)
1320--------- DSL syntax overloading ---------
1322pDSL :: SyntaxInfo -> IParser PDecl
1323pDSL syn = do reserved "dsl"
1324 n <- pfName
1325 openBlock
1326 pushIndent
1327 bs <- many1 (do notEndBlock
1328 b <- pOverload syn
1329 pKeepTerminator
1330 return b)
1331 popIndent; closeBlock
1332 let dsl = mkDSL bs (dsl_info syn)
1333 checkDSL dsl
1334 i <- getState
1335 setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1336 return (PDSL n dsl)
1337 where mkDSL bs dsl = let var = lookup "variable" bs
1338 first = lookup "index_first" bs
1339 next = lookup "index_next" bs
1340 leto = lookup "let" bs
1341 lambda = lookup "lambda" bs in
1342 initDSL { dsl_var = var,
1343 index_first = first,
1344 index_next = next,
1345 dsl_lambda = lambda,
1346 dsl_let = leto }
1348checkDSL :: DSL -> IParser ()
1349checkDSL dsl = return ()
1351pOverload :: SyntaxInfo -> IParser (String, PTerm)
1352pOverload syn = do o <- identifier <|> do reserved "let"
1353 return "let"
1354 if o `notElem` overloadable
1355 then fail $ show o ++ " is not an overloading"
1356 else do
1357 lchar '='
1358 t <- pExpr syn
1359 return (o, t)
1360 where overloadable = ["let","lambda","index_first","index_next","variable"]
1362--------- Pattern match clauses ---------
1364pPattern :: SyntaxInfo -> IParser PDecl
1365pPattern syn = do fc <- pfc
1366 clause <- pClause syn
1367 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
1369pCAF :: SyntaxInfo -> IParser PDecl
1370pCAF syn = do reserved "let"
1371 n_in <- pfName; let n = expandNS syn n_in
1372 lchar '='
1373 t <- pExpr syn
1374 pTerminator
1375 fc <- pfc
1376 return (PCAF fc n t)
1378pArgExpr syn = let syn' = syn { inPattern = True } in
1379 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
1381pRHS :: SyntaxInfo -> Name -> IParser PTerm
1382pRHS syn n = do lchar '='; pExpr syn
1383 <|> do symbol "?="; rhs <- pExpr syn;
1384 return (addLet rhs)
1385 <|> do reserved "impossible"; return PImpossible
1386 where mkN (UN x) = UN (x++"_lemma_1")
1387 mkN (NS x n) = NS (mkN x) n
1388 n' = mkN n
1390 addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)
1391 addLet (PCase fc t cs) = PCase fc t (map addLetC cs)
1392 where addLetC (l, r) = (l, addLet r)
1393 addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))
1395pClause :: SyntaxInfo -> IParser PClause
1396pClause syn
1397 = try (do pushIndent
1398 n_in <- pfName; let n = expandNS syn n_in
1399 cargs <- many (pConstraintArg syn)
1400 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1401 fc <- pfc
1402 args <- many (try (pImplicitArg (syn { inPattern = True } ))
1403 <|> (fmap pexp (pArgExpr syn)))
1404 wargs <- many (pWExpr syn)
1405 rhs <- pRHS syn n
1406 ist <- getState
1407 let ctxt = tt_ctxt ist
1408 let wsyn = syn { syn_namespace = [] }
1409 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1410 popIndent
1411 return x,
1412 do pTerminator
1413 return ([], [])]
1414 let capp = PApp fc (PRef fc n)
1415 (iargs ++ cargs ++ args)
1416 ist <- getState
1417 setState (ist { lastParse = Just n })
1418 return $ PClause fc n capp wargs rhs wheres)
1419 <|> try (do pushIndent
1420 ty <- pSimpleExpr syn
1421 symbol "<=="
1422 fc <- pfc
1423 n_in <- pfName; let n = expandNS syn n_in
1424 rhs <- pRHS syn n
1425 ist <- getState
1426 let ctxt = tt_ctxt ist
1427 let wsyn = syn { syn_namespace = [] }
1428 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1429 popIndent
1430 return x,
1431 do pTerminator
1432 return ([], [])]
1433 let capp = PLet (MN 0 "match")
1434 ty
1435 (PMatchApp fc n)
1436 (PRef fc (MN 0 "match"))
1437 ist <- getState
1438 setState (ist { lastParse = Just n })
1439 return $ PClause fc n capp [] rhs wheres)
1440 <|> try (do pushIndent
1441 wargs <- many1 (pWExpr syn)
1442 ist <- getState
1443 n <- case lastParse ist of
1444 Just t -> return t
1445 Nothing -> fail "Invalid clause"
1446 fc <- pfc
1447 rhs <- pRHS syn n
1448 let ctxt = tt_ctxt ist
1449 let wsyn = syn { syn_namespace = [] }
1450 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1451 popIndent
1452 return x,
1453 do pTerminator
1454 return ([], [])]
1455 return $ PClauseR fc wargs rhs wheres)
1457 <|> try (do pushIndent
1458 n_in <- pfName; let n = expandNS syn n_in
1459 cargs <- many (pConstraintArg syn)
1460 iargs <- many (pImplicitArg (syn { inPattern = True } ))
1461 fc <- pfc
1462 args <- many (try (pImplicitArg (syn { inPattern = True } ))
1463 <|> (fmap pexp (pArgExpr syn)))
1464 wargs <- many (pWExpr syn)
1465 let capp = PApp fc (PRef fc n)
1466 (iargs ++ cargs ++ args)
1467 ist <- getState
1468 setState (ist { lastParse = Just n })
1469 reserved "with"
1470 wval <- pSimpleExpr syn
1471 openBlock
1472 ds <- many1 $ pFunDecl syn
1473 let withs = map (fillLHSD n capp wargs) $ concat ds
1474 closeBlock
1475 popIndent
1476 return $ PWith fc n capp wargs wval withs)
1478 <|> try (do wargs <- many1 (pWExpr syn)
1479 fc <- pfc
1480 reserved "with"
1481 wval <- pSimpleExpr syn
1482 openBlock
1483 ds <- many1 $ pFunDecl syn
1484 let withs = concat ds
1485 closeBlock
1486 return $ PWithR fc wargs wval withs)
1488 <|> do pushIndent
1489 l <- pArgExpr syn
1490 op <- operator
1491 let n = expandNS syn (UN op)
1492 r <- pArgExpr syn
1493 fc <- pfc
1494 wargs <- many (pWExpr syn)
1495 rhs <- pRHS syn n
1496 let wsyn = syn { syn_namespace = [] }
1497 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1498 popIndent
1499 return x,
1500 do pTerminator
1501 return ([], [])]
1502 ist <- getState
1503 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1504 setState (ist { lastParse = Just n })
1505 return $ PClause fc n capp wargs rhs wheres
1507 <|> do l <- pArgExpr syn
1508 op <- operator
1509 let n = expandNS syn (UN op)
1510 r <- pArgExpr syn
1511 fc <- pfc
1512 wargs <- many (pWExpr syn)
1513 reserved "with"
1514 wval <- pSimpleExpr syn
1515 openBlock
1516 ds <- many1 $ pFunDecl syn
1517 closeBlock
1518 ist <- getState
1519 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1520 let withs = map (fillLHSD n capp wargs) $ concat ds
1521 setState (ist { lastParse = Just n })
1522 return $ PWith fc n capp wargs wval withs
1523 where
1524 fillLHS n capp owargs (PClauseR fc wargs v ws)
1525 = PClause fc n capp (owargs ++ wargs) v ws
1526 fillLHS n capp owargs (PWithR fc wargs v ws)
1527 = PWith fc n capp (owargs ++ wargs) v
1528 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1529 fillLHS _ _ _ c = c
1531 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1532 fillLHSD n c a x = x
1534pWExpr :: SyntaxInfo -> IParser PTerm
1535pWExpr syn = do lchar '|'
1536 pExpr' syn
1538pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1539pWhereblock n syn
1540 = do reserved "where"; openBlock
1541 ds <- many1 $ pDecl syn
1542 let dns = concatMap (concatMap declared) ds
1543 closeBlock
1544 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1546pCodegen :: IParser Codegen
1547pCodegen = try (do reserved "C"; return ViaC)
1548 <|> try (do reserved "Java"; return ViaJava)
1549 <|> try (do reserved "JavaScript"; return ViaJavaScript)
1550 <|> try (do reserved "Node"; return ViaNode)
1551 <|> try (do reserved "LLVM"; return ViaLLVM)
1552 <|> try (do reserved "Bytecode"; return Bytecode)
1554pDirective :: SyntaxInfo -> IParser [PDecl]
1555pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strlit;
1556 return [PDirective (do addLib cgn lib
1557 addIBC (IBCLib cgn lib))])
1558 <|> try (do lchar '%'; reserved "link"; cgn <- pCodegen; obj <- strlit;
1559 return [PDirective (do datadir <- liftIO getDataDir
1560 o <- liftIO $ findInPath [".", datadir] obj
1561 addIBC (IBCObj cgn o)
1562 addObjectFile cgn o)])
1563 <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit;
1564 return [PDirective (do addHdr cgn hdr
1565 addIBC (IBCHeader cgn hdr))])
1566 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1567 return [PDirective (do setAccessibility n Hidden
1568 addIBC (IBCAccess n Hidden))])
1569 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1570 return [PDirective (do setAccessibility n Frozen
1571 addIBC (IBCAccess n Frozen))])
1572 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1573 return [PDirective (do i <- getIState
1574 putIState (i { default_access = acc }))])
1575 <|> try (do lchar '%'; reserved "default"; tot <- pTotality
1576 i <- getState
1577 setState (i { default_total = tot } )
1578 return [PDirective (do i <- getIState
1579 putIState (i { default_total = tot }))])
1580 <|> try (do lchar '%'; reserved "logging"; i <- natural;
1581 return [PDirective (setLogLevel (fromInteger i))])
1582 <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 strlit (lchar ',');
1583 return [PDirective (do added <- addDyLib libs
1584 case added of
1585 Left lib -> addIBC (IBCDyLib (lib_name lib))
1586 Right msg ->
1587 fail $ msg)])
1588 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
1589 return [PDirective (addLangExt TypeProviders)])
1591pProvider :: SyntaxInfo -> IParser [PDecl]
1592pProvider syn = do lchar '%'; reserved "provide";
1593 lchar '('; n <- pfName; t <- pTSig syn; lchar ')'
1594 fc <- pfc
1595 reserved "with"
1596 e <- pExpr syn
1597 return [PProvider syn fc n t e]
1599pTactic :: SyntaxInfo -> IParser PTactic
1600pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1601 return $ Intro ns
1602 <|> do reserved "intros"; return Intros
1603 <|> try (do reserved "refine"; n <- pName
1604 imps <- many1 imp
1605 return $ Refine n imps)
1606 <|> do reserved "refine"; n <- pName
1607 i <- getState
1608 return $ Refine n []
1609 <|> do reserved "mrefine"; n <- pName
1610 i <- getState
1611 return $ MatchRefine n
1612 <|> do reserved "rewrite"; t <- pExpr syn;
1613 i <- getState
1614 return $ Rewrite (desugar syn i t)
1615 <|> do reserved "equiv"; t <- pExpr syn;
1616 i <- getState
1617 return $ Equiv (desugar syn i t)
1618 <|> try (do reserved "let"; n <- pName; lchar ':';
1619 ty <- pExpr' syn; lchar '='; t <- pExpr syn;
1620 i <- getState
1621 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1622 <|> try (do reserved "let"; n <- pName; lchar '=';
1623 t <- pExpr syn;
1624 i <- getState
1625 return $ LetTac n (desugar syn i t))
1626 <|> do reserved "focus"; n <- pName
1627 return $ Focus n
1628 <|> do reserved "exact"; t <- pExpr syn;
1629 i <- getState
1630 return $ Exact (desugar syn i t)
1631 <|> do reserved "applyTactic"; t <- pExpr syn;
1632 i <- getState
1633 return $ ApplyTactic (desugar syn i t)
1634 <|> do reserved "reflect"; t <- pExpr syn;
1635 i <- getState
1636 return $ Reflect (desugar syn i t)
1637 <|> do reserved "fill"; t <- pExpr syn;
1638 i <- getState
1639 return $ Fill (desugar syn i t)
1640 <|> do reserved "try"; t <- pTactic syn;
1641 lchar '|';
1642 t1 <- pTactic syn
1643 return $ Try t t1
1644 <|> do lchar '{'
1645 t <- pTactic syn;
1646 lchar ';';
1647 t1 <- pTactic syn;
1648 lchar '}'
1649 return $ TSeq t t1
1650 <|> do reserved "compute"; return Compute
1651 <|> do reserved "trivial"; return Trivial
1652 <|> do reserved "solve"; return Solve
1653 <|> do reserved "attack"; return Attack
1654 <|> do reserved "state"; return ProofState
1655 <|> do reserved "term"; return ProofTerm
1656 <|> do reserved "undo"; return Undo
1657 <|> do reserved "qed"; return Qed
1658 <|> do reserved "abandon"; return Abandon
1659 <|> do lchar ':'; reserved "q"; return Abandon
1660 where
1661 imp = do lchar '?'; return False
1662 <|> do lchar '_'; return True