e07c13d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add :refine (:ref) command for refining a hole

Like :ps, but instead of a recursive search, it simply applies the function given and fills in other arguments *by unification only*. (In particular, this means it will fail if any implicit arguments need other arguments, rather than the return type, in order to be solved by unification). So, this will work: append : (n, m : Nat) -> Vect n a -> Vect m a -> Vect (n + m) a append Z m [] ys = ys append (S k) m (x :: xs) ys = x :: ?append_rhs1 *testref> :ref 6 append_rhs1 append append k m ?append_rhs2 ?append_rhs3 But this will not: vZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c vZipWith f [] [] = [] vZipWith f (x :: xs) (y :: ys) = f x y :: ?vZipWith_rhs1 *Vect> :ref 18 vZipWith_rhs1 vZipWith ?vZipWith_rhs1 ...because unification alone is not enough to work out the implicit arguments a and b (even if there is only one thing that will work, it needs a deeper proof search to find it).

commite07c13d42d64e202c0fd20cbbc1b7d22c041a0fc authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 17 Apr 2014, 15:41 (13 years ago) parent3d50580

14 files changed+99−28

compare with master

unifiedsplit

idris.cabal+4 src/Idris/AbsSyntaxTree.hs+5−2 src/Idris/DeepSeq.hs+1−1 src/Idris/ElabTerm.hs+4−4 src/Idris/IBC.hs+8 src/Idris/IdeSlave.hs+5−2 src/Idris/ParseExpr.hs+1−1 src/Idris/ProofSearch.hs+43−10 src/Idris/REPL.hs+6−6 src/Idris/REPLParser.hs+7−2 test/interactive004/expected+3 test/interactive004/input+2 test/interactive004/interactive004.idr+7 test/interactive004/run+3

idris.cabal+4

@@ -324,6 +324,10 @@ Extra-source-files:

324324 test/interactive003/input

