acb1f19 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add :a comment, to add most recent proof script to source file

acb1f19Edwin Brady15 years ago

lib/nat.idr+2−3

compare with master

unifiedsplit

@@ -1,6 +1,6 @@

1−import builtins;

1+module nat;

3−namespace nat {

3+import builtins;

5data Nat = O | S Nat;

@@ -66,4 +66,3 @@ plus_commutes_Sk = proof {

66 refine plusn_Sm;

67};

69−}

src/Idris/AbsSyntax.hs+3−2

@@ -45,11 +45,12 @@ data IState = IState { tt_ctxt :: Context,

45 idris_objs :: [FilePath],

46 idris_libs :: [String],

47 idris_hdrs :: [String],

48+ last_proof :: Maybe (Name, [String]),

48 errLine :: Maybe Int

49 errLine :: Maybe Int

49 }

50 }

51idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

52idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

52− "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing

53+ "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing

54-- The monad for the main REPL - reading and processing files and updating

55-- The monad for the main REPL - reading and processing files and updating

55-- global state (hence the IO inner monad).

56-- global state (hence the IO inner monad).

@@ -186,7 +187,7 @@ setTypeCase t = do i <- get

186

187

188 | Compile String | Execute String

189 | Compile String | Execute String

189− | Metavars | Prove Name | Universes

190+ | Metavars | Prove Name | AddProof | Universes

190 | TTShell

191 | TTShell

191 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

192 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

192 | NOP

193 | NOP

src/Idris/Prover.hs+7−5

@@ -25,17 +25,19 @@ prover x = do ctxt <- getContext

25 else fail $ show x ++ " is not a metavariable"

26 _ -> fail "No such metavariable"

28−dumpProof :: Name -> [String] -> IO ()

28+showProof :: Name -> [String] -> String

29−dumpProof n ps = do putStrLn $ show n ++ " = proof {"

29+showProof n ps = show n ++ " = proof {" ++ "\n" ++

30− mapM_ (\x -> putStrLn $ " " ++ x ++ ";") ps

30+ showSep "\n" (map (\x -> " " ++ x ++ ";") ps) ++

31− putStrLn "};\n"

31+ "\n};\n"

33prove :: Context -> Name -> Type -> Idris ()

34prove ctxt n ty

35 = do let ps = initElaborator n ctxt ty

36 (tm, prf) <- ploop True ("-" ++ show n) [] (ES ps "" Nothing)

37 iLOG $ "Adding " ++ show tm

38− lift $ dumpProof n prf

38+ iputStrLn $ showProof n prf

39+ i <- get

40+ put (i { last_proof = Just (n, prf) })

39 let tree = simpleCase False [(P Ref n ty, tm)]

41 let tree = simpleCase False [(P Ref n ty, tm)]

40 logLvl 3 (show tree)

42 logLvl 3 (show tree)

41 (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm

43 (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm

src/Idris/REPL.hs+28−3

@@ -22,6 +22,7 @@ import System.Console.Readline

22import System.FilePath

23import System.Environment

24import System.Process

25+import System.Directory

25import Control.Monad

26import Control.Monad

26import Control.Monad.State

27import Control.Monad.State

27import Data.List

28import Data.List

@@ -60,6 +61,9 @@ processInput cmd orig inputs

60 return (Just inputs)

61 return (Just inputs)

61 Right Edit -> do edit fn orig

62 Right Edit -> do edit fn orig

62 return (Just inputs)

63 return (Just inputs)

64+ Right AddProof -> do idrisCatch (addProof fn orig)

65+ (\e -> iputStrLn (report e))

66+ return (Just inputs)

63 Right Quit -> do iputStrLn "Bye bye"

67 Right Quit -> do iputStrLn "Bye bye"

64 return Nothing

68 return Nothing

65 Right cmd -> do idrisCatch (process cmd)

69 Right cmd -> do idrisCatch (process cmd)

@@ -85,6 +89,26 @@ edit f orig

85 | Just ed <- lookup "VISUAL" env = ed

89 | Just ed <- lookup "VISUAL" env = ed

86 | otherwise = "vi"

90 | otherwise = "vi"

92+addProof :: FilePath -> IState -> Idris ()

93+addProof "" orig = iputStrLn "Nothing to add to"

94+addProof f orig

95+ = do let fb = f ++ "~"

96+ lift $ copyFile f fb -- make a backup in case something goes wrong!

97+ prog <- lift $ readFile fb

98+ i <- get

99+ case last_proof i of

100+ Nothing -> iputStrLn "No proof to add"

101+ Just (n, p) -> do let prog' = insertScript (showProof n p) (lines prog)

102+ lift $ writeFile f (unlines prog')

103+ iputStrLn $ "Added proof " ++ show n

104+ -- lift $ removeFile fb -- uncomment when less scared :)

105+

106+insertScript :: String -> [String] -> [String]

107+insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]

108+insertScript prf (p@"---------- Proofs ----------" : "" : xs)

109+ = p : "" : prf : xs

110+insertScript prf (x : xs) = x : insertScript prf xs

111+

88process :: Command -> Idris ()

112process :: Command -> Idris ()

89process Help = iputStrLn displayHelp

113process Help = iputStrLn displayHelp

90process (Eval t) = do (tm, ty) <- elabVal toplevel False t

114process (Eval t) = do (tm, ty) <- elabVal toplevel False t

@@ -149,7 +173,7 @@ displayHelp = let vstr = showVersion version in

149 "\nIdris version " ++ vstr ++ "\n" ++

173 "\nIdris version " ++ vstr ++ "\n" ++

150 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

174 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

151 concatMap cmdInfo help

175 concatMap cmdInfo help

152− where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) args text

176+ where cmdInfo (cmds, args, text) = " " ++ col 16 10 (showSep " " cmds) args text

153 col c1 c2 l m r =

177 col c1 c2 l m r =

154 l ++ take (c1 - length l) (repeat ' ') ++

178 l ++ take (c1 - length l) (repeat ' ') ++

155 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

179 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

@@ -157,12 +181,13 @@ displayHelp = let vstr = showVersion version in

157help =

181help =

158 [ (["Command"], "Arguments", "Purpose"),

182 [ (["Command"], "Arguments", "Purpose"),

159 ([""], "", ""),

183 ([""], "", ""),

160− (["<expression>"], "", "Evaluate an expression"),

184+ (["<expr>"], "", "Evaluate an expression"),

161− ([":t"], "<expression>", "Check the type of an expression"),

185+ ([":t"], "<expr>", "Check the type of an expression"),

162 ([":r",":reload"], "", "Reload current file"),

186 ([":r",":reload"], "", "Reload current file"),

163 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),

187 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),

164 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),

188 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),

165 ([":p",":prove"], "<name>", "Prove a metavariable"),

189 ([":p",":prove"], "<name>", "Prove a metavariable"),

190+ ([":a",":addproof"], "", "Add last proof to source file"),

166 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

191 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

167 ([":exec",":execute"], "<filename>", "Compile to an executable <filename> and run"),

192 ([":exec",":execute"], "<filename>", "Compile to an executable <filename> and run"),

168 ([":?",":h",":help"], "", "Display this help text"),

193 ([":?",":h",":help"], "", "Display this help text"),

src/Idris/REPLParser.hs+1

@@ -29,6 +29,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

29 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))

30 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

31 <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))

32+ <|> try (do cmd ["a", "addproof"]; eof; return AddProof)

32 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

33 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

33 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

34 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

34 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

35 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))