488c5b7 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+15−15

@@ -1306,8 +1306,8 @@ expandParams dec ps ns infs tm = en 0 tm

13061306

13071307 nseq x y = nsroot x == nsroot y

13081308

1309− enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)

1310− enTacImp ql other = other

1309+ enTacImp ql (TacImp aos st scr rig) = TacImp aos st (en ql scr) rig

1310+ enTacImp ql other = other

13111311

13121312expandParamsD :: Bool -> -- True = RHS only

13131313 IState ->

@@ -1511,8 +1511,8 @@ addStatics n tm ptm =

15111511 -- if a name appears in an interface or tactic implicit index, it doesn't

15121512 -- affect its 'uniquely inferrable' from a static status since these are

15131513 -- resolved by searching.

1514− searchArg (Constraint _ _) = True

1515− searchArg (TacImp _ _ _) = True

1514+ searchArg (Constraint _ _ _) = True

1515+ searchArg (TacImp _ _ _ _) = True

15161516 searchArg _ = False

15171517

15181518 staticList sts (Bind n (Pi _ _ _ _) sc) = (n `elem` sts) : staticList sts sc

@@ -1547,14 +1547,14 @@ addUsingConstraints syn fc t

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

15481548 doAdd (UConstraint c args : cs) ns t

15491549 | all (\n -> elem n ns) args

1550− = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC

1550+ = PPi (Constraint [] Dynamic RigW) (sMN 0 "cu") NoFC

15511551 (mkConst c args) (doAdd cs ns t)

15521552 | otherwise = doAdd cs ns t

15531553

15541554 mkConst c args = PApp fc (PRef fc [] c)

15551555 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)

15561556

1557− getConstraints (PPi (Constraint _ _) _ _ c sc)

1557+ getConstraints (PPi (Constraint _ _ _) _ _ c sc)

15581558 = getcapp c ++ getConstraints sc

15591559 getConstraints (PPi _ _ _ c sc) = getConstraints sc

15601560 getConstraints _ = []

@@ -1628,17 +1628,17 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

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

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

16301630 where

1631− argInfo n (Imp opt _ _ _ _) Placeholder

1631+ argInfo n (Imp opt _ _ _ _ _) Placeholder

16321632 = (True, PImp 0 True opt n Placeholder)

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

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

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

1635− argInfo n (Exp opt _ _) t'

1635+ argInfo n (Exp opt _ _ _) t'

