ab36099 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use a zipper-like proof state

ab36099Edwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+1−4

compare with master

unifiedsplit

@@ -1714,7 +1714,7 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

1714 (nub (concatMap (ni env) (map snd os))

1715 \\ nub (concatMap (ni env) (map fst os)))

1716 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1717− ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1717+ ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc

1718 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

1719 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1720 ni env (PTyped l r) = ni env l ++ ni env r

@@ -1728,9 +1728,6 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

1728 ni env (PNoImplicits tm) = ni env tm

1729 ni env _ = []

1730

1731− niTacImp env (TacImp _ _ scr) = ni env scr

1732− niTacImp _ _ = []

1733−

1734-- Return names which are free in the given term.

1731-- Return names which are free in the given term.

1735namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

1732namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

1736namesIn uvars ist tm = nub $ ni [] tm

1733namesIn uvars ist tm = nub $ ni [] tm

src/Idris/Core/Elaborate.hs+1

@@ -628,6 +628,7 @@ simple_app fun arg appstr =

628arg :: Name -> Name -> Elab' aux ()

629arg n tyhole = do ty <- unique_hole tyhole

630 claim ty RType

631+ movelast ty

631 forall n (Var ty)

632 forall n (Var ty)

632

633

633-- try a tactic, if it adds any unification problem, return an error

634-- try a tactic, if it adds any unification problem, return an error

src/Idris/Core/ProofState.hs+5−3

@@ -216,9 +216,11 @@ unify' ctxt env topx topy =

216-- ++ show (pterm ps)

217 ++ "\n----------") $

218 do let (h, ns) = unified ps

219+ -- solve in results (maybe unify should do this itself...)

220+ let u' = map (\(n, sol) -> (n, updateSolvedTerm u sol)) u

219 -- if a metavar has multiple solutions, make a new unification

221 -- if a metavar has multiple solutions, make a new unification

220 -- problem for each.

222 -- problem for each.

221− uns <- mergeSolutions env (u ++ ns)

