a2a5141 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow interleaving of explicit and implicit arguments in top level types

commita2a51415c6f6c826f00510310833695670d75281 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 12 Oct 2011, 02:09 (15 years ago) parent7123e31

6 files changed+164−104

compare with master

unifiedsplit

src/Core/Elaborate.hs+2−2 src/Core/TT.hs+1−1 src/Idris/AbsSyntax.hs+97−67 src/Idris/Delaborate.hs+7−4 src/Idris/ElabDecls.hs+20−11 src/Idris/Parser.hs+37−19

src/Core/Elaborate.hs+2−2

@@ -196,7 +196,7 @@ prepare_apply fn imps =

196196 when i (movelast n)

197197 doClaims sc' is (n : claims)

198198 doClaims t [] claims = return (reverse claims)

199− doClaims _ _ _ = fail "Wrong number of arguments"

199+ doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn

200200

201201 mkMN n@(MN _ _) = n

202202 mkMN n@(UN [x]) = MN 0 x

@@ -233,7 +233,7 @@ apply_elab n args =

233233 claim n (forget t)

234234 doClaims sc' is ((n, i) : claims)

235235 doClaims t [] claims = return (reverse claims)

236− doClaims _ _ _ = fail "Wrong number of arguments"

236+ doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n

237237

238238 elabClaims [] = return ()

239239 elabClaims ((n, Nothing) : xs) = elabClaims xs

src/Core/TT.hs+1−1

@@ -290,7 +290,7 @@ showEnv' env t dbg = se 10 env t where

290290 if dbg then "{" ++ show i ++ "}" else ""

291291 | otherwise = "!!V " ++ show i ++ "!!"

292292 se p env (Bind n b@(Pi t) sc)

293− | noOccurrence n sc && not dbg = bracket p 2 $ se 10 env t ++ " -> " ++ se 10 ((n,b):env) sc

293+ | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ " -> " ++ se 10 ((n,b):env) sc

294294 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

295295 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

296296 se p env (Constant c) = show c

src/Idris/AbsSyntax.hs+97−67

@@ -9,6 +9,7 @@ import Core.Evaluate

99import Control.Monad.State

1010import Data.List

1111import Data.Char

12+import Debug.Trace

1213

1314data IOption = IOption { opt_logLevel :: Int }

1415 deriving (Show, Eq)

@@ -22,7 +23,7 @@ defaultOpts = IOption 0

2223

2324data IState = IState { tt_ctxt :: Context,

2425 idris_infixes :: [FixDecl],

25− idris_implicits :: Ctxt ([Name], Int), -- implicits, arity

26+ idris_implicits :: Ctxt [PArg],

2627 idris_log :: String,

2728 idris_options :: IOption

2829 }

@@ -99,7 +100,7 @@ data PDecl' t = PFix Fixity [String] -- fixity declaration

99100 | PData (PData' t) -- data declaration

100101 deriving Functor

101102

102−data PClause' t = PClause Name t t

103+data PClause' t = PClause Name t t [PDecl]

103104 deriving Functor

104105

105106data PData' t = PDatadecl { d_name :: Name,

@@ -112,20 +113,27 @@ data PData' t = PDatadecl { d_name :: Name,

112113

113114type PDecl = PDecl' PTerm

114115type PData = PData' PTerm

115−type PClause = PClause' PTerm

116−-- High level language terms

116+type PClause = PClause' PTerm

117117

118+-- High level language terms

119+--

118120data PTerm = PQuote Raw

119121 | PRef Name

120122 | PLam Name PTerm PTerm

121123 | PPi Plicity Name PTerm PTerm

122124 | PLet Name PTerm PTerm PTerm -- not implemented yet

123− | PApp PTerm [(Name, PTerm)] [PTerm]

125+ | PApp PTerm [PArg]

124126 | PHidden PTerm -- irrelevant or hidden pattern

125127 | PSet

126128 | PConstant Const

127129 | Placeholder

128130

131+data PArg' t = PImp { pname :: Name, getTm :: t }

132+ | PExp { getTm :: t }

133+ deriving (Show, Functor)

134+

135+type PArg = PArg' PTerm

136+

129137-- Syntactic sugar info (TODO: namespaces, parameters, modules)

130138

131139data SyntaxInfo = Syn { using :: [(Name, PTerm)] }

@@ -151,14 +159,27 @@ instance Show PData where

151159 show d = showDImp False d

152160

153161showCImp :: Bool -> PClause -> String

154−showCImp impl (PClause n l r) = showImp impl l ++ " = " ++ showImp impl r

155−

162+showCImp impl (PClause n l r w) = showImp impl l ++ " = " ++ showImp impl r

163+ ++ " where " ++ show w

156164showDImp :: Bool -> PData -> String

157165showDImp impl (PDatadecl n ty cons)

158166 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"

159167 ++ showSep "\n\t| "

160168 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)

