cbc60eb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Unification, and unify tactic

commitcbc60eb3c537c8650b93cca1f84401537f2e2943 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 27 Sep 2011, 14:13 (15 years ago) parent77be0d0

7 files changed+120−39

compare with master

unifiedsplit

impl-paper/overview.tex+2 src/Core.hs+9 src/CoreParser.hs+1−8 src/Evaluate.hs−9 src/ProofState.hs+48−17 src/ShellParser.hs+2−1 src/Unify.hs+58−4

impl-paper/overview.tex+2

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

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

1313 indices becomes tricky.

1414\end{itemize}

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

16+\item An Elaborator, as an EDSL

1517\end{itemize}

1618

1719For 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,

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

116116 deriving (Show, Functor, Eq)

117117

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

119+

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

119121

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

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

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

136138arity _ = 0

137139

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+

138147type Term = TT Name

139148type Type = Term

140149

src/CoreParser.hs+1−8

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

101101 reserved "in";

102102 sc <- pTerm

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

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

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

113106 lchar '.';

114107 sc <- pTerm

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

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

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

117110 return (RSet (fromInteger i)))

118111 <|> try (do x <- iName

119112 return (Var x))

src/Evaluate.hs−9

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

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

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

3232

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−

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

3934

4035bindEnv :: EnvTT n -> TT n -> TT n

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

5752 | Just v <- lookupVal n ctxt = v

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

5954 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

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

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

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

src/ProofState.hs+48−17

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

3434data Tactic = Attack

3535 | Claim Name Raw

3636 | Fill Raw

37+ | UnifyFill Raw

3738 | Regret

3839 | Solve

3940 | Compute

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

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

5051 | FocusGoal Name -- focus on this goal next

5152 | Solved Name

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

5254 | Log String

5355

5456-- Some utilites on proof and tactic states

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

162164 return $ Bind x (Guess ty val) sc

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

164166

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+

165181solve :: RunTactic

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

167183 | pureTerm val = do action (Solved x)

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

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

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

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

212−processTactic t ps = case holes ps of

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

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

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

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

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

218− logs actions)

228+processTactic t ps

229+ = case holes ps of

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

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

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

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

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

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

236+ logs actions)

219237 where logs [] = ""

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

221239 logs (_ : xs) = logs xs

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

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

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

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

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

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

229248

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+

230260

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

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

233− where mktac Attack = attack

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

235− mktac (Fill r) = fill r

236− mktac Regret = regret

237− mktac Solve = solve

238− mktac Compute = compute

239− mktac (Intro n) = intro n

240− mktac (CheckIn r) = check_in r

241− mktac (EvalIn r) = eval_in r

242− mktac (Focus n) = focus n

263+ where mktac Attack = attack

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

265+ mktac (Fill r) = fill r

266+ mktac (UnifyFill r) = unify_fill r

267+ mktac Regret = regret

268+ mktac Solve = solve

269+ mktac Compute = compute

270+ mktac (Intro n) = intro n

271+ mktac (CheckIn r) = check_in r

272+ mktac (EvalIn r) = eval_in r

273+ mktac (Focus n) = focus n

src/ShellParser.hs+2−1

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

4747pTactic = do reserved "attack"; return Attack

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

4949 return (Claim n ty)

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

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

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

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

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

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

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

src/Unify.hs+58−4

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

55import Core

66import Evaluate

8+import Control.Monad

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

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

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

1113

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

1315unify ctxt env x y

14− = case un' [] x y of

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

1517 OK v -> return v

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

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

19+ OK v -> return v

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

1721 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

1935 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

2175

2276holeIn :: Env -> Name -> Bool

2377holeIn env n = case lookup n env of