a3407cb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Display 'Hole' instead of 'Metavariable'

commita3407cb11cdee55007be5eedfe72f06c0437285f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 23 Jun 2015, 11:21 (11 years ago) parent0b68452

5 files changed+9−9

compare with master

unifiedsplit

src/IRTS/Compiler.hs+1−1 src/Idris/Help.hs+2−2 src/Idris/Prover.hs+2−2 src/Idris/REPL.hs+3−3 src/Idris/REPLParser.hs+1−1

src/IRTS/Compiler.hs+1−1

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

120120 where checkMVs = do i <- getIState

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

122122 [] -> return ()

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

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

124124 checkTotality = do i <- getIState

125125 case idris_totcheckfail i of

126126 [] -> return ()

src/Idris/Help.hs+2−2

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

2727 show NumberArg = "<number>"

2828 show NamespaceArg = "<namespace>"

2929 show OptionArg = "<option>"

30− show MetaVarArg = "<metavar>"

30+ show MetaVarArg = "<hole>"

3131 show ColourArg = "<option>"

3232 show NoArg = ""

3333 show SpecialHeaderArg = "Arguments"

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

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

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

4848 , ([":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")

5050 ]

src/Idris/Prover.hs+2−2

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

5151 case lookupTy x ctxt of

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

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

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

55− _ -> fail "No such metavariable"

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

55+ _ -> fail "No such hole"

5656

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

5858showProof lit n ps

src/Idris/REPL.hs+3−3

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

137137 act -- repl orig mods

138138

139139 showMVs c thm [] = ""

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

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

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

142142

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

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

12191219 = do ist <- getIState

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

12211221 case mvs of

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

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

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

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

12241224process fn NOP = return ()

12251225

12261226process fn (SetOpt ErrContext) = setErrContext True

src/Idris/REPLParser.hs+1−1

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

6363 , strArg ChangeDirectory)

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

6565 , 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)"

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

6868 , nameArg (Prove False))

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