38123a4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Resugaring for do and fromInteger

38123a4David Raymond Christiansen11 years ago

CHANGELOG+3

compare with master

unifiedsplit

@@ -3,6 +3,9 @@ New in 0.9.19:

3* The Show class has been moved into Prelude.Show and augmented with the method

4 showPrec, which allows correct parenthesization of showed terms. This comes

5 with the type Prec of precedences and a few helper functions.

6+* Compiler output shows applications of >>= in do-notation

7+* fromInteger i where i is an integer constant is now shown just as i in

8+ compiler output

7New in 0.9.18:

10New in 0.9.18:

8--------------

11--------------

src/Idris/AbsSyntaxTree.hs+22−1

@@ -1633,7 +1633,28 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1633 prettySe p bnd (PReturn f) = kwd "return"

1634 prettySe p bnd PImpossible = kwd "impossible"

1635 prettySe p bnd Placeholder = text "_"

1636− prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

1636+ prettySe p bnd (PDoBlock dos) =

1637+ bracket p startPrec $

1638+ kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))

1639+ where ppdo bnd (DoExp _ tm:dos) = prettySe startPrec bnd tm : ppdo bnd dos

1640+ ppdo bnd (DoBind _ bn _ tm : dos) =

1641+ (prettyBindingOf bn False <+> text "<-" <+>

1642+ group (align (hang 2 (prettySe startPrec bnd tm)))) :

1643+ ppdo ((bn, False):bnd) dos

1644+ ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab

1645+ text "no pretty printer for pattern-matching do binding" :

1646+ ppdo bnd dos

1647+ ppdo bnd (DoLet _ ln _ ty v : dos) =

1648+ (kwd "let" <+> prettyBindingOf ln False <+>

1649+ (if ty /= Placeholder

1650+ then colon <+> prettySe startPrec bnd ty <+> text "="

1651+ else text "=") <+>

1652+ group (align (hang 2 (prettySe startPrec bnd v)))) :

1653+ ppdo ((ln, False):bnd) dos

1654+ ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab

1655+ text "no pretty printer for pattern-matching do binding" :

1656+ ppdo bnd dos

1657+ ppdo _ [] = []

1637 prettySe p bnd (PCoerced t) = prettySe p bnd t

1658 prettySe p bnd (PCoerced t) = prettySe p bnd t

1638 prettySe p bnd (PElabError s) = pretty s

1659 prettySe p bnd (PElabError s) = pretty s

1639 -- Quasiquote pprinting ignores bound vars

1660 -- Quasiquote pprinting ignores bound vars

src/Idris/Delaborate.hs+32−6

@@ -26,23 +26,49 @@ import Debug.Trace

26bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

28-- | Re-add syntactic sugar in a term

29−resugar :: PTerm -> PTerm

29+resugar :: IState -> PTerm -> PTerm

30−resugar = transform resugarApp

30+resugar ist = transform flattenDoLet . transform resugarApp

31 where

32 resugarApp (PApp fc (PRef _ n) args)

33 | [c, t, f] <- mapMaybe explicitTerm args

34 , basename n == sUN "ifThenElse"

35 = PIfThenElse fc c (dedelay t) (dedelay f)

36+ resugarApp (PApp fc (PRef _ n) args)

37+ | [v, PLam _ bn _ _ next] <- mapMaybe explicitTerm args

38+ , basename n == sUN ">>="

39+ = let step = if bn `elem` namesIn [] ist next

40+ then DoBind fc bn NoFC v

41+ else DoExp NoFC v

42+ in case resugarApp next of

43+ PDoBlock dos -> PDoBlock (step : dos)

44+ expr -> PDoBlock [step, DoExp NoFC expr]

45+ resugarApp (PApp fc (PRef _ n) args)

46+ | [PConstant fc (BI i)] <- mapMaybe explicitTerm args

47+ , basename n == sUN "fromInteger"

48+ = PConstant fc (BI i)

36 resugarApp tm = tm

49 resugarApp tm = tm

50+

51+ flattenDoLet (PLet _ ln _ ty v bdy)

52+ | PDoBlock dos <- flattenDoLet bdy

53+ = PDoBlock (DoLet NoFC ln NoFC ty v : dos)

54+ flattenDoLet (PDoBlock dos) =

55+ PDoBlock $ concatMap fixExp dos

56+ where fixExp (DoExp _ (PLet _ ln _ ty v bdy)) =

57+ DoLet NoFC ln NoFC ty v : fixExp (DoExp NoFC bdy)

58+ fixExp d = [d]

59+ flattenDoLet tm = tm

60+

37 dedelay (PApp _ (PRef _ delay) [_, _, obj])

61 dedelay (PApp _ (PRef _ delay) [_, _, obj])

38 | delay == sUN "Delay" = getTm obj

62 | delay == sUN "Delay" = getTm obj

39 dedelay x = x

63 dedelay x = x

64+

40 explicitTerm (PExp {getTm = tm}) = Just tm

65 explicitTerm (PExp {getTm = tm}) = Just tm

41 explicitTerm _ = Nothing

66 explicitTerm _ = Nothing

68+

43-- | Delaborate and resugar a term

69-- | Delaborate and resugar a term

44delabSugared :: IState -> Term -> PTerm

70delabSugared :: IState -> Term -> PTerm

45−delabSugared ist tm = resugar $ delab ist tm

71+delabSugared ist tm = resugar ist $ delab ist tm

47-- | Delaborate a term without resugaring

73-- | Delaborate a term without resugaring

48delab :: IState -> Term -> PTerm

74delab :: IState -> Term -> PTerm

@@ -205,8 +231,8 @@ pprintDelabTy i n

205 = case lookupTy n (tt_ctxt i) of

231 = case lookupTy n (tt_ctxt i) of

206 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $

232 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $

207 case lookupCtxt n (idris_implicits i) of

233 case lookupCtxt n (idris_implicits i) of

208− (imps:_) -> resugar $ delabTy' i imps ty False False

234+ (imps:_) -> resugar i $ delabTy' i imps ty False False

209− _ -> resugar $ delabTy' i [] ty False False

235+ _ -> resugar i $ delabTy' i [] ty False False

210 [] -> error "pprintDelabTy got a name that doesn't exist"

236 [] -> error "pprintDelabTy got a name that doesn't exist"

211

237

212pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

238pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

@@ -564,7 +590,7 @@ fancifyAnnots ist meta annot@(AnnName n _ _ _) =

564 return (out "")

590 return (out "")

565 getTy :: IState -> Name -> String -- fails if name not already extant!

591 getTy :: IState -> Name -> String -- fails if name not already extant!

566 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

592 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

567− resugar $ delabTy ist n

593+ resugar ist $ delabTy ist n

568 in (displayS . renderPretty 1.0 50 $ theTy) ""

594 in (displayS . renderPretty 1.0 50 $ theTy) ""

569fancifyAnnots _ _ annot = annot

595fancifyAnnots _ _ annot = annot

570

596

test/error004/expected+1−2

@@ -5,5 +5,4 @@ When elaborating argument cons1 to function FunErrTest.cadr:

5FunErrTest.idr:38:10:

6When elaborating right hand side of badCadr2:

7When elaborating argument cons2 to function FunErrTest.cadr:

8− Could not prove that tail [(fromInteger 1)] has at least two

8+ Could not prove that tail [1] has at least two elements.

9− elements.