f9a1dab · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix pattern variable problem when patterns generated by unification

commitf9a1dab036be89bc7eac8908b528717f2ac3fb4b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 13 Nov 2012, 10:58 (14 years ago) parent2b7db6a

6 files changed+53−28

compare with master

unifiedsplit

src/Core/Elaborate.hs+20−5 src/Core/ProofState.hs+16−12 src/Core/TT.hs+5−3 src/Idris/Docs.hs+2−2 src/Idris/ElabTerm.hs+8−4 src/Idris/Prover.hs+2−2

src/Core/Elaborate.hs+20−5

@@ -96,6 +96,12 @@ get_term :: Elab' aux Term

9696get_term = do ES p _ _ <- get

9797 return (pterm (fst p))

9898

99+-- get the proof term

100+update_term :: (Term -> Term) -> Elab' aux ()

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

102+ let p' = p { pterm = f (pterm p) }

103+ put (ES (p', a) logs prev)

104+

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

100106get_env :: Elab' aux Env

101107get_env = do ES p _ _ <- get

@@ -145,11 +151,20 @@ get_instances = do ES p _ _ <- get

145151 return (instances (fst p))

146152

147153-- given a desired hole name, return a unique hole name

148−unique_hole :: Name -> Elab' aux Name

149−unique_hole n = do ES p _ _ <- get

150− let bs = bound_in (pterm (fst p)) ++ bound_in (ptype (fst p))

151− n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p) ++ bs ++ dontunify (fst p))

152− return n'

154+unique_hole = unique_hole' False

155+

156+unique_hole' :: Bool -> Name -> Elab' aux Name

157+unique_hole' reusable n

158+ = do ES p _ _ <- get

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

160+ bound_in (ptype (fst p))

161+ n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p)

162+ ++ bs ++ dontunify (fst p) ++ usedns (fst p))

163+ ES (p, a) s u <- get

164+ -- Hmm: Do we need this level of uniqueness?

165+ let p' = p -- if reusable then p else p { usedns = n' : usedns p }

166+ put (ES (p', a) s u)

167+ return n'

153168 where

154169 bound_in (Bind n b sc) = n : bi b ++ bound_in sc

155170 where

src/Core/ProofState.hs+16−12

@@ -21,6 +21,7 @@ import Util.Pretty

2121

2222data ProofState = PS { thname :: Name,

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

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

2425 nextname :: Int, -- name supply

2526 pterm :: Term, -- current proof term

2627 ptype :: Type, -- original goal

@@ -74,8 +75,8 @@ data Tactic = Attack

7475-- Some utilites on proof and tactic states

7576

7677instance Show ProofState where

77− show (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

78− show (PS nm (h:hs) _ tm _ _ _ _ _ _ i _ _ ctxt _ _)

78+ show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

79+ show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _)

7980 = let OK g = goal (Just h) tm

8081 wkenv = premises g in

8182 "Other goals: " ++ show hs ++ "\n" ++

@@ -98,12 +99,12 @@ instance Show ProofState where

9899 showG ps b = showEnv ps (binderTy b)

99100

100101instance Pretty ProofState where

101− pretty (PS nm [] _ trm _ _ _ _ _ _ _ _ _ _ _ _) =

102+ pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _) =

102103 if size nm > breakingSize then

103104 pretty nm <> colon $$ nest nestingSize (text " no more goals.")

104105 else

105106 pretty nm <> colon <+> text " no more goals."

106− pretty p@(PS nm (h:hs) _ tm _ _ _ _ _ _ i _ _ ctxt _ _) =

107+ pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _) =

107108 let OK g = goal (Just h) tm in

108109 let wkEnv = premises g in

109110 text "Other goals" <+> colon <+> pretty hs $$

@@ -171,7 +172,8 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

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

172173newProof n ctxt ty = let h = holeName 0

173174 ty' = vToP ty in

174− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty [] (h, [])

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

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

175177 Nothing [] []

176178 [] []

177179 Nothing ctxt "" False

@@ -505,14 +507,16 @@ dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us

505507-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us

506508dropGiven du (u : us) = u : dropGiven du us

507509

508−updateSolved xs (Bind n (Hole ty) t)

509− | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

510−updateSolved xs (Bind n b t)

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

512−updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

513−updateSolved xs (P _ n _)

510+updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

511+ updateSolved' xs x

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

513+ | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))