16361636 = (InaccessibleArg `elem` opt,

16371637 PExp (getPriority i t') opt n t')

1638− argInfo n (Constraint opt _) t'

1638+ argInfo n (Constraint opt _ _) t'

16391639 = (InaccessibleArg `elem` opt,

16401640 PConstraint 10 opt n t')

1641− argInfo n (TacImp opt _ scr) t'

1641+ argInfo n (TacImp opt _ scr _) t'

16421642 = (InaccessibleArg `elem` opt,

16431643 PTacImplicit 10 opt n scr t')

16441644 getImps (Bind n (Pi _ _ t _) sc) imps = impBind n t : getImps sc imps

@@ -1724,13 +1724,13 @@ implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

17241724 = do (decls, ns) <- get

17251725 let isn = nub (implNamesIn uvars ty)

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

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

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

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

17291729 (decls , ns) <- get

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

17311731 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

17321732 imps True (n:env) sc

1733− imps top env (PPi (Exp l _ _) n _ ty sc)

1733+ imps top env (PPi (Exp l _ _ _) n _ ty sc)

17341734 = do let isn = nub (implNamesIn uvars ty ++ case sc of

17351735 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]

17361736 _ -> [])

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

17381738 put (PExp (getPriority ist ty) l n Placeholder : decls,

17391739 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

17401740 imps True (n:env) sc

1741− imps top env (PPi (Constraint l _) n _ ty sc)

1741+ imps top env (PPi (Constraint l _ _) n _ ty sc)

17421742 = do let isn = nub (implNamesIn uvars ty ++ case sc of

17431743 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]

17441744 _ -> [])

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

17461746 put (PConstraint 10 l n Placeholder : decls,

17471747 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

17481748 imps True (n:env) sc

1749− imps top env (PPi (TacImp l _ scr) n _ ty sc)

1749+ imps top env (PPi (TacImp l _ scr _) n _ ty sc)

17501750 = do let isn = nub (implNamesIn uvars ty ++ case sc of

17511751 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]

17521752 _ -> [])

src/Idris/AbsSyntaxTree.hs+24−20

@@ -599,17 +599,21 @@ data Plicity = Imp { pargopts :: [ArgOpt]

599599 , pparam :: Bool

600600 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level

601601 , pinsource :: Bool -- ^ Explicitly written in source

602+ , pcount :: RigCount

602603 }

603604 | Exp { pargopts :: [ArgOpt]

604605 , pstatic :: Static

605606 , pparam :: Bool -- ^ this is a param (rather than index)

607+ , pcount :: RigCount

606608 }

607609 | Constraint { pargopts :: [ArgOpt]

608− , pstatic :: Static

610+ , pstatic :: Static

611+ , pcount :: RigCount

609612 }

610613 | TacImp { pargopts :: [ArgOpt]

611614 , pstatic :: Static

612615 , pscript :: PTerm

616+ , pcount :: RigCount

613617 }

614618 deriving (Show, Eq, Ord, Data, Generic, Typeable)

615619

@@ -618,24 +622,24 @@ deriving instance Binary Plicity

618622!-}

619623

620624is_scoped :: Plicity -> Maybe ImplicitInfo

621−is_scoped (Imp _ _ _ s _) = s

622−is_scoped _ = Nothing

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

626+is_scoped _ = Nothing

623627

624628-- Top level implicit

625−impl = Imp [] Dynamic False (Just (Impl False True False)) False

629+impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW

626630-- Machine generated top level implicit

627−impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False

631+impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW

628632

629633-- Scoped implicits

630−forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False

631−forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False

634+forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW

635+forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW

632636

633−expl = Exp [] Dynamic False

634−expl_param = Exp [] Dynamic True

637+expl = Exp [] Dynamic False RigW

638+expl_param = Exp [] Dynamic True RigW

635639

636−constraint = Constraint [] Static

640+constraint = Constraint [] Static RigW

637641

638−tacimpl t = TacImp [] Dynamic t

642+tacimpl t = TacImp [] Dynamic t RigW

639643

640644data FnOpt = Inlinable -- ^ always evaluate when simplifying

641645 | TotalFn | PartialFn | CoveringFn

@@ -1815,7 +1819,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18151819 depth d . bracket p startPrec . group . align $

18161820 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>

18171821 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)

1818− prettySe d p bnd (PPi (Exp l s _) n _ ty sc)

1822+ prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)

18191823 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs

18201824 || ppopt_pinames ppo && uname n =

18211825 depth d . bracket p startPrec . group $

@@ -1835,7 +1839,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18351839 case s of

18361840 Static -> text "%static" <> space

18371841 _ -> empty

1838− prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)

1842+ prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)

18391843 | ppopt_impl ppo =

18401844 depth d . bracket p startPrec $

18411845 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>

@@ -1846,13 +1850,13 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18461850 case s of

18471851 Static -> text "%static" <> space

18481852 _ -> empty

1849− prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =

1853+ prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =

18501854 depth d . bracket p startPrec $

18511855 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1852− prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =

1856+ prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =

18531857 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

18541858 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1855− prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =

1859+ prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =

18561860 depth d . bracket p startPrec $

18571861 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

18581862 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

@@ -2380,7 +2384,7 @@ allNamesIn tm = nub $ ni 0 [] tm

23802384 ni i env (PUnquote tm) = ni (i - 1) env tm

23812385 ni i env tm = concatMap (ni i env) (children tm)

23822386

2383− niTacImp i env (TacImp _ _ scr) = ni i env scr

2387+ niTacImp i env (TacImp _ _ scr _) = ni i env scr

23842388 niTacImp _ _ _ = []

23852389

23862390

@@ -2416,7 +2420,7 @@ boundNamesIn tm = S.toList (ni 0 S.empty tm)

24162420 niTms i set [] = set

24172421 niTms i set (x : xs) = niTms i (ni i set x) xs

24182422

2419− niTacImp i set (TacImp _ _ scr) = ni i set scr

2423+ niTacImp i set (TacImp _ _ scr _) = ni i set scr

24202424 niTacImp i set _ = set

24212425

24222426-- Return names which are valid implicits in the given term (type).

@@ -2527,7 +2531,7 @@ namesIn uvars ist tm = nub $ ni 0 [] tm

25272531

25282532 ni i env tm = concatMap (ni i env) (children tm)

25292533

2530− niTacImp i env (TacImp _ _ scr) = ni i env scr

2534+ niTacImp i env (TacImp _ _ scr _) = ni i env scr

25312535 niTacImp _ _ _ = []

25322536

25332537-- Return which of the given names are used in the given term.

