54c8a04 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Checking pattern match clauses

commit54c8a0419c20c2a86e4cdba486c389b4e1bc2aee authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 7 Oct 2011, 19:59 (15 years ago) parent7a30f10

6 files changed+79−6

compare with master

unifiedsplit

src/Core/Elaborate.hs+3 src/Core/ProofState.hs+11−1 src/Core/Typecheck.hs+1−1 src/Idris/AbsSyntax.hs+22 src/Idris/ElabDecls.hs+41−4 src/Main.hs+1

src/Core/Elaborate.hs+3

@@ -147,6 +147,9 @@ 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)

152+

150153focus :: Name -> Elab ()

151154focus n = processTactic' (Focus n)

152155

src/Core/ProofState.hs+11−1

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

4848 | Intro Name

4949 | Forall Name Raw

5050 | PatVar Name

51+ | PatBind Name Raw

5152 | Focus Name

5253 | MoveLast Name

5354 | ProofState

@@ -223,7 +224,7 @@ intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

223224 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

224225 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

225226 _ -> fail "Nothing to introduce"

226−intro ctxt env _ _ = fail "Can't introduce here."

227+intro n ctxt env _ = fail "Can't introduce here."

227228

228229forall :: Name -> Raw -> RunTactic

229230forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

@@ -231,12 +232,20 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

231232 lift $ isSet ctxt env tyt

232233 lift $ isSet ctxt env t

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

235+forall n ty ctxt env _ = fail "Can't pi bind here"

234236

235237patvar :: Name -> RunTactic

236238patvar n ctxt env (Bind x (Hole t) sc) =

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

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

239241

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"

248+

240249compute :: RunTactic

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

242251 do return $ Bind x (Hole (normalise ctxt env ty)) sc

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

336345 mktac (Intro n) = intro n

337346 mktac (Forall n t) = forall n t

338347 mktac (PatVar n) = patvar n

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

339349 mktac (CheckIn r) = check_in r

340350 mktac (EvalIn r) = eval_in r

341351 mktac (Focus n) = focus n

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

121+ = return (Bind n (PVar t) scv, Bind n (PVar 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/AbsSyntax.hs+22

@@ -60,6 +60,7 @@ iLOG str = do i <- get

6060 $ do lift (putStrLn str)

6161 put (i { idris_log = idris_log i ++ str ++ "\n" } )

6262

63+-- Taken from the library source code - for ghc 6.12/7 compatibility

6364liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->

6465 StateT s m a -> (e -> StateT s m a) -> StateT s m a

6566liftCatch catchError m h =

@@ -210,6 +211,27 @@ namesIn ist tm = nub $ ni [] tm

210211 ni env (PHidden tm) = ni env tm

211212 ni env _ = []

212213

214+-- For inferring types of things

215+

216+inferTy = MN 0 "__Infer"

217+inferCon = MN 0 "__infer"

218+inferDecl = PDatadecl inferTy

219+ PSet

220+ [(inferCon, PPi Imp (MN 0 "A") PSet (

221+ PPi Exp (MN 0 "a") (PRef (MN 0 "A"))

222+ (PRef inferTy)))]

223+

224+infTerm t = PApp (PRef inferCon) [(MN 0 "A", Placeholder)] [t]

225+infP = P (TCon 0) inferTy (Set 0)

226+

227+getInferTerm, getInferType :: Term -> Term

228+getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

229+getInferTerm (App (App _ _) tm) = tm

230+

231+getInferType (Bind n b sc) = Bind n b $ getInferType sc

232+getInferType (App (App _ ty) _) = ty

233+

234+

213235-- Dealing with implicit arguments

214236

215237-- Add implicit Pi bindings for any names in the term which appear in an

src/Idris/ElabDecls.hs+41−4

@@ -9,6 +9,8 @@ import Core.Elaborate

99import Core.Evaluate

1010import Core.Typecheck

1111

12+import Control.Monad

13+

1214elabType :: Name -> PTerm -> Idris ()

1315elabType n ty

1416 = do ctxt <- getContext

@@ -38,10 +40,38 @@ elabCon (n, t)

3840 return (n, cty)

3941

4042elabClauses :: [PClause] -> Idris ()

41−elabClauses _ = return ()

43+elabClauses cs = do pats <- mapM elabClause cs

44+ iLOG (showSep "\n" (map (\ (l,r) ->

45+ show l ++ " = " ++

46+ show r) pats))

47+

48+elabClause :: PClause -> Idris (Term, Term)

49+elabClause (PClause _ lhs rhs)

50+ = do ctxt <- getContext

51+ (lhs', _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

52+ (build True (infTerm lhs))

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

57+ (do pbinds lhs_tm

58+ build False (infTerm 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

64+ iLOG $ show clhsty

65+ iLOG $ show crhsty

66+ tclift $ converts ctxt [] clhsty crhsty

67+ return (clhs, crhs)

68+ where

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

70+ pbinds sc

71+ pbinds tm = return ()

4272

43−elabClause :: PClause -> Idris ()

44−elabClause _ = return ()

73+ psolve (Bind n (PVar t) sc) = do solve; psolve sc

74+ psolve tm = return ()

4575

4676elabDecl :: PDecl -> Idris ()

4777elabDecl d = idrisCatch (elabDecl' d) (\e -> iputStrLn (show e))

@@ -65,11 +95,18 @@ build pattern tm = do elab pattern tm

6595 get_term

6696

6797elab :: Bool -> PTerm -> Elab ()

68−elab pattern tm = elab' tm

98+elab pattern tm = do elab' tm

99+ when pattern -- convert remaining holes to pattern vars

100+ mkPat

69101 where

70102 isph (_, Placeholder) = True

71103 isph _ = False

72104

105+ mkPat = do hs <- get_holes

106+ case hs of

107+ (h: hs) -> do patvar h; mkPat

108+ [] -> return ()

109+

73110 elab' PSet = do exact (RSet 0); solve

74111 elab' (PQuote r) = do exact r; solve

75112 elab' (PRef n) | pattern

src/Main.hs+1

@@ -46,6 +46,7 @@ loadModule f = do iLOG ("Reading " ++ show f)

4646 i <- get

4747 iLOG (show (idris_infixes i))

4848 -- Now add all the declarations to the context

49+ elabDecl (PData inferDecl) -- a handy primitive

4950 mapM_ elabDecl ds

5051 return ()

5152