a9dd2e4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Lift out proof term into a separate module

This should make it easier to experiment with alternative (hopefully more efficient) representations

commita9dd2e4b6c3406c1ed987537de420e8a89a9c017 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 31 Jul 2014, 20:42 (12 years ago) parent382542a

4 files changed+161−118

compare with master

unifiedsplit

idris.cabal+1 src/Idris/Core/Elaborate.hs+5−16 src/Idris/Core/ProofState.hs+25−102 src/Idris/Core/ProofTerm.hs+130

idris.cabal+1

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

551551 , Idris.Core.Evaluate

552552 , Idris.Core.Execute

553553 , Idris.Core.ProofState

554+ , Idris.Core.ProofTerm

554555 , Idris.Core.TC

555556 , Idris.Core.TT

556557 , Idris.Core.Typecheck

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

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

1212 module Idris.Core.ProofState) where

1313

1414import Idris.Core.ProofState

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

1516import Idris.Core.TT

1617import Idris.Core.Evaluate

1718import Idris.Core.Typecheck

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

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

129130 return $! (a, str)

130131

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−

135132-- | Modify the auxiliary state

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

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

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

190187-- get the proof term

191188get_term :: Elab' aux Term

192189get_term = do ES p _ _ <- get

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

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

194191

195192-- get the proof term

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

197194update_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))) }

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

200197

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

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

271268unique_hole' reusable n

272269 = do ES p _ _ <- get

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

274− bound_in (ptype (fst p))

271+ bound_in_term (ptype (fst p))

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

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

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

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

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

281278 _ -> return $! ()

282279 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 _ = []

291280

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

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

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

429418qed :: Elab' aux Term

430419qed = do processTactic' QED

431420 ES p _ _ <- get

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

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

433422

434423undo :: Elab' aux ()

435424undo = processTactic' Undo

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

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

1212import Idris.Core.Evaluate

1313import Idris.Core.TT

1414import Idris.Core.Unify

15+import Idris.Core.ProofTerm

1516

1617import Control.Monad.State.Strict

1718import Control.Applicative hiding (empty)

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

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

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

2728 nextname :: Int, -- name supply

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

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

2930 ptype :: Type, -- original goal

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

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

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

4344 while_elaborating :: [FailContext]

4445 }

4546

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

47− goalType :: Binder Term

48− }

49−

5047data Tactic = Attack

5148 | Claim Name Raw

5249 | Reorder Name

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

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

142139 nest nestingSize (prettyPs env bs))

143140

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−

151141holeName i = sMN i "hole"

152142

153143qshow :: Fails -> String

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

165155 " in " ++ show env ++

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

167157 ++ "\n"

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

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

169159 ) $

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

171161 OK u -> traceWhen (unifylog ps)

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

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

291281newProof n ctxt ty = let h = holeName 0

292282 ty' = vToP ty in

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

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

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

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

295285 Nothing [] []

296286 [] []

297287 Nothing ctxt "" False False []

298288

299289type TState = ProofState -- [TacticAction])

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

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

290+type RunTactic = RunTactic' TState

302291

303292envAtFocus :: ProofState -> TC Env

304293envAtFocus ps

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

310299goalAtFocus ps

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

312301 return (goalType g)

313− | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (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)

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

330303

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

332305tactic h f = do ps <- get

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

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

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

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

371309

372310computeLet :: Context -> Name -> Term -> Term

373311computeLet ctxt n tm = cl [] tm where

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

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

698636 let scr = last $ tail args'

699637 let indxnames = makeIndexNames indicies

700− currentNames <- query $ allTTNames . pterm

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

701639 let tmnm = case tm of

702640 Var nm -> uniqueNameCtxt ctxt nm currentNames

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

704642 let tmvar = P Bound tmnm tmt'

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

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

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

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

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

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

801739 holes ps \\ map fst unify })

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

803− return (updateSolved unify tm)

741+ return (updateSolvedTerm unify tm)

804742

805743dropGiven du [] hs = []

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

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

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

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

823761

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−

841762updateEnv [] e = e

842763updateEnv 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

844765

845766updateError [] err = err

846767updateError 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)

848769updateError ns (ElaboratingArg f a env e)

849770 = ElaboratingArg f a env (updateError ns e)

850771updateError 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

852773updateError ns e = e

853774

854775solveInProblems x val [] = []

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

868789updateNotunified [] nu = nu

869790updateNotunified ns nu = up nu where

870791 up [] = []

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

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

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

873794

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

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

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

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

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

881− let x' = updateSolved ns x

882− y' = updateSolved ns y

802+ let x' = updateSolvedTerm ns x

803+ y' = updateSolvedTerm ns y

883804 err' = updateError ns err

884805 env' = updateEnv ns env in

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

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

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

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

897818 | all || um == Match =

898− let x' = updateSolved ns x

899− y' = updateSolved ns y

819+ let x' = updateSolvedTerm ns x

820+ y' = updateSolvedTerm ns y

900821 err' = updateError ns err

901822 env' = updateEnv ns env in

902823 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

909830

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

911832processTactic 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)

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

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

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

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

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

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

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

918839processTactic Undo ps = case previous ps of

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

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

921842processTactic EndUnify ps

922843 = let (h, ns_in) = unified ps

923844 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

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

926847 (injective ps) (holes ps)

927848 (map fst (notunified ps))

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

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

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

943864processTactic (ComputeLet n) ps

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

865+ = return (ps { pterm = mkProofTerm $

866+ computeLet (context ps) n

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

945868processTactic UnifyProblems ps

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

947870 (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+