e0cab49 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+6−6

compare with master

unifiedsplit

@@ -1242,7 +1242,7 @@ addUsingImpls syn n fc t

1242 -- if all of args in ns, then add it

1243 doAdd (UImplicit n ty : cs) ns t

1244 | elem n ns

1245− = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)

1245+ = PPi (Imp [] Dynamic False False) n ty (doAdd cs ns t)

1246 | otherwise = doAdd cs ns t

1247

1248 -- bind the free names which weren't in the using block

@@ -1250,7 +1250,7 @@ addUsingImpls syn n fc t

1250 bindFree (n:ns) tm

1251 | elem n (map iname uimpls) = bindFree ns tm

1252 | otherwise

1253− = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)

1253+ = PPi (Imp [] Dynamic False False) n Placeholder (bindFree ns tm)

1254

1255 getArgnames (PPi _ n c sc)

1256 = n : getArgnames sc

@@ -1269,7 +1269,7 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1269 getImps (Bind n (Pi _ t _) sc) imps

1270 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1271 where

1272− argInfo n (Imp opt _ _) t'

1272+ argInfo n (Imp opt _ _ _) t'

1273 = (True, PImp (getPriority i t') True opt n t')

1274 argInfo n (Exp opt _ _) t'

1275 = (InaccessibleArg `elem` opt,

@@ -1359,7 +1359,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1359 = do (decls, ns) <- get

1360 let isn = concatMap (namesIn uvars ist) (map getTm as)

1361 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1362− imps top env (PPi (Imp l _ _) n ty sc)

1362+ imps top env (PPi (Imp l _ _ _) n ty sc)

1363 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]

1364 (decls , ns) <- get

1365 put (PImp (getPriority ist ty) True l n Placeholder : decls,

@@ -1427,8 +1427,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1427 pibind using [] sc = sc

1428 pibind using (n:ns) sc

1429 = case lookup n using of

1430− Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)

1430+ Just ty -> PPi (Imp [] Dynamic False False) n ty (pibind using ns sc)

1431− Nothing -> PPi (Imp [] Dynamic False) n Placeholder

1431+ Nothing -> PPi (Imp [] Dynamic False False) n Placeholder

1432 (pibind using ns sc)

1433

1434-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+10−3

@@ -488,7 +488,9 @@ deriving instance NFData Static

488-- Mark bindings with their explicitness, and laziness

489data Plicity = Imp { pargopts :: [ArgOpt],

490 pstatic :: Static,

491− pparam :: Bool }

491+ pparam :: Bool,

492+ pscoped :: Bool -- forall bound

493+ }

492 | Exp { pargopts :: [ArgOpt],

494 | Exp { pargopts :: [ArgOpt],

493 pstatic :: Static,

495 pstatic :: Static,

494 pparam :: Bool } -- this is a param (rather than index)

496 pparam :: Bool } -- this is a param (rather than index)

@@ -504,7 +506,12 @@ deriving instance Binary Plicity

504deriving instance NFData Plicity

506deriving instance NFData Plicity

505!-}

507!-}

506

508

509+is_scoped :: Plicity -> Bool

510+is_scoped (Imp _ _ _ s) = s

511+is_scoped _ = False

512+

507−impl = Imp [] Dynamic False

513+impl = Imp [] Dynamic False False

514+forall_imp = Imp [] Dynamic False True

508expl = Exp [] Dynamic False

515expl = Exp [] Dynamic False

509expl_param = Exp [] Dynamic True

516expl_param = Exp [] Dynamic True

510constraint = Constraint [] Static

517constraint = Constraint [] Static

@@ -1326,7 +1333,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1326 case s of

1333 case s of

1327 Static -> text "[static]" <> space

1334 Static -> text "[static]" <> space

1328 _ -> empty

1335 _ -> empty

1329− prettySe p bnd (PPi (Imp l s _) n ty sc)

1336+ prettySe p bnd (PPi (Imp l s _ fa) n ty sc)

1330 | ppopt_impl ppo =

1337 | ppopt_impl ppo =

1331 bracket p startPrec $

1338 bracket p startPrec $

1332 lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

1339 lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

src/Idris/Core/Elaborate.hs+17−12

@@ -369,8 +369,8 @@ intro n = processTactic' (Intro n)

