c7fded1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added 'mrefine' tactic

Like refine, but uses matching instead of unification to resolve implicit arguments. All will become clear, I hope :). This is intended for an additional style of pattern matching (on types) for better explanation of proofs.

commitc7fded1e95e10cf67f78c677ea297d49970f4268 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 27 Jun 2013, 00:06 (13 years ago) parent357e6b1

7 files changed+160−32

compare with master

unifiedsplit

src/Core/Elaborate.hs+10−3 src/Core/ProofState.hs+29−1 src/Core/Unify.hs+85−27 src/Idris/AbsSyntaxTree.hs+2 src/Idris/Completion.hs+1 src/Idris/ElabTerm.hs+12 src/Idris/Parser.hs+21−1

src/Core/Elaborate.hs+10−3

@@ -235,6 +235,9 @@ exact t = processTactic' (Exact t)

235235fill :: Raw -> Elab' aux ()

236236fill t = processTactic' (Fill t)

237237

238+match_fill :: Raw -> Elab' aux ()

239+match_fill t = processTactic' (MatchFill t)

240+

238241prep_fill :: Name -> [Name] -> Elab' aux ()

239242prep_fill n ns = processTactic' (PrepFill n ns)

240243

@@ -375,10 +378,14 @@ prepare_apply fn imps =

375378 rebind hs (App f a) = App (rebind hs f) (rebind hs a)

376379 rebind hs t = t

377380

378−apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

379−apply fn imps =

381+apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

382+apply = apply' fill

383+match_apply = apply' match_fill

384+

385+apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [Name]

386+apply' fillt fn imps =

380387 do args <- prepare_apply fn (map fst imps)

381− fill (raw_apply fn (map Var args))

388+ fillt (raw_apply fn (map Var args))

382389 -- _Don't_ solve the arguments we're specifying by hand.

383390 -- (remove from unified list before calling end_unify)

384391 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

src/Core/ProofState.hs+29−1

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

4949 | Reorder Name

5050 | Exact Raw

5151 | Fill Raw

52+ | MatchFill Raw

5253 | PrepFill Name [Name]

5354 | CompleteFill

5455 | Regret

@@ -154,7 +155,18 @@ holeName i = MN i "hole"

154155qshow :: Fails -> String

155156qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)

156157

157−unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]

158+match_unify' :: Context -> Env -> TT Name -> TT Name ->

159+ StateT TState TC [(Name, TT Name)]

160+match_unify' ctxt env topx topy =

161+ do ps <- get

162+ let dont = dontunify ps

163+ u <- lift $ match_unify ctxt env topx topy dont (holes ps)

164+ let (h, ns) = unified ps

165+ put (ps { unified = (h, u ++ ns) })

166+ return u

167+

168+unify' :: Context -> Env -> TT Name -> TT Name ->

169+ StateT TState TC [(Name, TT Name)]

158170unify' ctxt env topx topy =

159171 do ps <- get

160172 let dont = dontunify ps

@@ -372,6 +384,21 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

372384 return $ Bind x (Guess ty val) sc

373385fill _ _ _ _ = fail "Can't fill here."

374386

387+-- As fill, but attempts to solve other goals by matching

388+

389+match_fill :: Raw -> RunTactic

390+match_fill guess ctxt env (Bind x (Hole ty) sc) =

391+ do (val, valty) <- lift $ check ctxt env guess

392+-- let valtyn = normalise ctxt env valty

393+-- let tyn = normalise ctxt env ty

394+ ns <- match_unify' ctxt env valty ty

395+ ps <- get

396+ let (uh, uns) = unified ps

397+-- put (ps { unified = (uh, uns ++ ns) })

398+-- addLog (show (uh, uns ++ ns))

399+ return $ Bind x (Guess ty val) sc

400+match_fill _ _ _ _ = fail "Can't fill here."

401+

375402prep_fill :: Name -> [Name] -> RunTactic

376403prep_fill f as ctxt env (Bind x (Hole ty) sc) =

377404 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)

@@ -680,6 +707,7 @@ process t h = tactic (Just h) (mktac t)

680707 mktac (Claim n r) = claim n r

681708 mktac (Exact r) = exact r

682709 mktac (Fill r) = fill r

710+ mktac (MatchFill r) = match_fill r

683711 mktac (PrepFill n ns) = prep_fill n ns

684712 mktac CompleteFill = complete_fill

685713 mktac Regret = regret

src/Core/Unify.hs+85−27

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

3−module Core.Unify(unify, Fails) where

3+module Core.Unify(match_unify, unify, Fails) where

55import Core.TT

66import Core.Evaluate

@@ -27,6 +27,66 @@ data UResult a = UOK a

