a2e981e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #4239 from eraserhd/lhs-extents

a2e981eJason Felice9 years ago

src/Idris/AbsSyntaxTree.hs−11

compare with master

unifiedsplit

@@ -927,17 +927,6 @@ updateNs ns t = mapPT updateRef t

927 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)

928 updateRef t = t

929

930−-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl

931−-- updateDNs [] t = t

932−-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t

933−-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)

934−-- where updateCNs ns (PClause n l ts r ds)

935−-- = PClause (updateN ns n) (fmap (updateNs ns) l)

936−-- (map (fmap (updateNs ns)) ts)

937−-- (fmap (updateNs ns) r)

938−-- (map (updateDNs ns) ds)

939−-- updateDNs ns c = c

940−

941data PunInfo = IsType

930data PunInfo = IsType

942 | IsTerm

931 | IsTerm

943 | TypeOrTerm

932 | TypeOrTerm

src/Idris/Elab/Clause.hs+7−4

@@ -662,8 +662,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

662

663 -- Check if we have "with" patterns outside of "with" block

664 when (isOutsideWith lhs_in && (not $ null withs)) $

665+ ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)

665− ierror (At fc (Elaborating "left hand side of " fname Nothing

666+ (Elaborating "left hand side of " fname Nothing

666− (Msg "unexpected patterns outside of \"with\" block")))

667+ (Msg "unexpected patterns outside of \"with\" block")))

667

668

668 -- get the parameters first, to pass through to any where block

669 -- get the parameters first, to pass through to any where block

669 let fn_ty = case lookupTy fname ctxt of

670 let fn_ty = case lookupTy fname ctxt of

@@ -689,7 +690,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

689 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-

690 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-

690 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

691 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