@@ -2562,7 +2566,7 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm

25622566

25632567 ni i env tm = concatMap (ni i env) (children tm)

25642568

2565− niTacImp i env (TacImp _ _ scr) = ni i env scr

2569+ niTacImp i env (TacImp _ _ scr _) = ni i env scr

25662570 niTacImp _ _ _ = []

25672571

25682572-- Return the list of inaccessible (= dotted) positions for a name.

src/Idris/CaseSplit.hs+3−3

@@ -408,14 +408,14 @@ getClause l fn un fp

408408 return (showLHSName un ++ " " ++ ap ++ "= ?"

409409 ++ showRHSName un ++ "_rhs")

410410 where mkApp :: IState -> PTerm -> [Name] -> String

411− mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used

411+ mkApp i (PPi (Exp _ _ False _) (MN _ _) _ ty sc) used

412412 = let n = getNameFrom i used ty in

413413 show n ++ " " ++ mkApp i sc (n : used)

414− mkApp i (PPi (Exp _ _ False) (UN n) _ ty sc) used

414+ mkApp i (PPi (Exp _ _ False _) (UN n) _ ty sc) used

415415 | thead n == '_'

416416 = let n = getNameFrom i used ty in

417417 show n ++ " " ++ mkApp i sc (n : used)

418− mkApp i (PPi (Exp _ _ False) n _ _ sc) used

418+ mkApp i (PPi (Exp _ _ False _) n _ _ sc) used

419419 = show n ++ " " ++ mkApp i sc (n : used)

420420 mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used

421421 mkApp i _ _ = ""

src/Idris/Delaborate.hs+7−7

@@ -139,25 +139,25 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

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

140140 de env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)

141141 | toplevel_imp impl -- information in 'imps' repeated

142− = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

142+ = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)

143143 de env is (Bind n (Pi rig (Just impl) ty _) sc)

144144 | tcimplementation impl

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

146146 | otherwise

147− = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

147+ = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)

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

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

149+ = PPi (Imp opts Dynamic False Nothing False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)

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

151− = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

151+ = PPi (constraint { pcount = rig}) n NoFC (de env [] ty) (de ((n,n):env) is sc)

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

153− = PPi (tacimpl tac) n NoFC (de env [] ty) (de ((n,n):env) is sc)

153+ = PPi ((tacimpl tac) { pcount = rig }) n NoFC (de env [] ty) (de ((n,n):env) is sc)

154154 de env (plic:is) (Bind n (Pi rig _ ty _) sc)

155− = PPi (Exp (argopts plic) Dynamic False)

155+ = PPi (Exp (argopts plic) Dynamic False rig)

156156 n NoFC

157157 (de env [] ty)

158158 (de ((n,n):env) is sc)

159159 de env [] (Bind n (Pi rig _ ty _) sc)

160− = PPi expl n NoFC (de env [] ty) (de ((n,n):env) [] sc)

160+ = PPi (expl { pcount = rig }) n NoFC (de env [] ty) (de ((n,n):env) [] sc)

161161

162162 de env imps (Bind n (Let ty val) sc)

163163 | docases

src/Idris/Docs.hs+3−3

@@ -220,7 +220,7 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_

220220 dumpImplementation :: PTerm -> Doc OutputAnnotation

221221 dumpImplementation = pprintPTerm ppo params' [] infixes

222222

223− prettifySubInterfaces (PPi (Constraint _ _) _ _ tm _) = prettifySubInterfaces tm

223+ prettifySubInterfaces (PPi (Constraint _ _ _) _ _ tm _) = prettifySubInterfaces tm

224224 prettifySubInterfaces (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubInterfaces t1) (prettifySubInterfaces t2)

225225 prettifySubInterfaces (PApp fc ref args) = PApp fc ref $ updateArgs pNames args

226226 prettifySubInterfaces tm = tm

@@ -235,7 +235,7 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_

235235 updateRef nm (PRef fc _ _) = PRef fc [] nm

236236 updateRef _ pt = pt

237237

238− isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'

238+ isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'

239239 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

240240 isSubInterface _ = False

241241

@@ -356,7 +356,7 @@ docInterface n ci

356356 getDImpl (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t

357357 getDImpl _ = Nothing

358358

359− isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))

359+ isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))

360360 = nm == n && map getTm args == map getTm args'

361361 isSubInterface (PPi _ _ _ _ pt)

362362 = isSubInterface pt

src/Idris/Elab/Implementation.hs+5−5

@@ -310,16 +310,16 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

310310 where

311311 needed is p = pname p `elem` map pname is

