a2a5141 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow interleaving of explicit and implicit arguments in top level types

a2a5141Edwin Brady15 years ago

src/Core/Elaborate.hs+2−2

compare with master

unifiedsplit

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

196 when i (movelast n)

197 doClaims sc' is (n : claims)

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

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

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

200

201 mkMN n@(MN _ _) = n

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

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

233 claim n (forget t)

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

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

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

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

237

238 elabClaims [] = return ()

239 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

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

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

292 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

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

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

296 se p env (Constant c) = show c

src/Idris/AbsSyntax.hs+97−67

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

9import Control.Monad.State

10import Data.List

11import Data.Char

12+import Debug.Trace

13data IOption = IOption { opt_logLevel :: Int }

14data IOption = IOption { opt_logLevel :: Int }

14 deriving (Show, Eq)

15 deriving (Show, Eq)

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

23data IState = IState { tt_ctxt :: Context,

24data IState = IState { tt_ctxt :: Context,

24 idris_infixes :: [FixDecl],

25 idris_infixes :: [FixDecl],

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

26+ idris_implicits :: Ctxt [PArg],

26 idris_log :: String,

27 idris_log :: String,

27 idris_options :: IOption

28 idris_options :: IOption

28 }

29 }

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

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

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

100 deriving Functor

101 deriving Functor

101

102

102−data PClause' t = PClause Name t t

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

103 deriving Functor

104 deriving Functor

104

105

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

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

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

112

113

113type PDecl = PDecl' PTerm

114type PDecl = PDecl' PTerm

114type PData = PData' PTerm

115type PData = PData' PTerm

115−type PClause = PClause' PTerm

116+type PClause = PClause' PTerm

116−-- High level language terms

117

118+-- High level language terms

119+--

118data PTerm = PQuote Raw

120data PTerm = PQuote Raw

119 | PRef Name

121 | PRef Name

120 | PLam Name PTerm PTerm

122 | PLam Name PTerm PTerm

121 | PPi Plicity Name PTerm PTerm

123 | PPi Plicity Name PTerm PTerm

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

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

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

125+ | PApp PTerm [PArg]

124 | PHidden PTerm -- irrelevant or hidden pattern

126 | PHidden PTerm -- irrelevant or hidden pattern

125 | PSet

127 | PSet

126 | PConstant Const

128 | PConstant Const

127 | Placeholder

129 | Placeholder

128

130

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

132+ | PExp { getTm :: t }

133+ deriving (Show, Functor)

134+

135+type PArg = PArg' PTerm

136+

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

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

130

138

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

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

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

151 show d = showDImp False d

159 show d = showDImp False d

152

160

153showCImp :: Bool -> PClause -> String

161showCImp :: Bool -> PClause -> String

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

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

155−

163+ ++ " where " ++ show w

156showDImp :: Bool -> PData -> String

164showDImp :: Bool -> PData -> String

157showDImp impl (PDatadecl n ty cons)

165showDImp impl (PDatadecl n ty cons)

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

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

159 ++ showSep "\n\t| "

167 ++ showSep "\n\t| "

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

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

161

169

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+

162showImp :: Bool -> PTerm -> String

183showImp :: Bool -> PTerm -> String

163showImp impl tm = se 10 tm where

184showImp impl tm = se 10 tm where

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

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

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

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

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

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

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

170 ") -> " ++ se 10 sc

191 ") -> " ++ 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

172 se p (PPi Imp n ty sc)

193 se p (PPi Imp n ty sc)

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

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

174 "} -> " ++ se 10 sc

195 "} -> " ++ se 10 sc

175 | otherwise = se 10 sc

196 | otherwise = se 10 sc

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

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

177 | not impl = show f

198 | not impl = show f

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

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

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

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

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

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

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

181− se p (PApp f imps args)

203+ se p (PApp f as)

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

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

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

183− ++ concatMap seArg args

206+ ++ concatMap seArg args

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

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

185 se p PSet = "Set"

208 se p PSet = "Set"

186 se p (PConstant c) = show c

209 se p (PConstant c) = show c

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

197 where

220 where

198 ni env (PRef n)

221 ni env (PRef n)

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

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

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

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

201− concatMap (ni env) es

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

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

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

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

204 ni env (PHidden tm) = ni env tm

226 ni env (PHidden tm) = ni env tm

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

212 = case lookupCtxt n (idris_implicits ist) of

234 = case lookupCtxt n (idris_implicits ist) of

213 Nothing -> [n]

235 Nothing -> [n]

214 _ -> []

236 _ -> []

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

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

216− concatMap (ni env) es

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

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

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

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

