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

git.iko.soy/Idris-dev

Add 'unify' tactic

Normally, we give every explicit argument to a function after 'refine', even if some may be solvable by unification. The 'unify' tactic goes back and fills in the unifiable ones. (I don't expect this to be useful *that* often but I have occasionally encountered such situations.)

commit51394aac23a216b0fa7f9a822f7a756212998c3f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 23 Apr 2014, 21:40 (13 years ago) parent601342f

7 files changed+19−2

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Completion.hs+1−1 src/Idris/Core/Elaborate.hs+4 src/Idris/Core/ProofState.hs+8 src/Idris/ElabTerm.hs+2 src/Idris/IBC.hs+2 src/Idris/ParseExpr.hs+1

src/Idris/AbsSyntaxTree.hs+1−1

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

710710

711711

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

713− | Refine Name [Bool] | Rewrite t

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

714714 | Induction Name

715715 | Equiv t

716716 | MatchRefine Name

src/Idris/Completion.hs+1−1

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

5151 , (":eval", Just ExprTArg)

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

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

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

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

5555 ]

5656tactics = map fst tacticArgs

5757

src/Idris/Core/Elaborate.hs+4

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

328328end_unify :: Elab' aux ()

329329end_unify = processTactic' EndUnify

330330

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+

331335regret :: Elab' aux ()

332336regret = processTactic' Regret

333337

src/Idris/Core/ProofState.hs+8

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

5959 | Solve

6060 | StartUnify Name

6161 | EndUnify

62+ | UnifyAll

6263 | Compute

6364 | ComputeLet Name

6465 | Simplify

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

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

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

783784

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

784786updateSolved xs x = updateSolved' xs x

785787updateSolved' [] x = x

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

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

874876 problems = probs',

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

876878 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) }, "")

877885processTactic (Reorder n) ps

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

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

src/Idris/ElabTerm.hs+2

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

995995 _ -> return []

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

997997 when autoSolve solveAll

998+ runT DoUnify = do unify_all

999+ when autoSolve solveAll

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

9991001 = do attack

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

src/Idris/IBC.hs+2

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

19431943 put x1

19441944 put x2

19451945 put x3

1946+ DoUnify -> putWord8 22

19461947 get

19471948 = do i <- getWord8

19481949 case i of

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

19881989 x2 <- get

19891990 x3 <- get

19901991 return (ProofSearch x1 x2 x3)

1992+ 22 -> return DoUnify

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

19921994

19931995

src/Idris/ParseExpr.hs+1

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

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

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

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