161169

170+getImps :: [PArg] -> [(Name, PTerm)]

171+getImps [] = []

172+getImps (PImp n tm : xs) = (n, tm) : getImps xs

173+getImps (_ : xs) = getImps xs

174+

175+getExps :: [PArg] -> [PTerm]

176+getExps [] = []

177+getExps (PExp tm : xs) = tm : getExps xs

178+getExps (_ : xs) = getExps xs

179+

180+getAll :: [PArg] -> [PTerm]

181+getAll = map getTm

182+

162183showImp :: Bool -> PTerm -> String

163184showImp impl tm = se 10 tm where

164185 se p (PQuote r) = "![" ++ show r ++ "]"

@@ -168,19 +189,21 @@ showImp impl tm = se 10 tm where

168189 | n `elem` allNamesIn sc = bracket p 2 $

169190 "(" ++ show n ++ " : " ++ se 10 ty ++

170191 ") -> " ++ se 10 sc

171− | otherwise = bracket p 2 $ se 10 ty ++ " -> " ++ se 10 sc

192+ | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc

172193 se p (PPi Imp n ty sc)

173194 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++

174195 "} -> " ++ se 10 sc

175196 | otherwise = se 10 sc

176− se p (PApp (PRef f) _ [])

197+ se p (PApp (PRef f) [])

177198 | not impl = show f

178− se p (PApp (PRef op@(UN [f:_])) _ [l, r])

179− | not impl && not (isAlpha f)

180− = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r

181− se p (PApp f imps args)

182− = bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")

183− ++ concatMap seArg args

199+ se p (PApp (PRef op@(UN [f:_])) args)

200+ | length (getExps args) == 2 && not impl && not (isAlpha f)

201+ = let [l, r] = getExps args in

202+ bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r

203+ se p (PApp f as)

204+ = let (imps, args) = (getImps as, getExps as) in

205+ bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")

206+ ++ concatMap seArg args

184207 se p (PHidden tm) = "." ++ se 0 tm

185208 se p PSet = "Set"

186209 se p (PConstant c) = show c

@@ -197,8 +220,7 @@ allNamesIn tm = nub $ ni [] tm

197220 where

198221 ni env (PRef n)

199222 | not (n `elem` env) = [n]

200− ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++

201− concatMap (ni env) es

223+ ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)

202224 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

203225 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

204226 ni env (PHidden tm) = ni env tm

@@ -212,8 +234,7 @@ namesIn ist tm = nub $ ni [] tm

212234 = case lookupCtxt n (idris_implicits ist) of

213235 Nothing -> [n]

214236 _ -> []

215− ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++

216− concatMap (ni env) es

237+ ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)

217238 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

218239 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

219240 ni env (PHidden tm) = ni env tm

@@ -229,7 +250,7 @@ inferDecl = PDatadecl inferTy

229250 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))

230251 (PRef inferTy)))]

231252

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

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

233254infP = P (TCon 0) inferTy (Set 0)

234255

235256getInferTerm, getInferType :: Term -> Term

@@ -246,52 +267,53 @@ getInferType (App (App _ ty) _) = ty

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

247268-- argument position.

248269

