@@ -1,8 +1,9 @@
11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
22
3−{- Implements a proof state, some primitive tactics for manipulating
4− proofs, and some high level commands for introducing new theorems,
5− evaluation/checking inside the proof system, etc. --}
3+{- | Implements a proof state, some primitive tactics for manipulating
4+proofs, and some high level commands for introducing new theorems,
5+evaluation/checking inside the proof system, etc.
6+-}
67
78module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,
89 updateSolved, updateSolvedTerm, updateSolvedTerm',
@@ -18,6 +19,7 @@ import Control.Monad.State.Strict
1819import Data.List
1920import Debug.Trace
2021
22+-- | A zipper over terms, in order to efficiently update proof terms.
2123data TermPath = Top
2224 | AppL TermPath Term
2325 | AppR Term TermPath
@@ -25,6 +27,7 @@ data TermPath = Top
2527 | InScope Name (Binder Term) TermPath
2628 deriving Show
2729
30+-- | A zipper over binders, because terms and binders are mutually defined.
2831data BinderPath = Binder (Binder TermPath)
2932 | LetT TermPath Term
3033 | LetV Term TermPath
@@ -32,6 +35,8 @@ data BinderPath = Binder (Binder TermPath)
3235 | GuessV Term TermPath
3336 deriving Show
3437
38+-- | Replace the top of a term path with another term path. In other
39+-- words, "graft" one term path into another.
3540replaceTop :: TermPath -> TermPath -> TermPath
3641replaceTop p Top = p
3742replaceTop 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
4550 replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)
4651replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)
4752
53+-- | Build a term from a zipper, given something to put in the hole.
4854rebuildTerm :: Term -> TermPath -> Term
4955rebuildTerm tm Top = tm
5056rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a
@@ -52,6 +58,7 @@ rebuildTerm tm (AppR f p) = App f (rebuildTerm tm p)
5258rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)
5359rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc
5460
61+-- | Build a binder from a zipper, given something to put in the hole.
5562rebuildBinder :: Term -> BinderPath -> Binder Term
5663rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p
5764rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t
@@ -59,6 +66,9 @@ rebuildBinder tm (LetV v p) = Let v (rebuildTerm tm p)
5966rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t
6067rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)
6168
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.
6272findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
6373findHole n env t = fh' env Top t where
6474 fh' env path tm@(Bind x h sc)
@@ -80,7 +90,7 @@ findHole n env t = fh' env Top t where
8090 fhB env path b
8191 | Just (p, env', tm) <- fh' env path (binderTy b)
8292 = Just (Binder (fmap (\_ -> p) b), env', tm)
83− fhB _ _ _ = Nothing
93+ fhB _ _ _ = Nothing
8494
8595data ProofTerm = PT { -- wholeterm :: Term,
8696 path :: TermPath,
@@ -92,13 +102,17 @@ data ProofTerm = PT { -- wholeterm :: Term,
92102type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
93103type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
94104
105+-- | Refocus the proof term zipper on a particular hole, if it
106+-- exists. If not, return the original proof term.
95107refocus :: Hole -> ProofTerm -> ProofTerm
96108refocus h t = let res = refocus' h t in res
97109-- trace ("OLD: " ++ show t ++ "\n" ++
98110-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res
99111refocus' (Just n) pt@(PT path env tm ups)
112+ -- First look for the hole in the proof term as-is
100113 | Just (p', env', tm') <- findHole n env tm
101114 = PT (replaceTop p' path) env' tm' ups
115+ -- Next apply the updates, and look for the hole in the resulting term
102116 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))
103117 = PT p' env' tm' []
104118 | otherwise = pt
@@ -118,27 +132,32 @@ same :: Eq a => Maybe a -> a -> Bool
118132same Nothing n = True
119133same (Just x) n = x == n
120134
135+-- | Is a particular binder a hole or a guess?
121136hole :: Binder b -> Bool
122137hole (Hole _) = True
123138hole (Guess _ _) = True
124139hole _ = False
125140
126−updateSolvedTerm :: [(Name, Term)] -> Term -> Term
141+-- | Given a list of solved holes, fill out the solutions in a term
142+updateSolvedTerm :: [(Name, Term)] -> Term -> Term
127143updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x
128144
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)
129149updateSolvedTerm' [] x = (x, False)
130−updateSolvedTerm' xs x = -- updateSolved' xs x where
131−-- This version below saves allocations, because it doesn't need to reallocate
132−-- the term if there are no updates to do.
133−-- 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 :).
135− updateSolved' xs x where
150+updateSolvedTerm' xs x = updateSolved' xs x where
151+ -- This version below saves allocations, because it doesn't need to reallocate
152+ -- the term if there are no updates to do.
153+ -- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is
154+ -- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).
136155 updateSolved' [] x = (x, False)
137156 updateSolved' xs (Bind n (Hole ty) t)
138− | Just v <- lookup n xs
157+ | Just v <- lookup n xs
139158 = case xs of
140159 [_] -> (subst n v t, True) -- some may be Vs! Can't assume
141− -- explicit names
160+ -- explicit names
142161 _ -> let (t', _) = updateSolved' xs t in
143162 (subst n v t', True)
144163 updateSolved' xs tm@(Bind n b t)
@@ -146,7 +165,7 @@ updateSolvedTerm' xs x = -- updateSolved' xs x where
146165 (b', ub) = updateSolvedB' xs b in
147166 if ut || ub then (Bind n b' t', True)
148167 else (tm, False)
149− updateSolved' xs t@(App f a)
168+ updateSolved' xs t@(App f a)
150169 = let (f', uf) = updateSolved' xs f
151170 (a', ua) = updateSolved' xs a in
152171 if uf || ua then (App f' a', True)
@@ -176,10 +195,14 @@ updateSolvedTerm' xs x = -- updateSolved' xs x where
176195 noneOfB ns b = noneOf ns (binderTy b)
177196 noneOf ns _ = True
178197
198+-- | Apply solutions to an environment.
199+updateEnv :: [(Name, Term)] -> Env -> Env
179200updateEnv [] e = e
180201updateEnv ns [] = []
181202updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
182203
204+-- | Fill out solved holes in a term zipper.
205+updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath
183206updateSolvedPath [] t = t
184207updateSolvedPath ns Top = Top
185208updateSolvedPath ns (AppL p r) = AppL (updateSolvedPath ns p) (updateSolvedTerm ns r)