git.iko.soy/Idris-dev
on master help sign in
Add RigCount to PPi/Plicity
488c5b7Edwin Brady
src/Idris/AbsSyntax.hs+15−15
compare with master
unifiedsplit
@@ -1306,8 +1306,8 @@ expandParams dec ps ns infs tm = en 0 tm
1306
1306
1307 nseq x y = nsroot x == nsroot y
1307 nseq x y = nsroot x == nsroot y
1308
1308
1309− enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1309+ enTacImp ql (TacImp aos st scr rig) = TacImp aos st (en ql scr) rig
1310− enTacImp ql other = other
1310+ enTacImp ql other = other
1311
1311
1312expandParamsD :: Bool -> -- True = RHS only
1312expandParamsD :: Bool -> -- True = RHS only
1313 IState ->
1313 IState ->
@@ -1511,8 +1511,8 @@ addStatics n tm ptm =
1511 -- if a name appears in an interface or tactic implicit index, it doesn't
1511 -- if a name appears in an interface or tactic implicit index, it doesn't
1512 -- affect its 'uniquely inferrable' from a static status since these are
1512 -- affect its 'uniquely inferrable' from a static status since these are
1513 -- resolved by searching.
1513 -- resolved by searching.
1514− searchArg (Constraint _ _) = True
1514+ searchArg (Constraint _ _ _) = True
1515− searchArg (TacImp _ _ _) = True
1515+ searchArg (TacImp _ _ _ _) = True
1516 searchArg _ = False
1516 searchArg _ = False
1517
1517
1518 staticList sts (Bind n (Pi _ _ _ _) sc) = (n `elem` sts) : staticList sts sc
1518 staticList sts (Bind n (Pi _ _ _ _) sc) = (n `elem` sts) : staticList sts sc
@@ -1547,14 +1547,14 @@ addUsingConstraints syn fc t
1547 -- if all of args in ns, then add it
1547 -- if all of args in ns, then add it
1548 doAdd (UConstraint c args : cs) ns t
1548 doAdd (UConstraint c args : cs) ns t
1549 | all (\n -> elem n ns) args
1549 | all (\n -> elem n ns) args
1550− = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
1550+ = PPi (Constraint [] Dynamic RigW) (sMN 0 "cu") NoFC
1551 (mkConst c args) (doAdd cs ns t)
1551 (mkConst c args) (doAdd cs ns t)
1552 | otherwise = doAdd cs ns t
1552 | otherwise = doAdd cs ns t
1553
1553
1554 mkConst c args = PApp fc (PRef fc [] c)
1554 mkConst c args = PApp fc (PRef fc [] c)
1555 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1555 (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)
1556
1556
1557− getConstraints (PPi (Constraint _ _) _ _ c sc)
1557+ getConstraints (PPi (Constraint _ _ _) _ _ c sc)
1558 = getcapp c ++ getConstraints sc
1558 = getcapp c ++ getConstraints sc
1559 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1559 getConstraints (PPi _ _ _ c sc) = getConstraints sc
1560 getConstraints _ = []
1560 getConstraints _ = []
@@ -1628,17 +1628,17 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)
1628 getImps (Bind n (Pi _ _ t _) sc) imps
1628 getImps (Bind n (Pi _ _ t _) sc) imps
1629 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1629 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1630 where
1630 where
1631− argInfo n (Imp opt _ _ _ _) Placeholder
1631+ argInfo n (Imp opt _ _ _ _ _) Placeholder
1632 = (True, PImp 0 True opt n Placeholder)
1632 = (True, PImp 0 True opt n Placeholder)
1633− argInfo n (Imp opt _ _ _ _) t'
1633+ argInfo n (Imp opt _ _ _ _ _) t'
1634 = (False, PImp (getPriority i t') True opt n t')
1634 = (False, PImp (getPriority i t') True opt n t')
1635− argInfo n (Exp opt _ _) t'
1635+ argInfo n (Exp opt _ _ _) t'
1636 = (InaccessibleArg `elem` opt,
1636 = (InaccessibleArg `elem` opt,
1637 PExp (getPriority i t') opt n t')
1637 PExp (getPriority i t') opt n t')
1638− argInfo n (Constraint opt _) t'
1638+ argInfo n (Constraint opt _ _) t'
1639 = (InaccessibleArg `elem` opt,
1639 = (InaccessibleArg `elem` opt,
1640 PConstraint 10 opt n t')
1640 PConstraint 10 opt n t')
1641− argInfo n (TacImp opt _ scr) t'
1641+ argInfo n (TacImp opt _ scr _) t'
1642 = (InaccessibleArg `elem` opt,
1642 = (InaccessibleArg `elem` opt,
1643 PTacImplicit 10 opt n scr t')
1643 PTacImplicit 10 opt n scr t')
1644 getImps (Bind n (Pi _ _ t _) sc) imps = impBind n t : getImps sc imps
1644 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) $
1724 = do (decls, ns) <- get
1724 = do (decls, ns) <- get
1725 let isn = nub (implNamesIn uvars ty)
1725 let isn = nub (implNamesIn uvars ty)
1726 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1726 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)
1728 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1728 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1729 (decls , ns) <- get
1729 (decls , ns) <- get
1730 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1730 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1731 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1731 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1732 imps True (n:env) sc
1732 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)
1734 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1734 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1735 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1735 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1736 _ -> [])
1736 _ -> [])
@@ -1738,7 +1738,7 @@ implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1738 put (PExp (getPriority ist ty) l n Placeholder : decls,
1738 put (PExp (getPriority ist ty) l n Placeholder : decls,
1739 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1739 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1740 imps True (n:env) sc
1740 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)
1742 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1742 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1743 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1743 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1744 _ -> [])
1744 _ -> [])
@@ -1746,7 +1746,7 @@ implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1746 put (PConstraint 10 l n Placeholder : decls,
1746 put (PConstraint 10 l n Placeholder : decls,
1747 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1747 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1748 imps True (n:env) sc
1748 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)
1750 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1750 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1751 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1751 (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
1752 _ -> [])
1752 _ -> [])
src/Idris/AbsSyntaxTree.hs+24−20
@@ -599,17 +599,21 @@ data Plicity = Imp { pargopts :: [ArgOpt]
599 , pparam :: Bool
599 , pparam :: Bool
600 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
600 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
601 , pinsource :: Bool -- ^ Explicitly written in source
601 , pinsource :: Bool -- ^ Explicitly written in source
602+ , pcount :: RigCount
602 }
603 }
603 | Exp { pargopts :: [ArgOpt]
604 | Exp { pargopts :: [ArgOpt]
604 , pstatic :: Static
605 , pstatic :: Static
605 , pparam :: Bool -- ^ this is a param (rather than index)
606 , pparam :: Bool -- ^ this is a param (rather than index)
607+ , pcount :: RigCount
606 }
608 }
607 | Constraint { pargopts :: [ArgOpt]
609 | Constraint { pargopts :: [ArgOpt]
608− , pstatic :: Static
610+ , pstatic :: Static
611+ , pcount :: RigCount
609 }
612 }
610 | TacImp { pargopts :: [ArgOpt]
613 | TacImp { pargopts :: [ArgOpt]
611 , pstatic :: Static
614 , pstatic :: Static
612 , pscript :: PTerm
615 , pscript :: PTerm
616+ , pcount :: RigCount
613 }
617 }
614 deriving (Show, Eq, Ord, Data, Generic, Typeable)
618 deriving (Show, Eq, Ord, Data, Generic, Typeable)
615
619
@@ -618,24 +622,24 @@ deriving instance Binary Plicity
618!-}
622!-}
619
623
620is_scoped :: Plicity -> Maybe ImplicitInfo
624is_scoped :: Plicity -> Maybe ImplicitInfo
621−is_scoped (Imp _ _ _ s _) = s
625+is_scoped (Imp _ _ _ s _ _) = s
622−is_scoped _ = Nothing
626+is_scoped _ = Nothing
623
627
624-- Top level implicit
628-- 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
626-- Machine generated top level implicit
630-- 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
628
632
629-- Scoped implicits
633-- Scoped implicits
630−forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False
634+forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
631−forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False
635+forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
632
636
633−expl = Exp [] Dynamic False
637+expl = Exp [] Dynamic False RigW
634−expl_param = Exp [] Dynamic True
638+expl_param = Exp [] Dynamic True RigW
635
639
636−constraint = Constraint [] Static
640+constraint = Constraint [] Static RigW
637
641
638−tacimpl t = TacImp [] Dynamic t
642+tacimpl t = TacImp [] Dynamic t RigW
639
643
640data FnOpt = Inlinable -- ^ always evaluate when simplifying
644data FnOpt = Inlinable -- ^ always evaluate when simplifying
641 | TotalFn | PartialFn | CoveringFn
645 | TotalFn | PartialFn | CoveringFn
@@ -1815,7 +1819,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1815 depth d . bracket p startPrec . group . align $
1819 depth d . bracket p startPrec . group . align $
1816 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1820 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1817 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1821 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)
1819 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1823 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1820 || ppopt_pinames ppo && uname n =
1824 || ppopt_pinames ppo && uname n =
1821 depth d . bracket p startPrec . group $
1825 depth d . bracket p startPrec . group $
@@ -1835,7 +1839,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1835 case s of
1839 case s of
1836 Static -> text "%static" <> space
1840 Static -> text "%static" <> space
1837 _ -> empty
1841 _ -> 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)
1839 | ppopt_impl ppo =
1843 | ppopt_impl ppo =
1840 depth d . bracket p startPrec $
1844 depth d . bracket p startPrec $
1841 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1845 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
1846 case s of
1850 case s of
1847 Static -> text "%static" <> space
1851 Static -> text "%static" <> space
1848 _ -> empty
1852 _ -> empty
1849− prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1853+ prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1850 depth d . bracket p startPrec $
1854 depth d . bracket p startPrec $
1851 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1855 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) =
1853 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1857 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1854 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1858 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) =
1856 depth d . bracket p startPrec $
1860 depth d . bracket p startPrec $
1857 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1861 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1858 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1862 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
@@ -2380,7 +2384,7 @@ allNamesIn tm = nub $ ni 0 [] tm
2380 ni i env (PUnquote tm) = ni (i - 1) env tm
2384 ni i env (PUnquote tm) = ni (i - 1) env tm
2381 ni i env tm = concatMap (ni i env) (children tm)
2385 ni i env tm = concatMap (ni i env) (children tm)
2382
2386
2383− niTacImp i env (TacImp _ _ scr) = ni i env scr
2387+ niTacImp i env (TacImp _ _ scr _) = ni i env scr
2384 niTacImp _ _ _ = []
2388 niTacImp _ _ _ = []
2385
2389
2386
2390
@@ -2416,7 +2420,7 @@ boundNamesIn tm = S.toList (ni 0 S.empty tm)
2416 niTms i set [] = set
2420 niTms i set [] = set
2417 niTms i set (x : xs) = niTms i (ni i set x) xs
2421 niTms i set (x : xs) = niTms i (ni i set x) xs
2418
2422
2419− niTacImp i set (TacImp _ _ scr) = ni i set scr
2423+ niTacImp i set (TacImp _ _ scr _) = ni i set scr
2420 niTacImp i set _ = set
2424 niTacImp i set _ = set
2421
2425
2422-- Return names which are valid implicits in the given term (type).
2426-- Return names which are valid implicits in the given term (type).
@@ -2527,7 +2531,7 @@ namesIn uvars ist tm = nub $ ni 0 [] tm
2527
2531
2528 ni i env tm = concatMap (ni i env) (children tm)
2532 ni i env tm = concatMap (ni i env) (children tm)
2529
2533
2530− niTacImp i env (TacImp _ _ scr) = ni i env scr
2534+ niTacImp i env (TacImp _ _ scr _) = ni i env scr
2531 niTacImp _ _ _ = []
2535 niTacImp _ _ _ = []
2532
2536
2533-- Return which of the given names are used in the given term.
2537-- Return which of the given names are used in the given term.
@@ -2562,7 +2566,7 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm
2562
2566
2563 ni i env tm = concatMap (ni i env) (children tm)
2567 ni i env tm = concatMap (ni i env) (children tm)
2564
2568
2565− niTacImp i env (TacImp _ _ scr) = ni i env scr
2569+ niTacImp i env (TacImp _ _ scr _) = ni i env scr
2566 niTacImp _ _ _ = []
2570 niTacImp _ _ _ = []
2567
2571
2568-- Return the list of inaccessible (= dotted) positions for a name.
2572-- 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
408 return (showLHSName un ++ " " ++ ap ++ "= ?"
408 return (showLHSName un ++ " " ++ ap ++ "= ?"
409 ++ showRHSName un ++ "_rhs")
409 ++ showRHSName un ++ "_rhs")
410 where mkApp :: IState -> PTerm -> [Name] -> String
410 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
412 = let n = getNameFrom i used ty in
412 = let n = getNameFrom i used ty in
413 show n ++ " " ++ mkApp i sc (n : used)
413 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
415 | thead n == '_'
415 | thead n == '_'
416 = let n = getNameFrom i used ty in
416 = let n = getNameFrom i used ty in
417 show n ++ " " ++ mkApp i sc (n : used)
417 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
419 = show n ++ " " ++ mkApp i sc (n : used)
419 = show n ++ " " ++ mkApp i sc (n : used)
420 mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used
420 mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used
421 mkApp i _ _ = ""
421 mkApp i _ _ = ""
src/Idris/Delaborate.hs+7−7
@@ -139,25 +139,25 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm
139 = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)
139 = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)
140 de env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)
140 de env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)
141 | toplevel_imp impl -- information in 'imps' repeated
141 | 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)
143 de env is (Bind n (Pi rig (Just impl) ty _) sc)
143 de env is (Bind n (Pi rig (Just impl) ty _) sc)
144 | tcimplementation impl
144 | tcimplementation impl
145 = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)
145 = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)
146 | otherwise
146 | 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)
148 de env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)
148 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)
150 de env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)
150 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)
152 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)
152 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)
154 de env (plic:is) (Bind n (Pi rig _ ty _) sc)
154 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)
156 n NoFC
156 n NoFC
157 (de env [] ty)
157 (de env [] ty)
158 (de ((n,n):env) is sc)
158 (de ((n,n):env) is sc)
159 de env [] (Bind n (Pi rig _ ty _) sc)
159 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)
161
161
162 de env imps (Bind n (Let ty val) sc)
162 de env imps (Bind n (Let ty val) sc)
163 | docases
163 | docases
src/Idris/Docs.hs+3−3
@@ -220,7 +220,7 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_
220 dumpImplementation :: PTerm -> Doc OutputAnnotation
220 dumpImplementation :: PTerm -> Doc OutputAnnotation
221 dumpImplementation = pprintPTerm ppo params' [] infixes
221 dumpImplementation = pprintPTerm ppo params' [] infixes
222
222
223− prettifySubInterfaces (PPi (Constraint _ _) _ _ tm _) = prettifySubInterfaces tm
223+ prettifySubInterfaces (PPi (Constraint _ _ _) _ _ tm _) = prettifySubInterfaces tm
224 prettifySubInterfaces (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubInterfaces t1) (prettifySubInterfaces t2)
224 prettifySubInterfaces (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubInterfaces t1) (prettifySubInterfaces t2)
225 prettifySubInterfaces (PApp fc ref args) = PApp fc ref $ updateArgs pNames args
225 prettifySubInterfaces (PApp fc ref args) = PApp fc ref $ updateArgs pNames args
226 prettifySubInterfaces tm = tm
226 prettifySubInterfaces tm = tm
@@ -235,7 +235,7 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_
235 updateRef nm (PRef fc _ _) = PRef fc [] nm
235 updateRef nm (PRef fc _ _) = PRef fc [] nm
236 updateRef _ pt = pt
236 updateRef _ pt = pt
237
237
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'
239 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt
239 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt
240 isSubInterface _ = False
240 isSubInterface _ = False
241
241
@@ -356,7 +356,7 @@ docInterface n ci
356 getDImpl (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t
356 getDImpl (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t
357 getDImpl _ = Nothing
357 getDImpl _ = Nothing
358
358
359− isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))
359+ isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))
360 = nm == n && map getTm args == map getTm args'
360 = nm == n && map getTm args == map getTm args'
361 isSubInterface (PPi _ _ _ _ pt)
361 isSubInterface (PPi _ _ _ _ pt)
362 = isSubInterface pt
362 = 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
310 where
310 where
311 needed is p = pname p `elem` map pname is
311 needed is p = pname p `elem` map pname is
312
312
313− lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'
313+ lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'
314 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
314 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
315 lamBind i (PPi _ n _ ty sc) sc'
315 lamBind i (PPi _ n _ ty sc) sc'
316 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
316 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
317 lamBind i _ sc = sc
317 lamBind i _ sc = sc
318− methArgs i (PPi (Imp _ _ _ _ _) n _ ty sc)
318+ methArgs i (PPi (Imp _ _ _ _ _ _) n _ ty sc)
319 = PImp 0 True [] n (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
319 = 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)
321 = PExp 0 [] (sMN 0 "marg") (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
321 = 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)
323 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
323 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
324 methArgs i _ = []
324 methArgs i _ = []
325
325
@@ -354,7 +354,7 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
354 extrabind [] x = x
354 extrabind [] x = x
355
355
356 coninsert :: [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm
356 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)
358 coninsert cs ex sc = conbind cs (extrabind ex sc)
358 coninsert cs ex sc = conbind cs (extrabind ex sc)
359
359
360 -- Reorder declarations to be in the same order as defined in the
360 -- 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
210 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
210 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
211 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
211 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
212 (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
212 (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'))),
214 (n, (nfc, syn, o, t) ) )
214 (n, (nfc, syn, o, t) ) )
215 tdecl impps allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))
215 tdecl impps allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))
216 = do let o = []
216 = do let o = []
@@ -218,7 +218,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
218 logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'
218 logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'
219 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
219 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
220 (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
220 (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'))),
222 (n, (nfc, syn, o, t) ) )
222 (n, (nfc, syn, o, t) ) )
223 tdecl impps allmeths (PData doc _ syn _ _ _)
223 tdecl impps allmeths (PData doc _ syn _ _ _)
224 = ierror $ At fc (Msg "Data definitions not allowed in an interface declaration")
224 = 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
294 return [PTy doc [] syn fc o m mfc ty',
294 return [PTy doc [] syn fc o m mfc ty',
295 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
295 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
296
296
297− getMArgs (PPi (Imp _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc
297+ getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc
298− getMArgs (PPi (Exp _ _ _) n _ ty sc) = EA n : getMArgs sc
298+ getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc
299− getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc
299+ getMArgs (PPi (Constraint _ _ _) n _ ty sc) = CA : getMArgs sc
300 getMArgs _ = []
300 getMArgs _ = []
301
301
302 getMeth :: [Name] -> [Name] -> Name -> PTerm
302 getMeth :: [Name] -> [Name] -> Name -> PTerm
@@ -337,9 +337,9 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
337 addC _ _ tm = tm
337 addC _ _ tm = tm
338
338
339 -- make arguments explicit and don't bind interface parameters
339 -- 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)
341 | n `elem` ns = toExp ns e sc
341 | 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)
343 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
343 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
344 toExp ns e sc = sc
344 toExp ns e sc = sc
345
345
src/Idris/Elab/Record.hs+4−4
@@ -460,10 +460,10 @@ in_name n = n
460
460
461-- | Creates a PArg with a given plicity, name, and term.
461-- | Creates a PArg with a given plicity, name, and term.
462asArg :: Plicity -> Name -> PTerm -> PArg
462asArg :: Plicity -> Name -> PTerm -> PArg
463−asArg (Imp os _ _ _ _) n t = PImp 0 False os n t
463+asArg (Imp os _ _ _ _ _) n t = PImp 0 False os n t
464−asArg (Exp os _ _) n t = PExp 0 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
465+asArg (Constraint os _ _) n t = PConstraint 0 os n t
466−asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t
466+asArg (TacImp os _ s _) n t = PTacImplicit 0 os n s t
467
467
468-- | Machine name "rec".
468-- | Machine name "rec".
469recName :: Name
469recName :: Name
src/Idris/Elab/Term.hs+1−1
@@ -1587,7 +1587,7 @@ elab ist info emode opts fn tm
1587 fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
1587 fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
1588
1588
1589 addAutoBind :: Plicity -> Name -> ElabD ()
1589 addAutoBind :: Plicity -> Name -> ElabD ()
1590− addAutoBind (Imp _ _ _ _ False) n
1590+ addAutoBind (Imp _ _ _ _ False _) n
1591 = updateAux (\est -> est { auto_binds = n : auto_binds est })
1591 = updateAux (\est -> est { auto_binds = n : auto_binds est })
1592 addAutoBind _ _ = return ()
1592 addAutoBind _ _ = return ()
1593
1593
src/Idris/IBC.hs+17−9
@@ -47,7 +47,7 @@ import System.Directory
47import System.FilePath
47import System.FilePath
48
48
49ibcVersion :: Word16
49ibcVersion :: Word16
50−ibcVersion = 156
50+ibcVersion = 157
51
51
52-- | When IBC is being loaded - we'll load different things (and omit
52-- | When IBC is being loaded - we'll load different things (and omit
53-- different structures/definitions) depending on which phase we're in.
53-- different structures/definitions) depending on which phase we're in.
@@ -1328,26 +1328,30 @@ instance Binary Static where
1328instance Binary Plicity where
1328instance Binary Plicity where
1329 put x
1329 put x
1330 = case x of
1330 = case x of
1331− Imp x1 x2 x3 x4 _ ->
1331+ Imp x1 x2 x3 x4 _ x5 ->
1332 do putWord8 0
1332 do putWord8 0
1333 put x1
1333 put x1
1334 put x2
1334 put x2
1335 put x3
1335 put x3
1336 put x4
1336 put x4
1337+ put x5
1337− Exp x1 x2 x3 ->
1338+ Exp x1 x2 x3 x4 ->
1338 do putWord8 1
1339 do putWord8 1
1339 put x1
1340 put x1
1340 put x2
1341 put x2
1341 put x3
1342 put x3
1343+ put x4
1342− Constraint x1 x2 ->
1344+ Constraint x1 x2 x3 ->
1343 do putWord8 2
1345 do putWord8 2
1344 put x1
1346 put x1
1345 put x2
1347 put x2
1348+ put x3
1346− TacImp x1 x2 x3 ->
1349+ TacImp x1 x2 x3 x4 ->
1347 do putWord8 3
1350 do putWord8 3
1348 put x1
1351 put x1
1349 put x2
1352 put x2
1350 put x3
1353 put x3
1354+ put x4
1351 get
1355 get
1352 = do i <- getWord8
1356 = do i <- getWord8
1353 case i of
1357 case i of
@@ -1355,18 +1359,22 @@ instance Binary Plicity where
1355 x2 <- get
1359 x2 <- get
1356 x3 <- get
1360 x3 <- get
1357 x4 <- get
1361 x4 <- get
1362+ x5 <- get
1358− return (Imp x1 x2 x3 x4 False)
1363+ return (Imp x1 x2 x3 x4 False x5)
1359 1 -> do x1 <- get
1364 1 -> do x1 <- get
1360 x2 <- get
1365 x2 <- get
1361 x3 <- get
1366 x3 <- get
1367+ x4 <- get
1362− return (Exp x1 x2 x3)
1368+ return (Exp x1 x2 x3 x4)
1363 2 -> do x1 <- get
1369 2 -> do x1 <- get
1364 x2 <- get
1370 x2 <- get
1371+ x3 <- get
1365− return (Constraint x1 x2)
1372+ return (Constraint x1 x2 x3)
1366 3 -> do x1 <- get
1373 3 -> do x1 <- get
1367 x2 <- get
1374 x2 <- get
1368 x3 <- get
1375 x3 <- get
1376+ x4 <- get
1369− return (TacImp x1 x2 x3)
1377+ return (TacImp x1 x2 x3 x4)
1370 _ -> error "Corrupted binary data for Plicity"
1378 _ -> error "Corrupted binary data for Plicity"
1371
1379
1372
1380
src/Idris/Parser/Expr.hs+9−9
@@ -261,8 +261,8 @@ updateSynMatch = update
261 updTactic ns (TDocStr (Left n)) = TDocStr . Left . fst $ updateB ns (n, NoFC)
261 updTactic ns (TDocStr (Left n)) = TDocStr . Left . fst $ updateB ns (n, NoFC)
262 updTactic ns t = fmap (update ns) t
262 updTactic ns t = fmap (update ns) t
263
263
264− updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)
264+ updTacImp ns (TacImp o st scr r) = TacImp o st (update ns scr) r
265− updTacImp _ x = x
265+ updTacImp _ x = x
266
266
267 dropn :: Name -> [(Name, a)] -> [(Name, a)]
267 dropn :: Name -> [(Name, a)] -> [(Name, a)]
268 dropn n [] = []
268 dropn n [] = []
@@ -1072,7 +1072,7 @@ Pi' ::=
1072
1072
1073bindsymbol opts st syn
1073bindsymbol opts st syn
1074 = do symbol "->"
1074 = do symbol "->"
1075− return (Exp opts st False)
1075+ return (Exp opts st False RigW)
1076
1076
1077explicitPi opts st syn
1077explicitPi opts st syn
1078 = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')
1078 = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')
@@ -1089,7 +1089,7 @@ autoImplicit opts st syn
1089 sc <- expr (allowConstr syn)
1089 sc <- expr (allowConstr syn)
1090 highlightP kw AnnKeyword
1090 highlightP kw AnnKeyword
1091 return (bindList (PPi
1091 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)
1093
1093
1094defaultImplicit opts st syn = do
1094defaultImplicit opts st syn = do
1095 kw <- reservedFC "default"
1095 kw <- reservedFC "default"
@@ -1102,7 +1102,7 @@ defaultImplicit opts st syn = do
1102 symbol "->"
1102 symbol "->"
1103 sc <- expr (allowConstr syn)
1103 sc <- expr (allowConstr syn)
1104 highlightP kw AnnKeyword
1104 highlightP kw AnnKeyword
1105− return (bindList (PPi (TacImp [] Dynamic script)) xt sc)
1105+ return (bindList (PPi (TacImp [] Dynamic script RigW)) xt sc)
1106
1106
1107normalImplicit opts st syn = do
1107normalImplicit opts st syn = do
1108 xt <- typeDeclList syn <* lchar '}'
1108 xt <- typeDeclList syn <* lchar '}'
@@ -1111,10 +1111,10 @@ normalImplicit opts st syn = do
1111 sc <- expr syn
1111 sc <- expr syn
1112 let (im,cl)
1112 let (im,cl)
1113 = if implicitAllowed syn
1113 = 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,
1115 constraint)
1115 constraint)
1116− else (Imp opts st False (Just (Impl False 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)
1117+ Imp opts st False (Just (Impl True False False)) True RigW)
1118 return (bindList (PPi im) xt
1118 return (bindList (PPi im) xt
1119 (bindList (PPi cl) cs sc))
1119 (bindList (PPi cl) cs sc))
1120
1120
@@ -1123,7 +1123,7 @@ constraintPi opts st syn =
1123 sc <- expr syn
1123 sc <- expr syn
1124 if implicitAllowed syn
1124 if implicitAllowed syn
1125 then return (bindList (PPi constraint) cs sc)
1125 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))
1127 cs sc)
1127 cs sc)
1128
1128
1129implicitPi opts st syn =
1129implicitPi opts st syn =