219 ni env (PHidden tm) = ni env tm

240 ni env (PHidden tm) = ni env tm

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

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

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

230 (PRef inferTy)))]

251 (PRef inferTy)))]

231

252

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

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

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

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

234

255

235getInferTerm, getInferType :: Term -> Term

256getInferTerm, getInferType :: Term -> Term

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

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

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

247-- argument position.

268-- argument position.

248

269

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

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

250implicitise syn ist tm

271implicitise syn ist tm

251 = let uvars = using syn

272 = let uvars = using syn

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

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

253 if null ns

274 if null ns

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

275+ then (tm, reverse declimps)

255 else implicitise syn ist (pibind uvars ns tm)

276 else implicitise syn ist (pibind uvars ns tm)

256 where

277 where

257− imps env (PApp f is es)

278+ imps top env (PApp f as)

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

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

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

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

260− let esn = concatMap (namesIn ist) es

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

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

262− imps env (PPi Imp n ty sc)

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

263− = do imps env ty

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

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

284+ (decls , ns) <- get

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

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

266− imps (n:env) sc

286+ imps True (n:env) sc

267− imps env (PPi Exp n ty sc)

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

268− = do imps env ty

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

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

289+ (PRef x) -> namesIn ist sc

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

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

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

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

271− imps (n:env) sc

293+ imps True (n:env) sc

272− imps env (PLam n ty sc)

294+ imps top env (PLam n ty sc)

273− = do imps env ty

295+ = do imps False env ty

274− imps (n:env) sc

296+ imps False (n:env) sc

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

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

276− imps env _ = return ()

298+ imps top env _ = return ()

277

299

278 pibind using [] sc = sc

300 pibind using [] sc = sc

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

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

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

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

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

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

282

304

305+-- Add implicit arguments in function calls

306+

283addImpl :: IState -> PTerm -> PTerm

307addImpl :: IState -> PTerm -> PTerm

284addImpl ist ptm = ai [] ptm

308addImpl ist ptm = ai [] ptm

285 where

309 where

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

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

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

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

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

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

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

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

313+ aiFn env (PRef f) as'

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

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

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

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

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

294− aiFn env f' is' es'

316+ aiFn env f' as'

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

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

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

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

297 PLam n ty' sc'

319 PLam n ty' sc'

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

301 ai env (PHidden tm) = PHidden (ai env tm)

323 ai env (PHidden tm) = PHidden (ai env tm)

302 ai env tm = tm

324 ai env tm = tm

303

325

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

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

305 = case lookupCtxt f (idris_implicits ist) of

327 = case lookupCtxt f (idris_implicits ist) of

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

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

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

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

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

330+ aiFn env f as = pApp 1 f as

309

331

310− pApp a f [] [] = f

332+ pApp a f [] = f

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

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

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

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

313

335

314 appRest f [] = f

336 appRest f [] = f

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

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

316−

338+

317− insertImpl [] given = []

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

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

341+ PExp tm : insertImpl ps given

318− insertImpl (n:ns) given

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

319− = case lookup n given of

343+ case find n given [] of

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

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

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

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

322−

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)

323

353

src/Idris/Delaborate.hs+7−4

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

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

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

29 mkPApp n args

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

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

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

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

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

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

33+

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

35+ imp (PExp _) arg = PExp arg

src/Idris/ElabDecls.hs+20−11

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

12import Core.CaseTree

14import Control.Monad

15+import Debug.Trace

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

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

17elabType n ty

18elabType n ty

18 = do ctxt <- getContext

19 = do ctxt <- getContext

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

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

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

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

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

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

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

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

70 tclift $ recheck ctxt [] vtm

72 tclift $ recheck ctxt [] vtm

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

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

73−elabClause (PClause _ lhs rhs)

75+elabClause (PClause _ lhs rhs whereblock)

74 = do ctxt <- getContext

76 = do ctxt <- getContext

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

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

76 -- pattern bindings

78 -- pattern bindings

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

80 let lhs_ty = getInferType lhs'

82 let lhs_ty = getInferType lhs'

81 logLvl 3 (show lhs_tm)

83 logLvl 3 (show lhs_tm)

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

