git.iko.soy/Idris-dev
on b63e9bb help sign in
Idris-dev/src/Idris/Parser.hs
1247 lines 49 kB history raw
1module Idris.Parser where
3import Idris.AbsSyntax
4import Idris.Imports
5import Idris.Error
6import Idris.ElabDecls
7import Idris.ElabTerm
8import Idris.IBC
9import Idris.Unlit
10import Paths_idris
12import Core.CoreParser
13import Core.TT
14import Core.Evaluate
16import Text.ParserCombinators.Parsec
17import Text.ParserCombinators.Parsec.Error
18import Text.ParserCombinators.Parsec.Expr
19import Text.ParserCombinators.Parsec.Language
20import qualified Text.ParserCombinators.Parsec.Token as PTok
22import Data.List
23import Control.Monad.State
24import Debug.Trace
25import Data.Maybe
26import System.FilePath
28type TokenParser a = PTok.TokenParser a
30type IParser = GenParser Char IState
32lexer :: TokenParser IState
33lexer = PTok.makeTokenParser idrisDef
35whiteSpace= PTok.whiteSpace lexer
36lexeme = PTok.lexeme lexer
37symbol = PTok.symbol lexer
38natural = PTok.natural lexer
39parens = PTok.parens lexer
40semi = PTok.semi lexer
41comma = PTok.comma lexer
42identifier= PTok.identifier lexer
43reserved = PTok.reserved lexer
44operator = PTok.operator lexer
45reservedOp= PTok.reservedOp lexer
46integer = PTok.integer lexer
47float = PTok.float lexer
48strlit = PTok.stringLiteral lexer
49chlit = PTok.charLiteral lexer
50lchar = lexeme.char
52-- Loading modules
54loadModule :: FilePath -> Idris String
55loadModule f
56 = idrisCatch (do datadir <- liftIO $ getDataDir
57 fp <- liftIO $ findImport [".", datadir] f
58 i <- getIState
59 if (f `elem` imported i)
60 then iLOG $ "Already read " ++ f
61 else do putIState (i { imported = f : imported i })
62 case fp of
63 IDR fn -> loadSource False fn
64 LIDR fn -> loadSource True fn
65 IBC fn src ->
66 idrisCatch (loadIBC fn)
67 (\c -> do iLOG $ fn ++ " failed " ++ show c
68 case src of
69 IDR sfn -> loadSource False sfn
70 LIDR sfn -> loadSource True sfn)
71 let (dir, fh) = splitFileName f
72 return (dropExtension fh))
73 (\e -> do let msg = show e
74 setErrLine (getErrLine msg)
75 iputStrLn msg
76 return "")
78loadSource :: Bool -> FilePath -> Idris ()
79loadSource lidr f
80 = do iLOG ("Reading " ++ f)
81 file_in <- liftIO $ readFile f
82 file <- if lidr then tclift $ unlit f file_in else return file_in
83 (mname, modules, rest, pos) <- parseImports f file
84 i <- getIState
85 putIState (i { default_access = Hidden })
86 mapM_ loadModule modules
87 clearIBC -- start a new .ibc file
88 mapM_ (\m -> addIBC (IBCImport m)) modules
89 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
90 f rest pos
91 let ds = namespaces mname ds'
92 logLvl 3 (dumpDecls ds)
93 i <- getIState
94 logLvl 10 (show (toAlist (idris_implicits i)))
95 logLvl 3 (show (idris_infixes i))
96 -- Now add all the declarations to the context
97 v <- verbose
98 when v $ iputStrLn $ "Type checking " ++ f
99 mapM_ (elabDecl toplevel) ds
100 iLOG ("Finished " ++ f)
101 let ibc = dropExtension f ++ ".ibc"
102 iucheck
103 i <- getIState
104 addHides (hide_list i)
105 ok <- noErrors
106 when ok $
107 idrisCatch (do writeIBC f ibc; clearIBC)
108 (\c -> return ()) -- failure is harmless
109 putIState (i { hide_list = [] })
110 return ()
111 where
112 namespaces [] ds = ds
113 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
115addHides :: [(Name, Maybe Accessibility)] -> Idris ()
116addHides xs = do i <- getIState
117 let defh = default_access i
118 let (hs, as) = partition isNothing xs
119 if null as then return ()
120 else mapM_ doHide
121 (map (\ (n, _) -> (n, defh)) hs ++
122 map (\ (n, Just a) -> (n, a)) as)
123 where isNothing (_, Nothing) = True
124 isNothing _ = False
126 doHide (n, a) = do setAccessibility n a
127 addIBC (IBCAccess n a)
129parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
130parseTac i = runParser (do t <- pTactic defaultSyntax
131 eof
132 return t) i "(proof)"
134parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
135parseImports fname input
136 = do i <- get
137 case (runParser (do mname <- pHeader
138 ps <- many pImport
139 rest <- getInput
140 pos <- getPosition
141 return ((mname, ps, rest, pos), i)) i fname input) of
142 Left err -> fail (ishow err)
143 Right (x, i) -> do put i
144 return x
145 where ishow err = let ln = sourceLine (errorPos err) in
146 fname ++ ":" ++ show ln ++ ":parse error"
147-- show (map messageString (errorMessages err))
149pHeader :: IParser [String]
150pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
151 return (parseName i))
152 <|> return []
153 where parseName x = case span (/='.') x of
154 (x, "") -> [x]
155 (x, '.':y) -> x : parseName y
157push_indent :: IParser ()
158push_indent = do pos <- getPosition
159 ist <- getState
160 setState (ist { indent_stack = sourceColumn pos :
161 indent_stack ist })
163last_indent :: IParser Int
164last_indent = do ist <- getState
165 case indent_stack ist of
166 (x : xs) -> return x
167 _ -> return 1
169indent :: IParser Int
170indent = do pos <- getPosition
171 return (sourceColumn pos)
173pop_indent :: IParser ()
174pop_indent = do ist <- getState
175 let (x : xs) = indent_stack ist
176 setState (ist { indent_stack = xs })
178open_block :: IParser ()
179open_block = do lchar '{'
180 ist <- getState
181 setState (ist { brace_stack = Nothing : brace_stack ist })
182 <|> do ist <- getState
183 lvl <- indent
184 setState (ist { brace_stack = Just lvl : brace_stack ist })
186close_block :: IParser ()
187close_block = do ist <- getState
188 bs <- case brace_stack ist of
189 Nothing : xs -> do lchar '}'
190 return xs
191 Just lvl : xs -> do i <- indent
192 inp <- getInput
193-- trace (show (take 10 inp, i, lvl)) $
194 if (i >= lvl && take 1 inp /= ")")
195 then fail "Not end of block"
196 else return xs
197 setState (ist { brace_stack = bs })
199pTerminator = do lchar ';'; pop_indent
200 <|> do c <- indent; l <- last_indent
201 if (c <= l) then pop_indent
202 else fail "Not a terminator"
203 <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent
204 else fail "Not a terminator"
205 <|> lookAhead eof
207pBarTerminator
208 = do lchar '|'; return ()
209 <|> do c <- indent; l <- last_indent
210 if (c <= l) then return ()
211 else fail "Not a terminator"
212 <|> lookAhead eof
214pKeepTerminator
215 = do lchar ';'; return ()
216 <|> do c <- indent; l <- last_indent
217 if (c <= l) then return ()
218 else fail "Not a terminator"
219 <|> do i <- getInput; let h = take 1 i
220 if (h == "}" || h == ")" || h == "|") then return ()
221 else fail "Not a terminator"
222 <|> lookAhead eof
224notEndApp = do c <- indent; l <- last_indent
225 i <- getInput
226 if (c <= l) then fail "Terminator"
227 else return ()
229notEndBlock = do ist <- getState
230 case brace_stack ist of
231 Just lvl : xs -> do i <- indent
232 inp <- getInput
233 if (i < lvl || take 1 inp == ")")
234 then fail "End of block"
235 else return ()
236 _ -> return ()
238pfc :: IParser FC
239pfc = do s <- getPosition
240 let (dir, file) = splitFileName (sourceName s)
241 let f = case dir of
242 "./" -> file
243 _ -> sourceName s
244 return $ FC f (sourceLine s)
246pImport :: IParser String
247pImport = do reserved "import"
248 f <- identifier
249 option ';' (lchar ';')
250 return (map dot f)
251 where dot '.' = '/'
252 dot c = c
254parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
255parseProg syn fname input pos
256 = do i <- get
257 case (runParser (do setPosition pos
258 whiteSpace
259 ps <- many (pDecl syn)
260 eof
261 i' <- getState
262 return (concat ps, i')) i fname input) of
263 Left err -> fail (ishow err)
264 Right (x, i) -> do put i
265 return (collect x)
266 where ishow err = let ln = sourceLine (errorPos err) in
267 fname ++ ":" ++ show ln ++ ":parse error"
268 ++ " at column " ++ show (sourceColumn (errorPos err))
269-- show (map messageString (errorMessages err))
271-- Collect PClauses with the same function name
273collect :: [PDecl] -> [PDecl]
274collect (c@(PClauses _ o _ _) : ds)
275 = clauses (cname c) [] (c : ds)
276 where clauses n acc (PClauses fc _ _ [PClause n' l ws r w] : ds)
277 | n == n' = clauses n (PClause n' l ws r (collect w) : acc) ds
278 clauses n acc (PClauses fc _ _ [PWith n' l ws r w] : ds)
279 | n == n' = clauses n (PWith n' l ws r (collect w) : acc) ds
280 clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
282 cname (PClauses fc _ _ [PClause n _ _ _ _]) = n
283 cname (PClauses fc _ _ [PWith n _ _ _ _]) = n
284 getfc (PClauses fc _ _ _) = fc
286collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
287collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
288collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'
289collect (PInstance f s cs n ps t ds : ds')
290 = PInstance f s cs n ps t (collect ds) : collect ds'
291collect (d : ds) = d : collect ds
292collect [] = []
294pFullExpr :: SyntaxInfo -> IParser PTerm
295pFullExpr syn
296 = do x <- pExpr syn; eof;
297 i <- getState
298 return $ desugar syn i x
300pDecl :: SyntaxInfo -> IParser [PDecl]
301pDecl syn = do notEndBlock
302 pDeclBody where
303 pDeclBody
304 = do d <- pDecl' syn
305 i <- getState
306 let d' = fmap (desugar syn i) d
307 return [d']
308 <|> pUsing syn
309 <|> pParams syn
310 <|> pNamespace syn
311 <|> pClass syn
312 <|> pInstance syn
313 <|> pDirective
314 <|> try (do reserved "import"
315 fp <- identifier
316 fail "imports must be at the top of file")
318pFunDecl :: SyntaxInfo -> IParser [PDecl]
319pFunDecl syn
320 = try (do notEndBlock
321 d <- pFunDecl' syn
322 i <- getState
323 let d' = fmap (desugar syn i) d
324 return [d'])
326--------- Top Level Declarations ---------
328pDecl' :: SyntaxInfo -> IParser PDecl
329pDecl' syn
330 = try pFixity
331 <|> pFunDecl' syn
332 <|> try (pData syn)
333 <|> try (pRecord syn)
334 <|> pSyntaxDecl syn
336pSyntaxDecl :: SyntaxInfo -> IParser PDecl
337pSyntaxDecl syn
338 = do s <- pSyntaxRule syn
339 i <- getState
340 let rs = syntax_rules i
341 let ns = syntax_keywords i
342 let ibc = ibc_write i
343 let ks = map show (names s)
344 setState (i { syntax_rules = s : rs,
345 syntax_keywords = ks ++ ns,
346 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
347 })
348 fc <- pfc
349 return (PSyntax fc s)
350 where
351 names (Rule syms _ _) = mapMaybe ename syms
352 ename (Keyword n) = Just n
353 ename _ = Nothing
355pSyntaxRule :: SyntaxInfo -> IParser Syntax
356pSyntaxRule syn
357 = do push_indent
358 sty <- option AnySyntax (do reserved "term"; return TermSyntax
359 <|> do reserved "pattern"; return PatternSyntax)
360 reserved "syntax"
361 syms <- many1 pSynSym
362 when (all expr syms) $ fail "No keywords in syntax rule"
363 let ns = mapMaybe name syms
364 when (length ns /= length (nub ns))
365 $ fail "Repeated variable in syntax rule"
366 lchar '='
367 tm <- pExpr syn
368 pTerminator
369 return (Rule (mkSimple syms) tm sty)
370 where
371 expr (Expr _) = True
372 expr _ = False
373 name (Expr n) = Just n
374 name _ = Nothing
376 -- Can't parse two full expressions (i.e. expressions with application) in a row
377 -- so change the first to a simple expression
379 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
380 mkSimple xs = mkSimple' xs
382 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : mkSimple' (Expr e1 : es)
383 mkSimple' (e : es) = e : mkSimple' es
384 mkSimple' [] = []
386pSynSym :: IParser SSymbol
387pSynSym = try (do lchar '['; n <- pName; lchar ']'
388 return (Expr n))
389 <|> do n <- iName []
390 return (Keyword n)
391 <|> do sym <- strlit
392 return (Symbol sym)
394pFunDecl' :: SyntaxInfo -> IParser PDecl
395pFunDecl' syn = try (do push_indent
396 acc <- pAccessibility
397 n_in <- pfName
398 let n = expandNS syn n_in
399 ty <- pTSig syn
400 fc <- pfc
401 pTerminator
402-- ty' <- implicit syn n ty
403 addAcc n acc
404 return (PTy syn fc n ty))
405 <|> try (pPattern syn)
407pUsing :: SyntaxInfo -> IParser [PDecl]
408pUsing syn =
409 do reserved "using";
410 lchar '('
411 ns <- tyDeclList syn
412 lchar ')'
413 open_block
414 let uvars = using syn
415 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
416 close_block
417 return (concat ds)
419pParams :: SyntaxInfo -> IParser [PDecl]
420pParams syn =
421 do reserved "params";
422 lchar '('
423 ns <- tyDeclList syn
424 lchar ')'
425 lchar '{'
426 let pvars = syn_params syn
427 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
428 lchar '}'
429 fc <- pfc
430 return [PParams fc ns (concat ds)]
432pNamespace :: SyntaxInfo -> IParser [PDecl]
433pNamespace syn =
434 do reserved "namespace";
435 n <- identifier
436 open_block
437 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
438 close_block
439 return [PNamespace n (concat ds)]
441expandNS :: SyntaxInfo -> Name -> Name
442expandNS syn n@(NS _ _) = n
443expandNS syn n = case syn_namespace syn of
444 [] -> n
445 xs -> NS n xs
447--------- Fixity ---------
449pFixity :: IParser PDecl
450pFixity = do push_indent
451 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
452 pTerminator
453 let prec = fromInteger i
454 istate <- getState
455 let fs = map (Fix (f prec)) ops
456 setState (istate {
457 idris_infixes = sort (fs ++ idris_infixes istate),
458 ibc_write = map IBCFix fs ++ ibc_write istate })
459 fc <- pfc
460 return (PFix fc (f prec) ops)
462fixity :: IParser (Int -> Fixity)
463fixity = try (do reserved "infixl"; return Infixl)
464 <|> try (do reserved "infixr"; return Infixr)
465 <|> try (do reserved "infix"; return InfixN)
466 <|> try (do reserved "prefix"; return PrefixN)
468--------- Tyoe classes ---------
470pClass :: SyntaxInfo -> IParser [PDecl]
471pClass syn = do acc <- pAccessibility
472 reserved "class"
473 fc <- pfc
474 cons <- pConstList syn
475 n_in <- pName; let n = expandNS syn n_in
476 cs <- many1 carg
477 reserved "where"; open_block
478 ds <- many1 $ pFunDecl syn
479 close_block
480 let allDs = concat ds
481 accData acc n (concatMap declared allDs)
482 return [PClass syn fc cons n cs allDs]
483 where
484 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
485 return (i, ty)
486 <|> do i <- pName;
487 return (i, PSet)
489pInstance :: SyntaxInfo -> IParser [PDecl]
490pInstance syn = do reserved "instance"
491 fc <- pfc
492 cs <- pConstList syn
493 cn <- pName
494 args <- many1 (pSimpleExpr syn)
495 let sc = PApp fc (PRef fc cn) (map pexp args)
496 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
497 reserved "where"; open_block
498 ds <- many1 $ pFunDecl syn
499 close_block
500 return [PInstance syn fc cs cn args t (concat ds)]
502--------- Expressions ---------
504pExpr syn = do i <- getState
505 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
507pExpr' :: SyntaxInfo -> IParser PTerm
508pExpr' syn
509 = try (pExtExpr syn)
510 <|> pNoExtExpr syn
512pExtExpr :: SyntaxInfo -> IParser PTerm
513pExtExpr syn = do i <- getState
514 pExtensions syn (syntax_rules i)
516pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
517pSimpleExtExpr syn = do i <- getState
518 pExtensions syn (filter simple (syntax_rules i))
519 where
520 simple (Rule (Expr x:xs) _ _) = False
521 simple (Rule (SimpleExpr x:xs) _ _) = False
522 simple (Rule [Keyword _] _ _) = True
523 simple (Rule [Symbol _] _ _) = True
524 simple (Rule (_:xs) _ _) = case (last xs) of
525 Keyword _ -> True
526 Symbol _ -> True
527 _ -> False
528 simple _ = False
530pNoExtExpr syn =
531 try (pApp syn)
532 <|> try (pSimpleExpr syn)
533 <|> pLambda syn
534 <|> pLet syn
535 <|> pPi syn
536 <|> pDoBlock syn
537 <|> pComprehension syn
539pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
540pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))
541 where
542 valid (Rule _ _ AnySyntax) = True
543 valid (Rule _ _ PatternSyntax) = inPattern syn
544 valid (Rule _ _ TermSyntax) = not (inPattern syn)
547pExt :: SyntaxInfo -> Syntax -> IParser PTerm
548pExt syn (Rule ssym ptm _)
549 = do smap <- mapM pSymbol ssym
550 let ns = mapMaybe id smap
551 return (update ns ptm) -- updated with smap
552 where
553 pSymbol (Keyword n) = do reserved (show n); return Nothing
554 pSymbol (Expr n) = do tm <- pExpr syn
555 return $ Just (n, tm)
556 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn
557 return $ Just (n, tm)
558 pSymbol (Symbol s) = do symbol s
559 return Nothing
560 dropn n [] = []
561 dropn n ((x,t) : xs) | n == x = xs
562 | otherwise = (x,t):dropn n xs
564 update ns (PRef fc n) = case lookup n ns of
565 Just t -> t
566 _ -> PRef fc n
567 update ns (PLam n ty sc) = PLam n (update ns ty) (update (dropn n ns) sc)
568 update ns (PPi p n ty sc) = PPi p n (update ns ty) (update (dropn n ns) sc)
569 update ns (PLet n ty val sc) = PLet n (update ns ty) (update ns val)
570 (update (dropn n ns) sc)
571 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
572 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
573 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
574 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
575 update ns (PAlternative as) = PAlternative (map (update ns) as)
576 update ns (PHidden t) = PHidden (update ns t)
577 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
578 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
579 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
580 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
581 : upd (dropn n ns) ds
582 upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
583 : upd ns ds
584 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
585 : upd ns ds
586 update ns t = t
588pName = do i <- getState
589 iName (syntax_keywords i)
590 <|> do reserved "instance"
591 i <- getState
592 UN n <- iName (syntax_keywords i)
593 return (UN ('@':n))
596pfName = try pName
597 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)
599pAccessibility' :: IParser Accessibility
600pAccessibility'
601 = do reserved "public"; return Public
602 <|> do reserved "abstract"; return Frozen
603 <|> do reserved "private"; return Hidden
605pAccessibility :: IParser (Maybe Accessibility)
606pAccessibility
607 = do acc <- pAccessibility'; return (Just acc)
608 <|> return Nothing
610addAcc :: Name -> Maybe Accessibility -> IParser ()
611addAcc n a = do i <- getState
612 setState (i { hide_list = (n, a) : hide_list i })
614pSimpleExpr syn =
615 try (do symbol "!["; t <- pTerm; lchar ']'
616 return $ PQuote t)
617 <|> do lchar '?'; x <- pName; return (PMetavar x)
618 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
619-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
620 <|> do reserved "proof"; lchar '{';
621 ts <- endBy (pTactic syn) (lchar ';')
622 lchar '}'
623 return (PProof ts)
624 <|> do reserved "tactics"; lchar '{';
625 ts <- endBy (pTactic syn) (lchar ';')
626 lchar '}'
627 return (PTactics ts)
628 <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";
629 open_block
630 push_indent
631 opts <- many1 (do notEndBlock
632 x <- pCaseOpt syn
633 pKeepTerminator
634 return x) -- sepBy1 (pCaseOpt syn) (lchar '|')
635 pop_indent
636 close_block
637 return (PCase fc scr opts)
638 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
639 <|> try (pList syn)
640 <|> try (pAlt syn)
641 <|> try (pIdiom syn)
642 <|> try (do lchar '('; bracketed syn)
643 <|> try (do c <- pConstant; fc <- pfc
644 return (modifyConst syn fc (PConstant c)))
645 <|> do reserved "Set"; return PSet
646 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
647 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
648 <|> do lchar '_'; return Placeholder
649 <|> pSimpleExtExpr syn
651bracketed syn =
652 try (pPair syn)
653 <|> try (do e <- pExpr syn; lchar ')'; return e)
654-- <|> try (do reserved "typed"
655-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'
656-- return (PTyped e t))
657 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'
658 return $ PLam (MN 0 "x") Placeholder
659 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")),
660 pexp e]))
661 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'
662 return $ PLam (MN 0 "x") Placeholder
663 (PApp fc (PRef fc (UN o)) [pexp e,
664 pexp (PRef fc (MN 0 "x"))]))
666pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)
667pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";
668 rhs <- pExpr syn
669 return (lhs, rhs)
671modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
672modifyConst syn fc (PConstant (I x))
673 | not (inPattern syn)
674 = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]
675modifyConst syn fc x = x
677pList syn = do lchar '['; fc <- pfc
678 xs <- sepBy (pExpr syn) (lchar ','); lchar ']'
679 return (mkList fc xs)
680 where
681 mkList fc [] = PRef fc (UN "Nil")
682 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
684pPair syn = try (do l <- pExpr syn
685 fc <- pfc
686 rest <- restTuple
687 case rest of
688 [] -> return l
689 [Left r] -> return (PPair fc l r)
690 [Right r] -> return (PDPair fc l Placeholder r))
691 <|> try (do x <- ntuple
692 lchar ')'
693 return x)
694 <|> do ln <- pName; lchar ':'; lty <- pExpr syn;
695 reservedOp "**";
696 fc <- pfc
697 r <- pExpr syn; lchar ')';
698 return (PDPair fc (PRef fc ln) lty r)
699 where
700 restTuple = do lchar ')'; return []
701 <|> do lchar ','
702 r <- pExpr syn
703 lchar ')'
704 return [Left r]
705 <|> do reservedOp "**"
706 r <- pExpr syn
707 lchar ')'
708 return [Right r]
709 ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','
710 rest <- ntuple
711 return (PPair fc l rest))
712 <|> (do l <- pExpr syn; fc <- pfc; lchar ','
713 r <- pExpr syn
714 return (PPair fc l r))
716pAlt syn = do symbol "(|";
717 alts <- sepBy1 (pExpr' syn) (lchar ',')
718 symbol "|)"
719 return (PAlternative alts)
721pHSimpleExpr syn
722 = do lchar '.'
723 e <- pSimpleExpr syn
724 return $ PHidden e
725 <|> pSimpleExpr syn
727pApp syn = do f <- pSimpleExpr syn
728 fc <- pfc
729 args <- many1 (do notEndApp
730 pArg syn)
731 return (PApp fc f args)
733pArg :: SyntaxInfo -> IParser PArg
734pArg syn = try (pImplicitArg syn)
735 <|> try (pConstraintArg syn)
736 <|> do e <- pSimpleExpr syn
737 return (pexp e)
739pImplicitArg syn = do lchar '{'; n <- pName
740 fc <- pfc
741 v <- option (PRef fc n) (do lchar '='; pExpr syn)
742 lchar '}'
743 return (pimp n v)
745pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"
746 return (pconst e)
748pTSig syn = do lchar ':'
749 cs <- pConstList syn
750 sc <- pExpr syn
751 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
753pLambda syn = do lchar '\\'
754 (try (do xt <- tyOptDeclList syn
755 symbol "=>"
756 sc <- pExpr syn
757 return (bindList PLam xt sc))
758 <|> (do ps <- sepBy (do fc <- pfc
759 e <- pSimpleExpr syn
760 return (fc, e)) (lchar ',')
761 symbol "=>"
762 sc <- pExpr syn
763 return (pmList (zip [0..] ps) sc)))
764 where pmList [] sc = sc
765 pmList ((i, (fc, x)) : xs) sc
766 = PLam (MN i "lamp") Placeholder
767 (PCase fc (PRef fc (MN i "lamp"))
768 [(x, (pmList xs sc))])
770pLet syn = try (do reserved "let"; n <- pName;
771 ty <- option Placeholder (do lchar ':'; pExpr' syn)
772 lchar '='; v <- pExpr syn
773 reserved "in"; sc <- pExpr syn
774 return (PLet n ty v sc))
775 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn
776 symbol "="; v <- pExpr syn
777 reserved "in"; sc <- pExpr syn
778 return (PCase fc v [(pat, sc)]))
780pPi syn =
781 try (do lazy <- option False (do lchar '|'; return True)
782 st <- pStatic
783 lchar '('; xt <- tyDeclList syn; lchar ')'
784 symbol "->"
785 sc <- pExpr syn
786 return (bindList (PPi (Exp lazy st)) xt sc))
787 <|> try (do lazy <- option False (do lchar '|'; return True)
788 st <- pStatic
789 lchar '{'; xt <- tyDeclList syn; lchar '}'
790 symbol "->"
791 sc <- pExpr syn
792 return (bindList (PPi (Imp lazy st)) xt sc))
793 <|> do --lazy <- option False (do lchar '|'; return True)
794 lchar '{'; reserved "static"; lchar '}'
795 t <- pExpr' syn
796 symbol "->"
797 sc <- pExpr syn
798 return (PPi (Exp False Static) (MN 42 "__pi_arg") t sc)
800pConstList :: SyntaxInfo -> IParser [PTerm]
801pConstList syn = try (do lchar '('
802 tys <- sepBy1 (pExpr' syn) (lchar ',')
803 lchar ')'
804 reservedOp "=>"
805 return tys)
806 <|> try (do t <- pExpr syn
807 reservedOp "=>"
808 return [t])
809 <|> return []
811tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
812 (lchar ','))
813 <|> do ns <- sepBy1 pName (lchar ',')
814 t <- pTSig syn
815 return (map (\x -> (x, t)) ns)
817tyOptDeclList syn = sepBy1 (do x <- pfName;
818 t <- option Placeholder (do lchar ':'
819 pExpr syn)
820 return (x,t))
821 (lchar ',')
823bindList b [] sc = sc
824bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
826pComprehension syn
827 = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|';
828 qs <- sepBy1 (pDo syn) (lchar ','); lchar ']';
829 return (PDoBlock (map addGuard qs ++
830 [DoExp fc (PApp fc (PRef fc (UN "return"))
831 [pexp pat])]))
832 where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
833 [pexp e])
834 addGuard x = x
836pDoBlock syn
837 = do reserved "do"; open_block
838 push_indent
839 ds <- many1 (do notEndBlock
840 x <- pDo syn; pKeepTerminator; return x)
841 pop_indent
842 close_block
843 return (PDoBlock ds)
845pDo syn
846 = try (do reserved "let"; i <- pName;
847 ty <- option Placeholder (do lchar ':'; pExpr' syn)
848 reservedOp "="; fc <- pfc
849 e <- pExpr syn
850 return (DoLet fc i ty e))
851 <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc
852 sc <- pExpr syn
853 return (DoLetP fc i sc))
854 <|> try (do i <- pName; symbol "<-"; fc <- pfc
855 e <- pExpr syn;
856 return (DoBind fc i e))
857 <|> try (do i <- pExpr' syn; symbol "<-"; fc <- pfc
858 e <- pExpr syn;
859 return (DoBindP fc i e))
860 <|> try (do e <- pExpr syn; fc <- pfc
861 return (DoExp fc e))
863pIdiom syn
864 = do symbol "[|"; fc <- pfc; e <- pExpr syn; symbol "|]"
865 return (PIdiom fc e)
867pConstant :: IParser Const
868pConstant = do reserved "Integer";return BIType
869 <|> do reserved "Int"; return IType
870 <|> do reserved "Char"; return ChType
871 <|> do reserved "Float"; return FlType
872 <|> do reserved "String"; return StrType
873 <|> do reserved "Ptr"; return PtrType
874 <|> try (do f <- float; return $ Fl f)
875 <|> try (do i <- natural; lchar 'L'; return $ BI i)
876 <|> try (do i <- natural; return $ I (fromInteger i))
877 <|> try (do s <- strlit; return $ Str s)
878 <|> try (do c <- chlit; return $ Ch c)
880pStatic :: IParser Static
881pStatic = do lchar '['; reserved "static"; lchar ']';
882 return Static
883 <|> return Dynamic
885table fixes
886 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
887 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
888 ++ toTable (reverse fixes) ++
889 [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],
890 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
892toTable fs = map (map toBin)
893 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
894 where toBin (Fix (PrefixN _) op) = prefix op
895 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
896 toBin (Fix f op)
897 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
898 assoc (Infixl _) = AssocLeft
899 assoc (Infixr _) = AssocRight
900 assoc (InfixN _) = AssocNone
902binary name f assoc = Infix (do { reservedOp name; fc <- pfc;
903 return (f fc) }) assoc
904prefix name f = Prefix (do { reservedOp name; fc <- pfc;
905 return (f fc) })
907--------- Data declarations ---------
909-- (works for classes too - 'abstract' means the data/class is visible but members not)
910accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()
911accData (Just Frozen) n ns = do addAcc n (Just Frozen)
912 mapM_ (\n -> addAcc n (Just Hidden)) ns
913accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
915pRecord :: SyntaxInfo -> IParser PDecl
916pRecord syn = try (do acc <- pAccessibility
917 reserved "record"; fc <- pfc
918 tyn_in <- pfName; ty <- pTSig syn
919 let tyn = expandNS syn tyn_in
920 reserved "where"
921 (cn, cty, _) <- pConstructor syn
922 pTerminator
923 accData acc tyn [cn]
924 return $ PRecord syn fc tyn ty cn cty)
926pData :: SyntaxInfo -> IParser PDecl
927pData syn = try (do acc <- pAccessibility
928 reserved "data"; fc <- pfc
929 tyn_in <- pfName; ty <- pTSig syn
930 let tyn = expandNS syn tyn_in
931 reserved "where"
932 open_block
933 push_indent
934 cons <- many (do notEndBlock
935 c <- pConstructor syn
936 pKeepTerminator
937 return c) -- (lchar '|')
938 pop_indent
939 close_block
940 accData acc tyn (map (\ (n, _, _) -> n) cons)
941 return $ PData syn fc (PDatadecl tyn ty cons))
942 <|> try (do push_indent
943 acc <- pAccessibility
944 reserved "data"; fc <- pfc
945 tyn_in <- pfName; args <- many pName
946 let tyn = expandNS syn tyn_in
947 lchar '='
948 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
949 pTerminator
950 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
951 let ty = bindArgs (map (\a -> PSet) args) PSet
952 cons' <- mapM (\ (x, cargs, cfc) ->
953 do let cty = bindArgs cargs conty
954 return (x, cty, cfc)) cons
955 accData acc tyn (map (\ (n, _, _) -> n) cons')
956 return $ PData syn fc (PDatadecl tyn ty cons'))
957 where
958 mkPApp fc t [] = t
959 mkPApp fc t xs = PApp fc t (map pexp xs)
961bindArgs :: [PTerm] -> PTerm -> PTerm
962bindArgs [] t = t
963bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)
965pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
966pConstructor syn
967 = do cn_in <- pfName; fc <- pfc
968 let cn = expandNS syn cn_in
969 ty <- pTSig syn
970-- ty' <- implicit syn cn ty
971 return (cn, ty, fc)
973pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)
974pSimpleCon syn
975 = do cn_in <- pfName
976 let cn = expandNS syn cn_in
977 fc <- pfc
978 args <- many (do notEndApp
979 pSimpleExpr syn)
980 return (cn, args, fc)
982--------- Pattern match clauses ---------
984pPattern :: SyntaxInfo -> IParser PDecl
985pPattern syn = do clause <- pClause syn
986 fc <- pfc
987 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
989pArgExpr syn = let syn' = syn { inPattern = True } in
990 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
992pRHS :: SyntaxInfo -> Name -> IParser PTerm
993pRHS syn n = do lchar '='; pExpr syn
994 <|> do symbol "?="; rhs <- pExpr syn;
995 return (PLet (UN "value") Placeholder rhs (PMetavar n'))
996 <|> do reserved "impossible"; return PImpossible
997 where mkN (UN x) = UN (x++"_lemma_1")
998 mkN (NS x n) = NS (mkN x) n
999 n' = mkN n
1001pClause :: SyntaxInfo -> IParser PClause
1002pClause syn
1003 = try (do push_indent
1004 n_in <- pfName; let n = expandNS syn n_in
1005 cargs <- many (pConstraintArg syn)
1006 iargs <- many (pImplicitArg syn)
1007 fc <- pfc
1008 args <- many (pArgExpr syn)
1009 wargs <- many (pWExpr syn)
1010 rhs <- pRHS syn n
1011 ist <- getState
1012 let ctxt = tt_ctxt ist
1013 let wsyn = syn { syn_namespace = [] }
1014 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1015 pop_indent
1016 return x,
1017 do pTerminator
1018 return ([], [])]
1019 let capp = PApp fc (PRef fc n)
1020 (iargs ++ cargs ++ map pexp args)
1021 ist <- getState
1022 setState (ist { lastParse = Just n })
1023 return $ PClause n capp wargs rhs wheres)
1024 <|> try (do push_indent
1025 wargs <- many1 (pWExpr syn)
1026 ist <- getState
1027 n <- case lastParse ist of
1028 Just t -> return t
1029 Nothing -> fail "Invalid clause"
1030 rhs <- pRHS syn n
1031 let ctxt = tt_ctxt ist
1032 let wsyn = syn { syn_namespace = [] }
1033 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1034 pop_indent
1035 return x,
1036 do pTerminator
1037 return ([], [])]
1038 return $ PClauseR wargs rhs wheres)
1040 <|> try (do push_indent
1041 n_in <- pfName; let n = expandNS syn n_in
1042 cargs <- many (pConstraintArg syn)
1043 iargs <- many (pImplicitArg syn)
1044 fc <- pfc
1045 args <- many (pArgExpr syn)
1046 wargs <- many (pWExpr syn)
1047 let capp = PApp fc (PRef fc n)
1048 (iargs ++ cargs ++ map pexp args)
1049 reserved "with"
1050 wval <- pSimpleExpr syn
1051 open_block
1052 ds <- many1 $ pFunDecl syn
1053 let withs = map (fillLHSD n capp wargs) $ concat ds
1054 close_block
1055 ist <- getState
1056 setState (ist { lastParse = Just n })
1057 pop_indent
1058 return $ PWith n capp wargs wval withs)
1060 <|> try (do wargs <- many1 (pWExpr syn)
1061 reserved "with"
1062 wval <- pSimpleExpr syn
1063 open_block
1064 ds <- many1 $ pFunDecl syn
1065 let withs = concat ds
1066 close_block
1067 return $ PWithR wargs wval withs)
1069 <|> do push_indent
1070 l <- pArgExpr syn
1071 op <- operator
1072 let n = expandNS syn (UN op)
1073 r <- pArgExpr syn
1074 fc <- pfc
1075 wargs <- many (pWExpr syn)
1076 rhs <- pRHS syn n
1077 let wsyn = syn { syn_namespace = [] }
1078 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn
1079 pop_indent
1080 return x,
1081 do pTerminator
1082 return ([], [])]
1083 ist <- getState
1084 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1085 setState (ist { lastParse = Just n })
1086 return $ PClause n capp wargs rhs wheres
1088 <|> do l <- pArgExpr syn
1089 op <- operator
1090 let n = expandNS syn (UN op)
1091 r <- pArgExpr syn
1092 fc <- pfc
1093 wargs <- many (pWExpr syn)
1094 reserved "with"
1095 wval <- pSimpleExpr syn
1096 open_block
1097 ds <- many1 $ pFunDecl syn
1098 close_block
1099 ist <- getState
1100 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
1101 let withs = map (fillLHSD n capp wargs) $ concat ds
1102 setState (ist { lastParse = Just n })
1103 return $ PWith n capp wargs wval withs
1104 where
1105 fillLHS n capp owargs (PClauseR wargs v ws)
1106 = PClause n capp (owargs ++ wargs) v ws
1107 fillLHS n capp owargs (PWithR wargs v ws)
1108 = PWith n capp (owargs ++ wargs) v
1109 (map (fillLHSD n capp (owargs ++ wargs)) ws)
1110 fillLHS _ _ _ c = c
1112 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
1113 fillLHSD n c a x = x
1115pWExpr :: SyntaxInfo -> IParser PTerm
1116pWExpr syn = do lchar '|'; pExpr' syn
1118pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
1119pWhereblock n syn
1120 = do reserved "where"; open_block
1121 ds <- many1 $ pFunDecl syn
1122 let dns = concatMap (concatMap declared) ds
1123 close_block
1124 return (concat ds, map (\x -> (x, decoration syn x)) dns)
1126pDirective :: IParser [PDecl]
1127pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
1128 return [PDirective (do addLib lib
1129 addIBC (IBCLib lib))])
1130 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
1131 return [PDirective (do datadir <- liftIO $ getDataDir
1132 o <- liftIO $ findInPath [".", datadir] obj
1133 addIBC (IBCObj o)
1134 addObjectFile o)])
1135 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
1136 return [PDirective (do addHdr hdr
1137 addIBC (IBCHeader hdr))])
1138 <|> try (do lchar '%'; reserved "hide"; n <- iName []
1139 return [PDirective (do setAccessibility n Hidden
1140 addIBC (IBCAccess n Hidden))])
1141 <|> try (do lchar '%'; reserved "freeze"; n <- iName []
1142 return [PDirective (do setAccessibility n Frozen
1143 addIBC (IBCAccess n Frozen))])
1144 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
1145 return [PDirective (do i <- getIState
1146 putIState (i { default_access = acc }))])
1147 <|> do lchar '%'; reserved "logging"; i <- natural;
1148 return [PDirective (setLogLevel (fromInteger i))]
1150pTactic :: SyntaxInfo -> IParser PTactic
1151pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
1152 return $ Intro ns
1153 <|> do reserved "intros"; return Intros
1154 <|> try (do reserved "refine"; n <- pName
1155 imps <- many1 imp
1156 return $ Refine n imps)
1157 <|> do reserved "refine"; n <- pName
1158 i <- getState
1159 return $ Refine n []
1160 <|> do reserved "rewrite"; t <- pExpr syn;
1161 i <- getState
1162 return $ Rewrite (desugar syn i t)
1163 <|> do reserved "let"; n <- pName; lchar '=';
1164 t <- pExpr syn;
1165 i <- getState
1166 return $ LetTac n (desugar syn i t)
1167 <|> do reserved "focus"; n <- pName
1168 return $ Focus n
1169 <|> do reserved "exact"; t <- pExpr syn;
1170 i <- getState
1171 return $ Exact (desugar syn i t)
1172 <|> do reserved "try"; t <- pTactic syn;
1173 lchar '|';
1174 t1 <- pTactic syn
1175 return $ Try t t1
1176 <|> do lchar '{'
1177 t <- pTactic syn;
1178 lchar ';';
1179 t1 <- pTactic syn;
1180 lchar '}'
1181 return $ TSeq t t1
1182 <|> do reserved "compute"; return Compute
1183 <|> do reserved "trivial"; return Trivial
1184 <|> do reserved "solve"; return Solve
1185 <|> do reserved "attack"; return Attack
1186 <|> do reserved "state"; return ProofState
1187 <|> do reserved "term"; return ProofTerm
1188 <|> do reserved "undo"; return Undo
1189 <|> do reserved "qed"; return Qed
1190 <|> do reserved "abandon"; return Abandon
1191 <|> do lchar ':'; reserved "q"; return Abandon
1192 where
1193 imp = do lchar '?'; return False
1194 <|> do lchar '_'; return True
1196desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
1197desugar syn i t = let t' = expandDo (dsl_info syn) t in
1198 t' -- addImpl i t'
1200expandDo :: DSL -> PTerm -> PTerm
1201expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)
1202expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
1203expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
1204expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
1205 (map (fmap (expandDo dsl)) args)
1206expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)
1207 (map (pmap (expandDo dsl)) opts)
1208expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)
1209expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)
1210 (expandDo dsl r)
1211expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)
1212expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
1213expandDo dsl (PReturn fc) = dsl_return dsl
1214expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
1215 where
1216 block b [DoExp fc tm] = tm
1217 block b [a] = PElabError "Last statement in do block must be an expression"
1218 block b (DoBind fc n tm : rest)
1219 = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]
1220 block b (DoBindP fc p tm : rest)
1221 = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder
1222 (PCase fc (PRef fc (MN 0 "bpat"))
1223 [(p, block b rest)]))]
1224 block b (DoLet fc n ty tm : rest)
1225 = PLet n ty tm (block b rest)
1226 block b (DoLetP fc p tm : rest)
1227 = PCase fc tm [(p, block b rest)]
1228 block b (DoExp fc tm : rest)
1229 = PApp fc b
1230 [pexp tm,
1231 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]
1232 block b _ = PElabError "Invalid statement in do block"
1233expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
1234expandDo dsl t = t
1236unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
1237unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in
1238 mkap (getFn e)
1239 where
1240 getFn (PApp fc f args) = (PApp fc pure [pexp f], args)
1241 getFn f = (f, [])
1243 mkap (f, []) = f
1244 mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as)
1246unIdiom ap pure fc e = PApp fc pure [pexp e]