369introTy :: Raw -> Maybe Name -> Elab' aux ()

370introTy ty n = processTactic' (IntroTy ty n)

371

372−forall :: Name -> Raw -> Elab' aux ()

372+forall :: Name -> Bool -> Raw -> Elab' aux ()

373−forall n t = processTactic' (Forall n t)

373+forall n i t = processTactic' (Forall n i t)

374

375letbind :: Name -> Raw -> Raw -> Elab' aux ()

376letbind n t v = processTactic' (LetBind n t v)

@@ -493,7 +493,9 @@ prepare_apply fn imps =

493 env <- get_env

494 -- let claims = getArgs ty imps

495 -- claims <- mkClaims (normalise ctxt env ty) imps []

496− claims <- mkClaims (finalise ty) imps [] (map fst env)

496+ claims <- mkClaims (finalise ty)

497+ (normalise ctxt env (finalise ty))

498+ imps [] (map fst env)

497 ES (p, a) s prev <- get

499 ES (p, a) s prev <- get

498 -- reverse the claims we made so that args go left to right

500 -- reverse the claims we made so that args go left to right

499 let n = length (filter not imps)

501 let n = length (filter not imps)

@@ -502,11 +504,12 @@ prepare_apply fn imps =

502 return $! claims

504 return $! claims

503 where

505 where

504 mkClaims :: Type -- ^ The type of the operation being applied

506 mkClaims :: Type -- ^ The type of the operation being applied

507+ -> Type -- ^ Normalised version if we need it

505 -> [Bool] -- ^ Whether the arguments are implicit

508 -> [Bool] -- ^ Whether the arguments are implicit

506 -> [(Name, Name)] -- ^ Accumulator for produced claims

509 -> [(Name, Name)] -- ^ Accumulator for produced claims

507 -> [Name] -- ^ Hypotheses

510 -> [Name] -- ^ Hypotheses

508 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

511 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

509− mkClaims (Bind n' (Pi _ t_in _) sc) (i : is) claims hs =

512+ mkClaims (Bind n' (Pi _ t_in _) sc) (Bind _ _ scn) (i : is) claims hs =

510 do let t = rebind hs t_in

513 do let t = rebind hs t_in

511 n <- getNameFrom (mkMN n')

514 n <- getNameFrom (mkMN n')

512-- when (null claims) (start_unify n)

515-- when (null claims) (start_unify n)

@@ -514,9 +517,11 @@ prepare_apply fn imps =

514-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

517-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

515 claim n (forget t)

518 claim n (forget t)

516 when i (movelast n)

519 when i (movelast n)

517− mkClaims sc' is ((n', n) : claims) hs

520+ mkClaims sc' scn is ((n', n) : claims) hs

521+ -- if we run out of arguments, we need the normalised version...

522+ mkClaims t tn@(Bind _ _ sc) (i : is) cs hs = mkClaims tn tn (i : is) cs hs

518− mkClaims t [] claims _ = return $! (reverse claims)

523+ mkClaims t _ [] claims _ = return $! (reverse claims)

519− mkClaims _ _ _ _

524+ mkClaims _ _ _ _ _

520 | Var n <- fn

525 | Var n <- fn

521 = do ctxt <- get_context

526 = do ctxt <- get_context

522 case lookupTy n ctxt of

527 case lookupTy n ctxt of

@@ -693,11 +698,11 @@ simple_app fun arg appstr =

693

698

694-- Abstract over an argument of unknown type, giving a name for the hole

699-- Abstract over an argument of unknown type, giving a name for the hole

695-- which we'll fill with the argument type too.

700-- which we'll fill with the argument type too.

696−arg :: Name -> Name -> Elab' aux ()

701+arg :: Name -> Bool -> Name -> Elab' aux ()

697−arg n tyhole = do ty <- unique_hole tyhole

702+arg n i tyhole = do ty <- unique_hole tyhole

698− claim ty RType

703+ claim ty RType

699− movelast ty

704+ movelast ty

700− forall n (Var ty)

705+ forall n i (Var ty)

701

706

702-- try a tactic, if it adds any unification problem, return an error

707-- try a tactic, if it adds any unification problem, return an error

703no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()

708no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()