312312

313− lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'

313+ lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'

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

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

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

317317 lamBind i _ sc = sc

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

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

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

320− methArgs i (PPi (Exp _ _ _) n _ ty sc)

320+ methArgs i (PPi (Exp _ _ _ _) n _ ty sc)

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

322− methArgs i (PPi (Constraint _ _) n _ ty sc)

322+ methArgs i (PPi (Constraint _ _ _) n _ ty sc)

323323 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc

324324 methArgs i _ = []

325325

@@ -354,7 +354,7 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

354354 extrabind [] x = x

355355

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

357− coninsert cs ex (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs ex sc)

357+ coninsert cs ex (PPi p@(Imp _ _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs ex sc)

358358 coninsert cs ex sc = conbind cs (extrabind ex sc)

359359

360360 -- Reorder declarations to be in the same order as defined in the

src/Idris/Elab/Interface.hs+7−7

@@ -210,7 +210,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

210210 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

211211 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

212212 (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

213− (\ l s p -> Imp l s p Nothing True) t'))),

213+ (\ l s p r -> Imp l s p Nothing True r) t'))),

214214 (n, (nfc, syn, o, t) ) )

215215 tdecl impps allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))

216216 = do let o = []

@@ -218,7 +218,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

218218 logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'

219219 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

220220 (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

221− (\ l s p -> Imp l s p Nothing True) t'))),

221+ (\ l s p r -> Imp l s p Nothing True r) t'))),

222222 (n, (nfc, syn, o, t) ) )

223223 tdecl impps allmeths (PData doc _ syn _ _ _)

224224 = ierror $ At fc (Msg "Data definitions not allowed in an interface declaration")

@@ -294,9 +294,9 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

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

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

296296

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

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

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

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

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

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

300300 getMArgs _ = []

301301

302302 getMeth :: [Name] -> [Name] -> Name -> PTerm

@@ -337,9 +337,9 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

337337 addC _ _ tm = tm

338338

339339 -- make arguments explicit and don't bind interface parameters

340− toExp ns e (PPi (Imp l s p _ _) n fc ty sc)

340+ toExp ns e (PPi (Imp l s p _ _ r) n fc ty sc)

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

342− | otherwise = PPi (e l s p) n fc ty (toExp ns e sc)

342+ | otherwise = PPi (e l s p r) n fc ty (toExp ns e sc)

343343 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

344344 toExp ns e sc = sc

345345

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

@@ -460,10 +460,10 @@ in_name n = n

460460

461461-- | Creates a PArg with a given plicity, name, and term.

462462asArg :: Plicity -> Name -> PTerm -> PArg

463−asArg (Imp os _ _ _ _) n t = PImp 0 False os n t

464−asArg (Exp os _ _) n t = PExp 0 os n t

465−asArg (Constraint os _) n t = PConstraint 0 os n t

466−asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t

463+asArg (Imp os _ _ _ _ _) n t = PImp 0 False os n t

464+asArg (Exp os _ _ _) n t = PExp 0 os n t

465+asArg (Constraint os _ _) n t = PConstraint 0 os n t

466+asArg (TacImp os _ s _) n t = PTacImplicit 0 os n s t

467467

468468-- | Machine name "rec".

469469recName :: Name

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

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

15871587 fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole

15881588

15891589 addAutoBind :: Plicity -> Name -> ElabD ()

1590− addAutoBind (Imp _ _ _ _ False) n

1590+ addAutoBind (Imp _ _ _ _ False _) n

15911591 = updateAux (\est -> est { auto_binds = n : auto_binds est })

15921592 addAutoBind _ _ = return ()

15931593

src/Idris/IBC.hs+17−9

@@ -47,7 +47,7 @@ import System.Directory

4747import System.FilePath

4848

4949ibcVersion :: Word16

50−ibcVersion = 156

50+ibcVersion = 157

5151

5252-- | When IBC is being loaded - we'll load different things (and omit

5353-- different structures/definitions) depending on which phase we're in.

@@ -1328,26 +1328,30 @@ instance Binary Static where

13281328instance Binary Plicity where

13291329 put x

13301330 = case x of

1331− Imp x1 x2 x3 x4 _ ->

1331+ Imp x1 x2 x3 x4 _ x5 ->

13321332 do putWord8 0

13331333 put x1

13341334 put x2

13351335 put x3

13361336 put x4

1337− Exp x1 x2 x3 ->

1337+ put x5

1338+ Exp x1 x2 x3 x4 ->

13381339 do putWord8 1

