07f3b19 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add patvar tactic; fix apply to deal with names properly

07f3b19Edwin Brady15 years ago

src/Elaborate.hs+11−8

compare with master

unifiedsplit

@@ -61,7 +61,7 @@ get_type :: Raw -> Elab Type

61get_type tm = do ctxt <- get_context

62 env <- get_env

63 (val, ty) <- lift $ check ctxt env tm

64− return (vToP ty)

64+ return (finalise ty)

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

67unique_hole :: Name -> Elab Name

@@ -119,6 +119,9 @@ intro n = processTactic' (Intro n)

119forall :: Name -> Raw -> Elab ()

120forall n t = processTactic' (Forall n t)

121

122+patvar :: Name -> Raw -> Elab ()

123+patvar n t = processTactic' (PatVar n t)

124+

122focus :: Name -> Elab ()

125focus :: Name -> Elab ()

123focus n = processTactic' (Focus n)

126focus n = processTactic' (Focus n)

124

127

@@ -134,17 +137,17 @@ qed = processTactic' QED

134prepare_apply :: Raw -> [Bool] -> Elab [Name]

137prepare_apply :: Raw -> [Bool] -> Elab [Name]

135prepare_apply fn imps =

138prepare_apply fn imps =

136 do ty <- get_type fn

139 do ty <- get_type fn

137− let claims = getArgs ty imps

140+ -- let claims = getArgs ty imps

138− mapM doClaim claims

141+ doClaims ty imps []

139 where

142 where

140− getArgs (Bind n (Pi t) sc) (i : is) = (n, t, i):getArgs sc is

143+ doClaims (Bind n' (Pi t) sc) (i : is) claims =

141− getArgs t i = []

142−

143− doClaim (n', t, i) =

144 do n <- unique_hole n'

145+ let sc' = instantiate (P Bound n t) sc

145 claim n (forget t)

146 claim n (forget t)

146 when i (movelast n)

147 when i (movelast n)

147− return n

148+ doClaims sc' is (n : claims)

149+ doClaims t [] claims = return (reverse claims)

150+ doClaims _ _ _ = fail "Wrong number of arguments"

148

151

149apply :: Raw -> [Bool] -> Elab ()

152apply :: Raw -> [Bool] -> Elab ()

150apply fn imps =

153apply fn imps =

src/ProofState.hs+7

@@ -41,6 +41,7 @@ data Tactic = Attack

41 | CheckIn Raw

42 | Intro Name

43 | Forall Name Raw

44+ | PatVar Name Raw

44 | Focus Name

45 | Focus Name

45 | MoveLast Name

46 | MoveLast Name

46 | ProofState

47 | ProofState

@@ -218,6 +219,11 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

218 lift $ isSet ctxt env t

219 lift $ isSet ctxt env t

219 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))

220 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))

220

221

222+patvar :: Name -> Raw -> RunTactic

223+patvar n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

224+ do (tyv, tyt) <- lift $ check ctxt env ty

225+ lift $ isSet ctxt env tyt

226+ return $ Bind n (PVar tyv) (Bind x (Hole t) (P Bound x t))

221

227

222compute :: RunTactic

228compute :: RunTactic

223compute ctxt env (Bind x (Hole ty) sc) =

229compute ctxt env (Bind x (Hole ty) sc) =

@@ -294,6 +300,7 @@ process t h ps = tactic (Just h) ps (context ps) (mktac t)

294 mktac Compute = compute

300 mktac Compute = compute

295 mktac (Intro n) = intro n

301 mktac (Intro n) = intro n

296 mktac (Forall n t) = forall n t

302 mktac (Forall n t) = forall n t

303+ mktac (PatVar n t) = patvar n t

297 mktac (CheckIn r) = check_in r

304 mktac (CheckIn r) = check_in r

298 mktac (EvalIn r) = eval_in r

305 mktac (EvalIn r) = eval_in r

299 mktac (Focus n) = focus n

306 mktac (Focus n) = focus n

src/ShellParser.hs+2

@@ -57,6 +57,8 @@ pTactic = do reserved "attack"; return attack

57 <|> do reserved "intro"; n <- iName; return (intro n)

58 <|> do reserved "forall"; n <- iName; lchar ':'; ty <- pTerm

59 return (forall n ty)

60+ <|> do reserved "patvar"; n <- iName; lchar ':'; ty <- pTerm

61+ return (patvar n ty)

60 <|> do reserved "eval"; t <- pTerm; return (eval_in t)

62 <|> do reserved "eval"; t <- pTerm; return (eval_in t)

61 <|> do reserved "check"; t <- pTerm; return (check_in t)

63 <|> do reserved "check"; t <- pTerm; return (check_in t)

62 <|> do reserved "focus"; n <- iName; return (focus n)

64 <|> do reserved "focus"; n <- iName; return (focus n)