325325 test/interactive003/*.idr

326326 test/interactive003/expected

327+ test/interactive004/run

328+ test/interactive004/input

329+ test/interactive004/*.idr

330+ test/interactive004/expected

327331

328332 test/io001/run

329333 test/io001/*.idr

src/Idris/AbsSyntaxTree.hs+5−2

@@ -297,7 +297,9 @@ data Command = Quit

297297 | AddProofClauseFrom Bool Int Name

298298 | AddMissing Bool Int Name

299299 | MakeWith Bool Int Name

300− | DoProofSearch Bool Int Name [Name]

300+ | DoProofSearch Bool -- ^ update

301+ Bool -- ^ recursive (i.e. do arguments too)

302+ Int Name [Name]

301303 | SetOpt Opt

302304 | UnsetOpt Opt

303305 | NOP

@@ -710,7 +712,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

710712 | MatchRefine Name

711713 | LetTac Name t | LetTacTy Name t t

712714 | Exact t | Compute | Trivial | TCInstance

713− | ProofSearch (Maybe Name) [Name]

715+ | ProofSearch Bool -- ^ recursive

716+ (Maybe Name) [Name]

714717 | Solve

715718 | Attack

716719 | ProofState | ProofTerm | Undo

src/Idris/DeepSeq.hs+1−1

@@ -245,7 +245,7 @@ instance (NFData t) => NFData (PTactic' t) where

245245 rnf (Exact x1) = rnf x1 `seq` ()

246246 rnf Compute = ()

247247 rnf Trivial = ()

248− rnf (ProofSearch x1 x2)

248+ rnf (ProofSearch r x1 x2)

249249 = rnf x1 `seq` rnf x2 `seq` ()

250250 rnf Solve = ()

251251 rnf Attack = ()

src/Idris/ElabTerm.hs+4−4

@@ -820,8 +820,8 @@ findInstances ist t

820820

821821trivial' ist

822822 = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

823−proofSearch' ist top n hints

824− = proofSearch (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

823+proofSearch' ist rec top n hints

824+ = proofSearch rec (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

825825

826826

827827resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

@@ -1050,8 +1050,8 @@ runTac autoSolve ist fn tac

10501050 runT Compute = compute

10511051 runT Trivial = do trivial' ist; when autoSolve solveAll

10521052 runT TCInstance = runT (Exact (PResolveTC emptyFC))

1053− runT (ProofSearch top hints)

1054− = do proofSearch' ist top fn hints; when autoSolve solveAll

1053+ runT (ProofSearch rec top hints)

1054+ = do proofSearch' ist rec top fn hints; when autoSolve solveAll

10551055 runT (Focus n) = focus n

10561056 runT Solve = solve

10571057 runT (Try l r) = do try' (runT l) (runT r) True

src/Idris/IBC.hs+8

@@ -1939,6 +1939,10 @@ instance (Binary t) => Binary (PTactic' t) where

19391939 put x1

19401940 ByReflection x1 -> do putWord8 20

19411941 put x1

1942+ ProofSearch x1 x2 x3 -> do putWord8 21

1943+ put x1

1944+ put x2

1945+ put x3

19421946 get

19431947 = do i <- getWord8

19441948 case i of

@@ -1980,6 +1984,10 @@ instance (Binary t) => Binary (PTactic' t) where

19801984 return (Induction x1)

19811985 20 -> do x1 <- get

19821986 return (ByReflection x1)

1987+ 21 -> do x1 <- get

1988+ x2 <- get

1989+ x3 <- get

1990+ return (ProofSearch x1 x2 x3)

19831991 _ -> error "Corrupted binary data for PTactic'"

19841992

19851993

src/Idris/IdeSlave.hs+5−2

@@ -145,7 +145,7 @@ data IdeSlaveCommand = REPLCompletions String

145145 | AddProofClause Int String

146146 | AddMissing Int String

147147 | MakeWithBlock Int String

148− | ProofSearch Int String [String]

148+ | ProofSearch Bool Int String [String]

149149 | LoadFile String

150150 | DocsFor String

151151 | Apropos String

@@ -166,7 +166,10 @@ sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n

166166sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

167167sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

168168sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)

169−sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch (fromInteger line) name hints)

169+-- XXX: The Boolean in ProofSearch means "search recursively"

170+-- If it's False, that means "refine", i.e. apply the name and fill in any

171+-- arguments which can be done by unification.

172+sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints)

170173 where getHints = mapM (\h -> case h of

171174 StringAtom s -> Just s

172175 _ -> Nothing)

src/Idris/ParseExpr.hs+1−1

@@ -1180,7 +1180,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

11801180 return $ TSeq t (mergeSeq ts)

11811181 <|> do reserved "compute"; return Compute

11821182 <|> do reserved "trivial"; return Trivial

1183− <|> do reserved "search"; return (ProofSearch Nothing [])

1183+ <|> do reserved "search"; return (ProofSearch True Nothing [])

11841184 <|> do reserved "instance"; return TCInstance

11851185 <|> do reserved "solve"; return Solve

11861186 <|> do reserved "attack"; return Attack

src/Idris/ProofSearch.hs+43−10

@@ -14,6 +14,7 @@ import Idris.Error

1414

1515import Control.Applicative ((<$>))

1616import Control.Monad

17+import Data.List

1718import Debug.Trace

1819

1920-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

@@ -36,12 +37,41 @@ trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

3637 (tryAll xs) True

3738 else tryAll xs

3839

39−proofSearch :: (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

40+proofSearch :: Bool ->

41+ (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

4042 IState -> ElabD ()

41−proofSearch elab fn nroot hints ist

43+proofSearch False elab _ nroot [fn] ist

44+ = do -- get all possible versions of the name, take the first one that

45+ -- works

46+ let all_imps = lookupCtxtName fn (idris_implicits ist)

47+ tryAllFns all_imps

48+ where

49+ -- if nothing worked, make a new metavariable

50+ tryAllFns [] = do attack; defer nroot; solve

51+ tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True

52+

53+ tryFn (f, args) = do let imps = map isImp args

54+ ps <- get_probs

55+ hs <- get_holes

56+ args <- map snd <$> try' (apply (Var f) imps)

57+ (match_apply (Var f) imps) True

58+ ps' <- get_probs

59+-- when (length ps < length ps') $ fail "Can't apply constructor"

60+ -- Make metavariables for new holes

61+ hs' <- get_holes

62+ ptm <- get_term

63+ mapM_ (\ h -> do focus h

64+ attack; defer nroot; solve)

65+ (hs' \\ hs)

66+-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))

67+ solve

68+

69+ isImp (PImp p _ _ _ _) = (True, p)

70+ isImp arg = (True, priority arg) -- try to get all of them by unification

71+proofSearch rec elab fn nroot hints ist

4272 = case lookupCtxt nroot (idris_tyinfodata ist) of

4373 [TISolution ts] -> findInferredTy ts

44− _ -> psRec maxDepth

74+ _ -> psRec rec maxDepth

4575 where

4676 maxDepth = 6

4777

@@ -53,10 +83,11 @@ proofSearch elab fn nroot hints ist

5383 toUN (App f a) = App (toUN f) (toUN a)

5484 toUN t = t

5585

56− psRec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"

57− psRec d = try' (trivial elab ist)

58− (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

59− True)

86+ psRec rec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"

87+ psRec False d = tryCons d hints

88+ psRec True d = try' (trivial elab ist)

89+ (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

90+ True)

6091 -- if all else fails, make a new metavariable

6192 (do attack; defer nroot; solve) True) True

6293

@@ -91,7 +122,7 @@ proofSearch elab fn nroot hints ist

91122

92123 tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)

93124 tryLocalArg d n i = simple_app (tryLocalArg d n (i - 1))

94− (psRec d) "proof search local apply"

125+ (psRec True d) "proof search local apply"

95126

96127 -- Like type class resolution, but searching with constructors

97128 tryCon d n =

@@ -100,15 +131,17 @@ proofSearch elab fn nroot hints ist

100131 [args] -> map isImp (snd args)

101132 _ -> fail "Ambiguous name"

102133 ps <- get_probs

134+ hs <- get_holes

103135 args <- map snd <$> try' (apply (Var n) imps)

104136 (match_apply (Var n) imps) True

105137 ps' <- get_probs

138+ hs' <- get_holes

106139 when (length ps < length ps') $ fail "Can't apply constructor"

107140 mapM_ (\ (_, h) -> do focus h

108− psRec d)

141+ psRec True d)

109142 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

110143 solve

111144

112145 isImp (PImp p _ _ _ _) = (True, p)

113− isImp arg = (False, priority arg)

146+ isImp arg = (False, priority arg)

114147

src/Idris/REPL.hs+6−6

@@ -286,8 +286,8 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =

286286 process stdout fn (AddMissing False line (sUN name))

287287runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

288288 process stdout fn (MakeWith False line (sUN name))

289−runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch line name hints) =

290− process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

289+runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints) =

290+ process stdout fn (DoProofSearch False r line (sUN name) (map sUN hints))

291291runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =

292292 process stdout fn (Apropos a)

293293runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

@@ -425,7 +425,7 @@ ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddPr

425425ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)

426426ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)

427427ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)

428−ideslaveProcess fn (DoProofSearch False pos str xs) = process stdout fn (DoProofSearch False pos str xs)

428+ideslaveProcess fn (DoProofSearch False r pos str xs) = process stdout fn (DoProofSearch False r pos str xs)

429429ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)

430430 iPrintResult ""

431431ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)

@@ -809,7 +809,7 @@ process h fn (MakeWith updatefile l n)

809809 else ihPrintResult h with

810810 where getIndent s = length (takeWhile isSpace s)

811811

812−process h fn (DoProofSearch updatefile l n hints)

812+process h fn (DoProofSearch updatefile rec l n hints)

813813 = do src <- runIO $ readFile fn

814814 let (before, tyline : later) = splitAt (l-1) (lines src)

815815 ctxt <- getContext

@@ -822,8 +822,8 @@ process h fn (DoProofSearch updatefile l n hints)

822822 Just (t, e, False) -> (t, e, False)

823823 _ -> (Nothing, 0, True)

824824 let fc = fileFC fn

825− let body t = PProof [Try (TSeq Intros (ProofSearch t hints))

826− (ProofSearch t hints)]

825+ let body t = PProof [Try (TSeq Intros (ProofSearch rec t hints))

826+ (ProofSearch rec t hints)]

827827 let def = PClause fc mn (PRef fc mn) [] (body top) []

828828 newmv <- idrisCatch

829829 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

src/Idris/REPLParser.hs+7−2

@@ -87,8 +87,13 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

8787 <|> try (do cmd ["ps", "proofsearch"]; P.whiteSpace;

8888 upd <- option False (do P.lchar '!'; return True)

8989 l <- P.natural; n <- P.name;

90− hints <- many P.name

91− return (DoProofSearch upd (fromInteger l) n hints))

90+ hints <- many P.fnName

91+ return (DoProofSearch upd True (fromInteger l) n hints))

92+ <|> try (do cmd ["ref", "refine"]; P.whiteSpace;

93+ upd <- option False (do P.lchar '!'; return True)

94+ l <- P.natural; n <- P.name;

95+ hint <- P.fnName

96+ return (DoProofSearch upd False (fromInteger l) n [hint]))

9297 <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))

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

9499 <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

test/interactive004/expectednew file+3

@@ -0,0 +1,3 @@

1+Type checking ./interactive004.idr

2+plus ?foo_rhs2 ?foo_rhs3

3+append k m ?append_rhs2 ?append_rhs3

test/interactive004/inputnew file+2

@@ -0,0 +1,2 @@

1+:ref 2 foo_rhs1 plus

2+:ref 6 append_rhs1 append

test/interactive004/interactive004.idrnew file+7

@@ -0,0 +1,7 @@

1+foo : Nat -> Nat -> Nat

2+foo k j = ?foo_rhs1

4+append : (n : Nat) -> (m : Nat) -> Vect n a -> Vect m a -> Vect (n + m) a

5+append Z m [] ys = ys

6+append (S k) m (x :: xs) ys = x :: ?append_rhs1

test/interactive004/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --quiet interactive004.idr < input

3+rm -f *.ibc