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

src/Core/Elaborate.hs+2−2

compare with master

unifiedsplit

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

147patvar :: Name -> Elab ()

148patvar n = processTactic' (PatVar n)

149

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

150+patbind :: Name -> Elab ()

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

151+patbind n = processTactic' (PatBind n)

152

153focus :: Name -> Elab ()

154focus n = processTactic' (Focus n)

src/Core/ProofState.hs+10−8

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

48 | Intro Name

49 | Forall Name Raw

50 | PatVar Name

51− | PatBind Name Raw

51+ | PatBind Name

52 | Focus Name

53 | MoveLast Name

54 | ProofState

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

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

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

241

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

242+patbind :: Name -> RunTactic

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

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

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

244+ do let t' = normalise ctxt env t

245− lift $ isSet ctxt env tyt

245+ case t' of

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

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

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

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

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

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

248

250

249compute :: RunTactic

251compute :: RunTactic

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

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

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

345 mktac (Intro n) = intro n

347 mktac (Intro n) = intro n

346 mktac (Forall n t) = forall n t

348 mktac (Forall n t) = forall n t

347 mktac (PatVar n) = patvar n

349 mktac (PatVar n) = patvar n

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

350+ mktac (PatBind n) = patbind n

349 mktac (CheckIn r) = check_in r

351 mktac (CheckIn r) = check_in r

350 mktac (EvalIn r) = eval_in r

352 mktac (EvalIn r) = eval_in r

351 mktac (Focus n) = focus n

353 mktac (Focus n) = focus n

src/Core/TT.hs+2

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

103 | Guess { binderTy :: b,

104 binderVal :: b }

105 | PVar { binderTy :: b }

106+ | PVTy { binderTy :: b }

106 deriving (Show, Eq, Functor)

107 deriving (Show, Eq, Functor)

107

108

108raw_apply :: Raw -> [Raw] -> Raw

109raw_apply :: Raw -> [Raw] -> Raw

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

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

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

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

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

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

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

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

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

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

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

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

230

232

src/Core/Typecheck.hs+1−1

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

118 checkNotHoley 0 sct

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

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

122

123 checkNotHoley i (V v)

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

53 let lhs_tm = getInferTerm lhs'

54 let lhs_ty = getInferType lhs'

55 (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

57 (do pbinds lhs_tm

58− build False (infTerm rhs)

58+ build False rhs

59 psolve lhs_tm

60 get_term)

61− let rhs_tm = getInferTerm rhs'

62− let rhs_ty = getInferType rhs'

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

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

64− iLOG $ show clhsty

65− iLOG $ show crhsty

66− tclift $ converts ctxt [] clhsty crhsty

67 return (clhs, crhs)

62 return (clhs, crhs)

68 where

63 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

70 pbinds sc

65 pbinds sc

71 pbinds tm = return ()

66 pbinds tm = return ()

72

67