51394aa · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1−1

compare with master

unifiedsplit

@@ -710,7 +710,7 @@ mapPT f t = f (mpt t) where

710

711

712data PTactic' t = Intro [Name] | Intros | Focus Name

713− | Refine Name [Bool] | Rewrite t

713+ | Refine Name [Bool] | Rewrite t | DoUnify

714 | Induction Name

715 | Equiv t

716 | MatchRefine Name

src/Idris/Completion.hs+1−1

@@ -51,7 +51,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

51 , (":eval", Just ExprTArg)

52 ] ++ map (\x -> (x, Nothing)) [

53 "intros", "compute", "trivial", "search", "solve", "attack",

54− "state", "term", "undo", "qed", "abandon", ":q"

54+ "unify", "state", "term", "undo", "qed", "abandon", ":q"

55 ]

56tactics = map fst tacticArgs

57

src/Idris/Core/Elaborate.hs+4

@@ -328,6 +328,10 @@ start_unify n = processTactic' (StartUnify n)

328end_unify :: Elab' aux ()

329end_unify = processTactic' EndUnify

330

331+-- Clear the list of variables not to unify, and try to solve them

332+unify_all :: Elab' aux ()

333+unify_all = processTactic' UnifyAll

334+

331regret :: Elab' aux ()

335regret :: Elab' aux ()

332regret = processTactic' Regret

336regret = processTactic' Regret

333

337

src/Idris/Core/ProofState.hs+8

@@ -59,6 +59,7 @@ data Tactic = Attack

59 | Solve

60 | StartUnify Name

61 | EndUnify

62+ | UnifyAll

62 | Compute

63 | Compute

63 | ComputeLet Name

64 | ComputeLet Name

64 | Simplify

65 | Simplify

@@ -781,6 +782,7 @@ keepGiven du (u@(n, _) : us) hs

781 | n `elem` du = u : keepGiven du us hs

782 | n `elem` du = u : keepGiven du us hs

782keepGiven du (u : us) hs = keepGiven du us hs

783keepGiven du (u : us) hs = keepGiven du us hs

783

784

785+updateSolved :: [(Name, Term)] -> Term -> Term

784updateSolved xs x = updateSolved' xs x

786updateSolved xs x = updateSolved' xs x

785updateSolved' [] x = x

787updateSolved' [] x = x

786updateSolved' xs (Bind n (Hole ty) t)

788updateSolved' xs (Bind n (Hole ty) t)

@@ -874,6 +876,12 @@ processTactic EndUnify ps

874 problems = probs',

876 problems = probs',

875 notunified = updateNotunified ns'' (notunified ps),

877 notunified = updateNotunified ns'' (notunified ps),

876 holes = holes ps \\ map fst ns'' }, "")

878 holes = holes ps \\ map fst ns'' }, "")

879+processTactic UnifyAll ps

880+ = trace (show (notunified ps)) $

881+ let tm' = updateSolved (notunified ps) (pterm ps) in

882+ return (ps { pterm = tm',

883+ notunified = [],

884+ holes = holes ps \\ map fst (notunified ps) }, "")

877processTactic (Reorder n) ps

885processTactic (Reorder n) ps

878 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

886 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

879 return (ps' { previous = Just ps, plog = "" }, plog ps')

887 return (ps' { previous = Just ps, plog = "" }, plog ps')

src/Idris/ElabTerm.hs+2

@@ -995,6 +995,8 @@ runTac autoSolve ist fn tac

995 _ -> return []

996 runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)

997 when autoSolve solveAll

998+ runT DoUnify = do unify_all

999+ when autoSolve solveAll

998 runT (Equiv tm) -- let bind tm, then

1000 runT (Equiv tm) -- let bind tm, then

999 = do attack

1001 = do attack

1000 tyn <- getNameFrom (sMN 0 "ety")

1002 tyn <- getNameFrom (sMN 0 "ety")

src/Idris/IBC.hs+2

@@ -1943,6 +1943,7 @@ instance (Binary t) => Binary (PTactic' t) where

1943 put x1

1944 put x2

1945 put x3

1946+ DoUnify -> putWord8 22

1946 get

1947 get

1947 = do i <- getWord8

1948 = do i <- getWord8

1948 case i of

1949 case i of

@@ -1988,6 +1989,7 @@ instance (Binary t) => Binary (PTactic' t) where

1988 x2 <- get

1989 x2 <- get

1989 x3 <- get

1990 x3 <- get

1990 return (ProofSearch x1 x2 x3)

1991 return (ProofSearch x1 x2 x3)

1992+ 22 -> return DoUnify

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

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

1992

1994

1993

1995

src/Idris/ParseExpr.hs+1

@@ -1180,6 +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 "unify"; return DoUnify

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

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

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

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

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

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