f9a1dab · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix pattern variable problem when patterns generated by unification

f9a1dabEdwin Brady14 years ago

src/Core/Elaborate.hs+20−5

compare with master

unifiedsplit

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

96get_term = do ES p _ _ <- get

97 return (pterm (fst p))

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+

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

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

100get_env :: Elab' aux Env

106get_env :: Elab' aux Env

101get_env = do ES p _ _ <- get

107get_env = do ES p _ _ <- get

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

145 return (instances (fst p))

151 return (instances (fst p))

146

152

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

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

154+unique_hole = unique_hole' False

155+

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

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

157+unique_hole' reusable n

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

158+ = do ES p _ _ <- get

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

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

160+ bound_in (ptype (fst p))

151− n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p) ++ bs ++ dontunify (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)

152− return n'

167+ return n'

153 where

168 where

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

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

155 where

170 where

src/Core/ProofState.hs+16−12

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

22data ProofState = PS { thname :: Name,

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

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

24 nextname :: Int, -- name supply

25 nextname :: Int, -- name supply

25 pterm :: Term, -- current proof term

26 pterm :: Term, -- current proof term

26 ptype :: Type, -- original goal

27 ptype :: Type, -- original goal

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

74-- Some utilites on proof and tactic states

75-- Some utilites on proof and tactic states

76instance Show ProofState where

77instance Show ProofState where

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

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

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

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

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

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

80 wkenv = premises g in

81 wkenv = premises g in

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

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

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

98 showG ps b = showEnv ps (binderTy b)

99 showG ps b = showEnv ps (binderTy b)

100

100instance Pretty ProofState where

101instance Pretty ProofState where

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

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

102 if size nm > breakingSize then

103 if size nm > breakingSize then

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

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

104 else

105 else

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

106 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 _ _) =

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

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

108 let wkEnv = premises g in

109 let wkEnv = premises g in

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

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

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

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

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

172newProof n ctxt ty = let h = holeName 0

173newProof n ctxt ty = let h = holeName 0

173 ty' = vToP ty in

174 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, [])

175 Nothing [] []

177 Nothing [] []

176 [] []

178 [] []

177 Nothing ctxt "" False

179 Nothing ctxt "" False

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

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

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

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

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

507

509

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

511+ updateSolved' xs x

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

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

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

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

510−updateSolved xs (Bind n b t)

514+updateSolved' xs (Bind n b t)

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

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

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

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

513−updateSolved xs (P _ n _)

517+updateSolved' xs (P _ n _)

514 | Just v <- lookup n xs = v

518 | Just v <- lookup n xs = v

515−updateSolved xs t = t

519+updateSolved' xs t = t

516

520

517updateProblems ns [] = []

521updateProblems ns [] = []

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

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

786orderPats :: Term -> Term

787orderPats tm = op [] tm

788 where

789− op ps (Bind n (PVar t) sc) = op ((n, t) : 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

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

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

791

792

792 sortP ps = pick [] (reverse ps)

793 sortP ps = pick [] (reverse ps)

793

794

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

804

805

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

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

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

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

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

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

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

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

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

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

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

810

812

src/Idris/Docs.hs+2−2

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

20 [FunDoc] -- method docs

22showDoc "" = ""

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

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

25instance Show FunDoc where

26 show (Doc n doc args ty)

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

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

28 let argshow = mapMaybe showArg args in

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

30 showSep "\t" argshow

src/Idris/ElabTerm.hs+8−4

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

69elab ist info pattern tcgen fn tm

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

71 when pattern -- convert remaining holes to pattern vars

72+ (do update_term orderPats

73+-- tm <- get_term

72− mkPat

74+ mkPat)

73 inj <- get_inj

75 inj <- get_inj

74 mapM_ checkInjective inj

76 mapM_ checkInjective inj

75 where

77 where

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

86 v -> Just (elabE ina v)

88 v -> Just (elabE ina v)

88 mkPat = do hs <- get_holes

90 mkPat = do hs <- get_holes

91+ tm <- get_term

89 case hs of

92 case hs of

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

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

91 [] -> return ()

94 [] -> return ()

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

293 focus valn

296 focus valn

294 elabE (True, a) scr

297 elabE (True, a) scr

295 args <- get_env

298 args <- get_env

296− cname <- unique_hole (mkCaseName fn)

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

297− elab' ina (PMetavar cname)

298 let cname' = mkN cname

300 let cname' = mkN cname

301+ elab' ina (PMetavar cname')

302+ let newdef = PClauses fc [] cname'

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

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

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

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

301 -- elaborate case

305 -- elaborate case

302 updateAux (newdef : )

306 updateAux (newdef : )

src/Idris/Prover.hs+2−2

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

62 fail (pshow i a)

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

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

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

66 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

68 let OK ty = goalAtFocus ps

69 let OK env = envAtFocus ps

70 putStrLn . render $