src/Idris/Core/ProofState.hs+6−6

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

69 | CheckIn Raw

70 | Intro (Maybe Name)

71 | IntroTy Raw (Maybe Name)

72− | Forall Name Raw

72+ | Forall Name Bool Raw

73 | LetBind Name Raw Raw

74 | ExpandLet Name Term

75 | Rewrite Raw

@@ -569,13 +569,13 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

569 _ -> lift $ tfail $ CantIntroduce t'

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

571

572−forall :: Name -> Raw -> RunTactic

572+forall :: Name -> Bool -> Raw -> RunTactic

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

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

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

575 unify' ctxt env tyt (TType (UVar 0))

576 unify' ctxt env t (TType (UVar 0))

577− return $ Bind n (Pi False tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

577+ return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

578−forall n ty ctxt env _ = fail "Can't pi bind here"

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

579

580patvar :: Name -> RunTactic

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

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

973 mktac HNF_Compute = hnf_compute

974 mktac (Intro n) = intro n

975 mktac (IntroTy ty n) = introTy ty n

976− mktac (Forall n t) = forall n t

976+ mktac (Forall n i t) = forall n i t

977 mktac (LetBind n t v) = letbind n t v

978 mktac (ExpandLet n b) = expandLet n b

979 mktac (Rewrite t) = rewrite t

src/Idris/DeepSeq.hs+2−2

@@ -94,8 +94,8 @@ instance NFData ArgOpt where

94 rnf _ = ()

95

96instance NFData Plicity where

97− rnf (Imp x1 x2 x3)

97+ rnf (Imp x1 x2 x3 x4)

98− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

98+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

99 rnf (Exp x1 x2 x3)

100 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

101 rnf (Constraint x1 x2)

src/Idris/Delaborate.hs+1−1

@@ -58,7 +58,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

58 de env _ (Bind n (Lam ty) sc)

59 = PLam un n (de env [] ty) (de ((n,n):env) [] sc)

60 de env ((PImp { argopts = opts }):is) (Bind n (Pi _ ty _) sc)

61− = PPi (Imp opts Dynamic False) n (de env [] ty) (de ((n,n):env) is sc)

61+ = PPi (Imp opts Dynamic False False) n (de env [] ty) (de ((n,n):env) is sc)

62 de env (PConstraint _ _ _ _:is) (Bind n (Pi _ ty _) sc)

63 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

64 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi _ ty _) sc)

src/Idris/Elab/Class.hs+5−4

@@ -133,7 +133,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

133 = do t' <- implicit' info syn allmeths n t

134 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

