a9dd2e4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Lift out proof term into a separate module

a9dd2e4Edwin Brady12 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -551,6 +551,7 @@ Library

551 , Idris.Core.Evaluate

552 , Idris.Core.Execute

553 , Idris.Core.ProofState

554+ , Idris.Core.ProofTerm

554 , Idris.Core.TC

555 , Idris.Core.TC

555 , Idris.Core.TT

556 , Idris.Core.TT

556 , Idris.Core.Typecheck

557 , Idris.Core.Typecheck

src/Idris/Core/Elaborate.hs+5−16

@@ -12,6 +12,7 @@ module Idris.Core.Elaborate(module Idris.Core.Elaborate,

12 module Idris.Core.ProofState) where

14import Idris.Core.ProofState

15+import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term)

15import Idris.Core.TT

16import Idris.Core.TT

16import Idris.Core.Evaluate

17import Idris.Core.Evaluate

17import Idris.Core.Typecheck

18import Idris.Core.Typecheck

@@ -128,10 +129,6 @@ elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty

128 (a, ES ps' str _) <- runElab d elab ps

129 (a, ES ps' str _) <- runElab d elab ps

129 return $! (a, str)

130 return $! (a, str)

130

131

131−force_term :: Elab' aux ()

132−force_term = do ES (ps, a) l p <- get

133− put (ES (ps { pterm = force (pterm ps) }, a) l p)

134−

135-- | Modify the auxiliary state

132-- | Modify the auxiliary state

136updateAux :: (aux -> aux) -> Elab' aux ()

133updateAux :: (aux -> aux) -> Elab' aux ()

137updateAux f = do ES (ps, a) l p <- get

134updateAux f = do ES (ps, a) l p <- get

@@ -190,12 +187,12 @@ set_context ctxt = do ES (p, a) logs prev <- get

190-- get the proof term

187-- get the proof term

191get_term :: Elab' aux Term

188get_term :: Elab' aux Term

192get_term = do ES p _ _ <- get

189get_term = do ES p _ _ <- get

193− return $! (pterm (fst p))

190+ return $! (getProofTerm (pterm (fst p)))

194

191

195-- get the proof term

192-- get the proof term

196update_term :: (Term -> Term) -> Elab' aux ()

193update_term :: (Term -> Term) -> Elab' aux ()

197update_term f = do ES (p,a) logs prev <- get

194update_term f = do ES (p,a) logs prev <- get

198− let p' = p { pterm = f (pterm p) }

195+ let p' = p { pterm = mkProofTerm (f (getProofTerm (pterm p))) }

199 put (ES (p', a) logs prev)

196 put (ES (p', a) logs prev)

200

197

201-- get the local context at the currently in focus hole

198-- get the local context at the currently in focus hole

@@ -271,7 +268,7 @@ unique_hole' :: Bool -> Name -> Elab' aux Name

271unique_hole' reusable n

268unique_hole' reusable n

272 = do ES p _ _ <- get

269 = do ES p _ _ <- get

273 let bs = bound_in (pterm (fst p)) ++

270 let bs = bound_in (pterm (fst p)) ++

274− bound_in (ptype (fst p))

271+ bound_in_term (ptype (fst p))

275 let nouse = holes (fst p) ++ bs ++ dontunify (fst p) ++ usedns (fst p)

272 let nouse = holes (fst p) ++ bs ++ dontunify (fst p) ++ usedns (fst p)

276 n' <- return $! uniqueNameCtxt (context (fst p)) n nouse

273 n' <- return $! uniqueNameCtxt (context (fst p)) n nouse

277 ES (p, a) s u <- get

274 ES (p, a) s u <- get

@@ -280,14 +277,6 @@ unique_hole' reusable n

280 put (ES (p { nextname = i + 1 }, a) s u)

277 put (ES (p { nextname = i + 1 }, a) s u)

281 _ -> return $! ()

278 _ -> return $! ()

282 return $! n'

279 return $! n'

283− where

284− bound_in (Bind n b sc) = n : bi b ++ bound_in sc

285− where

286− bi (Let t v) = bound_in t ++ bound_in v

287− bi (Guess t v) = bound_in t ++ bound_in v

288− bi b = bound_in (binderTy b)

289− bound_in (App f a) = bound_in f ++ bound_in a

290− bound_in _ = []

291

280

292elog :: String -> Elab' aux ()

281elog :: String -> Elab' aux ()

293elog str = do ES p logs prev <- get

282elog str = do ES p logs prev <- get

@@ -429,7 +418,7 @@ reorder_claims n = processTactic' (Reorder n)

429qed :: Elab' aux Term

418qed :: Elab' aux Term

430qed = do processTactic' QED

419qed = do processTactic' QED

431 ES p _ _ <- get

420 ES p _ _ <- get

432− return $! (pterm (fst p))

421+ return $! (getProofTerm (pterm (fst p)))

433

422

434undo :: Elab' aux ()

423undo :: Elab' aux ()

435undo = processTactic' Undo

424undo = processTactic' Undo

src/Idris/Core/ProofState.hs+25−102

@@ -12,6 +12,7 @@ import Idris.Core.Typecheck

12import Idris.Core.Evaluate

13import Idris.Core.TT

14import Idris.Core.Unify

15+import Idris.Core.ProofTerm

16import Control.Monad.State.Strict

17import Control.Monad.State.Strict

17import Control.Applicative hiding (empty)

18import Control.Applicative hiding (empty)

@@ -25,7 +26,7 @@ data ProofState = PS { thname :: Name,

25 holes :: [Name], -- holes still to be solved

26 holes :: [Name], -- holes still to be solved

26 usedns :: [Name], -- used names, don't use again

27 usedns :: [Name], -- used names, don't use again

27 nextname :: Int, -- name supply

28 nextname :: Int, -- name supply

28− pterm :: Term, -- current proof term

29+ pterm :: ProofTerm, -- current proof term

29 ptype :: Type, -- original goal

30 ptype :: Type, -- original goal

30 dontunify :: [Name], -- explicitly given by programmer, leave it

31 dontunify :: [Name], -- explicitly given by programmer, leave it

31 unified :: (Name, [(Name, Term)]),

32 unified :: (Name, [(Name, Term)]),

@@ -43,10 +44,6 @@ data ProofState = PS { thname :: Name,

43 while_elaborating :: [FailContext]

44 while_elaborating :: [FailContext]

44 }

45 }

46−data Goal = GD { premises :: Env,

47− goalType :: Binder Term

48− }

49−

50data Tactic = Attack

47data Tactic = Attack

51 | Claim Name Raw

48 | Claim Name Raw

52 | Reorder Name

49 | Reorder Name

@@ -141,13 +138,6 @@ instance Pretty ProofState OutputAnnotation where

141 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>

138 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>

142 nest nestingSize (prettyPs env bs))

139 nest nestingSize (prettyPs env bs))

143

140

144−same Nothing n = True

145−same (Just x) n = x == n

146−

147−hole (Hole _) = True

148−hole (Guess _ _) = True

149−hole _ = False

150−

151holeName i = sMN i "hole"

141holeName i = sMN i "hole"

152

142

153qshow :: Fails -> String

143qshow :: Fails -> String

@@ -165,7 +155,7 @@ match_unify' ctxt env topx topy =

165 " in " ++ show env ++

155 " in " ++ show env ++

166 "\nHoles: " ++ show (holes ps)

156 "\nHoles: " ++ show (holes ps)

167 ++ "\n"

157 ++ "\n"

168− ++ "\n" ++ show (pterm ps) ++ "\n\n"

158+ ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"

169 ) $

159 ) $

170 case match_unify ctxt env topx topy inj (holes ps) while of

160 case match_unify ctxt env topx topy inj (holes ps) while of

171 OK u -> traceWhen (unifylog ps)

161 OK u -> traceWhen (unifylog ps)

@@ -290,15 +280,14 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

290newProof :: Name -> Context -> Type -> ProofState

280newProof :: Name -> Context -> Type -> ProofState

291newProof n ctxt ty = let h = holeName 0

281newProof n ctxt ty = let h = holeName 0

292 ty' = vToP ty in

282 ty' = vToP ty in

293− PS n [h] [] 1 (Bind h (Hole ty')

283+ PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

294− (P Bound h ty')) ty [] (h, []) []

284+ (P Bound h ty'))) ty [] (h, []) []

295 Nothing [] []

285 Nothing [] []

296 [] []

286 [] []

297 Nothing ctxt "" False False []

287 Nothing ctxt "" False False []

298

288

299type TState = ProofState -- [TacticAction])

289type TState = ProofState -- [TacticAction])

300−type RunTactic = Context -> Env -> Term -> StateT TState TC Term

290+type RunTactic = RunTactic' TState

301−type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

302

291

303envAtFocus :: ProofState -> TC Env

292envAtFocus :: ProofState -> TC Env

304envAtFocus ps

293envAtFocus ps

@@ -310,64 +299,13 @@ goalAtFocus :: ProofState -> TC (Binder Type)

310goalAtFocus ps

299goalAtFocus ps

311 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)

300 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)

312 return (goalType g)

301 return (goalType g)

313− | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (pterm ps)

302+ | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (getProofTerm (pterm ps))

314−

315−goal :: Hole -> Term -> TC Goal

316−goal h tm = g [] tm where

317− g env (Bind n b@(Guess _ _) sc)

318− | same h n = return $ GD env b

319− | otherwise

320− = gb env b `mplus` g ((n, b):env) sc

321− g env (Bind n b sc) | hole b && same h n = return $ GD env b

322− | otherwise

323− = g ((n, b):env) sc `mplus` gb env b

324− g env (App f a) = g env f `mplus` g env a

325− g env t = fail "Can't find hole"

326−

327− gb env (Let t v) = g env v `mplus` g env t

328− gb env (Guess t v) = g env v `mplus` g env t

329− gb env t = g env (binderTy t)

330

303

331tactic :: Hole -> RunTactic -> StateT TState TC ()

304tactic :: Hole -> RunTactic -> StateT TState TC ()

332tactic h f = do ps <- get

305tactic h f = do ps <- get

333− (tm', _) <- atH (context ps) [] (pterm ps)

306+ (tm', _) <- atHole h f (context ps) [] (pterm ps)

334 ps <- get -- might have changed while processing

307 ps <- get -- might have changed while processing

335 put (ps { pterm = tm' })

308 put (ps { pterm = tm' })

336− where

337− updated o = do o' <- o

338− return (o', True)

339−

340− ulift2 c env op a b

341− = do (b', u) <- atH c env b

342− if u then return (op a b', True)

343− else do (a', u) <- atH c env a

344− return (op a' b', u)

345−

346− -- Search the things most likely to contain the binding first!

347−

348− atH :: Context -> Env -> Term -> StateT TState TC (Term, Bool)

349− atH c env binder@(Bind n b@(Guess t v) sc)

350− | same h n = updated (f c env binder)

351− | otherwise

352− = do -- binder first

353− (b', u) <- ulift2 c env Guess t v

354− if u then return (Bind n b' sc, True)

355− else do (sc', u) <- atH c ((n, b) : env) sc

356− return (Bind n b' sc', u)

357− atH c env binder@(Bind n b sc)

358− | hole b && same h n = updated (f c env binder)

359− | otherwise -- scope first

360− = do (sc', u) <- atH c ((n, b) : env) sc

361− if u then return (Bind n b sc', True)

362− else do (b', u) <- atHb c env b

363− return (Bind n b' sc', u)

364− atH c env (App f a) = ulift2 c env App f a

365− atH c env t = return (t, False)

366−

367− atHb c env (Let t v) = ulift2 c env Let t v

368− atHb c env (Guess t v) = ulift2 c env Guess t v

369− atHb c env t = do (ty', u) <- atH c env (binderTy t)

370− return (t { binderTy = ty' }, u)

371

309

372computeLet :: Context -> Name -> Term -> Term

310computeLet :: Context -> Name -> Term -> Term

373computeLet ctxt n tm = cl [] tm where

311computeLet ctxt n tm = cl [] tm where

@@ -697,13 +635,13 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

697 let indxargs = drop (length restargs - length indicies) $ restargs

635 let indxargs = drop (length restargs - length indicies) $ restargs

698 let scr = last $ tail args'

636 let scr = last $ tail args'

699 let indxnames = makeIndexNames indicies

637 let indxnames = makeIndexNames indicies

700− currentNames <- query $ allTTNames . pterm

638+ currentNames <- query $ allTTNames . getProofTerm . pterm

701 let tmnm = case tm of

639 let tmnm = case tm of

702 Var nm -> uniqueNameCtxt ctxt nm currentNames

640 Var nm -> uniqueNameCtxt ctxt nm currentNames

703 _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames

641 _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames

704 let tmvar = P Bound tmnm tmt'

642 let tmvar = P Bound tmnm tmt'

705 prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)

643 prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)

706− consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (pterm ps)) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (pterm ps))) consargs)

644+ consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)

707 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))

645 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))

708 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

646 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

709 action (\ps -> ps {holes = holes ps \\ [x]})

647 action (\ps -> ps {holes = holes ps \\ [x]})

@@ -800,7 +738,7 @@ solve_unified ctxt env tm =

800 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $

738 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $

801 holes ps \\ map fst unify })

739 holes ps \\ map fst unify })

802 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

740 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

803− return (updateSolved unify tm)

741+ return (updateSolvedTerm unify tm)

804

742

805dropGiven du [] hs = []

743dropGiven du [] hs = []

806dropGiven du ((n, P Bound t ty) : us) hs

744dropGiven du ((n, P Bound t ty) : us) hs

@@ -821,26 +759,9 @@ keepGiven du (u@(n, _) : us) hs

821 | n `elem` du = u : keepGiven du us hs

759 | n `elem` du = u : keepGiven du us hs

822keepGiven du (u : us) hs = keepGiven du us hs

760keepGiven du (u : us) hs = keepGiven du us hs

823

761

824−updateSolved :: [(Name, Term)] -> Term -> Term

825−updateSolved xs x = updateSolved' xs x

826−updateSolved' [] x = x

827−updateSolved' xs (Bind n (Hole ty) t)

828− | Just v <- lookup n xs

829− = case xs of

830− [_] -> substV v $ psubst n v t -- some may be Vs! Can't assume

831− -- explicit names

832− _ -> substV v $ psubst n v (updateSolved' xs t)

833−updateSolved' xs (Bind n b t)

834− | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)

835−updateSolved' xs (App f a)

836− = App (updateSolved' xs f) (updateSolved' xs a)

837−updateSolved' xs (P _ n@(MN _ _) _)

838− | Just v <- lookup n xs = v

839−updateSolved' xs t = t

840−

841updateEnv [] e = e

762updateEnv [] e = e

842updateEnv ns [] = []

763updateEnv ns [] = []

843−updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env

764+updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

844

765

845updateError [] err = err

766updateError [] err = err

846updateError ns (At f e) = At f (updateError ns e)

767updateError ns (At f e) = At f (updateError ns e)

@@ -848,7 +769,7 @@ updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

848updateError ns (ElaboratingArg f a env e)

769updateError ns (ElaboratingArg f a env e)

849 = ElaboratingArg f a env (updateError ns e)

770 = ElaboratingArg f a env (updateError ns e)

850updateError ns (CantUnify b l r e xs sc)

771updateError ns (CantUnify b l r e xs sc)

851− = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc

772+ = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc

852updateError ns e = e

773updateError ns e = e

853

774

854solveInProblems x val [] = []

775solveInProblems x val [] = []

@@ -868,7 +789,7 @@ mergeNotunified env ns = mnu ns [] [] where

868updateNotunified [] nu = nu

789updateNotunified [] nu = nu

869updateNotunified ns nu = up nu where

790updateNotunified ns nu = up nu where

870 up [] = []

791 up [] = []

871− up ((n, t) : nus) = let t' = updateSolved ns t in

792+ up ((n, t) : nus) = let t' = updateSolvedTerm ns t in

872 ((n, t') : up nus)

793 ((n, t') : up nus)

873

794

874-- FIXME: Why not just pass the whole proof state?

795-- FIXME: Why not just pass the whole proof state?

@@ -878,8 +799,8 @@ updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [

878updateProblems ctxt ns ps inj holes usupp = up ns ps where

799updateProblems ctxt ns ps inj holes usupp = up ns ps where

879 up ns [] = (ns, [])

800 up ns [] = (ns, [])

880 up ns ((x, y, env, err, while, um) : ps) =

801 up ns ((x, y, env, err, while, um) : ps) =

881− let x' = updateSolved ns x

802+ let x' = updateSolvedTerm ns x

882− y' = updateSolved ns y

803+ y' = updateSolvedTerm ns y

883 err' = updateError ns err

804 err' = updateError ns err

884 env' = updateEnv ns env in

805 env' = updateEnv ns env in

885-- trace ("Updating " ++ show (x',y')) $

806-- trace ("Updating " ++ show (x',y')) $

@@ -895,8 +816,8 @@ matchProblems all ns ctxt ps inj holes = up ns ps where

895 up ns [] = (ns, [])

816 up ns [] = (ns, [])

896 up ns ((x, y, env, err, while, um) : ps)

817 up ns ((x, y, env, err, while, um) : ps)

897 | all || um == Match =

818 | all || um == Match =

898− let x' = updateSolved ns x

819+ let x' = updateSolvedTerm ns x

899− y' = updateSolved ns y

820+ y' = updateSolvedTerm ns y

900 err' = updateError ns err

821 err' = updateError ns err

901 env' = updateEnv ns env in

822 env' = updateEnv ns env in

902 case match_unify ctxt env' x' y' inj holes while of

823 case match_unify ctxt env' x' y' inj holes while of

@@ -909,19 +830,19 @@ matchProblems all ns ctxt ps inj holes = up ns ps where

909

830

910processTactic :: Tactic -> ProofState -> TC (ProofState, String)

831processTactic :: Tactic -> ProofState -> TC (ProofState, String)

911processTactic QED ps = case holes ps of

832processTactic QED ps = case holes ps of

912− [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)

833+ [] -> do let tm = {- normalise (context ps) [] -} getProofTerm (pterm ps)

913 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm

834 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm

914− return (ps { done = True, pterm = tm' },

835+ return (ps { done = True, pterm = mkProofTerm tm' },

915 "Proof complete: " ++ showEnv [] tm')

836 "Proof complete: " ++ showEnv [] tm')

916 _ -> fail "Still holes to fill."

837 _ -> fail "Still holes to fill."

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

838+processTactic ProofState ps = return (ps, showEnv [] (getProofTerm (pterm ps)))

918processTactic Undo ps = case previous ps of

839processTactic Undo ps = case previous ps of

919 Nothing -> Error . Msg $ "Nothing to undo."

840 Nothing -> Error . Msg $ "Nothing to undo."

920 Just pold -> return (pold, "")

841 Just pold -> return (pold, "")

921processTactic EndUnify ps

842processTactic EndUnify ps

922 = let (h, ns_in) = unified ps

843 = let (h, ns_in) = unified ps

923 ns = dropGiven (dontunify ps) ns_in (holes ps)

844 ns = dropGiven (dontunify ps) ns_in (holes ps)

924− ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

845+ ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns

925 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

846 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

926 (injective ps) (holes ps)

847 (injective ps) (holes ps)

927 (map fst (notunified ps))

848 (map fst (notunified ps))

@@ -941,7 +862,9 @@ processTactic (Reorder n) ps

941 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

862 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

942 return (ps' { previous = Just ps, plog = "" }, plog ps')

863 return (ps' { previous = Just ps, plog = "" }, plog ps')

943processTactic (ComputeLet n) ps

864processTactic (ComputeLet n) ps

865+ = return (ps { pterm = mkProofTerm $

944− = return (ps { pterm = computeLet (context ps) n (pterm ps) }, "")

866+ computeLet (context ps) n

867+ (getProofTerm (pterm ps)) }, "")

945processTactic UnifyProblems ps

868processTactic UnifyProblems ps

946 = let (ns', probs') = updateProblems (context ps) []

869 = let (ns', probs') = updateProblems (context ps) []

947 (problems ps)

870 (problems ps)

src/Idris/Core/ProofTerm.hsnew file+130

@@ -0,0 +1,130 @@

1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

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. --}

7+module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,

8+ updateSolved, updateSolvedTerm,

9+ bound_in, bound_in_term,

10+ Hole, RunTactic',

11+ goal, atHole) where

12+

13+import Idris.Core.Typecheck

14+import Idris.Core.Evaluate

15+import Idris.Core.TT

16+

17+import Control.Monad.State.Strict

18+import Data.List

19+import Debug.Trace

20+

21+newtype ProofTerm = PT Term

22+

23+type RunTactic' a = Context -> Env -> Term -> StateT a TC Term

24+type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

25+

26+data Goal = GD { premises :: Env,

27+ goalType :: Binder Term

28+ }

29+

30+mkProofTerm :: Term -> ProofTerm

31+mkProofTerm tm = PT tm

32+

33+getProofTerm :: ProofTerm -> Term

34+getProofTerm (PT tm) = tm

35+

36+same Nothing n = True

37+same (Just x) n = x == n

38+

39+hole (Hole _) = True

40+hole (Guess _ _) = True

41+hole _ = False

42+

43+updateSolvedTerm :: [(Name, Term)] -> Term -> Term

44+updateSolvedTerm xs x = updateSolved' xs x where

45+ updateSolved' [] x = x

46+ updateSolved' xs (Bind n (Hole ty) t)

47+ | Just v <- lookup n xs

48+ = case xs of

49+ [_] -> substV v $ psubst n v t -- some may be Vs! Can't assume

50+ -- explicit names

51+ _ -> substV v $ psubst n v (updateSolved' xs t)

52+ updateSolved' xs (Bind n b t)

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

54+ updateSolved' xs (App f a)

55+ = App (updateSolved' xs f) (updateSolved' xs a)

56+ updateSolved' xs (P _ n@(MN _ _) _)

57+ | Just v <- lookup n xs = v

58+ updateSolved' xs t = t

59+

60+updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm

61+updateSolved xs (PT x) = PT (updateSolvedTerm xs x)

62+

63+goal :: Hole -> ProofTerm -> TC Goal

64+goal h (PT tm) = g [] tm where

65+ g env (Bind n b@(Guess _ _) sc)

66+ | same h n = return $ GD env b

67+ | otherwise

68+ = gb env b `mplus` g ((n, b):env) sc

69+ g env (Bind n b sc) | hole b && same h n = return $ GD env b

70+ | otherwise

71+ = g ((n, b):env) sc `mplus` gb env b

72+ g env (App f a) = g env f `mplus` g env a

73+ g env t = fail "Can't find hole"

74+

75+ gb env (Let t v) = g env v `mplus` g env t

76+ gb env (Guess t v) = g env v `mplus` g env t

77+ gb env t = g env (binderTy t)

78+

79+atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->

80+ 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)

83+ where

84+ updated o = do o' <- o

85+ return (o', True)

86+

87+ ulift2 f c env op a b

88+ = do (b', u) <- atH f c env b

89+ if u then return (op a b', True)

90+ else do (a', u) <- atH f c env a

91+ return (op a' b', u)

92+

93+ -- Search the things most likely to contain the binding first!

94+

95+ atH :: RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)

96+ atH f c env binder@(Bind n b@(Guess t v) sc)

97+ | same h n = updated (f c env binder)

98+ | otherwise

99+ = do -- binder first

100+ (b', u) <- ulift2 f c env Guess t v

101+ if u then return (Bind n b' sc, True)

102+ else do (sc', u) <- atH f c ((n, b) : env) sc

103+ return (Bind n b' sc', u)

104+ atH f c env binder@(Bind n b sc)

105+ | hole b && same h n = updated (f c env binder)

106+ | otherwise -- scope first

107+ = do (sc', u) <- atH f c ((n, b) : env) sc

108+ if u then return (Bind n b sc', True)

109+ else do (b', u) <- atHb f c env b

110+ return (Bind n b' sc', u)

111+ atH tac c env (App f a) = ulift2 tac c env App f a

112+ atH tac c env t = return (t, False)

113+

114+ atHb f c env (Let t v) = ulift2 f c env Let t v

115+ atHb f c env (Guess t v) = ulift2 f c env Guess t v

116+ atHb f c env t = do (ty', u) <- atH f c env (binderTy t)

117+ return (t { binderTy = ty' }, u)

118+

119+bound_in :: ProofTerm -> [Name]

120+bound_in (PT tm) = bound_in_term tm

121+

122+bound_in_term :: Term -> [Name]

123+bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc

124+ where

125+ bi (Let t v) = bound_in_term t ++ bound_in_term v

126+ bi (Guess t v) = bound_in_term t ++ bound_in_term v

127+ bi b = bound_in_term (binderTy b)

128+bound_in_term (App f a) = bound_in_term f ++ bound_in_term a

129+bound_in_term _ = []

130+