223+ uns <- mergeSolutions env (u' ++ ns)

222 ps <- get

224 ps <- get

223 let (ns', probs') = updateProblems (context ps) uns

225 let (ns', probs') = updateProblems (context ps) uns

224 (fails ++ problems ps)

226 (fails ++ problems ps)

@@ -550,7 +552,7 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

550forall n ty ctxt env _ = fail "Can't pi bind here"

552forall n ty ctxt env _ = fail "Can't pi bind here"

551

553

552patvar :: Name -> RunTactic

554patvar :: Name -> RunTactic

553−patvar n ctxt env (Bind x (Hole t) sc) =

555+patvar n ctxt env (Bind x (Hole t) sc) =

554 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $

556 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $

555 holes ps \\ [x],

557 holes ps \\ [x],

556 solved = Just (x, P Bound n t),

558 solved = Just (x, P Bound n t),

@@ -900,7 +902,7 @@ processTactic t ps

900 = case solved ps' of

902 = case solved ps' of

901 Just s -> traceWhen (unifylog ps')

903 Just s -> traceWhen (unifylog ps')

902 ("SOLVED " ++ show s) $

904 ("SOLVED " ++ show s) $

903− updateProblems (context ps')

905+ updateProblems (context ps')

904 [s] (problems ps')

906 [s] (problems ps')

905 (injective ps')

907 (injective ps')

906 (holes ps')

908 (holes ps')

src/Idris/Core/ProofTerm.hs+119−8

@@ -18,20 +18,100 @@ import Control.Monad.State.Strict

18import Data.List

19import Debug.Trace

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+

21−newtype ProofTerm = PT Term

85+data ProofTerm = PT { -- wholeterm :: Term,

86+ path :: TermPath,

87+ subterm_env :: Env,

88+ subterm :: Term }

89+ deriving Show

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

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

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

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

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+

26data Goal = GD { premises :: Env,

106data Goal = GD { premises :: Env,

27 goalType :: Binder Term

107 goalType :: Binder Term

28 }

108 }

109

30mkProofTerm :: Term -> ProofTerm

110mkProofTerm :: Term -> ProofTerm

31−mkProofTerm tm = PT tm

111+mkProofTerm tm = PT Top [] tm

112

33getProofTerm :: ProofTerm -> Term

113getProofTerm :: ProofTerm -> Term

34−getProofTerm (PT tm) = tm

114+getProofTerm (PT path _ sub) = rebuildTerm sub path

115

36same Nothing n = True

116same Nothing n = True

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

117same (Just x) n = x == n

@@ -57,11 +137,40 @@ updateSolvedTerm xs x = updateSolved' xs x where

57 | Just v <- lookup n xs = v

137 | Just v <- lookup n xs = v

58 updateSolved' xs t = t

138 updateSolved' xs t = t

139

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+

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

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

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

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

168+ (updateSolvedTerm xs sub)

169

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

170goal :: 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

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

174 g env (Bind n b@(Guess _ _) sc)

66 | same h n = return $ GD env b

175 | same h n = return $ GD env b

67 | otherwise

176 | otherwise

@@ -78,8 +187,10 @@ goal h (PT tm) = g [] tm where

187

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

188atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->

80 StateT a TC (ProofTerm, Bool)

189 StateT a TC (ProofTerm, Bool)

81−atHole h f c e (PT t) = do (tm, u) <- atH f c e t

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

82− return (PT tm, u)

193+ return (PT path env tm, u)

83 where

194 where

84 updated o = do o' <- o

195 updated o = do o' <- o

85 return (o', True)

196 return (o', True)

@@ -117,7 +228,7 @@ atHole h f c e (PT t) = do (tm, u) <- atH f c e t

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

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

118

229

119bound_in :: ProofTerm -> [Name]

230bound_in :: ProofTerm -> [Name]

120−bound_in (PT tm) = bound_in_term tm

231+bound_in (PT path _ tm) = bound_in_term (rebuildTerm tm path)

121

232

122bound_in_term :: Term -> [Name]

233bound_in_term :: Term -> [Name]

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

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

src/Idris/Core/Unify.hs+9

@@ -333,6 +333,15 @@ unify ctxt env topx topy inj holes usersupp from =

333 = unifyTmpFail tx ty

334 | injective ty && not (holeIn env x || x `elem` holes)

335 = unifyTmpFail tx ty

336+ -- pick the one bound earliest if both are holes

337+ | tx /= ty && (holeIn env x || x `elem` holes)

338+ && (holeIn env y || y `elem` holes)

339+ = case compare (envPos 0 x env) (envPos 0 y env) of

340+ LT -> do sc 1; checkCycle bnames (x, ty)

341+ _ -> do sc 1; checkCycle bnames (y, tx)

342+ where envPos i n ((n',_):env) | n == n' = i

343+ envPos i n (_:env) = envPos (i+1) n env

344+ envPos _ _ _ = 100000

336 un' fn bnames xtm@(P _ x _) tm

345 un' fn bnames xtm@(P _ x _) tm

337 | pureTerm tm, holeIn env x || x `elem` holes

346 | pureTerm tm, holeIn env x || x `elem` holes

338 = do UI s f <- get

347 = do UI s f <- get

src/Idris/ElabTerm.hs+1−1

@@ -144,6 +144,7 @@ elab ist info emode opts fn tm

144 compute -- expand type synonyms, etc

145 elabE (False, False, False, False) tm -- (in argument, guarded, in type, in qquote)

146 end_unify

147+ ptm <- get_term

147 when pattern -- convert remaining holes to pattern vars

148 when pattern -- convert remaining holes to pattern vars

148 (do update_term orderPats

149 (do update_term orderPats

149 unify_all

150 unify_all

@@ -690,7 +691,6 @@ elab ist info emode opts fn tm

690 (caseBlock fc cname'

691 (caseBlock fc cname'

691 (map (isScr scr) (reverse args)) opts)

692 (map (isScr scr) (reverse args)) opts)

692 -- elaborate case

693 -- elaborate case

693− env <- get_env

694 updateAux (newdef : )

695 -- if we haven't got the type yet, hopefully we'll get it later!

696 movelast tyn

test/proof007/DefaultArgUnknownName.idr+7−1

@@ -1,4 +1,10 @@

1module DefaultArgUnknownName

3+-- FIXME: What is the expected behaviour here? Should the type declaration

4+-- not compile?

3funWithBadDefArg : { default sadgjhsag arg : () } -> ()

5funWithBadDefArg : { default sadgjhsag arg : () } -> ()

4−funWithBadDefArg : _ = ()

6+funWithBadDefArg = ()

8+test : ()

9+test = funWithBadDefArg

10+

test/proof007/expected+3−2

@@ -1,2 +1,3 @@

1−DefaultArgUnknownName.idr:3:18:When elaborating type of DefaultArgUnknownName.funWithBadDefArg:

1+DefaultArgUnknownName.idr:5:30:When elaborating right hand side of test:

2−Can't infer type for sadgjhsag

2+When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:

3+ No such variable sadgjhsag