135 return ( (n, (toExp (map fst ps) Exp t')),

136− (n, (doc, o, (toExp (map fst ps) Imp t'))),

136+ (n, (doc, o, (toExp (map fst ps)

137+ (\ l s p -> Imp l s p False) t'))),

137 (n, (syn, o, t) ) )

138 (n, (syn, o, t) ) )

138 tdecl _ _ = ifail "Not allowed in a class declaration"

139 tdecl _ _ = ifail "Not allowed in a class declaration"

139

140

@@ -200,7 +201,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

200 return [PTy doc [] syn fc o m ty',

201 return [PTy doc [] syn fc o m ty',

201 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

202 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

202

203

203− getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

204+ getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

204 getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

205 getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

205 getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

206 getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

206 getMArgs _ = []

207 getMArgs _ = []

@@ -218,13 +219,13 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

218 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

219 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

219 rhsArgs [] _ = []

220 rhsArgs [] _ = []

220

221

221− insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

222+ insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

222 = PPi p n ty (insertConstraint c sc)

223 = PPi p n ty (insertConstraint c sc)

223 insertConstraint c sc = PPi (constraint { pstatic = Static })

224 insertConstraint c sc = PPi (constraint { pstatic = Static })

224 (sMN 0 "class") c sc

225 (sMN 0 "class") c sc

225

226

226 -- make arguments explicit and don't bind class parameters

227 -- make arguments explicit and don't bind class parameters

227− toExp ns e (PPi (Imp l s p) n ty sc)

228+ toExp ns e (PPi (Imp l s p _) n ty sc)

228 | n `elem` ns = toExp ns e sc

229 | n `elem` ns = toExp ns e sc

229 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

230 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

230 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

231 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

src/Idris/Elab/Instance.hs+2−2

@@ -199,7 +199,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

199 lamBind i (PPi _ n ty sc) sc'

200 = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

201 lamBind i _ sc = sc

202− methArgs i (PPi (Imp _ _ _) n ty sc)

202+ methArgs i (PPi (Imp _ _ _ _) n ty sc)

203 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

204 methArgs i (PPi (Exp _ _ _) n ty sc)

205 = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc

@@ -230,7 +230,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

230 conbind [] x = x

231

232 coninsert :: [(Name, PTerm)] -> PTerm -> PTerm

233− coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

233+ coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

234 coninsert cs sc = conbind cs sc

235

236 insertDefaults :: IState -> Name ->

src/Idris/Elab/Record.hs+4−4

@@ -130,13 +130,13 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

130-- ++ "\n" ++ pshow i v

131 putIState i)

132

133− getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc

133+ getBoundImpls (PPi (Imp _ _ _ _) n ty sc) = (n, ty) : getBoundImpls sc

134 getBoundImpls _ = []

135

136− getImplB k (PPi (Imp l s _) n Placeholder sc)

136+ getImplB k (PPi (Imp l s _ _) n Placeholder sc)

137 = getImplB k sc

138− getImplB k (PPi (Imp l s p) n ty sc)

138+ getImplB k (PPi (Imp l s p fa) n ty sc)

139− = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc

139+ = getImplB (\x -> k (PPi (Imp l s p fa) n ty x)) sc

140 getImplB k (PPi _ n ty sc)

141 = getImplB k sc

142 getImplB k _ = k

src/Idris/Elab/Utils.hs+1−1

@@ -56,7 +56,7 @@ inaccessibleImps _ _ _ = []

56

57-- Get the list of (index, name) of inaccessible arguments from the type.

58inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

59−inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)

59+inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

60 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

61inaccessibleArgs i (PPi plicity n ty t)

62 | InaccessibleArg `elem` pargopts plicity

src/Idris/ElabTerm.hs+27−6

@@ -244,7 +244,8 @@ elab ist info emode opts fn tm

244 then solveAuto ist fn False a

245 else return ()) as

246

247+ itm <- if not pattern then insertImpLam t else return t

247− ct <- insertCoerce ina t

248+ ct <- insertCoerce ina itm

248 t' <- insertLazy ct

249 t' <- insertLazy ct

249 g <- goal

250 g <- goal

250 tm <- get_term

251 tm <- get_term

@@ -468,17 +469,17 @@ elab ist info emode opts fn tm

468 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

469 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

469 elabE (ec { e_inarg = True }) (Just fc) sc

470 elabE (ec { e_inarg = True }) (Just fc) sc

470 solve

471 solve

471− elab' ina fc (PPi _ n Placeholder sc)

472+ elab' ina fc (PPi p n Placeholder sc)

472− = do attack; arg n (sMN 0 "ty")

473+ = do attack; arg n (is_scoped p) (sMN 0 "ty")

473 elabE (ina { e_inarg = True, e_intype = True }) fc sc

474 elabE (ina { e_inarg = True, e_intype = True }) fc sc

474 solve

475 solve

475− elab' ina fc (PPi _ n ty sc)

476+ elab' ina fc (PPi p n ty sc)

476 = do attack; tyn <- getNameFrom (sMN 0 "ty")

477 = do attack; tyn <- getNameFrom (sMN 0 "ty")

477 claim tyn RType

478 claim tyn RType

478 n' <- case n of

479 n' <- case n of

479 MN _ _ -> unique_hole n

480 MN _ _ -> unique_hole n

480 _ -> return n

481 _ -> return n

481− forall n' (Var tyn)

482+ forall n' (is_scoped p) (Var tyn)

482 focus tyn

483 focus tyn

483 let ec' = ina { e_inarg = True, e_intype = True }

484 let ec' = ina { e_inarg = True, e_intype = True }

484 elabE ec' fc ty

485 elabE ec' fc ty

@@ -594,13 +595,15 @@ elab ist info emode opts fn tm

594-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

595-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

595-- = lift $ tfail (Msg "Typecase is not allowed")

596-- = lift $ tfail (Msg "Typecase is not allowed")

596 -- if f is local, just do a simple_app

597 -- if f is local, just do a simple_app

597− elab' ina _ tm@(PApp fc (PRef _ f) args)

598+ elab' ina _ tm@(PApp fc (PRef _ f) args_in)

598 | pattern && not reflection && e_nomatching ina

599 | pattern && not reflection && e_nomatching ina

599 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

600 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

600 | otherwise

601 | otherwise

601 = do env <- get_env

602 = do env <- get_env

602 ty <- goal

603 ty <- goal

604+ fty <- get_type (Var f)

603 ctxt <- get_context

605 ctxt <- get_context

606+ let args = insertScopedImps (normalise ctxt env fty) args_in

604 let unmatchableArgs = if pattern

607 let unmatchableArgs = if pattern

605 then getUnmatchable (tt_ctxt ist) f

608 then getUnmatchable (tt_ctxt ist) f

606 else []

609 else []

@@ -1049,6 +1052,24 @@ elab ist info emode opts fn tm

1049 notImplicitable (PCase _ _ _) = True

1052 notImplicitable (PCase _ _ _) = True

1050 notImplicitable _ = False

1053 notImplicitable _ = False

1051

1054

1055+ insertScopedImps (Bind n (Pi True _ _) sc) xs

1056+ = pimp n Placeholder True : insertScopedImps sc xs

1057+ insertScopedImps (Bind n (Pi _ _ _) sc) (x : xs)

1058+ = x : insertScopedImps sc xs

1059+ insertScopedImps _ xs = xs

1060+

1061+ insertImpLam t =

1062+ do ty <- goal

1063+ env <- get_env

1064+ let ty' = normalise (tt_ctxt ist) env ty

1065+ addLam ty' t

1066+ where

1067+ addLam (Bind n (Pi True _ _) sc) t

1068+ = do impn <- unique_hole (sUN "imp")

1069+ t' <- addLam sc t

1070+ return (PLam emptyFC impn Placeholder t')

1071+ addLam _ t = return t

1072+

1052 insertCoerce ina t@(PCase _ _ _) = return t

1073 insertCoerce ina t@(PCase _ _ _) = return t

1053 insertCoerce ina t | notImplicitable t = return t

1074 insertCoerce ina t | notImplicitable t = return t

1054 insertCoerce ina t =

1075 insertCoerce ina t =

src/Idris/IBC.hs+4−2

@@ -1111,11 +1111,12 @@ instance Binary Static where

1111instance Binary Plicity where

1112 put x

1113 = case x of

1114− Imp x1 x2 x3 ->

1114+ Imp x1 x2 x3 x4 ->

1115 do putWord8 0

1116 put x1

1117 put x2

1118 put x3

1119+ put x4

1119 Exp x1 x2 x3 ->

1120 Exp x1 x2 x3 ->

1120 do putWord8 1

1121 do putWord8 1

1121 put x1

1122 put x1

@@ -1136,7 +1137,8 @@ instance Binary Plicity where

1136 0 -> do x1 <- get

1137 0 -> do x1 <- get

1137 x2 <- get

1138 x2 <- get

1138 x3 <- get

1139 x3 <- get

1140+ x4 <- get

1139− return (Imp x1 x2 x3)

1141+ return (Imp x1 x2 x3 x4)

1140 1 -> do x1 <- get

1142 1 -> do x1 <- get

1141 x2 <- get

1143 x2 <- get

1142 x3 <- get

1144 x3 <- get

src/Idris/ParseExpr.hs+4−2

@@ -883,8 +883,10 @@ pi syn =

883 symbol "->"

884 sc <- expr syn

885 if implicitAllowed syn

886− then return (bindList (PPi (Imp opts st False)) xt sc)

886+ then return (bindList (PPi (Imp opts st False False)) xt sc)

887+ -- TODO: TIDY BEFORE COMMITTING!

888+ else return (bindList (PPi (Imp opts st False True)) xt sc)))

887− else fail "no implicit arguments allowed here"))

889+ -- fail "no implicit arguments allowed here"))

888 <|> (do x <- opExpr syn

890 <|> (do x <- opExpr syn

889 (do symbol "->"

891 (do symbol "->"

890 sc <- expr syn

892 sc <- expr syn