@@ -1,8 +1,9 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
3−{- Implements a proof state, some primitive tactics for manipulating
3+{- | Implements a proof state, some primitive tactics for manipulating
4− proofs, and some high level commands for introducing new theorems,
4+proofs, and some high level commands for introducing new theorems,
5− evaluation/checking inside the proof system, etc. --}
5+evaluation/checking inside the proof system, etc.
7module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,
8module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,
8 updateSolved, updateSolvedTerm, updateSolvedTerm',
9 updateSolved, updateSolvedTerm, updateSolvedTerm',
@@ -18,6 +19,7 @@ import Control.Monad.State.Strict
18import Data.List
19import Data.List
19import Debug.Trace
20import Debug.Trace
22+-- | A zipper over terms, in order to efficiently update proof terms.
21data TermPath = Top
23data TermPath = Top
22 | AppL TermPath Term
24 | AppL TermPath Term
23 | AppR Term TermPath
25 | AppR Term TermPath
@@ -25,6 +27,7 @@ data TermPath = Top
25 | InScope Name (Binder Term) TermPath
27 | InScope Name (Binder Term) TermPath
26 deriving Show
28 deriving Show
30+-- | A zipper over binders, because terms and binders are mutually defined.
28data BinderPath = Binder (Binder TermPath)
31data BinderPath = Binder (Binder TermPath)
29 | LetT TermPath Term
32 | LetT TermPath Term
30 | LetV Term TermPath
33 | LetV Term TermPath
@@ -32,6 +35,8 @@ data BinderPath = Binder (Binder TermPath)
32 | GuessV Term TermPath
35 | GuessV Term TermPath
33 deriving Show
36 deriving Show
38+-- | Replace the top of a term path with another term path. In other
39+-- words, "graft" one term path into another.
35replaceTop :: TermPath -> TermPath -> TermPath
40replaceTop :: TermPath -> TermPath -> TermPath
36replaceTop p Top = p
41replaceTop p Top = p
37replaceTop p (AppL l t) = AppL (replaceTop p l) t
42replaceTop p (AppL l t) = AppL (replaceTop p l) t
@@ -45,6 +50,7 @@ replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc
45 replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)
50 replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)
46replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)
51replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)
53+-- | Build a term from a zipper, given something to put in the hole.
48rebuildTerm :: Term -> TermPath -> Term
54rebuildTerm :: Term -> TermPath -> Term
49rebuildTerm tm Top = tm
55rebuildTerm tm Top = tm
50rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a
56rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a
@@ -52,6 +58,7 @@ rebuildTerm tm (AppR f p) = App f (rebuildTerm tm p)
52rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)
58rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)
53rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc
59rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc
61+-- | Build a binder from a zipper, given something to put in the hole.
55rebuildBinder :: Term -> BinderPath -> Binder Term
62rebuildBinder :: Term -> BinderPath -> Binder Term
56rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p
63rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p
57rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t
64rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t
@@ -59,6 +66,9 @@ rebuildBinder tm (LetV v p) = Let v (rebuildTerm tm p)
59rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t
66rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t
60rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)
67rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)
69+-- | Find the binding of a hole in a term. If present, return the path
70+-- to the hole's binding, the environment extended by the binders that
71+-- are crossed, and the actual binding term.
62findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
72findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
63findHole n env t = fh' env Top t where
73findHole n env t = fh' env Top t where
64 fh' env path tm@(Bind x h sc)
74 fh' env path tm@(Bind x h sc)
@@ -80,7 +90,7 @@ findHole n env t = fh' env Top t where
80 fhB env path b
90 fhB env path b
81 | Just (p, env', tm) <- fh' env path (binderTy b)
91 | Just (p, env', tm) <- fh' env path (binderTy b)
82 = Just (Binder (fmap (\_ -> p) b), env', tm)
92 = Just (Binder (fmap (\_ -> p) b), env', tm)
83− fhB _ _ _ = Nothing
93+ fhB _ _ _ = Nothing
85data ProofTerm = PT { -- wholeterm :: Term,
95data ProofTerm = PT { -- wholeterm :: Term,
86 path :: TermPath,
96 path :: TermPath,
@@ -92,13 +102,17 @@ data ProofTerm = PT { -- wholeterm :: Term,
92type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
102type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
93type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
103type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
105+-- | Refocus the proof term zipper on a particular hole, if it
106+-- exists. If not, return the original proof term.
95refocus :: Hole -> ProofTerm -> ProofTerm
107refocus :: Hole -> ProofTerm -> ProofTerm
96refocus h t = let res = refocus' h t in res
108refocus h t = let res = refocus' h t in res
97-- trace ("OLD: " ++ show t ++ "\n" ++
109-- trace ("OLD: " ++ show t ++ "\n" ++
98-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res
110-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res
99refocus' (Just n) pt@(PT path env tm ups)
111refocus' (Just n) pt@(PT path env tm ups)
112+ -- First look for the hole in the proof term as-is
100 | Just (p', env', tm') <- findHole n env tm
113 | Just (p', env', tm') <- findHole n env tm
101 = PT (replaceTop p' path) env' tm' ups
114 = PT (replaceTop p' path) env' tm' ups
115+ -- Next apply the updates, and look for the hole in the resulting term
102 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))
116 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))
103 = PT p' env' tm' []
117 = PT p' env' tm' []
104 | otherwise = pt
118 | otherwise = pt
@@ -118,27 +132,32 @@ same :: Eq a => Maybe a -> a -> Bool
118same Nothing n = True
132same Nothing n = True
119same (Just x) n = x == n
133same (Just x) n = x == n
135+-- | Is a particular binder a hole or a guess?
121hole :: Binder b -> Bool
136hole :: Binder b -> Bool
122hole (Hole _) = True
137hole (Hole _) = True
123hole (Guess _ _) = True
138hole (Guess _ _) = True
124hole _ = False
139hole _ = False
141+-- | Given a list of solved holes, fill out the solutions in a term
126−updateSolvedTerm :: [(Name, Term)] -> Term -> Term
142+updateSolvedTerm :: [(Name, Term)] -> Term -> Term
127updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x
143updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x
145+-- | Given a list of solved holes, fill out the solutions in a
146+-- term. Return whether updates were performed, to facilitate sharing
147+-- when there are no updates.
148+updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)
129updateSolvedTerm' [] x = (x, False)
149updateSolvedTerm' [] x = (x, False)
130−updateSolvedTerm' xs x = -- updateSolved' xs x where
150+updateSolvedTerm' xs x = updateSolved' xs x where
131−-- This version below saves allocations, because it doesn't need to reallocate
151+ -- This version below saves allocations, because it doesn't need to reallocate
132−-- the term if there are no updates to do.
152+ -- the term if there are no updates to do.
133−-- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is
153+ -- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is
134−-- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).
154+ -- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).
135− updateSolved' xs x where
136 updateSolved' [] x = (x, False)
155 updateSolved' [] x = (x, False)
137 updateSolved' xs (Bind n (Hole ty) t)
156 updateSolved' xs (Bind n (Hole ty) t)
138− | Just v <- lookup n xs
157+ | Just v <- lookup n xs
139 = case xs of
158 = case xs of
140 [_] -> (subst n v t, True) -- some may be Vs! Can't assume
159 [_] -> (subst n v t, True) -- some may be Vs! Can't assume
141− -- explicit names
160+ -- explicit names
142 _ -> let (t', _) = updateSolved' xs t in
161 _ -> let (t', _) = updateSolved' xs t in
143 (subst n v t', True)
162 (subst n v t', True)
144 updateSolved' xs tm@(Bind n b t)
163 updateSolved' xs tm@(Bind n b t)
@@ -146,7 +165,7 @@ updateSolvedTerm' xs x = -- updateSolved' xs x where
146 (b', ub) = updateSolvedB' xs b in
165 (b', ub) = updateSolvedB' xs b in
147 if ut || ub then (Bind n b' t', True)
166 if ut || ub then (Bind n b' t', True)
148 else (tm, False)
167 else (tm, False)
149− updateSolved' xs t@(App f a)
168+ updateSolved' xs t@(App f a)
150 = let (f', uf) = updateSolved' xs f
169 = let (f', uf) = updateSolved' xs f
151 (a', ua) = updateSolved' xs a in
170 (a', ua) = updateSolved' xs a in
152 if uf || ua then (App f' a', True)
171 if uf || ua then (App f' a', True)
@@ -176,10 +195,14 @@ updateSolvedTerm' xs x = -- updateSolved' xs x where
176 noneOfB ns b = noneOf ns (binderTy b)
195 noneOfB ns b = noneOf ns (binderTy b)
177 noneOf ns _ = True
196 noneOf ns _ = True
198+-- | Apply solutions to an environment.
199+updateEnv :: [(Name, Term)] -> Env -> Env
179updateEnv [] e = e
200updateEnv [] e = e
180updateEnv ns [] = []
201updateEnv ns [] = []
181updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
202updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
204+-- | Fill out solved holes in a term zipper.
205+updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath
183updateSolvedPath [] t = t
206updateSolvedPath [] t = t
184updateSolvedPath ns Top = Top
207updateSolvedPath ns Top = Top
185updateSolvedPath ns (AppL p r) = AppL (updateSolvedPath ns p) (updateSolvedTerm ns r)
208updateSolvedPath ns (AppL p r) = AppL (updateSolvedPath ns p) (updateSolvedTerm ns r)