e07c13d · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

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

324 test/interactive003/input

325 test/interactive003/*.idr

326 test/interactive003/expected

327+ test/interactive004/run

328+ test/interactive004/input

329+ test/interactive004/*.idr

330+ test/interactive004/expected

327

331

328 test/io001/run

332 test/io001/run

329 test/io001/*.idr

333 test/io001/*.idr

src/Idris/AbsSyntaxTree.hs+5−2

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

297 | AddProofClauseFrom Bool Int Name

298 | AddMissing Bool Int Name

299 | 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]

301 | SetOpt Opt

303 | SetOpt Opt

302 | UnsetOpt Opt

304 | UnsetOpt Opt

303 | NOP

305 | NOP

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

710 | MatchRefine Name

712 | MatchRefine Name

711 | LetTac Name t | LetTacTy Name t t

713 | LetTac Name t | LetTacTy Name t t

712 | Exact t | Compute | Trivial | TCInstance

714 | Exact t | Compute | Trivial | TCInstance

715+ | ProofSearch Bool -- ^ recursive

713− | ProofSearch (Maybe Name) [Name]

716+ (Maybe Name) [Name]

714 | Solve

717 | Solve

715 | Attack

718 | Attack

716 | ProofState | ProofTerm | Undo

719 | ProofState | ProofTerm | Undo

src/Idris/DeepSeq.hs+1−1

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

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

246 rnf Compute = ()

247 rnf Trivial = ()

248− rnf (ProofSearch x1 x2)

248+ rnf (ProofSearch r x1 x2)

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

250 rnf Solve = ()

251 rnf Attack = ()

src/Idris/ElabTerm.hs+4−4

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

820

821trivial' ist

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

823−proofSearch' ist top n hints

823+proofSearch' ist rec top n hints

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

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

825

826

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

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

1050 runT Compute = compute

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

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

1053− runT (ProofSearch top hints)

1053+ runT (ProofSearch rec top hints)

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

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

1055 runT (Focus n) = focus n

1056 runT Solve = solve

1057 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

1939 put x1

1940 ByReflection x1 -> do putWord8 20

1941 put x1

1942+ ProofSearch x1 x2 x3 -> do putWord8 21

1943+ put x1

1944+ put x2

1945+ put x3

1942 get

1946 get

1943 = do i <- getWord8

1947 = do i <- getWord8

1944 case i of

1948 case i of

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

1980 return (Induction x1)

1984 return (Induction x1)

1981 20 -> do x1 <- get

1985 20 -> do x1 <- get

1982 return (ByReflection x1)

1986 return (ByReflection x1)

1987+ 21 -> do x1 <- get

1988+ x2 <- get

1989+ x3 <- get

1990+ return (ProofSearch x1 x2 x3)

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

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

1984

1992

1985

1993

src/Idris/IdeSlave.hs+5−2

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

145 | AddProofClause Int String

146 | AddMissing Int String

147 | MakeWithBlock Int String

148− | ProofSearch Int String [String]

148+ | ProofSearch Bool Int String [String]

149 | LoadFile String

150 | DocsFor String

151 | Apropos String

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

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

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

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

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.

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

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

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

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

171 StringAtom s -> Just s

174 StringAtom s -> Just s

172 _ -> Nothing)

175 _ -> Nothing)

src/Idris/ParseExpr.hs+1−1

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

1180 return $ TSeq t (mergeSeq ts)

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

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

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

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

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

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

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

src/Idris/ProofSearch.hs+43−10

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

14

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

16import Control.Monad

17+import Data.List

17import Debug.Trace

18import Debug.Trace

18

19

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

20-- 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)

36 (tryAll xs) True

37 (tryAll xs) True

37 else tryAll xs

38 else tryAll xs

38

39

40+proofSearch :: Bool ->

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

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

40 IState -> ElabD ()

42 IState -> ElabD ()

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

41−proofSearch elab fn nroot hints ist

71+proofSearch rec elab fn nroot hints ist

42 = case lookupCtxt nroot (idris_tyinfodata ist) of

72 = case lookupCtxt nroot (idris_tyinfodata ist) of

43 [TISolution ts] -> findInferredTy ts

73 [TISolution ts] -> findInferredTy ts

44− _ -> psRec maxDepth

74+ _ -> psRec rec maxDepth

45 where

75 where

46 maxDepth = 6

76 maxDepth = 6

47

77

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

53 toUN (App f a) = App (toUN f) (toUN a)

83 toUN (App f a) = App (toUN f) (toUN a)

54 toUN t = t

84 toUN t = t

55

85

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

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

87+ psRec False d = tryCons d hints

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

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

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

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

59− True)

90+ True)

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

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

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

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

62

93

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

91

122

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

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

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

124 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"

95

126

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

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

97 tryCon d n =

128 tryCon d n =

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

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

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

101 _ -> fail "Ambiguous name"

132 _ -> fail "Ambiguous name"

102 ps <- get_probs

133 ps <- get_probs

134+ hs <- get_holes

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

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

104 (match_apply (Var n) imps) True

136 (match_apply (Var n) imps) True

105 ps' <- get_probs

137 ps' <- get_probs

138+ hs' <- get_holes

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

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

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

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

108− psRec d)

141+ psRec True d)

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

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

110 solve

143 solve

111

144

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

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

113− isImp arg = (False, priority arg)

146+ isImp arg = (False, priority arg)

114

147

src/Idris/REPL.hs+6−6

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

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

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

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

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

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

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

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

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

292 process stdout fn (Apropos a)

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

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

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

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

427ideslaveProcess 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)

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

430 iPrintResult ""

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

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

809 else ihPrintResult h with

810 where getIndent s = length (takeWhile isSpace s)

811

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

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

813 = do src <- runIO $ readFile fn

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

815 ctxt <- getContext

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

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

823 _ -> (Nothing, 0, True)

824 let fc = fileFC fn

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

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

826− (ProofSearch t hints)]

826+ (ProofSearch rec t hints)]

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

828 newmv <- idrisCatch

829 (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)

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

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

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

90− hints <- many P.name

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

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

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

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

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

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

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

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

99 <|> 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

3+

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

7+

test/interactive004/runnew file+3

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

1+#!/usr/bin/env bash

2+idris --quiet interactive004.idr < input

3+rm -f *.ibc