@@ -914,7 +914,7 @@ TypeExpr ::= ConstraintList? Expr;
914914typeExpr :: SyntaxInfo -> IdrisParser PTerm
915915typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
916916 sc <- expr (allowConstr syn)
917− return (bindList (PPi constraint) cs sc)
917+ return (bindList (\r -> PPi (constraint { pcount = r })) cs sc)
918918 <?> "type signature"
919919
920920{- | Parses a lambda expression
@@ -941,7 +941,7 @@ lambda syn = do lchar '\\' <?> "lambda expression"
941941 ((do xt <- try $ tyOptDeclList (disallowImp syn)
942942 fc <- getFC
943943 sc <- lambdaTail
944− return (bindList (PLam fc) xt sc))
944+ return (bindList (\r -> PLam fc) xt sc))
945945 <|>
946946 (do ps <- sepBy (do fc <- getFC
947947 e <- simpleExpr (disallowImp (syn { inPattern = True }))
@@ -1078,7 +1078,7 @@ explicitPi opts st syn
10781078 = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')
10791079 binder <- bindsymbol opts st syn
10801080 sc <- expr (allowConstr syn)
1081− return (bindList (PPi binder) xt sc)
1081+ return (bindList (\r -> PPi (binder { pcount = r })) xt sc)
10821082
10831083autoImplicit opts st syn
10841084 = do kw <- reservedFC "auto"
@@ -1088,8 +1088,8 @@ autoImplicit opts st syn
10881088 symbol "->"
10891089 sc <- expr (allowConstr syn)
10901090 highlightP kw AnnKeyword
1091− return (bindList (PPi
1092− (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]) RigW)) xt sc)
1091+ return (bindList (\r -> PPi
1092+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]) r)) 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 RigW)) xt sc)
1105+ return (bindList (\r -> PPi (TacImp [] Dynamic script r)) xt sc)
11061106
11071107normalImplicit opts st syn = do
11081108 xt <- typeDeclList syn <* lchar '}'
@@ -1115,15 +1115,15 @@ normalImplicit opts st syn = do
11151115 constraint)
11161116 else (Imp opts st False (Just (Impl False False False)) True RigW,
11171117 Imp opts st False (Just (Impl True False False)) True RigW)
1118− return (bindList (PPi im) xt
1119− (bindList (PPi cl) cs sc))
1118+ return (bindList (\r -> PPi (im { pcount = r })) xt
1119+ (bindList (\r -> PPi (cl { pcount = r })) cs sc))
11201120
11211121constraintPi opts st syn =
11221122 do cs <- constraintList1 syn
11231123 sc <- expr syn
11241124 if implicitAllowed syn
1125− then return (bindList (PPi constraint) cs sc)
1126− else return (bindList (PPi (Imp opts st False (Just (Impl True False False)) True RigW))
1125+ then return (bindList (\r -> PPi constraint { pcount = r }) cs sc)
1126+ else return (bindList (\r -> PPi (Imp opts st False (Just (Impl True False False)) True r))
11271127 cs sc)
11281128
11291129implicitPi opts st syn =
@@ -1181,11 +1181,11 @@ ConstraintList ::=
11811181 ;
11821182@
11831183-}
1184−constraintList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1184+constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
11851185constraintList syn = try (constraintList1 syn)
11861186 <|> return []
11871187
1188−constraintList1 :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1188+constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
11891189constraintList1 syn = try (do lchar '('
11901190 tys <- sepBy1 nexpr (lchar ',')
11911191 lchar ')'
@@ -1193,13 +1193,13 @@ constraintList1 syn = try (do lchar '('
11931193 return tys)
11941194 <|> try (do t <- opExpr (disallowImp syn)
11951195 reservedOp "=>"
1196− return [(defname, NoFC, t)])
1196+ return [(RigW, defname, NoFC, t)])
11971197 <?> "type constraint list"
11981198 where nexpr = try (do (n, fc) <- name; lchar ':'
11991199 e <- expr (disallowImp syn)
1200− return (n, fc, e))
1200+ return (RigW, n, fc, e))
12011201 <|> do e <- expr (disallowImp syn)
1202− return (defname, NoFC, e)
1202+ return (RigW, defname, NoFC, e)
12031203 defname = sMN 0 "constraint"
12041204
12051205{- | Parses a type declaration list
@@ -1217,16 +1217,18 @@ FunctionSignatureList ::=
12171217 ;
12181218@
12191219-}
1220−typeDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1221−typeDeclList syn = try (sepBy1 (do (x, xfc) <- fnName
1220+typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
1221+typeDeclList syn = try (sepBy1 (do rig <- option RigW (do lchar '1'
1222+ return Rig1)
1223+ (x, xfc) <- fnName
12221224 lchar ':'
12231225 t <- typeExpr (disallowImp syn)
1224− return (x, xfc, t))
1226+ return (rig, x, xfc, t))
12251227 (lchar ','))
12261228 <|> do ns <- sepBy1 name (lchar ',')
12271229 lchar ':'
12281230 t <- typeExpr (disallowImp syn)
1229− return (map (\(x, xfc) -> (x, xfc, t)) ns)
1231+ return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)
12301232 <?> "type declaration list"
12311233
12321234{- | Parses a type declaration list with optional parameters
@@ -1241,11 +1243,11 @@ TypeOptDeclList ::=
12411243NameOrPlaceHolder ::= Name | '_';
12421244@
12431245-}
1244−tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1246+tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
12451247tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder
12461248 t <- option Placeholder (do lchar ':'
12471249 expr syn)
1248− return (x, fc, t))
1250+ return (RigW, x, fc, t))
12491251 (lchar ',')
12501252 <?> "type declaration list"
12511253 where nameOrPlaceholder :: IdrisParser (Name, FC)