@@ -1135,23 +1135,29 @@ Constant ::=
11351135 ;
11361136@
11371137-}
1138+
1139+constants :: [(String, Idris.Core.TT.Const)]
1140+constants =
1141+ [ ("Integer", AType (ATInt ITBig))
1142+ , ("Int", AType (ATInt ITNative))
1143+ , ("Char", AType (ATInt ITChar))
1144+ , ("Float", AType ATFloat)
1145+ , ("String", StrType)
1146+ , ("Ptr", PtrType)
1147+ , ("ManagedPtr", ManagedPtrType)
1148+ , ("prim__UnsafeBuffer", BufferType)
1149+ , ("Bits8", AType (ATInt (ITFixed IT8)))
1150+ , ("Bits16", AType (ATInt (ITFixed IT16)))
1151+ , ("Bits32", AType (ATInt (ITFixed IT32)))
1152+ , ("Bits64", AType (ATInt (ITFixed IT64)))
1153+ , ("Bits8x16", AType (ATInt (ITVec IT8 16)))
1154+ , ("Bits16x8", AType (ATInt (ITVec IT16 8)))
1155+ , ("Bits32x4", AType (ATInt (ITVec IT32 4)))
1156+ , ("Bits64x2", AType (ATInt (ITVec IT64 2)))
1157+ ]
1158+
11381159constant :: IdrisParser Idris.Core.TT.Const
1139−constant = do reserved "Integer"; return (AType (ATInt ITBig))
1140− <|> do reserved "Int"; return (AType (ATInt ITNative))
1141− <|> do reserved "Char"; return (AType (ATInt ITChar))
1142− <|> do reserved "Float"; return (AType ATFloat)
1143− <|> do reserved "String"; return StrType
1144− <|> do reserved "Ptr"; return PtrType
1145− <|> do reserved "ManagedPtr"; return ManagedPtrType
1146− <|> do reserved "prim__UnsafeBuffer"; return BufferType
1147− <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
1148− <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
1149− <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
1150− <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))
1151− <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))
1152− <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
1153− <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
1154− <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1160+constant = choice [ do reserved name; return ty | (name, ty) <- constants ]
11551161 <|> do f <- try float; return $ Fl f
11561162 <|> do i <- natural; return $ BI i
11571163 <|> do s <- verbatimStringLiteral; return $ Str s
@@ -1224,116 +1230,109 @@ TacticSeq ::=
12241230@
12251231-}
12261232
1233+-- | A specification of the arguments that tactics can take
1234+data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
1235+ | ExprTArg
1236+ | AltsTArg
1237+ | StringLitTArg
1238+
1239+-- The FIXMEs are Issue #1766 in the issue tracker.
1240+-- https://github.com/idris-lang/Idris-dev/issues/1766
1241+-- | A list of available tactics and their argument requirements
1242+tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
1243+tactics =
1244+ [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)
1245+ do ns <- sepBy (spaced name) (lchar ','); return $ Intro ns)
1246+ , noArgs ["intros"] Intros
1247+ , (["refine"], Just ExprTArg, const $
1248+ do n <- spaced fnName
1249+ imps <- many imp
1250+ return $ Refine n imps)
1251+ , (["mrefine"], Just ExprTArg, const $
1252+ do n <- spaced fnName
1253+ return $ MatchRefine n)
1254+ , expressionTactic ["rewrite"] Rewrite
1255+ , expressionTactic ["case"] CaseTac
1256+ , expressionTactic ["induction"] Induction
1257+ , expressionTactic ["equiv"] Equiv
1258+ , (["let"], Nothing, \syn -> -- FIXME syntax for let
1259+ do n <- (indentPropHolds gtProp *> name)
1260+ (do indentPropHolds gtProp *> lchar ':'
1261+ ty <- indentPropHolds gtProp *> expr' syn
1262+ indentPropHolds gtProp *> lchar '='
1263+ t <- indentPropHolds gtProp *> expr syn
1264+ i <- get
1265+ return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1266+ <|> (do indentPropHolds gtProp *> lchar '='
1267+ t <- indentPropHolds gtProp *> expr syn
1268+ i <- get
1269+ return $ LetTac n (desugar syn i t)))
1270+
1271+ , (["focus"], Just ExprTArg, const $
1272+ do n <- spaced name
1273+ return $ Focus n)
1274+ , expressionTactic ["exact"] Exact
1275+ , expressionTactic ["applyTactic"] ApplyTactic
1276+ , expressionTactic ["byReflection"] ByReflection
1277+ , expressionTactic ["reflect"] Reflect
1278+ , expressionTactic ["fill"] Fill
1279+ , (["try"], Just AltsTArg, \syn ->
1280+ do t <- spaced (tactic syn)
1281+ lchar '|'
1282+ t1 <- spaced (tactic syn)
1283+ return $ Try t t1)
1284+ , noArgs ["compute"] Compute
1285+ , noArgs ["trivial"] Trivial
1286+ , noArgs ["unify"] DoUnify
1287+ , (["search"], Nothing, const $
1288+ do depth <- option 10 natural
1289+ return (ProofSearch True True (fromInteger depth) Nothing []))
1290+ , noArgs ["instance"] TCInstance
1291+ , noArgs ["solve"] Solve
1292+ , noArgs ["attack"] Attack
1293+ , noArgs ["state"] ProofState
1294+ , noArgs ["term"] ProofTerm
1295+ , noArgs ["undo"] Undo
1296+ , noArgs ["qed"] Qed
1297+ , noArgs ["abandon", ":q"] Abandon
1298+ , noArgs ["skip"] Skip
1299+ , noArgs ["sourceLocation"] SourceFC
1300+ , expressionTactic [":e", ":eval"] TEval
1301+ , expressionTactic [":t", ":type"] TCheck
1302+ , expressionTactic [":search"] TSearch
1303+ , (["fail"], Just StringLitTArg, const $
1304+ do msg <- stringLiteral
1305+ return $ TFail [Idris.Core.TT.TextPart msg])
1306+ , ([":doc"], Just ExprTArg, const $
1307+ do whiteSpace
1308+ doc <- (Right <$> constant) <|> (Left <$> fnName)
1309+ eof
1310+ return (TDocStr doc))
1311+ ]
1312+ where
1313+ expressionTactic names tactic = (names, Just ExprTArg, \syn ->
1314+ do t <- spaced (expr syn)
1315+ i <- get
1316+ return $ tactic (desugar syn i t))
1317+ noArgs names tactic = (names, Nothing, const (return tactic))
1318+ spaced parser = indentPropHolds gtProp *> parser
1319+ imp :: IdrisParser Bool
1320+ imp = do lchar '?'; return False
1321+ <|> do lchar '_'; return True
1322+
1323+
12271324tactic :: SyntaxInfo -> IdrisParser PTactic
1228−tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (lchar ',')
1229− return $ Intro ns
1230− <|> do reserved "intros"; return Intros
1231− <|> try (do reserved "refine"; n <- (indentPropHolds gtProp *> fnName)
1232− imps <- some imp
1233− return $ Refine n imps)
1234− <|> do reserved "refine"; n <- (indentPropHolds gtProp *> fnName)
1235− i <- get
1236− return $ Refine n []
1237− <|> do reserved "mrefine"; n <- (indentPropHolds gtProp *> fnName)
1238− i <- get
1239− return $ MatchRefine n
1240− <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);
1241− i <- get
1242− return $ Rewrite (desugar syn i t)
1243− <|> do reserved "case"; t <- (indentPropHolds gtProp *> expr syn);
1244− i <- get
1245− return $ CaseTac (desugar syn i t)
1246− <|> do reserved "induction"; t <- (indentPropHolds gtProp *> expr syn);
1247− i <- get
1248− return $ Induction (desugar syn i t)
1249− <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);
1250− i <- get
1251− return $ Equiv (desugar syn i t)
1252− <|> try (do reserved "let"; n <- (indentPropHolds gtProp *> name); (indentPropHolds gtProp *> lchar ':');
1253− ty <- (indentPropHolds gtProp *> expr' syn); (indentPropHolds gtProp *> lchar '='); t <- (indentPropHolds gtProp *> expr syn);
1254− i <- get
1255− return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1256− <|> try (do reserved "let"; n <- (indentPropHolds gtProp *> name); (indentPropHolds gtProp *> lchar '=');
1257− t <- (indentPropHolds gtProp *> expr syn);
1258− i <- get
1259− return $ LetTac n (desugar syn i t))
1260− <|> do reserved "focus"; n <- (indentPropHolds gtProp *> name)
1261− return $ Focus n
1262− <|> do reserved "exact"; t <- (indentPropHolds gtProp *> expr syn);
1263− i <- get
1264− return $ Exact (desugar syn i t)
1265− <|> do reserved "applyTactic"; t <- (indentPropHolds gtProp *> expr syn);
1266− i <- get
1267− return $ ApplyTactic (desugar syn i t)
1268− <|> do reserved "byReflection"; t <- (indentPropHolds gtProp *> expr syn);
1269− i <- get
1270− return $ ByReflection (desugar syn i t)
1271− <|> do reserved "reflect"; t <- (indentPropHolds gtProp *> expr syn);
1272− i <- get
1273− return $ Reflect (desugar syn i t)
1274− <|> do reserved "fill"; t <- (indentPropHolds gtProp *> expr syn);
1275− i <- get
1276− return $ Fill (desugar syn i t)
1277− <|> do reserved "try"; t <- (indentPropHolds gtProp *> tactic syn);
1278− lchar '|';
1279− t1 <- (indentPropHolds gtProp *> tactic syn)
1280− return $ Try t t1
1325+tactic syn = choice [ do choice (map reserved names); parser syn
1326+ | (names, _, parser) <- tactics ]
12811327 <|> do lchar '{'
12821328 t <- tactic syn;
12831329 lchar ';';
12841330 ts <- sepBy1 (tactic syn) (lchar ';')
12851331 lchar '}'
12861332 return $ TSeq t (mergeSeq ts)
1287− <|> do reserved "compute"; return Compute
1288− <|> do reserved "trivial"; return Trivial
1289− <|> do reserved "unify"; return DoUnify
1290− <|> do reserved "search"
1291− depth <- option 10 natural
1292− return (ProofSearch True True (fromInteger depth) Nothing [])
1293− <|> do reserved "instance"; return TCInstance
1294− <|> do reserved "solve"; return Solve
1295− <|> do reserved "attack"; return Attack
1296− <|> do reserved "state"; return ProofState
1297− <|> do reserved "term"; return ProofTerm
1298− <|> do reserved "undo"; return Undo
1299− <|> do reserved "qed"; return Qed
1300− <|> do reserved "abandon"; return Abandon
1301− <|> do reserved "skip"; return Skip
1302− <|> do reserved "fail"
1303− msg <- stringLiteral
1304− return $ TFail [Idris.Core.TT.TextPart msg]
1305− <|> do reserved "sourceLocation"; return SourceFC
1306− <|> do lchar ':';
1307− ( (do reserved "q"; return Abandon)
1308− <|> (do (reserved "e" <|> reserved "eval");
1309− t <- (indentPropHolds gtProp *> expr syn);
1310− i <- get
1311− return $ TEval (desugar syn i t))
1312− <|> (do (reserved "t" <|> reserved "type");
1313− t <- (indentPropHolds gtProp *> expr syn);
1314− i <- get
1315− return $ TCheck (desugar syn i t))
1316− <|> try (do reserved "doc"
1317− whiteSpace
1318− c <- constant
1319− eof
1320− return (TDocStr (Right c)))
1321− <|> try (do reserved "doc"
1322− whiteSpace
1323− n <- fnName
1324− eof
1325− return (TDocStr (Left n)))
1326− <|> try (do reserved "search"
1327− whiteSpace
1328− t <- (indentPropHolds gtProp *> expr syn);
1329− i <- get
1330− return $ TSearch (desugar syn i t))
1331− <?> "prover command")
1333+ <|> ((lchar ':' >> empty) <?> "prover command")
13321334 <?> "tactic"
13331335 where
1334− imp :: IdrisParser Bool
1335− imp = do lchar '?'; return False
1336− <|> do lchar '_'; return True
13371336 mergeSeq :: [PTactic] -> PTactic
13381337 mergeSeq [t] = t
13391338 mergeSeq (t:ts) = TSeq t (mergeSeq ts)