acb1f19 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitacb1f197fa3de3c5e934c0376a6e81f749d9b83a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 29 Nov 2011, 14:04 (15 years ago) parent57c8ed3

5 files changed+41−13

compare with master

unifiedsplit

lib/nat.idr+2−3 src/Idris/AbsSyntax.hs+3−2 src/Idris/Prover.hs+7−5 src/Idris/REPL.hs+28−3 src/Idris/REPLParser.hs+1

lib/nat.idr+2−3

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

1−import builtins;

1+module nat;

3−namespace nat {

3+import builtins;

55data Nat = O | S Nat;

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

6666 refine plusn_Sm;

6767};

6868

69−}

src/Idris/AbsSyntax.hs+3−2

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

4545 idris_objs :: [FilePath],

4646 idris_libs :: [String],

4747 idris_hdrs :: [String],

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

4849 errLine :: Maybe Int

4950 }

5051

5152idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

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

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

5354

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

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

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

186187

188189 | Compile String | Execute String

189− | Metavars | Prove Name | Universes

190+ | Metavars | Prove Name | AddProof | Universes

190191 | TTShell

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

192193 | NOP

src/Idris/Prover.hs+7−5

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

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

2626 _ -> fail "No such metavariable"

2727

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

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

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

31− putStrLn "};\n"

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

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

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

31+ "\n};\n"

3232

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

3434prove ctxt n ty

3535 = do let ps = initElaborator n ctxt ty

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

3737 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) })

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

4042 logLvl 3 (show tree)

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

src/Idris/REPL.hs+28−3

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

2222import System.FilePath

2323import System.Environment

2424import System.Process

25+import System.Directory

2526import Control.Monad

2627import Control.Monad.State

2728import Data.List

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

6061 return (Just inputs)

6162 Right Edit -> do edit fn orig

6263 return (Just inputs)

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

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

66+ return (Just inputs)

6367 Right Quit -> do iputStrLn "Bye bye"

6468 return Nothing

6569 Right cmd -> do idrisCatch (process cmd)

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

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

8690 | otherwise = "vi"

8791

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+

88112process :: Command -> Idris ()

89113process Help = iputStrLn displayHelp

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

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

149173 "\nIdris version " ++ vstr ++ "\n" ++

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

151175 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

153177 col c1 c2 l m r =

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

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

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

157181help =

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

159183 ([""], "", ""),

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

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

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

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

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

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

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

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

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

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

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

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

src/Idris/REPLParser.hs+1

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

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

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

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

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

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

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

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