2727 | UPartOK a

2828 | UFail Err

2929

30+-- Solve metavariables by matching terms against each other

31+-- Not really unification, of course!

32+

33+match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

34+ TC [(Name, TT Name)]

35+match_unify ctxt env topx topy dont holes =

36+-- trace ("Matching " ++ show (topx, topy)) $

37+ case runStateT (un [] topx topy) (UI 0 []) of

38+ OK (v, UI _ fails) -> return (filter notTrivial v)

39+ Error e -> tfail e

40+ where

41+ un names (P _ x _) tm

42+ | holeIn env x || x `elem` holes

43+ = do sc 1; checkCycle (x, tm)

44+ un names tm (P _ y _)

45+ | holeIn env y || y `elem` holes

46+ = do sc 1; checkCycle (y, tm)

47+ un names x y

48+ | OK True <- convEq' ctxt x y = do sc 1; return []

49+ un bnames (V i) (P _ x _)

50+ | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

51+ un bnames (P _ x _) (V i)

52+ | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

53+ un names (App fx ax) (App fy ay)

54+ = do hf <- un names fx fy

55+ ha <- un names ax ay

56+ combine names hf ha

57+

58+

59+ -- TODO: there's an annoying amount of repetition between this and the

60+ -- main unification function. Consider lifting it out.

61+

62+ sc i = do UI s f <- get

63+ put (UI (s+i) f)

64+

65+ unifyFail x y = do UI s f <- get

66+ let r = recoverable x y

67+ let err = CantUnify r

68+ topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

69+ put (UI s ((x, y, env, err) : f))

70+ lift $ tfail err

71+ combine bnames as [] = return as

72+ combine bnames as ((n, t) : bs)

73+ = case lookup n as of

74+ Nothing -> combine bnames (as ++ [(n,t)]) bs

75+ Just t' -> do ns <- un bnames t t'

76+ -- make sure there's n mapping from n in ns

77+ let ns' = filter (\ (x, _) -> x/=n) ns

78+ sc 1

