cbc60eb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unification, and unify tactic

cbc60ebEdwin Brady15 years ago

impl-paper/overview.tex+2

compare with master

unifiedsplit

@@ -12,6 +12,8 @@ High level view of steps we've taken to implement this new version:

12 \item Dealing with names: typechecking and evaluation in a context, managing de Bruijn

13 indices becomes tricky.

14\end{itemize}

15+\item Unification, and incorporation into the tactic engine.

16+\item An Elaborator, as an EDSL

15\end{itemize}

17\end{itemize}

17For the high level language: we need nothing more than the core type theory,

19For the high level language: we need nothing more than the core type theory,

src/Core.hs+9

@@ -115,6 +115,8 @@ data Datatype n = Data { d_typename :: n,

115 d_cons :: [(n, TT n)] }

116 deriving (Show, Functor, Eq)

117

118+-- A few handy operations on well typed terms:

119+

118-- Returns true if V 0 and bound name n do not occur in the term

120-- Returns true if V 0 and bound name n do not occur in the term

119

121

120noOccurrence :: Eq n => n -> TT n -> Bool

122noOccurrence :: Eq n => n -> TT n -> Bool

@@ -135,6 +137,13 @@ arity :: TT n -> Int

135arity (Bind n (Pi t) sc) = 1 + arity sc

137arity (Bind n (Pi t) sc) = 1 + arity sc

136arity _ = 0

138arity _ = 0

137

139

140+-- deconstruct an application; returns the function and a list of arguments

141+

142+unApply :: TT n -> (TT n, [TT n])

143+unApply t = ua [] t where

144+ ua args (App f a) = ua (a:args) f

145+ ua args t = (t, reverse args)

146+

138type Term = TT Name

147type Term = TT Name

139type Type = Term

148type Type = Term

140

149

src/CoreParser.hs+1−8

@@ -101,19 +101,12 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

101 reserved "in";

102 sc <- pTerm

103 return (RBind x (Let ty val) sc))

104−-- <|> try (do reserved "nlet";

105−-- x <- iName; lchar ':'; ty <- pTerm

106−-- lchar '=';

107−-- val <- pTerm

108−-- reserved "in";

109−-- sc <- pTerm

110−-- return (RBind x (NLet ty val) sc))

111 <|> try (do lchar '_';

104 <|> try (do lchar '_';

112 x <- iName; lchar ':'; ty <- pTerm

105 x <- iName; lchar ':'; ty <- pTerm

113 lchar '.';

106 lchar '.';

114 sc <- pTerm

107 sc <- pTerm

115 return (RBind x (PVar ty) sc))

108 return (RBind x (PVar ty) sc))

116− <|> try (do reserved "Set"; i <- natural

109+ <|> try (do reserved "Set"; i <- option 0 natural

117 return (RSet (fromInteger i)))

110 return (RSet (fromInteger i)))

118 <|> try (do x <- iName

111 <|> try (do x <- iName

119 return (Var x))

112 return (Var x))

src/Evaluate.hs−9

@@ -30,11 +30,6 @@ instance Show Value where

30normalise :: Context -> Env -> TT Name -> TT Name

31normalise ctxt env t = quote 0 (eval ctxt env t)

33−-- let evtm = bindEnv (reverse env) t

34−-- evtm' = quote 0 (evalCtxt ctxt evtm) in

35−-- trace (show (evtm, evtm')) $

36−-- unbindEnv env evtm'

37−

38-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))

33-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))

40bindEnv :: EnvTT n -> TT n -> TT n

35bindEnv :: EnvTT n -> TT n -> TT n

@@ -57,10 +52,6 @@ eval ctxt genv tm = ev [] tm where

57 | Just v <- lookupVal n ctxt = v

52 | Just v <- lookupVal n ctxt = v

58 ev env (P nt n ty) = VP nt n (ev env ty)

53 ev env (P nt n ty) = VP nt n (ev env ty)

59 ev env (V i) | i < length env = env !! i

54 ev env (V i) | i < length env = env !! i

60−-- | i < length env + length genv

61−-- = case genv !! (i - length env) of

62−-- (_, Let t v) -> ev env v

63−-- _ -> VV i

64 | otherwise = error $ "Internal error: V" ++ show i

55 | otherwise = error $ "Internal error: V" ++ show i

65 ev env (Bind n (Let t v) sc)

56 ev env (Bind n (Let t v) sc)

66 = wknV (-1) $ ev (ev env v : env) sc

57 = wknV (-1) $ ev (ev env v : env) sc

src/ProofState.hs+48−17

@@ -34,6 +34,7 @@ data Command = Theorem Name Raw

34data Tactic = Attack

35 | Claim Name Raw

36 | Fill Raw

37+ | UnifyFill Raw

37 | Regret

38 | Regret