249−implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, ([Name], Int))

270+implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

250271implicitise syn ist tm

251272 = let uvars = using syn

252− (declimps, a, ns) = execState (imps [] tm) ([], 0, []) in

273+ (declimps, ns) = execState (imps True [] tm) ([], []) in

253274 if null ns

254− then (tm, (reverse declimps, a))

275+ then (tm, reverse declimps)

255276 else implicitise syn ist (pibind uvars ns tm)

256277 where

257− imps env (PApp f is es)

258− = do (decls, a, ns) <- get

259− let isn = concatMap (namesIn ist) (map snd is)

260− let esn = concatMap (namesIn ist) es

261− put (decls, a, nub (ns ++ ((isn ++ esn) \\ (env ++ decls))))

262− imps env (PPi Imp n ty sc)

263− = do imps env ty

264− (impdecls, a, ns) <- get

265− put (n:impdecls, a, ns)

266− imps (n:env) sc

267− imps env (PPi Exp n ty sc)

268− = do imps env ty

269− (impdecls, a, ns) <- get

270− put (impdecls, a+1, ns)

271− imps (n:env) sc

272− imps env (PLam n ty sc)

273− = do imps env ty

274− imps (n:env) sc

275− imps env (PHidden tm) = imps env tm

276− imps env _ = return ()

278+ imps top env (PApp f as)

279+ = do (decls, ns) <- get

280+ let isn = concatMap (namesIn ist) (map getTm as)

281+ put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

282+ imps top env (PPi Imp n ty sc)

283+ = do let isn = namesIn ist ty \\ [n]

284+ (decls , ns) <- get

285+ put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

286+ imps True (n:env) sc

287+ imps top env (PPi Exp n ty sc)

288+ = do let isn = (namesIn ist ty ++ case sc of

289+ (PRef x) -> namesIn ist sc

290+ _ -> []) \\ [n]

291+ (decls, ns) <- get -- ignore decls in HO types

292+ put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

293+ imps True (n:env) sc

294+ imps top env (PLam n ty sc)

295+ = do imps False env ty

296+ imps False (n:env) sc

297+ imps top env (PHidden tm) = imps False env tm

298+ imps top env _ = return ()

277299

278300 pibind using [] sc = sc

279301 pibind using (n:ns) sc = case lookup n using of

280302 Just ty -> PPi Imp n ty (pibind using ns sc)

281303 Nothing -> PPi Imp n Placeholder (pibind using ns sc)

282304

305+-- Add implicit arguments in function calls

306+

283307addImpl :: IState -> PTerm -> PTerm

284308addImpl ist ptm = ai [] ptm

285309 where

286− ai env (PRef f) = aiFn env (PRef f) [] []

287− ai env (PApp (PRef f) is es)

288− = let is' = map (\ (n, tm) -> (n, ai env tm)) is

289− es' = map (ai env) es in

290− aiFn env (PRef f) is' es'

291− ai env (PApp f is es) = let f' = ai env f

292− is' = map (\ (n, tm) -> (n, ai env tm)) is

293− es' = map (ai env) es in

294− aiFn env f' is' es'

310+ ai env (PRef f) = aiFn env (PRef f) []

311+ ai env (PApp (PRef f) as)

312+ = let as' = map (fmap (ai env)) as in

313+ aiFn env (PRef f) as'

314+ ai env (PApp f as) = let f' = ai env f

315+ as' = map (fmap (ai env)) as in

316+ aiFn env f' as'

295317 ai env (PLam n ty sc) = let ty' = ai env ty

296318 sc' = ai (n:env) sc in

297319 PLam n ty' sc'

@@ -301,23 +323,31 @@ addImpl ist ptm = ai [] ptm

301323 ai env (PHidden tm) = PHidden (ai env tm)

302324 ai env tm = tm

303325

304− aiFn env (PRef f) is es | not (f `elem` env)

326+ aiFn env (PRef f) as | not (f `elem` env)

305327 = case lookupCtxt f (idris_implicits ist) of

