{-# LANGUAGE PatternGuards, ScopedTypeVariables #-} -- | Parse the full Idris language. module Idris.Parser where import Idris.AbsSyntax import Idris.DSL import Idris.Imports import Idris.Error import Idris.ElabDecls import Idris.ElabTerm import Idris.Coverage import Idris.IBC import Idris.Unlit import Idris.Providers import Paths_idris import Util.DynamicLinker import Core.CoreParser import Core.TT import Core.Evaluate import Text.Parsec import Text.Parsec.Error import Text.Parsec.Expr import Text.Parsec.Language import Text.Parsec.String import qualified Text.Parsec.Token as PTok import Data.List import Data.List.Split(splitOn) import Control.Monad.State import Control.Monad.Error import Debug.Trace import Data.Maybe import System.FilePath type TokenParser a = PTok.TokenParser a type IParser = GenParser Char IState lexer :: TokenParser IState lexer = idrisLexer whiteSpace = PTok.whiteSpace lexer lexeme = PTok.lexeme lexer symbol = PTok.symbol lexer natural = PTok.natural lexer parens = PTok.parens lexer semi = PTok.semi lexer comma = PTok.comma lexer identifier = PTok.identifier lexer reserved = PTok.reserved lexer operator = PTok.operator lexer reservedOp = PTok.reservedOp lexer integer = PTok.integer lexer float = PTok.float lexer strlit = PTok.stringLiteral lexer chlit = PTok.charLiteral lexer lchar = lexeme.char fixErrorMsg :: String -> [String] -> String fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes) -- Loading modules loadModule :: FilePath -> Idris String loadModule f = idrisCatch (do i <- getIState let file = takeWhile (/= ' ') f ibcsd <- valIBCSubDir i ids <- allImportDirs i fp <- liftIO $ findImport ids ibcsd file if file `elem` imported i then iLOG $ "Already read " ++ file else do putIState (i { imported = file : imported i }) case fp of IDR fn -> loadSource False fn LIDR fn -> loadSource True fn IBC fn src -> idrisCatch (loadIBC fn) (\c -> do iLOG $ fn ++ " failed " ++ show c case src of IDR sfn -> loadSource False sfn LIDR sfn -> loadSource True sfn) let (dir, fh) = splitFileName file return (dropExtension fh)) (\e -> do let msg = show e setErrLine (getErrLine msg) iputStrLn msg return "") loadSource :: Bool -> FilePath -> Idris () loadSource lidr f = do iLOG ("Reading " ++ f) i <- getIState let def_total = default_total i file_in <- liftIO $ readFile f file <- if lidr then tclift $ unlit f file_in else return file_in (mname, modules, rest, pos) <- parseImports f file i <- getIState putIState (i { default_access = Hidden }) mapM_ loadModule modules clearIBC -- start a new .ibc file mapM_ (addIBC . IBCImport) modules ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname }) f rest pos unless (null ds') $ do let ds = namespaces mname ds' logLvl 3 (dumpDecls ds) i <- getIState logLvl 10 (show (toAlist (idris_implicits i))) logLvl 3 (show (idris_infixes i)) -- Now add all the declarations to the context v <- verbose when v $ iputStrLn $ "Type checking " ++ f elabDecls toplevel ds i <- getIState -- simplify every definition do give the totality checker -- a better chance mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n updateContext (simplifyCasedef n)) (map snd (idris_totcheck i)) -- build size change graph from simplified definitions iLOG "Totality checking" i <- getIState mapM_ buildSCG (idris_totcheck i) mapM_ checkDeclTotality (idris_totcheck i) iLOG ("Finished " ++ f) ibcsd <- valIBCSubDir i let ibc = ibcPathNoFallback ibcsd f iLOG "Universe checking" iucheck i <- getIState addHides (hide_list i) ok <- noErrors when ok $ idrisCatch (do writeIBC f ibc; clearIBC) (\c -> return ()) -- failure is harmless i <- getIState putIState (i { default_total = def_total, hide_list = [] }) return () return () where namespaces [] ds = ds namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)] addHides :: [(Name, Maybe Accessibility)] -> Idris () addHides xs = do i <- getIState let defh = default_access i let (hs, as) = partition isNothing xs unless (null as) $ mapM_ doHide (map (\ (n, _) -> (n, defh)) hs ++ map (\ (n, Just a) -> (n, a)) as) where isNothing (_, Nothing) = True isNothing _ = False doHide (n, a) = do setAccessibility n a addIBC (IBCAccess n a) parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)" parseTac i = runParser (do t <- pTactic defaultSyntax eof return t) i "(proof)" parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos) parseImports fname input = do i <- getIState case runParser (do whiteSpace mname <- pHeader ps <- many pImport rest <- getInput pos <- getPosition return ((mname, ps, rest, pos), i)) i fname input of Left err -> fail (show err) Right (x, i) -> do putIState i return x pHeader :: IParser [String] pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';') return (parseName i)) <|> return [] where parseName x = case span (/='.') x of (x, "") -> [x] (x, '.':y) -> x : parseName y pushIndent :: IParser () pushIndent = do pos <- getPosition ist <- getState setState (ist { indent_stack = sourceColumn pos : indent_stack ist }) lastIndent :: IParser Int lastIndent = do ist <- getState case indent_stack ist of (x : xs) -> return x _ -> return 1 indent :: IParser Int indent = liftM sourceColumn getPosition popIndent :: IParser () popIndent = do ist <- getState let (x : xs) = indent_stack ist setState (ist { indent_stack = xs }) openBlock :: IParser () openBlock = do lchar '{' ist <- getState setState (ist { brace_stack = Nothing : brace_stack ist }) <|> do ist <- getState lvl <- indent setState (ist { brace_stack = Just lvl : brace_stack ist }) closeBlock :: IParser () closeBlock = do ist <- getState bs <- case brace_stack ist of [] -> eof >> return [] Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return []) Just lvl : xs -> (do i <- indent inp <- getInput -- trace (show (take 10 inp, i, lvl)) $ if i >= lvl && take 1 inp /= ")" then fail "Not end of block" else return xs) <|> (eof >> return []) setState (ist { brace_stack = bs }) pTerminator = do lchar ';'; popIndent <|> do c <- indent; l <- lastIndent if c <= l then popIndent else fail "Not a terminator" <|> do i <- getInput if "}" `isPrefixOf` i || ")" `isPrefixOf` i then popIndent else fail "Not a terminator" <|> lookAhead eof pBarTerminator = do lchar '|'; return () <|> do c <- indent; l <- lastIndent unless (c <= l) $ fail "Not a terminator" <|> lookAhead eof pKeepTerminator = do lchar ';'; return () <|> do c <- indent; l <- lastIndent unless (c <= l) $ fail "Not a terminator" <|> do i <- getInput let h = take 1 i unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator" <|> lookAhead eof notEndApp = do c <- indent; l <- lastIndent i <- getInput when (c <= l) $ fail "Terminator" notEndBlock = do ist <- getState case brace_stack ist of Just lvl : xs -> do i <- indent inp <- getInput when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block" _ -> return () -- | Use Parsec's internal state to construct a source code position pfc :: IParser FC pfc = do s <- getPosition let (dir, file) = splitFileName (sourceName s) let f = if dir == addTrailingPathSeparator "." then file else sourceName s return $ FC f (sourceLine s) pImport :: IParser String pImport = do reserved "import"; f <- identifier; option ';' (lchar ';') return (toPath f) where toPath n = foldl1' () $ splitOn "." n -- | A program is a list of declarations, possibly with associated -- documentation strings. parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl] parseProg syn fname input pos = do i <- getIState case runParser (do setPosition pos whiteSpace ps <- many (pDecl syn) eof i' <- getState return (concat ps, i')) i fname input of Left err -> do iputStrLn (show err) return [] Right (x, i) -> do putIState i return (collect x) -- | Collect 'PClauses' with the same function name collect :: [PDecl] -> [PDecl] collect (c@(PClauses _ o _ _) : ds) = clauses (cname c) [] (c : ds) where clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds) | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds) | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds clauses (Just n) acc xs = PClauses (getfc c) o n (reverse acc) : collect xs clauses Nothing acc (x:xs) = collect xs clauses Nothing acc [] = [] cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing getfc (PClauses fc _ _ _) = fc collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds collect (PClass doc f s cs n ps ds : ds') = PClass doc f s cs n ps (collect ds) : collect ds' collect (PInstance f s cs n ps t en ds : ds') = PInstance f s cs n ps t en (collect ds) : collect ds' collect (d : ds) = d : collect ds collect [] = [] pFullExpr :: SyntaxInfo -> IParser PTerm pFullExpr syn = do x <- pExpr syn; eof; i <- getState return $ desugar syn i x -- | Parse a top-level declaration pDecl :: SyntaxInfo -> IParser [PDecl] pDecl syn = do notEndBlock pDeclBody where pDeclBody = do d <- pDecl' syn i <- getState let d' = fmap (desugar syn i) d return [d'] <|> pUsing syn <|> pParams syn <|> pMutual syn <|> pNamespace syn <|> pClass syn <|> pInstance syn <|> do d <- pDSL syn; return [d] <|> pDirective syn <|> try (pProvider syn) <|> pTransform syn <|> try (do reserved "import"; fp <- identifier fail "imports must be at the top of file") pFunDecl :: SyntaxInfo -> IParser [PDecl] pFunDecl syn = try (do notEndBlock d <- pFunDecl' syn i <- getState let d' = fmap (desugar syn i) d return [d']) --------- Top Level Declarations --------- pDecl' :: SyntaxInfo -> IParser PDecl pDecl' syn = try pFixity <|> try (pFunDecl' syn) <|> try (pData syn) <|> try (pRecord syn) <|> try (pSyntaxDecl syn) pSyntaxDecl :: SyntaxInfo -> IParser PDecl pSyntaxDecl syn = do s <- pSyntaxRule syn i <- getState let rs = syntax_rules i let ns = syntax_keywords i let ibc = ibc_write i let ks = map show (names s) setState (i { syntax_rules = s : rs, syntax_keywords = ks ++ ns, ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }) fc <- pfc return (PSyntax fc s) where names (Rule syms _ _) = mapMaybe ename syms ename (Keyword n) = Just n ename _ = Nothing pSyntaxRule :: SyntaxInfo -> IParser Syntax pSyntaxRule syn = do pushIndent sty <- option AnySyntax (do reserved "term"; return TermSyntax <|> do reserved "pattern"; return PatternSyntax) reserved "syntax" syms <- many1 pSynSym when (all expr syms) $ fail "No keywords in syntax rule" let ns = mapMaybe name syms when (length ns /= length (nub ns)) $ fail "Repeated variable in syntax rule" lchar '=' tm <- pTExpr (impOK syn) pTerminator return (Rule (mkSimple syms) tm sty) where expr (Expr _) = True expr _ = False name (Expr n) = Just n name _ = Nothing -- Can't parse two full expressions (i.e. expressions with application) in a row -- so change them both to a simple expression mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es mkSimple xs = mkSimple' xs mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 : mkSimple es mkSimple' (e : es) = e : mkSimple' es mkSimple' [] = [] pSynSym :: IParser SSymbol pSynSym = try (do lchar '['; n <- pName; lchar ']' return (Expr n)) <|> try (do lchar '{'; n <- pName; lchar '}' return (Binding n)) <|> do n <- iName [] return (Keyword n) <|> do sym <- strlit return (Symbol sym) pFunDecl' :: SyntaxInfo -> IParser PDecl pFunDecl' syn = try (do doc <- option "" (pDocComment '|') pushIndent ist <- getState let initOpts = if default_total ist then [TotalFn] else [] opts <- pFnOpts initOpts acc <- pAccessibility opts' <- pFnOpts opts n_in <- pfName let n = expandNS syn n_in fc <- pfc ty <- pTSig (impOK syn) pTerminator -- ty' <- implicit syn n ty addAcc n acc return (PTy doc syn fc opts' n ty)) <|> try (pPostulate syn) <|> try (pPattern syn) <|> try (pCAF syn) pPostulate :: SyntaxInfo -> IParser PDecl pPostulate syn = do doc <- option "" (pDocComment '|') pushIndent reserved "postulate" ist <- getState let initOpts = if default_total ist then [TotalFn] else [] opts <- pFnOpts initOpts acc <- pAccessibility opts' <- pFnOpts opts n_in <- pfName let n = expandNS syn n_in ty <- pTSig (impOK syn) fc <- pfc pTerminator addAcc n acc return (PPostulate doc syn fc opts' n ty) pUsing :: SyntaxInfo -> IParser [PDecl] pUsing syn = do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')' openBlock let uvars = using syn ds <- many1 (pDecl (syn { using = uvars ++ ns })) closeBlock return (concat ds) pParams :: SyntaxInfo -> IParser [PDecl] pParams syn = do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')' openBlock let pvars = syn_params syn ds <- many1 (pDecl syn { syn_params = pvars ++ ns }) closeBlock fc <- pfc return [PParams fc ns (concat ds)] pMutual :: SyntaxInfo -> IParser [PDecl] pMutual syn = do reserved "mutual" openBlock let pvars = syn_params syn ds <- many1 (pDecl syn) closeBlock fc <- pfc return [PMutual fc (concat ds)] pNamespace :: SyntaxInfo -> IParser [PDecl] pNamespace syn = do reserved "namespace"; n <- identifier; openBlock ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn }) closeBlock return [PNamespace n (concat ds)] --------- Fixity --------- pFixity :: IParser PDecl pFixity = do pushIndent f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',') pTerminator let prec = fromInteger i istate <- getState let infixes = idris_infixes istate let fs = map (Fix (f prec)) ops let redecls = map (alreadyDeclared infixes) fs let ill = filter (not . checkValidity) redecls if null ill then do setState (istate { idris_infixes = nub $ sort (fs ++ infixes) , ibc_write = map IBCFix fs ++ ibc_write istate }) fc <- pfc return (PFix fc (f prec) ops) else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\"" ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl]) alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs) checkValidity :: (FixDecl, [FixDecl]) -> Bool checkValidity (f, fs) = all (== f) fs extractName :: FixDecl -> String extractName (Fix _ n) = n fixity :: IParser (Int -> Fixity) fixity = try (do reserved "infixl"; return Infixl) <|> try (do reserved "infixr"; return Infixr) <|> try (do reserved "infix"; return InfixN) <|> try (do reserved "prefix"; return PrefixN) --------- Type classes --------- pClass :: SyntaxInfo -> IParser [PDecl] pClass syn = do doc <- option "" (pDocComment '|') acc <- pAccessibility reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName let n = expandNS syn n_in cs <- many carg reserved "where"; openBlock ds <- many $ pFunDecl syn closeBlock let allDs = concat ds accData acc n (concatMap declared allDs) return [PClass doc syn fc cons n cs allDs] where carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')' return (i, ty) <|> do i <- pName; return (i, PType) pInstance :: SyntaxInfo -> IParser [PDecl] pInstance syn = do reserved "instance"; fc <- pfc en <- option Nothing (do lchar '['; n_in <- pfName; lchar ']' let n = expandNS syn n_in return (Just n)) cs <- pConstList syn cn <- pName args <- many (pSimpleExpr syn) let sc = PApp fc (PRef fc cn) (map pexp args) let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc reserved "where"; openBlock ds <- many $ pFunDecl syn closeBlock return [PInstance syn fc cs cn args t en (concat ds)] --------- Expressions --------- pExpr syn = do i <- getState buildExpressionParser (table (idris_infixes i)) (pExpr' syn) pExpr' :: SyntaxInfo -> IParser PTerm pExpr' syn = try (pExtExpr syn) <|> pNoExtExpr syn pExtExpr :: SyntaxInfo -> IParser PTerm pExtExpr syn = do i <- getState pExtensions syn (syntax_rules i) pSimpleExtExpr :: SyntaxInfo -> IParser PTerm pSimpleExtExpr syn = do i <- getState pExtensions syn (filter simple (syntax_rules i)) where simple (Rule (Expr x:xs) _ _) = False simple (Rule (SimpleExpr x:xs) _ _) = False simple (Rule [Keyword _] _ _) = True simple (Rule [Symbol _] _ _) = True simple (Rule (_:xs) _ _) = case last xs of Keyword _ -> True Symbol _ -> True _ -> False simple _ = False pNoExtExpr syn = try (pApp syn) <|> try (pMatchApp syn) <|> try (pUnifyLog syn) <|> pRecordType syn <|> try (pSimpleExpr syn) <|> pLambda syn <|> pLet syn <|> pRewriteTerm syn <|> pPi syn <|> pDoBlock syn pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules)) where valid (Rule _ _ AnySyntax) = True valid (Rule _ _ PatternSyntax) = inPattern syn valid (Rule _ _ TermSyntax) = not (inPattern syn) data SynMatch = SynTm PTerm | SynBind Name pExt :: SyntaxInfo -> Syntax -> IParser PTerm pExt syn (Rule ssym ptm _) = do smap <- mapM pSymbol ssym let ns = mapMaybe id smap return (update ns ptm) -- updated with smap where pSymbol (Keyword n) = do reserved (show n); return Nothing pSymbol (Expr n) = do tm <- pExpr syn return $ Just (n, SynTm tm) pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn return $ Just (n, SynTm tm) pSymbol (Binding n) = do b <- pName return $ Just (n, SynBind b) pSymbol (Symbol s) = do symbol s return Nothing dropn n [] = [] dropn n ((x,t) : xs) | n == x = xs | otherwise = (x,t):dropn n xs updateB ns n = case lookup n ns of Just (SynBind t) -> t _ -> n update ns (PRef fc n) = case lookup n ns of Just (SynTm t) -> t _ -> PRef fc n update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc) update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc) update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val) (update (dropn n ns) sc) update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args) update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts) update ns (PPair fc l r) = PPair fc (update ns l) (update ns r) update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r) update ns (PAlternative a as) = PAlternative a (map (update ns) as) update ns (PHidden t) = PHidden (update ns t) update ns (PDoBlock ds) = PDoBlock $ upd ns ds where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t) : upd (dropn n ns) ds upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t) : upd ns ds upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t) : upd ns ds update ns t = t pName = do i <- getState iName (syntax_keywords i) <|> do reserved "instance" i <- getState UN n <- iName (syntax_keywords i) return (UN ('@':n)) -- | Parser for an operator in function position, i.e. enclosed by `()', with an -- optional namespace. pOpFront = maybeWithNS pOpFrontNoNS False [] where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o pfName = try pOpFront <|> pName pTotality :: IParser Bool pTotality = do reserved "total"; return True <|> do reserved "partial"; return False pAccessibility' :: IParser Accessibility pAccessibility' = do reserved "public"; return Public <|> do reserved "abstract"; return Frozen <|> do reserved "private"; return Hidden pAccessibility :: IParser (Maybe Accessibility) pAccessibility = do acc <- pAccessibility'; return (Just acc) <|> return Nothing pFnOpts :: [FnOpt] -> IParser [FnOpt] pFnOpts opts = do reserved "total"; pFnOpts (TotalFn : opts) <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn])) <|> try (do lchar '%'; reserved "export"; c <- strlit; pFnOpts (CExport c : opts)) <|> try (do lchar '%'; reserved "assert_total"; pFnOpts (AssertTotal : opts)) <|> do lchar '%'; reserved "specialise"; lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']' pFnOpts (Specialise ns : opts) <|> do reserved "implicit"; pFnOpts (Implicit : opts) <|> return opts where nameTimes = do n <- pfName t <- option Nothing (do reds <- natural return (Just (fromInteger reds))) return (n, t) addAcc :: Name -> Maybe Accessibility -> IParser () addAcc n a = do i <- getState setState (i { hide_list = (n, a) : hide_list i }) pCaseExpr syn = do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of"; openBlock pushIndent opts <- many1 (do notEndBlock x <- pCaseOpt syn pKeepTerminator return x) -- sepBy1 (pCaseOpt syn) (lchar '|') popIndent closeBlock return (PCase fc scr opts) pProofExpr syn = do reserved "proof"; lchar '{' ts <- endBy (pTactic syn) (lchar ';') lchar '}' return (PProof ts) pTacticsExpr syn = do reserved "tactics"; lchar '{' ts <- endBy (pTactic syn) (lchar ';') lchar '}' return (PTactics ts) pSimpleExpr syn = try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t) <|> do lchar '?'; x <- pName; return (PMetavar x) <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc) <|> do reserved "refl"; fc <- pfc; tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}'; return t) return (PRefl fc tm) -- <|> do reserved "return"; fc <- pfc; return (PReturn fc) <|> pProofExpr syn <|> pTacticsExpr syn <|> pCaseExpr syn <|> try (do x <- pfName fc <- pfc return (PRef fc x)) <|> try (do lchar '!'; x <- pfName fc <- pfc return (PInferRef fc x)) <|> try (pList syn) <|> try (pComprehension syn) <|> try (pAlt syn) <|> try (pIdiom syn) <|> try (do lchar '(' bracketed (noImp syn)) <|> try (do c <- pConstant fc <- pfc return (modifyConst syn fc (PConstant c))) <|> do reserved "Type"; return PType <|> try (do symbol "()" fc <- pfc return (PTrue fc)) <|> try (do symbol "_|_" fc <- pfc return (PFalse fc)) <|> do lchar '_'; return Placeholder <|> pSimpleExtExpr syn bracketed syn = try (pPair syn) <|> try (do e <- pExpr syn; lchar ')'; return e) -- <|> try (do reserved "typed" -- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')' -- return (PTyped e t)) <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')' return $ PLam (MN 1000 "ARG") Placeholder (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")), pexp e])) <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')' return $ PLam (MN 1000 "ARG") Placeholder (PApp fc (PRef fc (UN o)) [pexp e, pexp (PRef fc (MN 1000 "ARG"))])) pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm) pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True }) symbol "=>"; rhs <- pExpr syn return (lhs, rhs) -- bit of a hack here. If the integer doesn't fit in an Int, treat it as a -- big integer, otherwise try fromInteger and the constants as alternatives. -- a better solution would be to fix fromInteger to work with Integer, as the -- name suggests, rather than Int modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm modifyConst syn fc (PConstant (BI x)) | not (inPattern syn) = PAlternative False (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))] : consts) | otherwise = PAlternative False consts where consts = [ PConstant (BI x) , PConstant (I (fromInteger x)) , PConstant (B8 (fromInteger x)) , PConstant (B16 (fromInteger x)) , PConstant (B32 (fromInteger x)) , PConstant (B64 (fromInteger x)) ] modifyConst syn fc x = x pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']' return (mkList fc xs) where mkList fc [] = PRef fc (UN "Nil") mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)] pPair syn = try (do l <- pExpr syn fc <- pfc rest <- restTuple case rest of [] -> return l [Left r] -> return (PPair fc l r) [Right r] -> return (PDPair fc l Placeholder r)) <|> try (do x <- ntuple lchar ')' return x) <|> do ln <- pName; lchar ':' lty <- pExpr syn reservedOp "**" fc <- pfc r <- pExpr syn lchar ')' return (PDPair fc (PRef fc ln) lty r) where restTuple = do lchar ')'; return [] <|> do lchar ',' r <- pExpr syn lchar ')' return [Left r] <|> do reservedOp "**" r <- pExpr syn lchar ')' return [Right r] ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ',' rest <- ntuple return (PPair fc l rest)) <|> (do l <- pExpr syn; fc <- pfc; lchar ',' r <- pExpr syn return (PPair fc l r)) pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)" return (PAlternative False alts) pHSimpleExpr syn = do lchar '.' e <- pSimpleExpr syn return $ PHidden e <|> pSimpleExpr syn pMatchApp syn = do ty <- pSimpleExpr syn symbol "<==" fc <- pfc f <- pfName return (PLet (MN 0 "match") ty (PMatchApp fc f) (PRef fc (MN 0 "match"))) pUnifyLog syn = do lchar '%'; reserved "unifyLog"; tm <- pSimpleExpr syn return (PUnifyLog tm) pApp syn = do f <- pSimpleExpr syn fc <- pfc args <- many1 (do notEndApp pArg syn) i <- getState return (dslify i $ PApp fc f args) where dslify i (PApp fc (PRef _ f) [a]) | [d] <- lookupCtxt f (idris_dsls i) = desugar (syn { dsl_info = d }) i (getTm a) dslify i t = t pArg :: SyntaxInfo -> IParser PArg pArg syn = try (pImplicitArg syn) <|> try (pConstraintArg syn) <|> do e <- pSimpleExpr syn return (pexp e) pImplicitArg syn = do lchar '{' n <- pName fc <- pfc v <- option (PRef fc n) (do lchar '=' pExpr syn) lchar '}' return (pimp n v) pConstraintArg syn = do symbol "@{" e <- pExpr syn symbol "}" return (pconst e) pRecordType syn = do reserved "record" lchar '{' fields <- sepBy1 pFieldType (lchar ',') lchar '}' fc <- pfc rec <- option Nothing (do e <- pSimpleExpr syn return (Just e)) case rec of Nothing -> return (PLam (MN 0 "fldx") Placeholder (applyAll fc fields (PRef fc (MN 0 "fldx")))) Just v -> return (applyAll fc fields v) where pFieldType = do n <- pfName lchar '=' e <- pExpr syn return (n, e) applyAll fc [] x = x applyAll fc ((n, e) : es) x = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x]) mkType (UN n) = UN ("set_" ++ n) mkType (MN 0 n) = MN 0 ("set_" ++ n) mkType (NS n s) = NS (mkType n) s noImp syn = syn { implicitAllowed = False } impOK syn = syn { implicitAllowed = True } pTSig syn = do lchar ':'; pTExpr syn pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return [] sc <- pExpr syn return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc) pLambda syn = do lchar '\\' try (do xt <- tyOptDeclList syn symbol "=>" sc <- pExpr syn return (bindList PLam xt sc) <|> (do ps <- sepBy (do fc <- pfc e <- pSimpleExpr syn return (fc, e)) (lchar ',') symbol "=>" sc <- pExpr syn return (pmList (zip [0..] ps) sc))) where pmList [] sc = sc pmList ((i, (fc, x)) : xs) sc = PLam (MN i "lamp") Placeholder (PCase fc (PRef fc (MN i "lamp")) [(x, pmList xs sc)]) pRewriteTerm syn = do reserved "rewrite" fc <- pfc prf <- pExpr syn giving <- option Nothing (do symbol "==>"; tm <- pExpr' syn return (Just tm)) reserved "in"; sc <- pExpr syn return (PRewrite fc (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc giving) pLet syn = try (do reserved "let"; n <- pName; ty <- option Placeholder (do lchar ':'; pExpr' syn) lchar '=' v <- pExpr syn reserved "in"; sc <- pExpr syn return (PLet n ty v sc)) <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } ) symbol "="; v <- pExpr syn reserved "in"; sc <- pExpr syn return (PCase fc v [(pat, sc)])) pPi syn = try (do lazy <- if implicitAllowed syn -- laziness is top level only then option False (do lchar '|'; return True) else return False st <- pStatic lchar '('; xt <- tyDeclList syn; lchar ')' doc <- option "" (pDocComment '^') symbol "->" sc <- pExpr syn return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> try (if implicitAllowed syn then do lazy <- option False (do lchar '|' return True) st <- pStatic lchar '{' xt <- tyDeclList syn lchar '}' symbol "->" sc <- pExpr syn return (bindList (PPi (Imp lazy st "")) xt sc) else fail "No implicit arguments allowed here") <|> try (do lchar '{' reserved "auto" xt <- tyDeclList syn lchar '}' symbol "->" sc <- pExpr syn return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc)) <|> try (do lchar '{' reserved "default" script <- pSimpleExpr syn xt <- tyDeclList syn lchar '}' symbol "->" sc <- pExpr syn return (bindList (PPi (TacImp False Dynamic script "")) xt sc)) <|> do --lazy <- option False (do lchar '|'; return True) lchar '{' reserved "static" lchar '}' t <- pExpr' syn symbol "->" sc <- pExpr syn return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc) pConstList :: SyntaxInfo -> IParser [PTerm] pConstList syn = try (do lchar '(' tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',') lchar ')' reservedOp "=>" return tys) <|> try (do t <- pExpr (noImp syn) reservedOp "=>" return [t]) <|> return [] usingDeclList syn = try (sepBy1 (usingDecl syn) (lchar ',')) <|> do ns <- sepBy1 pName (lchar ',') t <- pTSig (noImp syn) return (map (\x -> UImplicit x t) ns) usingDecl syn = try (do x <- pfName t <- pTSig (noImp syn) return (UImplicit x t)) <|> do c <- pfName xs <- many1 pfName return (UConstraint c xs) tyDeclList syn = try (sepBy1 (do x <- pfName t <- pTSig (noImp syn) return (x,t)) (lchar ',')) <|> do ns <- sepBy1 pName (lchar ',') t <- pTSig (noImp syn) return (map (\x -> (x, t)) ns) tyOptDeclList syn = sepBy1 (do x <- pfName; t <- option Placeholder (do lchar ':' pExpr syn) return (x,t)) (lchar ',') bindList b [] sc = sc bindList b ((n, t):bs) sc = b n t (bindList b bs sc) pComprehension syn = do lchar '[' fc <- pfc pat <- pExpr syn lchar '|' qs <- sepBy1 (pDo syn) (lchar ',') lchar ']' return (PDoBlock (map addGuard qs ++ [DoExp fc (PApp fc (PRef fc (UN "return")) [pexp pat])])) where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard")) [pexp e]) addGuard x = x pDoBlock syn = do reserved "do" openBlock pushIndent ds <- many1 (do notEndBlock x <- pDo syn pKeepTerminator return x) popIndent closeBlock return (PDoBlock ds) pDo syn = try (do reserved "let" i <- pName; ty <- option Placeholder (do lchar ':' pExpr' syn) reservedOp "=" fc <- pfc e <- pExpr syn return (DoLet fc i ty e)) <|> try (do reserved "let" i <- pExpr' syn reservedOp "=" fc <- pfc sc <- pExpr syn return (DoLetP fc i sc)) <|> try (do i <- pName symbol "<-" fc <- pfc e <- pExpr syn; return (DoBind fc i e)) <|> try (do i <- pExpr' syn symbol "<-" fc <- pfc e <- pExpr syn; return (DoBindP fc i e)) <|> try (do e <- pExpr syn fc <- pfc return (DoExp fc e)) pIdiom syn = do symbol "[|" fc <- pfc e <- pExpr syn symbol "|]" return (PIdiom fc e) pConstant :: IParser Const pConstant = do reserved "Integer";return (AType (ATInt ITBig)) <|> do reserved "Int"; return (AType (ATInt ITNative)) <|> do reserved "Char"; return (AType (ATInt ITChar)) <|> do reserved "Float"; return (AType ATFloat) <|> do reserved "String"; return StrType <|> do reserved "Ptr"; return PtrType <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8))) <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16))) <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32))) <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64))) <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16))) <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8))) <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4))) <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2))) <|> try (do f <- float; return $ Fl f) <|> try (do i <- natural; return $ BI i) <|> try (do s <- strlit; return $ Str s) <|> try (do c <- chlit; return $ Ch c) pStatic :: IParser Static pStatic = do lchar '[' reserved "static" lchar ']'; return Static <|> return Dynamic table fixes = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-")) [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]] ++ toTable (reverse fixes) ++ [[backtick], [binary "=" PEq AssocLeft], [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]] toTable fs = map (map toBin) (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs) where toBin (Fix (PrefixN _) op) = prefix op (\fc x -> PApp fc (PRef fc (UN op)) [pexp x]) toBin (Fix f op) = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f) assoc (Infixl _) = AssocLeft assoc (Infixr _) = AssocRight assoc (InfixN _) = AssocNone binary name f = Infix (do fc <- pfc reservedOp name doc <- option "" (pDocComment '^') return (f fc)) prefix name f = Prefix (do reservedOp name fc <- pfc; return (f fc)) backtick = Infix (do lchar '`'; n <- pfName lchar '`' fc <- pfc return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone --------- Data declarations --------- -- (works for classes too - 'abstract' means the data/class is visible but members not) accData :: Maybe Accessibility -> Name -> [Name] -> IParser () accData (Just Frozen) n ns = do addAcc n (Just Frozen) mapM_ (\n -> addAcc n (Just Hidden)) ns accData a n ns = do addAcc n a mapM_ (`addAcc` a) ns pRecord :: SyntaxInfo -> IParser PDecl pRecord syn = do doc <- option "" (pDocComment '|') acc <- pAccessibility reserved "record" fc <- pfc tyn_in <- pfName ty <- pTSig (impOK syn) let tyn = expandNS syn tyn_in reserved "where" openBlock pushIndent (cdoc, cn, cty, _) <- pConstructor syn pKeepTerminator popIndent closeBlock accData acc tyn [cn] let rsyn = syn { syn_namespace = show (nsroot tyn) : syn_namespace syn } let fns = getRecNames rsyn cty mapM_ (\n -> addAcc n acc) fns return $ PRecord doc rsyn fc tyn ty cdoc cn cty where getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)] ++ getRecNames syn sc getRecNames _ _ = [] toFreeze (Just Frozen) = Just Hidden toFreeze x = x pDataI = do reserved "data"; return False <|> do reserved "codata"; return True pData :: SyntaxInfo -> IParser PDecl pData syn = try (do doc <- option "" (pDocComment '|') acc <- pAccessibility co <- pDataI fc <- pfc tyn_in <- pfName ty <- pTSig (impOK syn) let tyn = expandNS syn tyn_in option (PData doc syn fc co (PLaterdecl tyn ty)) (do reserved "where" openBlock pushIndent cons <- many (do notEndBlock c <- pConstructor syn pKeepTerminator return c) -- (lchar '|') popIndent closeBlock accData acc tyn (map (\ (_, n, _, _) -> n) cons) return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> try (do doc <- option "" (pDocComment '|') pushIndent acc <- pAccessibility co <- pDataI fc <- pfc tyn_in <- pfName args <- many pName let ty = bindArgs (map (const PType) args) PType let tyn = expandNS syn tyn_in option (PData doc syn fc co (PLaterdecl tyn ty)) (do try (lchar '=') <|> do reserved "where" let kw = (if co then "co" else "") ++ "data " let n = show tyn_in ++ " " let s = kw ++ n let as = concat (intersperse " " $ map show args) ++ " " let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args) let ss = concat (intersperse " -> " $ map (const "Type") args) let fix1 = s ++ as ++ " = ..." let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..." let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..." fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3] cons <- sepBy1 (pSimpleCon syn) (lchar '|') pTerminator let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args) cons' <- mapM (\ (doc, x, cargs, cfc) -> do let cty = bindArgs cargs conty return (doc, x, cty, cfc)) cons accData acc tyn (map (\ (_, n, _, _) -> n) cons') return $ PData doc syn fc co (PDatadecl tyn ty cons'))) where mkPApp fc t [] = t mkPApp fc t xs = PApp fc t (map pexp xs) bindArgs :: [PTerm] -> PTerm -> PTerm bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC) pConstructor syn = do doc <- option "" (pDocComment '|') cn_in <- pfName; fc <- pfc let cn = expandNS syn cn_in ty <- pTSig (impOK syn) -- ty' <- implicit syn cn ty return (doc, cn, ty, fc) pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC) pSimpleCon syn = do cn_in <- pfName let cn = expandNS syn cn_in fc <- pfc args <- many (do notEndApp pSimpleExpr syn) doc <- option "" (pDocComment '^') return (doc, cn, args, fc) --------- DSL syntax overloading --------- pDSL :: SyntaxInfo -> IParser PDecl pDSL syn = do reserved "dsl" n <- pfName openBlock pushIndent bs <- many1 (do notEndBlock b <- pOverload syn pKeepTerminator return b) popIndent; closeBlock let dsl = mkDSL bs (dsl_info syn) checkDSL dsl i <- getState setState (i { idris_dsls = addDef n dsl (idris_dsls i) }) return (PDSL n dsl) where mkDSL bs dsl = let var = lookup "variable" bs first = lookup "index_first" bs next = lookup "index_next" bs leto = lookup "let" bs lambda = lookup "lambda" bs in initDSL { dsl_var = var, index_first = first, index_next = next, dsl_lambda = lambda, dsl_let = leto } checkDSL :: DSL -> IParser () checkDSL dsl = return () pOverload :: SyntaxInfo -> IParser (String, PTerm) pOverload syn = do o <- identifier <|> do reserved "let" return "let" if o `notElem` overloadable then fail $ show o ++ " is not an overloading" else do lchar '=' t <- pExpr syn return (o, t) where overloadable = ["let","lambda","index_first","index_next","variable"] --------- Pattern match clauses --------- pPattern :: SyntaxInfo -> IParser PDecl pPattern syn = do fc <- pfc clause <- pClause syn return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later pCAF :: SyntaxInfo -> IParser PDecl pCAF syn = do reserved "let" n_in <- pfName; let n = expandNS syn n_in lchar '=' t <- pExpr syn pTerminator fc <- pfc return (PCAF fc n t) pArgExpr syn = let syn' = syn { inPattern = True } in try (pHSimpleExpr syn') <|> pSimpleExtExpr syn' pRHS :: SyntaxInfo -> Name -> IParser PTerm pRHS syn n = do lchar '='; pExpr syn <|> do symbol "?="; name <- option n' (do symbol "{"; n <- pfName; symbol "}"; return n) rhs <- pExpr syn return (addLet name rhs) <|> do reserved "impossible"; return PImpossible where mkN (UN x) = UN (x++"_lemma_1") mkN (NS x n) = NS (mkN x) n n' = mkN n addLet nm (PLet n ty val rhs) = PLet n ty val (addLet nm rhs) addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs) where addLetC (l, r) = (l, addLet nm r) addLet nm rhs = (PLet (UN "value") Placeholder rhs (PMetavar nm)) pClause :: SyntaxInfo -> IParser PClause pClause syn = try (do pushIndent n_in <- pfName; let n = expandNS syn n_in cargs <- many (pConstraintArg syn) iargs <- many (pImplicitArg (syn { inPattern = True } )) fc <- pfc args <- many (try (pImplicitArg (syn { inPattern = True } )) <|> (fmap pexp (pArgExpr syn))) wargs <- many (pWExpr syn) rhs <- pRHS syn n ist <- getState let ctxt = tt_ctxt ist let wsyn = syn { syn_namespace = [] } (wheres, nmap) <- choice [do x <- pWhereblock n wsyn popIndent return x, do pTerminator return ([], [])] let capp = PApp fc (PRef fc n) (iargs ++ cargs ++ args) ist <- getState setState (ist { lastParse = Just n }) return $ PClause fc n capp wargs rhs wheres) <|> try (do pushIndent ty <- pSimpleExpr syn symbol "<==" fc <- pfc n_in <- pfName; let n = expandNS syn n_in rhs <- pRHS syn n ist <- getState let ctxt = tt_ctxt ist let wsyn = syn { syn_namespace = [] } (wheres, nmap) <- choice [do x <- pWhereblock n wsyn popIndent return x, do pTerminator return ([], [])] let capp = PLet (MN 0 "match") ty (PMatchApp fc n) (PRef fc (MN 0 "match")) ist <- getState setState (ist { lastParse = Just n }) return $ PClause fc n capp [] rhs wheres) <|> try (do pushIndent wargs <- many1 (pWExpr syn) ist <- getState n <- case lastParse ist of Just t -> return t Nothing -> fail "Invalid clause" fc <- pfc rhs <- pRHS syn n let ctxt = tt_ctxt ist let wsyn = syn { syn_namespace = [] } (wheres, nmap) <- choice [do x <- pWhereblock n wsyn popIndent return x, do pTerminator return ([], [])] return $ PClauseR fc wargs rhs wheres) <|> try (do pushIndent n_in <- pfName; let n = expandNS syn n_in cargs <- many (pConstraintArg syn) iargs <- many (pImplicitArg (syn { inPattern = True } )) fc <- pfc args <- many (try (pImplicitArg (syn { inPattern = True } )) <|> (fmap pexp (pArgExpr syn))) wargs <- many (pWExpr syn) let capp = PApp fc (PRef fc n) (iargs ++ cargs ++ args) ist <- getState setState (ist { lastParse = Just n }) reserved "with" wval <- pSimpleExpr syn openBlock ds <- many1 $ pFunDecl syn let withs = map (fillLHSD n capp wargs) $ concat ds closeBlock popIndent return $ PWith fc n capp wargs wval withs) <|> try (do wargs <- many1 (pWExpr syn) fc <- pfc reserved "with" wval <- pSimpleExpr syn openBlock ds <- many1 $ pFunDecl syn let withs = concat ds closeBlock return $ PWithR fc wargs wval withs) <|> do pushIndent l <- pArgExpr syn op <- operator let n = expandNS syn (UN op) r <- pArgExpr syn fc <- pfc wargs <- many (pWExpr syn) rhs <- pRHS syn n let wsyn = syn { syn_namespace = [] } (wheres, nmap) <- choice [do x <- pWhereblock n wsyn popIndent return x, do pTerminator return ([], [])] ist <- getState let capp = PApp fc (PRef fc n) [pexp l, pexp r] setState (ist { lastParse = Just n }) return $ PClause fc n capp wargs rhs wheres <|> do l <- pArgExpr syn op <- operator let n = expandNS syn (UN op) r <- pArgExpr syn fc <- pfc wargs <- many (pWExpr syn) reserved "with" wval <- pSimpleExpr syn openBlock ds <- many1 $ pFunDecl syn closeBlock ist <- getState let capp = PApp fc (PRef fc n) [pexp l, pexp r] let withs = map (fillLHSD n capp wargs) $ concat ds setState (ist { lastParse = Just n }) return $ PWith fc n capp wargs wval withs where fillLHS n capp owargs (PClauseR fc wargs v ws) = PClause fc n capp (owargs ++ wargs) v ws fillLHS n capp owargs (PWithR fc wargs v ws) = PWith fc n capp (owargs ++ wargs) v (map (fillLHSD n capp (owargs ++ wargs)) ws) fillLHS _ _ _ c = c fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs) fillLHSD n c a x = x pWExpr :: SyntaxInfo -> IParser PTerm pWExpr syn = do lchar '|' pExpr' syn pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)]) pWhereblock n syn = do reserved "where"; openBlock ds <- many1 $ pDecl syn let dns = concatMap (concatMap declared) ds closeBlock return (concat ds, map (\x -> (x, decoration syn x)) dns) pCodegen :: IParser Codegen pCodegen = try (do reserved "C"; return ViaC) <|> try (do reserved "Java"; return ViaJava) <|> try (do reserved "JavaScript"; return ViaJavaScript) <|> try (do reserved "Node"; return ViaNode) <|> try (do reserved "LLVM"; return ViaLLVM) <|> try (do reserved "Bytecode"; return Bytecode) pDirective :: SyntaxInfo -> IParser [PDecl] pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strlit; return [PDirective (do addLib cgn lib addIBC (IBCLib cgn lib))]) <|> try (do lchar '%'; reserved "link"; cgn <- pCodegen; obj <- strlit; return [PDirective (do datadir <- liftIO getDataDir o <- liftIO $ findInPath [".", datadir] obj addIBC (IBCObj cgn o) addObjectFile cgn o)]) <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit; return [PDirective (do addHdr cgn hdr addIBC (IBCHeader cgn hdr))]) <|> try (do lchar '%'; reserved "hide"; n <- iName [] return [PDirective (do setAccessibility n Hidden addIBC (IBCAccess n Hidden))]) <|> try (do lchar '%'; reserved "freeze"; n <- iName [] return [PDirective (do setAccessibility n Frozen addIBC (IBCAccess n Frozen))]) <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility' return [PDirective (do i <- getIState putIState (i { default_access = acc }))]) <|> try (do lchar '%'; reserved "default"; tot <- pTotality i <- getState setState (i { default_total = tot } ) return [PDirective (do i <- getIState putIState (i { default_total = tot }))]) <|> try (do lchar '%'; reserved "logging"; i <- natural; return [PDirective (setLogLevel (fromInteger i))]) <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 strlit (lchar ','); return [PDirective (do added <- addDyLib libs case added of Left lib -> addIBC (IBCDyLib (lib_name lib)) Right msg -> fail $ msg)]) <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders"; return [PDirective (addLangExt TypeProviders)]) pProvider :: SyntaxInfo -> IParser [PDecl] pProvider syn = do lchar '%'; reserved "provide"; lchar '('; n <- pfName; t <- pTSig syn; lchar ')' fc <- pfc reserved "with" e <- pExpr syn return [PProvider syn fc n t e] pTransform :: SyntaxInfo -> IParser [PDecl] pTransform syn = do lchar '%'; reserved "transform"; -- leave it unchecked, until we work out what this should -- actually mean... -- safety <- option True (do reserved "unsafe" -- return False) lhs <- pExpr syn fc <- pfc symbol "==>" rhs <- pExpr syn return [PTransform fc False lhs rhs] pTactic :: SyntaxInfo -> IParser PTactic pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',') return $ Intro ns <|> do reserved "intros"; return Intros <|> try (do reserved "refine"; n <- pName imps <- many1 imp return $ Refine n imps) <|> do reserved "refine"; n <- pName i <- getState return $ Refine n [] <|> do reserved "mrefine"; n <- pName i <- getState return $ MatchRefine n <|> do reserved "rewrite"; t <- pExpr syn; i <- getState return $ Rewrite (desugar syn i t) <|> do reserved "equiv"; t <- pExpr syn; i <- getState return $ Equiv (desugar syn i t) <|> try (do reserved "let"; n <- pName; lchar ':'; ty <- pExpr' syn; lchar '='; t <- pExpr syn; i <- getState return $ LetTacTy n (desugar syn i ty) (desugar syn i t)) <|> try (do reserved "let"; n <- pName; lchar '='; t <- pExpr syn; i <- getState return $ LetTac n (desugar syn i t)) <|> do reserved "focus"; n <- pName return $ Focus n <|> do reserved "exact"; t <- pExpr syn; i <- getState return $ Exact (desugar syn i t) <|> do reserved "applyTactic"; t <- pExpr syn; i <- getState return $ ApplyTactic (desugar syn i t) <|> do reserved "reflect"; t <- pExpr syn; i <- getState return $ Reflect (desugar syn i t) <|> do reserved "fill"; t <- pExpr syn; i <- getState return $ Fill (desugar syn i t) <|> do reserved "try"; t <- pTactic syn; lchar '|'; t1 <- pTactic syn return $ Try t t1 <|> do lchar '{' t <- pTactic syn; lchar ';'; t1 <- pTactic syn; lchar '}' return $ TSeq t t1 <|> do reserved "compute"; return Compute <|> do reserved "trivial"; return Trivial <|> do reserved "solve"; return Solve <|> do reserved "attack"; return Attack <|> do reserved "state"; return ProofState <|> do reserved "term"; return ProofTerm <|> do reserved "undo"; return Undo <|> do reserved "qed"; return Qed <|> do reserved "abandon"; return Abandon <|> do lchar ':'; reserved "q"; return Abandon where imp = do lchar '?'; return False <|> do lchar '_'; return True