38 | Solve

39 | Solve

39 | Compute

40 | Compute

@@ -49,6 +50,7 @@ data TacticAction = AddGoal Name -- add a new goal, solve immediately

49 | NextGoal Name -- add a new goal, solve it after current one

50 | NextGoal Name -- add a new goal, solve it after current one

50 | FocusGoal Name -- focus on this goal next

51 | FocusGoal Name -- focus on this goal next

51 | Solved Name

52 | Solved Name

53+ | AlsoSolved Name Term -- goals solved by unification

52 | Log String

54 | Log String

54-- Some utilites on proof and tactic states

56-- Some utilites on proof and tactic states

@@ -162,6 +164,20 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

162 return $ Bind x (Guess ty val) sc

164 return $ Bind x (Guess ty val) sc

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

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

164

166

167+-- As fill, but attempts to solve other goals by unification

168+

169+unify_fill :: Raw -> RunTactic

170+unify_fill guess ctxt env (Bind x (Hole ty) sc) =

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

172+ ns <- lift $ unify ctxt env valty ty

173+ solve_all ns

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

175+ where

176+ solve_all [] = return ()

177+ solve_all ((n, tm): ns) = do action (AlsoSolved n tm)

178+ solve_all ns

179+unify_fill _ _ _ _ = fail "Can't fill here."

180+

165solve :: RunTactic

181solve :: RunTactic

166solve ctxt env (Bind x (Guess ty val) sc)

182solve ctxt env (Bind x (Guess ty val) sc)

167 | pureTerm val = do action (Solved x)

183 | pureTerm val = do action (Solved x)

@@ -209,13 +225,15 @@ processTactic QED ps = case holes ps of

209 "Proof complete: " ++ showEnv [] tm)

225 "Proof complete: " ++ showEnv [] tm)

210 _ -> Error "Still holes to fill."

226 _ -> Error "Still holes to fill."

211processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

227processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

212−processTactic t ps = case holes ps of

228+processTactic t ps

229+ = case holes ps of

213− [] -> Error "Nothing to fill in."

230+ [] -> Error "Nothing to fill in."

214− (h:_) -> do let n = nextname ps

231+ (h:_) -> do let n = nextname ps

215− (ps',(n', actions)) <- runStateT (process t h ps) (n, [])

232+ (ps', (n', actions)) <- runStateT (process t h ps) (n, [])