691 (do res <- errAt "left hand side of " fname Nothing

692 (do res <- errAt "left hand side of " fname Nothing

693+ (erun (fromMaybe NoFC $ highestFC lhs_in_as)

692− (erun fc (buildTC i info ELHS opts fname

694+ (buildTC i info ELHS opts fname

693 (allNamesIn lhs_in)

695 (allNamesIn lhs_in)

694 (infTerm lhs)))

696 (infTerm lhs)))

695 probs <- get_probs

697 probs <- get_probs

@@ -950,7 +952,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

950 (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-

952 (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-

951 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

953 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

952 (errAt "left hand side of with in " fname Nothing

954 (errAt "left hand side of with in " fname Nothing

955+ (erun (fromMaybe NoFC $ highestFC lhs_in)

953− (erun fc (buildTC i info ELHS opts fname

956+ (buildTC i info ELHS opts fname

954 (allNamesIn lhs_in)

957 (allNamesIn lhs_in)

955 (infTerm lhs))) )

958 (infTerm lhs))) )

956 setContext ctxt'

959 setContext ctxt'

src/Idris/Parser.hs+29−44

@@ -1103,6 +1103,7 @@ WhereOrTerminator ::= WhereBlock | Terminator;

1103-}

1104clause :: SyntaxInfo -> IdrisParser PClause

1105clause syn

1106+ -- unnamed with or function clause (inside a with)

1106 = appExtent (do

1107 = appExtent (do

1107 wargs <- P.try (do pushIndent; some (wExpr syn))

1108 wargs <- P.try (do pushIndent; some (wExpr syn))

1108 ist <- get

1109 ist <- get

@@ -1123,6 +1124,7 @@ clause syn

1123 let withs = concat ds

1124 let withs = concat ds

1124 closeBlock

1125 closeBlock

1125 return $ \fc -> PWithR fc wargs wval pn withs))

1126 return $ \fc -> PWithR fc wargs wval pn withs))

1127+ -- <==

1126 <|> do ty <- P.try (do pushIndent

1128 <|> do ty <- P.try (do pushIndent

1127 ty <- simpleExpr syn

1129 ty <- simpleExpr syn

1128 symbol "<=="

1130 symbol "<=="

@@ -1139,23 +1141,14 @@ clause syn

1139 ist <- get

1141 ist <- get

1140 put (ist { lastParse = Just n })

1142 put (ist { lastParse = Just n })

1141 return $ PClause fc n capp [] r wheres

1143 return $ PClause fc n capp [] r wheres

1142− <|> do (l, op, nfc) <- P.try (do

1144+ -- lhs application "with" clause or function clause

1143− pushIndent

1145+ <|> do pushIndent

1144− l <- argExpr syn

1146+ (n, nfc, capp, wargs) <- lhs

1145− (op, nfc) <- withExtent symbolicOperator

1147+ modify $ \ist -> ist { lastParse = Just n }

1146− when (op == "=" || op == "?=" ) $

1147− fail "infix clause definition with \"=\" and \"?=\" not supported "

1148− return (l, op, nfc))

1149− let n = expandNS syn (sUN op)

1150− r <- argExpr syn

1151− wargs <- many (wExpr syn)

1152 (do (rs, fc) <- withExtent (rhs syn n)

1148 (do (rs, fc) <- withExtent (rhs syn n)

1153 let wsyn = syn { syn_namespace = [] }

1149 let wsyn = syn { syn_namespace = [] }

1154 (wheres, nmap) <- whereBlock n wsyn <* popIndent

1150 (wheres, nmap) <- whereBlock n wsyn <* popIndent

1155 <|> ([], []) <$ terminator

1151 <|> ([], []) <$ terminator

1156− ist <- get

1157− let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]

1158− put (ist { lastParse = Just n })

1159 return $ PClause fc n capp wargs rs wheres) <|> (do

1152 return $ PClause fc n capp wargs rs wheres) <|> (do

1160 popIndent

1153 popIndent

1161 ((wval, pn), fc) <- withExtent $ do

1154 ((wval, pn), fc) <- withExtent $ do

@@ -1166,41 +1159,33 @@ clause syn

1166 openBlock

1159 openBlock

1167 ds <- some $ fnDecl syn

1160 ds <- some $ fnDecl syn

1168 closeBlock

1161 closeBlock

1169− ist <- get

1170− let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]

1171− let withs = map (fillLHSD n capp wargs) $ concat ds

1172− put (ist { lastParse = Just n })

1173− return $ PWith fc n capp wargs wval pn withs)

1174− <|> do pushIndent

1175− (n_in, nfc) <- withExtent fnName; let n = expandNS syn n_in

1176− args <- many (P.try (implicitArg (syn { inPattern = True } ))

1177− <|> P.try (constraintArg (syn { inPattern = True }))

1178− <|> (fmap pexp (argExpr syn)))

1179− wargs <- many (wExpr syn)

1180− (do (r, fc) <- withExtent (rhs syn n)

1181− let capp = PApp fc (PRef nfc [nfc] n) args

1182− let wsyn = syn { syn_namespace = [] }

1183− (wheres, nmap) <- whereBlock n wsyn <* popIndent

1184− <|> ([], []) <$ terminator

1185− ist <- get

1186− put (ist { lastParse = Just n })

1187− return $ PClause fc n capp wargs r wheres) <|> (do

1188− keyword "with"

1189− ist <- get

1190− put (ist { lastParse = Just n })

1191− ((wval, pn), fc) <- withExtent $ do

1192− wval <- bracketed syn

1193− pn <- optProof

1194− return (wval, pn)

1195− openBlock

1196− ds <- some $ fnDecl syn

1197− closeBlock

1198− popIndent

1199− let capp = PApp fc (PRef nfc [nfc] n) args

1200 let withs = map (fillLHSD n capp wargs) $ concat ds

1162 let withs = map (fillLHSD n capp wargs) $ concat ds

1201 return $ PWith fc n capp wargs wval pn withs)

1163 return $ PWith fc n capp wargs wval pn withs)

1202 <?> "function clause"

1164 <?> "function clause"

1203 where

1165 where

1166+ lhsInfixApp :: IdrisParser (Name, FC, [PArg], [PTerm])

1167+ lhsInfixApp = do l <- argExpr syn

1168+ (op, nfc) <- withExtent symbolicOperator

1169+ when (op == "=" || op == "?=" ) $

1170+ fail "infix clause definition with \"=\" and \"?=\" not supported "

1171+ let n = expandNS syn (sUN op)

1172+ r <- argExpr syn

1173+ wargs <- many (wExpr syn)

1174+ return (n, nfc, [pexp l, pexp r], wargs)

1175+

1176+ lhsPrefixApp :: IdrisParser (Name, FC, [PArg], [PTerm])

1177+ lhsPrefixApp = do (n, nfc) <- withExtent (expandNS syn <$> fnName)

1178+ args <- many (P.try (implicitArg (syn { inPattern = True } ))

1179+ <|> P.try (constraintArg (syn { inPattern = True }))

1180+ <|> (fmap pexp (argExpr syn)))

1181+ wargs <- many (wExpr syn)

1182+ return (n, nfc, args, wargs)

1183+

1184+ lhs :: IdrisParser (Name, FC, PTerm, [PTerm])

1185+ lhs = do ((n, nfc, args, wargs), lhs_fc) <- withExtent (P.try lhsInfixApp <|> lhsPrefixApp)

1186+ let capp = PApp lhs_fc (PRef nfc [nfc] n) args

1187+ return (n, nfc, capp, wargs)

1188+

1204 optProof = P.option Nothing (do keyword "proof"

1189 optProof = P.option Nothing (do keyword "proof"

1205 n <- withExtent fnName

1190 n <- withExtent fnName

1206 return (Just n))

1191 return (Just n))

test/error006/expected+1−1

@@ -1,2 +1,2 @@

1−WithPatsNoWith.idr:4:15-20:When checking left hand side of foo:

1+WithPatsNoWith.idr:4:1-13:When checking left hand side of foo:

2unexpected patterns outside of "with" block

test/layout001/expected−1

@@ -14,7 +14,6 @@ Wrong indention: should be greater than context indentation

14 |

153 | 2

16 | ^

17−= is not a valid operator

18Wrong indention: should be greater than context indentation

17Wrong indention: should be greater than context indentation

20./layout001e.idr:6:1:

19./layout001e.idr:6:1:

test/regression002/expected+10−10

@@ -20,7 +20,7 @@ Specifically:

20 1

21 and

22 0

23−reg010.idr:5:28-31:

23+reg010.idr:5:3-26:

24When checking left hand side of with block in usubst.unsafeSubst:

25Can't match on with block in usubst.unsafeSubst warg a P x x px

26reg018a.idr:16:1-18:

@@ -46,9 +46,9 @@ reg028a.idr:17:14-18:

46This style of tactic proof is deprecated. See %runElab for the replacement.

47reg028a.idr:11:1-14:

48tbad.qsort' is possibly not total due to: with block in tbad.qsort'

49−reg034.idr:6:16-21:When checking left hand side of bar:

49+reg034.idr:6:1-14:When checking left hand side of bar:

50Can't match on bar xs xs Refl

51−reg034.idr:9:16-21:When checking left hand side of foo:

51+reg034.idr:9:1-14:When checking left hand side of foo:

52Can't match on foo f x x Refl

53reg035b.idr:8:12-38:No such variable __pi_arg

54reg044.idr:4:6-10:

@@ -84,12 +84,12 @@ No such variable Bogus

84 | ^

85unexpected Operator without known fixity: !!

87−reg054.idr:18:19-24:When checking left hand side of inf:

87+reg054.idr:18:1-17:When checking left hand side of inf:

88When checking an application of constructor Main.MkInfer:

89 Attempting concrete match on polymorphic argument: 0

90−reg054.idr:34:20-24:When checking left hand side of weird:

90+reg054.idr:34:1-18:When checking left hand side of weird:

91No explicit types on left hand side: Char

92−reg054.idr:37:32-34:When checking left hand side of weird':

92+reg054.idr:37:1-30:When checking left hand side of weird':

93No explicit types on left hand side: Nat

94reg054.idr:40:1-7:When checking left hand side of tctrick:

95When checking an application of Main.tctrick:

@@ -97,14 +97,14 @@ When checking an application of Main.tctrick:

97 Maybe a1 (Type of Just x)

98 and

99 a (Expected type)

100−reg055.idr:5:9-11:When checking left hand side of g:

100+reg055.idr:5:1-7:When checking left hand side of g:

101Can't match on g (f 0)

102−reg055.idr:8:7-9:When checking left hand side of h:

102+reg055.idr:8:1-5:When checking left hand side of h:

103Can't match on h x x

104−reg055a.idr:8:20-23:When checking left hand side of foo:

104+reg055a.idr:8:1-18:When checking left hand side of foo:

105When checking an application of constructor Foo.CAny:

106 Attempting concrete match on polymorphic argument: Nothing

107−reg055a.idr:13:25-27:When checking left hand side of Foo.apply:

107+reg055a.idr:13:1-23:When checking left hand side of Foo.apply:

108Can't match on apply (\x, y => x) a

109reg056.idr:7:16-25:dodgy n m Refl is a valid case

110reg056.idr:10:11-20:nonk Refl is a valid case