306− Just (ns, a) -> pApp a (PRef f) (insertImpl ns is) es

307− Nothing -> pApp 1 (PRef f) is es

308− aiFn env f is es = pApp 1 f is es

328+ Just ns -> pApp (length ns) (PRef f) (insertImpl ns as)

329+ Nothing -> pApp 1 (PRef f) as

330+ aiFn env f as = pApp 1 f as

309331

310− pApp a f [] [] = f

311− pApp a f is es = let rest = drop a es in

312− appRest (PApp f is (take a es)) rest

332+ pApp a f [] = f

333+ pApp a f as = let rest = drop a as in

334+ appRest (PApp f (take a as)) rest

313335

314336 appRest f [] = f

315− appRest f (a : as) = appRest (PApp f [] [a]) as

316−

317− insertImpl [] given = []

318− insertImpl (n:ns) given

319− = case lookup n given of

320− Just val -> (n, val) : insertImpl ns given

321− Nothing -> (n, Placeholder) : insertImpl ns given

322−

337+ appRest f (a : as) = appRest (PApp f [a]) as

338+

339+ insertImpl :: [PArg] -> [PArg] -> [PArg]

340+ insertImpl (PExp ty : ps) (PExp tm : given) =

341+ PExp tm : insertImpl ps given

342+ insertImpl (PImp n ty : ps) given =

343+ case find n given [] of

