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

git.iko.soy/Idris-dev

Add patvar tactic; fix apply to deal with names properly

commit07f3b19571f524e9ef7470329008dcfa12254922 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 28 Sep 2011, 13:29 (15 years ago) parent12f9368

3 files changed+20−8

compare with master

unifiedsplit

src/Elaborate.hs+11−8 src/ProofState.hs+7 src/ShellParser.hs+2

src/Elaborate.hs+11−8

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

6161get_type tm = do ctxt <- get_context

6262 env <- get_env

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

64− return (vToP ty)

64+ return (finalise ty)

6565

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

6767unique_hole :: Name -> Elab Name

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

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

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

121121

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

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

124+

122125focus :: Name -> Elab ()

123126focus n = processTactic' (Focus n)

124127

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

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

135138prepare_apply fn imps =

136139 do ty <- get_type fn

137− let claims = getArgs ty imps

138− mapM doClaim claims

140+ -- let claims = getArgs ty imps

141+ doClaims ty imps []

139142 where

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

141− getArgs t i = []

142−

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

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

144144 do n <- unique_hole n'

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

145146 claim n (forget t)

146147 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"

148151

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

150153apply fn imps =

src/ProofState.hs+7

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

4141 | CheckIn Raw

4242 | Intro Name

4343 | Forall Name Raw

44+ | PatVar Name Raw

4445 | Focus Name

4546 | MoveLast Name

4647 | ProofState

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

218219 lift $ isSet ctxt env t

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

220221

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

221227

222228compute :: RunTactic

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

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

294300 mktac Compute = compute

295301 mktac (Intro n) = intro n

296302 mktac (Forall n t) = forall n t

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

297304 mktac (CheckIn r) = check_in r

298305 mktac (EvalIn r) = eval_in r

299306 mktac (Focus n) = focus n

src/ShellParser.hs+2

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

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

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

5959 return (forall n ty)

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

61+ return (patvar n ty)

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

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

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