84 (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.

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

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

84 iLOG (showImp True rhs)

91 iLOG (showImp True rhs)

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

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

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

124 when pattern -- convert remaining holes to pattern vars

131 when pattern -- convert remaining holes to pattern vars

125 mkPat

132 mkPat

126 where

133 where

134+ isph arg = case getTm arg of

127− isph (_, Placeholder) = True

135+ Placeholder -> True

128− isph _ = False

136+ _ -> False

129

137

138+ toElab arg = case getTm arg of

130− toElab (_, Placeholder) = Nothing

139+ Placeholder -> Nothing

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

140+ v -> Just (elab' v)

132

141

133 mkPat = do hs <- get_holes

142 mkPat = do hs <- get_holes

134 case hs of

143 case hs of

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

154 elab' ty

163 elab' ty

155 elab' sc

164 elab' sc

156 solve

165 solve

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

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

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

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

159 solve

168 solve

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

169+ elabArgs ns (map getTm args))

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

170+ (do apply_elab f (map toElab args)

162 solve)

171 solve)

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

172+ elab' (PApp f [arg])

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

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

165 solve

174 solve

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

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

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

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

src/Idris/Parser.hs+37−19

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

55-- Collect PClauses with the same function name

56collect :: [PDecl] -> [PDecl]

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

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

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

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

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

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

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

61collect (d : ds) = d : collect ds

62collect [] = []

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

75 return [fmap (addImpl i) d]

76 <|> try (pUsing syn)

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+

78--------- Top Level Declarations ---------

85--------- Top Level Declarations ---------

80pDecl' :: SyntaxInfo -> IParser PDecl

87pDecl' :: SyntaxInfo -> IParser PDecl

81pDecl' syn

88pDecl' syn

82 = try pFixity

89 = try pFixity

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

90+ <|> pFunDecl' syn

84− ty' <- implicit syn n ty

85− return (PTy n ty'))

86 <|> try (pData syn)

91 <|> try (pData 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'))

87− <|> try (pPattern syn)

97+ <|> try (pPattern syn)

89pUsing :: SyntaxInfo -> IParser [PDecl]

99pUsing :: SyntaxInfo -> IParser [PDecl]

90pUsing syn =

100pUsing syn =

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

148pApp syn = do f <- pSimpleExpr syn

158pApp syn = do f <- pSimpleExpr syn

149 iargs <- many (pImplicitArg syn)

159 iargs <- many (pImplicitArg syn)

150 args <- many1 (pSimpleExpr syn)

160 args <- many1 (pSimpleExpr syn)

151− return (PApp f iargs args)

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

152

162

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

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

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

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

155 lchar '}'

165 lchar '}'

156− return (n, v)

166+ return (PImp n v)

157

167

158pTSig syn = do lchar ':'

168pTSig syn = do lchar ':'

159 pExpr syn

169 pExpr syn

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

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

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

194

204

195table fixes

205table fixes

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

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

197 ++ toTable (reverse fixes) ++

207 ++ 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],

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

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

200

210

201toTable fs = map (map toBin)

211toTable fs = map (map toBin)

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

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

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

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

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

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

205 toBin (Fix f op) = binary op

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

207 assoc (Infixl _) = AssocLeft

217 assoc (Infixl _) = AssocLeft

208 assoc (Infixr _) = AssocRight

218 assoc (Infixr _) = AssocRight

209 assoc (InfixN _) = AssocNone

219 assoc (InfixN _) = AssocNone

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

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

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

232

242

233mkPApp t [] = t

243mkPApp t [] = t

234−mkPApp t xs = PApp t [] xs

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

235

245

236bindArgs :: [PTerm] -> PTerm -> PTerm

246bindArgs :: [PTerm] -> PTerm -> PTerm

237bindArgs [] t = t

247bindArgs [] t = t

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

253

263

254pPattern :: SyntaxInfo -> IParser PDecl

264pPattern :: SyntaxInfo -> IParser PDecl

255pPattern syn = do clause <- pClause syn

265pPattern syn = do clause <- pClause syn

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

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

257

267

258pClause :: SyntaxInfo -> IParser PClause

268pClause :: SyntaxInfo -> IParser PClause

259pClause syn

269pClause syn

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

262 args <- many (pHSimpleExpr syn)

272 args <- many (pHSimpleExpr syn)

263 lchar '='

273 lchar '='

264 rhs <- pExpr syn

274 rhs <- pExpr syn

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

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

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

266 <|> do l <- pSimpleExpr syn

277 <|> do l <- pSimpleExpr syn

267 op <- operator

278 op <- operator

268 let n = UN [op]

279 let n = UN [op]

269 r <- pSimpleExpr syn

280 r <- pSimpleExpr syn

270 lchar '='

281 lchar '='

271 rhs <- pExpr syn

282 rhs <- pExpr syn

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

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

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

273

291

274-- Dealing with implicit arguments

292-- Dealing with implicit arguments

275

293

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

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

277implicit syn n ptm

295implicit syn n ptm

278 = do i <- getState

296 = do i <- getState

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

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

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

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

281 return tm'

299 return tm'

282

300

283

301