344+ Just (tm, given') -> PImp n ty : insertImpl ps given'

345+ Nothing -> PImp n Placeholder : insertImpl ps given

346+ insertImpl expected [] = []

347+ insertImpl [] given = given

348+

349+ find n [] acc = Nothing

350+ find n (PImp n' t : gs) acc

351+ | n == n' = Just (t, reverse acc ++ gs)

352+ find n (g : gs) acc = find n gs (g : acc)

323353

src/Idris/Delaborate.hs+7−4

@@ -24,10 +24,13 @@ delab ist tm = de [] tm

2424

2525 deFn env (App f a) args = deFn env f (a:args)

2626 deFn env (P _ n _) args = mkPApp n (map (de env) args)

27− deFn env f args = PApp (de env f) [] (map (de env) args)

27+ deFn env f args = PApp (de env f) (map PExp (map (de env) args))

2828

2929 mkPApp n args

30− | Just (ns, i) <- lookupCtxt n (idris_implicits ist)

31− = PApp (PRef n) (zip ns args) (drop (length ns) args)

32− | otherwise = PApp (PRef n) [] args

30+ | Just imps <- lookupCtxt n (idris_implicits ist)

31+ = PApp (PRef n) (zipWith imp imps args)

32+ | otherwise = PApp (PRef n) (map PExp args)

33+

34+ imp (PImp n _) arg = PImp n arg

35+ imp (PExp _) arg = PExp arg

3336

src/Idris/ElabDecls.hs+20−11

@@ -12,10 +12,12 @@ import Core.Typecheck

1212import Core.CaseTree

1313

1414import Control.Monad

15+import Debug.Trace

1516

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

1718elabType n ty

1819 = do ctxt <- getContext

20+ logLvl 2 $ "Type " ++ showImp True ty

1921 (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build False ty)

2022 (cty, _) <- tclift $ recheck ctxt [] ty'

2123 logLvl 2 $ "---> " ++ show cty

@@ -70,7 +72,7 @@ elabVal tm

7072 tclift $ recheck ctxt [] vtm

7173

7274elabClause :: PClause -> Idris (Term, Term)

73−elabClause (PClause _ lhs rhs)

75+elabClause (PClause _ lhs rhs whereblock)

7476 = do ctxt <- getContext

7577 -- Build the LHS as an "Infer", and pull out its type and

7678 -- pattern bindings

@@ -80,6 +82,11 @@ elabClause (PClause _ lhs rhs)

8082 let lhs_ty = getInferType lhs'

8183 logLvl 3 (show lhs_tm)

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

85+ -- TODO: elaborate where block here.

86+ -- probably the way to check the where clauses is to

87+ -- treat them as in a params block.

88+ -- Will need to know what the params are and add them while

89+ -- elaborating.

8390 -- Now build the RHS, using the type of the LHS as the goal.

8491 iLOG (showImp True rhs)

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

@@ -124,11 +131,13 @@ elab pattern tm = do elab' tm

124131 when pattern -- convert remaining holes to pattern vars

125132 mkPat

126133 where

127− isph (_, Placeholder) = True

128− isph _ = False

134+ isph arg = case getTm arg of

135+ Placeholder -> True

136+ _ -> False

129137

130− toElab (_, Placeholder) = Nothing

131− toElab (_, v) = Just (elab' v)

138+ toElab arg = case getTm arg of

139+ Placeholder -> Nothing

140+ v -> Just (elab' v)

132141

133142 mkPat = do hs <- get_holes

134143 case hs of

@@ -154,14 +163,14 @@ elab pattern tm = do elab' tm

154163 elab' ty

155164 elab' sc

156165 solve

157− elab' (PApp (PRef f) imps args)

158− = try (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)

166+ elab' (PApp (PRef f) args)

167+ = try (do ns <- apply (Var f) (map isph args)

159168 solve

160− elabArgs ns (map snd imps ++ args))

161− (do apply_elab f (map toElab imps ++ map (Just . elab') args)

169+ elabArgs ns (map getTm args))

170+ (do apply_elab f (map toElab args)

162171 solve)

163− elab' (PApp f [] [arg])

164− = do simple_app (elab' f) (elab' arg)

172+ elab' (PApp f [arg])

173+ = do simple_app (elab' f) (elab' (getTm arg))

165174 solve

166175 elab' Placeholder = fail $ "Can't deal with a placeholder here"

167176 elab' x = fail $ "Not implemented " ++ show x

src/Idris/Parser.hs+37−19

@@ -54,9 +54,9 @@ parseProg syn fname

5454

5555-- Collect PClauses with the same function name

5656collect :: [PDecl] -> [PDecl]

57−collect (PClauses _ [c@(PClause n l r)] : ds) = clauses n [c] ds

58− where clauses n acc (PClauses _ [c@(PClause n' l r)] : ds)

59− | n == n' = clauses n (c : acc) ds

57+collect (PClauses _ [c@(PClause n l r w)] : ds) = clauses n [c] ds

58+ where clauses n acc (PClauses _ [PClause n' l r w] : ds)

59+ | n == n' = clauses n (PClause n' l r (collect w) : acc) ds

6060 clauses n acc xs = PClauses n (reverse acc) : collect xs

6161collect (d : ds) = d : collect ds

6262collect [] = []

@@ -75,16 +75,26 @@ pDecl syn

7575 return [fmap (addImpl i) d]

7676 <|> try (pUsing syn)

7777

78+pFunDecl :: SyntaxInfo -> IParser [PDecl]

79+pFunDecl syn

80+ = try (do d <- pFunDecl' syn

81+ lchar ';'

82+ i <- getState

83+ return [fmap (addImpl i) d])

84+

7885--------- Top Level Declarations ---------

7986

8087pDecl' :: SyntaxInfo -> IParser PDecl

8188pDecl' syn

8289 = try pFixity

83− <|> try (do n <- pfName; ty <- pTSig syn

84− ty' <- implicit syn n ty

85− return (PTy n ty'))

90+ <|> pFunDecl' syn

8691 <|> try (pData syn)

87− <|> try (pPattern syn)

92+

93+pFunDecl' :: SyntaxInfo -> IParser PDecl

94+pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

95+ ty' <- implicit syn n ty

96+ return (PTy n ty'))

97+ <|> try (pPattern syn)

8898

8999pUsing :: SyntaxInfo -> IParser [PDecl]

90100pUsing syn =

@@ -148,12 +158,12 @@ pHSimpleExpr syn

148158pApp syn = do f <- pSimpleExpr syn

149159 iargs <- many (pImplicitArg syn)

150160 args <- many1 (pSimpleExpr syn)

151− return (PApp f iargs args)

161+ return (PApp f (iargs ++ map PExp args))

152162

153163pImplicitArg syn = do lchar '{'; n <- iName

154164 v <- option (PRef n) (do lchar '='; pExpr syn)

155165 lchar '}'

156− return (n, v)

166+ return (PImp n v)

157167

158168pTSig syn = do lchar ':'

159169 pExpr syn

@@ -193,17 +203,17 @@ pConstant = do reserved "Int"; return IType

193203 <|> try (do i <- natural; return $ I (fromInteger i))

194204

195205table fixes

196− = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [] [PConstant (I 0), x])]]

206+ = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]

197207 ++ toTable (reverse fixes) ++

198− [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],

208+ [[binary "=" (\x y -> PApp (PRef (UN ["="])) [PExp x,PExp y]) AssocLeft],

199209 [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]

200210

201211toTable fs = map (map toBin)

202212 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

203213 where toBin (Fix (PrefixN _) op) = prefix op

204− (\x -> PApp (PRef (UN [op])) [] [x])

214+ (\x -> PApp (PRef (UN [op])) [PExp x])

205215 toBin (Fix f op) = binary op

206− (\x y -> PApp (PRef (UN [op])) [] [x,y]) (assoc f)

216+ (\x y -> PApp (PRef (UN [op])) [PExp x,PExp y]) (assoc f)

207217 assoc (Infixl _) = AssocLeft

208218 assoc (Infixr _) = AssocRight

209219 assoc (InfixN _) = AssocNone

@@ -231,7 +241,7 @@ pData syn = try (do reserved "data"; tyn <- pfName; ty <- pTSig syn

231241 return $ PData (PDatadecl tyn ty' cons')

232242

233243mkPApp t [] = t

234−mkPApp t xs = PApp t [] xs

244+mkPApp t xs = PApp t (map PExp xs)

235245

236246bindArgs :: [PTerm] -> PTerm -> PTerm

237247bindArgs [] t = t

@@ -253,7 +263,7 @@ pSimpleCon syn

253263

254264pPattern :: SyntaxInfo -> IParser PDecl

255265pPattern syn = do clause <- pClause syn

256− return (PClauses (MN 0 "_") [clause]) -- collect together later

266+ return (PClauses (MN 2 "_") [clause]) -- collect together later

257267

258268pClause :: SyntaxInfo -> IParser PClause

259269pClause syn

@@ -262,22 +272,30 @@ pClause syn

262272 args <- many (pHSimpleExpr syn)

263273 lchar '='

264274 rhs <- pExpr syn

265− return $ PClause n (PApp (PRef n) iargs args) rhs)

275+ wheres <- option [] (pWhereblock syn)

276+ return $ PClause n (PApp (PRef n) (iargs ++ map PExp args)) rhs wheres)

266277 <|> do l <- pSimpleExpr syn

267278 op <- operator

268279 let n = UN [op]

269280 r <- pSimpleExpr syn

270281 lchar '='

271282 rhs <- pExpr syn

272− return $ PClause n (PApp (PRef n) [] [l,r]) rhs

283+ wheres <- option [] (pWhereblock syn)

284+ return $ PClause n (PApp (PRef n) [PExp l,PExp r]) rhs wheres

285+

286+pWhereblock :: SyntaxInfo -> IParser [PDecl]

287+pWhereblock syn = do reserved "where"; lchar '{'

288+ ds <- many1 $ pFunDecl syn;

289+ lchar '}';

290+ return $ concat ds

273291

274292-- Dealing with implicit arguments

275293

276294implicit :: SyntaxInfo -> Name -> PTerm -> IParser PTerm

277295implicit syn n ptm

278296 = do i <- getState

279− let (tm', name_arity) = implicitise syn i ptm

280− setState (i { idris_implicits = addDef n name_arity (idris_implicits i) })

297+ let (tm', impdata) = implicitise syn i ptm

298+ setState (i { idris_implicits = addDef n impdata (idris_implicits i) })

281299 return tm'

282300

283301