514+updateSolved' xs (Bind n b t)

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

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

517+updateSolved' xs (P _ n _)

514518 | Just v <- lookup n xs = v

515−updateSolved xs t = t

519+updateSolved' xs t = t

516520

517521updateProblems ns [] = []

518522updateProblems ns ((x, y, env, err) : ps) =

src/Core/TT.hs+5−3

@@ -786,8 +786,9 @@ weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))

786786orderPats :: Term -> Term

787787orderPats tm = op [] tm

788788 where

789− op ps (Bind n (PVar t) sc) = op ((n, t) : ps) sc

790− op ps sc = bindAll (map (\ (n, t) -> (n, PVar t)) (sortP ps)) sc

789+ op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc

790+ op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc

791+ op ps sc = bindAll (map (\ (n, t) -> (n, t)) (sortP ps)) sc

791792

792793 sortP ps = pick [] (reverse ps)

793794

@@ -804,7 +805,8 @@ orderPats tm = op [] tm

804805

805806 insert n t [] = [(n, t)]

806807 insert n t ((n',t') : ps)

807− | n `elem` (namesIn t' ++ concatMap namesIn (map snd ps))

808+ | n `elem` (namesIn (binderTy t') ++

809+ concatMap namesIn (map (binderTy . snd) ps))

808810 = (n', t') : insert n t ps

809811 | otherwise = (n,t):(n',t'):ps

810812

src/Idris/Docs.hs+2−2

@@ -20,11 +20,11 @@ data Doc = FunDoc FunDoc

2020 [FunDoc] -- method docs

2121

2222showDoc "" = ""

23−showDoc x = " -- " ++ x ++ "\n"

23+showDoc x = " -- " ++ x

2424

2525instance Show FunDoc where

2626 show (Doc n doc args ty)

27− = show n ++ " : " ++ show ty ++ "\n" ++ showDoc doc ++

27+ = show n ++ " : " ++ show ty ++ "\n" ++ showDoc doc ++ "\n" ++

2828 let argshow = mapMaybe showArg args in

2929 if (not (null argshow)) then "Arguments:\n\t" ++

3030 showSep "\t" argshow

src/Idris/ElabTerm.hs+8−4

@@ -69,7 +69,9 @@ elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

6969elab ist info pattern tcgen fn tm

7070 = do elabE (False, False) tm -- (in argument, guarded)

7171 when pattern -- convert remaining holes to pattern vars

72− mkPat

72+ (do update_term orderPats

73+-- tm <- get_term

74+ mkPat)

7375 inj <- get_inj

7476 mapM_ checkInjective inj

7577 where

@@ -86,6 +88,7 @@ elab ist info pattern tcgen fn tm

8688 v -> Just (elabE ina v)

8789

8890 mkPat = do hs <- get_holes

91+ tm <- get_term

8992 case hs of

9093 (h: hs) -> do patvar h; mkPat

9194 [] -> return ()

@@ -293,10 +296,11 @@ elab ist info pattern tcgen fn tm

293296 focus valn

294297 elabE (True, a) scr

295298 args <- get_env

296− cname <- unique_hole (mkCaseName fn)

297− elab' ina (PMetavar cname)

299+ cname <- unique_hole' True (mkCaseName fn)

298300 let cname' = mkN cname

299− let newdef = PClauses fc [] cname' (caseBlock fc cname' (reverse args) opts)

301+ elab' ina (PMetavar cname')

302+ let newdef = PClauses fc [] cname'

303+ (caseBlock fc cname' (reverse args) opts)

300304 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

301305 -- elaborate case

302306 updateAux (newdef : )

src/Idris/Prover.hs+2−2

@@ -62,9 +62,9 @@ elabStep st e = do case runStateT e st of

6262 fail (pshow i a)

6363

6464dumpState :: IState -> ProofState -> IO ()

65−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _ _) =

65+dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) =

6666 putStrLn . render $ pretty nm <> colon <+> text "No more goals."

67−dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ _ problems i _ _ ctxy _ _) = do

67+dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ problems i _ _ ctxy _ _) = do

6868 let OK ty = goalAtFocus ps

6969 let OK env = envAtFocus ps

7070 putStrLn . render $