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

src/Core/Elaborate.hs+3

compare with master

unifiedsplit

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

147patvar :: Name -> Elab ()

148patvar n = processTactic' (PatVar n)

149

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

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

152+

150focus :: Name -> Elab ()

153focus :: Name -> Elab ()

151focus n = processTactic' (Focus n)

154focus n = processTactic' (Focus n)

152

155

src/Core/ProofState.hs+11−1

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

48 | Intro Name

49 | Forall Name Raw

50 | PatVar Name

51+ | PatBind Name Raw

51 | Focus Name

52 | Focus Name

52 | MoveLast Name

53 | MoveLast Name

53 | ProofState

54 | ProofState

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

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

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

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

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

225 _ -> fail "Nothing to introduce"

226 _ -> fail "Nothing to introduce"

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

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

227

228

228forall :: Name -> Raw -> RunTactic

229forall :: Name -> Raw -> RunTactic

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

230forall 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' =

231 lift $ isSet ctxt env tyt

232 lift $ isSet ctxt env tyt

232 lift $ isSet ctxt env t

233 lift $ isSet ctxt env t

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

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

234

236

235patvar :: Name -> RunTactic

237patvar :: Name -> RunTactic

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

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

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

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

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

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

239

241

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+

240compute :: RunTactic

249compute :: RunTactic

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

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

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

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

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

336 mktac (Intro n) = intro n

345 mktac (Intro n) = intro n

337 mktac (Forall n t) = forall n t

346 mktac (Forall n t) = forall n t

338 mktac (PatVar n) = patvar n

347 mktac (PatVar n) = patvar n

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

339 mktac (CheckIn r) = check_in r

349 mktac (CheckIn r) = check_in r

340 mktac (EvalIn r) = eval_in r

350 mktac (EvalIn r) = eval_in r

341 mktac (Focus n) = focus n

351 mktac (Focus n) = focus n

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

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

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

60 $ do lift (putStrLn str)

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

62

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

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

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

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

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

65liftCatch catchError m h =

66liftCatch catchError m h =

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

210 ni env (PHidden tm) = ni env tm

211 ni env (PHidden tm) = ni env tm

211 ni env _ = []

212 ni env _ = []

212

213

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+

213-- Dealing with implicit arguments

235-- Dealing with implicit arguments

214

236

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

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

9import Core.Evaluate

10import Core.Typecheck

11

12+import Control.Monad

13+

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

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

13elabType n ty

15elabType n ty

14 = do ctxt <- getContext

16 = do ctxt <- getContext

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

38 return (n, cty)

40 return (n, cty)

39

41

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

42elabClauses :: [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 ()

42

72

43−elabClause :: PClause -> Idris ()

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

44−elabClause _ = return ()

74+ psolve tm = return ()

45

75

46elabDecl :: PDecl -> Idris ()

76elabDecl :: PDecl -> Idris ()

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

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

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

65 get_term

95 get_term

66

96

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

97elab :: 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

69 where

101 where

70 isph (_, Placeholder) = True

102 isph (_, Placeholder) = True

71 isph _ = False

103 isph _ = False

72

104

105+ mkPat = do hs <- get_holes

106+ case hs of

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

108+ [] -> return ()

109+

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

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

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

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

75 elab' (PRef n) | pattern

112 elab' (PRef n) | pattern

src/Main.hs+1

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

46 i <- get

47 iLOG (show (idris_infixes i))

48 -- Now add all the declarations to the context

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

49 mapM_ elabDecl ds

50 mapM_ elabDecl ds

50 return ()

51 return ()

51

52