@@ -18,20 +18,100 @@ import Control.Monad.State.Strict
1818import Data.List
1919import Debug.Trace
2020
21−newtype ProofTerm = PT Term
21+data TermPath = Top
22+ | AppL TermPath Term
23+ | AppR Term TermPath
24+ | InBind Name BinderPath Term
25+ | InScope Name (Binder Term) TermPath
26+ deriving Show
27+
28+data BinderPath = Binder (Binder TermPath)
29+ | LetT TermPath Term
30+ | LetV Term TermPath
31+ | GuessT TermPath Term
32+ | GuessV Term TermPath
33+ deriving Show
34+
35+replaceTop :: TermPath -> TermPath -> TermPath
36+replaceTop p Top = p
37+replaceTop p (AppL l t) = AppL (replaceTop p l) t
38+replaceTop p (AppR t r) = AppR t (replaceTop p r)
39+replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc
40+ where
41+ replaceTopB p (Binder b) = Binder (fmap (replaceTop p) b)
42+ replaceTopB p (LetT t v) = LetT (replaceTop p t) v
43+ replaceTopB p (LetV t v) = LetV t (replaceTop p v)
44+ replaceTopB p (GuessT t v) = GuessT (replaceTop p t) v
45+ replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)
46+replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)
47+
48+rebuildTerm :: Term -> TermPath -> Term
49+rebuildTerm tm Top = tm
50+rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a
51+rebuildTerm tm (AppR f p) = App f (rebuildTerm tm p)
52+rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)
53+rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc
54+
55+rebuildBinder :: Term -> BinderPath -> Binder Term
56+rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p
57+rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t
58+rebuildBinder tm (LetV v p) = Let v (rebuildTerm tm p)
59+rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t
60+rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)
61+
62+findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
63+findHole n env t = fh' env Top t where
64+ fh' env path tm@(Bind x h sc)
65+ | hole h && n == x = Just (path, env, tm)
66+ fh' env path (App f a)
67+ | Just (p, env', tm) <- fh' env path f = Just (AppL p a, env', tm)
68+ | Just (p, env', tm) <- fh' env path a = Just (AppR f p, env', tm)
69+ fh' env path (Bind x b sc)
70+ | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)
71+ | Just (p, env', tm) <- fh' ((x,b):env) path sc = Just (InScope x b p, env', tm)
72+ fh' _ _ _ = Nothing
73+
74+ fhB env path (Let t v)
75+ | Just (p, env', tm) <- fh' env path t = Just (LetT p v, env', tm)
76+ | Just (p, env', tm) <- fh' env path v = Just (LetV t p, env', tm)
77+ fhB env path (Guess t v)
78+ | Just (p, env', tm) <- fh' env path t = Just (GuessT p v, env', tm)
79+ | Just (p, env', tm) <- fh' env path v = Just (GuessV t p, env', tm)
80+ fhB env path b
81+ | Just (p, env', tm) <- fh' env path (binderTy b)
82+ = Just (Binder (fmap (\_ -> p) b), env', tm)
83+ fhB _ _ _ = Nothing
84+
85+data ProofTerm = PT { -- wholeterm :: Term,
86+ path :: TermPath,
87+ subterm_env :: Env,
88+ subterm :: Term }
89+ deriving Show
2290
2391type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
2492type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
2593
94+refocus :: Hole -> ProofTerm -> ProofTerm
95+refocus h t = let res = refocus' h t in res
96+-- trace ("OLD: " ++ show t ++ "\n" ++
97+-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res
98+refocus' (Just n) pt@(PT path env tm)
99+ | Just (p', env', tm') <- findHole n env tm
100+ = PT (replaceTop p' path) env' tm'
101+ | Just (p', env', tm') <- findHole n [] (rebuildTerm tm path)
102+ = PT p' env' tm'
103+ | otherwise = pt
104+refocus' _ pt = pt
105+
26106data Goal = GD { premises :: Env,
27107 goalType :: Binder Term
28108 }
29109
30110mkProofTerm :: Term -> ProofTerm
31−mkProofTerm tm = PT tm
111+mkProofTerm tm = PT Top [] tm
32112
33113getProofTerm :: ProofTerm -> Term
34−getProofTerm (PT tm) = tm
114+getProofTerm (PT path _ sub) = rebuildTerm sub path
35115
36116same Nothing n = True
37117same (Just x) n = x == n
@@ -57,11 +137,40 @@ updateSolvedTerm xs x = updateSolved' xs x where
57137 | Just v <- lookup n xs = v
58138 updateSolved' xs t = t
59139
140+updateEnv [] e = e
141+updateEnv ns [] = []
142+updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
143+
144+updateSolvedPath [] t = t
145+updateSolvedPath ns Top = Top
146+updateSolvedPath ns (AppL p r) = AppL p (updateSolvedTerm ns r)
147+updateSolvedPath ns (AppR l p) = AppR (updateSolvedTerm ns l) p
148+updateSolvedPath ns (InBind n b sc)
149+ = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)
150+ where
151+ updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)
152+ updateSolvedPathB (LetT p v) = LetT (updateSolvedPath ns p) (updateSolvedTerm ns v)
153+ updateSolvedPathB (LetV v p) = LetV (updateSolvedTerm ns v) (updateSolvedPath ns p)
154+ updateSolvedPathB (GuessT p v) = GuessT (updateSolvedPath ns p) (updateSolvedTerm ns v)
155+ updateSolvedPathB (GuessV v p) = GuessV (updateSolvedTerm ns v) (updateSolvedPath ns p)
156+updateSolvedPath ns (InScope n (Hole ty) t)
157+ | Just v <- lookup n ns = case ns of
158+ [_] -> updateSolvedPath [(n,v)] t
159+ _ -> updateSolvedPath ns $
160+ updateSolvedPath [(n,v)] t
161+updateSolvedPath ns (InScope n b sc)
162+ = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)
163+
60164updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
61−updateSolved xs (PT x) = PT (updateSolvedTerm xs x)
165+updateSolved xs pt@(PT path env sub)
166+ = PT (updateSolvedPath xs path)
167+ (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))
168+ (updateSolvedTerm xs sub)
62169
63170goal :: Hole -> ProofTerm -> TC Goal
64−goal h (PT tm) = g [] tm where
171+goal h pt@(PT path env sub) = do let tm = rebuildTerm sub path
172+ ginf <- g [] (rebuildTerm sub path)
173+ return ginf where
65174 g env (Bind n b@(Guess _ _) sc)
66175 | same h n = return $ GD env b
67176 | otherwise
@@ -78,8 +187,10 @@ goal h (PT tm) = g [] tm where
78187
79188atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->
80189 StateT a TC (ProofTerm, Bool)
81−atHole h f c e (PT t) = do (tm, u) <- atH f c e t
82− return (PT tm, u)
190+atHole h f c e pt -- @(PT path env sub)
191+ = do let pt'@(PT path env sub) = refocus h pt
192+ (tm, u) <- atH f c env sub
193+ return (PT path env tm, u)
83194 where
84195 updated o = do o' <- o
85196 return (o', True)
@@ -117,7 +228,7 @@ atHole h f c e (PT t) = do (tm, u) <- atH f c e t
117228 return (t { binderTy = ty' }, u)
118229
119230bound_in :: ProofTerm -> [Name]
120−bound_in (PT tm) = bound_in_term tm
231+bound_in (PT path _ tm) = bound_in_term (rebuildTerm tm path)
121232
122233bound_in_term :: Term -> [Name]
123234bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc