17e22af · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Feed a type to the elaborator for the RHS of a pattern. Also, change type of pattern binders

commit17e22af396269bde6c28012e7e9e0ce541489d29 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 7 Oct 2011, 21:18 (15 years ago) parent54c8a04

5 files changed+19−20

compare with master

unifiedsplit

src/Core/Elaborate.hs+2−2 src/Core/ProofState.hs+10−8 src/Core/TT.hs+2 src/Core/Typecheck.hs+1−1 src/Idris/ElabDecls.hs+4−9

src/Core/Elaborate.hs+2−2

@@ -147,8 +147,8 @@ forall n t = processTactic' (Forall n t)

147147patvar :: Name -> Elab ()

148148patvar n = processTactic' (PatVar n)

149149

150−patbind :: Name -> Raw -> Elab ()

151−patbind n ty = processTactic' (PatBind n ty)

150+patbind :: Name -> Elab ()

151+patbind n = processTactic' (PatBind n)

152152

153153focus :: Name -> Elab ()

154154focus n = processTactic' (Focus n)

src/Core/ProofState.hs+10−8

@@ -48,7 +48,7 @@ data Tactic = Attack

4848 | Intro Name

4949 | Forall Name Raw

5050 | PatVar Name

51− | PatBind Name Raw

51+ | PatBind Name

5252 | Focus Name

5353 | MoveLast Name

5454 | ProofState

@@ -239,12 +239,14 @@ patvar n ctxt env (Bind x (Hole t) sc) =

239239 do action (\ps -> ps { holes = holes ps \\ [x] })

240240 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))

241241

242−patbind :: Name -> Raw -> RunTactic

243−patbind n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

244− do (tyv, tyt) <- lift $ check ctxt env ty

245− lift $ isSet ctxt env tyt

246− return $ Bind n (PVar tyv) (Bind x (Hole t) (P Bound x t))

247−patbind n ty ctxt env _ = fail "Can't pattern bind here"

242+patbind :: Name -> RunTactic

243+patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

244+ do let t' = normalise ctxt env t

245+ case t' of

246+ Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

247+ return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))

248+ _ -> fail "Nothing to pattern bind"

249+patbind n ctxt env _ = fail "Can't pattern bind here"

248250

249251compute :: RunTactic

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

@@ -345,7 +347,7 @@ process t h = tactic (Just h) (mktac t)

345347 mktac (Intro n) = intro n

346348 mktac (Forall n t) = forall n t

347349 mktac (PatVar n) = patvar n

348− mktac (PatBind n t) = patbind n t

350+ mktac (PatBind n) = patbind n

349351 mktac (CheckIn r) = check_in r

350352 mktac (EvalIn r) = eval_in r

351353 mktac (Focus n) = focus n

src/Core/TT.hs+2

@@ -103,6 +103,7 @@ data Binder b = Lam { binderTy :: b }

103103 | Guess { binderTy :: b,

104104 binderVal :: b }

105105 | PVar { binderTy :: b }

106+ | PVTy { binderTy :: b }

106107 deriving (Show, Eq, Functor)

107108

108109raw_apply :: Raw -> [Raw] -> Raw

@@ -225,6 +226,7 @@ showEnv' env t dbg = se 10 env t where

225226 sb env n (Hole t) = showb env "? " ". " n t

226227 sb env n (Pi t) = showb env "(" ") -> " n t

227228 sb env n (PVar t) = showb env "pat " ". " n t

229+ sb env n (PVTy t) = showb env "pty " ". " n t

228230 sb env n (Let t v) = showbv env "let " " in " n t v

229231 sb env n (Guess t v) = showbv env "?? " " in " n t v

230232

src/Core/Typecheck.hs+1−1

@@ -118,7 +118,7 @@ check ctxt env (RBind n b sc)

118118 checkNotHoley 0 sct

119119 return (Bind n (Guess t v) scv, sct)

120120 discharge n (PVar t) scv sct

121− = return (Bind n (PVar t) scv, Bind n (PVar t) sct)

121+ = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

122122

123123 checkNotHoley i (V v)

124124 | v == i = fail "You can't put a hole where a hole don't belong"

src/Idris/ElabDecls.hs+4−9

@@ -53,20 +53,15 @@ elabClause (PClause _ lhs rhs)

5353 let lhs_tm = getInferTerm lhs'

5454 let lhs_ty = getInferType lhs'

5555 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

56− (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") infP

56+ (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

5757 (do pbinds lhs_tm

58− build False (infTerm rhs)

58+ build False rhs

5959 psolve lhs_tm

6060 get_term)

61− let rhs_tm = getInferTerm rhs'

62− let rhs_ty = getInferType rhs'

63− (crhs, crhsty) <- tclift $ recheck ctxt [] rhs_tm

64− iLOG $ show clhsty

65− iLOG $ show crhsty

66− tclift $ converts ctxt [] clhsty crhsty

61+ (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

6762 return (clhs, crhs)

6863 where

69− pbinds (Bind n (PVar t) sc) = do attack; patbind n (forget t)

64+ pbinds (Bind n (PVar t) sc) = do attack; patbind n

7065 pbinds sc

7166 pbinds tm = return ()

7267