216− return (ps' { nextname = n',

233+ return (ps' { nextname = n',

234+ pterm = updateSolved (getSolved actions) (pterm ps'),

217− holes = goals (holes ps') actions },

235+ holes = goals (holes ps') actions },

218− logs actions)

236+ logs actions)

219 where logs [] = ""

237 where logs [] = ""

220 logs (Log x : xs) = x ++ "\n" ++ logs xs

238 logs (Log x : xs) = x ++ "\n" ++ logs xs

221 logs (_ : xs) = logs xs

239 logs (_ : xs) = logs xs

@@ -225,18 +243,31 @@ processTactic t ps = case holes ps of

225 goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs

243 goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs

226 goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs

244 goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs

227 goals g (Solved n : xs) = goals (g \\ [n]) xs

245 goals g (Solved n : xs) = goals (g \\ [n]) xs

246+ goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs

228 goals g (_ : xs) = goals g xs

247 goals g (_ : xs) = goals g xs

229

248

249+ getSolved [] = []

250+ getSolved (AlsoSolved n tm : xs) = (n, tm) : getSolved xs

251+ getSolved (_ : xs) = getSolved xs

252+

253+ updateSolved xs (Bind n b t)

254+ | Just v <- lookup n xs = Bind n (Let (binderTy b) v) (updateSolved xs t)

255+ | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

256+ updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

257+ updateSolved xs t = t

258+

259+

230

260

231process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState

261process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState

232process t h ps = tactic (Just h) ps (context ps) (mktac t)

262process t h ps = tactic (Just h) ps (context ps) (mktac t)

233− where mktac Attack = attack

263+ where mktac Attack = attack

234− mktac (Claim n r) = claim n r

264+ mktac (Claim n r) = claim n r

235− mktac (Fill r) = fill r

265+ mktac (Fill r) = fill r

266+ mktac (UnifyFill r) = unify_fill r

236− mktac Regret = regret

267+ mktac Regret = regret

237− mktac Solve = solve

268+ mktac Solve = solve

238− mktac Compute = compute

269+ mktac Compute = compute

239− mktac (Intro n) = intro n

270+ mktac (Intro n) = intro n

240− mktac (CheckIn r) = check_in r

271+ mktac (CheckIn r) = check_in r

241− mktac (EvalIn r) = eval_in r

272+ mktac (EvalIn r) = eval_in r

242− mktac (Focus n) = focus n

273+ mktac (Focus n) = focus n

src/ShellParser.hs+2−1

@@ -47,8 +47,9 @@ pTactic :: Parser Tactic

47pTactic = do reserved "attack"; return Attack

48 <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm

49 return (Claim n ty)

50− <|> do reserved "fill"; tm <- pTerm; return (Fill tm)

51 <|> do reserved "regret"; return Regret

50 <|> do reserved "regret"; return Regret

51+ <|> do reserved "fill"; tm <- pTerm; return (Fill tm)

52+ <|> do reserved "unify"; tm <- pTerm; return (UnifyFill tm)

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

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

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

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

54 <|> do reserved "intro"; n <- iName; return (Intro n)

55 <|> do reserved "intro"; n <- iName; return (Intro n)

src/Unify.hs+58−4

@@ -5,19 +5,73 @@ module Unify(unify) where

5import Core

6import Evaluate

8+import Control.Monad

8-- Unification is applied inside the theorem prover. We're looking for holes

10-- Unification is applied inside the theorem prover. We're looking for holes

9-- which can be filled in, by matching one term's normal form against another.

11-- which can be filled in, by matching one term's normal form against another.

10-- Returns a list of hole names paired with the term which solves them.

12-- Returns a list of hole names paired with the term which solves them.

12unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

14unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

13unify ctxt env x y

15unify ctxt env x y

14− = case un' [] x y of

16+ = case un' [] x y of -- try without normalising first, for speed

15 OK v -> return v

17 OK v -> return v

18+ _ -> case un' [] (normalise ctxt env x) (normalise ctxt env y) of

19+ OK v -> return v

16− _ -> fail $ "Can't unify " ++ showEnv env x ++ " and " ++ showEnv env y

20+ _ -> fail $ "Can't unify " ++ showEnv env x ++ " and " ++ showEnv env y

17 where

21 where

18− un' bnames (P Bound x _) (P Bound y _) | (x,y) `elem` bnames = return []

22+ un' bnames (P Bound x _) (P Bound y _)

23+ | (x,y) `elem` bnames = return []

24+ un' bnames (P Bound x _) tm

25+ | holeIn env x = return [(x, tm)]

26+ un' bnames tm (P Bound y _)

27+ | holeIn env y = return [(y, tm)]

28+

29+ un' bnames x@(App _ _) y@(App _ _)

30+ = uApp bnames (unApply x) (unApply y)

31+ un' bnames (Bind x bx sx) (Bind y by sy)

32+ = do h1 <- uB bnames bx by

33+ h2 <- un' ((x,y):bnames) sx sy

34+ combine bnames h1 h2

19 un' bnames x y | x == y = return []

35 un' bnames x y | x == y = return []

20− | otherwise = fail "Can't unify"

36+ | otherwise = fail "Can't unify"

37+

38+ uB bnames (Let tx vx) (Let ty vy)

39+ = do h1 <- un' bnames tx ty

40+ h2 <- un' bnames ty vy

41+ combine bnames h1 h2

42+ uB bnames (Guess tx vx) (Guess ty vy)

43+ = do h1 <- un' bnames tx ty

44+ h2 <- un' bnames ty vy

45+ combine bnames h1 h2

46+ uB bnames (Lam tx) (Lam ty) = un' bnames tx ty

47+ uB bnames (Pi tx) (Pi ty) = un' bnames tx ty

48+ uB bnames (Hole tx) (Hole ty) = un' bnames tx ty

49+ uB bnames (PVar tx) (PVar ty) = un' bnames tx ty

50+ uB bnames _ _ = fail "Can't unify"

51+

52+ uApp bnames (xp@(P xnt x xty), xargs) (yp@(P ynt y yty), yargs)

53+ | (x == y && all okToUnify [xnt, ynt]) ||

54+ (holeIn env x && okToUnify ynt) ||

55+ (okToUnify xnt && holeIn env y)

56+ = do h <- un' bnames xp yp

57+ hargs <- zipWithM (un' bnames) xargs yargs

58+ h' <- foldM (combine bnames) [] hargs

59+ combine bnames h h'

60+ uApp bnames (xf, xargs) (yf, yargs)

61+ = do un' bnames xf yf -- ignore result

62+ hargs <- zipWithM (un' bnames) xargs yargs

63+ foldM (combine bnames) [] hargs

64+

65+ okToUnify (DCon _ _) = True

66+ okToUnify (TCon _) = True

67+ okToUnify _ = False

68+

69+ combine bnames as [] = return as

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

71+ = case lookup n as of

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

73+ Just t' -> do un' bnames t t'

74+ combine bnames as bs

22holeIn :: Env -> Name -> Bool

76holeIn :: Env -> Name -> Bool

23holeIn env n = case lookup n env of

77holeIn env n = case lookup n env of