git.iko.soy/Idris-dev
on master help sign in
Resugaring for do and fromInteger
commit38123a426ed77aff22ddde3be64c38e20a867d4c authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 3 Jun 2015, 12:21 (11 years ago) parenta604143
4 files changed+58−9
compare with master
unifiedsplit
CHANGELOG+3 src/Idris/AbsSyntaxTree.hs+22−1 src/Idris/Delaborate.hs+32−6 test/error004/expected+1−2
CHANGELOG+3
@@ -3,6 +3,9 @@ New in 0.9.19:
33* The Show class has been moved into Prelude.Show and augmented with the method
44 showPrec, which allows correct parenthesization of showed terms. This comes
55 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
69
710New in 0.9.18:
811--------------
src/Idris/AbsSyntaxTree.hs+22−1
@@ -1633,7 +1633,28 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
16331633 prettySe p bnd (PReturn f) = kwd "return"
16341634 prettySe p bnd PImpossible = kwd "impossible"
16351635 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 _ [] = []
16371658 prettySe p bnd (PCoerced t) = prettySe p bnd t
16381659 prettySe p bnd (PElabError s) = pretty s
16391660 -- Quasiquote pprinting ignores bound vars
src/Idris/Delaborate.hs+32−6
@@ -26,23 +26,49 @@ import Debug.Trace
2626bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
2727
2828-- | Re-add syntactic sugar in a term
29−resugar :: PTerm -> PTerm
30−resugar = transform resugarApp
29+resugar :: IState -> PTerm -> PTerm
30+resugar ist = transform flattenDoLet . transform resugarApp
3131 where
3232 resugarApp (PApp fc (PRef _ n) args)
3333 | [c, t, f] <- mapMaybe explicitTerm args
3434 , basename n == sUN "ifThenElse"
3535 = 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)
3649 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+
3761 dedelay (PApp _ (PRef _ delay) [_, _, obj])
3862 | delay == sUN "Delay" = getTm obj
3963 dedelay x = x
64+
4065 explicitTerm (PExp {getTm = tm}) = Just tm
4166 explicitTerm _ = Nothing
4267
68+
4369-- | Delaborate and resugar a term
4470delabSugared :: IState -> Term -> PTerm
45−delabSugared ist tm = resugar $ delab ist tm
71+delabSugared ist tm = resugar ist $ delab ist tm
4672
4773-- | Delaborate a term without resugaring
4874delab :: IState -> Term -> PTerm
@@ -205,8 +231,8 @@ pprintDelabTy i n
205231 = case lookupTy n (tt_ctxt i) of
206232 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
207233 case lookupCtxt n (idris_implicits i) of
208− (imps:_) -> resugar $ delabTy' i imps ty False False
209− _ -> resugar $ delabTy' i [] ty False False
234+ (imps:_) -> resugar i $ delabTy' i imps ty False False
235+ _ -> resugar i $ delabTy' i [] ty False False
210236 [] -> error "pprintDelabTy got a name that doesn't exist"
211237
212238pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
@@ -564,7 +590,7 @@ fancifyAnnots ist meta annot@(AnnName n _ _ _) =
564590 return (out "")
565591 getTy :: IState -> Name -> String -- fails if name not already extant!
566592 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
567− resugar $ delabTy ist n
593+ resugar ist $ delabTy ist n
568594 in (displayS . renderPretty 1.0 50 $ theTy) ""
569595fancifyAnnots _ _ annot = annot
570596
test/error004/expected+1−2
@@ -5,5 +5,4 @@ When elaborating argument cons1 to function FunErrTest.cadr:
55FunErrTest.idr:38:10:
66When elaborating right hand side of badCadr2:
77When elaborating argument cons2 to function FunErrTest.cadr:
8− Could not prove that tail [(fromInteger 1)] has at least two
9− elements.
8+ Could not prove that tail [1] has at least two elements.