79+ combine bnames as (ns' ++ bs)

80+

81+ checkCycle p@(x, P _ _ _) = return [p]

82+ checkCycle (x, tm)

83+ | not (x `elem` freeNames tm) = return [(x, tm)]

84+ | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

85+

86+notTrivial (x, P _ x' _) = x /= x'

87+notTrivial _ = True

88+

89+

3090unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

3191 TC ([(Name, TT Name)], Fails)

3292unify ctxt env topx topy dont holes =

@@ -45,9 +105,6 @@ unify ctxt env topx topy dont holes =

45105-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

46106 Error e -> tfail e

47107 where

48− notTrivial (x, P _ x' _) = x /= x'

49− notTrivial _ = True

50−

51108 headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y

52109 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

53110 headDiff _ _ = False

@@ -311,6 +368,7 @@ unify ctxt env topx topy dont holes =

311368 | not (x `elem` freeNames tm) = return [(x, tm)]

312369 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

313370

371+

314372 combineArgs bnames args = ca [] args where

315373 ca acc [] = return acc

316374 ca acc (x : xs) = do x' <- combine bnames acc x

@@ -326,30 +384,30 @@ unify ctxt env topx topy dont holes =

326384 sc 1

327385 combine bnames as (ns' ++ bs)

328386

329− -- If there are any clashes of constructors, deem it unrecoverable, otherwise some

330− -- more work may help.

331− -- FIXME: Depending on how overloading gets used, this may cause problems. Better

332− -- rethink overloading properly...

333−

334− recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

335− | x == y = True

336− | otherwise = False

337− recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)

338− | x == y = True

339− | otherwise = False

340− recoverable (Constant _) (P (DCon _ _) y _) = False

341− recoverable (P (DCon _ _) x _) (Constant _) = False

342− recoverable (Constant _) (P (TCon _ _) y _) = False

343− recoverable (P (TCon _ _) x _) (Constant _) = False

344− recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

345− recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

346− recoverable p@(Constant _) (App f a) = recoverable p f

347− recoverable (App f a) p@(Constant _) = recoverable f p

348− recoverable p@(P _ n _) (App f a) = recoverable p f

387+-- If there are any clashes of constructors, deem it unrecoverable, otherwise some

388+-- more work may help.

389+-- FIXME: Depending on how overloading gets used, this may cause problems. Better

390+-- rethink overloading properly...

391+

392+recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

393+ | x == y = True

394+ | otherwise = False

395+recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)

396+ | x == y = True

397+ | otherwise = False

398+recoverable (Constant _) (P (DCon _ _) y _) = False

399+recoverable (P (DCon _ _) x _) (Constant _) = False

400+recoverable (Constant _) (P (TCon _ _) y _) = False

401+recoverable (P (TCon _ _) x _) (Constant _) = False

402+recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

403+recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

404+recoverable p@(Constant _) (App f a) = recoverable p f

405+recoverable (App f a) p@(Constant _) = recoverable f p

406+recoverable p@(P _ n _) (App f a) = recoverable p f

349407-- recoverable (App f a) p@(P _ _ _) = recoverable f p

350− recoverable (App f a) (App f' a')

351− = recoverable f f' -- && recoverable a a'

352− recoverable _ _ = True

408+recoverable (App f a) (App f' a')

409+ = recoverable f f' -- && recoverable a a'

410+recoverable _ _ = True

353411

354412errEnv = map (\(x, b) -> (x, binderTy b))

355413

src/Idris/AbsSyntaxTree.hs+2

@@ -382,6 +382,7 @@ data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level de

382382 | PWith FC Name t [t] t [PDecl' t]

383383 | PClauseR FC [t] t [PDecl' t]

384384 | PWithR FC [t] t [PDecl' t]

385+ | PTyClause FC Name t t [PDecl' t]

385386 deriving Functor

386387{-!

387388deriving instance Binary PClause'

@@ -543,6 +544,7 @@ mapPT f t = f (mpt t) where

543544

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

545546 | Refine Name [Bool] | Rewrite t

547+ | MatchRefine Name

546548 | LetTac Name t | LetTacTy Name t t

547549 | Exact t | Compute | Trivial

548550 | Solve

src/Idris/Completion.hs+1

@@ -31,6 +31,7 @@ tacticArgs :: [(String, Maybe TacticArg)]

3131tacticArgs = [ ("intro", Nothing)

3232 , ("intros", Nothing)

3333 , ("refine", Just ExprTArg)

34+ , ("mrefine", Just ExprTArg)

3435 , ("rewrite", Just ExprTArg)

3536 , ("let", Nothing) -- FIXME syntax for let

3637 , ("focus", Just ExprTArg)

src/Idris/ElabTerm.hs+12

@@ -728,6 +728,18 @@ runTac autoSolve ist tac

728728 bname _ = Nothing

729729 runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm

730730 when autoSolve solveAll

731+ runT (MatchRefine fn)

732+ = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

733+ [] -> do a <- envArgs fn

734+ return (fn, a)

735+ [(n, args)] -> return $ (n, map (const True) args)

736+ ns <- match_apply (Var fn') (map (\x -> (x, 0)) imps)

737+ when autoSolve solveAll

738+ where envArgs n = do e <- get_env

739+ case lookup n e of

740+ Just t -> return $ map (const False)

741+ (getArgTys (binderTy t))

742+ _ -> return []

731743 runT (Refine fn [])

732744 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

733745 [] -> do a <- envArgs fn

src/Idris/Parser.hs+21−1

@@ -1393,6 +1393,23 @@ pClause syn

13931393 ist <- getState

13941394 setState (ist { lastParse = Just n })

13951395 return $ PClause fc n capp wargs rhs wheres)

1396+ <|> try (do pushIndent

1397+ n_in <- pfName; let n = expandNS syn n_in

1398+ reserved "of"; reserved "type"

1399+ fc <- pfc

1400+ ty <- pSimpleExpr syn

1401+ rhs <- pRHS syn n

1402+ ist <- getState

1403+ let ctxt = tt_ctxt ist

1404+ let wsyn = syn { syn_namespace = [] }

1405+ (wheres, nmap) <- choice [do x <- pWhereblock n wsyn

1406+ popIndent

1407+ return x,

1408+ do pTerminator

1409+ return ([], [])]

1410+ ist <- getState

1411+ setState (ist { lastParse = Just n })

1412+ return $ PTyClause fc n ty rhs wheres)

13961413 <|> try (do pushIndent

13971414 wargs <- many1 (pWExpr syn)

13981415 ist <- getState

@@ -1440,7 +1457,7 @@ pClause syn

14401457 let withs = concat ds

14411458 closeBlock

14421459 return $ PWithR fc wargs wval withs)

1443−

1460+

14441461 <|> do pushIndent

14451462 l <- pArgExpr syn

14461463 op <- operator

@@ -1561,6 +1578,9 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

15611578 <|> do reserved "refine"; n <- pName

15621579 i <- getState

15631580 return $ Refine n []

1581+ <|> do reserved "mrefine"; n <- pName

1582+ i <- getState

1583+ return $ MatchRefine n

15641584 <|> do reserved "rewrite"; t <- pExpr syn;

15651585 i <- getState

15661586 return $ Rewrite (desugar syn i t)