c7fded1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added 'mrefine' tactic

c7fded1Edwin Brady13 years ago

src/Core/Elaborate.hs+10−3

compare with master

unifiedsplit

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

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

236fill t = processTactic' (Fill t)

237

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

239+match_fill t = processTactic' (MatchFill t)

240+

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

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

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

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

240

243

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

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

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

376 rebind hs t = t

379 rebind hs t = t

377

380

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

382+apply = apply' fill

383+match_apply = apply' match_fill

384+

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

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

379−apply fn imps =

386+apply' fillt fn imps =

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

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

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

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

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

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

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

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

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

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

src/Core/ProofState.hs+29−1

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

49 | Reorder Name

50 | Exact Raw

51 | Fill Raw

52+ | MatchFill Raw

52 | PrepFill Name [Name]

53 | PrepFill Name [Name]

53 | CompleteFill

54 | CompleteFill

54 | Regret

55 | Regret

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

154qshow :: Fails -> String

155qshow :: Fails -> String

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

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

156

157

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+

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

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

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

158unify' ctxt env topx topy =

170unify' ctxt env topx topy =

159 do ps <- get

171 do ps <- get

160 let dont = dontunify ps

172 let dont = dontunify ps

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

372 return $ Bind x (Guess ty val) sc

384 return $ Bind x (Guess ty val) sc

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

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

374

386

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+

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

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

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

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

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

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

680 mktac (Claim n r) = claim n r

707 mktac (Claim n r) = claim n r

681 mktac (Exact r) = exact r

708 mktac (Exact r) = exact r

682 mktac (Fill r) = fill r

709 mktac (Fill r) = fill r

710+ mktac (MatchFill r) = match_fill r

683 mktac (PrepFill n ns) = prep_fill n ns

711 mktac (PrepFill n ns) = prep_fill n ns

684 mktac CompleteFill = complete_fill

712 mktac CompleteFill = complete_fill

685 mktac Regret = regret

713 mktac Regret = regret

src/Core/Unify.hs+85−27

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

1{-# LANGUAGE PatternGuards #-}

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

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

5import Core.TT

6import Core.Evaluate

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

27 | UPartOK a

28 | UFail Err

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+

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

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

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

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

32unify ctxt env topx topy dont holes =

92unify ctxt env topx topy dont holes =

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

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

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

46 Error e -> tfail e

106 Error e -> tfail e

47 where

107 where

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

49− notTrivial _ = True

50−

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

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

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

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

53 headDiff _ _ = False

110 headDiff _ _ = False

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

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

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

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

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

313

370

371+

314 combineArgs bnames args = ca [] args where

372 combineArgs bnames args = ca [] args where

315 ca acc [] = return acc

373 ca acc [] = return acc

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

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

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

326 sc 1

384 sc 1

327 combine bnames as (ns' ++ bs)

385 combine bnames as (ns' ++ bs)

328

386

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

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

330− -- more work may help.

388+-- more work may help.

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

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

332− -- rethink overloading properly...

390+-- rethink overloading properly...

333−

391+

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

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

335− | x == y = True

393+ | x == y = True

336− | otherwise = False

394+ | otherwise = False

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

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

338− | x == y = True

396+ | x == y = True

339− | otherwise = False

397+ | otherwise = False

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

352− recoverable _ _ = True

410+recoverable _ _ = True

353

411

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

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

355

413

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

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

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

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

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

385 deriving Functor

386 deriving Functor

386{-!

387{-!

387deriving instance Binary PClause'

388deriving instance Binary PClause'

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

543

544

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

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

545 | Refine Name [Bool] | Rewrite t

546 | Refine Name [Bool] | Rewrite t

547+ | MatchRefine Name

546 | LetTac Name t | LetTacTy Name t t

548 | LetTac Name t | LetTacTy Name t t

547 | Exact t | Compute | Trivial

549 | Exact t | Compute | Trivial

548 | Solve

550 | Solve

src/Idris/Completion.hs+1

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

31tacticArgs = [ ("intro", Nothing)

32 , ("intros", Nothing)

33 , ("refine", Just ExprTArg)

34+ , ("mrefine", Just ExprTArg)

34 , ("rewrite", Just ExprTArg)

35 , ("rewrite", Just ExprTArg)

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

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

36 , ("focus", Just ExprTArg)

37 , ("focus", Just ExprTArg)

src/Idris/ElabTerm.hs+12

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

728 bname _ = Nothing

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

730 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 []

731 runT (Refine fn [])

743 runT (Refine fn [])

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

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

733 [] -> do a <- envArgs fn

745 [] -> do a <- envArgs fn

src/Idris/Parser.hs+21−1

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

1393 ist <- getState

1394 setState (ist { lastParse = Just n })

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

1396 <|> try (do pushIndent

1413 <|> try (do pushIndent

1397 wargs <- many1 (pWExpr syn)

1414 wargs <- many1 (pWExpr syn)

1398 ist <- getState

1415 ist <- getState

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

1440 let withs = concat ds

1457 let withs = concat ds

1441 closeBlock

1458 closeBlock

1442 return $ PWithR fc wargs wval withs)

1459 return $ PWithR fc wargs wval withs)

1443−

1460+

1444 <|> do pushIndent

1461 <|> do pushIndent

1445 l <- pArgExpr syn

1462 l <- pArgExpr syn

1446 op <- operator

1463 op <- operator

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

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

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

1562 i <- getState

1579 i <- getState

1563 return $ Refine n []

1580 return $ Refine n []

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

1582+ i <- getState

1583+ return $ MatchRefine n

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

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

1565 i <- getState

1585 i <- getState

1566 return $ Rewrite (desugar syn i t)

1586 return $ Rewrite (desugar syn i t)