13391340 put x1

13401341 put x2

13411342 put x3

1342− Constraint x1 x2 ->

1343+ put x4

1344+ Constraint x1 x2 x3 ->

13431345 do putWord8 2

13441346 put x1

13451347 put x2

1346− TacImp x1 x2 x3 ->

1348+ put x3

1349+ TacImp x1 x2 x3 x4 ->

13471350 do putWord8 3

13481351 put x1

13491352 put x2

13501353 put x3

1354+ put x4

13511355 get

13521356 = do i <- getWord8

13531357 case i of

@@ -1355,18 +1359,22 @@ instance Binary Plicity where

13551359 x2 <- get

13561360 x3 <- get

13571361 x4 <- get

1358− return (Imp x1 x2 x3 x4 False)

1362+ x5 <- get

1363+ return (Imp x1 x2 x3 x4 False x5)

13591364 1 -> do x1 <- get

13601365 x2 <- get

13611366 x3 <- get

1362− return (Exp x1 x2 x3)

1367+ x4 <- get

1368+ return (Exp x1 x2 x3 x4)

13631369 2 -> do x1 <- get

13641370 x2 <- get

1365− return (Constraint x1 x2)

1371+ x3 <- get

1372+ return (Constraint x1 x2 x3)

13661373 3 -> do x1 <- get

13671374 x2 <- get

13681375 x3 <- get

1369− return (TacImp x1 x2 x3)

1376+ x4 <- get

1377+ return (TacImp x1 x2 x3 x4)

13701378 _ -> error "Corrupted binary data for Plicity"

13711379

13721380

src/Idris/Parser/Expr.hs+9−9

@@ -261,8 +261,8 @@ updateSynMatch = update

261261 updTactic ns (TDocStr (Left n)) = TDocStr . Left . fst $ updateB ns (n, NoFC)

262262 updTactic ns t = fmap (update ns) t

263263

264− updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

265− updTacImp _ x = x

264+ updTacImp ns (TacImp o st scr r) = TacImp o st (update ns scr) r

265+ updTacImp _ x = x

266266

267267 dropn :: Name -> [(Name, a)] -> [(Name, a)]

268268 dropn n [] = []

@@ -1072,7 +1072,7 @@ Pi' ::=

10721072

10731073bindsymbol opts st syn

10741074 = do symbol "->"

1075− return (Exp opts st False)

1075+ return (Exp opts st False RigW)

10761076

10771077explicitPi opts st syn

10781078 = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

@@ -1089,7 +1089,7 @@ autoImplicit opts st syn

10891089 sc <- expr (allowConstr syn)

10901090 highlightP kw AnnKeyword

10911091 return (bindList (PPi

1092− (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)

1092+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]) RigW)) xt sc)

10931093

10941094defaultImplicit opts st syn = do

10951095 kw <- reservedFC "default"

@@ -1102,7 +1102,7 @@ defaultImplicit opts st syn = do

11021102 symbol "->"

11031103 sc <- expr (allowConstr syn)

11041104 highlightP kw AnnKeyword

1105− return (bindList (PPi (TacImp [] Dynamic script)) xt sc)

1105+ return (bindList (PPi (TacImp [] Dynamic script RigW)) xt sc)

11061106

11071107normalImplicit opts st syn = do

11081108 xt <- typeDeclList syn <* lchar '}'

@@ -1111,10 +1111,10 @@ normalImplicit opts st syn = do

11111111 sc <- expr syn

11121112 let (im,cl)

11131113 = if implicitAllowed syn

1114− then (Imp opts st False (Just (Impl False True False)) True,

1114+ then (Imp opts st False (Just (Impl False True False)) True RigW,

11151115 constraint)

1116− else (Imp opts st False (Just (Impl False False False)) True,

1117− Imp opts st False (Just (Impl True False False)) True)

1116+ else (Imp opts st False (Just (Impl False False False)) True RigW,

1117+ Imp opts st False (Just (Impl True False False)) True RigW)

11181118 return (bindList (PPi im) xt

11191119 (bindList (PPi cl) cs sc))

11201120

@@ -1123,7 +1123,7 @@ constraintPi opts st syn =

11231123 sc <- expr syn

11241124 if implicitAllowed syn

11251125 then return (bindList (PPi constraint) cs sc)

1126− else return (bindList (PPi (Imp opts st False (Just (Impl True False False)) True))

1126+ else return (bindList (PPi (Imp opts st False (Just (Impl True False False)) True RigW))

11271127 cs sc)

11281128

11291129implicitPi opts st syn =