a3407cb · Idris-dev · git.iko.soy

src/IRTS/Compiler.hs+1−1

compare with master

unifiedsplit

@@ -120,7 +120,7 @@ compile codegen f mtm

120 where checkMVs = do i <- getIState

121 case map fst (idris_metavars i) \\ primDefs of

122 [] -> return ()

123− ms -> ifail $ "There are undefined metavariables: " ++ show ms

123+ ms -> ifail $ "There are undefined holes: " ++ show ms

124 checkTotality = do i <- getIState

125 case idris_totcheckfail i of

126 [] -> return ()

src/Idris/Help.hs+2−2

@@ -27,7 +27,7 @@ instance Show CmdArg where

27 show NumberArg = "<number>"

28 show NamespaceArg = "<namespace>"

29 show OptionArg = "<option>"

30− show MetaVarArg = "<metavar>"

30+ show MetaVarArg = "<hole>"

31 show ColourArg = "<option>"

32 show NoArg = ""

33 show SpecialHeaderArg = "Arguments"

@@ -46,5 +46,5 @@ extraHelp =

46 , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")

47 , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")

48 , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")

49− , ([":refine!", ":ref!"], NoArg, ":ref! <line> <name> <name'> destructively attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable")

49+ , ([":refine!", ":ref!"], NoArg, ":ref! <line> <name> <name'> destructively attempts to partially solve name on line, with name' as hint, introducing holes for arguments that aren't inferrable")

50 ]

src/Idris/Prover.hs+2−2

@@ -51,8 +51,8 @@ prover mode lit x =

51 case lookupTy x ctxt of

52 [t] -> if elem x (map fst (idris_metavars i))

53 then prove mode (idris_optimisation i) ctxt lit x t

54− else ifail $ show x ++ " is not a metavariable"

54+ else ifail $ show x ++ " is not a hole"

55− _ -> fail "No such metavariable"

55+ _ -> fail "No such hole"

56

57showProof :: Bool -> Name -> [String] -> String

58showProof lit n ps

src/Idris/REPL.hs+3−3

@@ -137,7 +137,7 @@ repl orig mods efile

137 act -- repl orig mods

138

139 showMVs c thm [] = ""

140− showMVs c thm ms = "Metavariables: " ++

140+ showMVs c thm ms = "Holes: " ++

141 show' 4 c thm (map fst ms) ++ "\n"

142

143 show' 0 c thm ms = let l = length ms in

@@ -1219,8 +1219,8 @@ process fn Metavars

1219 = do ist <- getIState

1220 let mvs = map fst (idris_metavars ist) \\ primDefs

1221 case mvs of

1222− [] -> iPrintError "No global metavariables to solve"

1222+ [] -> iPrintError "No global holes to solve"

1223− _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs

1223+ _ -> iPrintResult $ "Global holes:\n\t" ++ show mvs

1224process fn NOP = return ()

1225

1226process fn (SetOpt ErrContext) = setErrContext True

src/Idris/REPLParser.hs+1−1

@@ -63,7 +63,7 @@ parserCommandsForHelp =

63 , strArg ChangeDirectory)

64 , (["module"], ModuleArg, "Import an extra module", moduleArg ModImport) -- NOTE: dragons

65 , noArgCmd ["e", "edit"] Edit "Edit current file using $EDITOR or $VISUAL"

66− , noArgCmd ["m", "metavars"] Metavars "Show remaining proof obligations (metavariables)"

66+ , noArgCmd ["m", "metavars"] Metavars "Show remaining proof obligations (metavariables or holes)"

67 , (["p", "prove"], MetaVarArg, "Prove a metavariable"

68 , nameArg (Prove False))

69 , (["elab"], MetaVarArg, "Build a metavariable using the elaboration shell"